Symbolic Execution and Separation Logic
What questions do you have? What questions does your neighbor have?
Announcements
Questions?
Review: A Verification-Condition Generator (VCGen)
\[ \begin{array}{rrl} \operatorname{vc}( \texttt{;}, \varphi_{\mathrm{post}}) & \mathrel{:=}& \varphi_{\mathrm{post}} \\ \operatorname{vc}( s_1 \mathbin{\texttt{;}} s_2 , \varphi_{\mathrm{post}}) & \mathrel{:=}& \operatorname{vc}(s_1, \operatorname{vc}(s_2, \varphi_{\mathrm{post}})) \\ \operatorname{vc}( x \mathrel{\texttt{=}}e , \varphi_{\mathrm{post}}) & \mathrel{:=}& [e/x]\varphi_{\mathrm{post}} \\ \operatorname{vc}( \mathbf{if}\;\texttt{(}e\texttt{)}\;s_1\;\mathbf{else}\;s_2 , \varphi_{\mathrm{post}}) & \mathrel{:=}& (e \Rightarrow\operatorname{vc}(s_1, \varphi_{\mathrm{post}})) \wedge (\neg e \Rightarrow\operatorname{vc}(s_2, \varphi_{\mathrm{post}})) \end{array} \]
Review: A VCGen for While
Let us write \(\operatorname{mod}(s)\) for the variables modified by statement \(s\).
\[ \begin{array}{l} \operatorname{vc}( \mathbf{while}_{\varphi_{\mathrm{inv}}}\;\texttt{(}e\texttt{)}\;s_1 , \varphi_{\mathrm{post}}) \quad \mathrel{:=} \\ \begin{array}{ll} \quad \varphi_{\mathrm{inv}}\;\wedge& \text{The loop invariant holds on entry.} \\ \quad\quad \forall \operatorname{mod}(s_1). & \text{Havoc the variables modified by the loop,} \\ \quad\quad\quad \varphi_{\mathrm{inv}}\Rightarrow& \text{except assuming the loop invariant.} \\ \quad\quad\quad\quad (e\Rightarrow\operatorname{vc}(s_1, \varphi_{\mathrm{inv}}) \;\wedge& \text{If the loop continues, the loop's effect preserves the invariant.} \\ \quad\quad\quad\quad \phantom{(}\neg e\Rightarrow\varphi_{\mathrm{post}}) & \text{Otherwise, if the loop exits, the post-condition is implied.} \\ \end{array} \end{array} \]
Review: An Example VC
\[ \begin{array}{l} \operatorname{vc}( \mathbf{while}_{\texttt{even}\texttt{(}\texttt{i}\texttt{)}}\;\texttt{(}e\texttt{)}\;\texttt{i} \mathrel{\texttt{=}}\texttt{i} \mathbin{\texttt{+}} \texttt{2} , \texttt{even}\texttt{(}\texttt{i}\texttt{)}) \colon \\ \begin{array}{ll} \quad \texttt{even}\texttt{(}\texttt{i}\texttt{)}\;\wedge& \text{The loop invariant holds on entry.} \\ \quad\quad \forall \texttt{i}. & \text{Havoc the variables modified by the loop,} \\ \quad\quad\quad \texttt{even}\texttt{(}\texttt{i}\texttt{)}\Rightarrow& \text{except assuming the loop invariant.} \\ \quad\quad\quad\quad (e\Rightarrow\texttt{even}\texttt{(} \texttt{i} \mathbin{\texttt{+}} \texttt{2}\texttt{)} \;\wedge& \text{If the loop continues, the loop's effect preserves the invariant.} \\ \quad\quad\quad\quad \phantom{(}\neg e\Rightarrow\texttt{even}\texttt{(}\texttt{i}\texttt{)}) & \text{Otherwise, if the loop exits, the post-condition is implied.} \\ \end{array} \end{array} \]
Symbolic Execution
Verification-Condition Generation and Symbolic Execution
What if we “symbolically executed” the program with store assertions?
Paths and Path Constraints
Along each path, we get a conjunction of path constraints to see if they imply the post-condition.
That is, we consider store assertions that are quantifier-free and in disjunctive normal form (with implicit existentials).
Hoare Logic: Forwards Assignment
\(\inferlab{EvalAssign}{ \rho \vdash e \Downarrow v }{ \rho \vdash x \mathrel{\texttt{=}}e \Downarrow \rho(x \leftarrow v) }\)
\(\inferlab{VerifyAssign}{ \phantom{\jhoare{}{}} }{ {} \vdash \{\varphi\}\; x \mathrel{\texttt{=}}e \;\{ \exists x_{\mathrm{old}}. x= [x_{\mathrm{old}}/x]e \wedge[x_{\mathrm{old}}/x]\varphi \} }\)
Stores
\[ \begin{array}{rrrl} \text{stores} & \rho& \mathrel{::=}& x \mapsto v \mid\circ \mid\rho_1 ,\rho_2 \\ \\ \text{first-order (symbolic) stores} & \varphi& \mathrel{::=}& e \mid\top \mid\varphi_1 \wedge\varphi_2 \mid\bot \mid\varphi_1 \vee\varphi_2 \\ && \mid& \varphi_1 \Rightarrow\varphi_2 \mid\neg\varphi_1 \mid\forall x.\varphi_1 \mid\exists x.\varphi_1 \\ \\ \text{separation (symbolic) stores} & \psi& \mathrel{::=}& x \mapsto\hat{e} \mid\mathsf{emp} \mid\psi_1 \ast\psi_2 \\ && \mid& \hat{e} \mid\top \mid\psi_1 \wedge\psi_2 \mid\bot \mid\psi_1 \vee\psi_2 \\ \\ \text{symbolic expressions} & \hat{e}& \mathrel{::=}& n\mid b \mid\hat{x} \mid\mathop{\mathit{uop}} \hat{e}_1 \mid\hat{e}_1 \mathbin{\mathit{bop}} \hat{e}_2 \\ \text{symbolic variables} & \hat{x} \\ \\ \text{expressions} & e& \mathrel{::=}& n\mid b \mid x \mid\mathop{\mathit{uop}} e_1 \mid e_1 \mathbin{\mathit{bop}} e_2 \\ \text{variables} & x \end{array} \]
Exercise: Symbolic Evaluation
Define a judgment form \(\psi \vdash e \Downarrow\hat{e}\) that says, “In separation store \(\psi\), expression \(e\) evaluates to symbolic expression \(\hat{e}\).”
Hint: Consider concrete evaluation \(\rho \vdash e \Downarrow v\), which says “In store \(\rho\), expression \(e\) evaluates to value \(v\).” Also consider partial evaluation \(\rho \vdash e \Downarrow e'\), which says “In store \(\rho\), expression \(e\) simplifies to expression \(e'\).”
Partial Evaluation
\[ \fbox{$\rho \vdash e \Downarrow e'$} \]
\(\inferlab{PEvalVar}{ x \mapsto v \in \rho }{ \rho \vdash x \Downarrow v }\)
\(\inferlab{PEvalVarPartial}{ x \mapsto- \notin \rho }{ \rho \vdash x \Downarrow x }\)
\(\inferlab{PEvalPlus}{ \rho \vdash e_1 \Downarrow n_1 \and \rho \vdash e_2 \Downarrow n_2 }{ \rho \vdash e_1 \mathbin{\texttt{+}} e_2 \Downarrow n_1 + n_2 }\)
\(\inferlab{PEvalPlusPartial}{ \rho \vdash e_1 \Downarrow e_1' \and \rho \vdash e_2 \Downarrow e_2' \and \text{$e_1' \neq n_1$ or $e_2' \neq n_2$} }{ \rho \vdash e_1 \mathbin{\texttt{+}} e_2 \Downarrow e_1' \mathbin{\texttt{+}} e_2' }\)
Symbolic Evaluation
\[ \fbox{$\psi \vdash e \Downarrow\hat{e}$} \]
\(\inferlab{SymevalVar}{ x \mapsto\hat{e} \in \rho }{ \rho \vdash x \Downarrow\hat{e} }\)
\(\inferlab{SymevalPlusConcrete}{ \rho \vdash e_1 \Downarrow n_1 \and \rho \vdash e_2 \Downarrow n_2 }{ \rho \vdash e_1 \mathbin{\texttt{+}} e_2 \Downarrow n_1 + n_2 }\)
\(\inferlab{SymevalPlus}{ \rho \vdash e_1 \Downarrow\hat{e}_1' \and \rho \vdash e_2 \Downarrow\hat{e}_2' \and \text{$\hat{e}_1' \neq n_1$ or $\hat{e}_2' \neq n_2$} }{ \rho \vdash e_1 \mathbin{\texttt{+}} \hat{e}_2 \Downarrow e_1' \mathbin{\texttt{+}} \hat{e}_2' }\)
Exercise: Semantics of Separation Stores
\[ \begin{array}{rrrl} \text{valuation} & \theta& \mathrel{::=}& \circ\mid\theta,\hat{x} \mapsto v \end{array} \]
Define the relation \(\rho \cdot \theta \models \psi\) for concrete store \(\rho\) modeling separation store \(\psi\).
We write \(\theta(\hat{e})\) for applying the substitution \({\cdots [v_i/\hat{x}_i] \cdots}(\hat{e})\) for each \(\hat{x}_i \mapsto v_i \in \theta\).
We write \(\theta \vdash \hat{e} \Downarrow v\) for the judgment form that says, “Under the valuation \(\theta\), the symbolic expression \(\hat{e}\) evaluates to value \(v\).” It should be case that \(\theta \vdash \hat{e} \Downarrow v\) if and only if \( \theta(\hat{e}) \Downarrow v\)
Semantics of Separation Stores
\[ \fbox{$\rho \cdot \theta \models \psi$} \]
\[ \begin{array}{lcl} x \mapsto v \cdot \theta \models x \mapsto\hat{e} & \text{iff} & \theta \vdash \hat{e} \Downarrow v \\ \circ \cdot \theta \models \mathsf{emp} & \text{iff} & \text{always} \\ \rho_1 ,\rho_2 \cdot \theta \models \psi_1 \ast\psi_2 & \text{iff} & \text{$\rho_1 \cdot \theta \models \psi_1$ and $\rho_2 \cdot \theta \models \psi_2$ s.t. $\operatorname{dom}(\rho_1) \cap \operatorname{dom}(\rho_2) = \emptyset$} \\ \rho \cdot \theta \models \hat{e} & \text{iff} & \theta \vdash \hat{e} \Downarrow\mathbf{true} \\ \rho \cdot \theta \models \top & \text{iff} & \text{always} \\ \rho \cdot \theta \models \psi_1 \wedge\psi_2 & \text{iff} & \text{$\rho \cdot \theta \models \psi_1$ and $\rho \cdot \theta \models \psi_2$} \\ \rho \cdot \theta \models \bot & \text{iff} & \text{never} \\ \rho \cdot \theta \models \psi_1 \vee\psi_2 & \text{iff} & \text{$\rho \cdot \theta \models \psi_1$ or $\rho \cdot \theta \models \psi_2$} \end{array} \]