cprover
single_loop_incremental_symex_checker.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Goto Checker using Multi-Path Symbolic Execution
4  with Incremental Unwinding of a specified Loop
5 
6 Author: Daniel Kroening, Peter Schrammel
7 
8 \*******************************************************************/
9 
13 
15 
16 #include <chrono>
17 
18 #include <util/structured_data.h>
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 
72 operator()(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 
95  if(count_properties(properties, property_statust::UNKNOWN) > 0)
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.
Definition: boolbv.h:44
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 ...
Definition: symex_main.cpp:493
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
mstreamt & status() const
Definition: message.h:414
static eomt eom
Definition: message.h:297
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.
Definition: properties.cpp:177
bool is_property_to_check(property_statust status)
Return true if the status is NOT_CHECKED or UNKNOWN.
Definition: properties.cpp:171
std::size_t count_properties(const propertiest &properties, property_statust status)
Return the number of properties with given status.
Definition: properties.cpp:160
@ 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)