Forward Symbolic Execution
Can be used for
- verification condition generation
- executing programs
- testing, bug finding
- proving programs correct (if extended with techniques for loop invariants)
Generalize an interpreter to work with symbolic instead of concrete values.
Assume the set of variables .
Symbolic execution maintains a formula describing the relation between the initial state and the current state.
Exploiting Analogy with Execution
Maintain symbolic state formula in the following normal form:
where is term describing symbolic state of and describes symbolic state of . The remaining part of the formula is given in path condition . It is a conjunction of all branch conditions up to current program point. We require to be expressed only in terms of , not .
Postcondition at current program point is .
If condition ever becomes contradictory, relation is empty and symbolic execution can stop (path is unreachable).
Special case: if initial condition specifies values of variables, then we know which branch to enter.
Symbolic Execution Rules
We derive these rules from semantics, taking into account the definition of R in terms of e_x,e_y,P.
x = f(x,y)
e_x := f(e_x,e_y)
P := P & F[x<-e_x, y<-e_y]
e_x := x_k
where x_k is a fresh variable.
emit proof obligation:
and change the state:
x := x_k (fresh) y := y_k (fresh) P := F
Handled implicitly: execute statements one by one.
Execute both branches and collect proof obligations from both branches.
Exponential explosion remedy:
- work on control-flow graph
- merge symbolic states when edges merge
Merging: Given two symbolic states:
x = e_x1 & y = e_y1 & P1 x = e_x2 & y = e_y2 & P2
generate a single symbolic state
x = x_k & y = y_k & P
where P is ((x_k = e_x1 & y_k = e_y1 & P1) | ((x_k = e_x2 & y_k = e_y2 & P2)
Then we continue only from this one state.
If the first statements are
assume (x=0) assume (x=1)
Then symbolic execution knows the exact values and can work as an interpreter.
Here we generate real counterexamples (underapproximation), we compute smaller relation than one given by program semantics.
If there are no loop invariants, we can still execute program on concrete inputs. For symbolic initial state (e.g. giving upper bound of loop) execution need not terminate.
- Bounding depth: stop executing for paths longer than some value
- Bounding state: small integer width, small number of objects in heap
- Loop unrolling: replace loop( c ) with cc;cc;c;c for some number of times
- Instantiating values: find a satisfying assignment for R, take value v of x in it and replace e_x with v (moves towards concrete execution)
In this case we compute overaproximation, bigger relation than the actual relation given by program semantics.
- do not maintain exact expressions for variables, but only whether they are positive
- maintain only linear or certain polynomial constraints - if actual constraints are more complex, keep only the polynomial constraints that are guaranteed to hold
Why we approximate we can obtain
- termination even for programs that have loops
- useful information about the program (not exactly all information that we are interested in, depends on the approximation)
- Lori Clarke and Debra Richardson: Symbolic Evaluation Methods for Program Analysis, in Program Flow Analysis: Theory and Applications, Prentice-Hall 1981.