Abstract Domains

Bor-Yuh Evan Chang

Thursday, October 30, 2025

$\newcommand{\TirName}[1]{\text{#1}} \newcommand{\inferlab}[3]{ \let\and\qquad \begin{array}{l} \TirName{#1} \\ \displaystyle \frac{#2}{#3} \end{array} } \newcommand{\inferright}[3]{ \let\and\qquad \displaystyle \frac{#2}{#3}\TirName{#1} } \newcommand{\inferrule}[3][]{\inferlab{#1}{#2}{#3}} \newcommand{\infer}[3][]{\inferrule[#1]{#2}{#3}} $

Meeting 20 - Abstract Domains

What questions do you have? What questions does your neighbor have?

Questions?

Announcements

Start thinking, talking with each other, talking with me about your final project.
More details coming soon.

Review: Abstraction

Abstract Operations: Soundness

Lemma 1 (Local Soundness)

If $n_1 \in \gamma(\hat{n}_1)$ and $n_2 \in \gamma(\hat{n}_2)$, then $n_1 + n_2 \in \gamma(\hat{n}_1 \mathbin{\mathbin{\hat{+}}} \hat{n}_2)$. Or alternatively, $\gamma( \hat{n}_1 \mathbin{\mathbin{\hat{+}}} \hat{n}_2 ) \supseteq \{ n_1 + n_2 \mid \text{\(n_1 \in \gamma(\hat{n}_1)$ and $n_2 \in \gamma(\hat{n}_2)$} \}\)
If $n_1 \in \gamma(\hat{n}_1)$ and $n_2 \in \gamma(\hat{n}_2)$, then $n_1 - n_2 \in \gamma(\hat{n}_1 \mathbin{\mathbin{\hat{-}}} \hat{n}_2)$. Or alternatively, $\gamma( \hat{n}_1 \mathbin{\mathbin{\hat{-}}} \hat{n}_2 ) \supseteq \{ n_1 - n_2 \mid \text{\(n_1 \in \gamma(\hat{n}_1)$ and $n_2 \in \gamma(\hat{n}_2)$} \}\)
If $n_1 \in \gamma(\hat{n}_1)$ and $n_2 \in \gamma(\hat{n}_2)$, then $n_1 \cdot n_2 \in \gamma(\hat{n}_1 \mathbin{\mathbin{\hat{\cdot}}} \hat{n}_2)$. Or alternatively, $\gamma( \hat{n}_1 \mathbin{\mathbin{\hat{\cdot}}} \hat{n}_2 ) \supseteq \{ n_1 \cdot n_2 \mid \text{\(n_1 \in \gamma(\hat{n}_1)$ and $n_2 \in \gamma(\hat{n}_2)$} \}\)
If $n_1 \in \gamma(\hat{n}_1)$ and $n_2 \in \gamma(\hat{n}_2)$, then $n_1 \div n_2 \in \gamma(\hat{n}_1 \mathbin{\mathbin{\hat{\div}}} \hat{n}_2)$. Or alternatively, $\gamma( \hat{n}_1 \mathbin{\mathbin{\hat{\div}}} \hat{n}_2 ) \supseteq \{ n_1 \div n_2 \mid \text{\(n_1 \in \gamma(\hat{n}_1)$ and $n_2 \in \gamma(\hat{n}_2)$} \}\)

Summary of Abstraction

What are the relationships between number values $n$, abstract numbers $\hat{n}$, and number properties $N$?

Abstract Interpretation

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}$}\).

State soundness of this abstract interpretation relation.

Exercise: Concretizing Abstract Stores

Define $\gamma(\hat{\rho}) = \rho$ as the pointwise lifting of $\gamma(\hat{n})$.

Concretizing Abstract Stores

\[ \begin{array}{rrl} \gamma( \hat{\rho}) & \mathrel{:=}& \{ \rho \mid \text{$\rho(x) \in \gamma(\hat{\rho}(x))$ for all $x\in \operatorname{dom}(\hat{\rho})$} \} \end{array} \]

Soundness of an Abstract Interpretation

Theorem 1 (Global Soundness: Denotationally with Collecting) $\gamma(\lbrack\!\lbrack e \rbrack\!\rbrack^\sharp\,\hat{\rho}) \supseteq \lbrace\!\lbrack\!\lbrack e \rbrack\!\rbrack\!\rbrace\,\gamma(\hat{\rho}) \supseteq \{ \lbrack\!\lbrack e \rbrack\!\rbrack{\rho} \mid \rho\in \gamma(\hat{\rho}) \}$.

Theorem 2 (Global Soundness: Operationally) If $\hat{\rho} \vdash e \mathrel{\Downarrow^\sharp}\hat{n}$ and $\rho \vdash e \Downarrow n$ s.t. $\rho \models \hat{\rho}$, then $n \models \hat{n}$.

Abstract Interpretation: Denotationally and Collecting

\[ \fbox{$\lbrack\!\lbrack e \rbrack\!\rbrack^\sharp = \lambda \hat{\rho}.\hat{n}$} \]

\[ \begin{array}{rrl} \lbrack\!\lbrack n \rbrack\!\rbrack^\sharp\,\hat{\rho} & \mathrel{:=}& \beta(n) \\ \lbrack\!\lbrack e_1 \mathbin{+} e_2 \rbrack\!\rbrack^\sharp\, \hat{\rho} & \mathrel{:=}& (\lbrack\!\lbrack e_1 \rbrack\!\rbrack^\sharp\,\hat{\rho}) \mathbin{\mathbin{\hat{+}}} (\lbrack\!\lbrack e_2 \rbrack\!\rbrack^\sharp\,P) \\ \lbrack\!\lbrack x \rbrack\!\rbrack^\sharp\, \hat{\rho} & \mathrel{:=}& \hat{\rho}(x) \\ \\ \lbrace\!\lbrack\!\lbrack n \rbrack\!\rbrack\!\rbrace\, P & \mathrel{:=}& \{ n \} \\ \lbrace\!\lbrack\!\lbrack e_1 \mathbin{+} e_2 \rbrack\!\rbrack\!\rbrace\, P & \mathrel{:=}& \{ n_1 + n_2 \mid \text{$n_1 \in \lbrace\!\lbrack\!\lbrack e_1 \rbrack\!\rbrack\!\rbrace\,P$ and $n_2 \in \lbrace\!\lbrack\!\lbrack e_2 \rbrack\!\rbrack\!\rbrace\,P$} \} \\ \lbrace\!\lbrack\!\lbrack x \rbrack\!\rbrack\!\rbrace\, P & \mathrel{:=}& \{ \rho(x) \mid \rho\in P \} \end{array} \]

where $\beta(n) = \hat{n}$ is the representation function.

Exercise: 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.