Range Analysis Example
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
which denote the set .
Thus, is the lower bound and is the upper bound. To ensure that we have only a few elements, we let
Example: denotes integers between and .
Furthermore, denotes all possible integers, and we denote it .
Instead of writing and other empty sets, we will always write , whose meaning is empty set, and therefore require that in we have that .
So, we only work with a finite number of sets
Denote the family of these sets by (domain).
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.
denotes the approximation of : it is the set that contains both and , that belongs to , and is otherwise as small as possible.
Also, we need to use approximate functions that give result in .
Now we replace the equations in Sets of States at Each Program Point with approximate equations:
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 ).
Sets after first iteration:
Final values of sets:
- 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
- cannot be zero at point
- value of is always non-negative
With a larger domain we can get better results, but analysis can take longer.