Add generic gcc overflow builtins

[hannes-steffenhagen-diffblue]

GCC has builtin operators __builtin_add_overflow, __builtin_sub_overflow
and __builtin_mul_overflow that perform an arithmetic operation and
check for overflow at the same time. This adds support for these
operators.

• 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.
• 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).
• My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[codecov-io]

Codecov Report

Merging #5249 into develop will increase coverage by <.01%.
The diff coverage is 75.55%.

@@             Coverage Diff             @@
##           develop    #5249      +/-   ##
===========================================
+ Coverage    67.42%   67.43%   +<.01%     
===========================================
  Files         1162     1162              
  Lines        95637    95682      +45     
===========================================
+ Hits         64484    64522      +38     
- Misses       31153    31160       +7

Flag	Coverage Δ
#cproversmt2	42.6% <75.55%> (+0.02%)	⬆️
#regression	63.96% <75.55%> (ø)	⬆️
#unit	31.88% <6.66%> (-0.02%)	⬇️

Impacted Files	Coverage Δ
src/ansi-c/c_typecheck_expr.cpp	74.08% <75.55%> (-0.19%)	⬇️
src/util/simplify_expr.cpp	88.12% <0%> (+0.6%)	⬆️
src/util/expr.cpp	68.59% <0%> (+0.82%)	⬆️

---

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 cd2c65b...af7acf9. Read the comment docs.

[hannes-steffenhagen-diffblue]

I had considered replacing the implementation of the non-generic __builtin_*_overflow in math.c with these, but unfortunately this runs afoul of the library check script in some configurations (for example, on travis we run library check against gcc 4.9, which doesn’t have these operators as they were added for gcc 5).

[NlightNFotis]

LGTM

[chrisr-diffblue]

Trying to do this in a single loop makes this a little complex to read. Would it be better to handle the argument type-check (seeing as their are only 3 args) as two separate blocks, one block to check arg 0 and 1, and one to check arg 2, with each block setting the arg_has_correct_type flag, then the error message block could stay the same (but not be in a loop).

[hannes-steffenhagen-diffblue]

Hm, maybe? Could you sketch out how you’d do it?

[chrisr-diffblue]

Sorry, yeah, some pseudo code would have been better :-)

bool correct_type=true;
// Typecheck args 0 and 1
for(int i = 0; i<1; i++) {
   correct_type &= is_correct_type(arg[i])
}
// Typecheck arg 2
correct_type &= is_correct_result_type(arg[2]);

// Error message if typecheck fails
if(!correct_type) {
 // user error message here
}

[chrisr-diffblue]

So basically the same logic you have, but without the tertiary operator which you effectively use to encode additional state in the argument index :-)

[chrisr-diffblue]

Oh, and I think you may be able to use the existing utility functions is_signed_or_unsigned_bitvector, is_c_integral_type and is_c_integral_pointer_type here too ?

[hannes-steffenhagen-diffblue]

I didn’t know about these, I’ll see about clarifying it using your suggestions.

[chrisr-diffblue]

Looks good - couple of queries around code structure (but not necessarily blockers). It might also be nice if some of the test cases also explored the case where arg 0 and arg 1 are not the same type... As far as I can tell from GCC docs, those first two arguments can be arbitrary (different) integral types, whereas I think all the test cases here use the same type for both arguments. I think everything will work fine if they are different, but would be nice to have one or two test cases that show that :-)

[chrisr-diffblue]

GCC docs show: (type1 a, type2 b, type3 *res) - implying a, b and res can all be different integral types, so might be worth writing this as (integral1, integral2, integral3 *) ? What does gcc give as an error message in this case?

[hannes-steffenhagen-diffblue]

Version dependent I suppose. gcc 10 says

test.c:4:46: error: argument 2 in call to function ‘__builtin_sub_overflow’ does not have integral type

I was kind of inspired by C++ concept syntax for this, but if you think it’s confusing I can change it to something else.

[chrisr-diffblue]

Well, I prefer what you have than what GCC has :-) No big deal.