Differences
This shows you the differences between two versions of the page.
sav08:interval_analysis_and_widening [2008/05/20 20:32] vkuncak |
sav08:interval_analysis_and_widening [2015/04/21 17:30] |
||
---|---|---|---|
Line 1: | Line 1: | ||
- | ====== Interval Analysis and Widening ====== | ||
- | Interval analysis domain, for each program point, maps each program variable to an interval. | ||
- | |||
- | Interval bounds may be $-\infty$ and $+\infty$. Interval $[-\infty,+\infty]$ represents no constraints. | ||
- | |||
- | Analysis domain has elements $m : V \to I$ where $I$ denotes the set of such intervals. | ||
- | |||
- | How to interpret a command | ||
- | \[ | ||
- | x = y \otimes z | ||
- | \] | ||
- | for some operation $\otimes$? | ||
- | |||
- | $m(x) = $ ++++| | ||
- | \[ | ||
- | [\min \{v_y \otimes v_z \mid v_y \in m(y), v_z \in m(z) \}, | ||
- | \max \{v_y \otimes v_z \mid v_y \in m(y), v_z \in m(z) \}] | ||
- | \] | ||
- | ++++ | ||
- | |||
- | What does the lattice of intervals look like? | ||
- | |||
- | Height of lattice of one interval for 64-bit integers: ++|around $2^{64}$++ | ||
- | |||
- | If we have $K$ variables in program and $N$ program points, height of lattice for the analysis domain is $K N$ times larger. | ||
- | |||
- | For unbounded integers, lattice is unbounded. | ||
- | |||
- | How to guarantee termination? | ||
- | |||
- | Widening technique: if we do not seem to be converging, make a "jump". | ||
- | |||
- | Finite set of "jump points" $J$ (e.g. set of all integer constants in the program) | ||
- | |||
- | In fixpoint computation, compose $H_i$ with function | ||
- | \[ | ||
- | w([a,b]) = [\max \{x \in J \mid x \le a\}, | ||
- | \min \{x \in J \mid b \le x\}] | ||
- | \] | ||
- | |||
- | Approaches: | ||
- | * always apply widening (we will assume this) | ||
- | * iterate a few times with $H_i$ only (without using $w$), if not a fixpoint at this program point, then widen. | ||
- | * this is not monotonic: if you start at fixpoint, it converges, if start below, can jump over fixpoint | ||
- | |||
- | Standard iteration: $\bot, \ldots, (F^{\#})^n(\bot), \ldots$ | ||
- | |||
- | Widening: $\bot, \ldots, ((W \circ F)^{\#})^n(\bot), \ldots$ | ||
- | |||
- | |||
- | Here, $x \sqsubseteq W(x)$ for all $x$ by definition of $W$ | ||
- | |||
- | Narrowing: after finding fixpoint of $(W \circ F)^{\#}$, apply $F^{\#}$ to improve precision. | ||
- | |||
- | Observation: if $F^{\#}$ and $W$ are $\omega$-continuous functions and $x \sqsubseteq W(x)$ for all $x$, then narrowing will improve the result, that is, if $x_* = lfp F^{\#}$ and $y_* = lfp (W \circ F^{\#})$, then | ||
- | \[ | ||
- | x_* = F(x_*) \sqsubseteq F^{\#}(y_*) \sqsubseteq (W \circ F^{\#})(y_*) \sqsubseteq y_* | ||
- | \] | ||
- | |||
- | |||
- | ===== References ===== | ||
- | |||
- | * {{sav08:schwartzbach.pdf|M. Schwartzbach's lecture notes}}, page 32 | ||
- | * [[http://www.di.ens.fr/~cousot/COUSOTpapers/POPL77.shtml|Cousot, Cousot: Abstract Interpretation Paper]] |