Skip to content

Commit d97f80f

Browse files
karkhazkarkhaz
committed
Add hybrid BDFS path exploration strategy
From the help text: explore breadth-first until we have N saved paths, at which point explore depth-first from each of those paths in round-robin order. N defaults to 8 and can be specified with the flag --bdfs-diameter N. This strategy is intended to be a nice compromise between low RAM usage and high coverage. The fact that we end paths as quickly as possible keeps memory use low, while branching very high up in the exploration tree means that we explore many different parts of the program.
1 parent 18be0df commit d97f80f

File tree

5 files changed

+287
-3
lines changed

5 files changed

+287
-3
lines changed

‎src/cbmc/bmc.cpp

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -577,6 +577,9 @@ int bmct::do_language_agnostic_bmc(
577577
if(tmp_result != safety_checkert::resultt::PAUSED)
578578
final_result &= tmp_result;
579579
worklist->pop();
580+
if(tmp_result != safety_checkert::resultt::PAUSED)
581+
if(worklist->interested_in_path_termination())
582+
worklist->notify_path_terminated();
580583
}
581584
}
582585
catch(const char *error_msg)

‎src/cbmc/bmc.h

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -300,6 +300,7 @@ class path_explorert : public bmct
300300
"(no-self-loops-to-assumptions)" \
301301
"(partial-loops)" \
302302
"(paths):" \
303+
"(bdfs-diameter):" \
303304
"(show-symex-strategies)" \
304305
"(depth):" \
305306
"(unwind):" \
@@ -309,6 +310,7 @@ class path_explorert : public bmct
309310

310311
#define HELP_BMC \
311312
" --paths [strategy] explore paths one at a time\n" \
313+
" --bdfs-diameter N read output of --show-symex-strategies\n" \
312314
" --show-symex-strategies list strategies for use with --paths\n" \
313315
" --program-only only show program expression\n" \
314316
" --show-loops show the loops in the program\n" \

‎src/goto-symex/path_storage.cpp

Lines changed: 157 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,136 @@ Author: Kareem Khazem <[email protected]>
1212

1313
#include <util/exit_codes.h>
1414
#include <util/make_unique.h>
15+
#include <util/string2int.h>
16+
17+
// _____________________________________________________________________________
18+
// breadth_depth_path_storaget
19+
20+
inline void breadth_depth_path_storaget::notify_path_terminated()
21+
{
22+
if(empty())
23+
return;
24+
do
25+
{
26+
++current_depth_queue;
27+
if(current_depth_queue == depth_list.end())
28+
current_depth_queue = depth_list.begin();
29+
} while(current_depth_queue->empty());
30+
last_peeked = current_depth_queue->end();
31+
}
32+
33+
path_storaget::patht &breadth_depth_path_storaget::private_peek()
34+
{
35+
INVARIANT(
36+
depth_list.empty() || current_depth_queue != depth_list.end(),
37+
"We have paths to explore DFS, but no pointer to which path to start with");
38+
39+
if(depth_list.empty())
40+
return breadth_list.front();
41+
42+
INVARIANT(
43+
last_peeked == current_depth_queue->end(),
44+
"Should have popped or notify_path_terminated() before peeking");
45+
46+
--last_peeked;
47+
return current_depth_queue->back();
48+
}
49+
50+
void breadth_depth_path_storaget::push(
51+
const path_storaget::patht &next_instruction,
52+
const path_storaget::patht &jump_target)
53+
{
54+
INVARIANT(
55+
depth_list.empty() || current_depth_queue != depth_list.end(),
56+
"We have paths to explore DFS, but no pointer to which path to start with");
57+
58+
source_locationt to_pop;
59+
60+
if(depth_list.empty())
61+
{
62+
if(!breadth_list.empty())
63+
to_pop = breadth_list.back().state.source.pc->source_location;
64+
breadth_list.push_back(next_instruction);
65+
breadth_list.push_back(jump_target);
66+
}
67+
else
68+
{
69+
current_depth_queue->push_back(next_instruction);
70+
current_depth_queue->push_back(jump_target);
71+
}
72+
73+
if(breadth_list.size() > diameter)
74+
{
75+
for(const auto &path : breadth_list)
76+
{
77+
std::list<patht> tmp;
78+
tmp.push_back(path);
79+
depth_list.push_back(tmp);
80+
context.log.debug()
81+
<< "DFS start point: " << path.state.saved_target->source_location
82+
<< context.log.eom;
83+
}
84+
// The path that led to next_instruction and jump_target being pushed is
85+
// currently the third-last item in breadth_list (the last and second-last
86+
// items are the two arguments to this method). We've just transferred
87+
// breadth_list into depth_list, but we need to ensure that when private_pop
88+
// is called, it actually pops the correct path from depth_list.
89+
std::list<std::list<patht>>::iterator tmp = depth_list.end();
90+
std::advance(tmp, -3);
91+
last_peeked = tmp->begin();
92+
INVARIANT(
93+
last_peeked->state.source.pc->source_location == to_pop,
94+
"Expected last_peeked to point to the precursor of next_instruction "
95+
"and jump_target");
96+
97+
// Meanwhile, when we peek, we should go through all the subtrees in a
98+
// round-robin fashion.
99+
current_depth_queue = depth_list.begin();
100+
101+
// From here onward, breadth_list will never be used.
102+
breadth_list.clear();
103+
}
104+
}
105+
106+
void breadth_depth_path_storaget::private_pop()
107+
{
108+
INVARIANT(
109+
depth_list.empty() || current_depth_queue != depth_list.end(),
110+
"We have paths to explore DFS, but no pointer to which path to start with");
111+
112+
if(depth_list.empty())
113+
breadth_list.pop_front();
114+
else
115+
{
116+
INVARIANT(
117+
last_peeked != current_depth_queue->end(),
118+
"Must peek immediately before popping");
119+
current_depth_queue->erase(last_peeked);
120+
last_peeked = current_depth_queue->end();
121+
}
122+
}
123+
124+
std::size_t breadth_depth_path_storaget::size() const
125+
{
126+
INVARIANT(
127+
depth_list.empty() || current_depth_queue != depth_list.end(),
128+
"We have paths to explore DFS, but no pointer to which path to start with");
129+
130+
if(depth_list.empty())
131+
return breadth_list.size();
132+
133+
std::size_t total = 0;
134+
for(const auto &paths : depth_list)
135+
total += paths.size();
136+
return total;
137+
}
138+
139+
void breadth_depth_path_storaget::clear()
140+
{
141+
breadth_list.clear();
142+
depth_list.clear();
143+
current_depth_queue = depth_list.end();
144+
}
15145

16146
// _____________________________________________________________________________
17147
// path_lifot
@@ -111,11 +241,37 @@ void path_strategy_choosert::set_path_strategy_options(
111241
}
112242
else
113243
options.set_option("exploration-strategy", default_strategy());
244+
245+
if(cmdline.isset("bdfs-diameter"))
246+
{
247+
if(!cmdline.isset("paths")
248+
|| options.get_option("exploration-strategy") != "hybrid-bdfs")
249+
{
250+
message.error() << "`--bdfs-diameter` can only be passed when passing "
251+
"`--paths hybrid-bdfs`."
252+
<< message.eom;
253+
exit(CPROVER_EXIT_USAGE_ERROR);
254+
}
255+
options.set_option(
256+
"bdfs-diameter",
257+
unsafe_string2unsigned(cmdline.get_value("bdfs-diameter")));
258+
}
114259
}
115260

116261
path_strategy_choosert::path_strategy_choosert()
117262
: strategies(
118-
{{"lifo",
263+
{{"hybrid-bdfs",
264+
{" hybrid-bdfs explore breadth-first until we have\n"
265+
" N saved paths, at which point explore\n"
266+
" depth-first from each of those paths\n"
267+
" in round-robin order. N defaults to 8\n"
268+
" and can be specified with the flag\n"
269+
" --bdfs-diameter N.\n",
270+
// NOLINTNEXTLINE(whitespace/braces)
271+
[](const path_storaget::strategy_contextt &ctx) {
272+
return util_make_unique<breadth_depth_path_storaget>(ctx);
273+
}}},
274+
{"lifo",
119275
{" lifo next instruction is pushed before\n"
120276
" goto target; paths are popped in\n"
121277
" last-in, first-out order. Explores\n"

‎src/goto-symex/path_storage.h

Lines changed: 58 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -18,8 +18,7 @@
1818
/// \brief Storage for symbolic execution paths to be resumed later
1919
///
2020
/// This data structure supports saving partially-executed symbolic
21-
/// execution \ref path_storaget::patht "paths" so that their execution can
22-
/// be halted and resumed later. The choice of which path should be
21+
/// execution \ref path_storaget::patht "paths" so that their execution can /// be halted and resumed later. The choice of which path should be
2322
/// resumed next is implemented by subtypes of this abstract class.
2423
class path_storaget
2524
{
@@ -114,6 +113,27 @@ class path_storaget
114113
return size() == 0;
115114
};
116115

116+
/// \brief Callback for clients to notify this path_storaget that we have
117+
/// symbolically executed to the end of a path, and the path has been
118+
/// model-checked.
119+
///
120+
/// This implementation does nothing. There is no need for clients to call
121+
/// this method if path_storaget::interested_in_path_termination() returns
122+
/// `false`.
123+
virtual void notify_path_terminated()
124+
{
125+
}
126+
127+
/// \brief Is this path_storaget interested in path termination?
128+
///
129+
/// If this method returns `true`, clients should call the
130+
/// path_storaget::notify_path_terminated() method whenever the client
131+
/// finishes symbolically executing a path.
132+
virtual bool interested_in_path_termination() const
133+
{
134+
return false;
135+
}
136+
117137
protected:
118138
const strategy_contextt &context;
119139

@@ -167,6 +187,42 @@ class path_fifot : public path_storaget
167187
void private_pop() override;
168188
};
169189

190+
/// \brief Hybrid breadth-then-depth search
191+
class breadth_depth_path_storaget : public path_storaget
192+
{
193+
public:
194+
void push(const patht &, const patht &) override;
195+
std::size_t size() const override;
196+
void clear() override;
197+
explicit breadth_depth_path_storaget(const strategy_contextt &ctx)
198+
: path_storaget(ctx),
199+
diameter(
200+
ctx.options.is_set("bdfs-diameter")
201+
? ctx.options.get_unsigned_int_option("bdfs-diameter")
202+
: 8U),
203+
depth_list(),
204+
current_depth_queue(depth_list.end())
205+
{
206+
}
207+
208+
virtual void notify_path_terminated() override;
209+
virtual bool interested_in_path_termination() const override
210+
{
211+
return true;
212+
}
213+
214+
protected:
215+
const unsigned diameter;
216+
std::list<patht> breadth_list;
217+
std::list<std::list<patht>> depth_list;
218+
std::list<std::list<patht>>::iterator current_depth_queue;
219+
std::list<patht>::iterator last_peeked;
220+
221+
private:
222+
patht &private_peek() override;
223+
void private_pop() override;
224+
};
225+
170226
/// \brief Dummy class for clients who will not use path exploration
171227
class degenerate_path_storaget : public path_storaget
172228
{

‎unit/path_strategies.cpp

Lines changed: 67 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -262,6 +262,73 @@ SCENARIO("path strategies")
262262
symex_eventt::result(symex_eventt::enumt::FAILURE)});
263263
}
264264
}
265+
266+
GIVEN("a very branchy program for testing hybrid strategy")
267+
{
268+
std::function<void(optionst &)> opts_callback;
269+
270+
c =
271+
"/* 1 */ void foo(int bar) \n"
272+
"/* 2 */ { \n"
273+
"/* 1 */ if(!bar) \n"
274+
"/* 2 */ return; \n"
275+
"/* 3 */ \n"
276+
"/* 4 */ int x; \n"
277+
"/* 5 */ if(x) \n"
278+
"/* 6 */ foo(bar - 1); \n"
279+
"/* 7 */ else \n"
280+
"/* 9 */ foo(bar - 1); \n"
281+
"/* 10 */ } \n"
282+
"/* 11 */ \n"
283+
"/* 12 */ int main() \n"
284+
"/* 13 */ { \n"
285+
"/* 14 */ foo(8); \n"
286+
"/* 15 */ } \n";
287+
288+
const symex_eventt::listt dfs_order =
289+
{symex_eventt::resume(symex_eventt::enumt::NEXT, 8),
290+
symex_eventt::resume(symex_eventt::enumt::JUMP, 10),
291+
symex_eventt::resume(symex_eventt::enumt::NEXT, 8),
292+
symex_eventt::resume(symex_eventt::enumt::JUMP, 10),
293+
symex_eventt::resume(symex_eventt::enumt::NEXT, 8),
294+
symex_eventt::resume(symex_eventt::enumt::JUMP, 10),
295+
symex_eventt::resume(symex_eventt::enumt::NEXT, 8),
296+
symex_eventt::result(symex_eventt::enumt::SUCCESS),
297+
symex_eventt::resume(symex_eventt::enumt::JUMP, 10),
298+
symex_eventt::result(symex_eventt::enumt::SUCCESS),
299+
symex_eventt::resume(symex_eventt::enumt::NEXT, 8),
300+
symex_eventt::result(symex_eventt::enumt::SUCCESS),
301+
symex_eventt::resume(symex_eventt::enumt::JUMP, 10),
302+
symex_eventt::result(symex_eventt::enumt::SUCCESS),
303+
symex_eventt::resume(symex_eventt::enumt::NEXT, 8),
304+
symex_eventt::result(symex_eventt::enumt::SUCCESS),
305+
symex_eventt::resume(symex_eventt::enumt::JUMP, 10),
306+
symex_eventt::result(symex_eventt::enumt::SUCCESS),
307+
symex_eventt::resume(symex_eventt::enumt::NEXT, 8),
308+
symex_eventt::result(symex_eventt::enumt::SUCCESS),
309+
symex_eventt::resume(symex_eventt::enumt::JUMP, 10),
310+
symex_eventt::result(symex_eventt::enumt::SUCCESS)};
311+
312+
// When --bdfs-diameter is huge, hybrid-bdfs should degenerate to BFS---that
313+
// is, they have exactly the same sequence of events. This is because
314+
// hybrid-bdfs never fills up its queue with enough paths to start DFSing
315+
// from the breadth-obtained paths.
316+
//
317+
opts_callback = [](optionst &opts)
318+
{
319+
opts.set_option("unwind", 2U);
320+
opts.set_option("bdfs-diameter", 1000U);
321+
};
322+
check_with_strategy("hybrid-bdfs", opts_callback, c, dfs_order);
323+
check_with_strategy("fifo", opts_callback, c, dfs_order);
324+
325+
opts_callback = [](optionst &opts)
326+
{
327+
opts.set_option("unwind", 2U);
328+
opts.set_option("bdfs-diameter", 2U);
329+
};
330+
check_with_strategy("hybrid-bdfs", opts_callback, c, dfs_order);
331+
}
265332
}
266333

267334
// In theory, there should be no need to change the code below when adding new

0 commit comments

Comments
 (0)