Make overflow expressions available in C/C++ language front-ends

This enables testing for arithmetic overflow without generating an
arithmetic overflow.

Author: tautschnig

doc/cprover-manual/api.md

@@ -112,6 +112,22 @@ float __CPROVER_fabsf(float x);
 
 These functions return the absolute value of the given argument.
 
+#### \_\_CPROVER\_overflow\_minus, \_\_CPROVER\_overflow\_mult, \_\_CPROVER\_overflow\_plus, \_\_CPROVER\_overflow\_shl, \_\_CPROVER\_overflow\_unary\_minus
+
+```C
+__CPROVER_bool __CPROVER_overflow_minus();
+__CPROVER_bool __CPROVER_overflow_mult();
+__CPROVER_bool __CPROVER_overflow_plus();
+__CPROVER_bool __CPROVER_overflow_shl();
+__CPROVER_bool __CPROVER_overflow_unary_minus();
+```
+
+These functions take two (`__CPROVER_overflow_unary_minus` only takes one)
+arguments of any numeric type. They return true, if, and only if, the named
+operation would overflow when applied to the arguments. For example,
+`__CPROVER_overflow_plus(x, y)` returns true if `x + y` would result in an
+arithmetic overflow.
+
 #### \_\_CPROVER\_array\_equal, \_\_CPROVER\_array\_copy, \_\_CPROVER\_array\_set
 
 ```C

src/ansi-c/c_typecheck_expr.cpp

@@ -2811,6 +2811,46 @@ exprt c_typecheck_baset::do_special_functions(
 
     return expr;
   }
+  else if(
+    identifier == CPROVER_PREFIX "overflow_minus" ||
+    identifier == CPROVER_PREFIX "overflow_mult" ||
+    identifier == CPROVER_PREFIX "overflow_plus" ||
+    identifier == CPROVER_PREFIX "overflow_shl" ||
+    identifier == CPROVER_PREFIX "overflow_unary_minus")
+  {
+    exprt overflow{identifier, typet{}, exprt::operandst{expr.arguments()}};
+    overflow.add_source_location() = f_op.source_location();
+
+    if(identifier == CPROVER_PREFIX "overflow_minus")
+    {
+      overflow.id(ID_minus);
+      typecheck_expr_binary_arithmetic(overflow);
+    }
+    else if(identifier == CPROVER_PREFIX "overflow_mult")
+    {
+      overflow.id(ID_mult);
+      typecheck_expr_binary_arithmetic(overflow);
+    }
+    else if(identifier == CPROVER_PREFIX "overflow_plus")
+    {
+      overflow.id(ID_plus);
+      typecheck_expr_binary_arithmetic(overflow);
+    }
+    else if(identifier == CPROVER_PREFIX "overflow_shl")
+    {
+      overflow.id(ID_shl);
+      typecheck_expr_shifts(to_shift_expr(overflow));
+    }
+    else if(identifier == CPROVER_PREFIX "overflow_unary_minus")
+    {
+      overflow.id(ID_unary_minus);
+      typecheck_expr_unary_arithmetic(overflow);
+    }
+
+    overflow.id("overflow-" + overflow.id_string());
+    overflow.type() = bool_typet{};
+    return overflow;
+  }
   else
     return nil_exprt();
 }

src/ansi-c/cprover_builtin_headers.h

@@ -98,3 +98,9 @@ void __CPROVER_k_induction_hint(unsigned min, unsigned max,
 // format string-related
 int __CPROVER_scanf(const char *, ...);
 
+// detect overflow
+__CPROVER_bool __CPROVER_overflow_minus();
+__CPROVER_bool __CPROVER_overflow_mult();
+__CPROVER_bool __CPROVER_overflow_plus();
+__CPROVER_bool __CPROVER_overflow_shl();
+__CPROVER_bool __CPROVER_overflow_unary_minus();

src/ansi-c/expr2c.cpp

@@ -3793,11 +3793,13 @@ std::string expr2ct::convert_with_precedence(
   else if(src.id()==ID_cond)
     return convert_cond(src, precedence);
 
-  else if(src.id()==ID_overflow_unary_minus ||
-      src.id()==ID_overflow_minus ||
-      src.id()==ID_overflow_mult ||
-      src.id()==ID_overflow_plus)
+  else if(
+    src.id() == ID_overflow_unary_minus || src.id() == ID_overflow_minus ||
+    src.id() == ID_overflow_mult || src.id() == ID_overflow_plus ||
+    src.id() == ID_overflow_shl)
+  {
     return convert_overflow(src, precedence);
+  }
 
   else if(src.id()==ID_unknown)
     return "*";

src/ansi-c/library/cprover.h

@@ -150,4 +150,16 @@ __CPROVER_bool __CPROVER_get_may(const void *, const char *);
 #define __CPROVER_danger_number_of_vars 1
 #define __CPROVER_danger_number_of_consts 1
 
+// detect overflow
+// NOLINTNEXTLINE(build/deprecated)
+__CPROVER_bool __CPROVER_overflow_minus();
+// NOLINTNEXTLINE(build/deprecated)
+__CPROVER_bool __CPROVER_overflow_mult();
+// NOLINTNEXTLINE(build/deprecated)
+__CPROVER_bool __CPROVER_overflow_plus();
+// NOLINTNEXTLINE(build/deprecated)
+__CPROVER_bool __CPROVER_overflow_shl();
+// NOLINTNEXTLINE(build/deprecated)
+__CPROVER_bool __CPROVER_overflow_unary_minus();
+
 #endif // CPROVER_ANSI_C_LIBRARY_CPROVER_H