following fix at line 5 works for tests 1–3

5: hw_ set = 0

 

The astute reader will notice this particular fix is not an ideal fix. Given another test

 

Test 4: arp H ETHER A INET Expected output: E THER Actual output: DEFAULT

 

This test will fail with the proposed fix, even though the location of the fix is the correct one. The correct fix is to eliminate the effect of line 5 altogether

 

5: hw_ set = hw_ set; // or delete the statement

 

The example reflects the limitations in attempting to fix a program when working with an incomplete notion of “specification.”

Using Other Implementations

Programs are usually not written from scratch; rather, versions of a program are gradually checked in. When we introduce changes into a previously working version (where we say the version is “working,” since all test cases pass), certain passing tests may thus fail. To debug the cause of the observed failure in such a failed test t, we can treat the behavior of t in the previous working version as a description of the programmer’s intention.

The technique presented in Qi et al., 22 called “Darwin,” developed in 2009, executes the failing test t in the previous program version P, as well as the current program version P′. It then calculates the path conditions of t in both program versions along the execution trace of t in both program versions; see Figure 5 for explanation of how such path conditions are computed. Calculating path conditions leads to path conditions f and f′. One can then solve the formula f ∧ ¬f′ to find test input t′ that follows the same path as t in the previous program version and a different path in the current program version. The execution of t′ in the current program version P′ can then be compared with the execution of the failing test t in current version P′ in terms of differences in their control flow. That is, the behavior of t′ in cur-

Figure 4. Symbolic execution tree.

Consider again the code fragment in Figure 2. Suppose input y is a symbolic input, with an unknown value of, say, α. In symbolic execution, 14 the store maps variables that may be concrete values or symbolic expressions. At an assignment, the store is updated with the evaluation of right-hand-side expression, which may be a symbolic expression. At a branch, if the decision involves a symbolic expression, both sides of the branch are executed in separate “threads,” with corresponding branch conditions taken into account.

At line 2, two threads of symbolic execution will be created. In the first, the environment e2T is [x =

0, z = 0, y = α;α > 0], and the other, e2F, is [x = 0, z = 0, y = α;α ≤ 0]; note we included the conditions encountered on the path thus far in the environment. These conditions appear following the semicolon (see also Figure 5.). Here is the symbolic execution tree for Figure 2

x;;  =;;  0,;;  z;;  =;;  0,;;  y;;  =;;  α;;;  ;;   x  =  0,  z  =  0,  y  =  α;  

α  >;;  0;;  

 y > 0 

x  =  0,  z  =  0,  y  =  α;  

α  ≤;;  0;;    ¬(y;;  >;;  0);;  

x  =  0,  z  =  2α,  y  =  α;  

α  >;;  0;;  

z=y* 2 

x  =  α-­‐ 2,  z  =  2α,  y  =  

α;  α >  0  

x=y-­‐ 2 

x  =  α-­‐ 4,  z  =  2α,  y  =  α;  

α  >;;  0;;  

x=x-­‐ 2 

x  =  0,  z  =  0,  y  =  α;  

α ≤  0  

z==;;  x;;  

x  =  α-­‐ 4,  z  =  2α,  y  =  α;   α  >;;  0;;  ∧ 2α  ==;;  α-­‐ 4;;  

 z;;  ==x;;  

x  =  α-­‐ 4,  z  =  2α,  y  =  α;  

α >;;  0∧ 2α !=;;  α-­‐ 4;;  

 z != x 
e2T e2F
e2T,6T e2T,6F
…;;  
…;;  
…;;  

At line 6, e2T forks into: e2T,6T and e2T,6F. e2T, 6 T will be [x = α – 4, z = α 2, y = α;α > 0 ∧ α – 4 = α 2], which will be discarded since the condition is unsatisfiable.

Symbolic execution tree construction is similar to the program formula construction in Figure 2. For this reason, it is also called “static symbolic execution.” The difference is, in program formula, threads were merged with control-flow join points, whereas in symbolic execution tree, there is no merging.

Figure 5. Illustration of path conditions.

Consider yet again the program in Figure 2. Suppose we want to find the path condition of the only way to reach the error statement, or the path ⟨ 1, 2, 3, 4, 5, 6, 8, 9⟩. We traverse for ward along the sequence of statements in the given path, starting with a null formula and gradually build it up. All variables start with symbolic values. At any point during the traversal of the trace, we maintain an assignment store and a logical formula. The result is

˲ For every assignment, we update the symbolic assignment store; and

˲ For every branch, we conjoin the branch condition—or its converse if the branch is not taken— with the path condition; while doing so, we use the symbolic assignment store for every variable appearing in the branch condition.

At the end of the path, the logical formula captures the path condition. For the example path

⟨ 1, 2, 3, 4, 5, 6, 8, 9⟩ in the given program, the path condition can be calculated as shown in the table here. Whenever the input satisfies y > 0∧2y ≠ y – 4∧2y > y – 4, the program execution will trace exactly this path.

Assignment store

1

2

3

4

5

6

8

9

Logical Formula
Note this form of symbolic execution is similar to the one in Figure 4; the difference is one path
is already given here, so there is no execution tree to be explored. This is sometimes also called
“dynamic symbolic execution.”