Typestate analysis

Nonlinear typestate lattice arising from initialization of a variable of type struct{int x;int y;int z;}.
The least element ⊥ coincides with the state ∅ of no struct components initialized.

Strom and Yemini (1986) required the set of typestates for a given type to be partially ordered such that a lower typestate can be obtained from a higher one by discarding some information. For example, an int variable in C typically has the typestates "uninitialized" < "initialized", and a FILE* pointer may have the typestates "unallocated" < "allocated, but uninitialized" < "initialized, but file not opened" < "file opened". Moreover, Strom and Yemini require that each two typestates have a greatest lower bound, i.e. that the partial order is even a meet-semilattice; and that each order has a least element, always called "⊥".

Their analysis is based on the simplification that each variable v is assigned only one typestate for each point in the program text; if a point p is reached by two different execution paths and v inherits different typestates via each path, then the typestate of v at p is taken to be the greatest lower bound of the inherited typestates. For example, in the following C snippet, the variable n inherits the typestate "initialized" and "uninitialized" from the then and the (empty) else part, respectively, hence it has typestate "uninitialized" after the whole conditional statement.

int n;                // here, n has typestate "uninitialized"
if (...) {
    n = 5;            // here, n has typestate   "initialized"
} else {
    /*do nothing*/    // here, n has typestate "uninitialized"
}                     // here, n has typestate "uninitialized" = greatest_lower_bound("initialized","uninitialized")

Every basic operation[note 1] has to be equipped with a typestate transition, i.e. for each parameter the required and ensured typestate before and after the operation, respectively. For example, an operation fwrite(...,fd) requires fd to have typestate "file opened". More precisely, an operation may have several outcomes, each of which needs its own typestate transition. For example, the C code FILE *fd=fopen("foo","r") sets fd's typestate to "file opened" and "unallocated" if opening succeeds and fails, respectively.

For each two typestates t₁ <· t₂, a unique typestate coercion operation needs to be provided which, when applied to an object of typestate t₂, reduces its typestate to t₁, possibly by releasing some resources. For example, fclose(fd) coerces fd's typestate from "file opened" to "initialized, but file not opened".

A program execution is called typestate-correct if

• before each basic operation, all parameters have exactly the typestate required by the operation's typestate transition, and
• on program termination, all variables are in typestate ⊥.[note 2]

A program text is called typestate-consistent if it can be transformed, by adding appropriate typestate coercions, to a program whose points can be statically labelled with typestates such that any path allowed by the control flow is typestate-correct. Strom and Yemini give a linear-time algorithm that checks a given program text for typestate-consistency, and computes where to insert which coercion operation, if any.

In order to achieve a precise and effective typestate analysis, it is necessary to address the problem of aliasing. Aliasing occurs when an object has more than one reference or pointer that points to it. For the analysis to be correct, state changes to a given object must be reflected in all references that point to that object, but in general it is a difficult problem to track all such references. This becomes especially hard if the analysis needs to be modular, that is, applicable to each part of a large program separately without taking the rest of the program into account.

As another issue, for some programs, the method of taking the greatest lower bound at converging execution paths and adding corresponding down-coercion operations appears to be inadequate. For example, before the return 1 in the following program,[note 3] all components x, y, and z of coord are initialized, but Strom's and Yemini's approach fails to recognize this, since each initialization of a struct component in the loop body has to be down-coerced at loop re-entry to meet the typestate of the very first loop entry, viz. ⊥. A related problem is that this example would require overloading of typestate transitions; for example, parse_int_attr("x",&coord->x) changes a typestate "no component initialized" to "x component initialized", but also "y component initialized" to "x and y component initialized".

int parse_coord(struct{int x;int y;int z;} *coord) {
    int seen = 0;     /* remember which attributes have been parsed */
    while (1)
        if      (parse_int_attr("x",&coord->x)) seen |= 1;
        else if (parse_int_attr("y",&coord->y)) seen |= 2;
        else if (parse_int_attr("z",&coord->z)) seen |= 4;
        else break;
    if (seen != 7)    /* some attribute missing, fail */
        return 0;
    ...               /* all attributes present, do some computations and succeed */
    return 1;
}

There are several approaches seeking to infer typestates out of programs (or even other artifacts such as contracts). Many of them can infer typestates at compile time [6][7][8][9] and others mine the models dynamically.[10][11][12][13][14][15]

Typestate is an experimental concept that has not yet crossed over into mainstream programming languages. However, many academic projects actively investigate how to make it more useful as an everyday programming technique. Two examples are the Plaid and Obsidian languages, which are being developed by Jonathan Aldrich's group at Carnegie Mellon University.[16] [17] Other examples include the Clara[18] language research framework, earlier versions of the Rust language, and the >> keyword in ATS.[19]

• Design by contract
• Linear type system
• Effect system
• Runtime verification