Loop constraints elimination

Loop constraints elimination performs when the following conditions hold:

1. the last constraint along the current path is a loop constraint, and

2. the wset of the corresponding loop statement does not intersect with the rset.

Loop constraints elimination will pop the constraints out until the branch of the second

Figure 13: Loop constraints elimination example function test()

Figure 14: Execution tree of function test()

Symbolic execution collects constraints along the execution path into a set S and systematically traverses all the execution paths in the test program by negate the last constraints in the set S, that is, symbolic execution traverses by depth first search. A loop constraint is a constraint that decides whether the loop statement should be executed. For example in Figure 13, the while loop statement is dependent on the constraint i < sym, and the constraint i < sym is a loop constraint. That is, it is a condition expression in loop statements. Figure 14 is an execution tree of the function test(). The nodes represent the condition expressions of while loop statement and if statement. The left edge of nodes

1 // sym and j are symbolic variables 2 test(){

3 while(i < sym){

4 if(j == 1){

5 //statements 6 }else{

7 //statements

8 }

9 } 10 }

i < sym

j == 1

i < sym

j == 1

i < sym

0 1

means the condition does not satisfy and represents by 0. The right edge of nodes means the condition satisfies and represents by 1. For example, if the while loop statement executes two iterations and the if statement j == 1 does not satisfy, then the execution path will be 1,0,1,0,0. and we say that there are three loop branch sets. The first set includes two nodes, one for the condition expression of the while loop statement, and one for the if statement.

The second set is as same as the first set. And the third set only includes one node which is the condition expression of the while loop statement. When the last constraint in the set S is a loop constraint and the intersection result of this execution is null, then we will pop the constraints out until the first loop branch set of this loop statement. For example in Figure14 the three nodes of the bottom will be popped out. And our system will try to negate the branch of the if statement in order to traverse all branches within or after loop statements.

The loop branches control the number of times of the loop iterations. If the intersection result of the corresponding loop statement in current execution is null, then we assume the loop iterations are independent with universal checks and we pops all branches until the first branch set of the loop iteration. By this method we reduce the number of times of iterations and universal checks, and we still can traverse all branches of if statements within or after the loop statement. Thus it can prevent from false negative due to lost collection of wset. If the west of the current loop statement intersects with rset then it implies that the number of times of this loop statement will affect the universal checks and the elimination will not perform.

Notice that the loop statements described in this paper are symbolic bounded, that is, the variable sym in the while statement in Figure13.is a symbolic value, and the number of times that the while statement should be executed in the traditional symbolic execution is bounded by the range of variable sym.

Figure 15: Special case of loop constraints elimination

Figure 15 is a special case, the if statement in line 3 is not satisfy in every iteration and it only satisfies in specific iteration. If we only pops out one loop branch set, there will be two situations: (1) the true branch in Figure 15 will not be traversed until the specific iteration.

(2) the worst case, the false negative may occurs due to lost collection of west.

One of the advantages of our loop constraint elimination strategy is the special case can be found and traversed quickly. By our strategy, if the loop can be reduced then the constraints will be reduced until the first loop branch set. And ALERT will try to negate the constraint of the if statement in line 3. Both branches of the if statement in line 3 will be traversed.

Figure 16: Loop constraint elimination algorithm

6 if(loop.wset != empty && loop.intersect == 0 && loop.begin == false){

7 pop until the first loop branch set;

8 is_loop_branch = loopbranchfind (loopbranchStack, current_branch);

9 }else

Figure 16 is the loop constraint elimination algorithm. In line 4 we first check if the current_branch is a loop branch. If false the loop constraint elimination will finish. If true we then check whether the elimination conditions are all satisfied in line 6. (1) the loop statement should be traversed. (2) the wset of this loop statement does not intersect with rset in the current execution. (3) it is not the first loop branch set because it is unnecessary to eliminate the first loop branch set. If the above conditions are all satisfied then the loop branch sets will be popped until one loop branch set left. And the steps will perform on all loop statements.