Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
sav08:forward_symbolic_execution [2009/03/10 22:54] vkuncak |
sav08:forward_symbolic_execution [2009/03/11 14:35] vkuncak |
||
|---|---|---|---|
| Line 17: | Line 17: | ||
| === Exploiting Analogy with Execution === | === Exploiting Analogy with Execution === | ||
| - | Maintain symbolic state formula $R(x_0,x)$ in the following normal form: | + | Maintain symbolic state formula $R(x_0,y_0,x,y)$ in the following normal form: |
| \[ | \[ | ||
| x = e_x \land y = e_y \land P | x = e_x \land y = e_y \land P | ||
| Line 42: | Line 42: | ||
| Special case: if initial condition specifies values of variables, then we know which branch to enter. | Special case: if initial condition specifies values of variables, then we know which branch to enter. | ||
| + | |||
| ===== Symbolic Execution Rules ===== | ===== Symbolic Execution Rules ===== | ||
| Line 74: | Line 75: | ||
| assume(F) | assume(F) | ||
| change state: | change state: | ||
| - | P := P & F | + | P := P & F[x<-e_x, y<-e_y] |
| === Havoc === | === Havoc === | ||
| Line 120: | Line 121: | ||
| Then we continue only from this one state. | Then we continue only from this one state. | ||
| + | ===== Execution ===== | ||
| - | ===== Underapproximations ===== | + | If the first statements are |
| + | assume (x=0) | ||
| + | assume (x=1) | ||
| + | Then symbolic execution knows the exact values and can work as an interpreter. | ||
| - | We next consider testing and debugging applications. | ||
| - | These can generate real counterexamples (underapproximation) as opposed to providing proofs (overapproximations). | + | ===== 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. | 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 path | + | * Bounding depth: stop executing for paths longer than some value |
| * Bounding state: small integer width, small number of objects in heap | * Bounding state: small integer width, small number of objects in heap | ||
| - | * Loop unrolling: replace loop( c ) with c;c;c for some number of times | + | * 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) | * 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 even for programs that have loops | ||
| + | * useful information about the program (not exactly all information that we are interested in, depends on the approximation) | ||
| ===== References ===== | ===== References ===== | ||
| - | * [[http://doi.acm.org/10.1145/360248.360252|Symbolic execution and program testing]] by James C. King | + | * [[http://doi.acm.org/10.1145/360248.360252|Symbolic execution and program testing]] by James C. King ({{sav08:king76symbolicexecution.pdf|pdf}}) |
| * Lori Clarke and Debra Richardson: Symbolic Evaluation Methods for Program Analysis, in Program Flow Analysis: Theory and Applications, Prentice-Hall 1981. | * Lori Clarke and Debra Richardson: Symbolic Evaluation Methods for Program Analysis, in Program Flow Analysis: Theory and Applications, Prentice-Hall 1981. | ||
| * [[http://www.cs.utexas.edu/users/sandip/publications/symbolic-lpar/main.html|Verification Condition Generation via Theorem Proving]] | * [[http://www.cs.utexas.edu/users/sandip/publications/symbolic-lpar/main.html|Verification Condition Generation via Theorem Proving]] | ||
| * [[http://osl.cs.uiuc.edu/~ksen/cute/|CUTE Tool]] | * [[http://osl.cs.uiuc.edu/~ksen/cute/|CUTE Tool]] | ||