From e823538bacd663bd4a700b0a7901f124a40972ab Mon Sep 17 00:00:00 2001 From: Kareem Khazem Date: Tue, 27 Feb 2018 06:40:58 +0000 Subject: [PATCH 1/7] Symex paths saved onto abstract data structure This commit introduces a new data type, path_queuet, representing saved symbolic execution paths, used instead of the std::list. This allows us to implement custom logic for saving and removing paths, rather than simply pushing to the back and popping the front. This commit introduces a concrete instantiation of path_queuet, called path_fifot, with the same functionality as the old std::list. This is in preparation for further instantiations that implement more sophisticated logic for deciding which path should be resumed next. --- src/cbmc/bmc.cpp | 21 ++--- src/cbmc/bmc.h | 28 ++++--- src/cbmc/symex_bmc.cpp | 4 +- src/cbmc/symex_bmc.h | 3 +- .../accelerate/scratch_program.h | 7 +- src/goto-symex/Makefile | 1 + src/goto-symex/goto_symex.h | 26 +----- src/goto-symex/path_storage.cpp | 40 +++++++++ src/goto-symex/path_storage.h | 82 +++++++++++++++++++ src/goto-symex/symex_goto.cpp | 4 +- 10 files changed, 163 insertions(+), 53 deletions(-) create mode 100644 src/goto-symex/path_storage.cpp create mode 100644 src/goto-symex/path_storage.h diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index 34edbb516a6..cec72e369dd 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -605,7 +605,8 @@ int bmct::do_language_agnostic_bmc( const symbol_tablet &symbol_table = model.get_symbol_table(); message_handlert &mh = message.get_message_handler(); safety_checkert::resultt result; - goto_symext::branch_worklistt worklist; + std::unique_ptr worklist = + path_storaget::make(path_storaget::disciplinet::FIFO); try { { @@ -614,17 +615,17 @@ int bmct::do_language_agnostic_bmc( std::unique_ptr cbmc_solver; cbmc_solver = solvers.get_solver(); prop_convt &pc = cbmc_solver->prop_conv(); - bmct bmc(opts, symbol_table, mh, pc, worklist, callback_after_symex); + bmct bmc(opts, symbol_table, mh, pc, *worklist, callback_after_symex); bmc.set_ui(ui); if(driver_configure_bmc) driver_configure_bmc(bmc, symbol_table); result = bmc.run(model); } INVARIANT( - opts.get_bool_option("paths") || worklist.empty(), + opts.get_bool_option("paths") || worklist->empty(), "the worklist should be empty after doing full-program " "model checking, but the worklist contains " + - std::to_string(worklist.size()) + " unexplored branches."); + std::to_string(worklist->size()) + " unexplored branches."); // When model checking, the bmc.run() above will already have explored // the entire program, and result contains the verification result. The @@ -641,10 +642,10 @@ int bmct::do_language_agnostic_bmc( // difference between the implementations of perform_symbolic_exection() // in bmct and path_explorert, for more information. - while(!worklist.empty()) + while(!worklist->empty()) { message.status() << "___________________________\n" - << "Starting new path (" << worklist.size() + << "Starting new path (" << worklist->size() << " to go)\n" << message.eom; cbmc_solverst solvers(opts, symbol_table, message.get_message_handler()); @@ -652,7 +653,7 @@ int bmct::do_language_agnostic_bmc( std::unique_ptr cbmc_solver; cbmc_solver = solvers.get_solver(); prop_convt &pc = cbmc_solver->prop_conv(); - goto_symext::branch_pointt &resume = worklist.front(); + path_storaget::patht &resume = worklist->peek(); path_explorert pe( opts, symbol_table, @@ -660,12 +661,12 @@ int bmct::do_language_agnostic_bmc( pc, resume.equation, resume.state, - worklist, + *worklist, callback_after_symex); if(driver_configure_bmc) driver_configure_bmc(pe, symbol_table); result &= pe.run(model); - worklist.pop_front(); + worklist->pop(); } } catch(const char *error_msg) @@ -701,7 +702,7 @@ void bmct::perform_symbolic_execution( { symex.symex_from_entry_point_of(get_goto_function, symex_symbol_table); INVARIANT( - options.get_bool_option("paths") || branch_worklist.empty(), + options.get_bool_option("paths") || path_storage.empty(), "Branch points were saved even though we should have been " "executing the entire program and merging paths"); } diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h index 551fa7c2b3d..3077f27d554 100644 --- a/src/cbmc/bmc.h +++ b/src/cbmc/bmc.h @@ -23,6 +23,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + #include #include #include @@ -49,32 +51,32 @@ class bmct:public safety_checkert /// constructor is `false` (unset), an instance of this class will /// symbolically execute the entire program, performing path merging /// to build a formula corresponding to all executions of the program - /// up to the unwinding limit. In this case, the `branch_worklist` + /// up to the unwinding limit. In this case, the `path_storage` /// member shall not be touched; this is enforced by the assertion in /// this class' implementation of bmct::perform_symbolic_execution(). /// /// - If the `--paths` flag is `true`, this `bmct` object will explore a /// single path through the codebase without doing any path merging. /// If some paths were not taken, the state at those branch points - /// will be appended to `branch_worklist`. After the single path that + /// will be appended to `path_storage`. After the single path that /// this `bmct` object executed has been model-checked, you can resume /// exploring further paths by popping an element from - /// `branch_worklist` and using it to construct a path_explorert + /// `path_storage` and using it to construct a path_explorert /// object. bmct( const optionst &_options, const symbol_tablet &outer_symbol_table, message_handlert &_message_handler, prop_convt &_prop_conv, - goto_symext::branch_worklistt &_branch_worklist, + path_storaget &_path_storage, std::function callback_after_symex) : safety_checkert(ns, _message_handler), options(_options), outer_symbol_table(outer_symbol_table), ns(outer_symbol_table, symex_symbol_table), equation(), - branch_worklist(_branch_worklist), - symex(_message_handler, outer_symbol_table, equation, branch_worklist), + path_storage(_path_storage), + symex(_message_handler, outer_symbol_table, equation, path_storage), prop_conv(_prop_conv), ui(ui_message_handlert::uit::PLAIN), driver_callback_after_symex(callback_after_symex) @@ -128,7 +130,7 @@ class bmct:public safety_checkert /// /// This constructor exists as a delegate for the path_explorert class. /// It differs from \ref bmct's public constructor in that it actually - /// does something with the branch_worklistt argument, and also takes a + /// does something with the path_storaget argument, and also takes a /// symex_target_equationt. See the documentation for path_explorert for /// details. bmct( @@ -137,15 +139,15 @@ class bmct:public safety_checkert message_handlert &_message_handler, prop_convt &_prop_conv, symex_target_equationt &_equation, - goto_symext::branch_worklistt &_branch_worklist, + path_storaget &_path_storage, std::function callback_after_symex) : safety_checkert(ns, _message_handler), options(_options), outer_symbol_table(outer_symbol_table), ns(outer_symbol_table), equation(_equation), - branch_worklist(_branch_worklist), - symex(_message_handler, outer_symbol_table, equation, branch_worklist), + path_storage(_path_storage), + symex(_message_handler, outer_symbol_table, equation, path_storage), prop_conv(_prop_conv), ui(ui_message_handlert::uit::PLAIN), driver_callback_after_symex(callback_after_symex) @@ -166,7 +168,7 @@ class bmct:public safety_checkert symbol_tablet symex_symbol_table; namespacet ns; symex_target_equationt equation; - goto_symext::branch_worklistt &branch_worklist; + path_storaget &path_storage; symex_bmct symex; prop_convt &prop_conv; std::unique_ptr memory_model; @@ -257,7 +259,7 @@ class path_explorert : public bmct prop_convt &_prop_conv, symex_target_equationt &saved_equation, const goto_symex_statet &saved_state, - goto_symext::branch_worklistt &branch_worklist, + path_storaget &path_storage, std::function callback_after_symex) : bmct( _options, @@ -265,7 +267,7 @@ class path_explorert : public bmct _message_handler, _prop_conv, saved_equation, - branch_worklist, + path_storage, callback_after_symex), saved_state(saved_state) { diff --git a/src/cbmc/symex_bmc.cpp b/src/cbmc/symex_bmc.cpp index 1bbd5af77e0..986e368ea45 100644 --- a/src/cbmc/symex_bmc.cpp +++ b/src/cbmc/symex_bmc.cpp @@ -22,8 +22,8 @@ symex_bmct::symex_bmct( message_handlert &mh, const symbol_tablet &outer_symbol_table, symex_target_equationt &_target, - goto_symext::branch_worklistt &branch_worklist) - : goto_symext(mh, outer_symbol_table, _target, branch_worklist), + path_storaget &path_storage) + : goto_symext(mh, outer_symbol_table, _target, path_storage), record_coverage(false), max_unwind(0), max_unwind_is_set(false), diff --git a/src/cbmc/symex_bmc.h b/src/cbmc/symex_bmc.h index b1b6108de9a..bc43242037b 100644 --- a/src/cbmc/symex_bmc.h +++ b/src/cbmc/symex_bmc.h @@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include "symex_coverage.h" @@ -26,7 +27,7 @@ class symex_bmct: public goto_symext message_handlert &mh, const symbol_tablet &outer_symbol_table, symex_target_equationt &_target, - goto_symext::branch_worklistt &branch_worklist); + path_storaget &path_storage); // To show progress source_locationt last_source_location; diff --git a/src/goto-instrument/accelerate/scratch_program.h b/src/goto-instrument/accelerate/scratch_program.h index 0bd76634bd0..ef07e370115 100644 --- a/src/goto-instrument/accelerate/scratch_program.h +++ b/src/goto-instrument/accelerate/scratch_program.h @@ -23,6 +23,7 @@ Author: Matt Lewis #include #include +#include #include #include @@ -41,8 +42,8 @@ class scratch_programt:public goto_programt symex_symbol_table(), ns(symbol_table, symex_symbol_table), equation(), - branch_worklist(), - symex(mh, symbol_table, equation, branch_worklist), + path_storage(), + symex(mh, symbol_table, equation, path_storage), satcheck(util_make_unique()), satchecker(ns, *satcheck), z3(ns, "accelerate", "", "", smt2_dect::solvert::Z3), @@ -78,7 +79,7 @@ class scratch_programt:public goto_programt symbol_tablet symex_symbol_table; namespacet ns; symex_target_equationt equation; - goto_symext::branch_worklistt branch_worklist; + path_fifot path_storage; goto_symext symex; std::unique_ptr satcheck; diff --git a/src/goto-symex/Makefile b/src/goto-symex/Makefile index 76f9bb61d91..dc4c73f3c15 100644 --- a/src/goto-symex/Makefile +++ b/src/goto-symex/Makefile @@ -8,6 +8,7 @@ SRC = adjust_float_expressions.cpp \ memory_model_sc.cpp \ memory_model_tso.cpp \ partial_order_concurrency.cpp \ + path_storage.cpp \ postcondition.cpp \ precondition.cpp \ rewrite_union.cpp \ diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index 117693b8391..7b71c1f0bbb 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "goto_symex_state.h" +#include "path_storage.h" #include "symex_target_equation.h" class byte_extract_exprt; @@ -47,30 +48,11 @@ class goto_symext public: typedef goto_symex_statet statet; - /// \brief Information saved at a conditional goto to resume execution - struct branch_pointt - { - symex_target_equationt equation; - statet state; - - explicit branch_pointt(const symex_target_equationt &e, const statet &s) - : equation(e), state(s, &equation) - { - } - - explicit branch_pointt(const branch_pointt &other) - : equation(other.equation), state(other.state, &equation) - { - } - }; - - typedef std::list branch_worklistt; - goto_symext( message_handlert &mh, const symbol_tablet &outer_symbol_table, symex_target_equationt &_target, - branch_worklistt &branch_worklist) + path_storaget &path_storage) : total_vccs(0), remaining_vccs(0), constant_propagation(true), @@ -81,7 +63,7 @@ class goto_symext atomic_section_counter(0), log(mh), guard_identifier("goto_symex::\\guard"), - branch_worklist(branch_worklist) + path_storage(path_storage) { options.set_option("simplify", true); options.set_option("assertions", true); @@ -462,7 +444,7 @@ class goto_symext void replace_nondet(exprt &); void rewrite_quantifiers(exprt &, statet &); - branch_worklistt &branch_worklist; + path_storaget &path_storage; }; #endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_H diff --git a/src/goto-symex/path_storage.cpp b/src/goto-symex/path_storage.cpp new file mode 100644 index 00000000000..528f1ce2b4e --- /dev/null +++ b/src/goto-symex/path_storage.cpp @@ -0,0 +1,40 @@ +/*******************************************************************\ + +Module: Path Storage + +Author: Kareem Khazem + +\*******************************************************************/ + +#include "path_storage.h" + +std::unique_ptr +path_storaget::make(path_storaget::disciplinet discipline) +{ + switch(discipline) + { + case path_storaget::disciplinet::FIFO: + return std::unique_ptr(new path_fifot()); + } + UNREACHABLE; +} + +path_storaget::patht &path_fifot::peek() +{ + return paths.front(); +} + +void path_fifot::push(const path_storaget::patht &bp) +{ + paths.push_back(bp); +} + +void path_fifot::pop() +{ + paths.pop_front(); +} + +std::size_t path_fifot::size() const +{ + return paths.size(); +} diff --git a/src/goto-symex/path_storage.h b/src/goto-symex/path_storage.h new file mode 100644 index 00000000000..eac73dab57e --- /dev/null +++ b/src/goto-symex/path_storage.h @@ -0,0 +1,82 @@ +/// \file path_storage.h +/// \brief Storage of symbolic execution paths to resume +/// \author Kareem Khazem + +#ifndef CPROVER_GOTO_SYMEX_PATH_STORAGE_H +#define CPROVER_GOTO_SYMEX_PATH_STORAGE_H + +#include "goto_symex_state.h" +#include "symex_target_equation.h" + +#include + +/// \brief Storage for symbolic execution paths to be resumed later +/// +/// This data structure supports saving partially-executed symbolic +/// execution \ref path_storaget::patht "paths" so that their execution can +/// be halted and resumed later. The choice of which path should be +/// resumed next is implemented by subtypes of this abstract class. +class path_storaget +{ +public: + /// \brief Derived types of path_storaget + enum class disciplinet + { + /// path_fifot + FIFO + }; + + /// \brief Information saved at a conditional goto to resume execution + struct patht + { + symex_target_equationt equation; + goto_symex_statet state; + + explicit patht(const symex_target_equationt &e, const goto_symex_statet &s) + : equation(e), state(s, &equation) + { + } + + explicit patht(const patht &other) + : equation(other.equation), state(other.state, &equation) + { + } + }; + + /// \brief Factory method for building a subtype of path_storaget + static std::unique_ptr make(disciplinet discipline); + virtual ~path_storaget() = default; + + /// \brief Reference to the next path to resume + virtual patht &peek() = 0; + + /// \brief Add a path to resume to the storage + virtual void push(const patht &bp) = 0; + + /// \brief Remove the next path to resume from the storage + virtual void pop() = 0; + + /// \brief How many paths does this storage contain? + virtual std::size_t size() const = 0; + + /// \brief Is this storage empty? + bool empty() const + { + return size() == 0; + }; +}; + +/// \brief FIFO save queue: paths are resumed in the order that they were saved +class path_fifot : public path_storaget +{ +public: + patht &peek() override; + void push(const patht &bp) override; + void pop() override; + std::size_t size() const override; + +protected: + std::list paths; +}; + +#endif /* CPROVER_GOTO_SYMEX_PATH_STORAGE_H */ diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index e25add14741..9255567a34e 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -181,14 +181,14 @@ void goto_symext::symex_goto(statet &state) // executing from, so that goto_symex::symex_goto() knows that we've already // explored the branch starting from `state_pc` when it is later called at // this branch. - branch_pointt branch_point(target, state); + path_storaget::patht branch_point(target, state); branch_point.state.saved_target = new_state_pc; branch_point.state.has_saved_target = true; // `forward` tells us where the branch we're _currently_ executing is // pointing to; this needs to be inverted for the branch that we're saving, // so let its truth value for `backwards` be the same as ours for `forward`. branch_point.state.saved_target_is_backwards = forward; - branch_worklist.push_back(branch_point); + path_storage.push(branch_point); log.debug() << "Saving '" << new_state_pc->source_location << "'" << log.eom; } From 2a86fb47d01171371c0bf3cfd30fc33f11c4838d Mon Sep 17 00:00:00 2001 From: Kareem Khazem Date: Sat, 3 Mar 2018 07:43:57 +0000 Subject: [PATCH 2/7] Bugfix: always print path exploration resume point Before this commit, CBMC would occasionally print "Resuming from ''" because the source location that it was accessing was null. --- src/goto-symex/symex_goto.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index 9255567a34e..1306f1a6ae1 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -169,7 +169,8 @@ void goto_symext::symex_goto(statet &state) goto_programt::const_targett tmp = new_state_pc; new_state_pc = state_pc; state_pc = tmp; - log.debug() << "Resuming from '" << state_pc->code.source_location() << "'" + + log.debug() << "Resuming from '" << state_pc->source_location << "'" << log.eom; } else if(options.get_bool_option("paths")) From 685937a79e9dc87016cb4d0a84455ed655b35b4b Mon Sep 17 00:00:00 2001 From: Kareem Khazem Date: Tue, 6 Mar 2018 07:51:17 +0000 Subject: [PATCH 3/7] Path exploration pushes both successors onto queue When doing path exploration and encountering a conditional goto instruction, both successors of the goto (the next instruction, and the target) are pushed onto the path exploration workqueue. This allows the symbolic execution caller to have complete control over which path to execute next. Prior to this commit, symex would push one successor onto the workqueue and continue executing the path of the other successor until the path was terminated. This commit introduces the possibility that symbolic execution pauses without reaching the end of a path, and needs to be resumed by the caller. Thus, new safety checker results are introduced (SUSPENDED and UNKNOWN); the former signals to the caller of symex that symex has not reached the end of a branch, and therefore no safety check has been performed. The (currently only) path exploration strategy still pops paths in the order that they were pushed. This behaviour means that the paths that it pops will always alternate between the next instruction of a goto, and the target of that same goto. The test suite is updated to reflect this strategy. --- src/cbmc/bmc.cpp | 33 +++++++++++++------ src/goto-programs/safety_checker.h | 44 +++++++++++++++++++++++++- src/goto-symex/goto_symex.h | 12 ++++++- src/goto-symex/goto_symex_state.h | 8 ++++- src/goto-symex/path_storage.cpp | 11 ++++--- src/goto-symex/path_storage.h | 40 ++++++++++++++++++----- src/goto-symex/symex_goto.cpp | 51 ++++++++++++++++++++---------- src/goto-symex/symex_main.cpp | 10 ++++-- 8 files changed, 165 insertions(+), 44 deletions(-) diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index cec72e369dd..be441f53443 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -342,6 +342,9 @@ safety_checkert::resultt bmct::execute( const goto_functionst &goto_functions = goto_model.get_goto_functions(); + if(symex.should_pause_symex) + return safety_checkert::resultt::PAUSED; + // This provides the driver program the opportunity to do things like a // symbol-table or goto-functions dump instead of actually running the // checker, like show-vcc except driver-program specific. @@ -602,9 +605,10 @@ int bmct::do_language_agnostic_bmc( std::function driver_configure_bmc, std::function callback_after_symex) { + safety_checkert::resultt final_result = safety_checkert::resultt::UNKNOWN; + safety_checkert::resultt tmp_result = safety_checkert::resultt::UNKNOWN; const symbol_tablet &symbol_table = model.get_symbol_table(); message_handlert &mh = message.get_message_handler(); - safety_checkert::resultt result; std::unique_ptr worklist = path_storaget::make(path_storaget::disciplinet::FIFO); try @@ -619,7 +623,9 @@ int bmct::do_language_agnostic_bmc( bmc.set_ui(ui); if(driver_configure_bmc) driver_configure_bmc(bmc, symbol_table); - result = bmc.run(model); + tmp_result = bmc.run(model); + if(tmp_result != safety_checkert::resultt::PAUSED) + final_result = tmp_result; } INVARIANT( opts.get_bool_option("paths") || worklist->empty(), @@ -628,8 +634,8 @@ int bmct::do_language_agnostic_bmc( std::to_string(worklist->size()) + " unexplored branches."); // When model checking, the bmc.run() above will already have explored - // the entire program, and result contains the verification result. The - // worklist (containing paths that have not yet been explored) is thus + // the entire program, and final_result contains the verification result. + // The worklist (containing paths that have not yet been explored) is thus // empty, and we don't enter this loop. // // When doing path exploration, there will be some saved paths left to @@ -644,10 +650,11 @@ int bmct::do_language_agnostic_bmc( while(!worklist->empty()) { - message.status() << "___________________________\n" - << "Starting new path (" << worklist->size() - << " to go)\n" - << message.eom; + if(tmp_result != safety_checkert::resultt::PAUSED) + message.status() << "___________________________\n" + << "Starting new path (" << worklist->size() + << " to go)\n" + << message.eom; cbmc_solverst solvers(opts, symbol_table, message.get_message_handler()); solvers.set_ui(ui); std::unique_ptr cbmc_solver; @@ -665,7 +672,9 @@ int bmct::do_language_agnostic_bmc( callback_after_symex); if(driver_configure_bmc) driver_configure_bmc(pe, symbol_table); - result &= pe.run(model); + tmp_result = pe.run(model); + if(tmp_result != safety_checkert::resultt::PAUSED) + final_result &= tmp_result; worklist->pop(); } } @@ -685,7 +694,7 @@ int bmct::do_language_agnostic_bmc( throw std::current_exception(); } - switch(result) + switch(final_result) { case safety_checkert::resultt::SAFE: return CPROVER_EXIT_VERIFICATION_SAFE; @@ -693,6 +702,10 @@ int bmct::do_language_agnostic_bmc( return CPROVER_EXIT_VERIFICATION_UNSAFE; case safety_checkert::resultt::ERROR: return CPROVER_EXIT_INTERNAL_ERROR; + case safety_checkert::resultt::UNKNOWN: + return CPROVER_EXIT_INTERNAL_ERROR; + case safety_checkert::resultt::PAUSED: + UNREACHABLE; } UNREACHABLE; } diff --git a/src/goto-programs/safety_checker.h b/src/goto-programs/safety_checker.h index 599669f4cce..b2aee4fab3e 100644 --- a/src/goto-programs/safety_checker.h +++ b/src/goto-programs/safety_checker.h @@ -30,7 +30,23 @@ class safety_checkert:public messaget const namespacet &_ns, message_handlert &_message_handler); - enum class resultt { SAFE, UNSAFE, ERROR }; + enum class resultt + { + /// No safety properties were violated + SAFE, + /// Some safety properties were violated + UNSAFE, + /// Safety is unknown due to an error during safety checking + ERROR, + /// Symbolic execution has been suspended due to encountering a GOTO while + /// doing path exploration; the symex state has been saved, and symex should + /// be resumed by the caller. + PAUSED, + /// We haven't yet assigned a safety check result to this object. A value of + /// UNKNOWN can be used to initialize a resultt object, and that object may + /// then safely be used with the |= and &= operators. + UNKNOWN + }; // check whether all assertions in goto_functions are safe // if UNSAFE, then a trace is returned @@ -47,11 +63,22 @@ class safety_checkert:public messaget }; /// \brief The worst of two results +/// +/// A result of PAUSED means that the safety check has not yet completed, +/// thus it makes no sense to compare it to the result of a completed safety +/// check. Therefore do not pass safety_checkert::resultt:PAUSED as an +/// argument to this function. inline safety_checkert::resultt & operator&=(safety_checkert::resultt &a, safety_checkert::resultt const &b) { + PRECONDITION( + a != safety_checkert::resultt::PAUSED && + b != safety_checkert::resultt::PAUSED); switch(a) { + case safety_checkert::resultt::UNKNOWN: + a = b; + return a; case safety_checkert::resultt::ERROR: return a; case safety_checkert::resultt::SAFE: @@ -60,16 +87,29 @@ operator&=(safety_checkert::resultt &a, safety_checkert::resultt const &b) case safety_checkert::resultt::UNSAFE: a = b == safety_checkert::resultt::ERROR ? b : a; return a; + case safety_checkert::resultt::PAUSED: + UNREACHABLE; } UNREACHABLE; } /// \brief The best of two results +/// +/// A result of PAUSED means that the safety check has not yet completed, +/// thus it makes no sense to compare it to the result of a completed safety +/// check. Therefore do not pass safety_checkert::resultt:PAUSED as an +/// argument to this function. inline safety_checkert::resultt & operator|=(safety_checkert::resultt &a, safety_checkert::resultt const &b) { + PRECONDITION( + a != safety_checkert::resultt::PAUSED && + b != safety_checkert::resultt::PAUSED); switch(a) { + case safety_checkert::resultt::UNKNOWN: + a = b; + return a; case safety_checkert::resultt::SAFE: return a; case safety_checkert::resultt::ERROR: @@ -78,6 +118,8 @@ operator|=(safety_checkert::resultt &a, safety_checkert::resultt const &b) case safety_checkert::resultt::UNSAFE: a = b == safety_checkert::resultt::SAFE ? b : a; return a; + case safety_checkert::resultt::PAUSED: + UNREACHABLE; } UNREACHABLE; } diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index 7b71c1f0bbb..7811a4497eb 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -53,7 +53,8 @@ class goto_symext const symbol_tablet &outer_symbol_table, symex_target_equationt &_target, path_storaget &path_storage) - : total_vccs(0), + : should_pause_symex(false), + total_vccs(0), remaining_vccs(0), constant_propagation(true), language_mode(), @@ -159,6 +160,15 @@ class goto_symext goto_programt::const_targett first, goto_programt::const_targett limit); + /// \brief Have states been pushed onto the workqueue? + /// + /// If this flag is set at the end of a symbolic execution run, it means that + /// symex has been paused because we encountered a GOTO instruction while + /// doing path exploration, and thus pushed the successor states of the GOTO + /// onto path_storage. The symbolic execution caller should now choose which + /// successor state to continue executing, and resume symex from that state. + bool should_pause_symex; + protected: /// Initialise the symbolic execution and the given state with pc /// as entry point. diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h index b30c3a27448..8b00a1db968 100644 --- a/src/goto-symex/goto_symex_state.h +++ b/src/goto-symex/goto_symex_state.h @@ -372,7 +372,13 @@ class goto_symex_statet final incremental_dirtyt dirty; goto_programt::const_targett saved_target; - bool has_saved_target; + + /// \brief This state is saved, with the PC pointing to the target of a GOTO + bool has_saved_jump_target; + + /// \brief This state is saved, with the PC pointing to the next instruction + /// of a GOTO + bool has_saved_next_instruction; bool saved_target_is_backwards; private: diff --git a/src/goto-symex/path_storage.cpp b/src/goto-symex/path_storage.cpp index 528f1ce2b4e..918740ce72e 100644 --- a/src/goto-symex/path_storage.cpp +++ b/src/goto-symex/path_storage.cpp @@ -19,17 +19,20 @@ path_storaget::make(path_storaget::disciplinet discipline) UNREACHABLE; } -path_storaget::patht &path_fifot::peek() +path_storaget::patht &path_fifot::private_peek() { return paths.front(); } -void path_fifot::push(const path_storaget::patht &bp) +void path_fifot::push( + const path_storaget::patht &next_instruction, + const path_storaget::patht &jump_target) { - paths.push_back(bp); + paths.push_back(next_instruction); + paths.push_back(jump_target); } -void path_fifot::pop() +void path_fifot::private_pop() { paths.pop_front(); } diff --git a/src/goto-symex/path_storage.h b/src/goto-symex/path_storage.h index eac73dab57e..30d0b45c86e 100644 --- a/src/goto-symex/path_storage.h +++ b/src/goto-symex/path_storage.h @@ -48,13 +48,29 @@ class path_storaget virtual ~path_storaget() = default; /// \brief Reference to the next path to resume - virtual patht &peek() = 0; - - /// \brief Add a path to resume to the storage - virtual void push(const patht &bp) = 0; + patht &peek() + { + PRECONDITION(!empty()); + return private_peek(); + } + + /// \brief Add paths to resume to the storage + /// + /// Symbolic execution is suspended when we reach a conditional goto + /// instruction with two successors. Thus, we always add a pair of paths to + /// the path storage. + /// + /// \param next_instruction the instruction following the goto instruction + /// \param jump_target the target instruction of the goto instruction + virtual void + push(const patht &next_instruction, const patht &jump_target) = 0; /// \brief Remove the next path to resume from the storage - virtual void pop() = 0; + void pop() + { + PRECONDITION(!empty()); + private_pop(); + } /// \brief How many paths does this storage contain? virtual std::size_t size() const = 0; @@ -64,19 +80,27 @@ class path_storaget { return size() == 0; }; + +private: + // Derived classes should override these methods, allowing the base class to + // enforce preconditions. + virtual patht &private_peek() = 0; + virtual void private_pop() = 0; }; /// \brief FIFO save queue: paths are resumed in the order that they were saved class path_fifot : public path_storaget { public: - patht &peek() override; - void push(const patht &bp) override; - void pop() override; + void push(const patht &, const patht &) override; std::size_t size() const override; protected: std::list paths; + +private: + patht &private_peek() override; + void private_pop() override; }; #endif /* CPROVER_GOTO_SYMEX_PATH_STORAGE_H */ diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index 1306f1a6ae1..5951cd8284c 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -152,7 +152,7 @@ void goto_symext::symex_goto(statet &state) // new_state_pc for later. But if we're executing from a saved state, then // new_state_pc should be the state that we saved from earlier, so let's // execute that instead. - if(state.has_saved_target) + if(state.has_saved_jump_target) { INVARIANT( new_state_pc == state.saved_target, @@ -170,28 +170,45 @@ void goto_symext::symex_goto(statet &state) new_state_pc = state_pc; state_pc = tmp; - log.debug() << "Resuming from '" << state_pc->source_location << "'" - << log.eom; + log.debug() << "Resuming from jump target '" << state_pc->source_location + << "'" << log.eom; + } + else if(state.has_saved_next_instruction) + { + log.debug() << "Resuming from next instruction '" + << state_pc->source_location << "'" << log.eom; } else if(options.get_bool_option("paths")) { - // At this point, `state_pc` is the instruction we should execute - // immediately, and `new_state_pc` is the instruction that we should execute - // later (after we've finished exploring this branch). For path-based - // exploration, save `new_state_pc` to the saved state that we will resume - // executing from, so that goto_symex::symex_goto() knows that we've already - // explored the branch starting from `state_pc` when it is later called at - // this branch. - path_storaget::patht branch_point(target, state); - branch_point.state.saved_target = new_state_pc; - branch_point.state.has_saved_target = true; + // We should save both the instruction after this goto, and the target of + // the goto. + + path_storaget::patht next_instruction(target, state); + next_instruction.state.saved_target = state_pc; + next_instruction.state.has_saved_next_instruction = true; + next_instruction.state.saved_target_is_backwards = !forward; + + path_storaget::patht jump_target(target, state); + jump_target.state.saved_target = new_state_pc; + jump_target.state.has_saved_jump_target = true; // `forward` tells us where the branch we're _currently_ executing is // pointing to; this needs to be inverted for the branch that we're saving, // so let its truth value for `backwards` be the same as ours for `forward`. - branch_point.state.saved_target_is_backwards = forward; - path_storage.push(branch_point); - log.debug() << "Saving '" << new_state_pc->source_location << "'" + jump_target.state.saved_target_is_backwards = forward; + + log.debug() << "Saving next instruction '" + << next_instruction.state.saved_target->source_location << "'" + << log.eom; + log.debug() << "Saving jump target '" + << jump_target.state.saved_target->source_location << "'" << log.eom; + path_storage.push(next_instruction, jump_target); + + // It is now up to the caller of symex to decide which path to continue + // executing. Signal to the caller that states have been pushed (therefore + // symex has not yet completed and must be resumed), and bail out. + should_pause_symex = true; + return; } // put into state-queue @@ -242,7 +259,7 @@ void goto_symext::symex_goto(statet &state) state.rename(guard_expr, ns); } - if(state.has_saved_target) + if(state.has_saved_jump_target) { if(forward) state.guard.add(guard_expr); diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index 97c2c127c22..83e5b7e22ae 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -149,6 +149,8 @@ void goto_symext::symex_threaded_step( statet &state, const get_goto_functiont &get_goto_function) { symex_step(get_goto_function, state); + if(should_pause_symex) + return; // is there another thread to execute? if(state.call_stack().empty() && @@ -197,10 +199,15 @@ void goto_symext::symex_with_state( PRECONDITION(state.top().end_of_function->is_end_function()); symex_threaded_step(state, get_goto_function); + if(should_pause_symex) + return; while(!state.call_stack().empty()) { - state.has_saved_target = false; + state.has_saved_jump_target = false; + state.has_saved_next_instruction = false; symex_threaded_step(state, get_goto_function); + if(should_pause_symex) + return; } // Clients may need to construct a namespace with both the names in @@ -227,7 +234,6 @@ void goto_symext::resume_symex_from_saved_state( // its equation member point to the (valid) equation passed as an argument. statet state(saved_state, saved_equation); - symex_transition(state, state.source.pc); // Do NOT do the same initialization that `symex_with_state` does for a // fresh state, as that would clobber the saved state's program counter symex_with_state( From 17951c86c3ee0ddcf636eebcba6b2e5a6237189f Mon Sep 17 00:00:00 2001 From: Kareem Khazem Date: Thu, 12 Apr 2018 10:50:22 +0100 Subject: [PATCH 4/7] Add path strategy chooser class A new class is introduced to hold the names, descriptions and constructor thunks for all path exploration strategies. This provides a uniform way for strategy descriptions to be displayed, which can be done with the --show-symex-strategies flag. --- src/cbmc/bmc.cpp | 9 +++-- src/cbmc/bmc.h | 7 ++-- src/cbmc/cbmc_parse_options.cpp | 21 +++++++++--- src/cbmc/cbmc_parse_options.h | 1 + src/goto-symex/path_storage.cpp | 57 ++++++++++++++++++++++++------ src/goto-symex/path_storage.h | 61 ++++++++++++++++++++++++++++----- src/jbmc/jbmc_parse_options.cpp | 23 +++++++++++-- src/jbmc/jbmc_parse_options.h | 3 ++ 8 files changed, 151 insertions(+), 31 deletions(-) diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index be441f53443..ea7b3e17f30 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -598,6 +598,7 @@ void bmct::setup_unwind() /// \param callback_after_symex: optional callback to be run after symex. /// See class member `bmct::driver_callback_after_symex` for details. int bmct::do_language_agnostic_bmc( + const path_strategy_choosert &path_strategy_chooser, const optionst &opts, abstract_goto_modelt &model, const ui_message_handlert::uit &ui, @@ -609,8 +610,12 @@ int bmct::do_language_agnostic_bmc( safety_checkert::resultt tmp_result = safety_checkert::resultt::UNKNOWN; const symbol_tablet &symbol_table = model.get_symbol_table(); message_handlert &mh = message.get_message_handler(); - std::unique_ptr worklist = - path_storaget::make(path_storaget::disciplinet::FIFO); + std::unique_ptr worklist; + std::string strategy = opts.get_option("exploration-strategy"); + INVARIANT( + path_strategy_chooser.is_valid_strategy(strategy), + "Front-end passed us invalid path strategy '" + strategy + "'"); + worklist = path_strategy_chooser.get(strategy); try { { diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h index 3077f27d554..0e7efe46da9 100644 --- a/src/cbmc/bmc.h +++ b/src/cbmc/bmc.h @@ -117,6 +117,7 @@ class bmct:public safety_checkert } static int do_language_agnostic_bmc( + const path_strategy_choosert &path_strategy_chooser, const optionst &opts, abstract_goto_modelt &goto_model, const ui_message_handlert::uit &ui, @@ -294,7 +295,8 @@ class path_explorert : public bmct "(no-unwinding-assertions)" \ "(no-pretty-names)" \ "(partial-loops)" \ - "(paths)" \ + "(paths):" \ + "(show-symex-strategies)" \ "(depth):" \ "(unwind):" \ "(unwindset):" \ @@ -302,7 +304,8 @@ class path_explorert : public bmct "(unwindset):" #define HELP_BMC \ - " --paths explore paths one at a time\n" \ + " --paths [strategy] explore paths one at a time\n" \ + " --show-symex-strategies list strategies for use with --paths\n" \ " --program-only only show program expression\n" \ " --show-loops show the loops in the program\n" \ " --depth nr limit search depth\n" \ diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index f18d7756b95..295efe9c38f 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -68,7 +68,8 @@ cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv): parse_options_baset(CBMC_OPTIONS, argc, argv), xml_interfacet(cmdline), messaget(ui_message_handler), - ui_message_handler(cmdline, "CBMC " CBMC_VERSION) + ui_message_handler(cmdline, "CBMC " CBMC_VERSION), + path_strategy_chooser() { } @@ -79,7 +80,8 @@ ::cbmc_parse_optionst::cbmc_parse_optionst( parse_options_baset(CBMC_OPTIONS+extra_options, argc, argv), xml_interfacet(cmdline), messaget(ui_message_handler), - ui_message_handler(cmdline, "CBMC " CBMC_VERSION) + ui_message_handler(cmdline, "CBMC " CBMC_VERSION), + path_strategy_chooser() { } @@ -146,8 +148,13 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) exit(CPROVER_EXIT_USAGE_ERROR); } - if(cmdline.isset("paths")) - options.set_option("paths", true); + if(cmdline.isset("show-symex-strategies")) + { + std::cout << path_strategy_chooser.show_strategies(); + exit(CPROVER_EXIT_SUCCESS); + } + + path_strategy_chooser.set_path_strategy_options(cmdline, options, *this); if(cmdline.isset("program-only")) options.set_option("program-only", true); @@ -531,7 +538,11 @@ int cbmc_parse_optionst::doit() return CPROVER_EXIT_SET_PROPERTIES_FAILED; return bmct::do_language_agnostic_bmc( - options, goto_model, ui_message_handler.get_ui(), *this); + path_strategy_chooser, + options, + goto_model, + ui_message_handler.get_ui(), + *this); } bool cbmc_parse_optionst::set_properties() diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index b50c5160ba3..25ff6b50628 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -110,6 +110,7 @@ class cbmc_parse_optionst: protected: goto_modelt goto_model; ui_message_handlert ui_message_handler; + const path_strategy_choosert path_strategy_chooser; void eval_verbosity(); void register_languages(); diff --git a/src/goto-symex/path_storage.cpp b/src/goto-symex/path_storage.cpp index 918740ce72e..5c6ef9037ff 100644 --- a/src/goto-symex/path_storage.cpp +++ b/src/goto-symex/path_storage.cpp @@ -8,16 +8,10 @@ Author: Kareem Khazem #include "path_storage.h" -std::unique_ptr -path_storaget::make(path_storaget::disciplinet discipline) -{ - switch(discipline) - { - case path_storaget::disciplinet::FIFO: - return std::unique_ptr(new path_fifot()); - } - UNREACHABLE; -} +#include + +#include +#include path_storaget::patht &path_fifot::private_peek() { @@ -41,3 +35,46 @@ std::size_t path_fifot::size() const { return paths.size(); } + +std::string path_strategy_choosert::show_strategies() const +{ + std::stringstream ss; + for(auto &pair : strategies) + ss << pair.second.first; + return ss.str(); +} + +void path_strategy_choosert::set_path_strategy_options( + const cmdlinet &cmdline, + optionst &options, + messaget &message) const +{ + if(cmdline.isset("paths")) + { + options.set_option("paths", true); + std::string strategy = cmdline.get_value("paths"); + if(!is_valid_strategy(strategy)) + { + message.error() << "Unknown strategy '" << strategy + << "'. Pass the --show-symex-strategies flag to list " + "available strategies." + << message.eom; + exit(CPROVER_EXIT_USAGE_ERROR); + } + options.set_option("exploration-strategy", strategy); + } + else + options.set_option("exploration-strategy", default_strategy()); +} + +path_strategy_choosert::path_strategy_choosert() + : strategies( + {{"fifo", + {" fifo next instruction is pushed before\n" + " goto target; paths are popped in\n" + " first-in, first-out order\n", + []() { // NOLINT(whitespace/braces) + return util_make_unique(); + }}}}) +{ +} diff --git a/src/goto-symex/path_storage.h b/src/goto-symex/path_storage.h index 30d0b45c86e..8faf45cf16e 100644 --- a/src/goto-symex/path_storage.h +++ b/src/goto-symex/path_storage.h @@ -8,6 +8,11 @@ #include "goto_symex_state.h" #include "symex_target_equation.h" +#include +#include +#include +#include + #include /// \brief Storage for symbolic execution paths to be resumed later @@ -19,13 +24,6 @@ class path_storaget { public: - /// \brief Derived types of path_storaget - enum class disciplinet - { - /// path_fifot - FIFO - }; - /// \brief Information saved at a conditional goto to resume execution struct patht { @@ -43,8 +41,6 @@ class path_storaget } }; - /// \brief Factory method for building a subtype of path_storaget - static std::unique_ptr make(disciplinet discipline); virtual ~path_storaget() = default; /// \brief Reference to the next path to resume @@ -103,4 +99,51 @@ class path_fifot : public path_storaget void private_pop() override; }; +/// \brief Factory and information for path_storaget +class path_strategy_choosert +{ +public: + path_strategy_choosert(); + + /// \brief suitable for displaying as a front-end help message + std::string show_strategies() const; + + /// \brief is there a factory constructor for the named strategy? + bool is_valid_strategy(const std::string strategy) const + { + return strategies.find(strategy) != strategies.end(); + } + + /// \brief Factory for a path_storaget + /// + /// Ensure that path_strategy_choosert::is_valid_strategy() returns true for a + /// particular string before calling this function on that string. + std::unique_ptr get(const std::string strategy) const + { + auto found = strategies.find(strategy); + INVARIANT( + found != strategies.end(), "Unknown strategy '" + strategy + "'."); + return found->second.second(); + } + + /// \brief add `paths` and `exploration-strategy` option, suitable to be + /// invoked from front-ends. + void + set_path_strategy_options(const cmdlinet &, optionst &, messaget &) const; + +protected: + std::string default_strategy() const + { + return "fifo"; + } + + /// Map from the name of a strategy (to be supplied on the command line), to + /// the help text for that strategy and a factory thunk returning a pointer to + /// a derived class of path_storaget that implements that strategy. + std::map()>>> + strategies; +}; + #endif /* CPROVER_GOTO_SYMEX_PATH_STORAGE_H */ diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp index 26427ffe703..72c7c1eacdd 100644 --- a/src/jbmc/jbmc_parse_options.cpp +++ b/src/jbmc/jbmc_parse_options.cpp @@ -16,6 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include @@ -63,7 +64,8 @@ Author: Daniel Kroening, kroening@kroening.com jbmc_parse_optionst::jbmc_parse_optionst(int argc, const char **argv): parse_options_baset(JBMC_OPTIONS, argc, argv), messaget(ui_message_handler), - ui_message_handler(cmdline, "JBMC " CBMC_VERSION) + ui_message_handler(cmdline, "JBMC " CBMC_VERSION), + path_strategy_chooser() { } @@ -73,7 +75,8 @@ ::jbmc_parse_optionst::jbmc_parse_optionst( const std::string &extra_options): parse_options_baset(JBMC_OPTIONS+extra_options, argc, argv), messaget(ui_message_handler), - ui_message_handler(cmdline, "JBMC " CBMC_VERSION) + ui_message_handler(cmdline, "JBMC " CBMC_VERSION), + path_strategy_chooser() { } @@ -100,6 +103,14 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options) exit(1); // should contemplate EX_USAGE from sysexits.h } + if(cmdline.isset("show-symex-strategies")) + { + std::cout << path_strategy_chooser.show_strategies(); + exit(CPROVER_EXIT_SUCCESS); + } + + path_strategy_chooser.set_path_strategy_options(cmdline, options, *this); + if(cmdline.isset("program-only")) options.set_option("program-only", true); @@ -533,7 +544,12 @@ int jbmc_parse_optionst::doit() // The `configure_bmc` callback passed will enable enum-unwind-static if // applicable. return bmct::do_language_agnostic_bmc( - options, goto_model, ui_message_handler.get_ui(), *this, configure_bmc); + path_strategy_chooser, + options, + goto_model, + ui_message_handler.get_ui(), + *this, + configure_bmc); } else { @@ -573,6 +589,7 @@ int jbmc_parse_optionst::doit() // applicable. return bmct::do_language_agnostic_bmc( + path_strategy_chooser, options, lazy_goto_model, ui_message_handler.get_ui(), diff --git a/src/jbmc/jbmc_parse_options.h b/src/jbmc/jbmc_parse_options.h index 22871752ab4..d0c1919d93c 100644 --- a/src/jbmc/jbmc_parse_options.h +++ b/src/jbmc/jbmc_parse_options.h @@ -27,6 +27,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + #include class bmct; @@ -103,6 +105,7 @@ class jbmc_parse_optionst: protected: ui_message_handlert ui_message_handler; std::unique_ptr cover_config; + path_strategy_choosert path_strategy_chooser; void eval_verbosity(); void get_command_line_options(optionst &); From feef06980726fd51d5bd9e357785c3027369b851 Mon Sep 17 00:00:00 2001 From: Kareem Khazem Date: Thu, 15 Mar 2018 04:50:27 +0000 Subject: [PATCH 5/7] Doxygen uses C++ parser for .h files --- src/doxyfile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/doxyfile b/src/doxyfile index 1c21026929f..409422346ce 100644 --- a/src/doxyfile +++ b/src/doxyfile @@ -281,7 +281,7 @@ OPTIMIZE_OUTPUT_VHDL = NO # Note that for custom extensions you also need to set FILE_PATTERNS otherwise # the files are not read by doxygen. -EXTENSION_MAPPING = +EXTENSION_MAPPING = h=c++ # If the MARKDOWN_SUPPORT tag is enabled then doxygen pre-processes all comments # according to the Markdown format, which allows for more readable From 85aba52313c0539fdaa16dfba5f4efb86b03e03b Mon Sep 17 00:00:00 2001 From: Kareem Khazem Date: Fri, 6 Apr 2018 12:21:04 +0100 Subject: [PATCH 6/7] Make new LIFO path exploration the default This commits adds the "lifo" strategy, which explores program paths using depth-first search. This is now the default strategy due to its favourable memory consumption compared to other strategies; tests on a few benchmarks show that its memory usage is basically constant and comparable to regular model-checking, since this strategy finishes paths as quickly as possible rather than saving them for later. --- src/goto-symex/path_storage.cpp | 49 +++++++++++++++++++++++++++++++-- src/goto-symex/path_storage.h | 18 +++++++++++- 2 files changed, 64 insertions(+), 3 deletions(-) diff --git a/src/goto-symex/path_storage.cpp b/src/goto-symex/path_storage.cpp index 5c6ef9037ff..58a2498a07d 100644 --- a/src/goto-symex/path_storage.cpp +++ b/src/goto-symex/path_storage.cpp @@ -13,6 +13,39 @@ Author: Kareem Khazem #include #include +// _____________________________________________________________________________ +// path_lifot + +path_storaget::patht &path_lifot::private_peek() +{ + last_peeked = paths.end(); + --last_peeked; + return paths.back(); +} + +void path_lifot::push( + const path_storaget::patht &next_instruction, + const path_storaget::patht &jump_target) +{ + paths.push_back(next_instruction); + paths.push_back(jump_target); +} + +void path_lifot::private_pop() +{ + PRECONDITION(last_peeked != paths.end()); + paths.erase(last_peeked); + last_peeked = paths.end(); +} + +std::size_t path_lifot::size() const +{ + return paths.size(); +} + +// _____________________________________________________________________________ +// path_fifot + path_storaget::patht &path_fifot::private_peek() { return paths.front(); @@ -36,6 +69,9 @@ std::size_t path_fifot::size() const return paths.size(); } +// _____________________________________________________________________________ +// path_strategy_choosert + std::string path_strategy_choosert::show_strategies() const { std::stringstream ss; @@ -69,10 +105,19 @@ void path_strategy_choosert::set_path_strategy_options( path_strategy_choosert::path_strategy_choosert() : strategies( - {{"fifo", + {{"lifo", + {" lifo next instruction is pushed before\n" + " goto target; paths are popped in\n" + " last-in, first-out order. Explores\n" + " the program tree depth-first.\n", + []() { // NOLINT(whitespace/braces) + return util_make_unique(); + }}}, + {"fifo", {" fifo next instruction is pushed before\n" " goto target; paths are popped in\n" - " first-in, first-out order\n", + " first-in, first-out order. Explores\n" + " the program tree breadth-first.\n", []() { // NOLINT(whitespace/braces) return util_make_unique(); }}}}) diff --git a/src/goto-symex/path_storage.h b/src/goto-symex/path_storage.h index 8faf45cf16e..e5d5120cfea 100644 --- a/src/goto-symex/path_storage.h +++ b/src/goto-symex/path_storage.h @@ -84,6 +84,22 @@ class path_storaget virtual void private_pop() = 0; }; +/// \brief LIFO save queue: depth-first search, try to finish paths +class path_lifot : public path_storaget +{ +public: + void push(const patht &, const patht &) override; + std::size_t size() const override; + +protected: + std::list::iterator last_peeked; + std::list paths; + +private: + patht &private_peek() override; + void private_pop() override; +}; + /// \brief FIFO save queue: paths are resumed in the order that they were saved class path_fifot : public path_storaget { @@ -134,7 +150,7 @@ class path_strategy_choosert protected: std::string default_strategy() const { - return "fifo"; + return "lifo"; } /// Map from the name of a strategy (to be supplied on the command line), to From 916eb1ff3790fbbc223ffda2556b23b6e5403912 Mon Sep 17 00:00:00 2001 From: Kareem Khazem Date: Wed, 11 Apr 2018 16:56:41 +0100 Subject: [PATCH 7/7] Unit tests for path exploration strategies --- unit/CMakeLists.txt | 1 + unit/Makefile | 30 ++++ unit/path_strategies.cpp | 364 +++++++++++++++++++++++++++++++++++++++ unit/path_strategies.h | 62 +++++++ 4 files changed, 457 insertions(+) create mode 100644 unit/path_strategies.cpp create mode 100644 unit/path_strategies.h diff --git a/unit/CMakeLists.txt b/unit/CMakeLists.txt index 5b4cdf42335..300f6c08fef 100644 --- a/unit/CMakeLists.txt +++ b/unit/CMakeLists.txt @@ -43,6 +43,7 @@ target_link_libraries( java_bytecode goto-programs goto-instrument-lib + cbmc-lib ) add_test( diff --git a/unit/Makefile b/unit/Makefile index b150bfa632c..b7b2ceef442 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -30,6 +30,7 @@ SRC += unit_tests.cpp \ java_bytecode/java_types/java_type_from_string.cpp \ java_bytecode/java_utils_test.cpp \ java_bytecode/inherited_static_fields/inherited_static_fields.cpp \ + path_strategies.cpp \ pointer-analysis/custom_value_set_analysis.cpp \ sharing_node.cpp \ solvers/refinement/string_constraint_generator_valueof/calculate_max_string_length.cpp \ @@ -71,6 +72,34 @@ cprover.dir: testing-utils.dir: $(MAKE) $(MAKEARGS) -C testing-utils +# We need to link bmc.o to the unit test, so here's everything it depends on... +BMC_DEPS =../src/cbmc/all_properties$(OBJEXT) \ + ../src/cbmc/bmc$(OBJEXT) \ + ../src/cbmc/bmc_cover$(OBJEXT) \ + ../src/cbmc/bv_cbmc$(OBJEXT) \ + ../src/cbmc/cbmc_dimacs$(OBJEXT) \ + ../src/cbmc/cbmc_languages$(OBJEXT) \ + ../src/cbmc/cbmc_parse_options$(OBJEXT) \ + ../src/cbmc/cbmc_solvers$(OBJEXT) \ + ../src/cbmc/counterexample_beautification$(OBJEXT) \ + ../src/cbmc/fault_localization$(OBJEXT) \ + ../src/cbmc/show_vcc$(OBJEXT) \ + ../src/cbmc/symex_bmc$(OBJEXT) \ + ../src/cbmc/symex_coverage$(OBJEXT) \ + ../src/cbmc/xml_interface$(OBJEXT) \ + ../src/jsil/expr2jsil$(OBJEXT) \ + ../src/jsil/jsil_convert$(OBJEXT) \ + ../src/jsil/jsil_entry_point$(OBJEXT) \ + ../src/jsil/jsil_internal_additions$(OBJEXT) \ + ../src/jsil/jsil_language$(OBJEXT) \ + ../src/jsil/jsil_lex.yy$(OBJEXT) \ + ../src/jsil/jsil_parser$(OBJEXT) \ + ../src/jsil/jsil_parse_tree$(OBJEXT) \ + ../src/jsil/jsil_typecheck$(OBJEXT) \ + ../src/jsil/jsil_types$(OBJEXT) \ + ../src/jsil/jsil_y.tab$(OBJEXT) \ + # Empty last line +# CPROVER_LIBS =../src/java_bytecode/java_bytecode$(LIBEXT) \ ../src/miniz/miniz$(OBJEXT) \ ../src/ansi-c/ansi-c$(LIBEXT) \ @@ -86,6 +115,7 @@ CPROVER_LIBS =../src/java_bytecode/java_bytecode$(LIBEXT) \ ../src/assembler/assembler$(LIBEXT) \ ../src/analyses/analyses$(LIBEXT) \ ../src/solvers/solvers$(LIBEXT) \ + $(BMC_DEPS) # Empty last line OBJ += $(CPROVER_LIBS) testing-utils/testing-utils$(LIBEXT) diff --git a/unit/path_strategies.cpp b/unit/path_strategies.cpp new file mode 100644 index 00000000000..171fe71d7ee --- /dev/null +++ b/unit/path_strategies.cpp @@ -0,0 +1,364 @@ +/*******************************************************************\ + +Module: Path Strategy Tests + +Author: Kareem Khazem , 2018 + +\*******************************************************************/ + +#include + +#include + +#include +#include +#include + +#include + +#include +#include +#include + +#include +#include + +#include +#include +#include +#include + +// The actual test suite. +// +// Whenever you add a new path exploration strategy 'my-cool-strategy', for each +// of the test programs (under the GIVEN macros), add a new test using a call to +// `check_with_strategy("my-cool-strategy", c, event_list)` where `event_list` +// is a list of the events that you expect to see during symbolic execution. +// Events are either resumes or results. +// +// Whenever symbolic execution pauses and picks a path to resume from, you +// should note the line number of the path you expect that path strategy to +// resume from. A resume is either a JUMP, meaning that it's the target of a +// `goto` instruction, or a NEXT, meaning that it's the instruction following a +// `goto` instruction. +// +// Whenever symbolic execution reaches the end of a path, you should expect a +// result. Results are either SUCCESS, meaning that verification of that path +// succeeded, or FAILURE, meaning that there was an assertion failure on that +// path. +// +// To figure out what the events should be, run CBMC on the test program with +// your strategy with `--verbosity 10` and look out for lines like +// +// Resuming from jump target 'file nested-if/main.c line 13 function main' +// +// Resuming from next instruction 'file nested-if/main.c line 14 function main' +// +// VERIFICATION SUCCESSFUL +// +// VERIFICATION FAILED +// +// And note the order in which they occur. + +SCENARIO("path strategies") +{ + std::string c; + GIVEN("a simple conditional program") + { + c = + "/* 1 */ int main() \n" + "/* 2 */ { \n" + "/* 3 */ int x; \n" + "/* 4 */ if(x) \n" + "/* 5 */ x = 1; \n" + "/* 6 */ else \n" + "/* 7 */ x = 0; \n" + "/* 8 */ } \n"; + + const unsigned unwind_limit = 0U; + + check_with_strategy( + "lifo", + c, + {symex_eventt::resume(symex_eventt::enumt::JUMP, 7), + symex_eventt::result(symex_eventt::enumt::SUCCESS), + symex_eventt::resume(symex_eventt::enumt::NEXT, 5), + symex_eventt::result(symex_eventt::enumt::SUCCESS)}, + unwind_limit); + check_with_strategy( + "fifo", + c, + {symex_eventt::resume(symex_eventt::enumt::NEXT, 5), + symex_eventt::result(symex_eventt::enumt::SUCCESS), + symex_eventt::resume(symex_eventt::enumt::JUMP, 7), + symex_eventt::result(symex_eventt::enumt::SUCCESS)}, + unwind_limit); + } + + GIVEN("a program with nested conditionals") + { + c = + "/* 1 */ int main() \n" + "/* 2 */ { \n" + "/* 3 */ int x, y; \n" + "/* 4 */ if(x) \n" + "/* 5 */ { \n" + "/* 6 */ if(y) \n" + "/* 7 */ y = 1; \n" + "/* 8 */ else \n" + "/* 9 */ y = 0; \n" + "/* 10 */ } \n" + "/* 11 */ else \n" + "/* 12 */ { \n" + "/* 13 */ if(y) \n" + "/* 14 */ y = 1; \n" + "/* 15 */ else \n" + "/* 16 */ y = 0; \n" + "/* 17 */ } \n" + "/* 18 */ } \n"; + + const unsigned unwind_limit = 0U; + + check_with_strategy( + "lifo", + c, + {// Outer else, inner else + symex_eventt::resume(symex_eventt::enumt::JUMP, 13), + symex_eventt::resume(symex_eventt::enumt::JUMP, 16), + symex_eventt::result(symex_eventt::enumt::SUCCESS), + // Outer else, inner if + symex_eventt::resume(symex_eventt::enumt::NEXT, 14), + symex_eventt::result(symex_eventt::enumt::SUCCESS), + // Outer if, inner else + symex_eventt::resume(symex_eventt::enumt::NEXT, 6), + symex_eventt::resume(symex_eventt::enumt::JUMP, 9), + symex_eventt::result(symex_eventt::enumt::SUCCESS), + // Outer if, inner if + symex_eventt::resume(symex_eventt::enumt::NEXT, 7), + symex_eventt::result(symex_eventt::enumt::SUCCESS)}, + unwind_limit); + + check_with_strategy( + "fifo", + c, + {// Expand outer if, but don't continue depth-first + symex_eventt::resume(symex_eventt::enumt::NEXT, 6), + // Jump to outer else, but again don't continue depth-first + symex_eventt::resume(symex_eventt::enumt::JUMP, 13), + // Expand inner if of the outer if + symex_eventt::resume(symex_eventt::enumt::NEXT, 7), + // No more branch points, so complete the path + symex_eventt::result(symex_eventt::enumt::SUCCESS), + // Continue BFSing + symex_eventt::resume(symex_eventt::enumt::JUMP, 9), + symex_eventt::result(symex_eventt::enumt::SUCCESS), + symex_eventt::resume(symex_eventt::enumt::NEXT, 14), + symex_eventt::result(symex_eventt::enumt::SUCCESS), + symex_eventt::resume(symex_eventt::enumt::JUMP, 16), + symex_eventt::result(symex_eventt::enumt::SUCCESS)}, + unwind_limit); + } + + GIVEN("a loop program to test functional correctness") + { + c = + "/* 1 */ int main() \n" + "/* 2 */ { \n" + "/* 3 */ int x; \n" + "/* 4 */ __CPROVER_assume(x == 1); \n" + "/* 5 */ \n" + "/* 6 */ while(x) \n" + "/* 7 */ --x; \n" + "/* 8 */ \n" + "/* 9 */ assert(x); \n" + "/* 10 */ } \n"; + + const unsigned unwind_limit = 2U; + + check_with_strategy( + "lifo", + c, + { + // The path where we skip the loop body. Successful because the path is + // implausible, we cannot have skipped the body if x == 1. + symex_eventt::resume(symex_eventt::enumt::JUMP, 9), + symex_eventt::result(symex_eventt::enumt::SUCCESS), + + // Enter the loop body once. Since we decrement x, the assertion should + // fail. + symex_eventt::resume(symex_eventt::enumt::NEXT, 7), + symex_eventt::resume(symex_eventt::enumt::JUMP, 9), + symex_eventt::result(symex_eventt::enumt::FAILURE), + + // The path where we enter the loop body twice. Successful because + // infeasible. + symex_eventt::resume(symex_eventt::enumt::NEXT, 7), + symex_eventt::result(symex_eventt::enumt::SUCCESS), + }, + unwind_limit); + + check_with_strategy( + "fifo", + c, + { + // The path where we skip the loop body. Successful because the path is + // implausible, we cannot have skipped the body if x == 1. + // + // In this case, although we resume from line 7, we don't proceed until + // the end of the path after executing line 7. + symex_eventt::resume(symex_eventt::enumt::NEXT, 7), + symex_eventt::resume(symex_eventt::enumt::JUMP, 9), + symex_eventt::result(symex_eventt::enumt::SUCCESS), + + // Pop line 7 that we saved from above, and execute the loop a second + // time. Successful, since this path is infeasible. + symex_eventt::resume(symex_eventt::enumt::NEXT, 7), + symex_eventt::result(symex_eventt::enumt::SUCCESS), + + // Pop line 7 that we saved from above and bail out. That corresponds to + // executing the loop once, decrementing x to 0; assert(x) should fail. + symex_eventt::resume(symex_eventt::enumt::JUMP, 9), + symex_eventt::result(symex_eventt::enumt::FAILURE), + }, + unwind_limit); + } +} + +// In theory, there should be no need to change the code below when adding new +// test cases... + +void symex_eventt::validate_result( + listt &events, + const safety_checkert::resultt result) +{ + INFO( + "Expecting result to be '" + << (result == safety_checkert::resultt::SAFE ? "success" : "failure") + << "'"); + + REQUIRE(result != safety_checkert::resultt::ERROR); + + if(result == safety_checkert::resultt::SAFE) + { + REQUIRE(!events.empty()); + REQUIRE(events.front().first == symex_eventt::enumt::SUCCESS); + events.pop_front(); + } + else if(result == safety_checkert::resultt::UNSAFE) + { + REQUIRE(!events.empty()); + REQUIRE(events.front().first == symex_eventt::enumt::FAILURE); + events.pop_front(); + } +} + +void symex_eventt::validate_resume( + listt &events, + const goto_symex_statet &state) +{ + REQUIRE(!events.empty()); + + int dst = std::stoi(state.saved_target->source_location.get_line().c_str()); + + if(state.has_saved_jump_target) + { + INFO("Expecting resume to be 'jump' to line " << dst); + REQUIRE(events.front().first == symex_eventt::enumt::JUMP); + } + else if(state.has_saved_next_instruction) + { + INFO("Expecting resume to be 'next' to line " << dst); + REQUIRE(events.front().first == symex_eventt::enumt::NEXT); + } + else + REQUIRE(false); + + REQUIRE(events.front().second == dst); + + events.pop_front(); +} + +// This is a simplified version of bmct::do_language_agnostic_bmc, without all +// the edge cases to deal with java programs, bytecode loaded on demand, etc. We +// need to replicate some of this stuff because the worklist is a local variable +// of do_language_agnostic_bmc, and we need to check the worklist every time +// symex returns. +void _check_with_strategy( + const std::string &strategy, + const std::string &program, + const unsigned unwind_limit, + symex_eventt::listt &events) +{ + temporary_filet tmp("path-explore_", ".c"); + std::ofstream of(tmp().c_str()); + REQUIRE(of.is_open()); + + of << program << std::endl; + of.close(); + + register_language(new_ansi_c_language); + cmdlinet cmdline; + cmdline.args.push_back(tmp()); + config.main = "main"; + config.set(cmdline); + + optionst opts; + cbmc_parse_optionst::set_default_options(opts); + opts.set_option("paths", true); + opts.set_option("exploration-strategy", strategy); + + if(unwind_limit) + { + opts.set_option("unwind", unwind_limit); + cmdline.set("unwind", std::to_string(unwind_limit)); + } + + ui_message_handlert mh(cmdline, "path-explore"); + messaget log(mh); + + path_strategy_choosert chooser; + REQUIRE(chooser.is_valid_strategy(strategy)); + std::unique_ptr worklist = chooser.get(strategy); + + goto_modelt gm; + int ret; + ret = cbmc_parse_optionst::get_goto_program(gm, opts, cmdline, log, mh); + REQUIRE(ret == -1); + + cbmc_solverst solvers(opts, gm.get_symbol_table(), mh); + solvers.set_ui(mh.get_ui()); + std::unique_ptr cbmc_solver = solvers.get_solver(); + prop_convt &pc = cbmc_solver->prop_conv(); + std::function callback = []() { return false; }; + + bmct bmc(opts, gm.get_symbol_table(), mh, pc, *worklist, callback); + bmc.set_ui(mh.get_ui()); + safety_checkert::resultt result = bmc.run(gm); + symex_eventt::validate_result(events, result); + + while(!worklist->empty()) + { + cbmc_solverst solvers(opts, gm.get_symbol_table(), mh); + solvers.set_ui(mh.get_ui()); + cbmc_solver = solvers.get_solver(); + prop_convt &pc = cbmc_solver->prop_conv(); + path_storaget::patht &resume = worklist->peek(); + + symex_eventt::validate_resume(events, resume.state); + + path_explorert pe( + opts, + gm.get_symbol_table(), + mh, + pc, + resume.equation, + resume.state, + *worklist, + callback); + result = pe.run(gm); + + symex_eventt::validate_result(events, result); + worklist->pop(); + } + REQUIRE(events.empty()); +} diff --git a/unit/path_strategies.h b/unit/path_strategies.h new file mode 100644 index 00000000000..c1f4c63c8d1 --- /dev/null +++ b/unit/path_strategies.h @@ -0,0 +1,62 @@ +/// \file Test for path strategies set through `cbmc --paths ...` +/// +/// \author Kareem Khazem + +#ifndef CPROVER_PATH_STRATEGIES_H +#define CPROVER_PATH_STRATEGIES_H + +#include +#include + +#include + +/// \brief Events that we expect to happen during path exploration +/// +/// See the description in the .cpp file on how to use this class. +struct symex_eventt +{ +public: + enum class enumt + { + JUMP, + NEXT, + SUCCESS, + FAILURE + }; + typedef std::pair pairt; + typedef std::list listt; + + static pairt resume(enumt kind, int location) + { + return pairt(kind, location); + } + + static pairt result(enumt kind) + { + return pairt(kind, -1); + } + + static void + validate_result(listt &events, const safety_checkert::resultt result); + + static void validate_resume(listt &events, const goto_symex_statet &state); +}; + +void _check_with_strategy( + const std::string &strategy, + const std::string &program, + const unsigned unwind_limit, + symex_eventt::listt &events); + +/// Call this one, not the underscore version +void check_with_strategy( + const std::string &strategy, + const std::string &program, + symex_eventt::listt events, + const unsigned unwind_limit) +{ + WHEN("strategy is '" + strategy + "'") + _check_with_strategy(strategy, program, unwind_limit, events); +} + +#endif // CPROVER_PATH_STRATEGIES_H