@@ -162,38 +162,39 @@ static exprt transform_external_objects(const exprt& e)
162
162
return e;
163
163
}
164
164
165
+ // / Use the output of LVSA to create a set of expressions which `query` might
166
+ // / point to at a given point in the program. String literals, null objects and
167
+ // / precise access path external values sets are not included in the output.
168
+ // / \param query: input expression
169
+ // / \param ns: namespace
170
+ // / \param lvsa: the output of LVSA, to work out what `query` might point to
171
+ // / \param instit: the point in the program to do the query
172
+ // / \param [out] result: output
165
173
static void collect_lvsa_access_paths (
166
- exprt const & query_in ,
167
- namespacet const & ns,
168
- local_value_set_analysist& lvsa,
169
- instruction_iteratort const & instit,
174
+ exprt const &query ,
175
+ namespacet const & ns,
176
+ local_value_set_analysist & lvsa,
177
+ instruction_iteratort const & instit,
170
178
std::set<exprt> &result)
171
179
{
172
180
TMPROF_BLOCK ();
173
181
174
- if (query_in .id ()== ID_side_effect)
182
+ if (query .id () == ID_side_effect)
175
183
{
176
- side_effect_exprt const see= to_side_effect_expr (query_in );
184
+ side_effect_exprt const & see = to_side_effect_expr (query );
177
185
if (see.get_statement ()==ID_nondet)
178
186
{
179
187
// TODO(marek-trtik): Add computation of a proper points-to set for NONDET
180
188
// in a side-effect expression
181
- assert (false );
182
189
}
183
190
}
184
191
185
- const exprt* query=&query_in;
186
- while (query->id ()==ID_typecast)
187
- query=&query->op0 ();
188
- const exprt& e = *query;
189
-
190
- if (e.id ()==ID_symbol ||
191
- e.id ()==ID_index ||
192
- e.id ()==ID_member ||
193
- e.id ()==ID_dereference)
192
+ if (
193
+ query.id () == ID_symbol || query.id () == ID_index ||
194
+ query.id () == ID_member || query.id () == ID_dereference)
194
195
{
195
196
value_setst::valuest referees;
196
- lvsa.get_values_reconstructed (instit,address_of_exprt (e), referees);
197
+ lvsa.get_values_reconstructed (instit, address_of_exprt (query), referees);
197
198
for (const auto & target : referees)
198
199
{
199
200
if (target.id ()==ID_unknown)
@@ -230,7 +231,7 @@ static void collect_lvsa_access_paths(
230
231
}
231
232
else
232
233
{
233
- forall_operands (it,e )
234
+ forall_operands (it, query )
234
235
collect_lvsa_access_paths (
235
236
*it,
236
237
ns,
@@ -240,6 +241,8 @@ static void collect_lvsa_access_paths(
240
241
}
241
242
}
242
243
244
+ // / Call `collect_lvsa_access_paths` and use taint_object_numbering to convert
245
+ // / the results from `exprt`s to the format required for `lvalue_numbers_sett`
243
246
static void collect_lvsa_access_paths (
244
247
exprt const & query_in,
245
248
namespacet const & ns,
@@ -361,52 +364,20 @@ exprt dereference_if_pointer(exprt expr)
361
364
return expr;
362
365
}
363
366
364
- // / \brief Checks whether the passed expression represents an up cast to a
365
- // / parent.
366
- // / \param expr: The examined expression.
367
- // / \param hierarchy: The class heierarchy used for checking parent-child
368
- // / relation.
369
- // / \param ns: A namespace; the 'follow' method is needed.
370
- // / \return True, if 'expr' is an up cast, and false otherwise.
371
- bool is_parent_member_access (
372
- const member_exprt &expr,
373
- const class_hierarchyt &hierarchy,
374
- const namespacet &ns)
375
- {
376
- if (expr.get_component_number () != 0UL )
377
- return false ;
378
- const typet &parent_type = ns.follow (expr.type ());
379
- if (parent_type.id () != ID_struct)
380
- return false ;
381
- const typet &child_type = ns.follow (expr.compound ().type ());
382
- INVARIANT (child_type.id () == ID_struct, " Compound of member_exprt is struct" );
383
- const std::string parent_name =
384
- " java::" + as_string (to_struct_type (parent_type).get_tag ());
385
- const std::string child_name =
386
- " java::" + as_string (to_struct_type (child_type).get_tag ());
387
- const auto it = hierarchy.class_map .find (parent_name);
388
- if (it == hierarchy.class_map .cend ())
389
- return false ;
390
- for (const auto &child : it->second .children )
391
- if (child == child_name)
392
- return true ;
393
- return false ;
394
- }
395
-
396
367
// / \brief An extended version of the original LVSA utility function
397
368
// / 'collect_lvsa_access_paths'. Namely, when the original function
398
369
// / returns an empty set, then the extended one introduces a fresh
399
- // / EVS object for the passed (and dereferenced) expression. For non-empy
370
+ // / EVS object for the passed (and dereferenced) expression. For non-empty
400
371
// / output from the original function it iterates over all retrieved
401
372
// / numbers and for each number representing an upcast (member_exprt) it calls
402
373
// / itself in order to retrieve numbers also to parent accesses. This is because
403
374
// / an upcast is represented in LVSA by one number and we also need LVSA
404
375
// / number(s) of the actual parent object.
405
- // / \param expr: The expression whose dereference is passed to LVSA.
406
- // / \param it: The current program location (instruction iteratior )
376
+ // / \param expr: The expression to look up in LVSA.
377
+ // / \param it: The current program location (instruction iterator )
407
378
// / \param lvsa: The LVSA analysis.
408
379
// / \param result: The resulting points-to set.
409
- // / \return True, if the resulting points-to set is definitelly singular, and
380
+ // / \return True, if the resulting points-to set is definitely singular, and
410
381
// / false otherwise.
411
382
bool taint_algorithm_computing_summary_of_functiont::
412
383
collect_lvsa_access_paths_extended (
@@ -419,7 +390,8 @@ bool taint_algorithm_computing_summary_of_functiont::
419
390
TMPROF_BLOCK ();
420
391
421
392
bool singular = false ;
422
- const exprt query_expr = dereference_if_pointer (expr);
393
+ const exprt query_expr =
394
+ dereference_if_pointer (remove_casts (expr, program->get_namespace ()));
423
395
lvalue_numbers_sett raw_result;
424
396
collect_lvsa_access_paths (
425
397
query_expr,
@@ -454,11 +426,7 @@ bool taint_algorithm_computing_summary_of_functiont::
454
426
const exprt &raw_expr = numbering->at (raw_number);
455
427
if (auto member_expr = expr_try_dynamic_cast<member_exprt>(raw_expr))
456
428
{
457
- if (
458
- is_parent_member_access (
459
- *member_expr,
460
- program->get_class_hierarchy (),
461
- program->get_namespace ()))
429
+ if (is_parent_member_access (*member_expr, program->get_namespace ()))
462
430
{
463
431
if (
464
432
!collect_lvsa_access_paths_extended (
@@ -1202,7 +1170,7 @@ numbered_lvalue_to_taint_mapt taint_algorithm_computing_summary_of_functiont::
1202
1170
std::to_string (propagation_rule.get_id ()),
1203
1171
" Although a propagation rule " +
1204
1172
std::to_string (propagation_rule.get_id ()) +
1205
- " was found, it was NOT applied, because the symbolic value "
1173
+ " was found, it was NOT applied, because the symbolic value "
1206
1174
" to be assigned is actually BOTTOM." });
1207
1175
}
1208
1176
else
0 commit comments