Principles of Program AnalysisSpringer Science & Business Media, 10.12.2004 - 452 Seiten 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. |
Inhalt
Introduction | 1 |
12 Setting the Scene | 3 |
13 Data Flow Analysis | 5 |
132 The Constraint Based Approach | 8 |
14 Constraint Based Analysis | 10 |
15 Abstract Interpretation | 13 |
16 Type and Effect Systems | 17 |
161 Annotated Type Systems | 18 |
411 Correctness Relations | 214 |
412 Representation Functions | 216 |
413 A Modest Generalisation | 219 |
42 Approximation of Fixed Points | 221 |
421 Widening Operators | 224 |
422 Narrowing Operators | 230 |
43 Galois Connections | 233 |
431 Properties of Galois Connections | 239 |
162 Effect Systems | 22 |
17 Algorithms | 25 |
18 Transformations | 27 |
Concluding Remarks | 29 |
Exercises | 31 |
Data Flow Analysis | 35 |
211 Available Expressions Analysis | 39 |
212 Reaching Definitions Analysis | 43 |
213 Very Busy Expressions Analysis | 46 |
214 Live Variables Analysis | 49 |
215 Derived Data Flow Information | 52 |
22 Theoretical Properties | 54 |
222 Correctness of Live Variables Analysis | 60 |
23 Monotone Frameworks | 65 |
231 Basic Definitions | 67 |
232 The Examples Revisited | 70 |
233 A Nondistributive Example | 72 |
24 Equation Solving | 74 |
242 The MOP Solution | 78 |
25 Interprocedural Analysis | 82 |
251 Structural Operational Semantics | 85 |
252 Intraprocedural versus Interprocedural Analysis | 88 |
253 Making Context Explicit | 90 |
254 Call Strings as Context | 95 |
255 Assumption Sets as Context | 99 |
256 FlowSensitivity versus FlowInsensitivity | 101 |
26 Shape Analysis | 104 |
261 Structural Operational Semantics | 105 |
262 Shape Graphs | 109 |
263 The Analysis | 115 |
Concluding Remarks | 128 |
Mini Projects | 132 |
Exercises | 135 |
Constraint Based Analysis | 141 |
311 The Analysis | 143 |
312 Welldefinedness of the Analysis | 150 |
32 Theoretical Properties | 153 |
322 Semantic Correctness | 158 |
323 Existence of Solutions | 162 |
324 Coinduction versus Induction | 165 |
33 Syntax Directed 0CFA Analysis | 168 |
331 Syntax Directed Specification | 169 |
332 Preservation of Solutions | 171 |
34 Constraint Based 0CFA Analysis | 173 |
341 Preservation of Solutions | 175 |
342 Solving the Constraints | 176 |
35 Adding Data Flow Analysis | 182 |
352 Abstract Values as Complete Lattices | 185 |
36 Adding Context Information | 189 |
361 Uniform kCFA Analysis | 191 |
362 The Cartesian Product Algorithm | 196 |
Concluding Remarks | 198 |
Mini Projects | 202 |
Exercises | 205 |
Abstract Interpretation | 211 |
432 Galois Insertions | 242 |
44 Systematic Design of Galois Connections | 246 |
441 Componentwise Combinations | 249 |
442 Other Combinations | 253 |
45 Induced Operations | 258 |
452 Application to Data Flow Analysis | 262 |
453 Inducing along the Concretisation Function | 267 |
Concluding Remarks | 270 |
Mini Projects | 274 |
Exercises | 276 |
Type and Effect Systems | 283 |
511 The Underlying Type System | 284 |
512 The Analysis | 287 |
52 Theoretical Properties | 291 |
521 Natural Semantics | 292 |
522 Semantic Correctness | 294 |
523 Existence of Solutions | 297 |
53 Inference Algorithms | 300 |
532 An Algorithm for Control Flow Analysis | 306 |
533 Syntactic Soundness and Completeness | 312 |
534 Existence of Solutions | 317 |
54 Effects | 319 |
542 Exception Analysis | 325 |
543 Region Inference | 330 |
55 Behaviours | 339 |
Concluding Remarks | 349 |
Mini Projects | 353 |
Exercises | 359 |
Algorithms | 365 |
611 The Structure of Worklist Algorithms | 368 |
612 Iterating in LIFO and FIFO | 372 |
62 Iterating in Reverse Postorder | 374 |
621 The Round Robin Algorithm | 378 |
63 Iterating Through Strong Components | 381 |
Concluding Remarks | 384 |
Mini Projects | 387 |
Exercises | 389 |
Partially Ordered Sets | 393 |
A2 Construction of Complete Lattices | 397 |
A3 Chains | 398 |
A4 Fixed Points | 402 |
Concluding Remarks | 404 |
Induction and Coinduction | 405 |
B2 Introducing Coinduction | 407 |
B3 Proof by Coinduction | 411 |
Concluding Remarks | 415 |
Graphs and Regular Expressions | 417 |
C2 Reverse Postorder | 421 |
C3 Regular Expressions | 426 |
Concluding Remarks | 427 |
| 429 | |
| 433 | |
| 439 | |
Andere Ausgaben - Alle anzeigen
Principles of Program Analysis Flemming Nielson,Hanne R. Nielson,Chris Hankin Eingeschränkte Leseprobe - 2015 |
Principles of Program Analysis Flemming Nielson,Hanne R. Nielson,Chris Hankin Keine Leseprobe verfügbar - 2010 |
Häufige Begriffe und Wortgruppen
Abstract Interpretation abstract location algorithm annotated types annotation variables Ascending Chain Condition assignment axioms cdr cdr Chapter clause coinduction complete lattice computation consider constraint system construct context Control Flow Analysis Data Flow Analysis defined e₁ edges element environment equations evaluate Example Exercise expression final(S finite flow(S follows fun ƒ function abstraction Galois connection Galois insertion heap hence induction inference init(S iteration l₁ labels language least fixed point least solution Lemma Mini Project Monotone Framework monotone function node Operational Semantics P(Sign partially ordered set path program analysis proof properties RD entry RD exit Reaching Definitions recursive result reverse postorder rule S₁ Section semantic correctness sequence shape graphs specified strong components structure Subsection subtyping syntax directed transfer functions Type and Effect type system type variables upper bound v₁ WCFA widening operator
Beliebte Passagen
Seite 442 - M. Emami, R. Ghiya, and LJ Hendren. Context-sensitive interprocedural points-to analysis in the presence of function pointers.
Seite 439 - Ole Agesen, Jens Palsberg, and Michael I. Schwartzbach. Type Inference of SELF: Analysis of Objects with Dynamic and Multiple Inheritance.
Seite 445 - Press, jun 200 1 . [7] S. Jagannathan and S. Weeks. A unified treatment of flow analysis in higher-order languages. In 22nd ACM Symposium on Principles of Programming Languages, pages 392-401, jan 1995.
Seite 439 - J. Foster, and Z. Su. A toolkit for constructing type- and constraint-based program analyses. In Proc.
Seite 449 - G. Ramalingam, J. Field, and F. Tip. Aggregate structure identification and its application to program analysis. In Symposium on Principles of Programming Languages, pages 119-132, Jan.
Seite 440 - Programming, 7(3):321347, 1997. 3. T. Amtoft, F. Nielson, HR Nielson, and J. Ammann. Polymorphic subtyping for effect analysis: The dynamic semantics. In Analysis and Verification of MultipleAgent Languages, volume 1192 of Lecture Notes in Computer Science, pages 172206.
Seite 447 - F. Nielson and HR Nielson. From CML to process algebras. In Proc.