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 &); 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..30b97108776 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; @@ -161,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, @@ -207,6 +215,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, 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)); + } + } + } + } + } +}