Simplify overflow-* expressions

[tautschnig]

We can simplify these over constants and for some trivial cases when
mathematical types are used.

• 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.

[martin-cs]

Useful for #5841

[TGWDB]

Maybe we should also have:
__CPROVER_assert(__CPROVER_overflow_minus(0U, 2U), "");
To check the case below where a 0 value can still have overflow?

[martin-cs]

If so, it should probably be in a separate test case as the trick @tautschnig is using for testing that it is simplification that handles these will not work for false things.

while (__CPROVER_overflow_minus(0U, 2U) {}

could do something interesting though...

[tautschnig]

Trying to cover this in the test spec: ^Generated 7 VCC\(s\), 0 remaining after simplification$

[kroening]

I would say that this is both frail and also obscure.
How about using __builtin_constant_p?

[tautschnig]

Fair. I'm now using _Static_assert instead.

[kroening]

The #ifdef _MSC_VER suggests that the test might work with goto-cl?

[tautschnig]

Ah, thank you, that was a left-over from when I thought about the __builtin_constant_p approach. Fixed.

[codecov]

Codecov Report

Merging #5872 (e6943df) into develop (42896e7) will increase coverage by 0.00%.
The diff coverage is 84.36%.

@@            Coverage Diff            @@
##           develop    #5872    +/-   ##
=========================================
  Coverage    72.90%   72.91%            
=========================================
  Files         1423     1425     +2     
  Lines       154159   154272   +113     
=========================================
+ Hits        112397   112481    +84     
- Misses       41762    41791    +29     

Impacted Files	Coverage Δ
...yses/variable-sensitivity/abstract_environment.cpp	87.42% <ø> (ø)
...ble-sensitivity/constant_pointer_abstract_object.h	100.00% <ø> (ø)
...sensitivity/variable_sensitivity_configuration.cpp	70.37% <0.00%> (ø)
...e-sensitivity/variable_sensitivity_configuration.h	100.00% <ø> (ø)
...riable-sensitivity/variable_sensitivity_domain.cpp	87.11% <ø> (ø)
...-sensitivity/variable_sensitivity_object_factory.h	100.00% <ø> (ø)
src/util/simplify_expr_class.h	100.00% <ø> (ø)
...e-sensitivity/constant_pointer_abstract_object.cpp	86.51% <66.66%> (ø)
...s/variable-sensitivity/abstract_pointer_object.cpp	76.66% <70.00%> (ø)
...-sensitivity/value_set_pointer_abstract_object.cpp	78.82% <80.72%> (+18.82%)	⬆️
... and 16 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 b26d347...e6943df. Read the comment docs.