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.