Differences
This shows you the differences between two versions of the page.
sav08:analyses_based_on_formulas [2010/04/19 13:14] vkuncak |
sav08:analyses_based_on_formulas [2015/04/21 17:30] |
||
---|---|---|---|
Line 1: | Line 1: | ||
- | ====== Analyses Based on Formulas ====== | ||
- | |||
- | Many analyses can be viewed in this way. | ||
- | |||
- | ===== Fixpoint Approach ===== | ||
- | |||
- | Let the domain be the set of quantifier-free formulas of some logic, ordered by implication | ||
- | |||
- | Is this a partial order? ++|We would need to do a quotient construction to obtain it.++ | ||
- | |||
- | Non-existence of limits: infinite disjunction need not be a formula of our logic, e.g. consider formulas on linear arithmetic and take the limit | ||
- | \[ | ||
- | \bigvee_{i=1}^{\infty} y = i x | ||
- | \] | ||
- | In general, a logic that can represent exact least upper bounds needs to express the conditions such as "there exists a sequence of statements that produces the given state". | ||
- | |||
- | |||
- | |||
- | |||
- | ==== Approximation ==== | ||
- | |||
- | Rule for computing formula (called 'fact') in step $k+1$ at program point $p'$ | ||
- | \[ | ||
- | \mbox{fact}^{k+1}(p') := N\left(\mbox{fact}^k(p) \vee \bigvee_{(p,p') \in E} sp^{\#}(\mbox{fact}^k(p),r(p,p'))\right) | ||
- | \] | ||
- | where $N$ is some approximation function. This is analogous to [[Abstract interpretation recipe]]. | ||
- | |||
- | Here the goal of $N$ is to ensure termination (and efficiency). The essential condition is that | ||
- | \[ | ||
- | F \rightarrow N(F) | ||
- | \] | ||
- | is a valid formula. | ||
- | |||
- | One generic approch: use a syntactic widening. | ||
- | |||
- | View formula as a conjunction. Then define | ||
- | \[ | ||
- | \begin{array}{l} | ||
- | N\left( (C_1 \land \ldots \land C_n) \lor (D_1 \land \ldots \land D_m) \right) = \\ | ||
- | \ \ \ \bigwedge (\{C_1, \ldots, C_n \} \cap \{D_1, \ldots, D_m\}) | ||
- | \end{array} | ||
- | \] | ||
- | |||
- | Why are there no infinite chains when using such $N$ ? | ||
- | |||
- | To make it less syntactic: deduce some consequences of the conjunction (taken from a finite set): | ||
- | \[ | ||
- | \begin{array}{l} | ||
- | N\left( (C_1 \land \ldots \land C_n) \lor (D_1 \land \ldots \land D_m) \right) = \\ | ||
- | \ \ \ \bigwedge (conseq(\{C_1, \ldots, C_n \}) \cap conseq(\{D_1, \ldots, D_m\})) | ||
- | \end{array} | ||
- | \] | ||
- | where | ||
- | \[ | ||
- | conseq(S) = \{ F \in U.\ \ (S \rightarrow F) \mbox{ is valid } \} | ||
- | \] | ||
- | where $U$ is some class of useful formulas. | ||
- | |||
- | === References === | ||
- | |||
- | * [[http://citeseer.ist.psu.edu/244634.html|Safety Checking of Machine Code]] described induction iteration method (wp instead of sp) | ||
- | * analysis based on sets in the Hob analysis system | ||
- | |||
- | ===== Constraint-Based Approach ===== | ||
- | |||
- | Give up //least// fixpoint requirement (it is approximation anyway). | ||
- | |||
- | Search for //any// fixpoint - it will be a set of loop invariants: | ||
- | |||
- | \[ | ||
- | \left(\bigvee_{(p,p') \in E} sp^{\#}(\mbox{fact}(p),r(p,p'))\right) \rightarrow \mbox{fact}(p) | ||
- | \] | ||
- | |||
- | Works better if we also have postconditions and assertions that need to be satisfied (otherwise we may come up with trivial invariants). | ||
- | |||
- | Assume a 'template' for the invariant, e.g. (Karr's analysis) each fact is a linear equation $c_1 x_1 + \ldots + c_n x_n = c_0$ on program variables $x_1,\ldots,x_n$. | ||
- | |||
- | The condition for loop invariants gives a system of equations on coefficients $c_0(p),c_1(p),\ldots,c_n(p)$ for each of the finitely many program points $p$. | ||
- | |||
- | If there exists a solution, this gives an invariant. | ||
- | |||
- | <code> | ||
- | X := 10 | ||
- | Y := 0 | ||
- | while (X >= 0) { | ||
- | X := X-1 | ||
- | if random() { Y = Y+1 } | ||
- | } | ||
- | </code> | ||
- | |||
- | Invariant of the form $a_1 X + a_2 Y = a_0$. | ||
- | |||
- | \[ | ||
- | X=10 \land Y = 0 \rightarrow a_1 X + a_2 Y = a_0 | ||
- | \] | ||
- | \[ | ||
- | a_1 X + a_2 Y = a_0 \land X \ge 0 \rightarrow a_1 (X-1) + a_2 Y = a_0 | ||
- | \] | ||
- | \[ | ||
- | a_1 X + a_2 Y = a_0 \land X \ge 0 \rightarrow a_1 (X-1) + a_2 (Y+1) = a_0 | ||
- | \] | ||
- | |||
- | Such equations need to hold for all values of $X$,$Y$, which gives constraints on $a_0,a_1,a_2$ that can be solved based on properties of real fields (linear programming, Farkas lemma). | ||
- | |||
- | Thanks to quantifier elimination for real fields, the technique extends to polynomial invariants as well. | ||
- | |||
- | If there is no solution, there is no invariant **of that particular template form**. | ||
- | |||
- | Note: for non-numerical domains, we obtain different kinds of constraints. A popular class are [[sav08:lecture25|set constraints]]. | ||
- | |||
- | ===== References ===== | ||
- | |||
- | * [[Calculus of Computation Textbook]], Chapter 12 | ||