Support overflow plus/minus expressions over pointers

regression/cbmc/pointer-overflow3/no-simplify.desc

@@ -5,7 +5,9 @@ main.c
 ^\[main.pointer_arithmetic.\d+\] line 7 pointer arithmetic: pointer outside object bounds in p - \(signed (long (long )?)?int\)10: FAILURE
 ^\[main.pointer_arithmetic.\d+\] line 10 pointer arithmetic: pointer outside object bounds in arr \+ \(signed (long (long )?)?int\)10: FAILURE
 ^\[main.pointer_arithmetic.\d+\] line 11 pointer arithmetic: pointer outside object bounds in arr - \(signed (long (long )?)?int\)10: FAILURE
-^\*\* 4 of \d+ failed
+^\[main.overflow.\d+\] line 7 arithmetic overflow on pointer \- in p \- \(signed (long (long )?)?int\)10: FAILURE
+^\[main.overflow.\d+\] line 11 arithmetic overflow on pointer \- in arr \- \(signed (long (long )?)?int\)10: FAILURE
+^\*\* 6 of \d+ failed
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

regression/cbmc/pointer-overflow3/test.desc

@@ -5,7 +5,9 @@ main.c
 ^\[main.pointer_arithmetic.\d+\] line 7 pointer arithmetic: pointer outside object bounds in p - \(signed (long (long )?)?int\)10: FAILURE
 ^\[main.pointer_arithmetic.\d+\] line 10 pointer arithmetic: pointer outside object bounds in arr \+ \(signed (long (long )?)?int\)10: FAILURE
 ^\[main.pointer_arithmetic.\d+\] line 11 pointer arithmetic: pointer outside object bounds in arr - \(signed (long (long )?)?int\)10: FAILURE
-^\*\* 4 of \d+ failed
+^\[main.overflow.\d+\] line 7 arithmetic overflow on pointer \- in p \- \(signed (long (long )?)?int\)10: FAILURE
+^\[main.overflow.\d+\] line 11 arithmetic overflow on pointer \- in arr \- \(signed (long (long )?)?int\)10: FAILURE
+^\*\* 6 of \d+ failed
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

regression/cbmc/pointer-overflow4/test.desc

@@ -1,7 +1,7 @@
 CORE
 main.c
 --pointer-overflow-check
-^\[main.overflow.1\] line 10 arithmetic overflow on signed \* in (0x)?[0-9a-fA-F]+l* \* \(signed (long (long )?)?int\)4ul*: FAILURE$
+^\[main.overflow.1\] line 10 arithmetic overflow on pointer \+ in p \+ (0x)?[0-9a-fA-F]+l*: FAILURE$
 ^\*\* 1 of \d+ failed
 ^VERIFICATION FAILED$
 ^EXIT=10$

regression/contracts/no_redudant_checks/test.desc

@@ -23,7 +23,7 @@ main.c
 ^\[main.pointer_arithmetic.15\].*: SUCCESS
 ^\[main.pointer_arithmetic.16\].*: SUCCESS
 ^\[main.pointer_arithmetic.17\].*: SUCCESS
-^\*\* 0 of 20 failed \(1 iterations\)
+^\*\* 0 of 23 failed \(1 iterations\)
 ^VERIFICATION SUCCESSFUL$
 --
 ^\[main.overflow.\d+\].*: FAILURE
@@ -32,10 +32,10 @@ Checks that assertions generated by the first --pointer-overflow-check:
 - do not get duplicated by the second --unsigned-overflow-check
 - do not get instrumented with --unsigned-overflow-check (would fail the proof)
 
-We expect 20 assertions to be generated:
+We expect 23 assertions to be generated:
 In the goto-instrument run:
 - 2 for using malloc
-- 17 caused by --pointer-overflow-check
+- 20 caused by --pointer-overflow-check
 
 In the final cbmc run:
 - 0 caused by --pointer-overflow-check

src/ansi-c/goto_check_c.cpp

@@ -819,9 +819,6 @@ void goto_check_ct::integer_overflow_check(
   const exprt &expr,
   const guardt &guard)
 {
-  if(!enable_signed_overflow_check && !enable_unsigned_overflow_check)
-    return;
-
   // First, check type.
   const typet &type = expr.type();
 
@@ -831,6 +828,9 @@ void goto_check_ct::integer_overflow_check(
   if(type.id() == ID_unsignedbv && !enable_unsigned_overflow_check)
     return;
 
+  if(type.id() == ID_pointer && !enable_pointer_overflow_check)
+    return;
+
   // add overflow subgoal
 
   if(expr.id() == ID_div)
@@ -1021,7 +1021,10 @@ void goto_check_ct::integer_overflow_check(
         tmp.operands().resize(i);
       }
 
-      std::string kind = type.id() == ID_unsignedbv ? "unsigned" : "signed";
+      std::string kind =
+        type.id() == ID_pointer
+          ? "pointer"
+          : (type.id() == ID_unsignedbv ? "unsigned" : "signed");
 
       add_guarded_property(
         not_exprt{binary_overflow_exprt{tmp, expr.id(), expr.operands()[i]}},
@@ -1034,7 +1037,9 @@ void goto_check_ct::integer_overflow_check(
   }
   else if(expr.operands().size() == 2)
   {
-    std::string kind = type.id() == ID_unsignedbv ? "unsigned" : "signed";
+    std::string kind = type.id() == ID_pointer
+                         ? "pointer"
+                         : (type.id() == ID_unsignedbv ? "unsigned" : "signed");
 
     const binary_exprt &bexpr = to_binary_expr(expr);
     add_guarded_property(
@@ -1335,31 +1340,7 @@ void goto_check_ct::pointer_overflow_check(
     expr.operands().size() == 2,
     "pointer arithmetic expected to have exactly 2 operands");
 
-  // multiplying the offset by the object size must not result in arithmetic
-  // overflow
-  const typet &object_type = to_pointer_type(expr.type()).base_type();
-  if(object_type.id() != ID_empty)
-  {
-    auto size_of_expr_opt = size_of_expr(object_type, ns);
-    CHECK_RETURN(size_of_expr_opt.has_value());
-    exprt object_size = size_of_expr_opt.value();
-
-    const binary_exprt &binary_expr = to_binary_expr(expr);
-    exprt offset_operand = binary_expr.lhs().type().id() == ID_pointer
-                             ? binary_expr.rhs()
-                             : binary_expr.lhs();
-    mult_exprt mul{
-      offset_operand,
-      typecast_exprt::conditional_cast(object_size, offset_operand.type())};
-    mul.add_source_location() = offset_operand.source_location();
-
-    flag_overridet override_overflow(offset_operand.source_location());
-    override_overflow.set_flag(
-      enable_signed_overflow_check, true, "signed_overflow_check");
-    override_overflow.set_flag(
-      enable_unsigned_overflow_check, true, "unsigned_overflow_check");
-    integer_overflow_check(mul, guard);
-  }
+  integer_overflow_check(expr, guard);
 
   // the result must be within object bounds or one past the end
   const auto size = from_integer(0, size_type());

src/ansi-c/library/stdlib.c

@@ -449,6 +449,7 @@ inline char *getenv(const char *name)
   // the range.
 
   __CPROVER_assume(buf_size >= 1);
+  __CPROVER_assume((__CPROVER_size_t)buf_size <= __CPROVER_max_malloc_size);
   char *buffer = (char *)__CPROVER_allocate(buf_size * sizeof(char), 0);
   buffer[buf_size-1]=0;
 

src/solvers/flattening/bv_pointers.cpp

@@ -9,6 +9,7 @@ Author: Daniel Kroening, [email protected]
 #include "bv_pointers.h"
 
 #include <util/arith_tools.h>
+#include <util/bitvector_expr.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/config.h>
@@ -204,6 +205,79 @@ literalt bv_pointerst::convert_rest(const exprt &expr)
           bv_utilst::representationt::SIGNED));
     }
   }
+  else if(
+    (expr.id() == ID_overflow_plus || expr.id() == ID_overflow_minus) &&
+    operands.size() == 2 &&
+    (operands[0].type().id() == ID_pointer) !=
+      (operands[1].type().id() == ID_pointer))
+  {
+    // this has to be pointer plus/minus integer
+    const exprt &pointer_op =
+      operands[0].type().id() == ID_pointer ? operands[0] : operands[1];
+    const pointer_typet &pointer_type = to_pointer_type(pointer_op.type());
+    const typet &object_type = pointer_type.base_type();
+
+    const exprt &offset_op =
+      operands[0].type().id() == ID_pointer ? operands[1] : operands[0];
+    if(
+      offset_op.type().id() != ID_unsignedbv &&
+      offset_op.type().id() != ID_signedbv)
+    {
+      return SUB::convert_rest(expr);
+    }
+    exprt offset_bytes = offset_op;
+    literalt offset_overflow = const_literal(false);
+
+    // Arithmetic over void* is a gcc extension.
+    // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
+    if(object_type.id() != ID_empty)
+    {
+      auto object_size_opt = size_of_expr(object_type, ns);
+      CHECK_RETURN(object_size_opt.has_value());
+
+      offset_bytes = mult_exprt{
+        offset_op,
+        typecast_exprt::conditional_cast(*object_size_opt, offset_op.type())};
+
+      // multiplying the offset by the object size may result in arithmetic
+      // overflow
+      mult_overflow_exprt of{
+        to_mult_expr(offset_bytes).op0(), to_mult_expr(offset_bytes).op1()};
+      offset_overflow = convert(of);
+    }
+
+    const std::size_t full_width = pointer_type.get_width();
+
+    bv_utilst::representationt rep = offset_bytes.type().id() == ID_signedbv
+                                       ? bv_utilst::representationt::SIGNED
+                                       : bv_utilst::representationt::UNSIGNED;
+    bvt offset_bv = convert_bv(offset_bytes);
+    CHECK_RETURN(!offset_bv.empty());
+    offset_bv = bv_utils.extension(offset_bv, full_width, rep);
+    if(expr.id() == ID_overflow_minus)
+      offset_bv = bv_utils.negate(offset_bv);
+
+    bvt pointer_offset_bv = bv_utils.sign_extension(
+      offset_literals(convert_bv(pointer_op), pointer_type), full_width);
+
+    // add and determine (signed) overflow of this addition
+    bvt offset_sum = bv_utils.add(pointer_offset_bv, offset_bv);
+    literalt addition_overflow = prop.land(
+      prop.lequal(
+        bv_utils.sign_bit(pointer_offset_bv), bv_utils.sign_bit(offset_bv)),
+      prop.lxor(
+        bv_utils.sign_bit(offset_sum), bv_utils.sign_bit(pointer_offset_bv)));
+
+    // there is an overflow iff any of [offset width - 1 .. full_width - 1] bits
+    // are non-zero or there was an overflow in the addition or the earlier
+    // multiplication
+    const std::size_t offset_bits = get_offset_width(pointer_type);
+    CHECK_RETURN(offset_bits > 0);
+    offset_sum.erase(offset_sum.begin(), offset_sum.begin() + offset_bits - 1);
+    offset_sum.push_back(addition_overflow);
+    offset_sum.push_back(offset_overflow);
+    return prop.lor(offset_sum);
+  }
 
   return SUB::convert_rest(expr);
 }

src/solvers/smt2/smt2_conv.cpp

@@ -1878,7 +1878,52 @@ void smt2_convt::convert_expr(const exprt &expr)
     const typet &op_type = op0.type();
     std::size_t width=boolbv_width(op_type);
 
-    if(op_type.id()==ID_signedbv)
+    if(op0.type().id() == ID_pointer || op1.type().id() == ID_pointer)
+    {
+      exprt p = op0, i = op1;
+
+      if(p.type().id() != ID_pointer)
+        p.swap(i);
+
+      const auto &object_type = to_pointer_type(p.type()).base_type();
+      exprt offset_bytes = i;
+      exprt::operandst disjuncts;
+
+      // Arithmetic over void* is a gcc extension.
+      // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
+      if(object_type.id() != ID_empty)
+      {
+        auto object_size_opt = size_of_expr(object_type, ns);
+        CHECK_RETURN(object_size_opt.has_value());
+
+        offset_bytes = mult_exprt{
+          i, typecast_exprt::conditional_cast(*object_size_opt, i.type())};
+
+        // multiplying the offset by the object size may result in arithmetic
+        // overflow
+        disjuncts.push_back(mult_overflow_exprt{
+          to_mult_expr(offset_bytes).op0(), to_mult_expr(offset_bytes).op1()});
+      }
+
+      exprt pointer_offset_op = pointer_offset(p);
+      offset_bytes = typecast_exprt::conditional_cast(
+        offset_bytes, pointer_offset_op.type());
+
+      if(can_cast_expr<minus_overflow_exprt>(expr))
+        offset_bytes = unary_minus_exprt{offset_bytes};
+
+      disjuncts.push_back(plus_overflow_exprt{pointer_offset_op, offset_bytes});
+
+      plus_exprt sum{pointer_offset_op, offset_bytes};
+      exprt pointer_offset_sum = pointer_offset(typecast_exprt{sum, p.type()});
+
+      disjuncts.push_back(binary_relation_exprt{
+        pointer_offset_sum, ID_lt, from_integer(0, pointer_offset_sum.type())});
+      disjuncts.push_back(notequal_exprt{pointer_offset_sum, sum});
+
+      convert_expr(disjunction(disjuncts));
+    }
+    else if(op_type.id() == ID_signedbv)
     {
       // an overflow occurs if the top two bits of the extended sum differ
       out << "(let ((?sum (";
@@ -1894,8 +1939,7 @@ void smt2_convt::convert_expr(const exprt &expr)
                    "((_ extract " << (width-1) << " " << (width-1) << ") ?sum)";
       out << ")))"; // =, not, let
     }
-    else if(op_type.id()==ID_unsignedbv ||
-            op_type.id()==ID_pointer)
+    else if(op_type.id() == ID_unsignedbv)
     {
       // overflow is simply carry-out
       out << "(= ";