From 90145061e6ecc925c23c0c1ed1d7a57a4553e7d5 Mon Sep 17 00:00:00 2001
From: Chris Smowton <chris@smowton.net>
Date: Mon, 15 Apr 2019 12:13:07 +0100
Subject: [PATCH] Restore recognition of dynamic objects

These were accidentally disabled when distinguishing ID_is_dynamic_object (a predicate that tests
whether an object is dynamic) from ID_dynamic_object (a reference to the object itself, similar to
symbol_exprt). I also take the opportunity to restore pretty-printing of dynamic object expressions
(while also keeping pretty-printing of the predicate).
---
 src/ansi-c/expr2c.cpp              |  3 +++
 src/util/simplify_expr_int.cpp     |  4 ++--
 src/util/simplify_expr_pointer.cpp |  2 +-
 unit/util/simplify_expr.cpp        | 33 ++++++++++++++++++++++++++++++
 4 files changed, 39 insertions(+), 3 deletions(-)

diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
index da3e16c4d11..fb3cb85967b 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/src/ansi-c/expr2c.cpp
@@ -3486,6 +3486,9 @@ std::string expr2ct::convert_with_precedence(
     return convert_function(
       src, CPROVER_PREFIX "is_invalid_pointer", precedence = 16);
 
+  else if(src.id() == ID_dynamic_object)
+    return convert_function(src, "DYNAMIC_OBJECT", precedence = 16);
+
   else if(src.id() == ID_is_dynamic_object)
     return convert_function(src, "IS_DYNAMIC_OBJECT", precedence = 16);
 
diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp
index c0415b1c983..e35b1280099 100644
--- a/src/util/simplify_expr_int.cpp
+++ b/src/util/simplify_expr_int.cpp
@@ -1711,7 +1711,7 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr)
       {
         if(
           expr.op0().op0().id() == ID_symbol ||
-          expr.op0().op0().id() == ID_is_dynamic_object ||
+          expr.op0().op0().id() == ID_dynamic_object ||
           expr.op0().op0().id() == ID_member ||
           expr.op0().op0().id() == ID_index ||
           expr.op0().op0().id() == ID_string_constant)
@@ -1728,7 +1728,7 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr)
       {
         if(
           expr.op0().op0().op0().id() == ID_symbol ||
-          expr.op0().op0().op0().id() == ID_is_dynamic_object ||
+          expr.op0().op0().op0().id() == ID_dynamic_object ||
           expr.op0().op0().op0().id() == ID_member ||
           expr.op0().op0().op0().id() == ID_index ||
           expr.op0().op0().op0().id() == ID_string_constant)
diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp
index 6c66addad52..e1e41941896 100644
--- a/src/util/simplify_expr_pointer.cpp
+++ b/src/util/simplify_expr_pointer.cpp
@@ -468,7 +468,7 @@ bool simplify_exprt::simplify_inequality_pointer_object(exprt &expr)
     {
       if(
         op.operands().size() != 1 ||
-        (op.op0().id() != ID_symbol && op.op0().id() != ID_is_dynamic_object &&
+        (op.op0().id() != ID_symbol && op.op0().id() != ID_dynamic_object &&
          op.op0().id() != ID_string_constant))
       {
         return true;
diff --git a/unit/util/simplify_expr.cpp b/unit/util/simplify_expr.cpp
index 0c4cd5b682a..33b172f5b37 100644
--- a/unit/util/simplify_expr.cpp
+++ b/unit/util/simplify_expr.cpp
@@ -183,3 +183,36 @@ TEST_CASE("Simplify shift")
     simplify_expr(lshr_exprt(from_integer(-4, signedbv_typet(8)), 1), ns) ==
     from_integer(126, signedbv_typet(8)));
 }
+
+TEST_CASE("Simplify dynamic object comparison", "[core][util]")
+{
+  const symbol_tablet symbol_table;
+  const namespacet ns(symbol_table);
+
+  dynamic_object_exprt dynamic_object(signedbv_typet(8));
+  dynamic_object.set_instance(1);
+
+  address_of_exprt address_of_dynamic_object(dynamic_object);
+
+  equal_exprt compare_null(
+    address_of_dynamic_object,
+    null_pointer_exprt(to_pointer_type(address_of_dynamic_object.type())));
+  REQUIRE(simplify_expr(compare_null, ns) == false_exprt());
+
+  typecast_exprt cast_address(
+    address_of_dynamic_object, pointer_type(signedbv_typet(16)));
+
+  equal_exprt compare_null_through_cast(
+    cast_address, null_pointer_exprt(to_pointer_type(cast_address.type())));
+  REQUIRE(simplify_expr(compare_null_through_cast, ns) == false_exprt());
+
+  dynamic_object_exprt other_dynamic_object(signedbv_typet(8));
+  dynamic_object.set_instance(2);
+  address_of_exprt address_of_other_dynamic_object(other_dynamic_object);
+
+  equal_exprt compare_pointer_objects(
+    pointer_object(address_of_dynamic_object),
+    pointer_object(address_of_other_dynamic_object));
+
+  REQUIRE(simplify_expr(compare_pointer_objects, ns) == false_exprt());
+}