Generalized Symbolic Execution

Question

Explain the term Generalized Symbolic Execution?

Answer 1

Generalized Symbolic Execution: Using symbolic execution for test input generation is a well-known approach, but typically only handles sequential code with simple data. In (Khurshid, Pasareanu, and Visser 2003; Pasareanu and Visser 2004), this technique has been extended to support advanced constructs of modern programming languages, like Java and C++. The approach handles dynamically allocated structures, arrays, as well as concurrency.

The algorithm begins execution of a technique on inputs with uninitialized fields and uses lazy initialization to assign values to such fields; that is, it initializes fields whenever they are first accessed during the method's symbolic execution. This permits symbolic execution of methods without requiring an a priori bound on the number of input objects. Whenever the execution accesses an uninitialized reference field, the algorithm non-deterministically initializes the field to null, to a reference to a new object with uninitialized fields, or to the reference of an object created throughout a prior field initialization; this systematically treats aliasing. When the execution accesses an uninitialized primitive (or string) field, and the algorithm first initializes the field to a new symbolic value of the appropriate type and then the execution proceeds.

When a branching condition on primitive fields is evaluated, the algorithm non-deterministically adds the condition or its negation to the corresponding path condition and checks the path condition's satisfiability using an “off-the-shelf” decision procedure. If the path condition becomes infeasible, the current execution terminates (i.e., the algorithm backtracks).

The approach applies both to (executable) models and to code. It generates an optimized test suite for flexible/user specified criteria, while it checks for errors during test generation. Moreover, it uses method pre-conditions (if available) to generate only test inputs that satisfy these preconditions.

Our symbolic execution framework is built on top of the JPF model checker. It explores the symbolic execution tree of the analyzed program, using its usual state space exploration techniques. Essentially, a state includes a heap configuration, a path condition on primitive fields, and thread scheduling. Whenever a path condition is updated, it is checked for satisfiability using an appropriate decision procedure, like the Omega library (Omega website) for linear integer constraints. If the path condition is unsatisfiable, the model checker backtracks. The framework can be used for test input generation and for finding counterexamples to safety properties. Model checking lends itself to test input generation, since one simply writes as a set of (temporal) properties that say that some coverage cannot be achieved and the model checker will find counterexamples and associated path conditions, if they exist, that encode program paths that achieve the stated coverage goal. The path conditions are solved to obtain the actual test inputs.