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


  • 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


never fails, we encode it as

if (!e) {

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

     m \sqsubseteq m'  \ \leftrightarrow\ \forall x \in Var.\ m(x) \sqsubseteq_0 m'(x)

Meaning of Lattice Elements

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

We lift it to $\gamma$ pointwise, as usual:

   \gamma(m) = \{ c : Var \to Int \mid \forall x \in Var.\ c(x) \in \gamma_0(m(x)) \}

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

NOTE: if $m(x)=\emptyset$ then $\gamma(m)=\emptyset$

  • when analysis finishes, if $m(x)=\emptyset$ at program point $P$, then $P$ is unreachable

Monotonicity: by construction

    m \sqsubseteq m' \ \rightarrow \gamma(m) \subseteq \gamma(m')

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


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