Contents
1 Introduction 1
1.1 The Nature of Program Analysis 1
1.2 Setting the Scene o o 3
1.3 Data Flow Analysis o 5
1.301 The Equational Approach 5
1.302 The Constraint Based Approach 8
1.4 Constraint Based Analysis o 10
1.5 Abstract Interpretation 13
1.6 Type and Effect Systems o 17
1.601 Annotated Type Systems 18
1.602 Effect Systems 22
1.7 Algorithms o o o 25
1.8 Transformations 27
Concluding Remarks 29
Mini Projects 29
Exercises o o 31
2 Data Flow Analysis 35
201 Intraprocedural Analysis o o o ••••• 35
201.1 A vailable Expressions Analysis 39
201.2 Reaching Definitions Analysis o 43
201.3 Very Busy Expressions Analysis 46
201.4 Live Variables Analysis ••• o • 49
201.5 Derived Data Flow Information o 52
XII Contents
2.2 Theoretical Properties . . . . . . . . . . . 54
2.2.1 Structural Operational Semantics . 54
2.2.2 Correctness of Live Variables Analysis 60
2.3 Monotone Frameworks . 65
2.3.1 Basic Definitions 67
2.3.2 The Examples Revisited . 70
2.3.3 A Non-distributive Example. 72
2.4 Equation Solving . . . . . 74
2.4.1 The MFP Solution 74
2.4.2 The MOP Solution . 78
2.5 Interprocedural Analysis .. 82
2.5.1 Structural Operational Semantics . 85
2.5.2 Intraprocedural versus Interprocedural Analysis . 88
2.5.3 Making Context Explicit . 90
2.5.4 Call Strings as Context 95
2.5.5 Assumption Sets as Context . 99
2.5.6 Flow-Sensitivity versus Flow-Insensitivity 101
2.6 Shape Analysis •••••••••••••• o 104
2.6.1 Structural Operational Semantics . 105
2.6.2 Shape Graphs . 109
2.6.3 The Analysis 115
Concluding Remarks 128
Mini Projects 132
Exercises .. 135
3 Constraint Based Analysis 141
3.1 Abstract 0-CFA Analysis 141
3.1.1 The Analysis ... 143
3.1.2 Well-definedness of the Analysis 150
3.2 Theoretical Properties . . . . . . . . . . 153
3.2.1 Structural Operational Semantics . 153
3.2.2 Semantic Correctness 158
3.2.3 Existence of Solutions 162
Contents XIII
3.2.4 Coinduction versus Induction 165
3.3 Syntax Directed 0-CFA Analysis .. 168
3.3.1 Syntax Directed Specification 169
3.3.2 Preservation of Solutions 171
3.4 Constraint Based 0-CFA Analysis . 173
3.4.1 Preservation of Solutions 175
3.4.2 Solving the Constraints 176
3.5 Adding Data Flow Analysis . . 182
3.5.1 Abstract Values as Powersets 182
3.5.2 Abstract Values as Complete Lattices 185
3.6 Adding Context Information . . . 189
3.6.1 Uniform k-CFA Analysis. 191
3.6.2 The Cartesian Product Algorithm 196
Concluding Remarks 198
Mini Projects 202
Exercises .. 205
4 Abstract Interpretation 211
4.1 A Mundane Approach to Correctness. 211
4.1.1 Correctness Relations .. 214
4.1.2 Representation Functions 216
4.1.3 A Modest Generalisation 219
4.2 Approximation of Fixed Points 221
4.2.1 Widening Operators 224
4.2.2 N arrowing Opera tors . 230
4.3 Galois Connections . . . . . . 233
4.3.1 Properties of Galois Connections 239
4.3.2 Galois Insertions ......... 242
4.4 Systematic Design of Galois Connections . 246
4.4.1 Component-wise Combinations 249
4.4.2 Other Combinations 253
4.5 Induced Operations . . . . . 258
4.5.1 Inducing along the Abstraction Function . 258
XIV
4.5.2 Application to Data Flow Analysis . . . . .
4.5.3 Inducing along the Concretisation Function
Concluding Remarks
Mini Projects
Exercises ..
5 Type and Effect Systems
5.1 Control Flow Analysis ....... .
5.1.1 The Underlying Type System
5.1.2 The Analysis ...
5.2 Theoretical Properties ..
5.2.1 Natural Semantics
5.2.2 Semantic Correctness
5.2.3 Existence of Solutions 297
5.3 Inference Algorithms . . . . . 300
5.3.1 An Algorithm for the Underlying Type System 300
5.3.2 An Algorithm for Control Flow Analysis . 306
5.3.3 Syntactic Soundness and Completeness 312
5.3.4 Existence of Solutions 317
5.4 Effects . . . . . . . . . . . . 319
5.4.1 Side Effect Analysis
5.4.2 Exception Analysis .
5.4.3 Region Inference ..
5.5 Behaviours . . . . . . . . .
5.5.1 Communication Analysis
Concluding Remarks
Mini Projects
Exercises ..
6 Algorithms
6.1 Worklist Algorithms . . . . . . . . . . . . . .
6.1.1 The Structure of Worklist Algorithms
6.1.2 Iterating in LIFO and FIFO.
6.2 Iterating in Reverse Postorder ....
6.2.1 The Round Robin Algorithm .
6.3 Iterating Through Strong Components
Concluding Remarks
Mini Projects
Exercises ..
Partially Ordered Sets
A.1 Basic Definitions . . •••• o •••
A.2 Construction of Complete Lattices
A.3 Chains ....
A.4 Fixed Points
Concluding Remarks
Induction and Coinduction
B.1 Proof by Induction . . . .
B.2 Introducing Coinduction .
B.3 Proof by Coinduction
Concluding Remarks . . . .
Graphs and Regular Expressions
C.1 Graphs and Forests .
C.2 Reverse Postorder .
C.3 Regular Expressions
Concluding Remarks
Index of N otation
Index
Bibliography