Points-To Analysis (as an Abstract Interpretation)
What questions do you have? What questions does your neighbor have?
Announcements
Project presentation:
Mon Dec 8 1:30-4 p.m.- Tue Dec 9 1:30-4 p.m. possible???
Project paper: Fri Dec 12 AoE
FCQs due today
Extra support
- Extra office hours (before and after class Thursday 8:30am-12:00pm)
See advice on final projects.
FCQ
https://colorado.campuslabs.com/eval-home/
Review: Summary: An Abstract Interpretation Template
Syntax
expressions \(\quad e\)
statements \(\quad s\)
Concrete Semantic Domains
values \(\quad v\)
states \(\quad \sigma\)
Concrete Semantics
\(\fbox{$\sigma \vdash e \Downarrow v$}\)
\(\fbox{$\sigma \vdash s \Downarrow\sigma'$}\)
Forward-Reachable Collecting Semantics
\(\begin{array}{rrrl} \text{value properties} & V& \mathrel{::=}& \circ\mid V,v \end{array}\)
\(\begin{array}{rrrl} \text{state properties} & \Sigma& \mathrel{::=}& \circ\mid\Sigma,\sigma \end{array}\)
\(\fbox{$\lbrace\!\lbrack\!\lbrack e \rbrack\!\rbrack\!\rbrace = \lambda \Sigma.V$}\)
\(\fbox{$\lbrace\!\lbrack\!\lbrack s \rbrack\!\rbrack\!\rbrace = \lambda \Sigma.\Sigma'$}\)
\(\lbrace\!\lbrack\!\lbrack e \rbrack\!\rbrack\!\rbrace\,\Sigma = \{ v \mid \text{$\sigma \vdash e \Downarrow v$ and $\sigma\in \Sigma$} \}\)
\(\lbrace\!\lbrack\!\lbrack s \rbrack\!\rbrack\!\rbrace\,\Sigma = \{ \sigma' \mid \text{$\sigma \vdash s \Downarrow\sigma'$ and $\sigma\in \Sigma$} \}\)
Abstract Domains
\(\begin{array}{rrrl} \text{abstract values} & \hat{v} \end{array}\)
\(\begin{array}{rrrl} \text{abstract states} & \hat{\sigma} \end{array}\)
\(\fbox{$\gamma(\hat{v}) = V$}\)
\(\fbox{$\gamma(\hat{\sigma}) = \Sigma$}\)
\(\fbox{$\lbrack\!\lbrack e \rbrack\!\rbrack^\sharp = \lambda \hat{\sigma}.\hat{v}$}\)
\(\fbox{$\lbrack\!\lbrack s \rbrack\!\rbrack^\sharp = \lambda \hat{\sigma}.\hat{\sigma}'$}\)
\(\gamma( \lbrack\!\lbrack e \rbrack\!\rbrack^\sharp\,\hat{\sigma} ) \supseteq \lbrace\!\lbrack\!\lbrack e \rbrack\!\rbrack\!\rbrace\, \gamma(\hat{\sigma}) \quad \)for all \(\hat{\sigma}\)
\(\gamma( \lbrack\!\lbrack s \rbrack\!\rbrack^\sharp\,\hat{\sigma} ) \supseteq \lbrace\!\lbrack\!\lbrack s \rbrack\!\rbrack\!\rbrace\, \gamma(\hat{\sigma}) \quad \)for all \(\hat{\sigma}\)
Review: Dynamic Memory Allocation
JavaScripty Syntax
\(\begin{array}{rrrl} \text{expressions} & e& \mathrel{::=}& \cdots \mid e\texttt{.}f \end{array}\)
\(\begin{array}{rrrl} \text{statements} & s& \mathrel{::=}& \cdots \mid x \mathrel{\texttt{=}}\texttt{\{\}} \mid e_1\texttt{.}f \mathrel{\texttt{=}}e_2 \end{array}\)
\[ \text{fields} \quad f \]
Concrete Semantic Domains
\(\begin{array}{rrrl} \text{values} & v& \mathrel{::=}& \cdots \mid a \\ \text{addresses} & a \end{array}\)
\(\begin{array}{rrrl} \text{states} & \sigma& \mathrel{::=}& \rho \\ \text{stores} & \rho& \mathrel{::=}& \circ \mid\rho,l \mapsto v \\ \text{l-values} & l& \mathrel{::=}& x\mid a\mathord{.}f \end{array}\)
Exercise: Abstract Domains for Dynamic Memory Allocation
What are concrete semantic components are unbounded? Suggest some abstraction ideas.
Points-To Analysis
Allocation Sites
\(\begin{array}{rrrl} \text{statements} & s& \mathrel{::=}& \cdots \mid\ell\colon s \end{array}\)
locations \(\quad \ell\)
Statement \(\ell\colon s\) is a location-labeled statement. For example, \(\ell\colon x \mathrel{\texttt{=}}\texttt{\{\}}\) is an object allocation statement \(x \mathrel{\texttt{=}}\texttt{\{\}}\) at location \(\ell\).
Pointer Language: Syntax
\(\begin{array}{rrrl} \text{statements} & s& \mathrel{::=}& x \mathrel{\texttt{=}}y \mid\ell\colon x \mathrel{\texttt{=}}\texttt{\{\}} \mid x \mathrel{\texttt{=}}y\texttt{.}f \mid x\texttt{.}f \mathrel{\texttt{=}}y \mid s_1\;s_2 \end{array}\)
variables \(\quad x , y\)
\(\begin{array}{rrrl} \text{values} & v& \mathrel{::=}& a^{\ell} \\ \text{addresses} & a \\ \text{locations} & \ell \end{array}\)
\(\begin{array}{rrrl} \text{states} & \sigma& \mathrel{::=}& \rho \\ \text{stores} & \rho& \mathrel{::=}& \circ \mid\rho,l \mapsto v \\ \text{l-values} & l& \mathrel{::=}& x\mid a^{\ell} \mathord{.}f \end{array}\)
The composite statement \(s_1\;s_2\) executes an arbitrary interleaving of \(s_1\) and \(s_2\) an arbitrary number of times (i.e., the program is viewed as a bag of the atomic statements).
Variants of this language \(s\) are called Andersen-style statements. Note that there is no expression language, and statements are in an A-normal form.
Exercise: Pointer Language: Concrete Semantics
\[ \fbox{$\sigma \vdash s \Downarrow\sigma'$} \]
Define the judgment form \(\sigma \vdash s \Downarrow\sigma'\) to say, “In state \(\sigma\), pointer statement \(s\) can evaluate to \(\sigma'\).” Note that evaluation for pointer statements is non-deterministic.
Pointer Language: Concrete Semantics
\[ \fbox{$\sigma \vdash s \Downarrow\sigma'$} \]
\(\infer{ }{ \sigma \vdash x \mathrel{\texttt{=}}y \Downarrow \sigma(x \leftarrow \sigma(y) ) }\)
\(\infer{ a\notin \sigma }{ \sigma \vdash \ell\colon x \mathrel{\texttt{=}}\texttt{\{\}} \Downarrow \sigma(x \leftarrow a^{\ell} ) }\)
\(\infer{ a^{\ell} = \sigma(y) }{ \sigma \vdash x \mathrel{\texttt{=}}y\texttt{.}f \Downarrow \sigma(x \leftarrow \sigma( a^{\ell}\mathord{.}f ) ) }\)
\(\infer{ a^{\ell} = \sigma(x) }{ \sigma \vdash x\texttt{.}f \mathrel{\texttt{=}}y \Downarrow \sigma( a^{\ell}\mathord{.}f \leftarrow \sigma(y) ) }\)
\(\infer{ \sigma \vdash s_1 \Downarrow\sigma' \and \sigma' \vdash s_1\;s_2 \Downarrow\sigma'' }{ \sigma \vdash s_1\;s_2 \Downarrow\sigma'' }\)
\(\infer{ \sigma \vdash s_2 \Downarrow\sigma' \and \sigma' \vdash s_1\;s_2 \Downarrow\sigma'' }{ \sigma \vdash s_1\;s_2 \Downarrow\sigma'' }\)
\(\infer{ }{ \sigma \vdash s_1\;s_2 \Downarrow\sigma }\)
Exercise: Allocation-Site Address Abstraction
Define an abstract domain \(\hat{v}\) and its concretization \(\gamma(\hat{v})\) for the allocation-site abstraction.
Allocation-Site Address Abstraction: Domain
\(\begin{array}{rrrl} \text{value properties} & V& \mathrel{::=}& A \\ \text{address properties} & A& \mathrel{::=}& \circ\mid A,a^{\ell} \end{array}\)
\(\begin{array}{rrrl} \text{abstract values} & \hat{v}& \mathrel{::=}& \circ\mid\hat{v},\hat{a} \\ \text{abstract addresses} & \hat{a}& \mathrel{::=}& \ell \end{array}\)
Abstract addresses \(\hat{a}\) are allocation sites, and abstract values \(\hat{v}\) are sets of abstract addresses. Sets of abstract addresses are also called points-to sets.
Allocation-Site Address Abstraction: Concretization
\(\fbox{$\gamma(\hat{v}) = V$}\)
\(\fbox{$\gamma(\hat{a}) = A$}\)
\(\begin{array}{rrl} \gamma(\circ) & \mathrel{:=}& \emptyset \\ \gamma( \hat{v},\hat{a} ) & \mathrel{:=}& \gamma(\hat{v}) \cup \gamma(\hat{a}) \end{array}\)
\(\begin{array}{rrl} \gamma(\ell) & \mathrel{:=}& \{ a^{\ell} \mid \text{true} \} \end{array}\)
Exercise: Store Abstraction
Define an abstract domain \(\hat{\rho}\) and its concretization \(\gamma(\hat{\rho})\) to lift the allocation-site abstraction to stores.
Field-Sensitive Store Abstraction
\[ \begin{array}{rrrl} \text{abstract states} & \hat{\sigma}& \mathrel{::=}& \hat{\rho} \\ \text{abstract stores} & \hat{\rho}& \mathrel{::=}& \circ \mid\hat{\rho},\hat{l} \mapsto\hat{v} \\ \text{abstract l-values} & \hat{l}& \mathrel{::=}& x\mid\hat{a}\mathord{.}f \end{array} \]
The field-sensitive store abstraction is a non-relational lifting of the allocation-site abstraction to stores.
Field-Sensitive Store Abstraction: Concretization
\(\fbox{$\gamma(\hat{\rho}) = P$}\)
\(\begin{array}{rrl} \gamma(\circ) & \mathrel{:=}& \{ \circ \} \\ \gamma( \hat{\rho},x \mapsto\hat{v} ) & \mathrel{:=}& \{ \rho,x \mapsto v \mid \text{$\rho\in \gamma(\hat{\rho})$ and $v\in \gamma(\hat{v})$} \} \\ \gamma( \hat{\rho},\hat{a}\mathord{.}f \mapsto\hat{v} ) & \mathrel{:=}& \{ \rho,a^{\ell}\mathord{.}f \mapsto v \mid \text{$\rho\in \gamma(\hat{\rho})$ and $a^{\ell} \in \gamma(\hat{a})$ and $v\in \gamma(\hat{v})$} \} \end{array}\)
Points-To Analysis as an Abstract Interpretation
Define points-to analysis as an abstract interpretation \(\lbrack\!\lbrack s \rbrack\!\rbrack^\sharp = \lambda \hat{\sigma}.\hat{\sigma}'\) on pointer statements \(s\).
Points-To Analysis as an Abstract Interpretation
\[ \fbox{$\lbrack\!\lbrack s \rbrack\!\rbrack^\sharp = \lambda \hat{\sigma}.\hat{\sigma}'$} \]
\[ \begin{array}{rrl} \lbrack\!\lbrack x \mathrel{\texttt{=}}y \rbrack\!\rbrack^\sharp\,\hat{\sigma} & \mathrel{:=}& \hat{\sigma}(x \leftarrow \hat{\sigma}(y) ) \\ \lbrack\!\lbrack \ell\colon x \mathrel{\texttt{=}}\texttt{\{\}} \rbrack\!\rbrack^\sharp\,\hat{\sigma} & \mathrel{:=}& \hat{\sigma}(x \leftarrow \ell) \\ \lbrack\!\lbrack x \mathrel{\texttt{=}}y\texttt{.}f \rbrack\!\rbrack^\sharp\,\hat{\sigma} & \mathrel{:=}& \hat{\sigma}(x \leftarrow \bigcup_{\hat{a}\in \hat{\sigma}(y)} \hat{\sigma}( \hat{a}\mathord{.}f ) ) \\ \lbrack\!\lbrack x\texttt{.}f \mathrel{\texttt{=}}y \rbrack\!\rbrack^\sharp\,\hat{\sigma} & \mathrel{:=}& \bigsqcup_{\hat{a}\in \hat{\sigma}(x)} \hat{\sigma}( \hat{a}\mathord{.}f \leftarrow \hat{\sigma}(y) ) \\ \lbrack\!\lbrack s_1\;s_2 \rbrack\!\rbrack^\sharp\,\hat{\sigma} & \mathrel{:=}& \operatorname{lfp}\,\lambda \hat{\sigma}'. \hat{\sigma}\mathbin{\sqcup}\lbrack\!\lbrack s_1 \rbrack\!\rbrack^\sharp\,\hat{\sigma}' \mathbin{\sqcup}\lbrack\!\lbrack s_2 \rbrack\!\rbrack^\sharp{\hat{\sigma}'} \end{array} \]
Points-To Analysis as Set Constraints
\[ \fbox{$\hat{\sigma}( \hat{l}) \supseteq \hat{v}$} \]
\(\infer{ x \mathrel{\texttt{=}}y }{ \hat{\sigma}( x) \supseteq \hat{\sigma}(y) }\)
\(\infer{ \ell\colon x \mathrel{\texttt{=}}\texttt{\{\}} }{ \hat{\sigma}( x) \supseteq \{ \ell \} }\)
\(\infer{ x \mathrel{\texttt{=}}y\texttt{.}f \and \hat{a}\in \hat{\sigma}(y) }{ \hat{\sigma}( x) \supseteq \hat{\sigma}( \hat{a}\mathord{.}f ) }\)
\(\infer{ x\texttt{.}f \mathrel{\texttt{=}}y \and \hat{a}\in \hat{\sigma}(x) }{ \hat{\sigma}( \hat{a}\mathord{.}f ) \supseteq \hat{\sigma}( y) }\)
The judgment form \(s\) says, “Atomic statement \(s\) is in the program (i.e., the bag of atomic statements).” The program is an implicit parameter of the judgment form.
The result of a points-to analysis is the least \(\hat{\sigma}\) that satisfies \(\hat{\sigma}( \hat{l}) \supseteq \hat{v}\) for a given program.
This subset-based formulation is called Andersen’s Analysis. Replacing subset \(\supseteq\)-constraints with equality \(=\)-constraints is called unification-based or Steensgaard’s Analysis.
Points-To Analysis as Set Constraints
\[ \fbox{$\operatorname{pt}( \hat{l}) \supseteq \hat{v}$} \]
\(\infer{ x \mathrel{\texttt{=}}y }{ \operatorname{pt}( x) \supseteq \operatorname{pt}(y) }\)
\(\infer{ \ell\colon x \mathrel{\texttt{=}}\texttt{\{\}} }{ \operatorname{pt}( x) \supseteq \{ \ell \} }\)
\(\infer{ x \mathrel{\texttt{=}}y\texttt{.}f \and \hat{a}\in \hat{\sigma}(y) }{ \operatorname{pt}( x) \supseteq \operatorname{pt}( \hat{a}\mathord{.}f ) }\)
\(\infer{ x\texttt{.}f \mathrel{\texttt{=}}y \and \hat{a}\in \operatorname{pt}(x) }{ \operatorname{pt}( \hat{a}\mathord{.}f ) \supseteq \operatorname{pt}( y) }\)
Field-Insensitive Store Abstraction
\(\begin{array}{rrrl} \text{abstract states} & \hat{\sigma}& \mathrel{::=}& \hat{\rho} \\ \text{abstract stores} & \hat{\rho}& \mathrel{::=}& \circ \mid\hat{\rho},\hat{l} \mapsto\hat{v} \\ \text{abstract l-values} & \hat{l}& \mathrel{::=}& x\mid\hat{a} \end{array}\)
\(\infer{ x \mathrel{\texttt{=}}y }{ \hat{\sigma}( x) \supseteq \hat{\sigma}(y) }\)
\(\infer{ \ell\colon x \mathrel{\texttt{=}}\texttt{\{\}} }{ \hat{\sigma}( x) \supseteq \{ \ell \} }\)
\(\infer{ x \mathrel{\texttt{=}}y\texttt{.}f \and \hat{a}\in \hat{\sigma}(y) }{ \hat{\sigma}( x) \supseteq \hat{\sigma}( \hat{a}) }\)
\(\infer{ x\texttt{.}f \mathrel{\texttt{=}}y \and \hat{a}\in \hat{\sigma}(x) }{ \hat{\sigma}( \hat{a}) \supseteq \hat{\sigma}( y) }\)
Field-Based Store Abstraction
\(\begin{array}{rrrl} \text{abstract states} & \hat{\sigma}& \mathrel{::=}& \hat{\rho} \\ \text{abstract stores} & \hat{\rho}& \mathrel{::=}& \circ \mid\hat{\rho},\hat{l} \mapsto\hat{v} \\ \text{abstract l-values} & \hat{l}& \mathrel{::=}& x\mid f \end{array}\)
\(\infer{ x \mathrel{\texttt{=}}y }{ \hat{\sigma}( x) \supseteq \hat{\sigma}(y) }\)
\(\infer{ \ell\colon x \mathrel{\texttt{=}}\texttt{\{\}} }{ \hat{\sigma}( x) \supseteq \{ \ell \} }\)
\(\infer{ x \mathrel{\texttt{=}}y\texttt{.}f }{ \hat{\sigma}( x) \supseteq \hat{\sigma}( f) }\)
\(\infer{ x\texttt{.}f \mathrel{\texttt{=}}y }{ \hat{\sigma}( f) \supseteq \hat{\sigma}( y) }\)