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.