Skip to content

Commit e39ea2e

Browse files
tautschnigtautschnig
authored
Merge pull request #2683 from karkhaz/kk-continue-unsafe
Make --stop-on-fail halt symex early when doing path exploration
2 parents 18d08bf + 424ab4f commit e39ea2e

File tree

5 files changed

+117
-28
lines changed

5 files changed

+117
-28
lines changed

‎src/cbmc/bmc.cpp‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -588,6 +588,15 @@ int bmct::do_language_agnostic_bmc(
588588
if(driver_configure_bmc)
589589
driver_configure_bmc(bmc, symbol_table);
590590
tmp_result = bmc.run(model);
591+
592+
if(
593+
tmp_result == safety_checkert::resultt::UNSAFE &&
594+
opts.get_bool_option("stop-on-fail") && opts.is_set("paths"))
595+
{
596+
worklist->clear();
597+
return CPROVER_EXIT_VERIFICATION_UNSAFE;
598+
}
599+
591600
if(tmp_result != safety_checkert::resultt::PAUSED)
592601
final_result = tmp_result;
593602
}
@@ -637,6 +646,15 @@ int bmct::do_language_agnostic_bmc(
637646
if(driver_configure_bmc)
638647
driver_configure_bmc(pe, symbol_table);
639648
tmp_result = pe.run(model);
649+
650+
if(
651+
tmp_result == safety_checkert::resultt::UNSAFE &&
652+
opts.get_bool_option("stop-on-fail") && opts.is_set("paths"))
653+
{
654+
worklist->clear();
655+
return CPROVER_EXIT_VERIFICATION_UNSAFE;
656+
}
657+
640658
if(tmp_result != safety_checkert::resultt::PAUSED)
641659
final_result &= tmp_result;
642660
worklist->pop();

‎src/goto-symex/path_storage.cpp‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,11 @@ std::size_t path_lifot::size() const
4343
return paths.size();
4444
}
4545

46+
void path_lifot::clear()
47+
{
48+
paths.clear();
49+
}
50+
4651
// _____________________________________________________________________________
4752
// path_fifot
4853

@@ -69,6 +74,11 @@ std::size_t path_fifot::size() const
6974
return paths.size();
7075
}
7176

77+
void path_fifot::clear()
78+
{
79+
paths.clear();
80+
}
81+
7282
// _____________________________________________________________________________
7383
// path_strategy_choosert
7484

‎src/goto-symex/path_storage.h‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -50,6 +50,14 @@ class path_storaget
5050
return private_peek();
5151
}
5252

53+
/// \brief Clear all saved paths
54+
///
55+
/// This is typically used because we want to terminate symbolic execution
56+
/// early. It doesn't matter too much in terms of memory usage since CBMC
57+
/// typically exits soon after we do that, however it's nice to have tests
58+
/// that check that the worklist is always empty when symex finishes.
59+
virtual void clear() = 0;
60+
5361
/// \brief Add paths to resume to the storage
5462
///
5563
/// Symbolic execution is suspended when we reach a conditional goto
@@ -90,6 +98,7 @@ class path_lifot : public path_storaget
9098
public:
9199
void push(const patht &, const patht &) override;
92100
std::size_t size() const override;
101+
void clear() override;
93102

94103
protected:
95104
std::list<path_storaget::patht>::iterator last_peeked;
@@ -106,6 +115,7 @@ class path_fifot : public path_storaget
106115
public:
107116
void push(const patht &, const patht &) override;
108117
std::size_t size() const override;
118+
void clear() override;
109119

110120
protected:
111121
std::list<patht> paths;

‎unit/path_strategies.cpp‎

Lines changed: 75 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -65,6 +65,8 @@ SCENARIO("path strategies")
6565
std::string c;
6666
GIVEN("a simple conditional program")
6767
{
68+
std::function<void(optionst &)> opts_callback = [](optionst &opts) {};
69+
6870
c =
6971
"/* 1 */ int main() \n"
7072
"/* 2 */ { \n"
@@ -75,28 +77,28 @@ SCENARIO("path strategies")
7577
"/* 7 */ x = 0; \n"
7678
"/* 8 */ } \n";
7779

78-
const unsigned unwind_limit = 0U;
79-
8080
check_with_strategy(
8181
"lifo",
82+
opts_callback,
8283
c,
8384
{symex_eventt::resume(symex_eventt::enumt::JUMP, 7),
8485
symex_eventt::result(symex_eventt::enumt::SUCCESS),
8586
symex_eventt::resume(symex_eventt::enumt::NEXT, 5),
86-
symex_eventt::result(symex_eventt::enumt::SUCCESS)},
87-
unwind_limit);
87+
symex_eventt::result(symex_eventt::enumt::SUCCESS)});
8888
check_with_strategy(
8989
"fifo",
90+
opts_callback,
9091
c,
9192
{symex_eventt::resume(symex_eventt::enumt::NEXT, 5),
9293
symex_eventt::result(symex_eventt::enumt::SUCCESS),
9394
symex_eventt::resume(symex_eventt::enumt::JUMP, 7),
94-
symex_eventt::result(symex_eventt::enumt::SUCCESS)},
95-
unwind_limit);
95+
symex_eventt::result(symex_eventt::enumt::SUCCESS)});
9696
}
9797

9898
GIVEN("a program with nested conditionals")
9999
{
100+
std::function<void(optionst &)> opts_callback = [](optionst &opts) {};
101+
100102
c =
101103
"/* 1 */ int main() \n"
102104
"/* 2 */ { \n"
@@ -117,10 +119,9 @@ SCENARIO("path strategies")
117119
"/* 17 */ } \n"
118120
"/* 18 */ } \n";
119121

120-
const unsigned unwind_limit = 0U;
121-
122122
check_with_strategy(
123123
"lifo",
124+
opts_callback,
124125
c,
125126
{// Outer else, inner else
126127
symex_eventt::resume(symex_eventt::enumt::JUMP, 13),
@@ -135,11 +136,11 @@ SCENARIO("path strategies")
135136
symex_eventt::result(symex_eventt::enumt::SUCCESS),
136137
// Outer if, inner if
137138
symex_eventt::resume(symex_eventt::enumt::NEXT, 7),
138-
symex_eventt::result(symex_eventt::enumt::SUCCESS)},
139-
unwind_limit);
139+
symex_eventt::result(symex_eventt::enumt::SUCCESS)});
140140

141141
check_with_strategy(
142142
"fifo",
143+
opts_callback,
143144
c,
144145
{// Expand outer if, but don't continue depth-first
145146
symex_eventt::resume(symex_eventt::enumt::NEXT, 6),
@@ -155,12 +156,15 @@ SCENARIO("path strategies")
155156
symex_eventt::resume(symex_eventt::enumt::NEXT, 14),
156157
symex_eventt::result(symex_eventt::enumt::SUCCESS),
157158
symex_eventt::resume(symex_eventt::enumt::JUMP, 16),
158-
symex_eventt::result(symex_eventt::enumt::SUCCESS)},
159-
unwind_limit);
159+
symex_eventt::result(symex_eventt::enumt::SUCCESS)});
160160
}
161161

162162
GIVEN("a loop program to test functional correctness")
163163
{
164+
std::function<void(optionst &)> opts_callback = [](optionst &opts) {
165+
opts.set_option("unwind", 2U);
166+
};
167+
164168
c =
165169
"/* 1 */ int main() \n"
166170
"/* 2 */ { \n"
@@ -173,10 +177,9 @@ SCENARIO("path strategies")
173177
"/* 9 */ assert(x); \n"
174178
"/* 10 */ } \n";
175179

176-
const unsigned unwind_limit = 2U;
177-
178180
check_with_strategy(
179181
"lifo",
182+
opts_callback,
180183
c,
181184
{
182185
// The path where we skip the loop body. Successful because the path is
@@ -194,11 +197,11 @@ SCENARIO("path strategies")
194197
// infeasible.
195198
symex_eventt::resume(symex_eventt::enumt::NEXT, 7),
196199
symex_eventt::result(symex_eventt::enumt::SUCCESS),
197-
},
198-
unwind_limit);
200+
});
199201

200202
check_with_strategy(
201203
"fifo",
204+
opts_callback,
202205
c,
203206
{
204207
// The path where we skip the loop body. Successful because the path is
@@ -219,8 +222,46 @@ SCENARIO("path strategies")
219222
// executing the loop once, decrementing x to 0; assert(x) should fail.
220223
symex_eventt::resume(symex_eventt::enumt::JUMP, 9),
221224
symex_eventt::result(symex_eventt::enumt::FAILURE),
222-
},
223-
unwind_limit);
225+
});
226+
}
227+
228+
GIVEN("program to check for stop-on-fail with path exploration")
229+
{
230+
std::function<void(optionst &)> halt_callback = [](optionst &opts) {
231+
opts.set_option("stop-on-fail", true);
232+
};
233+
std::function<void(optionst &)> no_halt_callback = [](optionst &opts) {};
234+
235+
c =
236+
"/* 1 */ int main() \n"
237+
"/* 2 */ { \n"
238+
"/* 3 */ int x, y; \n"
239+
"/* 4 */ if(x) \n"
240+
"/* 5 */ assert(0); \n"
241+
"/* 6 */ else \n"
242+
"/* 7 */ assert(0); \n"
243+
"/* 8 */ } \n";
244+
245+
GIVEN("no stopping on failure")
246+
{
247+
check_with_strategy(
248+
"lifo",
249+
no_halt_callback,
250+
c,
251+
{symex_eventt::resume(symex_eventt::enumt::JUMP, 7),
252+
symex_eventt::result(symex_eventt::enumt::FAILURE),
253+
symex_eventt::resume(symex_eventt::enumt::NEXT, 5),
254+
symex_eventt::result(symex_eventt::enumt::FAILURE)});
255+
}
256+
GIVEN("stopping on failure")
257+
{
258+
check_with_strategy(
259+
"lifo",
260+
halt_callback,
261+
c,
262+
{symex_eventt::resume(symex_eventt::enumt::JUMP, 7),
263+
symex_eventt::result(symex_eventt::enumt::FAILURE)});
264+
}
224265
}
225266
}
226267

@@ -286,7 +327,7 @@ void symex_eventt::validate_resume(
286327
void _check_with_strategy(
287328
const std::string &strategy,
288329
const std::string &program,
289-
const unsigned unwind_limit,
330+
std::function<void(optionst &)> opts_callback,
290331
symex_eventt::listt &events)
291332
{
292333
temporary_filet tmp("path-explore_", ".c");
@@ -307,11 +348,7 @@ void _check_with_strategy(
307348
opts.set_option("paths", true);
308349
opts.set_option("exploration-strategy", strategy);
309350

310-
if(unwind_limit)
311-
{
312-
opts.set_option("unwind", unwind_limit);
313-
cmdline.set("unwind", std::to_string(unwind_limit));
314-
}
351+
opts_callback(opts);
315352

316353
ui_message_handlert mh(cmdline, "path-explore");
317354
mh.set_verbosity(0);
@@ -337,6 +374,13 @@ void _check_with_strategy(
337374
safety_checkert::resultt result = bmc.run(gm);
338375
symex_eventt::validate_result(events, result);
339376

377+
if(
378+
result == safety_checkert::resultt::UNSAFE &&
379+
opts.get_bool_option("stop-on-fail") && opts.is_set("paths"))
380+
{
381+
worklist->clear();
382+
}
383+
340384
while(!worklist->empty())
341385
{
342386
cbmc_solverst solvers(opts, gm.get_symbol_table(), mh);
@@ -360,6 +404,13 @@ void _check_with_strategy(
360404

361405
symex_eventt::validate_result(events, result);
362406
worklist->pop();
407+
408+
if(
409+
result == safety_checkert::resultt::UNSAFE &&
410+
opts.get_bool_option("stop-on-fail"))
411+
{
412+
worklist->clear();
413+
}
363414
}
364415
REQUIRE(events.empty());
365416
}

‎unit/path_strategies.h‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -45,18 +45,18 @@ struct symex_eventt
4545
void _check_with_strategy(
4646
const std::string &strategy,
4747
const std::string &program,
48-
const unsigned unwind_limit,
48+
std::function<void(optionst &)>,
4949
symex_eventt::listt &events);
5050

5151
/// Call this one, not the underscore version
5252
void check_with_strategy(
5353
const std::string &strategy,
54+
std::function<void(optionst &)> opts_callback,
5455
const std::string &program,
55-
symex_eventt::listt events,
56-
const unsigned unwind_limit)
56+
symex_eventt::listt events)
5757
{
5858
WHEN("strategy is '" + strategy + "'")
59-
_check_with_strategy(strategy, program, unwind_limit, events);
59+
_check_with_strategy(strategy, program, opts_callback, events);
6060
}
6161

6262
#endif // CPROVER_PATH_STRATEGIES_H

0 commit comments

Comments
 (0)