19.3 Symbolic Testing

19.3 Symbolic Testing

The basic technique of executing a program with symbolic values can be applied much like program testing. The values of some variables are summarized to elements of a small set of symbolic values. For example, if analysis is concerned with misuse of pointers, values for a pointer variable might be taken from the set

Values of other variables might be represented by a constraint or elided entirely. Since the representation of program state may not include enough information to determine the outcome of a conditional statement, symbolic execution can continue down either or both branches, possibly accumulating constraints in the program state. Unlike formal program verification using symbolic execution, symbolic testing does not follow every possible program execution path until all representations of all possible program states have been visited. It may explore paths to a limited depth or prune exploration by some other criterion, such as a heuristic regarding the likelihood that a particular path is really executable and leads to a potential failure.

Symbolic testing is a path-sensitive analysis: We may obtain different symbolic states by exploring program paths to the same program location. Usually it is also at least partly context sensitive, exploring execution through different procedure call and return sequences. The combination of path and context sensitivity is a key strength of symbolic testing, which can produce a warning with a detailed description of how a particular execution sequence leads to a potential failure, but it is also very costly. Often the ways in which the values passed to a procedure can affect execution are limited, and it is possible to build up a model of a procedure's effects by memoizing entry and exit conditions. A new path need be explored only when symbolic execution encounters an entry condition that differs from previously encountered conditions. Models of unchanged portions of a system, including external libraries, can be retained for future analysis.

Specializing the analysis to detect only a few classes of faults, and exploring a sample of program execution paths rather than attempting to summarize all possible behaviors, produce error reports that are more precise and focused than those that could be obtained from an attempt to verify program correctness. Nonetheless, abstraction in the symbolic representation of program state can lead to situations in which an apparent program fault is not actually possible. For example, a failure that appears to be possible when a loop body is executed zero times may actually be impossible because the loop always executes at least once. False alarms degrade the value of analysis, and a developer or tester who must wade through many false alarms (expending considerable effort on manually checking each one) will soon abandon the static checking tool. It is particularly frustrating to users if the same false alarm appears each time a program is re-analyzed; an essential facility of any static checking tool is suppression of warnings that have previously been marked as false or uninteresting.

A symbolic testing tool can simply prune execution paths whose execution conditions involve many constraints, suggesting a high likelihood of infeasibility, or it may suppress reports depending on a combination of likelihood and severity. A particularly useful technique is to order warnings, with those that are almost certainly real program faults given first. It is then up to the user to decide how far to dig into the warning list.