Use bitvector types to implement __builtin_{add,sub,mul}_overflow

[tautschnig]

The use of mathematical integers is not supported by the SAT back-end.
Although GCC's specification describes the operations over mathematical
integers, the same precision can be achieved by using bitvector types of
sufficient width.

The implementation now also introduces a fresh symbol to store the
result of the full-precision operation. This ensures that the arguments
to _builtin{add,sub,mul}_overflow are evaluated exactly once.

• Each commit message has a non-empty body, explaining why the change was made.
• n/a 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 #5544 (e789c67) into develop (95e1161) will increase coverage by 0.00%.
The diff coverage is 77.23%.

@@            Coverage Diff            @@
##           develop    #5544    +/-   ##
=========================================
  Coverage    75.02%   75.02%            
=========================================
  Files         1431     1433     +2     
  Lines       155595   155785   +190     
=========================================
+ Hits        116734   116877   +143     
- Misses       38861    38908    +47     

Impacted Files	Coverage Δ
src/ansi-c/c_typecheck_base.h	100.00% <ø> (ø)
src/goto-programs/goto_convert_class.h	87.30% <ø> (ø)
...rc/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp	76.58% <45.07%> (-4.36%)	⬇️
src/ansi-c/c_typecheck_expr.cpp	75.12% <78.37%> (-0.17%)	⬇️
src/goto-programs/goto_convert_side_effect.cpp	93.45% <94.73%> (+0.22%)	⬆️
src/ansi-c/c_expr.cpp	96.55% <96.55%> (ø)
src/ansi-c/c_expr.h	100.00% <100.00%> (ø)
src/util/expr.cpp	75.73% <0.00%> (-0.74%)	⬇️
src/util/simplify_expr.cpp	84.49% <0.00%> (-0.57%)	⬇️
... and 3 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 390f5c2...e789c67. Read the comment docs.

[kroening]

Note that we've got expressions ID_overflow_plus, ID_overflow_minus and ID_overflow_mult -- these make attempts at optimizing the encoding required for these predicates.

[tautschnig]

Note that we've got expressions ID_overflow_plus, ID_overflow_minus and ID_overflow_mult -- these make attempts at optimizing the encoding required for these predicates.

I am well aware of those, and did wonder whether we can just use them instead of making a big fuzz here. My concern was twofold, and I'd appreciate further thoughts on this:

1. What type should be used for the operands? __builtin_{add,sub,mul}_overflow permit using three different types.
2. __builtin_{add,sub,mul}_overflow require computing/storing the result, not just performing the overflow check. Thus, preferably, the actual arithmetic operation should only be done once.

[kroening]

1. ID_overflow_{plus, minus, mult} support the three types needed for __builtin_{add,sub,mul}_overflow.

2. There is a bit of savings potential when doing the overflow check for multiplication given the way it's implemented now. No significant savings when doing plus/minus. There is the option to do something iterative:

https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/z3prefix.pdf

[tautschnig]

ID_overflow_{plus, minus, mult} support the three types needed for __builtin_{add,sub,mul}_overflow.

Where would that be supported? boolbvt::convert_overflow appears to assume that the two operands have the same type.

[kroening]

https://gcc.gnu.org/onlinedocs/gcc/Integer-Overflow-Builtins.html appears to suggest that the two operands do indeed have the same type.

[tautschnig]

https://gcc.gnu.org/onlinedocs/gcc/Integer-Overflow-Builtins.html appears to suggest that the two operands do indeed have the same type.

I'm not sure I can see this? The signature bool __builtin_add_overflow (type1 a, type2 b, type3 *res) doesn't seem to require this? The comment also says "The first built-in function allows arbitrary integral types for operands and the result type must be pointer to some integral type other than enumerated or boolean type, [...]"