Add {binary,unary_overflow_exprt}

[tautschnig]

Create a dedicated exprt to construct overflow expressions for improved
type checking.

• Each commit message has a non-empty body, explaining why the change was made.
• Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[codecov]

Codecov Report

Merging #5897 (5f3a55d) into develop (81d075d) will increase coverage by 0.00%.
The diff coverage is 88.17%.

@@           Coverage Diff            @@
##           develop    #5897   +/-   ##
========================================
  Coverage    73.09%   73.10%           
========================================
  Files         1428     1428           
  Lines       155075   155102   +27     
========================================
+ Hits        113357   113388   +31     
+ Misses       41718    41714    -4     

Impacted Files	Coverage Δ
...java_bytecode/java_bytecode_internal_additions.cpp	100.00% <ø> (ø)
jbmc/src/java_bytecode/remove_exceptions.cpp	95.58% <ø> (ø)
...rams/remove_virtual_functions_without_fallback.cpp	98.52% <ø> (ø)
...s/variable-sensitivity/abstract_pointer_object.cpp	76.66% <ø> (ø)
src/ansi-c/c_nondet_symbol_factory.cpp	100.00% <ø> (ø)
src/cpp/cpp_is_pod.cpp	100.00% <ø> (ø)
src/cpp/cpp_type2name.cpp	89.13% <ø> (ø)
src/cpp/expr2cpp.cpp	40.24% <ø> (ø)
...to-instrument/accelerate/overflow_instrumenter.cpp	0.00% <0.00%> (ø)
src/goto-programs/xml_expr.cpp	53.98% <ø> (ø)
... and 19 more

---

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 94c64da...5f3a55d. Read the comment docs.

[martin-cs]

Yeah... this has the feel of "why didn't we always do it like this" which is a good sign.

I hate to be that person but ... what about divide? Specifically INT_MIN / -1.

[martin-cs]

This is not a request for this PR but more a general observation that this code seems to be not covered by the regression tests. I have a feeling that at one point Matt had tests for this code. Maybe @cristina-david could help?

[tautschnig]

We have regression/acceleration, it just seems the script in there needs some love to make this work. Adding this to my to-do list.

[martin-cs]

I'm also having horrible thoughts about what happens with signs when taking modulo. Is it possible to get an overflow with INT_{MAX,MIN} % INT_{MAX,MIN} ?

[tautschnig]

I'm also having horrible thoughts about what happens with signs when taking modulo. Is it possible to get an overflow with INT_{MAX,MIN} % INT_{MAX,MIN} ?

We do generate some of these checks in goto_checkt, though not using overflow_* expressions, but by specifically testing for boundary values. I think that's the right approach, but I do wonder whether we have the necessary coverage for floating-point operands for all of these...