Abstraction
What questions do you have? What questions does your neighbor have?
Questions?
Review: Collecting Semantics
Verification as Reachability
We want to collect all reachable states — properties.
\[ \begin{array}{rr} \text{store properties} & P& \mathrel{::=}& \circ\mid P,\rho \end{array} \]
That is, we want to define a collecting semantics \(\lbrace\!\lbrack\!\lbrack s \rbrack\!\rbrack\!\rbrace = \lambda P.P'\) for the forward state-reachability property. That is, we want the following equation to hold:
\[ \lbrace\!\lbrack\!\lbrack s \rbrack\!\rbrack\!\rbrace{P} = \{ \rho' \mid \text{$\rho \vdash s \Downarrow\rho'$ for all $\rho\in P$} \} \]
Exercise: State-Collecting Semantics
Define \(\lbrace\!\lbrack\!\lbrack s \rbrack\!\rbrack\!\rbrace = \lambda P.P'\) by induction on the structure of statement \(s\). You may assume a denotation for expressions \(\lbrack\!\lbrack e \rbrack\!\rbrack = \lambda \rho.v\).
State-Collecting Semantics
\[ \begin{array}{rrrl} \text{statements} & s& \mathrel{::=}& \cdots \mid\mathbf{assume}\;e \\ \text{store-property transformers} & f& \mathrel{::=}& \lambda P.P' \end{array} \]
\[ \fbox{$\lbrace\!\lbrack\!\lbrack s \rbrack\!\rbrack\!\rbrace = \lambda P.P'$} \]
\[ \begin{array}{rrl} \lbrace\!\lbrack\!\lbrack \texttt{;} \rbrack\!\rbrack\!\rbrace & \mathrel{:=}& \lambda P. P \\ \lbrace\!\lbrack\!\lbrack s_1 \mathbin{\texttt{;}} s_2 \rbrack\!\rbrack\!\rbrace & \mathrel{:=}& \lbrace\!\lbrack\!\lbrack s_2 \rbrack\!\rbrack\!\rbrace \circ \lbrace\!\lbrack\!\lbrack s_1 \rbrack\!\rbrack\!\rbrace \\ \lbrace\!\lbrack\!\lbrack \mathbf{assume}\;e \rbrack\!\rbrack\!\rbrace & \mathrel{:=}& \lambda P. \{ \rho \mid \text{$\lbrack\!\lbrack e \rbrack\!\rbrack\,\rho = \mathbf{true}$ for all $\rho\in P$} \} \\ \lbrace\!\lbrack\!\lbrack \mathbf{if}\;\texttt{(}e\texttt{)}\;s_1\;\mathbf{else}\;s_2 \rbrack\!\rbrack\!\rbrace & \mathrel{:=}& \lambda P. \lbrace\!\lbrack\!\lbrack \mathbf{assume}\;e \mathbin{\texttt{;}} s_1 \rbrack\!\rbrack\!\rbrace\,P \cup \lbrace\!\lbrack\!\lbrack \mathbf{assume}\;\texttt{!}{e} \mathbin{\texttt{;}} s_2 \rbrack\!\rbrack\!\rbrace\,P \\ \lbrace\!\lbrack\!\lbrack x \mathrel{\texttt{=}}e \rbrack\!\rbrack\!\rbrace & \mathrel{:=}& \lambda P. \{ \rho(x \leftarrow \lbrack\!\lbrack e \rbrack\!\rbrack\,\rho ) \mid \rho\in P \} \\ \\ \lbrace\!\lbrack\!\lbrack \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \rbrack\!\rbrack\!\rbrace & \mathrel{:=}& \lambda P. \lbrace\!\lbrack\!\lbrack\mathbf{assume}\;\texttt{!}{e} \rbrack\!\rbrack\!\rbrace\left( \bigcup_i (\lbrace\!\lbrack\!\lbrack \mathbf{assume}\;e \mathbin{\texttt{;}} s_1 \rbrack\!\rbrack\!\rbrace)^i\,P \right) \\ & \text{or} & \\ \lbrace\!\lbrack\!\lbrack \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \rbrack\!\rbrack\!\rbrace & \mathrel{:=}& \lambda P.\lbrace\!\lbrack\!\lbrack\mathbf{assume}\;\texttt{!}{e} \rbrack\!\rbrack\!\rbrace\left( \operatorname{lfp}\,(\lambda P'. P \cup \lbrace\!\lbrack\!\lbrack \mathbf{assume}\;e \mathbin{\texttt{;}} s_1 \rbrack\!\rbrack\!\rbrace\,P' ) \right) \end{array} \]
Abstraction
Exercise: Value-Collecting Semantics
Let’s simplify and consider arithmetic expressions with variables:
\[ \begin{array}{rrrl} \text{expressions} & e& \mathrel{::=}& x\mid n\mid e_1 \mathbin{\mathit{bop}} e_2 \\ \text{binary operators} & \mathit{bop}& \mathrel{::=}& \texttt{+}\mid\texttt{-}\mid\texttt{*}\mid\texttt{/} \\\\ \text{number properties} & N& \mathrel{::=}& \circ\mid N,n \end{array} \]
Define \(\lbrace\!\lbrack\!\lbrack e \rbrack\!\rbrack\!\rbrace = \lambda P.N\) by induction on the structure of expression \(e\).
Exercise: Sign Abstraction
Let us abstract number properties in a finite manner by partitioning into signs:
\[ \begin{array}{rrrl} \text{signs} & \mathit{sign}& \mathrel{::=}& \mathsf{-}\mid\mathsf{0}\mid\mathsf{+} \\ \text{abstract numbers} & \hat{n}& \mathrel{::=}& \bot \mid\mathit{sign}\mid\top \end{array} \]
Define a concretization relation \(n \models \hat{n}\) by cases on \(\hat{n}\).
We write \(\gamma(\hat{n}) = N\) for the concretization function such that \(\gamma(\hat{n}) = N\) iff \(n \models \hat{n}\) for all \(n\in N\).
Abstract Interpretation
Exercise: Abstract Operations
Define operations on abstract numbers:
\(\fbox{$\hat{n}_1 \mathbin{\mathbin{\hat{+}}} \hat{n}_2 = \hat{n}'$}\)
\(\fbox{$\hat{n}_1 \mathbin{\mathbin{\hat{-}}} \hat{n}_2 = \hat{n}'$}\)
\(\fbox{$\hat{n}_1 \mathbin{\mathbin{\hat{\cdot}}} \hat{n}_2 = \hat{n}'$}\)
\(\fbox{$\hat{n}_1 \mathbin{\mathbin{\hat{\div}}} \hat{n}_2 = \hat{n}'$}\)
State soundness of these abstract operations.
Exercise: Abstract Interpretation: Denotationally
Consider the non-relational abstract store:
\[ \begin{array}{rr} \text{(non-relational) abstract stores} & \hat{\rho}& \mathrel{::=}& \circ\mid\hat{\rho},x \mapsto\hat{n} \end{array} \]
Define the abstract interpretation function \(\lbrack\!\lbrack e \rbrack\!\rbrack^\sharp = \lambda \hat{\rho}.\hat{n}\) by induction on the structure of \(e\).
State soundness of this abstract interpretation function.
Exercise: Abstract Interpretation: Operationally
Or similarly, define the abstract interpretation judgment form \(\fbox{\(\hat{\rho} \vdash e \mathrel{\Downarrow^\sharp}\hat{n}\)}\).
Exercise: Abstract Domains
We can define a partial order on abstract elements, that is, consider the judgment form \(\hat{n}_1 \sqsubseteq \hat{n}_2\) that says, “Abstract number \(\hat{n}_1\) is included in \(\hat{n}_2\).”
This judgment form should be sound with respect concrete inclusion. State this soundness condition.
Exercise: Galois Connections
For some abstract domains, we can define the best abstraction function \(\alpha(N) = \hat{n}\) where \(\gamma\) and \(\alpha\) are “almost inverses.” State this almost-inverse property, which is called a Galois connection.
Exercise: Abstract Booleans
Consider abstract booleans that similarly constructs the flat lattice out of booleans:
\[ \begin{array}{rrrl} \text{abstract booleans} & \hat{b}& \mathrel{::=}& \bot \mid b\mid\top \end{array} \]
Define concretization of abstract booleans \(\hat{b}\).
Cartesian-Product Abstract Domain
\[ \begin{array}{rrrl} \text{values} & v& \mathrel{::=}& n\mid b \\ \text{abstract values} & \hat{v}& \mathrel{::=}& \hat{n} \cdot\hat{b} \end{array} \]
Define concretization of abstract values \(\hat{v}\).
Define inclusion \(\hat{v}_1 \sqsubseteq \hat{v}_2\).
Exercise: Abstract Interpretation with Numbers and Booleans
\[ \begin{array}{rr} \text{(non-relational) abstract stores} & \hat{\rho}& \mathrel{::=}& \circ\mid\hat{\rho},x \mapsto\hat{v} \end{array} \]
Define the abstract interpretation function \(\lbrack\!\lbrack e \rbrack\!\rbrack^\sharp = \lambda \hat{\rho}.\hat{v}\) by induction on the structure of \(e\).
Or similarly, define the abstract interpretation judgment form \(\fbox{\(\hat{\rho} \vdash e \mathrel{\Downarrow^\sharp}\hat{v}\)}\).
Exercise: Type Checking
How is type checking an abstract interpretation?
Appendix
\(\fbox{$\hat{\rho} \vdash e \Downarrow e'$}\)
\(\fbox{$\hat{\rho} \vdash s \Downarrow\hat{\rho}'$}\)
\[ \inferlab{AbsexeAssign}{ \hat{\rho} \vdash e \Downarrow e' }{ \hat{\rho} \vdash x \mathrel{\texttt{=}}e \Downarrow \hat{\rho}(x \leftarrow e') } \]