• English only

# Differences

This shows you the differences between two versions of the page.

sav08:abstract_interpretation_recipe [2008/05/08 12:41]
vkuncak
sav08:abstract_interpretation_recipe [2015/04/21 17:30] (current)
Line 17: Line 17:
(for example, by defining function $\alpha$ so that $(\alpha,​\gamma)$ becomes a [[Galois Connection on Lattices]])     (for example, by defining function $\alpha$ so that $(\alpha,​\gamma)$ becomes a [[Galois Connection on Lattices]])
* extend $sp^{\#}$ to work on control-flow graphs, by defining $F^\# : (V \to A) \to (V \to A)$ as follows (below, $g^{\#} : V \to A$)   * extend $sp^{\#}$ to work on control-flow graphs, by defining $F^\# : (V \to A) \to (V \to A)$ as follows (below, $g^{\#} : V \to A$)
-$+\begin{equation*} - ​F^{\#​}(g^{\#​})(p_2) = g^{\#}(p_2) \sqcup \bigsqcup_{(p_1,p_2) \in E} sp^{\#​}(g^{\#​}(p_1),r(p_1,p_2)) + ​F^{\#​}(g^{\#​})(p') = g^{\#}(p') \sqcup \bigsqcup_{(p,p') \in E} sp^{\#​}(g^{\#​}(p),r(p,p')) -$+\end{equation*}
which is analogous to [[Collecting Semantics]] which is analogous to [[Collecting Semantics]]
* compute $g^{\#}_* = lfp(F^\#)$ (this is easier than computing collecting semantics because lattice $A^n$ is simpler than $C^n$):   * compute $g^{\#}_* = lfp(F^\#)$ (this is easier than computing collecting semantics because lattice $A^n$ is simpler than $C^n$):
-$+\begin{equation*} ​g^{\#​}_* = \bigsqcup_{n \ge 0} (F^{\#​})^{n}(\bot^{\#​}) ​g^{\#​}_* = \bigsqcup_{n \ge 0} (F^{\#​})^{n}(\bot^{\#​}) -$+\end{equation*}

where $\bot^{\#​}(p) = \bot_A$ for all $p \in V$ where $\bot^{\#​}(p) = \bot_A$ for all $p \in V$