@@ -11,11 +11,46 @@ Author: Diffblue Ltd.
11
11
#include < testing-utils/use_catch.h>
12
12
13
13
#include < algorithm>
14
- #include < util/expr_iterator.h>
15
14
#include < goto-programs/goto_functions.h>
15
+ #include < goto-programs/show_goto_functions.h>
16
16
#include < java_bytecode/java_types.h>
17
+ #include < util/expr_iterator.h>
18
+ #include < util/expr_util.h>
17
19
#include < util/suffix.h>
18
20
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
+
19
54
// / Expand value of a function to include all child codets
20
55
// / \param function_value: The value of the function (e.g. got by looking up
21
56
// / the function in the symbol table and getting the value)
@@ -104,8 +139,8 @@ require_goto_statements::find_struct_component_assignments(
104
139
ode.build (superclass_expr, ns);
105
140
if (
106
141
superclass_expr.get_component_name () == supercomponent_name &&
107
- to_symbol_expr (ode.root_object ()). get_identifier () ==
108
- structure_name)
142
+ root_object (ode.root_object (), symbol_table)-> get_identifier () ==
143
+ structure_name)
109
144
{
110
145
if (
111
146
code_assign.rhs () ==
@@ -126,9 +161,11 @@ require_goto_statements::find_struct_component_assignments(
126
161
// member_exprt member_expr:
127
162
// - component name: \p component_name
128
163
// - operand (component of): symbol for \p structure_name
164
+
165
+ const auto &root_object =
166
+ ::root_object (member_expr.struct_op(), symbol_table);
129
167
if (
130
- member_expr.op ().id () == ID_symbol &&
131
- to_symbol_expr (member_expr.op ()).get_identifier () == structure_name &&
168
+ root_object && root_object->get_identifier () == structure_name &&
132
169
member_expr.get_component_name () == component_name)
133
170
{
134
171
if (
@@ -317,42 +354,32 @@ const irep_idt &require_goto_statements::require_struct_component_assignment(
317
354
superclass_name,
318
355
component_name,
319
356
symbol_table);
357
+ INFO (
358
+ " looking for component assignment " << component_name << " in "
359
+ << structure_name);
320
360
REQUIRE (component_assignments.non_null_assignments .size () == 1 );
321
361
322
- // We are expecting that the resulting statement can be of two forms :
362
+ // We are expecting that the resulting statement can be of the form :
323
363
// 1. structure_name.(@superclass_name if given).component =
324
- // (struct cast_type_name *) tmp_object_factory$1;
364
+ // (optional type cast *) tmp_object_factory$1;
325
365
// followed by a direct assignment like this:
326
366
// tmp_object_factory$1 = &tmp_object_factory$2;
327
- // 2. structure_name.component = &tmp_object_factory$1;
367
+ // 2. structure_name.component = (optional cast *) &tmp_object_factory$1
328
368
exprt component_assignment_rhs_expr =
329
- component_assignments.non_null_assignments [0 ].rhs ();
369
+ skip_typecast ( component_assignments.non_null_assignments [0 ].rhs () );
330
370
331
- // If the rhs is a typecast (case 1 above), deconstruct it to get the name of
332
- // the variable and find the assignment to it
333
- if (component_assignment_rhs_expr.id () == ID_typecast)
371
+ // If the rhs is not an address of must be in case 1
372
+ if (!can_cast_expr<address_of_exprt>(component_assignment_rhs_expr))
334
373
{
335
- const auto &component_assignment_rhs =
336
- to_typecast_expr (component_assignment_rhs_expr);
337
-
338
- // Check the type we are casting to
339
- if (typecast_name.has_value ())
340
- {
341
- REQUIRE (component_assignment_rhs.type ().id () == ID_pointer);
342
- REQUIRE (
343
- to_struct_tag_type (
344
- to_pointer_type (component_assignment_rhs.type ()).subtype ())
345
- .get (ID_identifier) == typecast_name.value ());
346
- }
347
-
348
374
const auto &component_reference_tmp_name =
349
- to_symbol_expr (component_assignment_rhs. op () ).get_identifier ();
375
+ to_symbol_expr (component_assignment_rhs_expr ).get_identifier ();
350
376
const auto &component_reference_assignments =
351
377
require_goto_statements::find_pointer_assignments (
352
378
component_reference_tmp_name, entry_point_instructions)
353
379
.non_null_assignments ;
354
380
REQUIRE (component_reference_assignments.size () == 1 );
355
- component_assignment_rhs_expr = component_reference_assignments[0 ].rhs ();
381
+ component_assignment_rhs_expr =
382
+ skip_typecast (component_reference_assignments[0 ].rhs ());
356
383
}
357
384
358
385
// The rhs assigns an address of a variable, get its name
@@ -480,7 +507,8 @@ require_goto_statements::require_entry_point_argument_assignment(
480
507
const auto &argument_assignment =
481
508
argument_assignments.non_null_assignments [0 ];
482
509
const auto &argument_tmp_name =
483
- to_symbol_expr (to_address_of_expr (argument_assignment.rhs ()).object ())
510
+ to_symbol_expr (
511
+ to_address_of_expr (skip_typecast (argument_assignment.rhs ())).object ())
484
512
.get_identifier ();
485
513
return argument_tmp_name;
486
514
}
0 commit comments