cprover
Loading...
Searching...
No Matches
single_loop_incremental_symex_checker.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Goto Checker using Multi-Path Symbolic Execution
4 with Incremental Unwinding of a specified Loop
5
6Author: Daniel Kroening, Peter Schrammel
7
8\*******************************************************************/
9
13
15
16#include <chrono>
17
19
20#include <goto-symex/slice.h>
21
22#include "bmc_util.h"
24
26 const optionst &options,
27 ui_message_handlert &ui_message_handler,
28 abstract_goto_modelt &goto_model)
29 : incremental_goto_checkert(options, ui_message_handler),
30 goto_model(goto_model),
31 ns(goto_model.get_symbol_table(), symex_symbol_table),
32 equation(ui_message_handler),
33 unwindset(goto_model),
34 symex(
35 ui_message_handler,
36 goto_model.get_symbol_table(),
37 equation,
38 options,
39 path_storage,
40 guard_manager,
41 unwindset,
42 ui_message_handler.get_ui()),
43 property_decider(options, ui_message_handler, equation, ns)
44{
46
47 // Freeze all symbols if we are using a prop_conv_solvert
48 prop_conv_solvert *prop_conv_solver = dynamic_cast<prop_conv_solvert *>(
50 if(prop_conv_solver != nullptr)
51 prop_conv_solver->set_all_frozen();
52}
53
55 const propertiest &properties,
56 messaget &message_hander)
57{
58 const auto any_failures = std::any_of(
59 properties.begin(),
60 properties.end(),
61 [](const std::pair<irep_idt, property_infot> &property) {
62 return property.second.status == property_statust::FAIL;
63 });
64 std::string status = any_failures ? "FAILURE" : "INCONCLUSIVE";
65 structured_datat incremental_status{
66 {{labelt({"incremental", "status"}),
68 message_hander.statistics() << incremental_status;
69}
70
72operator()(propertiest &properties)
73{
74 resultt result(resultt::progresst::DONE);
75
76 std::chrono::duration<double> solver_runtime(0);
77
78 // we haven't got an equation yet
80 {
83
84 // This might add new properties such as unwinding assertions, for instance.
86 properties, result.updated_properties, equation);
87
89 }
90
91 while(has_properties_to_check(properties))
92 {
93 // There are NOT_CHECKED or UNKNOWN properties.
94
96 {
97 // We have UNKNOWN properties, i.e. properties that we can check
98 // on the current equation.
99
100 log.status()
101 << "Passing problem to "
103 << messaget::eom;
104
105 const auto solver_start = std::chrono::steady_clock::now();
106
108 {
110
111 log.status() << "converting SSA" << messaget::eom;
114
116 properties);
117
118 // We convert the assertions in a new context.
123
125 }
126
128 [&properties](const irep_idt &property_id) {
129 return is_property_to_check(properties.at(property_id).status);
130 });
131
132 log.status()
133 << "Running "
135 << messaget::eom;
136
138
140 properties, result.updated_properties, dec_result, false);
141
142 const auto solver_stop = std::chrono::steady_clock::now();
143 solver_runtime +=
144 std::chrono::duration<double>(solver_stop - solver_start);
145 log.status() << "Runtime decision procedure: " << solver_runtime.count()
146 << "s" << messaget::eom;
147
148 result.progress =
150 ? resultt::progresst::FOUND_FAIL
151 : resultt::progresst::DONE;
152
153 // We've got a trace to report.
154 if(result.progress == resultt::progresst::FOUND_FAIL)
155 break;
156
157 // Nothing else to do with the current set of assertions.
158 // Let's pop them.
160 }
161
162 // Now we are finally done.
164 {
165 // For now, we assume that UNKNOWN properties are PASS.
167 properties, result.updated_properties);
168
169 // For now, we assume that NOT_REACHED properties are PASS.
171 properties, result.updated_properties);
172
173 break;
174 }
175
176 output_incremental_status(properties, log);
177
178 // We continue symbolic execution
182
183 // This might add new properties such as unwinding assertions, for instance.
185 properties, result.updated_properties, equation);
186
188 }
189
190 return result;
191}
192
194{
195 goto_tracet goto_trace;
197 equation,
198 equation.SSA_steps.end(),
200 ns,
201 goto_trace);
202
203 return goto_trace;
204}
205
207{
208 if(options.get_bool_option("beautify"))
209 {
210 // NOLINTNEXTLINE(whitespace/braces)
213 equation);
214 }
215
216 goto_tracet goto_trace;
219
220 return goto_trace;
221}
222
224 const irep_idt &property_id) const
225{
226 goto_tracet goto_trace;
228 equation,
231 ns,
232 goto_trace);
233
234 return goto_trace;
235}
236
238{
239 return ns;
240}
241
243{
245}
246
248 const goto_tracet &error_trace)
249{
250 output_graphml(error_trace, ns, options);
251}
void update_status_of_unknown_properties(propertiest &properties, std::unordered_set< irep_idt > &updated_properties)
Sets the property status of UNKNOWN properties to PASS.
Definition bmc_util.cpp:291
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.
Definition bmc_util.cpp:239
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.
Definition bmc_util.cpp:275
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
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.
Definition bmc_util.cpp:323
void setup_symex(symex_bmct &symex, const namespacet &ns, const optionst &options, ui_message_handlert &ui_message_handler)
Definition bmc_util.cpp:179
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.
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.
Definition dstring.h:37
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.
stack_decision_proceduret & get_stack_decision_procedure() const
Returns the solver instance.
static get_goto_functiont get_goto_function(abstract_goto_modelt &goto_model)
Return a function to get/load a goto function from the given goto model Create a default delegate to ...
Trace of a GOTO program.
Definition goto_trace.h:175
An implementation of incremental_goto_checkert provides functionality for checking a set of propertie...
ui_message_handlert & ui_message_handler
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
mstreamt & statistics() const
Definition message.h:419
static eomt eom
Definition message.h:297
mstreamt & status() const
Definition message.h:414
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool get_bool_option(const std::string &option) const
Definition options.cpp:44
goto_tracet build_trace(const irep_idt &) const override
Builds and returns the trace for the FAILed property with the given property_id.
goto_tracet build_shortest_trace() const override
Builds and returns the trace up to the first failed property.
resultt operator()(propertiest &) override
Check whether the given properties with status NOT_CHECKED, UNKNOWN or properties newly discovered by...
single_loop_incremental_symex_checkert(const optionst &options, ui_message_handlert &ui_message_handler, abstract_goto_modelt &goto_model)
goto_tracet build_full_trace() const override
Builds and returns the complete trace.
const namespacet & get_namespace() const override
Returns the namespace associated with the traces.
virtual void pop()=0
Pop whatever is on top of the stack.
virtual void push(const std::vector< exprt > &assumptions)=0
Pushes a new context on the stack that consists of the given (possibly empty vector of) assumptions.
A way of representing nested key/value data.
bool resume(const get_goto_functiont &get_goto_function)
Return true if symex can be resumed.
bool from_entry_point_of(const get_goto_functiont &get_goto_function, symbol_tablet &new_symbol_table)
Return true if symex can be resumed.
void convert_without_assertions(decision_proceduret &decision_procedure)
Interface method to initiate the conversion into a decision procedure format.
void convert_assertions(decision_proceduret &decision_procedure, bool optimized_for_single_assertions=true)
Converts assertions: build a disjunction of negated assertions.
Counterexample Beautification.
bool has_properties_to_check(const propertiest &properties)
Return true if there as a property with NOT_CHECKED or UNKNOWN status.
bool is_property_to_check(property_statust status)
Return true if the status is NOT_CHECKED or UNKNOWN.
std::size_t count_properties(const propertiest &properties, property_statust status)
Return the number of properties with given status.
@ UNKNOWN
The checker was unable to determine the status of the property.
std::map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
Definition properties.h:76
void output_incremental_status(const propertiest &properties, messaget &message_hander)
Goto Checker using multi-path symbolic execution with incremental unwinding of a specified loop.
void revert_slice(symex_target_equationt &equation)
Undo whatever has been done by slice
Definition slice.cpp:261
Slicer for symex traces.
std::unordered_set< irep_idt > updated_properties
Changed properties since the last call to incremental_goto_checkert::operator()
static structured_data_entryt data_node(const jsont &data)