Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav07_lecture_7 [2007/04/18 03:00] philippe.suter |
sav07_lecture_7 [2009/04/08 01:26] vkuncak |
||
---|---|---|---|
Line 1: | Line 1: | ||
====== Lecture 7: Formulas as a unifying domain for static analysis ====== | ====== Lecture 7: Formulas as a unifying domain for static analysis ====== | ||
+ | |||
Line 54: | Line 55: | ||
Analysis stops when $\forall v. \mbox{fact}_{i+1}(v) \rightarrow \mbox{fact}_i(v)$. That is, no new states are generated by strongest postcondition (we have reached a fix point - formula not trivial). | Analysis stops when $\forall v. \mbox{fact}_{i+1}(v) \rightarrow \mbox{fact}_i(v)$. That is, no new states are generated by strongest postcondition (we have reached a fix point - formula not trivial). | ||
- | __Note__: If you end up with a situation where $\exists$ a state $v$ for which $\mbox{fact}(v) = true$, then the analysis is useless. In this case, you may want to refine $A$ (and hence also change the function $N$). Sometimes, this can be done automatically. | + | __Note__: If you end up with a situation where $\exists$ a state $v$ for which $\mbox{fact}(v) = true$, then the analysis gives no useful information about state $v$. In this case, you may want to refine $A$ (and hence also change the function $N$). Sometimes, this can be done automatically. |
===== Examples ===== | ===== Examples ===== | ||
Line 119: | Line 120: | ||
The fact that we only used conjunctions is our analysis makes it **path-insensitive**. Intuitively, since we're only taking conjunctions, our normalization is too conservative and we will not be able to retain properties associated to certain paths. **Path-sensitivity** is often used as a measure of the precision of an analysis. | The fact that we only used conjunctions is our analysis makes it **path-insensitive**. Intuitively, since we're only taking conjunctions, our normalization is too conservative and we will not be able to retain properties associated to certain paths. **Path-sensitivity** is often used as a measure of the precision of an analysis. | ||
+ | |||
Line 132: | Line 134: | ||
$A^+ = \{ \bigvee (P_{i1} \wedge ... \wedge P_{in}) | P_{ij} \in \{Q_1, ..., Q_n\}) \}$ | $A^+ = \{ \bigvee (P_{i1} \wedge ... \wedge P_{in}) | P_{ij} \in \{Q_1, ..., Q_n\}) \}$ | ||
- | The use of disjunctions allows us to write predicates about attributes for some particular paths. For this reason, this is called **regional** (or **dependent**) **attribute analysis**. | + | The use of disjunctions allows us to write predicates about attributes for some particular paths. For this reason, this is called **relational** (or **dependent**) **attribute analysis**. |
If we go back to our previous example, we could end up with a predicate at the final point which would look (at least partially) somehow like: | If we go back to our previous example, we could end up with a predicate at the final point which would look (at least partially) somehow like: | ||
Line 158: | Line 160: | ||
* [[predicate abstraction]] (Cartesian abstraction) | * [[predicate abstraction]] (Cartesian abstraction) | ||
* [[http://research.microsoft.com/esp/pubs/esp-dataflow.pdf|ESP paper]] | * [[http://research.microsoft.com/esp/pubs/esp-dataflow.pdf|ESP paper]] | ||
+ | |||
==== Linear inequalities ==== | ==== Linear inequalities ==== | ||
+ | |||
+ | (section not covered in class) | ||
Example implementation: [[http://www.cs.unipr.it/ppl/|Parma Polyhedra Library]] and a [[http://www.cs.unipr.it/ppl/Documentation/BagnaraHZ06TR.pdf|paper about Parma]]. Geometric interpretation of linear equations. | Example implementation: [[http://www.cs.unipr.it/ppl/|Parma Polyhedra Library]] and a [[http://www.cs.unipr.it/ppl/Documentation/BagnaraHZ06TR.pdf|paper about Parma]]. Geometric interpretation of linear equations. |