This is an old revision of the document!
Lecture 21: More on interprocedural analysis
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
Reference:
Non-regular properties using visibly pushdown languages
Reference: * 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
Computations on heap can give different result depending on whether in precondition certain references refer to same objects or not. Procedure specifications are therefore important for such programs and automatically inferring them is challenging.
Reference:
- Sophisticated Pointer and Escape Analysis with Procedure Summaries (Alex Salcianu PhD thesis)
General 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.