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
17
18#include <goto-symex/slice.h>
19
20#include "bmc_util.h"
22
24 const optionst &options,
25 ui_message_handlert &ui_message_handler,
26 abstract_goto_modelt &goto_model)
27 : incremental_goto_checkert(options, ui_message_handler),
28 goto_model(goto_model),
29 ns(goto_model.get_symbol_table(), symex_symbol_table),
30 equation(ui_message_handler),
31 unwindset(goto_model),
32 symex(
33 ui_message_handler,
34 goto_model.get_symbol_table(),
35 equation,
36 options,
37 path_storage,
38 guard_manager,
39 unwindset,
40 ui_message_handler.get_ui()),
41 property_decider(options, ui_message_handler, equation, ns)
42{
44
45 // Freeze all symbols if we are using a prop_conv_solvert
46 prop_conv_solvert *prop_conv_solver = dynamic_cast<prop_conv_solvert *>(
48 if(prop_conv_solver != nullptr)
49 prop_conv_solver->set_all_frozen();
50}
51
53 const propertiest &properties,
54 messaget &message_hander)
55{
56 const auto any_failures = std::any_of(
57 properties.begin(),
58 properties.end(),
59 [](const std::pair<irep_idt, property_infot> &property) {
60 return property.second.status == property_statust::FAIL;
61 });
62 std::string status = any_failures ? "FAILURE" : "INCONCLUSIVE";
63 structured_datat incremental_status{
64 {{labelt({"incremental", "status"}),
66 message_hander.statistics() << incremental_status;
67}
68
70operator()(propertiest &properties)
71{
72 resultt result(resultt::progresst::DONE);
73
74 std::chrono::duration<double> solver_runtime(0);
75
76 // we haven't got an equation yet
78 {
81
82 // This might add new properties such as unwinding assertions, for instance.
84 properties, result.updated_properties, equation);
85
87 }
88
89 while(has_properties_to_check(properties))
90 {
91 // There are NOT_CHECKED or UNKNOWN properties.
92
94 {
95 // We have UNKNOWN properties, i.e. properties that we can check
96 // on the current equation.
97
98 log.status()
99 << "Passing problem to "
101 << messaget::eom;
102
103 const auto solver_start = std::chrono::steady_clock::now();
104
106 {
108
109 log.status() << "converting SSA" << messaget::eom;
112
114 properties);
115
116 // We convert the assertions in a new context.
121
123 }
124
126 [&properties](const irep_idt &property_id) {
127 return is_property_to_check(properties.at(property_id).status);
128 });
129
130 log.status()
131 << "Running "
133 << messaget::eom;
134
136
138 properties, result.updated_properties, dec_result, false);
139
140 const auto solver_stop = std::chrono::steady_clock::now();
141 solver_runtime +=
142 std::chrono::duration<double>(solver_stop - solver_start);
143 log.status() << "Runtime decision procedure: " << solver_runtime.count()
144 << "s" << messaget::eom;
145
146 result.progress =
148 ? resultt::progresst::FOUND_FAIL
149 : resultt::progresst::DONE;
150
151 // We've got a trace to report.
152 if(result.progress == resultt::progresst::FOUND_FAIL)
153 break;
154
155 // Nothing else to do with the current set of assertions.
156 // Let's pop them.
158 }
159
160 // Now we are finally done.
162 {
163 // For now, we assume that UNKNOWN properties are PASS.
165 properties, result.updated_properties);
166
167 // For now, we assume that NOT_REACHED properties are PASS.
169 properties, result.updated_properties);
170
171 break;
172 }
173
174 output_incremental_status(properties, log);
175
176 // We continue symbolic execution
180
181 // This might add new properties such as unwinding assertions, for instance.
183 properties, result.updated_properties, equation);
184
186 }
187
188 return result;
189}
190
192{
193 goto_tracet goto_trace;
195 equation,
196 equation.SSA_steps.end(),
198 ns,
199 goto_trace);
200
201 return goto_trace;
202}
203
205{
206 if(options.get_bool_option("beautify"))
207 {
208 // NOLINTNEXTLINE(whitespace/braces)
211 equation);
212 }
213
214 goto_tracet goto_trace;
217
218 return goto_trace;
219}
220
222 const irep_idt &property_id) const
223{
224 goto_tracet goto_trace;
226 equation,
229 ns,
230 goto_trace);
231
232 return goto_trace;
233}
234
239
244
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:39
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:177
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)