LARA

This is an old revision of the document!


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) = $

What does the lattice of intervals look like?

Height of lattice of one interval for 64-bit integers:

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