diff --git a/jbmc/unit/java-testing-utils/require_goto_statements.cpp b/jbmc/unit/java-testing-utils/require_goto_statements.cpp index 871fd74c3d2..4e2ef931915 100644 --- a/jbmc/unit/java-testing-utils/require_goto_statements.cpp +++ b/jbmc/unit/java-testing-utils/require_goto_statements.cpp @@ -18,39 +18,6 @@ Author: Diffblue Ltd. #include #include -/// Given an expression, attempt to find the underlying symbol it represents -/// by skipping over type casts and removing balanced dereference/address_of -/// operations -optionalt -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(expr)) - { - if(const auto deref = expr_try_dynamic_cast(expr)) - { - ++dereference_balance; - expr = skip_typecast(deref->pointer()); - } - else if( - const auto address_of = expr_try_dynamic_cast(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( diff --git a/src/util/std_expr.cpp b/src/util/std_expr.cpp index e21d6d2339a..251d00b7c27 100644 --- a/src/util/std_expr.cpp +++ b/src/util/std_expr.cpp @@ -10,11 +10,10 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include - #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(expr)) + { + const exprt &pointer = skip_typecast(deref->pointer()); + if(const auto address_of = expr_try_dynamic_cast(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(expr)) + { + const exprt &object = skip_typecast(address_of->object()); + if(const auto deref = expr_try_dynamic_cast(object)) + { + dest.object() = deref->pointer(); + build_object_descriptor_rec(ns, deref->pointer(), dest); + } + } } /// Build an object_descriptor_exprt from a given expr diff --git a/src/util/std_expr.h b/src/util/std_expr.h index f01f0150f1f..2473c4cb907 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -2026,6 +2026,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() diff --git a/unit/util/std_expr.cpp b/unit/util/std_expr.cpp index 162ade636fc..731de139ef6 100644 --- a/unit/util/std_expr.cpp +++ b/unit/util/std_expr.cpp @@ -9,11 +9,16 @@ Author: Diffblue Ltd #include #include +#include +#include #include +#include +#include #include #include +#include -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())); + } +}