diff --git a/regression/goto-instrument/aggressive_slicer1/main.c b/regression/goto-instrument/aggressive_slicer1/main.c new file mode 100644 index 00000000000..ded2b118a5c --- /dev/null +++ b/regression/goto-instrument/aggressive_slicer1/main.c @@ -0,0 +1,30 @@ +void D() +{ + __CPROVER_assert(0,""); +} + +void C() +{ + int nondet; + if(nondet) + D(); +} + +void B() +{ + C(); +}; + +int main() +{ + int nondet; + + __CPROVER_assume(nondet!=3); + switch(nondet) + { + case 1: B(); break; + case 3: C(); break; + default: break; + } +return 0; +} \ No newline at end of file diff --git a/regression/goto-instrument/aggressive_slicer1/test.desc b/regression/goto-instrument/aggressive_slicer1/test.desc new file mode 100644 index 00000000000..c10f611316f --- /dev/null +++ b/regression/goto-instrument/aggressive_slicer1/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--aggressive-slice +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring \ No newline at end of file diff --git a/regression/goto-instrument/aggressive_slicer2/main.c b/regression/goto-instrument/aggressive_slicer2/main.c new file mode 100644 index 00000000000..ded2b118a5c --- /dev/null +++ b/regression/goto-instrument/aggressive_slicer2/main.c @@ -0,0 +1,30 @@ +void D() +{ + __CPROVER_assert(0,""); +} + +void C() +{ + int nondet; + if(nondet) + D(); +} + +void B() +{ + C(); +}; + +int main() +{ + int nondet; + + __CPROVER_assume(nondet!=3); + switch(nondet) + { + case 1: B(); break; + case 3: C(); break; + default: break; + } +return 0; +} \ No newline at end of file diff --git a/regression/goto-instrument/aggressive_slicer2/test.desc b/regression/goto-instrument/aggressive_slicer2/test.desc new file mode 100644 index 00000000000..4e4584eb814 --- /dev/null +++ b/regression/goto-instrument/aggressive_slicer2/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--aggressive-slice --property D.assertion.1 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring \ No newline at end of file diff --git a/regression/goto-instrument/aggressive_slicer3/main.c b/regression/goto-instrument/aggressive_slicer3/main.c new file mode 100644 index 00000000000..db3ed7e203b --- /dev/null +++ b/regression/goto-instrument/aggressive_slicer3/main.c @@ -0,0 +1,29 @@ +void D() +{ + __CPROVER_assert(0,""); +} + +void C() +{ + int nondet; + if(nondet) + D(); +} + +void B() +{ + C(); +}; + +int main() +{ + int nondet; + + switch(nondet) + { + case 1: B(); break; + case 3: C(); break; + default: break; + } +return 0; +} \ No newline at end of file diff --git a/regression/goto-instrument/aggressive_slicer3/test.desc b/regression/goto-instrument/aggressive_slicer3/test.desc new file mode 100644 index 00000000000..a37279572b5 --- /dev/null +++ b/regression/goto-instrument/aggressive_slicer3/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--aggressive-slice +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring \ No newline at end of file diff --git a/regression/goto-instrument/aggressive_slicer4/main.c b/regression/goto-instrument/aggressive_slicer4/main.c new file mode 100644 index 00000000000..85d56f13603 --- /dev/null +++ b/regression/goto-instrument/aggressive_slicer4/main.c @@ -0,0 +1,29 @@ +void D() +{ + __CPROVER_assert(0,""); +} + +void C() +{ + int nondet; + if(nondet) + D(); +} + +void B() +{ + C(); +}; + +int main() +{ + int nondet; + __CPROVER_assume(nondet!=3); + switch(nondet) + { + case 1: B(); break; + case 3: C(); break; + default: break; + } +return 0; +} \ No newline at end of file diff --git a/regression/goto-instrument/aggressive_slicer4/test.desc b/regression/goto-instrument/aggressive_slicer4/test.desc new file mode 100644 index 00000000000..75d03f51c09 --- /dev/null +++ b/regression/goto-instrument/aggressive_slicer4/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--aggressive-slice --preserve-function B +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring \ No newline at end of file diff --git a/regression/goto-instrument/aggressive_slicer5/main.c b/regression/goto-instrument/aggressive_slicer5/main.c new file mode 100644 index 00000000000..f3bc92a8e9a --- /dev/null +++ b/regression/goto-instrument/aggressive_slicer5/main.c @@ -0,0 +1,29 @@ +void D() +{ + __CPROVER_assert(0,""); +} + +void C() +{ + int nondet; + if(nondet) + D(); +} + +void B() +{ + C(); +}; + +int main() +{ + int nondet; +__CPROVER_assume(nondet!=3); + switch(nondet) + { + case 1: B(); break; + case 3: C(); break; + default: break; + } +return 0; +} \ No newline at end of file diff --git a/regression/goto-instrument/aggressive_slicer5/test.desc b/regression/goto-instrument/aggressive_slicer5/test.desc new file mode 100644 index 00000000000..08c29c68d99 --- /dev/null +++ b/regression/goto-instrument/aggressive_slicer5/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--aggressive-slice --property D.assertion.1 --preserve-all-direct-paths +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring \ No newline at end of file diff --git a/regression/goto-instrument/aggressive_slicer6/main.c b/regression/goto-instrument/aggressive_slicer6/main.c new file mode 100644 index 00000000000..85d56f13603 --- /dev/null +++ b/regression/goto-instrument/aggressive_slicer6/main.c @@ -0,0 +1,29 @@ +void D() +{ + __CPROVER_assert(0,""); +} + +void C() +{ + int nondet; + if(nondet) + D(); +} + +void B() +{ + C(); +}; + +int main() +{ + int nondet; + __CPROVER_assume(nondet!=3); + switch(nondet) + { + case 1: B(); break; + case 3: C(); break; + default: break; + } +return 0; +} \ No newline at end of file diff --git a/regression/goto-instrument/aggressive_slicer6/test.desc b/regression/goto-instrument/aggressive_slicer6/test.desc new file mode 100644 index 00000000000..b40f55b4185 --- /dev/null +++ b/regression/goto-instrument/aggressive_slicer6/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--aggressive-slice --call-depth 1 +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring \ No newline at end of file diff --git a/src/analyses/Makefile b/src/analyses/Makefile index a63a4d4e1c6..8094a345251 100644 --- a/src/analyses/Makefile +++ b/src/analyses/Makefile @@ -22,6 +22,7 @@ SRC = ai.cpp \ locals.cpp \ natural_loops.cpp \ reaching_definitions.cpp \ + reachable_call_graph.cpp \ static_analysis.cpp \ uncaught_exceptions_analysis.cpp \ uninitialized_domain.cpp \ diff --git a/src/analyses/call_graph.cpp b/src/analyses/call_graph.cpp index 93850f64d1d..7b24e163ce1 100644 --- a/src/analyses/call_graph.cpp +++ b/src/analyses/call_graph.cpp @@ -7,7 +7,7 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ /// \file -/// Function Call Graphs +/// Function Call Graph #include "call_graph.h" @@ -51,50 +51,158 @@ void call_grapht::add( const irep_idt &caller, const irep_idt &callee) { - graph.insert(std::pair(caller, callee)); + std::size_t caller_idx = node_numbering.number(caller); + if(caller_idx >= nodes.size()) + { + node_indext node_index = add_node(); + nodes[node_index].function_name = caller; + } + + std::size_t callee_idx = node_numbering.number(callee); + if(callee_idx >= nodes.size()) + { + node_indext node_index = add_node(); + nodes[node_index].function_name = callee; + } + + add_edge(caller_idx, callee_idx); +} + + +void call_grapht::output_dot_node(std::ostream &out, node_indext n) const +{ + const nodet &node = nodes.at(n); + + for(const auto &edge : node.out) + { + out << " \"" << node.function_name << "\" -> " << "\"" + << nodes[edge.first].function_name << "\" " << " [arrowhead=\"vee\"];" + << "\n"; + } +} + +void call_grapht::output_xml_node(std::ostream &out, node_indext n) const +{ + const nodet &node = nodes.at(n); + + for(const auto &edge : node.out) + { + out << "\n"; + } +} + +void call_grapht::output_xml(std::ostream &out) const +{ + for(node_indext n = 0; n < nodes.size(); n++) + output_xml_node(out, n); } -/// Returns an inverted copy of this call graph -/// \return Inverted (callee -> caller) call graph call_grapht call_grapht::get_inverted() const { call_grapht result; - for(const auto &caller_callee : graph) - result.add(caller_callee.second, caller_callee.first); + for(const auto &n : nodes) + { + for(const auto &i : n.in) + result.add(n.function_name, nodes[i.first].function_name); + } return result; } -void call_grapht::output_dot(std::ostream &out) const +std::list call_grapht::shortest_function_path( + irep_idt src, irep_idt dest) { - out << "digraph call_graph {\n"; - - for(const auto &edge : graph) + std::list result; + node_indext src_idx, dest_idx; + if(!get_node_index(src, src_idx)) + throw "unable to find src function in call graph"; + if(!get_node_index(dest, dest_idx)) + throw "unable to find destination function in call graph"; + + patht path; + shortest_path(src_idx, dest_idx, path); + for(const auto &n : path) { - out << " \"" << edge.first << "\" -> " - << "\"" << edge.second << "\" " - << " [arrowhead=\"vee\"];" - << "\n"; + result.push_back(nodes[n].function_name); } - - out << "}\n"; + return result; } -void call_grapht::output(std::ostream &out) const +void call_grapht::reachable_within_n_steps( + std::size_t steps, + std::unordered_set & function_list) { - for(const auto &edge : graph) + std::list worklist; + + for(const auto &f : function_list) { - out << edge.first << " -> " << edge.second << "\n"; + node_indext start_index; + if(get_node_index(f, start_index)) + worklist.push_back(start_index); + else + throw "function not found in call graph"; + } + + // mark end of level 0 + worklist.push_back(std::numeric_limits::max()); + std::size_t depth=0; + + while(!worklist.empty()) + { + const node_indext id = worklist.front(); + worklist.pop_front(); + + // check if we have hit end of level + if(id == std::numeric_limits::max()) + { + depth++; + // mark end of next level + if(!worklist.empty()) + worklist.push_back(id); + continue; + } + function_list.insert(nodes[id].function_name); + + if(depth < steps) + { + for(const auto &o : nodes[id].out) + { + if(function_list.find(nodes[o.first].function_name) + == function_list.end()) + worklist.push_back(o.first); + } + } } } -void call_grapht::output_xml(std::ostream &out) const +std::unordered_set +call_grapht::reachable_functions(irep_idt start_function) { - for(const auto &edge : graph) + std::unordered_set result; + std::list worklist; + node_indext start_index; + + if(get_node_index(start_function, start_index)) + worklist.push_back(start_index); + else + throw "no start function found in call graph"; + + while(!worklist.empty()) { - out << "\n"; + const node_indext id = worklist.front(); + worklist.pop_front(); + + result.insert(nodes[id].function_name); + for(const auto &o : nodes[id].out) + { + if(result.find(nodes[o.first].function_name) == result.end()) + worklist.push_back(o.first); + } } + + return result; } diff --git a/src/analyses/call_graph.h b/src/analyses/call_graph.h index 684f74c3a3a..9b50ee4f984 100644 --- a/src/analyses/call_graph.h +++ b/src/analyses/call_graph.h @@ -7,34 +7,111 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ /// \file -/// Function Call Graphs +/// Function Call Graph #ifndef CPROVER_ANALYSES_CALL_GRAPH_H #define CPROVER_ANALYSES_CALL_GRAPH_H #include #include +#include #include -class call_grapht +#include +#include +#include + + +/// \brief Function call graph: each node represents a function +/// in the GOTO model, a directed edge from A to B indicates +/// that function A calls function B. +/// Inherits from grapht to allow forward and +/// backward traversal of the function call graph +struct call_graph_nodet: public graph_nodet +{ + typedef graph_nodet::edget edget; + typedef graph_nodet::edgest edgest; + + irep_idt function_name; + bool visited = false; +}; + +class call_grapht: public grapht { public: call_grapht(); explicit call_grapht(const goto_modelt &); explicit call_grapht(const goto_functionst &); - void output_dot(std::ostream &out) const; - void output(std::ostream &out) const; + void add(const irep_idt &caller, const irep_idt &callee); void output_xml(std::ostream &out) const; - typedef std::multimap grapht; - grapht graph; - - void add(const irep_idt &caller, const irep_idt &callee); + /// \return the inverted call graph call_grapht get_inverted() const; + /// \brief get the names of all functions reachable from a start function + /// \param start name of initial function + /// \return set of all names of the reachable functions + std::unordered_set + reachable_functions(irep_idt start); + + /// \brief Function returns the shortest path on the function call graph + /// between a source and a destination function + /// \param src name of the starting function + /// \param dest name of the destination function + /// \return list of function names on the shortest path between src and dest + std::listshortest_function_path(irep_idt src, irep_idt dest); + + /// \brief get the names of all functions reachable from a list of functions + /// within N function call steps. + /// \param function_list list of functions to start from. + /// Functions reachable within + /// N function call steps are appended to this list + /// \param steps number of function call steps + void reachable_within_n_steps(std::size_t steps, + std::unordered_set &function_list); + + + /// get the index of the node that corresponds to a function name + /// \param[in] function_name function_name passed by reference + /// \param[out] n variable for the node index to be written to + /// \return true if a node with the given function name exists, + /// false if it does not exist + bool get_node_index(const irep_idt& function_name, node_indext &n) const + { + for(node_indext idx = 0; idx < nodes.size(); idx++) + { + if(nodes[idx].function_name == function_name) + { + n = idx; + return true; + } + } + return false; + } + + /// \brief get a list of functions called by a function + /// \param function_name the irep_idt of the function + /// \return an unordered set of all functions called by function_name + std::unordered_set get_successors( + const irep_idt& function_name) const + { + std::unordered_set result; + node_indext function_idx; + if(!get_node_index(function_name, function_idx)) + return result; + + for(const auto &o : nodes[function_idx].out) + result.insert(nodes[o.first].function_name); + return result; + } + + protected: + void output_dot_node(std::ostream &out, node_indext n) const override; + void output_xml_node(std::ostream &out, node_indext n) const; + numbering node_numbering; void add(const irep_idt &function, const goto_programt &body); }; diff --git a/src/analyses/reachable_call_graph.cpp b/src/analyses/reachable_call_graph.cpp new file mode 100644 index 00000000000..4c65c60bef4 --- /dev/null +++ b/src/analyses/reachable_call_graph.cpp @@ -0,0 +1,105 @@ +/*******************************************************************\ + +Module: Reachable Call Graphs + +Author: + +\*******************************************************************/ + +/// \file +/// Reachable Call Graph +#include "reachable_call_graph.h" +#include + +reachable_call_grapht::reachable_call_grapht +(const goto_modelt & _goto_model) +{ + build(_goto_model.goto_functions); +} + +void reachable_call_grapht::initialize(const goto_modelt & _goto_model) +{ + build(_goto_model.goto_functions); +} + +void reachable_call_grapht::build(const goto_functionst & goto_functions) +{ + irep_idt start_function_name = goto_functions.entry_point(); + build(goto_functions, start_function_name); +} + + +void reachable_call_grapht::build( + const goto_functionst & goto_functions, + irep_idt start_function_name) +{ + std::set working_queue; + std::set done; + + // start from entry point + working_queue.insert(start_function_name); + + while(!working_queue.empty()) + { + irep_idt caller=*working_queue.begin(); + working_queue.erase(working_queue.begin()); + + if(!done.insert(caller).second) + continue; + + const goto_functionst::function_mapt::const_iterator f_it= + goto_functions.function_map.find(caller); + + if(f_it==goto_functions.function_map.end()) + continue; + + const goto_programt &program= + f_it->second.body; + + forall_goto_program_instructions(i_it, program) + { + if(i_it->is_function_call()) + { + const exprt &function_expr=to_code_function_call(i_it->code).function(); + if(function_expr.id()==ID_symbol) + { + irep_idt callee = to_symbol_expr(function_expr).get_identifier(); + add(caller, callee); + working_queue.insert(callee); + } + } + } + } +} + +std::unordered_set +reachable_call_grapht::backward_slice(irep_idt destination_function) +{ + std::unordered_set result; + std::list worklist; + for(node_indext idx=0; idx + backward_slice(irep_idt destination_function); + /// \brief used to initialise reachable_call_graph if we have used the + /// empty constructor. Necessary for aggressive slicer, to avoid constructing + /// reachable call graph unless we need it. + void initialize(const goto_modelt &); +protected: + void build(const goto_functionst &); + void build(const goto_functionst &, irep_idt start_function); +}; + +#endif /* SRC_ANALYSES_REACHABLE_CALL_GRAPH_H_ */ diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 2218fd68235..7ef82bf4cb6 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -61,6 +61,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include + #include @@ -648,17 +650,35 @@ int goto_instrument_parse_optionst::doit() { do_indirect_call_and_rtti_removal(); call_grapht call_graph(goto_model); - if(cmdline.isset("xml")) call_graph.output_xml(std::cout); - else if(cmdline.isset("dot")) - call_graph.output_dot(std::cout); else - call_graph.output(std::cout); + call_graph.output_dot(std::cout); return CPROVER_EXIT_SUCCESS; } + if(cmdline.isset("reachable-call-graph")) + { + do_indirect_call_and_rtti_removal(); + reachable_call_grapht reach_graph(goto_model); + if(cmdline.isset("property")) + { + std::list function_names = cmdline.get_values("property"); + if(function_names.size() > 1) + status() << "Only one destination allowed, " + "using only first function name given\n"; + cmdline.get_value("property"); + std::cout << "list of reachable functions: \n"; + for(const auto f : + reach_graph.backward_slice(function_names.front())) + std::cout << f << "\n"; + } + else + reach_graph.output_dot(std::cout); + return 0; + } + if(cmdline.isset("dot")) { namespacet ns(goto_model.symbol_table); @@ -1410,6 +1430,54 @@ void goto_instrument_parse_optionst::instrument_goto_program() throw 0; } + // aggressive slicer + if(cmdline.isset("aggressive-slice")) + { + do_indirect_call_and_rtti_removal(); + + status() << "Slicing away initializations of unused global variables" + << eom; + slice_global_inits(goto_model); + + status() << "Performing an aggressive slice" << eom; + aggressive_slicert aggressive_slicer(goto_model, get_message_handler()); + + if(cmdline.isset("preserve-all-direct-paths")) + { + if(!cmdline.isset("property")) + { + error() << "Property must be specified" + << " with the sound aggressive slicer" + << eom; + throw 0; + } + aggressive_slicer.preserve_all_direct_paths=true; + } + + if(cmdline.isset("call-depth")) + aggressive_slicer.call_depth = safe_string2unsigned( + cmdline.get_value("call-depth")); + + if(cmdline.isset("preserve-function")) + aggressive_slicer.preserve_functions( + cmdline.get_values("preserve-function")); + + if(cmdline.isset("property")) + aggressive_slicer.properties = cmdline.get_values("property"); + + if(cmdline.isset("preserve-functions-containing")) + aggressive_slicer.name_snippets = cmdline.get_values( + "preserve-functions-containing"); + + aggressive_slicer.doit(); + + status() << "Performing a reachability slice" << eom; + if(cmdline.isset("property")) + reachability_slicer(goto_model, cmdline.get_values("property")); + else + reachability_slicer(goto_model); + } + // recalculate numbers, etc. goto_model.goto_functions.update(); } @@ -1454,6 +1522,8 @@ void goto_instrument_parse_optionst::help() " --list-calls-args list all function calls with their arguments\n" // NOLINTNEXTLINE(whitespace/line_length) " --print-path-lengths print statistics about control-flow graph paths\n" + " --call-graph show graph of function calls\n" + " --reachable-call-graph show graph of function calls potentially reachable from main function\n" // NOLINT(*) "\n" "Safety checks:\n" " --no-assertions ignore user assertions\n" @@ -1507,6 +1577,15 @@ void goto_instrument_parse_optionst::help() " --full-slice slice away instructions that don't affect assertions\n" // NOLINT(*) " --property id slice with respect to specific property only\n" // NOLINT(*) " --slice-global-inits slice away initializations of unused global variables\n" // NOLINT(*) + " --aggressive-slice remove bodies of any functions not on the shortest path between\n" // NOLINT(*) + " the start function and the function containing the property(s)\n" // NOLINT(*) + " --call-depth used with aggressive-slice, preserves all functions within function calls\n" // NOLINT(*) + " of the functions on the shortest path\n" + " --preserve-function force the aggressive slicer to preserve function \n" // NOLINT(*) + " --preserve-function containing \n" + " force the aggressive slicer to preserve all functions with names containing \n" // NOLINT(*) + " --preserve-all-direct-paths force the aggressive slicer to preserve all functions on direct paths to the property\n" // NOLINT(*) + " Must be used with a specified property\n" "\n" "Further transformations:\n" " --constant-propagator propagate constants and simplify expressions\n" // NOLINT(*) diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 04b3a8f7b2b..55db20837d9 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -44,6 +44,7 @@ Author: Daniel Kroening, kroening@kroening.com "(max-var):(max-po-trans):(ignore-arrays)" \ "(cfg-kill)(no-dependencies)(force-loop-duplication)" \ "(call-graph)" \ + "(reachable-call-graph)" \ "(no-po-rendering)(render-cluster-file)(render-cluster-function)" \ "(nondet-volatile)(isr):" \ "(stack-depth):(nondet-static)" \ @@ -79,7 +80,12 @@ Author: Daniel Kroening, kroening@kroening.com "(undefined-function-is-assume-false)" \ "(remove-function-body):"\ "(splice-call):" \ - + "(aggressive-slice)" \ + "(call-depth):" \ + "(harness-generator):" \ + "(preserve-function):" \ + "(preserve-functions-containing):" \ + "(preserve-all-direct-paths)" \ class goto_instrument_parse_optionst: public parse_options_baset, diff --git a/src/goto-instrument/remove_function.cpp b/src/goto-instrument/remove_function.cpp index 6376b4a5512..ffaf3f1bfe3 100644 --- a/src/goto-instrument/remove_function.cpp +++ b/src/goto-instrument/remove_function.cpp @@ -12,10 +12,100 @@ Date: April 2017 /// Remove function definition #include "remove_function.h" +#include "function_modifies.h" #include #include +#include + +#include + + +void aggressive_slicert::get_property_list() +{ + for(const auto &fct : goto_model.goto_functions.function_map) + { + if(!fct.second.is_inlined()) + { + for(const auto &ins : fct.second.body.instructions) + if(ins.is_assert()) + { + for(const auto &func : call_graph.shortest_function_path( + start_function, ins.function)) + { + functions_to_keep.insert(func); + } + } + } + } +} + + +void aggressive_slicert::find_functions_that_contain_name_snippet() +{ + for(const auto &name_snippet : name_snippets) + { + forall_goto_functions(f_it, goto_model.goto_functions) + { + if(id2string(f_it->first).find(name_snippet)!=std::string::npos) + functions_to_keep.insert(f_it->first); + } + } +} + + +void aggressive_slicert::doit() +{ + messaget message(message_handler); + + functions_to_keep.insert(CPROVER_PREFIX "initialize"); + functions_to_keep.insert(start_function); + + // if no properties are specified, get list of all properties + if(properties.empty()) + get_property_list(); + + // if a name snippet is given, get list of all functions containing + // name snippet + if(!name_snippets.empty()) + find_functions_that_contain_name_snippet(); + + if(preserve_all_direct_paths) + reach_graph.initialize(goto_model); + + for(const auto &p : properties) + { + source_locationt property_loc = find_property(p, goto_model.goto_functions); + irep_idt dest = property_loc.get_function(); + + if(preserve_all_direct_paths) + { + for(const auto & func : reach_graph.backward_slice(dest)) + functions_to_keep.insert(func); + } + else + { + for(const auto &func : call_graph.shortest_function_path(start_function, + dest)) + functions_to_keep.insert(func); + } + } + + // Add functions within distance of shortest path functions + // to the list + if(call_depth != 0) + call_graph.reachable_within_n_steps(call_depth, functions_to_keep); + + for(const auto &func : functions_to_keep) + message.status() << "Keeping: " << func << messaget::eom; + + forall_goto_functions(f_it, goto_model.goto_functions) + { + if(functions_to_keep.find(f_it->first)==functions_to_keep.end()) + remove_function(goto_model, f_it->first, message_handler); + } +} /// Remove the body of function "identifier" such that an analysis will treat it /// as a side-effect free function with non-deterministic return value. diff --git a/src/goto-instrument/remove_function.h b/src/goto-instrument/remove_function.h index 3c88b8ce803..b161a4c391e 100644 --- a/src/goto-instrument/remove_function.h +++ b/src/goto-instrument/remove_function.h @@ -16,9 +16,13 @@ Date: April 2017 #include #include +#include #include +#include +#include + class goto_modelt; class message_handlert; @@ -32,4 +36,70 @@ void remove_functions( const std::list &names, message_handlert &); +/// \brief The aggressive slicer removes the body of all the functions except +/// those on the shortest path, those within the call-depth of the +/// shortest path, those given by name as command line argument, +/// and those that contain a given irep_idt snippet +/// If no properties are set by the user, we preserve all functions on +/// the shortest paths to each property. +class aggressive_slicert +{ +public: + aggressive_slicert( + goto_modelt & _goto_model, + message_handlert &_msg) : + preserve_all_direct_paths(false), + call_depth(0), + start_function(_goto_model.goto_functions.entry_point()), + goto_model(_goto_model), + message_handler(_msg), + call_graph(_goto_model), + reach_graph() + { + } + + /// \brief Removes the body of all functions except those on the + /// shortest path or functions + /// that are reachable from functions on the shortest path within + /// N calls, where N is given by the parameter "distance" + void doit(); + + /// \brief Adds a list of functions to the set of functions for the aggressive + /// slicer to preserve + /// \param function_list a list of functions in form + /// std::list, as returned by get_cmdline_option. + void preserve_functions(const std::list& function_list) + { + for(const auto &f : function_list) + functions_to_keep.insert(f); + }; + + /// \brief When set to true we preserve all functions on direct paths between + /// the start function + /// and any given properties. We do not allow this option to be used without + /// specifying a property, as that would effectively be doing a full-slice + bool preserve_all_direct_paths; + std::list properties; + std::size_t call_depth; + std::list name_snippets; + +private: + irep_idt start_function; + goto_modelt & goto_model; + message_handlert & message_handler; + std::unordered_set functions_to_keep; + call_grapht call_graph; + reachable_call_grapht reach_graph; + + /// \brief Finds all functions whose name contains a name snippet + /// and adds them to the std::unordered_set of irep_idts of functions + /// for the aggressive slicer to preserve + void find_functions_that_contain_name_snippet(); + + /// \brief Finds all properties in the goto_model and writes their + /// names to a list. This function is only called if no properties + /// are given by the user + void get_property_list(); +}; + #endif // CPROVER_GOTO_INSTRUMENT_REMOVE_FUNCTION_H diff --git a/src/goto-programs/show_properties.cpp b/src/goto-programs/show_properties.cpp index 7f0be70cc64..663f1d03393 100644 --- a/src/goto-programs/show_properties.cpp +++ b/src/goto-programs/show_properties.cpp @@ -23,6 +23,30 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_functions.h" #include "goto_model.h" + +source_locationt find_property( + const irep_idt &property, + const goto_functionst & goto_functions) +{ + for(const auto &fct : goto_functions.function_map) + { + const goto_programt &goto_program = fct.second.body; + + for(const auto &ins : goto_program.instructions) + { + if(ins.is_assert()) + { + if(ins.source_location.get_property_id() == property) + { + return ins.source_location; + } + } + } + } + throw "property not found"; +} + + void show_properties( const namespacet &ns, const irep_idt &identifier, diff --git a/src/goto-programs/show_properties.h b/src/goto-programs/show_properties.h index 0cb0d1c641f..19109bd1d5f 100644 --- a/src/goto-programs/show_properties.h +++ b/src/goto-programs/show_properties.h @@ -28,4 +28,11 @@ void show_properties( ui_message_handlert::uit ui, const goto_functionst &goto_functions); +/// \brief Returns a source_locationt that corresponds +/// to the property given by an irep_idt. +/// \param property irep_idt and goto_functions +source_locationt find_property( + const irep_idt &property, + const goto_functionst &); + #endif // CPROVER_GOTO_PROGRAMS_SHOW_PROPERTIES_H diff --git a/src/goto-programs/slice_global_inits.cpp b/src/goto-programs/slice_global_inits.cpp index cc4f7349eb7..a08b3331449 100644 --- a/src/goto-programs/slice_global_inits.cpp +++ b/src/goto-programs/slice_global_inits.cpp @@ -30,11 +30,8 @@ void slice_global_inits(goto_modelt &goto_model) // gather all functions reachable from the entry point call_grapht call_graph(goto_model); - const call_grapht::grapht &graph=call_graph.graph; - goto_functionst &goto_functions=goto_model.goto_functions; - std::list worklist; - std::unordered_set functions_reached; + goto_functionst &goto_functions=goto_model.goto_functions; const irep_idt entry_point=goto_functionst::entry_point(); @@ -44,26 +41,8 @@ void slice_global_inits(goto_modelt &goto_model) if(e_it==goto_functions.function_map.end()) throw "entry point not found"; - worklist.push_back(entry_point); - - do - { - const irep_idt id=worklist.front(); - worklist.pop_front(); - - functions_reached.insert(id); - - const auto &p=graph.equal_range(id); - - for(auto it=p.first; it!=p.second; it++) - { - const irep_idt callee=it->second; - - if(functions_reached.find(callee)==functions_reached.end()) - worklist.push_back(callee); - } - } - while(!worklist.empty()); + std::unordered_set functions_reached= + call_graph.reachable_functions(entry_point); const irep_idt initialize=CPROVER_PREFIX "initialize"; functions_reached.erase(initialize); diff --git a/src/util/graph.h b/src/util/graph.h index b0b5713b5ee..f7eec376a9f 100644 --- a/src/util/graph.h +++ b/src/util/graph.h @@ -263,7 +263,7 @@ class grapht std::list topsort() const; void output_dot(std::ostream &out) const; - void output_dot_node(std::ostream &out, node_indext n) const; + virtual void output_dot_node(std::ostream &out, node_indext n) const; protected: class tarjant @@ -655,20 +655,26 @@ std::list::node_indext> grapht::topsort() const template void grapht::output_dot(std::ostream &out) const { + out << "digraph call_graph {\n"; + for(node_indext n=0; n void grapht::output_dot_node(std::ostream &out, node_indext n) const { - const nodet &node=nodes[n]; + const nodet &node=nodes.at(n); - for(typename edgest::const_iterator - it=node.out.begin(); - it!=node.out.end(); - it++) - out << n << " -> " << it->first << '\n'; + for(const auto &edge : node.out) + { + out << " \"" << n << "\" -> " + << "\"" << edge.first << "\" " + << " [arrowhead=\"vee\"];" + << "\n"; + } } #endif // CPROVER_UTIL_GRAPH_H diff --git a/unit/analyses/call_graph.cpp b/unit/analyses/call_graph.cpp index 985c804c91c..77c328cecac 100644 --- a/unit/analyses/call_graph.cpp +++ b/unit/analyses/call_graph.cpp @@ -30,15 +30,13 @@ static symbolt create_void_function_symbol( return function; } -static bool multimap_key_matches( - const std::multimap &map, +static bool graph_key_matches( + const call_grapht graph, const irep_idt &key, - const std::set &values) + const std::unordered_set &values) { - auto matching_values=map.equal_range(key); - std::set matching_set; - for(auto it=matching_values.first; it!=matching_values.second; ++it) - matching_set.insert(it->second); + std::unordered_set matching_set = + graph.get_successors(key); return matching_set==values; } @@ -106,10 +104,11 @@ SCENARIO("call_graph", { THEN("We expect A -> { A, B }, B -> { C, D }") { - const auto &check_graph=call_graph_from_goto_functions.graph; - REQUIRE(check_graph.size()==4); - REQUIRE(multimap_key_matches(check_graph, "A", {"A", "B"})); - REQUIRE(multimap_key_matches(check_graph, "B", {"C", "D"})); + REQUIRE(call_graph_from_goto_functions.size()==4); + REQUIRE(graph_key_matches + (call_graph_from_goto_functions, "A", {"A", "B"})); + REQUIRE(graph_key_matches + (call_graph_from_goto_functions, "B", {"C", "D"})); } } @@ -119,12 +118,15 @@ SCENARIO("call_graph", call_graph_from_goto_functions.get_inverted(); THEN("We expect A -> { A }, B -> { A }, C -> { B }, D -> { B }") { - const auto &check_graph=inverse_call_graph_from_goto_functions.graph; - REQUIRE(check_graph.size()==4); - REQUIRE(multimap_key_matches(check_graph, "A", {"A"})); - REQUIRE(multimap_key_matches(check_graph, "B", {"A"})); - REQUIRE(multimap_key_matches(check_graph, "C", {"B"})); - REQUIRE(multimap_key_matches(check_graph, "D", {"B"})); + REQUIRE(inverse_call_graph_from_goto_functions.size()==4); + REQUIRE(graph_key_matches + (inverse_call_graph_from_goto_functions, "A", {"A"})); + REQUIRE(graph_key_matches + (inverse_call_graph_from_goto_functions, "B", {"A"})); + REQUIRE(graph_key_matches + (inverse_call_graph_from_goto_functions, "C", {"B"})); + REQUIRE(graph_key_matches + (inverse_call_graph_from_goto_functions, "D", {"B"})); } }