Support overflow plus/minus expressions over pointers

We did not specify that using overflow+/overflow- for pointer +/-
integer was unsupported. The translation via regular arithmetic
overflow, however, would produce results that did not take into account
the peculiarities of pointer arithmetic.

Fixing this now also makes it possible to take into account the
implementation details of the object/offset encoding, which would result
in overflows even when full-width addition/subtraction would not have
overflowed.

Fixes: #6842

Author: tautschnig

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$

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/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(sum);
+
+      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 << "(= ";