This is an old revision of the document!
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)
Basic Ideas
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:
\[
x = e_x \land y = e_y \land P
\]
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
.
Checking Assertions
Postcondition at current program point is .
Branch Pruning
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.
Assignment
Assume
Given
assume(F)
change state:
P := P & F
Havoc
Given
havoc(x)
change state:
e_x := x_k
where x_k is a fresh variable.
Assert
Given
assert(F(x,y))
emit proof obligation: \[
(x = e_x \land y = e_y \land P) \rightarrow F(e_x,e_y)
\] and change the state:
x := x_k (fresh) y := y_k (fresh) P := F
Sequential composition
Handled implicitly: execute statements one by one.
Non-deterministic choice
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.
Execution
If the first statements are
assume (x=0) assume (x=1)
Then symbolic execution knows the exact values and can work as an interpreter.
Underapproximations
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 c[]c;c[]c;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)
Overaproximation
In this case we compute overaproximation, bigger relation than the actual relation given by program semantics.
Examples:
- 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
- useful information (not exactly all information that we are interested in, depends on the approximation)
References
- Symbolic execution and program testing by James C. King
- Lori Clarke and Debra Richardson: Symbolic Evaluation Methods for Program Analysis, in Program Flow Analysis: Theory and Applications, Prentice-Hall 1981.