49 status() <<
"Building error trace" <<
eom;
75 json_result[
"property"] =
77 json_result[
"description"] =
81 json_result.push_back_stream_array(
"trace");
82 convert<json_stream_arrayt>(
ns, goto_trace, json_trace,
trace_options());
107 std::ofstream out(graphml);
126 status() <<
"Passing problem to " 131 auto solver_start = std::chrono::steady_clock::now();
140 auto solver_stop = std::chrono::steady_clock::now();
141 status() <<
"Runtime decision procedure: " 142 << std::chrono::duration<double>(solver_stop-solver_start).count()
151 result() <<
"VERIFICATION SUCCESSFUL" <<
eom;
178 result() <<
"VERIFICATION FAILED" <<
eom;
207 std::cout <<
"\n" <<
"Program constraints:" <<
"\n";
211 std::cout <<
"// " << step.source.pc->location_number <<
" ";
212 std::cout << step.source.pc->source_location.as_string() <<
"\n";
213 const irep_idt &
function = step.source.pc->function;
215 if(step.is_assignment())
217 std::string string_value =
from_expr(
ns,
function, step.cond_expr);
218 std::cout <<
"(" << count <<
") " << string_value <<
"\n";
220 if(!step.guard.is_true())
222 std::string string_value =
from_expr(
ns,
function, step.guard);
224 std::cout <<
"guard: " << string_value <<
"\n";
229 else if(step.is_assert())
231 std::string string_value =
from_expr(
ns,
function, step.cond_expr);
232 std::cout <<
"(" << count <<
") ASSERT(" 233 << string_value <<
") " <<
"\n";
235 if(!step.guard.is_true())
237 std::string string_value =
from_expr(
ns,
function, step.guard);
239 std::cout <<
"guard: " << string_value <<
"\n";
244 else if(step.is_assume())
246 std::string string_value =
from_expr(
ns,
function, step.cond_expr);
247 std::cout <<
"(" << count <<
") ASSUME(" 248 << string_value <<
") " <<
"\n";
250 if(!step.guard.is_true())
252 std::string string_value =
from_expr(
ns,
function, step.guard);
254 std::cout <<
"guard: " << string_value <<
"\n";
259 else if(step.is_constraint())
261 std::string string_value =
from_expr(
ns,
function, step.cond_expr);
262 std::cout <<
"(" << count <<
") CONSTRAINT(" 263 << string_value <<
") " <<
"\n";
267 else if(step.is_shared_read() || step.is_shared_write())
269 std::string string_value =
from_expr(
ns,
function, step.ssa_lhs);
270 std::cout <<
"(" << count <<
") SHARED_" 271 << (step.is_shared_write()?
"WRITE":
"READ")
272 <<
"(" << string_value <<
")\n";
274 if(!step.guard.is_true())
276 std::string string_value =
from_expr(
ns,
function, step.guard);
278 std::cout <<
"guard: " << string_value <<
"\n";
291 if(mm.empty() || mm==
"sc")
299 error() <<
"Invalid memory model " << mm
300 <<
" -- use one of sc, tso, pso" <<
eom;
301 throw "invalid memory model";
315 status() <<
"Starting Bounded Model Checking" <<
eom;
328 auto get_goto_function = [&goto_model](
const irep_idt &id) ->
362 statistics() <<
"size of program expression: " 370 if(!cov_out.empty() &&
373 error() <<
"Failed to write symex coverage report" <<
eom;
385 return cover(goto_functions)?
392 goto_functions, *
this,
options);
393 return fault_localization();
414 catch(
const std::string &error_str)
423 catch(
const char *error_str)
432 catch(
const std::bad_alloc &)
462 <<
" assignments"<<
eom;
471 <<
" assignments"<<
eom;
478 <<
" remaining after simplification" <<
eom;
542 error() <<
"decision procedure failed" <<
eom;
566 std::function<
bool(
void)> callback_after_symex)
572 std::unique_ptr<path_storaget> worklist;
573 std::string strategy = opts.
get_option(
"exploration-strategy");
576 "Front-end passed us invalid path strategy '" + strategy +
"'");
577 worklist = path_strategy_chooser.
get(strategy);
583 std::unique_ptr<cbmc_solverst::solvert> cbmc_solver;
584 cbmc_solver = solvers.get_solver();
586 bmct bmc(opts, symbol_table, mh, pc, *worklist, callback_after_symex);
588 if(driver_configure_bmc)
589 driver_configure_bmc(bmc, symbol_table);
590 tmp_result = bmc.
run(model);
601 final_result = tmp_result;
605 "the worklist should be empty after doing full-program " 606 "model checking, but the worklist contains " +
624 while(!worklist->empty())
627 message.
status() <<
"___________________________\n" 628 <<
"Starting new path (" << worklist->size()
633 std::unique_ptr<cbmc_solverst::solvert> cbmc_solver;
634 cbmc_solver = solvers.get_solver();
645 callback_after_symex);
646 if(driver_configure_bmc)
647 driver_configure_bmc(pe, symbol_table);
648 tmp_result = pe.
run(model);
659 final_result &= tmp_result;
663 catch(
const char *error_msg)
665 message.
error() << error_msg << message.
eom;
668 catch(
const std::string &error_msg)
670 message.
error() << error_msg << message.
eom;
673 catch(std::runtime_error &e)
675 message.
error() << e.what() << message.
eom;
701 "Branch points were saved even though we should have been " 702 "executing the entire program and merging paths");
void build_goto_trace(const symex_target_equationt &target, ssa_step_predicatet is_last_step_to_keep, const prop_convt &prop_conv, const namespacet &ns, goto_tracet &goto_trace)
virtual void perform_symbolic_execution(goto_symext::get_goto_functiont get_goto_function)
Class-specific symbolic execution.
void set_ui(ui_message_handlert::uit _ui)
bool cover(const goto_functionst &goto_functions)
Try to cover all goals.
Abstract interface to eager or lazy GOTO models.
void convert(prop_convt &prop_conv)
void simple_slice(symex_target_equationt &equation)
virtual resultt all_properties(const goto_functionst &goto_functions, prop_convt &solver)
irep_idt mode
Language mode.
void set_ui(ui_message_handlert::uit _ui)
Provides methods for streaming JSON objects.
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Slicer for matching with trace files.
json_stream_objectt & push_back_stream_object()
Add a JSON object child stream.
path_storaget & path_storage
virtual void report_failure()
prop_convt & prop_conv() const
We haven't yet assigned a safety check result to this object.
virtual const goto_functionst & get_goto_functions() const =0
Accessor to get a raw goto_functionst.
const value_listt & get_list_option(const std::string &option) const
Memory models for partial order concurrency.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
std::function< const goto_functionst::goto_functiont &(const irep_idt &)> get_goto_functiont
static mstreamt & eom(mstreamt &m)
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
xmlt xml(const source_locationt &location)
goto_programt::const_targett pc
symex_target_equationt equation
virtual resultt decide(const goto_functionst &, prop_convt &)
#define INVARIANT(CONDITION, REASON)
virtual const goto_functionst::goto_functiont & get_goto_function(const irep_idt &id)=0
Get a GOTO function by name, or throw if no such function exists.
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, messaget &message, std::function< void(bmct &, const symbol_tablet &)> driver_configure_bmc=nullptr, std::function< bool(void)> callback_after_symex=nullptr)
Perform core BMC, using an abstract model to supply GOTO function bodies (perhaps created on demand)...
Factory and information for path_storaget.
const goto_symex_statet & saved_state
virtual void error_trace()
virtual void symex_from_entry_point_of(const goto_functionst &goto_functions, symbol_tablet &new_symbol_table)
symex entire program starting from entry point
virtual resultt dec_solve()=0
Some safety properties were violated.
ui_message_handlert::uit ui
bool output_coverage_report(const goto_functionst &goto_functions, const std::string &path) const
void perform_symbolic_execution(goto_symext::get_goto_functiont get_goto_function) override
Resume symbolic execution from saved branch point.
source_locationt source_location
const std::string get_option(const std::string &option) const
Safety is unknown due to an error during safety checking.
virtual void resume_symex_from_saved_state(const get_goto_functiont &get_goto_function, const statet &saved_state, symex_target_equationt *const saved_equation, symbol_tablet &new_symbol_table)
Performs symbolic execution using a state and equation that have already been used to symex part of t...
#define INITIALIZE_FUNCTION
bool is_valid_strategy(const std::string strategy) const
is there a factory constructor for the named strategy?
bool get_bool_option(const std::string &option) const
Provides methods for streaming JSON arrays.
::goto_functiont goto_functiont
virtual const symbol_tablet & get_symbol_table() const =0
Accessor to get the symbol table.
Symbolic execution from a saved branch point.
static bool convert(const irep_idt &identifier, const std::ostringstream &s, symbol_tablet &symbol_table, message_handlert &message_handler)
virtual void set_message_handler(message_handlert &_message_handler)
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
No safety properties were violated.
virtual decision_proceduret::resultt run_decision_procedure(prop_convt &prop_conv)
void parse_unwindset(const std::string &unwindset)
#define CPROVER_EXIT_EXCEPTION
An (unanticipated) exception was thrown during computation.
std::unique_ptr< path_storaget > get(const std::string strategy) const
Factory for a path_storaget.
message_handlert & get_message_handler()
Bounded Model Checking for ANSI-C + HDL.
Document and give macros for the exit codes of CPROVER binaries.
mstreamt & result() const
mstreamt & status() const
irep_idt language_mode
language_mode: ID_java, ID_C or another language identifier if we know the source language in use...
safety_checkert::resultt execute(abstract_goto_modelt &)
bool should_pause_symex
Have states been pushed onto the workqueue?
void slice_by_trace(std::string trace_files, symex_target_equationt &equation)
Symbolic execution has been suspended due to encountering a GOTO while doing path exploration; the sy...
#define CPROVER_EXIT_VERIFICATION_UNSAFE
Verification successful indiciates the analysis has been performed without error AND the software is ...
virtual resultt run(const goto_functionst &goto_functions)
bool write_graphml(const graphmlt &src, std::ostream &os)
virtual void show_program()
virtual resultt stop_on_fail(prop_convt &solver)
std::string to_string(const string_constraintt &expr)
Used for debug printing.
symbol_tablet symex_symbol_table
symbol table generated during symbolic execution
Information saved at a conditional goto to resume execution.
bool empty() const
Is this storage empty?
void show_goto_trace(std::ostream &out, const namespacet &ns, const goto_tracet &goto_trace, const trace_optionst &options)
Bounded model checking or path exploration for goto-programs.
Bounded Model Checking for ANSI-C + HDL.
std::unique_ptr< memory_model_baset > memory_model
symex_target_equationt equation
std::size_t count_ignored_SSA_steps() const
#define CPROVER_EXIT_VERIFICATION_SAFE
Verification successful indiciates the analysis has been performed without error AND the software is ...
std::function< bool(void)> driver_callback_after_symex
Optional callback, to be run after symex but before handing the resulting equation to the solver...
virtual void report_success()
source_locationt last_source_location
void parse_unwind(const std::string &unwind)
trace_optionst trace_options()
json_stream_arrayt & json_stream()
Returns a reference to the top-level JSON array stream.
virtual void freeze_program_variables()
Hook used by CEGIS to selectively freeze variables in the SAT solver after the SSA formula is added t...
mstreamt & statistics() const
bool is_set(const std::string &option) const
N.B. opts.is_set("foo") does not imply opts.get_bool_option("foo")
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
void output_graphml(resultt result)
outputs witnesses in graphml format
Witnesses for Traces and Proofs.
Counterexample Beautification.
virtual std::string decision_procedure_text() const =0