Pointer subtraction in back-end: no need for bounds checking

5b8028a added pointer validity checks in the back-end when
performing pointer minus pointer operations. Given our pointer encoding
it seems important to do a same-object test as, for distinct objects,
the object identifier part would start to play into the subtraction.
When operating on the same object, however, even out-of-bounds pointers'
subtraction should be indistinguishable from how this works on actual
hardware.

Therefore, this commit removes the bounds-checking part. (C semantics
have a pointer-validity requirement, and we catch this via checks
inserted in the front-end as the regression test demonstrates. We do not
need to catch this in the back-end.)

Author: tautschnig

regression/cbmc/Pointer_difference2/test.desc

@@ -5,11 +5,11 @@ main.c
 ^\[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.assertion.7\] line 26 end plus 2 is nondet: (UNKNOWN|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.assertion.8\] line 28 end plus 2 is nondet: (UNKNOWN|FAILURE)$
 ^\[main.pointer_arithmetic.\d+\] line 28 pointer relation: pointer outside object bounds in p: FAILURE$
-^\*\* 9 of \d+ failed
+^\*\* [789] of \d+ failed
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

src/solvers/flattening/bv_pointers.cpp

@@ -665,39 +665,8 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
           difference, element_size_bv, bv_utilst::representationt::SIGNED);
       }
 
-      // test for null object (integer constants)
-      const exprt null_object = ::null_object(minus_expr.lhs());
-      literalt in_bounds = convert(null_object);
-
-      if(!in_bounds.is_true())
-      {
-        // 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);
-
-        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 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));
-
-        in_bounds =
-          prop.lor(in_bounds, prop.land(lhs_in_bounds, rhs_in_bounds));
-      }
-
-      prop.l_set_to_true(prop.limplies(
-        prop.land(same_object_lit, in_bounds), bv_utils.equal(difference, bv)));
+      prop.l_set_to_true(
+        prop.limplies(same_object_lit, bv_utils.equal(difference, bv)));
     }
 
     return bv;