[Theory] Static Program Analysis
5. Dataflow Analysis with Monotone Frameworks
Dataflow Analysis
- Sign Analysis
- Constant Propagation Analysis
- Live Variables Analysis
- Available Expressions Analysis
- Very Busy Expressions Analysis
- Reaching Definitions Analysis
- Initialized Variables Analysis
Classical dataflow analysis starts with a CFG and a lattice with finite height. The lattice describes abstract information we wish to infer for the different CFG nodes.
The combination of a lattice and a space of monotone functions is called a monotone framework.
An analysis is sound if all solutions to the constraints correspond to correct information about the program. The solutions may be more or less imprecise, but computing the least solution will give the highest degree of precision possible.
- naive fixed-point algorithm
- round-robin algorithm
- chaotic-iteration algorithm
- work-list algorithm
A variable is live at a program point if there exists an execution where its value is read later in the execution without it is being written to in between. Clearly undecidable, this property can be approximated by a static analysis called live variables analysis (or liveness analysis).
The typical use of live variables analysis is optimization: there is no need to store the value of a variable that is not live. For this reason, we want the analysis to be conservative in the direction where the answer “not live” can be trusted and “live” is the safe but useless answer.
- parameterized lattice
The set of available expressions for all program points can be approximated using a dataflow analysis.
An expression is very busy if it will definitely be evaluated again before its value changes.
The reaching definitions for a given program point are those assignments that may have defined the current values of variables.
A dataflow analysis is specified by providing the lattice and the constraint rules.
A forward analysis is one that for each program point computes information about the past behavior. A backward analysis is one that for each program point computes information about the future behavior.
A may analysis is one that describes information that may possibly be true and, thus, computes an over-approximation. Conversely, a must analysis is one that describes information that must definitely be true and, thus, computes an under-approximation.
| Forward | Backward | |
|---|---|---|
| May | Reaching Definitions | Live Variables |
| Must | Available Expressions | Very Busy Expressions |
- transfer function
6. Widening
（待续）
