diff --git a/jbmc/src/jbmc/Makefile b/jbmc/src/jbmc/Makefile index ec96389eefc..aa34a1f1810 100644 --- a/jbmc/src/jbmc/Makefile +++ b/jbmc/src/jbmc/Makefile @@ -1,6 +1,4 @@ -SRC = all_properties.cpp \ - bmc.cpp \ - jbmc_main.cpp \ +SRC = jbmc_main.cpp \ jbmc_parse_options.cpp \ # Empty last line diff --git a/jbmc/src/jbmc/all_properties.cpp b/jbmc/src/jbmc/all_properties.cpp deleted file mode 100644 index ca0cd584e42..00000000000 --- a/jbmc/src/jbmc/all_properties.cpp +++ /dev/null @@ -1,306 +0,0 @@ -/*******************************************************************\ - -Module: Symbolic Execution of ANSI-C - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// Symbolic Execution of ANSI-C - -#include "all_properties_class.h" - -#include -#include - -#include -#include - -#include -#include - -#include -#include - -#include -#include -#include - -void bmc_all_propertiest::goal_covered(const cover_goalst::goalt &) -{ - for(auto &g : goal_map) - { - // failed already? - if(g.second.status == goalt::statust::FAILURE) - continue; - - // check whether failed - for(auto &c : g.second.instances) - { - literalt cond = c->cond_literal; - - if(solver.l_get(cond).is_false()) - { - g.second.status = goalt::statust::FAILURE; - if(bmc.options.get_bool_option("trace")) - { - build_goto_trace( - bmc.equation, c, solver, bmc.ns, g.second.goto_trace); - } - break; - } - } - } -} - -safety_checkert::resultt bmc_all_propertiest::operator()() -{ - status() << "Passing problem to " << solver.decision_procedure_text() << eom; - - auto solver_start = std::chrono::steady_clock::now(); - - convert_symex_target_equation( - bmc.equation, bmc.prop_conv, get_message_handler()); - bmc.freeze_program_variables(); - - // Collect _all_ goals in `goal_map'. - // This maps property IDs to 'goalt' - forall_goto_functions(f_it, goto_functions) - forall_goto_program_instructions(i_it, f_it->second.body) - if(i_it->is_assert()) - goal_map[i_it->source_location.get_property_id()] = goalt(*i_it); - - // get the conditions for these goals from formula - // collect all 'instances' of the properties - for(symex_target_equationt::SSA_stepst::iterator it = - bmc.equation.SSA_steps.begin(); - it != bmc.equation.SSA_steps.end(); - it++) - { - if(it->is_assert()) - { - irep_idt property_id = it->get_property_id(); - - if(property_id.empty()) - continue; - - if(it->source.pc->is_goto()) - { - // goto may yield an unwinding assertion - goal_map[property_id].description = it->comment; - } - - goal_map[property_id].instances.push_back(it); - } - } - - do_before_solving(); - - cover_goalst cover_goals(solver); - - cover_goals.register_observer(*this); - - for(const auto &g : goal_map) - { - // Our goal is to falsify a property, i.e., we will - // add the negation of the property as goal. - cover_goals.add(not_exprt(g.second.as_expr())); - } - - status() << "Running " << solver.decision_procedure_text() << eom; - - bool error = false; - - const decision_proceduret::resultt result = - cover_goals(get_message_handler()); - - if(result == decision_proceduret::resultt::D_ERROR) - { - error = true; - for(auto &g : goal_map) - if(g.second.status == goalt::statust::UNKNOWN) - g.second.status = goalt::statust::ERROR; - } - else - { - for(auto &g : goal_map) - if(g.second.status == goalt::statust::UNKNOWN) - g.second.status = goalt::statust::SUCCESS; - } - - { - auto solver_stop = std::chrono::steady_clock::now(); - - statistics() - << "Runtime decision procedure: " - << std::chrono::duration(solver_stop - solver_start).count() - << "s" << eom; - } - - // report - report(cover_goals); - - if(error) - return safety_checkert::resultt::ERROR; - - bool safe = (cover_goals.number_covered() == 0); - - if(safe) - report_success(bmc.ui_message_handler); // legacy, might go away - else - report_failure(bmc.ui_message_handler); // legacy, might go away - - return safe ? safety_checkert::resultt::SAFE - : safety_checkert::resultt::UNSAFE; -} - -void bmc_all_propertiest::report(const cover_goalst &cover_goals) -{ - switch(bmc.ui_message_handler.get_ui()) - { - case ui_message_handlert::uit::PLAIN: - { - result() << "\n** Results:" << eom; - - // collect goals in a vector - std::vector goals; - - for(auto g_it = goal_map.begin(); g_it != goal_map.end(); g_it++) - goals.push_back(g_it); - - // now determine an ordering for those goals: - // 1. alphabetical ordering of file name - // 2. numerical ordering of line number - // 3. alphabetical ordering of goal ID - std::sort( - goals.begin(), - goals.end(), - [](goal_mapt::const_iterator git1, goal_mapt::const_iterator git2) { - const auto &g1 = git1->second.source_location; - const auto &g2 = git2->second.source_location; - if(g1.get_file() != g2.get_file()) - return id2string(g1.get_file()) < id2string(g2.get_file()); - else if(!g1.get_line().empty() && !g2.get_line().empty()) - return std::stoul(id2string(g1.get_line())) < - std::stoul(id2string(g2.get_line())); - else - return id2string(git1->first) < id2string(git2->first); - }); - - // now show in the order we have determined - - irep_idt previous_function; - irep_idt current_file; - for(const auto &g : goals) - { - const auto &l = g->second.source_location; - - if(l.get_function() != previous_function) - { - if(!previous_function.empty()) - result() << '\n'; - previous_function = l.get_function(); - if(!previous_function.empty()) - { - current_file = l.get_file(); - if(!current_file.empty()) - result() << current_file << ' '; - if(!l.get_function().empty()) - result() << "function " << l.get_function(); - result() << eom; - } - } - - result() << faint << '[' << g->first << "] " << reset; - - if(l.get_file() != current_file) - result() << "file " << l.get_file() << ' '; - - if(!l.get_line().empty()) - result() << "line " << l.get_line() << ' '; - - result() << g->second.description << ": "; - - if(g->second.status == goalt::statust::SUCCESS) - result() << green; - else - result() << red; - - result() << g->second.status_string() << reset << eom; - } - - if(bmc.options.get_bool_option("trace")) - { - for(const auto &g : goal_map) - if(g.second.status == goalt::statust::FAILURE) - { - result() << "\n" - << "Trace for " << g.first << ":" - << "\n"; - show_goto_trace( - result(), bmc.ns, g.second.goto_trace, bmc.trace_options()); - result() << eom; - } - } - - status() << "\n** " << cover_goals.number_covered() << " of " - << cover_goals.size() << " failed (" << cover_goals.iterations() - << " iteration" << (cover_goals.iterations() == 1 ? "" : "s") - << ")" << eom; - } - break; - - case ui_message_handlert::uit::XML_UI: - { - for(const auto &g : goal_map) - { - xmlt xml_result( - "result", - {{"property", id2string(g.first)}, - {"status", g.second.status_string()}}, - {}); - - if(g.second.status == goalt::statust::FAILURE) - convert(bmc.ns, g.second.goto_trace, xml_result.new_element()); - - result() << xml_result; - } - break; - } - - case ui_message_handlert::uit::JSON_UI: - { - if(result().tellp() > 0) - result() << eom; // force end of previous message - json_stream_objectt &json_result = - bmc.ui_message_handler.get_json_stream().push_back_stream_object(); - json_stream_arrayt &result_array = - json_result.push_back_stream_array("result"); - - for(const auto &g : goal_map) - { - json_stream_objectt &result = result_array.push_back_stream_object(); - result["property"] = json_stringt(g.first); - result["description"] = json_stringt(g.second.description); - result["status"] = json_stringt(g.second.status_string()); - - if(g.second.status == goalt::statust::FAILURE) - { - json_stream_arrayt &json_trace = result.push_back_stream_array("trace"); - convert( - bmc.ns, g.second.goto_trace, json_trace, bmc.trace_options()); - } - } - } - break; - } -} - -safety_checkert::resultt -bmct::all_properties(const goto_functionst &goto_functions) -{ - bmc_all_propertiest bmc_all_properties(goto_functions, prop_conv, *this); - bmc_all_properties.set_message_handler(get_message_handler()); - return bmc_all_properties(); -} diff --git a/jbmc/src/jbmc/all_properties_class.h b/jbmc/src/jbmc/all_properties_class.h deleted file mode 100644 index a5fc881ada4..00000000000 --- a/jbmc/src/jbmc/all_properties_class.h +++ /dev/null @@ -1,108 +0,0 @@ -/*******************************************************************\ - -Module: Symbolic Execution of ANSI-C - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// Symbolic Execution of ANSI-C - -#ifndef CPROVER_CBMC_ALL_PROPERTIES_CLASS_H -#define CPROVER_CBMC_ALL_PROPERTIES_CLASS_H - -#include -#include - -#include "bmc.h" - -class bmc_all_propertiest : public cover_goalst::observert, public messaget -{ -public: - bmc_all_propertiest( - const goto_functionst &_goto_functions, - prop_convt &_solver, - bmct &_bmc) - : goto_functions(_goto_functions), solver(_solver), bmc(_bmc) - { - } - - safety_checkert::resultt operator()(); - - virtual void goal_covered(const cover_goalst::goalt &); - - struct goalt - { - // a property holds if all instances of it are true - typedef std::vector - instancest; - instancest instances; - std::string description; - source_locationt source_location; - - // if failed, we compute a goto_trace for the first failing instance - enum statust - { - UNKNOWN, - FAILURE, - SUCCESS, - ERROR - } status; - goto_tracet goto_trace; - - std::string status_string() const - { - switch(status) - { - case UNKNOWN: - return "UNKNOWN"; - case FAILURE: - return "FAILURE"; - case SUCCESS: - return "SUCCESS"; - case ERROR: - return "ERROR"; - } - - // make some poor compilers happy - UNREACHABLE; - return ""; - } - - explicit goalt(const goto_programt::instructiont &instruction) - : status(statust::UNKNOWN) - { - source_location = instruction.source_location; - description = id2string(instruction.source_location.get_comment()); - } - - goalt() : status(statust::UNKNOWN) - { - } - - exprt as_expr() const - { - std::vector tmp; - tmp.reserve(instances.size()); - for(const auto &inst : instances) - tmp.push_back(literal_exprt(inst->cond_literal)); - return conjunction(tmp); - } - }; - - typedef std::map goal_mapt; - goal_mapt goal_map; - -protected: - const goto_functionst &goto_functions; - prop_convt &solver; - bmct &bmc; - - virtual void report(const cover_goalst &cover_goals); - virtual void do_before_solving() - { - } -}; - -#endif // CPROVER_CBMC_ALL_PROPERTIES_CLASS_H diff --git a/jbmc/src/jbmc/bmc.cpp b/jbmc/src/jbmc/bmc.cpp deleted file mode 100644 index 7cb6f68f95b..00000000000 --- a/jbmc/src/jbmc/bmc.cpp +++ /dev/null @@ -1,401 +0,0 @@ -/*******************************************************************\ - -Module: Symbolic Execution of ANSI-C - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// Symbolic Execution of ANSI-C - -#include "bmc.h" - -#include -#include - -#include -#include - -#include - -#include -#include - -#include - -#include -#include -#include -#include - -/// Hook used by CEGIS to selectively freeze variables -/// in the SAT solver after the SSA formula is added to the solver. -/// Freezing variables is necessary to make use of incremental -/// solving with MiniSat SimpSolver. -/// Potentially a useful hook for other applications using -/// incremental solving. -void bmct::freeze_program_variables() -{ - // this is a hook for cegis -} - -decision_proceduret::resultt bmct::run_decision_procedure() -{ - status() << "Passing problem to " << prop_conv.decision_procedure_text() - << eom; - - auto solver_start = std::chrono::steady_clock::now(); - - convert_symex_target_equation(equation, prop_conv, get_message_handler()); - - // hook for cegis to freeze synthesis program vars - freeze_program_variables(); - - status() << "Running " << prop_conv.decision_procedure_text() << eom; - - decision_proceduret::resultt dec_result = prop_conv(); - - { - auto solver_stop = std::chrono::steady_clock::now(); - statistics() - << "Runtime decision procedure: " - << std::chrono::duration(solver_stop - solver_start).count() - << "s" << eom; - } - - return dec_result; -} - -safety_checkert::resultt bmct::execute(abstract_goto_modelt &goto_model) -{ - try - { - auto get_goto_function = - [&goto_model]( - const irep_idt &id) -> const goto_functionst::goto_functiont & { - return goto_model.get_goto_function(id); - }; - - perform_symbolic_execution(get_goto_function); - - // Borrow a reference to the goto functions map. This reference, or - // iterators pointing into it, must not be stored by this function or its - // callees, as goto_model.get_goto_function (as used by symex) - // will have side-effects on it. - const goto_functionst &goto_functions = goto_model.get_goto_functions(); - - // 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. - // In particular clients that use symex-driven program loading need to print - // GOTO functions after symex, as function bodies are not produced until - // symex first requests them. - if(driver_callback_after_symex && driver_callback_after_symex()) - return safety_checkert::resultt::SAFE; // to indicate non-error - - if(equation.has_threads()) - { - // When doing path exploration in a concurrent setting, we should avoid - // model-checking the program until we reach the end of a path. - if(symex.should_pause_symex) - return safety_checkert::resultt::PAUSED; - - // add a partial ordering, if required - memory_model->set_message_handler(get_message_handler()); - (*memory_model)(equation); - } - - statistics() << "size of program expression: " << equation.SSA_steps.size() - << " steps" << eom; - - slice(symex, equation, ns, options, ui_message_handler); - - // coverage report - std::string cov_out = options.get_option("symex-coverage-report"); - if( - !cov_out.empty() && symex.output_coverage_report(goto_functions, cov_out)) - { - error() << "Failed to write symex coverage report" << eom; - return safety_checkert::resultt::ERROR; - } - - if(options.get_bool_option("show-vcc")) - { - show_vcc(options, ui_message_handler, equation); - return safety_checkert::resultt::SAFE; // to indicate non-error - } - - // any properties to check at all? - if( - !options.get_bool_option("program-only") && - symex.get_remaining_vccs() == 0) - { - if(options.is_set("paths")) - return safety_checkert::resultt::PAUSED; - report_success(ui_message_handler); - output_graphml(equation, ns, options); - return safety_checkert::resultt::SAFE; - } - - if(options.get_bool_option("program-only")) - { - show_program(ns, equation); - return safety_checkert::resultt::SAFE; - } - - if(!options.is_set("paths") || symex.path_segment_vccs > 0) - return decide(goto_functions); - - return safety_checkert::resultt::PAUSED; - } - - catch(const std::string &error_str) - { - messaget message(get_message_handler()); - message.error().source_location = symex.last_source_location; - message.error() << error_str << messaget::eom; - - return safety_checkert::resultt::ERROR; - } - - catch(const char *error_str) - { - messaget message(get_message_handler()); - message.error().source_location = symex.last_source_location; - message.error() << error_str << messaget::eom; - - return safety_checkert::resultt::ERROR; - } - - catch(const std::bad_alloc &) - { - error() << "Out of memory" << eom; - return safety_checkert::resultt::ERROR; - } -} - -safety_checkert::resultt bmct::run(abstract_goto_modelt &goto_model) -{ - memory_model = get_memory_model(options, ns); - setup_symex(symex, ns, options, ui_message_handler); - - return execute(goto_model); -} - -safety_checkert::resultt bmct::decide(const goto_functionst &goto_functions) -{ - if(options.get_bool_option("stop-on-fail")) - return stop_on_fail(); - else - return all_properties(goto_functions); -} - -safety_checkert::resultt bmct::stop_on_fail() -{ - switch(run_decision_procedure()) - { - case decision_proceduret::resultt::D_UNSATISFIABLE: - report_success(ui_message_handler); - output_graphml(equation, ns, options); - return resultt::SAFE; - - case decision_proceduret::resultt::D_SATISFIABLE: - if(options.get_bool_option("trace")) - { - if(options.get_bool_option("beautify")) - { - // NOLINTNEXTLINE(whitespace/braces) - counterexample_beautificationt{ui_message_handler}( - dynamic_cast(prop_conv), equation); - } - - build_error_trace( - error_trace, ns, equation, prop_conv, ui_message_handler); - output_error_trace(error_trace, ns, trace_options(), ui_message_handler); - output_graphml(error_trace, ns, options); - } - - report_failure(ui_message_handler); - return resultt::UNSAFE; - - default: - if(options.get_bool_option("dimacs") || options.get_option("outfile") != "") - return resultt::SAFE; - - error() << "decision procedure failed" << eom; - - return resultt::ERROR; - } - - UNREACHABLE; -} - -/// Perform core BMC, using an abstract model to supply GOTO function bodies -/// (perhaps created on demand). -/// \param opts: command-line options affecting BMC -/// \param model: provides goto function bodies and the symbol table, perhaps -/// creating those function bodies on demand. -/// \param ui: user-interface mode (plain text, XML output, JSON output, ...) -/// \param driver_configure_bmc: function provided by the driver program, -/// which applies driver-specific configuration to a bmct before running. -/// \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 optionst &opts, - abstract_goto_modelt &model, - ui_message_handlert &ui, - std::function driver_configure_bmc, - std::function callback_after_symex) -{ - safety_checkert::resultt final_result = safety_checkert::resultt::SAFE; - safety_checkert::resultt tmp_result = safety_checkert::resultt::SAFE; - const symbol_tablet &symbol_table = model.get_symbol_table(); - namespacet ns(symbol_table); - messaget message(ui); - std::unique_ptr worklist; - guard_managert guard_manager; - std::string strategy = opts.get_option("exploration-strategy"); - worklist = get_path_strategy(strategy); - try - { - solver_factoryt solvers( - opts, ns, ui, ui.get_ui() == ui_message_handlert::uit::XML_UI); - - { - std::unique_ptr cbmc_solver = - solvers.get_solver(); - prop_convt &pc = cbmc_solver->prop_conv(); - bmct bmc( - opts, - symbol_table, - ui, - pc, - *worklist, - callback_after_symex, - guard_manager); - if(driver_configure_bmc) - driver_configure_bmc(bmc, symbol_table); - tmp_result = bmc.run(model); - - if( - tmp_result == safety_checkert::resultt::UNSAFE && - opts.get_bool_option("stop-on-fail") && opts.is_set("paths")) - { - worklist->clear(); - return CPROVER_EXIT_VERIFICATION_UNSAFE; - } - - if(tmp_result != safety_checkert::resultt::PAUSED) - final_result = tmp_result; - } - INVARIANT( - 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."); - - // When model checking, the bmc.run() above will already have explored - // 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 - // explore in the worklist. We thus need to run the above code again, - // once for each saved path in the worklist, to continue symbolically - // execute the program. Note that the code in the loop is similar to - // the code above except that we construct a path_explorert rather than - // a bmct, which allows us to execute from a saved state rather than - // from the entry point. See the path_explorert documentation, and the - // difference between the implementations of perform_symbolic_exection() - // in bmct and path_explorert, for more information. - - while(!worklist->empty()) - { - std::unique_ptr cbmc_solver = - solvers.get_solver(); - prop_convt &pc = cbmc_solver->prop_conv(); - path_storaget::patht &resume = worklist->peek(); - path_explorert pe( - opts, - symbol_table, - ui, - pc, - resume.equation, - resume.state, - *worklist, - guard_manager, - callback_after_symex); - if(driver_configure_bmc) - driver_configure_bmc(pe, symbol_table); - tmp_result = pe.run(model); - - if( - tmp_result == safety_checkert::resultt::UNSAFE && - opts.get_bool_option("stop-on-fail") && opts.is_set("paths")) - { - worklist->clear(); - return CPROVER_EXIT_VERIFICATION_UNSAFE; - } - - if(tmp_result != safety_checkert::resultt::PAUSED) - final_result &= tmp_result; - worklist->pop(); - } - } - catch(const char *error_msg) - { - message.error() << error_msg << message.eom; - return CPROVER_EXIT_EXCEPTION; - } - catch(const std::string &error_msg) - { - message.error() << error_msg << message.eom; - return CPROVER_EXIT_EXCEPTION; - } - catch(std::runtime_error &e) - { - message.error() << e.what() << message.eom; - return CPROVER_EXIT_EXCEPTION; - } - - switch(final_result) - { - case safety_checkert::resultt::SAFE: - if(opts.is_set("paths")) - report_success(ui); - return CPROVER_EXIT_VERIFICATION_SAFE; - case safety_checkert::resultt::UNSAFE: - if(opts.is_set("paths")) - report_failure(ui); - return CPROVER_EXIT_VERIFICATION_UNSAFE; - case safety_checkert::resultt::ERROR: - return CPROVER_EXIT_INTERNAL_ERROR; - case safety_checkert::resultt::PAUSED: - UNREACHABLE; - } - UNREACHABLE; -} - -void bmct::perform_symbolic_execution( - goto_symext::get_goto_functiont get_goto_function) -{ - symex.symex_from_entry_point_of(get_goto_function, symex_symbol_table); - - if(options.get_bool_option("validate-ssa-equation")) - { - symex.validate(validation_modet::INVARIANT); - } - - INVARIANT( - 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"); -} - -void path_explorert::perform_symbolic_execution( - goto_symext::get_goto_functiont get_goto_function) -{ - symex.resume_symex_from_saved_state( - get_goto_function, saved_state, &equation, symex_symbol_table); -} diff --git a/jbmc/src/jbmc/bmc.h b/jbmc/src/jbmc/bmc.h deleted file mode 100644 index e0bc5326ed7..00000000000 --- a/jbmc/src/jbmc/bmc.h +++ /dev/null @@ -1,270 +0,0 @@ -/*******************************************************************\ - -Module: Bounded Model Checking for ANSI-C + HDL - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// Bounded Model Checking for ANSI-C + HDL - -#ifndef CPROVER_CBMC_BMC_H -#define CPROVER_CBMC_BMC_H - -#include -#include - -#include -#include -#include - -#include - -#include - -#include -#include - -#include -#include -#include - -#include - -class cbmc_solverst; - -/// \brief Bounded model checking or path exploration for goto-programs -/// -/// Higher-level architectural information on symbolic execution is -/// documented in the \ref symex-overview -/// "Symbolic execution module page". -class bmct : public safety_checkert -{ -public: - /// \brief Constructor for path exploration with freshly-initialized state - /// - /// This constructor should be used for symbolically executing a program - /// from the entry point with fresh state. There are two main behaviours - /// that can happen when constructing an instance of this class: - /// - /// - If the `--paths` flag in the `options` argument to this - /// 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 `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 `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 - /// `path_storage` and using it to construct a path_explorert - /// object. - bmct( - const optionst &_options, - const symbol_tablet &outer_symbol_table, - ui_message_handlert &_message_handler, - prop_convt &_prop_conv, - path_storaget &_path_storage, - std::function callback_after_symex, - guard_managert &guard_manager) - : safety_checkert(ns, _message_handler), - options(_options), - outer_symbol_table(outer_symbol_table), - ns(outer_symbol_table, symex_symbol_table), - equation(_message_handler), - guard_manager(guard_manager), - path_storage(_path_storage), - symex( - _message_handler, - outer_symbol_table, - equation, - options, - path_storage, - guard_manager), - prop_conv(_prop_conv), - ui_message_handler(_message_handler), - driver_callback_after_symex(callback_after_symex) - { - } - - virtual resultt run(const goto_functionst &goto_functions) - { - wrapper_goto_modelt model(outer_symbol_table, goto_functions); - return run(model); - } - resultt run(abstract_goto_modelt &); - void setup(); - safety_checkert::resultt execute(abstract_goto_modelt &); - virtual ~bmct() - { - } - - // the safety_checkert interface - virtual resultt operator()(const goto_functionst &goto_functions) - { - return run(goto_functions); - } - - void add_loop_unwind_handler(symex_bmct::loop_unwind_handlert handler) - { - symex.add_loop_unwind_handler(handler); - } - - void - add_unwind_recursion_handler(symex_bmct::recursion_unwind_handlert handler) - { - symex.add_recursion_unwind_handler(handler); - } - - static int do_language_agnostic_bmc( - const optionst &opts, - abstract_goto_modelt &goto_model, - ui_message_handlert &ui, - std::function driver_configure_bmc = - nullptr, - std::function callback_after_symex = nullptr); - -protected: - /// \brief Constructor for path exploration from saved state - /// - /// 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 path_storaget argument, and also takes a - /// symex_target_equationt. See the documentation for path_explorert for - /// details. - bmct( - const optionst &_options, - const symbol_tablet &outer_symbol_table, - ui_message_handlert &_message_handler, - prop_convt &_prop_conv, - symex_target_equationt &_equation, - path_storaget &_path_storage, - std::function callback_after_symex, - guard_managert &guard_manager) - : safety_checkert(ns, _message_handler), - options(_options), - outer_symbol_table(outer_symbol_table), - ns(outer_symbol_table), - equation(_equation), - guard_manager(guard_manager), - path_storage(_path_storage), - symex( - _message_handler, - outer_symbol_table, - equation, - options, - path_storage, - guard_manager), - prop_conv(_prop_conv), - ui_message_handler(_message_handler), - driver_callback_after_symex(callback_after_symex) - { - INVARIANT( - options.get_bool_option("paths"), - "Should only use saved equation & goto_state constructor " - "when doing path exploration"); - } - - const optionst &options; - /// \brief symbol table for the goto-program that we will execute - const symbol_tablet &outer_symbol_table; - /// \brief symbol table generated during symbolic execution - symbol_tablet symex_symbol_table; - namespacet ns; - symex_target_equationt equation; - guard_managert &guard_manager; - path_storaget &path_storage; - symex_bmct symex; - prop_convt &prop_conv; - std::unique_ptr memory_model; - // use gui format - ui_message_handlert &ui_message_handler; - - virtual decision_proceduret::resultt run_decision_procedure(); - - virtual resultt decide(const goto_functionst &); - - virtual void freeze_program_variables(); - - trace_optionst trace_options() - { - return trace_optionst(options); - } - - virtual resultt all_properties(const goto_functionst &goto_functions); - virtual resultt stop_on_fail(); - - friend class bmc_all_propertiest; - -private: - /// \brief Class-specific symbolic execution - /// - /// This private virtual should be overridden by derived classes to - /// invoke the symbolic executor in a class-specific way. This - /// implementation invokes goto_symext::operator() to perform - /// full-program model-checking from the entry point of the program. - virtual void - perform_symbolic_execution(goto_symext::get_goto_functiont get_goto_function); - - /// Optional callback, to be run after symex but before handing the resulting - /// equation to the solver. If it returns true then we will skip the solver - /// stage and return "safe" (no assertions violated / coverage goals reached), - /// similar to the behaviour when 'show-vcc' or 'program-only' are specified. - std::function driver_callback_after_symex; -}; - -/// \brief Symbolic execution from a saved branch point -/// -/// Instances of this class execute a single program path from a saved -/// branch point. The saved branch point is supplied to the constructor -/// as a pair of goto_target_equationt (which holds the SSA steps -/// executed so far), and a goto_symex_statet Note that the \ref bmct -/// base class can also execute a single path (it will do so if the -/// `--paths` flag is set in its `options` member), but will always -/// begin symbolic execution from the beginning of the program with -/// fresh state. -class path_explorert : public bmct -{ -public: - path_explorert( - const optionst &_options, - const symbol_tablet &outer_symbol_table, - ui_message_handlert &_message_handler, - prop_convt &_prop_conv, - symex_target_equationt &saved_equation, - const goto_symex_statet &saved_state, - path_storaget &path_storage, - guard_managert &guard_manager, - std::function callback_after_symex) - : bmct( - _options, - outer_symbol_table, - _message_handler, - _prop_conv, - saved_equation, - path_storage, - callback_after_symex, - guard_manager), - saved_state(saved_state) - { - } - -protected: - const goto_symex_statet &saved_state; - -private: - /// \brief Resume symbolic execution from saved branch point - /// - /// This overrides the base implementation to call the symbolic executor with - /// the saved symex_target_equationt, symbol_tablet, and goto_symex_statet - /// provided as arguments to the constructor of this class. - void perform_symbolic_execution( - goto_symext::get_goto_functiont get_goto_function) override; -}; - -#endif // CPROVER_CBMC_BMC_H diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index da0d056609b..61dc2bef46f 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -61,8 +61,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include "bmc.h" // will go away - #include #include #include @@ -419,7 +417,7 @@ int jbmc_parse_optionst::doit() if(cmdline.isset("version")) { std::cout << CBMC_VERSION << '\n'; - return 0; // should contemplate EX_OK from sysexits.h + return CPROVER_EXIT_SUCCESS; } messaget::eval_verbosity( @@ -471,7 +469,7 @@ int jbmc_parse_optionst::doit() if(cmdline.args.size()!=1) { log.error() << "Please give exactly one source file" << messaget::eom; - return 6; + return CPROVER_EXIT_INCORRECT_TASK; } std::string filename=cmdline.args[0]; @@ -486,7 +484,7 @@ int jbmc_parse_optionst::doit() { log.error() << "failed to open input file `" << filename << "'" << messaget::eom; - return 6; + return CPROVER_EXIT_INCORRECT_TASK; } std::unique_ptr language= @@ -496,7 +494,7 @@ int jbmc_parse_optionst::doit() { log.error() << "failed to figure out type of file `" << filename << "'" << messaget::eom; - return 6; + return CPROVER_EXIT_INCORRECT_TASK; } language->set_language_options(options); @@ -507,27 +505,11 @@ int jbmc_parse_optionst::doit() if(language->parse(infile, filename)) { log.error() << "PARSING ERROR" << messaget::eom; - return 6; + return CPROVER_EXIT_PARSE_ERROR; } language->show_parse(std::cout); - return 0; - } - - std::function configure_bmc = nullptr; - if(options.get_bool_option("java-unwind-enum-static")) - { - configure_bmc = - [](bmct &bmc, const symbol_tablet &symbol_table) { - bmc.add_loop_unwind_handler([&symbol_table]( - const call_stackt &context, - unsigned loop_number, - unsigned unwind, - unsigned &max_unwind) { - return java_enum_static_init_unwind_handler( - context, loop_number, unwind, max_unwind, symbol_table); - }); - }; + return CPROVER_EXIT_SUCCESS; } object_factory_params.set(options); @@ -538,7 +520,7 @@ int jbmc_parse_optionst::doit() if(cmdline.args.empty()) { log.error() << "Please provide a program to verify" << messaget::eom; - return 6; + return CPROVER_EXIT_INCORRECT_TASK; } if(cmdline.args.size() != 1) @@ -549,265 +531,201 @@ int jbmc_parse_optionst::doit() " or '--lazy-methods-extra-entry-point " "somepackage.SomeClass.method' along with '--classpath'" << messaget::eom; - return 6; + return CPROVER_EXIT_INCORRECT_TASK; } - if(!cmdline.isset("symex-driven-lazy-loading")) - { - std::unique_ptr goto_model_ptr; - int get_goto_program_ret=get_goto_program(goto_model_ptr, options); - if(get_goto_program_ret!=-1) - return get_goto_program_ret; + std::unique_ptr goto_model_ptr; + int get_goto_program_ret = get_goto_program(goto_model_ptr, options); + if(get_goto_program_ret != -1) + return get_goto_program_ret; - goto_modelt &goto_model = *goto_model_ptr; - - if(cmdline.isset("show-properties")) + if( + options.get_bool_option("program-only") || + options.get_bool_option("show-vcc") || + (options.get_bool_option("symex-driven-lazy-loading") && + (cmdline.isset("show-symbol-table") || cmdline.isset("list-symbols") || + cmdline.isset("show-goto-functions") || + cmdline.isset("list-goto-functions") || + cmdline.isset("show-properties") || cmdline.isset("show-loops")))) + { + if(options.get_bool_option("paths")) { - show_properties( - goto_model, log.get_message_handler(), ui_message_handler.get_ui()); - return 0; // should contemplate EX_OK from sysexits.h + all_properties_verifiert verifier( + options, ui_message_handler, *goto_model_ptr); + (void)verifier(); } - - if(set_properties(goto_model)) - return 7; // should contemplate EX_USAGE from sysexits.h - - if( - options.get_bool_option("program-only") || - options.get_bool_option("show-vcc")) + else { - if(options.get_bool_option("paths")) - { - all_properties_verifiert verifier( - options, ui_message_handler, goto_model); - (void)verifier(); - } - else - { - all_properties_verifiert verifier( - options, ui_message_handler, goto_model); - (void)verifier(); - } - - return CPROVER_EXIT_SUCCESS; + all_properties_verifiert verifier( + options, ui_message_handler, *goto_model_ptr); + (void)verifier(); } - if( - options.get_bool_option("dimacs") || - !options.get_option("outfile").empty()) + if(options.get_bool_option("symex-driven-lazy-loading")) { - if(options.get_bool_option("paths")) - { - stop_on_fail_verifiert verifier( - options, ui_message_handler, goto_model); - (void)verifier(); - } - else - { - stop_on_fail_verifiert verifier( - options, ui_message_handler, goto_model); - (void)verifier(); - } - - return CPROVER_EXIT_SUCCESS; + // We can only output these after goto-symex has run. + (void)show_loaded_symbols(*goto_model_ptr); + (void)show_loaded_functions(*goto_model_ptr); } - std::unique_ptr verifier = nullptr; + return CPROVER_EXIT_SUCCESS; + } - if( - options.get_bool_option("stop-on-fail") && - options.get_bool_option("paths")) + if( + options.get_bool_option("dimacs") || !options.get_option("outfile").empty()) + { + if(options.get_bool_option("paths")) { - verifier = util_make_unique< - stop_on_fail_verifiert>( - options, ui_message_handler, goto_model); + stop_on_fail_verifiert verifier( + options, ui_message_handler, *goto_model_ptr); + (void)verifier(); } - else if( - options.get_bool_option("stop-on-fail") && - !options.get_bool_option("paths")) - { - if(options.get_bool_option("localize-faults")) - { - verifier = - util_make_unique>( - options, ui_message_handler, goto_model); - } - else - { - verifier = util_make_unique< - stop_on_fail_verifiert>( - options, ui_message_handler, goto_model); - } - } - else if( - !options.get_bool_option("stop-on-fail") && - options.get_bool_option("paths")) + else { - verifier = util_make_unique>( - options, ui_message_handler, goto_model); + stop_on_fail_verifiert verifier( + options, ui_message_handler, *goto_model_ptr); + (void)verifier(); } - else if( - !options.get_bool_option("stop-on-fail") && - !options.get_bool_option("paths")) + + return CPROVER_EXIT_SUCCESS; + } + + std::unique_ptr verifier = nullptr; + + if( + options.get_bool_option("stop-on-fail") && options.get_bool_option("paths")) + { + verifier = + util_make_unique>( + options, ui_message_handler, *goto_model_ptr); + } + else if( + options.get_bool_option("stop-on-fail") && + !options.get_bool_option("paths")) + { + if(options.get_bool_option("localize-faults")) { - if(options.get_bool_option("localize-faults")) - { - verifier = - util_make_unique>( - options, ui_message_handler, goto_model); - } - else - { - verifier = util_make_unique>( - options, ui_message_handler, goto_model); - } + options, ui_message_handler, *goto_model_ptr); } else { - // fall back until everything has been ported to goto-checker - - // The `configure_bmc` callback passed will enable enum-unwind-static if - // applicable. - return bmct::do_language_agnostic_bmc( - options, goto_model, ui_message_handler, configure_bmc); + verifier = util_make_unique< + stop_on_fail_verifiert>( + options, ui_message_handler, *goto_model_ptr); } - - const resultt result = (*verifier)(); - verifier->report(); - return result_to_exit_code(result); } - else + else if( + !options.get_bool_option("stop-on-fail") && + options.get_bool_option("paths")) { - // Use symex-driven lazy loading: - lazy_goto_modelt lazy_goto_model = - lazy_goto_modelt::from_handler_object(*this, options, ui_message_handler); - lazy_goto_model.initialize(cmdline.args, options); - - class_hierarchy = - util_make_unique(lazy_goto_model.symbol_table); - - // The precise wording of this error matches goto-symex's complaint when no - // __CPROVER_start exists (if we just go ahead and run it anyway it will - // trip an invariant when it tries to load it) - if(!lazy_goto_model.symbol_table.has_symbol(goto_functionst::entry_point())) + verifier = util_make_unique>( + options, ui_message_handler, *goto_model_ptr); + } + else if( + !options.get_bool_option("stop-on-fail") && + !options.get_bool_option("paths")) + { + if(options.get_bool_option("localize-faults")) { - log.error() << "the program has no entry point"; - return 6; + verifier = + util_make_unique>( + options, ui_message_handler, *goto_model_ptr); } - - // Add failed symbols for any symbol created prior to loading any - // particular function: - add_failed_symbols(lazy_goto_model.symbol_table); - - if(cmdline.isset("validate-goto-model")) + else { - lazy_goto_model.validate(); + verifier = util_make_unique>( + options, ui_message_handler, *goto_model_ptr); } - - // Provide show-goto-functions and similar dump functions after symex - // executes. If --paths is active, these dump routines run after every - // paths iteration. Its return value indicates that if we ran any dump - // function, then we should skip the actual solver phase. - auto callback_after_symex = [this, &lazy_goto_model]() { - return show_loaded_functions(lazy_goto_model); - }; - - // The `configure_bmc` callback passed will enable enum-unwind-static if - // applicable. - return bmct::do_language_agnostic_bmc( - options, - lazy_goto_model, - ui_message_handler, - configure_bmc, - callback_after_symex); } -} - -bool jbmc_parse_optionst::set_properties(goto_modelt &goto_model) -{ - if(cmdline.isset("property")) - ::set_properties(goto_model, cmdline.get_values("property")); + else + { + UNREACHABLE; + } - return false; + const resultt result = (*verifier)(); + verifier->report(); + return result_to_exit_code(result); } int jbmc_parse_optionst::get_goto_program( - std::unique_ptr &goto_model, + std::unique_ptr &goto_model_ptr, const optionst &options) { - { - lazy_goto_modelt lazy_goto_model = - lazy_goto_modelt::from_handler_object(*this, options, ui_message_handler); - lazy_goto_model.initialize(cmdline.args, options); + lazy_goto_modelt lazy_goto_model = + lazy_goto_modelt::from_handler_object(*this, options, ui_message_handler); + lazy_goto_model.initialize(cmdline.args, options); - class_hierarchy = - util_make_unique(lazy_goto_model.symbol_table); + class_hierarchy = + util_make_unique(lazy_goto_model.symbol_table); - // Show the class hierarchy - if(cmdline.isset("show-class-hierarchy")) - { - show_class_hierarchy(*class_hierarchy, ui_message_handler); - return CPROVER_EXIT_SUCCESS; - } + // Show the class hierarchy + if(cmdline.isset("show-class-hierarchy")) + { + show_class_hierarchy(*class_hierarchy, ui_message_handler); + return CPROVER_EXIT_SUCCESS; + } - // Add failed symbols for any symbol created prior to loading any - // particular function: - add_failed_symbols(lazy_goto_model.symbol_table); + // Add failed symbols for any symbol created prior to loading any + // particular function: + add_failed_symbols(lazy_goto_model.symbol_table); + if(!options.get_bool_option("symex-driven-lazy-loading")) + { log.status() << "Generating GOTO Program" << messaget::eom; lazy_goto_model.load_all_functions(); - // Show the symbol table before process_goto_functions mangles return - // values, etc - if(cmdline.isset("show-symbol-table")) - { - show_symbol_table(lazy_goto_model.symbol_table, ui_message_handler); - return 0; - } - else if(cmdline.isset("list-symbols")) - { - show_symbol_table_brief(lazy_goto_model.symbol_table, ui_message_handler); - return 0; - } + // show symbol table or list symbols + if(show_loaded_symbols(lazy_goto_model)) + return CPROVER_EXIT_SUCCESS; // Move the model out of the local lazy_goto_model // and into the caller's goto_model - goto_model=lazy_goto_modelt::process_whole_model_and_freeze( + goto_model_ptr = lazy_goto_modelt::process_whole_model_and_freeze( std::move(lazy_goto_model)); - if(goto_model == nullptr) - return 6; + if(goto_model_ptr == nullptr) + return CPROVER_EXIT_INTERNAL_ERROR; + + goto_modelt &goto_model = dynamic_cast(*goto_model_ptr); if(cmdline.isset("validate-goto-model")) { - goto_model->validate(); + goto_model.validate(); } - // show it? - if(cmdline.isset("show-loops")) + if(show_loaded_functions(goto_model)) + return CPROVER_EXIT_SUCCESS; + + if(cmdline.isset("property")) + ::set_properties(goto_model, cmdline.get_values("property")); + } + else + { + // The precise wording of this error matches goto-symex's complaint when no + // __CPROVER_start exists (if we just go ahead and run it anyway it will + // trip an invariant when it tries to load it) + if(!lazy_goto_model.symbol_table.has_symbol(goto_functionst::entry_point())) { - show_loop_ids(ui_message_handler.get_ui(), *goto_model); - return 0; + log.error() << "the program has no entry point" << messaget::eom; + return CPROVER_EXIT_INCORRECT_TASK; } - // show it? - if( - cmdline.isset("show-goto-functions") || - cmdline.isset("list-goto-functions")) + if(cmdline.isset("validate-goto-model")) { - show_goto_functions( - *goto_model, - log.get_message_handler(), - ui_message_handler.get_ui(), - cmdline.isset("list-goto-functions")); - return 0; + lazy_goto_model.validate(); } - log.status() << config.object_bits_info() << messaget::eom; + goto_model_ptr = + util_make_unique(std::move(lazy_goto_model)); } + log.status() << config.object_bits_info() << messaget::eom; + return -1; // no error, continue } @@ -823,87 +741,83 @@ void jbmc_parse_optionst::process_goto_function( bool using_symex_driven_loading = options.get_bool_option("symex-driven-lazy-loading"); - { - // Removal of RTTI inspection: - remove_instanceof( - function.get_function_id(), - goto_function, - symbol_table, - *class_hierarchy, - log.get_message_handler()); - // Java virtual functions -> explicit dispatch tables: - remove_virtual_functions(function); - - auto function_is_stub = [&symbol_table, &model](const irep_idt &id) { - return symbol_table.lookup_ref(id).value.is_nil() && - !model.can_produce_function(id); - }; - - remove_returns(function, function_is_stub); + // Removal of RTTI inspection: + remove_instanceof( + function.get_function_id(), + goto_function, + symbol_table, + *class_hierarchy, + log.get_message_handler()); + // Java virtual functions -> explicit dispatch tables: + remove_virtual_functions(function); - replace_java_nondet(function); + auto function_is_stub = [&symbol_table, &model](const irep_idt &id) { + return symbol_table.lookup_ref(id).value.is_nil() && + !model.can_produce_function(id); + }; - // Similar removal of java nondet statements: - convert_nondet( - function, ui_message_handler, object_factory_params, ID_java); + remove_returns(function, function_is_stub); - if(using_symex_driven_loading) - { - // remove exceptions - // If using symex-driven function loading we need to do this now so that - // symex doesn't have to cope with exception-handling constructs; however - // the results are slightly worse than running it in whole-program mode - // (e.g. dead catch sites will be retained) - remove_exceptions( - function.get_function_id(), - goto_function.body, - symbol_table, - *class_hierarchy.get(), - ui_message_handler); - } + replace_java_nondet(function); - // add generic checks - goto_check( - function.get_function_id(), function.get_goto_function(), ns, options); + // Similar removal of java nondet statements: + convert_nondet(function, ui_message_handler, object_factory_params, ID_java); - // Replace Java new side effects - remove_java_new( + if(using_symex_driven_loading) + { + // remove exceptions + // If using symex-driven function loading we need to do this now so that + // symex doesn't have to cope with exception-handling constructs; however + // the results are slightly worse than running it in whole-program mode + // (e.g. dead catch sites will be retained) + remove_exceptions( function.get_function_id(), - goto_function, + goto_function.body, symbol_table, + *class_hierarchy.get(), ui_message_handler); + } - // checks don't know about adjusted float expressions - adjust_float_expressions(goto_function, ns); - - // add failed symbols for anything created relating to this particular - // function (note this means subseqent passes mustn't create more!): - journalling_symbol_tablet::changesett new_symbols = - symbol_table.get_inserted(); - for(const irep_idt &new_symbol_name : new_symbols) - { - add_failed_symbol_if_needed( - symbol_table.lookup_ref(new_symbol_name), - symbol_table); - } + // add generic checks + goto_check( + function.get_function_id(), function.get_goto_function(), ns, options); + + // Replace Java new side effects + remove_java_new( + function.get_function_id(), + goto_function, + symbol_table, + ui_message_handler); + + // checks don't know about adjusted float expressions + adjust_float_expressions(goto_function, ns); + + // add failed symbols for anything created relating to this particular + // function (note this means subsequent passes mustn't create more!): + journalling_symbol_tablet::changesett new_symbols = + symbol_table.get_inserted(); + for(const irep_idt &new_symbol_name : new_symbols) + { + add_failed_symbol_if_needed( + symbol_table.lookup_ref(new_symbol_name), symbol_table); + } - // If using symex-driven function loading we must label the assertions - // now so symex sees its targets; otherwise we leave this until - // process_goto_functions, as we haven't run remove_exceptions yet, and that - // pass alters the CFG. - if(using_symex_driven_loading) - { - // label the assertions - label_properties(goto_function.body); + // If using symex-driven function loading we must label the assertions + // now so symex sees its targets; otherwise we leave this until + // process_goto_functions, as we haven't run remove_exceptions yet, and that + // pass alters the CFG. + if(using_symex_driven_loading) + { + // label the assertions + label_properties(goto_function.body); - goto_function.body.update(); - function.compute_location_numbers(); - goto_function.body.compute_loop_numbers(); - } + goto_function.body.update(); + function.compute_location_numbers(); + goto_function.body.compute_loop_numbers(); } } -bool jbmc_parse_optionst::show_loaded_functions( +bool jbmc_parse_optionst::show_loaded_symbols( const abstract_goto_modelt &goto_model) { if(cmdline.isset("show-symbol-table")) @@ -917,6 +831,12 @@ bool jbmc_parse_optionst::show_loaded_functions( return true; } + return false; +} + +bool jbmc_parse_optionst::show_loaded_functions( + const abstract_goto_modelt &goto_model) +{ if(cmdline.isset("show-loops")) { show_loop_ids(ui_message_handler.get_ui(), goto_model.get_goto_functions()); @@ -955,96 +875,94 @@ bool jbmc_parse_optionst::process_goto_functions( goto_modelt &goto_model, const optionst &options) { - { - log.status() << "Running GOTO functions transformation passes" - << messaget::eom; - - bool using_symex_driven_loading = - options.get_bool_option("symex-driven-lazy-loading"); + log.status() << "Running GOTO functions transformation passes" + << messaget::eom; - // When using symex-driven lazy loading, *all* relevant processing is done - // during process_goto_function, so we have nothing to do here. - if(using_symex_driven_loading) - return false; + bool using_symex_driven_loading = + options.get_bool_option("symex-driven-lazy-loading"); - // remove catch and throw - remove_exceptions( - goto_model, *class_hierarchy.get(), log.get_message_handler()); + // When using symex-driven lazy loading, *all* relevant processing is done + // during process_goto_function, so we have nothing to do here. + if(using_symex_driven_loading) + return false; - // instrument library preconditions - instrument_preconditions(goto_model); + // remove catch and throw + remove_exceptions( + goto_model, *class_hierarchy.get(), log.get_message_handler()); - // ignore default/user-specified initialization - // of variables with static lifetime - if(cmdline.isset("nondet-static")) - { - log.status() << "Adding nondeterministic initialization " - "of static/global variables" - << messaget::eom; - nondet_static(goto_model); - } + // instrument library preconditions + instrument_preconditions(goto_model); - // recalculate numbers, etc. - goto_model.goto_functions.update(); + // ignore default/user-specified initialization + // of variables with static lifetime + if(cmdline.isset("nondet-static")) + { + log.status() << "Adding nondeterministic initialization " + "of static/global variables" + << messaget::eom; + nondet_static(goto_model); + } - if(cmdline.isset("drop-unused-functions")) - { - // Entry point will have been set before and function pointers removed - log.status() << "Removing unused functions" << messaget::eom; - remove_unused_functions(goto_model, log.get_message_handler()); - } + // recalculate numbers, etc. + goto_model.goto_functions.update(); - // remove skips such that trivial GOTOs are deleted - remove_skip(goto_model); + if(cmdline.isset("drop-unused-functions")) + { + // Entry point will have been set before and function pointers removed + log.status() << "Removing unused functions" << messaget::eom; + remove_unused_functions(goto_model, log.get_message_handler()); + } - // label the assertions - // This must be done after adding assertions and - // before using the argument of the "property" option. - // Do not re-label after using the property slicer because - // this would cause the property identifiers to change. - label_properties(goto_model); - - // reachability slice? - if(cmdline.isset("reachability-slice-fb")) - { - if(cmdline.isset("reachability-slice")) - { - log.error() << "--reachability-slice and --reachability-slice-fb " - << "must not be given together" << messaget::eom; - return true; - } + // remove skips such that trivial GOTOs are deleted + remove_skip(goto_model); - log.status() << "Performing a forwards-backwards reachability slice" - << messaget::eom; - if(cmdline.isset("property")) - reachability_slicer(goto_model, cmdline.get_values("property"), true); - else - reachability_slicer(goto_model, true); - } + // label the assertions + // This must be done after adding assertions and + // before using the argument of the "property" option. + // Do not re-label after using the property slicer because + // this would cause the property identifiers to change. + label_properties(goto_model); + // reachability slice? + if(cmdline.isset("reachability-slice-fb")) + { 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")); - else - reachability_slicer(goto_model); + log.error() << "--reachability-slice and --reachability-slice-fb " + << "must not be given together" << messaget::eom; + return true; } - // full slice? - if(cmdline.isset("full-slice")) - { - log.status() << "Performing a full slice" << messaget::eom; - if(cmdline.isset("property")) - property_slicer(goto_model, cmdline.get_values("property")); - else - full_slicer(goto_model); - } + log.status() << "Performing a forwards-backwards reachability slice" + << messaget::eom; + if(cmdline.isset("property")) + reachability_slicer(goto_model, cmdline.get_values("property"), true); + else + reachability_slicer(goto_model, true); + } + + 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")); + else + reachability_slicer(goto_model); + } - // remove any skips introduced - remove_skip(goto_model); + // full slice? + if(cmdline.isset("full-slice")) + { + log.status() << "Performing a full slice" << messaget::eom; + if(cmdline.isset("property")) + property_slicer(goto_model, cmdline.get_values("property")); + else + full_slicer(goto_model); } + // remove any skips introduced + remove_skip(goto_model); + return false; } diff --git a/jbmc/src/jbmc/jbmc_parse_options.h b/jbmc/src/jbmc/jbmc_parse_options.h index 8196dfe591c..b2685cab415 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.h +++ b/jbmc/src/jbmc/jbmc_parse_options.h @@ -125,10 +125,10 @@ class jbmc_parse_optionst : public parse_options_baset void get_command_line_options(optionst &); int get_goto_program( - std::unique_ptr &goto_model, const optionst &); + std::unique_ptr &goto_model, + const optionst &); bool show_loaded_functions(const abstract_goto_modelt &goto_model); - - bool set_properties(goto_modelt &goto_model); + bool show_loaded_symbols(const abstract_goto_modelt &goto_model); }; #endif // CPROVER_JBMC_JBMC_PARSE_OPTIONS_H diff --git a/src/goto-checker/all_properties_verifier.h b/src/goto-checker/all_properties_verifier.h index 8462a845d0e..2ef72dcb81a 100644 --- a/src/goto-checker/all_properties_verifier.h +++ b/src/goto-checker/all_properties_verifier.h @@ -35,10 +35,6 @@ class all_properties_verifiert : public goto_verifiert resultt operator()() override { - // have we got anything to check? otherwise we return PASS - if(!has_properties_to_check(properties)) - return resultt::PASS; - while(incremental_goto_checker(properties).progress != incremental_goto_checkert::resultt::progresst::DONE) { diff --git a/src/goto-checker/multi_path_symex_only_checker.cpp b/src/goto-checker/multi_path_symex_only_checker.cpp index d068b28b364..c03fb9ca9b3 100644 --- a/src/goto-checker/multi_path_symex_only_checker.cpp +++ b/src/goto-checker/multi_path_symex_only_checker.cpp @@ -75,6 +75,9 @@ void multi_path_symex_only_checkert::update_properties( propertiest &properties, std::unordered_set &updated_properties) { + if(options.get_bool_option("symex-driven-lazy-loading")) + update_properties_from_goto_model(properties, goto_model); + update_properties_status_from_symex_target_equation( properties, updated_properties, equation); // Since we will not symex any further we can decide the status diff --git a/src/goto-checker/properties.cpp b/src/goto-checker/properties.cpp index c88a2f91846..1e4f8d2847b 100644 --- a/src/goto-checker/properties.cpp +++ b/src/goto-checker/properties.cpp @@ -63,10 +63,17 @@ property_infot::property_infot( { } -/// Return the properties in the goto model and initialize them to NOT_CHECKED propertiest initialize_properties(const abstract_goto_modelt &goto_model) { propertiest properties; + update_properties_from_goto_model(properties, goto_model); + return properties; +} + +void update_properties_from_goto_model( + propertiest &properties, + const abstract_goto_modelt &goto_model) +{ const auto &goto_functions = goto_model.get_goto_functions(); for(const auto &function_pair : goto_functions.function_map) { @@ -86,7 +93,6 @@ propertiest initialize_properties(const abstract_goto_modelt &goto_model) property_infot{i_it, description, property_statust::NOT_CHECKED}); } } - return properties; } std::string diff --git a/src/goto-checker/properties.h b/src/goto-checker/properties.h index a4ee9cf7303..68a22341ca9 100644 --- a/src/goto-checker/properties.h +++ b/src/goto-checker/properties.h @@ -77,6 +77,11 @@ typedef std::unordered_map propertiest; /// Returns the properties in the goto model propertiest initialize_properties(const abstract_goto_modelt &); +/// Updates \p properties with the assertions in \p goto_model +void update_properties_from_goto_model( + propertiest &properties, + const abstract_goto_modelt &goto_model); + std::string as_string(const irep_idt &property_id, const property_infot &property_info); diff --git a/src/goto-checker/single_path_symex_only_checker.cpp b/src/goto-checker/single_path_symex_only_checker.cpp index 4489ff8a05b..5668691c426 100644 --- a/src/goto-checker/single_path_symex_only_checker.cpp +++ b/src/goto-checker/single_path_symex_only_checker.cpp @@ -143,6 +143,9 @@ void single_path_symex_only_checkert::update_properties( std::unordered_set &updated_properties, const symex_target_equationt &equation) { + if(options.get_bool_option("symex-driven-lazy-loading")) + update_properties_from_goto_model(properties, goto_model); + update_properties_status_from_symex_target_equation( properties, updated_properties, equation); } diff --git a/src/goto-symex/README.md b/src/goto-symex/README.md index d9f63ec3a78..cc7789db74b 100644 --- a/src/goto-symex/README.md +++ b/src/goto-symex/README.md @@ -47,11 +47,11 @@ digraph G { \subsection symex-overview Overview -The \ref bmct class gets a reference to an \ref symex_target_equationt +The \ref goto_symext class gets a reference to a \ref symex_target_equationt "equation" (initially, an empty list of \ref SSA_stept "single-static assignment steps") and a goto-program from the frontend. -The \ref bmct creates a goto_symext to symbolically execute the -goto-program, thereby filling the equation, which can then be passed +\ref multi_path_symex_checkert then calls goto_symext to symbolically execute +the goto-program, thereby filling the equation, which can then be passed along to the SAT solver. The class \ref goto_symext holds the global state of the symbol executor, while @@ -131,12 +131,11 @@ representing that path, then continues to execute other paths. The 'other paths' that would have been taken when the program branches are saved onto a workqueue so that the driver program can continue to execute the current path, and then later retrieve saved paths from the workqueue. -Implementation-wise, \ref bmct passes a worklist to goto_symext in -\ref bmct::do_language_agnostic_bmc. If path exploration is enabled, -goto_symext will fill up the worklist whenever it encounters a branch, -instead of merging the paths on the branch. After the initial symbolic -execution (i.e. the first call to \ref bmct::run in -\ref bmct::do_language_agnostic_bmc), \ref bmct continues popping the +Implementation-wise, \ref single_path_symex_checkert maintains a worklist +and passes it to goto_symext. If path exploration is enabled, goto_symext will +fill up the worklist whenever it encounters a branch, instead of merging the +paths on the branch. The worklist is initialized with the initial state at the +entry point. Then \ref single_path_symex_checkert continues popping the worklist and executing untaken paths until the worklist empties. Note that this means that the default model-checking behaviour is a special case of path exploration: when model-checking, the initial symbolic @@ -261,7 +260,6 @@ In the \ref goto-symex directory. **Key classes:** * \ref symex_target_equationt * \ref prop_convt -* \ref bmct * \ref counterexample_beautificationt \dot diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index c48145e94d5..f0d337b1e64 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -631,8 +631,8 @@ class goto_symext /// The actual number of total and remaining VCCs should be assigned to /// the relevant members of goto_symex_statet. The members below are used to /// cache the values from goto_symex_statet after symbolic execution has - /// ended, so that \ref bmct can read those values even after the state has - /// been deallocated. + /// ended, so that the user of \ref goto_symext can read those values even + /// after the state has been deallocated. unsigned _total_vccs, _remaining_vccs; ///@} diff --git a/src/solvers/README.md b/src/solvers/README.md index 1909f3e9c3b..fe6bebb4454 100644 --- a/src/solvers/README.md +++ b/src/solvers/README.md @@ -297,7 +297,6 @@ In the \ref solvers directory. **Key classes:** * symex_target_equationt * \ref propt -* \ref bmct \dot digraph G {