Concolic testing is a well-known unit test generation technique. However, bottlenecks such as constraint solving prevents concolic testers to be used in large projects. We propose a modification to a standard concolic tester. Our modification makes more but smaller queries to the constraint solver, i.e. ignores some path conditions. We show that it is possible to reach the same branch coverage as the standard concolic tester while decreasing the burden on the constraint solver. We support our claims by testing several C programs with our method. Experimental results show that our modification improves runtime performance of the standard concolic tester in half of the experiments and results in more than 5x speedup when the unit under test has many infeasible paths.
Software testing is an important but resource consuming part of software development process.
According to a study in 2005, 79% of Microsoft developers write unit tests [
We propose a modification to the input generation method of concolic testing, called Incremental
Partial Path Constraints (IPPC). A standard concolic tester instruments the unit under test (UUT) to
collect operations that either affect or depend on symbolic variables during a concrete execution. This
sequence of operations is called an execution trace. A concolic tester symbolically reexecutes the
execution trace to generate path conditions that solely depend on the symbolic variables. Then, the concolic
tester negates the last path condition that is not negated before. At the final step, constraint solver is
called only once with all path conditions to generate a new input vector. As noted in [
This paper makes two contributions. First, we propose an input generation strategy based on partial
path constraints, called IPPC and incorporate our strategy into a standard concolic testing algorithm.
Partial path constraints contain a subset of path conditions of an execution trace. Second, we implement
our modification using the CREST tool [
We illustrate our approach on a small example in the next section. In section 4, we describe our approach in detail. We present our experimental results in section 5. We discuss the related work in section 3 and conclude in section 7. 2
In this section, we run both the standard concolic tester and IPPC on a small program unit which checks if three numbers are sorted or not, denoted by isSorted(a, b, c). The control-flow graph of the unit under test (UUT) is given in Figure 1.
Figure 2 shows an execution of the standard concolic testing algorithm on isSorted(a, b, c). A standard concolic tester starts from an arbitrary input ([0; 0; 0] in this case), executes the UUT using the input values. The concolic tester collects the execution trace of this concrete execution and generates the path constraint p0 = [a b; a c; b c]. The last condition of p0 is negated and we get p1 = [a b; a c; b > c]. We invoke the constraint solver with p1, denoted as CS(3), where 3 represents the number of path conditions in p1. We get [0; 1; 0] as the new input from the constraint solver. We execute the program with new inputs and collect the path constraint p2 = [a b; a c; b > c]. Now, we negate the second condition of p2 and remove all conditions after the second condition and get p3 = [a b; a > c]. We explain the reasons to exclude path conditions that come after the negated condition in Section 4.2. We get [0; 1; 1] by invoking CS(2). Concrete execution of the program results in p4 = [a b; a > c]. Then, we negate the only remaining path condition and get p5 = [a > b] after removing the last condition. CS(1) generates [2; 1; 1]. The concolic tester stops generating test inputs after executing the program since the resulting path constraint p6 = [a > b] has no path condition that is not negated before. At the [collected] [generated]
[CS(3)] [collected] [generated]
[CS(2)] [collected] [generated]
[CS(1)] [collected] [Path Exhaustion] end, we have invoked the constraint solver three times with an average path constraint length of two.
Figure 3 illustrates the execution of our IPPC algorithm on isSorted(a, b ,c). In this case, each time we generate a new path constraint, we do not immediately call the constraint solver. We define the constraint obtained by executing the program a full path constraint. We generate a subset of the full path constraint, f 0, which we call a partial path constraint. Partial path constraint f 0 is initialized as an array which contains only the negated path condition. Partial path constraint generation phase is called overapproximation. We call the constraint solver with f 0. In case the constraint solver does not generate an input which satisfies p, we add the remaining path conditions of p to f 0 and generate larger path constraints such as f 1, f 2 etc. until the constraint solver generates an input that satisfies p. For our example, we only made three calls to the constraint solver with average constraint length of one. 3
The idea of incremental constraint solving for concolic testing is as old as concolic testing itself and
suggested along with CUTE, one of the first concolic testing tools [
Solving only a subset of path conditions instead of the whole path constraint is an approach recently
used in finding integer overflows [
All concolic testers require a constraint solver. Z3 and Yices are commonly used constraint solvers b; a b; a c; b f30 = [a > c] f50 = [a > b] i4 = [2; 1; 0] i4 satisfies p5 [collected] [generated]
[CS(1)]
[collected] [generated] [CS(1)]
[collected] [generated] [overapproximation] [CS(1)]
[collected]
[
Concolic testing is not restricted to sequential programs. There are concolic testers which test
concurrent software [
Many concolic testers (e.g. CUTE) use bounded depth first search (bDFS) instead of bounding
the number of iterations as in IPPC and CREST [
Random branch selection (RND) is an approach introduced in CREST [
Control flow directed search (CFG) is a search strategy which guides the search using the static
structure of the UUT. CFG assigns weights to edges of the control flow graph of the UUT and calculates
distances to each unvisited branch. Then, CFG solves a path constraint which leads to the unvisited
branch with the least distance to the current execution trace [
A recent study on CREST proposes a new search strategy, called DYNASTY, which uses the control
flow graph of the UUT to guide the search as in CFG technique [
4.1
Background We have previously stated that a concolic tester generates path conditions from an execution trace of the UUT. We define the following using this fact: Definition 1. A path condition is a function of symbolic variables to fT; Fg.
Definition 2. An input vector is an assignment to all symbolic variables of UUT.
Definition 3. A full path constraint is an array whose elements form a set of path conditions. Definition 4. Any array whose elements form a subset of the elements of the full path constraint is called a partial path constraint.
Definition 5. An input vector is said to satis f y a path constraint if and only if the input vector makes all conditions of the path constraint T .
Conjunction of all conditions in a partial path constraint is an overapproximation of conjunction of all conditions in the full path constraint. Therefore the process of generating partial path constraints from full path constraints is called an overapproximation.
Definition 6. An algorithm which takes a path constraint and returns an input vector which satisfies that constraint is called a constraint solver. If there exists no such input vector, it returns null.
We used the Yices constraint solver, which is the default solver in CREST [
Algorithm Design of IPPC We implemented IPPC on top of CREST’s standard concolic testing algorithm (denoted by DFS) as shown in Algorithm 1. We initially give nIterations 0, TestInput random input and TestInputs 0/ . We can see from line 1 that the algorithm is bounded by the maximum number of iterations. At line 2, we check the input vector because constraint solver is assumed to return null if an input vector can not be generated, i.e. given path constraint is infeasible. We increment iterations only if the path constraint is satisfiable. At line 4, we execute UU T with input and save the full path constraint of the execution trace as p. Lines 8 and 9 ensure that the algorithm performs a depth first search (DFS). We always negate the last unvisited condition of a path constraint. If there exists no path condition that is not negated before, we stop because all paths are executed. At line 11, constraintSolver takes a path constraint and returns a satisfying input vector. We don’t terminate the solver, we use it in it’s built-in incremental mode. Notice that we exclude the path conditions which come after the negated path condition. Any input vector which satisfies path conditions up to the negated path condition must generate the same execution trace input : uut (unit under test) maxIterations testInput testInputs nIterations output: testInputs end for i sizeOf(p) 1 to 0 do if !isNegatedBefore(p[i]) then setNegatedBefore(p[i]); p[i] :p[i]; testInput constraintSolver(fp[0]:::p[i]g); return crest(uut, maxIterations, testInput, testInputs, nIterations);
Algorithm 1: Concolic Testing Algorithm Implementing DFS with Maximum Iterations (CREST) up to the occurrence of the negated path condition. Negated path condition will force the program to a different execution trace. So, path conditions coming after the negated condition is not a part of the new execution trace and therefore should be removed. If the unnecessary path conditions are not excluded, they may cause false path constraint infeasibilities. False infeasibilities force the concolic tester not to generate any input vector for the path constraint and therefore cause a decrease in test coverage.
IPPC is exactly the same as Algorithm 1 except we replace line 11 with input IPPC Solve (UU T; fp[0]:::p[i]g; fp[i]g). We describe IPPC Solve in Algorithm 2. We keep the solver running in incremental mode.
Line 1 of Algorithm 2 invokes the constraint solver with f . If the constraint solver is unable to generate an input vector, we conclude that the full path constraint is also infeasible and return null. We prove the infeasiblity of a full path constraint given the infeasibility of a partial path constraint in Theorem 1. The for loop starting at line 5 checks if the input vector satisfies the full path constraint. If input satisfies p, we can return input. If not, we learn the unsatisfied path condition by adding it to f and generate a new input vector. This process may be continued until f = p in the worst case where either an input can be generated or p is infeasible given that the constraint solver is sound (if exists, returns a correct test input) and complete (terminates and is correct for all cases). This worst case condition is rare or non existent at least in our experiments. 4.3
Correctness and Completeness To be able to produce readable proofs, we assume all boolean operations on a path constraint are performed on the conjunction of all conditions of the path constraint.
input : uut (unit under test) p (full path constraint) f (partial path constraint) output: testInput 1 testInput constraintSolver(f ); 2 if testInput = null then 3 return null; 4 end 5 for i 0 to sizeOf(p) 1 do 6 if !sat(testInput; p[i]) then 7 append(f ; p[i]); 8 return IPPC Solve (uut, p, f );
end 9 10 end 11 return testInput;
Algorithm 2: IPPC Solve
isfiable.
Proof. Since f is unsatisfiable, :f is valid. Since f is an overapproximation of p, p ! f by definition. Therefore by modus tollens, :p is valid. In other words, p is unsatisfiable.
We now show the correctness of IPPC Solve. We change only one line in Algorithm 1. Therefore, to prove the correctness of IPPC, we only need to ensure that for all path constraints, IPPC Solve generates an input vector that has the same property as the input vector generated by the constraint solver. If such an input vector exists, a constraint solver always generates an input vector that satisfies the full path constraint.
generates null. (b) Otherwise IPPC Solve always generates an input vector that satisfies the full path constraint.
Proof. Proof of (a) is trivial due to lines 1-4 of Algorithm 2. We can see from lines 5-10, that Algorithm 2 would not stop until the input vector satisfies the full path constraint. Therefore proof of (b) is trivial as well.
Proof. IPPC Solve is correct by Theorem 2. The second part of the proof is as follows. At any time, partial path constraint f is either (a) unsatisfiable, or an input vector i is generated. If an input vector i is generated, either (b) i satisfies p, or (c) we add a new path condition of full path constraint to f . If (a), IPPC Solve returns null and terminates. If (b), IPPC Solve returns i and terminates. If (c) happens N 1 times, where N denotes the number of path conditions in p, f $ p must hold. In other words, we build up the partial path constraint up to the full path constraint. In that case, the constraint solver must either generate null or generate a satisfying input vector, therefore the algorithm terminates.
2. CFG: Control flow directed testing algorithm. 3. RND: Random branch testing heuristic on top of the standard concolic testing algorithm. 4. IPPC: Our Incremental Partial Path Constraint algorithm.
1. Time elapsed: Time spent to test the UUT. 2. Total CS Calls: Total number of constraint solver calls made by the concolic tester. 3. Avg Const. Size: Average size of path constraints solved by the constraint solver. 4. Branch Coverage: Measurement of total branch coverage of UUT.
Concolic testing involves a degree of randomness due to the randomness of initial inputs. Therefore we performed 10 executions of each experiment and took average values of each measure. All of our experimental results can be found in Table 2.
Table 1 shows the program units we used in our experiments. Column KLOC represents the lines of code measured in thousands. Column #vars represents the number of symbolic variables.
We implemented five small benchmarks, gcd, bsort, sqrt, prime and factor to conduct our initial
experiments. gcd implements the binary greatest common divisor algorithm. We downloaded and
modified the bubble sort algorithm bsort, which sorts a given array of integers [
In our experiments, we used programs in different sizes. None of the given programs are too large in size so they can be tested in reasonable time without getting into scalability issues. In our experimental set, we argue that the structure of UUT is related to the performance of the testers that we use rather than the sizes of the programs. We observed that small programs such as factor can have very long runtimes (120 sec). We argue that IPPC will perform well not when the program is small or large, but when the program contains many infeasible paths. Although being small, prime and factor contain many infeasible paths. Although being large, grep and replace did not contain many infeasible paths.
We show all experimental results in Table 2. CFG method is not applicable to grep due to a bug in CREST, therefore we used N/A to denote the results we could not observe. We used 1000, 5000 and 10000 as the maximum number of iterations (#Itr) in experiments. We decreased #Itr for prime, factor, bsort and grep, since those units have few distinct execution traces. When there are few distinct execution traces and #Itr is too high, DFS and IPPC are able to stop before completing #Itr iterations, since they check if all execution traces are explored or not. However, CFG and RND have no such stopping condition and iterate #Itr times. So, if we kept #Itr high for prime, factor, bsort and grep, it would unfairly result in bad runtimes for CFG and RND.
We show the best algorithms for each benchmark in Table 3 where All Equal means all techniques are equally well. The column denoted as by Runtime First compares techniques by runtime first, if techniques have similar runtimes, compares branch coverages. The last column compares techniques by coverage first. DFS does not perform well in both columns. In terms of runtimes RND is the best and IPPC is the second. In terms of coverage CFG and IPPC are the best. Hence, IPPC performs well in both categories.
We next compare IPPC with DFS in more detail since IPPC is derived from DFS. We observe from Table 4 that there exists a correlation between Avg Const. Size of DFS / Avg Const. Size of IPPC and speedup of IPPC over DFS. When the gap between the constraint sizes of DFS and IPPC increases, the speedup of IPPC over DFS increases with the slight exception of grep. Similarly, Figure 4 shows that whenever the number of constraint solver calls (Total CS Calls) of DFS is close to the maximum number of iterations (#Itr), DFS works faster. If DFS makes many more calls than the number of iterations, IPPC works faster. Normally, DFS is expected to call constraint solver exactly once for each iteration. DFS makes more than one constraint solver call for an iteration only if the generated path constraint for that iteration is infeasible. In that case, DFS changes the path constraint and calls constraint solver repeatedly until a feasible path is found. We believe factor has the largest number of infeasibilities since DFS makes many constraint solver calls for few iterations. Figure 4 shows that the speedup of IPPC over DFS is above 5x when DFS generates four or more infeasible path constraints for each feasible path constraint (i.e. DFS makes more than five constraint solver calls for each iteration, #Itr=Total CS Calls of DFS < 0:2). Therefore, IPPC finds infeasibilities faster for all benchmarks.
In all experiments, the largest path constraint produced by IPPC had a length of 157, whereas the largest path constraints of DFS, CFG and RND had lengths of 2922, 1603 and 1391, respectively. We conclude that we eliminated the need for solving large path constraints to generate test inputs while keeping the runtimes fast and coverage high using IPPC.
We get exactly the same coverage results for both IPPC and DFS. We expect this since both algorithms perform a depth-first search. We argue that the coverage results being similar indicates that IPPC correctly does DFS on the UUT while improving the performance.
IPPC considers constraints that are 10x smaller than other techniques. We believe it is because that IPPC finds infeasibilities early, since most infeasibilities arise from a combination of few conditions in the constraint.
We assume that the constraint solver is sound, i.e. the constraint solver can find an input vector whenever
there exists an input vector which satisfies the path constraint. In general, this assumption is not valid.
We know that the constraint solver used in CREST, Yices [
The UUT can have intermediary variables calculated from symbolic variables and therefore can have path conditions on those intermediary variables. All path conditions that CREST returns are on the initial symbolic variables. Therefore, even if all branch conditions in the code may seem trivial, CREST may fail to generate correct inputs if variables are nonlinear (e.g. multiplication of two symbolic variables).
We assume the UUT to be sequential and deterministic, i.e. if an input vector i produces an execution trace e, i will always produce e for this UUT. However, for example a process which depends on random numbers could violate this assumption. We carefully chose the experiments so that we never violate these basic assumptions.
We assume the UUT is terminating, since if UUT halts, so does the tester as well. The test cases we chose and the test cases in previous work are all terminating.
We report runtimes that we acquired from a virtual environment. We got similar results on an host machine as well.
It is possible that IPPC may learn partial path constraints up to a point that they become full path constraints. So in the worst case, a standard concolic tester is more efficient than IPPC. However, our experimental results show that we require only a small portion of the full path constraint to generate input vectors belonging to the same equivalence class, i.e. input vectors which generate same execution traces when given to UUT. 7
In this paper, we designed a constraint solving strategy, called Incremental Partial Path Constraints (IPPC), which eliminates the need for solving large constraints to generate unit tests. We compared our design with other concolic testing algorithms in experiments. We observed that when there are many infeasible path constraints in a program, IPPC has more than 5x speedup over a standard concolic tester. We significantly reduce the number of path conditions required to generate an input vector and show that IPPC dominates other techniques in two of eight cases and has the best coverage levels in three of eight cases. We show that it is possible to reach high branch coverage while decreasing the burden on the constraint solver.
We believe that our constraint solving strategy contains room for improvement and shows promise for future work. The performance of IPPC on nonlinear path constraints (i.e. path constraints that contain at least one nonlinear path condition) or on concurrent software is an important question. Also, it is possible to further improve IPPC by input vector caching, i.e. trying the previously generated input vectors first to avoid calling constraint solver. We believe that our work sufficiently motivates further research on constraint solving strategies involving partial path constraints.