Merge pull request #3898 from tautschnig/use-object_descriptor

Extend object_descriptor_exprt::build and use it

Author: tautschnig

jbmc/unit/java-testing-utils/require_goto_statements.cpp

@@ -18,39 +18,6 @@ Author: Diffblue Ltd.
 #include <util/expr_util.h>
 #include <util/suffix.h>
 
-/// Given an expression, attempt to find the underlying symbol it represents
-/// by skipping over type casts and removing balanced dereference/address_of
-/// operations
-optionalt<symbol_exprt>
-root_object(const exprt &lhs_expr, const symbol_tablet &symbol_table)
-{
-  auto expr = skip_typecast(lhs_expr);
-  int dereference_balance = 0;
-  while(!can_cast_expr<symbol_exprt>(expr))
-  {
-    if(const auto deref = expr_try_dynamic_cast<dereference_exprt>(expr))
-    {
-      ++dereference_balance;
-      expr = skip_typecast(deref->pointer());
-    }
-    else if(
-      const auto address_of = expr_try_dynamic_cast<address_of_exprt>(expr))
-    {
-      --dereference_balance;
-      expr = skip_typecast(address_of->object());
-    }
-    else
-    {
-      return {};
-    }
-  }
-  if(dereference_balance != 0)
-  {
-    return {};
-  }
-  return to_symbol_expr(expr);
-}
-
 /// Expand value of a function to include all child codets
 /// \param function_value: The value of the function (e.g. got by looking up
 ///  the function in the symbol table and getting the value)
@@ -139,7 +106,7 @@ require_goto_statements::find_struct_component_assignments(
             ode.build(superclass_expr, ns);
             if(
               superclass_expr.get_component_name() == supercomponent_name &&
-              root_object(ode.root_object(), symbol_table)->get_identifier() ==
+              to_symbol_expr(ode.root_object()).get_identifier() ==
                 structure_name)
             {
               if(
@@ -162,10 +129,13 @@ require_goto_statements::find_struct_component_assignments(
           // - component name: \p component_name
           // - operand (component of): symbol for \p structure_name
 
-          const auto &root_object =
-            ::root_object(member_expr.struct_op(), symbol_table);
+          object_descriptor_exprt ode;
+          const namespacet ns(symbol_table);
+          ode.build(member_expr, ns);
           if(
-            root_object && root_object->get_identifier() == structure_name &&
+            ode.root_object().id() == ID_symbol &&
+            to_symbol_expr(ode.root_object()).get_identifier() ==
+              structure_name &&
             member_expr.get_component_name() == component_name)
           {
             if(

src/util/std_expr.cpp

@@ -10,11 +10,10 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/namespace.h>
 
-#include <cassert>
-
 #include "arith_tools.h"
 #include "byte_operators.h"
 #include "c_types.h"
+#include "expr_util.h"
 #include "mathematical_types.h"
 #include "pointer_offset_size.h"
 
@@ -114,6 +113,24 @@ static void build_object_descriptor_rec(
 
     build_object_descriptor_rec(ns, tc.op(), dest);
   }
+  else if(const auto deref = expr_try_dynamic_cast<dereference_exprt>(expr))
+  {
+    const exprt &pointer = skip_typecast(deref->pointer());
+    if(const auto address_of = expr_try_dynamic_cast<address_of_exprt>(pointer))
+    {
+      dest.object() = address_of->object();
+      build_object_descriptor_rec(ns, address_of->object(), dest);
+    }
+  }
+  else if(const auto address_of = expr_try_dynamic_cast<address_of_exprt>(expr))
+  {
+    const exprt &object = skip_typecast(address_of->object());
+    if(const auto deref = expr_try_dynamic_cast<dereference_exprt>(object))
+    {
+      dest.object() = deref->pointer();
+      build_object_descriptor_rec(ns, deref->pointer(), dest);
+    }
+  }
 }
 
 /// Build an object_descriptor_exprt from a given expr

src/util/std_expr.h

@@ -2027,6 +2027,10 @@ class object_descriptor_exprt:public binary_exprt
   {
   }
 
+  /// Given an expression \p expr, attempt to find the underlying object it
+  /// represents by skipping over type casts and removing balanced
+  /// dereference/address_of operations; that object will then be available
+  /// as root_object().
   void build(const exprt &expr, const namespacet &ns);
 
   exprt &object()

unit/util/std_expr.cpp

@@ -9,11 +9,16 @@ Author: Diffblue Ltd
 #include <testing-utils/use_catch.h>
 
 #include <util/arith_tools.h>
+#include <util/c_types.h>
+#include <util/config.h>
 #include <util/mathematical_types.h>
+#include <util/namespace.h>
+#include <util/simplify_expr.h>
 #include <util/std_expr.h>
 #include <util/std_types.h>
+#include <util/symbol_table.h>
 
-TEST_CASE("for a division expression...")
+TEST_CASE("for a division expression...", "[unit][util][std_expr]")
 {
   auto dividend = from_integer(10, integer_typet());
   auto divisor = from_integer(5, integer_typet());
@@ -30,3 +35,42 @@ TEST_CASE("for a division expression...")
     REQUIRE(div.type() == integer_typet());
   }
 }
+
+TEST_CASE("object descriptor expression", "[unit][util][std_expr]")
+{
+  config.ansi_c.set_LP64();
+
+  symbol_tablet symbol_table;
+  const namespacet ns(symbol_table);
+
+  array_typet array_type(signed_int_type(), from_integer(2, size_type()));
+  struct_typet struct_type({{"foo", array_type}});
+
+  SECTION("object descriptors of index expressions")
+  {
+    const symbol_exprt s("array", array_type);
+    // s[1]
+    const index_exprt index(s, from_integer(1, index_type()));
+
+    object_descriptor_exprt ode;
+    ode.build(index, ns);
+    REQUIRE(ode.root_object() == s);
+    // in LP64 a signed int is 4 bytes
+    REQUIRE(simplify_expr(ode.offset(), ns) == from_integer(4, index_type()));
+  }
+
+  SECTION("object descriptors of member expressions")
+  {
+    const symbol_exprt s("struct", struct_type);
+    // s.foo
+    const member_exprt member(s, "foo", array_type);
+    // s.foo[1]
+    const index_exprt index(member, from_integer(1, index_type()));
+
+    object_descriptor_exprt ode;
+    ode.build(index, ns);
+    REQUIRE(ode.root_object() == s);
+    // in LP64 a signed int is 4 bytes
+    REQUIRE(simplify_expr(ode.offset(), ns) == from_integer(4, index_type()));
+  }
+}