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

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.

Author: tautschnig

regression/cbmc/gcc_builtin_add_overflow/main.c

@@ -110,6 +110,15 @@ void check_generic(void)
   assert(0 && "reachability");
 }
 
+void check_non_const()
+{
+  int a, b, c, d, r;
+  // this may overflow (negated assertion fails)
+  assert(!__builtin_add_overflow(a, b, &r));
+  // but need not overflow (assertion fails)
+  assert(__builtin_add_overflow(c, d, &c));
+}
+
 int main(void)
 {
   check_int();
@@ -119,4 +128,5 @@ int main(void)
   check_unsigned_long();
   check_unsigned_long_long();
   check_generic();
+  check_non_const();
 }

regression/cbmc/gcc_builtin_add_overflow/test.desc

@@ -57,6 +57,8 @@ main.c
 \[check_generic.assertion.9\] line \d+ assertion big_result == 2ll \* .*: SUCCESS
 \[check_generic.assertion.10\] line \d+ assertion __builtin_add_overflow\(.* / 2 \+ 1, .*/ 2 \+ 1, &big_result\): SUCCESS
 \[check_generic.assertion.11\] line \d+ assertion 0 && "reachability": FAILURE
+\[check_non_const\.assertion\.1\] line \d+ assertion !__builtin_add_overflow\(a, b, &r\): FAILURE
+\[check_non_const\.assertion\.2\] line \d+ assertion __builtin_add_overflow\(c, d, &c\): FAILURE
 VERIFICATION FAILED
 ^EXIT=10$
 ^SIGNAL=0$

src/ansi-c/c_typecheck_expr.cpp

@@ -19,6 +19,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/cprover_prefix.h>
 #include <util/expr_util.h>
 #include <util/floatbv_expr.h>
+#include <util/fresh_symbol.h>
 #include <util/ieee_float.h>
 #include <util/mathematical_expr.h>
 #include <util/mathematical_types.h>
@@ -3014,48 +3015,85 @@ exprt c_typecheck_baset::do_special_functions(
       }
     }
 
-    // actual logic implementing the operators
+    // actual logic implementing the operators: perform operations on signed
+    // bitvector types of sufficiently large size to hold the result
     auto const make_operation = [&identifier](exprt lhs, exprt rhs) -> exprt {
+      std::size_t lhs_ssize = to_bitvector_type(lhs.type()).get_width();
+      if(lhs.type().id() == ID_unsignedbv)
+        ++lhs_ssize;
+      std::size_t rhs_ssize = to_bitvector_type(rhs.type()).get_width();
+      if(rhs.type().id() == ID_unsignedbv)
+        ++rhs_ssize;
+
       if(identifier == "__builtin_add_overflow")
       {
-        return plus_exprt{lhs, rhs};
+        std::size_t ssize = std::max(lhs_ssize, rhs_ssize) + 1;
+        integer_bitvector_typet ssize_type{ID_signedbv, ssize};
+        return plus_exprt{typecast_exprt{lhs, ssize_type},
+                          typecast_exprt{rhs, ssize_type}};
       }
       else if(identifier == "__builtin_sub_overflow")
       {
-        return minus_exprt{lhs, rhs};
+        std::size_t ssize = std::max(lhs_ssize, rhs_ssize) + 1;
+        integer_bitvector_typet ssize_type{ID_signedbv, ssize};
+        return minus_exprt{typecast_exprt{lhs, ssize_type},
+                           typecast_exprt{rhs, ssize_type}};
       }
       else
       {
         INVARIANT(
           identifier == "__builtin_mul_overflow",
           "the three overflow operations are add, sub and mul");
-        return mult_exprt{lhs, rhs};
+        std::size_t ssize = lhs_ssize + rhs_ssize;
+        integer_bitvector_typet ssize_type{ID_signedbv, ssize};
+        return mult_exprt{typecast_exprt{lhs, ssize_type},
+                          typecast_exprt{rhs, ssize_type}};
       }
     };
 
-    // we’re basically generating this expression
-    // (*result = (result_type)((integer)lhs OP (integer)rhs)),
-    //   ((integer)result == (integer)lhs OP (integer)rhs)
-    // i.e. perform the operation (+, -, *) on arbitrary length integer,
-    // cast to result type, check if the casted result is still equivalent
-    // to the arbitrary length result.
-    auto operation = make_operation(
-      typecast_exprt{lhs, integer_typet{}},
-      typecast_exprt{rhs, integer_typet{}});
-
-    auto operation_result =
-      typecast_exprt{operation, result_ptr.type().subtype()};
-    typecheck_expr_typecast(operation_result);
-    auto overflow_check = notequal_exprt{
-      typecast_exprt{dereference_exprt{result_ptr}, integer_typet{}},
-      operation};
-    typecheck_expr(overflow_check);
-    return exprt{ID_comma,
-                 bool_typet{},
-                 {side_effect_expr_assignt{dereference_exprt{result_ptr},
-                                           operation_result,
-                                           expr.source_location()},
-                  overflow_check}};
+    // Generating the following statement expression:
+    // ({ large_signedbv tmp = (large_signedbv)lhs OP (large_signedbv)rhs;
+    //    *result = (result_type)large_signedbv;
+    //    (large_signedbv)*result != tmp; })
+    // This performs the operation (+, -, *) on a signed bitvector type of
+    // sufficiently large width to store the precise result, cast to result
+    // type, check if the casted result is not equivalent to the full-length
+    // result.
+    auto operation = make_operation(lhs, rhs);
+    // Disable overflow checks as the operation cannot overflow on the larger
+    // type
+    operation.add_source_location() = expr.source_location();
+    operation.add_source_location().add_pragma("disable:signed-overflow-check");
+
+    const symbolt &new_symbol = get_fresh_aux_symbol(
+      operation.type(),
+      id2string(current_symbol.name) + "$tmp",
+      id2string(current_symbol.base_name) + "$tmp",
+      expr.source_location(),
+      mode,
+      symbol_table);
+
+    code_declt decl{new_symbol.symbol_expr()};
+    decl.add_source_location() = expr.source_location();
+
+    code_assignt tmp_assignment{decl.symbol(), operation};
+    tmp_assignment.add_source_location() = expr.source_location();
+
+    const auto &result_type = to_pointer_type(result_ptr.type()).subtype();
+    code_assignt result_assignment{dereference_exprt{result_ptr},
+                                   typecast_exprt{decl.symbol(), result_type}};
+    result_assignment.add_source_location() = expr.source_location();
+
+    notequal_exprt overflow_check{
+      typecast_exprt{dereference_exprt{result_ptr}, operation.type()},
+      decl.symbol()};
+    overflow_check.add_source_location() = expr.source_location();
+    code_expressiont return_expr{overflow_check};
+
+    code_blockt statements{
+      {decl, tmp_assignment, result_assignment, return_expr}};
+    return side_effect_expr_statement_expressiont{
+      statements, overflow_check.type(), expr.source_location()};
   }
   else
     return nil_exprt();