@@ -358,21 +358,32 @@ symbol_exprt find_or_create_symbol_expr(
358
358
return symbol_ptr->symbol_expr ();
359
359
}
360
360
361
+ // / \brief If the passed expression in a non-null pointer expression, then
362
+ // / the dereference expression is returned. Otherwise the original expression
363
+ // / is returned.
364
+ // / \param expr: The expression to be dereferenced, if it is non-null pointer.
365
+ // / \return See 'brief' section.
361
366
exprt dereference_if_pointer (exprt expr)
362
367
{
363
- if (expr.type ().id () == ID_pointer)
364
- {
365
- if (expr.id () == ID_typecast)
366
- return dereference_if_pointer (expr.op0 ());
367
- // Based on experimentation, it looks like the similar IDs:
368
- // ID_nullptr, ID_null, and ID_null_object
369
- // are not used in this context. I.e. ID_NULL suffices for the check.
370
- if (!(expr.is_constant () && to_constant_expr (expr).get_value () == ID_NULL))
371
- return dereference_exprt (expr);
372
- }
368
+ if (expr.type ().id () != ID_pointer)
369
+ return expr;
370
+ if (expr.id () == ID_typecast)
371
+ return dereference_if_pointer (expr.op0 ());
372
+ // Based on experimentation, it looks like the similar IDs:
373
+ // ID_nullptr, ID_null, and ID_null_object
374
+ // are not used in this context. I.e. ID_NULL suffices for the check.
375
+ if (!(expr.is_constant () && to_constant_expr (expr).get_value () == ID_NULL))
376
+ return dereference_exprt (expr);
373
377
return expr;
374
378
}
375
379
380
+ // / \brief Checks whether the passed expression represents an up cast to a
381
+ // / parent.
382
+ // / \param expr: The examined expression.
383
+ // / \param hierarchy: The class heierarchy used for checking parent-child
384
+ // / relation.
385
+ // / \param ns: A namespace; the 'follow' method is needed.
386
+ // / \return True, if 'expr' is an up cast, and false otherwise.
376
387
bool is_parent_member_access (
377
388
const member_exprt &expr,
378
389
const class_hierarchyt &hierarchy,
@@ -384,8 +395,7 @@ bool is_parent_member_access(
384
395
if (parent_type.id () != ID_struct)
385
396
return false ;
386
397
const typet &child_type = ns.follow (expr.compound ().type ());
387
- if (child_type.id () != ID_struct)
388
- return false ;
398
+ INVARIANT (child_type.id () == ID_struct, " Compound of member_exprt is struct" );
389
399
const std::string parent_name =
390
400
" java::" + as_string (to_struct_type (parent_type).get_tag ());
391
401
const std::string child_name =
@@ -399,8 +409,23 @@ bool is_parent_member_access(
399
409
return false ;
400
410
}
401
411
412
+ // / \brief An extended version of the original LVSA utility function
413
+ // / 'collect_lvsa_access_paths'. Namely, when the original function
414
+ // / returns an empty set, then the extended one introduces a fresh
415
+ // / EVS object for the passed (and dereferenced) expression. For non-empy
416
+ // / output from the original function it iterates over all retrieved
417
+ // / numbers and for each number representing an upcast (member_exprt) it calls
418
+ // / itself in order to retrieve numbers also to parent accesses. This is because
419
+ // / an upcast is represented in LVSA by one number and we also need LVSA
420
+ // / number(s) of the actual parent object.
421
+ // / \param expr: The expression whose dereference is passed to LVSA.
422
+ // / \param it: The current program location (instruction iteratior)
423
+ // / \param lvsa: The LVSA analysis.
424
+ // / \param result: The resulting points-to set.
425
+ // / \return True, if the resulting points-to set is definitelly singular, and
426
+ // / false otherwise.
402
427
bool taint_algorithm_computing_summary_of_functiont::
403
- collect_lvsa_access_paths_ex (
428
+ collect_lvsa_access_paths_extended (
404
429
const exprt &expr,
405
430
const instruction_iteratort &it,
406
431
local_value_set_analysist &lvsa,
@@ -423,7 +448,7 @@ bool taint_algorithm_computing_summary_of_functiont::
423
448
{
424
449
external_value_set_exprt new_lhs (
425
450
query_expr.type (),
426
- constant_exprt (" external_objects " , string_typet ()),
451
+ constant_exprt (" " , string_typet ()),
427
452
external_value_set_typet::ROOT_OBJECT,
428
453
false );
429
454
// Use access path "[]" to dereference the pointer
@@ -446,9 +471,11 @@ bool taint_algorithm_computing_summary_of_functiont::
446
471
program->get_namespace ()))
447
472
{
448
473
if (
449
- !collect_lvsa_access_paths_ex (
474
+ !collect_lvsa_access_paths_extended (
450
475
member_expr->compound (), it, lvsa, result))
476
+ {
451
477
singular = false ;
478
+ }
452
479
}
453
480
}
454
481
result.insert (raw_number);
@@ -629,7 +656,7 @@ void taint_algorithm_computing_summary_of_functiont::
629
656
630
657
assert (param_idx<fn_call.arguments ().size ());
631
658
632
- collect_lvsa_access_paths_ex (
659
+ collect_lvsa_access_paths_extended (
633
660
fn_call.arguments ().at (param_idx), Iit, lvsa, argument_lvalues);
634
661
}
635
662
else
@@ -651,7 +678,7 @@ void taint_algorithm_computing_summary_of_functiont::
651
678
{
652
679
for (const auto param_index : it->second )
653
680
{
654
- collect_lvsa_access_paths_ex (
681
+ collect_lvsa_access_paths_extended (
655
682
fn_call.arguments ().at (param_index), Iit, lvsa, resolved_lvalues);
656
683
}
657
684
}
@@ -687,11 +714,7 @@ void taint_algorithm_computing_summary_of_functiont::
687
714
for (const std::pair<taint_lvalue_numbert, taint_sett> &lvalue_taint :
688
715
summary->get_output ())
689
716
{
690
- const auto &lvalue=numbering->at (lvalue_taint.first );
691
- if (lvalue.is_nil ())
692
- continue ;
693
717
lvalue_numbers_sett argument_lvalues;
694
- if (symbol_utilst (program->get_namespace ()).is_parameter (lvalue))
695
718
{
696
719
const auto it = summary->get_map_output_lvalues_to_param_indices ().find (
697
720
lvalue_taint.first );
@@ -701,7 +724,7 @@ void taint_algorithm_computing_summary_of_functiont::
701
724
{
702
725
for (const auto param_index : it->second )
703
726
{
704
- collect_lvsa_access_paths_ex (
727
+ collect_lvsa_access_paths_extended (
705
728
fn_call.arguments ().at (param_index), Iit, lvsa, argument_lvalues);
706
729
}
707
730
}
@@ -752,8 +775,8 @@ void taint_algorithm_computing_summary_of_functiont::initialise_domain(
752
775
if (it->type ==ASSIGN)
753
776
{
754
777
const code_assignt &asgn = to_code_assign (it->code );
755
- collect_lvsa_access_paths_ex (asgn.lhs (), it, lvsa, environment);
756
- collect_lvsa_access_paths_ex (asgn.lhs (), it, lvsa, written);
778
+ collect_lvsa_access_paths_extended (asgn.lhs (), it, lvsa, environment);
779
+ collect_lvsa_access_paths_extended (asgn.lhs (), it, lvsa, written);
757
780
if (asgn.rhs ().id ()==ID_side_effect)
758
781
{
759
782
const side_effect_exprt see=to_side_effect_expr (asgn.rhs ());
@@ -763,12 +786,8 @@ void taint_algorithm_computing_summary_of_functiont::initialise_domain(
763
786
program->get_NONDET_retvals_replacements ().find (it);
764
787
if (replace_it != program->get_NONDET_retvals_replacements ().cend ())
765
788
{
766
- const auto env_size = environment.size ();
767
- collect_lvsa_access_paths_ex (
789
+ collect_lvsa_access_paths_extended (
768
790
replace_it->second , it, lvsa, environment);
769
- if (env_size == environment.size ())
770
- collect_lvsa_access_paths_ex (
771
- replace_it->second , it, lvsa, environment);
772
791
}
773
792
else
774
793
{
@@ -778,10 +797,10 @@ void taint_algorithm_computing_summary_of_functiont::initialise_domain(
778
797
}
779
798
}
780
799
else
781
- collect_lvsa_access_paths_ex (asgn.rhs (), it, lvsa, environment);
800
+ collect_lvsa_access_paths_extended (asgn.rhs (), it, lvsa, environment);
782
801
}
783
802
else if (it->type == ASSERT)
784
- collect_lvsa_access_paths_ex (it->guard , it, lvsa, environment);
803
+ collect_lvsa_access_paths_extended (it->guard , it, lvsa, environment);
785
804
else if (it->type ==FUNCTION_CALL)
786
805
{
787
806
const code_function_callt &fn_call = to_code_function_call (it->code );
@@ -805,7 +824,7 @@ void taint_algorithm_computing_summary_of_functiont::initialise_domain(
805
824
// In the future we could be more precise about exactly which arguments
806
825
// are used in the rule.
807
826
for (const auto &arg : fn_call.arguments ())
808
- collect_lvsa_access_paths_ex (arg, it, lvsa, environment);
827
+ collect_lvsa_access_paths_extended (arg, it, lvsa, environment);
809
828
if (!database.contains (callee_id))
810
829
continue ;
811
830
}
@@ -829,7 +848,7 @@ void taint_algorithm_computing_summary_of_functiont::initialise_domain(
829
848
" Parameter symbol doesn't match?" );
830
849
const auto paramidx=
831
850
std::distance (fn_type.parameters ().begin (), findit);
832
- collect_lvsa_access_paths_ex (
851
+ collect_lvsa_access_paths_extended (
833
852
fn_call.arguments ()[paramidx], it, lvsa, environment);
834
853
}
835
854
else if (!symbol_utilst (program->get_namespace ()).is_parameter (
@@ -958,7 +977,7 @@ void taint_algorithm_computing_summary_of_functiont::handle_assignment(
958
977
asgn.rhs (), Iit, lvsa, input, a);
959
978
960
979
lvalue_numbers_sett lhs;
961
- if (collect_lvsa_access_paths_ex (asgn.lhs (), Iit, lvsa, lhs))
980
+ if (collect_lvsa_access_paths_extended (asgn.lhs (), Iit, lvsa, lhs))
962
981
{
963
982
// Singular implies that lhs has exactly one element,
964
983
// so we can access it directly
@@ -984,7 +1003,7 @@ taint_sett taint_algorithm_computing_summary_of_functiont::
984
1003
TMPROF_BLOCK ();
985
1004
986
1005
lvalue_numbers_sett numbers_of_aliases;
987
- collect_lvsa_access_paths_ex (lvalue, Iit, lvsa, numbers_of_aliases);
1006
+ collect_lvsa_access_paths_extended (lvalue, Iit, lvsa, numbers_of_aliases);
988
1007
taint_sett result;
989
1008
for (taint_lvalue_numbert lvalue_number : numbers_of_aliases)
990
1009
{
@@ -1014,7 +1033,7 @@ void taint_algorithm_computing_summary_of_functiont::
1014
1033
1015
1034
lvalue_numbers_sett numbers_of_aliases;
1016
1035
bool singular =
1017
- collect_lvsa_access_paths_ex (lvalue, Iit, lvsa, numbers_of_aliases);
1036
+ collect_lvsa_access_paths_extended (lvalue, Iit, lvsa, numbers_of_aliases);
1018
1037
if (singular || (is_allowed_pure_assignment && numbers_of_aliases.size () == 1 ))
1019
1038
{
1020
1039
// Singular implies that lhs has exactly one element,
@@ -1070,7 +1089,7 @@ numbered_lvalue_to_taint_mapt taint_algorithm_computing_summary_of_functiont::
1070
1089
replace_it->second , Iit, lvsa, input, a);
1071
1090
1072
1091
lvalue_numbers_sett numbers_of_aliases;
1073
- collect_lvsa_access_paths_ex (
1092
+ collect_lvsa_access_paths_extended (
1074
1093
replace_it->second , Iit, lvsa, numbers_of_aliases);
1075
1094
assert (!numbers_of_aliases.empty ());
1076
1095
std::stringstream sstr;
@@ -1093,7 +1112,7 @@ numbered_lvalue_to_taint_mapt taint_algorithm_computing_summary_of_functiont::
1093
1112
sstr.str ()});
1094
1113
1095
1114
lvalue_numbers_sett lhs;
1096
- collect_lvsa_access_paths_ex (asgn.lhs (), Iit, lvsa, lhs);
1115
+ collect_lvsa_access_paths_extended (asgn.lhs (), Iit, lvsa, lhs);
1097
1116
for (const auto & path : lhs)
1098
1117
{
1099
1118
if (lhs.size () > 1UL )
@@ -1584,11 +1603,11 @@ void taint_algorithm_computing_summary_of_functiont::
1584
1603
program->get_functions ().function_map .at (fn_id);
1585
1604
const code_typet &fn_type = to_code_type (func_ref.type );
1586
1605
const auto fn_end_iter = std::prev (fn_to_summarise.body .instructions .cend ());
1587
- for (std::size_t i = 0UL , n = fn_type.parameters ().size (); i != n ; ++i)
1606
+ for (std::size_t i = 0UL ; i ! = fn_type.parameters ().size (); ++i)
1588
1607
{
1589
1608
const code_typet::parametert ¶m = fn_type.parameters ().at (i);
1590
1609
lvalue_numbers_sett numbers;
1591
- collect_lvsa_access_paths_ex (param, fn_end_iter, lvsa, numbers);
1610
+ collect_lvsa_access_paths_extended (param, fn_end_iter, lvsa, numbers);
1592
1611
for (const auto number : numbers)
1593
1612
{
1594
1613
if (summary.output .count (number) != 0UL )
0 commit comments