Skip to content

Commit 3487bf7

Browse files
smowtonsmowton
committed
Reachability slicer: mark reachable code more precisely
The reachability slicer currently uses a very simple graph walk, and in particular walks out of a function to all possible callers, regardless of whether we know the actual caller. This commit fixes that shortcoming by adding the callsite successor *at the callsite*, and tracking the fact that the callee's successor has already been taken care of in the graph search stack, thus allowing it to ignore the END_FUNCTION -> callsite edges which are less precise. Functions whose caller is genuinely unknown, such as the root function containing a reachability target (e.g. assert instruction) are treated as before, considering all possible callees. The backwards search is improved similarly to the forwards.
1 parent a06503b commit 3487bf7

File tree

4 files changed

+223
-8
lines changed

4 files changed

+223
-8
lines changed

‎regression/cbmc/reachability-slice-interproc/test.c‎

Lines changed: 76 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,76 @@
1+
#include <assert.h>
2+
3+
// After a reachability slice based on the assertion in `target`, we should
4+
// retain both its possible callers (...may_call_target_1, ...may_call_target_2)
5+
// and their callees, but should be more precise concerning before_target and
6+
// after_target, which even though they are also called by
7+
// `unreachable_calls_before_target` and `unreachable_calls_after_target`, those
8+
// functions are not reachable.
9+
10+
void before_target()
11+
{
12+
const char *local = "before_target_kept";
13+
}
14+
15+
void after_target()
16+
{
17+
const char *local = "after_target_kept";
18+
}
19+
20+
void target()
21+
{
22+
const char *local = "target_kept";
23+
24+
before_target();
25+
assert(0);
26+
after_target();
27+
}
28+
29+
void unreachable_calls_before_target()
30+
{
31+
const char *local = "unreachable_calls_before_target_kept";
32+
before_target();
33+
}
34+
35+
void unreachable_calls_after_target()
36+
{
37+
const char *local = "unreachable_calls_after_target_kept";
38+
after_target();
39+
}
40+
41+
void reachable_before_target_caller_1()
42+
{
43+
const char *local = "reachable_before_target_caller_1_kept";
44+
}
45+
46+
void reachable_after_target_caller_1()
47+
{
48+
const char *local = "reachable_after_target_caller_1_kept";
49+
}
50+
51+
void reachable_may_call_target_1()
52+
{
53+
const char *local = "reachable_may_call_target_1_kept";
54+
reachable_before_target_caller_1();
55+
target();
56+
reachable_after_target_caller_1();
57+
}
58+
59+
void reachable_before_target_caller_2()
60+
{
61+
const char *local = "reachable_before_target_caller_2_kept";
62+
}
63+
64+
void reachable_after_target_caller_2()
65+
{
66+
const char *local = "reachable_after_target_caller_2_kept";
67+
}
68+
69+
void reachable_may_call_target_2()
70+
{
71+
const char *local = "reachable_may_call_target_2_kept";
72+
reachable_before_target_caller_2();
73+
target();
74+
reachable_after_target_caller_2();
75+
}
76+

‎regression/cbmc/reachability-slice-interproc/test.desc‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
test.c
3+
--reachability-slice-fb --show-goto-functions
4+
target_kept
5+
reachable_before_target_caller_1_kept
6+
reachable_after_target_caller_1_kept
7+
reachable_may_call_target_1_kept
8+
reachable_before_target_caller_2_kept
9+
reachable_after_target_caller_2_kept
10+
reachable_may_call_target_2_kept
11+
--
12+
unreachable_calls_before_target_kept
13+
unreachable_calls_after_target_kept

‎src/goto-instrument/reachability_slicer.cpp‎

Lines changed: 111 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -44,6 +44,15 @@ reachability_slicert::get_sources(
4444
return sources;
4545
}
4646

47+
static bool is_same_target(
48+
goto_programt::const_targett it1,
49+
goto_programt::const_targett it2)
50+
{
51+
// Avoid comparing iterators belonging to different functions, and therefore
52+
// different std::lists.
53+
return it1->function == it2->function && it1 == it2;
54+
}
55+
4756
/// Perform backwards depth-first search of the control-flow graph of the
4857
/// goto program, starting from the nodes corresponding to the criterion and
4958
/// the instructions that might be executed concurrently. Set reaches_assertion
@@ -54,11 +63,50 @@ void reachability_slicert::fixedpoint_to_assertions(
5463
const is_threadedt &is_threaded,
5564
slicing_criteriont &criterion)
5665
{
57-
std::vector<cfgt::node_indext> src = get_sources(is_threaded, criterion);
66+
std::vector<search_stack_entryt> stack;
67+
std::vector<cfgt::node_indext> sources = get_sources(is_threaded, criterion);
68+
for(const auto source : sources)
69+
stack.emplace_back(source, false);
70+
71+
while(!stack.empty())
72+
{
73+
auto &node = cfg[stack.back().node_index];
74+
const auto caller_is_known = stack.back().caller_is_known;
75+
stack.pop_back();
5876

59-
std::vector<cfgt::node_indext> reachable = cfg.get_reachable(src, false);
60-
for(const auto index : reachable)
61-
cfg[index].reaches_assertion = true;
77+
if(node.reaches_assertion)
78+
continue;
79+
node.reaches_assertion = true;
80+
81+
for(const auto &edge : node.in)
82+
{
83+
const auto &pred_node = cfg[edge.first];
84+
85+
if(pred_node.PC->is_end_function())
86+
{
87+
// This is an end-of-function -> successor-of-callsite edge.
88+
// Queue both the caller and the end of the callee.
89+
INVARIANT(
90+
std::prev(node.PC)->is_function_call(),
91+
"all function return edges should point to the successor of a "
92+
"FUNCTION_CALL instruction");
93+
stack.emplace_back(edge.first, true);
94+
stack.emplace_back(
95+
cfg.entry_map[std::prev(node.PC)], caller_is_known);
96+
}
97+
else if(pred_node.PC->is_function_call())
98+
{
99+
// Skip this predecessor, unless this is a bodyless function, or we
100+
// don't know who our callee was:
101+
if(!caller_is_known || is_same_target(std::next(pred_node.PC), node.PC))
102+
stack.emplace_back(edge.first, caller_is_known);
103+
}
104+
else
105+
{
106+
stack.emplace_back(edge.first, caller_is_known);
107+
}
108+
}
109+
}
62110
}
63111

64112
/// Perform forwards depth-first search of the control-flow graph of the
@@ -71,11 +119,66 @@ void reachability_slicert::fixedpoint_from_assertions(
71119
const is_threadedt &is_threaded,
72120
slicing_criteriont &criterion)
73121
{
74-
std::vector<cfgt::node_indext> src = get_sources(is_threaded, criterion);
122+
std::vector<search_stack_entryt> stack;
123+
std::vector<cfgt::node_indext> sources = get_sources(is_threaded, criterion);
124+
for(const auto source : sources)
125+
stack.emplace_back(source, false);
75126

76-
const std::vector<cfgt::node_indext> reachable = cfg.get_reachable(src, true);
77-
for(const auto index : reachable)
78-
cfg[index].reachable_from_assertion = true;
127+
while(!stack.empty())
128+
{
129+
auto &node = cfg[stack.back().node_index];
130+
const auto caller_is_known = stack.back().caller_is_known;
131+
stack.pop_back();
132+
133+
if(node.reachable_from_assertion)
134+
continue;
135+
node.reachable_from_assertion = true;
136+
137+
if(node.PC->is_function_call())
138+
{
139+
// Queue the instruction's natural successor (function head, or next
140+
// instruction if the function is bodyless)
141+
INVARIANT(node.out.size() == 1, "Call sites should have one successor");
142+
const auto successor_index = node.out.begin()->first;
143+
144+
// If the function has a body, mark the function head, but note that we
145+
// have already taken care of the return site.
146+
const auto &callee_head_node = cfg[successor_index];
147+
auto callee_it = callee_head_node.PC;
148+
if(!is_same_target(callee_it, std::next(node.PC)))
149+
{
150+
stack.emplace_back(successor_index, true);
151+
152+
// Check if it can return, and if so mark the callsite's successor:
153+
while(!callee_it->is_end_function())
154+
++callee_it;
155+
156+
if(!cfg[cfg.entry_map[callee_it]].out.empty())
157+
{
158+
stack.emplace_back(
159+
cfg.entry_map[std::next(node.PC)], caller_is_known);
160+
}
161+
}
162+
else
163+
{
164+
// Bodyless function -- mark the successor instruction only.
165+
stack.emplace_back(successor_index, caller_is_known);
166+
}
167+
}
168+
else if(node.PC->is_end_function() && caller_is_known)
169+
{
170+
// Special case -- the callsite successor was already queued when entering
171+
// this function, more precisely than we can see from the function return
172+
// edges (which lead to all possible callers), so nothing to do here.
173+
}
174+
else
175+
{
176+
// General case, including end-of-function where we don't know our caller.
177+
// Queue all successors.
178+
for(const auto &edge : node.out)
179+
stack.emplace_back(edge.first, caller_is_known);
180+
}
181+
}
79182
}
80183

81184
/// This function removes all instructions that have the flag

‎src/goto-instrument/reachability_slicer_class.h‎

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -51,6 +51,29 @@ class reachability_slicert
5151

5252
typedef std::stack<cfgt::entryt> queuet;
5353

54+
/// A search stack entry, used in tracking nodes to mark reachable when
55+
/// walking over the CFG in `fixedpoint_to_assertions` and
56+
/// `fixedpoint_from_assertions`.
57+
struct search_stack_entryt
58+
{
59+
/// CFG node to mark reachable
60+
cfgt::node_indext node_index;
61+
62+
/// If true, this function's caller is known and has already been queued to
63+
/// mark reachable, so there is no need to queue anything when walking out
64+
/// of the function, whether forwards (via END_FUNCTION) or backwards (via a
65+
/// callsite).
66+
/// If false, this function's caller is not known, so when walking forwards
67+
/// from the end or backwards from the beginning we should queue all
68+
/// possible callers.
69+
bool caller_is_known;
70+
71+
search_stack_entryt(cfgt::node_indext node_index, bool caller_is_known) :
72+
node_index(node_index), caller_is_known(caller_is_known)
73+
{
74+
}
75+
};
76+
5477
void fixedpoint_to_assertions(
5578
const is_threadedt &is_threaded,
5679
slicing_criteriont &criterion);

0 commit comments

Comments
 (0)