ROPAS

Research On Program Analysis System

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

ROPAS MEMO 1999-3 April 19, 2000

Automatic Test Data Generation for Exceptions in First-Order ML Programs

Sukyoung Ryu and Kwangkeun Yi

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

Abstract

We present a static analysis to automatically generate test data that raise exceptions in the input programs. Using the test data from our analysis, the programmer can check whether the raised exceptions are correctly handled with respect to the program’s specification.

For a given program, starting from the initial constraint that a particular raise expression should be executed, our analysis derives necessary constraints for its input variable. The correctness of our analysis assures that any value that satisfies the derived constraints for the input variable will activate the designated raise expression.

In this paper, we formally present such an analysis for a first-order language with the ML-style exception handling constructs and algebraic data values, prove its correctness, and show a set of examples.

1 Introduction

Exception facilities in modern programming languages (e.g., ML[MTHM97], Modula-3[CDJ^{+}89], Java[GJS96], and Ada[HP83]) can be problematic in assuring the software quality. First, even for type-safe programming languages like ML, exceptions provide a hole for program safety. ML programs can abruptly halt when an exception is raised and never handled. Uncaught exceptions are sometimes disastrous [Ar996]. Second, even though there is no escaping exception from the program, the dynamic nature of abnormal situations makes it difficult to assure that every raised exception will be correctly handled.

There already exist practical tools [YR97, YRon, PL99, YR98, YC99] to the first problem but, as far as we know, the second problem of assuring exception’s correct handling is not yet addressed.

Our proposed solution to the second problem is a static analysis that automatically generates test data that will execute all the exception-raise expressions in the input program. By running the program with the generated test inputs, the programmer can execute all the exception-raise expressions in the program, monitor the flows of the raised exceptions and check whether the raised exceptions are to be correctly handled. The exception-raise expressions are the explicit raise-expressions in the input programs. Non-raise expressions (e.g. e_{1} + e_{2}) that can raise some primitive exceptions (e.g. Overflow) are outside of our test coverage.

For example, let us consider the following program of substituting e for a variable x in an input expression, written in ML^{1}:

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

1This example program is a core part of an instance of what Gérard Huet, in the mid-80’s, called “sharing transducers.”

e ::= 0  constant
| x  variable
| (λx.e_{1}) e_{2}  immediate function application
| (fix f λx.e_{1}) e_{2}  | f e  recursive function application
| κ e  | κ^{−1} e  data construction/deconstruction
| fst e  | snd e  projection
| (e_{1}, e_{2})  tuple
| case e_{1} κ e_{2} e_{3}  conditional branch
| raise E  exception raise
| handle e_{1} E e_{2}  exception handle

Figure 1: Abstract Syntax of L

     fun subst (VAR x') = if x = x' then e else raise Same
       | subst (LAM (x', b')) = if x = x' then raise Same
                                else LAM (x', subst b')
       | subst (APP (e1, e2)) = APP (subst e1, subst e2)

Our analysis generates test data as follows: (1) VAR x′ where x′ ≠ x which will execute the first raise expression, (2) LAM (x, e′) with e′ an arbitrary expression which will execute the second raise expression, or (3) APP (e_{1}, e_{2}) where e_{1} or e_{2} has (1) or (2) as its subexpression.

This paper is organized as follows. Section 2 defines the syntax and semantics of our source language. Section 3 presents our analysis and Section 4 proves the soundness of the analysis. Section 5 provides a set of explanatory examples. Section 6 discusses some issues and concludes.

2 Language L

The source language L is a call-by-value, first-order language with algebraic data values and a subset of the ML-style exception-handling constructs:

• Data values are algebraic: values are finitely constructed with a finite number of data constructors. For example, a natural number is constructed with either a constructor ZERO with a constant 0 as its argument or a constructor SUC with a natural number as its argument.

• Expressions’ values are first-order. Thus, functions can neither be passed to other functions, be stored in a location, nor be paired with exceptions. This limitation implies that for every call expression it is manifest from the program text which function to call.

• Exceptions do not have arguments. Exceptions are constructed with a 0-ary constructor, the exception name.

• Every raise expression has an exception name at its exception part, like “raise ERROR.”

Language L’s abstract syntax is shown in Figure 1. Note that every function application expression has the function immediate in the program text. For brevity, we have omitted strings, numbers, primitive operators, and memory operations (assignment, reference, and dereference).

A datum value is constructed by “κ e” where κ is a data constructor name and expression e is for its argument value. The argument of datum is recovered by “κ^{−1} e”. A tuple value is constructed by “(e_{1}, e_{2})”. The first argument of a tuple is recovered by “fst e” and the second argument is recovered by “snd e”. Recursive function f is defined as “fix f λx.e”. 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}. Exception E is raised by “raise E”. The handle expression “handle e_{1} E e_{2}” evaluates e_{1} first. If e_{1}’s result is a normal value, the value is returned; if e_{1}’s result is a raised exception E, e_{2} is evaluated; otherwise, the raised exception is uncaught and propagated backward along the dynamic evaluation chain. Multiple exceptions can be handled by nested handle expressions. For example, handle (handle e_{1} E e_{2}) F e_{3} can handle two exceptions E and F.

For brevity, we have omitted the formal definition of the semantics. The semantics is defined in the natural semantics formalism [Kah88].

Throughout this paper,

• we assume that all variables are uniquely named (alpha-converted).

• we assume that no expression of a program is a dead code.

• by “L program” we mean an L expression with free (input) variables.

3 Analysis by Constraint Propagation

We shall now introduce a static analysis that generates test data to raise a designated exception from the input program. Our analysis is presented in the set-constraint framework [Hei92, AH95].

We construct a relation se ⊳ e : C for each expression e of the input program. Informally, se is the set of values where e’s value should be included, and C is the set of constraints that are necessary for e to evaluate into the values of se. Thus we can read “se ⊳ e : C” as “C is necessary for e to be included in se”. Syntax and semantics of the set expressions and constraints are shown in Figure 2.

An interpretation I is a mapping from set expressions se (respectively set constraints C) to sets of values or exception packets^{2} (respectively boolean values). An interpretation I is a model (a solution) of a conjunction C of constraints if, for each constraint X ⊆ se and a ⊆ X in C, I(se) and I(a) are defined and I(X) ⊆ I(se) and I(a) ⊆ I(X). We write gm(C) for the greatest model of C.

C is a set of set constraints. The collection of set constraints means the conjunction of the constraints. The meaning of se is a set of values or exception packets. For example, κ X indicates the values constructed with constructor κ and its argument values in X:

I(κ X) = {κ v | v ∈ I(X)}

and κ^{−1} X indicates the values deconstructed with κ from values in X:

I(κ^{−1} X) = {v | κ v ∈ I(X)}.

3.1 Constructing Set Constraints

We present the analysis rules in Figure 3 and Figure 4.

2A raised exception is particularly called an exception packet.

April 19, 2000  ROPAS-1999-3  4
v ∈ Val  = {0} + FtnExpr + Data + Val × Val  values
λx.e ∈ FtnExpr  function expressions in a program
κ v ∈ Data = Con × Val data
κ, κ′ ∈ Con  data constructors in a program
E, E′ ∈ Exn  exception constructors in a program
Ê, Ê′ ∈ Packet  exception packets
C ::= {true}

     | {false}

| {X ⊆ se}
| {a ⊆ X }
| C_{1} ∪ C_{2}
a ::= 0
| λx.e
| κ a
| (a_{1}, a_{2})

se ::= X  set variable
| κ X  constructed set with κ
| κ^{−1} X  deconstructed set with κ
| κ̄ X  constructed set with non κ
| (se, X) set of tuples
| (X , se) set of tuples
| (X , Y)  set of tuples
| a  atomic set
| Ê  exception packet
I(C)  ∈ {true, false}
I({true}) = true
I({false}) = false
I({X ⊆ se}) = I(X) ⊆ I(se)
I({a ⊆ X }) = I(a) ⊆ I(X)
I(C_{1} ∪ C_{2})  = I(C_{1}) ∧ I(C_{2})
I(a)  ⊆ Val
I(0)  = {0}
I(λx.e)  = {λx.e}
I(κ a)  = {κ v | v ∈ I(a)}

I(se)  ⊆ Val + Packet
I(X)  ⊆ Val
I(κ X)  = {κ v | v ∈ I(X)}
I(κ^{−1} X) = {v | κ v ∈ I(X)}
I(κ̄ X)  = {κ′ v | v ∈ I(X), κ′ ≠ κ}
I((se, X)) = {(v_{1}, v_{2}) | v_{1} ∈ I(se), v_{2} ∈ I(X)}
I((X , se)) = {(v_{1}, v_{2}) | v_{1} ∈ I(X), v_{2} ∈ I(se)}
I((X , Y)) = {(v_{1}, v_{2}) | v_{1} ∈ I(X), v_{2} ∈ I(Y)}
I(a)  ⊆ Val
I(Ê)  = {Ê}

I((a_{1}, a_{2})) = {(v_{1}, v_{2}) | v_{1} ∈ I(a_{1}), v_{2} ∈ I(a_{2})}

Figure 2: Set Constraints

Let’s consider the four rules for 0 in Figure 3. 0 is always included in the set {0}, hence:

       [C-1a]        0 ⊳ 0 : {true}.

In order for 0 to be in X, the necessary constraint is obviously {0 ⊆ X }:

       [C-2a]  X ⊳ 0 : {0 ⊆ X }.

In order for 0 to be included in κ^{−1} X, X has to include κ 0:

[C-3a]  κ^{−1} X ⊳ 0 : {κ 0 ⊆ X }.

There’s no way for 0 to be included in the other kinds of sets:

[C-4a]  se ⊳ 0 : {false} where se ∉ {0, X , κ^{−1} X }.

[C-1a]        0 ⊳ 0 : {true}
[C-2a]  X ⊳ 0 : {0 ⊆ X }

[C-3a]  κ^{−1} X ⊳ 0 : {κ 0 ⊆ X }
[C-4a]  se ⊳ 0 : {false}  se ∉ {0, X , κ^{−1} X }
[NVN-a]  se ⊳ x : {X ⊆ se}  se ∉ {Ê}

[NVX-a]       Ê ⊳ x : {false}
[RSN-a]  se ⊳ raise E : {false}  se ∉ {Ê}
[RSX-1a]      Ê ⊳ raise E : {true}
[RSX-2a]      Ê′ ⊳ raise E : {false}  E′ ≠ E

[CONN-1a]              \frac{κ^{−1} X ⊳ e : C}{X ⊳ κ e : C}  [CONN-2a]    \frac{X ⊳ e : C}{κ X ⊳ κ e : C}

[CONN-3a]                 \frac{κ^{−1} Y ⊳ e : C}{κ^{′−1} X ⊳ κ e : C ∪ \{Y ⊆ κ^{′−1} X \}} fresh Y

[CONN-4a]                          \frac{X ⊳ e : C}{\overline{κ′} X ⊳ κ e : C} κ′ ≠ κ

[CONN-5a]               \frac{a ⊳ e : C}{κ a ⊳ κ e : C}  [CONX-a]      \frac{Ê ⊳ e : C}{Ê ⊳ κ e : C}

[CONN-6a]  se ⊳ κ e : \{false\} se ∉ \{X , κ X , κ^{′−1} X , \overline{κ′} X (κ′ ≠ κ), κ a, Ê\}

[DCONN-1a]      \frac{κ se ⊳ e : C}{se ⊳ κ^{−1} e : C}  se ∈ \{X , a\}  [DCONX-a]    \frac{Ê ⊳ e : C}{Ê ⊳ κ^{−1} e : C}

[DCONN-2a]               \frac{κ Y ⊳ e : C}{se ⊳ κ^{−1} e : C ∪ \{Y ⊆ se\}} fresh Y, se ∉ \{X , a, Ê\}

[FSTN-a]          \frac{(se, X) ⊳ e : C}{se ⊳ fst e : C}  fresh X, ; se ∉ \{Ê\}  [FSTX-a]     \frac{Ê ⊳ e : C}{Ê ⊳ fst e : C}

[SNDN-a]          \frac{(X , se) ⊳ e : C}{se ⊳ snd e : C}  fresh X, ; se ∉ \{Ê\}  [SNDX-a]     \frac{Ê ⊳ e : C}{Ê ⊳ snd e : C}

[TUPN-1a]             \frac{Y ⊳ e_{1} : C_{1} Z ⊳ e_{2} : C_{2}}{X ⊳ (e_{1}, e_{2}) : C_{1} ∪ C_{2} ∪ \{X ⊆ (Y, Z)\}} fresh Y, Z

[TUPN-2a]           \frac{Y ⊳ e_{1} : C_{1} Z ⊳ e_{2} : C_{2}}{\begin{aligned}κ^{−1} X ⊳ (e_{1}, e_{2}) : C_{1} ∪ C_{2} & ∪\{X ⊆ κ W\} \\ & ∪\{W ⊆ (Y, Z)\} \end{aligned}}  fresh W, Y, Z

[TUPN-3a]  se ⊳ (e_{1}, e_{2}) : {false} se ∈ {κ X , κ̄ X }

Figure 3: Analysis Rules (Part I)

[TUPN-4a]     \frac{se ⊳ e_{1} : C_{1} X ⊳ e_{2} : C_{2}}{(se, X) ⊳ (e_{1}, e_{2}) : C_{1} ∪ C_{2}}  [TUPN-5a]    \frac{X ⊳ e_{1} : C_{1} se ⊳ e_{2} : C_{2}}{(X , se) ⊳ (e_{1}, e_{2}) : C_{1} ∪ C_{2}}

[TUPN-6a]     \frac{X ⊳ e_{1} : C_{1} Y ⊳ e_{2} : C_{2}}{(X , Y) ⊳ (e_{1}, e_{2}) : C_{1} ∪ C_{2}}  [TUPN-7a]    \frac{a_{1} ⊳ e_{1} : C_{1} a_{2} ⊳ e_{2} : C_{2}}{(a_{1}, a_{2}) ⊳ (e_{1}, e_{2}) : C_{1} ∪ C_{2}}

[TUPN-8a]  a ⊳ (e_{1}, e_{2}) : {false} a ∉ {(a_{1}, a_{2})}

[TUPX-1a]      \frac{Ê ⊳ e_{1} : C}{Ê ⊳ (e_{1}, e_{2}) : C}  [TUPX-2a]    \frac{X ⊳ e_{1} : C_{1} Ê ⊳ e_{2} : C_{2}}{Ê ⊳ (e_{1}, e_{2}) : C_{1} ∪ C_{2}}  fresh X

[APPX-1a]                             \frac{Ê ⊳ e_{2} : C}{Ê ⊳ (λx.e_{1}) e_{2} : C}

[APPX-2a]                    \frac{Ê ⊳ e_{2} : C}{Ê ⊳ (fix f λx.e_{1}) e_{2} : C ∪ \{F ⊆ λx.e_{1}\}}

[APPX-3a]                    \frac{Ê ⊳ e_{2} : C}{Ê ⊳ f e_{2} : C}  fix f λx.e_{1} in a program

[APP-1a]                     \frac{X_{n} ⊳ e_{2} : C_{1} se ⊳ [x_{n}/x]e_{1} : C_{2}}{se ⊳ (λx.e_{1}) e_{2} : C_{1} ∪ C_{2}}  fresh n

[APP-2a]               \frac{X_{n} ⊳ e_{2} : C_{1} se ⊳ [x_{n}/x]e_{1} : C_{2}}{se ⊳ (fix f λx.e_{1}) e_{2} : C_{1} ∪ C_{2} ∪ \{F ⊆ λx.e_{1}\}}  fresh n

[APP-3a]               \frac{X_{n} ⊳ e_{2} : C_{1} se ⊳ [x_{n}/x]e_{1} : C_{2}}{se ⊳ f e_{2} : C_{1} ∪ C_{2}}  fix f λx.e_{1} in a program, fresh n, Used_{f}() ≤ N

[CASEX-a]                          \frac{Ê ⊳ e_{1} : C}{Ê ⊳ case e_{1} κ e_{2} e_{3} : C}

[CASE-1a]                   \frac{κ X ⊳ e_{1} : C_{1}  se ⊳ e_{2} : C_{2}}{se ⊳ case e_{1} κ e_{2} e_{3} : C_{1} ∪ C_{2}}  fresh X

[CASE-2a]                   \frac{κ̄ X ⊳ e_{1} : C_{1}  se ⊳ e_{3} : C_{2}}{se ⊳ case e_{1} κ e_{2} e_{3} : C_{1} ∪ C_{2}}  fresh X

[HNDLN-a]                      \frac{se ⊳ e_{1} : C}{se ⊳ handle e_{1} E e_{2} : C}  se ∉ \{Ê\}

[HNDLX-a]                       \frac{Ê′ ⊳ e_{1} : C}{Ê′ ⊳ handle e_{1} E e_{2} : C}  E′ ≠ E

[HNDL-a]                         \frac{Ê ⊳ e_{1} : C_{1}  se ⊳ e_{2} : C_{2}}{se ⊳ handle e_{1} E e_{2} : C_{1} ∪ C_{2}}

Figure 4: Analysis Rules (Part II)

Rule [CONN-1a] dictates that because the value of κ e should be included in X the value of e should be included in κ^{−1} X:

[CONN-1a] \frac{κ^{−1} X ⊳ e : C}{X ⊳ κ e : C} .

   Rules [CONN-3a], [DCONN-2a], [TUPN-1a], and [TUPN-2a] in Figure 3 introduce new set

variables. For example, consider:

[CONN-3a] \frac{κ^{−1} Y ⊳ e : C}{κ^{′−1} X ⊳ κ e : C ∪ \{Y ⊆ κ^{′−1} X \}} fresh Y.

In order for κ e to be included in κ^{′−1} X, the value of e has to be included in κ^{−1}(κ^{′−1} X). Because our set expression syntax does not allow κ^{−1} in front of κ^{′−1} X, we replace κ^{′−1} X by a fresh variable Y and add a new constraint Y ⊆ κ^{′−1} X.

Unlike those rules in Figure 3, some rules in Figure 4 are alternatives, in the sense that for a given se and e, constraints C for se ⊳ e : C can vary.

Consider rules [CASEX-a], [CASE-1a], and [CASE-2a] in Figure 4. If a case expression raises an exception, there are three possibilities depending on where the exception is raised from: e_{1}, e_{2}, and e_{3}. Rule [CASEX-a] is for a raised exception from e_{1}:

[CASEX-a]                 \frac{Ê ⊳ e_{1} : C}{Ê ⊳ case e_{1} κ e_{2} e_{3} : C} .

It dictates that if C is necessary for e_{1} to raise the exception E, then C is necessary for the case expression case e_{1} κ e_{2} e_{3} to raise the exception. Rule [CASE-1a] is for a raised exception from e_{2}:

[CASE-1a]          \frac{κ X ⊳ e_{1} : C_{1}  Ê ⊳ e_{2} : C_{2}}{Ê ⊳ case e_{1} κ e_{2} e_{3} : C_{1} ∪ C_{2}}  fresh X .

if C_{1} is necessary for e_{1} to be in κ X for some X and C_{2} is necessary for e_{2} to raise the exception E, then C_{1} ∪ C_{2} is necessary for the case expression case e_{1} κ e_{2} e_{3} to raise the exception. And rule [CASE-2a] is for a raised exception from e_{3}:

[CASE-2a]          \frac{κ̄ X ⊳ e_{1} : C_{1}  Ê ⊳ e_{3} : C_{2}}{Ê ⊳ case e_{1} κ e_{2} e_{3} : C_{1} ∪ C_{2}}  fresh X .

It dictates that if C_{1} is necessary for e_{1} to be in κ̄ X for some X and C_{2} is necessary for e_{3} to raise the exception E, then C_{1} ∪ C_{2} is necessary for the case expression case e_{1} κ e_{2} e_{3} to raise the exception.

Rules [APPX-2a] and [APP-2a] in Figure 4 make a constraint for the function variable f. For example, consider:

[APP-2a]     \frac{X_{n} ⊳ e_{2} : C_{1}  se ⊳ [x_{n}/x]e_{1} : C_{2}}{se ⊳ (fix f λx.e_{1}) e_{2} : C_{1} ∪ C_{2} ∪ \{F ⊆ λx.e_{1}\}} fresh n.

The rule forces the value of F to be included in {λx.e_{1}}. These two rules are the only rules that make a constraint for each function variable, so every F represents a singleton set {λx.e_{1}}. In order to uniquely name all the variables in the derivation tree, we replace all occurrences of the argument variable x in the function body e_{1} by a fresh variable x_{n}: [x_{n}/x]e_{1}.

Rule [APP-3a] in Figure 4 for recursive calls cannot be used an indefinite number of times. The counter Used_{f}() for each recursive function f records the number of times that the rule for recursive calls is used. If the counter hits a finite, pre-fixed, limit N the rule cannot be applied. For example, consider:

[APP-3a]   \frac{X_{n} ⊳ e_{2} : C_{1} se ⊳ [x_{n}/x]e_{1} : C_{2}}{se ⊳ f e_{2} : C_{1} ∪ C_{2}}  fix f λx.e_{1} in a program, fresh n, Used_{f}() ≤ N .

That the side condition Used_{f}() ≤ N is imposed only for recursive call expressions (rule [APP-3a]) implies that we bound the number of recursive call tracings while we propagate the constraints. This arbitrary bound for recursive call may fail to generate some constraints that would otherwise allow non-empty test data. Notice that the fixed bound for recursive derivations will not violate the safety of our analysis because failing to find test data vacuously satisfies the soundness condition: every generated test datum will cause the program to execute the designated raise expression.

   Rules [FSTN-a], [SNDN-a], [TUPX-2a], [CASE-1a], and [CASE-2a] introduce new set vari-

ables in order to collect constraints for subexpressions. For example, consider:

[TUPX-2a]            \frac{X ⊳ e_{1} : C_{1} Ê ⊳ e_{2} : C_{2}}{Ê ⊳ (e_{1}, e_{2}) : C_{1} ∪ C_{2}} fresh X

If C_{1} is necessary for e_{1} to be in X for some X and C_{2} is necessary for e_{2} to raise the exception E, then C_{1} ∪ C_{2} is necessary for the tuple expression (e_{1}, e_{2}) to raise the exception E.

3.2 Solving Set Constraints

Several set-constraint solving algorithms[HJ90, HJ91, CP97, CP98] are reported for a number of subclasses of set constraints. Our set constraints are co-definite, as defined by Charatonik and Podelski [CP97, CP98], hence, whenever satisfiable, have the greatest solution.

Computing the constraints’ greatest solution uses the conventional fixpoint iteration. For a set of constraints C which is an analysis result of a given program, we initialize each set variable X in C to be the universe set. We get the constraints’ greatest solution gm(C) by repeatedly computing the values of set variables according to the set constraints in C.

4 Soundness

We prove that if we evaluate the program with the test data which is the C’s model of our analysis Ê ⊳ e : C (where C ≠ {false}), then the program raises the exception E. Let us start with some definitions.

Definition 1 ([[Ê ⊳ e : C ]]) For a program e, we write [[Ê ⊳ e : C ]] for the derivation tree of the analysis Ê ⊳ e : C.

Definition 2 ([[σ ⊢ e → o]]) For a program e, we write [[σ ⊢ e → o]] for the derivation tree of the evaluation σ ⊢ e → o.

We prove the soundness of our analysis by simulating the evaluation of the program under a fixed environment σ^{v} which is induced by a test data v from our analysis:

Definition 3 (σ^{v}) For a program e_{0} with a free variable x_{0}, let [x_{0} ↦ v] ⊢ e_{0} → o. We write σ^{v} for the environment satisfying the followings:

For every σ occurring in [[[x_{0} ↦ v] ⊢ e_{0} → o]],

(1) every [x ↦ v′] in σ is collected, and

(2) for each [f ↦ ⟨σ′, fix f λx.e⟩] in σ, [f ↦ ⟨σ^{v}, fix f λx.e⟩] is collected.

Fixed environment σ^{v} preserves the semantics of e_{0}:

Lemma 1 For a program e_{0} with a free variable x_{0}, let [x_{0} ↦ v] ⊢ e_{0} → o. Then, σ^{v} does not change during the evaluation [[σ^{v} ⊢ e_{0} → o]].

Proof. During the evaluation of a program, environments can change only in function applications. Because x_{0} is the only one free variable of e_{0} and [x_{0} ↦ v](x_{0}) = σ^{v}(x_{0}), [[[x_{0} ↦ v] ⊢ e_{0} → o]] and [[σ^{v} ⊢ e_{0} → o]]is identical modulo environments. Thus, for each σ ⊢ e → o′ in [[σ^{v} ⊢ e_{0} → o]], σ′ ⊢ e → o′ exists in [[[x_{0} ↦ v] ⊢ e_{0} → o]], dom(σ′) ⊆ dom(σ^{v}) by the definition of σ^{v}, and σ′(x) = σ^{v}(x) for every variable x ∈ dom(σ′). By using these facts, the proof shows that the changed environment in each function application is the same as σ^{v}. That is, we prove that all value bindings introduced in each function application are already included in σ^{v}. □

We will use two inductions for se ⊳ e : C occurring in [[Ê ⊳ e_{0} : C_{0} ]]: one on the evaluation order of se ⊳ e : C and the other on the number of relations se_{i} ⊳ e_{i} : C_{i} in [[Ê ⊳ e_{0} : C_{0} ]] that contribute to the set expression se. Since se of se ⊳ e : C is determined by se_{i} ⊳ e_{i} : C_{i} in the path from Ê ⊳ e_{0} : C_{0} to se ⊳ e : C in the analysis [[Ê ⊳ e_{0} : C_{0} ]], the number of relations that contribute to se is n of e_{0} ∼^{n} e:

Definition 4 (e_{0} ∼^{n} e) For a program e_{0}, let Ê ⊳ e_{0} : C_{0}. We write e_{0} ∼^{n} e for the path of length n from the root Ê ⊳ e_{0} : C_{0} to any node se ⊳ e : C in the analysis [[Ê ⊳ e_{0} : C_{0} ]].

(1) e_{0} ∼^{0} e_{0}  (2) \frac{e_{0} ∼^{n−1} e′  \frac{⋯ se ⊳ e : C ⋯}{se′ ⊳ e′ : C′} ∈ [[Ê ⊳ e_{0} : C_{0} ]]}{e_{0} ∼^{n} e}

For a program e_{0}, let σ ⊢ e_{0} → o. We similarly define e_{0} ∼^{n} e for the path of length n from the root σ ⊢ e_{0} → o to any node σ′ ⊢ e → o′ in the evaluation [[σ ⊢ e_{0} → o]].

Every relation se ⊳ e : C in [[Ê ⊳ e_{0} : C_{0} ]] is correct, i.e., “C is necessary for e’s value to be included in se”:

Lemma 2 For a program e_{0} with a free variable x_{0}, let Ê ⊳ e_{0} : C_{0}. Then, every relation se ⊳ e : C occurring in [[Ê ⊳ e_{0} : C_{0} ]] satisfies the followings:

For every v ∈ gm(C_{0})(X_{0}),

(1) σ^{v} ⊢ e → o′ exists in [[σ^{v} ⊢ e_{0} → o]], and (2) o′ ∈ gm(C_{0})(se).

Proof. We prove by induction on the evaluation order of se ⊳ e : C occurring in [[Ê ⊳ e_{0} : C_{0} ]]. The proof consists of two main parts.

(1) We have to show that σ^{v} ⊢ e → o′ exists in [[σ^{v} ⊢ e_{0} → o]]. Because se ⊳ e : C occurs in [[Ê ⊳ e_{0} : C_{0} ]], e_{0} ∼^{n} e exists in [[Ê ⊳ e_{0} : C_{0} ]]. By showing that the same e_{0} ∼^{n} e exists in [[σ^{v} ⊢ e_{0} → o]], we prove that σ^{v} ⊢ e → o′ exists in [[σ^{v} ⊢ e_{0} → o]]. The proof is done by induction on n of e_{0} ∼^{n} e.

(2) For se ⊳ e : C ∈ [[Ê ⊳ e_{0} : C_{0} ]], after showing that σ^{v} ⊢ e → o′ exists in [[σ^{v} ⊢ e_{0} → o]], we show that o′ ∈ gm(C_{0})(se). This proof is done for each case of se ⊳ e : C. □

Theorem 1 (Soundness) For a program e_{0} with a free variable x_{0}, let Ê ⊳ e_{0} : C_{0}. Then, for every v ∈ gm(C_{0})(X_{0}), [x_{0} ↦ v] ⊢ e_{0} → Ê holds.

Proof. By lemma 2, (1) σ^{v} ⊢ e_{0} → o exists in [[σ^{v} ⊢ e_{0} → o]] and (2) o ∈ {Ê}, thus σ^{v} ⊢ e_{0} → Ê holds. Because x_{0} is the only one free variable of e_{0} and [x_{0} ↦ v](x_{0}) = σ^{v}(x_{0}), the evaluation of e_{0} under [x_{0} ↦ v] makes the identical result to the result of the evaluation of e_{0} under σ^{v}. Thus, [x_{0} ↦ v] ⊢ e_{0} → Ê holds. □

5 Examples

We shall present some examples to show how the analysis works for a given program. We include datatype declarations to make explicit the data constructors available in a given example program. Throughout this section, we write U for the universe set.

5.1 Example 1

Because of alternative rules in Figure 4, there can be several derivation trees for a given expression. In this section, we shall present all the derivation trees for the following program. The program raises an exception E, when the input value x is constructed with A. Otherwise, the program returns its input value.

                        datatype t = A of t | B of t | C of 0
                        case x A (raise E) x

In order for a case expression to raise an exception E, we can apply [CASEX-a], [CASE-1a],

or [CASE-2a].

• A possible derivation:

                           \frac{Ê ⊳ x : \{false\}}{Ê ⊳ case x A (raise E) x : \{false\}}

This case is when we apply [CASEX-a]. There’s no way for x to be included in {Ê}, hence the constraint is obviously {false}.

• A possible derivation:

                    \frac{A Y ⊳ x : \{X ⊆ A Y\}  Ê ⊳ raise E : \{true\}}{Ê ⊳ case x A (raise E) x : \{X ⊆ A Y, true\}}

This case is when we apply [CASE-1a]. In order for x to be included in A Y, X has to be included in A Y. Because raise E always evaluates into Ê, the constraint is {true}. The final constraint is:

{X ⊆ A Y, true}

and, as we expected, its greatest solution is X = A U because a variable without constraints has the universe as its greatest model.

• A possible derivation:

                     \frac{Ā Y ⊳ x : \{X ⊆ Ā Y\}  Ê ⊳ x : \{false\}}{Ê ⊳ case x A (raise E) x : \{X ⊆ Ā Y, false\}}

This case is when we apply [CASE-2a]. In order for x to be included in Ā Y, X has to be included in Ā Y. Because x can’t raise any exception, the constraint is {false}.

5.2 Example 2

In the following program, the function f raises an exception E when the input is constructed with Zero, otherwise, calls itself with a decreased input.

We shall consider the derivation tree where the recursive call is traced only once. (We set the N in rule [APP-3a] to be one.)

                  datatype n = Zero of 0 | Suc of n

(fix f λx. \overbrace{case x Zero (raise E) (\underbrace{f (Suc^{−1} x)}_{e_{2}})}^{e_{1}}) y

By applying [APP-2a] and [NVN-a] to the program:

\frac{X_{1} ⊳ y : \{Y ⊆ X_{1}\}  Ê ⊳ [x_{1}/x]e_{1} : C_{1}}{Ê ⊳ (fix f λx. e_{1}) y : \{Y ⊆ X_{1}\} ∪ C_{1}} .

By applying [CASE-2a] and [NVN-a] to Ê ⊳ [x_{1}/x]e_{1} : C_{1}:

\frac{\overline{Zero} Z ⊳ x_{1} : \{X_{1} ⊆ \overline{Zero} Z\}  Ê ⊳ [x_{1}/x]e_{2} : C_{2}}{Ê ⊳ \underbrace{case x_{1} Zero (raise E) [x_{1}/x]e_{2}}_{[x_{1}/x]e_{1}} : C_{1} = \{X_{1} ⊆ \overline{Zero} Z\} ∪ C_{2}} ,

and by applying [APP-3a], [DCONN-1a], and [NVN-a] to Ê ⊳ [x_{1}/x]e_{2} : C_{2}:

\frac{\frac{Suc X_{2} ⊳ x_{1} : \{X_{1} ⊆ Suc X_{2}\}}{X_{2} ⊳ Suc^{−1} x_{1} : \{X_{1} ⊆ Suc X_{2}\}}  Ê ⊳ [x_{2}/x]e_{1} : C_{3}}{Ê ⊳ \underbrace{f (Suc^{−1} x_{1})}_{[x_{1}/x]e_{2}} : C_{2} = \{X_{1} ⊆ Suc X_{2}\} ∪ C_{3}} .

By applying [CASE-1a], [NVN-a], and [RSX-1a] to Ê ⊳ [x_{2}/x]e_{1} : C_{3}:

\frac{Zero W ⊳ x_{2} : \{X_{2} ⊆ Zero W\}  Ê ⊳ raise E : \{true\}}{Ê ⊳ \underbrace{case x_{2} Zero (raise E) [x_{2}/x]e_{2}}_{[x_{2}/x]e_{1}} : C_{3} = \{X_{2} ⊆ Zero W, true\}} .

Thus the constraint at the bottom of the derivation tree is:

\{Y ⊆ X_{1}, X_{1} ⊆ \overline{Zero} Z, X_{1} ⊆ Suc X_{2}, X_{2} ⊆ Zero W, true\},

and its greatest solution is:

Y = Suc (Zero U), X_{1} = Suc (Zero U), Z = U, X_{2} = Zero U, W = U.

When we evaluate the program with the test data Y = Suc (Zero U), the recursive call is done only once and the program raises an exception E.

6 Conclusion

For a call-by-value, first-order language with the ML-style exception mechanism, we have presented a test data generation to cover all the exception-raise expressions in the input program. Our test data derivation is defined as a set-constraint propagation. Given a syntax tree representing the program and the initial constraint that the program has a unique uncaught exception (which will be raised by a particular raise expression), our analysis backwardly propagates constraints towards the leaves of the tree, to yield constraints about the input variable.

Our constraint propagation maintains a necessary-condition for each sub-expression by tracing back a single execution flow of the program. If multiple execution flows can be traced, only one flow is taken at a time. Thus we can avoid approximate constraints (“may” information in contrast to “must” information) that will be unavoidable when we try to subsume multiple possibilities into a single choice.

Even though in the worst case we have to trace all the possible execution traces, the large number of constraint-propagation trees would be quickly trimmed. First, because expressions that contribute to the uncaught exception would be sparse in the program, constraints along the majority of execution traces will quickly meet a contradicting result hence are immediately removed from consideration. Second, because it is sufficient for us to find at least one test datum to execute the designated raise expression, we can stop once the first-ever non-contradicting constraints are derived. Lastly, the constraint propagation takes time linearly proportional to the input program size.

We rigorously prove that every value that satisfies the constraints at the input variable will necessarily cause the program to execute the designated raise expression. For recursive calls we bound the number of repetitive tracings of the function’s body by a fixed number, and this arbitrary bound for recursive propagations may fail to generate some constraints that would otherwise allow non-empty test data. However, the analysis safety (every generated test datum will cause the program to execute the designated raise expression) will still vacuously hold for empty test data result.

6.1 Related Works

As far as we know, our method is the first approach to automatic test data generation for exceptions. One salient feature of our method is its formal approach to the test data generation. We present a precise definition of the constraint propagation system and rigorously prove its soundness with respect to the operational semantics of the source language.

Because our analysis covers a particular path (a path to execute an exception-raise expression) in the program, the analysis falls into the path-wise test data generators. There are three kinds of test data generators: path-wise test data generators to cover certain structural elements in the program [Kor90, DO91, OJP99, Cla76, BKM91, How77, RbFHC76, BBS^{+}79], data specification generators to generate test data from a formal grammar [Mau90], and random test data generators [VMM91].

Most of the path-wise test data generators [Cla76, BKM91, How77, RbFHC76, BBS^{+}79] have used symbolic execution and they do not consider languages with exception mechanisms nor rigorously prove their soundness. Given a program and a designated path, the analysis symbolically executes the path and creates a set of constraints on the program’s input variables. Depending on the target languages of the analyses, the constraints are integer-intervals for variables [Cla76] (Fortran), [BKM91] (Pascal-like language), numeric formula of variables [How77] (Fortran), types and integer-intervals for variables [RbFHC76] (Fortran), or inequalities for data fields [BBS^{+}79] (Cobol-like language). None of them considers exception mechanisms or mentioned their soundness with respect to the operational semantics of the language.

6.2 Adopting Our Analysis for the Higher-order ML

In order for our analysis to be adopted for the higher-order ML, we have to consider the following problems:

• We need to lower-approximate the function-call-graph of programs. In order to maintain the necessary condition of the test data, the call-graph estimation should not have

spurious information in the sense that a call edge should not be included when in doubt.

• Exceptions are first-class objects in ML. They are treated just like any other values (until they are raised). They can be passed as function arguments, returned as the results of function applications, bound to identifiers, stored in locations, etc. Therefore, our constraints have to express the flows of exception values intermingled with other normal values.

We are currently implementing this analysis. Our prototype has L programs as its input programs, construct set constraints by analyzing input programs, and solve set constraints by fixpoint iteration.

References

[AH95] Alex Aiken and Nevin Heintze. Constraint-based program analysis. Tutorial of the ACM Symposium on Principles of Programming Languages, January 1995.

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

[BBS^{+}79] Jānis Bic̆evskis, Juris Borzovs, Uldis Straujums, Andris Zarins̆, and JR. Edward F. Miller. SMOTL – a system to construct samples for data processing program debugging. IEEE Transactions on Software Engineering, 5:60–66, January 1979.

[BKM91] Juris Borzovs, Audris Kalninš, and Inga Medvedis. Automatic construction of test sets: Practical approach. volume 502 of Lecture Notes in Computer Science, pages 360–432. 1991.

[CDJ^{+}89] Luca Cardelli, J. Donahue, Michael Jordan, B. Kalsow, and Greg Nelson. The modula-3 type system. In ACM Symposium on Principles of Programming Languages, pages 202–212, Austin, TX, January 1989.

[Cla76] Lori A. Clarke. A system to generate test data and symbolically execute programs. IEEE Transactions on Software Engineering, 2(3):215–222, September 1976.

[CP97] Witold Charatonik and Andreas Podelski. Solving set constraints for greatest models. Technical Report MPI-I-97-2-004, Max-Planck-Institut für Informatik, April 1997.

[CP98] Witold Charatonik and Andreas Podelski. Co-definite set constraints. In Lecture Notes in Computer Science, volume 1379, pages 211–225. Springer-Verlag, Proceedings of the 9th International Conference on Rewriting Techniques and Applications - RTA’98 edition, 1998.

[DO91] Richard A. DeMillo and A. Jefferson Offutt. Constraint-based automatic test data generation. IEEE Transactions on Software Engineering, 17(9):900–910, September 1991.

[GJS96] James Gosling, Bill Joy, and Guy L. Jr. Steele. The Java Language Specification (Java Series). Addison-Wesley, September 1996.

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

[HJ90] Nevin Heintze and Joxan Jaffar. A finite presentation theorem for approximating logic programs. Technical Report IBM Technical Report RC 16089 (# 71415), IBM, August 1990.

[HJ91] Nevin Heintze and Joxan Jaffar. A decision procedure for a class of set constraints. Technical Report CMU-CS-91-110, Carnegie-Mellon University, February 1991.

[How77] William E. Howden. Symbolic testing and the DISSECT symbolic evaluation system. IEEE Transactions on Software Engineering, 4(4):266–278, 1977.

[HP83] A. Nico Habermann and Dewayne E. Perry. Ada for Experienced Programmers. Addison-Wesley, 1983.

[Kah88] G. Kahn. Natural semantics. In K. Fuchi and M. Nivaat, editors, Programming of Future Generation Computers, pages 237–257. Elsevier Science Publishers (North-Holland), 1988.

[Kor90] Bokdan Korel. Automated software test data generation. IEEE Transactions on Software Engineering, 16(8):870–879, August 1990.

[Mau90] Peter M. Maurer. Generating testing data with enhanced context-free grammars. IEEE Software, 7(4), July 1990.

[MTHM97] Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. The Definition of Standard ML (Revised). MIT Press, 1997.

[OJP99] A. Jefferson Offutt, Zhenyi Jin, and Jie Pan. The dynamic domain reduction approach to test data generation. Software Practice and Experience, 1999.

[PL99] François Pessaux and Xavier Leroy. Type-based analysis of uncaught exceptions. In ACM Symposium on Principles of Programming Languages, pages 276–290, January 1999.

[RbFHC76] C. V. Ramamoorthy, Siu bun F. Ho, and W. T. Chen. On the automated generation of program test data. IEEE Transactions on Software Engineering, 2(4):293– 300, December 1976.

[VMM91] Jeffrey Voas, Larry Morell, and Keith Miller. Predicting where faults can hide from testing. IEEE Software, 8(2):41–58, March 1991.

[YC99] Kwangkeun Yi and Byeong-Mo Chang. Exception analysis for java. In ECOOP’99 Workshop on Formal Techniques for Java Programs, June 1999.

[YR97] Kwangkeun Yi and Sukyoung Ryu. Towards a cost-effective estimation of uncaught exceptions in SML programs. In Lecture Notes in Computer Science, volume 1302, pages 98–113. Springer-Verlag, Proceedings of the 4th International Static Analysis Symposium edition, 1997.

[YR98]  Kwangkeun Yi and Sukyoung Ryu.  SML/NJ Exception Analyzer 0.98.

http://compiler.kaist.ac.kr/pub/exna/exna-README.html, December 1998.

[YRon] Kwangkeun Yi and Sukyoung Ryu. A cost-effective estimation of uncaught exceptions in Standard ML programs. Theoretical Computer Science, (invited submission).