Skip to content

Commit c5734a2

Browse files
peterschrammelpeterschrammel
committed
Add single-path symex checker
1 parent 57d21a9 commit c5734a2

File tree

3 files changed

+291
-0
lines changed

3 files changed

+291
-0
lines changed

‎src/goto-checker/Makefile

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

‎src/goto-checker/single_path_symex_checker.cpp

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

‎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)