Differences

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

--- sav08:interval_analysis_and_widening [2008/05/20 20:34]
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_* \sqsubseteq y_*$ and
-\[
-    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]]