This is an old revision of the document!
Lecture 21: More on interprocedural analysis
(Continuation of SAV07 Lecture 20.)
Analysis of regular properties of finite-state programs with stack (push down systems)
- Product construction based on push down automata and context-free grammar equivalence
Non-regular properties using visibly pushdown languages
Two basic methods for inferring contracts
- approximate the set of (stack, state) pairs - based on small step semantics
- call-string approach
- representing stack as e.g. linked list (see this paper)
- approximate the relation between initial and final state of procedure - based on big step semantics
- add procedure entry variables, then approximate (consider e.g. linear constraints)
- functional approach: map entry data flow facts to exit data flow facts
Analysis based on graph reachability
- distributive functions and supergraph
- checking context-free graph reachability
Summaries for pointer analysis
References
- M. Sharir, and A. Pnueli. Two Approaches to Inter-Procedural Data-Flow Analysis. In Jones and Muchnik, editors, Program Flow Analysis: Theory and Applications. Prentice-Hall, 1981.
- F. Nielson, H. R. Nielson, C. Hankin: Principles of program analysis, 2005. Chapter 2.5.