Widening

\(\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?

Widening

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

Abstract Interpretation: Denotationally

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

\[ \begin{array}{rrl} \lbrack\!\lbrack \texttt{;} \rbrack\!\rbrack^\sharp & \mathrel{:=}& \lambda \hat{\rho}. \hat{\rho} \\ \lbrack\!\lbrack s_1 \mathbin{\texttt{;}} s_2 \rbrack\!\rbrack^\sharp & \mathrel{:=}& \lbrack\!\lbrack s_2 \rbrack\!\rbrack^\sharp \circ \lbrack\!\lbrack s_1 \rbrack\!\rbrack^\sharp \\ \lbrack\!\lbrack x \mathrel{\texttt{=}}e \rbrack\!\rbrack^\sharp & \mathrel{:=}& \lambda \hat{\rho}. \hat{\rho}(x \leftarrow \lbrack\!\lbrack e \rbrack\!\rbrack^\sharp\,\hat{\rho} ) \\ \\ \lbrack\!\lbrack \mathbf{assume}\;e \rbrack\!\rbrack^\sharp & \mathrel{:=}& \lambda \hat{\rho}. \hat{\rho} \curlywedge e \\ \lbrack\!\lbrack \mathbf{if}\;\texttt{(}e\texttt{)}\;s_1\;\mathbf{else}\;s_2 \rbrack\!\rbrack^\sharp & \mathrel{:=}& \lambda \hat{\rho}. \lbrack\!\lbrack \mathbf{assume}\;e \mathbin{\texttt{;}} s_1 \rbrack\!\rbrack^\sharp\,\hat{\rho} \mathbin{\sqcup} \lbrack\!\lbrack \mathbf{assume}\;\texttt{!}{e} \mathbin{\texttt{;}} s_2 \rbrack\!\rbrack^\sharp\,\hat{\rho} \\ \\ \lbrack\!\lbrack \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \rbrack\!\rbrack^\sharp & \mathrel{:=}& \lambda \hat{\rho}. \lbrack\!\lbrack\mathbf{assume}\;\texttt{!}{e} \rbrack\!\rbrack^\sharp\left( \bigsqcup_i (\lbrack\!\lbrack \mathbf{assume}\;e \mathbin{\texttt{;}} s_1 \rbrack\!\rbrack^\sharp)^i\,P \right) \\ & \text{or} & \\ \lbrack\!\lbrack \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \rbrack\!\rbrack^\sharp & \mathrel{:=}& \lambda \hat{\rho}.\lbrack\!\lbrack\mathbf{assume}\;\texttt{!}{e} \rbrack\!\rbrack^\sharp\left( \operatorname{lfp}\,(\lambda \hat{\rho}'. \hat{\rho} \mathbin{\sqcup} \lbrack\!\lbrack \mathbf{assume}\;e \mathbin{\texttt{;}} s_1 \rbrack\!\rbrack^\sharp\,\hat{\rho}' ) \right) \end{array} \]

Collecting Semantics: Denotationally

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

Soundness of an Abstract Interpretation

Theorem 1 (Global Soundness: Denotationally)  

1. \(\gamma(\lbrack\!\lbrack s \rbrack\!\rbrack^\sharp\,\hat{\rho}) \supseteq \gamma(\lbrack\!\lbrack s \rbrack\!\rbrack{\rho})\) for all \(\rho\in \gamma(\hat{\rho})\).
2. \(\gamma(\lbrack\!\lbrack e \rbrack\!\rbrack^\sharp\,\hat{\rho}) \supseteq \gamma(\lbrack\!\lbrack e \rbrack\!\rbrack{\rho})\) for all \(\rho\in \gamma(\hat{\rho})\).

Abstract Interpretation of While

But what’s unsatisfying about the abstract interpretation of \(\mathbf{while}\)?

\[ \begin{array}{rrl} \lbrack\!\lbrack \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \rbrack\!\rbrack^\sharp & \mathrel{:=}& \lambda \hat{\rho}. \lbrack\!\lbrack\mathbf{assume}\;\texttt{!}{e} \rbrack\!\rbrack^\sharp\left( \bigsqcup_i (\lbrack\!\lbrack \mathbf{assume}\;e \mathbin{\texttt{;}} s_1 \rbrack\!\rbrack^\sharp)^i\,P \right) \\ & \text{or} & \\ \lbrack\!\lbrack \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \rbrack\!\rbrack^\sharp & \mathrel{:=}& \lambda \hat{\rho}.\lbrack\!\lbrack\mathbf{assume}\;\texttt{!}{e} \rbrack\!\rbrack^\sharp\left( \operatorname{lfp}\,(\lambda \hat{\rho}'. \hat{\rho} \mathbin{\sqcup} \lbrack\!\lbrack \mathbf{assume}\;e \mathbin{\texttt{;}} s_1 \rbrack\!\rbrack^\sharp\,\hat{\rho}' ) \right) \end{array} \]

Enforcing Convergence with the Widening Operator

\[ \begin{array}{rrl} \lbrack\!\lbrack \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \rbrack\!\rbrack^\sharp & \mathrel{:=}& \lambda \hat{\rho}.\lbrack\!\lbrack\mathbf{assume}\;\texttt{!}{e} \rbrack\!\rbrack^\sharp\left( \operatorname{lfp}\,(\lambda \hat{\rho}'. \hat{\rho} \mathbin{\nabla} \lbrack\!\lbrack \mathbf{assume}\;e \mathbin{\texttt{;}} s_1 \rbrack\!\rbrack^\sharp\,\hat{\rho}' ) \right) \end{array} \]

Widening

Definition 1 (Widening Operator) A widening is an upper-bound operator that enforces convergence:

upper-bound

For all \(\hat{\rho}_1, \hat{\rho}_2\), we have that \(\hat{\rho}_1 \mathrel{\sqsubseteq} \hat{\rho}_1 \mathbin{\nabla}\hat{\rho}_2 \) and \(\hat{\rho}_2 \mathrel{\sqsubseteq} \hat{\rho}_1 \mathbin{\nabla}\hat{\rho}_2 \)

convergence

For all chains \(\hat{\rho}_0 \mathrel{\sqsubseteq}\hat{\rho}_1 \mathrel{\sqsubseteq}\cdots\), the chain \(\hat{\rho}_0' \mathrel{\sqsubseteq}\hat{\rho}_1' \mathrel{\sqsubseteq}\cdots\) s.t \(\hat{\rho}_0' = \hat{\rho}_0\) and \(\hat{\rho}_i' = \hat{\rho}_{i-1}' \mathbin{\nabla}\hat{\rho}_i\) converges (i.e., there is some \(n\) where \(\hat{\rho}_i' = \hat{\rho}_n'\) for all \(i \geq n\)).

Exercise: Widening for the Interval Domain

Define a widening operator \(\mathbin{\nabla}\) for the interval abstract domain:

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

Widening for the Interval Domain

\[ \begin{array}{rrll} [n_1, n_2] \mathbin{\nabla}[n_1', n_2'] & \mathrel{:=}& [n_1, \infty) & \text{if $n_1 \leq n_1'$ and $n_2 < n_2'$} \\ [n_1, n_2] \mathbin{\nabla}[n_1', n_2'] & \mathrel{:=}& (-\infty, n_2] & \text{if $n_1 > n_1'$ and $n_2 \geq n_2'$} \\ [n_1, n_2] \mathbin{\nabla}[n_1', n_2'] & \mathrel{:=}& \top & \text{if $n_1 > n_1'$ and $n_2 < n_2'$} \\ \hat{n}_1 \mathbin{\nabla}\hat{n}_2 & \mathrel{:=}& \hat{n}_1 \mathbin{\sqcup}\hat{n}_2 & \text{otherwise} \end{array} \]