This is an old revision of the document!
Lecture 20: Interprocedural analysis
intraprocedural analysis = analysis for language without procedures
interprocedural analysis = analysis for language with procedures
Given intraprocedural analysis, how do we create interprocedural analysis?
Assumptions
- No concurrency
- Only global variables
- No parameters
The last two assumptions are made for simplicity, since parameter passing can be simulated using global variables and assignments. For example, a function called p with a parameter x, p(x), can be represented as a function without parameters, p'(), by introducing a global variable x.
Example
proc main() { p1(); p2(); } proc p1() { open(); readContent(); } proc p2() { startLog(); readContent(); stopLog(); close(); } proc readContent() { while (...) { read(); print(); } }
Desired properties
These are stated as regular expressions so that it is easier to check whether the program satisfies these constraints.
- must follow protocol: (open (read+write)* close)*
- must follow protocol: (startLog stopLog)*
Semantics for language with procedure calls
Big step
In this approach, we treat a procedure call as one step. This can be thought of like a step-over move in a debugger.
Let be the set of program states and be the set of vertices in the control flow graph. Then we can describe a point in the program as:
where , p()r\{(x,y), (x',y') | x'=100 \wedge y'=y\}\mapsto(c_{0},s_{1}) \mapsto (c_{3}, s_{2})(s_{1},s_{2}) \in r(c_{0},s_{1}) \rightarrow (c_{3},s_{2})(s, c, t)s \in S, c \in V, t \in V^{*}V^{*}\hookrightarrow(s,c,t_{1}) \hookrightarrow (s_{1}, c_{0}, c_{2} : t_{1}) \hookrightarrow … \hookrightarrow (s_{2}, c_{3}, c_{2} t_{1}) \hookrightarrow (s_{2}, c_{2}, t_{1})c_{2}c_{2}(s, l, c, t)l \in LLlsp\#(a,c) = a_{1}Aa,a_{1} \in Asp\#(a,p()) = TPL(P)AL(A)L(P) \subseteq L(A)\Sigma\GammaQL(CFG) \subseteq L(A)X \subseteq YX \cap \overline{Y} = \emptyset L(P) \subseteq L(A)L(P) \cap \overline{L(A)} = \emptysetL(P) \cap L(\overline{A}) = \emptysetQ_{1}PQ_{2}L(P) \cap L(\overline{A})P_{1}Q_{1} \times Q_{2}CFG_{1}P_{1}L(P_{1}) = \emptysetL(CFG_{1}) = \emptysetCFG_{1}L(CFG_{1})L(P) \nsubseteq L(A)ASSpre^{*}(S)pre^{*}(S)\mathcal{P} = (P, \Gamma, \Delta)P\Gamma\Delta \subseteq (P \times \Gamma) \times (P \times \Gamma^{*})1) \in \Delta(q, \gamma) \hookrightarrow (q', w)\mathcal{P} = (P, \Gamma, \Delta)P=\{p^{1},…,p^{m}\}\mathcal{P}\mathcal{A} = (\Gamma, Q, \delta, I, F)Q\delta \subseteq Q \times \Gamma \times QI \subseteq QF \subseteq Q\longrightarrow \subseteq Q \times \Gamma^{*} \times Q(q, \gamma, q')q \stackrel{\gamma}{\longrightarrow} q'q \stackrel{\varepsilon}{\longrightarrow} q'q \in Qq \stackrel{\w}{\longrightarrow} q$ and $q
\stackrel{\gamma}{\longrightarrow} q'q \stackrel{w\gamma}{\longrightarrow} q'\mathcal{A}\langle p^{i},w \rangles^{i} \stackrel{w}{\longrightarrow} qq \in F\mathcal{A}Conf(\mathcal{A})C\mathcal{P}\mathcal{A}\mathcal{A}_{pre*}pre^{*}(C)Cpre^{*}(C)$ includes the starting state configurations (in other words, whether any of the error states are reachable from the start state).
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.
Continued in SAV07 Lecture 21.