57 symex_target_equationt::SSA_stepst::const_iterator step,
59 return step->is_assert() && step->property_id == property_id &&
60 decision_procedure.get(step->cond_handle).is_false();
71 switch(ui_message_handler.
get_ui())
86 msg.
result() << xml_result;
100 convert<json_stream_arrayt>(ns, goto_trace, json_trace, trace_options);
112 const std::string graphml = options.
get_option(
"graphml-witness");
117 graphml_witness(goto_trace);
123 std::ofstream out(graphml);
134 const std::string graphml = options.
get_option(
"graphml-witness");
139 graphml_witness(symex_target_equation);
145 std::ofstream out(graphml);
158 equation.
convert(decision_procedure);
161 std::unique_ptr<memory_model_baset>
164 const std::string mm = options.
get_option(
"mm");
166 if(mm.empty() || mm ==
"sc")
167 return std::make_unique<memory_model_sct>(ns);
169 return std::make_unique<memory_model_tsot>(ns);
171 return std::make_unique<memory_model_psot>(ns);
174 throw "invalid memory model '" + mm +
"': use one of sc, tso, pso";
217 ::slice(symex_target_equation);
240 std::unordered_set<irep_idt> &updated_properties,
243 for(
const auto &step : equation.
SSA_steps)
245 if(!step.is_assert())
248 const irep_idt &property_id = step.property_id;
255 auto emplace_result = properties.emplace(
258 if(emplace_result.second)
260 updated_properties.insert(property_id);
266 property_info.
status |= status;
268 if(property_info.
status != old_status)
269 updated_properties.insert(property_id);
276 std::unordered_set<irep_idt> &updated_properties)
278 for(
auto &property_pair : properties)
285 updated_properties.insert(property_pair.first);
292 std::unordered_set<irep_idt> &updated_properties)
294 for(
auto &property_pair : properties)
301 updated_properties.insert(property_pair.first);
307 const std::string &cov_out,
317 log.error() <<
"Failed to write symex coverage report to '" << cov_out
329 const auto postprocess_equation_start = std::chrono::steady_clock::now();
333 std::unique_ptr<memory_model_baset> memory_model =
335 (*memory_model)(equation, ui_message_handler);
339 log.statistics() <<
"size of program expression: "
342 slice(symex, equation, ns, options, ui_message_handler);
349 const auto postprocess_equation_stop = std::chrono::steady_clock::now();
350 std::chrono::duration<double> postprocess_equation_runtime =
351 std::chrono::duration<double>(
352 postprocess_equation_stop - postprocess_equation_start);
353 log.statistics() <<
"Runtime Postprocess Equation: "
354 << postprocess_equation_runtime.count() <<
"s"
364 auto solver_start = std::chrono::steady_clock::now();
368 <<
"Passing problem to "
378 auto solver_stop = std::chrono::steady_clock::now();
379 return std::chrono::duration<double>(solver_stop - solver_start);
387 std::chrono::duration<double> solver_runtime,
390 auto solver_start = std::chrono::steady_clock::now();
399 [&properties](
const irep_idt &property_id) {
403 auto const sat_solver_start = std::chrono::steady_clock::now();
407 auto const sat_solver_stop = std::chrono::steady_clock::now();
408 std::chrono::duration<double> sat_solver_runtime =
409 std::chrono::duration<double>(sat_solver_stop - sat_solver_start);
410 log.statistics() <<
"Runtime Solver: " << sat_solver_runtime.count() <<
"s"
416 auto solver_stop = std::chrono::steady_clock::now();
417 solver_runtime += std::chrono::duration<double>(solver_stop - solver_start);
418 log.statistics() <<
"Runtime decision procedure: " << solver_runtime.count()
void run_property_decider(incremental_goto_checkert::resultt &result, propertiest &properties, goto_symex_property_decidert &property_decider, ui_message_handlert &ui_message_handler, std::chrono::duration< double > solver_runtime, bool set_pass)
Runs the property decider to solve the equation.
std::chrono::duration< double > prepare_property_decider(propertiest &properties, symex_target_equationt &equation, goto_symex_property_decidert &property_decider, ui_message_handlert &ui_message_handler)
Converts the equation and sets up the property decider, but does not call solve.
void slice(symex_bmct &symex, symex_target_equationt &symex_target_equation, const namespacet &ns, const optionst &options, ui_message_handlert &ui_message_handler)
void output_coverage_report(const std::string &cov_out, const abstract_goto_modelt &goto_model, const symex_bmct &symex, ui_message_handlert &ui_message_handler)
Output a coverage report as generated by symex_coveraget if cov_out is non-empty.
std::unique_ptr< memory_model_baset > get_memory_model(const optionst &options, const namespacet &ns)
void output_error_trace(const goto_tracet &goto_trace, const namespacet &ns, const trace_optionst &trace_options, ui_message_handlert &ui_message_handler)
void update_status_of_unknown_properties(propertiest &properties, std::unordered_set< irep_idt > &updated_properties)
Sets the property status of UNKNOWN properties to PASS.
void message_building_error_trace(messaget &log)
Outputs a message that an error trace is being built.
void update_properties_status_from_symex_target_equation(propertiest &properties, std::unordered_set< irep_idt > &updated_properties, const symex_target_equationt &equation)
Sets property status to PASS for properties whose conditions are constant true in the equation.
void update_status_of_not_checked_properties(propertiest &properties, std::unordered_set< irep_idt > &updated_properties)
Sets the property status of NOT_CHECKED properties to PASS.
ssa_step_predicatet ssa_step_matches_failing_property(const irep_idt &property_id)
Returns a function that checks whether an SSA step is an assertion with property_id.
void build_error_trace(goto_tracet &goto_trace, const namespacet &ns, const symex_target_equationt &symex_target_equation, const decision_proceduret &decision_procedure, ui_message_handlert &ui_message_handler)
void convert_symex_target_equation(symex_target_equationt &equation, decision_proceduret &decision_procedure, message_handlert &message_handler)
void output_graphml(const goto_tracet &goto_trace, const namespacet &ns, const optionst &options)
outputs an error witness in graphml format
void postprocess_equation(symex_bmct &symex, symex_target_equationt &equation, const optionst &options, const namespacet &ns, ui_message_handlert &ui_message_handler)
Post process the equation.
void setup_symex(symex_bmct &symex, const namespacet &ns, const optionst &options, ui_message_handlert &ui_message_handler)
Bounded Model Checking Utilities.
void build_goto_trace(const symex_target_equationt &target, ssa_step_predicatet is_last_step_to_keep, const decision_proceduret &decision_procedure, const namespacet &ns, goto_tracet &goto_trace)
Build a trace by going through the steps of target and stopping after the step matching a given condi...
std::function< bool(symex_target_equationt::SSA_stepst::const_iterator, const decision_proceduret &)> ssa_step_predicatet
static bool convert(const irep_idt &identifier, const std::ostringstream &s, symbol_table_baset &symbol_table, message_handlert &message_handler)
Abstract interface to eager or lazy GOTO models.
virtual const goto_functionst & get_goto_functions() const =0
Accessor to get a raw goto_functionst.
An interface for a decision procedure for satisfiability problems.
resultt
Result of running the decision procedure.
virtual std::string decision_procedure_text() const =0
Return a textual description of the decision procedure.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Provides management of goal variables that encode properties.
stack_decision_proceduret & get_decision_procedure() const
Returns the solver instance.
decision_proceduret::resultt solve()
Calls solve() on the solver instance.
void update_properties_goals_from_symex_target_equation(propertiest &properties)
Get the conditions for the properties from the equation and collect all 'instances' of the properties...
void update_properties_status_from_goals(propertiest &properties, std::unordered_set< irep_idt > &updated_properties, decision_proceduret::resultt dec_result, bool set_pass=true) const
Update the property status from the truth value of the goal variable.
void add_constraint_from_goals(std::function< bool(const irep_idt &property_id)> select_property)
Add disjunction of negated selected properties to the equation.
void convert_goals()
Convert the instances of a property into a goal variable.
irep_idt language_mode
language_mode: ID_java, ID_C or another language identifier if we know the source language in use,...
unsigned get_remaining_vccs() const
unsigned get_total_vccs() const
void validate(const validation_modet vm) const
Step of the trace of a GOTO program.
goto_programt::const_targett pc
goto_trace_stept & get_last_step()
Retrieves the final step in the trace for manipulation (used to fill a trace from code,...
Provides methods for streaming JSON arrays.
json_stream_objectt & push_back_stream_object()
Add a JSON object child stream.
Provides methods for streaming JSON objects.
json_stream_arrayt & push_back_stream_array(const std::string &key)
Add a JSON array stream for a specific key.
Class that provides messages with a built-in verbosity 'level'.
mstreamt & statistics() const
mstreamt & status() const
mstreamt & result() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
bool get_bool_option(const std::string &option) const
const std::string get_option(const std::string &option) const
const value_listt & get_list_option(const std::string &option) const
source_locationt last_source_location
bool output_coverage_report(const goto_functionst &goto_functions, const std::string &path) const
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
std::size_t count_ignored_SSA_steps() const
void convert(decision_proceduret &decision_procedure)
Interface method to initiate the conversion into a decision procedure format.
virtual uit get_ui() const
virtual json_stream_arrayt & get_json_stream()
void parse_unwind(const std::string &unwind)
void parse_unwindset(const std::list< std::string > &unwindset, message_handlert &message_handler)
xmlt & new_element(const std::string &key)
Decision Procedure Interface.
Property Decider for Goto-Symex.
void show_goto_trace(messaget::mstreamt &out, const namespacet &ns, const goto_tracet &goto_trace, const trace_optionst &options)
Output the trace on the given stream out.
bool write_graphml(const graphmlt &src, std::ostream &os)
Witnesses for Traces and Proofs.
static std::unordered_set< irep_idt > init_symbol(const symbolt &sym, code_blockt &code_block, symbol_table_baset &symbol_table, const source_locationt &source_location, bool assume_init_pointers_not_null, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, bool string_refinement_enabled, message_handlert &message_handler)
Memory models for partial order concurrency.
bool is_property_to_check(property_statust status)
Return true if the status is NOT_CHECKED or UNKNOWN.
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
property_statust
The status of a property.
@ UNKNOWN
The checker was unable to determine the status of the property.
@ PASS
The property was not violated.
@ FAIL
The property was violated.
@ NOT_CHECKED
The property was not checked (also used for initialization)
std::map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
void simple_slice(symex_target_equationt &equation)
#define CHECK_RETURN(CONDITION)
#define INITIALIZE_FUNCTION
std::unordered_set< irep_idt > updated_properties
Changed properties since the last call to incremental_goto_checkert::operator()
@ FOUND_FAIL
The goto checker may be able to find another FAILed property if operator() is called again.
property_statust status
The status of the property.
goto_programt::const_targett pc
A pointer to the corresponding goto instruction.
Options for printing the trace using show_goto_trace.
Bounded Model Checking for ANSI-C.
Generate Equation using Symbolic Execution.