STATIC ANALYSIS�

Key Concepts

• Facts
• Space of properties to track (a set, properly a lattice to support control flow, loops, and reasoning about termination)
• Merging
• How to merge from multiple branches? (joins and and meets)
• Symbolic/Abstract Execution
• How to specify the effect of a basic block on facts? Transfer Functions
• Algorithm
• How to compute? Chaotic Iteration
• Termination
• When does an analysis terminate? (Fixpoints)

Is a Constant in s = s+a*b?

Yes!

On all reaching

definitions

a = 4

Fact/Property

Analysis: Set of Facts/Properties

• An analysis is a set of facts/properties that it tracks.
• Constant Analysis
• Variable has a fact in Z that denotes its known value
• Example: Constant propagation
• Sign Analysis
• A variable has a fact in {0, positive, negative}
• Range Analysis
• Variable has a fact in the set of closed intervals [a, b], where a and b are integers
• Example: trim size of integer representation or check for overflow
• Mark Stephenson, Jonathan Babb and Saman Amarasinghe,�Bidwidth analysis with application to silicon compilation, PLDI'00
• Value Set
• Track set of values of variable
• Example: specialize code to small set of values

​

Key Concepts

• Facts
• Space of properties to track (a set, properly a lattice to support control flow, loops, and reasoning about termination)
• Symbolic/Abstract Execution
• How to specify the effect of a basic block on facts? Transfer Functions
• Merging
• How to merge from multiple branches? (joins and and meets)
• Algorithm
• How to compute? Chaotic Iteration
• Termination
• When does an analysis terminate? (Fixpoints)

Is b Constant in s = s+a*b?

No!

One reaching

definition with

b = 1

One reaching

definition with

b = 2

Merging Facts

• Control flow join points
• Require merging facts to produce a new fact
• New fact should be a union of facts from both branches
• Also, new fact should in the set of facts of the analysis
• Often new fact is an overapproximation – set of values for a new fact may be larger than the union of values of each.
• Introduces a concept of precision – analysis may not tract the most precise fact for a property

​

• Questions, which fact to use as merge? What is “?”

​

• Solution: place facts into a lattice that relate the precision of facts to each other and yield operations for unioning facts together

Merging Facts

Constant

Sign

Interval

Set

Merging Facts

Constant

Sign

Interval

Set

Merging Facts

Constant

Sign

Interval

Set

Merging Facts

Constant

Sign

Interval

Set

Part 2

Merging Facts

• Control flow join points
• Require merging facts to produce a new fact
• New fact should be a union of facts from both branches
• Also, new fact should in the set of facts of the analysis
• Often new fact is an overapproximation – set of values for a new fact may be larger than the union of values of each.
• Introduces a concept of precision – analysis may not tract the most precise fact for a property

​

• Questions, which fact to use as merge? What is “?”

​

• Solution: place facts into a lattice that relate the precision of facts to each other and yield operations for unioning facts together

Partial Orders

Saman Amarasinghe 15 6.035 ©MIT Fall 1998

Top and Bottom

• Greatest element of P (if it exists) is top (T)
• Typically, the least precise element
• Often means variable takes on any possible value
• This is our “?” from before.
• Least element of P (if it exists) is bottom (⊥)
• Typically denotes “unprocessed” or a “unknown” in the sense that we have no information about it. For example, may denote the empty set in a value analysis meaning we know of no potential values for it – if true, variable has yet to be executed in the analysis or is unreachable code

Saman Amarasinghe 16 6.035 ©MIT Fall 1998

Lattice of Facts/Properties (Hasse Diagram)

• Arrow from y to x indicates that x <= y.

​

​

​

​

​

​

​

• ��

​

​

Constant

Sign

Bounded Interval

Bounded Set

Upper Bounds

Saman Amarasinghe 18 6.035 ©MIT Fall 1998

Lattice of Facts/Properties

• Arrow from y to x indicates that x <= y.

​

​

​

​

​

​

​

• ��

​

​

Constant

Sign

Bounded Interval

Bounded Set

Lower Bounds

Saman Amarasinghe 20 6.035 ©MIT Fall 1998

Lattice of Facts/Properties

• Arrow from y to x indicates that x <= y.

​

​

​

​

​

​

​

• ��

​

​

Constant

Sign

Bounded Interval

Bounded Set

Merging Facts (use join operator)

Constant

Sign

Interval

Set

Lattice of Facts/Properties

• Arrow from y to x indicates that x <= y.

​

​

​

​

​

​

​

• ��

​

​

Constant

Sign

Bounded Interval

Bounded Set

Lattice (as Hasse Diagram)

• For a set P and partial order ≤ such that ∀x,y,z∈P
• �If x ∨ y (join/lub) and x ∧ y (meet/glb)�exist for all x,y∈P then P is a lattice

Saman Amarasinghe 24 6.035 ©MIT Fall 1998

Key Concepts

• Facts
• Space of properties to track (a set, properly a lattice to support control flow, loops, and reasoning about termination)
• Merging
• How to merge from multiple branches? (joins and and meets)
• Symbolic/Abstract Execution
• How to specify the effect of a basic block on facts? Transfer Functions

Algorithm

• How to compute? Chaotic Iteration
• Termination
• When does an analysis terminate? (Fixpoints)

Is a Constant in s = s+a*b?

Yes!

On all reaching

definitions

a = 4

Transfer Functions

Transfer Function - Constant

• Fact for operand is either integer constant or “?”

​

• x = n

​

​

• x = y + z

​

​

• x = y – z

​

Transfer Function - Sign

• Fact for operand is either 0, +, -, or “?”
• �x = n

​

​

• x = y + z

​

​

• x = y – z

​

Computing transfer function

• Define a transfer function specific to the lattice
• For finite lattices they can be implemented cheaply in terms of bitvector operations

​

• Build lattices for arbitrary facts about the program
• Need to make sure our transfer functions are monotonic

Part 2

Key Concepts

• Facts
• Space of properties to track (a set, properly a lattice to support control flow, loops, and reasoning about termination)
• Merging
• How to merge from multiple branches? (joins and and meets)
• Symbolic/Abstract Execution
• How to specify the effect of a basic block on facts? Transfer Functions
• Algorithm
• How to compute? Chaotic Iteration
• Termination
• When does an analysis terminate? (Fixpoints)

Forward Dataflow Analysis

Program Equations

1

4

0

2

3

5

Chaotic Iteration

P2

P1

P3

P5

Is b Constant in s = s+a*b?

1

4

0

2

3

5

Is b Constant in s = s+a*b?

1

4

0

2

3

5

Is b Constant in s = s+a*b?

1

4

0

2

3

5

Is b Constant in s = s+a*b?

1

4

0

2

3

5

Is b Constant in s = s+a*b?

1

4

0

2

3

5

Is b Constant in s = s+a*b?

1

4

0

2

3

5

Is b Constant in s = s+a*b?

1

4

0

2

3

5

Is b Constant in s = s+a*b?

1

4

0

2

3

5

Is b Constant in s = s+a*b?

1

4

0

2

3

5

Is b Constant in s = s+a*b?

1

4

0

2

3

5

Is b Constant in s = s+a*b?

Add three? No, already in queue

1

4

0

2

3

5

Is b Constant in s = s+a*b?

1

4

0

2

3

5

Is b Constant in s = s+a*b?

1

4

0

2

3

5

Is b Constant in s = s+a*b?

1

4

0

2

3

5

Is b Constant in s = s+a*b?

1

4

0

2

3

5

Is b Constant in s = s+a*b?

1

4

0

2

3

5

Is b Constant in s = s+a*b?

1

4

0

2

3

5

Is b Constant in s = s+a*b?

1

4

0

2

3

5

Is b Constant in s = s+a*b?

1

4

0

2

3

5

Is b Constant in s = s+a*b?

1

4

0

2

3

5

Is b Constant in s = s+a*b?

1

4

0

2

3

5

Is b Constant in s = s+a*b?

1

4

0

2

3

5

Is b Constant in s = s+a*b?

1

4

0

2

3

5

Is b Constant in s = s+a*b?

1

4

0

2

3

5

Is b Constant in s = s+a*b?

1

4

0

2

3

5

Is b Constant in s = s+a*b?

1

4

0

2

3

5

Is b Constant in s = s+a*b?

1

4

0

2

3

5

Is b Constant in s = s+a*b?

1

4

0

2

3

5

Is b Constant in s = s+a*b?

1

4

0

2

3

5

Is b Constant in s = s+a*b?

1

4

0

2

3

5

Is b Constant in s = s+a*b?

1

4

0

2

3

5

Is b Constant in s = s+a*b?

1

4

0

2

3

5

Is b Constant in s = s+a*b?

1

4

0

2

3

5

Is b Constant in s = s+a*b?

1

4

0

2

3

5

Is b Constant in s = s+a*b?

1

4

0

2

3

5

Is b Constant in s = s+a*b?

1

4

0

2

3

5

Is b Constant in s = s+a*b?

1

4

0

2

3

5

Is b Constant in s = s+a*b?

1

4

0

2

3

5

Is b Constant in s = s+a*b?

1

4

0

2

3

5

Is b Constant in s = s+a*b?

1

4

0

2

3

5

Is b Constant in s = s+a*b?

1

4

0

2

3

5

Is b Constant in s = s+a*b?

1

4

0

2

3

5

Programs to systems of equations

Need to combine the properties that are true on each branch

Equations on a Control Flow Graph

<-P1

<-P2

<-P3

<-P2

<-P5

P2

P1

P3

P5

Checkpoint

• 1) So we have defined a lattice of program properties

​

• 2) Now we have to define how individual program statements define the relationship between the properties that are true before the statement and the properties that are true after the statement.

​

• 3) These lead to a system of equations that will be solved iteratively

What about termination?

Key Concepts

• Facts
• Space of properties to track (a set, properly a lattice to support control flow, loops, and reasoning about termination)
• Symbolic/Abstract Execution
• How to specify the effect of a basic block on facts? Transfer Functions
• Merging
• How to merge from multiple branches? (joins and and meets)
• Algorithm
• How to compute? Chaotic Iteration
• Termination
• When does an analysis terminate? (Fixpoints)

Termination

• How does algorithm terminate?

i = i + 1;

i = 0

i < n

Termination

• How does algorithm terminate?

i = i + 1;

i = 0

i < n

Termination

• How does algorithm terminate?

i = i + 1;

i = 0

i < n

Constant

Termination

• How does algorithm terminate?

i = i + 1;

i = 0

i < n

Termination

• How does algorithm terminate?

i = i + 1;

i = 0

i < n

Termination

• How does algorithm terminate?

i = i + 1;

i = 0

i < n

Reaches fixpoint!

Termination

• How does algorithm terminate?

i = i + 1;

i = 0

i < n

i = i + 1;

i = 0

i < n

Reaches fixpoint!

Termination

• How does algorithm terminate?

i = i + 1;

i = 0

i < n

i = i + 1;

i = 0

i < n

Reaches fixpoint!

Termination

• How does algorithm terminate?

i = i + 1;

i = 0

i < n

i = i + 1;

i = 0

i < n

Reaches fixpoint!

Termination

• How does algorithm terminate?

i = i + 1;

i = 0

i < n

i = i + 1;

i = 0

i < n

Reaches fixpoint!

Termination

• How does algorithm terminate?

i = i + 1;

i = 0

i < n

i = i + 1;

i = 0

i < n

Reaches fixpoint!

Termination

• How does algorithm terminate?

i = i + 1;

i = 0

i < n

i = i + 1;

i = 0

i < n

Reaches fixpoint!

Termination

• How does algorithm terminate?

i = i + 1;

i = 0

i < n

i = i + 1;

i = 0

i < n

Reaches fixpoint!

Termination

• How does algorithm terminate?

i = i + 1;

i = 0

i < n

i = i + 1;

i = 0

i < n

Reaches fixpoint!

Runs forever!

Termination

• How does algorithm terminate?

​

• Key idea: design analysis so that on each step, analysis properties are ascending: either as precise or less precise than before. Analysis iterates until it reaches least fixpoint: the most precise fixpoint of analysis.
• Requirements for this work:
• Transfer functions are monotone: analysis always ascends lattice
• Lattice must be complete: always a least upper bound to reach.
• Monotonicity + completeness = always a least fixpoint to reach
• Lattice must have finite ascending chains: # iterations required to hit least fixpoint must be finite.

Monotonicity

Ascending Chains

Saman Amarasinghe 98 6.035 ©MIT Fall 1998

Complete Lattice

• For analysis to terminate there must be an upper bound to the chain.

​

• If x ∧ y and x ∨ y exist for all x,y∈P
• then P is a lattice.

​

• If ∧S and ∨S exist for all S ⊆ P
• then P is a complete lattice

​

• Completeness ensures that all chains (take S = set of elements in chain) have an upper bound.

Saman Amarasinghe 99 6.035 ©MIT Fall 1998

Termination

Potential Failures

Saman Amarasinghe 101 6.035 ©MIT Fall 1998

�

Incomplete Lattice

Example of a lattice that is not complete?

• P = Intervals over Z (all integers)
• P is a lattice
• For any [l1, u1], [l2, u2] ∈I,

[l1,u1] ∨ [l2, u2] = [min(l1,l2), max(u1,u2)]

• meet is intersection of intervals
• But ∨P does not exist

​

Intervals over Z ∪ {+∞,−∞ } is complete

​

…

…

Infinite Ascending Chains

Saman Amarasinghe 103 6.035 ©MIT Fall 1998

…

…

Knaster-Tarski Theorem

Values (Constant Propagation)

• Flat lattice on the integers.

​

​

​

​

​

​

​

​

• We’ve seen this many times in these lectures.

Types (Eliminate type checks)

• We can also use dataflow analysis to infer the type of variables in the function
• Transformation: given types, eliminate checks or specialize operators (e.g., arguments to + are strings)

​

• Lattice:
• Simple flat lattice of types
• One lattice value for each variable

​

​

​

​

​

• Can increase precision by tracking subsets of values

​

Int

String

None

Record

Function

Types (Eliminate type checks)

Register Allocation (Stack Caching)

• For each instruction in your function, you can statically compute what position in the stack it will read/write
• Transformation: a priori assign each stack height a register. Translate code to access register.�
• Lattice:
• This can be done with the simple constant propagation lattice

​

​

​

​

​

​

• One element corresponding to current length of the stack

Stack Positions (Stack Caching)

• For each instruction in your function, you can statically compute what position in the stack it will read/write
• Transformation: a priori assign each stack height a register. Translate code to access register

​

• Initial value:
• The stack starts with length 0

​

• Transfer function:
• For every instruction we can increment/decrement the abstract value for the stack length based on the number of elements pushed and popped by the instruction.

Static Analysis Implementations

• Three conceptual approaches:
• Wing it and write some code.
• You will probably get something to work. But reasoning for why it works will likely be pretty ad hoc.
• Dataflow as semantic framework
• Principled reasoning about the correctness of your implementation of above will almost certainly resemble reasoning about lattices, joins/meets, transfer functions, monotonicity, termination, etc.
• Structure your implementation to roughly reflect concepts here and reason about your implementation using what we’ve covered
• Dataflow as implementation framework
• Define an analysis framework parameterized by transfer function, lattice, that automatically applies a worklist algorithm to compute results. Production compilers often have such a framework because they use many analyses and w.
• Useful when you have several different static analysis to run as you only need one algorithmic implementation. May introduce lots of unnecessary complexity for P5.

​

​

​

Looking forward

Your static analysis can impose significant overhead for dynamic compilation. Make sure the expense is worth it.

​

An alternative, is dynamic analysis.

Dynamically record trace of program and facts that hold, generate code just as the same in – but insert guards that jump to unoptimized code in case program behavior changes and facts are no longer true.

Not an easy approach in general: which guards to generate and where? Surprise: requires static analysis.

Complete Lattice

• If x ∧ y and x ∨ y exist for all x,y∈P
• then P is a lattice

​

• If ∧S and ∨S exist for all S ⊆ P
• then P is a complete lattice

​

• All finite lattices are complete
• Example of a lattice that is not complete?
• Integers I with standard <= partial order
• For any x, y∈I, x ∨ y = max(x,y), x ∧ y = min(x,y)
• But ∨ I and ∧ I do not exist
• I ∪ {+∞,−∞ } is a complete lattice

Saman Amarasinghe 112 6.035 ©MIT Fall 1998

Finite Ascending Chains

A set S is a chain if ∀x,y∈S. y ≤ x or x ≤ y

All chains in P must be finite

​

​

​

Liveness Analysis

Escape analysis

• Lattices have represented the values of each variable
• For this analysis lattice values are associated with constructors and operations
• we want to know whether the object created by a particular operation can escape the function
• Lattice:

​

​

​

​

• What if a value never escapes?
• it means this value is only used locally in the function.
• Can be allocated in the stack instead of the heap

(may escape)

(private)

Escape analysis

• A value may escape in four ways:
• passed to another function call
• returned by the function
• assigned to a field of a record
• assigned to a global variable

[{v1}=p, {v2}=p, {v3}=p]

[{v1}=me, {v2}=p, {v3}=p]

[{v1}=me, {v2}=p, {v3}=me]

fun(x, y){

t = {v1: x + y};

v = foo(t);

t = {v2: x – y} ;

v.x = {v3: t.v2 + 1};

return v;

}

Three records created:

{v1: x + y},

{v2: x - y},� {v3: t.v2 + 1}

Example: Reaching Definitions

• Concept of definition and use
• a = x+y
• is a definition of a
• is a use of x and y
• A definition reaches a use if
• value written by definition
• may be read by use

Saman Amarasinghe 117 6.035 ©MIT Fall 1998

Reaching Definitions and Constant Propagation

• Is a use of a variable a constant?
• Check all reaching definitions
• If all assign variable to same constant
• Then use is in fact a constant
• Can replace variable with constant

Saman Amarasinghe 118 6.035 ©MIT Fall 1998

Is a Constant in s = s+a*b?

Yes!

On all reaching

definitions

a = 4

Constant Propagation Transform

Yes!

On all reaching

definitions

a = 4

Is b Constant in s = s+a*b?

No!

One reaching

definition with

b = 1

One reaching

definition with

b = 2

Covering

• x< y if x ≤ y and x≠y
• x is covered by y (y covers x) if
• x < y, and
• x ≤ z < y implies x = z
• Conceptually,
• y covers x if there are no elements between x and y

Saman Amarasinghe 123 6.035 ©MIT Fall 1998

Lattice (as Hasse Diagram)

• If x ∧ y and x ∨ y exist for all x,y∈P
• then P is a lattice

�If y covers x

• Line from y to x
• y above x in diagram

Can be arbitrarily deep

• Consider: Pos, neg, nonneg, nonpos

​

​

Saman Amarasinghe 124 6.035 ©MIT Fall 1998

111

011

101

110

010

001

000

100

• P = { 000, 001, 010, 011, 100, 101, 110, 111}

(standard boolean lattice, also called hypercube)

• x ≤ y iff (x & y) = x where & is bitwise and

Lattices

• If x ∧ y and x ∨ y exist for all x,y∈P
• then P is a lattice

​

Saman Amarasinghe 125 6.035 ©MIT Fall 1998

Facts

• Properties of interest can often be arranged into a lattice

​

​

​

​

​

​

• ��

​

• If the value of each variable is a lattice, the state of the program is a product lattice of the states of all variables.

Facts

• Properties of interest can often be arranged into a lattice

​

​

​

​

​

​

• ��

​

• If the value of each variable is a lattice, the state of the program is a product lattice of the states of all variables.

Types

Constants

Stack Depth

Product Latices