cprover
single_path_symex_checker.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Goto Checker using Single Path Symbolic Execution
4 
5 Author: Daniel Kroening, Peter Schrammel
6 
7 \*******************************************************************/
8 
11 
13 
14 #include "bmc_util.h"
16 #include "symex_bmc.h"
17 
19  const optionst &options,
20  ui_message_handlert &ui_message_handler,
21  abstract_goto_modelt &goto_model)
22  : single_path_symex_only_checkert(options, ui_message_handler, goto_model)
23 {
24 }
25 
27 operator()(propertiest &properties)
28 {
29  resultt result(resultt::progresst::DONE);
30 
31  // There might be more solutions from the previous equation.
33  {
35  result, properties, *property_decider, std::chrono::duration<double>(0));
36 
37  if(result.progress == resultt::progresst::FOUND_FAIL)
38  return result;
39  }
40 
41  if(!worklist->empty())
42  {
43  // We pop the item processed in the previous iteration.
44  worklist->pop();
45  }
46 
48  {
49  symex_initialized = true;
50 
52  }
53 
54  while(!has_finished_exploration(properties))
55  {
56  path_storaget::patht &path = worklist->peek();
57  const bool ready_to_decide = resume_path(path);
58 
59  if(ready_to_decide)
60  {
61  update_properties(properties, result.updated_properties, path.equation);
62 
63  property_decider = util_make_unique<goto_symex_property_decidert>(
65 
66  const auto solver_runtime =
68 
70  result, properties, *property_decider, solver_runtime);
71 
72  if(result.progress == resultt::progresst::FOUND_FAIL)
73  return result;
74  }
75 
76  worklist->pop();
77  }
78 
79  log.status() << "Runtime Symex: " << symex_runtime.count() << "s"
80  << messaget::eom;
81 
82  final_update_properties(properties, result.updated_properties);
83 
84  // Worklist is empty: we are done.
85  return result;
86 }
87 
89  const symex_bmct &symex,
90  const path_storaget::patht &)
91 {
92  return symex.get_remaining_vccs() > 0;
93 }
94 
95 std::chrono::duration<double>
97  propertiest &properties,
98  symex_target_equationt &equation,
99  goto_symex_property_decidert &property_decider)
100 {
101  std::chrono::duration<double> solver_runtime = ::prepare_property_decider(
102  properties, equation, property_decider, ui_message_handler);
103 
104  return solver_runtime;
105 }
106 
109  propertiest &properties,
110  goto_symex_property_decidert &property_decider,
111  std::chrono::duration<double> solver_runtime)
112 {
114  result,
115  properties,
118  solver_runtime,
119  false);
120 }
121 
123 {
124  goto_tracet goto_trace;
126  property_decider->get_equation(),
127  property_decider->get_equation().SSA_steps.end(),
128  property_decider->get_decision_procedure(),
129  ns,
130  goto_trace);
131 
132  return goto_trace;
133 }
134 
136 {
137  if(options.get_bool_option("beautify"))
138  {
139  // NOLINTNEXTLINE(whitespace/braces)
141  dynamic_cast<boolbvt &>(property_decider->get_stack_decision_procedure()),
142  property_decider->get_equation());
143  }
144 
145  goto_tracet goto_trace;
147  property_decider->get_equation(),
148  property_decider->get_decision_procedure(),
149  ns,
150  goto_trace);
151 
152  return goto_trace;
153 }
154 
157 {
158  goto_tracet goto_trace;
160  property_decider->get_equation(),
162  property_decider->get_decision_procedure(),
163  ns,
164  goto_trace);
165 
166  return goto_trace;
167 }
168 
170 {
171  return ns;
172 }
173 
175  const goto_tracet &goto_trace)
176 {
177  output_graphml(goto_trace, ns, options);
178 }
179 
181 {
182  // This is incorrect, but the best we can do at the moment.
183  const path_storaget::patht &resume = worklist->peek();
184  output_graphml(resume.equation, ns, options);
185 }
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:107
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:41
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Provides management of goal variables that encode properties.
unsigned get_remaining_vccs() const
Definition: goto_symex.h:835
Trace of a GOTO program.
Definition: goto_trace.h:177
ui_message_handlert & ui_message_handler
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:92
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.
single_path_symex_checkert(const optionst &options, ui_message_handlert &ui_message_handler, abstract_goto_modelt &goto_model)
const namespacet & get_namespace() const override
Returns the namespace associated with the traces.
std::unique_ptr< goto_symex_property_decidert > property_decider
virtual std::chrono::duration< double > prepare_property_decider(propertiest &properties, symex_target_equationt &equation, goto_symex_property_decidert &property_decider)
Prepare the property_decider for solving.
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, goto_symex_property_decidert &property_decider, std::chrono::duration< double > solver_runtime)
Run the property_decider, which calls the SAT solver, and set the status of checked properties accord...
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.
resultt operator()(propertiest &) override
Check whether the given properties with status NOT_CHECKED, UNKNOWN or properties newly discovered by...
bool is_ready_to_decide(const symex_bmct &, const path_storaget::patht &) override
Returns whether the given path produced by symex is ready to be checked.
Uses goto-symex to generate a symex_target_equationt for each path.
virtual void final_update_properties(propertiest &properties, std::unordered_set< irep_idt > &updated_properties)
Updates the properties after having finished exploration and adds their property IDs to updated_prope...
virtual void initialize_worklist()
Adds the initial goto-symex state as a path to the worklist.
std::chrono::duration< double > symex_runtime
std::unique_ptr< path_storaget > worklist
virtual void update_properties(propertiest &properties, std::unordered_set< irep_idt > &updated_properties, const symex_target_equationt &equation)
Updates the properties from the equation and adds their property IDs to updated_properties.
virtual bool resume_path(path_storaget::patht &path)
Continues exploring the given path using goto-symex.
virtual bool has_finished_exploration(const propertiest &)
Returns whether we should stop exploring paths.
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Counterexample Beautification.
std::unordered_map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
Definition: properties.h:75
Goto Checker using Single Path Symbolic Execution.
std::unordered_set< irep_idt > updated_properties
Changed properties since the last call to incremental_goto_checkert::operator()
Information saved at a conditional goto to resume execution.
Definition: path_storage.h:42
symex_target_equationt equation
Definition: path_storage.h:43
Bounded Model Checking for ANSI-C.