Fix pointer subtraction over integer constants

633875b replaced the simplification of `p - p` to zero, which
previously was the only code to correctly evaluate to zero expressions
like `(char *)n - (char *)n` for some integer `n` when using the SAT
back-end: 5b8028a removed such support from the propositional
back-end, as bounds-checking over the null object would have deemed each
of the pointers out-of-bounds.

Author: tautschnig

regression/cbmc/Pointer_difference1/main.c

@@ -8,5 +8,11 @@ int main()
   unsigned int diff2 = &arrayOfInt [1] - arrayOfInt;
   __CPROVER_assert(diff2==1, "pointer diff2");
 
+  int zero = (char **)8 - (char **)8;
+  __CPROVER_assert(zero == 0, "should be zero");
+
+  int ten = (char *)20 - (char *)10;
+  __CPROVER_assert(ten == 10, "should be ten");
+
   return 0;
 }

regression/cbmc/Pointer_difference1/no-simplify.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--no-simplify
+VERIFICATION SUCCESSFUL
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$

src/solvers/flattening/bv_pointers.cpp

@@ -624,11 +624,6 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
     const exprt same_object = ::same_object(minus_expr.lhs(), minus_expr.rhs());
     const literalt same_object_lit = convert(same_object);
 
-    // 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);
-
     bvt bv = prop.new_variables(width);
 
     if(!same_object_lit.is_false())
@@ -638,27 +633,11 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
       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
@@ -678,9 +657,39 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
         }
       }
 
+      // 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, prop.land(lhs_in_bounds, rhs_in_bounds)),
-        bv_utils.equal(difference, bv)));
+        prop.land(same_object_lit, in_bounds), bv_utils.equal(difference, bv)));
     }
 
     return bv;

src/util/simplify_expr_int.cpp

@@ -614,6 +614,7 @@ simplify_exprt::simplify_minus(const minus_exprt &expr)
       if(
         offset_op0.is_constant() && offset_op1.is_constant() &&
         object_size.has_value() && element_size.has_value() &&
+        element_size->is_constant() && !element_size->is_zero() &&
         numeric_cast_v<mp_integer>(to_constant_expr(offset_op0)) <=
           *object_size &&
         numeric_cast_v<mp_integer>(to_constant_expr(offset_op1)) <=
@@ -624,6 +625,30 @@ simplify_exprt::simplify_minus(const minus_exprt &expr)
           typecast_exprt{*element_size, minus_expr.type()}}));
       }
     }
+
+    const exprt &ptr_op0_skipped_tc = skip_typecast(ptr_op0);
+    const exprt &ptr_op1_skipped_tc = skip_typecast(ptr_op1);
+    if(
+      is_number(ptr_op0_skipped_tc.type()) &&
+      is_number(ptr_op1_skipped_tc.type()))
+    {
+      exprt offset_op0 = simplify_pointer_offset(
+        pointer_offset_exprt{operands[0], minus_expr.type()});
+      exprt offset_op1 = simplify_pointer_offset(
+        pointer_offset_exprt{operands[1], minus_expr.type()});
+
+      auto element_size =
+        size_of_expr(to_pointer_type(operands[0].type()).base_type(), ns);
+
+      if(
+        element_size.has_value() && element_size->is_constant() &&
+        !element_size->is_zero())
+      {
+        return changed(simplify_rec(div_exprt{
+          minus_exprt{offset_op0, offset_op1},
+          typecast_exprt{*element_size, minus_expr.type()}}));
+      }
+    }
   }
 
   return unchanged(expr);