# Range Analysis

## Properties of Interest

A more precise analysis that computes sets to which integer variables belong

- still no relations between variables - independent attribute analysis

For each program point compute interval (or a union of intervals) to which variable belongs

Applications:

- eliminate array bounds checks (and ensuring no run-time error)
- proving that certain parts are not reachable - can encode complex conditions

Encoding conditions: to check that

assert(e)

never fails, we encode it as

if (!e) { ERROR }

and show that ERROR program point is not reachable

## Definition of Analysis Lattice

## Meaning of Lattice Elements

for base lattice of variables - given in comments of RangeAnalysisLattice.scala

We lift it to pointwise, as usual:

If we view map from variables as a labelled n-tuple, then this is just Cartesian product of of components

NOTE: if then

- when analysis finishes, if at program point , then is unreachable

Monotonicity: by construction

Question: does the converse hold?

## Initial Lattice Elements

Bottom has empty intervals for all variables

Assuming all variables are initially zero, what is the initial abstract element?

## Transfer Functions

By definition – many cases, for each CFG statement and each kind of interval

- Assignments
- Tests - detecting branches that will not be taken

## Termination

What is the height of the lattice?

Ensuring termination by widening:

- push elements faster towards unbounded intervals
- if it does not stabilize quickly, jump to infinity