diff --git a/regression/goto-instrument/fp-reachability-slice1/main.c b/regression/goto-instrument/fp-reachability-slice1/main.c new file mode 100644 index 00000000000..c73647c2ea8 --- /dev/null +++ b/regression/goto-instrument/fp-reachability-slice1/main.c @@ -0,0 +1,34 @@ +void a() +{ + int e; +} + +void b() +{ + double f; + if(f == 0) + a(); +} + +void c() +{ + int d; +} + +int main() +{ + int k; + if(k == 0) + { + int l; + a(); + c(); + } + else + { + b(); + } + int n; + a(); + return n; +} diff --git a/regression/goto-instrument/fp-reachability-slice1/test.desc b/regression/goto-instrument/fp-reachability-slice1/test.desc new file mode 100644 index 00000000000..803f790ee84 --- /dev/null +++ b/regression/goto-instrument/fp-reachability-slice1/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--fp-reachability-slice c +^EXIT=0$ +^SIGNAL=0$ +1: ASSUME FALSE +dead e; +dead d; +-- +^warning: ignoring +dead f; diff --git a/regression/goto-instrument/fp-reachability-slice2/main.c b/regression/goto-instrument/fp-reachability-slice2/main.c new file mode 100644 index 00000000000..c73647c2ea8 --- /dev/null +++ b/regression/goto-instrument/fp-reachability-slice2/main.c @@ -0,0 +1,34 @@ +void a() +{ + int e; +} + +void b() +{ + double f; + if(f == 0) + a(); +} + +void c() +{ + int d; +} + +int main() +{ + int k; + if(k == 0) + { + int l; + a(); + c(); + } + else + { + b(); + } + int n; + a(); + return n; +} diff --git a/regression/goto-instrument/fp-reachability-slice2/test.desc b/regression/goto-instrument/fp-reachability-slice2/test.desc new file mode 100644 index 00000000000..36f6ee8dafc --- /dev/null +++ b/regression/goto-instrument/fp-reachability-slice2/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--fp-reachability-slice a,c +^EXIT=0$ +^SIGNAL=0$ +dead d; +dead e; +-- +^warning: ignoring +dead f; diff --git a/regression/goto-instrument/fp-reachability-slice3/main.c b/regression/goto-instrument/fp-reachability-slice3/main.c new file mode 100644 index 00000000000..c73647c2ea8 --- /dev/null +++ b/regression/goto-instrument/fp-reachability-slice3/main.c @@ -0,0 +1,34 @@ +void a() +{ + int e; +} + +void b() +{ + double f; + if(f == 0) + a(); +} + +void c() +{ + int d; +} + +int main() +{ + int k; + if(k == 0) + { + int l; + a(); + c(); + } + else + { + b(); + } + int n; + a(); + return n; +} diff --git a/regression/goto-instrument/fp-reachability-slice3/test.desc b/regression/goto-instrument/fp-reachability-slice3/test.desc new file mode 100644 index 00000000000..6d39cf164d8 --- /dev/null +++ b/regression/goto-instrument/fp-reachability-slice3/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--fp-reachability-slice b,c +^EXIT=0$ +^SIGNAL=0$ +1 file main.c line 34 +-- +^warning: ignoring +dead d; +dead e; +dead f; diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 09cc717343d..fb39602d9e1 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -933,6 +933,7 @@ void cbmc_parse_optionst::help() " --cover CC create test-suite with coverage criterion CC\n" // NOLINT(*) " --mm MM memory consistency model for concurrent programs\n" // NOLINT(*) HELP_REACHABILITY_SLICER + HELP_REACHABILITY_SLICER_FB " --full-slice run full slicer (experimental)\n" // NOLINT(*) " --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*) "\n" diff --git a/src/goto-instrument/full_slicer_class.h b/src/goto-instrument/full_slicer_class.h index 852d3c0c3b6..44aeec3b53c 100644 --- a/src/goto-instrument/full_slicer_class.h +++ b/src/goto-instrument/full_slicer_class.h @@ -113,6 +113,23 @@ class assert_criteriont:public slicing_criteriont } }; +class in_function_criteriont : public slicing_criteriont +{ +public: + explicit in_function_criteriont(const std::string &function_name) + : target_function(function_name) + { + } + + virtual bool operator()(goto_programt::const_targett target) + { + return target->function == target_function; + } + +protected: + const irep_idt target_function; +}; + class properties_criteriont:public slicing_criteriont { public: diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 8a1a8b7e938..311f9b802ad 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1430,6 +1430,15 @@ void goto_instrument_parse_optionst::instrument_goto_program() reachability_slicer(goto_model); } + if(cmdline.isset("fp-reachability-slice")) + { + do_indirect_call_and_rtti_removal(); + + status() << "Performing a function pointer reachability slice" << eom; + function_path_reachability_slicer( + goto_model, cmdline.get_comma_separated_values("fp-reachability-slice")); + } + // full slice? if(cmdline.isset("full-slice")) { @@ -1610,7 +1619,7 @@ void goto_instrument_parse_optionst::help() " --render-cluster-function clusterises the dot by functions\n" "\n" "Slicing:\n" - " --reachability-slice slice away instructions that can't reach assertions\n" // NOLINT(*) + HELP_REACHABILITY_SLICER " --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(*) diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 5f55a73792f..747cdd7b22d 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -71,6 +71,7 @@ Author: Daniel Kroening, kroening@kroening.com "(show-struct-alignment)(interval-analysis)(show-intervals)" \ "(show-uninitialized)(show-locations)" \ "(full-slice)(reachability-slice)(slice-global-inits)" \ + "(fp-reachability-slice):" \ "(inline)(partial-inline)(function-inline):(log):(no-caching)" \ OPT_REMOVE_CONST_FUNCTION_POINTERS \ "(print-internal-representation)" \ diff --git a/src/goto-instrument/reachability_slicer.cpp b/src/goto-instrument/reachability_slicer.cpp index 788e1fa52d6..61557c2f9a5 100644 --- a/src/goto-instrument/reachability_slicer.cpp +++ b/src/goto-instrument/reachability_slicer.cpp @@ -17,9 +17,12 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include +#include #include #include -#include + +#include "util/message.h" #include "full_slicer_class.h" #include "reachability_slicer_class.h" @@ -91,8 +94,7 @@ void reachability_slicert::fixedpoint_to_assertions( "all function return edges should point to the successor of a " "FUNCTION_CALL instruction"); stack.emplace_back(edge.first, true); - stack.emplace_back( - cfg.entry_map[std::prev(node.PC)], caller_is_known); + stack.emplace_back(cfg.entry_map[std::prev(node.PC)], caller_is_known); } else if(pred_node.PC->is_function_call()) { @@ -193,7 +195,7 @@ void reachability_slicert::slice(goto_functionst &goto_functions) { Forall_goto_program_instructions(i_it, f_it->second.body) { - const cfgt::nodet &e=cfg[cfg.entry_map[i_it]]; + cfgt::nodet &e = cfg[cfg.entry_map[i_it]]; if( !e.reaches_assertion && !e.reachable_from_assertion && !i_it->is_end_function()) @@ -240,6 +242,29 @@ void reachability_slicer( s(goto_model.goto_functions, p, include_forward_reachability); } +/// Perform reachability slicing on goto_model for selected functions. +/// \param goto_model Goto program to slice +/// \param functions_list The functions relevant for the slicing (i.e. starting +/// point for the search in the CFG). Anything that is reachable in the CFG +/// starting from these functions will be kept. +void function_path_reachability_slicer( + goto_modelt &goto_model, + const std::list &functions_list) +{ + for(const auto &function : functions_list) + { + in_function_criteriont matching_criterion(function); + reachability_slicert slicer; + slicer(goto_model.goto_functions, matching_criterion, true); + } + + remove_calls_no_bodyt remove_calls_no_body; + remove_calls_no_body(goto_model.goto_functions); + + goto_model.goto_functions.update(); + goto_model.goto_functions.compute_loop_numbers(); +} + /// Perform reachability slicing on goto_model, with respect to criterion /// comprising all properties. Only instructions from which the criterion /// is reachable will be kept. diff --git a/src/goto-instrument/reachability_slicer.h b/src/goto-instrument/reachability_slicer.h index 913d570b7e8..1d112084d60 100644 --- a/src/goto-instrument/reachability_slicer.h +++ b/src/goto-instrument/reachability_slicer.h @@ -23,6 +23,10 @@ void reachability_slicer( goto_modelt &, const std::list &properties); +void function_path_reachability_slicer( + goto_modelt &goto_model, + const std::list &functions_list); + void reachability_slicer( goto_modelt &, const bool include_forward_reachability); @@ -33,13 +37,18 @@ void reachability_slicer( const bool include_forward_reachability); // clang-format off -#define OPT_REACHABILITY_SLICER \ - "(reachability-slice)(reachability-slice-fb)" // NOLINT(*) - -#define HELP_REACHABILITY_SLICER \ - " --reachability-slice remove instructions that cannot appear on\n" \ - " a trace from entry point to a property\n" \ - " --reachability-slice-fb remove instructions that cannot appear on\n" \ - " a trace from entry point through a property\n" // NOLINT(*) +#define OPT_REACHABILITY_SLICER \ + "(fp-reachability-slice):(reachability-slice)(reachability-slice-fb)" // NOLINT(*) + +#define HELP_REACHABILITY_SLICER \ + " --fp-reachability-slice f remove instructions that cannot appear on a trace\n" \ + " that visits all given functions. The list of\n" \ + " functions has to be given as a comma separated\n" \ + " list f.\n" \ + " --reachability-slice remove instructions that cannot appear on a trace\n" \ + " from entry point to a property\n" // NOLINT(*) +#define HELP_REACHABILITY_SLICER_FB \ + " --reachability-slice-fb remove instructions that cannot appear on a trace\n" \ + " from entry point through a property\n" // NOLINT(*) // clang-format on #endif // CPROVER_GOTO_INSTRUMENT_REACHABILITY_SLICER_H diff --git a/src/util/cmdline.cpp b/src/util/cmdline.cpp index b022fdce78d..d4db5873266 100644 --- a/src/util/cmdline.cpp +++ b/src/util/cmdline.cpp @@ -118,6 +118,23 @@ const std::list &cmdlinet::get_values( return immutable_empty_list; } +std::list +cmdlinet::get_comma_separated_values(const char *option) const +{ + std::list separated_values; + auto i = getoptnr(option); + if(i.has_value() && !options[*i].values.empty()) + { + std::istringstream values_stream(options[*i].values.front()); + std::string single_value; + while(std::getline(values_stream, single_value, ',')) + { + separated_values.push_back(single_value); + } + } + return separated_values; +} + optionalt cmdlinet::getoptnr(char option) const { for(std::size_t i=0; i &get_values(const std::string &option) const; const std::list &get_values(char option) const; + std::list get_comma_separated_values(const char *option) const; + virtual bool isset(char option) const; virtual bool isset(const char *option) const; virtual void set(const std::string &option);