- English only

# Lab for Automated Reasoning and Analysis LARA

# Live-Variable Analysis

For each program point, and each variable approximately compute whether the variable is:

- definitely not
*live*: its current value will not be used in the future, or - it is possibly live: its value may be used in the future

The precise notion of liveness is given by program semantics, as follows.

**Definition:** a variable is **dynamically live** in a concrete program state , if there exists a control-flow graph execution

(where are control-flow graph nodes, are values of variables), such that

- the statement
**reads**the value of (i.e. it is a test mentioning or an assignment statement with on the right-hand side) - none of the statements
**writes**to (i.e. is an assignment of the form )

We design a data-flow analysis that, for each program point , computes **static liveness** information for program variables, given by the set of variables .

**Correctness statement for liveness analysis:** if then for every program execution that reaches a state , the variable is dynamically live at point .

NOTE: if a static analysis says that the variable is live at program point, the variable may or may not be dynamically live

- but if we know that it is
**not**statically live, this is useful information, we know that it is not dynamically alive

Consider a sequence of instructions:

code | live variables |
---|---|

{z} | |

x = 42 | |

{x,z} | |

y = x + 3 | |

{x,y,z} | |

z = y + z | |

{x} | |

y = 3 + x | |

{} |

Applications:

- allocating space for variables (e.g. register allocation for CPU)
- if variable not used in future, we can store another variable in the same address

- an alternative to initialization analysis: must be initialized if it will be used
- if variable is used in the future before being assigned, it must be initialized now
- we can do initialization check by checking that no variable is live at CFG entry

Liveness is naturally computed using **backwards data-flow analysis**

Consider the program execution backwards

- execution is very non-deterministic (e.g. x=3 goes into all values of x)
- mathematically equally well-defined
- introduce an additional state bit to variable, mark it “used” when it is used
- if a state is reached in backward execution where it is used, then it “will be used”

Corresponding backward analysis:

- variable uses flow towards their initializations
- edges in data-flow analysis are interpreted in the opposite way
- analysis starts from the exit point

Final state at the exit point

- no variable is live - no more statements at the end, so no future uses
- this is also the bottom of the lattice

#### Pointwise Representation

For each variable, store its liveness:

- (potentially) live (top)
- not live (bottom)

Bottom: map each variable to bottom

Join: pointwise join

- bottom top = top

#### An Alternative Representation

The set of potentially live variables, instead of

- consider
- , given by
- this is just a different notation for the same thing

Bottom: empty set

Top: set of all variables

Join: union

## Semilattice for Live-Variable Analysis

(Semilattice is like lattice but need not have meet.)

Elements are sets of live variables

- we assume that variables have been renamed according to scoping rules

Join is union

## Transfer Functions for Live-Variable Analysis

For each statement st in CFG, we introduce sets of variables

- use(st) denote variables used in statement
- def(st) denote variables overwritten in st

For SimpleCFG.scala we have

st | use(st) | def(st) |
---|---|---|

x = y op z | {y,z} | {x} |

x = y | {y} | {x} |

Assume[y relOp z] | {y,z} | {} |

print(y) | {y} |

Examples:

st | use(st) | def(st) |
---|---|---|

x = y + 1 | {y} | {x} |

x = x + 1 | {x} | {x} |

In ordinary execution, statement

- first uses variables in use(st) to compute some value
- then assigns this value to variables in def(st)

In backward execution, statement

- marks def(st) as not live
- marks use(st) as live

in that order

Transfer function

We have seen **forward analyses**, where for each point , we have:

in backward analysis, we instead have:

## References

- Tiger book, Chapter 10, Chapter 17 (page 358)