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/11 10:47] vkuncak |
sav08:forward_symbolic_execution [2015/04/21 17:30] (current) |
||
---|---|---|---|
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: |
- | \[ | + | \begin{equation*} |
x = e_x \land y = e_y \land P | x = e_x \land y = e_y \land P | ||
- | \] | + | \end{equation*} |
where $e_x$ is term describing symbolic state of $x$ and $e_y$ describes symbolic state of $y$. The remaining part of the formula $R$ is given in //path condition// $P$. It is a conjunction of all branch conditions up to current program point. We require $P$ to be expressed only in terms of $x_0,y_0$, not $x,y$. | where $e_x$ is term describing symbolic state of $x$ and $e_y$ describes symbolic state of $y$. The remaining part of the formula $R$ is given in //path condition// $P$. It is a conjunction of all branch conditions up to current program point. We require $P$ to be expressed only in terms of $x_0,y_0$, not $x,y$. | ||
Line 29: | Line 29: | ||
++++What should it do when encountering assert(F)? | ++++What should it do when encountering assert(F)? | ||
|Generate proof obligation | |Generate proof obligation | ||
- | \[ | + | \begin{equation*} |
\forall x,y.\ ((\exists x_0,y_0.R(x_0,y_0,x,y)) \rightarrow F(x,y)) | \forall x,y.\ ((\exists x_0,y_0.R(x_0,y_0,x,y)) \rightarrow F(x,y)) | ||
- | \] | + | \end{equation*} |
that is, check the validity of $R \rightarrow F$. | that is, check the validity of $R \rightarrow F$. | ||
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 55: | Line 56: | ||
++++How does this follow from relation composition?| | ++++How does this follow from relation composition?| | ||
- | \[ | + | \begin{equation*} |
\{((x0,y0),(x,y)) \mid (x = e_x \land y = e_y \land P)\} \circ \{ ((x,y),(x',y') \mid x' = f(x,y) \land y' = y \} | \{((x0,y0),(x,y)) \mid (x = e_x \land y = e_y \land P)\} \circ \{ ((x,y),(x',y') \mid x' = f(x,y) \land y' = y \} | ||
- | \] | + | \end{equation*} |
- | \[ | + | \begin{equation*} |
\{((x0,y0),(x',y')) \mid \exists x,y. (x = e_x \land y = e_y \land P \land x' = f(x,y) \land y' = y \} | \{((x0,y0),(x',y')) \mid \exists x,y. (x = e_x \land y = e_y \land P \land x' = f(x,y) \land y' = y \} | ||
- | \] | + | \end{equation*} |
- | \[ | + | \begin{equation*} |
\{((x0,y0),(x',y')) \mid (x' = f(e_x,e_y) \land y' = e_y \land P \} | \{((x0,y0),(x',y')) \mid (x' = f(e_x,e_y) \land y' = e_y \land P \} | ||
- | \] | + | \end{equation*} |
- | \[ | + | \begin{equation*} |
\{((x0,y0),(x,y)) \mid (x = f(e_x,e_y) \land y = e_y \land P \} | \{((x0,y0),(x,y)) \mid (x = f(e_x,e_y) \land y = e_y \land P \} | ||
- | \] | + | \end{equation*} |
++++ | ++++ | ||
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 89: | Line 90: | ||
assert(F(x,y)) | assert(F(x,y)) | ||
emit proof obligation: | emit proof obligation: | ||
- | \[ | + | \begin{equation*} |
(x = e_x \land y = e_y \land P) \rightarrow F(e_x,e_y) | (x = e_x \land y = e_y \land P) \rightarrow F(e_x,e_y) | ||
- | \] | + | \end{equation*} |
and change the state: | and change the state: | ||
x := x_k (fresh) | x := x_k (fresh) | ||
Line 153: | Line 154: | ||
===== 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]] |