• English only

# Differences

This shows you the differences between two versions of the page.

 sav08:forward_symbolic_execution [2009/03/11 12:44]philippe.suter sav08:forward_symbolic_execution [2015/04/21 17:30] (current) Both sides previous revision Previous revision 2009/03/11 14:35 vkuncak 2009/03/11 12:44 philippe.suter 2009/03/11 10:48 vkuncak 2009/03/11 10:47 vkuncak 2009/03/11 10:46 vkuncak 2009/03/10 23:00 vkuncak 2009/03/10 22:54 vkuncak 2009/03/10 22:53 vkuncak 2009/03/10 22:49 vkuncak 2008/04/09 10:24 vkuncak 2008/04/09 10:22 vkuncak 2008/03/10 17:55 pedagand 2008/03/10 17:53 pedagand 2008/03/06 19:02 vkuncak created Next revision Previous revision 2009/03/11 14:35 vkuncak 2009/03/11 12:44 philippe.suter 2009/03/11 10:48 vkuncak 2009/03/11 10:47 vkuncak 2009/03/11 10:46 vkuncak 2009/03/10 23:00 vkuncak 2009/03/10 22:54 vkuncak 2009/03/10 22:53 vkuncak 2009/03/10 22:49 vkuncak 2008/04/09 10:24 vkuncak 2008/04/09 10:22 vkuncak 2008/03/10 17:55 pedagand 2008/03/10 17:53 pedagand 2008/03/06 19:02 vkuncak created Line 18: Line 18: Maintain symbolic state formula $R(x_0,​y_0,​x,​y)$ 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 56: 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 90: 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 154: 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]]