cprover
multi_path_symex_checker.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Goto Checker using Bounded Model Checking
4
5Author: Daniel Kroening, Peter Schrammel
6
7\*******************************************************************/
8
11
13
14#include <chrono>
15
16#include <util/ui_message.h>
17
19
20#include "bmc_util.h"
23
25 const optionst &options,
26 ui_message_handlert &ui_message_handler,
27 abstract_goto_modelt &goto_model)
28 : multi_path_symex_only_checkert(options, ui_message_handler, goto_model),
29 equation_generated(false),
30 property_decider(options, ui_message_handler, equation, ns)
31{
32}
33
35operator()(propertiest &properties)
36{
37 resultt result(resultt::progresst::DONE);
38
39 // When the equation has been generated, we know all the properties.
40 // Have we got anything to check? Otherwise we return DONE.
42 return result;
43
44 std::chrono::duration<double> solver_runtime(0);
45
46 // we haven't got an equation yet
48 {
50
52 options.get_option("symex-coverage-report"),
54 symex,
56
57 update_properties(properties, result.updated_properties);
58
59 // Have we got anything to check? Otherwise we return DONE.
60 if(!has_properties_to_check(properties))
61 return result;
62
63 solver_runtime += prepare_property_decider(properties);
64
65 equation_generated = true;
66 }
67
68 run_property_decider(result, properties, solver_runtime);
69
70 return result;
71}
72
73std::chrono::duration<double>
75{
76 std::chrono::duration<double> solver_runtime = ::prepare_property_decider(
78
79 return solver_runtime;
80}
81
84 propertiest &properties,
85 std::chrono::duration<double> solver_runtime)
86{
88 result, properties, property_decider, ui_message_handler, solver_runtime);
89}
90
92{
93 goto_tracet goto_trace;
96 equation.SSA_steps.end(),
98 ns,
99 goto_trace);
100
101 return goto_trace;
102}
103
105{
106 if(options.get_bool_option("beautify"))
107 {
108 // NOLINTNEXTLINE(whitespace/braces)
111 equation);
112 }
113
114 goto_tracet goto_trace;
117
118 return goto_trace;
119}
120
123{
124 goto_tracet goto_trace;
126 equation,
129 ns,
130 goto_trace);
131
132 return goto_trace;
133}
134
136{
137 return ns;
138}
139
141{
143}
144
146 const goto_tracet &error_trace)
147{
148 output_graphml(error_trace, ns, options);
149}
150
153{
154 goto_symex_fault_localizert fault_localizer(
155 options,
157 equation,
159
160 return fault_localizer(property_id);
161}
162
164{
165 if(options.is_set("write-solver-stats-to"))
166 {
169 [](solver_hardnesst &hardness) { hardness.produce_report(); });
170 }
171}
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.
Definition: bmc_util.cpp:307
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.
Definition: bmc_util.cpp:55
void output_graphml(const goto_tracet &goto_trace, const namespacet &ns, const optionst &options)
outputs an error witness in graphml format
Definition: bmc_util.cpp:108
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...
Abstract interface to eager or lazy GOTO models.
Definition: boolbv.h:44
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
decision_proceduret & get_decision_procedure() const
Returns the solver instance.
stack_decision_proceduret & get_stack_decision_procedure() const
Returns the solver instance.
Trace of a GOTO program.
Definition: goto_trace.h:175
ui_message_handlert & ui_message_handler
void report() override
Additional reporting that may result from the underlying solver, no-op by default.
resultt operator()(propertiest &) override
Check whether the given properties with status NOT_CHECKED, UNKNOWN or properties newly discovered by...
goto_tracet build_full_trace() const override
Builds and returns the complete trace.
virtual void run_property_decider(incremental_goto_checkert::resultt &result, propertiest &properties, std::chrono::duration< double > solver_runtime)
Run the property decider, which calls the SAT solver, and set the status of checked properties accord...
fault_location_infot localize_fault(const irep_idt &property_id) const override
Returns the most likely fault locations for the given FAILed property_id.
goto_symex_property_decidert property_decider
virtual std::chrono::duration< double > prepare_property_decider(propertiest &properties)
Prepare the property decider for solving.
multi_path_symex_checkert(const optionst &options, ui_message_handlert &ui_message_handler, abstract_goto_modelt &goto_model)
void output_error_witness(const goto_tracet &) override
goto_tracet build_shortest_trace() const override
Builds and returns the trace up to the first failed property.
const namespacet & get_namespace() const override
Returns the namespace associated with the traces.
goto_tracet build_trace(const irep_idt &) const override
Builds and returns the trace for the FAILed property with the given property_id.
virtual void update_properties(propertiest &properties, std::unordered_set< irep_idt > &updated_properties)
Updates the properties from the equation and adds their property IDs to updated_properties.
virtual void generate_equation()
Generates the equation by running goto-symex.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool is_set(const std::string &option) const
N.B. opts.is_set("foo") does not imply opts.get_bool_option("foo")
Definition: options.cpp:62
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
const std::string get_option(const std::string &option) const
Definition: options.cpp:67
Counterexample Beautification.
Fault Localization for Goto Symex.
Goto Checker using Multi-Path Symbolic Execution.
bool has_properties_to_check(const propertiest &properties)
Return true if there as a property with NOT_CHECKED or UNKNOWN status.
Definition: properties.cpp:177
std::map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
Definition: properties.h:76
static void with_solver_hardness(decision_proceduret &maybe_hardness_collector, std::function< void(solver_hardnesst &hardness)> handler)
std::unordered_set< irep_idt > updated_properties
Changed properties since the last call to incremental_goto_checkert::operator()
A structure that facilitates collecting the complexity statistics from a decision procedure.