is satisfiable because arg[ 2] = NULL is
satisfiable, pointing to the condition
being misplaced in the code. This
is indeed where the bug lurks. Even
though the entire coding style and the
control flow in the buggy implementation was quite different from the
reference implementation, the debugging method is thus able to ignore
the differences in coding style in the
buggy implementation. Note arg[ 2]
= NULL is contributed by the branch
condition ap != NULL, a correlation
an automated debugging method can
keep track of. The method thus naturally zooms into the misplaced check
ap != NULL through a computation
of satisfiability of the deviations of
the failing test’s path condition.
One may question the choice of
considering the past version as a
specification of what the program is
supposed to achieve, a question that
arises because the software requirements of an earlier program version
may differ from the requirements of
the current program version. However, the comparison works as long as
the program features are common to
both versions and the requirements
are unchanged.
Perspectives
We have explored symbolic execution
and constraint solving for software debugging. We conclude by discussing
scalability and applicability of the presented techniques, along with possible
future research directions.
Scalability and applicability. The
scalability of the techniques de-
scribed here need greater investiga-
tion. Due to the semantic nature of the
analysis, symbolic execution-based
debugging of regression errors22 has
been adapted to multiple settings of
regression, resulting in wide applica-
bility, including regressions in a pro-
gram version as opposed to previous
version; regression in an embedded
software (such as Linux Busybox) as
opposed to reference software (such
as GNU Coreutils); 3 and regression
in a protocol implementation (such
as miniweb Web server implement-
ing the http protocol) as opposed to
a reference implementation of the
protocol, as in the Apache Web serv-
er. In these large-scale applications,
the symbolic analysis-based regres-
rent program P′ is taken as the “speci-
fication” against which the behavior of
the failing test t is compared for differ-
ence in control flow.
Such methods are based on semantic analysis, rather than a completely syntactic analysis of differences across program versions (such
as running a diff between program
versions). Being based on semantic
analysis these debugging methods
can analyze two versions with substantially different implementations
and locate causes of error.
To illustrate this point, consider
the fixed Address Resolution Protocol (ARP) implementation—Figure
1 with line 5 deleted—we discussed
earlier as the reference version. This
program will pass the test Test 2.
Now assume a buggy program implementation with a substantially different programming style but with intention to accomplish the same ARP
(see Figure 6). The test Test 2 fails in
this implementation
Test 2:
arp A INET (failing test).
Expected output: DEFAULT
Observed output: INET
First of all, a simple diff of the
program versions cannot help since
almost the entire program will ap-
pear in the diff. A careful com-
parison of the two implementations
shows the logic of the protocol the
programmer would want to imple-
ment has been mangled in this imple-
mentation. The computation of get
hwtype(DEFAULT) has been (cor-
rectly) moved. However, the compu-
tation of get _ hwtype(optarg)a
is executed under an incorrect condi-
tion, leading to the failure in the test
execution. A redundant check ap !=
NULL has slipped into line 8.
We now step through the localization of the error. For the test arp A
INET the path condition in the reference version is (since i is set to arg[ 1])
as follows
f ≡ arg[ 1] = A
The path condition in the buggy implementation is as follows (since i is set to
arg[ 1] and ap is set to arg[ 2] (via optarg)
f ′ ≡ arg[ 1] = A ∧ (arg[ 2] ≠ NULL ∨ arg[ 1] = H)
The negation of f ′ is the following disjunction
¬f ′ ≡ arg[ 1] ≠ A ∨ ¬(arg[ 2] ≠ NULL ∨ arg[ 1] = H)
f ∧ ¬f ′ thus has two possibilities to
consider, one for each disjunct in ¬f ′
1. arg[ 1] = A ∧ arg[ 1] ≠ A
2. arg[ 1] = A ∧ ¬(arg[ 2] ≠ NULL ∨
arg[ 1] = H)
The first formula is not satisfiable, and
the second one simplifies to
arg[ 1] = A ∧ arg[ 2] = NULL ∧ arg[ 1] ≠ H
A satisfying assignment to this second
formula is an input that shows the essential control-flow path deviation—
in the defective program—from the
failure-inducing input. This formula
a Assume get hwtype(INE T) returns INE T.
Figure 6. Assume line 5 in Figure 1 was removed yielding the correct program for the code
fragment; here we show a different implementation of the same code.