Principles of Program Analysis

by Nielson, Flemming; Nielson, Hanne Riis; Hankin, Chris

• ISBN13: 9783540654100
• ISBN10: 3540654100
• Format: Hardcover
• Copyright: 2004-12-17
• Publisher: SPRINGER-VERLAG

Summary

Program analysis concerns static techniques for computing reliable approximate information about the dynamic behaviour of programs. Applications include compilers (for code improvement), software validation (for detecting errors in algorithms or breaches of security) and transformations between data representation (for solving problems such as the Y2K problem). This book is unique in giving 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 demonstrates the extensive similarities between the approaches; this will aid the reader in choosing the right approach and in enhancing it with insights from the other approaches. The book covers basic semantic properties as well as more advanced algorithmic techniques. The book is aimed at M.Sc. and Ph.D. students but will be valuable also for experienced researchers and professionals.

Table of Contents

Introduction	1	(32)
The Nature of Program Analysis	1	(2)
Setting the Scene	3	(2)
Data Flow Analysis	5	(5)
The Equational Approach	5	(3)
The Constraint Based Approach	8	(2)
Constraint Based Analysis	10	(3)
Abstract Interpretation	13	(4)
Type and Effect Systems	17	(8)
Annotated Type Systems	18	(4)
Effect Systems	22	(3)
Algorithms	25	(1)
Transformations	26	(7)
Concluding Remarks	29	(1)
Mini Projects	29	(2)
Exercises	31	(2)
Data Flow Analysis	33	(106)
Intraprocedural Analysis	33	(19)
Available Expressions Analysis	37	(4)
Reaching Definitions Analysis	41	(3)
Very Busy Expressions Analysis	44	(3)
Live Variables Analysis	47	(3)
Derived Data Flow Information	50	(2)
Theoretical Properties	52	(11)
Structural Operational Semantics	52	(5)
Correctness of Live Variables Analysis	57	(6)
Monotone Frameworks	63	(9)
Basic Definitions	65	(3)
The Examples Revisited	68	(2)
A Non-distributive Example	70	(2)
Equation Solving	72	(8)
The MFP Solution	72	(4)
The MOP Solution	76	(4)
Interprocedural Analysis	80	(22)
Structural Operational Semantics	83	(3)
Intraprocedural versus Interprocedural Analysis	86	(2)
Making Context Explicit	88	(5)
Call Strings as Context	93	(4)
Assumption Sets as Context	97	(2)
Flow-Sensitivity versus Flow-Insensitivity	99	(3)
Shape Analysis	102	(37)
Structural Operational Semantics	103	(4)
Shape Graphs	107	(6)
The Analysis	113	(13)
Concluding Remarks	126	(4)
Mini Projects	130	(3)
Exercises	133	(6)
Constraint Based Analysis	139	(70)
Abstract O-CFA Analysis	139	(12)
The Analysis	141	(7)
Well-definedness of the Analysis	148	(3)
Theoretical Properties	151	(15)
Structural Operational Semantics	151	(5)
Semantic Correctness	156	(4)
Existence of Solutions	160	(3)
Coinduction versus Induction	163	(3)
Syntax Directed O-CFA Analysis	166	(5)
Syntax Directed Specification	167	(2)
Preservation of Solutions	169	(2)
Constraint Based O-CFA Analysis	171	(9)
Preservation of Solutions	173	(1)
Solving the Constraits	174	(6)
Adding Data Flow Analysis	180	(7)
Abstract Values as Powersets	180	(3)
Abstract Values as Complete Lattices	183	(4)
Adding Context Information	187	(22)
Uniform k-CFA Analysis	189	(5)
The Cartesian Product Algorithm	194	(2)
Concluding Remarks	196	(4)
Mini Projects	200	(3)
Exercises	203	(6)
Abstract Interpretation	209	(72)
A Mundane Approach to Correctness	209	(10)
Correctness Relations	212	(2)
Representation Functions	214	(3)
A Modest Generalisation	217	(2)
Approximation of Fixed Points	219	(12)
Widening Operators	222	(6)
Narrowing Operators	228	(3)
Galois Connections	231	(13)
Properties of Galois Connections	237	(3)
Galois Insertions	240	(4)
Systematic Design of Galois Connections	244	(12)
Component-wise Combinations	247	(4)
Other Combinations	251	(5)
Induced Operations	256	(25)
Inducing along the Abstraction Function	256	(4)
Application to Data Flow Analysis	260	(5)
Inducing along the Concretisation Function	265	(3)
Concluding Remarks	268	(4)
Mini Projects	272	(2)
Exercises	274	(7)
Type and Effect Systems	281	(82)
Control Flow Analysis	281	(8)
The Underlying Type System	282	(3)
The Analysis	285	(4)
Theoretical Properties	289	(9)
Natural Semantics	290	(2)
Semantic Correctness	292	(3)
Existence of Solutions	295	(3)
Inference Algorithms	298	(19)
An Algorithm for the Underlying Type System	298	(6)
An Algorithm for Control Flow Analysis	304	(6)
Syntactic Soundness and Completeness	310	(5)
Existence of Solutions	315	(2)
Effects	317	(20)
Side Effect Analysis	317	(6)
Exception Analysis	323	(5)
Region Inference	328	(9)
Behaviours	337	(26)
Communication Analysis	337	(10)
Concluding Remarks	347	(4)
Mini Projects	351	(6)
Exercises	357	(6)
Algorithms	363	(28)
Worklist Algorithms	363	(9)
The Structure of Worklist Algorithms	366	(4)
Iterating in LIFO and FIFO	370	(2)
Interating in Reverse Postorder	372	(7)
The Round Robin Algorithm	376	(3)
Iterating Through Strong Components	379	(12)
Concluding Remarks	382	(3)
Mini Projects	385	(2)
Exercises	387	(4)
A Partially Ordered Sets	391	(12)
Basic Definitions	391	(4)
Construction of Complete Lattices	395	(1)
Chains	396	(4)
Fixed Points	400	(3)
Concluding Remarks	402	(1)
B Induction and Coinduction	403	(12)
Proof by Induction	403	(2)
Introducing Coinduction	405	(4)
Proof by Coinduction	409	(6)
Concluding Remarks	413	(2)
C Graphs and Regular Expressions	415	(12)
Graphs and Forests	415	(4)
Reverse Postorder	419	(5)
Regular Expressions	424	(3)
Concluding Remarks	425	(2)
Index of Notation	427	(4)
Index	431	(6)
Bibliography	437