Merge pull request #6143 from tautschnig/pointer-comparison

Binary comparison <, <=, >, >= over pointers requires same-object

Author: tautschnig

regression/cbmc/Pointer29/main.c

@@ -3,6 +3,14 @@
 int main()
 {
   unsigned int *s_pdt = (unsigned int *)(0xdeadbeef);
-  assert(s_pdt > 1);
+  // this is well defined
+  assert((unsigned long long)s_pdt > 1);
+  // this is undefined as it could both be a comparison over integers as well as
+  // over pointers; the latter may mean comparing pointers to different objects,
+  // so guard against that
+  assert(
+    __CPROVER_POINTER_OBJECT(s_pdt) !=
+      __CPROVER_POINTER_OBJECT((unsigned int *)1) ||
+    s_pdt > 1);
   return 0;
 }

regression/cbmc/Pointer_comparison3/main.c

@@ -1,9 +1,29 @@
 #include <assert.h>
 #include <stdlib.h>
 
+char *nondet_pointer();
+
 int main()
 {
   int *p1 = malloc(sizeof(int));
 
   assert(p1 < p1 + 1);
+
+  int *p2 = malloc(sizeof(int));
+
+  assert(p1 != p2);
+
+  _Bool nondet;
+  // In the current implementation, CBMC always produces "false" for a
+  // comparison over different objects. This could change at any time, which
+  // would require updating this test.
+  if(nondet)
+    __CPROVER_assert(p1 < p2, "always false for different objects");
+  else
+    __CPROVER_assert(p1 > p2, "always false for different objects");
+
+  char *p = nondet_pointer();
+
+  __CPROVER_assume(p < p1 + 1);
+  assert(__CPROVER_POINTER_OBJECT(p) == __CPROVER_POINTER_OBJECT(p1));
 }

regression/cbmc/Pointer_comparison3/test.desc

@@ -1,8 +1,11 @@
 CORE
 main.c
 
-^VERIFICATION SUCCESSFUL$
-^EXIT=0$
+^\[main.assertion.3\] line 21 always false for different objects: FAILURE$
+^\[main.assertion.4\] line 23 always false for different objects: FAILURE$
+^\*\* 2 of 7 failed
+^VERIFICATION FAILED$
+^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring

src/solvers/flattening/bv_pointers.cpp

@@ -172,8 +172,30 @@ literalt bv_pointerst::convert_rest(const exprt &expr)
       const bvt &bv0=convert_bv(operands[0]);
       const bvt &bv1=convert_bv(operands[1]);
 
-      return bv_utils.rel(
-        bv0, expr.id(), bv1, bv_utilst::representationt::UNSIGNED);
+      const pointer_typet &type0 = to_pointer_type(operands[0].type());
+      bvt offset_bv0 = offset_literals(bv0, type0);
+
+      const pointer_typet &type1 = to_pointer_type(operands[1].type());
+      bvt offset_bv1 = offset_literals(bv1, type1);
+
+      // Comparison over pointers to distinct objects is undefined behavior in
+      // C; we choose to always produce "false" in such a case.  Alternatively,
+      // we could do a comparison over the integer representation of a pointer
+
+      // 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(operands[0], operands[1]);
+      const literalt same_object_lit = convert(same_object);
+      if(same_object_lit.is_false())
+        return same_object_lit;
+
+      return prop.land(
+        same_object_lit,
+        bv_utils.rel(
+          offset_bv0,
+          expr.id(),
+          offset_bv1,
+          bv_utilst::representationt::SIGNED));
     }
   }
 

src/solvers/smt2/smt2_conv.cpp

@@ -27,6 +27,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/namespace.h>
 #include <util/pointer_expr.h>
 #include <util/pointer_offset_size.h>
+#include <util/pointer_predicates.h>
 #include <util/prefix.h>
 #include <util/range.h>
 #include <util/simplify_expr.h>
@@ -3165,7 +3166,6 @@ void smt2_convt::convert_relation(const binary_relation_exprt &expr)
   const typet &op_type=expr.op0().type();
 
   if(op_type.id()==ID_unsignedbv ||
-     op_type.id()==ID_pointer ||
      op_type.id()==ID_bv)
   {
     out << "(";
@@ -3238,6 +3238,31 @@ void smt2_convt::convert_relation(const binary_relation_exprt &expr)
     convert_expr(expr.op1());
     out << ")";
   }
+  else if(op_type.id() == ID_pointer)
+  {
+    const exprt same_object = ::same_object(expr.op0(), expr.op1());
+
+    out << "(and ";
+    convert_expr(same_object);
+
+    out << " (";
+    if(expr.id() == ID_le)
+      out << "bvsle";
+    else if(expr.id() == ID_lt)
+      out << "bvslt";
+    else if(expr.id() == ID_ge)
+      out << "bvsge";
+    else if(expr.id() == ID_gt)
+      out << "bvsgt";
+
+    out << ' ';
+    convert_expr(pointer_offset(expr.op0()));
+    out << ' ';
+    convert_expr(pointer_offset(expr.op1()));
+    out << ')';
+
+    out << ')';
+  }
   else
     UNEXPECTEDCASE(
       "unsupported type for "+expr.id_string()+": "+op_type.id_string());

src/util/simplify_expr_int.cpp

@@ -1473,6 +1473,14 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_no_constant(
   if(expr.op0().type().id() == ID_floatbv)
     return unchanged(expr);
 
+  // simplifications below require same-object, which we don't check for
+  if(
+    expr.op0().type().id() == ID_pointer && expr.id() != ID_equal &&
+    expr.id() != ID_notequal)
+  {
+    return unchanged(expr);
+  }
+
   // eliminate strict inequalities
   if(expr.id()==ID_notequal)
   {