Skip to content

Commit 0acbd39

Browse files
peterschrammelpeterschrammel
committed
Add single-path symex checker
Extends single_path_symex_only_checkert with calling the solver and returning traces.
1 parent fe2448e commit 0acbd39

File tree

3 files changed

+294
-0
lines changed

3 files changed

+294
-0
lines changed

‎src/goto-checker/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ SRC = bmc_util.cpp \
77
goto_verifier.cpp \
88
multi_path_symex_checker.cpp \
99
multi_path_symex_only_checker.cpp \
10+
single_path_symex_checker.cpp \
1011
single_path_symex_only_checker.cpp \
1112
properties.cpp \
1213
report_util.cpp \

‎src/goto-checker/single_path_symex_checker.cpp

Lines changed: 238 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,238 @@
1+
/*******************************************************************\
2+
3+
Module: Goto Checker using Single Path Symbolic Execution
4+
5+
Author: Daniel Kroening, Peter Schrammel
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Goto Checker using Single Path Symbolic Execution
11+
12+
#include "single_path_symex_checker.h"
13+
14+
#include <chrono>
15+
16+
#include "bmc_util.h"
17+
#include "counterexample_beautification.h"
18+
#include "symex_bmc.h"
19+
20+
single_path_symex_checkert::single_path_symex_checkert(
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+
28+
incremental_goto_checkert::resultt single_path_symex_checkert::
29+
operator()(propertiest &properties)
30+
{
31+
resultt result(resultt::progresst::DONE);
32+
33+
// Unfortunately, the initial symex run is currently handled differently
34+
// from the subsequent runs
35+
if(!initial_symex_has_run)
36+
{
37+
initial_symex_has_run = true;
38+
first_equation = symex_target_equationt();
39+
symex_bmct symex(
40+
ui_message_handler,
41+
goto_model.get_symbol_table(),
42+
first_equation.value(),
43+
options,
44+
*worklist);
45+
46+
setup_symex(symex);
47+
perform_symex(
48+
goto_model,
49+
symex,
50+
symex_symbol_table,
51+
first_equation.value(),
52+
options,
53+
ns,
54+
ui_message_handler);
55+
56+
output_coverage_report(
57+
options.get_option("symex-coverage-report"),
58+
goto_model,
59+
symex,
60+
ui_message_handler);
61+
62+
if(symex.get_remaining_vccs() > 0)
63+
{
64+
prepare(result, properties, first_equation.value());
65+
decide(result, properties);
66+
67+
if(result.progress == resultt::progresst::FOUND_FAIL)
68+
return result;
69+
}
70+
}
71+
72+
// There might be more solutions from the previous equation.
73+
if(property_decider)
74+
{
75+
decide(result, properties);
76+
if(result.progress == resultt::progresst::FOUND_FAIL)
77+
return result;
78+
}
79+
80+
if(first_equation.has_value())
81+
{
82+
// We are in the second iteration. We don't need the equation
83+
// from the first iteration anymore.
84+
first_equation = {};
85+
}
86+
else
87+
{
88+
if(!worklist->empty())
89+
{
90+
// We are in iteration 3 or later; we pop the item processed
91+
// in the previous iteration.
92+
worklist->pop();
93+
}
94+
else
95+
{
96+
// We are already done.
97+
}
98+
}
99+
100+
while(!worklist->empty())
101+
{
102+
path_storaget::patht &resume = worklist->peek();
103+
symex_bmct symex(
104+
ui_message_handler,
105+
goto_model.get_symbol_table(),
106+
resume.equation,
107+
options,
108+
*worklist);
109+
110+
setup_symex(symex);
111+
perform_symex(
112+
goto_model,
113+
symex,
114+
resume,
115+
symex_symbol_table,
116+
options,
117+
ns,
118+
ui_message_handler);
119+
120+
output_coverage_report(
121+
options.get_option("symex-coverage-report"),
122+
goto_model,
123+
symex,
124+
ui_message_handler);
125+
126+
if(symex.get_remaining_vccs() > 0)
127+
{
128+
prepare(result, properties, resume.equation);
129+
decide(result, properties);
130+
131+
if(result.progress == resultt::progresst::FOUND_FAIL)
132+
return result;
133+
}
134+
135+
worklist->pop();
136+
}
137+
138+
// For now, we assume that NOT_REACHED properties are PASS.
139+
update_status_of_not_checked_properties(
140+
properties, result.updated_properties);
141+
142+
// For now, we assume that UNKNOWN properties are PASS.
143+
update_status_of_unknown_properties(properties, result.updated_properties);
144+
145+
// Worklist is empty: we are done.
146+
return result;
147+
}
148+
149+
goto_tracet single_path_symex_checkert::build_trace() const
150+
{
151+
if(options.get_bool_option("beautify"))
152+
{
153+
counterexample_beautificationt()(
154+
dynamic_cast<boolbvt &>(property_decider->get_solver()),
155+
property_decider->get_equation());
156+
}
157+
goto_tracet goto_trace;
158+
::build_error_trace(
159+
goto_trace,
160+
ns,
161+
property_decider->get_equation(),
162+
property_decider->get_solver(),
163+
ui_message_handler);
164+
return goto_trace;
165+
}
166+
167+
const namespacet &single_path_symex_checkert::get_namespace() const
168+
{
169+
return ns;
170+
}
171+
172+
void single_path_symex_checkert::output_error_witness(
173+
const goto_tracet &goto_trace)
174+
{
175+
output_graphml(goto_trace, ns, options);
176+
}
177+
178+
void single_path_symex_checkert::output_proof()
179+
{
180+
// This is incorrect, but the best we can do at the moment.
181+
const path_storaget::patht &resume = worklist->peek();
182+
output_graphml(resume.equation, ns, options);
183+
}
184+
185+
void single_path_symex_checkert::prepare(
186+
resultt &result,
187+
propertiest &properties,
188+
symex_target_equationt &equation)
189+
{
190+
update_properties_status_from_symex_target_equation(
191+
properties, result.updated_properties, equation);
192+
193+
property_decider = util_make_unique<goto_symex_property_decidert>(
194+
goto_symex_property_decidert(options, ui_message_handler, equation, ns));
195+
196+
log.status() << "Passing problem to "
197+
<< property_decider->get_solver().decision_procedure_text()
198+
<< messaget::eom;
199+
200+
convert_symex_target_equation(
201+
equation, property_decider->get_solver(), ui_message_handler);
202+
property_decider->update_properties_goals_from_symex_target_equation(
203+
properties);
204+
property_decider->convert_goals();
205+
property_decider->freeze_goal_variables();
206+
}
207+
208+
void single_path_symex_checkert::decide(
209+
resultt &result,
210+
propertiest &properties)
211+
{
212+
auto solver_start = std::chrono::steady_clock::now();
213+
214+
log.status() << "Running "
215+
<< property_decider->get_solver().decision_procedure_text()
216+
<< messaget::eom;
217+
218+
property_decider->add_constraint_from_goals(
219+
[&properties](const irep_idt &property_id) {
220+
return is_property_to_check(properties.at(property_id).status);
221+
});
222+
223+
decision_proceduret::resultt dec_result = property_decider->solve();
224+
225+
property_decider->update_properties_status_from_goals(
226+
properties, result.updated_properties, dec_result, false);
227+
228+
auto solver_stop = std::chrono::steady_clock::now();
229+
log.status()
230+
<< "Runtime decision procedure: "
231+
<< std::chrono::duration<double>(solver_stop - solver_start).count() << "s"
232+
<< messaget::eom;
233+
234+
if(dec_result == decision_proceduret::resultt::D_SATISFIABLE)
235+
{
236+
result.progress = resultt::progresst::FOUND_FAIL;
237+
}
238+
}

‎src/goto-checker/single_path_symex_checker.h

Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
/*******************************************************************\
2+
3+
Module: Goto Checker using Single Path Symbolic Execution
4+
5+
Author: Daniel Kroening, Peter Schrammel
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Goto Checker using Single Path Symbolic Execution
11+
12+
#ifndef CPROVER_GOTO_CHECKER_SINGLE_PATH_SYMEX_CHECKER_H
13+
#define CPROVER_GOTO_CHECKER_SINGLE_PATH_SYMEX_CHECKER_H
14+
15+
#include <util/optional.h>
16+
17+
#include "goto_symex_property_decider.h"
18+
#include "goto_trace_provider.h"
19+
#include "single_path_symex_only_checker.h"
20+
#include "solver_factory.h"
21+
#include "witness_provider.h"
22+
23+
class single_path_symex_checkert : public single_path_symex_only_checkert,
24+
public witness_providert,
25+
public goto_trace_providert
26+
{
27+
public:
28+
single_path_symex_checkert(
29+
const optionst &options,
30+
ui_message_handlert &ui_message_handler,
31+
abstract_goto_modelt &goto_model);
32+
33+
resultt operator()(propertiest &) override;
34+
35+
goto_tracet build_trace() const override;
36+
const namespacet &get_namespace() const override;
37+
38+
void output_error_witness(const goto_tracet &) override;
39+
void output_proof() override;
40+
41+
virtual ~single_path_symex_checkert() = default;
42+
43+
protected:
44+
bool initial_symex_has_run = false;
45+
optionalt<symex_target_equationt> first_equation; // for building traces
46+
std::unique_ptr<goto_symex_property_decidert> property_decider;
47+
48+
void prepare(
49+
resultt &result,
50+
propertiest &properties,
51+
symex_target_equationt &equation);
52+
void decide(resultt &result, propertiest &properties);
53+
};
54+
55+
#endif // CPROVER_GOTO_CHECKER_SINGLE_PATH_SYMEX_CHECKER_H

0 commit comments

Comments
 (0)