Abstract Domain Combinators
What questions do you have? What questions does your neighbor have?
Questions?
Review: Summary of Abstract Interpretation
What are the relationships between expressions \(e\), number values \(n\), abstract numbers \(\hat{n}\), and number properties \(N\)?
Abstract Domains
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 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: 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 Combinator
\[ \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?
Type Checking as an Abstract Interpretation
types \(\quad \tau \quad \mathrel{::=} \quad \mathbf{number} \mid \mathbf{boolean}\)
abstract values \(\quad \hat{v} \quad \mathrel{::=} \quad \tau\)
\[ \begin{array}{lcl} \gamma(\mathbf{number}) & \mathrel{:=}& \{ n \mid \text{true} \} \\ \gamma(\mathbf{boolean}) & \mathrel{:=}& \{ b \mid \text{true} \} \end{array} \]
Type Checking as an Abstract Interpretation
\[ \text{abstract values} \quad \hat{v}\quad \mathrel{::=}\quad \hat{n} \cdot\hat{b} \]
abstract numbers \(\quad \hat{n} \quad \mathrel{::=} \quad \bot \mid \top\)
abstract booleans \(\quad \hat{b} \quad \mathrel{::=} \quad \bot \mid \top\)
types \(\quad \tau \quad \mathrel{::=} \quad \mathbf{number} \mid \mathbf{boolean}\) \(\mid \tau _1 \wedge \tau _2 \mid \tau _1 \vee \tau _2\)
Widening
Exercise: Interval Abstraction
Let us abstract number properties as intervals:
\[ \begin{array}{rrrl} \text{values} & v& \mathrel{::=}& n \\ \text{abstract values} & \hat{v}& \mathrel{::=}& \hat{n} \\ \text{abstract numbers} & \hat{n}& \mathrel{::=}& \bot \mid r\mid\top \\ \text{intervals} & r& \mathrel{::=}& (-\infty, n_2] \mid[n_1, n_2] \mid[n_1, \infty) \end{array} \]
Define a concretization function \(\gamma(\hat{n}) = N\) by cases on \(\hat{n}\).
What is the height of the abstract domain of abstract numbers \(\hat{n}\)?
JavaScripty Statements
\(\begin{array}{rrrl} \text{statements} & s& \mathrel{::=}& \texttt{;} \mid x \mathrel{\texttt{=}}e \mid s_1 \mathbin{\texttt{;}} s_2 \mid\mathbf{assume}\;e \mid\mathbf{if}\;\texttt{(}e\texttt{)}\;s_1\;\mathbf{else}\;s_2 \mid\mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \end{array}\)
(non-relational) abstract stores \(\quad \hat{\rho} \quad \mathrel{::=} \quad \circ \mid \hat{\rho},x \mapsto\hat{v}\)
abstract values \(\quad \hat{v}\)
abstract-store transformers \(\quad \hat{f} \quad \mathrel{::=} \quad \lambda \hat{\rho}.\hat{\rho}'\)
Exercise: Abstract Interpretation: Denotationally
Define the abstract interpretation function \(\lbrack\!\lbrack s \rbrack\!\rbrack^\sharp = \lambda \hat{\rho}.\hat{\rho}'\) by induction on the structure of \(s\).
State soundness of this abstract interpretation function.