RICE UNIVERSITY

Effective Static Debugging via

Componential Set-Based Analysis

by

Cormac Flanagan

A Thesis Submitted in Partial Fulfillment of the Requirements for the Degree

Doctor of Philosophy

Approved, Thesis Committee:

Matthias Felleisen Professor of Computer Science

Robert S. Cartwright Professor of Computer Science

J. E. Dennis Noah Harding Professor of Computational and Applied Mathematics

Houston, Texas

May, 1997

Abstract

Effective Static Debugging via Componential Set-Based Analysis

by Cormac Flanagan

Sophisticated software systems are inherently complex. Understanding, debugging and maintaining such systems requires inferring high-level characteristics of the system’s behavior from a myriad of low-level details. For large systems, this quickly becomes an extremely difficult task.

MrSpidey is a static debugger that augments the programmers ability to deal with such complex systems. It statically analyzes the program and uses the results of the analysis to identify and highlight any program operation may cause a run-time fault. The programmer can then investigate each potential fault site and, using the graphical explanation facilities of MrSpidey, determine if the fault will really happen or whether the corresponding correctness proof is beyond the analysis’s capabilities. In practice, MrSpidey has proven to be an effective tool for debugging program under development and understanding existing programs.

The key technology underlying MrSpidey is componential set-based analysis. This is a constraint-based, whole-program analysis for object-oriented and functional programs. The analysis first processes each program component (eg. module or package) independently, generating and simplifying a constraint system describing the data flow behavior of that component. The analysis then combines and solves these simplified constraint systems to yield invariants characterizing the run-time behavior of the entire program. This component-wise approach yields an analysis that handles significantly larger programs than previous analyses of comparable accuracy.

The simplification of constraint systems raises a number of questions. In particular, we need to ensure that simplification preserves the observable behavior, or solution space, of a constraint system. This dissertation provides a complete prooftheoretic and algorithmic characterization of the observable behavior of constraint systems, and establishes a close connection between the observable equivalence of constraint systems and the equivalence of regular tree grammars. We exploit this connection to develop a complete algorithm for deciding the observable equivalence of constraint systems, and to adapt a variety of algorithms for simplifying regular tree grammars to the problem of simplifying constraint systems. The resulting constraint simplification algorithms yield an order of magnitude reduction in the size of constraint systems for typical program expressions.

Acknowledgments

Many people have contributed to making my graduate career rewarding and enjoyable. First, and foremost, I would like to thank my advisor, Matthias Felleisen. He got me started in research, taught me a great deal about programming language semantics and pragmatics (with the occasional detour into philosophy or economics), spent hours giving me feedback on research ideas and papers, and inspired much of MrSpidey’s user interface. I would also like to thank my other committee members: Robert (Corky) Cartwright, for valuable feedback on this and other research, and for the class he taught on fully abstract denotational semantics, which led to some of the key ideas of this thesis; and John Dennis, for taking time off his already busy schedule to serve on my committee.

My research environment at Rice was valuably enriched by my collogues in the programming languages theory group. I would like to thank all the members for their various contributions, including Matthew, Shriram, and Robby, who provided the DrScheme infrastructure without which the development of MrSpidey would have been impossible, and Amr, Andrew, Bruce, Mike and John, who helped me get started on research when I arrived at Rice.

Outside the programming languages group there are many other people at Rice whose valuable support and friendship helped me see this thesis through to completion, and who made my time at Rice more enjoyable.

Finally, this research would not have been possible with the support of Rice University, the Professional Activities Committee of the Association for Computing Machinery’s Special Interest Group on Programming Languages, and the National Science Foundation.

I gratefully acknowledge all this help.

Contents

Abstract ii Acknowledgments iv

1 The Need for Static Debugging 1

1.1 Reliability and Safety . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.2 MrSpidey . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.3 Componential Set-Based Analysis . . . . . . . . . . . . . . . . . . . . 5

1.3.1 Set-Based Analysis . . . . . . . . . . . . . . . . . . . . . . . . 5 1.3.2 Constraint Simplification . . . . . . . . . . . . . . . . . . . . . 7 1.3.3 Componential Set-Based Analysis . . . . . . . . . . . . . . . . 7

1.4 Thesis Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8

2 Set-Based Analysis 10

2.1 The Source Language . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 2.1.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 2.1.2 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12

2.2 The Constraint Language . . . . . . . . . . . . . . . . . . . . . . . . 12 2.3 The Meaning of Set Constraints . . . . . . . . . . . . . . . . . . . . . 13

2.3.1 The Semantic Domain . . . . . . . . . . . . . . . . . . . . . . 13 2.3.2 The Semantics of Constraints . . . . . . . . . . . . . . . . . . 15

2.4 Deriving Constraints . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 2.5 Soundness of the Derived Constraints . . . . . . . . . . . . . . . . . . 19 2.6 Solving Set Constraints . . . . . . . . . . . . . . . . . . . . . . . . . . 21

2.6.1 Computing the Least Solution . . . . . . . . . . . . . . . . . . 23 2.7 An Implementation of Set-Based Analysis . . . . . . . . . . . . . . . 24

2.7.1 Representation of constraint systems . . . . . . . . . . . . . . 24 2.7.2 Closing constraint systems . . . . . . . . . . . . . . . . . . . . 25 2.7.3 Deriving constraints . . . . . . . . . . . . . . . . . . . . . . . 25

3 Extending Set-Based Analysis 29

3.1 Additional Selectors . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 3.2 Analysis of Pairs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31

3.2.1 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 3.2.2 Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31

3.3 Analysis of First-Class Continuations . . . . . . . . . . . . . . . . . . 33 3.3.1 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 3.3.2 Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34

3.4 Analysis of Assignable Variables . . . . . . . . . . . . . . . . . . . . . 37 3.4.1 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 3.4.2 Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38

3.5 Analysis of Assignable Boxes . . . . . . . . . . . . . . . . . . . . . . . 38 3.5.1 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 3.5.2 Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40

3.6 Analysis of Units . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 3.6.1 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 3.6.2 Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44

3.7 Analysis of Classes . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 3.7.1 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 3.7.2 Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46

4 Using Set-Based Analysis for Static Debugging 49

4.1 The Type Language . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 4.2 Computing Type Information . . . . . . . . . . . . . . . . . . . . . . 50 4.3 Identifying Unsafe Operations . . . . . . . . . . . . . . . . . . . . . . 53

5 User Interface to the Static Debugger 55

5.1 Displaying Unsafe Operations . . . . . . . . . . . . . . . . . . . . . . 55 5.2 Pop-Up Menu . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 5.3 Presenting Type Information . . . . . . . . . . . . . . . . . . . . . . . 57 5.4 The Value Flow Browser . . . . . . . . . . . . . . . . . . . . . . . . . 58 5.5 A Sample Debugging Session . . . . . . . . . . . . . . . . . . . . . . . 61

6 Constraint Simplification 62

6.1 Conditions for Constraint Simplification . . . . . . . . . . . . . . . . 62 6.2 The Proof Theory of Observable Equivalence . . . . . . . . . . . . . . 64 6.3 Deciding Observable Equivalence . . . . . . . . . . . . . . . . . . . . 67

6.3.1 Regular Grammars . . . . . . . . . . . . . . . . . . . . . . . . 68 6.3.2 Regular Tree Grammars . . . . . . . . . . . . . . . . . . . . . 70 6.3.3 Staging . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71 6.3.4 The Entailment Algorithm . . . . . . . . . . . . . . . . . . . . 72

6.4 Practical Constraint System Simplification . . . . . . . . . . . . . . . 74 6.4.1 Empty Constraint Simplification . . . . . . . . . . . . . . . . . 75 6.4.2 Unreachable Constraint Simplification . . . . . . . . . . . . . 76 6.4.3 Removing ϵ-Constraints . . . . . . . . . . . . . . . . . . . . . 76 6.4.4 Hopcroft’s Algorithm . . . . . . . . . . . . . . . . . . . . . . . 77

6.5 Simplification Benchmarks . . . . . . . . . . . . . . . . . . . . . . . . 78

7 Componential Set-Based Analysis 80

7.1 Componential Set-Based Analysis . . . . . . . . . . . . . . . . . . . . 80 7.2 Experimental Results . . . . . . . . . . . . . . . . . . . . . . . . . . . 81 7.3 User Interface for Multi-File Programs . . . . . . . . . . . . . . . . . 82 7.4 Efficient Polymorphic Analysis . . . . . . . . . . . . . . . . . . . . . . 84

8 Evaluation of MrSpidey 88

8.1 Verifying a Web Server . . . . . . . . . . . . . . . . . . . . . . . . . . 88 8.2 Verifying gunzip . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 88 8.3 Verifying an Extended Direct Semantics Interpreter . . . . . . . . . . 90 8.4 Statically Debugging HHL . . . . . . . . . . . . . . . . . . . . . . . . 91

9 Related Work 93

9.1 Static Debuggers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93 9.2 Constraint Simplification . . . . . . . . . . . . . . . . . . . . . . . . . 94

10Limitations and Future Work 96

10.1 Size of Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 96 10.2 Accuracy of the Analysis . . . . . . . . . . . . . . . . . . . . . . . . . 97 10.3 State in the User Interface . . . . . . . . . . . . . . . . . . . . . . . . 97 10.4 Signatures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97

A Proofs for Chapter 3 99

A.1 Subject Reduction Proof . . . . . . . . . . . . . . . . . . . . . . . . . 99 A.2 Proofs for Computing Set-Based Analysis . . . . . . . . . . . . . . . . 107

B Proofs for Chapter 5 112

B.1 Correctness of MkType . . . . . . . . . . . . . . . . . . . . . . . . . . 112

C Proofs for Chapter 6 114

C.1 Proofs for Conditions for Constraint Simplification . . . . . . . . . . 114 C.2 Proofs for Proof Theory of Observable Equivalence . . . . . . . . . . 114 C.3 Proofs for Deciding Observable Equivalence . . . . . . . . . . . . . . 122 C.4 Correctness of the Entailment Algorithm . . . . . . . . . . . . . . . . 126 C.5 Correctness of the Hopcroft Algorithm . . . . . . . . . . . . . . . . . 129

D MrSpidey Reference Manual 132

D.1 Using MrSpidey . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 132 D.1.1 The Program Window . . . . . . . . . . . . . . . . . . . . . . 133 D.1.2 The Summary Window . . . . . . . . . . . . . . . . . . . . . . 138

D.2 Preferences . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 138 D.2.1 MrSpidey Analysis Preferences Window . . . . . . . . . . . . . 138 D.2.2 MrSpidey Type Display Preferences Window . . . . . . . . . . . 140

D.3 Analysis of Large Programs . . . . . . . . . . . . . . . . . . . . . . . 142

D.3.1 Inter-File Arrows . . . . . . . . . . . . . . . . . . . . . . . . . 143 D.4 The Type Language . . . . . . . . . . . . . . . . . . . . . . . . . . . 145

D.4.1 Accurate Numeric Operations . . . . . . . . . . . . . . . . . . 147 D.5 Extensions to DrScheme . . . . . . . . . . . . . . . . . . . . . . . . . 147

D.5.1 Type Assertions . . . . . . . . . . . . . . . . . . . . . . . . . . 147 D.5.2 Polymorphic Annotations . . . . . . . . . . . . . . . . . . . . 147 D.5.3 Declaring New Primitives . . . . . . . . . . . . . . . . . . . . 148 D.5.4 Declaring Constructors . . . . . . . . . . . . . . . . . . . . . . 148 D.5.5 Declaring New Types . . . . . . . . . . . . . . . . . . . . . . . 148

D.6 Restrictions on Source Programs . . . . . . . . . . . . . . . . . . . . . 148

E Implementation Details 150

E.1 Zodiac . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 150 E.2 MrEd . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 150 E.3 Multiple-Arity Functions . . . . . . . . . . . . . . . . . . . . . . . . . 151 E.4 Multiple Values . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 151 E.5 Checking Scheme Primitives . . . . . . . . . . . . . . . . . . . . . . . 152

E.5.1 Type Schemas . . . . . . . . . . . . . . . . . . . . . . . . . . . 153 E.5.2 New Constraint Classes . . . . . . . . . . . . . . . . . . . . . 153 E.5.3 Converting Type Schemas to Constraints . . . . . . . . . . . . 156

F Notations 157

Bibliography 160

Chapter 1

The Need for Static Debugging

Sophisticated software systems are inherently complex. A typical program such as a compiler or a word processor contains an enormous amount of detail. Developing, maintaining, or debugging this kind of system requires inferring high-level characteristic of the system’s behavior from a large number of low-level details. For large systems, this quickly becomes an extremely difficult task, particularly since programmers, being human, have finite limits in the amount of complexity they can manage.

MrSpidey is a static debugger for Scheme that augments the programmers ability to deal with such complex systems. It statically analyzes the program and uses the results of the analysis to identify and highlight any program operation that may cause a run-time error. The programmer can then investigate each potential fault site and, using the graphical explanation facilities of MrSpidey, determine if the fault will really happen or whether the corresponding correctness proof is beyond the analysis’s capabilities. In practice, MrSpidey has proven to be an effective tool for debugging a variety of programs, including a staged interpreter, a hardware verifier, and portions of Rice’s Scheme program development environment.

The following section describes the kinds of program errors that MrSpidey helps identify; the next section shows how MrSpidey presents information concerning these potential errors to the programmer; and section 1.3 describes the underlying analysis that MrSpidey uses to infer that information. The last section provides an overview of the rest of the thesis.

1.1 Reliability and Safety

A reliable program does not mis-apply program operations. Addition always operates on numbers, not strings. Concatenation works with strings, not numbers. To avoid the abuse of program operations, most languages impose a restrictive type system, which forbids the syntactic formation of certain faulty program phrases. However, type systems are too coarse to solve the general problem, which includes indexing an array outside of its proper bounds, division by zero, dereferencing of null pointers, and jumping to non-function pointers. These problems are beyond the capabilities of standard type systems, and different languages deal with such run-time errors in different ways.

Unsafe languages like C [31] ignore the problem and leave it to the programmer to insert checks where appropriate. As a result C programs are notoriously prone to inexplicable crashes [33], or, worse, inexplicable, correct-looking results. In contrast, safe languages such as SML [34], Scheme [5], and Java [22] equip program operations with appropriate run-time checks where necessary. These checks guarantee that a misapplied program operation immediately raises an error signal, instead of returning a random bit-pattern. Although this solution ensures that programs don’t produce random results, it is unsatisfactory because certain errors are not signaled until runtime.

A better approach is to verify the pre-conditions of each program operation statically. If we can prove that that a particular program operation is only applied to appropriate arguments, we say that that operation is safe. In the absence of such a proof, we have to consider that operation unsafe, since it may be applied to inappropriate arguments. Verifying the safety of program operations requires inferring invariants describing the sets of values that may occur at different points in the program. These invariants could be inferred manually, but for large systems this quickly becomes an extremely difficult and error-prone task. What is needed instead is a static analysis tool that assists the programmer in inferring invariants and reasoning about the safety of program operations. We call this kind of tool a static debugger.

Past research on static debuggers mainly focused on the synthesis of the invariants [3, 8]. However, the presentation and, in particular, the explanation of these invariants were neglected. We believe that synthesizing invariants is not enough. Instead, a programmer must be able to inspect the invariants and browse their underlying proof. Then, if some invariant contains an unexpected element, the programmer can determine whether the element results from a flaw in the program or approximations introduced by the proof system.

1.2 MrSpidey

MrSpidey is a static debugger for Scheme that allows the programmer to browse program invariants and their derivations. On demand, MrSpidey statically analyzes the program and uses the resulting invariants to identify and highlight program operations that are not provably safe (according to MrSpidey’s underlying proof system). Associated pop-up menus provide access to additional information, including:

• a value-set invariant for each expression and variable, and

• a graphical explanation for each invariant.

The programmer can investigate each unsafe operation and determine whether (a) the fault will really happen, or (b) the corresponding correctness proof is beyond MrSpidey’s capabilities. MrSpidey’s graphical explanation facilities make it easy to distinguish these two situations.

As an illustration of MrSpidey’s explanatory capabilities, consider the program sum.ss shown in figure 1.1. The program defines a function that sums binary trees. A tree is either a leaf node, represented as a number, or an internal node, represented as a cons-cell containing two subtrees.

Figure 1.1 The program sum.ss

The mark-ups in in figure 1.1 indicate that the operation + is provably safe, since it is not underlined. Conversely, car, which is underlined, is unsafe. That is, MrSpidey’s proof system is unable to verify that this operation is only applied to appropriate arguments. Indeed, the proof system yields an invariant for car’s argument tree that contains values that are inappropriate arguments for car. Clicking on the argument variable tree displays that invariant, as shown in figure 1.2. The invariant shows that tree may be bound to the value nil, which is outside the domain of car. Using MrSpidey’s explanatory facilities to investigate the source of this erroneous value results in the display shown in figure 1.3. The displayed arrows show how nil originated in the argument to sum. Since the argument is not actually a correct binary tree, we have identified the original source of the problem, and can now fix the program by providing a correct tree as the argument to sum.

Figure 1.2 The value set invariant for tree

Although sum.ss is a trivial program, MrSpidey also works reasonably well on substantially larger programs. The key problem in developing a static debugger for large programs is developing an underlying proof system that can infer accurate invariants for such programs. MrSpidey is based on a componential,^{∗} or component-wise, analysis that can effective handle programs of up to tens of thousands of lines of code.

∗componential a. of or pertaining to components; spec. (Ling.) designating the analysis of distinctive sound units or grammatical elements into phonetic or semantic components (New Shorter Oxford English Dictionary, Clarendon Press, 1993)

Figure 1.3 The flow of nil

1.3 Componential Set-Based Analysis

The key technology underlying MrSpidey is componential set-based analysis. This analysis is a derivative of Heintze’s set-based analysis of ML programs [24]. We begin with a discussion of Heintze’s analysis and its limitations, and then describe how we can develop a componential variant of Heintze’s analysis that overcomes those limitations.

1.3.1 Set-Based Analysis

Heintze’s original set-based analysis is a constraint-based, whole-program analysis for functional and object-oriented programming languages. It consists of two co-mingled phases: a specification phase and a solution phase. During the specification phase, the analysis tool derives constraints on the sets of values that program expressions may assume. These constraints describe the data-flow relationships amongst the expressions in the analyzed program. During the solution phase, the analysis produces finite descriptions of the potentially infinite sets of values that satisfy these constraints. The result provides an approximate set of values for each expression in the program.

We initially used set-based analysis as the underlying proof system for MrSpidey, for the following three reasons:

• Set-based analysis produces accurate program invariants for Scheme-like languages, even in the presence of complex control-flow and data-flow patterns.

• Set-based analysis is intuitive to the programmer. The analysis interprets program operations as naïve set-theoretic operations on sets of run-time values, and propagates these sets of values along the program’s data-flow paths, in a manner that is easily understood by the programmer.

• By exploiting the set-based analysis algorithm, we can provide a supporting explanation for each invariant produced by the analysis.

In practice, set-based analysis has proven highly effective for debugging pedagogic programming, which includes programs of several hundreds to 2,000 lines of code. However, it becomes less useful for debugging larger programs for three reasons:

• Set-based analysis has an O(n^{3}) worst-case time bound. Although the constant on the cubic element in the polynomial is small, it becomes noticeable for programs of several thousand lines.

• Large programming projects tend to re-use functions in a polymorphic fashion. To avoid merging information between unrelated calls to such functions, the analysis must duplicate the constraints for each call site. This duplication is expensive because the size of the constraint system is at best linear, and possibly quadratic, in the size of the function.

• MrSpidey presents value set invariants to the programmer that are computed from the information produced by the analysis, and as the constraints get larger these invariants become extremely verbose.

A closer look at these three obstacles quickly reveals that the major limitation of set-based analysis is the size of the constraint system describing the data-flow relationships of a program. If we could develop an algorithm for reducing the size of a constraint system without affecting the solution space that it denotes, we could simplify constraint systems at intermediate stages and thus reduce the analysis time. In particular, simplifying the constraint system for each module would substantially reduce the cost of solving the combined system of constraints for a modularized program; similarly, simplifying the constraint system of a polymorphic function would substantially reduce the cost of duplicating that constraint system at each polymorphic reference.

1.3.2 Constraint Simplification

The simplification of constraint systems raises both interesting theoretical and practical questions. On the theoretical side, we need to ensure that simplification preserves the observable behavior, or solution space, of a constraint system. In this dissertation, we provide a complete proof-theoretic and algorithmic characterization of the observable behavior of constraint systems. In the course of this development, we establish a close connection between the observable equivalence of constraint systems and the equivalence of regular tree grammars (RTGs).^{†} Exploiting this connection, we develop a complete algorithm for deciding the observable equivalence of constraint systems. Unfortunately, the problem is PSPACE-hard, and hence the algorithm takes exponential time.

Fortunately, a minimized constraint system is not necessary for our purposes. The practical question concerns finding algorithms for simplifying, though not necessarily minimizing, constraint systems. To answer this question, we exploit the correspondence between the minimization problems for RTGs and constraint systems to adapt a variety of algorithms for simplifying RTGs to the problem of simplifying constraint systems. The resulting constraint simplification algorithms yield an order of magnitude reduction in the size of constraint systems for typical program expressions.

1.3.3 Componential Set-Based Analysis

We exploit these simplification algorithms to develop a componential set-based analysis algorithms. The componential analysis first processes each program component independently, deriving and simplifying the constraint system for that component and saves the simplified system in a constraint file, for use in later runs of the analysis. This step can be skipped for each program component that has not changed since the last run of the analysis, since the component’s constraint file can be used instead.

The analysis then combines and solves these simplified constraint systems, thus propagating data-flow information between the constraint systems for the various program components. The resulting solution yields invariants characterizing the runtime behavior of the entire program.

†A number of researchers, including Reynolds [39], Jones and Muchnick [29], Heintze [24], Aiken [2], and Cousot and Cousot [7] previously exploited the relationship between RTGs and the least solution of a constraint system. We present an additional result, namely a connection between RTGs and the observable behavior (i.e., the entire solution space) of constraint systems.

This component-wise approach yields an analysis that can handle significantly larger programs than previous analyses of comparable accuracy. The new analysis also performs extremely well in an interactive setting because it exploits the saved constraint files where possible and thus avoids re-processing many program components unnecessarily.

1.4 Thesis Overview

This dissertation establishes that the results of set-based analysis can be effectively used to statically debug real programs. In the course of this investigation we present a new derivation of set-based analysis that is significantly more extensible that Heintze’s original derivation; we show how to present the invariants and derivations of the analysis to the programmer in a natural and easily-accessible manner; and we evaluate the effectiveness of the resulting static debugging system on a variety of programs, including a staged interpreter and a hardware verifier.

Since real programs also tend to be large, we develop a componential variant of setbased analysis that performs significantly better on large programs. The development of this analysis requires an investigation of the observable equivalence of constraint systems. We provide a complete proof-theoretic and algorithmic characterization of the observable behavior of constraint systems and establish a close connection between the observable equivalence of constraint systems and the equivalence of RTGs. We then exploit this connection to develop a complete algorithm for deciding the observable equivalence of constraint systems, and to adapt a variety of algorithms for simplifying RTGs to the problem of simplifying constraint systems.

The next chapter describes set-based analysis in the context of an idealized λcalculus-like language. This analysis is extended in chapter 3 to a number of additional features typically found in real program languages, such as pairs (or other compound data structures), first-class continuations, assignable variables, mutable data structures, modules and classes.

Chapter 4 explains how MrSpidey uses the analysis results to compute useful static debugging information, and chapter 5 describes how this information is presented to the programmer in a natural and intuitive manner.

Chapters 6 and 7 introduce componential set-based analysis. Chapter 6 describes our investigation of the observable equivalence of constraint systems and the development of the constraint simplification algorithms. Chapter 7 shows how to exploit these simplification algorithms in a componential analysis. These two chapters also contain experimental results describing the behavior of both the simplification algorithms and the componential analysis.

Chapter 8 evaluates the effectiveness of MrSpidey on a variety of programs, including a staged interpreter and a hardware verifier. Chapter 9 describes related work on static debugging, constraint simplification and program analysis. The final chapter examines of some of the problems and limitations of MrSpidey, and suggests directions for future work.

The thesis includes six appendices. The first three appendices present proofs for chapters 2, 4, and 6, respectively. The fourth appendix is a reference manual for MrSpidey. The fifth appendix describes a number of details concerning the implementation of MrSpidey, and the sixth appendix contains a list of the mathematical notations and symbols used in this dissertation.

Chapter 2

Set-Based Analysis

MrSpidey’s underlying analysis is derived from Heintze’s set-based analysis of ML programs [23, 24]. The analysis is a constraint-based, whole-program analysis for functional and object-oriented programming languages. It consists of two co-mingled phases: a specification phase and a solution phase.^{∗} During the specification phase, the analysis tool derives constraints on the sets of values that program expressions may assume. These constraints describe the data flow relationships amongst the expressions in the analyzed program. During the solution phase, the analysis produces finite descriptions of the potentially infinite sets of values that satisfy these constraints. The result provides an approximate set of values for each labeled expression in the program.

In this chapter, we provide a formal description of set-based analysis for a idealized, λ-calculus-like language with constants. The following chapter extends the analysis to realistic language features including pairs, first-class continuations, assignable variables, mutable data structures, modules and classes. Since it is difficult to extend Heintze’s development of set-based analysis beyond a functional core language, we develop Heintze’s ideas using an alternative formulation and semantics. Specifically, whereas Heintze’s development is based on “natural” semantics, which cannot easily accommodate non-local control operators and destructive data structure manipulations, our alternative formulation is based on an extensible reduction semantics. This change of framework also simplifies the derivation of the constraint simplification algorithms.

Section 2.1 introduces our idealized, λ-calculus-like language. Section 2.2 introduces the constraint language, and section 2.3 defines the meaning of those constraints. Section 2.4 describes how we derive appropriate constraints for a program, and section 2.5 proves the correctness of the derived constraints. Section 2.6 shows how to solve the derived constraints to yield information about the program’s runtime behavior. Section 2.7 contains an outline implementation of set-based analysis.

∗Cousot and Cousot showed that set-based analysis can alternatively be formulated as an abstract interpretation computed by chaotic iteration [7].

2.1 The Source Language

We develop the analysis for an idealized, λ-calculus-like language Λ with constants and labeled expressions. This section introduces the syntax and semantics of Λ.

2.1.1 Syntax

Syntax:

M ∈ Λ  = x | V | (M M) | (let (x V) M) | M^{l}  (Expressions)
V ∈ Value  = b | (λ^{t}x.M)  (Values)
x ∈ Var  = {x, y, z, …}  (Variables)
b ∈ BasicConst  (Basic Constants)
t ∈ FnTag  (Function Tags)
l ∈ Label  (Expression Labels)

Figure 2.1 The source language Λ

Expressions in the language are either variables, values, applications, let-expressions, or labeled expressions: see figure 2.1. Values include basic constants and functions. Each function has an identifying tag so that MrSpidey can reconstruct the textual source of function values from the results of the analysis. We use let-expressions to introduce polymorphic bindings, and hence restrict these bindings to syntactic values [48]. We use labels to identify those program expressions whose values we wish to predict.

We work with the usual conventions and terminology of the λ_{v}-calculus when discussing syntactic issues. In particular, the substitution operation M[x ← V] replaces all free occurrences of x within M by V, and Λ^{0} denotes the set of closed terms, also called programs.

2.1.2 Semantics

We specify the meaning of programs based upon three notions of reduction:

((λ^{t}x.M) V) ⟶ M[x ↦ V]  (β_{v})
(let (x V) M) ⟶ M[x ↦ V]  (βlet )
V^{l} ⟶ V  (unlabel)

The β_{v} and βlet rules are the conventional rules for the λ-calculus. The unlabel rule simply removes the label from an expression once its value is needed.

An evaluation context E is an expression containing a hole [ ] in place of the next sub-term to be evaluated:

E = [ ] | (E M) | (V E) | E^{l}

For example, in the term (N M), the next expression to be evaluated lies within N, and thus the definition of evaluation contexts includes the clause (E M). An evaluation context always contains a single hole [ ], and we use the notation E[ M ] to denote term produced by filling the hole in E with the term M.

The standard reduction relation ⟼ is the compatible closure of ⟶ with respect to evaluation contexts:

E[ M ] ⟼ E[ N ] iff M ⟶ N

The relation ⟼^{∗} is the reflexive, transitive closure of ⟼. The semantics of the language is defined via the partial function eval on programs:

eval : Λ^{0} ⟶_{p} Value
eval(M) = V  if M ⟼^{∗} V

2.2 The Constraint Language

To simplify the later derivation of the constraint simplification algorithms (see chapter 6), we express the constraint language in terms of selectors, instead of the more usual constructors. Specifically, a set expression τ is either a set variable; a constant; or one of the “selector” expressions dom(τ) or rng(τ):

τ ∈ SetExp = α | c | dom(τ) | rng(τ)
α, β ∈ SetVar ⊃ Label
c ∈ Const = BasicConst ∪ FnTag

By using selector expressions, we can specify each “quantum” of the program’s data-flow behavior independently; using constructors would combine several of these quanta into one constraint. For example, we specify a function’s behavior via the two constraints {dom(α) ≤ α_{1}, α_{2} ≤ rng(α)} instead of the combined constraint {(α_{1} → α_{2}) ≤ α}.

The meta-variables α, β, γ range over set variables, and we include program labels in the collection of set variables. Constants include both basic constants and function tags. A constraint C ∈ Constraint is an inequality τ_{1} ≤ τ_{2} relating two set expressions.

C ∈ Constraint = τ_{1} ≤ τ_{2}

We sometimes enclose constraints inside square brackets for clarity: [τ_{1} ≤ τ_{2}]. A constraint system S ∈ ConstraintSystem is a collection of constraints.

S ∈ ConstraintSystem = P_{fin}(Constraint)

We use SetVar(S) to denote the collection of set variables in a constraint system S. In some cases, the relevant constraints in a constraint system are those that only mention certain set variables. The restriction of a constraint system to a collection of set variables E is:

S |_{E} = {C ∈ S | C only mentions set variables in E}

2.3 The Meaning of Set Constraints

Intuitively, each set expression τ denotes a set of run-time values, and each constraint τ_{1} ≤ τ_{2} denotes a corresponding set containment relationship. We formalize the meaning of set constraints by mapping syntactic set expressions onto a semantic domain. The next subsection describes the precise structure of the semantic domain, and the second subsection describes the mapping from set expressions to that domain.

2.3.1 The Semantic Domain

A set expression denotes a collection of values. For our sample language, the collection consists of basic constants and functions and is therefore best represented as a triple X = ⟨C, D, R⟩. The first component C ∈ P(Const)^{†} is a set of basic constants and function tags. The second and third components of X denote the possible arguments and results of functions in X, respectively. Since these two components also denote value sets, the appropriate model for set expressions is the solution of the equation:

†P denotes the power-set constructor.

D = P(Const) × D × D

The solution D is equivalent to the set of all infinite binary trees^{‡} with each node labeled with an element of P(Const). This set can be formally defined as the set of total functions f : {dom, rng}^{∗} ⟶ P(Const), and the rest of the development can be adapted mutandis mutatis [36]. For clarity, we present our results using the more intuitive equational definition instead.

We use the functions const, dom, and rng to extract the respective components of an element in D:

const : D ⟶ P(Const)
const (⟨C, D, R⟩) = C
dom : D ⟶ D
dom (⟨C, D, R⟩) = D
rng : D ⟶ D
rng (⟨C, D, R⟩) = R

Each element of D represents a set of run-time values (relative to a given program) according to the set of basic constants and function tags in its first component. The set of values represented by an element X ∈ D is defined through the relation V in X:

b in ⟨C, D, R⟩ iff b ∈ C
(λ^{t}x.M) in ⟨C, D, R⟩ iff t ∈ C

We order the elements of D according to a relation that is anti-monotonic in the domain position:

⟨C_{1}, D_{1}, R_{1}⟩ ⊑ ⟨C_{2}, D_{2}, R_{2}⟩ iff C_{1} ⊆ C_{2}, D_{2} ⊑ D_{1}, R_{1} ⊑ R_{2}

This ordering is anti-monotonic in the domain position because information about argument values at an application needs to flow backward along data-flow paths to the formal parameter of the corresponding function definitions. To illustrate this idea, consider a program that binds a function f to a program variable g. This behavior is described in the semantic domain as the inequality X_{f} ⊑ X_{g}, where X_{f} and X_{g} describe the values sets for f and g respectively. Since the possible argument set for f must contain all values to which g is applied, the inequality dom (X_{g}) ⊑ dom (X_{f}) must also hold. Thus the domain D should satisfy the inference rule:

‡In order to analyze languages with additional data structures, we later extend D to infinite n-ary trees, where n is the number of selectors (e.g.. dom, rng) corresponding to the extended language.

\frac{X_{f} ⊑ X_{g}}{dom (X_{g}) ⊑ dom (X_{f})}

which is why the ordering ⊑ needs to be anti-monotonic in the domain element.

Under the defined ordering, the set D forms a complete lattice; the top and bottom elements are the solutions to the equations:

\begin{aligned}⊤ & = & ⟨Const, ⊥, ⊤⟩ \\ ⊥ & = & ⟨∅, ⊤, ⊥⟩ \end{aligned}

respectively. The least upper bound and greatest lower bound operations are recursively defined as:

\begin{aligned}⟨C_{1}, D_{1}, R_{1}⟩ ⊔ ⟨C_{2}, D_{2}, R_{2}⟩ & = & ⟨C_{1} ∪ C_{2}, D_{1} ⊓ D_{2}, R_{1} ⊔ R_{2}⟩ \\ ⟨C_{1}, D_{1}, R_{1}⟩ ⊓ ⟨C_{2}, D_{2}, R_{2}⟩ & = & ⟨C_{1} ∩ C_{2}, D_{1} ⊔ D_{2}, R_{1} ⊓ R_{2}⟩ \end{aligned}

2.3.2 The Semantics of Constraints

The semantics of constraints is defined with respect to a set environment ρ, which specifies an element of D for each set variable in a constraint:

ρ ∈ SetEnv = SetVar ⟶ D

The collection of set environments forms a complete lattice SetEnv under the pointwise extension of the ordering relation ⊑ on D.

For each set environment ρ, we define the following unique extension ρ^{∗} that specifies a meaning for set expressions:

ρ^{∗} : SetExp ⟶ D
ρ^{∗}(α) = ρ(α)
ρ^{∗}(c) = ⟨{c}, ⊤, ⊥⟩
ρ^{∗}(dom(τ)) = dom (ρ^{∗}(τ))
ρ^{∗}(rng(τ)) = rng (ρ^{∗}(τ))

Where there is no confusion, we remove the asterisk and simply use ρ to denote ρ^{∗}.

A set environment ρ satisfies a constraint C = [τ_{1} ≤ τ_{2}] (written ρ ⊧ C) if ρ(τ_{1}) ⊑ ρ(τ_{2}). Similarly, ρ satisfies S, or ρ is a solution of S (written ρ ⊧ S) if ρ ⊧ C for each C ∈ S. The relation ⊧ is obviously reflexive and transitive. The solution space of a constraint system S is:

Soln(S) = {ρ | ρ ⊧ S}

A constraints set S_{1} entails S_{2} (written S_{1} ⊧ S_{2}) iff Soln(S_{1}) ⊆ Soln(S_{2}), and S_{1} is observably equivalent to S_{2} (written S_{1} ≅ S_{2}) iff S_{1} ⊧ S_{2} and S_{2} ⊧ S_{1}.

The restriction of a solution space to a collection of set variables E is:

Soln(S) |_{E} = {ρ | ∃ρ′ ∈ Soln(S) such that ρ(α) = ρ′(α) ∀α ∈ E}

There are actually more set environments in the restricted solution space, since these additional environments can specify arbitrary domain elements for all set variables that are not in E.

We extend the notion of restriction to the entailment and observable equivalence of constraint systems. Definition 2.3.1. (Restricted Entailment, Restricted Observable Equivalence)

• If Soln(S_{1}) |_{E} ⊆ Soln(S_{2}) |_{E}, then S_{1} entails S_{2} with respect to E (written S_{1} ⊧_{E} S_{2}).

• If S_{1} ⊧_{E} S_{2} and S_{2} ⊧_{E} S_{1} then that S_{1} and S_{2} are observably equivalent with respect to E (written S_{1} ≅_{E} S_{2}) .

2.4 Deriving Constraints

The specification phase of set-based analysis derives constraints on the sets of values that program expressions may assume. Following Aiken et al. [2] and Palsberg and O’Keefe [36], we formulate this derivation as a proof system.

The derivation proceeds in a syntax-directed manner according to the constraint derivation rules presented in figure 2.2. Each rule infers a judgment of the form Γ ⊢ M : α, S, where:

Γ ∪ {x : β} ⊢ x : α, {β ≤ α}  (var)
Γ ⊢ b : α, {b ≤ α}  (const)
\frac{Γ ⊢ M : β, S}{Γ ⊢ M^{l} : α, S ∪ \{β ≤ l, β ≤ α\}}  (label)

\frac{Γ ∪ \{x : α_{1}\} ⊢ M : α_{2}, S}{Γ ⊢ (λ^{t}x.M) : α, S ∪ \{ \begin{matrix}t & ≤ & α \\ dom(α) & ≤ & α_{1} \\ α_{2} & ≤ & rng(α) \end{matrix} \}}  (abs)

\frac{Γ ⊢ M_{i} : β_{i}, S_{i}}{Γ ⊢ (M_{1} M_{2}) : α, S_{1} ∪ S_{2} ∪ \{ \begin{matrix}β_{2} & ≤ & dom(β_{1}) \\ rng(β_{1}) & ≤ & α \end{matrix} \}}  (app)

\frac{Γ ⊢ V : α_{V} , S_{V} \overline{α} = SetVar(S_{V}) \ (F V [range(Γ)] ∪ Label) Γ ∪ \{x : ∀\overline{α}. (α_{V} , S_{V})\} ⊢ M : β, S}{Γ ⊢ (let (x V) M) : β, S}  (let)

\frac{ψ is a substitution of set variables for \overline{α}}{Γ ∪ \{x : ∀\overline{α}. (α_{V} , S_{V})\} ⊢ x : β, ψ(S_{V}) ∪ \{ψ(α_{V}) ≤ β\}}  (inst)

Figure 2.2 Constraint derivation rules.

1. the derivation context Γ maps the free variables of the expression M to either set variables or constraint schemas (see below);

2. α names the value set of M; and

3. the constraint system S is a simple constraint system (see below) describes the data-flow relationships of M, using α.

The constraint derivation rules only generates a certain subset of the constraint language, called simple constraints. Simple constraints have the form:

C ∈  SimpleCon = c ≤ β
| α ≤ β
| α ≤ dom(β)
| rng(α) ≤ β
| dom(α) ≤ β
| α ≤ rng(β)
S ∈ SimpleConSystem = P_{fin}(SimpleCon)

A collection of such simple constraints forms a simple constraint system. We use the calligraphic letters C and S as meta-variables ranging over simple constraints and simple constraint systems, respectively.

The constraint derivation rule (var) derives appropriate constraints for a variable reference x. This rule generates the constraint β ≤ α, where β describes the value set of x, and α denoting the value set for this reference to x. The constraint derivation rule (const) generates the constraint b ≤ α, which ensures that the value set for a constant expression contains that constant. The rule (label) records the possible values of a labeled expression M^{l} in the label l.

The rule (abs) for functions records the function’s tag, and also propagates values from the function’s domain into its formal parameter and from the function’s body into its range. The rule (app) for applications propagates values from the argument expression into the domain of the applied function and from the range of that function into the result of the application expression. The correctness of the rules (abs) and (app) relies on the anti-monotonicity of the underlying ordering ⊑ in the domain position.

The rule (let) produces a constraint schema σ = ∀\overline{α}. (β, S) for polymorphic, letbound values [2, 42]. The set variable β names the result of the value; the simple constraint system S describes the data-flow relationships of the value, using β; and the set \overline{α} = \{α_{1}, …, α_{n}\} contains those internal set variables of the constraint system that must be duplicated at each reference to the let-bound variable via the rule (inst).

The derivation context Γ maps program variables to either set variables or constraint schemas:

Γ ∈ DerivCtxt = Var ⟶_{p} SetVar ∪ ConSchema
σ ∈ ConSchema = ∀\overline{α}. (β, S)

We use F V [range(Γ)] to denote the free set variables in the range of Γ. The free set variables of a constraint schema ∀\overline{α}. (β, S) are those in S but not in \overline{α}, and the free variables of a set variable is simply the set variable itself.

Many of the constraint derivation rules contain meta set variables. For example, the rule (const):

Γ ⊢ b : α, {b ≤ α}  (const)

mentions the meta set variable α. Any time this rule is applied, we need to choose an appropriate set variable for this meta variable. Choosing a fresh set variable not used elsewhere in the derivation yields a more accurate analysis. A most general constraint derivation is one that always uses fresh set variable for these meta variables, and a most general constraint system for an expression is one produced by a most general constraint derivation. However, the use of fresh variables is not strictly necessary for the correctness of the analysis. As an extreme example, we could perform the entire analysis using a single set variable, although this would yield extremely coarse results, and would be of no practical use. But the ability to consider constraint derivations that re-use certain set variables significantly simplifies the subject reduction proofs of the following section.

2.5 Soundness of the Derived Constraints

Let P be a program such that ∅ ⊢ P : α, S. Typically, S has many solutions. Each solution ρ of S correctly approximates the value sets of labeled expressions in P. That is, if ρ is a solution of S and V is a possible value of some expression M^{l} in P, then V in ρ(l). We prove this property using a subject reduction proof [13], following Wright and Felleisen [47] and Palsberg [35].

Main Lemma 2.5.1 (Soundness of the Derived Constraints). If ∅ ⊢ P : α, S and ρ ⊧ S and P ⟼^{∗} E[ V^{l} ] then V in ρ(l).

Proof: The Subject Reduction for ⟼ Lemma (2.5.2) shows that standard reduction steps preserve entailment. Hence, since P ⟼^{∗} E[ V^{l} ], there exists some S′ such that ∅ ⊢ E[ V^{l} ] : α, S′ and S ⊧ S′. The derivation of this judgment must contain a sub-derivation concluding:

\frac{Γ ⊢ V : β, S_{V}}{Γ ⊢ V^{l} : β, S_{V} ∪ \{β ≤ l\}} (label)

Except for the rule (let), each application of a constraint derivation rule can only extend the constraint system produced by its sub-derivation. Since definition of evaluation contexts does not contain a clause for let-expressions, there cannot be any let-expressions on the spine from V^{l} to E[ V^{l} ]. Hence S_{V} ∪ {β ≤ l} ⊆ S′.

Since ρ ⊧ S, S ⊧ S′, and S′ ⊇ S_{V} ∪ {β ≤ l}, we have that ρ ⊧ S_{V} ∪ {β ≤ l}. Hence V in ρ(β) by the Value Typing Lemma 2.5.6. But ρ(β) ⊑ ρ(l), hence V in ρ(l), as required.

The proof of the above result relies on the following lemma showing that standard reduction steps preserves the entailment of the derived constraint systems.

Lemma 2.5.2 (Subject Reduction for ⟼). If Γ ⊢ M_{1} : α, S_{1} and M_{1} ⟼ M_{2}, then Γ ⊢ M_{2} : α, S_{2} where S_{1} ⊧ S_{2}.

Proof: Follows from the Subject Reduction Lemma 2.5.3 and the Replacement Lemma 2.5.4.

Lemma 2.5.3 (Subject Reduction for ⟶). If Γ ⊢ M_{1} : α, S_{1} and M_{1} ⟶ M_{2}, then Γ ⊢ M_{2} : α, S_{2} such that S_{1} ⊧ S_{2}.

Proof: See Appendix A.1.

Lemma 2.5.4 (Replacement). If:

1. D is a deduction concluding Γ ⊢ E[ M_{1} ] : α, S_{1},

2. D_{1} is a sub-deduction of D concluding Γ′ ⊢ M_{1} : β, S′_{1},

3. D_{1} occurs in D in the position corresponding to the hole ([ ]) in E, and

4. Γ′ ⊢ M_{2} : β, S′_{2} where S′_{1} ⊧ S′_{2},

then Γ ⊢ E[ M_{2} ] : α, S_{2} where S_{1} ⊧ S_{2}.

Proof: Follows the proof idea of Hindley and Seldin [25:page 181].

The Flow Lemma describes conditions under which we can replace the result set variable returned by the constraint derivation rules.

Lemma 2.5.5 (Flow). If Γ ⊢ M : α, S then for all γ ∈ SetVar, Γ ⊢ M : γ, S′ with S ∪ {α ≤ γ} ⊧ S′.

Proof: See Appendix A.1.

The Value Typing Lemma simply states that any solution to the constraint system for a syntactic value always corresponds to a value set invariant that includes that value.

Lemma 2.5.6 (Value Typing). If Γ ⊢ V : α, S and ρ ⊧ S, then V in ρ(α).

Proof: By considering the two cases V = b and V = (λ^{t}x.M).

2.6 Solving Set Constraints

Every simple constraint system admits the trivial solution ρ^{⊤_{s}} defined by:

ρ^{⊤_{s}}(α) = ⊤_{s}

where ⊤_{s} is recursively defined as:

⊤_{s} = ⟨Const, ⊤_{s}, ⊤_{s}⟩

The domain element ⊤_{s} represents the set of all run-time values, including functions that can take any value as an argument, and return any value as a result.

Lemma 2.6.1 If S is a simple constraint system then ρ^{⊤_{s}} ⊧ S.

Proof: By a case analysis showing that ρ^{⊤_{s}} ⊧ C for any simple constraint C.

Since ⊤_{s} represents all run-time values, this solution is highly approximate and thus utterly useless. Fortunately, simple constraint systems yield many additional solutions that more accurately characterize the value sets of program expressions.

To illustrate this idea, consider the program P = (λ^{t}x.x). According to the constraint derivation rules of figure 2.2, this program yields the constraint system:

{t ≤ α_{P} , dom(α_{P}) ≤ α_{x}, α_{x} ≤ α_{M}, α_{M} ≤ rng(α_{P})}

In addition to the trivial solution ρ^{⊤_{s}}, this constraint system admits a number of other solutions, including:

\begin{aligned}ρ_{1} & = & \{α_{P} ↦ ⟨\{t\}, ⊥, ⊥⟩, α_{x} ↦ ⊥, α_{M} ↦ ⊥\} \\ ρ_{2} & = & \{α_{P} ↦ ⟨\{t\}, ⊤, ⊤⟩, α_{x} ↦ ⊤, α_{M} ↦ ⊤\} \\ ρ_{3} & = & \{α_{P} ↦ ⟨\{t, c_{1}\}, X, X⟩, α_{x} ↦ X, α_{M} ↦ X\} \end{aligned}

where X = ⟨{c_{2}}, ⊥, ⊥⟩, and c_{1} and c_{2} are arbitrary constants. Because we assume P to be the entire program, the function tagged t is never applied, and hence the set of run-time values for x is simply the empty set. The solution ρ_{1} describes this (empty) set of run-time values of x more accurately than either ρ_{2} or ρ_{3}. Yet these three solutions are incomparable under the ordering ⊑, since the ordering models the flow of values through a program, but does not rank set environments according to their accuracy.

Therefore we introduce an alternative ordering ⊑_{s} on D that ranks environments according to their accuracy. This ordering is monotonic in the domain position:

⟨C_{1}, D_{1}, R_{1}⟩ ⊑_{s} ⟨C_{2}, D_{2}, R_{2}⟩ iff C_{1} ⊆ C_{2}, D_{1} ⊑_{s} D_{2}, R_{1} ⊑_{s} R_{2}

The maximal and minimal elements of D under ⊑_{s} are the solutions to the equations:

\begin{aligned}⊤_{s} & = & ⟨Const, ⊤_{s}, ⊤_{s}⟩ \\ ⊥_{s} & = & ⟨∅, ⊥_{s}, ⊥_{s}⟩ \end{aligned}

respectively. The least upper bound and greatest lower bound operations are recursively defined as:

\begin{aligned}⟨C_{1}, D_{1}, R_{1}⟩ ⊔_{s} ⟨C_{2}, D_{2}, R_{2}⟩ & = & ⟨C_{1} ∪ C_{2}, D_{1} ⊔_{s} D_{2}, R_{1} ⊔_{s} R_{2}⟩ \\ ⟨C_{1}, D_{1}, R_{1}⟩ ⊓_{s} ⟨C_{2}, D_{2}, R_{2}⟩ & = & ⟨C_{1} ∩ C_{2}, D_{1} ⊓_{s} D_{2}, R_{1} ⊓_{s} R_{2}⟩ \end{aligned}

Under the ordering ⊑_{s}, a simple constraint system has both a maximal solution (ρ^{⊤_{s}} above) and a minimal solution. The minimal solution exists because the greatest lower bound ⊓_{s} with respect to ⊑_{s} of two solutions is also a solution [24].

Lemma 2.6.2 (Least Solution of Simple Constraint Systems). Every simple constraint system has a solution that is least with respect to ⊑_{s}.

Proof: See Appendix A.2.

Using Lemma 2.6.2, it makes sense to define LeastSoln(S) as the least solution of the simple constraint system S under the ordering ⊑_{s}. Since this solution yields the most accurate invariants consistent with the constraints S, we define set-based analysis as the function that extracts the possible values for each labeled expression from this least solution. Definition 2.6.3. (sba : Λ^{0} ⟶ (Label ⟶ P(Value))) If ∅ ⊢ P : α, S is a most general derivation, then

sba(P)(l) = {V | V in LeastSoln(S)(l)}

By Lemma 2.5.1, sba(P) correctly characterizes the possible value sets for each labeled expression. Theorem 2.6.4 If P ⟼^{∗} E[ V^{l} ] then V ∈ sba(P)(l). Proof: Follows from Lemma 2.5.1.

2.6.1 Computing the Least Solution

To compute sba(P), we derive the most general constraint system for P and close that constraint system under the rules Θ described in figure 2.3. Intuitively, these rules infer all the data-flow paths in the program, which are described by constraints of the form β ≤ γ (for β, γ ∈ SetVar), and propagate values along those dataflow paths. Specifically, the rules (s_{1}), (s_{2}), and (s_{3}) propagate information about constants, function domains and function ranges forward along the data-flow paths of the program. The rule (s_{4}) constructs the data-flow paths from actual to formal parameters for each function call, and the rule (s_{5}) similarly constructs data-flow paths from function bodies to corresponding call sites. We write S ⊢_{Θ} C if S proves C via the rules Θ, and use Θ(S) to denote the closure of S under Θ, i.e., the set {C | S ⊢_{Θ} C}. An algorithm for computing Θ(S) is included in the next section.

This closure process propagates all information concerning the possible constants for labeled expressions into constraints of the form c ≤ l. Hence, we can infer sba(P) from Θ(S) according to the following theorem. Theorem 2.6.5 If P ∈ Λ^{0} and ∅ ⊢ P : α, S is a most general constraint derivation then:

sba(P)(l) = \begin{aligned}& \{b | S ⊢_{Θ} b ≤ l\} \\ ∪ & \{(λ^{t}x.M) | S ⊢_{Θ} t ≤ l\} \end{aligned}

Proof: See Appendix A.2.

\frac{c ≤ β  β ≤ γ}{c ≤ γ}  (s_{1})
\frac{α ≤ rng(β) β ≤ γ}{α ≤ rng(γ)}  (s_{2})
\frac{dom(β) ≤ α β ≤ γ}{dom(γ) ≤ α}  (s_{3})
\frac{α ≤ rng(β) rng(β) ≤ γ}{α ≤ γ}  (s_{4})
\frac{α ≤ dom(β) dom(β) ≤ γ}{α ≤ γ}  (s_{5})

Figure 2.3 The rules Θ = {s_{1}, …, s_{5}}

2.7 An Implementation of Set-Based Analysis

We conclude this chapter with an outline implementation in MzScheme [17] of the analysis described above. The implementation is presented in figures 2.4, 2.5 and 2.6.

2.7.1 Representation of constraint systems

Since the most computationally-intensive part of the analysis is closing the constraint system under the rules Θ, we choose a representation for constraint systems that simplifies this task. If we take a closer look at Θ, we see that each rule in Θ combines a lower and upper bound for some set variable α into a single constraint, where the lower bound on α must be of the form:

c ≤ α β ≤ rng(α) dom(α) ≤ β

and the upper bound on α must be of the form:

α ≤ β β ≤ dom(α) rng(α) ≤ β

We represent the above lower and upper bounds for each set variable α separately. That is, a constraint system is represented as two mappings: one mapping from set variables to their lower bounds, and a second mapping from set variables to their upper bounds. Each kind of lower bound on α corresponds to a structure in the implementation:

                     c ≤ α  c-leq-this
                    β ≤ rng(α)  x-leq-rng-this
                dom(α) ≤ β  dom-this-leq-x

In a similar fashion, each kind of upper bound on α also corresponds to a structure in the implementation:

                    α ≤ β  this-leq-x
                    β ≤ dom(α)  x-leq-dom-this
                rng(α) ≤ β  rng-this-leq-x

2.7.2 Closing constraint systems

Set-based analysis consists of a specification phase and a solution phase. In this implementation, these two phases are co-mingled in that the constraint derivation algorithm keeps the derived constraint system closed under Θ. That is, whenever the constraint derivation algorithm adds a new constraint to the current constraint system, any consequences of the new constraint under Θ are also added to the constraint system.

Constraint systems are extended via the functions add-lower-bound+close! and add-upper-bound+close!. The function combine! checks if a new consequent can be inferred from a lower and upper bound for a set variable.

2.7.3 Deriving constraints

The function derive is a straightforward implementation of the constraint derivation rules described in figure 2.2. This function takes as arguments a constraint derivation context gamma, an expression M , and a constraint system S. The function then extends S with additional constraints and returns a set variable denoting the result value set of M . For simplicity, the implementation does not support let-expressions or constraint schemas, but these are straightforward to add.

;; —— Main analysis function (define (sba M )

(let ([S (create-constraint-system)]) (derive (make-empty-derivation-context) M S) S))

;; —— Abstract syntax structures (define-struct Var (x)) (define-struct Const (b)) (define-struct Lam (t x M )) (define-struct App (fn arg)) (define-struct Labeled (M l))

;; —— Deriving constraints (define (derive gamma M S)

(let ([alpha (gen-set-var)])

(match M

[($ Var x)

(add-upper-bound+close! S (lookup gamma x) (make-this-leq-x alpha))]

[($ Const b)

(add-lower-bound+close! S alpha (make-c-leq-this b))]

[($ Labeled M l)

(let ([beta (derive gamma M S)])

(add-upper-bound+close! S beta (make-this-leq-x l))

(add-upper-bound+close! S beta (make-this-leq-x alpha)))]

[($ Lam t x N )
(let∗ ( [alpha1 (gen-set-var)]

[alpha2 (derive (extend gamma x alpha1 ) N S)]) (add-lower-bound+close! S alpha (make-c-leq-this t)) (add-lower-bound+close! S alpha (make-dom-this-leq-x alpha1 )) (add-lower-bound+close! S alpha (make-x-leq-rng-this alpha2 )))]

[($ App fn arg)
(let ( [beta1 (derive gamma fn S)]

[beta2 (derive gamma arg S)]) (add-upper-bound+close! S beta1 (make-x-leq-dom-this beta2 )) (add-upper-bound+close! S beta1 (make-rng-this-leq-x alpha)))])

alpha))

Figure 2.4 Deriving constraints

;; —— Structures for constraints (define-struct c-leq-this (c)) (define-struct dom-this-leq-x (x)) (define-struct x-leq-rng-this (x))

(define-struct this-leq-x (x)) (define-struct x-leq-dom-this (x)) (define-struct rng-this-leq-x (x))

;; —— Extending and re-closing constraint system ;; For clarity, we have not abstracted over the following two functions (define (add-lower-bound+close! S alpha low-bound)

(unless (has-lower-bound? S alpha low-bound) (add-lower-bound! S alpha low-bound) (for-each

(lambda (up-bound) (combine! S low-bound up-bound))

(upper-bounds S alpha))))

(define (add-upper-bound+close! S alpha up-bound)

(unless (has-upper-bound? S alpha up-bound) (add-upper-bound! S alpha up-bound) (for-each

(lambda (low-bound) (combine! S low-bound up-bound))

(lower-bounds S alpha))))

;; —— Adding consequents of two constraints (define (combine! S low-bound up-bound)

(match (list low-bound up-bound)

;; The following cases applies rules (s1) through (s5), respectively

[(($ c-leq-this ) ($ this-leq-x gamma))

(add-lower-bound+close! S gamma low-bound)]

[(($ dom-this-leq-x ) ($ this-leq-x gamma))

(add-lower-bound+close! S gamma low-bound)]

[(($ x-leq-rng-this ) ($ this-leq-x gamma))

(add-lower-bound+close! S gamma low-bound)]

[(($ x-leq-rng-this alpha) ($ rng-this-leq-x gamma) )

(add-upper-bound+close! S alpha (make-this-leq-x gamma))]

[(($ dom-this-leq-x gamma) ($ x-leq-dom-this alpha) )

(add-upper-bound+close! S alpha (make-this-leq-x gamma))] [ (void)]))

Figure 2.5 Representing, extending and closing a constraint system

;; —— Functions for manipulating constraint systems

(define (gen-set-var) …) ;; Creates a fresh set variable

(define (create-constraint-system) …) ;; Creates an empty constraint system

(define (add-lower-bound! S alpha low-bound) …) ;; Extends the constraint system S with an additional lower bound for alpha

(define (has-lower-bound? S alpha low-bound) …) ;; Checks if the constraint system S already has the given lower bound for alpha

(define (lower-bounds S alpha) …) ;; Returns a list of lower bounds for alpha in the constraint system S

(define (add-upper-bound! S alpha up-bound) …) (define (has-upper-bound? S alpha up-bound) …) (define (upper-bounds S alpha) …) ;; Ditto for upper bounds

;; —— Functions for manipulating derivation contexts

(define (make-empty-derivation-context) …) ;; creates an empty derivation context

(define (extend gamma x alpha) …) ;; extends the derivation context gamma to map x to alpha

(define (lookup gamma x) …) ;; looks up the binding for x in the derivation context gamma

Figure 2.6 Manipulating constraint systems and derivation contexts

Chapter 3

Extending Set-Based Analysis

Realistic programming languages provide a variety of additional facilities on top of the idealized core language Λ. These facilities typically include pairs (or other compound data structures such as C’s structs or Pascal’s records), assignable variables, mutable data structures, and possibly objects, modules and non-local control operators. Since MrSpidey is designed to assist in the development of realistic Scheme programs, we need to extend the underlying set-based analysis to encompass these additional features of practical programming languages. This extension also suggests how MrSpidey can be adapted to other safe languages such as Java.

3.1 Additional Selectors

Most of the additional programming constructs mentioned above introduce additional kinds of values into the language. Modeling these additional values in the analysis requires the introduction of additional selectors into the constraint language and the corresponding extension of the underlying domain D and the set of operations and relations defined on D.

To simplify this process, we first abstract over the collection of selectors in the constraint language. The constraint language currently contains a single monotonic selector, rng, and a single anti-monotonic selector, dom. We generalize the constraint language with two sets, Sel^{+} and Sel^{−}, of monotonic and anti-monotonic selectors, respectively, which are currently defined as the singletons:

Sel^{+} = {rng}
Sel^{−} = {dom}

We use the meta-variables sel^{+}, sel^{−} and sel to range over selectors in Sel^{+}, Sel^{−}, and Sel^{+}∪Sel^{−}, respectively. Expressed in terms of these meta-variables, the language of set expressions becomes:

τ ∈ SetExp = α | c | sel^{+}(τ) | sel^{−}(τ)

and a simple constraint is of the form:

C ∈ SimpleCon = c ≤ β
| α ≤ β
| α ≤ sel^{−}(β)
| sel^{+}(α) ≤ β
| sel^{−}(α) ≤ β
| α ≤ sel^{+}(β)

These constraints have their expected semantics on an extended domain D that contains a product for each selector in the constraint language:

D = P(Const) × \underbrace{D × ⋯ × D}_{sel^{−}∈Sel^{−}} × \underbrace{D × ⋯ × D}_{sel^{+}∈Sel^{+}}

This reformulation simplifies the process of extending the analysis to cope with additional programming constructs. The remainder of the derivation from chapter 2 can be adapted to the modified formulation, mutandis mutatis. In particular, the appropriate inference rules Θ for the modified formulation are described in figure 3.1.

\frac{c ≤ β  β ≤ γ}{c ≤ γ}  (s_{1})
\frac{α ≤ sel^{+}(β) β ≤ γ}{α ≤ sel^{+}(γ)}  (s_{2})
\frac{sel^{−}(β) ≤ α β ≤ γ}{sel^{−}(γ) ≤ α}  (s_{3})
\frac{α ≤ sel^{+}(β) sel^{+}(β) ≤ γ}{α ≤ γ}  (s_{4})
\frac{α ≤ sel^{−}(β) sel^{−}(β) ≤ γ}{α ≤ γ}  (s_{5})

Figure 3.1 The adapted rules Θ = {s_{1}, …, s_{5}}

3.2 Analysis of Pairs

Let Λ^{p} be the following extension of Λ with immutable pairs.

M ∈ Λ^{p}  = …
| (cons M M)
| (car M)
| (cdr M)
V ∈ Value = …
| (cons V V)

3.2.1 Semantics

The additional syntactic forms have their usual Scheme semantics, which we formalize via two additional notions of reduction:

(car (cons V_{1} V_{2})) ⟶ V_{1}  (car)
(cdr (cons V_{1} V_{2})) ⟶ V_{2}  (cdr)

To allow the evaluation of sub-expressions inside the syntactic forms cons, car and cdr, we extend the notion of evaluation contexts as follows:

E = … | (cons E M) | (cons V E) | (car E) | (cdr E)

The standard reduction relation ⟼ and the evaluator eval for the extended language Λ^{p} can now be defined in the usual manner, following section 2.1.2.

3.2.2 Analysis

The analysis of the extended language Λ^{p} requires two additional monotonic selectors

car and cdr:

                        Sel^{+} = {rng, car, cdr}

Sel^{−} = {dom}

These additional selectors yield corresponding products in the domain D. Each element X ∈ D is now a 5-tuple ⟨C, D, R, A_{1}, A_{2}⟩, where the additional components A_{1} and A_{2} describe the possible car and cdr fields of pairs represented by X. We introduce the special tag pair ∈ Const, which denotes that an element of D also represents pairs, and we extend the relation V in X to describe the pairs represented by an element X = ⟨C, D, R, A_{1}, A_{2}⟩ in D as follows:

b in X iff b ∈ C
(λ^{t}x.M) in X iff t ∈ C
(cons V_{1} V_{2}) in X iff pair ∈ C, V_{1} in A_{1}, V_{2} in A_{2}

The constraint derivation rules for the new syntactic forms are described in figure 3.2. The rule (cons) records both the pairs tag and the possible values for each component of the pair. The rules (car) and (cdr) extract the appropriate component from the set variable for the argument expression.

\frac{Γ ⊢ M_{i} : α_{i}, S_{i}}{Γ ⊢ (cons M_{1} M_{2}) : β, S_{1} ∪ S_{2} ∪ \{pair ≤ β, α_{1} ≤ car(β), α_{2} ≤ cdr(β)\}} (cons)
\frac{Γ ⊢ M : α, S}{Γ ⊢ (car M) : β, S ∪ \{car(α) ≤ β\}}  (car)
\frac{Γ ⊢ M : α, S}{Γ ⊢ (cdr M) : β, S ∪ \{cdr(α) ≤ β\}}  (cdr)

Figure 3.2 Constraint derivation rules for pairs

The soundness proof for set-based analysis is easily adapted to the extended language. The Replacement (2.5.4), Value Typing (2.5.6), and Soundness (2.5.1) Lemmas are straightforward to adapt, and we extend the Subject Reduction for ⟶ Lemma (2.5.3) as follows. Lemma 3.2.1 (Subject Reduction for ⟶ on Λ^{p}). If Γ ⊢ M_{1} : α, S_{1} and M_{1} ⟶ M_{2}, then Γ ⊢ M_{2} : α, S_{2} such that S_{1} ⊧ S_{2}. Proof:

The proof proceeds by case analysis according to the relation M_{1} ⟶ M_{2}.

• Suppose M_{1} ⟶ M_{2} via (car). Then:

\begin{aligned}M_{1} & = & (car (cons V_{1} V_{2})) \\ M_{2} & = & V_{1} \end{aligned}

The typing derivation on M_{1} must be of the following form:

\frac{\frac{Γ ⊢ V_{i} : α_{i}, S′_{i}}{Γ ⊢ (cons V_{1} V_{2}) : β, S′_{1} ∪ S′_{2} ∪ S} (cons)}{Γ ⊢ M_{1} : γ, S′_{1} ∪ S′_{2} ∪ S ∪ S′} (car)

where:

S = {t ≤ β, α_{1} ≤ car(β), α_{2} ≤ cdr(β)}
S′ = {car(β) ≤ γ}

Hence S ∪ S′ ⊧ {α_{1} ≤ γ}, and by the Flow Lemma 2.5.5, Γ ⊢ V_{1} : γ, S_{2} where S′_{1} ∪ S ∪ S′ ⊧ S_{2}, as required.

• The case for the reduction rule (cdr) is similar.

The set-based analysis function sba for the extended language Λ^{p} is defined following definition 2.6.3. As in section 2.6, we can compute sba(P) from the closure of S under Θ:

sba(P)(l) = \{b | S ⊢_{Θ} b ≤ l\} ∪ \{(λ^{t}x.M) | S ⊢_{Θ} t ≤ l\} ∪ \{(cons V_{1} V_{2}) | \begin{matrix}S ⊢_{Θ} pair ≤ l, \\ S ⊢_{Θ} α_{1} ≤ car(l), V_{1} ∈ sba(P)(α_{1}) \\ S ⊢_{Θ} α_{2} ≤ cdr(l), V_{2} ∈ sba(P)(α_{2})\} \end{matrix}

3.3 Analysis of First-Class Continuations

Consider the following language Λ^{cc}, which extends Λ^{p} with first-class continuations in addition to functional core language and pairs:

M ∈ Λ^{cc} = … | (abort M) | (callcc^{t} M)

An abort-expression evaluates its sub-expression, and returns the resulting value as the result of the entire computation. The callcc-expression (callcc^{t} M) first evaluates its argument M to a function, then captures the current evaluation context (or continuation) surrounding the expression, and applies the function produced by M to this evaluation context. An invocation of a captured evaluation context causes the current evaluation context to be discarded and replaced by the captured context. Just like a function expression, a callcc-expression has an identifying tag so that MrSpidey can reconstruct the textual source of the corresponding continuation values from the results of the analysis.

3.3.1 Semantics

We define the semantics of the abort and callcc constructs by extending the standard reduction relation with the following rules for aborting and capturing evaluation contexts:

E[ (abort M) ] ⟼ M  (abort)
E[ (callcc^{t} M) ] ⟼ E[ (M (λ^{t}x.(abort E[ x ]))) ]  (callcc)

The evaluator for the extended language is defined in the usual manner, following section 2.1.2.

3.3.2 Analysis

Figure 3.3 introduces the additional derivation rules for abort and callcc expressions. An abort expression never returns, so the derivation rule (abort) introduces a fresh type variable for these expressions. The least solution (under ⊑_{s}) for this type variable is ⊥_{s}, denoting the empty set of values.

The rule (callcc) introduces a new type variable δ to denote the captured continuation. The rule records that:

1. the type variable δ contains the tag t from the callcc expression;

2. δ is the argument to the function (denoted by α) that is returned by M;

3. the result value this function becomes the result of the callcc expression;

4. argument values to δ are also returned as results of the callcc expression.

In addition, the rule adds the “dummy” constraint γ ≤ rng(δ). This dummy constraint is required in order that the constraint derivation rules satisfy the subject reduction lemma. That is, the (callcc) reduction rule produces a contractum containing the syntactic term (λ^{t}x.(abort E[ x ])), which is not present in the (callcc)-redex. Applying the constraint derivation rules to this contractum yields a number of constraints, including the constraint γ ≤ rng(δ), where γ describes the value set for (abort E[ x ]), and δ describes the value set for the λ-expression. The subject reduction lemma requires that this constraint is entailed by the constraint system for the (callcc)-redex. In order to satisfy this requirement, we include that constraint in the redex’s constraint system.

\frac{Γ ⊢ M : α, S}{Γ ⊢ (abort M) : β, S}  (abort)
\frac{Γ ⊢ M : α, S}{Γ ⊢ (callcc^{t} M) : β, S ∪ \{ \begin{matrix}t & ≤ & δ \\ δ & ≤ & dom(α) \\ rng(α) & ≤ & β \\ dom(δ) & ≤ & β \\ γ & ≤ & rng(δ) \end{matrix} \}}  (callcc)

Figure 3.3 Constraint derivation rules for first-class continuations

The Replacement (2.5.4), Value Typing (2.5.6), and Soundness (2.5.1) Lemmas are easily adapted to the extended language. We extend the Subject Reduction for ⟼ Lemma (2.5.2) to account for the additional standard reduction rules as follows.

Lemma 3.3.1 (Subject Reduction for ⟼ on Λ^{cc}). If ∅ ⊢ M_{1} : α, S_{1} and M_{1}⟼M_{2}, then ∅ ⊢ M_{2} : β, S_{2} such that S_{1} ⊧ S_{2}.

Proof: The proof proceeds by case analysis according to the relation M_{1} ⟼ M_{2}. Since the cases for the (β_{v}) and (unlabel) rules are the same as before, we only consider the cases for the additional rules (abort) and (callcc).

• Suppose M_{1} ⟼ M_{2} via (abort). Then:

M_{1} = E[ (abort M_{2}) ]

The derivation on M_{1} must include a sub-derivation concluding Γ ⊢ M_{2} : β, S_{2} where S_{2} ⊆ S_{1}. Since M_{1} is closed, so is M_{2}, and hence ∅ ⊢ M_{2} : β, S_{2}.

• Suppose M_{1} ⟼ M_{2} via (callcc). Then:

M_{1} = E[ (callcc^{t} M) ]
M_{2} = E[ (M (λ^{t}x.(abort E[ x ]))) ]

The derivation on M_{1} must include a sub-derivation concluding:

\frac{Γ ⊢ M : α_{M}, S_{M}}{Γ ⊢ (callcc^{t} M) : β, S_{M} ∪ S_{C}} (callcc)

where:

S_{C} = \{ \begin{matrix}t & ≤ & δ \\ δ & ≤ & dom(α_{M}) \\ rng(α_{M}) & ≤ & β \\ dom(δ) & ≤ & β \\ γ & ≤ & rng(δ) \end{matrix} \}

Let S_{E} be the additional constraints generated by the derivation on M_{1} due to the context E surrounding (callcc^{t} V). Then S_{1} = S_{E} ∪ S_{M} ∪ S_{C}, and the following derivation holds:

\frac{\frac{\frac{Γ ∪ \{x : β\} ⊢ x : β, \{β ≤ β\}}{Γ ∪ \{x : β\} ⊢ E[ x ] : α, S_{E}}}{Γ ∪ \{x : β\} ⊢ (abort E[ x ]) : γ, S_{E}} (abort)}{Γ ⊢ (λ^{t}x.(abort E[ x ])) : δ, S_{L}} (abs)

where:

S_{L} = S_{E} ∪ {t ≤ δ, dom(δ) ≤ β, γ ≤ rng(δ)}

Hence:

Γ ⊢ (M (λ^{t}x.(abort E[ x ]))) : β, S′_{2}

where:

S′_{2} = S_{L} ∪ S_{M} ∪ {δ ≤ dom(α_{M}), rng(α_{M}) ≤ β}

Therefore, by the Replacement Lemma 2.5.4:

Γ ⊢ M_{2} : β′, S_{2}

where:

S_{2} = S_{E} ∪ S′_{2}

Since S_{1} contains S_{2}, S_{1} ⊧ S_{2}, and the lemma holds for this case.

The set-based analysis function sba for the extended language Λ^{cc} is defined as in definition 2.6.3, and can be computed in the usual fashion based on the closure of the derived constraint system under Θ.

3.4 Analysis of Assignable Variables

Next we consider the set-based analysis of a language with assignable variables. Let Λ^{!} be the following extension of Λ^{p}:

M ∈ Λ^{!}  = …  (Expressions)
| (letrec (D^{∗}) M)
| (set! z M)
| z
D ∈ Defines  = (define z V)  (Definitions)
z, w ∈ AssignVar  (Assignable Variables)

The extended language contains assignable variables, in addition to the regular, immutable variables. These assignable variables are introduced by a letrec-expression (letrec (D^{∗}) M), where D^{∗} is a sequence of definitions of the form (define z V). Each assignable variable in these definitions is bound in the entire letrec-expression, and we work with the usual conventions concerning α-renaming for assignable variables. An assignment expression (set! z M) first evaluates M to some value, assigns the variable z to that value, and then returns the value.

3.4.1 Semantics

We evaluate programs within an enclosing letrec containing a heap and an expression. The heap is a sequence of definitions containing all currently defined assignable variables:

H ∈ Heap = D^{∗}

All references and assignments to assignable variables operate on this heap. We use the functional notation H(z) to extract the value bound to z in the heap H.

To allow the evaluation of sub-expressions inside the set! form, we extend the notion of evaluation contexts as follows:

E = … | (set! z E)

We extend the standard reduction relation with the following additional cases for the new syntactic forms. To evaluate an internal letrec, we lift its definitions out into the global heap, ensuring that the appropriate hygiene conditions are satisfied:

(letrec (H) E[ (letrec (D^{∗}) M) ])

⟼ (letrec (H ∪ D^{∗}) E[ M ])  (letrec)
if dom(H) ∩ dom(D^{∗}) = ∅
(letrec (H) E[ z ]) ⟼ (letrec (H) E[ V ]) if H(z) = V  (ref )

(letrec (H ∪ (define z V)) E[ (set! z V′) ])

⟼ (letrec (H ∪ (define z V′)) E[ V′ ])  (set!)

The semantics of the extended language is defined via the partial function eval on programs. This evaluator now returns a pair consisting of a heap and a value, where the heap provides bindings for the assignable variables in the value.

eval : Λ^{0} ⟶_{p} Heap × Value
eval(M) = ⟨H, V ⟩  if (letrec () M) ⟼^{∗} (letrec (H) V)

3.4.2 Analysis

The analysis of the extended language Λ^{!} is based on the additional constraint derivation rules described in figure 3.4. The rule (letrec) extends the derivation context Γ to map each assignable variable z_{i} to a fresh set variable α_{i} and generates constraints for both the defined values and the letrec-body using the extended derivation context. The rule (set!) simply propagates all possible assigned values into the value set for the assigned variable. A constraint derivation context now maps variables to either set variables or constraint schemas, as before, and now also maps assignable variables to set variables.

Adapting the soundness proof for the extended analysis is straightforward. The Replacement (2.5.4), Value Typing (2.5.6), and Soundness (2.5.1) Lemmas are easily adapted to the extended language. It is straightforward to extend the Subject Reduction for ⟼ Lemma (2.5.2) with cases for the additional reduction rules. The set-based analysis function sba for the extended language Λ^{!} can be defined and computed in the usual fashion.

3.5 Analysis of Assignable Boxes

Next, we extend our sample language with assignable boxes, where are somewhat more difficult to analyze than assignable variables. Let Λ^{b} be the following extension

\frac{\begin{matrix}Γ ∪ \{z_{i} : α_{i}\} ⊢ V_{i} : β_{i}, S_{i} \\ Γ ∪ \{z_{i} : α_{i}\} ⊢ M : γ, S \end{matrix}}{Γ ⊢ (letrec ((define z_{1} V_{1}) … (define z_{n} V_{n})) M) : γ, S ∪ S_{1} ∪ ⋯ ∪ S_{n} ∪ \{β_{i} ≤ α_{i} | 1 ≤ i ≤ n\}}  (letrec)

Γ ∪ {z : β} ⊢ z : α, S ∪ {α ≤ β}  (ref )
\frac{Γ ⊢ M : α, S}{Γ ⊢ (set! z M) : α, S ∪ \{α ≤ Γ(z)\}}  (set!)

Figure 3.4 Constraint derivation rules for assignable variables

of Λ^{!}:

M ∈ Λ^{b} = … (Expressions)
| (box M)
| (unbox M)
| (set-box! M M)
V ∈ Value = …  (Values)
| ⟨box z⟩

3.5.1 Semantics

The additional syntactic forms have their usual Scheme semantics. The value ⟨box z⟩ denotes a box containing the value bound to the assignable variable (or location) z. We formalize this semantics by extending the standard reduction relation as follows:

(letrec (H) E[ (box V) ])

⟼ (letrec (H ∪ (define z V)) E[ ⟨box z⟩ ])  (box)
if z ∉ dom(H)

(letrec (H) E[ (unbox ⟨box z⟩) ])

⟼ (letrec (H) E[ V ]) if H(z) = V  (unbox)

(letrec (H ∪ (define z V)) E[ (set-box! ⟨box z⟩ V′) ])

⟼ (letrec (H ∪ (define z V′)) E[ V′ ])  (set-box!)

The rule (box) allocates a new assignable variable, or location, z, that is not already bound in the heap, binds this location to the boxed value in the heap, and returns a new kind of value, ⟨box z⟩ as the result of the box expression. The rules (unbox) and (set-box!) are analogous to the rules (ref ) and (set!) described in the previous section, except that the new rules operate on box values of the form ⟨box z⟩, instead of directly on assignable variables.

To allow the evaluation of sub-expressions inside the syntactic forms box, unbox and set-box!, we extend the notion of evaluation contexts as follows:

E = … | (box E) | (unbox E) | (set-box! E M) | (set-box! V E)

The semantics of the extended language is defined via the partial function eval on programs, in the same manner as in the previous section.

3.5.2 Analysis

The assignable boxes of the extended language Λ^{b} are first-class values. Unlike assignable variables, these boxes can be passed around between various parts of the analyzed program. This flexibility makes assignable boxes significantly more difficult to analyze than assignable variables. ^{∗}

As a first attempt, we could try to analyze boxes by extending the constraint language with an single additional selector, box, such that box(τ) describes the set of values contained in the boxes denoted by τ. Unfortunately, this approach does not work very well. To illustrate the problem with this approach, consider the data-flow path in the analyzed program represented by the constraint α ≤ β. In order to ensure that boxed values flow forward along this data-flow path in the appropriate manner, we need to require that box(α) ≤ box(β), which implies that box is monotonic. But now suppose that a set-box! operation is performed on the value set described by β, thus increasing the set of possible boxed values at β. To insure that this effect is reflected in the boxed values of α, we need to require that box(β) ≤ box(α), which implies box is also anti-monotonic. Hence the constraint α ≤ β can hold if and only if box(α) = box(β). In practice, this means that any two boxed values that reach the same program point are unified. Unfortunately, our experience with Soft Scheme [45] indicates that the results of unification-based analyses are often unintuitive and difficult to explain.

∗We could alternatively define the semantics of the additional syntactic forms in Λ^{b} by macroexpanding them into the following Λ^{!} expressions:

(box M) ⟶ (letrec ([z M]) (cons (λd. z) (λx. (begin (set! z x) x))))

(unbox M) ⟶ ((car M) 1)

(set-box! M_{1} M_{2}) ⟶ ((cdr M_{1}) M_{2})

The analysis of these macro-expanded forms yields results are analogous to that produced by the analysis described in this section for the original forms.

In order to produce a more intuitive and accurate analysis, we introduce the notion of split boxes^{†}, which uses the following two additional selectors for the analysis of boxes:

1. a monotonic selector box^{+} that models how boxed values flow forward along

data-flow paths;

Sel^{+} = {…, box^{+}}

and

2. an anti-monotonic selector box^{−} that models how the values assigned to boxes flow backward along data-flow paths.

Sel^{−} = {…, box^{−}}

Appropriate constraint derivation rules for the new syntactic forms, based on the two selectors box^{+} and box^{−}, are described in figure 3.5. The rule (box) introduces a set variable δ to describe the set of values possibly contained in the newly constructed box. The set expression box^{+}(β) describes values that are contained in the box, and box^{−}(β) describes values that are assigned to the box. Both the initial value of the box (α) and any values assigned to the box (box^{−}(β)) must be contained in δ, and δ is contained in the set of values (box^{+}(β)) that can be extracted from the box. The rules (unbox) and (set-box!) are straightforward.

Proving the soundness of the new analysis is straightforward. The Replacement (2.5.4), Value Typing (2.5.6), and Soundness (2.5.1) Lemmas are easily adapted to the extended language, and the Subject Reduction for ⟼ Lemma (2.5.2) can be extended with cases for the additional reduction rules. The set-based analysis function sba for Λ^{b} is defined and computed in the usual fashion.

†This idea was also independently discovered by Scott Smith and Valerie Trifinov, and by Francois Pottier (private communications, ICFP’96), and earlier by Reynolds [40].

\frac{Γ ⊢ M : α, S}{Γ ⊢ (box M) : β, S ∪ \{ \begin{matrix}α & ≤ & δ \\ box^{−}(β) & ≤ & δ \\ δ & ≤ & box^{+}(β) \end{matrix} \}}  (box)

\frac{Γ ⊢ M : α, S}{Γ ⊢ (unbox M) : β, S ∪ \{box^{+}(α) ≤ β\}}  (unbox)
\frac{Γ ⊢ M_{i} : α_{i}, S_{i}}{Γ ⊢ (set-box! M_{1} M_{2}) : β, S_{1} ∪ S_{2} ∪ \{α_{2} ≤ box^{−}(α_{1}), α_{2} ≤ β\}}  (set-box!)

Figure 3.5 Constraint derivation rules for boxes

3.6 Analysis of Units

Realistic programming languages typically have a module system to help organize large software systems. In MzScheme [17], the module system is based on units [19]. In this section we consider the analysis of a simplified version of MzScheme’s unit system. The language Λ^{u} extends Λ^{!} as follows:

M ∈ Λ^{u}  = …  (Expressions)
| (link^{t} M M)
| (invoke M z)
V ∈ Value = …  (Values)
| (unit^{t} w_{1} D^{∗} M w_{2})

A unit expression (unit^{t} w_{1} D^{∗} M w_{2}) consists of:

1. an identifying tag t;

2. a single imported assignable variable w_{1};

3. a series of definitions D^{∗} binding assignable variables to syntactic values;

4. an expression M that may mutate those assignable variables, if required; and

5. an exported assignable variable w_{2}.

Assignments to the imported variable are syntactically disallowed.

A link clause contains an identifying tag and two sub-expressions. These subexpressions should evaluate to units, which the link clause then combines into a single (compound) unit. Both units and link clauses have identifying tags so that MrSpidey can reconstruct the textual source of various unit values from the results of the analysis. An invoke clause consists of an expression that should evaluate to a unit, and an assignable variable that becomes the imported variable of the unit, after which the definitions in the unit are evaluated in order.

3.6.1 Semantics

We specify the semantics of the new syntactic forms via the reduction rules:

(link^{t} (unit^{t_{1}} w_{1} D_{1}^{∗} M_{1} w_{2}) (unit^{t_{2}} w_{2} D_{2}^{∗} M_{2} w_{3}))

⟶ (unit^{t} w_{1} D_{1}^{∗}.D_{2}^{∗} (begin M_{1} M_{2}) w_{3}) (βlink )

(invoke (unit^{t} z D^{∗} M w) z)

⟶ (letrec (D^{∗}) (begin M w))  (invoke)

The rule (βlink ) for link expressions combines two units to produce a compound unit. The imported variable of the compound unit is the imported variable of the first subunit, the exported variable of the first sub-unit is connected to the imported variable of the second sub-unit, and the exported variable of the second sub-unit becomes the exported variable of the compound unit. The syntax (begin M_{1} M_{2}) is shorthand for ((λ^{t}d.M_{2}) M_{1}), where d ∉ F V [M_{2}]. The rule (invoke) converts a unit value into a letrec-expression, which is then evaluated as described in the previous section.

We augment the definition of evaluation contexts to permit evaluation of the subexpressions in link and invoke forms:

E = … | (link^{t} E M) | (link^{t} V E) | (invoke E z)

This semantics can easily be extended to handle mutually-recursive units by allowing units to have two imported variables, such that a link clause connects the exported variable of the first sub-unit to one of the imported variables of the second unit, and vice-versa.

3.6.2 Analysis

The analysis of the extended language Λ^{u} requires additional selectors ui and ue that extract the imported and exported value sets of a unit:

Sel^{+} = {…, ue}
Sel^{−} = {…, ui}

The additional constraint derivation rules for the new syntactic forms are described in figure 3.6. The rule (unit) for unit expressions introduces a number of additional set variables, including a set variable γ_{1} for the imported variable w_{1}; set variables α_{1}, …, α_{n} for the defined variables z_{1}, …, z_{n}; set variables β_{1}, …, β_{n} for the initial values V_{1}, …, V_{n}; and a set variable γ denoting the result of the unit expression. The rule (unit) then ensures that

• the set variable γ includes the identifying tag t of the unit;

• the imported value set of the unit is contained in the value set of the imported variable;

• the value set of the exported variable w_{2} is contained in the exported value set of the unit; and

• the set variable β_{i} (describing V_{i}) is contained in α_{i} (describing z_{i}).

The rule (link) ensures that the set variable α for the link expression includes the identifying tag t; that the imported value set of the resulting compound unit is contained in the imported value set of the first unit; that the exported value set of the first unit is contained in the imported value set of the second unit; and that the exported value set of the second unit is contained in the exported value set of the resulting compound unit.

The rule (invoke) ensures that the value set of the argument variable is contained in the imported value set of the unit; and that the exported value set of the unit becomes the result value set of the invoke expression.

We extend the relation V in X describing the set of run-time values represented by an element X ∈ D (relative to a given program) with the following additional clause for unit values:

(unit^{t} x D^{∗} M y) in ⟨C, …⟩ iff t ∈ C

\frac{\begin{matrix}Γ′ = Γ ∪ \{w_{1} : γ_{1}, z_{1} : α_{1}, …, z_{n} : α_{n}\} \\ Γ′ ⊢ V_{i} : β_{i}, S_{i} for i = 1, …, n \\ Γ′ ⊢ M : γ_{M}, S_{M} \end{matrix}}{Γ ⊢ (unit^{t} w_{1} (define z_{1} V_{1}) … (define z_{n} V_{n}) M w_{2}) : γ, S_{M} ∪ S_{1} ∪ ⋯ ∪ S_{n} ∪ \{ \begin{matrix}t & ≤ & γ \\ ui(γ) & ≤ & γ_{1} \\ Γ(w_{2}) & ≤ & ue(γ) \\ β_{i} & ≤ & α_{i} & 1 ≤ i ≤ n \end{matrix} \}}  (unit)

\frac{Γ ⊢ M_{i} : β_{i}, S_{i} for i = 1, 2}{Γ ⊢ (link^{t} M_{1} M_{2}) : α, S_{1} ∪ S_{2} ∪ \{ \begin{matrix}t & ≤ & α \\ ui(α) & ≤ & ui(β_{1}) \\ ue(β_{1}) & ≤ & ui(β_{2}) \\ ue(β_{2}) & ≤ & ue(α) \end{matrix} \}}  (link)

\frac{Γ ⊢ M : β, S}{Γ ⊢ (invoke M z) : α, S ∪ \{Γ(z) ≤ ui(β), ue(β) ≤ α\}}  (invoke)

Figure 3.6 Constraint derivation rules for units

The soundness proof for set-based analysis can be adapted to the extended language.

3.7 Analysis of Classes

In this section, we outline the extension of set-based analysis to a simple class system. Let Λ^{c} be the following extension of Λ^{u}:

M ∈ Λ^{c} = …
| (class N (z_{1} … z_{k}) [z_{k+1} V_{k+1}] … [z_{n} V_{n}])

                       | (make-obj M)

| M.z

In the class expression:

(class N (z_{1} … z_{k}) [z_{k+1} V_{k+1}] … [z_{n} V_{n}])

N describes the super-class; z_{1}, …, z_{k} are instance variables inherited from that superclass; and z_{k+1}, …, z_{n} are additional instance variables in the new class. These new instance variables are initialized to the values V_{k+1}, …, V_{n}, respectively.

The special form (make-obj M) creates new objects of the class described by M. Although the make-obj form does not allow arguments to be passed to the class, such arguments can be simulated by extending the class with additional instance variables that are initialized to the appropriate argument values. The special form M.z extracts the value bound to the instance variable z in the object described by M.

3.7.1 Semantics

We do not provide a formal semantics for this class system. Instead, we refer the interested reader to a paper on the formal semantics of a related class system [20].

3.7.2 Analysis

The analysis of programs in Λ^{c} requires that we add a number of additional selectors to the constraint language. For describing the behavior of class values, we introduce an additional, monotonic selector, cl-obj(·), such that cl-obj(τ) describes objects produced by classes in τ.

We also introduce additional selectors for describing the behavior of objects. Objects are similar to the assignable boxes of section 3.5, except that whereas boxes have a single assignable field, an object may have multiple assignable instance variables. The analysis of boxes required two additional selectors, box^{+} and box^{−}, which model how boxed values flow both forward and backward along data-flow paths. In a similar manner, for each instance variable z, we introduce two additional selectors, ivar_{z}^{+} and ivar_{z}^{−}. These additional selectors model how values for an instance variable z of an object flow both forward and backward along the data-flow paths of the object.

The additional constraint derivation rules for classes are described in figure 3.7. The rule (class) is the most complex, and introduces a number of new set variables, which have the following meaning:

• the set variable α_{s} describes the super-class;

• the set variables β_{1}, …, β_{n} describe the value set of the corresponding instance variables z_{1}, …, z_{n};

\frac{\begin{matrix}Γ ⊢ N : α_{s}, S_{s} \\ Γ[z_{1} : β_{1}, …, z_{n} : β_{n}] ⊢ V_{i} : γ_{i}, S_{i} for i = k + 1, …, n \end{matrix}}{Γ ⊢ (class N (z_{1} … z_{k}) [z_{k+1} V_{k+1}] … [z_{n} V_{n}]) : α, S_{s} ∪ S_{k+1} ∪ ⋯ ∪ S_{n} ∪ \{ \begin{matrix}cl-obj(α_{s}) & ≤ & α_{o} \\ ivar_{z_{i}}^{+}(α_{o}) & ≤ & β_{i} \\ β_{i} & ≤ & ivar_{z_{i}}^{−}(α_{o}) \\ γ_{i} & ≤ & β_{i} \\ α_{o} & ≤ & cl-obj(α) \end{matrix} \}}  (class)

\frac{Γ ⊢ M : β, S_{s}}{Γ ⊢ (make-obj M) : α, S ∪ \{cl-obj(β) ≤ α\}}  (make-obj )

\frac{Γ ⊢ M : β, S_{s}}{Γ ⊢ M.z : α, S ∪ \{ivar_{z}^{+}(β) ≤ α\}}  (ivar)

Figure 3.7 Constraint derivation rules for classes

• the set variables γ_{k+1}, …, γ_{n} describe the value set of the corresponding initialization expressions V_{k+1}, …, V_{n}; and

• the set variable α_{o} describes objects of the new class.

The rule (class) first derives constraints for the super-class expression N, and then derives constraints for each initialization expression V_{i} in an appropriate derivation context. It then ensures that:

• that the current object (α_{o}) contains instance variable values defined in the super class (α_{s}), via the constraint cl-obj(α_{s}) ≤ α_{o};

• that the values in β_{i} for the instance variable z_{i} reflect the values from α_{o};

• that the initial value V_{1}, described by γ_{i}, is contained the value set described by β_{i}; and

• that the resulting class, described by α, correctly refers to objects of the new class, which are described by α_{o}.

The rule (make-obj ) extracts the cl-obj(·) component from the set variable describing the class; and the rule (ivar) extracts the instance variable component from the set variable describing the object.

We do not provide a soundness proof for the extended analysis, but we conjecture the Subject Reduction for ⟼ Lemma (2.5.2) could be appropriately extended to the new analysis, based on suitable rewriting semantics for the extended language.

Chapter 4

Using Set-Based Analysis for Static Debugging

The constraint system inferred by set-based analysis provides information about the behavior of the analyzed program. MrSpidey uses this constraint system to:

• compute a compact and intuitive value set invariant, or type, for each expression in the program; and

• identify potentially unsafe program operations.

This chapter describes how this information is inferred from the results of the analysis.

4.1 The Type Language

The simple constraint system computed by set-based analysis is not suitable for presentation to the programmer. Simple constraint systems are well-suited for efficiently representing and manipulating information about a program’s run-time behavior, but are difficult for programmers to interpret, for two reasons.

• The constraints are expressed in terms of “selectors”, instead of the conventional “constructors”, which are familiar to most programmers.

• Simple constraint systems use set variables extensively as indirection pointers. For example, the constraint α ≤ rng(rng(β)) is represented as the simple constraint system {α ≤ rng(γ), γ ≤ rng(β)} with an indirection through γ. This extensive use of indirections makes constraint systems difficult to interpret.

To avoid the need for programmers to interpret constraint systems, MrSpidey uses a conventional type language for communication with programmers. We present the type language in the context of the programming language Λ^{p} described in section 3.2. This type language includes constants, set variables, the empty type ⊥_{s}, functions, pairs, unions and recursive type definitions: see figure 4.1. The scope rules for recursive type definitions are analogous to Scheme’s letrec construct. The notions of free and bound variables in types are defined in the usual manner, and we use Type^{0} to denote the set of closed types.

ω ∈ Type = c
| α
| ⊥_{s}
| (ω →^{T} ω)
| (cons ω ω)
| ω ∪ ω
| (rec ([α_{1} ω_{1}] … [α_{n} ω_{n}]) ω)
T ⊆ FnTag

Figure 4.1 The type language Type.

The semantics of closed types is specified via the meaning function M that maps each closed type into D. The semantics of open types is specified via a related function M_{ρ}, where the additional set environment ρ specifies the meaning of the free variables in the type. These two functions are defined in figure 4.2. The semantics of the types c, α, and ⊥_{s} are straightforward. The type (ω_{1} →^{T} ω_{2}) denotes an element of D with function tags T and whose dom and rng components are described by ω_{1} and ω_{2}, respectively. The type (cons ω_{1} ω_{2}) denotes an element of D with whose car and cdr components are denoted by ω_{1} and ω_{2}, respectively. The type ω_{1}∪ω_{2} denotes the union (or least upper bound) of ω_{1} and ω_{2}. The recursive type (rec ([α_{1} ω_{1}] … [α_{n} ω_{n}]) ω) denotes the element of D described by ω, where each α_{i} is bound to the element denoted by ω_{i}.

4.2 Computing Type Information

MrSpidey infers a type for each program expression from the constraint system S computed by set-based analysis. The least solution LeastSoln(S) of this constraint system is a set environment mapping set variables to elements of the domain D. For each labeled expression M^{l} in the program, LeastSoln(S)(l) describes the set of possible run-time values of M^{l}. To communicate this value set to the programmer,

M[·] : Type^{0} ⟶ D
M[ω] = M_{ρ}[ω]

(the choice of ρ does not affect the defn.)

M_{·}[·] : SetEnv × Type ⟶ D
M_{ρ}[c] = ⟨{c}, ⊥_{s}, ⊥_{s}, ⊥_{s}, ⊥_{s}⟩
M_{ρ}[α] = ρ(α)
M_{ρ}[⊥_{s}] = ⊥_{s}
M_{ρ}[(ω_{1} →^{T} ω_{2})] = ⟨T, ρ(ω_{1}), ρ(ω_{2}), ⊥_{s}, ⊥_{s}⟩
M_{ρ}[(cons ω_{1} ω_{2})] = ⟨{pair}, ⊥_{s}, ⊥_{s}, M_{ρ}[ω_{1}], M_{ρ}[ω_{2}]⟩
M_{ρ}[ω_{1} ∪ ω_{2}] = M_{ρ}[ω_{1}] ⊔_{s} M_{ρ}[ω_{2}]
M_{ρ}[(rec ([α_{1} ω_{1}] … [α_{n} ω_{n}]) ω)] = M_{ρ′}[ω]

where ρ′ = lfp(λρ. ρ[α_{i} ↦ M_{ρ}[ω_{i}]])

under the ordering ⊑_{s}

Figure 4.2 The semantics of types.

MrSpidey computes a type invariant describing LeastSoln(S)(l) from the program’s constraint system. This type invariant is computed in three steps.

Step 1

MrSpidey first uses one of the simplification algorithms from section 6.4 to simplify the constraint system S with respect to the external variable l, while preserving LeastSoln(S)(l).

Step 2

MrSpidey then computes a type from the simplified constraint system according to the function MkType : SimpleConSystem × SetVar ⟶ Type^{0}:

MkType(S, α) = (rec ([α_{1} ω_{1}] … [α_{n} ω_{n}]) α)
where {α_{1}, …, α_{n}} = SetVar(S)
and ω_{i} = MkType′(S, α_{i})

The auxiliary functionMkType′ maps a constraint system S and a set variable α_{i} to an open type that may refer to other set variables from S. The function MkType then links the open types for each set variable in S together in a single rec type, thus producing an appropriate closed type.

The auxiliary function MkType′ : SimpleConSystem × SetVar ⟶ Type is defined as:

MkType′(S, α) = ω_{b} ∪ ω_{p} ∪ ω_{f}
where  ω_{b} = {b ∈ BasicConst | S ⊢_{Θ} b ≤ α}

                           ω_{p} = (cons ω_{car} ω_{cdr})

ω_{car} = {β | S ⊢_{Θ} β ≤ car(α)}
ω_{cdr} = {β | S ⊢_{Θ} β ≤ cdr(α)}
ω_{f} = (ω_{dom} →^{T} ω_{rng})
T = {t ∈ FnTag | S ⊢_{Θ} t ≤ α}
ω_{dom} = {β | S ⊢_{Θ} α_{i} ≤^{∗} δ, β ≤ dom(δ)}
,  ω_{rng} = {β | S ⊢_{Θ} β ≤ rng(α)}

The auxiliary function MkType′ returns a union of three types. The first type ω_{b} describes the basic constants in LeastSoln(S)(α); the second type ω_{p} describes pairs in LeastSoln(S)(α); and the last type ω_{f} describes the function tags and argument and results sets in LeastSoln(S)(α). In the definition above, we use a set of types to denote the corresponding union type, i.e., the set of types {ω_{1}, ω_{2}, ω_{3}} denotes the union type ω_{1} ∪ ω_{2} ∪ ω_{3}, and the empty set denotes the type ⊥_{s}.

The type produced by MkType(S, α) correctly describes LeastSoln(S)(α).

Lemma 4.2.1 (Correctness of MkType). If S is a simple constraint system then:

M[MkType(S, α)] = LeastSoln(S)(α)

Proof: See Appendix B.1.

Step 3

Finally, MrSpidey uses the following reductions on Type to simplify type expressions.

ω ∪ ⊥_{s} ⟶ ω
⊥_{s} ∪ ω ⟶ ω
(cons ⊥_{s} ⊥_{s}) ⟶ ⊥_{s}
(⊥_{s} →^{∅} ⊥_{s}) ⟶ ⊥_{s}
(rec () ω) ⟶ ω
(rec ([α_{1} ω_{1}] … [α_{n} ω_{n}]) ω) ⟶

(rec ([α_{1} ω_{1}] … [α_{i−1} ω_{i−1}][α_{i+1} ω_{i+1}] … [α_{n} ω_{n}]) ω)[α_{i} ↦ ω_{i}]

provided α_{i} ∉ SetVar(ω_{i})

MrSpidey produces a type that is in normal form with respect to these reductions, each of which preserves the meaning of type expressions.

Lemma 4.2.2 (Correctness of Type Reductions). If ω_{1} ⟶ ω_{2} then M_{ρ}[ω_{1}] = M_{ρ}[ω_{2}] for any set environment ρ.

Proof: By case analysis on the reductions ω_{1} ⟶ ω_{2}.

The type produced by this three-step processes provides a compact description of the corresponding value-set invariant, and is more easily understood by the programmer than the original constraint system produced by set-based analysis.

4.3 Identifying Unsafe Operations

Unsafe program operations are a natural starting point in the static debugging process. MrSpidey identifies these unsafe operations using the results of set-based analysis. We consider the problem of identifying unsafe operations in the language Λ^{p}. To identify these unsafe operations, MrSpidey considers in turn each operation in the program.

• Suppose the operation is of the form (car M^{l}). Then MrSpidey considers the set of constants {c | [c ≤ l] ∈ S}, where S is the constraint system for the program closed under Θ. If this constant set only contains the tag pair, then, according to the definition of the relation V in X, the value set invariant for M^{l} contains only pairs. Hence the operation (car M^{l}) is safe, and can never raise an error during an execution.

Conversely, if the constant set contains additional constants such as function tags or basic constants, then the expression M^{l} may return values other than pairs, in which case operation (car M^{l}) is unsafe, since it may raise an error at run-time.

• Operations of the form (cdr M^{l}) are dealt with in a similar manner.

• Suppose the operation is an application of the form (M^{l} N). If the constant set {c | [c ≤ l] ∈ S} for M^{l} only contains function tags, then M^{l} only returns functions, and the application will always succeed. Conversely, if the constant set contains additional constants such as basic constants or the tag pair, then M^{l} may return values other than functions. Hence the application unsafe, and may raise an error at run-time.

Since car, cdr and function application are the only operations in the language that may cause errors in Λ^{p}, the above analysis will identify all unsafe operations.

Appendix E.5 describes how MrSpidey extends this idea to detect unsafe operations in full Scheme.

Chapter 5

User Interface to the Static Debugger

A useful static debugger must fit seamlessly into a programmer’s work pattern, and should provide the programmer with useful information in a natural and easily accessible manner. For these reasons, we integrated MrSpidey with DrScheme, Rice’s program development environment for Scheme.

On demand, MrSpidey analyzes the current project and uses the resulting constraint systems to infer useful static debugging information. Specifically, MrSpidey:

1. identifies unsafe program operations;

2. derives an appropriate type for each program expression; and

3. provides a graphical explanation of each derived invariant.

MrSpidey presents this information to the programmer using program mark-ups. These mark-ups are simple font and color changes that provide information about the analysis results without disturbing the familiar lexical and syntactic structure of the program. Additional information is available via a pop-up menu associated with each marked-up token. The programmer can thus browse through the derived information, and can resume program development based on an improved understanding of the program’s execution behavior.

5.1 Displaying Unsafe Operations

Unsafe program operations that may raise run-time errors are natural starting points in the static debugging process. MrSpidey highlights these unsafe operations via font and color changes. Any primitive operation that may be applied to inappropriate arguments, thus raising a run-time error, is highlighted in red (or underlined on monochrome screens). Conversely, primitive operations that never raise errors are shown in green. Any function definition that may be applied to an incorrect number of arguments is highlighted by displaying the lambda keyword in red (again, underlined on monochrome screens), and any application expression where the function position may yield a non-function is highlighted by displaying the enclosing parentheses in red (or underlined). Figure 5.1 contains an example of each of these three kinds of unsafe operations.

MrSpidey also presents summary information describing each unsafe operation, together with a hyper-link to that operation. The tab key moves the focus forward to the next unsafe operation, and the shift-tab key moves the focus backward to the previous unsafe operation. By using these facilities, the programmer can easily inspect the unsafe operations in a program.

Figure 5.1 Identifying unsafe operations

5.2 Pop-Up Menu

MrSpidey also provides a significant amount of additional information for each expression in the analyzed program. This information cannot be immediately displayed, since it would simply result in “information overload”. Instead, MrSpidey provides this information on a demand-driven basis via a pop-up menu associated with each program variable and expression. Figure 5.2 shows the pop-up menu displayed by clicking on the variable tree. The information available through the menu is described in the following sections.

Figure 5.2 The pop-up menu

5.3 Presenting Type Information

MrSpidey lazily computes a type for each program expression, as described in section 4.2. The selection of the Show Value Set option from an expression’s menu causes MrSpidey to compute the corresponding type, and to display that type in a box inserted to the right of the expression in the buffer. For example, figure 5.3 shows the inferred type for the variable tree.

Figure 5.3 Displaying type information

5.4 The Value Flow Browser

During the constraint derivation phase of the set-based analysis, MrSpidey infers subset constraints of the form [α ≤ β] that describe the flow of values between various points in the program.

Since the type invariant of an expression is derived from the values propagated along the incoming subset constraints to that expression, the collection of all subset constraints for a program provides an explanation of the derivation of type invariants for that program. MrSpidey can display each subset constraint as an arrow overlaid on the program text. Because a large numbers of arrows would clutter the program text, these arrows are presented in a demand-driven fashion. The Parent option in the pop-up menu for an expression allows the programmer to view incoming edges for that expression in the value-flow graph. For example, figure 5.4 shows the incoming edges for the parameter tree.

Hyper-links associated with the head and tail of each arrow provide a fast means of navigating through textually distinct but semantically related parts of the program, which is especially useful on large programs. Clicking on the head of an arrow moves the focus to the term at the tail of the arrow, and vice versa.

Figure 5.4 Value source information

Using these facilities, a programmer who encounters a surprising value set invariant can proceed in an iterative fashion to expose arrows that describe the derivation of that invariant. To expedite this iterative process, MrSpidey also provides an Ancestors facility that automatically exposes all portions of the value flow graph that influence a particular invariant, thus providing the programmer with a complete explanation of the derivation of that invariant. For example, figure 5.5 shows the ancestors of the argument variable tree.

In some cases, the number of arrows presented by the ancestor facility is excessive. Since the programmer is typically only interested in a particular class of values, MrSpidey incorporates a filter facility that allows the programmer to restrict the displayed arrows to those that affect the flow of certain kinds of values. This facility is extremely useful for quickly understanding why a primitive operation may be applied to inappropriate argument values. Figure 5.6 shows how to configure the filter facility to consider only values corresponding to a particular constructor.

By using an appropriate combination of the ancestor and filter facilities, the programmer can quickly view the flow of a particular class of value through the program.

Figure 5.5 Ancestors of tree

Figure 5.6 Configuring the filter facility

For example, figure 5.7 shows the derivation of the nil component in the value set invariant for tree.

Finally, MrSpidey also provides Children and Descendants options on the pop-up menu for each expression. These options allow the programmer to view possible uses of the expression’s return value.

Figure 5.7 Flow of nil

5.5 A Sample Debugging Session

To illustrate how the explanatory capabilities of MrSpidey can be used to identify and eliminate bugs, we describe how this tool could be used on the program sum.ss. When MrSpidey is invoked, it highlights the primitive operation car as unsafe (see Figure 5.1), indicating that this operation may raise a run-time error. Inspecting the type invariant for the operation argument, tree, shows that this set includes the inappropriate argument nil (see Figure 5.3). By using the ancestor and filter facilities, we can view how this erroneous value flows through the program, resulting in the display shown in figure 5.7. The displayed information makes it obvious that the error is caused by application of sum to the ill-formed tree (cons (cons nil 1) 2).

Although the example program sum presented in this section is trivial, it does provide a good example of the explanatory capabilities of MrSpidey. Before we can discuss how MrSpidey’s explanatory capabilities scale to significantly larger programs, we must first deal with the problem of analyzing those larger programs, which is the topic of the following two chapters.

Chapter 6

Constraint Simplification

The traditional set-based analysis described in chapters 2 and 3 has proven highly effective for programs of up to a couple of thousand lines of code. Unfortunately, it is useless for larger programs due to its nature as a whole-program analysis and due to the size of the constraint systems it produces, which are quadratic in the size of (large) programs. Storing and manipulating these constraint systems can be extremely expensive.

To overcome this problem, we have developed algorithms for simplifying constraint systems. A simplified version of a constraint system contains significantly fewer constraints, yet still preserves the essential characteristics of the original system. Applying these simplification algorithms at strategic points during the constraint derivation, e.g., to the constraint system for a module definition or a polymorphic function definition, significantly reduces both the time and space required by the overall analysis.

The following section shows that constraint simplification does not affect the analysis results, provided the simplified system is observably equivalent to the original system. Section 6.2 presents a proof-theoretic formulation of observable equivalence, and section 6.3 exploits this formulation to develop a complete algorithm for deciding the observable equivalence of constraint systems. The insights provided by this theoretical development lead to the practical constraint simplification algorithms of section 6.4.

6.1 Conditions for Constraint Simplification

Let us consider a program P containing a program component M, where M may be a module definition or a polymorphic function definition. Suppose the constraint derivations for M concludes:

Γ ⊢ M : α, S_{1}

where S_{1} is the constraint system for M. Our goal is to replace S_{1} by a simpler constraint system, say S_{2}, without changing the results of the analysis.

Let the context surrounding M be C, i.e., P = C[M]. Since the constraint derivation process is compositional, the constraint derivation for the entire program concludes:

∅ ⊢ P : β, S_{C} ∪ S_{1}

where S_{C} is the constraint system for C. The union of the sets S_{C} and S_{1} describes the space of solutions for the entire program, which is the same as the intersection of the two respective solution spaces:

Soln(S_{C} ∪ S_{1}) = Soln(S_{C}) ∩ Soln(S_{1})

Hence Soln(S_{1}) describes at least all the properties of S_{1} relevant to the analysis, but it may also describe solutions for set variables that are not relevant to the analysis. In particular:

• sba(P) only references the solutions for label variables; and

• an inspection of the constraint derivation rules shows that the only interactions between S_{C} and S_{1} are due to the set variables in {α} ∪ F V [range(Γ)].

In short, the only properties of S_{1} relevant to the analysis is the solution space for its external set variables:

E = Label ∪ {α} ∪ F V [range(Γ)]

For our original problem, this means that we want a constraint system S_{2} whose solution space restricted to E is equivalent to that of S_{1} restricted to E:

Soln(S_{1}) |_{E} = Soln(S_{2}) |_{E}

or, with the notation from section 2.2, S_{1} and S_{2} are observably equivalent on E:

S_{1} ≅_{E} S_{2} .

We can translate this compaction idea into an additional rule for the constraint derivation system:

\frac{Γ ⊢≅ M : α, S_{1} S_{1} ≅_{E} S_{2} where E = Label ∪ F V [range(Γ)] ∪ \{α\}}{Γ ⊢≅ M : α, S_{2}}  (≅)

This rule is admissible in that any derivation (denoted using ⊢≅) in the extended constraint derivation system produces information that is equivalent to the information produced by the original analysis. Lemma 6.1.1 (Admissibility of (≅)). If ∅ ⊢≅ P : α, S is a most general constraint derivation then:

sba(P)(l) = const(LeastSoln(S)(l))

Proof: See Appendix C.1.

6.2 The Proof Theory of Observable Equivalence

Since the new derivation rule (≅) involves the semantic notion of observably equivalent constraint systems, it cannot be used in an algorithmic manner. To make this rule useful, we must first reformulate the observable equivalence relation (or some conservative approximation thereof) as a syntactic proof system.

The key properties of the observational equivalence relation are reflections of the reflexivity and transitivity of the ordering relation (⊑) and the monotonicity and anti-monotonicity of the functions rng and dom, respectively. We can reify these properties into a syntactic proof system via the following inference rules Δ:

α ≤ α (reflex)  \frac{τ_{1} ≤ τ τ ≤ τ_{2}}{τ_{1} ≤ τ_{2}} (trans_{τ})  \frac{κ_{1} ≤ κ_{2}}{rng(κ_{1}) ≤ rng(κ_{2}) dom(κ_{2}) ≤ dom(κ_{1})} (compat)

The meta-variables κ, κ_{1}, κ_{2} range over non-constant set expressions:

κ, κ_{1}, κ_{2} = α | dom(κ) | rng(κ)

This restriction avoids inferring useless tautologies. For example, without this restriction, the constraint c ≤ α would yield the constraint rng(c) ≤ rng(α) via (compat), which is a tautology since rng(c) = ⊥.

The rules (reflex) and (trans_{τ}) capture the reflexivity and transitivity of the ordering relation ⊑; (compat) reflects the monotonicity and anti-monotonicity of the functions rng and dom, respectively. Since many of the inferred constraints lie outside of the original language of simple constraints, we define an extended compound constraint language that includes all of the inferred constraints:

C ∈ CmpdConstraint = c ≤ κ | κ ≤ κ
S ∈ CmpdConSystem = P_{fin}(CmpdConstraint)

We use the boldface roman letters C and S as meta-variables ranging over compound constraints and compound constraint systems, respectively.

The proof system Δ completely captures the relevant properties of the ordering ⊑ and the functions rng and dom. That is, Δ is both sound and complete.

Lemma 6.2.1 (Soundness and Completeness of Δ). For a compound constraint system S and a compound constraint C:

S ⊢_{Δ} C ⟺ S ⊧ C

Proof: See Appendix C.2.

This lemma implies that Δ(S) contains exactly those compound constraints that hold in all environments in Soln(S). Hence, if we consider a collection of external set variables E, then Δ(S) |_{E} contains all compound constraints that hold in all environments in Soln(S) |_{E}. Therefore the following lemma holds.

Lemma 6.2.2 For a compound constraint system S, S ≅_{E} Δ(S) |_{E}.

Proof: See Appendix C.2.

We could use this result to define a proof-theoretic equivalent of restricted entailment as follows:

S_{1} ⊢_{Δ}^{E} S_{2} if and only if Δ(S_{1}) |_{E} ⊇ Δ(S_{2}) |_{E}

and then show that S_{1} ⊢_{Δ}^{E} S_{2} if and only if S_{1} ⊧_{E} S_{2}. However, this definition based on the proof system Δ does not lend itself to an efficient implementation. Specifically, checking if two potential antecedents of (trans_{τ}) contain the same set expression τ involves comparing two potentially large set expressions. Hence we develop an alternative proof system that is more suitable for an implementation, yet infers the same constraints as Δ.

The alternative system consists of the inference rules Ψ described in figure 6.1, together with the rules Θ from figure 2.3. The rules (compose_{1...4}) of Ψ replace a reference to a set variable by an upper or lower (non-constant) bound for that variable, as appropriate. The rules (reflex) and (compat) of Ψ are as described above. The rule (trans_{α}) of Ψ provides a weaker characterization of transitivity than the previous rule (trans_{τ}), but, provided we start from with a simple constraint system, the additional rules, Θ and (compose_{1...4}), compensate for this weakness. That is,

\frac{α ≤ rng(β) β ≤ κ}{α ≤ rng(κ)}  (compose_{1})
\frac{α ≤ dom(β) β ≥ κ}{α ≤ dom(κ)}  (compose_{2})
\frac{α ≥ rng(β) β ≥ κ}{α ≥ rng(κ)}  (compose_{3})
\frac{α ≥ dom(β) β ≤ κ}{α ≥ dom(κ)}  (compose_{4})
α ≤ α  (reflex)
\frac{τ_{1} ≤ α α ≤ τ_{2}}{τ_{1} ≤ τ_{2}}  (trans_{α})
\frac{κ_{1} ≤ κ_{2}}{rng(κ_{1}) ≤ rng(κ_{2}) dom(κ_{2}) ≤ dom(κ_{1})}  (compat)

Figure 6.1 The inference rule system Ψ

suitable combinations of these additional rules allow us to infer any constraint that could be inferred by the rule (trans_{τ}). Lemma 6.2.3 (Equivalence of Proof Systems). For a simple constraint system S:

Δ(S) = ΨΘ(S)

Proof: See Appendix C.2.

We could use this result to define a proof-theoretic equivalent of restricted entailment as follows:

S_{1} ⊢_{ΨΘ}^{E} S_{2} if and only if ΨΘ(S_{1}) |_{E} ⊇ ΨΘ(S_{2}) |_{E}

and then show that S_{1} ⊢_{ΨΘ}^{E} S_{2} if and only if S_{1} ⊧_{E} S_{2}. However, this definition is needlessly inefficient. Because (compat) does not eliminate any variables, any (compat)-consequent in ΨΘ(S_{2}) |_{E} is subsumed by its antecedent. If we define:

Π = Ψ \ {compat}

then this argument implies that ΨΘ(S_{2}) |_{E} ≅ ΠΘ(S_{2}) |_{E}. Hence we get the following lemma.

Lemma 6.2.4 ΨΘ(S) |_{E} ≅ ΠΘ(S) |_{E}.

Proof: See Appendix C.2.

Together, Lemmas 6.2.2, 6.2.3 and 6.2.4 provide the basis to introduce prooftheoretic equivalents of restricted entailment and observable equivalence. Definition 6.2.5. (⊢_{ΨΘ}^{E}, =_{ΨΘ}^{E})

• S_{1} ⊢_{ΨΘ}^{E} S_{2} if and only if ΨΘ(S_{1}) |_{E} ⊇ ΠΘ(S_{2}) |_{E},

• S_{1} =_{ΨΘ}^{E} S_{2} if and only if S_{1} ⊢_{ΨΘ}^{E} S_{2} and S_{2} ⊢_{ΨΘ}^{E} S_{1}.

The two relations ⊢_{ΨΘ}^{E} and =_{ΨΘ}^{E} completely characterize restricted entailment and observable equivalence of constraint systems.

Theorem 6.2.6 (Soundness and Completeness of ⊢_{ΨΘ}^{E} and =_{ΨΘ}^{E}).

1. S_{1} ⊢_{ΨΘ}^{E} S_{2} if and only if S_{1} ⊧_{E} S_{2}.

2. S_{1} =_{ΨΘ}^{E} S_{2} if and only if S_{1} ≅_{E} S_{2}.

Proof: See Appendix C.2.

6.3 Deciding Observable Equivalence

While the relation =_{ΨΘ}^{E} completely characterizes the model-theoretic observable equivalence relation ≅_{E}, an implementation of the extended constraint derivation system needs a decision algorithm for =_{ΨΘ}^{E}.

Given two simple constraint systems S_{1} and S_{2}, this algorithm needs to verify that ΨΘ(S_{1}) |_{E} = ΨΘ(S_{2}) |_{E}. If S_{1} and S_{2} are first closed under Θ, then the algorithm only needs to verify that Ψ(S_{1}) |_{E} = Ψ(S_{2}) |_{E}. The naive approach to enumerate and to compare the two constraint systems Ψ(S_{1}) |_{E} and Ψ(S_{2}) |_{E} does not work, since they are typically infinite. For example, if S = {α ≤ rng(α)}, then Ψ(S) is the infinite set {α ≤ rng(α), α ≤ rng(rng(α)), …}.

Fortunately, the infinite constraint systems inferred by Ψ exhibit a regular structure, which we exploit to decide observable equivalence as follows:

1. We generate regular grammars describing the upper and lower bounds for each set variable.

2. We extend these regular grammars to regular tree grammars (RTGs) describing all constraints in Π(S_{1}) |_{E} and Π(S_{2}) |_{E}. This representation allows us to use a standard RTG containment algorithm to decide if Π(S_{1}) |_{E} ⊇ Π(S_{2}) |_{E}.

3. Based on the RTG containment algorithm, we develop an extended algorithm that decides the more difficult entailment question Ψ(S_{1}) |_{E} ⊇ Π(S_{2}) |_{E} by allowing for the additional (compat) inferences on S_{1}.

By checking entailment in both directions, we can decide if two constraint systems are observably equivalent. These steps are described in more detail below.

6.3.1 Regular Grammars

Our first step is to describe, for each set variable α in a simple constraint system S, the following two languages of the lower and upper non-constant bounds of α:

{κ | [κ ≤ α] ∈ Π(S) and SetVar(κ) ⊆ E}
{κ | [α ≤ κ] ∈ Π(S) and SetVar(κ) ⊆ E}

These languages are generated by a regular grammar. For each set variable α, the grammar contains the non-terminals α_{L} and α_{U}, which generate the above lower and upper bounds of α, respectively.

To illustrate this idea consider the program component P = (λ^{g}y.((λ^{f}x.1) y)), where f and g are function tags, and take E = {α^{P} }. The constraint system S_{P} for P (closed under Θ) is described in figure 6.2, together with the productions in the corresponding regular grammar. This grammar describes the upper and lower nonconstant bounds for each set variable in Π(S_{P}) |_{E}. For example, the productions:

\begin{matrix}α_{L}^{x} & ↦ & α_{L}^{r} \\ α_{L}^{r} & ↦ & dom(α_{U}^{P}) \\ α_{U}^{P} & ↦ & α^{P} \end{matrix}

imply that α_{L}^{x} ↦^{∗} dom(α_{P}). This lower bound for x means that the value set for x must include all values to which the function P is applied.

Additional productions

Constraints S^{P}

Grammar G_{r}(S_{P} , E)

in G_{t}(S_{P} , E)
f ≤ α^{f}  R ↦ [f ≤ α_{U}^{f}]
dom(α^{f}) ≤ α^{x}  α_{L}^{x} ↦ dom(α_{U}^{f})
1 ≤ α^{1}  R ↦ [1 ≤ α_{U}^{1}]
α^{1} ≤ rng(α^{f}) α_{U}^{1} ↦ rng(α_{U}^{f})
rng(α^{f}) ≤ α^{a}  α_{L}^{a} ↦ rng(α_{L}^{f})
α^{y} ≤ α^{r} α_{U}^{y} ↦ α_{U}^{r} α_{L}^{r} ↦ α_{L}^{y}
α^{r} ≤ dom(α^{f}) α_{U}^{r} ↦ dom(α_{L}^{f})
g ≤ α^{P}  R ↦ [g ≤ α_{U}^{P}]
dom(α^{P}) ≤ α^{y}  α_{L}^{y} ↦ dom(α_{U}^{P})
α^{a} ≤ rng(α^{P}) α_{U}^{a} ↦ rng(α_{U}^{P})
α^{r} ≤ α^{x}  α_{U}^{r} ↦ α_{U}^{x}  α_{L}^{x} ↦ α_{L}^{r}
α^{1} ≤ α^{a}  α_{U}^{1} ↦ α_{U}^{a}  α_{L}^{a} ↦ α_{L}^{1}
1 ≤ α^{a}  R ↦ [1 ≤ α_{U}^{a}]
α_{L}^{P} ↦ α^{P}  α_{U}^{P} ↦ α^{P} R ↦ [α_{L} ≤ α_{U}] ∀α ∈ SetVar(S_{P})

Figure 6.2 The constraint system, regular grammar, and regular tree grammar for P = (λ^{g}y.((λ^{f}x.1) y))

The productions of the grammar are determined by S_{P} and Π. For example, the constraint [α^{1} ≤ rng(α^{f})] ∈ S_{P} implies that for each upper bound κ of α^{f}, the rule (compose_{1}) infers the upper bound rng(κ) of α^{1}. Since, by induction, α^{f}’s upper bounds are generated by α_{U}^{f}, the production α_{U}^{1} ↦ rng(α_{U}^{f}) generates the corresponding upper bounds of α^{1}.

More generally, the collection of productions:

{α_{U} ↦ rng(β_{U}) | [α ≤ rng(β)] ∈ S}

describes all bounds inferred via (compose_{1}) on a simple constraint system S. Bounds inferred via the remaining (compose) rules can be described in a similar manner. Bounds inferred via the rule (reflex) imply the productions α_{U} ↦ α and α_{L} ↦ α for α ∈ E. Finally, consider the rule (trans_{α}), and suppose this rule infers an upper bound τ on α. This bound must be inferred from an upper bound τ on β, using the additional antecedent [α ≤ β]. Hence the productions {α_{U} ↦ β_{U} | [α ≤ β] ∈ S} generate all upper bounds inferred via (trans_{α}). In a similar fashion, the productions {β_{L} ↦ α_{L} | [α ≤ β] ∈ S} generate all lower bounds inferred via (trans_{α}). Definition 6.3.1. (Regular Grammar G_{r}(S, E)) Let S be a simple constraint system and E a collection of set variables. The regular grammar G_{r}(S, E) consists of the non-terminals {α_{L}, α_{U} | α ∈ SetVar(S)} and the following productions:

α_{U} ↦ α, α_{L} ↦ α  ∀ α ∈ E
α_{U} ↦ β_{U}, β_{L} ↦ α_{L}  ∀ [α ≤ β] ∈ S
α_{U} ↦ dom(β_{L})  ∀ [α ≤ dom(β)] ∈ S
α_{U} ↦ rng(β_{U})  ∀ [α ≤ rng(β)] ∈ S
β_{L} ↦ dom(α_{U})  ∀ [dom(α) ≤ β] ∈ S
β_{L} ↦ rng(α_{L})  ∀ [rng(α) ≤ β] ∈ S

The grammar G_{r}(S, E) generates two languages for each set variable that describe the upper and lower non-constant bounds for that set variable. Specifically, if ↦_{G}^{∗} denotes a derivation in the grammar G, and L_{G}(x) denotes the language {τ | x ↦_{G}^{∗} τ} generated by a non-terminal x, then the following lemma holds.

Lemma 6.3.2 Let G = G_{r}(S, E). Then:

L_{G}(α_{L}) = {κ | [κ ≤ α] ∈ Π(S) and SetVar(κ) ⊆ E}
L_{G}(α_{U}) = {κ | [α ≤ κ] ∈ Π(S) and SetVar(κ) ⊆ E}

Proof: See Appendix C.3.

6.3.2 Regular Tree Grammars

The grammar G_{r}(S, E) does not describe all constraints in Π(S) |_{E}. In particular:

• G_{r}(S, E) does not describe constraints of the form [c ≤ τ]. Thus, for example, the regular grammar for the example program component P does not describe the constraint [1 ≤ rng(α^{P})] in Π(S_{P}) |_{E}.

• G_{r}(S, E) does not describe constraints inferred by the (trans_{α}) rule that are not bounds of the form [κ ≤ α] or [α ≤ κ]. To illustrate this idea, consider the program Q = (λ^{t}x.x) whose constraint system is:

S_{Q} = {t ≤ α^{Q}, dom(α^{Q}) ≤ α^{x}, α^{x} ≤ rng(α^{Q})} .

The regular grammar G_{r}(S_{Q}, E) for Q describes the constraints {dom(α^{Q}) ≤ α^{x}, α^{x} ≤ rng(α^{Q})} in Π(S_{Q}) |_{E}, but it does not describe the trans_{α} consequent [dom(α^{Q}) ≤ rng(α^{Q})] of those constraints, which is also in Π(S_{Q}) |_{E}.

For an arbitrary constraint system S, we represent the constraint system Π(S) |_{E} by extending the grammar G_{r}(S, E) to a regular tree grammar G_{t}(S, E). The extended grammar combines upper and lower bounds for set variables in the same fashion as the (trans_{α}) rule, and also generates constraints of the form [c ≤ τ] where appropriate. Definition 6.3.3. (Regular Tree Grammar G_{t}(S, E)) The regular tree grammar G_{t}(S, E) extends the grammar G_{r}(S, E) with the root non-terminal R and the additional productions:

\begin{matrix}R ↦ [α_{L} ≤ α_{U}] & ∀ α ∈ SetVar(S) \\ R ↦ [c ≤ α_{U}] & ∀ [c ≤ α] ∈ S \end{matrix}

where [· ≤ ·] is viewed as a binary constructor.

The extended regular tree grammar G_{t}(S, E) describes all constraints in Π(S) |_{E}.

Lemma 6.3.4 Let G = G_{t}(S, E). Then Π(S) |_{E} = L_{G}(R).

Proof: See Appendix C.3.

The grammar G_{t}(S_{P} , E) for the example program component P is described in figure 6.2. This grammar yields all constraints in Π(S_{P}) |_{E}. For example, the productions:

R ↦ [1 ≤ α_{U}^{a}] α_{U}^{a} ↦ rng(α_{U}^{P}) α_{U}^{P} ↦ α^{P}

imply that R ↦^{∗} [1 ≤ rng(α^{P})], or that the constant 1 is returned as a possible result of the function P.

6.3.3 Staging

Before we can exploit the grammar representation of Π(S) |_{E}, we must prove that the closure under Θ ∪ Π ∪ {compat} can be performed in a staged manner. The following lemma justifies this staging of the closure algorithm. In particular, it states that Π does not create any additional opportunities for rules in Θ, and (compat) does not create any additional opportunities for Π or Θ.

Lemma 6.3.5 (Staging). For any simple constraint system S:

ΨΘ(S) = Ψ(Θ(S)) = compat(Π(Θ(S)))

Proof: See Appendix C.3.

6.3.4 The Entailment Algorithm

We can check entailment based on lemmas 6.3.4 and 6.3.5 as follows. Given S_{1} and S_{2}, we close them under Θ and then have:

S_{2} ⊢_{ΨΘ}^{E} S_{1}
⟺ ΨΘ(S_{2}) |_{E} ⊇ ΠΘ(S_{1}) |_{E}  by defn ⊢_{ΨΘ}^{E}
⟺ Ψ(Θ(S_{2})) |_{E} ⊇ Π(Θ(S_{1})) |_{E} by lemma 6.3.5
⟺ Ψ(S_{2}) |_{E} ⊇ Π(S_{1}) |_{E} as S_{i} = Θ(S_{i})
⟺ compat(Π(S_{2}) |_{E}) ⊇ Π(S_{1}) |_{E} by lemma 6.3.5
⟺ compat(L_{G_{2}}(R)) ⊇ L_{G_{1}}(R) by lemma 6.3.4
where G_{i} = G_{t}(S_{i}, E)

The containment question:

L_{G_{2}}(R) ⊇ L_{G_{1}}(R)

can be decided via a standard RTG containment algorithm [21]. To decide the more difficult question:

compat(L_{G_{2}}(R)) ⊇ L_{G_{1}}(R)

we extend the RTG containment algorithm to allow for constraints inferred via (compat) on the language L_{G_{2}}(R).

The extended algorithm is presented in figure 6.3. It first computes the largest relation R_{S_{1},S_{2}} such that R_{S_{1},S_{2}}[α_{L}, β_{U}, C, D] holds if and only if:

L([α_{L} ≤ β_{U}]) ⊆ compat(L(C)) ∪ L(D)

where α_{L}, β_{U} describe collections of types; C, D describe collections of constraints; and L([α_{L} ≤ β_{U}]) denotes the language {[τ_{L} ≤ τ_{U}] | α_{L} ↦^{∗} τ_{L}, β_{U} ↦^{∗} τ_{U}}. The first case in the definition of R uses an RTG containment algorithm to detect if L([α_{L} ≤ β_{U}]) ⊆ L(C) ∪ L(D). The two remaining cases handle constraints of the form [rng(α′_{L}) ≤ rng(β′_{U})] or [dom(α′_{U}) ≤ dom(β′_{L})], and allow for inferences via The Entailment Algorithm

In the following, P_{fin} denotes the finite power-set constructor. Let:

G_{1} = G_{t}(S_{1}, E)_{G_{2} = G_{t}(S_{2}, E)} L_{i} = {α_{L} | α ∈ SetVar(S_{i})}

U_{i} = {α_{U} | α ∈ SetVar(S_{i})}

Let G_{1} and G_{2} be pre-processed to remove ϵ-transitions. For C ∈ P_{fin}(L_{2} × U_{2}), define:

L_{G_{2}}(C) = {[τ_{L} ≤ τ_{U}] | ⟨α_{L}, β_{U}⟩ ∈ C, α_{L} ↦_{G_{2}} τ_{L}, β_{U} ↦_{G_{2}} τ_{U}}

The relation R_{S_{1},S_{2}}[·, ·, ·, ·] is defined as the largest relation on

L_{1} × U_{1} × P_{fin}(L_{2} × U_{2}) × P_{fin}(L_{2} × U_{2})

such that if:

R_{S_{1},S_{2}}[α_{L}, β_{U}, C, D]
α_{L} ↦_{G_{1}} X
β_{U} ↦_{G_{1}} Y

then one of the following cases hold:

1. L_{G_{1}}([X ≤ Y]) ⊆ L_{G_{2}}(C ∪ D).

2. X = rng(α′_{L}), Y = rng(β′_{U}) and R_{S_{1},S_{2}}[α′_{L}, β′_{U}, C, D′], where D′ = {⟨γ′_{L}, δ′_{U}⟩ | ⟨γ_{L}, δ_{U}⟩ ∈ C ∪ D, γ_{L} ↦_{G_{2}} rng(γ′_{L}), δ_{U} ↦_{G_{2}} rng(δ′_{U})}

3. X = dom(α′_{U}), Y = dom(β′_{L}) and R_{S_{1},S_{2}}[β′_{L}, α′_{U}, C, D′], where D′ = {⟨δ′_{L}, γ′_{U}⟩ | ⟨γ_{L}, δ_{U}⟩ ∈ C ∪ D, γ_{L} ↦_{G_{2}} dom(γ′_{U}), δ_{U} ↦_{G_{2}} dom(δ′_{L})}

4. In no other cases does R_{S_{1},S_{2}}[α_{L}, β_{U}, C, D] hold. The computable entailment relation S_{2} ⊢_{alg}^{E} S_{1} holds if and only if:

1. ∀R ↦_{G_{1}} [α_{L} ≤ α_{U}]. R_{S_{1},S_{2}}[α_{L}, α_{U}, {⟨γ_{L}, γ_{U}⟩ | γ ∈ SetVar(S_{2})}, ∅], and 2. ∀R ↦_{G_{1}} [c ≤ α_{U}]. L_{G_{1}}(α_{U}) ⊆ L_{G_{2}}({γ_{U} | R ↦_{G_{2}} [c ≤ γ_{U}]}).

Figure 6.3 The computable entailment relation ⊢_{alg}^{E} (compat). The relation R can be computed by starting with a maximal relation (true at every point), and then iteratively setting entries to false, until the largest relation satisfying the definition is reached.

Based on this relation, the algorithm then defines a computable entailment relation ⊢_{alg}^{E} on constraint systems. This relation is equivalent to ⊢_{Ψ}^{E}.

Theorem 6.3.6 (Correctness of the Entailment Algorithm). S_{2} ⊢_{Ψ}^{E} S_{1} if and only if S_{2} ⊢_{alg}^{E} S_{1}.

Proof: See Appendix C.4.

The entailment algorithm takes exponential time, since the size of R is exponential in the number of set variables in S_{2}. Although faster algorithms for the entailment may exist, these algorithms must all be in PSPACE, because the containment problem on NFA’s, which is PSPACE-complete [1], can be polynomially reduced to the entailment problem on constraint systems.

By using the entailment algorithm in both directions, we can now decide if two constraint systems are observable equivalent. Thus, given a constraint system, we can find a minimal, observably equivalent system by systematically generating all constraint systems in order of increasing size, until we find one observably equivalent to the original system. Of course, the process of computing the minimal equivalent system with this algorithm is far too expensive for use in practical program analysis systems.

6.4 Practical Constraint System Simplification

Fortunately, to take advantage of the rule (≅) in program analysis algorithms, we do not need a completely minimized constraint system. Any simplifications in a constraint system produces corresponding reductions in the time and space required for the overall analysis.

For this purpose, we exploit the connection between constraint systems and RTGs. By Lemma 6.3.4, any transformation on constraint systems that preserves the language:

L_{G_{t}(Θ(S),E)}(R)

also preserves the observable behavior of S with respect to E. Based on this observation, we have transformed a variety of existing algorithms for simplifying regular tree grammars to algorithms for simplifying constraint systems. In the following subsections, we present the four most promising algorithms found so far. We use G to denote G_{t}(S, E), and we let X range over non-terminals and p over paths, which are sequences of the constructors dom and rng. Each algorithm assumes that the constraint system S is closed under Θ. Computing this closure corresponds to propagating data-flow information locally within a program component. This step is relatively cheap, since program components are typically small (less than a thousand lines of code).

Constraints Production Rules Non-empty

Reachable

f ≤ α^{f}  R ↦ [f ≤ α_{U}^{f}]
dom(α^{f}) ≤ α^{x}  α_{L}^{x} ↦ dom(α_{U}^{f})
1 ≤ α^{1} R ↦ [1 ≤ α_{U}^{1}] 1 ≤ α^{1} 1 ≤ α^{1}
α^{1} ≤ rng(α^{f}) α_{U}^{1} ↦ rng(α_{U}^{f})
rng(α^{f}) ≤ α^{a}  α_{L}^{a} ↦ rng(α_{L}^{f})
α^{y} ≤ α^{r} α_{U}^{y} ↦ α_{U}^{r} α_{L}^{r} ↦ α_{L}^{y} α^{y} ≤ α^{r}
α^{r} ≤ dom(α^{f}) α_{U}^{r} ↦ dom(α_{L}^{f})
g ≤ α^{P}  R ↦ [g ≤ α_{U}^{P}]  g ≤ α^{P}  g ≤ α^{P}
dom(α^{P}) ≤ α^{y}  α_{L}^{y} ↦ dom(α_{U}^{P})  dom(α^{P}) ≤ α^{y}
α^{a} ≤ rng(α^{P}) α_{U}^{a} ↦ rng(α_{U}^{P})  α^{a} ≤ rng(α^{P}) α^{a} ≤ rng(α^{P})
α^{r} ≤ α^{x}  α_{U}^{r} ↦ α_{U}^{x}  α_{L}^{x} ↦ α_{L}^{r}  α^{r} ≤ α^{x}
α^{1} ≤ α^{a}  α_{U}^{1} ↦ α_{U}^{a}  α_{L}^{a} ↦ α_{L}^{1}  α^{1} ≤ α^{a}  α^{1} ≤ α^{a}
1 ≤ α^{a}  R ↦ [1 ≤ α_{U}^{a}]  1 ≤ α^{a}  1 ≤ α^{a}
α_{L}^{P} ↦ α^{P}  α_{U}^{P} ↦ α^{P}

Figure 6.4 The constraint system, grammar and simplified systems for P = (λ^{g}y.((λ^{f}x.1) y))

6.4.1 Empty Constraint Simplification

A non-terminal X is empty if L_{G}(X) = ∅. Similarly, a production is empty if it refers to empty non-terminals, and a constraint is empty if it only induces empty productions. Since empty productions have no effect on the language generated by G, an empty constraint in S can be deleted without changing S’s observable behavior.

Let us illustrate this idea with the program component P = (λ^{g}y.((λ^{f}x.1) y)) we considered earlier. Although this example is unrealistic, it illustrates the behavior of our simplification algorithms. The solved constraint system S_{P} for P is shown in figure 6.4, together with the corresponding grammar G_{t}(S_{P} , E) where E = {α^{P} }. An inspection of this grammar shows that the set of non-empty non-terminals is:

{α_{L}^{P}, α_{U}^{P}, α_{L}^{y}, α_{U}^{a}, α_{L}^{r}, α_{U}^{1}, α_{L}^{x}, R}

Five of the constraints in S_{P} are empty, and are removed by this simplification algorithm, yielding a simplified system of eight non-empty constraints.

6.4.2 Unreachable Constraint Simplification

A non-terminal X is unreachable if there is no production R ↦ [Y ≤ Z] or R ↦ [Z ≤ Y] such that L_{G}(Y) ≠ ∅ and Z →_{G}^{∗} p(X). Similarly, a production is unreachable if it refers to unreachable non-terminals, and a constraint is unreachable if it only induces unreachable productions. Unreachable productions have no effect on the language L_{G}(R), and hence unreachable constraints in S can be deleted without changing the observable behavior of S.

In the above example, the reachable non-terminals are α_{U}^{1}, α_{U}^{a} and α_{U}^{g}. Three of the constraints are unreachable, and are removed by this algorithm, yielding a simplified system with five reachable constraints.

6.4.3 Removing ϵ-Constraints

A constraint of the form [α ≤ β] ∈ S is an ϵ-constraint. Suppose α ∉ E and the only upper bound on α in S is the ϵ-constraint [α ≤ β], i.e., there are no other constraints of the form α ≤ τ, rng(α) ≤ γ, or γ ≤ dom(α) in S. Then, for any solution ρ of S, the set environment ρ′ defined by:

ρ′(δ) = \{ \begin{matrix}ρ(δ) & if δ ≢ α \\ ρ(β) & if δ ≡ α \end{matrix}

is also a solution of S. Therefore we can replace all occurrences of α in S by β while still preserving the observable behavior Soln(S) |_{E}. This substitution transforms the constraint [α ≤ β] to the tautology [β ≤ β], which can be deleted. Dually, if [α ≤ β] ∈ S with β ∉ E and β having no other lower bounds, then we can replace β by α, again eliminating the constraint [α ≤ β].

To illustrate this idea, consider the remaining constraints for P. In this system, the only upper bound for the set variable α^{1} is the ϵ-constraint [α^{1} ≤ α^{a}]. Hence this algorithm replaces all occurrences of α^{1} by α^{a}, which further simplifies this constraint system into:

{1 ≤ α^{a}, α^{a} ≤ rng(α^{P}), g ≤ α^{P} }

This system is the smallest simple constraint system observably equivalent to the original system Θ(S).

6.4.4 Hopcroft’s Algorithm

The previous algorithm merges set variables under certain circumstances, and only when they are related by an ϵ-constraint. We would like to identify more general circumstances under which set variables can be merged. To this end, we define a valid unifier for S to be an equivalence relation ∼ on the set variables of S such that we can merge the set variables in each equivalence class of ∼ without changing the observable behavior of S. Using a model-theoretic argument, we can show that an equivalence relation ∼ is a valid unifier for S if for all solutions ρ ∈ Soln(S) there exists another solution ρ′ ∈ Soln(S) such that ρ′ agrees with ρ on E and ρ′(α) = ρ′(β) for all α ∼ β.

A natural strategy for generating ρ′ from ρ is to map each set variable to the least upper bound of the set variables in its equivalence class:

ρ′(α) = ⨆_{α′∼α} ρ(α′)

Figure 6.5 describes sufficient conditions to ensure that ρ′ is a solution of S, and hence that ∼ is a valid unifier for S. To produce an equivalence relation satisfying these conditions, we use a variant of Hopcroft’s O(n lg n) time algorithm [27] for computing an equivalence relation on states in a DFA and then merge set variables according to their equivalence class.^{∗}

The following theorem states that this simplification algorithm preserves the observable behavior of constraint systems.

Theorem 6.4.1 (Correctness of the Hopcroft Algorithm). Let S be a simple constraint system with external variables E; let ∼ be an equivalence relation on the set variables in a constraint system S satisfying conditions (a) to (e) from figure 6.5; let 1. Use a variant of Hopcroft’s algorithm [27] to compute an equivalence relation

∗A similar development based on the definition ρ′(α) = ⊓{ρ(α′) | α ∼ α′} results in an alternative algorithm, which is less effective in practice.

∼ on the set variables of S that satisfies the following conditions:

(a) Each set variable in E is in an equivalence class by itself.

(b) If [α ≤ β] ∈ S then ∀α ∼ α′ ∃β ∼ β′ such that [α′ ≤ β′] ∈ S.

(c) If [α ≤ rng(β)] ∈ S then ∀α ∼ α′ ∃β ∼ β′ such that [α′ ≤ rng(β′)] ∈ S.

(d) If [rng(α) ≤ β] ∈ S then ∀α ∼ α′ ∃β ∼ β′ such that [rng(α′) ≤ β′] ∈ S.

(e) If [α ≤ dom(β)] ∈ S then ∀α ∼ α′ ∀β ∼ β′ such that [α′ ≤ dom(β′)] ∈ S.

2. Merge set variables according to their equivalence class.

Figure 6.5 The Hopcroft algorithm

the substitution f map each set variable to a representation element of its equivalence class; and let S′ = f(S), i.e., S′ denotes the constraint system S with set variables merged according to their equivalence class. Then S ≅_{E} S′. Proof: See Appendix C.5.

6.5 Simplification Benchmarks

To test the effectiveness of the simplification algorithms, we extended MrSpidey with the four algorithms that we have just described: empty, unreachable, ϵ-removal, and Hopcroft. Each algorithm also implements the preceding simplification strategies. The first three algorithms are linear in the number of non-empty constraints in the system, and Hopcroft is log-linear.

We tested the algorithms on the constraint systems for nine program components on a 167MHz Sparc Ultra 1 with 326M of memory, using the MzScheme compiler [17]. The results are described in figure 6.6. The second column gives the number of lines in each program component, and the third column gives the number of constraints in the original (unsimplified) constraint system after closing it under the rules Θ. The remaining columns describe the behavior of each simplification algorithm, presenting the factor by which the number of constraints was reduced, and the time (in milliseconds) required for this simplification. Since MzScheme is a byte code compiler,

empty  unreachable ϵ-removal  Hopcroft
Definition  lines  size factor time factor time factor time factor time
map  5  221  3 <10  6  20  11  30  13  30
reverse  6  287  4 <10  8  20  20  10  20  30
substring  8  579  12  10  64  10  64  10  96  20
qsort  41 1387  15 <10  15  30  58  50  66  40
unify  89 2921  10  10  11  80  55 120  65 150
hopcroft  201 8429  25  10  42 100 118 100 124 200
check  237 21854  4  50  4 1150  26 370 168 510
escher-fish 493 30509 187  10 678  40 678  40 678  80
scanner  1209 59215  3 180  17 840  45 2450  57 2120

Figure 6.6 Behavior of the constraint simplification algorithms.

porting the simplification algorithms to a native code compiler could be expected to produce a speed-up of roughly a factor of 5.

The results demonstrate the effectiveness and efficiency of our simplification algorithms. The resulting constraint systems are typically at least an order of magnitude smaller than the original system. The cost of these algorithms is reasonable, particularly considering that they were run on a byte code compiler. As expected, the more sophisticated algorithms are more effective, but are also more expensive.

Chapter 7

Componential Set-Based Analysis

Equipped with the simplification algorithms, we can now return to our original problem of extending set-based analysis to handle significantly larger programs. These programs are typically constructed as a collection of program components (e.g. modules, packages or files). Exploiting this component-based structure is the key to analyzing such programs efficiently.

The following section describes componential set-based analysis. Section 7.2 presents experimental results on the effectiveness of the analysis, and section 7.3 describes how MrSpidey presents the analysis results for multi-component programs to the programmer.

The constraint simplification algorithms also enables an efficient polymorphic, or context-sensitive, analysis that only duplicates a simplified constraint system for each reference to a polymorphic function. A description of this polymorphic analysis is presented in section 7.4, together with experimental results on the behavior of the analysis.

7.1 Componential Set-Based Analysis

Componential set-based analysis processes programs in three steps.

1. For each component in the program, the analysis derives and simplifies the constraint system for that component and saves the simplified system in a constraint file, for use in later runs of the analysis. The simplification is performed with respect to the external variables of the component, excluding expression labels, in order to minimize the size of the simplified system. Thus, the simplified system only needs to describe how the component interacts with the rest of the program, and the simplification algorithm can discard constraints that are only necessary to infer local value set invariants. These discarded constraints are reconstructed later as needed.

This step can be skipped for each program component that has not changed since the last run of the analysis, and the component’s constraint file can be used instead.

2. The analysis combines the simplified constraint systems of the entire program and closes the combined collection of constraints under Θ, thus propagating data-flow information between the constraint systems for the various program components.

3. Finally, to reconstruct the full analysis results for the program component that the programmer is focusing on, the analysis tool combines the constraint system from the second step with the unsimplified constraint system for that component. It closes the resulting system under Θ, which yields appropriate value set invariants for each labeled expression in the component.

The new analysis can easily process programs that consist of many components. For its first step, it eliminates all those constraints that have only local relevance, thus producing a small combined constraint system for the entire program. As a result, the analysis tool can solve the combined system more quickly and using less space than traditional set-based analysis [24]. Finally, it recreates as much precision as traditional set-based analysis as needed on a per-component basis.

The new analysis performs extremely well in an interactive setting because it exploits the saved constraint files where possible and thus avoids re-processing many program components unnecessarily.

7.2 Experimental Results

We implemented four variants of componential set-based analysis. Each analysis uses a particular simplification algorithm from chapter 6 to simplify the constraint systems for the program components. We tested these analyses with five benchmark programs, ranging from 1,200 to 17,000 lines. For comparison purposes, we also analyzed each benchmark with the standard set-based analysis that performs no simplification. The analyses handled library functions in a context-sensitive, polymorphic manner according to the constraint derivation rules (let) and (inst) to avoid merging information between unrelated calls to these functions. The remaining functions were analyzed in a context-insensitive, monomorphic manner. The results are documented in figure 7.1.

The fourth column in the figure shows the maximum size of the constraint system generated by each analysis, and also shows this size as a percentage of the constraint system generated by the standard analysis. The analyses based on the simplification algorithms produce significantly smaller constraint systems, and can also analyze more programs, such as sba and poly, for which the standard analysis exhausted heap space.

The fifth column shows the time required to analyze each program from scratch, without using any existing constraint files.^{∗} The analyses that exploit constraint simplification yield significant speed-ups over the standard analysis because they manipulate much smaller constraint systems. The results indicate that, for these benchmarks, the ϵ-removal algorithm yields the best trade-off between efficiency and effectiveness of the simplification algorithms. The additional simplification performed by the more expensive Hopcroft algorithm is out-weighed by the overhead of running the algorithm. The tradeoff may change as we analyze larger programs.

To test the responsiveness of the componential analyses in an interactive setting based on an analyze-debug-edit cycle, we re-analyzed each benchmark after changing a randomly chosen component in that benchmark. The re-analysis times are shown in the sixth column of figure 7.1. These times show an order-of-magnitude improvement in analysis times over the original, standard analysis, since the saved constraint files are used to avoid reanalyzing all of the unchanged program components. For example, the analysis of zodiac, which used to take over two minutes, now completes in under four seconds. Since practical debugging sessions using MrSpidey typically involve repeatedly analyzing the project each time the source code of one module is modified, e.g., when a bug is identified and eliminated, using separate analysis substantially improves the usability of MrSpidey.

The disk-space required to store the constraint files is shown in column seven. Even though these files use a straight-forward, text-based representation, their size is typically within a factor of two or three of the corresponding source file.

7.3 User Interface for Multi-File Programs

We extended MrSpidey’s user interface to cope with programs consisting of multiple source files, or components. MrSpidey first analyses the program, using the componential set-based analysis described above, and then displays an annotated version of

∗These times exclude scanning and parsing time.

Num. of  Analysis Re-analysis Constraint
Program  lines Analysis  constraints  time  time  file (bytes)
scanner  1253 standard  61K  14.1s  7.7s  572K
empty  24K (39%)  12.0s  3.1s  189K
unreachable  15K (25%)  9.7s  2.0s  39K
ϵ-removal  14K (23%)  9.5s  1.7s  28K
Hopcroft  14K (23%)  10.4s  1.7s  25K
zodiac  3419 standard  704K  133.4s  110.6s  1634K
empty  62K (9%)  34.1s  8.1s  328K
unreachable  21K (3%)  28.8s  4.5s  169K
ϵ-removal  13K (2%)  28.8s  3.8s  147K
Hopcroft  11K (2%)  31.4s  3.8s  136K
nucleic  3432 standard  333K  83.9s  51.2s  2882K
empty  90K (27%)  52.8s  17.8s  592K
unreachable  68K (20%)  48.4s  14.6s  386K
ϵ-removal  56K (17%)  48.3s  13.1s  330K
Hopcroft  56K (17%)  60.9s  13.2s  328K
sba  11560 standard *, >5M  *          *           *
empty  1908K (<38%) 181.5s  65.5s  1351K
unreachable  105K (<2%) 149.5s  43.3s  920K
ϵ-removal  76K (<2%) 147.1s  42.2s  770K
Hopcroft  65K (<1%) 156.8s  41.1s  716K
mod-poly 17661 standard *, >5M  *          *           *
empty  *, >5M  *          *           *
unreachable  201K (<4%) 259.6s  26.9s  1517K
ϵ-removal  68K (<1%) 239.6s  13.3s  1038K
Hopcroft  38K (<1%) 254.1s  10.9s  907K

* indicates the analysis exhausted heap space

Figure 7.1 Behavior of the modular analyses.

the program’s main file with the usual static debugging mark-ups. The programmer can also view annotated versions of any other source file by using the File|Open ... dialog box (shown in Figure 7.2) to select the source file of interest.

In multi-file programs, the source (or destination) of an arrow may sometimes refer to a program point in a separate file. In this case MrSpidey draws an arrow originating (or terminating) in the left margin of the program, as shown in figure 7.3. Clicking on the arrow provides the option to zoom to and highlight the term at the

Figure 7.2 The File|Open ... dialog box

other end of the arrow, as shown in figures 7.4 and 7.5. These facilities are useful for following the flow of values through multi-file programs.

7.4 Efficient Polymorphic Analysis

The constraint simplification algorithms also enables an efficient polymorphic, or context-sensitive, analysis. To avoid merging information between unrelated calls to functions that are used in a polymorphic fashion, a polymorphic analysis duplicates the function’s constraints at each call site. We extended MrSpidey with five polymorphic analyses. The first analysis is copy, which duplicates the constraint system for each polymorphic reference via a straightforward implementation of the rules (let) and (inst).^{†} The remaining four analyses are smart analyses that simplify the constraint system for each polymorphic definition.

†We also implemented a polymorphic analysis that re-analyzes a definition at each reference, but found its performance to be comparable to, and sometimes worse than, the copy analysis.

Figure 7.3 Source in another file

Figure 7.4 Zooming to the source in another file

We tested the analyses using a standard set of benchmarks [28]. The results of the test runs are documented in figure 7.6. The second column shows the number of lines in each benchmark; the third column presents the time for the copy analysis; and columns four to seven show the times for each smart polymorphic analysis, as a percentage of the copy analysis time. For comparison purposes, the last column shows the relative time of the original, but less accurate, monomorphic analysis.

Figure 7.5 The source in the other file

copy  Relative time of smart polymorphic analyses Mono.
Program lines analysis empty unreachable ϵ-removal Hopcroft analysis
lattice 215  4.2s  39%  36%  35%  38%  42%
browse  233  2.5s  76%  76%  76%  81%  75%
splay  265  7.9s  75%  73%  70%  72%  83%
check  281 50.1s  21%  23%  14%  14%  23%
graphs  621  2.8s  85%  85%  82%  87%  82%
boyer  624  4.3s  46%  46%  49%  50%  40%
matrix  744  7.5s  64%  57%  51%  52%  45%
maze  857  6.2s  64%  59%  58%  61%  54%
nbody  880 39.6s  57%  25%  25%  26%  28%
nucleic 3335  *    * 243s  * 42s  * 42s  * 44s  * 36s

* indicates the copy analysis exhausted heap space, and the table contains absolute times for the other analyses

Figure 7.6 Times for the smart polymorphic analyses, relative to the copy analysis.

The results again demonstrate the effectiveness of our constraint simplification algorithms. The smart analyses that exploit constraint simplification are always significantly faster and can analyze more programs than the copy analysis. For example, while copy exhausts heap space on the nucleic benchmark, all smart analyses successfully analyzed this benchmark.

Again, it appears that the ϵ-removal analysis yields the best trade-off between efficiency and effectiveness of the simplification algorithms. This analysis provides the additional accuracy of polymorphism without much additional cost over the coarse, monomorphic analysis. With the exception of the benchmarks browse, splay and graphs, which do not re-use many functions in a polymorphic fashion, this analysis is a factor of 2 to 4 times faster than the copy analysis, and it is also capable of analyzing larger programs.

Chapter 8

Evaluation of MrSpidey

We evaluated the usefulness of MrSpidey as static debugging tool using a number of programs.

8.1 Verifying a Web Server

Rice’s web server software consists of a normal, fully-functional web server and a simple backup server. The backup server consists of a 76 line Scheme program that accepts connections to the web port, and returns a HTML page saying:

     The Rice University computer science department's Web server has
     been disconnected temporarily.

We used MrSpidey to statically debug the backup server. MrSpidey detected a single, potentially unsafe operation, where the analysis suggested that the end-of-file value could be returned by read-line and then passed as an argument to the operation string-length. An inspection of the program revealed that this behavior could never actually occur. After simplifying two lines of code, MrSpidey was able to verify the safety of the string-length operation, and produced the summary:

     TOTAL CHECKS: 0 (of 56 possible checks is 0.0%)

8.2 Verifying gunzip

MzScheme’s standard library contains Scheme code for inflating deflated (PKZIP’s method 8 compressed) data. The code consists of a single 800 line file inflate.ss, translated directly from the gzip source distribution. MrSpidey initially reported that out of the 650 operations in the program, it was unable to verify the safety of 27 (or 5%) of them.

The majority of these unsafe operations were vector-ref operations that, according to MrSpidey’s analysis, could be applied to non-vector values. We used MrSpidey’s filter and path-to-source facilities to identify the source of these erroneous, non-vector values.

• Some of these non-vector values came from the third field in a structure called huft. This field contains a number in some situations and a vector in others. By splitting the field into separate fields for numeric and vector values, we reduced the unsafe operation count to 18.

• Some non-vector values came from a stack of tables, each of which should be a vector. However, the stack was initialized as a vector of zero’s. By changing the initial value of the stack to a vector of empty vectors, we reduced the unsafe operation count by one to 17.

• The non-vector value null value was mistakenly passed as an argument to a function huft build, instead of the empty vector. Changing the program to pass the empty vector instead reduced the unsafe operation count by two to 15.

• The non-vector value null also was the initial value of a variable that was later assigned to a vector. Initializing the variable to the empty vector reduced the unsafe operation count by three to 12.

Some of the remaining unsafe operations were caused by an extremely complicated return protocol from the function huft build. The function returns a tuple where the type of some fields depends on the value of other fields. We simplified the return protocol of the function by using exceptions to handle erroneous conditions. This reduced the unsafe operation count by three to 9.

Minor rewriting to produce a cleaner coding style further reduced the unsafe operation count by two to 7. All of the remaining unsafe operations are actual errors that resulted from failing to detect and handle a truncated input file. Thus the original program would crash on a truncated input file with a message such as:

> (gunzip "~/tmp/t")
char=?: expects type <character> as 1st arg;
given \#<eof> (type <eof>); other args: \#\Ø

By adding code to check of the end-of-file case, we finally reduced the unsafe operation count to 0, and the resulting statically debugged program gracefully handles truncated input files:

> (gunzip "~/tmp/t")
gunzip: Unexpected end of input file

8.3 Verifying an Extended Direct Semantics Interpreter

Extended direct semantics is a format for denotational language specifications that accommodates orthogonal extensions of a language without changing the denotations of existing phrases [4]. The semantics of a language is specified in this format using a tower of interpreters. The tower starts with a basic interpreter, which can only interpret certain trivial expressions. This basic interpreter is then composed with additional interpreters for the various constructs in the language.

We used MrSpidey to statically debug an interpreter expressed in this style. In addition to the basic interpreter, this program contains interpreters for:

• Arithmetic operations (integer constants, add1 and sub1)

• Call-by-value functions (variables, functions and applications)

• Control operations (catch and throw)

• Assignments (ref, deref and setref)

Each interpreter consists of two units: one unit defining the abstract syntax structures and a second unit that specifies how to interpret the new abstract syntax. An additional five units specify global definitions and test cases, for a total of 15 units in 15 separate files.

Porting the program to MzScheme’s unit system introduced an error, where one of the units was defined to take three input signatures:

(unit/sig (Program)

(import globalˆ languageˆ arith-ASTˆ )

…

but was only passed two signatures in the main compound-unit clause:

…

[PROGRAM : Programˆ ((reference-unit "program.ss") GLOBAL TOP)] …

When this program was analyzed, MrSpidey produced the warning:

Warning: Unit takes 47 imports, given 26 in file "program.ss" line 2

together with a hyper-link to the relevant unit.

After this bug was fixed, MrSpidey was able to verify the safety of the program, and produced the following summary:

main.ss         CHECKS:        0  (of 39 possible checks is 0.0%)
program.ss      CHECKS:        0  (of 4 possible checks is 0.0%)
top.ss          CHECKS:        0  (of 1 possible checks is 0.0%)
storeM.ss       CHECKS:        0  (of 161 possible checks is 0.0%)
controlM.ss     CHECKS:        0  (of 49 possible checks is 0.0%)
cbvM.ss         CHECKS:        0  (of 40 possible checks is 0.0%)
arithmM.ss      CHECKS:        0  (of 24 possible checks is 0.0%)
baseM.ss        CHECKS:        0  (of 21 possible checks is 0.0%)
storeAST.ss     CHECKS:        0  (of 11 possible checks is 0.0%)
controlAST.ss   CHECKS:        0  (of 5 possible checks is 0.0%)
arithAST.ss     CHECKS:        0  (of 2 possible checks is 0.0%)
cbvAST.ss       CHECKS:        0  (of 2 possible checks is 0.0%)
baseAST.ss      CHECKS:        0  (of 1 possible checks is 0.0%)
global.ss       CHECKS:        0  (of 41 possible checks is 0.0%)
tst.ss          CHECKS:        0  (of 46 possible checks is 0.0%)

Part of the reason that MrSpidey is so successful on this program is that the program had already been carefully written so that Soft Scheme [46] could verify its safety, and thus the style of the program was already well-suited for automatic analysis techniques.

8.4 Statically Debugging HHL

We used MrSpidey to statically debug a program under development. This program, called HHL, is a hardware verifier using heterogeneous logic. It consists of 3312 lines of Scheme code distributed over 12 files, and interfaces to the Omega calculator [38].

We used MrSpidey to analyze the entire program, and then concentrated on statically debugging one file, prover.ss, containing 500 lines of code. MrSpidey initially reported that out of 466 operations in the file, it was unable to verify the safety of 17 (or 4%) of them. Nine of these unsafe operations were caused by bugs in the program.

• Two unsafe string-append operations were caused by a variable being erroneously initialized with void, instead of with a string.

• An arity check was caused be a two-argument function being applied to a single argument.

• An unsafe car operation was applied to the result value of read, which is not necessarily a pair.

• Three other unsafe string operations were applied to the result of read-line, which can return the end-of-file value in addition to strings.

• On two occasions, the primitive andmap was applied to a single argument.

The remaining eight unsafe operations appear to be caused by limitations in the underlying analysis.

Chapter 9

Related Work

9.1 Static Debuggers

A number of interactive analysis tools and static debugging systems have been developed for various programming languages. Some address different concerns; none provide an explanation of the derived invariants.

Syntox [3] is a static debugger for a subset of Pascal. Like MrSpidey, it associates run-time invariants, i.e., numeric ranges, with statements in the program. Because Syntox does not provide an explanation of these invariants, it is difficult for a programmer to decide whether an unexpected invariant is caused by a weakness in the proof system or a flaw in the program. In addition, the existing system processes only a first-order language, though Bourdoncle explains how to extend the analysis [3:Section 5].

Several environments [30, 6, 26, 44, 41] have been built for parallel programming languages to expose dependencies, thus allowing the programmer to tune programs to minimize these dependencies. In particular, the ParaScope [6, 30] and D editors [26] have many similarities to MrSpidey. Both MrSpidey and the editors provide information at varying levels of granularity; both retain source correlation through transformations; and both depict dependencies graphically. However, unlike MrSpidey, the editors process a language with extremely simple control- and data-flow facilities, and therefore do not need to provide a supporting explanation for the derived dependencies.

The Extended Static Checking system (ESC) [8] is a static debugger designed to detect program errors such as nil dereferences, out-of-bound array accesses and deadlocks, and race conditions. If an error may occur, then ESC returns a counterexample in the form of an assignment of values to program variables that can cause the error. ESC is based on an automatic theorem prover that is more powerful than MrSpidey’s constraint-based approach, but which is also more expensive. Hence ESC cannot analyze large programs, and is restricted to working on a per-procedure basis.

Therefore, this approach requires that the programmer annotates the program with specifications for the interfaces between procedures, which significantly increases the start-up cost of using ESC. In contrast, MrSpidey can be immediately applied to existing programs without the need for any additional annotations.

Microsoft’s Program Analysis Group has developed a static debugger for small C programs.^{∗} In a fashion similar to MrSpidey, this debugger analyzes programs and uses the resulting invariants to identify potential bugs. However, it cannot explain the derivation of the resulting invariants, and only works on small programs of up to a few hundred lines of code.

9.2 Constraint Simplification

A number of researchers have investigated the problem of constraint simplification in order to derive faster and more scalable analyses and type systems.

Deutsch and Heintze [9] examine constraint simplification for set-based analysis. They discover two simplification algorithms, which are analogous to our empty and unreachable constraint simplification algorithms, but do not present results on the cost or effectiveness of these simplification algorithms.

Fähndrich and Aiken [12] examine constraint simplification for an analysis based on a more complex constraint language. They develop a number of heuristic algorithms for constraint simplification, which they test on programs of up to 6000 lines. Their fastest approach yields a factor of 3 saving in both time and space, but is slow in absolute times compared to other program analyses.

Pottier [37] studies an ML-style language with subtyping. Performing type inference on this language produces subtype constraints that are similar to our constraints. Pottier defines an entailment relation on constraints, and presents an incomplete algorithm for deciding entailment. In addition, he proposes some ad hoc algorithms for simplifying constraints. He does not report any results on the cost or effectiveness of these algorithms.

Trifonov and Smith [43] present constrained types that are similar to our constraint systems, and they describe an incomplete algorithm for deciding the subtyping relation between constrained types. They do not discuss constraint simplification. Eifrig, Smith and Trifonov [11] discuss constraint simplification in the context of type inference for objects. They present three algorithms for simplifying constraint systems, two of which which are similar to the empty and ϵ-removal algorithms, and the third is a special case of the Hopcroft algorithm. They do not present results on the cost or effectiveness of these algorithms.

∗Personal communication: Daniel Weise (February 97).

Duesterwald et al [10] describe algorithms for simplifying data-flow equations. These algorithms are similar to the ϵ-removal and Hopcroft algorithms. Their approach only preserves the greatest solution of the equation system and assumes that the control flow graph is already known. Hence it cannot be used to analyze programs in a componential manner or to analyze programs with advanced control-flow mechanisms such as first-class functions and virtual methods. The paper does not present results on the cost or effectiveness of these algorithms.

Chapter 10

Limitations and Future Work

Although MrSpidey has proven to be an effective tool for statically debugging a variety of programs, including the programs described above, there are several aspects of MrSpidey that could be improved.

10.1 Size of Types

The constraint simplification algorithms can reduce the size of type invariants by a significant factor, but in some cases the resulting types are still excessively large. This problem could be partly remedied by developing more aggressive constraint simplification algorithms. However, more aggressive algorithms may not completely solve the problem, because for a given constraint system, even the smallest equivalent system may yield an excessively large type.

Traditional static type systems avoid this problem by introducing a new type name each time a new datatype is declared. For example, the Standard ML declaration corresponding to the binary trees we considered earlier is:

   datatype tree = Leaf of int
                 | Node of tree * tree

This declaration introduces the type name tree that can be used as a shorthand for describing any valid tree build using Leaf and Node. By comparison, in MrSpidey the corresponding type expression would need to explicate the combination of Leaf and Node constructors used to build the tree.

As a partial solution to this problem, MrSpidey allows the programmer to configure the type display algorithm to avoid displaying the types for the fields of a structure or for the instance variables of an object (see appendix D.2.2). Since most excessively large types involve either structures or objects, selecting this option keeps the size of types manageable, even for complicated programs.

10.2 Accuracy of the Analysis

Componential set-based analysis infers reasonably accurate invariants describing the value sets for program expressions, even in the presence of complex control-flow and data-flow patterns. However, since the actual run-time behavior of a program is undecidable, these invariants are necessarily approximate, and there are some situations where the invariants are overly coarse.

A serious limitation of MrSpidey is that it does not perform any analysis of integer subranges. Thus, MrSpidey cannot detect errors that may occur due to an array index being out-of-bounds. Other static debuggers [3, 8] can detect this kind of error, but it is not clear how well these debuggers scale up to large, complex programs.

10.3 State in the User Interface

For the most part, MrSpidey’s graphical user interface presents static debugging information in a natural and intuitive manner. However, the filter facility (described in section 5.4) introduces some hidden state into the user interface. That is, although the currently selected filter affects the behavior of the interface, this filter is not displayed. Hence it is easy for the programmer to forget which filter is currently selected, and to be confused by the displayed value flow.

There are two possible solutions to this problem. The first is simply to display the currently selected filter. However, state can be confusing in a user interface, even when it is displayed. Therefore, a better solution would be develop an alternative interface that does not require this state information.

One such approach is to allow the programmer to click on the internal components of a type invariant, yielding a pop-up menu as before, and then to have options in that menu that display the value flow only for values corresponding to the selected component of the type. This approach would remove the need for state in the user interface, and would hopefully provide programmer with better access to the derivation of the program’s invariants.

10.4 Signatures

All the constraint simplification algorithms we considered preserve the observable behavior of constraint systems, and thus do not effect the accuracy of the analysis. If we were willing to tolerate a less accurate analysis, we could choose a simplified constraint system that does not preserve the observable behavior of the original system, but only entails, or conservatively approximates, that behavior. This approach allows the use of smaller constraint systems, and hence yields a faster analysis.

A promising approach for deriving such approximate constraint systems is to rely on a programmer-provided signature describing the behavior of a polymorphic function or module, and to derive the new constraint system from that signature. After checking the entailment condition to verify that signature-based constraints correctly approximates the behavior of the module, we could use those constraints in the remainder of the analysis. The appropriate constraint derivation rule is:

\frac{Γ ⊢ M : α, S_{1} S_{2} ⊧_{E} S_{1} where E = Label ∪ F V [range(Γ)] ∪ \{α\}}{Γ ⊢ M : α, S_{2}} (approx)

Since the signature-based constraints are expected to be smaller than the derived ones, this approach could significantly reduce analysis times for large programs. It would also allow for a program component to be statically debugged with respect to its signature, without needing to access the entire source program.

Appendix A Proofs for Chapter 3

A.1 Subject Reduction Proof

Lemma 2.5.3 (Subject Reduction for ⟶). If Γ ⊢ M_{1} : α, S_{1} and M_{1} ⟶ M_{2}, then Γ ⊢ M_{2} : α, S_{2} such that S_{1} ⊧ S_{2}. Proof: The proof proceeds by case analysis according to the relation M_{1} ⟶ M_{2}.

• Suppose M_{1} ⟶ M_{2} via (β_{v}). Then:

\begin{aligned}M_{1} & = & ((λ^{t}x.N) V) \\ M_{2} & = & N[x ↦ V] \end{aligned}

The typing derivation on M_{1} is of the form:

\frac{\frac{Γ ∪ \{x : β_{x}\} ⊢ N : β_{N}, S_{N}}{Γ ⊢ (λ^{t}x.N) : β_{t}, S_{t}} (abs) Γ ⊢ V : β_{V} , S_{V}}{Γ ⊢ M_{1} : α, S_{1}} (app)

where:

S_{t} = S_{N} ∪ {t ≤ β_{t}, dom(β_{t}) ≤ β_{x}, β_{N} ≤ rng(β_{t})}
S_{1} = S_{t} ∪ S_{V} ∪ {β_{V} ≤ dom(β_{t}), rng(β_{t}) ≤ α}

By the Substitution Lemma A.1.1:

Γ ⊢ M_{2} : β_{N}, S′_{2} where S_{N} ∪ S_{V} ∪ {β_{V} ≤ β_{x}} ⊧ S′_{2}

By the Flow Lemma 2.5.5:

Γ ⊢ M_{2} : α, S_{2} where S′_{2} ∪ {β_{N} ≤ α} ⊧ S_{2}

Since S_{1} ⊇ S_{N} ∪ S_{V}, we have that S_{1} ⊧ S_{N} ∪ S_{V}. Also:

S_{1} ⊇ {β_{V} ≤ dom(β_{t}), dom(β_{t}) ≤ β_{x}} ⊧ {β_{V} ≤ β_{x}}
S_{1} ⊇ {β_{N} ≤ rng(β_{t}), rng(β_{t}) ≤ α} ⊧ {β_{N} ≤ α}

Hence S_{1} ⊧ S_{2}, as required.

• Suppose M_{1} ⟶ M_{2} via (βlet ). Then:

\begin{aligned}M_{1} & = & (let (x V) N) \\ M_{2} & = & N[x ↦ V] \end{aligned}

The typing derivation on M_{1} is of the form:

\frac{Γ ⊢ V : α_{V} , S_{V} \overline{α} = SetVar(S_{V}) \ (F V [range(Γ)] ∪ Label) Γ ∪ \{x : ∀\overline{α}. (α_{V} , S_{V})\} ⊢ N : β, S}{Γ ⊢ M_{1} : β, S} (let)

By the Subject Reduction for let Lemma A.1.2:

Γ ⊢ M_{2} : β, S

as required.

• Suppose M_{1} ⟶ M_{2} via (unlabel). Then:

\begin{aligned}M_{1} & = & V^{l} \\ M_{2} & = & V \end{aligned}

The typing derivation on M_{1} is of the form:

\frac{Γ ⊢ V : α, S_{V}}{Γ ⊢ V^{l} : β, S_{V} ∪ \{α ≤ l, α ≤ β\}} (label)

Hence Γ ⊢ V : α, S_{V}, and by the Flow Lemma 2.5.5, Γ ⊢ V : β, S_{2} where S_{1} ⊧ S_{2}.

Lemma A.1.1 (Substitution). If

\begin{matrix}Γ ∪ \{x : α_{x}\} ⊢ N : α_{N}, S_{N} \\ Γ ⊢ V : α_{V} , S_{V} \end{matrix}

then

Γ ⊢ N[x ↦ V] : α_{N}, S where S_{N} ∪ S_{V} ∪ {α_{V} ≤ α_{x}} ⊧ S

Proof: The proof proceeds by induction on the number of let-expressions in N, and on the size of N:

Γ ∪ {x : α_{x}} ⊢ N : α_{N}, S_{N}

If x ∉ F V [N], then N[x ↦ V] = N, S = S_{N} and the lemma trivially holds.

Otherwise we proceed by case analysis on the constraint derivation rule used in the last step in the derivation.

• (var): Since x ∈ F V [N], N = x. Hence S_{N} = {α_{x} ≤ α_{N}}, N[x ↦ V] = V and this case holds via the Flow Lemma 2.5.5.

• (const): This case cannot occur since x ∈ F V [N].

• (label): This case is straightforward.

• (abs): In this case N = (λ^{t}y.M), and the constraint derivation is:

\frac{Γ ∪ \{x : α_{x}, y : α_{y}\} ⊢ M : α_{M}, S_{M}}{Γ ∪ \{x : α_{x}\} ⊢ (λ^{t}y.M) : α_{N}, S_{N}} (abs)

where:

S_{N} = S_{M} ∪ {t ≤ α_{N}, dom(α_{N}) ≤ α_{y}, α_{M} ≤ rng(α_{N})}

Since x ∈ F V [N], x ≠ y. Hence N[x ↦ V] = (λ^{t}y.M[x ↦ V]). By induction:

Γ ∪ {x : α_{x}, y : α_{y}} ⊢ M[x ↦ V] : α_{M}, S′_{M}

where:

S_{M} ∪ S_{V} ∪ {α_{V} ≤ α_{x}} ⊧ S′_{M}

Hence, via (abs):

Γ ⊢ N[x ↦ V] : α_{N}, S

where:

S = S′_{M} ∪ {t ≤ α_{N}, dom(α_{N}) ≤ α_{y}, α_{M} ≤ rng(α_{N})}

Since S_{N} ∪ S_{V} ∪ {α_{V} ≤ α_{x}} ⊧ S, the lemma holds for this case.

• (app): In this case M = (M_{1} M_{2}), and the constraint derivation is:

\frac{Γ ∪ \{x : α_{x}\} ⊢ M_{i} : β_{i}, S_{i}}{Γ ∪ \{x : α_{x}\} ⊢ (M_{1} M_{2}) : α_{N}, S_{N}} (app)

where

S_{N} = S_{1} ∪ S_{2} ∪ {β_{2} ≤ dom(β_{1}), rng(β_{1}) ≤ α_{N}}

By induction,

Γ ⊢ M_{i}[x ↦ V] : β_{i}, S′_{i}

where

S_{i} ∪ S_{V} ∪ {α_{V} ≤ α_{x}} ⊧ S′_{i}

Hence

Γ ⊢ M[x ↦ V] : α_{N}, S

where

S = S′_{1} ∪ S′_{2} ∪ {β_{2} ≤ dom(β_{1}), rng(β_{1}) ≤ α_{N}}

Obviously, S_{N} ∪ S_{V} ∪ {α_{V} ≤ α_{x}} ⊧ S, and the lemma holds for this case.

• (let): In this case N = (let (y W) M), where W ∈ Value. Hence:

Γ ∪ {x : α_{x}} ⊢ (let (y W) M) : α_{N}, S_{N}

and therefore by the following Subject Reduction for let Lemma A.1.2:

Γ ∪ {x : α_{x}} ⊢ M[y ↦ W] : α_{N}, S_{N}

By induction:

Γ ⊢ M[y ↦ W][x ↦ V] : α_{N}, S

where S_{N} ∪ S_{V} ∪ {α_{V} ≤ α_{x}} ⊧ S. Since:

M[y ↦ W][x ↦ N] = M[x ↦ N][y ↦ W [x ↦ N]]

we have that:

Γ ⊢ M[x ↦ V][y ↦ W [x ↦ V]] : α_{N}, S

and therefore, by the Subject Reduction for let Lemma A.1.2:

Γ ⊢ (let (y W [x ↦ V]) M[x ↦ V]) : α_{N}, S

or, equivalently:

Γ ⊢ (let (y W) M)[x ↦ V] : α_{N}, S

and thus the lemma holds in this case.

• (inst): This case cannot occur since x ∈ F V [N] and x is bound to a set variable in the derivation context.

The constraint derivation rules uses constraint schemas to accurately analyze polymorphic let-expressions. The constraint system for a let-expression is actually equivalent to the constraint system for the corresponding βlet -expanded expression^{∗}. The following lemma demonstrates this equivalence of constraint systems.

Lemma A.1.2 (Subject Reduction for let).

Γ ⊢ (let (x V) N) : α_{N}, S_{N}

if and only if

Γ ⊢ N[x ↦ V] : α_{N}, S_{N}

Proof: The derivation Γ ⊢ (let (x V) N) : α_{N}, S_{N} holds if and only if:

Γ ⊢ V : α_{V} , S_{V}
\overline{α} = SetVar(S_{V}) \ (F V [range(Γ)] ∪ Label)
σ = ∀\overline{α}. (α_{V} , S_{V})
Γ ∪ {x : σ} ⊢ N : α_{N}, S_{N}

The proof of both directions proceeds by induction on the number of let-expressions in N, and on the size of N:

If x ∉ F V [N], then N[x ↦ V] = N and the lemma trivially holds.

Otherwise we proceed by case analysis on the constraint derivation rule used in the last step in the derivation:

Γ ∪ {x : σ} ⊢ N : α_{N}, S_{N}

• (var): This case cannot occur since x ∈ F V [N] implies N = x, but x is bound to a schema in the derivation context and so the rule (inst) applies.

• (const): This case cannot occur since x ∈ F V [N].

• (abs): In this case N = (λ^{t}y.M), and the typing derivation is:

\frac{Γ ∪ \{x : σ, y : α_{y}\} ⊢ M : α_{M}, S_{M}}{Γ ∪ \{x : σ\} ⊢ (λ^{t}y.M) : α_{N}, S_{N}} (abs)

∗This equivalence contrasts with the situation for the other reduction rules, where the constraint system for the redex only entails the constraint system for the contractum, as shown in the Subject Reduction for ⟶ Lemma 2.5.3.

where:

S_{N} = S_{M} ∪ {t ≤ α_{N}, dom(α_{N}) ≤ α_{y}, α_{M} ≤ rng(α_{N})}

Since x ∈ F V [N], x ≠ y. Hence N[x ↦ V] = (λ^{t}y.M[x ↦ V]). By induction,

Γ ∪ {x : σ, y : α_{y}} ⊢ M[x ↦ V] : α_{M}, S_{M}

Hence, via (abs):

Γ ⊢ N[x ↦ V] : α_{N}, S_{N}

The reasoning for the converse direction is similar.

• (app): In this case M = (M_{1} M_{2}), and the typing derivation is:

\frac{Γ ∪ \{x : σ\} ⊢ M_{i} : β_{i}, S_{i}}{Γ ∪ \{x : σ\} ⊢ (M_{1} M_{2}) : α_{N}, S_{N}} (app)

where:

S_{N} = S_{1} ∪ S_{2} ∪ {β_{2} ≤ dom(β_{1}), rng(β_{1}) ≤ α_{N}}

By induction,

Γ ⊢ M_{i}[x ↦ V] : β_{i}, S_{i}

Hence

Γ ⊢ M[x ↦ V] : α_{N}, S_{N}

as required. The reasoning for the converse direction is similar.

• (label): This case is straightforward.

• (let): In this case N = (let (y W) M), where W ∈ Value. Hence:

Γ ∪ {x : σ} ⊢ (let (y W) M) : α_{N}, S_{N}

Since M has fewer let-expressions than N, by induction:

Γ ∪ {x : σ} ⊢ M[y ↦ W] : α_{N}, S_{N}

Since M[y ↦ W] has fewer let-expressions than N, by induction:

Γ ⊢ M[y ↦ W][x ↦ V] : α_{N}, S_{N}

Since:

M[y ↦ W][x ↦ N] = M[x ↦ N][y ↦ W [x ↦ N]]

we have that:

Γ ⊢ M[x ↦ V][y ↦ W [x ↦ V]] : α_{N}, S_{N}

Since M[x ↦ V][y ↦ W [x ↦ V]] is smaller than N, by induction:

Γ ⊢ (let (y W [x ↦ V]) M[x ↦ V]) : α_{N}, S_{N}

or, equivalently:

Γ ⊢ (let (y W) M)[x ↦ V] : α_{N}, S_{N}

and thus the lemma holds in this case.

• (inst): Since x ∈ F V [N], N = x, and the derivation on N must be:

Γ ∪ {x : σ} ⊢ x : α_{N}, S_{N}

where ψ is a substitution of fresh variables for \overline{α} and S_{N} = ψ(S_{V}) ∪ \{ψ(α_{V}) ≤ α_{N}}. If D is the derivation concluding

Γ ⊢ V : α_{V} , S_{V}

then ψ(D) is an analogous derivation concluding

Γ ⊢ V : ψ(α_{V}), ψ(S_{V})

Now N[x ↦ V] = V, and by the Flow Lemma 2.5.5:

Γ ⊢ V : α_{N}, S_{N}

as required.

Lemma 2.5.5 (Flow). If Γ ⊢ M : α, S then for all γ ∈ SetVar, Γ ⊢ M : γ, S′ with S ∪ {α ≤ γ} ⊧ S′.

Proof: By induction on the derivation Γ ⊢ M : α, S and by case analysis on the last step in this derivation.

• (var): In this case the derivation for M = x is:

Γ′ ∪ {x : β} ⊢ x : α, S

where S = {β ≤ α}. For any γ ∈ SetVar, let S′ = {β ≤ γ}, and then:

Γ′ ∪ {x : β} ⊢ x : γ, S′

with S ∪ {α ≤ γ} ⊧ S′, as required.

• (const): This case follows by reasoning similar to the (var) case.

• (label): The derivation for M = N^{l} must conclude:

\frac{Γ ⊢ N : β, S_{N}}{Γ ⊢ N^{l} : α, S} (label)

where S = S_{N} ∪ {β ≤ l, β ≤ α}. Let S′ = {β ≤ l, β ≤ γ}, and then:

\frac{Γ ⊢ N : β, S_{N}}{Γ ⊢ N^{l} : γ, S′} (label)

with S ∪ {α ≤ γ} ⊧ S′.

• (abs): The derivation for M = (λ^{t}x.N) must conclude:

\frac{Γ ∪ \{x : α_{1}\} ⊢ N : α_{2}, S_{N}}{Γ ⊢ (λ^{t}x.N) : α, S} (abs)

where S = {t ≤ α, dom(α) ≤ α_{1}, α_{2} ≤ rng(α)}. Let S = {t ≤ γ, dom(γ) ≤ α_{1}, α_{2} ≤ rng(γ)}, and then:

\frac{Γ ∪ \{x : α_{1}\} ⊢ N : α_{2}, S_{N}}{Γ ⊢ (λ^{x}N.:)γ, S} (abs)

with S ∪ {α ≤ γ} ⊧ S′.

• (app): This case follows by reasoning similar to the (app) case.

• (let): This case follows by induction.

• (abs): The derivation for M = x must be:

Γ ∪ \{x : ∀\overline{α}. (α_{V} , S_{V})\} ⊢ x : α, S

where S = ψ(S_{V}) ∪ \{ψ(α_{V}) ≤ α\}, and ψ is a substitution of set variables for \overline{α}. Let S′ = ψ(S_{V}) ∪ {ψ(α_{V}) ≤ γ}. Then

Γ ∪ \{x : ∀\overline{α}. (α_{V} , S_{V})\} ⊢ x : γ, S′

with S ∪ {α ≤ γ} ⊧ S′.

A.2 Proofs for Computing Set-Based Analysis

Lemma 2.6.2 (Least Solution of Simple Constraint Systems). Every simple constraint system has a solution that is least with respect to ⊑_{s}. Proof: Let S be a simple constraint system, and define ρ = _{⋂s}Soln(S), using the pointwise extension of_{⋂s} to set environments. We prove that ρ ∈ Soln(S) by showing that ρ satisfies any constraint C ∈ S. The proof proceeds by case analysis on C.

• The case where C = [α ≤ β] follows from Lemma A.2.1.

• Suppose C = [c ≤ β]. Then c ∈ const (ρ′(β)) for all ρ′ ∈ Soln(S), therefore c ∈ const (ρ(β)) and ρ ⊧ C.

• Suppose C = [α ≤ rng(β)]. Then:

ρ(α) = \begin{matrix}⋂ & s \\ ρ′∈Soln(S) \end{matrix} ρ′(α)
⊑ \begin{matrix}⋂ & s \\ ρ′∈Soln(S) \end{matrix} ρ′(rng(β))

by Lemma A.2.1, since ρ′(α) ⊑ ρ′(rng(β))

= rng (\begin{matrix}⋂ & s \\ ρ′∈Soln(S) \end{matrix} ρ′(β))  by definition of ⊓_{s}
= rng (ρ(β))
= ρ(rng(β))

Hence ρ ⊧ α ≤ rng(β).

The remaining cases are similar. Hence the set of environments satisfying S has a least element _{⋂s}{ρ | ρ ⊧ S}.

The following lemma describes some properties about how the two orderings ⊑ and ⊑_{s} defined on D interact. Lemma A.2.1 Let I be an index set, and let x_{i}, y_{i} ∈ D for all i ∈ I.

• If x_{i} ⊑ y_{i} for all i ∈ I, then:

\begin{matrix}\begin{matrix}⋂ & s \\ i∈I \end{matrix} x_{i} & ⊑ & \begin{matrix}⋂ & s \\ i∈I \end{matrix} y_{i} \\ \begin{matrix}⨆ & s \\ i∈I \end{matrix} x_{i} & ⊑ & \begin{matrix}⨆ & s \\ i∈I \end{matrix} y_{i} \end{matrix}

• If x_{i} ⊑_{s} y_{i} for all i ∈ I, then:

\begin{matrix}⊓_{i∈I} x_{i} & ⊑_{s} & ⊓_{i∈I} y_{i} \\ ⨆_{i∈I} x_{i} & ⊑_{s} & ⨆_{i∈I} y_{i} \end{matrix}

Proof: The proof is based on the interpretation of D as the set of total functions

f : {dom, rng}^{∗} ⟶ P(Const)

and proceeds by showing the appropriate relation holds between the sets of constant elements at any path in {dom, rng}^{∗}.

To prove the first relation, assume x_{i} ⊑ y_{i} for all i ∈ I, and let p be a path in {dom, rng}^{∗}. If p is monotonic, then p(x_{i}) ⊑ p(y_{i}). Hence:

p (\begin{matrix}⋂ & s \\ i∈I \end{matrix} x_{i}) = \begin{matrix}⋂ & s \\ i∈I \end{matrix} p(x_{i})
⊑ \begin{matrix}⋂ & s \\ i∈I \end{matrix} p(y_{i})

= p (\begin{matrix}⋂ & s \\ i∈I \end{matrix} y_{i})

Conversely, if p is anti-monotonic, then p(x_{i}) ⊒ p(y_{i}). Hence:

p (\begin{matrix}⋂ & s \\ i∈I \end{matrix} x_{i}) = \begin{matrix}⋂ & s \\ i∈I \end{matrix} p(x_{i})
⊒ \begin{matrix}⋂ & s \\ i∈I \end{matrix} p(y_{i})
= p (\begin{matrix}⋂ & s \\ i∈I \end{matrix} y_{i})

Hence

\begin{matrix}⋂ & s \\ i∈I \end{matrix} x_{i} ⊑ \begin{matrix}⋂ & s \\ i∈I \end{matrix} y_{i}

as required. Theorem 2.6.5 If P ∈ Λ^{0} and ∅ ⊢ P : α, S is a most general constraint derivation then:

sba(P)(l) = \begin{aligned}& \{b | S ⊢_{Θ} b ≤ l\} \\ ∪ & \{(λ^{t}x.M) | S ⊢_{Θ} t ≤ l\} \end{aligned}

Proof:

S ⊢_{Θ} c ≤ α ⟺ S ⊧ c ≤ α  by lemma A.2.2
⟺ ∀ρ ⊧ S. ρ ⊧ c ≤ α
⟺ ∀ρ ∈ Soln(S). c ∈ const(ρ(α))
⟺ c ∈ ⋂({const(ρ(α)) | ρ ∈ Soln(S)})
⟺ c ∈ const(⊓({ρ(α) | ρ ∈ Soln(S)}))
⟺ c ∈ const(⊓({ρ | ρ ∈ Soln(S)})(α))
⟺ c ∈ const(LeastSoln(S)(α))

The correctness of this theorem then follows from definition 2.6.3. Lemma A.2.2 (Soundness and Completeness of Θ). For any simple constraint system S:

S ⊧ c ≤ α ⟺ S ⊢_{Θ} c ≤ α

Proof: The soundness of Θ is straightforward. To prove the completeness of Θ, assume S ⊧ c ≤ α. Let ρ be any fixpoint of the functional F defined as:

F : SetEnv ⟶ SetEnv
F (ρ)(α) = ⟨ \begin{matrix}\{c | S ⊢_{Θ} c ≤ α\}, \\ ⨆\{ρ(γ) | S ⊢_{Θ} α ≤^{∗} δ, γ ≤ dom(δ)\}, \\ ⨆\{ρ(γ) | S ⊢_{Θ} γ ≤ rng(α)\} ⟩ \end{matrix}

where the notation S ⊢_{Θ} β ≤^{∗} δ means there exists some δ_{1}, …, δ_{n} with β ≡ δ_{1} and δ_{n} ≡ δ such that:

S ⊢_{Θ} {δ_{i} ≤ δ_{i+1}, | 1 ≤ i < n}

The asymmetry between the definition of the domain and range components F (ρ)(α) arises from the rules Θ. These rules propagate set variables denoting the result of functions in α forward along data-flow paths into constraints of the form γ ≤ rng(α). However, the same propagation does not occur for set variables denoting argument values to functions in α, and hence this propagation in performed in the definition of F (ρ)(α) by finding all γ such that γ ≤ dom(δ) and α ≤^{∗} δ.

If ρ ⊧ S, then ρ ⊧ c ≤ α and hence S ⊢_{Θ} c ≤ α by the definition of ρ, as required. Thus it just remains to prove that ρ ⊧ S. We proceed by case analysis on constraints C ∈ S.

• Suppose C = [α ≤ β]. We need to show that the correct ordering holds between the corresponding components of ρ(α) and ρ(β). For the first component, by (s_{1}), which is the first rule in Θ:

{c | S ⊢_{Θ} c ≤ α} ⊆ {c | S ⊢_{Θ} c ≤ β}
..^{.}  const (ρ(α)) ⊑ const (ρ(β))

For the second (domain) component, by (s_{3}):

[S ⊢_{Θ} β ≤^{∗} δ] ⇒ [S ⊢_{Θ} α ≤^{∗} δ]
..^{.} {ρ(γ) | S ⊢_{Θ} β ≤^{∗} δ, γ ≤ dom(δ)} ⊆ {ρ(γ) | S ⊢_{Θ} α ≤^{∗} δ, γ ≤ dom(δ)}
..^{.}⨆{ρ(γ) | S ⊢_{Θ} β ≤^{∗} δ, γ ≤ dom(δ)} ⊑ ⨆{ρ(γ) | S ⊢_{Θ} α ≤^{∗} δ, γ ≤ dom(δ)}
..^{.}  dom (ρ(β)) ⊑ dom (ρ(α))

For the third (range) component, by (s_{2}):

[S ⊢_{Θ} γ ≤ rng(α)] ⇒ [S ⊢_{Θ} γ ≤ rng(β)]
..^{.} {ρ(γ) | S ⊢_{Θ} γ ≤ rng(α)} ⊆ {ρ(γ) | S ⊢_{Θ} γ ≤ rng(β)}
..^{.} ⨆{ρ(γ) | S ⊢_{Θ} γ ≤ rng(α)} ⊑ ⨆{ρ(γ) | S ⊢_{Θ} γ ≤ rng(β)}
..^{.}  rng (ρ(α)) ⊑ rng (ρ(β))

Hence ρ(α) ⊑ ρ(β).

• Suppose C = [c ≤ β]:

ρ(β) ⊒ ⟨{c | S ⊢_{Θ} c ≤ β}, ⊤, ⊥⟩
⊒ ⟨{c}, ⊤, ⊥⟩
= ρ(c)

• Suppose C = [α ≤ rng(β)].

{ρ(α)} ⊆ {ρ(γ) | S ⊢_{Θ} γ ≤ rng(β)}
..^{.} ρ(α) ⊑ ⨆{ρ(γ) | S ⊢_{Θ} γ ≤ rng(β)}
= ρ(rng(β))

• Suppose C = [rng(α) ≤ β]. Then

ρ(β) ⊒ ρ(γ)  ∀S ⊢_{Θ} γ ≤ β
..^{.} ρ(β) ⊒ ⨆{ρ(γ) | S ⊢_{Θ} γ ≤ β}
⊒ ⨆{ρ(γ) | S ⊢_{Θ} γ ≤ rng(α)} by (s_{4})
= ρ(rng(α))

• Suppose C = [α ≤ dom(β)]. Then

ρ(α) ⊑ ⨆{ρ(γ) | S ⊢_{Θ} γ ≤ dom(β)}
⊑ ⨆{ρ(γ) | S ⊢_{Θ} β ≤^{∗} δ, γ ≤ dom(δ)}
= ρ(dom(β))

• Suppose S = [dom(α) ≤ β].

ρ(dom(α)) = ⨆{ρ(γ) | S ⊢_{Θ} α ≤^{∗} δ, γ ≤ dom(δ)}  by (s_{3})
⊑ _{⨆s}{ρ(γ) | S ⊢_{Θ} dom(δ) ≤ β, γ ≤ dom(δ)}
⊑ _{⨆s}{ρ(γ) | S ⊢_{Θ} γ ≤ β}
⊑ ρ(β)

Hence ρ ⊧ S, and the lemma holds.

Appendix B

Proofs for Chapter 5

B.1 Correctness of MkType

Lemma 4.2.1 (Correctness of MkType). If S is a simple constraint system then:

M[MkType(S, α)] = LeastSoln(S)(α)

Proof: By the definition of M and MkType:

M[MkType(S, α)] = ρ_{s}(α)

where ρ_{s} is the least fixed point under ⊑_{s} of the functional:

ρ ↦ M_{ρ}[MkType′(S, α_{i})]

where α_{i} ranges over SetVar(S) = {α_{1}, …, α_{n}}. Hence ρ_{s} is the least solution to the system of equalities:

ρ(α_{i}) = M_{ρ}[MkType′(S, α_{i})]

But (ignoring pairs to simplify the presentation):

M_{ρ}[MkType′(S, α_{i})] = ⟨ \begin{matrix}\{b | S ⊢_{Θ} b ≤ α_{i}\} ∪ \{t | S ⊢_{Θ} t ≤ α_{i}\}, \\ _{⨆s}\{ρ(β) | S ⊢_{Θ} α_{i} ≤^{∗} δ, β ≤ dom(δ)\}, \\ _{⨆s}\{ρ(β) | S ⊢_{Θ} β ≤ rng(α_{i})\} ⟩ \end{matrix}

Equating each component of ρ(α_{i}) with the corresponding component of the above tuple, we see that ρ_{s} must be the least solution to the system of equalities (1):

const(ρ(α_{i})) = {c | S ⊢_{Θ} c ≤ α_{i}}
dom (ρ(α_{i})) = _{⨆s}{ρ(β) | S ⊢_{Θ} α_{i} ≤^{∗} δ, β ≤ dom(δ)}
rng (ρ(α_{i})) = _{⨆s}{ρ(β) | S ⊢_{Θ} β ≤ rng(α_{i})}

An inductive argument shows that the system of equalities (1) holds if and only if the following system of equalities (2) also holds, where p ranges over paths:

const(p(ρ(α_{i}))) = {c | S ⊢_{Δ} c ≤ p(α_{i})}

Hence ρ_{s} is also the least solution to (2). But:

const(p(ρ(α_{i}))) = {c | ρ ⊧ c ≤ p(α_{i})} ,

hence ρ_{s} is the least solution for ρ to the following condition (3):

ρ ⊧ c ≤ p(α_{i}) ⟺ S ⊢_{Δ} c ≤ p(α_{i})

But (3) holds if and only if ρ ⊧ S. Therefore LeastSoln(S) = ρ_{s}, since ρ_{s} is the least solution to (3), and hence:

M[MkType(S, α)] = LeastSoln(S)(α)

as required.

Appendix C

Proofs for Chapter 6

C.1 Proofs for Conditions for Constraint Simplification

The following lemma demonstrates that the rule (≅) is admissible in that any derivation in the extended constraint derivation system produces information equivalent to that produced by the original analysis.

Lemma 6.1.1 (Admissibility of (≅)). If ∅ ⊢≅ P : α, S is a most general constraint derivation then:

sba(P)(l) = const(LeastSoln(S)(l))

Proof: This lemma follows from the induction hypothesis:

If Γ ⊢≅ M : α, S_{1}, and E = F V [range(Γ)] ∪ {α} ∪ Label, then there exists
S_{2} such that Γ ⊢ M : α, S_{2} and S_{1} ≅_{E} S_{2}.

We prove this hypothesis by induction on the derivation Γ ⊢≅ M : α, S_{1}, and by case analysis on the last step in the derivation.

• If the last step in the derivation Γ ⊢≅ M : α, S_{1} uses a derivation rule other that (≅), then the lemma holds based on the induction hypothesis.

• Suppose Γ ⊢≅ M : α, S_{1} via (≅) because Γ ⊢≅ M : α, S_{3} and S_{3} ≅_{E} S_{1}. By induction, Γ ⊢ M : α, S_{4} where S_{3} ≅_{E} S_{4}. Since ≅_{E} is an equivalence relation, S_{1} ≅_{E} S_{2}, and hence the lemma holds.

C.2 Proofs for Proof Theory of Observable Equivalence

The following proofs require a number of auxiliary definitions.

Definition C.2.1. (Paths)

• A path p, q ∈ Path is a sequence of the constructors dom and rng. We use ϵ to denote the empty sequence, and p.q to denote the concatenation of the paths p and q.

• The arity of a path p, denoted πp, is the number of dom’s in p, taken modulo 2. If πp is 0, we say p is monotonic, otherwise p is anti-monotonic.

• For a path p, the notation p(τ) denotes the set expression τ enclosed in the dom’s and rng’s of p, i.e., if p ≡ rng.dom, then p(α) ≡ rng(dom(α)).

• The relations ≤_{0} and ≤_{1} denote ≤ and ≥, respectively.

• The relations ⊑_{0} and ⊑_{1} denote ⊑ and ⊒, respectively.

• The relations ⊒_{0} and ⊒_{1} denote ⊒ and ⊑, respectively.

• The relations ⊆_{0} and ⊆_{1} denote ⊆ and ⊇, respectively.

• The operations ⨆_{0} and ⨆_{1} denote ⨆ and ⊓, respectively.

• For a path p and a domain element X ∈ D, the notation p(X) extracts the

component of X at the position p. This notation is formalized as follows:

ϵ(X) = X
(rng.p)(X) = rng (p(X))
(dom.p)(X) = dom (p(X))

• For a path p and a domain element X ∈ D, the notation X@p is defined as

follows:

·@· : D × path ⟶ D
X@ϵ = X
X@(dom.p) = ⟨∅, X, ⊥_{s}⟩@p
X@(rng.p) = ⟨∅, ⊥_{s}, X⟩@p

Lemma 6.2.1 (Soundness and Completeness of Δ). For a compound constraint system S and a compound constraint C:

S ⊢_{Δ} C ⟺ S ⊧ C Proof: The soundness of Δ is straightforward. To demonstrate the completeness of Δ, we assume S ⊧ C and prove that S ⊢_{Δ} C by case analysis on C.

• Suppose C = [c ≤ κ]. Define ρ by:

∀p ∈ Path. ∀α ∈ SetVar. const(p(ρ(α))) = {c | S ⊢_{Δ} c ≤ p(α)}

We prove ρ ⊧ S by a case analysis showing that ρ satisfies every constraint C′ ∈ S.

– Suppose C′ = [c ≤ q(β)]. Then, by the definition of ρ, c ∈ const(ρ(q(β))), and hence ρ ⊧ c ≤ q(β).

– Suppose C′ = [p(α) ≤ q(β)]. We need to show that ρ(p(α)) ⊑ ρ(q(β)). We prove this inequality by showing that for any path r:

const(r(ρ(p(α)))) ⊆_{πr} const(r(ρ(q(β))))

If r is monotonic, then:

const(r(ρ(p(α))))
= const(r(p(ρ(α))))
= {c | S ⊢_{Δ} c ≤ r(p(α))}
⊆ {c | S ⊢_{Δ} c ≤ r(q(β))}
via (trans_{τ}), since [p(α) ≤ q(β)] ∈ S
and hence S ⊢_{Δ} r(p(α)) ≤ r(q(β)) via (compat)
= const(r(q(ρ(β))))
= const(r(ρ(q(β))))

The case where r is anti-monotonic follows by a similar argument.

Hence ρ ⊧ S. But since S ⊧ c ≤ κ, ρ ⊧ c ≤ κ. Since κ = p(α) for some p and α, then we have that:

c ∈ const(ρ(p(α)))
= const(p(ρ(α)))
= {c | S ⊢_{Δ} c ≤ p(α)}

Hence, S ⊢_{Δ} c ≤ κ, as required.

• Suppose C = [κ_{1} ≤ κ_{2}]. Let c be a constant not used in S or C; let S′ = S ∪ {c ≤ κ_{1}}; and let ρ = LeastSoln(S′). Since ρ ⊧ C, we have that:

ρ ⊧ {c ≤ κ_{1}, κ_{1} ≤ κ_{2}}

Hence ρ ⊧ c ≤ κ_{2} and by the first part of this proof, S′ ⊢_{Δ} c ≤ κ_{2}.

We now show that for any κ′, S′ ⊢_{Δ} c ≤ κ′ if and only if S ⊢_{Δ} κ_{1} ≤ κ′. We prove this hypothesis by induction on the derivation of S′ ⊢_{Δ} c ≤ κ′.

– Suppose S′ ⊢_{Δ} c ≤ κ′ because [c ≤ κ′] ∈ S′. Then κ′ = κ_{1}, and by the rule

(reflex), S ⊢_{Δ} κ_{1} ≤ κ_{1}, as required.

– If [c ≤ κ′] ∉ S′, then S′ ⊢_{Δ} c ≤ κ′ must be derived via the rule (trans_{τ}) based on the antecedents S′ ⊢_{Δ} {c ≤ κ′′, κ′′ ≤ κ′}. By induction, S ⊢_{Δ}

κ_{1} ≤ κ′′. Hence S ⊢_{Δ} κ_{1} ≤ κ′ via (trans_{τ}), as required.

Since S′ ⊢_{Δ} c ≤ κ_{2}, the above induction hypothesis implies that S ⊢_{Δ} κ_{1} ≤ κ_{2}, as required.

Lemma 6.2.2 For a compound constraint system S, S ≅_{E} Δ(S) |_{E}.

Proof: We need to show that S ≅_{E} Δ(S) |_{E}, i.e.:

Soln(S) |_{E} = Soln(Δ(S) |_{E}) |_{E}

Since the rules Δ are sound:

Soln(S) |_{E} = Soln(Δ(S)) |_{E}
⊆ Soln(Δ(S) |_{E}) |_{E}

because the solution space increases as the constraints Δ(S) are restricted to E.

To show the containment in the other direction, assume ρ ⊧ Δ(S) |_{E}. Without loss of generality, assume ρ(α) = ⊥_{s} for all α ∉ E. We extend ρ to a superenvironment ρ′ that satisfies S as follows:

∀p ∈ Path. ∀α ∈ SetVar. const(p(ρ′(α))) = ⋃{const(ρ(τ)) | S ⊢_{Δ} τ ≤ p(α)}

We show that ρ′ ⊧ S by case analysis on the constraints C ∈ S.

• Suppose C = [c ≤ q(β)]. Then

const(q(β)) = ⋃{const(ρ(τ)) | S ⊢_{Δ} τ ≤ q(β)}
⊇ {c}

as required.

• Suppose C = [p(α) ≤ q(β)]. Then for any path r, S ⊢_{Δ} r(p(α)) ≤_{πr} r(q(β)).

Hence:

⋃{const(ρ(τ)) | S ⊢_{Δ} τ ≤ r(p(α))}
⊆_{πr} ⋃{const(ρ(τ)) | S ⊢_{Δ} τ ≤ r(q(β))}

Therefore:

const(ρ′(r(p(α)))) ⊆_{πr} const(ρ′(r(q(β))))

Hence:

ρ′(p(α)) ⊑ ρ′(q(β))

And hence ρ′ ⊧ C, as required.

Thus ρ′ ⊧ S. It remains to show that ρ and ρ′ agree on E. Let α ∈ E and r ∈ Path. Then:

const(ρ′(r(α))) = ⋃{const(ρ(τ)) | S ⊢_{Δ} τ ≤ r(α)}

by definition of ρ′

= ⋃{const(ρ(τ)) | S ⊢_{Δ} τ ≤ r(α), SetVar(τ) ⊆ E}

since ρ(β) = ⊥_{s} for β ∉ E

and hence ρ(τ) = ⊥_{s} for SetVar(τ) ⊈ E

= ⋃{const(ρ(τ)) | τ ≤ r(α) ∈ Δ(S) |_{E}}
= const(ρ(r(α)))

since [r(α) ≤ r(α)] ∈ Δ(S) |_{E} by (reflex) and (compat), and for [τ ≤ r(α)] ∈ Δ(S) |_{E}, const(ρ(τ)) ⊆ const(ρ(r(α))). Thus ρ and ρ′ agree on E, and the lemma holds.

Lemma C.2.2 For any p ∈ Path and X ∈ D, p(X@p) = X.

Proof: By induction on the length of p, and by case analysis on the top constructor in p.

Lemma 6.2.3 (Equivalence of Proof Systems). For a simple constraint system S:

Δ(S) = ΨΘ(S)

Proof: We show that ΨΘ(S) ⊆ Δ(S) by induction on the derivation of C ∈ ΨΘ(S). For the base case, if C ∈ ΨΘ(S) because C ∈ S, then C ∈ Δ(S). Otherwise we proceed by case analysis on the last rule used in the derivation of C ∈ ΨΘ(S).

• (compose_{1}): In this case C = [α ≤ rng(κ)] is derived from the antecedents {α ≤ rng(β), β ≤ κ} ∈ ΨΘ(S). By induction, these antecedents are also in Δ(S), and hence the following derivation shows that C ∈ Δ(S):

\frac{α ≤ rng(β)  \frac{β ≤ κ}{rng(β) ≤ rng(κ)} (compat)}{α ≤ rng(κ)} (trans_{τ})

• (compose_{2}), (compose_{3}), (compose_{3}): These cases follow by similar reasoning.

• (reflex), (trans_{α}), (compat): These rules are either equivalent to or subsumed by corresponding rules in Δ.

• (s_{1}), (s_{4}), (s_{5}): For these cases C ∈ Δ(S) via (trans_{τ}).

• (s_{2}), (s_{3}): These rules are special cases of the rules (compose_{1}) and (compose_{4}), respectively.

There are no other possibilities for the derivation C ∈ ΨΘ(S) \ Δ(S), and hence ΨΘ(S) ⊆ Δ(S).

We prove the converse inclusion Δ(S) ⊆ ΨΘ(S) by induction on the derivation of C ∈ Δ(S). Again, for the base case, if C ∈ Δ(S) because C ∈ S, then C ∈ ΨΘ(S). Otherwise we proceed by case analysis on the last rule used in the derivation of C ∈ Δ(S).

• (reflex), (compat): These rules are also in Ψ and, by induction, the antecedents are in ΨΘ(S), hence C ∈ ΨΘ(S).

• (trans_{τ}): The last step in the derivation must be:

\frac{τ_{1} ≤ τ  τ ≤ τ_{2}}{τ_{1} ≤ τ_{2}} (trans_{τ})

We proceed by case analysis on τ to show that [τ_{1} ≤ τ_{2}] ∈ ΨΘ(S).

– The case τ = c is impossible, since [τ_{1} ≤ c] is not a compound constraint.

– If τ ∈ SetVar, then [τ_{1} ≤ τ_{2}] ∈ ΨΘ(S) via (trans_{α}).

– Suppose τ = rng(τ′). If τ′ ∈ SetVar then [τ_{1} ≤ τ_{2}] ∈ ΨΘ(S) via (s_{4}). Otherwise τ_{1} ≤ rng(τ′) and rng(τ′) ≤ τ_{2} are not simple constraints, and we proceed by considering the derivation of these constraints in Δ(S). The last step in the derivation of τ_{1} ≤ rng(τ′) is either via:

\frac{α_{1} ≤ rng(β_{1}) β_{1} ≤ τ′}{α_{1} ≤ rng(τ′)} (compose_{1})

where τ_{1} = α_{1}, or:

\frac{τ′_{1} ≤ τ′}{rng(τ′_{1}) ≤ rng(τ′)} (compat)

where τ_{1} = rng(τ′_{1}). Similarly, the last step in the derivation of rng(τ′) ≤ τ_{2} is either via:

\frac{τ′ ≤ β_{2} rng(β_{2}) ≤ α_{2}}{rng(τ′) ≤ α_{2}} (compose_{3})

where τ_{2} = α_{2}, or:

\frac{τ′ ≤ τ′_{2}}{rng(τ′) ≤ rng(τ′_{2})} (compat)

where τ_{2} = rng(τ′_{2}). We consider the four possible combinations for the derivations of τ_{1} ≤ rng(τ′) and rng(τ′) ≤ τ_{2}:

∗ Suppose τ_{1} ≤ rng(τ′) is inferred via (compose_{1}) and rng(τ′) ≤ τ_{2} is inferred via (compose_{3}). Then {β_{1} ≤ τ′, τ′ ≤ β_{2}} ⊆ Δ(S), and therefore [β_{1} ≤ β_{2}] ∈ Δ(S) via (trans_{α}). By induction, [β_{1} ≤ β_{2}] ∈ ΨΘ(S), and the following derivation then shows that [τ_{1} ≤ τ_{2}] ∈ ΨΘ(S).

\frac{\frac{α_{1} ≤ rng(β_{1}) β_{1} ≤ β_{2}}{α_{1} ≤ rng(β_{2})} (s_{2}) rng(β_{2}) ≤ α_{2}}{α_{1} ≤ α_{2}} (s_{4})

∗ Suppose τ_{1} ≤ rng(τ′) is inferred via (compose_{1}) and rng(τ′) ≤ τ_{2} is inferred via (compat). Then {β_{1} ≤ τ′, τ′ ≤ τ′_{2}} ⊆ Δ(S), and therefore [β_{1} ≤ τ′_{2}] ∈ Δ(S) via (trans_{α}). By induction, [β_{1} ≤ τ′_{2}] ∈ ΨΘ(S), and the following derivation shows that [τ_{1} ≤ τ_{2}] ∈ ΨΘ(S).

\frac{α_{1} ≤ rng(β_{1}) β_{1} ≤ τ′_{2}}{α_{1} ≤ rng(τ′_{2})} (compose_{1})

∗ Suppose τ_{1} ≤ rng(τ′) is inferred via (compat) and rng(τ′) ≤ τ_{2} is inferred via (compose_{3}). This case holds by similar reasoning to the previous case.

∗ Suppose τ_{1} ≤ rng(τ′) is inferred via (compat) and rng(τ′) ≤ τ_{2} is inferred via (compat). Then {τ′_{1} ≤ τ′, τ′ ≤ τ′_{2}} ⊆ Δ(S), and therefore [τ′_{1} ≤ τ′_{2}] ∈ Δ(S) via (trans_{α}). By induction, [τ′_{1} ≤ τ′_{2}] ∈ ΨΘ(S), and therefore a (compat)-inference shows that [τ_{1} ≤ τ_{2}] ∈ ΨΘ(S).

There are no other possibilities for the derivations of τ_{1} ≤ rng(τ′) and rng(τ′) ≤ τ_{2}.

– Suppose τ = dom(τ′). This case holds by similar reasoning to the previous case where τ = rng(τ′).

There are no other possibilities for τ.

There are no other possibilities for the derivation of C ∈ Δ(S), and hence Δ(S) ⊆ ΨΘ(S).

Lemma 6.2.4 ΨΘ(S) |_{E} ≅ ΠΘ(S) |_{E}.

Proof: Since the rule (compat) does not create any Π or Θ opportunities, ΨΘ(S) = compat(ΠΘ(S)), and hence we just need to show that:

compat(ΠΘ(S)) |_{E} ≅ ΠΘ(S) |_{E}

Now:

compat(ΠΘ(S)) ⊇ ΠΘ(S)
..^{.} compat(ΠΘ(S)) |_{E} ⊇ ΠΘ(S) |_{E}
..^{.} compat(ΠΘ(S)) |_{E} ⊧ ΠΘ(S) |_{E}

To prove the converse direction, let ρ ⊧ ΠΘ(S) |_{E}. If ρ |̸= compat(ΠΘ(S)) |_{E}, then let C be the constraint in compat(ΠΘ(S)) |_{E} with the smallest derivation such that ρ |̸= C. Then the last step in the derivation of C must be via (compat). Let C′ be the antecedent of this rule in compat(ΠΘ(S)). Then SetVar(C′) = SetVar(C) ⊆ E, and hence C′ ∈ compat(ΠΘ(S)) |_{E} with a smaller derivation. Therefore ρ ⊧ C′, and hence since (compat) is sound, ρ ⊧ C. Thus ρ |̸= compat(ΠΘ(S)) |_{E}, as required.

Theorem 6.2.6 [Soundness and Completeness of ⊢_{ΨΘ}^{E} and =_{ΨΘ}^{E}]

1. S_{1} ⊢_{ΨΘ}^{E} S_{2} if and only if S_{1} ⊧_{E} S_{2}.

2. S_{1} =_{ΨΘ}^{E} S_{2} if and only if S_{1} ≅_{E} S_{2}.

1. Suppose S_{1} ⊧_{E} S_{2}. Then

S_{1} ⊧_{E} Δ(S_{2})  by the soundness of Δ
..^{.} S_{1} ⊧_{E} Δ(S_{2}) |_{E}
..^{.} ∀C ∈ Δ(S_{2}) |_{E}. S_{1} ⊧ C
..^{.} ∀C ∈ Δ(S_{2}) |_{E}. S_{1} ⊢_{Δ} C  by Lemma 6.2.1
..^{.} ∀C ∈ ΠΘ(S_{2}) |_{E}. S_{1} ⊢_{Δ} C  by Lemma 6.2.3
..^{.} ∀C ∈ ΠΘ(S_{2}) |_{E}. S_{1} ⊢_{ΨΘ} C  by Lemma 6.2.3
..^{.} ∀C ∈ ΠΘ(S_{2}) |_{E}. C ∈ ΨΘ(S_{1}) |_{E}
..^{.} ΨΘ(S_{1}) |_{E} ⊇ ΠΘ(S_{2}) |_{E}
..^{.} S_{1} ⊢_{ΨΘ}^{E} S_{2}

Conversely, suppose S_{1} ⊢_{ΨΘ}^{E} S_{2}. Then

ΨΘ(S_{1}) |_{E} ⊇ ΠΘ(S_{2}) |_{E}

..^{.} Soln(ΨΘ(S_{1}) |_{E}) ⊆ Soln(ΠΘ(S_{2}) |_{E})
..^{.} Soln(ΨΘ(S_{1}) |_{E}) |_{E} ⊆ Soln(ΠΘ(S_{2}) |_{E}) |_{E}
..^{.} Soln(S_{1}) |_{E} ⊆ Soln(S_{2}) |_{E}

by Lemmas 6.2.2, 6.2.3 and 6.2.4, since Soln(S_{i}) |_{E} = Soln(ΠΘ(S_{i}) |_{E}) |_{E}

..^{.} S_{1} ⊧_{E} S_{2}

2. Follows from part 1.

C.3 Proofs for Deciding Observable Equivalence

We repeat definition 6.3.1 here, to avoid having to refer back to the original definition earlier in the text.

Definition 6.3.1 (Regular Grammar G_{r}(S, E)) Let S be a simple constraint system and E a collection of set variables. The regular grammar G_{r}(S, E) consists of the non-terminals {α_{L}, α_{U} | α ∈ SetVar(S)} and the following productions:

α_{U} ↦ α, α_{L} ↦ α  ∀ α ∈ E
α_{U} ↦ β_{U}, β_{L} ↦ α_{L}  ∀ [α ≤ β] ∈ S
α_{U} ↦ dom(β_{L})  ∀ [α ≤ dom(β)] ∈ S
α_{U} ↦ rng(β_{U})  ∀ [α ≤ rng(β)] ∈ S
β_{L} ↦ dom(α_{U})  ∀ [dom(α) ≤ β] ∈ S
β_{L} ↦ rng(α_{L})  ∀ [rng(α) ≤ β] ∈ S

Lemma 6.3.2 Let G = G_{r}(S, E). Then:

L_{G}(α_{L}) = {κ | [κ ≤ α] ∈ Π(S) and SetVar(κ) ⊆ E}
L_{G}(α_{U}) = {κ | [α ≤ κ] ∈ Π(S) and SetVar(κ) ⊆ E}

Proof: We prove the left-to-right inclusion by induction on the derivation of the constraint C ∈ Ψ(S), and by case analysis on the last step in that derivation.

• Suppose C ∈ Ψ(S) because C ∈ S. We proceed by case analysis on C.

– Suppose C = [α ≤ β]. Then α ∈ E, so β_{L} ↦ α_{L} and α_{L} ↦ α are productions in the grammar. Hence α ∈ L_{G}(β_{L}). Similarly, β ∈ L_{G}(α_{U}).

The remaining cases for C follow by similar reasoning.

• Suppose C = [α ≤ rng(κ)] is inferred via (compose_{1}) from the antecedents [α ≤ rng(β)] and [β ≤ κ]. Then α_{U} ↦ rng(β_{U}), and by induction β_{U} ↦^{∗} κ. Hence α_{U} ↦ rng(κ), as required.

The remaining cases follow by similar reasoning.

We prove the right-to-left inclusion by induction on the derivation α_{L} ↦^{∗} κ or α_{U} ↦^{∗} κ, and by case analysis on the last step in the derivation. The reasoning for each case is straightforward.

We repeat definition 6.3.3 here, to avoid having to refer back to the original definition earlier in the text.

Definition 6.3.3 (Regular Tree Grammar G_{t}(S, E)) The regular tree grammar G_{t}(S, E) extends the grammar G_{r}(S, E) with the root non-terminal R and the additional productions:

\begin{matrix}R ↦ [α_{L} ≤ α_{U}] & ∀ α ∈ SetVar(S) \\ R ↦ [c ≤ α_{U}] & ∀ [c ≤ α] ∈ S \end{matrix}

where [· ≤ ·] is viewed as a binary constructor.

Lemma 6.3.4 Let G = G_{t}(S, E). Then Π(S) |_{E} = L_{G}(R).

Proof: We prove the left-to-right inclusion by case analysis on C ∈ Π(S) |_{E}.

• Suppose C = [α ≤ κ]. Then by Lemma 6.3.2, α_{U} ↦_{G}^{∗} κ. Since SetVar(C) ⊆ E, α ∈ E, and hence α_{L} ↦_{G} α. Thus R ↦_{G} [α_{L} ≤ α_{U}] ↦_{G}^{∗} [α ≤ κ], and hence [α ≤ κ] ∈ L_{G}(R).

• The case where C = [κ ≤ α] follows by similar reasoning.

• Suppose C = [c ≤ κ]. If C ∈ S, then κ = α, α ∈ E, and

R ↦_{G} [c ≤ α_{U}] ↦_{G} [c ≤ α]

as required. If C ∉ S, then an examination of the inference rules in Π shows that C can only be inferred via (trans_{α}), based on the antecedents [c ≤ α] and [α ≤ κ]. By Lemma 6.3.2, α_{L} ↦_{G}^{∗} c and α_{U} ↦_{G}^{∗} κ. Hence R ↦ [c ≤ κ], and hence [c ≤ κ] ∈ L_{G}(R), as required.

• Otherwise C = [κ_{1} ≤ κ_{2}], where κ_{1}, κ_{2} ∉ SetVar. An examination of the inference rules in Π shows that C can only be inferred via (trans_{α}), based on the antecedents [κ_{1} ≤ α] and [α ≤ κ_{2}]. By Lemma 6.3.2, α_{L} ↦_{G}^{∗} κ_{1} and α_{U} ↦_{G}^{∗} κ_{2}. Hence R ↦ [κ_{1} ≤ κ_{2}], and hence [κ_{1} ≤ κ_{2}] ∈ L_{G}(R), as required.

We prove the right-to-left inclusion by case analysis on C ∈ L_{G}(R).

• Suppose C = [κ_{1} ≤ κ_{2}]. Then for some α, α_{L} ↦_{G}^{∗} κ_{1} and α_{U} ↦_{G}^{∗} κ_{2}. By Lemma 6.3.2, {κ_{1} ≤ α, α ≤ κ_{2}} ⊆ Ψ(S) and SetVar(κ_{i}) ⊆ E. By Lemma 6.3.5, {κ_{1} ≤ α, α ≤ κ_{2}} ⊆ Π(S). Hence [κ_{1} ≤ κ_{2}] ∈ Π(S) |_{E}, as required.

• Otherwise C = [c ≤ κ]. Then for some α, [c ≤ α] ∈ S and α_{U} ↦_{G}^{∗} κ. By Lemma 6.3.2, {α ≤ κ} ⊆ Ψ(S) and SetVar(κ) ⊆ E. By Lemma 6.3.5, {α ≤ κ} ⊆ Π(S). Hence [c ≤ κ] ∈ Π(S) |_{E}, as required.

Lemma 6.3.5 (Staging) For any simple constraint system S:

ΨΘ(S) = Ψ(Θ(S)) = compat(Π(Θ(S)))

Proof: The equality Ψ(Θ(S)) = compat(Π(Θ(S))) holds since (compat) does not create any Π or Θ opportunities.

The inclusion ΨΘ(S) ⊇ Ψ(Θ(S)) obviously holds. To prove the inclusion ΨΘ(S) ⊆ Ψ(Θ(S)) holds, we suppose S ⊢_{ΨΘ} C, and prove Θ(S) ⊢_{Ψ} C by induction on the derivation S ⊢_{ΨΘ} C, and by case analysis on the last step in this derivation.

• Suppose S ⊢_{ΨΘ} C via some rule in Ψ. By induction, the antecedents of this rule are in Ψ(Θ(S)), and hence C is also in Ψ(Θ(S)).

• Suppose S ⊢_{ΨΘ} C via one of the rules (s_{1}), (s_{2}) or (s_{3}). These rules are subsumed by (trans_{α}), (compose_{1}) and (compose_{4}), and hence this case is subsumed by the previous case.

• Suppose S ⊢_{ΨΘ} C via (s_{4}), based on the antecedents {α ≤ rng(β), rng(β) ≤ γ}. By induction, these antecedents are in Ψ(Θ(S)). An examination of Ψ shows that Ψ can only infer [α ≤ rng(β)] if there exists α′, β′ such that Θ(S) contains the constraints:

α ≤^{∗} α′ α′ ≤ rng(β′) β′ ≤^{∗} β

Similarly, Ψ can only infer [rng(β) ≤ γ] if there exists β′′, γ′ such that Θ(S) contains the constraints:

β ≤^{∗} β′′ rng(β′′) ≤ γ′ γ′ ≤^{∗} γ

Hence:

S ⊢_{Θ} α′ ≤ rng(β′′) via multiple applications of (s_{2})
S ⊢_{Θ} α′ ≤ γ′  via (s_{4})
Θ(S) ⊢_{Ψ} α ≤ γ  via multiple applications of (trans_{α})

• The case for (s_{5}) holds by similar reasoning.

C.4 Correctness of the Entailment Algorithm

Theorem 6.3.6 (Correctness of the Entailment Algorithm). S_{2} ⊢_{Ψ}^{E} S_{1} if and only if S_{2} ⊢_{alg}^{E} S_{1}.

Proof: The definitions of the computable entailment relation and the relation R are shown in figure C.1. We prove this theorem based on the following invariant concerning the relation R_{S_{1},S_{2}}[·, ·, ·, ·]:

R_{S_{1},S_{2}}[α_{L}, β_{U}, C, D]  ⟺  L([α_{L} ≤ β_{U}]) ⊆ compat(L(C)) ∪ L(D)

Assume this relation holds, and that S_{2} ⊢_{Ψ}^{E} S_{1}. Then Π(S_{1}) |_{E} ⊆ compat(Π(S_{2})) |_{E}. By lemma 6.3.4, Π(S_{i}) |_{E} = L_{G_{i}}(R), and hence:

L_{G_{1}}(R) ⊆ compat(L_{G_{2}}(R))

Thus, for all R ↦_{G_{1}} [α_{L} ≤ α_{U}]:

L_{G_{1}}([α_{L} ≤ α_{U}]) ⊆ compat(L_{G_{2}}(R))
..^{.} L_{G_{1}}([α_{L} ≤ α_{U}]) ⊆ compat(L_{G_{2}}({⟨γ_{L}, γ_{U}⟩ | γ ∈ SetVar(S_{2})}))

Hence:

R_{S_{1},S_{2}}[α_{L}, α_{U}, {⟨γ_{L}, γ_{U}⟩ | γ ∈ SetVar(S_{2})}, ∅]

Also, from L_{G_{1}}(R) ⊆ compat(L_{G_{2}}(R)), we have that for all R ↦_{G_{1}} [c ≤ α_{U}]:

L_{G_{1}}([c ≤ α_{U}]) ⊆ compat(L_{G_{2}}(R))
..^{.} L_{G_{1}}([c ≤ α_{U}]) ⊆ L_{G_{2}}(R)
..^{.}  L_{G_{1}}(α_{U}) ⊆ L_{G_{2}}({γ_{U} | R ↦_{G} _{2}[c ≤ γ_{U}]})

Hence S_{2} ⊢_{alg}^{E} S_{1} holds. The proof of the converse implication that S_{2} ⊢_{alg}^{E} S_{1} implies S_{2} ⊢_{Ψ}^{E} S_{1} proceeds by a similar argument.

It remains to show that the invariant concerning R holds. To prove the left-to-right direction, suppose R_{S_{1},S_{2}}[α_{L}, β_{U}, C, D] and:

\begin{matrix}α_{L} & ↦_{G_{1}} X & ↦_{G_{1}}^{∗} τ_{L} \\ β_{U} & ↦_{G_{1}} Y & ↦_{G_{1}}^{∗} τ_{U} \end{matrix}

The Entailment Algorithm

In the following, P_{fin} denotes the finite power-set constructor. Let:

G_{1} = G_{t}(S_{1}, E)_{G_{2} = G_{t}(S_{2}, E)} L_{i} = {α_{L} | α ∈ SetVar(S_{i})}

U_{i} = {α_{U} | α ∈ SetVar(S_{i})}

Let G_{1} and G_{2} be pre-processed to remove ϵ-transitions. For C ∈ P_{fin}(L_{2} × U_{2}), define:

L_{G_{2}}(C) = {[τ_{L} ≤ τ_{U}] | ⟨α_{L}, β_{U}⟩ ∈ C, α_{L} ↦_{G_{2}} τ_{L}, β_{U} ↦_{G_{2}} τ_{U}}

The relation R_{S_{1},S_{2}}[·, ·, ·, ·] is defined as the largest relation on

L_{1} × U_{1} × P_{fin}(L_{2} × U_{2}) × P_{fin}(L_{2} × U_{2})

such that if:

R_{S_{1},S_{2}}[α_{L}, β_{U}, C, D]
α_{L} ↦_{G_{1}} X
β_{U} ↦_{G_{1}} Y

then one of the following cases hold:

1. L_{G_{1}}([X ≤ Y]) ⊆ L_{G_{2}}(C ∪ D).

2. X = rng(α′_{L}), Y = rng(β′_{U}) and R_{S_{1},S_{2}}[α′_{L}, β′_{U}, C, D′], where D′ = {⟨γ′_{L}, δ′_{U}⟩ | ⟨γ_{L}, δ_{U}⟩ ∈ C ∪ D, γ_{L} ↦_{G_{2}} rng(γ′_{L}), δ_{U} ↦_{G_{2}} rng(δ′_{U})}

3. X = dom(α′_{U}), Y = dom(β′_{L}) and R_{S_{1},S_{2}}[β′_{L}, α′_{U}, C, D′], where D′ = {⟨δ′_{L}, γ′_{U}⟩ | ⟨γ_{L}, δ_{U}⟩ ∈ C ∪ D, γ_{L} ↦_{G_{2}} dom(γ′_{U}), δ_{U} ↦_{G_{2}} dom(δ′_{L})}

4. In no other cases does R_{S_{1},S_{2}}[α_{L}, β_{U}, C, D] hold. The computable entailment relation S_{2} ⊢_{alg}^{E} S_{1} holds if and only if:

1. ∀R ↦_{G_{1}} [α_{L} ≤ α_{U}]. R_{S_{1},S_{2}}[α_{L}, α_{U}, {⟨γ_{L}, γ_{U}⟩ | γ ∈ SetVar(S_{2})}, ∅], and 2. ∀R ↦_{G_{1}} [c ≤ α_{U}]. L_{G_{1}}(α_{U}) ⊆ L_{G_{2}}({γ_{U} | R ↦_{G_{2}} [c ≤ γ_{U}]}).

Figure C.1 The computable entailment relation ⊢_{alg}^{E} We prove by induction on τ_{L} that

L([τ_{L} ≤ τ_{U}]) ⊆ compat(L(C)) ∪ L(D)

One of three cases in the definition of R must hold.

1. L([α_{L} ≤ β_{U}]) ⊆ L(C ∪ D). This case is trivial.

2. In this case:

X = rng(α′_{L})  α′_{L} ↦_{G_{1}}^{∗} τ′_{L}  τ_{L} = rng(τ′_{L})
Y = rng(β′_{U})  β′_{U} ↦_{G_{1}}^{∗} τ′_{U}  τ_{U} = rng(τ′_{U})

and R_{S_{1},S_{2}}[α′_{L}, β′_{U}, C, D′], where

D′ = {⟨γ′_{L}, δ′_{U}⟩ | ⟨γ_{L}, δ_{U}⟩ ∈ C ∪ D, γ_{L} ↦_{G_{2}} rng(γ′_{L}), δ_{U} ↦_{G_{2}} rng(δ′_{U})}

By induction, [τ′_{L} ≤ τ′_{U}] ∈ compat(L(C)) ∪ L(D′).

• If [τ′_{L} ≤ τ′_{U}] ∈ L(D′) then there exists ⟨γ′_{L}, δ_{U}⟩ ∈ D such that γ′_{L} ↦_{G_{2}}^{∗} τ′_{L} and δ′_{U} ↦_{G_{2}}^{∗} τ′_{U}. By the definition of D′, there exists ⟨γ_{L}, δ_{U}⟩ ∈ C ∪ D such that γ_{L} ↦_{G_{2}}^{∗} τ_{L} and δ_{U} ↦_{G_{2}}^{∗} τ_{U}. Therefore [τ_{L} ≤ τ_{U}] ∈ L(C ∪ D), as required.

• If [τ′_{L} ≤ τ′_{U}] ∈ compat(L(C)) then [τ_{L} ≤ τ_{U}] ∈ compat(L(C)), as required.

3. The proof for the third case of the definition of R_{S_{1},S_{2}}[·, ·, ·, ·] is similar to that for the second case.

To prove the right-to-left direction, suppose:

L([α_{L} ≤ β_{U}]) ⊆ compat(L(C)) ∪ L(D)

and that the relation R_{S_{1},S_{2}}[α_{L}, β_{U}, C, D] does not hold. Hence there exists X, Y such that α_{L} ↦_{G_{1}} X and β_{U} ↦_{G_{1}} Y and none of the three conditions in figure C.1 hold. Furthermore, since R is the largest relation satisfying the conditions in figure C.1, there exists a finite proof that none of the three conditions hold.

Of all possible such counter-examples ⟨α_{L}, β_{U}, X, Y, C, D⟩, we pick the one with the smallest proof that the relation R_{S_{1},S_{2}}[α_{L}, β_{U}, C, D] does not hold, and proceed by case analysis on the last step in this proof.

• Suppose R_{S_{1},S_{2}}[α_{L}, β_{U}, C, D] does not hold because of condition one. Then L([X ≤ Y]) ⊈ L(C ∪ D), which contradicts the assumptions above.

• Suppose R_{S_{1},S_{2}}[α_{L}, β_{U}, C, D] does not hold because of condition 2. Then X = rng(α′_{L}) and Y = rng(β′_{U}). Consider any pair of set expressions τ_{L} and τ_{U} such that α′_{L} ↦_{G_{1}}^{∗} τ_{L} and β′_{U} ↦_{G_{1}}^{∗} τ_{U}. We consider the two possibilities for [rng(τ_{L}) ≤ rng(τ_{U})] ∈ compat(L(C)) ∪ L(D) separately.

– If [rng(τ_{L}) ≤ rng(τ_{U})] ∈ L(C) ∪ L(D), then there exists ⟨γ_{L}, δ_{U}⟩ ∈ C ∪ D

such that:

γ_{L} ↦_{G_{2}} rng(γ′_{L}) ↦_{G_{2}}^{∗} rng(τ_{L})
δ_{U} ↦_{G_{2}} rng(δ′_{U}) ↦_{G_{2}}^{∗} rng(τ_{U})

Hence [τ_{L} ≤ τ_{U}] ∈ L(D′), where:

D′ = {⟨γ′_{L}, δ′_{U}⟩ | ⟨γ_{L}, δ_{U}⟩ ∈ C ∪ D, γ_{L} ↦_{G_{2}} rng(γ′_{L}), δ_{U} ↦_{G_{2}} rng(δ′_{U})}

– Otherwise [rng(τ_{L}) ≤ rng(τ_{U})] ∈ compat(L(C)) \ L(C), and hence [τ_{L} ≤ τ_{U}] ∈ compat(L(C)).

Hence

L([α′_{L} ≤ β′_{U}]) ⊆ compat(L(C)) ∪ L(D′)

The proof that R_{S_{1},S_{2}}[α_{L}, β_{U}, C, D] does not hold cannot rely on a smaller proof that R_{S_{1},S_{2}}[α′_{L}, β′_{U}, C, D′] does not hold, since that would yield a counterexample with a smaller proof.

• The case where R_{S_{1},S_{2}}[α_{L}, β_{U}, C, D] does not hold because of condition 3 is also impossible via similar reasoning.

Thus the invariant on R is true, and thus the lemma holds.

C.5 Correctness of the Hopcroft Algorithm

Theorem 6.4.1 (Correctness of the Hopcroft Algorithm). Let S be a simple constraint system with external variables E; let ∼ be an equivalence relation on the set variables in a constraint system S satisfying conditions (a) to (e) from figure 6.5; let the substitution f map each set variable to a representation element of its equivalence class; and let S′ = f(S), i.e., S′ denotes the constraint system S with set variables merged according to their equivalence class. Then S ≅_{E} S′.

Proof: Let ρ be a solution of S. Define ρ′ by:

ρ′(α) = ⨆_{α′∼α} ρ(α′)

Obviously ρ, ρ′ agree on E by condition (a) on ∼. We claim that ρ′ ⊧ C for all C ∈ S by case analysis on C.

• Suppose C = [α ≤ rng(β)]. Then for all α′ such that α ∼ α′ there exists β′ such

that β ∼ β′ and:

ρ(α′) ⊑ ρ(rng(β′))

Hence for all α ∼ α′:

ρ(α′) ⊑ ⨆_{β′∼β} ρ(rng(β′))

and therefore:

⨆_{α′∼α} ρ(α′) ⊑ ⨆_{β′∼β} ρ(rng(β′))

Hence:

ρ′(α) = ⨆_{α′∼α} ρ(α′)
⊑ ⨆_{β′∼β} ρ(rng(β′))

= rng ( ⨆_{β′∼β} ρ(β′))
= rng (ρ′(β))
= ρ′(rng(β))

and thus ρ′ ⊧ C, as required.

• The cases where C = [α ≤ β] and C = [rng(α) ≤ β] follow by similar reasoning.

• Suppose C = [α ≤ dom(β)]. Then ∀α ∼ α′ ∀β ∼ β′ such that:

ρ(α′) ⊑ ρ(dom(β′))

Hence ∀α ∼ α′:

ρ(α′) ⊑ ⊓_{β′∼β} ρ(dom(β′))

and therefore:

⨆_{α′∼α} ρ(α′) ⊑ ⊓_{β′∼β} ρ(dom(β′))

Hence:

ρ′(α) = ⨆_{α′∼α} ρ(α′)
⊑ ⊓_{β′∼β} ρ(dom(β′))
= dom ( ⨆_{β′∼β} ρ(β′))
= dom (ρ′(β))
= ρ′(dom(β))

• Suppose C = [dom(β) ≤ α]. Then:

ρ′(dom(β)) = dom (ρ′(β))
= dom ( ⨆_{β′∼β} ρ(β′))
= ⊓_{β′∼β} ρ(dom (β′))
⊑ ρ(dom (β))
⊑ ρ(α)
⊑ ⨆_{α′∼α} ρ(α′)
= ρ′(α)

• Suppose C = [c ≤ α]. Then

ρ′(α) = ⨆_{α′∼α} ρ(α′)
⊒ ρ(α)
= c

Appendix D

MrSpidey Reference Manual

MrSpidey is an interactive, static debugger for Scheme designed to help programmers understand and debug complex programs. It automatically infers information about the run-time behavior of programs, and uses this information to identify potential “danger-points” in those programs. Specifically, MrSpidey:

• infers a type, or value set invariant, describing the set of possible values for each program expression;

• uses this information to identify unsafe program operations that may cause run-time errors; and

• provides a supporting graphical explanation for these invariants.

MrSpidey supports almost all of DrScheme, which is an extension of R4RS Scheme with structures, a module system, an object system, and a GUI toolbox. For further information on the technology underlying MrSpidey, see [14, 15, 16, 13].

Thanks: Many thanks to both Matthew Flatt and Robby Findler for MrEd, and to Shriram Krishnamurthi for Zodiac, his source-correlating macro-expander. MrSpidey crucially depends on both of these packages. Thanks also to Stephanie Weirich for work on the first implementation of MrSpidey, and to Matthias Felleisen, Corky Cartwright, Jeremy Buhler, and the Rice University Spring ’96 COMP311 programming languages class for their feedback and help.

The typesetting sources for this manual are taken from Reference Manual for wxWindows 1.60: a portable C++ GUI toolkit.

D.1 Using MrSpidey

MrSpidey is an integrated portion of DrScheme. To analyze the current program in DrScheme, click on DrScheme’s Analyze button. MrSpidey analyzes the program and displays the analysis results in a new frame. This frame contains two sub-windows: a program window and a summary window. The display of these windows is controlled via the Show menu.

D.1.1 The Program Window

The program window contains an annotated version of original program. The additional annotations present information about the results of the analysis, as described below.

Unsafe Operations

An unsafe operation is one which may be applied to inappropriate arguments, thus raising an error. Unsafe operations are a natural starting point for static debugging. MrSpidey highlights these unsafe operations via font and color changes, as follows:

• Any primitive operation that may be applied to inappropriate arguments, thus raising a run-time error, is highlighted in red (or underlined on monochrome screens).^{∗} Conversely, primitive operations that never raise errors are shown in green.

• Any function that may be applied to an incorrect number of arguments is highlighted by displaying the lambda keyword in red (or underlined).

• Any application expression where the function position may return a nonfunction is highlighted by displaying the enclosing parentheses in red (or underlined).

Figure D.1 contains examples of these three different kinds of unsafe operations. The tab key moves the focus forward to the next unsafe operation, and the shift-tab key moves the focus backward to the previous unsafe operation. These keystrokes make it easy to inspect the unsafe operations in a program.

∗Certain unsafe operations, such as a vector-ref operation whose index argument may be out-of-range, are not detected. A list of such operations is contained in section D.6.

Figure D.1 Identifying unsafe operations

Popup Menus

MrSpidey also computes significant additional information for each analyzed expression. This information is available on a demand-driven basis via pop-up menus. MrSpidey associates a pop-up menu with all program variables, which are marked in bold, and also with the opening parenthesis of each expression, which is also marked in bold: see figure 5.2. Clicking on one of these bold tokens displays the associated menu, which then provides access to additional type and value flow information, as described below.

Type Information

MrSpidey provides an inferred type for each program expression. To view the type of an expression, select the Show Value Set option of the expression’s menu. Mrspidey then computes the expression’s type and displays it in a box inserted to the right of

Figure D.2 The pop-up menu

the expression, as illustrated in figure D.3. See Section D.4 for a complete description of the type language. The type box is deleted by selecting the Close Value Set option from the popup menu. Alternatively, selecting Clear|Types deletes all type boxes in the buffer.

The Value Flow Browser

MrSpidey can also explain the derivation of each value set invariant, or type. This explanation describes how the flow of values through the program yields a particular value set invariant. The collection of all potential paths along which value may flow through the program forms the program’s value flow graph. MrSpidey describes each edge in the data-flow graph as an arrow overlaid on the program text that connects the relevant points of the program. Because a large number of arrows would clutter the program text, these arrows are presented in a demand-driven fashion. Each expression’s popup menu provides facilities for inspecting relevant portions of the value flow graph.

Figure D.3 Displaying type information

• Parents: exposes arrows indicating the immediate parents of the current expression in the value flow graph. For example, figure D.4 shows the incoming edges for the parameter tree in the program sum.

• Ancestors: exposes all ancestors of the current expression in the value flow graph.

• Path to Source: finds the shortest path in the value flow graph from a constructor expression to the current expression.

• Children: exposes the immediate children of the current expression in the value flow graph.

• Descendants: exposes all descendants of the current expression in the value flow graph.

All of the above options can be customized to show only the flow of certain values by selecting the appropriate set of values from the Filter menu. This option is particularly useful in conjunction with the Path to Source facility for inspecting the flow of an unexpected value through the program. For example, in the program sum, the unexpected value for tree is nil. Setting the filter to this value, and then selecting Path to Source for tree results in the explanation described in figure D.5.

Figure D.4 Parents of tree Figure D.5 Flow of nil

Clicking on the head or tail of an arrow with the left mouse button moves the current focus to the term at the other end of the arrow, which can be useful for following the flow of values through large programs. Clicking on the head or tail of an arrow with the right mouse button deletes the arrow. Alternatively, selecting Clear|Arrows deletes all arrows in the buffer.

D.1.2 The Summary Window

The summary window lists all unsafe operations in the program, together with hyperlinks to those operation. It counts the number of unsafe operations, and expresses that number as a percentage of the total number of operations in the program. This window also contains warning about unbound variables and failed type assertions. A typical summary window is show in figure D.1.

D.2 Preferences

The Edit|Preferences ... menu item menu allows users to configure a variety of DrScheme options. Two of the preferences windows, MrSpidey Analysis and MrSpidey Type Display, control aspects of MrSpidey’s behavior. (These windows are only available after MrSpidey is loaded.)

D.2.1 MrSpidey Analysis Preferences Window

The MrSpidey Analysis preferences window configures MrSpidey’s analysis of programs. An example of this window is shown in figure D.6, and the controls are described below.

• Accurate constant types: When this button is off (default), then character, symbolic and numeric constants are given the types char, sym or num respectively. If the button is on, then these constants are typed accurately, i.e., the number 4 is assigned the type 4, etc.

• Constant merge size: Large quoted values in Scheme can yield large types that significantly increase the analysis time. To overcome this problem, MrSpidey generates approximate types for such constants. The Constant merge size slider controls how large constants can get before MrSpidey starts to approximate their type.

Figure D.6 MrSpidey Analysis preferences window

• If splitting: If this button is on (default), MrSpidey is smart about conditional expressions such as (if (number? x) …). MrSpidey only propagates numeric values for x in the then-part, and non-numbers in the else-part.

• Flow sensitivity: If this button is on (default), then after an expression such as (car x), MrSpidey knows that the value of x must be a pair.

• Accurate analysis of numeric operations: When this button is off (default), then numeric operations such as + simply return the type num. If the button is on, then the numeric operations are typed more accurately, as described in subsection D.4.1.

• Polymorphism: This radio box controls how polymorphic expressions are analyzed.

– No polymorphism: polymorphic annotation is ignored;

– Simplify constraints: The constraint system for the polymorphic expression is simplified (see below); and

– Reanalyze: The polymorphic expression is re-analyzed for each polymorphic reference.

• Polymorphism simplification algorithms: This radio box controls which constraint simplification algorithm is used to simplify the constraint system of polymorphic expression, provided the Polymorphism control is set to Simplify constraints. These constraint simplification algorithms are described in section 6.4.

• Save .za files in: MrSpidey generates and saves constraint (.za) files during the analysis of multi-file programs. This radio box controls where these constraint files are stored, either in the same directory as the corresponding source file (default), or in a temporary directory.

D.2.2 MrSpidey Type Display Preferences Window

The MrSpidey Type Display preference window controls how MrSpidey computes and displays type information. An example of this window is shown in figure D.7, and the controls are described below.

• Show types as: Types can be displayed either as basic types (default), which just show the range of functions, or as type schemas, which show how the domain and range of a function are related (e.g. (X1 − > X1)). Basic types contain less information, but are more compact, which is an important benefit when working with large programs. With basic types, users can also choose whether or not to show instance variables and structure fields. For large programs, it is often best not to show these components, in order to produce reasonably compact types.

• Constraint simplification algorithms: This radio box controls which constraint simplification algorithm is used to simplify the constraint system of an expression, before converting that constraint system to a type. These constraint simplification algorithms are described in section 6.4.

Figure D.7 MrSpidey Type Display preferences window

• Type naming: This parameter controls what types are named in a rec type

expression, and can be: – Recursive: Names just enough types to express recursive types.

– Multiple: (default) Names every type that is referred to more than once – Non-Trivial: Names every type except trivial types such as num, sym, etc.

– All: Names all types.

• Primitive types: This parameter can be:

– (prim ...): Displays primitive types as (prim car) etc.

– Given types: Displays the given types of primitives, e.g., ((cons a b) -> a).

– Inferred types: (default) Displays the inferred domain and range of primitive

         functions, e.g.: ((cons num 4) -> num).

• Use equivalences to simplify types: If this control is on (default), then a number of rewriting rules are used to simplify types before they are displayed.

• Use equivalences that make types tidy: If this control is on (default), then some of the type rewriting rules will merge types into disjoint unions, thus losing a certain amount of type information in order to produce a more compact type.

D.3 Analysis of Large Programs

Large programs in DrScheme are typically split into multiple source files, where each source file contains a unit (or unit/sig) expression. The main file for the program then refers to each source file via the reference-unit (or reference-unit/sig) form, and links these multiple units together into a single compound-unit that is then invoked.

To provide a quick turn-around time when statically debugging such programs, MrSpidey uses a componential analysis to avoid re-analyzing source files where possible. When each referenced unit file is first analyzed, MrSpidey:

1. derives a constraint system that describes the data-flow behavior of the unit;

2. simplifies the constraint system while preserving the externally-visible information about the unit’s data-flow behavior; and

3. saves the simplified constraint system in a constraint file named file.za (where file.ss is the name of the source file).

Although the use of constraint files does not reduce the time required for the first analysis, on subsequent analyses MrSpidey can use the saved constraint files to avoid the re-analysis of referenced unit files that have not been modified. This approach substantially reduces re-analysis times.

Once the analysis is completed, MrSpidey displays the program’s main file with the usual static debugging mark-ups. To view other source files, select the File|Open ... option from the MrSpidey window. This option displays a dialog box containing all the program’s source files, and allows the programmer to select the file of interest. A typical dialog box is contained in figure D.8. Alternatively:

• The File|Open All option opens a MrSpidey windows for each source file; and

• The File|Load All option loads all source files into memory but does not immediately display them.

The File|Close All option closes all the MrSpidey windows.

Figure D.8 The File|Open ... dialog box

D.3.1 Inter-File Arrows

In multi-file programs, the source (or destination) of an arrow may sometimes refer to a program point in a separate file. In this case MrSpidey draws an arrow originating (or terminating) in the left margin of the program: see figure D.9. If a margin arrow is painted red, then it refers to an expression in a file that has not yet been loaded, and clicking on the arrow provides the option to load the file. A blue margin arrow refers to an expression in a file that has been loaded. Clicking on a blue arrow provides the option to zoom to and highlight the term at the other end of the arrow, as shown in figure D.10. These facilities are useful for following the flow of values through multi-file programs.

Figure D.9 Source in another loaded file

Figure D.10 The highlighted source in the other file

D.4 The Type Language

The language of basic types in MrSpidey is defined as follows:

type is one of:

set-variable

empty

zeroary-constructor (constructor type ⋯ type) (union type ⋯ type) (rec ([set-variable type] ⋯) type) (class [ivar type] ⋯) (object [ivar type] ⋯) function-type type-abbreviation

set-variable is:

identifier

zeroary-constructor is one of:

nil num sym str char void true false bool eof

constructor is one of:

zeroary-constructor

vec box promise mvalues iport oport         Unary constructors
cons                                        Binary constructors

define-structure-constructor user-defined-constructor

define-structure-constructor is: identifier

user-defined-constructor is: identifier function-type is one of:

(type ⋯ type -> type)

(type · · · type *-> type)                 Rest argument
(type · · · type ->* type)                 Return value list
(type · · · type *->* type)                Rest argument and
                                        return value list
(lambda type type)                      same as (type *->* type)

type-abbreviation is one of:

                        Abbreviates

(MU set-variable type) (rec ([set-variable type]) set-variable)

noarg                   nil

(arg type type) (cons type type)

(list type · · · type)      (cons type (cons · · ·(cons type nil)))
(listof type)            (MU l (union (cons type l) nil))
null                    nil
bool                    (union true false)
atom                    (union nil num sym str char bool)
sexp                    (MU x (union atom (cons x x) (vec x)))

The behavior of primitive operations is defined using multiple-arity schemas. For each reference to a primitive operation, MrSpidey retrieves the corresponding multiple-arity schema and selects the schema appropriate for the number of arguments given to the primitive (or the last schema if the primitive is used in a higher-order manner). It then instantiates the schema by replacing the quantified set variables by set variables, and converts the resulting basic type into a constraint system. Multiplearity schemas are defined as follows:

multiple-arity-schema is one of: schema (case-> schema ⋯)

schema is one of:

type

(forall (set-variable ⋯) type)

D.4.1 Accurate Numeric Operations

When the Accurate numeric operations control in the MrSpidey Analysis preferences window is turned on, MrSpidey performs a more accurate analysis of numeric operations, as follows.

The type language is extended with the unary constructors apply+, apply-, apply* and apply/. The return type of the numeric operations +, -, *, and / record information about the numeric operation and its argument value sets. For example, the type returned by the operation + is (apply+ arglist), where arglist is the argument list to +. The resulting types are simplified before being presented to the programmer. For example, type (apply+ (list x1 ... xn)) is transformed into

(+ x1 ... xn), etc.

In addition, the binary constructors =, not=, <, <=, > and >= are added to the type language. The meaning of the type (< X Y) is the set of numbers x in X such that there exists some y in Y with x < y. MrSpidey generates these types for if-expressions where the predicate is one of zero?, =, <, <=, > or >=.

D.5 Extensions to DrScheme

D.5.1 Type Assertions

The form (: exp type) is an assertion that the values produced by exp must be contained in type. If MrSpidey is unable to prove that the type assertion is satisfied, then a warning is reported in the summary window. These : forms evaluate to void.

D.5.2 Polymorphic Annotations

The form (polymorphic exp) causes the expression exp to be analyzed in a polymorphic manner. That is, if the result of (polymorphic exp) is immediately bound to an identifier (e.g. by let or define), then all references to that identifier that occur below that binding will be polymorphic. The annotation has no runtime effect.

D.5.3 Declaring New Primitives

The form (type: multiple-arity-schema) declares new primitive of type multiple-arity-schema. Some example definitions are:

(define my-car (type: (forall (a) ((cons a ) -> a))))

(define my-map (type: (forall (a r) ((a -> r) (listof a) -> (listof r)))))

The expression (type: …) evaluates to void.

D.5.4 Declaring Constructors

The form (define-constructor name modes …) adds a new type constructor to the type language. The arguments mode ... are all booleans, each specifying whether the corresponding field in the constructor is mutable.

D.5.5 Declaring New Types

The form (define-type name type) adds a new type name that can later be used in type expressions.

D.6 Restrictions on Source Programs

The following DrScheme facilities are not handled.

• Primitives for dynamic loading and evaluation: load, load/cd, load-relative,

     load/use-compiled, current-load, require-library-use-compiled,
     compile, eval, current-eval, expand-defmacro and expand-defmacro-once.

• Primitives that dynamically manipulate the top-level environment: undefine,

     global-defined-value, invoke-open-unit and invoke-open-unit/sig.

• MzScheme’s interfaces, exception system and exception hierarchy.

• Primitives that access structures without the appropriate selectors: struct-ref

     and struct->vector.

• MrSpidey doesn’t know about DrScheme language levels.

• Primitive names should not be assigned or defined.

Certain potential errors are not detected:

• Returning an inappropriate number of multiple values to a single value context.

• Index out of bounds on vector, string and list operations.

• compound-unit errors. Since unit’s are normally used in a first-order manner, these errors are typically easy to detect using the evaluator.

• The arguments to primitive-name and primitive-result-arity are only

checked to be procedures, not primitive procedures.

• Errors in read due to ill-formed s-expression on the input port. The analysis of certain kinds of code is not completely sound:

• Values passed to exception handlers.

• Tracking values through parameters.

• Tracking values through will executors.

• MrSpidey doesn’t translate unit/sig into unit, as MzScheme does.

Appendix E

Implementation Details

E.1 Zodiac

A useful interface for MrSpidey must present the results of the program analysis in terms of the original source program. Hence, the environment requires a front-end for processing source text that can correlate the internal representation of programs with their source location. For Scheme, this correlation task is complicated by the powerful macro systems of typical implementations because macros permit arbitrary rearrangements of syntax.

MrSpidey exploits Zodiac [32] for its front-end. Zodiac is a tool-kit for generating language front-ends that are suitable for interactive environments. It includes a hygienic high-level macro system that relates each expression in the macro-expanded code to its source location. MrSpidey exploits this information to associate value set invariants with expressions in the source program and to present portions of the value flow-graph as arrows relating terms in the program text.

E.2 MrEd

MrSpidey’s graphical component is implemented using MrEd [18], a Scheme-based engine for constructing graphical user interfaces. The core of the engine is a C++- like object system and a portable graphics library. This library defines high-level GUI elements, such as windows, buttons, and menus, which are embedded within Scheme as special primitive classes.

MrEd’s graphical class library includes a powerful, extensible text editor class. This editor class is used in MrSpidey to display analyzed programs, including the boxes containing type invariants and the arrows describing the value flow graph. Type invariant boxes are easily embedded in the program text because an editor buffer can contain other buffers as part of its text. The arrows used to present flow information are not part of the editor’s built-in functionality, but it was straightforward to extend the editor class with arrow drawing capabilities using other components of the graphical library.

MrEd’s object system provides a robust integration between the Scheme implementation and the underlying graphical class library. The integration of the library through the object system is easily understood by GUI programmers. The object system also provides an important tool for designing and managing the components of a graphical interface. Because the implementation of MrSpidey exploits this object system, it can absorb future enhancements to the editor and it is easily integrated into the DrScheme environment.

Applications developed with MrEd—including MrSpidey and DrScheme—are fully portable across the major windowing systems (X–Windows, Microsoft Windows, and MacOS). MrEd’s portability, its object system, and its rich class library enabled us to focus on the interesting and novel parts of MrSpidey’s implementation.

E.3 Multiple-Arity Functions

In contrast to the idealized languages of chapters 2 and 3, realistic languages such as Scheme [5] provide more flexible parameter passing mechanisms. In particular, Scheme allows multiple arguments to be passed to a function. It also allows a list of arguments to be passed, via the apply primitive, and it allows for the incoming list of arguments to be bound to a formal parameter, via the syntax

(lambda x …)

To cope with these multiple argument passing and binding possibilities, MrSpidey models each function as taking a single argument, which is a list of the function’s actual arguments. Thus the function (lambda (x y) …) takes an argument list l, extracts the car of l into x, and the cadr of l into y. Conversely, at an application site, the arguments to the callee are wrapped up in a list, which is then passed as the single argument to the callee. Thus the application (f x y) actually applies f to (list x y). The various other parameter passing and binding modes of Scheme, including the apply primitive, can also be modeled within this framework.

E.4 Multiple Values

Scheme [5] allows expressions to return a collection of multiple values, which can be converted into an argument list via the call-with-values primitive.

To cope with multiple values, MrSpidey models each expression as returning a list of return values, in a manner analogous to the way functions take a list of argument values. Thus, the expression:

(values 1 2)

is modeled in MrSpidey as returning the value:

(list 1 2)

Similarly, the expressions (values 1) and 1 (which are equivalent) both return (list 1).

Thus each expression must return a list of multiple values, and each context needs to expect such a list. This convention substantially simplifies the analysis, but it does cause problems in explaining of the program’s value flow. If we consider the binding expression:

(let ([x M ]) …)

then we would expect that there should be a value flow arrow from the expression M to the variable x. In the absence of multiple values, this arrow corresponds to a subset constraint [α_{M} ≤ α_{x}] in the solved constraint system, where α_{M} and α_{x} are the set variables for M and x, respectively.

Once we introduce multiple values, this direct correspondence between the intuitive value flow arrows and subset constraints no longer exists. That is, in the presence of multiple values, the constraint corresponding to the above let expression is:

car(α_{M}) ≤ α_{x}

since α_{M} actually denotes a list of multiple values, which in this case should contain a single element, and that element should be extracted and bound to the variable x.

In order to produce intuitive value flow arrows that do not correspond to subset constraints, MrSpidey needs to preserve additional information for certain binding constructs such as the above let expression.

E.5 Checking Scheme Primitives

Section 4.3 describes how to identify unsafe operations in the idealized language Λ^{p}. However, realistic languages such as MzScheme [17] contains a large number of primitive procedures in addition to those in Λ^{p}. The set of valid argument values for each of these primitives is often more complicated than for the simple primitives car and cdr. For example, the primitive procedure member requires two arguments, the second of which must be a list, and each element of the list must be a pair. MrSpidey uses type schemas to describe both the behavior of each primitive procedure and the appropriate argument set for that primitive.

E.5.1 Type Schemas

Type schemas are used to describe the behavior and domain of primitive procedures, and have the form:

μ ∈ Schema = ∀\overline{α}.ω

For example, the operation car has the associated type schema:

μ_{car} = ∀β, γ.((cons β γ) →^{{car}} β)

where car is the function tag associated with the primitive car.

We define the semantics of type schemas via the function M_{·}[·] : SetEnv × Schema ⟶ P(D):

M_{ρ}[∀α_{1}, …, α_{n}.ω] = {M_{ρ′}[ω] | ρ′ = ρ[α_{i} ↦ X_{i}], X_{i} ∈ D}

Thus the meaning of a type schema ∀α_{1}, …, α_{n}.ω is the set of meanings for ω as the universally quantified variables α_{1}, …, α_{n} range over elements of D. For a closed type schema μ, we define:

M[μ] = M_{ρ}[μ]

where ρ can be chosen arbitrarily, and does not affect the definition.

E.5.2 New Constraint Classes

For each reference to a primitive operation, MrSpidey needs to translate the corresponding type schema into a constraint system. To assist in this process, we introduce two new classes of constraints: checking constraints and constructor constraints.

Checking Constraints: A checking constraint is of the form:

α ≤ C

for some C ⊆ Const, and the semantics of checking constraints is defined by:

ρ ⊧ α ≤ C ⟺ const(ρ(α)) ⊆ C

Checking constraints are used to describe restrictions on the set of appropriate arguments to a primitive operation. For example, suppose the program refers to the primitive procedure car, and that α is the set variable corresponding to that reference. Then the data-flow behavior of car can be extracted from the corresponding type schema μ_{car} as the simple constraint system:

{car ≤ α, dom(α) ≤ α_{d}, car(α_{d}) ≤ β, cdr(α_{d}) ≤ γ, β ≤ rng(α)}

and the restriction on appropriate arguments to car can also be extracted from μ_{car} as the checking constraint:

α_{d} ≤ {pair} .

Constructor Constraints: A constructor constraint is of the form:

ω ≤ α | α ≤ ω

and the semantics of constructor constraints is defined by:

\begin{aligned}ρ & ⊧ & ω ≤ α & ⟺ & M_{ρ}[ω] & ⊑ & ρ(α) \\ ρ & ⊧ & α ≤ ω & ⟺ & ρ(α) & ⊑ & M_{ρ}[ω] \end{aligned}

A constructor constraint can be converted into an equivalent collection of simple and checking constraints via the function CS described in figure E.1. That is:

• ρ ⊧ CS[ω ≤ α] if and only if ρ ⊧ ω ≤ α, and

• ρ ⊧ CS[α ≤ ω] if and only if ρ ⊧ α ≤ ω.

The cases for constructor constraints of the form ω ≤ α are straightforward. The cases for constructor constraints of the form α ≤ ω are more complicated. The function CS first extracts all the top-level constants in ω via the function call TLC [ω], and creates a checking constraint that ensures that α only contains constants in TLC [ω]. It then calls the function CS′[α ≤ ω] to handle containment within subcomponents of ω.

CS[c ≤ α] = {c ≤ α}
CS[β ≤ α] = {β ≤ α}
CS[⊥_{s} ≤ α] = ∅
CS[(ω_{d} →^{T} ω_{r}) ≤ α] = {T ≤ α, dom(α) ≤ α_{d}, α_{r} ≤ rng(α)}

∪CS[ω_{r} ≤ α_{r}] ∪ CS[α_{d} ≤ ω_{d}] where α_{d}, α_{r} are fresh

CS[(cons ω_{a} ω_{d}) ≤ α] = {α_{a} ≤ car(α), α_{r} ≤ rng(α)}

∪CS[ω_{a} ≤ α_{a}] ∪ CS[ω_{d} ≤ α_{d}] where α_{a}, α_{d} are fresh

CS[ω_{1} ∪ ω_{2} ≤ α] = CS[ω_{1} ≤ α] ∪ CS[ω_{2} ≤ α]
CS[(rec ([α_{1} ω_{1}] … [α_{n} ω_{n}]) ω) ≤ α] = CS[α_{i} ≤ ω_{i}] ∪ CS[ω_{i} ≤ α_{i}] ∪ CS[ω ≤ α]
CS[α ≤ ω] = {α ≤ TLC [ω]} ∪ CS′[α ≤ ω]

CS′[α ≤ C] = ∅
CS′[α ≤ ⊥_{s}] = ∅
CS′[α ≤ β] = {α ≤ β}
CS′[α ≤ (ω →^{T} ω)] = { α_{d} ≤ dom(α), rng(α) ≤ α_{r}}

∪CS[ω ≤ α_{d}] ∪ CS[α_{r} ≤ ω]

CS′[α ≤ (cons ω_{a} ω_{d})] = {car(α) ≤ α_{a}, cdr(α) ≤ α_{d}}

∪CS[α_{a} ≤ ω_{a}] ∪ CS[α_{d} ≤ ω_{d}]

CS′[α ≤ ω_{1} ∪ ω_{2}] = CS′[α ≤ ω_{1}] ∪ CS′[α ≤ ω_{2}]

Figure E.1 Converting constructor constraints to simple and checking constraints

The auxiliary function TLC : Type ⟶ P(Const) extracts the top level constants in a type, and is defined as follows:

TLC [c] = {c}
TLC [α] = ∅
TLC [⊥_{s}] = ∅
TLC [(ω →^{T} ω)] = T
TLC [(cons ω ω)] = {pair}
TLC [ω_{1} ∪ ω_{2}] = TLC [ω_{1}] ∪ TLC [ω_{2}]
TLC [(rec ([α_{1} ω_{1}] … [α_{n} ω_{n}]) ω)] =

TLC [ω]∪⋃_{α_{j}} TLC [(rec ([α_{1} ω_{1}] … [α_{n} ω_{n}]) ω_{j})] where α_{j} is mentioned at top level in ω E.5.3 Converting Type Schemas to Constraints

For each reference to a primitive operation, MrSpidey converts the corresponding type schema into collection of simple and checking constraints. This conversion process involves two steps.

Instantiating the Type Schema: First, the type schema is instantiated. For μ = ∀\overline{α}.ω, this instantiation involves replacing references in ω to the universally quantified variables α_{1}, …, α_{n} by fresh variables, producing an instantiated type ω′.

Converting the Instantiated Type into Constraints: Second, the instantiated type ω′ is converted into a collection of simple and checking constraints via the function CS. That is, if α is the set variable for the primitive procedure reference, then:

S ∪ S = CS[ω′ ≤ α]

where S is a simple constraint system and S is a checking constraint system.

Thus MrSpidey converts each reference to a primitive operation into two constraint systems: a simple constraint system and a checking constraint system. The simple constraint system is passed on to the set-based analysis algorithm and the analysis proceeds as usual. The analysis later terminates, yielding a closed constraint system S for the analyzed program. Since this constraint system is closed under Θ, it is straightforward to check if the least solution of this constraint system satisfies the checking constraints for the primitive operation. Specifically, LeastSoln(S) satisfies the checking constraint α ≤ C if and only if:

{c | [c ≤ α] ∈ S} ⊆ C

If the least solution satisfies the checking constraints for a primitive operation, then that operation is only applied to valid arguments at run-time, and hence that operation is safe. Conversely, if the least solution does not satisfy the checking constraints, then the primitive operation may be applied to erroneous arguments at run-time, and the operation should be marked as unsafe.

Appendix F Notations

Symbol  Meaning  Section  Page
M ∈ Λ  Terms  2.1  11
V ∈ Value  Values  2.1  11
x ∈ Var  Variables  2.1  11
b ∈ BasicConst  Basic constants  2.1  11
t ∈ FnTag  Function tags  2.1  11
l ∈ Label  Labels  2.1  11
β_{v}, βlet , unlabel  Reduction rules  2.1.2  12
⟶  Reduction relation  2.1.2  12
E  Evaluation contexts  2.1.2  12
⟼, ⟼^{∗}  Standard reduction relation  2.1.2  12
eval  Evaluator  2.1.2  12
τ ∈ SetExp  Set expressions  2.2  12
α, β, … ∈ SetVar  Set variables  2.2  12
c ∈ Const  Constants  2.2  12
dom, rng  Type expression constructors  2.2  12
C ∈ Constraint  Constraints  2.2  12
S ∈ ConstraintSystem Constraint systems  2.2  12
S |_{E}  Restriction of a constraint system  2.2  13
P  Power set constructor  2.2  13
D  Domain for constraints  2.3.1  14
const, dom, rng  Extract components of element of D  2.3.1  14
in  Values described by constants  2.3.1  14
⊑, ⊤, ⊥, ⊔, ⊓  Ordering, elements and operations on D 2.3.1  14

ρ ∈ SetEnv  Set environment  2.3.2  15
ρ^{∗}  Extended set environment  2.3.2  15
⊧  Satisfies, or entails  2.3.2  16
Soln(S)  Solution space  2.3.2  16
≅  Observable equivalence  2.3.2  16
⊧_{E}  Restricted entailment  2.3.2  16
Soln(S) |_{E}  Restricted solution space  2.3.2  16
≅_{E}  Restricted observable equivalence  2.3.2  16
⊢  Constraint derivation rules  2.4  17
Γ ∈ DerivCtxt  Set variable context  2.4  16
σ ∈ ConSchema  Constraint schema  2.4  18
F V [range(Γ)]  Free variables in the range of Γ  2.4  19
C ∈ SimpleCon  Simple constraints  2.4  18
S ∈ SimpleConSystem Simple constraint systems  2.4  18
⊑_{s}, ⊤_{s}, ⊥_{s}, ⊔_{s}, ⊓_{s}  Alternative ordering on domain  2.4  18
sba  Analysis function  2.6.3  23
LeastSoln  Least Solution  2.6  22
Θ = {s_{1}, …, s_{n}}  Inference rules  2.6.1  24
⊢_{Θ}  Deduction via Θ  2.6.1  23
Sel^{+}, Sel^{−}  Sets of selectors  3.1  29
sel^{+}, sel^{−}, sel  Selectors  3.1  29
Λ^{p}  Language Λ plus pairs  3.2  31
pair ∈ Const  Tag for pairs  3.2.2  31
car, cdr  Selectors for pairs  3.2.2  31
Λ^{cc}  Language Λ^{p} plus continuations  3.3  33
Λ^{!}  Language Λ^{p} plus assignments  3.4  37
D ∈ Defines  Definitions  3.4  37
z, w ∈ AssignVar  Assignable variables  3.4  37
H ∈ Heap  Heap of definitions  3.4.1  37
Λ^{b}  Language Λ^{!} plus boxes  3.5  38
box^{+}, box^{−}  Selectors for boxes  3.5.2  41

Λ^{u}  Language Λ^{!} plus units  3.6  42
ui, ue  Selectors for units  3.6.2  44
Λ^{c}  Language Λ^{!} plus objects  3.7  45
cl-obj, ivar_{z}^{+}, ivar_{z}^{−} Selectors for classes  3.7.2  46

E  External variables  6.1  63
Δ  Inference rules on constraint systems  6.2  64
κ  Non-constant set expression  6.2  64
C ∈ CmpdConstraint Compound constraints  6.2  65
S ∈ CmpdConSystem Compound constraint systems  6.2  65
Ψ  Inference rules on constraint systems  6.2  66
Π  Inference rules on constraint systems  6.2  67
⊢_{ΨΘ}^{E}, =_{ΨΘ}^{E}  Relations on constraint systems  6.2  67
G  Grammar  6.3.1  70
G_{r}  Function producing regular grammar  6.3.1  70
α_{L}, α_{U}  Grammar non-terminals  6.3.1  70
L_{G}(X)  Language for X in G  6.3.1  70
G_{t}  Function producing RTG  6.3.3  71
R  Root non-terminal  6.3.3  71
R  Relation for computing entailment  6.3.4  72
p, q ∈ Path  Paths  C.2  114
arity, π  Arity function  C.2  114
≤_{i}  Either ≤ or ≥  C.2  114
⊑_{i}, ⊒_{i}  Either ⊑ or ⊒  C.2  114
⊆_{i}  Either ⊆ or ⊇  C.2  114
⨆i  Either ⨆ or ⊓  C.2  114
X@p  Injection function  C.2  114

Bibliography

[1] Aho, A., J. Hopcroft and J. Ullman. The Design and Analysis of Computer Algorithms. Addison-Wesley, Reading, Mass., 1974.

[2] Aiken, A., Wimmers, E. L., and Lakshman, T. K. Soft typing with conditional types. In Proceedings of the ACM Sigplan Conference on Principles of Programming Languages (1994), pp. 163–173.

[3] Bourdoncle, F. Abstract debugging of higher-order imperative languages. In Proceedings of the ACM SIGPLAN ’93 Conference on Programming Language Design and Implementation (June 1993), pp. 46–55.

[4] Cartwright, R., and Felleisen, M. Extensible denotational language specifications. In Theoretical Aspects of Computer Software.

[5] Clinger, W., and Rees, J. (Eds.). The revised^{4} report on the algorithmic language scheme. ACM Lisp Pointers 4, 3 (July 1991).

[6] Cooper, K. D., Hall, M. W., Hood, R., Kennedy, K., McKinley, K., Mellor-Crummey, J., Torczon, L., and Warren, S. The Parascope parallel programming environment. Proceedings of the IEEE (February 1993), 244–263.

[7] Cousot, P., and Cousot, R. Formal language, grammar, and set-constraint-based program analysis by abstract interpretation. In Proceedings of the 1995 Conference on Functional Programming and Computer Architecture (1995), pp. 170–181.

[8] Detlefs, D. An overview of the extended static checking system. In Proceedings of The First Workshop on Formal Methods in Software Practice (January 1996), ACM (SIGSOFT), pp. 1–9.

[9] Deutsch, A., and Heintze, N. Partial solving of set constraints. Unpublished manuscript.

[10] Duesterwald, E., Gupta, R., and Soffa, M. L. Reducing the cost of data flow analysis by congruence partitioning. In International Conference on Compiler Construction (April 1994).

[11] Eifrig, J., Smith, S., and Trifonov, V. Sound polymorphic type inference for objects. In Conference on Object-Oriented Programming Systems, Languages, and Applications (1995).

[12] Fähndrich, M., and Aiken, A. Making set-constraint based program analyses scale. Technical Report UCB/CSD-96-917, University of California at Berkeley, 1996.

[13] Flanagan, C., and Felleisen, M. Set-based analysis for full Scheme and its use in soft-typing. Technical Report TR95-254, Rice University, 1995.

[14] Flanagan, C., and Felleisen, M. Modular and polymorphic set-based analysis: Theory and practice. Technical Report TR-96-266, Rice University, 1996.

[15] Flanagan, C., and Felleisen, M. Componential set-based analysis. In Proceedings of the ACM SIGPLAN ’97 Conference on Programming Language Design and Implementation (June 1997), pp. 235–248.

[16] Flanagan, C., Flatt, M., Krishnamurthi, S., Weirich, S., and Felleisen, M. Finding bugs in the web of program invariants. In Proceedings of the ACM Conference on Programming Language Design and Implementation (1996), pp. 23–32.

[17] Flatt, M. MzScheme Reference Manual. Rice University.

[18] Flatt, M. MrEd: An engine for portable graphical user interfaces. Technical Report TR-96-258, Rice University, 1996.

[19] Flatt, M., and Felleisen, M. First-class compilation units. Unpublished manuscript.

[20] Flatt, M., Krishnamurthi, S., and Felleisen, M. Mixins for java. POPL’97 submission.

[21] Gécseg, F., and Steinby, M. Tree Automata. Akadémiai Kiadó, Budapest, 1984.

[22] Gosling, J., Joy, B., and Steele, G. The Java Language Specification. Addison-Wesley, 1996.

[23] Heintze, N. Set Based Program Analysis. PhD thesis, Carnegie Mellon University, 1992.

[24] Heintze, N. Set-based analysis of ML programs. In Proceedings of the ACM Conference on Lisp and Functional Programming (1994), pp. 306–317.

[25] Hindley, R. J., and Seldin, J. P. Introduction to Combinators and λ-Calculus. Cambridge University Press, 1986.

[26] Hiranandani, S., Kennedy, K., Tseng, C.-W., and Warren, S. The D editor: A new interactive parallel programming tool. In Proceedings of Supercomputing (1994).

[27] Hopcroft, J. E. An n log n algorithm for minimizing the states of a finite automaton. The Theory of Machines and Computations (1971), 189–196.

[28] Jagannathan, S., and Wright, A. K. Effective flow analysis for avoiding run-time checks. In Proc. 2nd International Static Analysis Symposium, LNCS 983 (September 1995), Springer-Verlag, pp. 207–224.

[29] Jones, N., and Muchnick, S. A flexible approach to interprocedural data flow analysis and programs with recursive data structures. In Conference Record of the Ninth Annual ACM Symposium on Principles of Programming Languages (January 1982), pp. 66–74.

[30] Kennedy, K., McKinley, K., and Tseng, C.-W. Interactive parallel programming using the ParaScope Editor. IEEE Transactions on Parallel and Distributed Systems 2, 3 (July 1991).

[31] Kernighan, B. W., and Ritchie, D. M. The C Programming Language. Prentice-Hall, 1988.

[32] Krishnamurthi, S. Zodiac: A programming environment builder. Technical Report TR-96-259, Rice University, 1996.

[33] Miller, B., Koski, D., Lee, C. P., Maganty, V., Murthy, P., Natarajan, A., and Steidl, J. Fuzz revisited: A re-examination of the reliability of unix utilities and services. Computer Science Department, University of Wisconsin, 1995.

[34] Milner, R., Tofte, M., and Harper, R. The Definition of Standard ML. The MIT Press, Cambridge, Massachusetts and London, England, 1990.

[35] Palsberg, J. Closure analysis in constraint form. Transactions on Programming Languages and Systems 17, 1 (1995), 47–62.

[36] Palsberg, J., and O’Keefe, P. A type system equivalent to flow analysis. In Proceedings of the ACM SIGPLAN ’95 Conference on Principles of Programming Languages (1995), pp. 367–378.

[37] Pottier, F. Simplifying subtyping constraints. In Proceedings of the 1996 ACM SIGPLAN International Conference on Functional Programming (1996), pp. 122–133.

[38] Pugh, W. The omega test: a fast and practical integer programming algorithm for dependence analysis. In Supercomputing (1991).

[39] Reynolds, J. Automatic computation of data set defintions. Information Processing’68 (1969), 456–461.

[40] Reynolds, J. C. The essence of ALGOL. Algorithmic Languages (1981), 345–372.

[41] Shei, B., and Gannon, D. Sigmacs: A programmable programming environment. In Advances in Languages and Compilers for Parallel Computing. The MIT Press, August 1990.

[42] Tofte, M. Type inference for polymorphic references. Information and Computation 89, 1 (November 1990), 1–34.

[43] Trifonov, V., and Smith, S. Subtyping constrained types. In Third International Static Analysis Symposium (LNCS 1145) (1996), pp. 349–365.

[44] Wolfe, M. J. The Tiny loop restructuring research tool. In Proceedins of the 1991 International Conference on Parallel Processing (August 1991).

[45] Wright, A. Practical Soft Typing for Scheme. PhD thesis, Rice University, 1994.

[46] Wright, A., and Cartwright, R. A practical soft type system for scheme. In Proceedings of the ACM Conference on Lisp and Functional Programming (1994), pp. 250–262.

[47] Wright, A., and Felleisen, M. A syntactic approach to type soundness. Information and Computation 115, 1 (1994), 38–94.

[48] Wright, A. K. Simple imperative polymorphism. Lisp and Symbolic Computation 8, 4 (Dec. 1995), 343–356.