From 8ab58e6c03d5230ba6d726ed7be53079c58d757a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 4 Dec 2021 20:52:04 +0000 Subject: [PATCH 1/3] Remove reachability_slicert::operator() definition to cpp file This is a non-trivial implementation with external dependencies. Upcoming changes will make it even more complex. --- src/goto-instrument/reachability_slicer.cpp | 26 ++++++++++++++++--- .../reachability_slicer_class.h | 22 +++------------- 2 files changed, 26 insertions(+), 22 deletions(-) diff --git a/src/goto-instrument/reachability_slicer.cpp b/src/goto-instrument/reachability_slicer.cpp index a62caafc101..1a04b94f581 100644 --- a/src/goto-instrument/reachability_slicer.cpp +++ b/src/goto-instrument/reachability_slicer.cpp @@ -13,17 +13,37 @@ Author: Daniel Kroening, kroening@kroening.com /// (and possibly, depending on the parameters, keep those that can be reached /// from the criterion). +#include "full_slicer_class.h" #include "reachability_slicer.h" +#include "reachability_slicer_class.h" + +#include #include #include #include #include -#include +#include -#include "full_slicer_class.h" -#include "reachability_slicer_class.h" +void reachability_slicert::operator()( + goto_functionst &goto_functions, + const slicing_criteriont &criterion, + bool include_forward_reachability) +{ + cfg(goto_functions); + for(const auto &gf_entry : goto_functions.function_map) + { + forall_goto_program_instructions(i_it, gf_entry.second.body) + cfg[cfg.entry_map[i_it]].function_id = gf_entry.first; + } + + is_threadedt is_threaded(goto_functions); + fixedpoint_to_assertions(is_threaded, criterion); + if(include_forward_reachability) + fixedpoint_from_assertions(is_threaded, criterion); + slice(goto_functions); +} /// Get the set of nodes that correspond to the given criterion, or that can /// appear in concurrent execution. None of these should be sliced away so diff --git a/src/goto-instrument/reachability_slicer_class.h b/src/goto-instrument/reachability_slicer_class.h index 5bf92eab263..6a0163a85fa 100644 --- a/src/goto-instrument/reachability_slicer_class.h +++ b/src/goto-instrument/reachability_slicer_class.h @@ -12,11 +12,9 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_GOTO_INSTRUMENT_REACHABILITY_SLICER_CLASS_H #define CPROVER_GOTO_INSTRUMENT_REACHABILITY_SLICER_CLASS_H -#include -#include - -#include +#include +class goto_functionst; class slicing_criteriont; class reachability_slicert @@ -25,21 +23,7 @@ class reachability_slicert void operator()( goto_functionst &goto_functions, const slicing_criteriont &criterion, - bool include_forward_reachability) - { - cfg(goto_functions); - for(const auto &gf_entry : goto_functions.function_map) - { - forall_goto_program_instructions(i_it, gf_entry.second.body) - cfg[cfg.entry_map[i_it]].function_id = gf_entry.first; - } - - is_threadedt is_threaded(goto_functions); - fixedpoint_to_assertions(is_threaded, criterion); - if(include_forward_reachability) - fixedpoint_from_assertions(is_threaded, criterion); - slice(goto_functions); - } + bool include_forward_reachability); protected: struct slicer_entryt From 46e69a4b0de6bf7faf9b2f898545440105118516 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 4 Dec 2021 21:10:37 +0000 Subject: [PATCH 2/3] Reachability slice requires function bodies Reachability slicing relies on the CFG. The CFG, however, will not contain edges from a function call to the next instruction when no body is available for the function call. Therefore, reachability slicing requires two steps: - The model library needs to be applied. CBMC already did so, goto-instrument now does with this commit. - Remaining function calls without body need to be replaced by nondet-return-value assignments. Fixes: #6394 --- .../goto-instrument/reachability-slice/main.c | 21 +++++++++++++++++++ .../reachability-slice/test.desc | 8 +++++++ .../goto_instrument_parse_options.cpp | 7 +++++-- src/goto-instrument/reachability_slicer.cpp | 10 ++++++++- 4 files changed, 43 insertions(+), 3 deletions(-) create mode 100644 regression/goto-instrument/reachability-slice/main.c create mode 100644 regression/goto-instrument/reachability-slice/test.desc diff --git a/regression/goto-instrument/reachability-slice/main.c b/regression/goto-instrument/reachability-slice/main.c new file mode 100644 index 00000000000..5fcd6a1ff7a --- /dev/null +++ b/regression/goto-instrument/reachability-slice/main.c @@ -0,0 +1,21 @@ +#include + +void undefined_function(); + +void a() +{ + undefined_function(); +} + +void b() +{ + int should_be_sliced_away; +} + +int main() +{ + int *p = malloc(sizeof(int)); + a(); + __CPROVER_assert(0, "reach me"); + b(); +} diff --git a/regression/goto-instrument/reachability-slice/test.desc b/regression/goto-instrument/reachability-slice/test.desc new file mode 100644 index 00000000000..b7d09bbff42 --- /dev/null +++ b/regression/goto-instrument/reachability-slice/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--reachability-slice +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +should_be_sliced_away diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index a99d5caa850..e6328e738f5 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1066,8 +1066,11 @@ void goto_instrument_parse_optionst::instrument_goto_program() // we add the library in some cases, as some analyses benefit - if(cmdline.isset("add-library") || - cmdline.isset("mm")) + if( + cmdline.isset("add-library") || cmdline.isset("mm") || + cmdline.isset("reachability-slice") || + cmdline.isset("reachability-slice-fb") || + cmdline.isset("fp-reachability-slice")) { if(cmdline.isset("show-custom-bitvector-analysis") || cmdline.isset("custom-bitvector-analysis")) diff --git a/src/goto-instrument/reachability_slicer.cpp b/src/goto-instrument/reachability_slicer.cpp index 1a04b94f581..3a970f77a32 100644 --- a/src/goto-instrument/reachability_slicer.cpp +++ b/src/goto-instrument/reachability_slicer.cpp @@ -14,7 +14,6 @@ Author: Daniel Kroening, kroening@kroening.com /// from the criterion). #include "full_slicer_class.h" -#include "reachability_slicer.h" #include "reachability_slicer_class.h" #include @@ -26,11 +25,20 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include "reachability_slicer.h" + void reachability_slicert::operator()( goto_functionst &goto_functions, const slicing_criteriont &criterion, bool include_forward_reachability) { + // Replace function calls without body by non-deterministic return values to + // ensure the CFG does not consider instructions after such a call to be + // unreachable. + remove_calls_no_bodyt remove_calls_no_body; + remove_calls_no_body(goto_functions); + goto_functions.update(); + cfg(goto_functions); for(const auto &gf_entry : goto_functions.function_map) { From 0359a871f75ea03058d0c27238855dc400af6f70 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 14 Jan 2022 22:48:06 +0000 Subject: [PATCH 3/3] remove_calls_no_body: generate status output Use of this functionality will make symex warnings about functions without body go away. To make up for this, at least status output should be produced to ensure that this possible soundness issue of the verification result can be caught. --- jbmc/src/jbmc/jbmc_parse_options.cpp | 14 ++++-- .../reachability-slice/test.desc | 1 + src/cbmc/cbmc_parse_options.cpp | 18 ++++++-- .../goto_instrument_parse_options.cpp | 22 ++++++--- src/goto-instrument/reachability_slicer.cpp | 45 +++++++++++++------ src/goto-instrument/reachability_slicer.h | 15 ++++--- .../reachability_slicer_class.h | 4 +- src/goto-programs/remove_calls_no_body.cpp | 19 ++++++-- src/goto-programs/remove_calls_no_body.h | 6 ++- 9 files changed, 104 insertions(+), 40 deletions(-) diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 60e1adc98a5..873d0c2c2e3 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -962,18 +962,24 @@ bool jbmc_parse_optionst::process_goto_functions( log.status() << "Performing a forwards-backwards reachability slice" << messaget::eom; if(cmdline.isset("property")) - reachability_slicer(goto_model, cmdline.get_values("property"), true); + { + reachability_slicer( + goto_model, cmdline.get_values("property"), true, ui_message_handler); + } else - reachability_slicer(goto_model, true); + reachability_slicer(goto_model, true, ui_message_handler); } if(cmdline.isset("reachability-slice")) { log.status() << "Performing a reachability slice" << messaget::eom; if(cmdline.isset("property")) - reachability_slicer(goto_model, cmdline.get_values("property")); + { + reachability_slicer( + goto_model, cmdline.get_values("property"), ui_message_handler); + } else - reachability_slicer(goto_model); + reachability_slicer(goto_model, ui_message_handler); } // full slice? diff --git a/regression/goto-instrument/reachability-slice/test.desc b/regression/goto-instrument/reachability-slice/test.desc index b7d09bbff42..d7e1a6fc705 100644 --- a/regression/goto-instrument/reachability-slice/test.desc +++ b/regression/goto-instrument/reachability-slice/test.desc @@ -1,6 +1,7 @@ CORE main.c --reachability-slice +Removing call to undefined_function, which has no body ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index ba9d672de8a..f1315686b26 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -944,19 +944,29 @@ bool cbmc_parse_optionst::process_goto_program( log.status() << "Performing a forwards-backwards reachability slice" << messaget::eom; if(options.is_set("property")) + { reachability_slicer( - goto_model, options.get_list_option("property"), true); + goto_model, + options.get_list_option("property"), + true, + log.get_message_handler()); + } else - reachability_slicer(goto_model, true); + reachability_slicer(goto_model, true, log.get_message_handler()); } if(options.get_bool_option("reachability-slice")) { log.status() << "Performing a reachability slice" << messaget::eom; if(options.is_set("property")) - reachability_slicer(goto_model, options.get_list_option("property")); + { + reachability_slicer( + goto_model, + options.get_list_option("property"), + log.get_message_handler()); + } else - reachability_slicer(goto_model); + reachability_slicer(goto_model, log.get_message_handler()); } // full slice? diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index e6328e738f5..2413dcb6b23 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -841,7 +841,7 @@ int goto_instrument_parse_optionst::doit() log.status() << "Removing calls to functions without a body" << messaget::eom; remove_calls_no_bodyt remove_calls_no_body; - remove_calls_no_body(goto_model.goto_functions); + remove_calls_no_body(goto_model.goto_functions, ui_message_handler); log.status() << "Accelerating" << messaget::eom; guard_managert guard_manager; @@ -1248,7 +1248,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() << messaget::eom; remove_calls_no_bodyt remove_calls_no_body; - remove_calls_no_body(goto_model.goto_functions); + remove_calls_no_body(goto_model.goto_functions, ui_message_handler); goto_model.goto_functions.update(); goto_model.goto_functions.compute_loop_numbers(); @@ -1605,9 +1605,12 @@ void goto_instrument_parse_optionst::instrument_goto_program() goto_model.goto_functions.update(); if(cmdline.isset("property")) - reachability_slicer(goto_model, cmdline.get_values("property")); + { + reachability_slicer( + goto_model, cmdline.get_values("property"), ui_message_handler); + } else - reachability_slicer(goto_model); + reachability_slicer(goto_model, ui_message_handler); } if(cmdline.isset("fp-reachability-slice")) @@ -1617,7 +1620,9 @@ void goto_instrument_parse_optionst::instrument_goto_program() log.status() << "Performing a function pointer reachability slice" << messaget::eom; function_path_reachability_slicer( - goto_model, cmdline.get_comma_separated_values("fp-reachability-slice")); + goto_model, + cmdline.get_comma_separated_values("fp-reachability-slice"), + ui_message_handler); } // full slice? @@ -1690,9 +1695,12 @@ void goto_instrument_parse_optionst::instrument_goto_program() log.status() << "Performing a reachability slice" << messaget::eom; if(cmdline.isset("property")) - reachability_slicer(goto_model, cmdline.get_values("property")); + { + reachability_slicer( + goto_model, cmdline.get_values("property"), ui_message_handler); + } else - reachability_slicer(goto_model); + reachability_slicer(goto_model, ui_message_handler); } if(cmdline.isset("ensure-one-backedge-per-target")) diff --git a/src/goto-instrument/reachability_slicer.cpp b/src/goto-instrument/reachability_slicer.cpp index 3a970f77a32..ca594ec1819 100644 --- a/src/goto-instrument/reachability_slicer.cpp +++ b/src/goto-instrument/reachability_slicer.cpp @@ -30,13 +30,14 @@ Author: Daniel Kroening, kroening@kroening.com void reachability_slicert::operator()( goto_functionst &goto_functions, const slicing_criteriont &criterion, - bool include_forward_reachability) + bool include_forward_reachability, + message_handlert &message_handler) { // Replace function calls without body by non-deterministic return values to // ensure the CFG does not consider instructions after such a call to be // unreachable. remove_calls_no_bodyt remove_calls_no_body; - remove_calls_no_body(goto_functions); + remove_calls_no_body(goto_functions, message_handler); goto_functions.update(); cfg(goto_functions); @@ -392,13 +393,18 @@ void reachability_slicert::slice(goto_functionst &goto_functions) /// \param include_forward_reachability: Determines if only instructions /// from which the criterion is reachable should be kept (false) or also /// those reachable from the criterion (true) +/// \param message_handler: message handler void reachability_slicer( goto_modelt &goto_model, - const bool include_forward_reachability) + const bool include_forward_reachability, + message_handlert &message_handler) { reachability_slicert s; assert_criteriont a; - s(goto_model.goto_functions, a, include_forward_reachability); + s(goto_model.goto_functions, + a, + include_forward_reachability, + message_handler); } /// Perform reachability slicing on goto_model for selected properties. @@ -408,14 +414,19 @@ void reachability_slicer( /// \param include_forward_reachability: Determines if only instructions /// from which the criterion is reachable should be kept (false) or also /// those reachable from the criterion (true) +/// \param message_handler: message handler void reachability_slicer( goto_modelt &goto_model, const std::list &properties, - const bool include_forward_reachability) + const bool include_forward_reachability, + message_handlert &message_handler) { reachability_slicert s; properties_criteriont p(properties); - s(goto_model.goto_functions, p, include_forward_reachability); + s(goto_model.goto_functions, + p, + include_forward_reachability, + message_handler); } /// Perform reachability slicing on goto_model for selected functions. @@ -423,19 +434,22 @@ void reachability_slicer( /// \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. +/// \param message_handler: message handler void function_path_reachability_slicer( goto_modelt &goto_model, - const std::list &functions_list) + const std::list &functions_list, + message_handlert &message_handler) { for(const auto &function : functions_list) { in_function_criteriont matching_criterion(function); reachability_slicert slicer; - slicer(goto_model.goto_functions, matching_criterion, true); + slicer( + goto_model.goto_functions, matching_criterion, true, message_handler); } remove_calls_no_bodyt remove_calls_no_body; - remove_calls_no_body(goto_model.goto_functions); + remove_calls_no_body(goto_model.goto_functions, message_handler); goto_model.goto_functions.update(); goto_model.goto_functions.compute_loop_numbers(); @@ -445,9 +459,12 @@ void function_path_reachability_slicer( /// comprising all properties. Only instructions from which the criterion /// is reachable will be kept. /// \param goto_model: Goto program to slice -void reachability_slicer(goto_modelt &goto_model) +/// \param message_handler: message handler +void reachability_slicer( + goto_modelt &goto_model, + message_handlert &message_handler) { - reachability_slicer(goto_model, false); + reachability_slicer(goto_model, false, message_handler); } /// Perform reachability slicing on goto_model for selected properties. Only @@ -455,9 +472,11 @@ void reachability_slicer(goto_modelt &goto_model) /// \param goto_model: Goto program to slice /// \param properties: The properties relevant for the slicing (i.e. starting /// point for the search in the cfg) +/// \param message_handler: message handler void reachability_slicer( goto_modelt &goto_model, - const std::list &properties) + const std::list &properties, + message_handlert &message_handler) { - reachability_slicer(goto_model, properties, false); + reachability_slicer(goto_model, properties, false, message_handler); } diff --git a/src/goto-instrument/reachability_slicer.h b/src/goto-instrument/reachability_slicer.h index 1d112084d60..36fe5a4fef8 100644 --- a/src/goto-instrument/reachability_slicer.h +++ b/src/goto-instrument/reachability_slicer.h @@ -16,25 +16,30 @@ Author: Daniel Kroening, kroening@kroening.com #include class goto_modelt; +class message_handlert; -void reachability_slicer(goto_modelt &); +void reachability_slicer(goto_modelt &, message_handlert &); void reachability_slicer( goto_modelt &, - const std::list &properties); + const std::list &properties, + message_handlert &); void function_path_reachability_slicer( goto_modelt &goto_model, - const std::list &functions_list); + const std::list &functions_list, + message_handlert &); void reachability_slicer( goto_modelt &, - const bool include_forward_reachability); + const bool include_forward_reachability, + message_handlert &); void reachability_slicer( goto_modelt &, const std::list &properties, - const bool include_forward_reachability); + const bool include_forward_reachability, + message_handlert &); // clang-format off #define OPT_REACHABILITY_SLICER \ diff --git a/src/goto-instrument/reachability_slicer_class.h b/src/goto-instrument/reachability_slicer_class.h index 6a0163a85fa..f6831e71c5e 100644 --- a/src/goto-instrument/reachability_slicer_class.h +++ b/src/goto-instrument/reachability_slicer_class.h @@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com #include class goto_functionst; +class message_handlert; class slicing_criteriont; class reachability_slicert @@ -23,7 +24,8 @@ class reachability_slicert void operator()( goto_functionst &goto_functions, const slicing_criteriont &criterion, - bool include_forward_reachability); + bool include_forward_reachability, + message_handlert &); protected: struct slicer_entryt diff --git a/src/goto-programs/remove_calls_no_body.cpp b/src/goto-programs/remove_calls_no_body.cpp index 857d04d1f37..3384430a310 100644 --- a/src/goto-programs/remove_calls_no_body.cpp +++ b/src/goto-programs/remove_calls_no_body.cpp @@ -12,6 +12,7 @@ Author: Daniel Poetzl #include "remove_calls_no_body.h" #include +#include #include #include "goto_functions.h" @@ -94,14 +95,21 @@ bool remove_calls_no_bodyt::is_opaque_function_call( /// \param goto_program: goto program to operate on /// \param goto_functions: all goto functions; for looking up functions which /// the goto program may call -void remove_calls_no_bodyt:: -operator()(goto_programt &goto_program, const goto_functionst &goto_functions) +/// \param message_handler: message handler +void remove_calls_no_bodyt::operator()( + goto_programt &goto_program, + const goto_functionst &goto_functions, + message_handlert &message_handler) { for(goto_programt::targett it = goto_program.instructions.begin(); it != goto_program.instructions.end();) // no it++ { if(is_opaque_function_call(it, goto_functions)) { + messaget log{message_handler}; + log.status() << "Removing call to " + << to_symbol_expr(it->call_function()).get_identifier() + << ", which has no body" << messaget::eom; remove_call_no_body( goto_program, it, it->call_lhs(), it->call_arguments()); } @@ -116,10 +124,13 @@ operator()(goto_programt &goto_program, const goto_functionst &goto_functions) /// of the arguments of the call and a nondet assignment to the variable taking /// the return value. /// \param goto_functions: goto functions to operate on -void remove_calls_no_bodyt::operator()(goto_functionst &goto_functions) +/// \param message_handler: message handler +void remove_calls_no_bodyt::operator()( + goto_functionst &goto_functions, + message_handlert &message_handler) { for(auto &gf_entry : goto_functions.function_map) { - (*this)(gf_entry.second.body, goto_functions); + (*this)(gf_entry.second.body, goto_functions, message_handler); } } diff --git a/src/goto-programs/remove_calls_no_body.h b/src/goto-programs/remove_calls_no_body.h index 9b7382328ce..3a18adb66f9 100644 --- a/src/goto-programs/remove_calls_no_body.h +++ b/src/goto-programs/remove_calls_no_body.h @@ -15,6 +15,7 @@ Author: Daniel Poetzl #include "goto_program.h" class goto_functionst; +class message_handlert; class remove_calls_no_bodyt { @@ -32,9 +33,10 @@ class remove_calls_no_bodyt public: void operator()( goto_programt &goto_program, - const goto_functionst &goto_functions); + const goto_functionst &goto_functions, + message_handlert &); - void operator()(goto_functionst &goto_functions); + void operator()(goto_functionst &goto_functions, message_handlert &); }; #define OPT_REMOVE_CALLS_NO_BODY "(remove-calls-no-body)"