ROPAS

Research On Program Analysis System

National Creative Research Initiative Center Korea Advanced Institute of Science and Technology

ROPAS MEMO 2000-4 February 3, 2000

Modularization of 0-CFA Makes It Polyvariant

Oukseh Lee and Kwangkeun Yi

                       {cookcu; kwang}@ropas.kaist.ac.kr

Abstract

This article shows that (1) deriving a modular version (in the framework of incremental analysis) from a whole-program CFA makes the resulting analysis polyvariant at modulelevel, (2) if the original whole-program CFA was less accurate than or incomparable to module-level polyvariant analyses, then the correctness of its modular version may not be proven in general with respect to the original CFA, and (3) a convenient stepstone to prove the correctness of modular analyses is a whole-program CFA that is polyvariant at modulelevel. Our result can be seen as a clarification of possible problems in designing a correct modular analysis from a whole-program analysis, and as a hint of using the module-variant whole-program analysis in proving the correctness of modular static analyses.

1 Introduction

Modular analyses are necessary for analyzing large, realistic programs. A whole-program analysis needs the entire program text as its input, and it has to solve a large set of equations at once. If some parts of the program are modified, it has to re-analyze the entire program.

Usually, a program analysis is initially designed as a whole-program analysis, and then, only after its cost-effectiveness is assured by extensive testings, its modular version is designed.

In deriving a modular version from a whole analysis, however, it is not obvious to check whether the modular version is sound with respect to the original whole version. We tried to derive a modular version of the standard 0-CFA [Shi88] and observed that modularization of 0-CFA makes it unsound with respect to the original 0-CFA. That is, our derived modular analyses give us more accurate result than 0-CFA does.

Example 1 Consider the following two modules:

                      \begin{matrix}f = λx.x \\ g = f λy.y \end{matrix} and h = g (f λz.z).

0-CFA concludes that h can be evaluated to λz.z and λy.y, because 0-CFA estimates that h can be evaluated to x and that x can be evaluated to both functions from “f λy.y” and “f λz.z”. On the other hand, separate analyses of the modules (from left to right) give more accurate result. From the result of the left module, it is natural to bring only information that f can be evaluated to λx.x and g can be λy.y. Then the analysis result of the second module determines that h can be evaluated to only λz.z.

We have found that we can prove the safety of the modular version with respect to a whole-program CFA that is polyvariant at module-level. We call this analysis “module-variant CFA.”

0This work is supported by Creative Research Initiatives of the Korean Ministry of Science and Technology.

After we describe the model for our modular analysis in Section 2, we describe the language and its 0-CFA in Section 3. We then present, in Section 4, a naive modular version of 0-CFA, show that it is not sound with respect to the original 0-CFA, introduce a module-variant CFA, and prove the correctness of the naive modular version by using this module-variant CFA. In Section 5, we consider a more sophisticated modular analysis and proves its correctness also by using the module-variant CFA. We discuss the case when we modularize already polyvariant CFAs in Section 6, and conclude in Section 7.

2 Incremental Model for Modular Analysis

We assume that a modular analysis is to be integrated with an incremental compilation environment [AM94]. A module consists of declarations (implementation) and a signature (interface) which lists exported variables that are visible from the outside of the module. We assume that there exists partially ordered dependency between modules and we analyze modules in sequence by its topological order, as in the incremental compilation system. No circular dependency between modules is assumed.

2.1 Incremental Model

Figure 1 illustrates our incremental model of modular analysis. For a given module M = (decl, sig), we first derive equations D(M):

D : Module → Equations.

Then we solve S(D(M)) the derived equations:

S : Equations → Equations.

Let the result be Δ. If the module uses some variables of other modules, we obtain Δ by solving the set of equations of the current module and those exported from the referred modules. Among this Δ, we export some equations E(Δ, sig) that can be needed to analyze subsequent modules:

E : Equations × Signature → Equations.

For modules M_{1}, M_{2}, ⋯, and M_{n}, the intermediate solution Δ_{i} and exported set δ_{i} for module M_{i} (in Figure 1) are thus defined as

Δ_{i} = S (D(M_{i}) ∪ (∪_{M_{j}⊏M_{i}} δ_{j})) and
δ_{i} = E(Δ_{i}, sig_{i})

where relation M_{j} ⊏ M_{i} denotes that module M_{i} uses variables of module M_{j}, and sig_{i} is the signature of M_{i}. The final analysis result Sol(M_{1}, ⋯, M_{n}) for the whole-program is:

Sol(M_{1}, ⋯, M_{n}) = Δ_{1} ∪ Δ_{2} ∪ ⋯ ∪ Δ_{n}.

3 0-CFA

The whole-program 0-CFA [Shi88], whose modular versions we are designing, is shown in Figure 2. An input program is a sequence of declarations, and an expression is either a function, an application or a variable. We describe 0-CFA by the notation similar to that of Heintze

M^{1}^{1}  δ_{1}^{3}  Δ_{3}^{3}  ^{2}^{2} Δ_{1}  Δ_{2} δ_{2} δ_{3}^{1}  ^{2}^{3}  M M decl sig  decl sig decl sig  ^{derive} ^{solve}^{D}  ^{S} ^{export}^{E}  ^{export}^{E}^{solve}^{S}^{D}^{derive}^{solve}^{S} ^{export}^{E}^{derive}^{D}

Figure 1: Incremental Model for Modular Analysis. The case is that M_{2} uses M_{1}’s functions and M_{3} uses functions of M_{1} and M_{2}.

and McAllester [HM97]. Edge “n → m” means that the analysis result of n includes that of m. Applying the rules of Figure 2, we collect edges until no more edge is added. “n → λ(x, l)” in the collected edges denotes that the expression of node n can be evaluated to the function value λx.e where e’s label is l.

4 N: Naive Modular 0-CFA

In this section, we present a naive incremental version of 0-CFA. Rules in the deriving phase are those of 0-CFA that collect call-graph edges by examining only the program text. Rules in the solving phase are those of 0-CFA that estimate the information flow in function calls. In the exporting phase, we export every edge reachable from the names in the signature.

Interestingly enough, this obvious modular analysis N is not sound with respect to 0-CFA. This situation is not because N is an incorrect analysis but because even such a trivial modularization makes 0-CFA polyvariant. Therefore we need to find a new reference other than the original 0-CFA for proving the correctness of N.

We have found that a polyvariant version of 0-CFA at module-level, which is a straightforward extension to 0-CFA, can be conveniently used as a reference for the correctness of our modular 0-CFA. It is “convenient” because the proofs are between two static analyses which have a smaller semantic gap than that between our modular 0-CFA and the program’s actual control flow.

Label  l
Variable v ::= x | f
Expr  e ::= v | λx.e^{l} | e^{l} e^{l}
Decl  d ::= f = e^{l}
Program ℘ ::= d^{∗}
Node  n ::= v | l | λ(x, l)
Edge  c ::= n → n

{f = e^{l} ∈ ℘ \atop f → l} (Dec_{0}) {(e_{1}^{l_{1}} e_{2}^{l_{2}})^{l} ∈ ℘ l_{1} → λ(x, l_{0}) \atop l → l_{0} x → l_{2}} (App_{0})

{v^{l} ∈ ℘ \atop l → v} (Var_{0})  {n → m m → λ(x, l) \atop n → λ(x, l)} (Tr_{0})

{(λx.e^{l_{0}})^{l} ∈ ℘ \atop l → λ(x, l_{0})} (Lam_{0})

Figure 2: The language and its 0-CFA.

Let us examine the exact definition of N, why it is unsound with respect to the whole 0-CFA, and how the module-variant whole-program CFA helps in its soundness proof.

4.1 Definition

Figure 3 has the definition of N.

The deriving and solving phases are directly from the rules of 0-CFA. We divide the (App_{0}) rule into two: one (Appd) that needs the source text and the other (App) that does not. Rule (Appd) is applied in the deriving phase and rule (App) is applied in the solving phase. In order to make this separation clear, we have to add edge “l → @(l_{1}, l_{2}),” which encodes that there is an application labeled by l whose function part is labeled by l_{1} and whose argument is labeled by l_{2}.

This separation is necessary because modular analysis is not supposed to see the entire source of the program. Edges from analyzing module A that will be exported have to be encoded such that the analyses of subsequent modules work without module A’s text.

We devise the exporting phase conservatively in order to make sure that all the edges that can be needed by subsequent modules are exported. We simply export the edges that are reachable from the names in the signature. All declaration variables in the signature are in the Reachable set because they are directly referred to by subsequent modules (Sig). If subsequent modules may reach n, then they may reach n’s sub-expressions: (SubLam) and (SubApp). If subsequent modules may reach n, and n can be evaluated to m (n → m), then n → m is exported (n → m ∈ δ) to subsequent modules, and we estimate that m is reachable (Out). We repeatedly apply these rules until no more edge is exportable.

4.2 Proving Correctness by Using Module-Variant CFA

N is unsound with respect to 0-CFA. If a module has a dead code, the result of N does not

Signature  sig ::= {f_{1}, ⋯, f_{n}}
Declaration decl ::= ℘
Module  M ::= (decl, sig)
Node  n ::= v | l | λ(x, l) | @(l, l) | ⊤
Edge  c ::= n → n

D derives edges from module M :

{f = e^{l} ∈ M \atop f → l} (Dec)  {v^{l} ∈ M \atop l → v} (Var)

{(e_{1}^{l_{1}} e_{2}^{l_{2}})^{l} ∈ M \atop l → @(l_{1}, l_{2})} (Appd)  {(λx.e^{l_{0}})^{l} ∈ M \atop l → λ(x, l_{0})} (Lam)

S solves the edges :

{l → @(l_{1}, l_{2}) l_{1} → λ(x, l_{0}) \atop l → l_{0} x → l_{2}} (App)  {n → m m → λ(x, l) \atop n → λ(x, l)} (Tr)

E exports edges δ from Δ with respect to the signature sig :

f ∈ sig f ∈ Reachable (Sig)  @(l_{1}, l_{2}) ∈ Reachable l_{1} ∈ Reachable l_{2} ∈ Reachable (SubApp)

λ(x, l) ∈ Reachable l ∈ Reachable (SubLam)  n ∈ Reachable n → m ∈ Δ m ∈ Reachable n → m ∈ δ (Out)

Figure 3: N – a naive incremental version of 0-CFA.

include that of 0-CFA. The following example is an evidence. When we present examples, as nodes, we use expressions instead of labels if it is not ambiguous.

Example 2 Consider the following two modules:

                    M_{1} = ( \begin{matrix}f = λx.x \\ g = (f λy.y) λz.z \end{matrix} , \{f\}) and

M_{2} = ( h = f λw.w , {h}) .

If we analyze the whole program by 0-CFA, the result includes “w → λz.z” because (f λy.y) → x → λw.w. However, the exporting phase of N does not export (f λy.y) → x because (f λy.y) is not reachable from f which is in the signature. Thus the result of analyzing M_{2} by N does not include w → λz.z.

Because N is more accurate than the whole 0-CFA, we cannot prove its safety with respect to 0-CFA. We have to find a new reference to prove its correctness. The correctness relation between CFAs unexpectedly becomes

Semantics ⊆ 0-CFA  (correctness of 0-CFA)
N ⊆ 0-CFA  (N is not correct with respect to 0-CFA)

Node n ::= x_{M} | l_{M} | f | λ(x, e^{l})
Edge c ::= M ⊢ e^{l} | n → n

{f = e^{l} ∈ M \atop M ⊢ e^{l} f → l_{M}} (Dec_{M})  \begin{matrix}M ⊢ (e_{1}^{l_{1}} e_{2}^{l_{2}})^{l} \\ M ⊢ e_{1}^{l_{1}} & M ⊢ e_{2}^{l_{2}} \end{matrix} (Appd_{M})

{M ⊢ x^{l} \atop l_{M} → x_{M}} (Bvar_{M})  {M ⊢ (e_{1}^{l_{1}} e_{2}^{l_{2}})^{l} l_{1}_{M} → λ(x, e^{l_{0}}) \atop M ⊢ e^{l_{0}} x_{M} → l_{2}_{M} l_{M} → l_{0}_{M}} (App_{M})

{M ⊢ (λx.e^{l_{0}})^{l} \atop l_{M} → λ(x, e^{l_{0}})} (Lam_{M})  {n → m m → λ(x, e^{l}) \atop n → λ(x, e^{l})} (Tr_{M})

{M ⊢ f^{l} \atop l_{M} → f} (Dvar_{M})

Figure 4: Module-Variant CFA.

where A ⊆ B means that the result of B includes that of A. The goal is to establish

Semantics ⊆ N.

We want to find an analysis ⋆ which is obviously safe with respect to the semantics (Semantics⊆ ⋆ ⊆ N) and which is also easy to prove that ⋆ ⊆ N.

Such an analysis ⋆ must be polyvariant in terms of modules. In Example 2, there are two applications whose function part is f: (f λy.y) in M_{1} and (f λw.w) in M_{2}. By rule (App_{0}) of 0-CFA, both applications can be evaluated to x; that is, (f λy.y)→x and (f λw.w)→x. The former x is bound to only λy.y while the latter is bound to both λy.y and λw.w. The x’s two occurrences in the two modules are distinguished during our modular analysis.

Thus, as such an analysis ⋆, we devise a polyvariant CFA at module-level. We call it module-variant CFA. The module-variant CFA is similar to the 1-CFA [Shi88]. Note that 1-CFA distinguishes the same variable by the last caller’s label. Similarly, the module-variant CFA distinguishes the same variable (or label) by a module name whose analysis reaches it. For example, if λx.x is called by applications in modules M_{1} and M_{2} with arguments y and z, respectively, then we distinguish x by its callers’ module: M_{1} and M_{2}. That is, we bind y to x_{M_{1}} and z to x_{M_{2}}. Thus we can conclude that the application in M_{1} can be evaluated to only y and the application in M_{2} can be evaluated to only z.

This module-variant CFA is defined in Figure 4. Relation “M ⊢ e” means that expression e is necessary in evaluating expressions in module M. Program variable x (or label l) is indexed x_{M} (or l_{M}) with module name M, which indicates that the values of x (or l) are accessed or bound when expressions in module M are evaluated. The starting point is declarations (f = e^{l} ∈ M). A declared expression is necessary in evaluating expressions of its own module (M ⊢ e^{l}) and the values of the function name include those of the declared expression (f → l_{M}):

{f = e^{l} ∈ M \atop M ⊢ e^{l} f → l_{M}} (Dec_{M}).

If a function (respectively, a name) is necessary in evaluating expressions of module M, we just let its label link to the function value (respectively, the name):

{M ⊢ (λx.e^{l_{0}})^{l} \atop l_{M} → λ(x, e^{l_{0}})} (Lam_{M}), {M ⊢ x^{l} \atop l_{M} → x_{M}} (Bvar_{M}), and {M ⊢ f^{l} \atop l_{M} → f} (Dvar_{M}).

Note that a bound variable keeps the module index, hence having the effect of being modulevariant. If an application is needed in evaluating expressions of module M, then its subexpressions are also necessary:

\begin{matrix}M ⊢ (e_{1}^{l_{1}} e_{2}^{l_{2}})^{l} \\ M ⊢ e_{1}^{l_{1}} & M ⊢ e_{2}^{l_{2}} \end{matrix} (Appd_{M}).

If an application is necessary in evaluating expressions of module M (M ⊢ (e_{1}^{l_{1}} e_{2}^{l_{2}})^{l}) and, in addition, the function part of the application can be a value (l_{1}_{M} → λ(x, e^{l_{0}})), then (1) the body of the function value is needed to evaluate the expressions of module M (M ⊢ e^{l_{0}}), (2) the values of the application includes those of the function body (l_{M} → l_{0}_{M}), and (3) the function can have, as its argument, the values of the argument part of the application (x_{M} → l_{2}_{M}):

{M ⊢ (e_{1}^{l_{1}} e_{2}^{l_{2}})^{l} l_{1}_{M} → λ(x, e^{l_{0}}) \atop M ⊢ e^{l_{0}} x_{M} → l_{2}_{M} l_{M} → l_{0}_{M}} (App_{M}).

Note that the function body keeps the caller’s module index, having the effect of being modulevariant. Finally, we propagate function values; that is, if m can be a function value (m → λ(x, e^{l})) and the values of n includes those of m (n → m), then n can also be a function value (n → λ(x, e^{l})):

{n → m m → λ(x, e^{l}) \atop n → λ(x, e^{l})} (Tr_{M}).

Now, by using the correctness of the module-variant CFA, we can prove the correctness of N. Thanks to [NN97], the correctness of the module-variant CFA is easy to prove:

Theorem 1 (Correctness of Module-Variant CFA) The module-variant CFA is correct.

Proof. The module-variant CFA is correct by Theorem 4.1 in [NN97]. It is an instance of the infinitary control flow analysis.

The correctness of N is now proven by showing that N’s result includes that of the modulevariant CFA.

Corollary 1 (Correctness of N) Let Sol_{m}(℘) be the solution of a merged whole program ℘ of modules M_{1}, M_{2}, ⋯, and M_{n}, by the module-variant CFA. If n → λ(x, e^{l}) ∈ Sol_{m}(℘) then |n| → |λ(x, e^{l})| ∈ Sol_{N}(M_{1}, M_{2}, ⋯, M_{n}) which is the final analysis result by N. Note that |n| means the corresponding node of N to node n of the module-variant CFA.

Proof. This is a corollary of Theorem 2.

Theorem 2 For a merged whole program ℘ of modules, the following are true:

• If expression e is necessary to analyze expressions of a subsequent module M in the module-variant CFA, then naive modular analyses of modules before M assert that expression e is reachable.

• If e → e′ occurs in analyzing module M in the module-variant CFA, then

– |e| → |e′| occurs in naive modular analysis of module M.

– the naive modular analyses of modules before M assert that the two expressions are reachable.

Proof. The full proof is in Appendix A.

Thanks to the proofs of Theorem 1 and Corollary 1, we can avoid the burden of proof with respect to the standard semantics. We claim that the proofs of Theorem 1 and Corollary 1 are relatively simple because they are between two static analyses which have a smaller semantic gap than that between our modular 0-CFA and the program’s actual control flow.

The correctness relation between CFAs becomes:

Semantics ⊆ Module-variant CFA ⊆ N ⊆ 0-CFA.

5 S: More Sophisticated Modular 0-CFA

Given that module-variant CFA is a convenient vehicle to prove the correctness of the naive modular CFA, the next question is: is it also good for more sophisticated modular versions? In this section, we present another modular version S that exports less edges than N after an analysis of each module, and show that the module-variant CFA is still a reference for its correctness proof.

S has the same deriving and solving phases as N but has a sharper exporting phase (shown in Figure 5). The exporting is the process of finding edges that subsequent modules may depend on:

Definition 1 Expression e_{1} depends on expression e_{2} if and only if evaluating e_{1} evaluates e_{2}. Moreover, module m depends on expression e if and only if an expression of m depends on e.

(Note that N’s exporting phase using the notion of reachability is a naive upper approximation of this dependence relation.)

The starting point for our new exporting rules is the signature as usual. For a variable f in the signature, subsequent modules can directly refer to f; that is, subsequent modules may depend on f:

f ∈ sig ; f ∈ Depend (Sig).

If such f can be evaluated to a function value, then subsequent modules may depend on the function value (λ(x, l) ∈ Depend) and the solution edge (f → λ(x, l) ∈ δ) is exported:

f ∈ Depend f → λ(x, l) ∈ Δ
λ(x, l) ∈ Depend f → λ(x, l) ∈ δ

(FtoLam).

If subsequent modules may depend on a function value, then they may depend on the function’s body:

λ(x, l) ∈ Depend
l ∈ Depend

(SubLam).

If subsequent modules may depend on label l, then we export its edges excluding (Δ∩Π) those that are introduced during the solving phase of the current module. This exclusion is because such edges will be re-introduced anyway if they are needed to analyze the subsequent modules:

l ∈ Depend l → n ∈ Δ ∩ Π
n ∈ Depend l → n ∈ δ

(Excl)

f ∈ sig ; f ∈ Depend (Sig)  f ∈ Depend f → λ(x, l) ∈ Δ λ(x, l) ∈ Depend f → λ(x, l) ∈ δ (FtoLam)

@(l_{1}, l_{2}) ∈ Depend l_{1} ∈ Depend l_{2} ∈ Depend (SubApp)

l ∈ Depend l → n ∈ Δ ∩ Π
n ∈ Depend l → n ∈ δ

(Excl)

where Π = ⋃_{i=1}^{k} D(M_{i})
λ(x, l) ∈ Depend
l ∈ Depend

(SubLam)

Figure 5: The exporting phase of S for module M_{k}.

where Π is a set ∪_{i=1}^{k}D(M_{i}) of edges from the deriving phases of the previous modules including the current one M_{k}. If subsequent modules may depend on an application, then they may depend on its sub-expressions:

@(l_{1}, l_{2}) ∈ Depend
l_{1} ∈ Depend l_{2} ∈ Depend

(SubApp).

Compared with the exporting phase of N, S exports less edges. Rules (Sig), (SubApp) and (SubLam) are the same as in N, but rule (Out) of N becomes more selective in S by the two rules (Excl) and (FtoLam).

Example 3 Consider Example 1 and its edges:

( \begin{matrix}f = (λx.x^{2})^{1} \\ g = (f^{4} (λy.y^{6})^{5})^{3} \end{matrix} , \{f,g\}) and \begin{matrix}f → 1 → λ(x, 2) \\ g → 3 → 2 → x → 5 → λ(y, 6) \\ 3 → @(4, 5) \\ 6 → y. \end{matrix}

N exports all edges, while S exports f → λ(x, 2) and g → λ(y, 6) by (FtoLam), and 2 → x and 6 → y by (Excl).

S is still correct with respect to the module-variant CFA (Figure 4).

Corollary 2 (Correctness of S) For a merged whole program ℘ of modules M_{1}, M_{2}, ⋯, and M_{n}, if n → λ(x, e^{l}) ∈ Sol_{m}(℘), then |n| → |λ(x, e^{l})| ∈ Sol_{S}(M_{1}, M_{2}, ⋯, M_{n}) which is the final analysis result by S.

Proof. This is a corollary of Theorem 3 in Appendix B. Theorem 3 is a simple adaptation of Theorem 2 for the new exporting rules.

6 Modularization of Polyvariant CFAs

The next question is: what if we modularize an already polyvariant k-CFA[Shi88]? The answer is that modularizing an already polyvariant k-CFA can also make it module-variant. In other words, modular versions of k-CFA can be more accurate than the original k-CFA, hence, its correctness cannot be proven with respect to the original k-CFA.

Example 4 Consider the following two modules.

          ( \begin{matrix}f = (λx.(λz.z) x) \\ g = f λy.y \end{matrix} , \{f,g\}) and ( h = f (g λw.w) , \{h\}) .

1-CFA concludes that h can be evaluated to both λw.w and λy.y, because they cannot distinguish z’s bindings by the applications of g and h. (1-CFA can only distinguish variables by their last call sites.) However, we can export naturally, from the first module, f → (λx.(λz.z) x) and g → λy.y, and we can conclude that h can be evaluated to only λw.w, which is same to the result of the module-variant CFA. For any k-CFA, we can show similar counter-examples.

Therefore, in order to prove the correctness of modular version of k-CFA, we have to devise a module-variant k-CFA.

On the other hand, it is noteworthy that modular versions of the polymorphic-splitting CFA [WJ98] are always sound with respect to the original version. It is because the polymorphicsplitting CFA is already more accurate than the module-variant CFA. When an application uses a let-bound (declared) function, the polymorphic-splitting CFA separately copies the equations derived from the function, and analyzes the application with the copied equations. This process makes the polymorphic-splitting CFA already polyvariant at the declaration-level which is of a finer grain than module-level.

7 Conclusion

Designing modular analyses, which are practical alternatives to whole-program analysis for large-scale realistic programs, is usually after whole-program analyses’ cost-accuracy balance is assured. It is, however, not much studied on how to derive a correct modular version from a given whole-program analysis. For example, to our knowledge, the abstract interpretation framework [CC77, CC92] does not yet cover the practices of designing modular static analyses; it assumes that the whole-program text is available a priori.

This article is about our findings that we realized when we tried to derive modular controlflow analyses for a higher-order language from a whole-program analysis:

• Deriving a modular version (in the framework of incremental analysis) from a wholeprogram CFA makes the resulting analysis polyvariant at module-level.

• If the original whole-program CFA was less accurate than or incomparable to modulelevel polyvariant analyses, then the correctness of its modular version may not be proven with respect to the original analysis, because the modular CFA, in that case, becomes more accurate than the original whole-program CFA.

• A convenient vehicle to prove the correctness of modular CFAs is a whole-program CFA that is polyvariant at module-level.

Our result can be seen as a clarification of possible problems in designing a correct modular analysis from a whole-program analysis, and as a hint of using the module-variant wholeprogram analysis in proving the correctness of modular static analyses.

Appendix

A Proof of Corollary 1

We use the following notations. Solution Sol_{m}(℘) denotes a set of edges introduced in analyzing a program ℘ by the module-variant CFA. Relation A ≤ B denotes a transitive closure of module-dependency relation ⊏. Relation A < B denotes that A ≤ B and A ≠ B. Set Reachable_{I} denotes the Reachable set of the exporting phase in analyzing module I by N. Set Depend_{I} denotes the Depend set of the exporting phase in analyzing module I by S. Node |n| denotes the node of modular CFAs that corresponds to node n of the module-variant CFA. For example, |x_{M}| = x, |f| = f and |λ(x, e^{l})| = λ(x, l).

Theorem 2 For a merged whole program ℘ of modules, the followings are true:

• If M ⊢ e^{l} ∈ Sol_{m}(℘) where e^{l} ∈ A, then l ∈ Reachable_{I} for A ≤ I < M.

• If n → m ∈ Sol_{m}(℘) where m ∈ A, and n has M as its index or n is a function name in M, then

– |n| → |m| ∈ Δ_{M} and

– |m| ∈ Reachable_{I} for A ≤ I < M.

where Δ_{M} is the solved edges Δ (in Section 2) in analyzing module M by N.

Proof. We prove by induction on the size of the edge construction tree.

• case (Dec_{M}): Suppose that the edge is constructed by (Dec_{M}):

{f = e^{l} ∈ M \atop M ⊢ e^{l} f → l_{M}} (Dec_{M}).

Because e^{l} ∈ M, we have nothing to prove for M ⊢ e^{l}. By (Dec), f = e^{l} ∈ M implies f → l ∈ Δ_{M}.

• case (Dvar_{M}): Suppose that the edge is constructed by (Dvar_{M}):

{M ⊢ f^{l} \atop l_{M} → f} (Dvar_{M})

where f ∈ A and f^{l} ∈ B. By induction hypothesis,

l ∈ Reachable_{I} for B ≤ I < M.  (1)

By (Var), f^{l} ∈ B implies l → f ∈ Δ_{B}. By (1) and (Out),

l → f ∈ Δ_{I} for B ≤ I ≤ M

and

f ∈ Reachable_{I} for B ≤ I < M.

Because B directly refers to f, f is a function name in B (that is, A = B), or A is the next module of B (f ∈ sig_{A} and A ⊏ B). In the latter case, by (Sig), f ∈ Reachable_{A}. Therefore, whether A = B or not,

f ∈ Reachable_{I} for A ≤ I < M.

• case (Bvar_{M}): Suppose that the edge is constructed by (Bvar_{M}):

{M ⊢ x^{l} \atop l_{M} → x_{M}}

where x^{l} ∈ A. By (Var), x^{l} ∈ A implies l → x ∈ Δ_{A}. By induction hypothesis, l ∈ Reachable_{I} for A ≤ I < M. Thus by (Out),

l → x ∈ Δ_{I} for A ≤ I ≤ M

and

x ∈ Reachable_{I} for A ≤ I < M.

• case (Lam_{M}): Similar to the case of (Bvar_{M}).

• case (Appd_{M}): Suppose that the edges are constructed by (Appd_{M}):

{M ⊢ (e_{1}^{l_{1}} e_{2}^{l_{2}})^{l} \atop M ⊢ e_{1}^{l_{1}} M ⊢ e_{2}^{l_{2}}}

where (e_{1}^{l_{1}} e_{2}^{l_{2}})^{l} ∈ A. By (Appd), l → @(l_{1}, l_{2}) ∈ Δ_{A}. By induction, l ∈ Reachable_{I} for A ≤ I < M. By (Out), @(l_{1}, l_{2}) ∈ Reachable_{I} for A ≤ I < M. Thus by (SubApp),

l_{1}, l_{2} ∈ Reachable_{I} for A ≤ I < M.

• case (App_{M}): Suppose that the edges are constructed by (App_{M}):

{M ⊢ (e_{1}^{l_{1}} e_{2}^{l_{2}})^{l} l_{1}_{M} → λ(x, e^{l_{0}}) \atop M ⊢ e^{l_{0}} x_{M} → l_{2}_{M} l_{M} → l_{0}_{M}}

where (e_{1}^{l_{1}} e_{2}^{l_{2}})^{l} ∈ A and λx.e^{l_{0}} ∈ B. By induction hypothesis,

l ∈ Reachable_{I} for A ≤ I < M,  (2)
l_{1} → λ(x, l_{0}) ∈ Δ_{M}, and  (3)
λ(x, l_{0}) ∈ Reachable_{I} for B ≤ I < M.  (4)

By (4) and (SubLam),

l_{0} ∈ Reachable_{I} for B ≤ I < M.

By (Appd), (e_{1}^{l_{1}} e_{2}^{l_{2}})^{l} ∈ A implies l → @(l_{1}, l_{2}) ∈ Δ_{A}. Then by (2) and (Out),

l → @(l_{1}, l_{2}) ∈ Δ_{I} for A ≤ I ≤ M  (5)

and @(l_{1}, l_{2}) ∈ Reachable_{I} for A ≤ I < M. Thus by (SubApp),

l_{2} ∈ Reachable_{I} for A ≤ I < M.

By (3), (5) and (App),

l → l_{0} ∈ Δ_{M}

and x → l_{2} ∈ Δ_{M}.

• case (Tr_{M}): Suppose that the edge is constructed by (Tr_{M}):

{n_{N} → m_{M} m_{M} → λ(x, e^{l}) \atop n_{N} → λ(x, e^{l})}

where m ∈ A and λ(x, e^{l}) ∈ B. For convenience, if m is a declaration variable, then we assume that m has m’s own module A as its index (Note that a declaration variable has no index). By induction hypothesis,

n → m ∈ Δ_{N},  (6)
m ∈ Reachable_{I} for A ≤ I < N,  (7)
m → λ(x, l) ∈ Δ_{M},  (8)
λ(x, l) ∈ Reachable_{I} for B ≤ I < M  (9)

Because A ≤ M ≤ N, (7), (8) and (Out) imply

m → λ(x, l) ∈ Δ_{I} for M ≤ I ≤ N  (10)

and λ(x, l) ∈ Reachable_{I} for M ≤ I < N; that is, with (9),

λ(x, l) ∈ Reachable_{I} for B ≤ I < N.

By (6), (10) and (Tr),

n → λ(x, l) ∈ Δ_{N}.

B Proof of Corollary 2

Theorem 3 For a merged whole program ℘ of modules, the followings are true: • If M ⊢ e^{l} ∈ Sol_{m}(℘) and e^{l} ∈ A, then l ∈ Depend_{I} for A ≤ I < M.

• If n → m ∈ Sol_{m}(℘), and – n is not a declaration variable or

– n is a declaration variable and m is a function value, where m ∈ A, and n has M as its index or n is a declaration variable in M, then

– |n| → |m| ∈ Δ_{M},

– |m| ∈ Depend_{I} for A ≤ I < M. where Δ_{M} is the solved edges Δ (in Section 2) in analyzing module M by S. Proof. We also prove by induction on the size of the edge construction tree. There is nothing to prove for the case of (Dec_{M}), and other cases, except for the case of (Tr_{M}), are the same as the proof of Theorem 2 if we replace (Out) by (Excl), and Reachable by Depend.

• case (Tr_{M}): Suppose that the edges are constructed by (Tr_{M}):

{n → m m → λ(x, e^{l}) \atop n → λ(x, e^{l}).}

We prove for two cases: when m is a declaration variable and not.

– If m is a declaration variable g: then the edge is constructed by the following:

{l_{M} → g g → λ(x, e^{l_{0}}) \atop l_{M} → λ(x, e^{l})}

where g ∈ A and λ(x, e^{l_{0}}) ∈ B. By induction hypothesis,

l → g ∈ Δ_{M},  (11)
g ∈ Depend_{I} for A ≤ I < M,  (12)
g → λ(x, l_{0}) ∈ Δ_{A}, and  (13)
λ(x, l_{0}) ∈ Depend_{I} for B ≤ I < A.  (14)

By (12), (13) and (FtoLam),

g → λ(x, l_{0}) ∈ Δ_{I} for A ≤ I ≤ M  (15)

and λ(x, l_{0}) ∈ Depend_{I} for A ≤ I < M; that is, with (14),

λ(x, l_{0}) ∈ Depend_{I} for B ≤ I < M.

By (11), (15) and (Tr),

l → λ(x, l_{0}) ∈ Δ_{M}.

– If m is not a declaration variable: then the edge is constructed by the following:

{n_{M} → m_{M} m_{M} → λ(x, e^{l}) \atop n_{M} → λ(x, e^{l})}

where λ(x, e^{l}) ∈ A. By induction hypothesis,

n → m ∈ Δ_{M},  (16)
m → λ(x, l) ∈ Δ_{M}, and  (17)
λ(x, l) ∈ Depend_{I} for A ≤ I < M.  (18)

By (16), (17) and (Tr),

n → λ(x, l) ∈ Δ_{M}.

References

[AM94] Andrew W. Appel and David B. MacQueen. Separate compilation for Standard ML. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 13–23, June 1994.

[CC77] Patrick Cousot and Radhia Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction of approximation of fixpoints. In Proceedings of the ACM SIGPLAN Symposium on Principles of Programming Languages, pages 238–252, Los Angeles, January 1977.

[CC92] Patrick Cousot and Radhia Cousot. Abstract interpretation frameworks. Journal of Logic Computation, 2(4):511–547, 1992. Also as a tech report: Ecole Polytechnique, no. LIX/RR/92/10.

[HM97] Nevin Heintze and David McAllester. Linear-time subtransitive control flow analysis. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 261–272, June 1997.

[NN97] Flemming Nielson and Hanne Riis Nielson. Infinitary control flow analysis: a collecting semantics for closure analysis. In Proceedings of the ACM SIGPLAN Symposium on Principles of Programming Languages, 1997.

[Shi88] Olin Shivers. Control flow analysis in scheme. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, June 1988.

[WJ98] Andrew K. Wright and Suresh Jagannathan. Polymorphic splitting: an effective polyvariant flow analysis. ACM Transactions on Programming Languages and Systems, 20(1):166–207, 1998.