Differences
This shows you the differences between two versions of the page.
Next revision | Previous revision Last revision Both sides next revision | ||
sav08:abstract_interpretation [2008/04/29 23:22] vkuncak created |
sav08:abstract_interpretation [2008/04/30 11:02] vkuncak |
||
---|---|---|---|
Line 1: | Line 1: | ||
====== Abstract Interpretation ====== | ====== Abstract Interpretation ====== | ||
- | [[:sav07_lecture_6#Abstract interpretation]] | + | Goal: Invariant Inference by Approximation ====== |
+ | |||
+ | Approximate strongest postcondition $sp$ with operator $sp\#$ whose fixedpoint e.g. has a finite height. | ||
+ | |||
+ | Let PS denote program states and $C = 2^{PS}$ denote the set of all subsets of PS, so $S \subseteq PS$ and $S \in C$ for a set of states S. We introduce an abstract analysis domain A and functions | ||
+ | \begin{equation*} | ||
+ | \begin{array}{l} | ||
+ | \gamma : A \to C \ \ \mbox{concretization function} \\ | ||
+ | \end{array} | ||
+ | \end{equation*} | ||
+ | Instead of working with C, we work with simpler domain A, which is the data structure for analysis. | ||
+ | |||
+ | Examples of A: | ||
+ | * mapping from variables to information about the values they can have (interval analysis, sign analysis, constant propagation) | ||
+ | * formula F (usually in canonical form) such that $\gamma(F) = \{ x. F \}$ | ||
+ | |||
+ | So, we will impose that our domain is partial order. It is useful to require additional property, namely that we have lattice, which have "union"-like and "intersection"-like operations. | ||
+ | |||
+ | Note that $\gamma$ allows us to define set-like operations on A that correspond to operations on A: | ||
+ | \begin{equation*} | ||
+ | a_1 \sqsubseteq a_2 \iff \gamma(a_1) \subseteq \gamma(a_2) | ||
+ | \end{equation*} | ||
+ | |||
+ | Instead of $sp : C \to C$, we have its approximation $sp\# : A \to A$. To be sound we need to have | ||
+ | |||
+ | \begin{equation*} | ||
+ | \gamma(sp\#(a_1,r)) \supseteq sp(\gamma(a_1),r) | ||
+ | \end{equation*} | ||
+ | |||
+ | This is the most important condition for abstract interpretation. | ||
+ | |||
+ | One way to find $sp\#$ it is to have $\alpha$ that goes the other way | ||
+ | \begin{equation*} | ||
+ | \begin{array}{l} | ||
+ | \alpha : C \to A \ \ \mbox{abstraction function} | ||
+ | \end{array} | ||
+ | \end{equation*} | ||
+ | such that | ||
+ | \begin{equation*} | ||
+ | \begin{array}{l} | ||
+ | \gamma(\alpha(S)) \supseteq S \\ | ||
+ | \alpha(\gamma(a)) = a | ||
+ | \end{array} | ||
+ | \end{equation*} | ||
+ | |||
+ | Then we can write a definition of $sp\# : A \to A$ in terms of it: | ||
+ | \begin{equation*} | ||
+ | sp\#(a,r) = \alpha(sp(\gamma(a),r)) | ||
+ | \end{equation*} | ||
+ | and we call this "the best transformer". | ||
+ | |||
+ | |||
+ | ==== Abstract computation of program semantics ==== | ||
+ | |||
+ | In our lattice we have | ||
+ | \begin{eqnarray*} | ||
+ | \gamma(a_1 \sqcup a_2) &\supseteq& \gamma(a_1) \cup \gamma(a_2) | ||
+ | \end{eqnarray*} | ||
+ | because of the way we defined order. | ||
+ | |||
+ | Consider first only a single loop. | ||
+ | |||
+ | Then we rewrite our computation of sp for the loop by replacing $sp$ with $sp\#$ and replacing $\cup$ with $\sqcup$. We obtain fixpoint equation for computing the effect of a transitive closur eof a relation (i.e. a loop): | ||
+ | \begin{equation*} | ||
+ | sp\#(a,r^*) = a \sqcup sp\#(sp\#(a,r),r^*) | ||
+ | \end{equation*} | ||
+ | We can then iterate this equation until it stabilizes. | ||
+ | |||
+ | From the properties of $\gamma$ it follows that the result is approximation of the set of reachable states. | ||
+ | |||
+ | When does it stabilize? Note that the sequence is increasing and if we ever repeat we have stabilized. If there are no infinite ascending chains, the computation terminates. | ||
+ | |||
+ | ==== References ==== | ||
+ | |||
+ | * [[http://www.di.ens.fr/~cousot/COUSOTtalks/VMCAI05_TOOLS.shtml|A Tutorial Abstract Interpretation by the inventor Patrick Cousot]] | ||
+ | * [[:sav07_lecture_7|Approximation Expressed Using Formulas]] | ||
+ | * [[Calculus of Computation Textbook]], Chapter 12 on invariant generation | ||