LARA

Differences

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

Link to this comparison view

sav08:abstract_interpretation_recipe [2008/05/08 12:41]
vkuncak 		sav08:abstract_interpretation_recipe [2015/04/21 17:30]
Line 1: Line 1:
-====== Abstract Interpretation Recipe ====== 
- 
-===== Program Representation ===== 
- 
-Control-flow graph: $(V,E,r)$ where  
-  * $V = \{p_1,​\ldots,​p_n\}$ is set of program points 
-  * $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$ 
-We can define meaning of program in this form using [[Collecting Semantics]]. 
- 
-===== Summary of key steps ==== 
- 
-  * design abstract domain $A$ that represents sets of program states 
-  * define $\gamma : A \to C$ giving meaning to elements of $A$ 
-  * 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))$ 
-    (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$) 
-\[ 
-   ​F^{\#​}(g^{\#​})(p_2) = g^{\#}(p_2) \sqcup \bigsqcup_{(p_1,​p_2) \in E} sp^{\#​}(g^{\#​}(p_1),​r(p_1,​p_2)) 
-\] 
-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$): 
-\[ 
-   ​g^{\#​}_* = \bigsqcup_{n \ge 0} (F^{\#​})^{n}(\bot^{\#​}) 
-\] 
- 
-where $\bot^{\#​}(p) = \bot_A$ for all $p \in V$