From e03b0cb464a27fc465724d2544d4e8236394825f Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Fri, 10 Nov 2017 15:45:59 +0000 Subject: [PATCH 1/3] Abstract interpreter: add finalize hook At least dependence_grapht has good reason to do work at the end of the day-- namely to create an alternative data representation that is trickier to keep up to date incrementally than to produce in one go at the end. It seems likely other AIs will have use for a post-fixedpoint hook. --- src/analyses/ai.cpp | 5 +++++ src/analyses/ai.h | 7 +++++++ 2 files changed, 12 insertions(+) diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp index c70206a41ad..dedb2da9a3c 100644 --- a/src/analyses/ai.cpp +++ b/src/analyses/ai.cpp @@ -280,6 +280,11 @@ void ai_baset::initialize(const goto_functionst &goto_functions) initialize(it->second); } +void ai_baset::finalize() +{ + // Nothing to do per default +} + ai_baset::locationt ai_baset::get_next( working_sett &working_set) { diff --git a/src/analyses/ai.h b/src/analyses/ai.h index 1cecf984953..a09e43f699f 100644 --- a/src/analyses/ai.h +++ b/src/analyses/ai.h @@ -133,6 +133,7 @@ class ai_baset initialize(goto_program); entry_state(goto_program); fixedpoint(goto_program, goto_functions, ns); + finalize(); } void operator()( @@ -142,6 +143,7 @@ class ai_baset initialize(goto_functions); entry_state(goto_functions); fixedpoint(goto_functions, ns); + finalize(); } void operator()(const goto_modelt &goto_model) @@ -150,6 +152,7 @@ class ai_baset initialize(goto_model.goto_functions); entry_state(goto_model.goto_functions); fixedpoint(goto_model.goto_functions, ns); + finalize(); } void operator()( @@ -160,6 +163,7 @@ class ai_baset initialize(goto_function); entry_state(goto_function.body); fixedpoint(goto_function.body, goto_functions, ns); + finalize(); } /// Returns the abstract state before the given instruction @@ -264,6 +268,9 @@ class ai_baset virtual void initialize(const goto_functionst::goto_functiont &); virtual void initialize(const goto_functionst &); + // override to add a cleanup step after fixedpoint has run + virtual void finalize(); + void entry_state(const goto_programt &); void entry_state(const goto_functionst &); From 1abc75ed321313e1524219be90947a8cb25da4ca Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Fri, 10 Nov 2017 15:47:38 +0000 Subject: [PATCH 2/3] Dependence graph: ensure grapht representation is consistent with domain Previously the grapht representation was incrementally populated at the same time as the domain representation was computed, but at least one case (control dependencies crossing function callsites) was missing, leading to inconsistency, and doing it this way invites future similar mistakes. Instead, this commit switches to generating the grapht representation in one go after the AI fixedpoint has been computed. --- src/analyses/dependence_graph.cpp | 23 ++++++++++------------- src/analyses/dependence_graph.h | 11 +++++++++++ 2 files changed, 21 insertions(+), 13 deletions(-) diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp index 9707f9a3eb9..5f1bae158bc 100644 --- a/src/analyses/dependence_graph.cpp +++ b/src/analyses/dependence_graph.cpp @@ -120,10 +120,6 @@ void dep_graph_domaint::control_dependencies( it=next; } - - // add edges to the graph - for(const auto &c_dep : control_deps) - dep_graph.add_dep(dep_edget::kindt::CTRL, c_dep, to); } static bool may_be_def_use_pair( @@ -185,15 +181,6 @@ void dep_graph_domaint::data_dependencies( dep_graph.reaching_definitions()[to].clear_cache(it->first); } - - // add edges to the graph - for(const auto &d_dep : data_deps) - { - // *it might be handled in a future call call to visit only, - // depending on the sequence of successors; make sure it exists - dep_graph.get_state(d_dep); - dep_graph.add_dep(dep_edget::kindt::DATA, d_dep, to); - } } void dep_graph_domaint::transform( @@ -326,3 +313,13 @@ void dependence_grapht::add_dep( nodes[n_from].out[n_to].add(kind); nodes[n_to].in[n_from].add(kind); } + +void dep_graph_domaint::populate_dep_graph( + dependence_grapht &dep_graph, goto_programt::const_targett this_loc) const +{ + for(const auto &c_dep : control_deps) + dep_graph.add_dep(dep_edget::kindt::CTRL, c_dep, this_loc); + + for(const auto &d_dep : data_deps) + dep_graph.add_dep(dep_edget::kindt::DATA, d_dep, this_loc); +} diff --git a/src/analyses/dependence_graph.h b/src/analyses/dependence_graph.h index 2508174b443..9497b870255 100644 --- a/src/analyses/dependence_graph.h +++ b/src/analyses/dependence_graph.h @@ -154,6 +154,9 @@ class dep_graph_domaint:public ai_domain_baset return node_id; } + void populate_dep_graph( + dependence_grapht &, goto_programt::const_targett) const; + private: tvt has_values; node_indext node_id; @@ -207,6 +210,14 @@ class dependence_grapht: } } + void finalize() + { + for(const auto &location_state : state_map) + { + location_state.second.populate_dep_graph(*this, location_state.first); + } + } + void add_dep( dep_edget::kindt kind, goto_programt::const_targett from, From a59dea60c6d7cc7eddd551f150e53932735e6f61 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Sun, 12 Nov 2017 09:57:09 +0000 Subject: [PATCH 3/3] Add unit test checking dependence graph consistency This ensures that the dependence graph's internal representation has been accurately transcribed to its grapht external interface, and exposes the particular case of control dependencies being preserved across callsites. --- src/analyses/dependence_graph.h | 5 + unit/analyses/dependence_graph.cpp | 158 +++++++++++++++++++++++++++++ 2 files changed, 163 insertions(+) create mode 100644 unit/analyses/dependence_graph.cpp diff --git a/src/analyses/dependence_graph.h b/src/analyses/dependence_graph.h index 9497b870255..30b97108776 100644 --- a/src/analyses/dependence_graph.h +++ b/src/analyses/dependence_graph.h @@ -164,6 +164,11 @@ class dep_graph_domaint:public ai_domain_baset typedef std::set depst; depst control_deps, data_deps; + friend const depst & + dependence_graph_test_get_control_deps(const dep_graph_domaint &); + friend const depst & + dependence_graph_test_get_data_deps(const dep_graph_domaint &); + void control_dependencies( goto_programt::const_targett from, goto_programt::const_targett to, diff --git a/unit/analyses/dependence_graph.cpp b/unit/analyses/dependence_graph.cpp new file mode 100644 index 00000000000..6a499be1a76 --- /dev/null +++ b/unit/analyses/dependence_graph.cpp @@ -0,0 +1,158 @@ +/*******************************************************************\ + +Module: Unit test for dependence_graph.h + +Author: Chris Smowton, chris.smowton@diffblue.com + +\*******************************************************************/ + +#include + +#include +#include +#include +#include +#include +#include +#include +#include +#include + +static symbolt create_void_function_symbol( + const irep_idt &name, + const codet &code) +{ + code_typet void_function_type; + symbolt function; + function.name = name; + function.type = void_function_type; + function.mode = ID_java; + function.value = code; + return function; +} + +const std::set& + dependence_graph_test_get_control_deps(const dep_graph_domaint &domain) +{ + return domain.control_deps; +} + +const std::set& + dependence_graph_test_get_data_deps(const dep_graph_domaint &domain) +{ + return domain.data_deps; +} + +SCENARIO("dependence_graph", "[core][analyses][dependence_graph]") +{ + GIVEN("A call under a control dependency") + { + // Create code like: + // void __CPROVER__start() { + // int x; + // if(NONDET(int) == 0) { + // b(); + // x = 1; + // } + // } + // void b() { } + + register_language(new_java_bytecode_language); + + goto_modelt goto_model; + namespacet ns(goto_model.symbol_table); + + typet int_type = signed_int_type(); + + symbolt x_symbol; + x_symbol.name = id2string(goto_functionst::entry_point()) + "::x"; + x_symbol.base_name = "x"; + x_symbol.type = int_type; + x_symbol.is_lvalue = true; + x_symbol.is_state_var = true; + x_symbol.is_thread_local = true; + x_symbol.is_file_local = true; + goto_model.symbol_table.add(x_symbol); + + code_typet void_function_type; + + code_blockt a_body; + code_declt declare_x(x_symbol.symbol_expr()); + a_body.move_to_operands(declare_x); + + code_ifthenelset if_block; + + if_block.cond() = + equal_exprt( + side_effect_expr_nondett(int_type), + from_integer(0, int_type)); + + code_blockt then_block; + code_function_callt call; + call.function() = symbol_exprt("b", void_function_type); + then_block.move_to_operands(call); + code_assignt assign_x( + x_symbol.symbol_expr(), from_integer(1, int_type)); + then_block.move_to_operands(assign_x); + + if_block.then_case() = then_block; + + a_body.move_to_operands(if_block); + + goto_model.symbol_table.add( + create_void_function_symbol(goto_functionst::entry_point(), a_body)); + goto_model.symbol_table.add( + create_void_function_symbol("b", code_skipt())); + + stream_message_handlert msg(std::cerr); + goto_convert(goto_model, msg); + + WHEN("Constructing a dependence graph") + { + dependence_grapht dep_graph(ns); + dep_graph(goto_model.goto_functions, ns); + + THEN("The function call and assignment instructions " + "should have a control dependency") + { + for(std::size_t node_idx = 0; node_idx < dep_graph.size(); ++node_idx) + { + const dep_nodet &node = dep_graph[node_idx]; + const dep_graph_domaint &node_domain = dep_graph[node.PC]; + if(node.PC->is_assign() || node.PC->is_function_call()) + { + REQUIRE( + dependence_graph_test_get_control_deps(node_domain).size() == 1); + } + } + } + + THEN("The graph's domain and its grapht representation " + "should be consistent") + { + for(std::size_t node_idx = 0; node_idx < dep_graph.size(); ++node_idx) + { + const dep_nodet &node = dep_graph[node_idx]; + const dep_graph_domaint &node_domain = dep_graph[node.PC]; + const std::set &control_deps = + dependence_graph_test_get_control_deps(node_domain); + const std::set &data_deps = + dependence_graph_test_get_data_deps(node_domain); + + std::size_t domain_dep_count = + control_deps.size() + data_deps.size(); + + REQUIRE(domain_dep_count == node.in.size()); + + for(const auto &dep_edge : node.in) + { + if(dep_edge.second.get() == dep_edget::kindt::CTRL) + REQUIRE(control_deps.count(dep_graph[dep_edge.first].PC)); + else if(dep_edge.second.get() == dep_edget::kindt::DATA) + REQUIRE(data_deps.count(dep_graph[dep_edge.first].PC)); + } + } + } + } + } +}