# Termination and Efficiency of Abstract Interpretation Analysis

Definition: A chain of length is a sequence such that

where means, as usual,

Definition: A lattice has a finite height if it has a chain of length and every chain is of length at most .

A finite lattice is of finite height

Example: The constant propagation lattice is an infinite lattice of height 2. One example chain of length 2 is

Example: If a state of a (one-variable) program is given by an integer, then a concrete lattice element is a set of integers. This lattice has infinite height. There is a chain

for every .

Consider a finite-height lattice

Values at each program point in DataflowAnalysis.scala is monotonically increasing

• stabilization happens in finite number of steps when the lattice has finite height
• at each step the size of lattice in at least one point increases
• termination in |CFG.V| |L.Elem| steps
• in many cases can be shown to be better

## Worklist Algorithm

The simple algorithm in DataflowAnalysis.scala always goes through all vertices

There is no need to go through vertices whose predecessors have not changed

Worklist algorithm:

• maintain a worklist (queue) of vertices whose fact needs to be updated
• initially: put entry into queue
• remove a vertex from queue, compute its new fact
• if the value changed, add all its successors into queue

Can avoid some unnecessary traversals

Note: we can re-order vertices in the queue

• different orderings correspond to different algorithm variations
• useful strategy: iterate over inner loops first