Symbolic Execution and Separation Logic
What questions do you have? What questions does your neighbor have?
Announcements
- No class this Thursday, October 9 (Mid-Semester Reading Day)
Questions?
Review: Separation 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: 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} \]
Exercise: Symbolic Execution
Define a judgment form \(\psi \vdash s \Downarrow\psi'\) that says, “In symbolic pre-store \(\psi\), statement \(s\) evaluates to symbolic post-store \(\psi'\).”
\(\inferrule[SymexeSeq]{ \psi \vdash s_1 \Downarrow \psi' \and \psi' \vdash s_2 \Downarrow \psi'' }{ \psi \vdash s_1 \mathbin{\texttt{;}} s_2 \Downarrow \psi'' }\)
c.f.
\(\inferrule[EvalSeq]{ \rho \vdash s_1 \Downarrow\rho' \and \rho' \vdash s_2 \Downarrow\rho'' }{ \rho \vdash s_1 \mathbin{\texttt{;}} s_2 \Downarrow \rho'' }\)
\(\inferrule[VerifySeq]{ {} \vdash \{\varphi\}\; s_1 \;\{ \varphi' \} \and {} \vdash \{\varphi'\}\; s_2 \;\{ \varphi'' \} }{ {} \vdash \{\varphi\}\; s_1 \mathbin{\texttt{;}} s_2 \;\{ \varphi'' \} }\)
Exercise: Symbolic Execution: If
c.f.
\(\inferrule[EvalIfTrue]{ \rho \vdash e \Downarrow\mathbf{true} \and \rho \vdash s_1 \Downarrow\rho' }{ \rho \vdash \mathbf{if}\;\texttt{(}e\texttt{)}\;s_1\;\mathbf{else}\;s_2 \Downarrow \rho' }\)
\(\inferrule[EvalIfFalse]{ \rho \vdash e \Downarrow\mathbf{false} \and \rho \vdash s_2 \Downarrow\rho' }{ \rho \vdash \mathbf{if}\;\texttt{(}e\texttt{)}\;s_1\;\mathbf{else}\;s_2 \Downarrow \rho' }\)
\[ \inferrule[VerifyIf]{ {} \vdash \{ \varphi \wedge e \}\;s_1\;\{\varphi'\} \and {} \vdash \{ \varphi \wedge\neg e \}\;s_2\;\{\varphi'\} }{ {} \vdash \{\varphi\}\; \mathbf{if}\;\texttt{(}e\texttt{)}\;s_1\;\mathbf{else}\;s_2 \;\{ \varphi' \} } \]
Symbolic Execution: If
\(\inferrule[SymexeIfTrue]{ \psi \vdash e \Downarrow\hat{e} \and \psi \wedge\hat{e} \vdash s_1 \Downarrow\psi_1 \and \psi \wedge\neg\hat{e} \vdash \bot }{ \psi \vdash \mathbf{if}\;\texttt{(}e\texttt{)}\;s_1\;\mathbf{else}\;s_2 \Downarrow \psi_1 }\)
\(\inferrule[SymexeIfFalse]{ \psi \vdash e \Downarrow\hat{e} \and \psi \wedge\hat{e} \vdash \bot \and \psi \wedge\neg\hat{e} \vdash s_2 \Downarrow\psi_2 }{ \psi \vdash \mathbf{if}\;\texttt{(}e\texttt{)}\;s_1\;\mathbf{else}\;s_2 \Downarrow \psi_1 }\)
\(\inferrule[SymexeIf]{ \psi \vdash e \Downarrow\hat{e} \and \psi \wedge\hat{e} \vdash s_1 \Downarrow\psi_1 \and \psi \wedge\neg\hat{e} \vdash s_2 \Downarrow\psi_2 }{ \psi \vdash \mathbf{if}\;\texttt{(}e\texttt{)}\;s_1\;\mathbf{else}\;s_2 \Downarrow \psi_1 \vee\psi_2 }\)
Exercise: Symbolic Execution: While
c.f.
\(\inferrule[EvalWhileFalse]{ \rho \vdash e \Downarrow\mathbf{false} }{ \rho \vdash \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \Downarrow \rho }\)
\(\inferrule[EvalWhileTrue]{ \rho \vdash e \Downarrow\mathbf{true} \and \rho \vdash s_1 \mathbin{\texttt{;}} \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \Downarrow \rho' }{ \rho \vdash \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \Downarrow \rho' }\)
\[ \inferrule[VerifyWhile]{ {} \vdash \{ \varphi \wedge e \}\;s_1\;\{\varphi\} }{ {} \vdash \{\varphi\}\; \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \;\{ \varphi \wedge\neg e \} } \]
Symbolic Execution: While
\[ \inferrule[SymexeWhile]{ \psi \vdash \mathbf{if}\;\texttt{(}e\texttt{)}\;s_1 \mathbin{\texttt{;}} \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1\;\mathbf{else}\;\texttt{;} \Downarrow\psi' }{ \psi \vdash \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \Downarrow\psi' } \]
Exercise: Symbolic Execution: Assignment
cf.
\[ \inferrule[EvalAssign]{ \rho \vdash e \Downarrow v }{ \rho \vdash x \mathrel{\texttt{=}}e \Downarrow \rho(x \leftarrow v) } \]
\[ \inferrule[VerifyAssign]{ \phantom{\jhoare{}{}} }{ {} \vdash \{\varphi\}\; x \mathrel{\texttt{=}}e \;\{ \exists x_{\mathrm{old}}. [x_{\mathrm{old}}/x]\varphi \wedge x= [x_{\mathrm{old}}/x]e \} } \]
Symbolic Execution: Assignment
\[ \inferrule[SymexeAssign]{ \psi \ast x \mapsto\hat{e}_{\mathrm{old}} \vdash e \Downarrow\hat{e} }{ \psi \ast x \mapsto\hat{e}_{\mathrm{old}} \vdash x \mathrel{\texttt{=}}e \Downarrow \psi \ast x \mapsto\hat{e} } \]
Rule of Consequence
\[ \inferrule[SymexeConsequence]{ \psi_{\mathrm{pre}} \vdash \psi_{\mathrm{pre}}' \and \psi_{\mathrm{pre}}' \vdash s \Downarrow\psi_{\mathrm{post}}' \and \psi_{\mathrm{post}}' \vdash \psi_{\mathrm{post}} }{ \psi_{\mathrm{pre}} \vdash s \Downarrow\psi_{\mathrm{post}} } \]
Case Analysis
\[ \inferrule[SymexeCases]{ \psi_1 \vdash s \Downarrow\psi_1' \and \psi_2 \vdash s \Downarrow\psi_2' }{ \psi_1 \vee\psi_2 \vdash s \Downarrow \psi_1' \vee\psi_2' } \]
Frame Rule
\[ \inferrule[SymexeFrame]{ \psi \vdash s \Downarrow\psi' \and \operatorname{dom}(\psi_{\mathrm{frame}}) \cap \operatorname{modref}(s) = \emptyset }{ \psi_{\mathrm{frame}} \ast\psi \vdash s \Downarrow\psi_{\mathrm{frame}} \ast\psi' } \]
Denotational Semantics
Them’s Just Semantics
An operational semantics is …
An axiomatic semantics is …
A denotational semantics is …
Denotations
We define a (compilation) function \(\lbrack\!\lbrack\cdot \rbrack\!\rbrack\) on syntax to its denotation. A denotation is something in the meta logic (e.g., sets, functions, partial-ordered sets, complete lattices, monotone functions, continuous functions).
Exercise: Denotational Semantics of Expressions
Define a denotation \(\lbrack\!\lbrack e \rbrack\!\rbrack\) by induction on the structure of \(e\) to a function from stores to values \(\lambda \rho.v\), that is, \(\lbrack\!\lbrack e \rbrack\!\rbrack : \operatorname{Store}\rightarrow \operatorname{Val}\) where \(\rho: \operatorname{Store}\) and \(v: \operatorname{Val}\).
Exercise: Denotational Semantics of Statements
Define a denotation \(\lbrack\!\lbrack s \rbrack\!\rbrack\) by induction on the structure of \(s\) to a function from stores to stores \(\lambda \rho.\rho'\), that is, \(\lbrack\!\lbrack s \rbrack\!\rbrack : \operatorname{Store}\rightarrow \operatorname{Store}\).