Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:abstract_interpretation_recipe [2008/05/08 12:39] vkuncak |
sav08:abstract_interpretation_recipe [2015/04/21 17:30] (current) |
||
---|---|---|---|
Line 7: | Line 7: | ||
* $E \subseteq V \times V$ are control-flow graph edges | * $E \subseteq V \times V$ are control-flow graph edges | ||
* $r : E \to 2^{PS \times PS}$, so each $r(p_1,p_2) \subseteq PS \times PS$ is relation describing the meaning of command between $p_1$ and $p_2$ | * $r : E \to 2^{PS \times PS}$, so each $r(p_1,p_2) \subseteq PS \times PS$ is relation describing the meaning of command between $p_1$ and $p_2$ | ||
+ | We can define meaning of program in this form using [[Collecting Semantics]]. | ||
===== Summary of key steps ==== | ===== Summary of key steps ==== | ||
Line 14: | Line 15: | ||
* define lattice ordering $\sqsubseteq$ on $A$ such that $a_1 \le a_2 \rightarrow \gamma(a_1) \subseteq \gamma(a_2)$ | * define lattice ordering $\sqsubseteq$ on $A$ such that $a_1 \le a_2 \rightarrow \gamma(a_1) \subseteq \gamma(a_2)$ | ||
* define $sp^\# : A \times R \to A$ that maps an abstract element and a CFG statement to new abstract element, such that $sp(\gamma(a),r) \subseteq \gamma ( sp^{\#} (a,r))$ | * define $sp^\# : A \times R \to A$ that maps an abstract element and a CFG statement to new abstract element, such that $sp(\gamma(a),r) \subseteq \gamma ( sp^{\#} (a,r))$ | ||
- | (for example, by defining function $\alpha$ so that $(\alpha,\gamma)$ becomes a [[Galois Connection]]) | + | (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$ | ||