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 L
L
l
sp\#(a,c) = a_{1}
A
a,a_{1} \in A
sp\#(a,p()) = T
P
L(P)
A
L(A)
L(P) \subseteq L(A)
\Sigma
\Gamma
Q
L(CFG) \subseteq L(A)
X \subseteq Y
X \cap \overline{Y} = \emptyset
L(P) \subseteq L(A)
L(P) \cap \overline{L(A)} = \emptyset
L(P) \cap L(\overline{A}) = \emptyset
Q_{1}
P
Q_{2}
L(P) \cap L(\overline{A})
P_{1}
Q_{1} \times Q_{2}
CFG_{1}
P_{1}
L(P_{1}) = \emptyset
L(CFG_{1}) = \emptyset
CFG_{1}
L(CFG_{1})
L(P) \nsubseteq L(A)
A
S
S
pre^{*}(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 Q
I \subseteq Q
F \subseteq Q
\longrightarrow \subseteq Q \times \Gamma^{*} \times Q
(q, \gamma, q')
q \stackrel{\gamma}{\longrightarrow} q'
q \stackrel{\varepsilon}{\longrightarrow} q'
q \in Q
q \stackrel{\w}{\longrightarrow} q
$ and $q
\stackrel{\gamma}{\longrightarrow} q'q \stackrel{w\gamma}{\longrightarrow} q'
\mathcal{A}
\langle p^{i},w \rangle
s^{i} \stackrel{w}{\longrightarrow} q
q \in F
\mathcal{A}
Conf(\mathcal{A})
C
\mathcal{P}
\mathcal{A}
\mathcal{A}_{pre*}
pre^{*}(C)
C
pre^{*}(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.