Lecture 21: More on interprocedural analysis
The idea is to avoid having to specify contracts for all procedures
- abstract interpretation for general case (precision depends on the example)
- decidability results: no approximation, but works for restricted classes of programs (which can be obtained by abstract interpretation)
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
- intersection of regular and context-free language is context-free
Reference:
Non-regular properties using visibly pushdown languages
Reference: * Visibly pushdown languages
Two basic methods for inferring contracts using Abstract Interpretation
- 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.