CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
single_path_symex_checker.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Goto Checker using Single Path Symbolic Execution
4
5Author: Daniel Kroening, Peter Schrammel
6
7\*******************************************************************/
8
11
13
14#include <util/ui_message.h>
15
16#include "bmc_util.h"
18#include "symex_bmc.h"
19
21 const optionst &options,
22 ui_message_handlert &ui_message_handler,
23 abstract_goto_modelt &goto_model)
24 : single_path_symex_only_checkert(options, ui_message_handler, goto_model)
25{
26}
27
29operator()(propertiest &properties)
30{
31 resultt result(resultt::progresst::DONE);
32
33 // There might be more solutions from the previous equation.
35 {
37 result, properties, *property_decider, std::chrono::duration<double>(0));
38
39 if(result.progress == resultt::progresst::FOUND_FAIL)
40 return result;
41 }
42
43 if(!worklist->empty())
44 {
45 // We pop the item processed in the previous iteration.
46 worklist->pop();
47 }
48
50 {
51 symex_initialized = true;
52
54 }
55
56 while(!has_finished_exploration(properties))
57 {
58 path_storaget::patht &path = worklist->peek();
59 const bool ready_to_decide = resume_path(path);
60
62 {
63 update_properties(properties, result.updated_properties, path.equation);
64
65 property_decider = std::make_unique<goto_symex_property_decidert>(
67
68 const auto solver_runtime =
70
72 result, properties, *property_decider, solver_runtime);
73
74 if(result.progress == resultt::progresst::FOUND_FAIL)
75 return result;
76 }
77
78 // leave the last worklist item in place for the benefit of output_proof
79 if(worklist->size() == 1)
80 break;
81
82 worklist->pop();
83 }
84
85 log.statistics() << "Runtime Symex: " << symex_runtime.count() << "s"
87
89
90 // Worklist just has the last element left: we are done.
91 return result;
92}
93
95 const symex_bmct &symex,
97{
98 return symex.get_remaining_vccs() > 0;
99}
100
101std::chrono::duration<double>
103 propertiest &properties,
104 symex_target_equationt &equation,
105 goto_symex_property_decidert &property_decider)
106{
107 std::chrono::duration<double> solver_runtime = ::prepare_property_decider(
108 properties, equation, property_decider, ui_message_handler);
109
110 return solver_runtime;
111}
112
115 propertiest &properties,
116 goto_symex_property_decidert &property_decider,
117 std::chrono::duration<double> solver_runtime)
118{
120 result,
121 properties,
125 false);
126}
127
129{
132 property_decider->get_equation(),
133 property_decider->get_equation().SSA_steps.end(),
134 property_decider->get_decision_procedure(),
135 ns,
136 goto_trace);
137
138 return goto_trace;
139}
140
142{
143 if(options.get_bool_option("beautify"))
144 {
145 // NOLINTNEXTLINE(whitespace/braces)
147 property_decider->get_boolbv_decision_procedure(),
148 property_decider->get_equation());
149 }
150
153 property_decider->get_equation(),
154 property_decider->get_decision_procedure(),
155 ns,
156 goto_trace);
157
158 return goto_trace;
159}
160
163{
166 property_decider->get_equation(),
168 property_decider->get_decision_procedure(),
169 ns,
170 goto_trace);
171
172 return goto_trace;
173}
174
176{
177 return ns;
178}
179
185
187{
188 // This is incorrect, but the best we can do at the moment.
189 // operator()(propertiest &properties) leaves in place the last worklist item
190 // just for this purpose.
191 const path_storaget::patht &resume = worklist->peek();
193}
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:54
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.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Provides management of goal variables that encode properties.
unsigned get_remaining_vccs() const
Definition goto_symex.h:851
Trace of a GOTO program.
Definition goto_trace.h:177
ui_message_handlert & ui_message_handler
mstreamt & statistics() const
Definition message.h:411
static eomt eom
Definition message.h:289
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
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::map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
Definition properties.h:76
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.
symex_target_equationt equation
Bounded Model Checking for ANSI-C.