- English only

# Lab for Automated Reasoning and Analysis LARA

# Widening and Narrowing in Variable Range Analysis

Interval analysis domain, for each program point, maps each program variable to an interval.

Analysis domain has elements where denotes the set of such intervals.

Height of lattice for unbounded integers: infinite.

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

Moreover, if we have variables in program and program points, height of lattice for the analysis domain is times larger.

How to guarantee (reasonably fast) termination?

**Widening technique:** if the iteration does not seem to be converging, take a “jump” and make the interval much **wider** (larger).

Finite set of *jump points* (e.g. set of all integer constants in the program)

In fixpoint computation, compose with function

We require the condition:

for all .

The condition holds for the example above.

Approaches:

- always apply widening (we will assume this)
- iterate a few times with only (without using ), if we are not at 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:

Widening:

**Example where widening works nicely**

Consider program:

x = 0; while (x < 1000) { x = x + 1; }

Interval analysis without widening will need around 1000 iterations to converge to interval for at the end of the program. This may be too slow.

Let us derive the set by taking all constants that appear in the program, as well as and :

After a few iterations, widening maps interval into . This gives for at loop entry and again for at the end of the program, but in many fewer iterations.

**Example showing problems with widening**

Consider program:

x = 0; y = 1; while (x < 1000) { x = x + 1; y = 2*x; y = y + 1; print(y); }

Interval analysis without widening will need around 1000 iterations to converge to

This may be too slow.

Now apply widening with the same as before. When within loop we obtain , applying widening function to the interval for results in . We obtain at the end of the program:

# Narrowing

## Observation

Consider a monotonic function, such as on the set of real numbers. If we consider a sequence this sequence is monotonically increasing iff (e.g. for ) and it is monotonically decreasing iff (e.g. for ). Informally, the sequence continues of the direction in which it starts in the first step.

This is because implies by monotonicity of that etc., whereas implies .

## The Idea

Let such that .

After finding fixpoint of , apply to improve precision.

## Widen and Narrow

**Lemma:** Let and be monotonic functions on a partial order such that for all . Define the following:

where we also assume that the two and one exist. Then

- is the least fixpoint of and , is the least fixpoint of (by Tarski's Fixpoint Theorem), and
- .

**Proof:**
By induction, for each we have

Thus by Comparing Fixpoints of Sequences, we have .

Next, we have that

Thus, . From there by induction and monotonicity of we obtain

i.e. the sequence is **decreasing**. Therefore, is its upper bound and therefore .

On the other hand, we have by monotonicity of , the fact that is fixpoint, and that:

Thus, is the lower bound on , so .

**End of proof.**

Note: even if does not exist, we can simply compute for any chosen value of , it is still a sound over-approximation, because it approximates , which approximates the concrete value:

so

Being able to stop at any point gives us an **anytime algorithm**.

## Example

**Example showing how narrowing may improve result after widening**

In the above example for the program, the results obtained using widening are:

x = 0; y = 1; // x -> [0,0], y -> [1,1] // (merge point) // x -> [0,1000], y -> [1,+infty) while (x < 1000) { // x -> [0,999], y -> [1,+infty) x = x + 1; // x -> [0,1000], y -> [1,+infty) y = 2*x; // x -> [0,1000], y -> [0,+infty) y = y + 1; // x -> [0,1000], y -> [1,+infty) print(y); } // x -> [1000,1000], y -> [1,+infty)

Let us now apply one ordinary iteration, without widening. We obtain:

x = 0; y = 1; // x -> [0,0], y -> [1,1] // (merge point) // x -> [0,1000], y -> [1,2001] while (x < 1000) { // x -> [0,999], y -> [1,+infty) x = x + 1; // x -> [0,1000], y -> [1,+infty) y = 2*x; // x -> [0,1000], y -> [0,2000] y = y + 1; // x -> [0,1000], y -> [1,2001] print(y); } // x -> [1000,1000], y -> [1,2001]

Thus, we obtained a good first approximation by a few iterations with widening and then improved it with a single iteration without widening.