# 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

For each variable: RangeAnalysisLattice.scala

Pointwise lattice - a range for each variable

## 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