From 830593671eb33a318f7fa35e2f778d7b3facc445 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 7 Mar 2022 22:19:59 +0000 Subject: [PATCH] Program dependence graph: track SET_RETURN_VALUE instruction We did track a dependency from END_FUNCTION towards the call site when a return value was being assigned, but failed to keep track of the data dependency between SET_RETURN_VALUE and END_FUNCTION. Also clean up commented-out code that used to handle return values, but has since been superseded. --- regression/cbmc/return3/full-slice.desc | 8 +++++ src/analyses/dependence_graph.cpp | 18 +++++++++++ src/analyses/dependence_graph.h | 14 +++++++++ src/analyses/reaching_definitions.cpp | 41 ------------------------- 4 files changed, 40 insertions(+), 41 deletions(-) create mode 100644 regression/cbmc/return3/full-slice.desc diff --git a/regression/cbmc/return3/full-slice.desc b/regression/cbmc/return3/full-slice.desc new file mode 100644 index 00000000000..3793f7374e1 --- /dev/null +++ b/regression/cbmc/return3/full-slice.desc @@ -0,0 +1,8 @@ +CORE +main.c +--full-slice +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp index f442d365bc9..c57bdeb7289 100644 --- a/src/analyses/dependence_graph.cpp +++ b/src/analyses/dependence_graph.cpp @@ -188,6 +188,24 @@ void dep_graph_domaint::data_dependencies( dep_graph.reaching_definitions()[to].clear_cache(read_object_entry.first); } + + if(to->is_set_return_value()) + { + auto entry = dep_graph.end_function_map.find(function_to); + CHECK_RETURN(entry != dep_graph.end_function_map.end()); + + goto_programt::const_targett end_function = entry->second; + + dep_graph_domaint *s = + dynamic_cast(&(dep_graph.get_state(end_function))); + CHECK_RETURN(s != nullptr); + + if(s->is_bottom()) + s->has_values = tvt::unknown(); + + if(s->data_deps.insert(to).second) + s->has_changed = true; + } } void dep_graph_domaint::transform( diff --git a/src/analyses/dependence_graph.h b/src/analyses/dependence_graph.h index d3f150b84b9..dadf90638dd 100644 --- a/src/analyses/dependence_graph.h +++ b/src/analyses/dependence_graph.h @@ -224,6 +224,16 @@ class dependence_grapht: { ait::initialize(goto_functions); rd(goto_functions, ns); + + for(const auto &entry : goto_functions.function_map) + { + const goto_programt &goto_program = entry.second.body; + if(!goto_program.empty()) + { + end_function_map.emplace( + entry.first, std::prev(goto_program.instructions.end())); + } + } } void initialize(const irep_idt &function, const goto_programt &goto_program) @@ -238,6 +248,9 @@ class dependence_grapht: { cfg_post_dominatorst &pd = post_dominators[function]; pd(goto_program); + + end_function_map.emplace( + function, std::prev(goto_program.instructions.end())); } } @@ -273,6 +286,7 @@ class dependence_grapht: post_dominators_mapt post_dominators; reaching_definitions_analysist rd; + std::map end_function_map; }; #endif // CPROVER_ANALYSES_DEPENDENCE_GRAPH_H diff --git a/src/analyses/reaching_definitions.cpp b/src/analyses/reaching_definitions.cpp index cf6e3be40a0..ab97e79f957 100644 --- a/src/analyses/reaching_definitions.cpp +++ b/src/analyses/reaching_definitions.cpp @@ -126,41 +126,6 @@ void rd_range_domaint::transform( // initial (non-deterministic) value else if(from->is_decl()) transform_assign(ns, from, function_from, from, *rd); - -#if 0 - // handle return values - if(to->is_function_call()) - { - const code_function_callt &code=to_code_function_call(to->code); - - if(code.lhs().is_not_nil()) - { - rw_range_set_value_sett rw_set(ns, rd->get_value_sets()); - goto_rw(to, rw_set); - const bool is_must_alias=rw_set.get_w_set().size()==1; - - for(const auto &written_object_entry : rw_set.get_w_set()) - { - const irep_idt &identifier = written_object_entry.first; - // ignore symex::invalid_object - const symbolt *symbol_ptr; - if(ns.lookup(identifier, symbol_ptr)) - continue; - assert(symbol_ptr!=0); - - const range_domaint &ranges = - rw_set.get_ranges(written_object_entry.second); - - if(is_must_alias && - (!rd->get_is_threaded()(from) || - (!symbol_ptr->is_shared() && - !rd->get_is_dirty()(identifier)))) - for(const auto &range : ranges) - kill(identifier, range.first, range.second); - } - } - } -#endif } /// Computes an instance obtained from a `*this` by transformation over `DEAD v` @@ -322,12 +287,6 @@ void rd_range_domaint::transform_end_function( // handle return values if(call->call_lhs().is_not_nil()) { -#if 0 - rd_range_domaint *rd_state= - dynamic_cast(&(rd.get_state(call))); - assert(rd_state!=0); - rd_state-> -#endif transform_assign(ns, from, function_to, call, rd); } }