Principles of Program Analysis

Program analysis utilizes static techniques for computing reliable information about the dynamic behavior of programs. Applications include compilers (for code improvement), software validation (for detecting errors) and transformations between data representation (for solving problems such as Y2K). This book is unique in providing an overview of the four major approaches to pr...

(展开全部)

Program analysis utilizes static techniques for computing reliable information about the dynamic behavior of programs. Applications include compilers (for code improvement), software validation (for detecting errors) and transformations between data representation (for solving problems such as Y2K). This book is unique in providing an overview of the four major approaches to program analysis: data flow analysis, constraint-based analysis, abstract interpretation, and type and effect systems. The presentation illustrates the extensive similarities between the approaches, helping readers to choose the best one to utilize.

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
· · · · · · (更多)

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
· · · · · · (收起)