diff --git a/regression/goto-analyzer/dependence-graph13/main.c b/regression/goto-analyzer/dependence-graph13/main.c new file mode 100644 index 00000000000..d01d8203a7a --- /dev/null +++ b/regression/goto-analyzer/dependence-graph13/main.c @@ -0,0 +1,12 @@ +void bar(int a, int b) +{ + int result = b; +} + +void main() +{ + int a = 1; + int b = 2; + int c = 3; + bar(a, b + c); +} diff --git a/regression/goto-analyzer/dependence-graph13/test.desc b/regression/goto-analyzer/dependence-graph13/test.desc new file mode 100644 index 00000000000..f1e80bc28a2 --- /dev/null +++ b/regression/goto-analyzer/dependence-graph13/test.desc @@ -0,0 +1,26 @@ +CORE +main.c +--dependence-graph --show +activate-multi-line-match +^EXIT=0$ +^SIGNAL=0$ +\/\/ ([0-9]+).*\n.*b = 2;(.*\n)*Data dependencies: (([0-9]+,\1)|(\1,[0-9]+))\n(.*\n){2,3}.*result = b +\/\/ ([0-9]+).*\n.*c = 3;(.*\n)*Data dependencies: (([0-9]+,\1)|(\1,[0-9]+))\n(.*\n){2,3}.*result = b +-- +^warning: ignoring +-- + +The two regular expressions above match output portions like shown below (with + being a location number). The intention is to check whether a function +parameter in the callee correctly depends on the caller-provided argument. + + // 3 file main.c line 11 function main + b = 2; +... +**** 12 file main.c line 5 function bar +Data dependencies: (,...)|(...,) + + // 12 file main.c line 5 function bar + result = b; + +The second regex matches for c. diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp index e047991b8bf..a947334cc8a 100644 --- a/src/analyses/goto_rw.cpp +++ b/src/analyses/goto_rw.cpp @@ -493,6 +493,23 @@ void rw_range_sett::add( static_cast(*entry->second).push_back( {range_start, range_end}); + + // add to the single expression read set + if(mode == get_modet::READ && expr_r_range_set.has_value()) + { + objectst::iterator expr_entry = + expr_r_range_set + ->insert( + std::pair>( + identifier, nullptr)) + .first; + + if(expr_entry->second == nullptr) + expr_entry->second = util_make_unique(); + + static_cast(*expr_entry->second) + .push_back({range_start, range_end}); + } } void rw_range_sett::get_objects_rec( diff --git a/src/analyses/goto_rw.h b/src/analyses/goto_rw.h index 49ce2de73c7..d191d1bd4f5 100644 --- a/src/analyses/goto_rw.h +++ b/src/analyses/goto_rw.h @@ -121,8 +121,7 @@ class rw_range_sett virtual ~rw_range_sett(); - explicit rw_range_sett(const namespacet &_ns): - ns(_ns) + explicit rw_range_sett(const namespacet &_ns) : ns(_ns) { } @@ -136,6 +135,21 @@ class rw_range_sett return w_range_set; } + /// Enable maintaining a read set for a single expression + void enable_expr_read_set() + { + expr_r_range_set = objectst{}; + } + + /// Obtain the read set for a single expression. Requires a prior call to + /// \ref enable_expr_read_set. + objectst fetch_expr_read_set() + { + objectst result = std::move(*expr_r_range_set); + expr_r_range_set.reset(); + return result; + } + const range_domaint &get_ranges(objectst::const_iterator it) const { PRECONDITION(dynamic_cast(it->second.get())!=nullptr); @@ -167,6 +181,7 @@ class rw_range_sett const namespacet &ns; objectst r_range_set, w_range_set; + optionalt expr_r_range_set; virtual void get_objects_rec( get_modet mode, diff --git a/src/analyses/reaching_definitions.cpp b/src/analyses/reaching_definitions.cpp index 6912385a90a..b475f2b961d 100644 --- a/src/analyses/reaching_definitions.cpp +++ b/src/analyses/reaching_definitions.cpp @@ -211,22 +211,33 @@ void rd_range_domaint::transform_function_call( ++it; } - const symbol_exprt &fn_symbol_expr=to_symbol_expr(code.function()); - const code_typet &code_type= - to_code_type(ns.lookup(fn_symbol_expr.get_identifier()).type); + rw_range_set_value_sett rw_set(ns, rd.get_value_sets()); - for(const auto ¶m : code_type.parameters()) + const code_typet &code_type = to_code_type(ns.lookup(function_to).type); + PRECONDITION(code_type.parameters().size() == code.arguments().size()); + auto arg_it = code.arguments().begin(); + for(const auto ¶meter : code_type.parameters()) { - const irep_idt &identifier=param.get_identifier(); + const irep_idt &identifier = parameter.get_identifier(); - if(identifier.empty()) - continue; + // get read set of the argument + rw_set.enable_expr_read_set(); + rw_set.get_objects_rec( + function_from, from, rw_range_sett::get_modet::READ, *arg_it); - auto param_bits = pointer_offset_bits(param.type(), ns); - if(param_bits.has_value()) - gen(from, identifier, 0, to_range_spect(*param_bits)); - else - gen(from, identifier, 0, -1); + for(const auto &r_set_pair : rw_set.fetch_expr_read_set()) + { + const rd_range_domaint::ranges_at_loct &w_ranges = + rd[from].get(r_set_pair.first); + for(const auto &w_range : w_ranges) + { + for(const auto &wr : w_range.second) + gen(w_range.first, identifier, wr.first, wr.second); + } + } + + // next argument/parameter pair + ++arg_it; } } else