Data Flow Analysis 2: Bit Vector Frameworks

A data flow analysis frameworks can be represented with the property space, a (semi-)lattice, \(L = (\mathcal{P}(D), \sqcap, \sqsubseteq)\), and a space of functions \(\mathcal{F}\), which contains transfer functions of the form \(f:\mathcal{P}(D) \rightarrow \mathcal{P}(D)\). (\(\mathcal{F}\) contains all the transfer functions for the analysis, contains the the identity function, and is closed under composition.) The framework is monotonic if for all \(X,Y\subseteq D\), \(X \sqsubseteq Y \implies f(X) \sqsubseteq f(Y)\). The framework is distributive if for all \(X,Y\subseteq D\), \(f(X \sqcap Y) = f(X) \sqcap f(Y)\).

• Exercise: All distributive frameworks are monotonic.

This is quite easy; all that needs to be shown is that \(f(X \sqcap Y) \sqsubseteq f(X) \sqcap f(Y)\) is equivalent to \(X \sqsubseteq Y \implies f(X) \sqsubseteq f(Y)\).

It is worth noting that not all monotnic frameworks are distributive. For instance constant propagation  is monotonic but not distributive.

Bit Vector Frameworks

Bit vector frameworks are a special type of frame works such that:

• \(L = (P(D),\sqcap)\) for some finite set \(D\) and \(\sqcap\) is either set union (\(\cup\)) or set intersection (\(\cap\)), and
• \(\mathcal{F}=\{f:\mathcal{P}(D) \rightarrow \mathcal{P}(D) \mid \exists G,K \subseteq D: \forall S\subseteq D, f(S)=(S\cap K)\cup G\}\).

Most common analyses, such as live variables, available expressions, reaching definitions, are bit vector frameworks. Try to prove this by formally stating the transfer functions of these analyses in the form of those of bit vector frameworks.

• Exercise: All bit vector frameworks are distributive.

Both set union (\(\cup\)) and set intersection (\(\cap\)) distribute over set intersection (\(\cap\)). Thus for a bit vector framework with \(\sqcap\) as \(\cap\) we would have, $$\begin{align} f(X\cap Y) & = ((X\cap Y) \cap K)\cup G \\ & = ((X\cap K) \cap (Y\cap K))\cup G \\ & = ((X\cap K)\cup G) \cap ((Y\cap K)\cup G) \\ & = f(X) \cap f(Y) \end{align}$$ We can similarly show \(f(X\cup Y) = f(X)\cup f(Y)\).

• Exercise: Not all distributive frameworks are bit vector.

We can come up with a simple example for this. Consider \(D=\{0,1\}\), \(\sqcap\) is \(\cup\), and a transfer function \(f: \mathcal{P}(D) \rightarrow \mathcal{P}(D)\) such that \(f(X) = \{1-x\mid x\in X\} \). So \(f(\emptyset)=\emptyset\), \(f(\{0\})=\{1\}\), \(f(\{1\})=\{0\}\), and \(f(\{0,1\})=\{0,1\}\). It can be seen this framework is distributive.

Assume this is a bit vector framework; then there exist \(K, G\subseteq D\) such that for all \(X\subseteq D\), \(f(X)=(X\cap K)\cup G\).
So \(f(\emptyset)=(\emptyset\cap K)\cup G = G\), i.e. \(G = \emptyset\). But \(f(\{0\})=(\{0\}\cap K)\cup G = \{1\}\). Here \((\{0\}\cap K)\subseteq \{0\}\), so \(1\notin (\{0\}\cap K)\), which implies \(1\in G\), a contradiction.

Considering examples from real-world analysis, maybe-uninitialized variable analysis and faint/alert variable analysis are examples of distributive frameworks which are not bit vector.