Path Slicing
∗
Ranjit Jhala
CS Department, UC San Diego
jhala@cs.ucsd.edu
Rupak Majumdar
CS Department, UC Los Angeles
rupak@cs.ucla.edu
Abstract
We present a new technique, path slicing, that takes as input a possibly in-
feasible path to a target location, and eliminates all the operations that are
irrelevant towards the reachability of the target location. A path slice is a
subsequence of the original path whose infeasibility guarantees the infea-
sibility of the original path, and whose feasibility guarantees the existence
of some feasible variant of the given path that reaches the target location
even though the given path may itself be infeasible. Our method combines
the ability of program slicing to look at several program paths, with the pre-
cision that dynamic slicing enjoys by focusing on a single path. We have
implemented Path Slicing to analyze possible counterexamples returned by
the software model checker BLAST. We show its effectiveness in drastically
reducing the size of the counterexamples to less than 1% of their origi-
nal size. This enables the precise veri cation of application programs (upto
100KLOC), by allowing the analysis to focus on the part of the counterex-
ample that is relevant to the property being checked.
Categories and Subject Descriptors: D.2.4 [Software Engineer-
ing]: Software/Program Veri cation; D.3.4 [Programming Lan-
guages]: Processors.
General Terms: Languages, Veri cation, Reliability.
Keywords: Program slicing, counterexample analysis.
1. Introduction
We introduce path slicing, a technique to determine which subset
of the edges along a given control ow path to particular target
location are relevant towards demonstrating the (un)reachability of
the target location along the given path.
Static analyses used to verify safety properties return control
ow paths to an error location as possible counterexamples demon-
strating that the program is unsafe. As the static analysis is typically
conservative, this path may or may not represent an actual violation
of the property. Traditionally, such control ow paths, are examined
manually to determine whether they correspond to a feasible pro-
gram execution, and therefore, a bug [9, 8, 14, 23]. For large pro-
grams, the sheer length of the path makes such manual inspection
dif cult. More recently, counterexample-guided program analyses
[3, 18, 7, 12] attempt to automatically nd out if the path is feasi-
ble, and if not, they exploit the infeasibility of the path to re ne the
∗
This research was supported in part by the grant NSF CCR-0427202.
Permission to make digital or hard copies of all or part of this work for personal or
classroom use is granted without fee provided that copies are not made or distributed
for pro t or commercial advantage and that copies bear this notice and the full citation
on the rst page. To copy otherwise, to republish, to post on servers or to redistribute
to lists, requires prior speci c permission and/or a fee.
PLDI 05, June 12—15, 2005, Chicago, Illinois, USA.
Copyright 2005 ACM 1-59593-056-6/05/0006...$5.00.
Figure 1. (A) Ex2 (B) CFA for Ex2 (C)Path, Slice
abstraction used for analysis. Once again, long counterexamples
complicate this process.
Consider the program Ex2 shown in Figure 1(A). For the mo-
ment, let us assume that the shaded grey code is missing, i.e., the
program begins from the label 2:. This program is a simpli ed
version of the following veri cation instance: The variable x corre-
sponds to a le; it is non-zero if the le has been opened. The le
may be opened and read depending on some condition, captured by
the variable a, that is unconstrained in the example (suppose it is an
input). The le should only be read if open; the branch at 6: mod-
els the check that the le is indeed open, which is an assert that we
put in just before an actual read from the le takes place. Thus, the
label ERR is reached if this assertion is violated. Let us suppose that
the function f, whose code is not shown, always terminates, and
that f does not modify the variables a, x. In this case, as the pro-
gram eventually breaks out of the loop, a is unconstrained, and x is
not set anywhere (recall that we are assuming the shaded lines are
missing), the target is indeed reachable. However, any feasible path
to the target must contain a thousand unrollings of the for-loop ,
not to mention feasible paths through f. Any path to the target loca-
tion that does not meet these requirements is infeasible, and if our
static analysis returns such a path, we have no option but to dismiss
it as a false positive arising from the imprecision of the analysis.
In this case, the analysis cannot be used to make any claim about
the reachability of the target location. Counterexample-guided re-
nement based techniques are doomed to either take a long time to
nd an abstraction precise enough to force them around the loop a
thousand times, or worse, not terminate, because of the dif culty
of nding a feasible path through f, which may be arbitrarily com-
plex.
The question then is, is it possible to use (overapproximate)
static analyses to precisely report that the target location is reach-
38

Figure 2. (A)Program Ex1 (B)Path Slice
able, without actually nding a feasible path to it? Intuitively, the
code through the for-loop is irrelevant to the reachability of the er-
ror location. In other words, if we can reason that there exists some
path from the start to the end of the loop, i.e., from location 3: to
5:, and along such a path, the variables x, a are not modi ed, then
we are guaranteed that the location ERR: can be reached.
Consider a candidate path to the location ERR: shown in Fig-
ure 1(C). While this particular path is infeasible, as we unroll the
loop only once, if we delete the irrelevant operations correspond-
ing to the loop (shown via the dotted edges), then the remaining
sequence of operations is feasible. We formalize this notion of re-
moving irrelevant instructions along a path as path slicing.
A path slice of a control ow path pi in a program is a subse-
quence of the edges of pi such that (1) if the sequence of slice op-
erations is infeasible, then the original path is infeasible, and (2) if
the sequence of slice operations is feasible, then the last location
of pi is reachable (modulo program termination). Intuitively, a path
slice is obtained by dropping some edges along the path, but leav-
ing the edges corresponding to branches that must be taken to reach
the target, and assignments that feed the values to the expressions
in the branches.
Since a path slice concentrates attention on a particular control
ow path through the program, it can be much more precise than
a statically computed program slice [25, 19, 24]. Consider the
program fragment shown in Figure 2(A). The function complex()
does some computation that is hard to reason about statically, say
it factors large numbers. Hence it is dif cult to statically nd a
feasible path through it. However, suppose that complex() does
not modify a. A backward program slice of Ex1 with respect to
the target location marked ERR, would not be able to remove the
procedure complex(). This happens as there is a path (namely that
corresponding to the then branch of the conditional a > 0) along
which the result of the function ows into x, which in turn guards
the branch before the target location.
If instead, we focus on the path shown in Figure 2(B), we nd
that the value returned by complex along this path is irrelevant, and
so a path slice would (1) eliminate the path through the function
complex and (2) preserve the conditional corresponding to the
else branch. Thus the states that can execute the path slice, namely
those satisfying a ≤ 0, all reach the target location (provided
complex terminates).
Hence, a path slice can be signi cantly more precise than static
program slice. In the case where counterexamples are manually
inspected, a path slice enables the human to focus on relevant
sections of the abstract counterexample path. In the case where
counterexamples are automatically analyzed to guide abstraction
re nement, this extra precision can make the difference between
termination and divergence: without this slice, we would iterate
forever trying to nd a feasible path through complex.
Path slicing is distinct from dynamic slicing [20, 27] in two
ways. First, the paths are not the result of a dynamic execution
and hence are not guaranteed to be feasible. Second, and more
importantly, we consider alternative program paths to nd if some
variant of the given path is in fact feasible, as shown by the path
through Ex2.
We show how to ef ciently compute a path slice, by performing
a backwards data ow analysis over the given path. Our algorithm,
called PathSlice, iterates backwards over the path, tracking, at each
point, the set of lvalues that determine if the suf x of the path from
that point is feasible, called the live lvalues and the source location
of the last edge added to the slice, called the step location. We take
an edge corresponding to an assignment if the assignment is to a
live variable. We take an edge corresponding to a conditional if
either the conditional corresponds to the branch direction that must
be taken to reach the step location, or if in the branch not taken,
the program may have modi ed a live variable. If an edge is taken,
the live set and step location are appropriately updated. We show
how a must-reachability analysis can be used to detect the former
case, and a modi ed-variable analysis can be used to detect the
latter case. Both these analyses are intraprocedural and hence give
us an ef cient path slicing algorithm. For function calls, we only
enter the body of the call if the function can modify a live variable,
otherwise the entire path through the call is sliced away.
One limitation of path slicing is that it avoids the dif cult ques-
tion of statically reasoning about termination. As a result, the fea-
sibility of a path slice guarantees that either the target location is
reachable, or all states that can execute the path slice, cause the
program to enter an in nite loop.
We have implemented Algorithm PathSlice in the counterex-
ample analysis phase of the software model checker BLAST [18].
We ran this enhanced algorithm to check for le handling errors in
a set of application programs. The largest programs checked had
about 100K lines of code. Without the path slicing algorithm, the
counterexample analysis phase of BLAST did not scale to any of
these examples, because rst the counterexamples were too large
to analyze for feasibility, and second they contained many irrele-
vant reasons for infeasibility, causing a blowup in the size of the
abstractions as well as the number of iterations taken to nd the
abstraction relevant to the property.
With the path slicing algorithm we were able to check le han-
dling errors in all the programs, and found violations of the prop-
erty in some of them. In general, we found that slicing reduced
counterexample traces to less than 1% of their original size in most
cases. In fact, as the size of counterexample traces got bigger, the
slicing was more effective (traces over 5000 basic blocks almost al-
ways produced slices between 0.1% and 1% of their original sizes.
The end-to-end veri cation times (including model checking) for
these examples were all below one hour. In the cases where tool
returns a feasible path slice it is much easier for the user to go over
the more succinct slice to ascertain the veracity of the counterex-
ample. Thus, our experiments suggest that path slicing can extend
the scope of static analysis by eliminating irrelevant details.
Related Work. Program slicing [25] has been developed as a useful
tool program debugging, comprehension and testing [24]. Slicing is
studied primarily in two forms: static and dynamic.
In static slicing [19], the input is the static text of the program
and a slicing criterion (for example, a set of variables at a par-
ticular program point), and a static analysis algorithm is used to
overapproximate the set of all variables that may affect the slicing
criterion [24]. Unfortunately, while the sliced program generated
by these algorithms contains a subset of the statements and control
39