Skip to content

Commit bb511db

Browse files
committed
Extend object_descriptor_exprt::build and use it
Move the implementation from the unit test to object_descriptor_exprt to have all users of object_descriptor_exprt benefit from it.
1 parent 02744e6 commit bb511db

File tree

3 files changed

+21
-39
lines changed

3 files changed

+21
-39
lines changed

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

Lines changed: 7 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -18,39 +18,6 @@ Author: Diffblue Ltd.
1818
#include <util/expr_util.h>
1919
#include <util/suffix.h>
2020

21-
/// Given an expression, attempt to find the underlying symbol it represents
22-
/// by skipping over type casts and removing balanced dereference/address_of
23-
/// operations
24-
optionalt<symbol_exprt>
25-
root_object(const exprt &lhs_expr, const symbol_tablet &symbol_table)
26-
{
27-
auto expr = skip_typecast(lhs_expr);
28-
int dereference_balance = 0;
29-
while(!can_cast_expr<symbol_exprt>(expr))
30-
{
31-
if(const auto deref = expr_try_dynamic_cast<dereference_exprt>(expr))
32-
{
33-
++dereference_balance;
34-
expr = skip_typecast(deref->pointer());
35-
}
36-
else if(
37-
const auto address_of = expr_try_dynamic_cast<address_of_exprt>(expr))
38-
{
39-
--dereference_balance;
40-
expr = skip_typecast(address_of->object());
41-
}
42-
else
43-
{
44-
return {};
45-
}
46-
}
47-
if(dereference_balance != 0)
48-
{
49-
return {};
50-
}
51-
return to_symbol_expr(expr);
52-
}
53-
5421
/// Expand value of a function to include all child codets
5522
/// \param function_value: The value of the function (e.g. got by looking up
5623
/// the function in the symbol table and getting the value)
@@ -139,7 +106,7 @@ require_goto_statements::find_struct_component_assignments(
139106
ode.build(superclass_expr, ns);
140107
if(
141108
superclass_expr.get_component_name() == supercomponent_name &&
142-
root_object(ode.root_object(), symbol_table)->get_identifier() ==
109+
to_symbol_expr(ode.root_object()).get_identifier() ==
143110
structure_name)
144111
{
145112
if(
@@ -162,10 +129,13 @@ require_goto_statements::find_struct_component_assignments(
162129
// - component name: \p component_name
163130
// - operand (component of): symbol for \p structure_name
164131

165-
const auto &root_object =
166-
::root_object(member_expr.struct_op(), symbol_table);
132+
object_descriptor_exprt ode;
133+
const namespacet ns(symbol_table);
134+
ode.build(member_expr, ns);
167135
if(
168-
root_object && root_object->get_identifier() == structure_name &&
136+
ode.root_object().id() == ID_symbol &&
137+
to_symbol_expr(ode.root_object()).get_identifier() ==
138+
structure_name &&
169139
member_expr.get_component_name() == component_name)
170140
{
171141
if(

src/util/std_expr.cpp

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,11 +10,10 @@ Author: Daniel Kroening, [email protected]
1010

1111
#include <util/namespace.h>
1212

13-
#include <cassert>
14-
1513
#include "arith_tools.h"
1614
#include "byte_operators.h"
1715
#include "c_types.h"
16+
#include "expr_util.h"
1817
#include "mathematical_types.h"
1918
#include "pointer_offset_size.h"
2019

@@ -114,6 +113,15 @@ static void build_object_descriptor_rec(
114113

115114
build_object_descriptor_rec(ns, tc.op(), dest);
116115
}
116+
else if(const auto deref = expr_try_dynamic_cast<dereference_exprt>(expr))
117+
{
118+
const exprt &pointer = skip_typecast(deref->pointer());
119+
if(const auto address_of = expr_try_dynamic_cast<address_of_exprt>(pointer))
120+
{
121+
dest.object() = address_of->object();
122+
build_object_descriptor_rec(ns, address_of->object(), dest);
123+
}
124+
}
117125
}
118126

119127
/// Build an object_descriptor_exprt from a given expr

src/util/std_expr.h

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2026,6 +2026,10 @@ class object_descriptor_exprt:public binary_exprt
20262026
{
20272027
}
20282028

2029+
/// Given an expression \p expr, attempt to find the underlying object it
2030+
/// represents by skipping over type casts and removing balanced
2031+
/// dereference/address_of operations; that object will then be available
2032+
/// as root_object().
20292033
void build(const exprt &expr, const namespacet &ns);
20302034

20312035
exprt &object()

0 commit comments

Comments
 (0)