Towards a Cost-effective Estimation of Uncaught Exceptions in SML Programs^{⋆}

[The 4th International Static Analysis Symposium, Paris, Sept. 1997]

Kwangkeun Yi and Sukyoung Ryu

                 {kwang,puppy}@cs.kaist.ac.kr

Dept. of Computer Science Korea Advanced Institute of Science and Technology(KAIST)

Abstract. We present a static analysis that detects potential runtime exceptions that are raised and never handled inside Standard ML (SML) programs. This analysis will predict abrupt termination of SML programs, which is SML’s only one “safety hole.” Even though SML program’s control flow and exception flow are in general mutually dependent, analyzing the two flows are safely decoupled. Program’s control-flow is firstly estimated from a set of equations defined by simple case analysis of call expressions. Using this call-graph information, program’s exception flow is derived as set-constraints, whose least model is our analysis result. Both of these two analyses are proven safe and the reasons behind each design decision are discussed. A preliminary implementation of this analysis has been applied to realistic SML programs and shows a promising cost-accuracy performance. For the ML-Lex program, for example, the analysis takes 4.58 seconds and it reports 4 may-uncaught exceptions, among which 3 exceptions can really escape. Our final goal is to make the analysis overhead less than 10% of the compilation time (compiling the ML-Lex takes 6 to 7 seconds) and to analyze modules in isolation.

1 Introduction

Exception handling facilities in Standard ML [MTH90] allow the programmer to define, raise and handle exceptional conditions. Exceptional conditions are brought (by a raise expression) to the attention of another expression where the raised exceptions may be handled.

The exception facilities, however, can provide a hole for program safety. SML programs can abruptly halt when an exception is raised and never handled. This is the only one “safety hole” in well-typed SML programs. Uncaught exceptions are sometimes disastrous [Ar996].

In this paper, we present a static analysis that detects exceptions that may cause this abrupt halt of SML programs. Our goal is to develop an effective such analysis that has less than 10% overhead of the total compilation time.

⋆ This work is supported in part by KOSEF (Grant 95-0100-54-3), by Korea Ministry of Information and Communication (Grant 96151-IT2-12), by Korea Ministry of Science and Technology, and by Samsung Electronics Corp.

1.1 Analysis Problems

– SML exceptions are first-class objects. Consider:

                          fun f(x) = · · · raise !x · · ·

Function f raises an exception !x in a location x passed to f.

– Precise exception analysis needs a precise call-graph estimation. Consider:

                      fun f(g) = · · · g(x) handle E => · · ·

In order to estimate the uncaught exceptions from g(x), we must analyze which functions are bound to g when f is called.

– Conversely, precise call-graph estimation needs a precise exception analysis. Con-

sider:

                fun f(x) = · · · e handle E(g) => g(x) · · ·  (*)

In order to decide which functions are called at g(x), we must decide whether the e’s uncaught exceptions include E and, if so, which functions are carried by it.

Caveat: Our analysis cannot analyze programs that utilize the generative nature of the exception (and the datatype) declarations. This limitation is not severe; exceptions (and datatypes) are largely declared at the global scope^{2} or at a module level, or we can move existing local declarations out to the global level without affecting the “observational” behavior of the programs. Programs where this hoisting is impossible cannot be analyzed correctly by our analysis.

We consider only exceptions that appear in the program’s text (including library sources). This limitation can easily be lifted if our analysis starts with a table of primitive operators and their exceptions.

1.2 Our Approach

In the earlier work [Yi94], all the above problems were tackled by a monolithic abstract interpreter. Functions, exceptions, and other data values were parts of the abstract values. The analysis was a collecting analysis that computed stable program states at each expression point of the input program. This monolithic approach was appealing because the analysis design and its correctness proof was done at once by a sound abstraction of the SML’s concrete semantics. The collecting analyzer was, however, too expensive. It took about one hour to analyze the ML-Lex program, for example.

For a better cost-effective analysis, we surveyed SML codes and found that such a full-fledged analysis may be an overkill in almost all cases. In particular, we found that such case as (*) almost never happened (Figure 1)^{3}. This suggests that, in most cases, the call-graph estimation can be done independent of the exception analysis. Preparing for the rare case that exceptions carry functions would not pay-off in practice.

This does not mean that we don’t guarantee the safety of our call-graph estimation. For such cases when functions to call are brought by uncaught exceptions, we choose to do a crude approximation, believing that this “large” approximation would be rarely detrimental to the call-graph accuracy. Please note that we cannot use standard techniques (e.g., 0CFA) for closure analysis [Shi91, Hei93, PS92, JW96] because their correctness does not consider languages with function-carrying exceptions.

2 In CAML, only top-level exception declarations are permitted. 3 At least for hand-written codes. Situation may be different in automatically gener-

ated programs.

program  exns^{a} w/ args^{b} arg types^{c}  ftn arg^{d}
Knuth-Bendix.sml  1  1 string  0
ml-lex.sml  8  1 int list * string

0

SML/NJ 109 339 34 string, string*int, int list, intmap, System.Unsafe.object list, symbol list, exn, unit→unit 1 (the Found exception in debug/

                                                     run.sml)

HOL  60  18 string, int, record of

string/int

0

a number of exception declarations (static count) b number of exceptions with arguments (static count) c argument types: basic building blocks after chasing type abbreviations and datatype arguments

d number of exceptions whose argument has a function (static count)

Fig. 1. Exception Use Statistics in SML Programs

Program’s call-graph is defined as the least solution satisfying a set of simultaneous equations. These equations are defined by case analysis of function expressions. For example, “x(0)” calls functions that are bound to x when λx.e is called (programs are alpha-converted), “(f 0) 1” calls functions (f 0) that the f’s body (a function expression) represents. The crude approximation is when an exception’s argument is the function to call. In this case we look up the places where exceptions are made and collect functions that are paired at those places. To fine-tune this approximation, among such functions we collect those whose types unify with the call expression’s function type. The exact definition is in Proposition 4, after we fix the source language.

This call graph information is then used in exception analysis. For each function f, we express its exception flow as two classes of set constraints:

– One class is for set P_{f} of f’s uncaught exceptions^{4}. For example, P_{f} of the following

function

                              fun f(x) = e(0)+1

includes the sum ⋃_{g} P_{g} of P_{g}’s for g that may be called at “e(0).” In some cases, P_{f} is also composed of the set of exceptions that are available in f.^{5} For example, P_{f} of the following function

                              fun f(x) = raise x

includes the set of exceptions passed to f.

– The other class of constraints is for set X_{f} of exception values that are available during f’s application. In the previous example function f, X_{f} includes the sum ⋃_{g} X_{g} of X_{g}’s for g that may call f, because the caller g may pass its available exceptions to f through x.

4 In SML, uncaught exceptions are called exception packets. Hence “P_{f}.” 5 A value v is available in a function f iff, during program execution, the v is a result

of a sub-expression of the function body.

e ::= x  variable
| λx_{τ} .e  function
| e_{1} e_{2}  application
| exn κ e  exception construction
| decon e  deconstruction
| case e_{1} κ e_{2} e_{3} switch
| fix f λx_{τ} .e_{1} in e_{2} recursive function binding
| raise e  exception raise
| +raise e κ  exception raise-only
| -raise e κ_{1} ⋯ κ_{n} exception raise-except
| handle e_{1} λx_{τ} .e_{2} exception handler
| 1  constant
τ ::= τ exn exception type with argument type τ
| τ → τ function type
| ι  constant type

Fig. 2. L’s Abstract Syntax

Our exception analysis is to build the set of constraints (for P_{f} and X_{f}) and to compute its least solution (model). After the analysis, two things are reported to the programmer:

1. The solution of P_{f} for each top-level function f. The existence of such exceptions implies that the program can terminate abnormally.

2. Uncaught exceptions from each handle expression. From this information the programmer can check the completeness of the handler patterns.

2 Language L

For presentation brevity we present our analysis for an imaginary language L. The language is a monomorphically typed, call-by-value, high-order language. The language L’s abstract syntax is shown in Figure 2. The usual monomorphic type rules are omitted.

Values in L are either exceptions or functions. An exception value “exn κ e” is constructed from an exception name κ and an expression e for its argument value. The argument of an exception is recovered by “decon e”. “fix f λx_{τ} .e_{1} in e_{2}” binds recursive function f = λx_{τ} .e_{1} in e_{2}. The case expression “case e_{1} κ e_{2} e_{3}” branches to e_{2} if the value of e_{1} is constructed with κ, otherwise, to e_{3}. “raise e” raises exception e. The +raise and -raise expressions are used in limited contexts, which we will discuss in the next section. The handle expression “handle e_{1} λx_{τ} .e_{2}”, where e_{2} is typically a case expression on x, evaluates e_{1} first. If e_{1}’s result is a raised exception whose type is τ, the exception is bound to x inside e_{2}. Otherwise, e_{1}’s normal value is returned.^{6}

6 Note that this handle expression can handle only one type of exceptions. To be more realistic, handle expression must have multiple functions (handle e_{1} [λx_{τ_{i}}.e_{2}]^{+}) for different exception types τ_{i}. Considering such handle expression, however, unnecessarily complicates our presentation.

The function “λx_{τ} .e_{2}” in a handle expression “handle e_{1} λx_{τ} .e_{2}” is called a handler function, the expression “e_{1}” a handlee expression, and the argument “x” of the handler function a handle variable.

Definition 1 (type(e)). For a program p, type_{p}(e) denotes the type of an expression e in p. We write type(e) when it is clear from the context which program the expression e belongs to.

2.1 SML Programs in L

We assume that SML programs in L satisfy the following noteworthy things. It is straightforward to find such L program that corresponds to a given SML program. (Note that, in this section, some examples in L are not supported by the abstract syntax of Figure 2. For convenience we use numbers, multiple branches with the wild pattern, and exceptions with no argument.)

-raise and +raise expressions are used inside the handler expression to make the exception-handling situation explicit in the text, which facilitates our analysis design.

– -raise The handler patterns are always augmented with an extra raise (-raise) expression, in order to re-raise exceptions that are not caught.

                 e handle ERROR => 1 | FAIL => 2

\underrightarrow{is}

handle e λ x_{exn}.

                                           case x
                                             ERROR 1
                                             FAIL  2
                                               -raise x ERROR FAIL

“-raise x ERROR FAIL” indicates that the re-raised exceptions are those bound to x excluding ERROR and FAIL.

– +raise If a handler’s pattern for exception’s argument part is not complete, the exception is explicitly re-raised by +raise:

       exception E of int list

⋯

       e handle E nil => 1

\underrightarrow{is} handle e λ x_{(ιlist)exn}.

                                          case x

E (λ y_{ιlist}.

                                                 case y
                                                   NIL 1
                                                    +raise x E) (decon x)
                                             -raise x E

Above program’s handler can handle exception E only with nil list. Program in L makes this situation explicit by re-raising the E exceptions if their arguments are non-empty list. “+raise x E” indicates the re-raised exception shall only be the E exceptions.

– Exception constructors that need arguments are translated into a function, which

is β-reduced whenever appropriate. For example,

       exception E of int

⋯ E, ⋯

\underrightarrow{is} · · · (λ x_{ι}.(exn E x)), · · ·

– Every functor applications are in-lined. That is, functor definitions and applications disappear and are replaced by in-lined structures.^{7}

7 In SML, parameterized modules are called functors. A functor is a function that, given an argument structure, returns a new structure. A structure is a named collection of declarations.

3 Set-Constraint Systems

Our exception analysis is presented in the set-constraint framework[Hei92, AH95]. We use this framework not because we will use its computation method (infinite solution as a grammar form) but because the modular nature of the constraints makes our presentation easy. Our exception analysis is computed by the conventional iterative fixpoint method because our solution space is finite: exception names in the program. Correctness proves are done by the fixpoint induction over the continuous functions that are derived [CC95] from our constraint systems.

We present three set-constraint systems: ⊳_{1}, ⊳_{2}, and ⊳_{3}. Our analysis is the last one ⊳_{3}. Other two constraint systems are stepping stones to prove ⊳_{3}’s safety. Note that 1) our analysis decouples control-flow analysis from exception analysis and 2) our interest is in uncaught exceptions from functions. These two things are done by ⊳_{2} and ⊳_{3} in order. ⊳_{2} (Section 3.3) decouples control-flow analysis (Section 3.2) from exception analysis. ⊳_{3} (Section 3.4) increases the constraint granularity to the functionlevel. Because exception-related expressions are sparse in programs, it is wasteful to generate constraints for every expression of the input program as in ⊳_{2}. ⊳_{3} is proven consistent with ⊳_{2}, ⊳_{2} with ⊳_{1}, and ⊳_{1} (Section 3.1) is assumed correct with respect to the standard semantics.

In presenting the set-constraint rules, we assume that 1) L programs are well-typed and 2) all variables in L programs are uniquely named.

To review some notions of set constraint formalism, an interpretation I is a model of a conjunction C of constraints if, for each constraint X ⊇ se (set variable X and set expression se) in C, I(se) is defined and I(X) ⊇ I(se). We write lm(C) for the least model of C. All the systems(⊳_{1}, ⊳_{2}, ⊳_{3}) guarantee the existence of the least model because every operator is monotonic (in terms of set-inclusion) and each constraint’s left-hand-side is a single variable [Hei92].

3.1 Concrete Constraint Construction ⊳_{1}

Every expression e of the input program has two set constraints: V_{e} ⊇ se and P_{e} ⊇ se. The set variable (the unknown) V_{e} is for e’s values, P_{e} is for the uncaught exceptions (packets) during e’s evaluation. A constraint V_{e} ⊇ se (P_{e} ⊇ se) may be read as “expression e evaluates into a set of values (has uncaught exceptions) including those of se.”

In Figure 3 we show only three cases: application, raise, and handle expression. Other cases are straightforward adaptation of [Hei93]. We index V and P sometimes with expressions, sometimes with numbers. The subscript “e” of set variables “V_{e}” and “P_{e}” denotes the current expression to which the current rule applies. For constraint variables for e’s i-th sub-expression, we write “V_{i}” as a shorthand for “V_{e_{i}}”.

Our analysis could have been computing the solution of the ⊳_{1} constraints by using Heintze’s method [Hei93]. However, it is wasteful to consider all expressions and their values because exception-related expressions are sparse in programs and function values (for control-flow analysis) can be separately estimated. These two observations are reflected in the forthcoming constraint systems, ⊳_{2} and ⊳_{3}.

Proposition 2 (Typefulness of ⊳_{1}). For a closed term e, let ⊳_{1} e: C_{1}. Then its least model lm(C_{1}) preserves types: ∀e_{i} ∈ e.lm(C_{1})(V_{i}) ⊆ Val_{type(e_{i})}(the set of values of type(e_{i})).

v ∈ Val  = Closure + Exn + {1} values
λx_{τ} .e ∈ Closure = Lambda  lambda exprs
κ v ∈ Exn = Con × Val  exceptions
κ ∈ Con = {κ_{1}, ⋯, κ_{N}}  exception constructors
κ v ∈ Packet = Exn  raised exceptions
I(V_{e}) ⊆ Val  I(P_{e})  ⊆ Packet
I(λx_{τ} .e) = {λx_{τ} .e}  I(se ∪ se′) = I(se) ∪ I(se′)
I(app_{V} (V_{1}))  = {v | λx_{τ} .e ∈ I(V_{1}), v ∈ I(V_{e})}
I(app_{P} (V_{1}))  = {κ v | λx_{τ} .e ∈ I(V_{1}), κ v ∈ I(P_{e})}
I(-raise(V_{1}, κ_{1}, ⋯, κ_{n})) = {κ′v | κ′v ∈ I(V_{1}), ∀i.κ_{i} ≠ κ′}
I(+raise(V_{1}, κ))  = {κ v | κ v ∈ I(V_{1})}
[APP_{⊳_{1}} ] \begin{matrix}⊳_{1} e_{1}: C_{1} & ⊳_{1} e_{2}: C_{2} \\ ⊳_{1} e_{1} e_{2}: \{V_{e} ⊇ app_{V} (V_{1}), P_{e} ⊇ app_{P} (V_{1}) ∪ P_{1} ∪ P_{2}\} ∪ C_{1} ∪ C_{2} \end{matrix}

[RS_{⊳_{1}} ]  {⊳_{1} e_{1}: C_{1} \atop ⊳_{1} raise e_{1}: \{P_{e} ⊇ V_{1} ∪ P_{1}\} ∪ C_{1}}

[-RS_{⊳_{1}} ] ⊳_{1} e_{1}: C_{1} ⊳_{1} -raise e_{1} κ_{1} ⋯ κ_{n}: {P_{e} ⊇ -raise(V_{1}, κ_{1}, ⋯, κ_{n}) ∪ P_{1}} ∪ C_{1}

[+RS_{⊳_{1}} ] (⊳_{1} e_{1}: C_{1}) / (⊳_{1} +raise e_{1} κ: {P_{e} ⊇ +raise(V_{1}, κ) ∪ P_{1}} ∪ C_{1})

[HNDL_{⊳_{1}} ]

⊳_{1} e_{1}: C_{1}  ⊳_{1} e_{2}: C_{2}
⊳_{1} handle e_{1} λx_{τ} .e_{2}: { V_{e} ⊇ app_{V} (λx_{τ} .e_{2}) ∪ V_{1},
P_{e} ⊇ app_{P} (λx_{τ} .e_{2}), V_{x} ⊇ P_{1}
} ∪ C_{1} ∪ C_{2}

Fig. 3. Constructing Concrete Constraints: ⊳_{1}

This typefulness is important for the consistency of the forthcoming constraint system ⊳_{2}.

The correctness of ⊳_{1} (i.e., the least model of ⊳_{1}-constraints for a program includes the actual values and uncaught exceptions) is assumed; the proof must not be much different from those outlined in [Hei93], using a “set-based operational semantics” as an intermediate form.

3.2 Separate Call-graph Estimation

Definition 3. Lam is safe with respect to ⊳_{1} iff ⊳_{1} e: C implies that, for every functiontyped expression e′ of the program e, Lam(e′) ⊇ lm(C)(V_{e′}).

Proposition 4 (A safe call table Lam). Given a program e, let FtnExpr be the set of function-typed expressions in e, and 2^{Lambda} be the powerset of lambda expressions in e. Define

Lam: FtnExpr → 2^{Lambda}

to be the least table satisfying the following equations:

Lam(λx_{τ} .e) = {λx_{τ} .e}  constant function
Lam(f)  = {λx_{τ} .e | fix f λx_{τ} .e in program} named function
Lam(x)  = ∪{Lam(e_{2}) | e_{1} e_{2} in program ∧ λx_{τ} .e ∈ Lam(e_{1})} ftn var
Lam(e_{1} e_{2}) = ∪{Lam(e) | λx_{τ} .e ∈ Lam(e_{1})} function from application
Lam(decon e) = ∪{Lam(e′) | exn κ e′ in program ∧ type(e′) = type(decon e)}
Lam(fix f λx_{τ} e_{1} in e_{2}) = Lam(e_{2})
Lam(case e_{1} κ e_{2} e_{3}) = Lam(e_{2}) ∪ Lam(e_{3})
Lam(handle e_{1} λ_{τ} .e_{2}) = Lam(e_{1}) ∪ Lam(e_{2})

Then Lam is safe with respect to ⊳_{1}.

Note that the last case: if functions to call are the arguments of exceptions then we look up the exception construction expressions in the program and collect functions that are paired. Among those exception expressions we selectively choose those whose argument type is equal to the target function. (Note that the L language is monomorphic. In SML, the “is equal to” must be “unifies with.”)

3.3 Exception Constraint Construction ⊳_{2}

We now consider a new system ⊳_{2}(Figure 4) where only exceptions are considered. Constraints for function (non-exception) values are removed and instead, a pre-computed, safe call-graph table Lam (Proposition 4) is used.

Every expression e has two set constraints: X_{e} ⊇ se (for its exception values) and P_{e} ⊇ se (for uncaught exceptions during its evaluation). For solutions of X_{e} and P_{e} we will consider only exception names. That is, X_{e} is for the projection |V_{e}| of e’s values V_{e}:

I(X_{e}) ⊇ |V_{e}| =^{def} {κ | κ v ∈ V_{e}} ∪ |{v | κ v ∈ V_{e}}|.

The use of set expression app(e_{1}) for function calls is similar to that in ⊳_{1}, except that we use the call-graph table Lam: FtnExpr → 2^{Lambda}(Proposition 4).

Set variable’s indexing convention is the same as in the previous section (⊳_{1}). Consider the rule for -raise expression:

[-RS_{⊳_{2}} ] {⊳_{2} e_{1}: C_{1} \atop ⊳_{2} -raise e_{1} κ_{1} ⋯ κ_{n}: \{P_{e} ⊇ (X_{1} \_{e_{1}} \{κ_{1}, ⋯, κ_{n}\}) ∪ P_{1}\} ∪ C_{1}}

The constraint P_{e} ⊇ X_{1} \_{e} {κ_{1}, ⋯, κ_{n}} collects raised exceptions excluding the κ_{i}’s. Note the meaning of \_{e}:

I(X_{1} \_{e} \{κ_{1}, ⋯, κ_{n}\}) = \{ \begin{matrix}I(X_{1}) & if type(e) = τ′exn ∧ isExn(τ′) \\ I(X_{1}) \ \{κ_{1}, ⋯, κ_{n}\} & otherwise \end{matrix}

If an exception can have other exceptions as its arguments then the exclusion \_{e} has no effect. If blindly excluded, exceptions that are hidden as arguments of the escaping exception are considered caught. This makes the analysis unsafe. (The same reason is for the definition of ∩_{e}.)

The constraint-construction rule ⊳_{2} is a safe approximation of ⊳_{1}:

κ ∈ Exn = {κ_{1}, ⋯, κ_{N}} exception names in program
κ ∈ Packet = Exn  raised exceptions
I(X_{e}) ⊆ Exn  I(P_{e}) ⊆ Packet
I(var(x))  = {κ | “e_{1} e_{2}” ∈ e, λx_{τ} .• ∈ Lam(e_{1}), κ ∈ I(X_{2})}
I(app_{X}(e_{1}))  = {κ | λx_{τ} .e ∈ Lam(e_{1}), κ ∈ I(X_{e})}
I(app_{P} (e_{1}))  = {κ | λx_{τ} .e ∈ Lam(e_{1}), κ ∈ I(P_{e})}
isExn(τ)  = true iff τ = τ′ exn
I(X_{1} \_{e} \{κ_{1}, ⋯, κ_{n}\}) = \{ \begin{matrix}I(X_{1}) & if type(e) = τ′exn ∧ isExn(τ′) \\ I(X_{1}) \ \{κ_{1}, ⋯, κ_{n}\} & otherwise \end{matrix}
I(X_{1} ∩_{e} \{κ\})  = \{ \begin{matrix}I(X_{1}) & if type(e) = τ′exn ∧ isExn(τ′) \\ I(X_{1}) ∩ \{κ\} & otherwise \end{matrix}
I(κ)  = {κ}

I(λx_{τ} .e) and I(se ∪ se) are the same as in ⊳_{1} (Figure 3).

[VAR_{⊳_{2}} ] ⊳_{2} x: {X_{x} ⊇ var(x)}  [C_{⊳_{2}} ]  ⊳_{2} 1: ∅

[ABS_{⊳_{2}} ]  {⊳_{2} e_{1}: C_{1} \atop ⊳_{2} λx_{τ} .e_{1}: C_{1}}  [FIX_{⊳_{2}} ]  \begin{matrix}⊳_{2} e_{1}: C_{1} & ⊳_{2} e_{2}: C_{2} \\ ⊳_{2} fix f λx_{τ} .e_{1} in e_{2}: \{X_{e} ⊇ X_{2}, P_{e} ⊇ P_{2}\} ∪ C_{1} ∪ C_{2} \end{matrix}

[EXN_{⊳_{2}} ]  {⊳_{2} e_{1}: C_{1} \atop ⊳_{2} exn κ e_{1}: \{X_{e} ⊇ κ ∪ X_{1}, P_{e} ⊇ P_{1}\} ∪ C_{1}}

[DCON_{⊳_{2}} ]  {⊳_{2} e_{1}: C_{1} \atop ⊳_{2} decon e_{1}: \{X_{e} ⊇ X_{1}, P_{e} ⊇ P_{1}\} ∪ C_{1}}

[APP_{⊳_{2}} ]  \begin{matrix}⊳_{2} e_{1}: C_{1} & ⊳_{2} e_{2}: C_{2} \\ ⊳_{2} e_{1} e_{2}: \{X_{e} ⊇ app_{X}(e_{1}), P_{e} ⊇ app_{P} (e_{1}) ∪ P_{1} ∪ P_{2}\} ∪ C_{1} ∪ C_{2} \end{matrix}

[CASE_{⊳_{2}} ] \begin{matrix}⊳_{2} e_{1}: C_{1} & ⊳_{2} e_{2}: C_{2} & ⊳_{2} e_{3}: C_{3} \\ ⊳_{2} case e_{1} κ e_{2} e_{3}: \{X_{e} ⊇ X_{2} ∪ X_{3}, P_{e} ⊇ P_{1} ∪ P_{2} ∪ P_{3}\} ∪ C_{1} ∪ C_{2} ∪ C_{3} \end{matrix}

[RS_{⊳_{2}} ]  {⊳_{2} e_{1}: C_{1} \atop ⊳_{2} raise e_{1}: \{P_{e} ⊇ X_{1} ∪ P_{1}\} ∪ C_{1}}

[-RS_{⊳_{2}} ]  {⊳_{2} e_{1}: C_{1} \atop ⊳_{2} -raise e_{1} κ_{1} ⋯ κ_{n}: \{P_{e} ⊇ (X_{1} \_{e_{1}} \{κ_{1}, ⋯, κ_{n}\}) ∪ P_{1}\} ∪ C_{1}}

[+RS_{⊳_{2}} ]  {⊳_{2} e_{1}: C_{1} \atop ⊳_{2} +raise e_{1} κ: \{P_{e} ⊇ (X_{1} ∩_{e_{1}} \{κ\}) ∪ P_{1}\} ∪ C_{1}}

[HNDL_{⊳_{2}} ]

⊳_{2} e_{1}: C_{1}  ⊳_{2} e_{2}: C_{2}
⊳_{2} handle e_{1} λx_{τ} .e_{2}: { X_{e} ⊇ app_{X}(λx_{τ} .e_{2}) ∪ X_{1},
P_{e} ⊇ app_{P} (λx_{τ} .e_{2}), X_{x} ⊇ P_{1}
} ∪ C_{1} ∪ C_{2}

Fig. 4. Constructing Exception Constraints: ⊳_{2} Proposition 5 (Correctness of ⊳_{2}). For a closed term e, let ⊳_{1} e: C_{1} and ⊳_{2} e: C_{2} with their least models, I_{1} = lm(C_{1}) and I_{2} = lm(C_{2}). If Lam is safe with respect to ⊳_{1}, then for every sub-expression e_{i} ∈ e:

I_{2}(X_{i}) ⊇ |I_{1}(V_{i})| and I_{2}(P_{i}) ⊇ |I_{1}(P_{i})|

where |V| is the set of exception names constituting exception values in V

|V| =^{def} {κ | κ v ∈ V} ∪ |{v | κ v ∈ V}|.

3.4 Function’s Exception Constraint Construction ⊳_{3}

It is wasteful to compute uncaught exceptions from every expression because exceptionrelated expressions are sparse in a program. We need to sparsely generate constraints. Using the ⊳_{2} as our stepping stone, we arrive at our constraint system ⊳_{3}(Figure 5) that generates constraints only for functions. The number of unknowns thus becomes proportional to the number of functions, not to the number of expressions. The least model of ⊳_{3}-constraints for an input program is our analysis result: uncaught exceptions from each function.

In ⊳_{3}, set variables are indexed by the lambda and handlee expressions of the input program. We assume that all lambda and handlee expressions are uniquely named as f, g, h, etc. We subscript the lambda with its name: “λ_{f} x_{τ} .e”. Similarly for handlee expression such as “e_{g}” in “handle e_{g} λ_{h}x_{τ} .e_{2}”.

Every function (or handlee expression) f of the input program has two set constraints: X_{f} ⊇ se and P_{f} ⊇ se. The set variable X_{f} is for exceptions that are available in f, and P_{f} is for uncaught exceptions during the call to f.

Consider the rule for application expression:

[APP_{⊳_{3}} ] \begin{matrix}f ⊳_{3} e_{1}: C_{1} & f ⊳_{3} e_{2}: C_{2} \\ f ⊳_{3} e_{1} e_{2}: \{X_{f} ⊇ app_{X}(e_{1}, X_{f}), P_{f} ⊇ app_{P} (e_{1}, X_{f})\} ∪ C_{1} ∪ C_{2} \end{matrix}

The left-hand-side f of “f ⊳_{3} e” indicates that the expression e appears in f. Thus, if f has a call e_{1} e_{2}, available exceptions X_{f} in f must include the exceptions app_{X}(e_{1}, X_{f}) returned from the call. The uncaught exceptions P_{f} in f must include the exceptions app_{P} (e_{1}, X_{f}) uncaught during the call.

One noticeable rule is [VAR_{⊳_{3}} ]. Because the constraint granularity is a function, constraint for a variable x must be expressed in terms of two functions: function f that variable x provides with exceptions and another function g that provides x with exceptions. The f is the function that appears in the left-hand-side of “⊳_{3} x” and the g is the function (Owner(x)) that has x as its argument. Therefore,

[VAR_{⊳_{3}} ] f ⊳_{3} x: {X_{f} ⊇ X_{Owner(x)}}.

One missing constraint is for the effect of passing exceptions through x when its owner Owner(x)(=^{let} g) is called. This is expressed as app_{X}(e_{1}, X_{f})’s third condition I(X_{g}) ⊇ I(X_{f}) (in terms of caller f and callee g):

I(app_{X}(e_{1}, X_{f})) = {κ | λ_{g}x_{τ} .e ∈ Lam(e_{1}), κ ∈ I(X_{g}), I(X_{g}) ⊇ I(X_{f})}.

κ ∈ Exn = {κ_{1}, ⋯, κ_{N}} exception constructors
κ ∈ Packet = Exn  raised exceptions
I(X_{f}) ⊆ Exn  I(P_{f}) ⊆ Packet  X ::= X_{f} | P_{f}
Owner(x)  = f where λ_{f} x_{τ} .e (f’s parameter is x)
I(var(x))  = I(X_{Owner(x)})
I(app_{X}(e_{1}, X)) = {κ | λ_{g}x_{τ} .e ∈ Lam(e_{1}), κ ∈ I(X_{g}), I(X_{g}) ⊇ I(X)}
I(app_{P} (e_{1}, X)) = {κ | λ_{g}x_{τ} .e ∈ Lam(e_{1}), κ ∈ I(P_{g}), I(X_{g}) ⊇ I(X)}

I(X_{f} \_{e} {κ_{1}, ⋯, κ_{n}}), I(X_{f} ∩_{e} {κ}), I(κ), and I(λx_{τ} .e) are the same as in ⊳_{2} (Figure 4)

[VAR_{⊳_{3}} ] f ⊳_{3} x: {X_{f} ⊇ var(x)}  [C_{⊳_{3}} ]  f ⊳_{3} 1: ∅

[ABS_{⊳_{3}} ]  {g ⊳_{3} e_{1}: C_{1} \atop f ⊳_{3} λ_{g}x_{τ} .e_{1}: C_{1}}  [FIX_{⊳_{3}} ] \begin{matrix}g ⊳_{3} e_{1}: C_{1} & f ⊳_{3} e_{2}: C_{2} \\ f ⊳_{3} fix g λ_{g}x_{τ} .e_{1} in e_{2}: C_{1} ∪ C_{2} \end{matrix}

[EXN_{⊳_{3}} ] {f ⊳_{3} e_{1}: C_{1} \atop f ⊳_{3} exn κ e_{1}: \{X_{f} ⊇ κ\} ∪ C_{1}} [DCON_{⊳_{3}} ]  {f ⊳_{3} e_{1}: C_{1} \atop f ⊳_{3} decon e_{1}: C_{1}}

[APP_{⊳_{3}} ] \begin{matrix}f ⊳_{3} e_{1}: C_{1} & f ⊳_{3} e_{2}: C_{2} \\ f ⊳_{3} e_{1} e_{2}: \{X_{f} ⊇ app_{X}(e_{1}, X_{f}), P_{f} ⊇ app_{P} (e_{1}, X_{f})\} ∪ C_{1} ∪ C_{2} \end{matrix}

[CASE_{⊳_{3}} ]  \begin{matrix}f ⊳_{3} e_{1}: C_{1} & f ⊳_{3} e_{2}: C_{2} & f ⊳_{3} e_{3}: C_{3} \\ f ⊳_{3} case e_{1} κ e_{2} e_{3}: C_{1} ∪ C_{2} ∪ C_{3} \end{matrix}

[RS_{⊳_{3}} ]  {f ⊳_{3} e_{1}: C_{1} \atop f ⊳_{3} raise e_{1}: \{P_{f} ⊇ X_{f} \} ∪ C_{1}}

[-RS_{⊳_{3}} ]  {f ⊳_{3} e_{1}: C_{1} \atop f ⊳_{3} -raise e_{1} κ_{1} ⋯ κ_{n}: \{P_{f} ⊇ X_{f} \_{e_{1}} \{κ_{1}, ⋯, κ_{n}\}\} ∪ C_{1}}

[+RS_{⊳_{3}} ]  {f ⊳_{3} e_{1}: C_{1} \atop f ⊳_{3} +raise e_{1} κ: \{P_{f} ⊇ X_{f} ∩_{e_{1}} \{κ\}\} ∪ C_{1}}

[HNDL_{⊳_{3}} ]

g ⊳_{3} e_{g}: C_{1}  h ⊳_{3} e_{2}: C_{2}
f ⊳_{3} handle e_{g} λ_{h}x_{τ} .e_{2}: { X_{f} ⊇ app_{X}(λ_{h}x_{τ} .e_{2}, P_{g}) ∪ X_{g},
P_{f} ⊇ app_{P} (λ_{h}x_{τ} .e_{2}, P_{g})
} ∪ C_{1} ∪ C_{2}

Fig. 5. Constructing Function’s Exception Constraints: ⊳_{3}

Proposition 6 (Correctness of ⊳_{3}). For a closed term e, let ⊳_{2} e: C_{2} and main ⊳_{3} e: C_{3} with their least models, I_{2} = lm(C_{2}) and I_{3} = lm(C_{3}). Then, if g ⊳_{3} e′: C′ occurs during main ⊳_{3} e: C_{3} then

I_{3}(X_{g}) ⊇ I_{2}(X_{e′}) and I_{3}(P_{g}) ⊇ I_{2}(P_{e′}).

Example 1. As an analysis example, consider the following program:

(1)       fun m() = f(exn κ 1)
(2)       fun f(x) = handle g(x) λ_{h} y. 1  ( in SML g(x) handle   => 1)
(3)       fun g(x) = raise x

From line (1) \{ \begin{matrix}X_{m} ⊇ κ \\ X_{f} ⊇ X_{m}, X_{m} ⊇ X_{f} & (from X_{m} ⊇ app_{X}(f, X_{m})) \\ P_{m} ⊇ P_{f} & (from P_{m} ⊇ app_{P} (f, X_{m})) \end{matrix}

From line (2) \{ \begin{matrix}X_{g} ⊇ X_{f} , X_{f} ⊇ X_{g} & (from X_{f} ⊇ app_{X}(g, X_{f})) \\ P_{f} ⊇ P_{h}, X_{h} ⊇ P_{g} & (from P_{f} ⊇ app_{P} (h, P_{g})) \end{matrix}
From line (3) P_{g} ⊇ X_{g}

The least model of the above 9 constraints is the least solution of the equations:

X_{m} = {κ}, X_{f} = X_{m} ∪ X_{g}, X_{g} = X_{f} , X_{h} = P_{g}, P_{m} = P_{f} , P_{f} = P_{h}, P_{g} = X_{g}.

The least solution is:

X_{m} = {κ}, X_{f} = {κ}, X_{g} = {κ}, P_{m} = P_{f} = ∅, P_{g} = {κ}.

3.5 Typeful Constraints for Improved Accuracy

Some constraint rules of ⊳_{3} can be safely sharpened using types. Our actual analysis uses this sharpened ⊳_{3} rules. 1) a function f has exceptions through a variable x only when the x is of an exception type and 2) exceptions X_{f} in f are returned only when f’s return type is an exception type:

I(app_{X}(e_{1}, X)) = {κ | λ_{f} x_{τ} .e ∈ Lam(e_{1}), κ ∈ I(X_{f} |isExn(type(e))),
I(X_{f}) ⊇ I(X |isExn(τ)) }
I(app_{P} (e_{1}, X)) = {κ | λ_{f} x_{τ} .e ∈ Lam(e_{1}), κ ∈ I(P_{f}), I(X_{f}) ⊇ I(X |isExn(τ))}
I(var(x))  = I(X_{Owner(x)}|isExn(type(x)))
X_{f}  ⊇ app_{X}(⋯) ∪ (X_{g}|isExn(type(e_{g})))  in [HNDL_{⊳_{3}} ]

where I(X |cond) = I(X) if the cond true, ∅ otherwise.

The correctness of this new ⊳_{3} can be proved with respect to a typeful version of ⊳_{2} that maps non-exception-typed expressions to the empty set. The typeful ⊳_{2} is consistent with ⊳_{1} because ⊳_{1} is already typeful. The ⊳_{2} becomes typeful by the new [DCON_{⊳_{2}} ] rule:

[DCON_{⊳_{2}} ] (⊳_{2} e_{1}: C_{1}) / (⊳_{2} decon e_{1}: {X_{e} ⊇ (X_{1}|isExn(type(e))), P_{e} ⊇ P_{1}} ∪ C_{1})

3.6 Adapting ⊳_{3} to Standard ML

Because of SML’s polymorphic types,

– isExn needs to be conservative. The new definition is:

isExn(ι ∨ τ → τ′) = false  constant or function type
isExn(α ∨ τ exn) = true  generic type var or exn type
isExn(τ ref )  = isExn(τ)  reference type
isExn(τ_{1} × τ_{2})  = isExn(τ_{1}) or isExn(τ_{2})  record type
isExn(u)  = ∃κ ∈ Con(u).isExn(Arg(κ)) user-defined datatype u

The last case is for when a data type u’s constructor κ ∈ Con(u) receives exceptions as its argument.

program  lines cfa + setup(sec)^{a} solve(sec)^{b} analysis result
Knuth-Bendix.sml  519  8.62^{c}  0.09^{d} 1 (1x,1r,10h)^{e}
ml-lex.sml  1204  4.58  0.01 4 (10x,19r,10h)
pathname.sml(library) 426  0.34  0.00^{f} 4 (4x,6r,3h)
string-cvt.sml(library) 454  0.21  0.00 1 (1x,10r,4h)
class compiler  3511  47.77  0.04 3 (11x,34r,4h)

a Control-flow analysis and constraints set-up: in SML, run on DEC Alpha Server1000(4/200), compiled by SML/NJ 108.13 b Solving constraints: in C, run on Sparc 20, compiled by GCC c SML user+system+gc time d C user+system time e 1 may-uncaught exceptions from top-level functions among 1 exns(1x), 1 raise exprs(1r), and 10 handlers(10h).

f ≤ 10 milli-seconds

Fig. 6. Experimental Results

– Lam’s last case must test for type unifiability instead of type equality: (In this case, type(e) - for an expression e of a program - indicates the SML type of the expression, determined during the program’s let-polymorphic type inference[Mil78, MTH90].)

Lam(decon e) = ⋃{Lam(e′) | exn κ e′ in pgm ∧ type(e′) unifies with type(decon e)}
Lam(!e)  = ⋃{Lam(e′) | := e′, ref e′ in pgm ∧ type(e′) unifies with type(!e)}
Lam(#k e) = ⋃{Lam(e_{k}) | (e_{1}, ⋯, e_{n}) in pgm ∧ type(e_{k}) unifies with type(#k e)}

4 Experimental Results

A prototype’s preliminary performance is shown in Figure 6.

Currently, the analysis speed ranges from 60 to 2160 SML-lines/sec. ([Yi94] ran at 0.2 SML-lines/sec and [FA96] at about 10 SML-lines/sec). We expect still a considerable improvement in the analysis speed as we better implement the control flow analysis part. In particular, a performance bottleneck is in computing the table that partitions user functions into unifiable ones. This process’ cost is proportional to the “size” of function types in the program. This is why the control flow analysis speed is not proportional to the program size.

Computing the Lam uses the fixpoint iteration of cubic complexity. We currently investigate a way for adapting Heintze’s technique [HM97] of quadruple complexity. For this adaptation we must re-formulate his approach for languages where exceptions and functions are intertwined. Computing the constraints’ least solution also uses the conventional fixpoint iteration^{8} of cubic complexity.

The analysis accuracy is satisfying. We manually checked the above test programs and found that the reported exceptions for Knuth-Bendix.sml, pathname.sml, stringcvt.sml, and compiler.sml can actually be uncaught. For ml-lex.sml, we find that 3 among the 4 may-uncaught exceptions can actually escape.

8 The iterative method is possible because the set domain is finite (the set of exception names in the input program) and all set operators (set union “∪”, “X_{f} ∩ {κ}”, “X_{f} \ {κ_{1} ⋯ κ_{n}}”, etc.) are monotonic.

To our knowledge, the cost-accuracy performance of Guzmán and Suárez [GS94]’s exception type system is not available to compare with ours.

5 Handling of Exception’s Arguments

Because our analysis does not recognize exception’s arguments unless the arguments were also exceptions, the analysis leads into a too conservative result for some programs.

Example 2. Consider the following program that has no uncaught exception:

          exception Fail of int
          fun f() = g() handle Fail(1) => 1
          fun g() = raise (exn Fail 1)

Because the handler pattern “Fail(1)” is not exhaustive for the argument part, the handler is annotated with “+raise x Fail” expression and our analysis conclude that f has an escaping exception Fail.

Resolving this problem by adding constraints for non-exception values and risking the subsequent increase of the analysis cost is not appealing in two reasons. Incomplete handler patterns for exception’s argument (like the above example) is rare, and the existing pattern compiler already can warn of incomplete patterns for exception’s arguments unless the argument type is an exception.

Our proposal is to make ⊳_{3} bring extra data by which the programmer trim overly conservative results. We pair an exception name κ with the index of the expression (“exn κ e”) at which the exception value is made.^{9} Given a pair of exception name and its birth place information, the programmer can decide which may-uncaught exceptions are real, assuming that the birth place expression has the argument data explicit in the text. In the above example, the programmer safely decide the may-uncaught exception Fail is not real because its birth place is “(exn Fail 1)” hence the handler pattern “Fail(1)” is exhaustive enough.

This can be achieved by a slight change to ⊳_{3}. The exception space becomes the set of tuples: Exn = {κ_{1}, ⋯, κ_{N}} × Expr. The rule for exn expression becomes:

[EXN_{⊳_{3}} ] {f ⊳_{3} e_{1}: C_{1} \atop f ⊳_{3} exn κ e_{1}: \{X_{f} ⊇ ⟨κ, e⟩\} ∪ C_{1}} where e ≡ exn κ e_{1}

And X_{1} \_{e} {κ_{1}, ⋯, κ_{n}} and X_{1} ∩_{e} {κ} removes (respectively, selects) tuples headed by κ_{i}’s (respectively, by κ).

6 Conclusion

We safely and cost-effectively decoupled the exception flow and control flow analyses. For cases where exceptions carry functions (i.e., where control flow analysis needs exception analysis) our control flow analysis uses a crude approximation to assure its safety against the decoupling. Our early experimental evidence suggests that this

9 This can be understood as abstracting the expression values by the expression index. Similar technique is occasionally used in abstracting memory locations: every malloc expression is an abstract location, abstracting all the locations allocated at that point during execution. separation is not detrimental to the accuracy of the exception analysis, while it makes the analysis significantly faster than the earlier methods. We are optimistic that we are near to a right-balance of the cost-accuracy performance.

We showed the safety of our exception analysis (constraint system ⊳_{3}) in two steps, using two intermediate systems (⊳_{1} and ⊳_{2}). This safety proves were done by showing the consistencies between the three constraint systems. We used the fixpoint induction for continuous functions that were derived from the constraint rules [CC95] (Section A). Our method may be seen as a kind of abstract interpretation [CC77]. This paper’s technique for enlarging the constraint granularity and proving its consistency with smaller-grained constraint systems can be applied to other analysis problems where the data to analyze are sparse in programs.

We are currenlty implementing the idea of Section 5 and streamlining the control flow analysis part. Other than the analysis speed, for the analysis to be realistic, it must be able to analyze SML modules in isolation. We are working on our preliminary ideas.

Acknowledgment

We thank Dave MacQueen for his encouragement and keen interest in this work. We thank Nevin Heintze for sending us a draft of [HM97].

References

[AH95] Alex Aiken and Nevin Heintze. Constraint-based program analysis. POPL’95 Tutorial, January 1995.

[Ar996] Ariane 5: Flight 501 Failure. http://www.esrin.esa.it/htdocs/tidc/Press/ Press96/ariane5rep.html, July 1996.

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

[CC95] Patrick Cousot and Radhia Cousot. Compositional and inductive semantic definitions in fixpoint, equational, constraint, closure-condition, rule-based and game-theoretic form. In Lecture Notes in Computer Science, volume 939, pages 293–308. 1995.

[FA96] Manuel Fahndrich and Alexander Aiken. Making set-constraint program analyses scale. In Workshop on Set Constraints, August 1996.

[GS94] Juan Carlos Guzmán and Ascánder Suárez. A type system for exceptions. In Proceedings of the ACM SIGPLAN Workshop on ML and its Applications, June 1994.

[Hei92] Nevin Heintze. Set Based Program Analysis. PhD thesis, Carnegie Mellon University, October 1992.

[Hei93] Nevin Heintze. Set based analysis of ml programs. Technical Report CMU-CS-93-193, Carnegie Mellon University, July 1993.

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

[JW96] Suresh Jagannathan and Andrew Wright. Flow-directed inlining. In Proceedings of the SIGPLAN Conference on Programming Language Design and Implementation, pages 193–205, May 1996.

[Mil78] Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348–375, 1978.

[MTH90] Robin Milner, Mads Tofte, and Robert Haper. The Definition of Standard ML. MIT Press, 1990.

[PS92] Jens Palsberg and Michael I. Schwartzbach. Safety analysis versus type inference. Information and Computation, 1992.

[Shi91] Olin Shivers. Control-Flow Analysis of Higher-Order Languages. PhD thesis, Carnegie Mellon University, May 1991.

[Yi94] Kwangkeun Yi. Compile-time detection of uncaught exceptions for Standard ML programs. In Lecture Notes in Computer Science, volume 864, pages 238– 254. Proceedings of the first international static analysis symposium edition, 1994.

A Proof of Proposition 6 (Correctness of ⊳_{3})

Proof. We will prove that for any model I of C_{3}, the above holds.

Note that the least model I_{2} is equivalent to the ⊆-least fixpoint fixF_{2} [CC95]. The continuous function F_{2} is derived from C_{2} as follows:

Ψ  = {X_{i} | e_{i} ∈ e} ∪ {P_{i} | e_{i} ∈ e} the set of constraint variables for a program e
2^{Exn}  = the powerset of Exn, ordered by ⊆

F_{2}: (Ψ → 2^{Exn}) → (Ψ → 2^{Exn})

F_{2}(φ)(X_{i}) = \{ \begin{matrix}φ(P_{1})  if e_{i} = x(handle var) where “handle e_{1} λx_{τ} .e_{2}”∈ e \\ \{κ | “e_{1} e_{2}” ∈ e, λx_{τ} .e′ ∈ Lam(e_{1}), κ ∈ φ(X_{2})\} & if e_{i} = x(normal var) \\ \{κ\} ∪ φ(X_{1}) & if e_{i} = exn κ e_{1} \\ φ(X_{1}) & if e_{i} = decon e_{1} \\ \{κ | λx_{τ} .e′ ∈ Lam(e_{1}), κ ∈ φ(X_{e′})\} & if e_{i} = e_{1} e_{2} \\ φ(X_{2}) & if e_{i} = fix f λx_{τ} e_{1} in e_{2} \\ φ(X_{2}) ∪ φ(X_{3}) & if e_{i} = case e_{1} κ e_{2} e_{3} \\ φ(X_{2}) ∪ φ(X_{1}) & if e_{i} = handle e_{1} λx_{τ} .e_{2} \end{matrix}

Similarly for F_{2}(φ)(P_{i}).

We prove Q(fixF_{2}) by the fixpoint induction, where the assertion Q(φ) is: for a program e,

∀modelIof C_{3}.“f ⊳_{3} e_{i}: C”occursduring(main ⊳_{3} e: C_{3}) ⇒ I(X_{f}) ⊇ φ(X_{i})∧I(P_{f}) ⊇ φ(P_{i}).

Base case Q(∅) trivially holds. We claim that Q(F_{2}(φ)) holds given the induction hypothesis Q(φ). We consider only the X_{f} case for handle. Other cases are similarly done.

[HNDL] e ≡ f ⊳_{3} handle e_{g}λ_{h}x_{τ} .e_{2}.
I(X_{f}) ⊇ {κ | κ ∈ I(X_{h}), I(X_{h}) ⊇ I(P_{g})} ∪ I(X_{g}) (by [HNDL_{⊳_{3}} ])
= I(X_{h}) ∪ I(X_{g})  (because any model I of C_{3} satisfies I(X_{h}) ⊇ I(P_{g}))
⊇ φ(X_{2}) ∪ I(X_{g})  (because “h ⊳_{3} e_{2}” occurs and by I.H.)
⊇ φ(X_{2}) ∪ φ(X_{g})  (because “g ⊳_{3} e_{g}” occurs and by I.H.)
= F_{2}(φ)(X_{e})  (by difinition of F_{2}(φ)(X_{e}))

□ This article was processed using the L^{A}TEX macro package with LLNCS style