Range Analysis Example

Analysis Domain

Continue the example from Sets of States at Each Program Point but instead of allowing to denote all possible sets, we will allow sets represented by expressions

$\begin{equation*} [L, U] \end{equation*}$

which denote the set $\{ x \mid L \le x \land x \le U \}$ .

Thus, $L$ is the lower bound and $U$ is the upper bound. To ensure that we have only a few elements, we let

$\begin{equation*} L, U \in \{ \mbox{MININT}, -128, 1, 0, 1, 127, \mbox{MAXINT} \} \end{equation*}$

Example: $[0,127]$ denotes integers between $0$ and $127$ .

Furthermore, $[\mbox{MININT},\mbox{MAXINT}]$ denotes all possible integers, and we denote it $\top$ .

Instead of writing $[1,0]$ and other empty sets, we will always write $\bot$ , whose meaning is empty set, and therefore require that in $[L,U]$ we have that $L \le U$ .

So, we only work with a finite number of sets

$\begin{equation*} 1 + {7 \choose 2} = 22 \end{equation*}$

Denote the family of these sets by $D$ (domain).

Initial Sets

In the 'entry' point, we put $\top$ , in all others we put $\bot$ .

Updating Sets

Now we want to write the same set of equations. But because we have only a finite number of sets, we must approximate. We approximate sets with possibly larger sets.

$S_1 \sqcup S_2$ denotes the approximation of $S_1 \cup S_2$ : it is the set that contains both $S_1$ and $S_2$ , that belongs to $D$ , and is otherwise as small as possible.

Also, we need to use approximate functions $T^\#(S,c)$ that give result in $D$ .

Now we replace the equations in Sets of States at Each Program Point with approximate equations:

$\begin{equation*} \begin{array}{l} S^\#(a) = \top \\ S^\#(b) = T^\#(S^\#(a),i=0) \sqcup T(S(g),skip) \\ S^\#(c) = T^\#(S^\#(b),[\lnot(i<10)]) \\ S^\#(d) = T^\#(S^\#(b),[i<10]) \\ S^\#(e) = T^\#(S^\#(d),[i>1]) \\ S^\#(f) = T^\#(S^\#(d),[\lnot(i>1)]) \\ S^\#(g) = T^\#(S^\#(e),i=i+3) \sqcup T(S(f),i=i+2) \end{array} \end{equation*}$

We solve the equations by starting in the initial state and repeatedly applying them. One can prove that (because this computation is monotonic), the sequence is growing and must terminate (in worst case when all sets are $\top$ ).

Sets after first iteration:

Final values of sets:

Note:

analysis terminates even if the original program does not terminate or takes very long (important for a compiler!)
it proves that:
- in all executions i=0 at point $f$
- $i$ cannot be zero at point $e$
- value of $i$ is always non-negative

With a larger domain $D$ we can get better results, but analysis can take longer.