plication domains, programmers do
not write down detailed specifications
of the intended behavior of their code.
Protocol specifications, even when
available, are usually at a much higher
level than the level of the implementation described here. In this particular
case, when Test 2 fails, how does the
programmer infer where the program
execution turned incorrect?
The execution trace of Test 2 is as
follows
0 hw _ set = 0; hw = NULL; ap = NULL;
1 while (i = getopt(....)) {
2 switch (i) {
3 case 'A':
4 ap = getaftype(optarg);
5 hw _ set = 1;
6 break;
11 } // exit switch statement
1 while (i = getopt(....)) {
12 } // exit while loop
13 if (hw _ set == 0)
{ // this condition is false
16 assert(hw != NULL);
// assertion fails
So, when the assertion fails in line
16, which line in the program does the
programmer hold responsible for this
observed error? Is it line 13, where the
condition checked could have been
different (such as hw set == 1)? If this
was indeed the condition checked in
line 13, Test 2 would not fail. Is it line
5, where hw _ set is assigned? This
is the line we hypothesized as the bug
when we presented the buggy code to
a human, but how does a computer-aided debugging method know which
line is the real culprit for the observed
error, and can it be fixed?
In general, for any observable error,
there are several ways to fix a fault, and
the definition of the fault often depends
on how it is fixed. Since specifications
are unavailable, have we thus reached
the limit of what can be achieved in
computer-assisted debugging? Fortunately, it turns out some notion of
intended behavior of the program can
be recovered through indirect means
(such as internal inconsistency of the
failed trace, passing test cases, or an
older working version of the same program). In this article, we discuss debugging methods that rely on such indirect
program specifications to find the root
cause of an observable error.
Using Satisfiability
The technique we discuss first is called
“BugAssist” 13 in which the input and
desired output information from a failing test are encoded as constraints.
These input-output constraints are then
conjoined with the program formula,
which encodes the operational semantics of the program symbolically along
all paths; see Figure 2 for an overview
of conversion from a program to a formula. In the example program of Figure
1, we produce the following formula (φ):
φ = arg[ 1] = A ∧ arg[ 2] = INET ∧ arg[ 3]
= NULL
∧ hw_set0 = 0 ∧ hw0 = NULL ∧ ap0 =
NULL
∧ i1 = arg[ 1] ∧ i1 ≠ NULL
∧ guard3 = (i1 = = A)
∧ ap4 = arg[ 2]
∧ hw_set5 = 1
∧ ap11 = guard3 ap4 : ap0
∧ hw_set11 = guard3 hw_set5 : hw_set0
∧ i′ 1 = arg[ 3] ∧ i′ 1 = = NULL
∧ guard13 = (hw_set11 = = 0)
∧ hw14 = DEFAULT
∧ hw15 = guard13 hw14 : hw0
∧ hw15 ≠ NULL ∧ hw15 = = DEFAULT
The arg elements refer to the input
values, similar to argv of the C language; here, the inputs are for Test 2.
The last line of clauses represents the
expectation of Test 2. The remainder
of the formula represents the program
logic. (For brevity, we have omitted the
parts of the formula corresponding to
the case 'H', as it does not matter for
this input.) The variable i′ 1 refers to the
second time the loop condition while
is evaluated, at which point the loop
exits. We use = to indicate assignment
and == to indicate equality test in the
program, though for the satisfiability of
the formula both have the same meaning.
The formula φ, though lengthy, has
one-to-one correspondence to the trace
of Test 2 outlined earlier. Since the
test input used corresponds to a failing
test, the formula is unsatisfiable.
The BugAssist tool tries to infer
what went wrong by trying to make a
large part of the formula satisfiable,
accomplishing it through MAX-SAT19
or MAX-SMT solvers. As the name suggests, a MAX-SAT solver returns the
largest possible satisfiable sub-formula of a formula; the sub-formula omits
Fortunately,
it turns out
some notion of
intended behavior
of the program
can be recovered
through
indirect means.