Simplify inequality over pointers

When using pointers as iterators we may see less-than (or less-or-equal)
comparison of pointers with some offsets. When the base pointers point
to the same root object we can safely simplify this.

Also avoid undefined behaviour (pointer below object bounds) in
regression test.

Author: tautschnig

regression/cbmc-incr-smt2/pointers-relational-operators/pointers_stack_lessthan.c

@@ -2,8 +2,8 @@
 
 int main()
 {
-  int i = 12;
-  int *x = &i;
+  int i[2] = {12, 13};
+  int *x = &i[0] + 1;
   int *y = x + 1;
   int *z = x - 1;
 

regression/cbmc/Pointer_comparison4/main.c

@@ -0,0 +1,6 @@
+int main()
+{
+  int A[5] = {0, 1, 2, 3, 4};
+  for(int *iter = &A[0]; iter < &A[5]; ++iter)
+    __CPROVER_assert(*iter == iter - &A[0], "values match");
+}

regression/cbmc/Pointer_comparison4/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--unwind 10 --unwinding-assertions
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+Unwinding loop .* iteration 6
+^warning: ignoring
+--
+Simplification and constant propagation should ensure that unwinding the loop
+stops when reaching the array bound.

src/util/simplify_expr_int.cpp

@@ -1587,12 +1587,24 @@ 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)
+  if(expr.op0().type().id() == ID_pointer)
   {
-    return unchanged(expr);
+    exprt ptr_op0 = simplify_object(expr.op0()).expr;
+    exprt ptr_op1 = simplify_object(expr.op1()).expr;
+
+    if(ptr_op0 == ptr_op1)
+    {
+      pointer_offset_exprt offset_op0{expr.op0(), size_type()};
+      pointer_offset_exprt offset_op1{expr.op1(), size_type()};
+
+      return changed(simplify_rec(binary_relation_exprt{
+        std::move(offset_op0), expr.id(), std::move(offset_op1)}));
+    }
+    // simplifications below require same-object, which we don't check for
+    else if(expr.id() != ID_equal && expr.id() != ID_notequal)
+    {
+      return unchanged(expr);
+    }
   }
 
   // eliminate strict inequalities
@@ -1651,19 +1663,6 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_no_constant(
       new_expr.rhs() = simplify_node(new_expr.rhs());
       return changed(simplify_inequality(new_expr)); // recursive call
     }
-    else if(expr.op0().type().id() == ID_pointer)
-    {
-      exprt ptr_op0 = simplify_object(expr.op0()).expr;
-      exprt ptr_op1 = simplify_object(expr.op1()).expr;
-
-      if(ptr_op0 == ptr_op1)
-      {
-        pointer_offset_exprt offset_op0{expr.op0(), size_type()};
-        pointer_offset_exprt offset_op1{expr.op1(), size_type()};
-
-        return changed(simplify_rec(equal_exprt{offset_op0, offset_op1}));
-      }
-    }
   }
 
   return unchanged(expr);