Merge pull request #5922 from tautschnig/fix-5921

Use simplification for more reliable pointer comparison

Author: tautschnig

regression/cbmc/Pointer_comparison2/main.c

@@ -0,0 +1,18 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int *get_ptr_minus_one(int *ptr)
+{
+  if(ptr)
+    return ptr - 1;
+  return 0;
+}
+
+int main()
+{
+  int *begin = malloc(4 * 4);
+  int *end = begin + 1;
+
+  if(begin != get_ptr_minus_one(end))
+    assert(0);
+}

regression/cbmc/Pointer_comparison2/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

src/goto-symex/symex_goto.cpp

@@ -85,10 +85,9 @@ static optionalt<renamedt<exprt, L2>> try_evaluate_pointer_comparison(
 {
   const constant_exprt *constant_expr =
     expr_try_dynamic_cast<constant_exprt>(other_operand);
-  const exprt other_without_typecast = skip_typecast(other_operand);
 
   if(
-    other_without_typecast.id() != ID_address_of &&
+    skip_typecast(other_operand).id() != ID_address_of &&
     (!constant_expr || constant_expr->get_value() != ID_NULL))
   {
     return {};
@@ -129,12 +128,25 @@ static optionalt<renamedt<exprt, L2>> try_evaluate_pointer_comparison(
         value_set_dereferencet::build_reference_to(
           value_set_element, symbol_expr, ns);
 
-      if(skip_typecast(value.pointer) == other_without_typecast)
+      // use the simplifier to test equality as we need to skip over typecasts
+      // and cannot rely on canonical representations, which would permit a
+      // simple syntactic equality test
+      exprt test_equal = simplify_expr(
+        equal_exprt{
+          typecast_exprt::conditional_cast(value.pointer, other_operand.type()),
+          other_operand},
+        ns);
+      if(test_equal.is_true())
       {
         constant_found = true;
         // We can't break because we have to make sure we find any instances of
         // ID_unknown or ID_invalid
       }
+      else if(!test_equal.is_false())
+      {
+        // We can't conclude anything about the value-set
+        return {};
+      }
     }
   }
 

src/util/simplify_expr_int.cpp

@@ -1243,13 +1243,8 @@ simplify_exprt::simplify_inequality(const binary_relation_exprt &expr)
 
   // see if we are comparing pointers that are address_of
   if(
-    (tmp0.id() == ID_address_of ||
-     (tmp0.id() == ID_typecast &&
-      to_typecast_expr(tmp0).op().id() == ID_address_of)) &&
-    (tmp1.id() == ID_address_of ||
-     (tmp1.id() == ID_typecast &&
-      to_typecast_expr(tmp1).op().id() == ID_address_of)) &&
-    (expr.id() == ID_equal || expr.id() == ID_notequal))
+    skip_typecast(tmp0).id() == ID_address_of &&
+    skip_typecast(tmp1).id() == ID_address_of)
   {
     return simplify_inequality_address_of(expr);
   }

src/util/simplify_expr_pointer.cpp

@@ -426,12 +426,8 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_address_of(
 
   PRECONDITION(expr.id() == ID_equal || expr.id() == ID_notequal);
 
-  exprt tmp0=expr.op0();
-
   // skip over the typecast
-  if(tmp0.id()==ID_typecast)
-    tmp0 = to_typecast_expr(tmp0).op();
-
+  exprt tmp0 = skip_typecast(expr.op0());
   PRECONDITION(tmp0.id() == ID_address_of);
 
   auto &tmp0_address_of = to_address_of_expr(tmp0);
@@ -444,12 +440,8 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_address_of(
       address_of_exprt(to_index_expr(tmp0_address_of.object()).array());
   }
 
-  exprt tmp1=expr.op1();
-
   // skip over the typecast
-  if(tmp1.id()==ID_typecast)
-    tmp1 = to_typecast_expr(tmp1).op();
-
+  exprt tmp1 = skip_typecast(expr.op1());
   PRECONDITION(tmp1.id() == ID_address_of);
 
   auto &tmp1_address_of = to_address_of_expr(tmp1);