@@ -11,11 +11,47 @@ Author: Diffblue Ltd.
11
11
#include < testing-utils/catch.hpp>
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
+ #include < iostream>
16
17
#include < java_bytecode/java_types.h>
18
+ #include < util/expr_iterator.h>
19
+ #include < util/expr_util.h>
17
20
#include < util/suffix.h>
18
21
22
+ // / Given an expression, attempt to find the underlying symbol it represents
23
+ // / by skipping over type casts and removing balanced dereference/address_of
24
+ // / operations
25
+ optionalt<symbol_exprt>
26
+ root_object (const exprt &lhs_expr, const symbol_tablet &symbol_table)
27
+ {
28
+ auto expr = skip_typecast (lhs_expr);
29
+ int dereference_balance = 0 ;
30
+ while (!can_cast_expr<symbol_exprt>(expr))
31
+ {
32
+ if (const auto deref = expr_try_dynamic_cast<dereference_exprt>(expr))
33
+ {
34
+ ++dereference_balance;
35
+ expr = skip_typecast (deref->pointer ());
36
+ }
37
+ else if (
38
+ const auto address_of = expr_try_dynamic_cast<address_of_exprt>(expr))
39
+ {
40
+ --dereference_balance;
41
+ expr = skip_typecast (address_of->object ());
42
+ }
43
+ else
44
+ {
45
+ return {};
46
+ }
47
+ }
48
+ if (dereference_balance != 0 )
49
+ {
50
+ return {};
51
+ }
52
+ return to_symbol_expr (expr);
53
+ }
54
+
19
55
// / Expand value of a function to include all child codets
20
56
// / \param function_value: The value of the function (e.g. got by looking up
21
57
// / the function in the symbol table and getting the value)
@@ -104,8 +140,8 @@ require_goto_statements::find_struct_component_assignments(
104
140
ode.build (superclass_expr, ns);
105
141
if (
106
142
superclass_expr.get_component_name () == supercomponent_name &&
107
- to_symbol_expr (ode.root_object ()). get_identifier () ==
108
- structure_name)
143
+ root_object (ode.root_object (), symbol_table)-> get_identifier () ==
144
+ structure_name)
109
145
{
110
146
if (
111
147
code_assign.rhs () ==
@@ -126,9 +162,11 @@ require_goto_statements::find_struct_component_assignments(
126
162
// member_exprt member_expr:
127
163
// - component name: \p component_name
128
164
// - operand (component of): symbol for \p structure_name
165
+
166
+ const auto &root_object =
167
+ ::root_object (member_expr.struct_op(), symbol_table);
129
168
if (
130
- member_expr.op ().id () == ID_symbol &&
131
- to_symbol_expr (member_expr.op ()).get_identifier () == structure_name &&
169
+ root_object && root_object->get_identifier () == structure_name &&
132
170
member_expr.get_component_name () == component_name)
133
171
{
134
172
if (
@@ -317,42 +355,32 @@ const irep_idt &require_goto_statements::require_struct_component_assignment(
317
355
superclass_name,
318
356
component_name,
319
357
symbol_table);
358
+ INFO (
359
+ " looking for component assignment " << component_name << " in "
360
+ << structure_name);
320
361
REQUIRE (component_assignments.non_null_assignments .size () == 1 );
321
362
322
- // We are expecting that the resulting statement can be of two forms :
363
+ // We are expecting that the resulting statement can be of the form :
323
364
// 1. structure_name.(@superclass_name if given).component =
324
- // (struct cast_type_name *) tmp_object_factory$1;
365
+ // (optional type cast *) tmp_object_factory$1;
325
366
// followed by a direct assignment like this:
326
367
// tmp_object_factory$1 = &tmp_object_factory$2;
327
- // 2. structure_name.component = &tmp_object_factory$1;
368
+ // 2. structure_name.component = (optional cast *) &tmp_object_factory$1
328
369
exprt component_assignment_rhs_expr =
329
- component_assignments.non_null_assignments [0 ].rhs ();
370
+ skip_typecast ( component_assignments.non_null_assignments [0 ].rhs () );
330
371
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)
372
+ // If the rhs is not an address of must be in case 1
373
+ if (!can_cast_expr<address_of_exprt>(component_assignment_rhs_expr))
334
374
{
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
375
const auto &component_reference_tmp_name =
349
- to_symbol_expr (component_assignment_rhs. op () ).get_identifier ();
376
+ to_symbol_expr (component_assignment_rhs_expr ).get_identifier ();
350
377
const auto &component_reference_assignments =
351
378
require_goto_statements::find_pointer_assignments (
352
379
component_reference_tmp_name, entry_point_instructions)
353
380
.non_null_assignments ;
354
381
REQUIRE (component_reference_assignments.size () == 1 );
355
- component_assignment_rhs_expr = component_reference_assignments[0 ].rhs ();
382
+ component_assignment_rhs_expr =
383
+ skip_typecast (component_reference_assignments[0 ].rhs ());
356
384
}
357
385
358
386
// The rhs assigns an address of a variable, get its name
@@ -480,7 +508,8 @@ require_goto_statements::require_entry_point_argument_assignment(
480
508
const auto &argument_assignment =
481
509
argument_assignments.non_null_assignments [0 ];
482
510
const auto &argument_tmp_name =
483
- to_symbol_expr (to_address_of_expr (argument_assignment.rhs ()).object ())
511
+ to_symbol_expr (
512
+ to_address_of_expr (skip_typecast (argument_assignment.rhs ())).object ())
484
513
.get_identifier ();
485
514
return argument_tmp_name;
486
515
}
0 commit comments