Symbolic Heap Analysis (as an Abstract Interpretation)
What questions do you have? What questions does your neighbor have?
Announcements
- Project presentation:
Mon Dec 8 1:30-4 p.m.- Tue Dec 9 1:30-4 p.m.
- Project paper:
- Fri Dec 12 AoE
- Submission via GitHub
- Extra support
- Extra office hours (before and after class today 8:30am-12:00pm)
See advice on final projects.
Questions?
Review: Points-To Analysis
Allocation-Site Address Abstraction: Domain
\(\begin{array}{rrrl} \text{abstract values} & \hat{v}& \mathrel{::=}& \circ\mid\hat{v},\hat{a} \\ \text{abstract addresses} & \hat{a}& \mathrel{::=}& \ell \end{array}\)
Abstract addresses \(\hat{a}\) are allocation sites, and abstract values \(\hat{v}\) are sets of abstract addresses. Sets of abstract addresses are also called points-to sets.
Exercise: Store Abstraction
Define an abstract domain \(\hat{\rho}\) and its concretization \(\gamma(\hat{\rho})\) to lift the allocation-site abstraction to stores.
Field-Sensitive Store Abstraction
\[ \begin{array}{rrrl} \text{abstract states} & \hat{\sigma}& \mathrel{::=}& \hat{\rho} \\ \text{abstract stores} & \hat{\rho}& \mathrel{::=}& \circ \mid\hat{\rho},\hat{l} \mapsto\hat{v} \\ \text{abstract l-values} & \hat{l}& \mathrel{::=}& x\mid\hat{a}\mathord{.}f \end{array} \]
The field-sensitive store abstraction is a non-relational lifting of the allocation-site abstraction to stores.
Field-Sensitive Store Abstraction: Concretization
\(\fbox{$\gamma(\hat{\rho}) = P$}\)
\(\begin{array}{rrl} \gamma(\circ) & \mathrel{:=}& \{ \circ \} \\ \gamma( \hat{\rho},x \mapsto\hat{v} ) & \mathrel{:=}& \{ \rho,x \mapsto v \mid \text{$\rho\in \gamma(\hat{\rho})$ and $v\in \gamma(\hat{v})$} \} \\ \gamma( \hat{\rho},\hat{a}\mathord{.}f \mapsto\hat{v} ) & \mathrel{:=}& \{ \rho,a^{\ell}\mathord{.}f \mapsto v \mid \text{$\rho\in \gamma(\hat{\rho})$ and $a^{\ell} \in \gamma(\hat{a})$ and $v\in \gamma(\hat{v})$} \} \end{array}\)
Points-To Analysis as an Abstract Interpretation
\[ \fbox{$\lbrack\!\lbrack s \rbrack\!\rbrack^\sharp = \lambda \hat{\sigma}.\hat{\sigma}'$} \]
\[ \begin{array}{rrl} \lbrack\!\lbrack x \mathrel{\texttt{=}}y \rbrack\!\rbrack^\sharp\,\hat{\sigma} & \mathrel{:=}& \hat{\sigma}(x \leftarrow \hat{\sigma}(y) ) \\ \lbrack\!\lbrack \ell\colon x \mathrel{\texttt{=}}\texttt{\{\}} \rbrack\!\rbrack^\sharp\,\hat{\sigma} & \mathrel{:=}& \hat{\sigma}(x \leftarrow \ell) \\ \lbrack\!\lbrack x \mathrel{\texttt{=}}y\texttt{.}f \rbrack\!\rbrack^\sharp\,\hat{\sigma} & \mathrel{:=}& \hat{\sigma}(x \leftarrow \bigcup_{\hat{a}\in \hat{\sigma}(y)} \hat{\sigma}( \hat{a}\mathord{.}f ) ) \\ \lbrack\!\lbrack x\texttt{.}f \mathrel{\texttt{=}}y \rbrack\!\rbrack^\sharp\,\hat{\sigma} & \mathrel{:=}& \bigsqcup_{\hat{a}\in \hat{\sigma}(x)} \hat{\sigma}( \hat{a}\mathord{.}f \leftarrow \hat{\sigma}(y) ) \\ \lbrack\!\lbrack s_1\;s_2 \rbrack\!\rbrack^\sharp\,\hat{\sigma} & \mathrel{:=}& \operatorname{lfp}\,\lambda \hat{\sigma}'. \hat{\sigma}\mathbin{\sqcup}\lbrack\!\lbrack s_1 \rbrack\!\rbrack^\sharp\,\hat{\sigma}' \mathbin{\sqcup}\lbrack\!\lbrack s_2 \rbrack\!\rbrack^\sharp{\hat{\sigma}'} \end{array} \]
Points-To Analysis as Set Constraints
\[ \fbox{$\hat{\sigma}( \hat{l}) \supseteq \hat{v}$} \]
\(\infer{ x \mathrel{\texttt{=}}y }{ \hat{\sigma}( x) \supseteq \hat{\sigma}(y) }\)
\(\infer{ \ell\colon x \mathrel{\texttt{=}}\texttt{\{\}} }{ \hat{\sigma}( x) \supseteq \{ \ell \} }\)
\(\infer{ x \mathrel{\texttt{=}}y\texttt{.}f \and \hat{a}\in \hat{\sigma}(y) }{ \hat{\sigma}( x) \supseteq \hat{\sigma}( \hat{a}\mathord{.}f ) }\)
\(\infer{ x\texttt{.}f \mathrel{\texttt{=}}y \and \hat{a}\in \hat{\sigma}(x) }{ \hat{\sigma}( \hat{a}\mathord{.}f ) \supseteq \hat{\sigma}( y) }\)
Field-Insensitive Store Abstraction
\(\begin{array}{rrrl} \text{abstract states} & \hat{\sigma}& \mathrel{::=}& \hat{\rho} \\ \text{abstract stores} & \hat{\rho}& \mathrel{::=}& \circ \mid\hat{\rho},\hat{l} \mapsto\hat{v} \\ \text{abstract l-values} & \hat{l}& \mathrel{::=}& x\mid\hat{a} \end{array}\)
\(\infer{ x \mathrel{\texttt{=}}y }{ \hat{\sigma}( x) \supseteq \hat{\sigma}(y) }\)
\(\infer{ \ell\colon x \mathrel{\texttt{=}}\texttt{\{\}} }{ \hat{\sigma}( x) \supseteq \{ \ell \} }\)
\(\infer{ x \mathrel{\texttt{=}}y\texttt{.}f \and \hat{a}\in \hat{\sigma}(y) }{ \hat{\sigma}( x) \supseteq \hat{\sigma}( \hat{a}) }\)
\(\infer{ x\texttt{.}f \mathrel{\texttt{=}}y \and \hat{a}\in \hat{\sigma}(x) }{ \hat{\sigma}( \hat{a}) \supseteq \hat{\sigma}( y) }\)
Field-Based Store Abstraction
\(\begin{array}{rrrl} \text{abstract states} & \hat{\sigma}& \mathrel{::=}& \hat{\rho} \\ \text{abstract stores} & \hat{\rho}& \mathrel{::=}& \circ \mid\hat{\rho},\hat{l} \mapsto\hat{v} \\ \text{abstract l-values} & \hat{l}& \mathrel{::=}& x\mid f \end{array}\)
\(\infer{ x \mathrel{\texttt{=}}y }{ \hat{\sigma}( x) \supseteq \hat{\sigma}(y) }\)
\(\infer{ \ell\colon x \mathrel{\texttt{=}}\texttt{\{\}} }{ \hat{\sigma}( x) \supseteq \{ \ell \} }\)
\(\infer{ x \mathrel{\texttt{=}}y\texttt{.}f }{ \hat{\sigma}( x) \supseteq \hat{\sigma}( f) }\)
\(\infer{ x\texttt{.}f \mathrel{\texttt{=}}y }{ \hat{\sigma}( f) \supseteq \hat{\sigma}( y) }\)
Symbolic Heap Analysis
Heap Language: Syntax
\(\begin{array}{rrrl} \text{expressions} & e& \mathrel{::=}& x \mid\mathbf{null} \mid e\texttt{.}f \\ \text{statements} & s& \mathrel{::=}& e_1 \mathrel{\texttt{=}}e_2 \mid x \mathrel{\texttt{=}}\texttt{\{\}} \mid\texttt{;} \mid\mathbf{if}\;\texttt{(}e \mathbin{\texttt{!==}} \mathbf{null}\texttt{)}\;s_1\;\mathbf{else}\;s_2 \mid\mathbf{while}\;\texttt{(}e \mathbin{\texttt{!==}} \mathbf{null}\texttt{)}\;s_1 \end{array}\)
variables \(\quad x , y\)
\(\begin{array}{rrrl} \text{l-values} & l& \mathrel{::=}& x\mid a\mathord{.}f \\ \text{values} & v& \mathrel{::=}& \mathsf{null}\mid a \\ \text{addresses} & a \end{array}\)
\(\begin{array}{rrrl} \text{states} & \sigma& \mathrel{::=}& \rho \\ \text{stores} & \rho& \mathrel{::=}& \circ \mid\rho,l \mapsto v \end{array}\)
Exercise: Heap Language: Concrete Semantics
What judgment forms do we need to define a big-step operational semantics for the heap language?
Exercise: Heap Language: Concrete Semantics
Define the judgment forms
\[ \begin{array}{ll} \fbox{$\sigma \vdash e \Downarrow l$} & \text{In state $\sigma$, heap expression $e$ evaluates to heap l-value $l$.} \\ \fbox{$\sigma \vdash e \Downarrow v$} & \text{In state $\sigma$, heap expression $e$ evaluates to heap value $v$.} \\ \fbox{$\sigma \vdash s \Downarrow\sigma'$} & \text{In state $\sigma$, heap statement $s$ executes to updated state $\sigma'$.} \end{array} \]
Heap Language: Concrete Semantics
\[ \fbox{$\sigma \vdash e \Downarrow l$} \]
\(\infer{ }{ \sigma \vdash x \Downarrow x }\)
\(\infer{ \sigma \vdash e \Downarrow a }{ \sigma \vdash e\texttt{.}f \Downarrow a\mathord{.}f }\)
\[ \fbox{$\sigma \vdash e \Downarrow v$} \]
\(\infer{ }{ \sigma \vdash \mathbf{null} \Downarrow \mathsf{null} }\)
\(\infer{ \sigma \vdash e \Downarrow l }{ \sigma \vdash e \Downarrow \sigma(l) }\)
Heap Language: Concrete Semantics
\[ \fbox{$\sigma \vdash s \Downarrow\sigma'$} \]
\(\infer{ \sigma \vdash e_1 \Downarrow l \and \sigma \vdash e_2 \Downarrow v }{ \sigma \vdash e_1 \mathrel{\texttt{=}}e_2 \Downarrow \sigma(l \leftarrow v) }\)
\(\infer{ a\notin \operatorname{dom}(\sigma) }{ \sigma \vdash x \mathrel{\texttt{=}}\texttt{\{\}} \Downarrow \sigma(x \leftarrow a) }\)
\(\infer{ \phantom{\Downarrow} }{ \sigma \vdash \texttt{;} \Downarrow \sigma }\)
\(\infer{ \sigma \vdash e \Downarrow a \and \sigma \vdash s_1 \Downarrow \sigma' }{ \sigma \vdash \mathbf{if}\;\texttt{(}e \mathbin{\texttt{!==}} \mathbf{null}\texttt{)}\;s_1\;\mathbf{else}\;s_2 \Downarrow \sigma' }\)
\(\infer{ \sigma \vdash e \Downarrow \mathsf{null} \and \sigma \vdash s_2 \Downarrow \sigma' }{ \sigma \vdash \mathbf{if}\;\texttt{(}e \mathbin{\texttt{!==}} \mathbf{null}\texttt{)}\;s_1\;\mathbf{else}\;s_2 \Downarrow \sigma' }\)
\(\infer{ \sigma \vdash e \Downarrow a \and \sigma \vdash s_1 \Downarrow \sigma' \and \sigma' \vdash \mathbf{while}\;\texttt{(}e \mathbin{\texttt{!==}} \mathbf{null}\texttt{)}\;s_1 \Downarrow \sigma'' }{ \sigma \vdash \mathbf{while}\;\texttt{(}e \mathbin{\texttt{!==}} \mathbf{null}\texttt{)}\;s_1 \Downarrow \sigma'' }\)
\(\infer{ \sigma \vdash e \Downarrow \mathsf{null} }{ \sigma \vdash \mathbf{while}\;\texttt{(}e \mathbin{\texttt{!==}} \mathbf{null}\texttt{)}\;s_1 \Downarrow \sigma }\)
Exercise: Buggy VerifyAssign
Suppose we have a symbolic store abstraction \(\varphi\). Consider assignments with l-values on the left-hand side \(l \mathrel{\texttt{=}}e\). What’s wrong with the following Hoare rule?
\[ \inferrule[BuggyVerifyAssign]{ }{ {} \vdash \{ [e/l]\varphi \}\; l \mathrel{\texttt{=}}e \;\{ \varphi\} } \]
Symbolic Addresses and Symbolic Stores
\[ \begin{array}{rrrl} \text{abstract l-values} & \hat{l}& \mathrel{::=}& x\mid\hat{a}\mathord{.}f \\ \text{abstract values} & \hat{v}& \mathrel{::=}& \mathsf{null}\mid\hat{a}\mid\mathsf{sel}(\hat{\rho}, \hat{l}) \\ \text{abstract addresses} & \hat{a} \end{array} \]
Abstract addresses \(\hat{a}\) are symbolic variables (i.e., existential logic variables).
\[ \begin{array}{rrrl} \text{abstract stores} & \hat{\rho}& \mathrel{::=}& h \mid\mathsf{upd}(\hat{\rho}, \hat{l}, \hat{v}) \\ \text{symbolic heaps} & h \\ \\ \text{symbolic variables} & \hat{x}& \mathrel{::=}& \hat{a}\mid h \end{array} \]
Abstract stores is the array theory. Symbolic heaps \(h\) are symbolic variables.
\[ \begin{array}{rrrl} \text{abstract states (i.e., symbolic stores $\varphi$)} & \hat{\sigma}& \mathrel{::=}& \hat{\rho} \mid\bot \mid\hat{\sigma}_1 \vee\hat{\sigma}_2 \mid\top \end{array} \]
Abstract states is the disjunctive completion or powerset domain of abstract stores.
Exercise: Concretization
\[ \begin{array}{rrrl} \text{valuation} & \theta& \mathrel{::=}& \circ\mid\theta,\hat{a} \mapsto a \mid\theta,h \mapsto\rho \end{array} \]
\(\fbox{$\gamma(\hat{l}) = \{ \ldots, l \cdot \theta, \ldots \}$}\)
\(\fbox{$\gamma(\hat{v}) = \{ \ldots, v \cdot \theta, \ldots \}$}\)
\(\fbox{$\gamma(\hat{a}) = \{ \ldots, a \cdot \theta, \ldots \}$}\)
Define concretization on abstract stores \(\hat{\rho}\) and abstract states \(\hat{\sigma}\).
\(\fbox{$\gamma(\hat{\rho}) = \{ \ldots, \rho \cdot \theta, \ldots \}$}\)
\(\fbox{$\gamma(\hat{\sigma}) = \{ \ldots, \sigma, \ldots \}$}\)
Concretization
\(\fbox{$\gamma(\hat{l}) = \{ \ldots, l \cdot \theta, \ldots \}$}\)
\(\fbox{$\gamma(\hat{v}) = \{ \ldots, v \cdot \theta, \ldots \}$}\)
\(\fbox{$\gamma(\hat{a}) = \{ \ldots, a \cdot \theta, \ldots \}$}\)
\[ \fbox{$\gamma(\hat{\rho}) = \{ \ldots, \rho \cdot \theta, \ldots \}$} \]
\(\begin{array}{rrl} \gamma( h) & \mathrel{:=}& \{ \rho \cdot \theta \mid \rho= \theta(h) \} \\ \gamma( \mathsf{upd}(\hat{\rho}, \hat{l}, \hat{v}) ) & \mathrel{:=}& \{ \rho(l \leftarrow v) \cdot \theta \mid \text{ $\rho \cdot \theta \in \gamma(\hat{\rho})$ and $l \cdot \theta \in \gamma(\hat{l})$ and $v \cdot \theta \in \gamma(\hat{v})$ } \} \end{array}\)
\[ \fbox{$\gamma(\hat{\sigma}) = \{ \ldots, \sigma, \ldots \}$} \]
\(\begin{array}{rrl} \gamma( \hat{\rho}) & \mathrel{:=}& \{ \rho \mid \rho \cdot \theta \in \gamma(\hat{\rho}) \} \\ \gamma( \bot ) & \mathrel{:=}& \{ \sigma \mid \text{false} \} \\ \gamma( \hat{\sigma}_1 \vee\hat{\sigma}_2 ) & \mathrel{:=}& \gamma(\hat{\sigma}_1) \cup \gamma(\hat{\sigma}_2) \\ \gamma( \top ) & \mathrel{:=}& \{ \sigma \mid \text{true} \} \end{array}\)
Exercise: Equivalences
Define the judgment form \(\Gamma \vdash \hat{v}_1 \equiv \hat{v}_2 \) that says, “Under assumptions \(\Gamma\), abstract value \(\hat{v}_1\) is equivalent to abstract value \(\hat{v}_2\).”
You may assume judgment forms for equivalences and dis-equivalences on l-values (i.e., \(\Gamma \vdash \hat{l}_1 \equiv \hat{l}_2 \) and \(\Gamma \vdash \hat{l}_1 \not\equiv \hat{l}_2 \)).
Equivalences: Theory of Arrays
\[ \fbox{$\Gamma \vdash \hat{v}_1 \equiv \hat{v}_2 $} \]
\(\infer{ }{ \Gamma \vdash \mathsf{null}\equiv \mathsf{null} }\)
\(\infer{ }{ \Gamma \vdash \hat{a}\equiv \hat{a} }\)
\(\infer{ }{ \Gamma, \hat{a}_1 \equiv \hat{a}_2 \vdash \hat{a}_1 \equiv \hat{a}_2 }\)
\(\infer{ \Gamma \vdash \hat{l}_1 \equiv \hat{l}_2 }{ \Gamma \vdash \mathsf{sel}( \mathsf{upd}(\hat{\rho}, \hat{l}_1, \hat{v}) , \hat{l}_2 ) \equiv \hat{v} }\)
\(\infer{ \Gamma \vdash \hat{l}_1 \not\equiv \hat{l}_2 }{ \Gamma \vdash \mathsf{sel}( \mathsf{upd}(\hat{\rho}, \hat{l}_1, \hat{v}) , \hat{l}_2 ) \equiv \mathsf{sel}(\hat{\rho}, \hat{l}_2) }\)
The last two rules are the McCarthy Axioms.
Exercise: Symbolic Execution as an Abstract Interpretation
\(\fbox{$\lbrack\!\lbrack e \rbrack\!\rbrack^\sharp = \lambda \hat{\sigma}.\hat{l}$}\)
\(\fbox{$\lbrack\!\lbrack e \rbrack\!\rbrack^\sharp = \lambda \hat{\sigma}.\hat{v}$}\)
Define an abstract interpretation on heap statements \(s\) using symbolic-heap abstract states:
\[ \fbox{$\lbrack\!\lbrack s \rbrack\!\rbrack^\sharp = \lambda \hat{\sigma}.\hat{\sigma}'$} \]
Symbolic Execution as an Abstract Interpretation
\(\fbox{$\lbrack\!\lbrack e \rbrack\!\rbrack^\sharp = \lambda \hat{\sigma}.\hat{l}$}\)
\(\fbox{$\lbrack\!\lbrack e \rbrack\!\rbrack^\sharp = \lambda \hat{\sigma}.\hat{v}$}\)
\[ \fbox{$\lbrack\!\lbrack s \rbrack\!\rbrack^\sharp = \lambda \hat{\sigma}.\hat{\sigma}'$} \]
\[ \begin{array}{rrll} \lbrack\!\lbrack e_1 \mathrel{\texttt{=}}e_2 \rbrack\!\rbrack^\sharp\,\hat{\sigma} & \mathrel{:=}& \mathsf{upd}(\hat{\sigma}, \lbrack\!\lbrack e_1 \rbrack\!\rbrack^\sharp\,\hat{\sigma} , \lbrack\!\lbrack e_2 \rbrack\!\rbrack^\sharp\,\hat{\sigma} ) \\ \lbrack\!\lbrack x \mathrel{\texttt{=}}\texttt{\{\}} \rbrack\!\rbrack^\sharp\,\hat{\sigma} & \mathrel{:=}& \mathsf{upd}(\hat{\sigma}, x, \hat{a}) & \text{where $\hat{a}\notin \hat{\sigma}$} \end{array} \]
\[ \begin{array}{rrll} \lbrack\!\lbrack \texttt{;} \rbrack\!\rbrack^\sharp\,\hat{\sigma} & \mathrel{:=}& \hat{\sigma} \\ \lbrack\!\lbrack \mathbf{if}\;\texttt{(}e \mathbin{\texttt{!==}} \mathbf{null}\texttt{)}\;s_1\;\mathbf{else}\;s_2 \rbrack\!\rbrack^\sharp\,\hat{\sigma} & \mathrel{:=}& (\lbrack\!\lbrack \mathbf{assume}\;e \mathbin{\texttt{!==}} \mathbf{null} \rbrack\!\rbrack^\sharp\,\hat{\sigma}) \mathbin{\sqcup} (\lbrack\!\lbrack \mathbf{assume}\;e \mathbin{\texttt{===}} \mathbf{null} \rbrack\!\rbrack^\sharp\,\hat{\sigma}) \\ \lbrack\!\lbrack \mathbf{while}\;\texttt{(}e \mathbin{\texttt{!==}} \mathbf{null}\texttt{)}\;s_1 \rbrack\!\rbrack^\sharp\,\hat{\sigma} & \mathrel{:=}& \lbrack\!\lbrack \mathbf{assume}\;e \mathbin{\texttt{===}} \mathbf{null} \rbrack\!\rbrack^\sharp\,\Bigl( \operatorname{lfp}\,\bigl(\lambda \hat{\sigma}'. \hat{\sigma}\mathbin{\sqcup}(\lbrack\!\lbrack \mathbf{assume}\;e \mathbin{\texttt{!==}} \mathbf{null} \mathbin{\texttt{;}} s_1 \rbrack\!\rbrack^\sharp\,\hat{\sigma}' )\bigr) \Bigr) \end{array} \]
Exercise: Symbolic Addresses and Separation-Based Symbolic Stores
For the same concrete semantic domains, formulate a separation-based symbolic store.
\(\begin{array}{rrrl} \text{l-values} & l& \mathrel{::=}& x\mid a\mathord{.}f \\ \text{values} & v& \mathrel{::=}& \mathsf{null}\mid a \\ \text{addresses} & a \end{array}\)
\(\begin{array}{rrrl} \text{states} & \sigma& \mathrel{::=}& \rho \\ \text{stores} & \rho& \mathrel{::=}& \circ \mid\rho,l \mapsto v \end{array}\)
Symbolic Addresses and Separation-Based Stores
\[ \begin{array}{rrrl} \text{abstract l-values} & \hat{l}& \mathrel{::=}& x\mid\hat{a}\mathord{.}f \\ \text{abstract values} & \hat{v}& \mathrel{::=}& \mathsf{null}\mid\hat{a} \\ \text{abstract addresses} & \hat{a} \end{array} \]
Abstract addresses \(\hat{a}\) are symbolic variables (i.e., existential logic variables).
\[ \begin{array}{rrrl} \text{abstract stores} & \hat{\rho}& \mathrel{::=}& \mathsf{emp}\mid\hat{l} \mapsto\hat{v} \mid\hat{\rho}_1 \ast\hat{\rho}_2 \\ \text{symbolic variables} & \hat{x}& \mathrel{::=}& \hat{a} \end{array} \]
Abstract stores are separation logic formulas. There is no symbolic heap variable.
\[ \begin{array}{rrrl} \text{abstract states (i.e., symbolic stores $\varphi$)} & \hat{\sigma}& \mathrel{::=}& \hat{\rho} \mid\bot \mid\hat{\sigma}_1 \vee\hat{\sigma}_2 \mid\top \end{array} \]
Abstract states is the disjunctive completion or powerset domain of abstract stores.
Exercise: Concretization
\[ \begin{array}{rrrl} \text{valuation} & \theta& \mathrel{::=}& \circ\mid\theta,\hat{a} \mapsto a \end{array} \]
\(\fbox{$\gamma(\hat{l}) = \{ \ldots, l \cdot \theta, \ldots \}$}\)
\(\fbox{$\gamma(\hat{v}) = \{ \ldots, v \cdot \theta, \ldots \}$}\)
\(\fbox{$\gamma(\hat{a}) = \{ \ldots, a \cdot \theta, \ldots \}$}\)
Define concretization on abstract stores \(\hat{\rho}\).
\(\fbox{$\gamma(\hat{\rho}) = \{ \ldots, \rho \cdot \theta, \ldots \}$}\)
\(\fbox{$\gamma(\hat{\sigma}) = \{ \ldots, \sigma, \ldots \}$}\)
Concretization
\(\fbox{$\gamma(\hat{l}) = \{ \ldots, l \cdot \theta, \ldots \}$}\)
\(\fbox{$\gamma(\hat{v}) = \{ \ldots, v \cdot \theta, \ldots \}$}\)
\(\fbox{$\gamma(\hat{a}) = \{ \ldots, a \cdot \theta, \ldots \}$}\)
\[ \fbox{$\gamma(\hat{\rho}) = \{ \ldots, \rho \cdot \theta, \ldots \}$} \]
\(\begin{array}{rrl} \gamma( \mathsf{emp}) & \mathrel{:=}& \{ \circ \cdot \theta \mid \text{true} \} \\ \gamma( \hat{l} \mapsto\hat{v} ) & \mathrel{:=}& \{ l \mapsto v \cdot \theta \mid \text{ $l \cdot \theta \in \gamma(\hat{l})$ and $v \cdot \theta \in \gamma(\hat{v})$ } \} \\ \gamma( \hat{\rho}_1 \ast\hat{\rho}_2 ) & \mathrel{:=}& \{ \rho_1 ,\rho_2 \cdot \theta \mid \text{ $\rho_1 \cdot \theta \in \gamma(\hat{\rho}_1)$ and $\rho_2 \cdot \theta \in \gamma(\hat{\rho}_2)$ and $\operatorname{dom}(\rho_1) \cap \operatorname{dom}(\rho_2) = \emptyset$ } \} \end{array}\)
Separation-Based Symbolic Execution as an Abstract Interpretation
\(\fbox{$\lbrack\!\lbrack e \rbrack\!\rbrack^\sharp = \lambda \hat{\sigma}.\hat{l}$}\)
\(\fbox{$\lbrack\!\lbrack e \rbrack\!\rbrack^\sharp = \lambda \hat{\sigma}.\hat{v}$}\)
\[ \fbox{$\lbrack\!\lbrack s \rbrack\!\rbrack^\sharp = \lambda \hat{\sigma}.\hat{\sigma}'$} \]
\[ \begin{array}{rrll} \lbrack\!\lbrack e_1 \mathrel{\texttt{=}}e_2 \rbrack\!\rbrack^\sharp\,( \hat{\sigma} \ast (\hat{l} \mapsto- ) ) & \mathrel{:=}& \hat{\sigma} \ast (\hat{l} \mapsto(\lbrack\!\lbrack e_2 \rbrack\!\rbrack^\sharp\,\hat{\sigma})) & \text{where $\hat{l}= \lbrack\!\lbrack e_1 \rbrack\!\rbrack^\sharp\,\hat{\sigma}$} \\ \lbrack\!\lbrack x \mathrel{\texttt{=}}\texttt{\{\}} \rbrack\!\rbrack^\sharp\,\hat{\sigma} & \mathrel{:=}& \hat{\sigma} \ast (x \mapsto\hat{a}) & \text{where $\hat{a}\notin \hat{\sigma}$} \end{array} \]
\[ \begin{array}{rrll} \lbrack\!\lbrack \texttt{;} \rbrack\!\rbrack^\sharp\,\hat{\sigma} & \mathrel{:=}& \hat{\sigma} \\ \lbrack\!\lbrack \mathbf{if}\;\texttt{(}e \mathbin{\texttt{!==}} \mathbf{null}\texttt{)}\;s_1\;\mathbf{else}\;s_2 \rbrack\!\rbrack^\sharp\,\hat{\sigma} & \mathrel{:=}& (\lbrack\!\lbrack \mathbf{assume}\;e \mathbin{\texttt{!==}} \mathbf{null} \rbrack\!\rbrack^\sharp\,\hat{\sigma}) \mathbin{\sqcup} (\lbrack\!\lbrack \mathbf{assume}\;e \mathbin{\texttt{===}} \mathbf{null} \rbrack\!\rbrack^\sharp\,\hat{\sigma}) \\ \lbrack\!\lbrack \mathbf{while}\;\texttt{(}e \mathbin{\texttt{!==}} \mathbf{null}\texttt{)}\;s_1 \rbrack\!\rbrack^\sharp\,\hat{\sigma} & \mathrel{:=}& \lbrack\!\lbrack \mathbf{assume}\;e \mathbin{\texttt{===}} \mathbf{null} \rbrack\!\rbrack^\sharp\,\Bigl( \operatorname{lfp}\,\bigl(\lambda \hat{\sigma}'. \hat{\sigma}\mathbin{\sqcup}(\lbrack\!\lbrack \mathbf{assume}\;e \mathbin{\texttt{!==}} \mathbf{null} \mathbin{\texttt{;}} s_1 \rbrack\!\rbrack^\sharp\,\hat{\sigma}' )\bigr) \Bigr) \end{array} \]
Termination?
What can be unbounded?
Widening?
We need to enrich abstract stores \(\hat{\rho}\) with summaries. What are some possible summaries?
Shape Analysis
Summarize pointer-based data structures.
Examples:
- canonical abstraction (three-valued logic): summarize addresses with the same pointed-by relations.
- inductive-predicate abstraction (separation logic): summarize heap fragments as inductive predicates.