Fix simplification of pointer-object comparison

1) pointer_object((T1 *)NULL) equals pointer_object((T2 *)NULL) for any
types T1, T2. Previously, this would return false, unless T1==T2.
2) Do not restrict the above to NULL, but instead let the existing logic
in simplify_inequality fully simplify this.
3) Add a unit test of this code, which highlighted further bugs and
limitations: the unit test previously did not set the instance of the
desired dynamic object, and address-of inequalities over dynamic objects
can also be simplified.

Author: tautschnig

src/util/simplify_expr_pointer.cpp

@@ -447,6 +447,25 @@ bool simplify_exprt::simplify_inequality_address_of(exprt &expr)
 
     return false;
   }
+  else if(
+    tmp0.op0().id() == ID_dynamic_object &&
+    tmp1.op0().id() == ID_dynamic_object)
+  {
+    bool equal = to_dynamic_object_expr(tmp0.op0()).get_instance() ==
+                 to_dynamic_object_expr(tmp1.op0()).get_instance();
+
+    expr.make_bool(expr.id() == ID_equal ? equal : !equal);
+
+    return false;
+  }
+  else if(
+    (tmp0.op0().id() == ID_symbol && tmp1.op0().id() == ID_dynamic_object) ||
+    (tmp0.op0().id() == ID_dynamic_object && tmp1.op0().id() == ID_symbol))
+  {
+    expr.make_bool(expr.id() != ID_equal);
+
+    return false;
+  }
 
   return true;
 }
@@ -458,6 +477,7 @@ bool simplify_exprt::simplify_inequality_pointer_object(exprt &expr)
   DATA_INVARIANT(
     expr.operands().size() == 2, "(in)equalities have two operands");
 
+  exprt::operandst new_inequality_ops;
   forall_operands(it, expr)
   {
     PRECONDITION(it->id() == ID_pointer_object);
@@ -474,16 +494,23 @@ bool simplify_exprt::simplify_inequality_pointer_object(exprt &expr)
         return true;
       }
     }
-    else if(op.id() != ID_constant || op.get(ID_value) != ID_NULL)
+    else if(op.id() != ID_constant || !op.is_zero())
     {
       return true;
     }
-  }
 
-  bool equal=expr.op0().op0()==expr.op1().op0();
-
-  expr.make_bool(expr.id()==ID_equal?equal:!equal);
+    if(new_inequality_ops.empty())
+      new_inequality_ops.push_back(op);
+    else
+    {
+      new_inequality_ops.push_back(typecast_exprt::conditional_cast(
+        op, new_inequality_ops.front().type()));
+      simplify_node(new_inequality_ops.back());
+    }
+  }
 
+  expr.operands() = std::move(new_inequality_ops);
+  simplify_inequality(expr);
   return false;
 }
 

unit/util/simplify_expr.cpp

@@ -20,7 +20,7 @@ Author: Michael Tautschnig
 #include <util/std_expr.h>
 #include <util/symbol_table.h>
 
-TEST_CASE("Simplify pointer_offset(address of array index)")
+TEST_CASE("Simplify pointer_offset(address of array index)", "[core][util]")
 {
   config.set_arch("none");
 
@@ -42,7 +42,7 @@ TEST_CASE("Simplify pointer_offset(address of array index)")
   REQUIRE(offset_value==1);
 }
 
-TEST_CASE("Simplify const pointer offset")
+TEST_CASE("Simplify const pointer offset", "[core][util]")
 {
   config.set_arch("none");
 
@@ -63,7 +63,7 @@ TEST_CASE("Simplify const pointer offset")
   REQUIRE(offset_value==1234);
 }
 
-TEST_CASE("Simplify byte extract")
+TEST_CASE("Simplify byte extract", "[core][util]")
 {
   // this test does require a proper architecture to be set so that byte extract
   // uses adequate endianness
@@ -84,7 +84,7 @@ TEST_CASE("Simplify byte extract")
   REQUIRE(simp == s);
 }
 
-TEST_CASE("expr2bits and bits2expr respect bit order")
+TEST_CASE("expr2bits and bits2expr respect bit order", "[core][util]")
 {
   symbol_tablet symbol_table;
   namespacet ns(symbol_table);
@@ -109,7 +109,7 @@ TEST_CASE("expr2bits and bits2expr respect bit order")
   REQUIRE(deadbeef == *should_be_deadbeef2);
 }
 
-TEST_CASE("Simplify extractbit")
+TEST_CASE("Simplify extractbit", "[core][util]")
 {
   // this test does require a proper architecture to be set so that byte extract
   // uses adequate endianness
@@ -139,7 +139,7 @@ TEST_CASE("Simplify extractbit")
   REQUIRE(eb2 == true_exprt());
 }
 
-TEST_CASE("Simplify extractbits")
+TEST_CASE("Simplify extractbits", "[core][util]")
 {
   // this test does require a proper architecture to be set so that byte extract
   // uses adequate endianness
@@ -158,7 +158,7 @@ TEST_CASE("Simplify extractbits")
   REQUIRE(eb == from_integer(0xbe, unsignedbv_typet(8)));
 }
 
-TEST_CASE("Simplify shift")
+TEST_CASE("Simplify shift", "[core][util]")
 {
   const symbol_tablet symbol_table;
   const namespacet ns(symbol_table);
@@ -207,7 +207,7 @@ TEST_CASE("Simplify dynamic object comparison", "[core][util]")
   REQUIRE(simplify_expr(compare_null_through_cast, ns) == false_exprt());
 
   dynamic_object_exprt other_dynamic_object(signedbv_typet(8));
-  dynamic_object.set_instance(2);
+  other_dynamic_object.set_instance(2);
   address_of_exprt address_of_other_dynamic_object(other_dynamic_object);
 
   equal_exprt compare_pointer_objects(
@@ -216,3 +216,23 @@ TEST_CASE("Simplify dynamic object comparison", "[core][util]")
 
   REQUIRE(simplify_expr(compare_pointer_objects, ns) == false_exprt());
 }
+
+TEST_CASE("Simplify pointer_object equality", "[core][util]")
+{
+  // this test requires a proper architecture to be set up so that pointers have
+  // a width
+  const cmdlinet cmdline;
+  config.set(cmdline);
+
+  symbol_tablet symbol_table;
+  namespacet ns(symbol_table);
+
+  exprt p_o_void =
+    pointer_object(null_pointer_exprt{pointer_type(empty_typet{})});
+  exprt p_o_int =
+    pointer_object(null_pointer_exprt{pointer_type(signedbv_typet(32))});
+
+  exprt simp = simplify_expr(equal_exprt{p_o_void, p_o_int}, ns);
+
+  REQUIRE(simp.is_true());
+}