An Abstract Interpretation for Estimating Uncaught Exceptions in Standard ML Programs^{∗}

Kwangkeun Yi^{†}

              kwang@cs.kaist.ac.kr

Korea Advanced Institute of Science & Technology

Abstract

We present a static analysis that detects potential runtime exceptions that are raised and never handled inside Standard ML (SML) programs. This analysis enhances the software safety by predicting, prior to the program execution, the abnormal termination caused by unhandled exceptions.

The analysis is specified as a finite, abstract semantics of an intermediate language. The intermediate language, into which SML programs are translated before the analysis begins, is defined such that the mechanism of SML’s exception propagation becomes explicit in its text. This syntactic manipulation makes our analysis easy.

Our analysis prototype has been implemented by using an analyzer generator called Z1 and has been used to analyze SML programs consisting of thousand lines. Our analysis is limited to SML programs that are typecorrect and are operationally invariant even if the generative nature of SML’s data-type and exception declarations is not considered.

(To appear in Science of Computer Programming, North-Holland Publishing Co., Netherlands)

1 Introduction

Exception handling facilities in programming languages 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.

∗A preliminary version of this paper was presented in the 1st International Static Analysis Symposium (SAS’94) and appeared in Lecture Notes in Computer Science Vol. 864.

†This work was done while the author was associated with AT&T Bell Laboratories. Current address: Dept. of Computer Science, KAIST, Taejon, 305-701, South Korea.

Use of the exception facilities is not necessarily limited to deal with errors. The programmer can use exceptions as a “control diverter” to escape any control structure to a point where the corresponding exception is handled. Also, using the exceptions, the programmer can tailor an operation’s results or effects to particular purposes in a wider variety of contexts than would otherwise be the case.

The exception facilities, however, can provide a hole for program safety. A program can terminate abnormally when an exception is raised and never handled.

Our goal is to develop a compile-time tool for eliminating this safety hole. The tool will detect, prior to the program execution, potential runtime exceptions that may be astray. In this paper, we present one such tool for Standard ML (SML) [MTH90] programs.

1.1 Exception Mechanism in Standard ML

In SML, exceptions are treated just like any other value (until they are raised). They can be passed as function arguments, returned as the results of function applications, bound to identifiers, stored in locations and etc.

An exception consists of an exception name possibly paired with some argument values. For example,

                        Error("at line 7")

constructs the Error exception with the string argument. (In what follows, an exception name such as Error is called an “exception constructor.” ) The exception constructor Error must be declared beforehand:

                    exception Error of string

An exception is raised by

                             raise e

where the expression e must evaluate to an exception. For example, raise !x, where x is dereferenced for an exception value. A raised exception is particularly called an exception packet. In this paper, however, when the context is clear we will use exception, exception value, and exception packet interchangeably.

Once an exception is raised, a handler is located by dynamic means: by going up the current evaluation chain to find potential handlers. During this process, one or more levels of the currently active call chain are aborted, up to the function containing the handler.

In SML, the syntax for an exception handler is:

e handle p_{1} => e_{1} | ⋯ | p_{n} => e_{2}

Patterns p_{i}’s are compared with a raised exception from the computation of e. When the exception’s name (constructor) matches with pattern p_{k}, the corresponding expression e_{k} is evaluated. If the match fails, the raised exception continues to propagate back along the evaluation chain until it meets another handler, and so on.

1.2 Analysis Problems

Since SML exceptions are first-class objects, it is not straightforward from the program texts whether a handler and a raise expression are properly paired to handle all potential exceptions.

Consider the following program fragment:

                       f(x) = · · · raise x · · ·

In order to find which exceptions are raised inside f, we must determine which exceptions are bound to x. We must also analyze which handlers are provided for expressions that call f, in order to deactivate exceptions that can be handled. For another example that has a higher-order function, consider:

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

We must analyze which procedures are bound to g in order to determine which exceptions g(x) can raise. As in the previous case, we must also analyze which handlers are provided for expressions that call f, in order to deactivate exceptions that may escape from the handler inside f.

Lastly, we must take the exception arguments into account. This is in order to catch, for example, the escaping exception Error[1]^{1} in

           (· · · raise Error[1] · · ·) handle Error nil => 1

1.2.1 Caveat

One subtlety of the SML’s exception declaration is that it is generative. (This is also true for the datatype declarations.) Each evaluation of an exception declaration binds a new, unique name to the exception constructor. An exception handler looks up this internal name to determine a match. For example, in the following incorrect definition of the factorial function, each recursive call to fact generates a new instance of exception ZERO (line (1)). Therefore, the handler in line (3), which can only handle exceptions declared in its lexical scope, cannot handle another instance of ZERO that is newly declared and raised inside the recursive call fact(n-1). Hence this fact function fails with an uncaught exception ZERO.

           fun fact(n) =

1[1] is the singleton list of 1.

               let exception ZERO                       (1)
               in if n <= 0 then raise ZERO             (2)
                  else n * fact(n-1) handle ZERO => 1   (3)
               end

Our analysis cannot analyze programs that utilize such generative nature of the exception (and the datatype) declarations. This limitation is not severe; exceptions (and datatypes) are largely declared at the global scope or at the structure^{2} 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.

Another limitation of our analysis is that we consider only exceptions that appear in the program’s text (including library sources). Thus, hidden exceptions from primitive functions^{3} are not considered. For example, for an integer division expression “e_{1} div e_{2}” we do not report the possibly-uncaught exception Div, which is raised when the value of e_{2} is zero. This limitation can easily be lifted if our analysis is equipped with a table of primitive operators and their exceptions.

1.3 Analysis Examples

Consider a program where a handler is not complete enough to handle all cases.

         exception NEGA and ZERO
         fun f(x) = if x<0 then raise NEGA
                    else if x=0 then raise ZERO
                    else x
         fun g h x = h(x) handle NEGA => x             (1)
         fun main(x) = g f x

The handler inside g (line (1)) cannot handle exception ZERO that may be raised inside f. Our analysis detects this.

Consider another program where a handler is complete but some exceptions can still escape.

          exception NEGA and ZERO
          fun f(x) = if x<0 then raise NEGA
                     else if x=0 then raise ZERO
                     else x
          fun g h x = h(x)                             (1)
                      handle NEGA => h(x+1)            (2)
                           | ZERO => h(1)              (3)
          fun main(x) = g f x

The handler inside g is complete enough to catch all exceptions from h(x) (line (1)). However, because of the repeated call to h (lines (2)) inside a handle branch, exceptions ZERO and NEGA can be raised again without being handled. Our analysis detects these uncaught exceptions.

2A structure in SML is a unit for modular programming; it may be said that an SML structure is analogous to a file in C programming.

3Functions of the SML/NJ’s base environment.

Lastly, consider the following example where exception constructor and its argument are passed as function parameters.^{4}

           exception ERROR of int list
           exception EXIT of int list
           fun f(n, x, y) =
                if n<0 then raise (x [n])          (1)
                else if n=0 then raise (y nil)     (2)
                else n
           fun g(m, x, y) =
                f(m, x, y)                         (3)
                handle ERROR [n] => g(n, y, x)     (4)
                     | EXIT nil => 0               (5)
           fun main(c) = g(c, ERROR, EXIT)

When g is first called inside main, a raised exception ERROR [n] or EXIT nil are handled by the handler inside g (line (4) and (5)). Meanwhile, when g is called recursively (line (4)), the two exception constructors are swapped. Hence, raised exceptions ERROR nil and EXIT [n], at this time, cannot be handled by the handler. Our analysis detects this situation.^{5}

1.4 Analysis Implementation

We use the collecting analyzer generator Z1 [YH93, Yi93] in specifying and implementing our analysis. The analysis specification is an abstract interpreter [CC77, CC92]. From this specification, Z1 generates an executable collecting analyzer. The collecting analysis computes, for each expression of the input program, a value that characterizes the run-time states that occur at that expression. The program state, in our case, contains a collection of uncaught exceptions. Details of our implementation by Z1 is discussed in Section 7.

After the analysis, the following information is conveyed to the programmer:

• Unhandled exceptions of top-level functions. The existence of such exceptions implies that the program can terminate abnormally.

• Raised exceptions at each handle expression. Using this information the programmer can check if the handler patterns are complete to cover all cases.

Our analyzer has been used to analyze some programs including SML/NJ libraries, ML-YACC, and ML-LEX. See Figure 1 for preliminary performance figures.

4Such cases are found in the source of SML/NJ 1.01 compiler’s environment module.

5Actually, these two exceptions are included in the analysis result; two other spurious exceptions ERROR [n] and EXIT nil are reported too. See Section 7.1.

program  statistics^{a}
ML-LEX  1.2K^{b}, 8x^{c}, 8h^{d}, 47r^{e}
ML-YACC 7.7K, 21x, 6h, 122r
OR-SML^{f} 1.8K, 21x, 14h, 65r
program  analysis cost result^{g}

 ML-LEX  53min^{h}/3.1Mb^{i} eof,Subscript,Match,error,lex error
 ML-YACC 617min/26.5Mb Subscript,Semantic,MkTable
 OR-SML  28min/2.7Mb Badobject, Dontunify, Badtypeorunion

                             Iscrewedup,Badtypealpha,Badtypemap
                             Badtyperho,Cannotsort,Unknownnilset

aAfter the source is translated into the intermediate form.

bNumber of SML source lines

cNumber of exception constructors dNumber of handle expressions eNumber of raise expressions f Core of an DB query interpreter for disjunctive data gpossibly-uncaught exceptions hminutes on SGI Challenger imega bytes

Figure 1: Preliminary performance figures

1.5 Related Works

Guzmán and Suárez [GS94] reported an instrumented type-inference system to collect unhandled exceptions for a simplified core ML. Their system does not allow exceptions with arguments. In order to consider exception arguments, they may need an idea similar to the “regions” [TJ92] for approximating the set of argument values accompanying an exception.

On the other hand, such type-inference or, in general, constraints-resolution based program analysis [TJ92, TT94, LG88, JG91, Hei92, AW93] seems to have some appealing characteristics: relatively small analysis cost (because, for some problems and target languages, it is possible to use the unification [Rob65] process rather than the iterative fixpoint method) and a natural support for separate analysis (as reported in [TJ94]). It remains to have a comparative study of the two analysis methods (unification of instrumented type inference versus iterative approach based on abstract interpreter) for the instance of the exception analysis.

2 The Intermediate Language

Our analysis does not directly analyze the SML programs. We have an intermediate language into which the SML programs are translated before the analysis begins. Figure 2 shows this intermediate language. expression

e ::= x  variable
|  (fn x e)  function
|  (apply e e)  application
|  (con κ e^{0})  datatype value
|  (exn κ e^{0})  exception value
|  (decon e)  datatype deconstruction
|  (case x of {p e}^{+}) switch expression
|  (fix f x e in e)  recursive function binding
|  (raise e)  exception raise
|  (handle e x e)  exception handler

pattern

p ::= κ  constructor name
|  wild-card

{} for grouping, •^{+} for one or more •’s, and •^{0} if • is optional.

Figure 2: (Simplified) Abstract Syntax of the Intermediate Language

In this paper we present a simplified version of the language. We do not show numbers, strings, records, primitive arithmetic operators, and memory operators (like allocation, assignment and dereference). In our implementation though, all these omitted features are supported.

The intermediate language is an applicative higher-order language (based on Lambda [App92] of the SML New Jersey (SML/NJ) compiler). An informal semantics of the language is as follows. (Formal semantics is presented in Section 4.) A datatype value (con κ e) or an exception value (exn κ e) is constructed from a constructor name κ and an expression e for its argument value. The argument of a datatype or of an exception is recovered by the deconstruction expression (decon e). That is, (decon (con κ e)) is equal to e. The case expression (case x of p_{1} e_{1} ⋯) branches to e_{i} when the value of x has a constructor name that matches with p_{i}. For example, (case x of A 1 _2) is 1 if x is a value (con A e) or (exn A e). The wild-card pattern _matches with every name. The handle expression (handle e_{1} x e_{2}), where e_{2} will typically be a case expression, evaluates e_{1} first. If e_{1}’s result is a raised exception \underline{v}, the exception value v, not the exception packet \underline{v}, is bound to x inside e_{2}. Otherwise, e_{1}’s value is returned. Expression (fix f x e_{1} in e_{2}) binds the recursive function f = λx.e_{1} inside e_{2}.

2.1 Translation

The translation of the SML programs into their intermediate forms does the following noteworthy things. (Note that, in this section, some examples in the intermediate forms are not legitimate according to the abstract syntax of Figure 2. For convenience, we use numbers, for example.)

• The handler patterns are always augmented with an extra raise expression, in order to re-raise exceptions that are not caught:

         e handle ; ERROR => 1 ; | FAIL => 2   ⟹^{translate} (handle e x ; (case x ; of ERROR 1 ; FAIL  2 ; (raise x)))

Note that the “x” has the exception value that was raised inside e. Hence the raise expression “(raise x)” in the last branch has the effect of propagating the exception packets that cannot be handled by the current handler.

A translation example for a handler of an argument-carrying exception is:

exception E of int list

⋯

e handle E nil => 1

⟹^{translate}

                                     (handle e x
                                       (case x
                                         of E (apply
                                                (fn y
                                                 (case y
                                                   of NIL 1
                                                         (raise x)))
                                                (decon x))
                                              (raise x)
                                       ))

Note that (decon x) considers the arguments of exceptions bound to x.

• When patterns in an SML source are not complete enough to cover all cases, the translation makes this situation manifest in the intermediate form. For example,

   datatype t = A | B | C
   case x
     of A => 1
      | B => 2

⟹^{translate}

                                     (case x
                                        of A 1
                                           B 2
                                            (raise (exn MATCH)))

Note that the incomplete patterns for a datatype can be statically detected. Our translation resorts to the SML/NJ compiler for this detection.

• Alpha conversion is done: every identifier for variable and function is made distinct.

• Functors in the SML module system are translated into ordinary functions. A functor’s argument and result are represented as records (as explained in [App92]). The record construct in our intermediate language is omitted for brevity in this paper.

• A datatype or exception constructor that requires an argument is translated into a function, which is β-reduced whenever appropriate. For example,

       datatype t = T of int

⋯ T, ⋯

⟹^{translate}

                                           · · · (fn x (con T x)), · · ·

• The input SML program is assumed to be type-correct. This condition is easily supported in our case because the program translation occurs after the program passes the type inference phase of the SML/NJ compiler.

3 Roadmap

We take the following steps to arrive at an abstract interpreter for the exception analysis. We start from a standard semantics of the language. This standard semantics is natural and simple, but it is difficult to create a finite semantics from it. Thus, we will tailor this standard semantics into one called concrete semantics that becomes easier to abstract (make finite). Finally, we abstract the concrete semantics, resulting in a finite, approximate interpreter that is suitable for the compile-time computation. We prove the correctness of our abstract interpreter against the concrete semantics.

4 Standard Semantics

The standard semantics is shown in Figure 3. Note that our semantics is not denotational in that the semantics of function application is not defined compositionally. Our semantics function

E: Expr → Env → Value = fixF

is defined to be the least fixpoint of the functional

F: (Expr → Env → Value) → (Expr → Env → Value).

Therefore an expression e’s semantics is not defined from the semantics of e’s subparts but is defined to be the image fixF[[e]] of the least fixpoint fixF of F.

Let us briefly review our notations. A_{⊥} is a lifted cpo^{6} : bottom (⊥) and incomparable elements of set A. For two cpos A and B, A + B is the coalesced Semantic domains

6Complete partial ordering. A partial-order set X is cpo iff X has a least element and every chain in X has a least upper bound in X.

σ ∈ Env = Id → Value environment
v ∈ Value  = Closure + Data + Exn + \underline{Exn} value
Closure = Expr_{⊥} × Env  closure
Data  = DataCon_{⊥} × Value  datatype value
Exn  = ExnCon_{⊥} × Value  exception
\underline{Exn}  = Exn  raised exception
e ∈ Expr  set of expressions
κ ∈ DataCon  set of datatype constructors
κ ∈ ExnCon  set of exception constructors
Id  set of variables

Semantic function E: Expr → Env → Value is the least fixpoint fixF of F: (Expr → Env → Value) → (Expr → Env → Value)

F E [[x]] σ  = σ(x)
F E [[(raise e)]] σ  = letx v = E[[e]] σ
in \underline{v}
F E [[(handle e_{1} x e_{2})]] σ  = let v_{1} = E[[e_{1}]] σ
in if v_{1} = \underline{v} ∈ \underline{Exn}
then E[[e_{2}]] σ[v/x]
else v_{1}

F E [[(case x of p_{1} e_{1} ⋯ p_{n} e_{n})]] σ = E[[e_{j}]] σ

(κ =^{match} p_{j} where ⟨κ, v⟩ = σ(x))

F E [[(apply e_{1} e_{2})]] σ  = letx ⟨(fn x e), σ′⟩ = E[[e_{1}]] σ
v = E[[e_{2}]] σ
in E[[e]] σ′[v/x]
F E [[(fn x e)]] σ  = ⟨(fn x e), σ⟩
F E [[(fix f x e_{1} in e_{2})]] σ = E[[e_{2}]] σ′

(σ′ = fixλν.σ[⟨(fn x e_{1}), ν⟩/f])

F E [[({con|exn} κ e)]] σ  = letx v = E[[e]] σ
in ⟨κ, v⟩
F E [[(decon e)]] σ  = letx ⟨κ, v⟩ = E[[e]] σ
in v

Figure 3: Standard Semantics for Exception Evaluation sum (⊥_{A} = ⊥_{B} = ⊥_{A+B}), A × B is the Cartesian product with the componentwise order, and A → B consists of strict, continuous functions with the pointwise order. For f ∈ X → Y, we write f[y/x] to represent the function that is identical to f, except at x, where its value is y.

The standard evaluation function E of an expression e returns a value of the expression for a given environment. An environment

σ ∈ Env = Id → Value

is a map (a continuous function) from variables Id to their values Value. Set Id consists of the names for functions, arguments and exception binders (x’s in the handle expression (handle e_{1} x e_{2})) A value v ∈ Value is either a closure Closure, a datatype value Data, an exception value Exn or an exception packet (a raised exception) \underline{Exn}:

v ∈ Value = Closure + Data + Exn + \underline{Exn}.

The closure is, as usual, a pair of the function text and the environment at the function definition:

Closure = Expr_{⊥} × Env.

The datatype value is a pair of a constructor name and its argument (similarly for the exception value):

Data = DataCon_{⊥} × Value
Exn = ExnCon_{⊥} × Value

An exception packet \underline{Exn} is the same as an exception value except that we mark it with the underline.

4.1 Expressing the SML Exception Convention

To express the exception convention, we use the “letx” notation

“letx v = []_{1} in []_{2}”

as a shorthand for

“let v = []_{1} in if v ∈ \underline{Exn} then v else []_{2}.”

That is, the evaluation of the “letx” bindings terminates with the first whose result is a raised exception. This raised exception becomes the result in conclusion of the “letx” expression. When no exception is raised, “letx” is the same as “let.” Note that in the semantics we do not use the “letx” for the handle expression, because a handler is the only way to stop the propagation of an exception.

5 Concrete Semantics

A semantics that is defined over recursively-defined domains is troublesome when we derive from it a finite, abstract interpreter.

The standard semantics of the previous section has infinite domains that are recursively defined. Consider the value domain Value:

Value = Closure + Data + ⋯
= (Expr_{⊥} × (Id → Value)) + (DataCon_{⊥} × Value) + ⋯

In this section, we will develop a new semantics (called concrete semantics) that uses no recursively-defined domains hence becomes easier to abstract than the standard semantics.

Our solution is to use the store^{7}: a map from locations to values, upon which some effects of the evaluation function are accumulated (i.e., the store is a part of both the input and the output of the evaluation function):

E: Expr → Env × Store → Value × Store

When a value v needs to be bound to a variable x, a new location ℓ is allocated in the store s ∈ Store

s ∈ Store = Loc → Value

and the value is written in that location s[v/ℓ]. The environment σ ∈ Env

σ ∈ Env = Id → Loc

then maps the identifier to the location σ[ℓ/x]. Thus, for example, the argument of a function is mapped to different locations, one for each invocation of the function. When variable x’s value is needed, x’s location e(x) is fetched from the current environment e and the store entry s(e(x)) of the location has the value of x.

By using the locations and the stores, the value domain can be defined nonrecursively. The domain for the closure is defined without the Value domain, because the environment component is now a map from identifiers to locations. The domains for the datatype and exception values has, for the argument component, the location Loc in place of the Value domain. That is, when a datatype value (a pair ∈ DataCon_{⊥} × Value in the standard semantics) is constructed, a new location is allocated in the current store to hold the argument value, and this new location (rather than the argument value itself) is paired with the constructor name.

The concrete semantics is shown in Fig. 4.

7Actually, in order to handle the allocation, assignment and dereference expressions that are included in the real intermediate language, we need the store domain anyway.

Semantic domains

s ∈ Store  = Loc → Value  store
σ ∈ Env  = Id → Loc  environment
v ∈ Value  = Closure + Data + Exn + \underline{Exn} value
Closure = Exp_{⊥} × Env  closure
Data  = DataCon_{⊥} × Loc  datatype value
Exn  = ExnCon_{⊥} × Loc  exception value
\underline{Exn}  = Exn  raised exception
Loc  = {ℓ | location ℓ}_{⊥}  location
e ∈ Expr  set of expressions
κ ∈ DataCon  set of datatype constructors
κ ∈ ExnCon  set of exception constructors
Id  set of variables

Semantic function E: Expr → Env × Store → Value × Store is the least fixpoint fixF of

F: (Expr → Env × Store → Value × Store) →

(Expr → Env × Store → Value × Store)

F E [[x]] ⟨σ, s_{0}⟩  = s_{0}(σ(x))
F E [[(raise e)]] ⟨σ, s_{0}⟩  = letx ⟨v, s_{1}⟩ = E[[e]] ⟨σ, s_{0}⟩
in ⟨\underline{v}, s_{1}⟩
F E [[(handle e_{1} x e_{2})]] ⟨σ, s_{0}⟩  = let ⟨v, s_{1}⟩ = E[[e_{1}]] ⟨σ, s_{0}⟩
in if v = \underline{v′} ∈ \underline{Exn} (new ℓ)

then E[[e_{2}]] ⟨σ[ℓ/x], s_{1}[v′/ℓ]⟩

else ⟨v, s_{1}⟩

F E [[(case x of p_{1} e_{1} ⋯ p_{n} e_{n})]] ⟨σ, s_{0}⟩ = E[[e_{j}]] ⟨σ, s_{0}⟩

(κ =^{match} p_{j} where ⟨κ, ℓ⟩ = s_{0}(σ(x)))

F E [[(apply e_{1} e_{2})]] ⟨σ, s_{0}⟩ = letx ⟨⟨(fn x e), σ′⟩, s_{1}⟩ = E[[e_{1}]] ⟨σ, s_{0}⟩

⟨v, s_{2}⟩ = E[[e_{2}]] ⟨σ, s_{1}⟩ in E[[e]] ⟨σ′[ℓ/x], s_{2}[v/ℓ]⟩ (new ℓ)

F E [[(fn x e)]] ⟨σ, s_{0}⟩  = ⟨⟨(fn x e), σ⟩, s_{0}⟩
F E [[(fix f x e_{1} in e_{2})]] ⟨σ, s_{0}⟩ = let σ′ = σ[ℓ/f] (new ℓ)

s′ = s_{0}[⟨(fn x e), σ′⟩/ℓ]

in E[[e_{2}]] ⟨σ′, s′⟩
F E [[({con|exn} κ e)]] ⟨σ, s_{0}⟩  = letx ⟨v, s_{1}⟩ = E[[e]] ⟨σ, s_{0}⟩
in ⟨⟨κ, ℓ⟩, s_{1}[v/ℓ]⟩ (new ℓ)
F E [[(decon e)]] ⟨σ, s_{0}⟩  = letx ⟨⟨κ, ℓ⟩, s_{1}⟩ = E[[e]] ⟨σ, s_{0}⟩
in ⟨s_{1}(ℓ), s_{1}⟩

Figure 4: Concrete Semantics for Exception Evaluation

6 Abstract Exception Evaluation

The abstraction of the concrete semantics is needed to make the resulting interpretation computable at compile-time. This abstraction consists of abstracting both the semantic domains and the interpreter function.

We makes the abstract domains be finite lattices^{8}. Each element x̂ ∈ D̂ in an abstract domain D̂ denotes an ideal^{9} γ(x̂) ⊆ D of concrete values. The partial order x̂ ⊑ ŷ in the abstract domain is when x̂’s information is more precise than that of ŷ, i.e., when γ(x̂) ⊆ γ(ŷ). The lattice structure ensures the existence of a safe element x̂ ⊔ ŷ whose information γ(x̂ ⊔ ŷ) is consistent with the others γ(x̂) and γ(ŷ).

The abstract evaluation function must be monotonic and be a upper approximate of its concrete correspondence. A function f̂: Â → B̂ is a upper approximation of its concrete counterpart f: A → B when the abstract result f̂(x̂) over x̂ must include the concrete result f(x) for every x meant by x̂. The monotonicity requires that f̂’s results for consistent inputs be consistent.

Both the finiteness of the abstract domains and the monotonicity of the abstract evaluation guarantee the termination of the induced program analysis. The upper approximate-ness is necessary for the soundness.

6.1 Abstracting Locations

In abstract semantics, we use a single location for each allocation site of the source program. Note that new locations are allocated at four places. When a function is defined (inside the fix expression), a new location for the function name is allocated to hold the closure. When a function is applied, a new location to hold its argument. When a handler is applied, a new location to hold, if any, exception value. Lastly, when a datatype or exception value is created, a new location to hold its argument.

We uniquely name the allocation sites of a program, and use these names for abstract locations. Let Ln be the set of unique names for the allocation sites. An abstract location ι ∈ Ln represents the set Allocated(ι) of all concrete locations that are allocated at site ι during the execution of the program. Formally, the abstract location L̂ and its abstraction map α_{L}: Loc → L̂ are:

L̂ = Ln_{⊥}
α_{L} = λℓ.if ℓ = ⊥ then ⊥ else ι such that ℓ ∈ Allocated(ι).

Generally, that a single abstract location ℓ represents multiple, concrete locations can deteriorate the analysis accuracy. This is because storing a value

8In general, abstract domains need not be finite. Even for infinite lattices, if their every chain is bounded we can have terminating abstract interpretation[CC77, Bou93, Bou92] by means of applying “widening” operators at flow cycles. However, in Z1 we cannot specify such operators that are selectively applied only to some flow points.

9An ideal I of a cpo D is a subset of D that is downwardly closed (x ⊑ y ∈ I implies x ∈ I)

and upwardly complete (every chain in I has the least upper bound inside I).

α_{L} : Loc → L̂  = λℓ.if ℓ = ⊥ then ⊥ else ι where ℓ ∈ Allocated(ι)
α_{C} : Closure → Ĉ = λc.if c = ⊥ then {} else {e} where c = ⟨e, σ⟩
α_{D} : Data → D̂  = λd.if d = ⊥ then {}
else {⟨κ, ι⟩|d = ⟨κ, ℓ⟩ ∧ ℓ ∈ Allocated(ι)}
α_{X} : Exn → X̂  = λx.if x = ⊥ then {}
else {⟨κ, ι⟩|x = ⟨κ, ℓ⟩ ∧ ℓ ∈ Allocated(ι)}
α\underline{X} : \underline{Exn} → \underline{X̂}  = α_{X}

α_{V} : Value → V̂ = λv. \{ \begin{matrix}if v = ⊥ then & ⟨⊥Ĉ, ⊥D̂, ⊥X̂, ⊥\underline{X̂}⟩ \\ else if v ∈ Closure then & ⟨α_{C}(v), ⊥D̂, ⊥X̂, ⊥\underline{X̂}⟩ \\ else if v ∈ Data then & ⟨⊥Ĉ, α_{D}(v), ⊥X̂, ⊥\underline{X̂}⟩ \\ else if v ∈ Exn then & ⟨⊥Ĉ, ⊥D̂, α_{X}(v), ⊥\underline{X̂}⟩ \\ else if v ∈ \underline{Exn} then & ⟨⊥Ĉ, ⊥D̂, ⊥X̂, α\underline{X}(v)⟩ \end{matrix}

α_{S} : Store → Ŝ  = λs.λℓ̂. ⨆_{α_{L}(ℓ)⊑ℓ̂}α_{V} (s(ℓ))

α_{E×S} : Env × Store → Ŝ = λ⟨e, s⟩.α_{S}(s)

α_{V ×S} : Value × Store → V̂ × Ŝ = λ⟨v, s⟩.⟨α_{V} (v), α_{S}(s)⟩

Figure 5: Abstraction functions for domains

to ℓ̂ must have the effect of raising the location’s value in its lattice; we cannot overwrite the existing value at the location.

This accuracy deterioration is not avoidable but can be reduced, to some extent. For example, instead of using a single abstract location for each allocation site, we can use multiple abstract locations each of which represents an exclusive subset of the locations allocated at that site. One technique is to use the “abstract procedure string” [Har89] that classifies the locations according to the procedural movements (calls and returns) that they experience after their births. Depending on the abstractions of locations, we can achieve the effects of various cost-accuracy balances (such as “call/single”, “dynamic/multiple” or “single/multiple” granularities [HDCM93]). We chose not to use these techniques because our exception analysis with our simple abstraction showed a satisfying accuracy.

Our abstraction of locations eliminates the use of the environment (a map from variables to locations) because only one abstract location is associated with each variable. The elimination of environments immediately entails an abstraction of closures. An abstract closure becomes a set of function definitions without the environment component.

The abstractions for other domains are straightforward. See Figure 5.

6.2 Abstract Evaluation

Abstract interpreter for the exception analysis is shown in Fig. 6. Notations: f[y//x] = f[f(x)⊔y/x]. x.D selects D component of x. x for ⟨⊥, ⋯, x, ⊥ ⋯⟩ in proper contexts. x : D casts x ∈ D′ into D (only when D and D′ are equivalent except for names). |v̂| is identical to v̂ except for |v̂|.\underline{X̂} = ⊥ (raised exception component). For abstract locations we use the program’s variable names (assuming that every variable is named uniquely). When an allocation site has no variable (such as the datatype and exception construction expressions), we choose a unique name for such sites.

Note that the abstract evaluation does not use the “letx” notation. That is, when an exception is raised during a subcomputation, the remaining evaluation is not aborted. Rather, the evaluation continues and its result, together with the exceptions raised during subcomputations, is collected in the value of the conclusion.

Consider the raise expression.

Ê[[(raise e)]] ŝ_{0} = let ⟨v̂_{1}, ŝ_{1}⟩ = Ê[[e]] ŝ_{0}
in ⟨v̂_{1}.\underline{X̂} ⊔ (v̂_{1}.X̂ : \underline{X̂}), ŝ_{1}⟩

We first evaluate the exception expression e. Any raised exception during this evaluation is collected in v̂_{1}.\underline{X̂}. By the current raise expression, the exception values v̂_{1}.X̂ are raised v̂_{1}.X̂ : \underline{X̂} and are collected (joined) with the already raised exceptions v̂_{1}.\underline{X̂}.

Consider the handle expression.

Ê[[(handle e_{1} x e_{2})]] ŝ_{0} = let ⟨v̂_{1}, ŝ_{1}⟩ = Ê[[e_{1}]] ŝ_{0}
⟨v̂_{2}, ŝ_{2}⟩ = Ê[[e_{2}]] ŝ_{1}[(v̂_{1}.\underline{X̂} : X̂)//x]
in ⟨|v̂_{1}| ⊔ v̂_{2}, ŝ_{1} ⊔ ŝ_{2}⟩

We first evaluate the expression e_{1}. The handler needs to handle, if any, raised exceptions v̂_{1}.\underline{X̂} inside e_{1}. With the store ŝ_{1}[(v̂_{1}.\underline{X̂} : X̂)//x] that holds the exceptions v̂_{1}.\underline{X̂} : X̂ at x. we evaluate the second expression e_{2}, which is usually a case expression. The value in conclusion is either the value v̂_{1} if expression e_{1} did not raise any exception or the value v̂_{2} after the handling if expression e_{1} raised some exceptions. These two possibilities are accommodated by the join operation |v̂_{1}| ⊔ v̂_{2}. We do not return the raised exceptions of v̂_{1} because they are considered inside the evaluation of e_{2}. (Hence |v̂_{1}|, not v̂_{1}, in |v̂_{1}| ⊔ v̂_{2}.) Note that if the handler patterns of e_{2} is not complete enough to handle all cases, the exceptions bound to x are re-raised,^{10} hence is captured inside v̂_{2}.

Consider the case expression.

Ê[[(case x of p_{1} e_{1} ⋯ p_{n} e_{n})]] ŝ_{0} =
⨆_{1≤i≤n}Ê[[e_{i}]] (ŝ_{0}[Screen(ŝ_{0}(x), {p_{i}}, {p_{1}, ⋯, p_{i−1}})//x])

10Note that when an SML source program is translated into the intermediate language, appropriate raise expressions are added for incomplete patterns – see discussions in Sect. 2.1.

Semantic domains

ŝ ∈ Ŝ  = L̂ → V̂  abstract store
ℓ̂ ∈ L̂  = Ln_{⊥}  abstract location
v̂ ∈ V̂  = Ĉ × D̂ × X̂ × \underline{X̂} abstract value
Ĉ  = 2^{Expr}  abstract closure
D̂  = 2^{DataCon×Ln}  abstract datatype value
X̂  = 2^{ExnCon×Ln}  abstract exception value
\underline{X̂}  = X̂  abstract raised exception
ι ∈ Ln  set of allocation sites
DataCon  set of datatype constructors
ExnCon  set of exception constructors
e ∈ Expr  set of expressions

Semantic function Ê: Expr → Ŝ → V̂ × Ŝ is the least fixpoint fixF̂ of

F̂: (Expr → Ŝ → V̂ × Ŝ) → (Expr → Ŝ → V̂ × Ŝ)

F̂ Ê [[x]] ŝ_{0}  = ⟨ŝ_{0}(x), ŝ_{0}⟩
F̂ Ê [[(raise e)]] ŝ_{0}  = let ⟨v̂_{1}, ŝ_{1}⟩ = Ê[[e]] ŝ_{0}
in ⟨v̂_{1}.\underline{X̂} ⊔ (v̂_{1}.X̂ : \underline{X̂}), ŝ_{1}⟩
F̂ Ê [[(handle e_{1} x e_{2})]] ŝ_{0} = let ⟨v̂_{1}, ŝ_{1}⟩ = Ê[[e_{1}]] ŝ_{0}

⟨v̂_{2}, ŝ_{2}⟩ = Ê[[e_{2}]] ŝ_{1}[(v̂_{1}.\underline{X̂} : X̂)//x]

in ⟨|v̂_{1}| ⊔ v̂_{2}, ŝ_{1} ⊔ ŝ_{2}⟩

F̂ Ê [[(case x of p_{1} e_{1} ⋯ p_{n} e_{n})]] ŝ_{0} =

⨆_{1≤i≤n}Ê[[e_{i}]] (ŝ_{0}[Screen(ŝ_{0}(x), {p_{i}}, {p_{1}, ⋯, p_{i−1}})//x])

F̂ Ê [[(apply e_{1} e_{2})]] ŝ_{0}  = let ⟨v̂_{1}, ŝ_{1}⟩ = Ê[[e_{1}]] ŝ_{0}
⟨v̂_{2}, ŝ_{2}⟩ = Ê[[e_{1}]] ŝ_{1}
in ⟨v̂_{1}.\underline{X̂} ⊔ v̂_{2}.\underline{X̂}, ŝ_{1} ⊔ ŝ_{2}⟩ ⊔
⨆_{1≤i≤n} Ê[[e′_{i}]] ŝ_{2}[|v̂_{2}|//x_{i}]

where v̂_{1}.Ĉ = {(fn x_{1} e′_{1}), ⋯, (fn x_{n} e′_{n})}

F̂ Ê [[(fn x e)]] ŝ_{0}  = ⟨{(fn x e)}, ŝ_{0}⟩
F̂ Ê [[(fix f x e in e′)]] ŝ_{0} = Ê[[e′]] ŝ_{0}[{(fn x e)}//f]
F̂ Ê [[({con|exn} κ e)]] ŝ_{0}  = let ⟨v̂_{1}, ŝ_{1}⟩ = Ê[[e]] ŝ_{0}
in ⟨{⟨κ, x_{e}⟩}, ŝ_{1}[v̂_{1}//x_{e}]⟩
F̂ Ê [[(decon e)]] ŝ_{0}  = let ⟨v̂_{1}, ŝ_{1}⟩ = Ê[[e]] ŝ_{0}
in ⟨⨆_{1≤i≤n}ŝ_{1}(ι_{i}), ŝ_{1}⟩

where v̂_{1}.D̂ ∪ v̂_{1}.X̂ = {⟨κ_{1}, ι_{1}⟩, ⋯ ⟨κ_{n}, ι_{n}⟩}

Figure 6: Abstract Semantics for Exception Analysis We evaluate every branch of the case expression and collect the results. Inside each branch e_{i}, the value of x will be appropriately trimmed (by the Screen operation) according to the case patterns {p_{1}, ⋯, p_{i−1}} that appear in the previous branches. The auxiliary operation

Screen(v̂, P, Q)

chooses among the data values v̂.D̂ and exceptions v̂.X̂ those that match with a pattern in P but not with any pattern in Q.

Screen: V̂ × 2^{Pattern} × 2^{Pattern} → V̂
Screen(v̂, P, Q) =
let screen = λ⟨x, P ⟩.{⟨κ, ι⟩ ∈ x|∃p ∈ P : κ =^{match} p}
in ⟨ ⊥Ĉ,
screen(v̂.D̂, P) − screen(v̂.D̂, Q),
screen(v̂.X̂, P) − screen(v̂.X̂, Q),
⊥\underline{X̂} ⟩

This auxiliary operation is used to sharpen our analysis as follows. When we analyze a program, we carry an approximate store whose entry is a collection of approximate values that a variable can have during execution. This collection always denotes a superset of actual values. The larger the collection, the less accurate the analysis becomes. In each branch of a case expression, blind use of this collection may result in overly conservative (hence very inaccurate) analysis.

For example, suppose that the current abstract store ŝ has two exceptions {E, F} for x below.

               (case x

E e_{1}

                       (raise x))

When we analyze the second branch (raise x) exception E should not be considered for x, because this exception matches with the first pattern. This trimming is achieved by the Screen operation:

Screen(ŝ(x), {_}, {E})

6.2.1 Accuracy Concern: An Implementation Details

Even with the Screen operation, the rule for the case expression has no effect on improving the analysis accuracy. This is because the Screen result does not replace the existing value of x in the store. Instead, the result is joined with the existing value of x (recall the notation: f[y//x] = f[y ⊔ f(x)/x]). We cannot overwrite the existing value because an abstract location x represents multiple concrete locations.

Therefore, even with the Screen operation the store value at x after

ŝ[Screen(⋯)//x]

remains unchanged.

This problem is simply solved by using different names for x inside each branch. Each trimmed value of x for each branch e_{i} is bound to a unique name, say x_{i}, instead of always to the same x. And every “x” inside each branch e_{i} is replaced by its unique name “x_{i}”. This replacement is straightforward because the source was already alpha-converted when translated from SML. For example,

     (case x
       of E (apply
              (fn y
               (case y
                 of NIL y
                       (raise x)))
              (decon x))
            (raise x)
     )

⟹^{becomes}

                                         (case x
                                           of E (apply
                                                  (fn y
                                                   (case y
                                                     of NIL y_{1}

                                                           (raise x_{1})))

                                                  (decon x_{1}))

                                                (raise x_{2})

                                         )

Let e′_{i} be the result of such replacement for i-th branch e_{i} in the case expression

(case x of p_{1} e_{1} ⋯ p_{n} e_{n})

Then the new abstract evaluation rule for case expression becomes

⨆_{1≤i≤n}Ê[[e′_{i}]] (ŝ_{0}[Screen(ŝ_{0}(x), {p_{i}}, {p_{1}, ⋯, p_{i−1}})//x_{i}]).

6.3 Correctness of the Abstract Semantics

Theorem 1 For a given program e, its abstract semantics fixF̂[[e]] can be computed in a finite time.

Proof. This fact immediately follows from that every operation used in the abstract semantics of Figure 6 is monotonic and all the abstract domains where the Expr is the set of expressions of the given program e are finite. □

Proving the soundness of the abstract semantics needs the following two lemmas.

Lemma 1 All abstraction functions (Figure 5) are strict and continuous.

Proof. The strictness of α_{L}, α_{C}, α_{D}, α_{X}, α\underline{X}, and α_{V} is obvious from their definitions. Store abstraction α_{S} is strict because α_{L} and α_{V} are strict. α_{E×S} and α_{V ×S} are strict because α_{S} and α_{V} are strict.

Similarly, it is trivial to see that every abstraction function is monotonic. Continuity immediately follows from that every chain of concrete domains is of finite length. □

Lemma 2 For every store s, value v, and location ℓ,

α(s[v/ℓ]) ⊑ α(s)[α(v)//α(ℓ)].

Proof. Recall the store abstraction:

α_{S} = λs.λℓ̂. ⨆_{α_{L}(ℓ)⊑ℓ̂}α_{V} (s(ℓ))

Thus,

α(s[v/ℓ])(α(ℓ)) = ⨆_{α(ℓ′)⊑α(ℓ)} α(s[v/ℓ](ℓ′))  by definition of α_{S}
⊑ α(v) ⊔ ⨆_{α(ℓ′)⊏α(ℓ)} α(s(ℓ′))
⊑ α(v) ⊔ ⨆_{α(ℓ′)⊑α(ℓ)} α(s(ℓ′)) by monotonicity of α
= α(v) ⊔ α(s)(α(ℓ))  by definition of α_{S}
= (α(s)[α(v)//α(ℓ)])(α(ℓ)) by definition of //

On the other hand, for ℓ′ ≠ ℓ,

α(s[v/ℓ])(α(ℓ′)) = ⨆_{α(ℓ′′)⊑α(ℓ′)} α(s[v/ℓ](ℓ′′))
= ⨆_{α(ℓ′′)⊑α(ℓ′)} α(s(ℓ′′))  because ℓ′ ≠ ℓ
= α(s)(α(ℓ′))
⊑ α(s)[α(v)//α(ℓ)](α(ℓ′)).

By the above two cases, α(s[v/ℓ]) ⊑ α(s)[α(v)//α(ℓ)]. □

The soundness of the abstract semantics fixF̂ (in Figure 6) with respect to the concrete semantics fixF (in Figure 4) is that for an arbitrary expression e and input x ∈ E × S the concrete evaluation result fixF[[e]] x must be implied by its abstract correspondence fixF̂[[e]] (α_{E×S}(x)):

Theorem 2 For any expression e

α_{V ×S} ∘ fixF[[e]] ⊑ fixF̂[[e]] ∘ α_{E×S}.

Proof. We can prove by Cousot’s inductive soundness proof method [CC92, Proposition 4.3]. However, a very similar yet simpler proof method is applicable: fixpoint induction [Sto77, page 213].

Let Q(f, g) be an assertion

Q(f, g) = ∀expression e : α_{Y} ∘ f[[e]] ⊑ g[[e]] ∘ α_{X}.

Base case: Q(⊥, ⊥) holds because all abstraction functions are strict (Lemma 1). Induction step: assuming that for continuous functions E and Ê, Q(E, Ê)

holds we will show Q(F(E), F̂(Ê)) holds. Then, by the fixpoint induction, the goal Q(fixF, fixF̂) holds.

We will present the proof of the induction step for the raise, handle, and case expressions. Proofs for other expressions can be done similarly. For abstract functions, we will simply write α without its type subscript; from the context, it is clear which domain abstraction α indicates. For easy reference, we juxtapose the concrete and abstract interpretation rules separated by ∥.

• (raise e):

\begin{matrix}letx & ⟨v, s_{1}⟩ = E e ⟨σ, s_{0}⟩ \\ in & ⟨\underline{v}, s_{1}⟩ \end{matrix} ∥ \begin{matrix}let & ⟨v̂_{1}, ŝ_{1}⟩ = Ê e ŝ_{0} \\ in & ⟨v̂_{1}.\underline{X̂} ⊔ (v̂_{1}.X̂ : \underline{X̂}), ŝ_{1}⟩ \end{matrix}

By the induction hypothesis (Q(E, Ê)), α(⟨v, s_{1}⟩) ⊑ ⟨v̂_{1}, ŝ_{1}⟩. Thus, the final abstract result

⟨v̂_{1}.\underline{X̂} ⊔ (v̂_{1}.X̂ : \underline{X̂}), ŝ_{1}⟩

is consistent with the two possibilities of the concrete evaluation because

– When v ∈ \underline{Exn}, α(⟨v, s_{1}⟩) ⊑ ⟨v̂_{1}.\underline{X̂}, ŝ_{1}⟩.

– When v ∈ Exn, α(⟨\underline{v}, s_{1}⟩) ⊑ ⟨v̂_{1}.X̂ : \underline{X̂}, ŝ_{1}⟩.

• (handle e_{1} x e_{2}):

\begin{matrix}let & ⟨v, s_{1}⟩ = E e_{1} ⟨σ, s_{0}⟩ \\ in & if v = \underline{v′} ∈ \underline{Exn} \\ & then E e_{2} ⟨σ[ℓ/x], s_{1}[v′/ℓ]⟩ \\ & (new ℓ) \\ & else ⟨v, s_{1}⟩ \end{matrix} ∥ \begin{matrix}let & ⟨v̂_{1}, ŝ_{1}⟩ = Ê e_{1} ŝ_{0} \\ & ⟨v̂_{2}, ŝ_{2}⟩ = Ê e_{2} ŝ_{1}[(v̂_{1}.\underline{X̂} : X̂)//x] \\ in & ⟨|v̂_{1}| ⊔ v̂_{2}, ŝ_{1} ⊔ ŝ_{2}⟩ \end{matrix}

By the induction hypothesis Q(E, Ê), α(⟨v, s_{1}⟩) ⊑ ⟨v̂_{1}, ŝ_{1}⟩.

– When v is not a raised exception, the concrete result ⟨v, s_{1}⟩ is subsumed by the abstract part ⟨|v̂_{1}|, ŝ_{1}⟩.

– On the other hand, when v = \underline{v′} ∈ \underline{Exn},

α(⟨σ[ℓ/x], s_{1}[v′/ℓ]⟩) ⊑ α(s_{1})[α(v′)//x] by Lemma 2
⊑ ŝ_{1}[α(v′)//x]  by monotonicity of ŝ_{1}
⊑ ŝ_{1}[(v̂_{1}.\underline{X̂} : X̂)//x] because α(v) ⊑ v̂_{1}

By Q(E, Ê) and by the monotonicity of Ê,

\begin{aligned}α(E e_{2} ⟨σ[ℓ/x], s_{1}[v′/ℓ]⟩) & ⊑ & Ê e_{2} α(⟨σ[ℓ/x], s_{1}[v′/ℓ]⟩) \\ & ⊑ & Ê e_{2} ŝ_{1}[(v̂_{1}.\underline{X̂} : X̂)//x] = ⟨v̂_{2}, ŝ_{2}⟩. \end{aligned}

• (case x of p_{1} e_{1} ⋯ p_{n} e_{n}):

\begin{matrix}E e_{j} ⟨σ, s_{0}⟩ \\ (κ =^{match} p_{j} where \\ ⟨κ, ℓ⟩ = s_{0}(σ(x))) \end{matrix}  ∥ ⨆_{1≤i≤n}Ê e_{i} (ŝ_{0}[Screen(ŝ_{0}(x), ⋯)//x])

By the induction hypothesis Q(E, Ê),

α(E e_{j} ⟨σ, s_{0}⟩) ⊑ Ê e_{j} ŝ_{0}
⊑ Ê e_{j} (ŝ_{0}[Screen(⋯)//x]) because ∀y : f ⊑ f[y//x]
⊑ ⨆_{1≤i≤n}Ê e_{i} (ŝ_{0}[Screen(⋯)//x])

• We will prove the case of Section 6.2.1 where we use distinct (subscripted) x_{i}’s in each case branch. For (case x of p_{1} e_{1} ⋯ p_{n} e_{n}), e′_{i} is equivalent to e_{i} except that every “x” inside e_{i} is replaced by “x_{i}.” Concrete semantics is: before a selected branch e_{j} is evaluated we allocate a new location for x_{j} and use this location inside e′_{j}.

\begin{matrix}E e′_{j} ⟨σ[ℓ′/x_{j}], s_{0}[v/ℓ′]⟩ \\ (new ℓ′, v as ⟨κ, ℓ⟩ = s_{0}(σ(x)), \\ and κ =^{match} p_{j}) \end{matrix} ∥ ⨆_{1≤i≤n}Ê e′_{i} (ŝ_{0}[Screen(ŝ_{0}(x), ⋯)//x_{i}])

Because α(s_{0}) = ŝ_{0},

α(s_{0}(σ(x)) =^{let} v) ⊑ ŝ_{0}(x) =^{let} v̂.

Furthermore, because v matches with p_{j},

α(v) ⊑ Screen(v̂, {p_{j}}, {p_{1}, ⋯, p_{j−1}}) (1)

Thus

α(s_{0}[v/ℓ′]) ⊑ ŝ_{0}[α(v)//α(ℓ′)]  by Lemma 2

By (1) and monotonicity of ŝ_{0}

⊑ ŝ_{0}[Screen(v̂, {p_{j}}, {p_{1}, ⋯, p_{j−1}}//x_{j}] (2)

By the induction hypothesis Q(E, Ê),

α(E e′_{j} ⟨σ[ℓ′/x_{j}], s_{0}[v/ℓ′]⟩) ⊑ Ê e′_{j} α(⟨σ[ℓ′/x_{j}], s_{0}[v/ℓ′]⟩)

By (2) and monotonicity of Ê

⊑ Ê e′_{j} (ŝ_{0}[Screen(⋯)//x_{j}])
⊑ ⨆_{1≤i≤n}Ê e′_{i} (ŝ_{0}[Screen(⋯)//x_{i}]).

□

7 Implementing the Analysis by Z1

Our analysis has been implemented by Z1 [YH93, Yi93].

The input to Z1 is a specification of the abstract interpreter of Figure 6. Neither the standard semantics nor the concrete semantics are processed by Z1. These non-abstract semantics are only necessary for us to derive a safe abstract interpreter.

An abstract interpreter specification in Z1 consists of three parts: lattice and set definitions (for abstract domains), auxiliary function definitions, and the main interpreter definition. The abstract domains (Ŝ, L̂, V̂, and etc.) of the exception analysis are exactly defined as lattices in Z1. For example,

    (lattice S (-> L V))  for Ŝ = L̂ → V̂
    (lattice L (flat Ln))  for L̂ = Ln_{⊥}
    (lattice V (* C D X R))  for V̂ = Ĉ × D̂ × X̂ × \underline{X̂}

⋯

    (set Ln (index numIds))  for Ln = {i ∈ Z|0 ≤ i ≤ numIds()}

defines the three abstract domains. Note that, in the definition of set Ln, numIds is a procedure that is implemented by us to return the number of allocation sites of an input program. Over these lattices and sets, the abstract interpreter F̂ is specified.

The output from Z1 is a C program that becomes an executable analyzer when linked with the target language ^{11} parser and syntax-tree interface procedures. This parser and the interface procedures must be implemented in C by us.

The specification of our abstract interpreter has 426 lines. Generated C code has 6965 lines. The executable size is 427 Kbytes.

The generated analyzer computes a collecting analysis of an input program. The collecting analyzer computes, for each program point of the input program, an abstract state that characterizes the run-time states that can occur at that point during execution. In Z1 a program state is a pair of the pre-state and the post-state, and the program points are the nodes of the program’s abstract syntax tree. As an example, for a function application expression “(apply e_{1} e_{2})” the pre-state at the program point (apply ⋯) is the program state immediately before the beginning of the application. The post-state is the state after the completion of the application.

Z1’s derivation of a collecting analysis from an abstract interpreter functional F̂ is straightforward. Note that an abstract interpreter is a function that defines, for each language construct, its evaluation rule: a state transformer from a prestate to a post-state. In our case, the abstract interpreter Ê has therefore the following type

11The target language is the language in which the programs to analyze are written. In our case, the intermediate language in Section 2.

Ê: Σ → Ŝ → V̂ × Ŝ

where Σ is the set of program points, and Ŝ (abstract store) is the lattice of prestates, V̂ ×Ŝ (pair of abstract value and store) is the lattice of post-states. This Ê function, which is usually recursively defined, is embedded in its associated functional F̂:

F̂ = λÊ.λe.λŝ_{0}. case e of
(raise e′): ⋯ Ê(e′, ŝ_{0}) ⋯
(handle e_{1} x e_{2}): ⋯ Ê(e_{1}, ŝ_{0}) ⋯
⋯

This abstract interpreter functional F̂, an input program P (actually, P ’s set of program points Σ_{P}), and the initial pre-state ŝ_{0} that is valid at the P ’s start point, are three inputs to the collecting analysis computation

Tabulate(F̂, Σ_{P} , ŝ_{0}). (see Figure 7)

The analysis results (two tables T_{X} and T_{Y}) have, for each program point p, a pre-state T_{X}(p) ∈ Ŝ and a post-state T_{Y} (p) ∈ V̂ × Ŝ that characterize run-time states that occur before and after that point during execution. The safeness of this collecting analysis algorithm is proven in [CHY95]. Note that the fixpoint algorithm is one that can be used only if the lattices are finite and the functions are monotonic. The monotonicity of F̂ in Figure 6 is straightforward to show.

Our collecting analyzer uses the same idea as minimal function graph [JM86] or collecting interpretation [HY88]. It iterates, given an initial state valid at the program’s start point, until all reachable states are computed for each program point. At each iteration, the algorithm computes, for each program point, a new state value reachable from the state values computed by the previous iteration. Note that our method is not the denotational approach [Bur87, BHA85, Nie82], where the table of the program’s semantic function is computed across the entire argument spaces.

Figure 7 presents a simplified version of our collecting analysis algorithm. In reality, Z1 uses a worklist algorithm that invokes F̂ only for a subset of program points whose T_{X} and T_{Y} entries were changed by the previous iteration. The fixpoint computation performance may vary, depending on the order in which elements are selected from the worklist. Z1 uses the heuristics in [CH93] for the selection order, which is guided by the structure of the dependence graph (an expression e_{1} depends on another expression e_{2} if the evaluation of e_{1} requires that of e_{2}) in order to approximate the optimal order of selecting an element from the worklist. (Similar fixpoint algorithms are reported in [CDMH93, Jør93]. Our algorithm may be seen as a mixture of the top-down and bottom-up fixpoint algorithms [CH92].) The reader may refer to [CHY95, CH93] for the complete algorithm and the proof of its correctness. eval(p: Σ, x: X): Y

begin

if x ⋢ T_{X}(p) then
T_{X}(p) = T_{X}(p) ⊔ x; /* join the pre-state */

       return T_{Y} (p);

end

Tabulate(F: (Σ → X → Y) → Σ → X → Y, Σ_{P}: 2^{Σ}, x_{0}: X): void T_{X}, T′_{X}: Σ_{P} → X; /* pgm point to pre-state */ T_{Y} , T′_{Y}: Σ_{P} → Y; /* pgm point to post-state */

begin

∀p ∈ Σ_{P} : T_{X}(p) = ⊥_{X}, T_{Y} (p) = ⊥_{Y};

T_{X}(p_{0}) = x_{0}; /* pre-state at the pgm’s entry point */

       repeat

⟨T′_{X}, T′_{Y} ⟩ = ⟨T_{X}, T_{Y} ⟩; /* remember the previous iteration */ foreach p ∈ Σ_{P} /* for each pgm point */

T_{Y} (p) = F (eval, p, T_{X}(p)); /* compute the post-state */

until (T_{X} ⊑ T′_{X}) ∧ (T_{Y} ⊑ T′_{Y}) /* repeat until stable */

end

In the exception analysis, F is F̂, eval is Ê, X is Ŝ, and Y is V̂ × Ŝ of the abstract semantics in Figure 6.

Figure 7: A primitive algorithm to compute collecting analysis from an abstract interpreter functional F

7.1 Analysis Snapshots

Some snapshots of our analysis of the last example in Section 1.3 are shown in the following table. For convenience, the program is shown here again:

           exception ERROR of int list
           exception EXIT of int list
           fun f(n, x, y) =
                if n<0 then raise (x [n])          (1)
                else if n=0 then raise (y nil)     (2)
                else n
           fun g(m, x, y) =
                f(m, x, y)                         (3)
                handle ERROR [n] => g(n, y, x)     (4)
                     | EXIT nil => 0               (5)
           fun main(c) = g(c, ERROR, EXIT)

The following table shows the raised exception and the store at the point right after the call f(m,x,y) at line (3). The column “non fixpoint” shows the case when f is initially called. It shows exception ⟨ERROR,ℓ⟩ and ⟨EXIT,ℓ′⟩ are raised, whose arguments (at locations ℓ and ℓ′) have constructors CONS^{12}and NIL, respectively. Location ℓ (respectively ℓ′) is the one allocated for “[n]” (resp. “nil”) in line (1) (resp. line (2)). After the multiple calls to f (by recursive call to g at line (4)), raised exceptions ERROR and EXIT have both CONS and NIL as their arguments. Among these exceptions, ⟨ERROR,ℓ′⟩ and ⟨EXIT,ℓ} escape the handler, which our analysis detects.

non fixpoint  fixpoint
v̂.\underline{X̂} \{⟨ERROR, ℓ⟩, ⟨EXIT, ℓ′⟩\} \{⟨ERROR, ℓ⟩, ⟨ERROR, ℓ′⟩, ⟨EXIT, ℓ⟩, ⟨EXIT, ℓ′⟩\}

  ŝ (x) {λx.(exn ERROR x)} {λx.(exn ERROR x), λx.(exn EXIT x)}
  ŝ (y) {λx.(exn EXIT x)}  {λx.(exn ERROR x), λx.(exn EXIT x)}

ŝ (ℓ) {⟨CONS,−⟩}  {⟨CONS,−⟩}
ŝ (ℓ′) {⟨NIL,⊥⟩}  {⟨NIL,⊥⟩}

8 Discussion

8.1 Semantic Sparse Analysis

We need a sparse analysis technique for reducing our analysis cost. It seems wasteful to trace all expressions of the input program, because only a small subset of the expressions may generate the exception behavior (creating, raising and handling). In conventional data flow analysis framework, many techniques [DRZ92, CCF91, CFR^{+}89, DGS94] have been developed. However, these methods are problematic for “higher-order” languages like SML, because the SML program’s flow graph, which is a prerequisite of the conventional methods, is not available prior to the analysis.

12List constructor name.

We will informally outline a semantics-based sparse analysis technique for the exception analysis. We will discuss at the level of the concrete semantics. Deriving an abstract correspondence will be straightforward. This sparse analysis technique is not implemented for our analysis. A similar idea was discussed in [Har89] for interprocedural dependence analysis of Scheme programs.

Proposition 1 Before we evaluate an expression, we can conservatively decide whether the evaluation will have the exception behavior or not, by examining the expression text with respect to the current environment and the store.

Before we evaluate an expression e

E e ⟨σ, s⟩

we can collect all values that might be used during this evaluation. These values consist of those that are “reachable” from the free variables FV (e) of e. This reachable set R is constructed as follows. First, it is initialized with the values {s(σ(x))|x ∈ FV (e)} of the free variables of e. For each closure value ⟨e′, σ′⟩ in R, we add to R the values {s(σ′(x′))|x′ ∈ FV (e′)} of the closure’s free variables, and so on. The final, transitively closed set R will contain the reachable values during the evaluation of e. This process of constructing the R set is analogous to the mark phase of the garbage collection. The root set of our case is the free variables of the expression e.

Conservative conditions under which the evaluation “E e ⟨σ, s⟩” may cause exception behavior are as follows: (We consider, for simplicity, that the expression e is also included in R as a closure ⟨e, σ⟩.)

• When there exists a closure in R whose body has a raise, handle or exn expression.

• When there is an expression that receives a exception value, manipulates it and returns it, without raising, handling nor creating a new exception. That is, when there exists a closure in R whose type has the exception type or a polymorphic type. Note that the intermediate expression can have the type information imported from the type inference phase (of the SML/NJ compiler) for its SML source.

• When the current expression e occurs during the computation of an exception argument (like in “(exn E e)”). This is because our analysis must take the exception arguments into account during the handler matches.

When we evaluate an expression, we check the above conditions. If any one of the conditions holds, we evaluate the expression. Otherwise, we skip the evaluation. This method will reduce the analysis cost, assuming that the time spent computing R is less than the time spent evaluating unnecessarily many expressions.

The computation cost of R for every expression may offset the gain we expect. In this case, we may apply the sparse evaluation rule only for, say, the function applications.

8.2 Conclusion

We have presented a static analysis that detects exceptions that are raised and never handled inside Standard ML programs. This analysis improves software safety by predicting, before program execution, the abnormal termination caused by potentially unhandled exceptions.

The analysis is specified as a finite, abstract semantics of an intermediate language. From this semantics, an executable collecting analyzer is derived. This derivation is done by a tool called Z1 [YH93, Yi93]. The generated analyzer was used to analyze SML/NJ Libraries, ML-YACC and ML-LEX programs.

The intermediate language is defined such that the mechanism of SML’s exception propagation becomes explicit in its text. For example, every handler expression is augmented with a raise expression that will re-raise the exceptions that are not caught by the handler patterns.

Our analysis is limited to SML programs that are type-correct and are operationally invariant even if the generative nature of SML’s data-type and exception declarations is not considered.

Acknowledgment

I thank Lal George, Carl Gunter, Lorenz Huelsbergen, Dave MacQueen, John Reppy, Jon Riecke and Zhong Shao for discussions and helps during this work. In particular, my thanks to Dave for his support and encouragement. I thank Manuel Fahndrich for correcting some typos. Also, thanks to anonymous referees for their helpful comments.

References

[App92] Andrew W. Appel. Compiling with Continuations. Cambridge University Press, 1992.

[AW93] Alexander Aiken and Edward L. Wimmers. Type inclusion constraints and type inference. In Proceedings of Functional Programming Languages and Computer Architecture, pages 31–41, 1993.

[BHA85] G.L. Burn, C.L. Hankin, and S. Abramsky. The theory and practice of strictness analysis for higher order functions. Technical Report DoC 85/6, Imperial College, 1985.

[Bou92] François Bourdoncle. Abstract interpretation by dynamic partitioning. Journal of Functional Programming, 2(4):407–435, 1992. Also as a tech report: DEC Paris Research Lab, March, 1992.

[Bou93] François Bourdoncle. Efficient chaotic iteration strategies with widenings. In Lecture Notes in Computer Science, volume 735 of Proceedings of Formal Methods in Programming and Their Applications, pages 128–141. 1993.

[Bur87] Geoffrey L. Burn. Abstract Interpretation and the Parallel Evaluation of Functional Languages. PhD thesis, Department of Computing, Imperial College, University of London, March 1987.

[CC77] Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the 4th ACM Symposium on Principles of Programming Languages, 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.

[CCF91] Jong-Deok Choi, Ron Cytron, and Jeanne Ferrante. Automatic construction of sparse data flow evaluation graphs. In Proceedings of the Annual ACM Symposium on Principles of Programming Languages, pages 55–66, 1991.

[CDMH93] B. Le Charlier, O. Degimbe, L. Michel, and P. Van Hentenryck. Optimization techniques for general purpose fixpoint algorithms: practical efficiency for the abstract interpretation of prolog. In Lecture Notes in Computer Science, volume 724, pages 15–26. Springer-Verlag, proceedings of the third international workshop on static analysis edition, September 1993.

[CFR^{+}89] R. Cytron, J. Ferrante, B. Rosen, M. Wegman, and F. Zadeck. Efficiently computing static single assignment form and control dependence graph. In Proceedings of the Annual ACM Symposium on Principles of Programming Languages, 1989.

[CH92] Baudouin Le Charlier and Pascal Van Hentenryck. A universal top-down fixpoint algorithm. Technical Report CS-92-25, Brown University, May 1992.

[CH93] Liling Chen and Luddy Harrison. Efficient computation of fixpoints that arise in complex program analysis. Technical Report CSRD Report No. 1245, Center for Supercomputing R & D, University of Illinois at Urbana-Champaign, 1993.

[CHY95] Liling Chen, Luddy Harrison, and Kwangkeun Yi. Efficient computation of fixpoints that arise in complex program analysis. Journal of Programming Languages, 1995.

[DGS94] Evelyn Duesterwald, Rajiv Gupta, and Mary Lou Soffa. Reducing the cost of data flow analysis by congruence partitioning. In International Confererence on Compiler Construction, April 1994.

[DRZ92] D. Dhamdhere, B. Rosen, and F. Zadeck. How to analyze large programs efficiently and informatively. In Proceedings of the SIGPLAN Conference on Programming Language Design and Implementation, 1992.

[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.

[Har89] Williams L. Harrison III. The interprocedural analysis and automatic parallelization of scheme programs. Lisp and Symbolic Computation, 2(3/4):179–396, 1989.

[HDCM93] Pascal Van Hentenryck, Olivier Degimbe, Baudouin Le Charlier, and Laurent Michel. The impact of granularity in abstract interpretation of prolog. In Patrick Cousot, Moreno Falaschi, Gilberto File, and Antoine Rauzy, editors, Lecture Notes in Computer Science, volume 724. Springer-Verlag, proceedings of the third international workshop on static analysis edition, 1993.

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

[HY88] Paul Hudak and Jonathan Young. A collecting interpretation of expressions (without powerdomains). In Proceedings of the Annual ACM Symposium on Principles of Programming Languages, pages 107–118, 1988.

[JG91] Pierre Jouvelot and David K. Gifford. Algebraic reconstruction of types and effects. In Proceedings of the Annual ACM Symposium on Principles of Programming Languages, 1991.

[JM86] Neil D. Jones and Alan Mycroft. Data flow analysis of applicative programs using minimal function graphs: Abridged version. In Proceedings of the Annual ACM Symposium on Principles of Programming Languages, 1986.

[Jør93] N. Jørgensen. Chaotic fixpoint iteration guided by dynamic dependency. In Lecture Notes in Computer Science, volume 724, pages 27–44. Springer-Verlag, proceedings of the third international workshop on static analysis edition, September 1993.

[LG88] John M. Lucassen and David K. Gifford. Polymorphic effect systems. In Proceedings of the Annual ACM Symposium on Principles of Programming Languages, pages 47–57, 1988.

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

[Nie82] Flemming Nielson. A denotational framework for data flow analysis. Acta Informatica, 18, 1982.

[Rob65] J. A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1):23–41, 1965.

[Sto77] Joseph E. Stoy. Denotational Semantics: the Scott-Strachey Approach to Programming Language Theory. MIT Press, 1977.

[TJ92] Jean-Piere Talpin and Pierre Jouvelot. Polymorphic type, region and effect inference. Journal of Functional Programming, 2(3):245–271, July 1992.

[TJ94] Yan Mei Tang and Pierre Jouvelot. Separate abstract interpretation for controlflow analysis. In Lecture Notes in Computer Science, volume 789, pages 224–243. Springer-Verlag, proceedings of the theoretical aspect in computer science edition, 1994.

[TT94] Mads Tofte and Jean-Pierre Talpin. Implementation of the typed call-by-value λcalculus using a stack of regions. In Proceedings of the Annual ACM Symposium on Principles of Programming Languages, January 1994.

[YH93] Kwangkeun Yi and Williams Ludwell Harrison III. Automatic generation and management of interprocedural program analyses. In Proceedings of the Annual ACM Symposium on Principles of Programming Languages, pages 246–259 (also as CSRD Report No. 1260), January 1993.

[Yi93] Kwangkeun Yi. Automatic Generation and Management of Program Analyses. PhD thesis, University of Illinois at Urbana-Champaign, August 1993. Report UIUCDCS-R-93-1828.