-Dynamic symbolic execution, or concolic execution, is a program testing technique that systematically executes a program with the aim of exploring all feasible program paths, and locating and reporting all errors encountered in these paths. However, as the complexity of the program grows, the number of program paths explodes, making it infeasible for concolic testers to explore all of them. To reduce the number of paths to explore, several concolic testing tools have recently started employing static analysis to prune paths guaranteed by the static analysis to be safe. The concolic tester must then only focus on those paths that might contain an error, as reported by the analysis. However, due to imprecisions in the analysis' result, the reported errors may just be false positives, and it is up to the tester to verify whether a reported alarm is an actual error or merely a false positive. In this position paper, we propose to increase the precision of these analyses by not only performing an initial static analysis before starting concolic testing of the program, but also by launching incremental static analyses over the program at run time, and incorporating into the analyses run-time information observed by the tester. The increased precision that results from incorporating such run-time information should enable further pruning of the program paths that must be explored by the concolic tester. Index Terms-Concolic Testing, Static Analysis, Blended Analysis
In recent years, there has been an interest in blending static
and dynamic analyses to combine the best of both worlds. The
results of a sound static analysis over-approximate all possible
program executions, at the cost of precision. The results of
a dynamic analysis are precise, yet only valid for a subset
of all program executions. In this position paper, we propose
a novel mechanism to blend an abstract interpretation-based
static analysis [
The remainder of this paper is organized as follows. Section II introduces the concept of run-time static analysis. Section III gives an introduction to concolic execution and explains how a concolic tester may benefit from (run-time) static analysis. Section IV briefly describes an implementation of a prototype of this technique. Section V concludes.
Our proposed technique focuses on the abstracting abstract
machines (AAM) technique, developed by Van Horn and
Might [
Our run-time static analysis technique builds on the close relationship between the interpreter and its derived static analysis. All run-time information on the program’s execution is encoded in the concrete machine’s program state. This information is made available to the analysis by abstracting the program state in a similar manner as the abstraction of the machine itself. In general, this technique therefore first involves executing a program and observing the interpreter’s concrete program state. When an external client decides to commence static analysis, the concrete state is abstracted, and the abstract interpreter is initialized with this abstract state and runs until it reaches a fixpoint. Figure 1 illustrates how the run-time information enables refining static analysis. As the predicate depicted in Figure 1a involves a variable with a random value, the flow graph (1b) computed by a traditional static analysis must contain both branches. However, should our run-time static analysis technique be launched after binding the variable r to its evaluated value, and before evaluating the predicate’s value, the run-time analysis has the variable’s value available, and can produce a flow graph (1c) that precisely predicts the (let ((r (random 10))) (if (> r 5)) (then) (else))) (a) (let ((r (random 10))) (if (> r 5)) (then) (else))) (if (> r 5)) (then) (else)) (then)
(else) (b) (if (> r 5)) (then) (else)) (then) (c) branch to be be taken. Such a run-time analysis only soundly predicts the future execution given the current execution of the program. Should the program be restarted, a different value for r may be generated, thus invalidating the result of the run-time analysis.
A concolic tester iteratively explores all feasible paths in
a program by manipulating the values of input parameters to
the program, such as program arguments, random numbers,
values that are read from files etc. [
In the first iteration, the tester assigns a random value to these input parameters while simultaneously collecting all conditional predicates it encounters into a path constraint that symbolically represents the conditions that must be true in order for the program to execute that particular path. After completing the first run of the program, a part of the path constraint is negated and the resulting path constraint is given to a SMT solver. If the solver can find some value for the input parameters so that this new path constraint is satisfied, concolic testing continues by restarting the program and assigning these newly computed values to the input parameters. This process continues until all feasible program paths have been explored, or until the tester exceeds some given time constraint.
We illustrate the working of a concolic tester in more detail via the example Scheme program depicted in Figure 2. In this program, the variables a and b are considered input parameters. Hence, they are symbolically represented as the input variables a0 and b0. Suppose now that in the first iteration, the concolic tester randomly assigns 67 to a and 31 to b. These values cause the concolic tester to execute the program statement on line 8, at which point the tester reports the error encountered there. Simultaneously with this concrete execution, the tester also collects the symbolic representation of the conditional predicates that were encountered at line 5 and 6, into a so-called path constraint, i.e., a0 > 50 ^ b0 <= a0+b0. After completing this run, the tester attempts to explore another path, such as the path leading to the program statement at line 7. To do this, the solver negates the last conditional predicate in the path constraint, resulting in the constraint a0 > 50 ^ b0 > a0 + b0 and feeds this resulting path to a SMT solver, which subsequently attempts to assign values to a0 and b0 so that the resulting path constraint is true. Note that, as a0 is guaranteed to be a positive number, the second conjunct b0 > a0 + b0 can never be true. Hence no values for a0 and b0 can be found so that the constraint is satisfied. The concolic tester thus concludes that the constraint is unsatisfiable and that the program statement at line 7 is unreachable. At this point, the concolic tester backtracks further into the execution and tries to negate the first conjunct in the path constraint, resulting in the new constraint a0 <= 50, and attempts to solve this constraint, for example by assigning the value 0 to a0. The concolic tester re-executes the program and assigns the value 0 to a. It completes the program by reaching the expression at line 9. As no new branches were encountered by the tester during this last run, the tester concludes that it has explored all feasible program paths and concolic testing terminates. The three path constraints that were constructed can be collected in a symbolic execution tree that represents all possible executions of the program, as shown in Figure 3. A. Combining Static Analysis and Concolic Testing
The number of program paths is exponential in the number
of conditional branches of the program. As it is therefore
often infeasible for concolic testers to explore more than a
fraction of all possible program paths in a real-world
application, testers employ sophisticated search strategies to select
a program path that can be explored and that is most likely
to result in a non-trivial error [
Consider the program listed in Figure 4 and its abstract state graph, produced by performing a simple initial static analysis over this program before starting concolic testing, in Figure 5. It can be seen from the state graph that the analysis considers the path where a is not larger than 5 to be safe, the path where both a and b are larger than 5 to be unsafe, and the path where a is larger than 5 but b is not to be potentially unsafe. The conclusion for this last path is due to imprecision that arose in the static analysis: if we employ e.g., a very simplebut-fast constant propagation analysis that does not precisely track reassignments to variables, such as the reassignment to the function h at line 7, then the analysis cannot conclude that calling h at line 10 is safe. As a result, any concolic tester relying on this analysis can only prune the first path and must still explore the other two paths.
B. Combining Run-time Static Analysis and Concolic Testing
The safe path where h is called can be pruned by employing a run-time static analysis, in combination with an initial static analysis performed before starting testing of the program. If the tester starts exploring the error path that results in the call to f at line 9, the tester could launch a run-time static analysis at line 7, after the reassignment to h but before the paths to the calls of f and h are split. At this point, the run-time analysis can incorporate the knowledge that h equals the safe function g, thereby avoiding the imprecision caused by the reassignment of h at line 7. In this case, the abstract state graph produced by the run-time analysis, as depicted in Figure 6, is precise enough to determine that calling h will not result in an error, hence this path should not be explored by the tester. In general, a run-time analysis could be launched over the program when the tester has reached a common ancestor node to two or more paths that are potentially unsafe, in the hope that the run-time information available at that point enables the static analysis to be precise enough to determine whether or not any of the potentially unsafe paths can be pruned.
We have implemented a prototype of this technique1 in the
Scala-AM framework [
We have proposed a novel technique for improving precision of a static analysis at run time, using run-time information on the program’s execution. We propose to couple this technique to a concolic tester, to reduce the number of program paths that the tester must explore.
prototype at https://github.com/mvdcamme/scala-am/tree/concolic