LARA

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

\begin{equation*} x = y \otimes z \end{equation*}

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

\begin{equation*} w([a,b]) = [\max \{x \in J \mid x \le a\}, \min \{x \in J \mid b \le x\}] \end{equation*}

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

\begin{equation*} x_* = F^{\#}(x_*) \sqsubseteq F^{\#}(y_*) \sqsubseteq (W \circ F^{\#})(y_*) \sqsubseteq y_* \end{equation*}

References