Abstract Interpretation

Author

Bor-Yuh Evan Chang

Published

Tuesday, October 28, 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}} $

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

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$.

Value-Collecting Semantics

\[ \begin{array}{rrl} \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} \]

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$.

Sign Abstraction

\[ \begin{array}{lcl} n \models \mathsf{-} & \text{iff} & n< 0 \\ n \models \mathsf{0} & \text{iff} & n= 0 \\ n \models \mathsf{+} & \text{iff} & n> 0 \\ n \models \top & \text{always} \\ n \models \bot & \text{never} \end{array} \]

\[ \begin{array}{lcl} \gamma(\mathsf{-}) & \mathrel{:=}& \{ n \mid n< 0 \} \\ \gamma(\mathsf{0}) & \mathrel{:=}& \{ n \mid n= 0 \} \\ \gamma(\mathsf{+}) & \mathrel{:=}& \{ n \mid n> 0 \} \\ \gamma(\top) & \mathrel{:=}& \{ n \mid \text{true} \} \\ \gamma(\bot) & \mathrel{:=}& \emptyset \end{array} \]

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.

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

Abstract Operations: Definition: Times

$\mathbin{\hat{\cdot}}$	$\mathsf{-}$	$\mathsf{0}$	$\mathsf{+}$
$\mathsf{-}$	$\mathsf{+}$	$\mathsf{0}$	$\mathsf{-}$
$\mathsf{0}$	$\mathsf{0}$	$\mathsf{0}$	$\mathsf{0}$
$\mathsf{+}$	$\mathsf{-}$	$\mathsf{0}$	$\mathsf{+}$

Abstract Operations: Definition: Plus

$\mathbin{\hat{+}}$	$\mathsf{-}$	$\mathsf{0}$	$\mathsf{+}$	$\top$
$\mathsf{-}$	$\mathsf{-}$	$\mathsf{-}$	$\top$	$\top$
$\mathsf{0}$	$\mathsf{-}$	$\mathsf{0}$	$\mathsf{+}$	$\top$
$\mathsf{+}$	$\top$	$\mathsf{+}$	$\mathsf{+}$	$\top$
$\top$	$\top$	$\top$	$\top$	$\top$

Abstract Operations: Definition: Divide

$\mathbin{\hat{\div}}$	$\mathsf{-}$	$\mathsf{0}$	$\mathsf{+}$	$\top$	$\bot$
$\mathsf{-}$	$\mathsf{+}$	$\bot$	$\mathsf{-}$	$\top$	$\bot$
$\mathsf{0}$	$\mathsf{0}$	$\bot$	$\mathsf{0}$	$\mathsf{0}$	$\bot$
$\mathsf{+}$	$\mathsf{-}$	$\bot$	$\mathsf{+}$	$\top$	$\bot$
$\top$	$\top$	$\bot$	$\top$	$\top$	$\bot$
$\bot$	$\bot$	$\bot$	$\bot$	$\bot$	$\bot$

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

\(\mathbin{\hat{\cdot}}\)	\(\mathsf{-}\)	\(\mathsf{0}\)	\(\mathsf{+}\)
\(\mathsf{-}\)	\(\mathsf{+}\)	\(\mathsf{0}\)	\(\mathsf{-}\)
\(\mathsf{0}\)	\(\mathsf{0}\)	\(\mathsf{0}\)	\(\mathsf{0}\)
\(\mathsf{+}\)	\(\mathsf{-}\)	\(\mathsf{0}\)	\(\mathsf{+}\)

\(\mathbin{\hat{+}}\)	\(\mathsf{-}\)	\(\mathsf{0}\)	\(\mathsf{+}\)	\(\top\)
\(\mathsf{-}\)	\(\mathsf{-}\)	\(\mathsf{-}\)	\(\top\)	\(\top\)
\(\mathsf{0}\)	\(\mathsf{-}\)	\(\mathsf{0}\)	\(\mathsf{+}\)	\(\top\)
\(\mathsf{+}\)	\(\top\)	\(\mathsf{+}\)	\(\mathsf{+}\)	\(\top\)
\(\top\)	\(\top\)	\(\top\)	\(\top\)	\(\top\)

\(\mathbin{\hat{\div}}\)	\(\mathsf{-}\)	\(\mathsf{0}\)	\(\mathsf{+}\)	\(\top\)	\(\bot\)
\(\mathsf{-}\)	\(\mathsf{+}\)	\(\bot\)	\(\mathsf{-}\)	\(\top\)	\(\bot\)
\(\mathsf{0}\)	\(\mathsf{0}\)	\(\bot\)	\(\mathsf{0}\)	\(\mathsf{0}\)	\(\bot\)
\(\mathsf{+}\)	\(\mathsf{-}\)	\(\bot\)	\(\mathsf{+}\)	\(\top\)	\(\bot\)
\(\top\)	\(\top\)	\(\bot\)	\(\top\)	\(\top\)	\(\bot\)
\(\bot\)	\(\bot\)	\(\bot\)	\(\bot\)	\(\bot\)	\(\bot\)