@@ -15,6 +15,40 @@ Author: Diffblue Ltd.
15
15
#include < goto-programs/goto_functions.h>
16
16
#include < java_bytecode/java_types.h>
17
17
#include < util/suffix.h>
18
+ #include < util/expr_util.h>
19
+ #include < iostream>
20
+ #include < goto-programs/show_goto_functions.h>
21
+
22
+ optionalt<symbol_exprt> root_object (exprt lhs_expr, const symbol_tablet &symbol_table)
23
+ {
24
+ auto expr = skip_typecast (lhs_expr);
25
+ int dereference_balance = 0 ;
26
+ while (!can_cast_expr<symbol_exprt>(expr))
27
+ {
28
+ if (const auto deref = expr_try_dynamic_cast<dereference_exprt>(expr))
29
+ {
30
+ ++dereference_balance;
31
+ expr = skip_typecast (deref->pointer ());
32
+ }
33
+ else if (
34
+ const auto address_of = expr_try_dynamic_cast<address_of_exprt>(expr))
35
+ {
36
+ --dereference_balance;
37
+ expr = skip_typecast (address_of->object ());
38
+ }
39
+ else
40
+ {
41
+ INFO (" Unrecognised assignment " << lhs_expr.pretty ());
42
+ return {};
43
+ }
44
+ }
45
+ if (dereference_balance != 0 )
46
+ {
47
+ INFO (" Unbalanced access " << lhs_expr.pretty ());
48
+ return {};
49
+ }
50
+ return to_symbol_expr (expr);
51
+ }
18
52
19
53
// / Expand value of a function to include all child codets
20
54
// / \param function_value: The value of the function (e.g. got by looking up
@@ -104,7 +138,7 @@ require_goto_statements::find_struct_component_assignments(
104
138
ode.build (superclass_expr, ns);
105
139
if (
106
140
superclass_expr.get_component_name () == supercomponent_name &&
107
- to_symbol_expr (ode.root_object ()). get_identifier () ==
141
+ root_object (ode.root_object (), symbol_table)-> get_identifier () ==
108
142
structure_name)
109
143
{
110
144
if (
@@ -126,9 +160,10 @@ require_goto_statements::find_struct_component_assignments(
126
160
// member_exprt member_expr:
127
161
// - component name: \p component_name
128
162
// - operand (component of): symbol for \p structure_name
163
+
164
+ const auto &root_object = ::root_object (member_expr.struct_op (), symbol_table);
129
165
if (
130
- member_expr.op ().id () == ID_symbol &&
131
- to_symbol_expr (member_expr.op ()).get_identifier () == structure_name &&
166
+ root_object && root_object->get_identifier () == structure_name &&
132
167
member_expr.get_component_name () == component_name)
133
168
{
134
169
if (
@@ -317,6 +352,7 @@ const irep_idt &require_goto_statements::require_struct_component_assignment(
317
352
superclass_name,
318
353
component_name,
319
354
symbol_table);
355
+ INFO (" looking for " << component_name << " in " << (superclass_name ? *superclass_name : structure_name));
320
356
REQUIRE (component_assignments.non_null_assignments .size () == 1 );
321
357
322
358
// We are expecting that the resulting statement can be of two forms:
@@ -325,34 +361,22 @@ const irep_idt &require_goto_statements::require_struct_component_assignment(
325
361
// followed by a direct assignment like this:
326
362
// tmp_object_factory$1 = &tmp_object_factory$2;
327
363
// 2. structure_name.component = &tmp_object_factory$1;
364
+ // 3. structure_name.component (cast *)&tmp_object_factory$1
328
365
exprt component_assignment_rhs_expr =
329
- component_assignments.non_null_assignments [0 ].rhs ();
366
+ skip_typecast ( component_assignments.non_null_assignments [0 ].rhs () );
330
367
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)
368
+ // If the rhs is not an address of must be in case 1
369
+ if (!can_cast_expr<address_of_exprt>(component_assignment_rhs_expr))
334
370
{
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
371
const auto &component_reference_tmp_name =
349
- to_symbol_expr (component_assignment_rhs. op () ).get_identifier ();
372
+ to_symbol_expr (component_assignment_rhs_expr ).get_identifier ();
350
373
const auto &component_reference_assignments =
351
374
require_goto_statements::find_pointer_assignments (
352
375
component_reference_tmp_name, entry_point_instructions)
353
376
.non_null_assignments ;
354
377
REQUIRE (component_reference_assignments.size () == 1 );
355
- component_assignment_rhs_expr = component_reference_assignments[0 ].rhs ();
378
+ component_assignment_rhs_expr =
379
+ skip_typecast (component_reference_assignments[0 ].rhs ());
356
380
}
357
381
358
382
// The rhs assigns an address of a variable, get its name
@@ -480,7 +504,8 @@ require_goto_statements::require_entry_point_argument_assignment(
480
504
const auto &argument_assignment =
481
505
argument_assignments.non_null_assignments [0 ];
482
506
const auto &argument_tmp_name =
483
- to_symbol_expr (to_address_of_expr (argument_assignment.rhs ()).object ())
507
+ to_symbol_expr (
508
+ to_address_of_expr (skip_typecast (argument_assignment.rhs ())).object ())
484
509
.get_identifier ();
485
510
return argument_tmp_name;
486
511
}
0 commit comments