Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | |||
|
sav08:abstract_interpretation_recipe [2008/05/20 12:14] 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') = g^{\#}(p') \sqcup \bigsqcup_{(p,p') \in E} sp^{\#}(g^{\#}(p),r(p,p')) | 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$ | ||