From 357358de5f08a4f07885962751f2c1c0968cdf4d Mon Sep 17 00:00:00 2001 From: Polgreen Date: Wed, 27 Jun 2018 09:17:13 +0200 Subject: [PATCH 1/7] remove mistake in grapht Function declaration exists but there is no body. Removing function declaration --- src/util/graph.h | 5 ----- 1 file changed, 5 deletions(-) diff --git a/src/util/graph.h b/src/util/graph.h index 7189a9ae39d..e0c201c3177 100644 --- a/src/util/graph.h +++ b/src/util/graph.h @@ -255,11 +255,6 @@ class grapht void disconnect_unreachable(node_indext src); void disconnect_unreachable(const std::vector &src); - std::vector depth_limited_search( - const node_indext &src, - std::size_t &limit, - bool forwards) const; - std::vector depth_limited_search(typename N::node_indext src, std::size_t limit) const; From de7e1af158a4f8d6a0744b269ed08c2cb15826b4 Mon Sep 17 00:00:00 2001 From: Polgreen Date: Wed, 27 Jun 2018 09:23:06 +0200 Subject: [PATCH 2/7] call graph helper functions --- src/analyses/call_graph_helpers.cpp | 30 ++++++++++++++++++++++++++--- src/analyses/call_graph_helpers.h | 25 ++++++++++++++++++++++-- 2 files changed, 50 insertions(+), 5 deletions(-) diff --git a/src/analyses/call_graph_helpers.cpp b/src/analyses/call_graph_helpers.cpp index 449de47c6cc..0723e3eb181 100644 --- a/src/analyses/call_graph_helpers.cpp +++ b/src/analyses/call_graph_helpers.cpp @@ -74,7 +74,7 @@ std::set get_reaching_functions( std::set get_functions_reachable_within_n_steps( const call_grapht::directed_grapht &graph, const std::set &start_functions, - std::size_t &n) + std::size_t n) { std::vector start_indices; std::set result; @@ -91,8 +91,32 @@ std::set get_functions_reachable_within_n_steps( std::set get_functions_reachable_within_n_steps( const call_grapht::directed_grapht &graph, const irep_idt &start_function, - std::size_t &n) + std::size_t n) { - std::set start_functions({ start_function }); + std::set start_functions({start_function}); return get_functions_reachable_within_n_steps(graph, start_functions, n); } + +void disconnect_unreachable_functions( + call_grapht::directed_grapht &graph, + const irep_idt &function) +{ + graph.disconnect_unreachable(*(graph.get_node_index(function))); +} + +std::list get_shortest_function_path( + const call_grapht::directed_grapht &graph, + const irep_idt &src, + const irep_idt &dest) +{ + std::list result; + std::list path; + + graph.shortest_path( + *(graph.get_node_index(src)), *(graph.get_node_index(dest)), path); + + for(const auto &n : path) + result.push_back(graph[n].function); + + return result; +} diff --git a/src/analyses/call_graph_helpers.h b/src/analyses/call_graph_helpers.h index faedd44f15c..4388c552797 100644 --- a/src/analyses/call_graph_helpers.h +++ b/src/analyses/call_graph_helpers.h @@ -59,7 +59,7 @@ std::set get_reaching_functions( std::set get_functions_reachable_within_n_steps( const call_grapht::directed_grapht &graph, const std::set &start_functions, - std::size_t &n); + std::size_t n); /// Get either callers or callees reachable from a given /// list of functions within N steps @@ -71,6 +71,27 @@ std::set get_functions_reachable_within_n_steps( std::set get_functions_reachable_within_n_steps( const call_grapht::directed_grapht &graph, const irep_idt &start_function, - std::size_t &n); + std::size_t n); + +/// Get list of functions on the shortest path between two functions +/// \param graph: call graph +/// \param src: function to start from +/// \param dest: function to reach +/// \return list of functions on shortest path +std::list get_shortest_function_path( + const call_grapht::directed_grapht &graph, + const irep_idt &src, + const irep_idt &dest); + +/// Disconnects all functions in the call graph that are unreachable from +/// a given start function. +/// Removing nodes requires re-indexing, so instead we disconnect them, removing +/// all in and out edges from those nodes. +/// This speeds up backwards reachability. +/// \param graph: call graph +/// \param function: start function +void disconnect_unreachable_functions( + call_grapht::directed_grapht &graph, + const irep_idt &function); #endif From 29542059e665e9b9c55e882915e9abfa6f8fbcb7 Mon Sep 17 00:00:00 2001 From: Polgreen Date: Thu, 21 Jun 2018 14:09:31 +0200 Subject: [PATCH 3/7] aggressive slicer regression tests --- .../goto-instrument/aggressive_slicer1/main.c | 36 +++++++++++++++ .../aggressive_slicer1/test.desc | 8 ++++ .../goto-instrument/aggressive_slicer2/main.c | 39 ++++++++++++++++ .../aggressive_slicer2/test.desc | 8 ++++ .../goto-instrument/aggressive_slicer3/main.c | 35 ++++++++++++++ .../aggressive_slicer3/test.desc | 8 ++++ .../goto-instrument/aggressive_slicer4/main.c | 39 ++++++++++++++++ .../aggressive_slicer4/test.desc | 8 ++++ .../goto-instrument/aggressive_slicer5/main.c | 38 +++++++++++++++ .../aggressive_slicer5/test.desc | 8 ++++ .../goto-instrument/aggressive_slicer6/main.c | 40 ++++++++++++++++ .../aggressive_slicer6/test.desc | 8 ++++ .../goto-instrument/aggressive_slicer7/main.c | 46 +++++++++++++++++++ .../aggressive_slicer7/test.desc | 8 ++++ 14 files changed, 329 insertions(+) create mode 100644 regression/goto-instrument/aggressive_slicer1/main.c create mode 100644 regression/goto-instrument/aggressive_slicer1/test.desc create mode 100644 regression/goto-instrument/aggressive_slicer2/main.c create mode 100644 regression/goto-instrument/aggressive_slicer2/test.desc create mode 100644 regression/goto-instrument/aggressive_slicer3/main.c create mode 100644 regression/goto-instrument/aggressive_slicer3/test.desc create mode 100644 regression/goto-instrument/aggressive_slicer4/main.c create mode 100644 regression/goto-instrument/aggressive_slicer4/test.desc create mode 100644 regression/goto-instrument/aggressive_slicer5/main.c create mode 100644 regression/goto-instrument/aggressive_slicer5/test.desc create mode 100644 regression/goto-instrument/aggressive_slicer6/main.c create mode 100644 regression/goto-instrument/aggressive_slicer6/test.desc create mode 100644 regression/goto-instrument/aggressive_slicer7/main.c create mode 100644 regression/goto-instrument/aggressive_slicer7/test.desc diff --git a/regression/goto-instrument/aggressive_slicer1/main.c b/regression/goto-instrument/aggressive_slicer1/main.c new file mode 100644 index 00000000000..e2ce3ffcd9b --- /dev/null +++ b/regression/goto-instrument/aggressive_slicer1/main.c @@ -0,0 +1,36 @@ +// test should pass. Shortest path main -> C -> D +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; +} diff --git a/regression/goto-instrument/aggressive_slicer1/test.desc b/regression/goto-instrument/aggressive_slicer1/test.desc new file mode 100644 index 00000000000..90b7781e4d4 --- /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 diff --git a/regression/goto-instrument/aggressive_slicer2/main.c b/regression/goto-instrument/aggressive_slicer2/main.c new file mode 100644 index 00000000000..a7cf787172d --- /dev/null +++ b/regression/goto-instrument/aggressive_slicer2/main.c @@ -0,0 +1,39 @@ +// test should pass. Shortest path is preserved, main -> C -> D, +// but is not a possible counterexample because of assumption that +// nondet != 3 + +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; +} diff --git a/regression/goto-instrument/aggressive_slicer2/test.desc b/regression/goto-instrument/aggressive_slicer2/test.desc new file mode 100644 index 00000000000..f8a015e2051 --- /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 diff --git a/regression/goto-instrument/aggressive_slicer3/main.c b/regression/goto-instrument/aggressive_slicer3/main.c new file mode 100644 index 00000000000..6116eefcb70 --- /dev/null +++ b/regression/goto-instrument/aggressive_slicer3/main.c @@ -0,0 +1,35 @@ +// test should fail. Shortest path is preserved, main -> C -> D, +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; +} diff --git a/regression/goto-instrument/aggressive_slicer3/test.desc b/regression/goto-instrument/aggressive_slicer3/test.desc new file mode 100644 index 00000000000..63633765441 --- /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 diff --git a/regression/goto-instrument/aggressive_slicer4/main.c b/regression/goto-instrument/aggressive_slicer4/main.c new file mode 100644 index 00000000000..4e6c05f22fa --- /dev/null +++ b/regression/goto-instrument/aggressive_slicer4/main.c @@ -0,0 +1,39 @@ +// test should fail +// shortest path only is not sufficient to violate assertion, +// but we specifically require that function B is kept, which +// allows path main -> B -> C -> D + +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; +} diff --git a/regression/goto-instrument/aggressive_slicer4/test.desc b/regression/goto-instrument/aggressive_slicer4/test.desc new file mode 100644 index 00000000000..66a104a02b7 --- /dev/null +++ b/regression/goto-instrument/aggressive_slicer4/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--aggressive-slice --aggressive-slice-preserve-function B +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/goto-instrument/aggressive_slicer5/main.c b/regression/goto-instrument/aggressive_slicer5/main.c new file mode 100644 index 00000000000..6119e412ab6 --- /dev/null +++ b/regression/goto-instrument/aggressive_slicer5/main.c @@ -0,0 +1,38 @@ +// Test should fail. Shortest path only is not sufficient +// due to assumption that nondet !=3, but +// preserve-all-direct-paths preserves the path main -> B -> C -> D. + +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; +} diff --git a/regression/goto-instrument/aggressive_slicer5/test.desc b/regression/goto-instrument/aggressive_slicer5/test.desc new file mode 100644 index 00000000000..47909b9840b --- /dev/null +++ b/regression/goto-instrument/aggressive_slicer5/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--aggressive-slice --property D.assertion.1 --aggressive-slice-preserve-all-direct-paths +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/goto-instrument/aggressive_slicer6/main.c b/regression/goto-instrument/aggressive_slicer6/main.c new file mode 100644 index 00000000000..95f9afecff9 --- /dev/null +++ b/regression/goto-instrument/aggressive_slicer6/main.c @@ -0,0 +1,40 @@ +// Test should fail +// Assertion in D is reachable when call depth of 1 is preserved, +// Shortest path = main -> C -> D, which is not possible due to assumption +// nondet!=3, but call depth 1 preserves the body of function B, which can also reach +// C. + +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; +} diff --git a/regression/goto-instrument/aggressive_slicer6/test.desc b/regression/goto-instrument/aggressive_slicer6/test.desc new file mode 100644 index 00000000000..a085d640373 --- /dev/null +++ b/regression/goto-instrument/aggressive_slicer6/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--aggressive-slice --aggressive-slice-call-depth 1 +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/goto-instrument/aggressive_slicer7/main.c b/regression/goto-instrument/aggressive_slicer7/main.c new file mode 100644 index 00000000000..3864c2bb68e --- /dev/null +++ b/regression/goto-instrument/aggressive_slicer7/main.c @@ -0,0 +1,46 @@ +// Test should fail +// Assertion in D is reachable by main -> C -> D +// Assertion in E is reachable by main -> E + +void D() +{ + __CPROVER_assert(0, ""); +} + +void C() +{ + int nondet; + if(nondet) + D(); +} + +void B() +{ + C(); +}; + +void E() +{ + __CPROVER_assert(0, ""); +} + +int main() +{ + int nondet; + + switch(nondet) + { + case 1: + B(); + break; + case 2: + E(); + break; + case 3: + C(); + break; + default: + break; + } + return 0; +} diff --git a/regression/goto-instrument/aggressive_slicer7/test.desc b/regression/goto-instrument/aggressive_slicer7/test.desc new file mode 100644 index 00000000000..63633765441 --- /dev/null +++ b/regression/goto-instrument/aggressive_slicer7/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--aggressive-slice +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring From 4ac9199bd587ae59b240129d83ec3565c06e80dc Mon Sep 17 00:00:00 2001 From: Polgreen Date: Mon, 25 Jun 2018 14:39:32 +0200 Subject: [PATCH 4/7] Aggressive slicer --- src/goto-instrument/Makefile | 1 + src/goto-instrument/aggressive_slicer.cpp | 116 ++++++++++++++++++ src/goto-instrument/aggressive_slicer.h | 100 +++++++++++++++ .../goto_instrument_parse_options.cpp | 52 ++++++++ .../goto_instrument_parse_options.h | 5 + 5 files changed, 274 insertions(+) create mode 100644 src/goto-instrument/aggressive_slicer.cpp create mode 100644 src/goto-instrument/aggressive_slicer.h diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index eb67f14f140..87885153a33 100644 --- a/src/goto-instrument/Makefile +++ b/src/goto-instrument/Makefile @@ -12,6 +12,7 @@ SRC = accelerate/accelerate.cpp \ accelerate/scratch_program.cpp \ accelerate/trace_automaton.cpp \ accelerate/util.cpp \ + aggressive_slicer.cpp \ alignment_checks.cpp \ branch.cpp \ call_sequences.cpp \ diff --git a/src/goto-instrument/aggressive_slicer.cpp b/src/goto-instrument/aggressive_slicer.cpp new file mode 100644 index 00000000000..7cf71a96d12 --- /dev/null +++ b/src/goto-instrument/aggressive_slicer.cpp @@ -0,0 +1,116 @@ +/*******************************************************************\ + +Module: Aggressive slicer + +Author: Elizabeth Polgreen, elizabeth.polgreen@cs.ox.ac.uk + +\*******************************************************************/ + +/// \file +/// Aggressive program slicer + +#include "aggressive_slicer.h" +#include "remove_function.h" +#include +#include +#include +#include + +void aggressive_slicert::note_functions_to_keep( + const irep_idt &destination_function) +{ + if(preserve_all_direct_paths) + { + /// Note that we have previously disconnected all nodes unreachable + /// from the start function, + /// which means that any reaching functions are also reachable from + /// the start function. + for(const auto &func : + get_reaching_functions(call_graph, destination_function)) + functions_to_keep.insert(func); + } + else + { + for(const auto &func : get_shortest_function_path( + call_graph, start_function, destination_function)) + functions_to_keep.insert(func); + } +} + +void aggressive_slicert::get_all_functions_containing_properties() +{ + 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()) + { + if(functions_to_keep.insert(ins.function).second) + note_functions_to_keep(ins.function); + } + } + } +} + +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(INITIALIZE_FUNCTION); + functions_to_keep.insert(start_function); + + // if no properties are specified, preserve all functions containing + // any property + if(user_specified_properties.empty()) + { + message.debug() << "No properties given, so aggressive slicer " + << "is running over all possible properties" + << messaget::eom; + get_all_functions_containing_properties(); + } + + // if a name snippet is given, get list of all functions containing + // name snippet to preserve + if(!name_snippets.empty()) + find_functions_that_contain_name_snippet(); + + for(const auto &p : user_specified_properties) + { + auto property_loc = find_property(p, goto_model.goto_functions); + if(!property_loc.has_value()) + throw "unable to find property in call graph"; + note_functions_to_keep(property_loc.value().get_function()); + } + + // Add functions within distance of shortest path functions + // to the list + if(call_depth != 0) + { + for(const auto &func : get_functions_reachable_within_n_steps( + call_graph, functions_to_keep, call_depth)) + functions_to_keep.insert(func); + } + + message.debug() << "Preserving the following functions \n"; + for(const auto &func : functions_to_keep) + message.debug() << 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); + } +} diff --git a/src/goto-instrument/aggressive_slicer.h b/src/goto-instrument/aggressive_slicer.h new file mode 100644 index 00000000000..d466983fdac --- /dev/null +++ b/src/goto-instrument/aggressive_slicer.h @@ -0,0 +1,100 @@ +/*******************************************************************\ + +Module: Aggressive Slicer + +Author: Elizabeth Polgreen, polgreen@amazon.com + +\*******************************************************************/ + +/// \file +/// Aggressive slicer +/// Consider the control flow graph of the goto program and a criterion +/// description of aggressive slicer here + +#ifndef CPROVER_GOTO_INSTRUMENT_AGGRESSIVE_SLICER_H +#define CPROVER_GOTO_INSTRUMENT_AGGRESSIVE_SLICER_H + +#include +#include +#include + +#include + +#include + +#include + +class goto_modelt; +class 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) + : call_depth(0), + preserve_all_direct_paths(false), + start_function(_goto_model.goto_functions.entry_point()), + goto_model(_goto_model), + message_handler(_msg) + { + call_grapht undirected_call_graph = + call_grapht::create_from_root_function(goto_model, start_function, false); + call_graph = undirected_call_graph.get_directed_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); + }; + + std::list user_specified_properties; + std::size_t call_depth; + std::list name_snippets; + bool preserve_all_direct_paths; + +private: + const irep_idt start_function; + goto_modelt &goto_model; + message_handlert &message_handler; + std::set functions_to_keep; + call_grapht::directed_grapht call_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 notes functions to keep in the slice based on the program + /// start function and the given destination function. Functions are noted + /// according to the configuration parameters set in the aggressive + /// slicer, i.e., shortest path between two functions, or all direct paths. + /// Inserts functions to preserve into the functions_to_keep set + /// \param destination_function name of destination function for slice + void note_functions_to_keep(const irep_idt &destination_function); + + /// \brief Finds all functions that contain a property, + /// and adds them to the list of functions to keep. This + /// function is only called if no properties are given by the user. + /// This behaviour mirrors the behaviour of the other program + /// slicers (reachability, global, full) + void get_all_functions_containing_properties(); +}; + +#endif /* CPROVER_GOTO_INSTRUMENT_AGGRESSIVE_SLICER_H */ diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index fd9a511eeb4..a7b6e44b657 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -100,6 +100,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "undefined_functions.h" #include "remove_function.h" #include "splice_call.h" +#include "aggressive_slicer.h" /// invoke main modules int goto_instrument_parse_optionst::doit() @@ -1457,6 +1458,46 @@ void goto_instrument_parse_optionst::instrument_goto_program() *message_handler); } + // 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("aggressive-slice-call-depth")) + aggressive_slicer.call_depth = + safe_string2unsigned(cmdline.get_value("aggressive-slice-call-depth")); + + if(cmdline.isset("aggressive-slice-preserve-function")) + aggressive_slicer.preserve_functions( + cmdline.get_values("aggressive-slice-preserve-function")); + + if(cmdline.isset("property")) + aggressive_slicer.user_specified_properties = + cmdline.get_values("property"); + + if(cmdline.isset("aggressive-slice-preserve-functions-containing")) + aggressive_slicer.name_snippets = + cmdline.get_values("aggressive-slice-preserve-functions-containing"); + + aggressive_slicer.preserve_all_direct_paths = + cmdline.isset("aggressive-slice-preserve-all-direct-paths"); + + 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(); } @@ -1562,6 +1603,17 @@ 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(*) + " --aggressive-slice-call-depth \n" + " used with aggressive-slice, preserves all functions within function calls\n" // NOLINT(*) + " of the functions on the shortest path\n" + " --aggressive-slice-preserve-function \n" + " force the aggressive slicer to preserve function \n" // NOLINT(*) + " --aggressive-slice-preserve-function containing \n" + " force the aggressive slicer to preserve all functions with names containing \n" // NOLINT(*) + "--aggressive-slice-preserve-all-direct-paths \n" + " force aggressive slicer to preserve all direct paths\n" // NOLINT(*) "\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 dd6950932e4..d44777f8435 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -90,6 +90,11 @@ Author: Daniel Kroening, kroening@kroening.com "(show-threaded)(list-calls-args)" \ "(undefined-function-is-assume-false)" \ "(remove-function-body):"\ + "(aggressive-slice)" \ + "(aggressive-slice-call-depth):" \ + "(aggressive-slice-preserve-function):" \ + "(aggressive-slice-preserve-functions-containing):" \ + "(aggressive-slice-preserve-all-direct-paths)" \ OPT_FLUSH \ "(splice-call):" \ OPT_REMOVE_CALLS_NO_BODY \ From aa4848d792801dab8d6f23c6bffc6d5ef3192413 Mon Sep 17 00:00:00 2001 From: Polgreen Date: Thu, 5 Jul 2018 12:04:11 +0200 Subject: [PATCH 5/7] Apply clang format to includes in goto_instrument_parse_options --- .../goto_instrument_parse_options.cpp | 52 +++++++++---------- 1 file changed, 26 insertions(+), 26 deletions(-) diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index a7b6e44b657..7cde684f21a 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -67,40 +67,40 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include "document_properties.h" -#include "uninitialized.h" -#include "full_slicer.h" -#include "reachability_slicer.h" -#include "show_locations.h" -#include "points_to.h" +#include "accelerate/accelerate.h" +#include "aggressive_slicer.h" #include "alignment_checks.h" -#include "race_check.h" -#include "nondet_volatile.h" -#include "interrupt.h" -#include "mmio.h" -#include "stack_depth.h" -#include "nondet_static.h" -#include "rw_set.h" +#include "branch.h" +#include "call_sequences.h" +#include "code_contracts.h" #include "concurrency.h" -#include "dump_c.h" +#include "document_properties.h" #include "dot.h" -#include "havoc_loops.h" -#include "k_induction.h" +#include "dump_c.h" +#include "full_slicer.h" #include "function.h" -#include "branch.h" -#include "wmm/weak_memory.h" -#include "call_sequences.h" -#include "accelerate/accelerate.h" +#include "havoc_loops.h" #include "horn_encoding.h" -#include "thread_instrumentation.h" -#include "skip_loops.h" -#include "code_contracts.h" -#include "unwind.h" +#include "interrupt.h" +#include "k_induction.h" +#include "mmio.h" #include "model_argc_argv.h" -#include "undefined_functions.h" +#include "nondet_static.h" +#include "nondet_volatile.h" +#include "points_to.h" +#include "race_check.h" +#include "reachability_slicer.h" #include "remove_function.h" +#include "rw_set.h" +#include "show_locations.h" +#include "skip_loops.h" #include "splice_call.h" -#include "aggressive_slicer.h" +#include "stack_depth.h" +#include "thread_instrumentation.h" +#include "undefined_functions.h" +#include "uninitialized.h" +#include "unwind.h" +#include "wmm/weak_memory.h" /// invoke main modules int goto_instrument_parse_optionst::doit() From ea085d3b9d3d44fd3719105b4ffa890d6c70654c Mon Sep 17 00:00:00 2001 From: Polgreen Date: Tue, 24 Jul 2018 09:35:01 +0200 Subject: [PATCH 6/7] move aggressive slicer options into macro --- src/goto-instrument/aggressive_slicer.h | 10 ++++++++++ src/goto-instrument/goto_instrument_parse_options.cpp | 1 - src/goto-instrument/goto_instrument_parse_options.h | 7 ++----- 3 files changed, 12 insertions(+), 6 deletions(-) diff --git a/src/goto-instrument/aggressive_slicer.h b/src/goto-instrument/aggressive_slicer.h index d466983fdac..b4ed1573d79 100644 --- a/src/goto-instrument/aggressive_slicer.h +++ b/src/goto-instrument/aggressive_slicer.h @@ -97,4 +97,14 @@ class aggressive_slicert void get_all_functions_containing_properties(); }; +// clang-format off +#define OPT_AGGRESSIVE_SLICER \ + "(aggressive-slice)" \ + "(aggressive-slice-call-depth):" \ + "(aggressive-slice-preserve-function):" \ + "(aggressive-slice-preserve-functions-containing):" \ + "(aggressive-slice-preserve-all-direct-paths)" + +// clang-format on + #endif /* CPROVER_GOTO_INSTRUMENT_AGGRESSIVE_SLICER_H */ diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 7cde684f21a..0151f563507 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -68,7 +68,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "accelerate/accelerate.h" -#include "aggressive_slicer.h" #include "alignment_checks.h" #include "branch.h" #include "call_sequences.h" diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index d44777f8435..706083df63e 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -26,6 +26,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include "aggressive_slicer.h" #include "count_eloc.h" @@ -90,11 +91,7 @@ Author: Daniel Kroening, kroening@kroening.com "(show-threaded)(list-calls-args)" \ "(undefined-function-is-assume-false)" \ "(remove-function-body):"\ - "(aggressive-slice)" \ - "(aggressive-slice-call-depth):" \ - "(aggressive-slice-preserve-function):" \ - "(aggressive-slice-preserve-functions-containing):" \ - "(aggressive-slice-preserve-all-direct-paths)" \ + OPT_AGGRESSIVE_SLICER \ OPT_FLUSH \ "(splice-call):" \ OPT_REMOVE_CALLS_NO_BODY \ From 8c7dc1789f65a0f076bee60d811b3419531144cd Mon Sep 17 00:00:00 2001 From: Polgreen Date: Tue, 24 Jul 2018 10:17:03 +0200 Subject: [PATCH 7/7] make comment // not /* --- src/goto-instrument/aggressive_slicer.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/goto-instrument/aggressive_slicer.h b/src/goto-instrument/aggressive_slicer.h index b4ed1573d79..6b8fe3fc42c 100644 --- a/src/goto-instrument/aggressive_slicer.h +++ b/src/goto-instrument/aggressive_slicer.h @@ -107,4 +107,4 @@ class aggressive_slicert // clang-format on -#endif /* CPROVER_GOTO_INSTRUMENT_AGGRESSIVE_SLICER_H */ +#endif // CPROVER_GOTO_INSTRUMENT_AGGRESSIVE_SLICER_H