From 4a92bfcc3278b38f69b99cf21bc3a7dc382e42a5 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 6 Nov 2024 21:39:59 +0000
Subject: [PATCH] Pointer subtraction in back-end: no need for bounds checking

5b8028a8a54 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.)
---
 regression/cbmc/Pointer_difference2/test.desc |  4 +--
 src/solvers/flattening/bv_pointers.cpp        | 35 ++-----------------
 2 files changed, 4 insertions(+), 35 deletions(-)

diff --git a/regression/cbmc/Pointer_difference2/test.desc b/regression/cbmc/Pointer_difference2/test.desc
index 9d993bd4dd6..08934f041f2 100644
--- a/regression/cbmc/Pointer_difference2/test.desc
+++ b/regression/cbmc/Pointer_difference2/test.desc
@@ -5,9 +5,9 @@ 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
 ^VERIFICATION FAILED$
diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp
index 931ad4a0634..b52c0da27f9 100644
--- a/src/solvers/flattening/bv_pointers.cpp
+++ b/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;