Fix pointer subtraction semantics

regression/cbmc-library/posix_memalign-02/test.desc

@@ -6,6 +6,5 @@ main.c
 ^VERIFICATION FAILED$
 \[main.precondition_instance.1\] .* memcpy src/dst overlap: FAILURE
 \[main.precondition_instance.3\] .* memcpy destination region writeable: FAILURE
-\*\* 2 of 14 failed
 --
 ^warning: ignoring

regression/cbmc/Pointer_difference2/main.c

@@ -0,0 +1,31 @@
+int main()
+{
+  int array[4];
+  int other_array[2];
+
+  __CPROVER_assert(&array[0] - &array[2] == -2, "correct");
+
+  int diff = array - other_array;
+  _Bool nondet;
+  if(nondet)
+    __CPROVER_assert(diff != 42, "undefined behavior");
+  else
+    __CPROVER_assert(diff == 42, "undefined behavior");
+
+  __CPROVER_assert(
+    ((char *)(&array[3])) - ((char *)(&array[1])) == 2 * sizeof(int),
+    "casting works");
+
+  int *p = &array[3];
+  ++p;
+  __CPROVER_assert(p - &array[0] == 4, "end plus one works");
+  __CPROVER_assert(p - &array[0] != 3, "end plus one works");
+  ++p;
+  _Bool nondet_branch;
+  if(nondet_branch)
+    __CPROVER_assert(p - &array[0] == 5, "end plus 2 is nondet");
+  else
+    __CPROVER_assert(p - &array[0] != 5, "end plus 2 is nondet");
+
+  return 0;
+}

regression/cbmc/Pointer_difference2/test.desc

@@ -0,0 +1,18 @@
+CORE broken-smt-backend
+main.c
+--pointer-check
+^\[main.assertion.1\] line 6 correct: SUCCESS
+^\[main.pointer.1\] line 8 same object violation in array - other_array: FAILURE$
+^\[main.assertion.2\] line 11 undefined behavior: FAILURE$
+^\[main.assertion.3\] line 13 undefined behavior: FAILURE$
+^\[main.assertion.7\] line 26 end plus 2 is nondet: FAILURE$
+^\[main.pointer_arithmetic.\d+\] line 26 pointer relation: pointer outside object bounds in p: FAILURE$
+^\[main.assertion.8\] line 28 end plus 2 is nondet: FAILURE$
+^\[main.pointer_arithmetic.\d+\] line 28 pointer relation: pointer outside object bounds in p: FAILURE$
+^\*\* 7 of \d+ failed
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$

regression/cbmc/void_pointer3/main.c

@@ -2,14 +2,14 @@
 
 int main()
 {
-  // make sure they are NULL objects
-  void *p=0, *q=0;
+  int array[1 << (sizeof(unsigned char) * 8)];
+
+  void *p = array, *q = array;
   // with the object:offset encoding we need to make sure the address arithmetic
   // below will only touch the offset part
   __CPROVER_assume(sizeof(unsigned char)<sizeof(void*));
   unsigned char o1, o2;
-  // there is ample undefined behaviour here, but the goal of this test solely
-  // is exercising CBMC's pointer subtraction encoding
+
   p+=o1;
   q+=o2;
 

src/analyses/goto_check.cpp

@@ -178,7 +178,7 @@ class goto_checkt
   void mod_overflow_check(const mod_exprt &, const guardt &);
   void enum_range_check(const exprt &, const guardt &);
   void undefined_shift_check(const shift_exprt &, const guardt &);
-  void pointer_rel_check(const binary_relation_exprt &, const guardt &);
+  void pointer_rel_check(const binary_exprt &, const guardt &);
   void pointer_overflow_check(const exprt &, const guardt &);
 
   /// Generates VCCs for the validity of the given dereferencing operation.
@@ -1117,7 +1117,7 @@ void goto_checkt::nan_check(
 }
 
 void goto_checkt::pointer_rel_check(
-  const binary_relation_exprt &expr,
+  const binary_exprt &expr,
   const guardt &guard)
 {
   if(!enable_pointer_check)
@@ -1128,17 +1128,33 @@ void goto_checkt::pointer_rel_check(
   {
     // add same-object subgoal
 
-    if(enable_pointer_check)
+    exprt same_object = ::same_object(expr.op0(), expr.op1());
+
+    add_guarded_property(
+      same_object,
+      "same object violation",
+      "pointer",
+      expr.find_source_location(),
+      expr,
+      guard);
+
+    for(const auto &pointer : expr.operands())
     {
-      exprt same_object=::same_object(expr.op0(), expr.op1());
+      // just this particular byte must be within object bounds or one past the
+      // end
+      const auto size = from_integer(0, size_type());
+      auto conditions = get_pointer_dereferenceable_conditions(pointer, size);
 
-      add_guarded_property(
-        same_object,
-        "same object violation",
-        "pointer",
-        expr.find_source_location(),
-        expr,
-        guard);
+      for(const auto &c : conditions)
+      {
+        add_guarded_property(
+          c.assertion,
+          "pointer relation: " + c.description,
+          "pointer arithmetic",
+          expr.find_source_location(),
+          pointer,
+          guard);
+      }
     }
   }
 }
@@ -1650,6 +1666,14 @@ void goto_checkt::check_rec_arithmetic_op(const exprt &expr, guardt &guard)
   if(expr.type().id() == ID_signedbv || expr.type().id() == ID_unsignedbv)
   {
     integer_overflow_check(expr, guard);
+
+    if(
+      expr.operands().size() == 2 && expr.id() == ID_minus &&
+      expr.operands()[0].type().id() == ID_pointer &&
+      expr.operands()[1].type().id() == ID_pointer)
+    {
+      pointer_rel_check(to_binary_expr(expr), guard);
+    }
   }
   else if(expr.type().id() == ID_floatbv)
   {

src/solvers/flattening/bv_pointers.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/exception_utils.h>
 #include <util/pointer_expr.h>
 #include <util/pointer_offset_size.h>
+#include <util/pointer_predicates.h>
 
 /// Map bytes according to the configured endianness. The key difference to
 /// endianness_mapt is that bv_endianness_mapt is aware of the bit-level
@@ -555,43 +556,82 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
 
   if(is_pointer_subtraction(expr))
   {
-    // pointer minus pointer
-    const auto &minus_expr = to_minus_expr(expr);
-    bvt lhs = convert_bv(minus_expr.lhs());
-    bvt rhs = convert_bv(minus_expr.rhs());
-
     std::size_t width=boolbv_width(expr.type());
 
     if(width==0)
       return conversion_failed(expr);
 
-    // we do a zero extension
-    lhs = bv_utils.zero_extension(lhs, width);
-    rhs = bv_utils.zero_extension(rhs, width);
+    // pointer minus pointer is subtraction over the offset divided by element
+    // size, iff the pointers point to the same object
+    const auto &minus_expr = to_minus_expr(expr);
 
-    bvt bv = bv_utils.sub(lhs, rhs);
+    // do the same-object-test via an expression as this may permit re-using
+    // already cached encodings of the equality test
+    const exprt same_object = ::same_object(minus_expr.lhs(), minus_expr.rhs());
+    const bvt &same_object_bv = convert_bv(same_object);
+    CHECK_RETURN(same_object_bv.size() == 1);
 
-    typet pointer_sub_type = minus_expr.lhs().type().subtype();
-    mp_integer element_size;
+    // compute the object size (again, possibly using cached results)
+    const exprt object_size = ::object_size(minus_expr.lhs());
+    const bvt object_size_bv =
+      bv_utils.zero_extension(convert_bv(object_size), width);
 
-    if(pointer_sub_type.id()==ID_empty)
+    bvt bv;
+    bv.reserve(width);
+
+    for(std::size_t i = 0; i < width; ++i)
+      bv.push_back(prop.new_variable());
+
+    if(!same_object_bv[0].is_false())
     {
-      // This is a gcc extension.
+      const pointer_typet &lhs_pt = to_pointer_type(minus_expr.lhs().type());
+      const bvt &lhs = convert_bv(minus_expr.lhs());
+      const bvt lhs_offset =
+        bv_utils.sign_extension(offset_literals(lhs, lhs_pt), width);
+
+      const literalt lhs_in_bounds = prop.land(
+        !bv_utils.sign_bit(lhs_offset),
+        bv_utils.rel(
+          lhs_offset,
+          ID_le,
+          object_size_bv,
+          bv_utilst::representationt::UNSIGNED));
+
+      const pointer_typet &rhs_pt = to_pointer_type(minus_expr.rhs().type());
+      const bvt &rhs = convert_bv(minus_expr.rhs());
+      const bvt rhs_offset =
+        bv_utils.sign_extension(offset_literals(rhs, rhs_pt), width);
+
+      const literalt rhs_in_bounds = prop.land(
+        !bv_utils.sign_bit(rhs_offset),
+        bv_utils.rel(
+          rhs_offset,
+          ID_le,
+          object_size_bv,
+          bv_utilst::representationt::UNSIGNED));
+
+      bvt difference = bv_utils.sub(lhs_offset, rhs_offset);
+
+      // Support for void* is a gcc extension, with the size treated as 1 byte
+      // (no division required below).
       // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
-      element_size = 1;
-    }
-    else
-    {
-      auto element_size_opt = pointer_offset_size(pointer_sub_type, ns);
-      CHECK_RETURN(element_size_opt.has_value() && *element_size_opt > 0);
-      element_size = *element_size_opt;
-    }
+      if(lhs_pt.subtype().id() != ID_empty)
+      {
+        auto element_size_opt = pointer_offset_size(lhs_pt.subtype(), ns);
+        CHECK_RETURN(element_size_opt.has_value() && *element_size_opt > 0);
 
-    if(element_size != 1)
-    {
-      bvt element_size_bv = bv_utils.build_constant(element_size, bv.size());
-      bv=bv_utils.divider(
-        bv, element_size_bv, bv_utilst::representationt::SIGNED);
+        if(*element_size_opt != 1)
+        {
+          bvt element_size_bv =
+            bv_utils.build_constant(*element_size_opt, width);
+          difference = bv_utils.divider(
+            difference, element_size_bv, bv_utilst::representationt::SIGNED);
+        }
+      }
+
+      prop.l_set_to_true(prop.limplies(
+        prop.land(same_object_bv[0], prop.land(lhs_in_bounds, rhs_in_bounds)),
+        bv_utils.equal(difference, bv)));
     }
 
     return bv;
@@ -794,11 +834,11 @@ bvt bv_pointerst::offset_arithmetic(
   else
   {
     bvt bv_factor=bv_utils.build_constant(factor, index.size());
-    bv_index=bv_utils.unsigned_multiplier(index, bv_factor);
+    bv_index = bv_utils.signed_multiplier(index, bv_factor);
   }
 
   const std::size_t offset_bits = bv_pointers_width.get_offset_width(type);
-  bv_index = bv_utils.zero_extension(bv_index, offset_bits);
+  bv_index = bv_utils.sign_extension(bv_index, offset_bits);
 
   bvt offset_bv = offset_literals(bv, type);