Skip to content

Documentation

Jump to bottom
João Mota edited this page Jun 21, 2023 · 23 revisions

Documentation

Table of contents

Introduction

The Java Typestate Checker (JaTyC) is a tool that verifies Java source code with respect to typestates. A typestate is associated with a Java class with the @Typestate annotation and defines: the object's states, the methods that can be safely called in each state, and the states resulting from the calls. The tool statically verifies that when a Java program runs: sequences of method calls obey to object's protocols; objects' protocols are completed; null-pointer exceptions are not raised; subclasses' instances respect the protocol of their superclasses.

JaTyC is implemented as a plugin for the Checker Framework. It is a purely transparent checker meaning that it does not modify the baseline Java compilation. As far as we tested, JaTyC verifies Java source code compatible with version 8 and 11.

JaTyC provides the following static guarantees:

  • Protocol compliance: objects are used according to their protocols (typestates);
  • Protocol completion: protocols reach the end state (assuming the program terminates without exceptions);
  • Null-pointer exceptions are not raised (in the code we can inspect);
  • The protocols of subclasses allow all the behavior provided by the protocol of the superclass.

To ensure these properties, typestated-objects must be used in a linear way (i.e. state changes can only be performed via a single object reference).

Currently, JaTyC has some limitations that we are working on:

  • Elements of arrays are always nullable;
  • No overall support for generics (parametric types are non-linear and nullable by default);
  • No overall support for dealing with state changes in the presence of exceptions (if an exception occurs, an object may be left in an inconsistent state which the static analysis will not detect);
  • No support for interface multiple inheritance (using it is undefined behavior);
  • Anytime methods cannot write to fields.

Installation

Check out the README file for the appropriate installation instructions for the current version of JaTyC.

Protocols

This tool requires that protocol specifications be associated with each Java class if one desires to check the behavior of instances of those classes. Protocol specifications are written in text files usually with the ".protocol" extension. Since these protocols resemble finite-state machines, they declare the states and the available transitions between those. Each specification must follow the following grammar. Note that id is a meta-variable ranging over values of the set of all the valid Java identifiers.

Select := id | id "." Select
Package := "package" Select ";"
Import := "import" "static"? Select ("." "*")? ";"
Destination := Select | State | DecisionState
Decision := id ":" ( id | State )
DecisionState := "<" Decision ( "," Decision )* ">"
Arguments := "(" Select ( "," Select )* ")"
Method := Select id Arguments ":" Destination
Methods := Method ( "," Method )*
State := "{" Methods ( "," "drop" ":" "end" )? "}"
NamedState := id "=" State
Protocol := "typestate" id "{" NamedState* "}"
Start := Package? Import* Protocol

Protocols may start with a package statement and zero or more import statements. Just like in Java classes, these statements indicate to which package the protocol belongs and which classes it wants to import. This is important for the resolution of Java types used in the protocol.

Following that, the keyword typestate must be used, followed by the name of the protocol. The name is used only for presentation purposes when reporting errors and does not need to match the file name. After the name, between curly brackets, zero or more named states may be declared. No state may be called end. The end state is the final state which is always implicit in the protocols and allows for no method calls. The initial state in the protocol is the first declared. If no state is declared, end is simultaneously the first and final state.

For each state, a set of methods which are allowed in that state may be declared. Each method in the protocol is composed by a return type, a list between parentheses of the types of the parameters separated by commas, and the state to which the method transits to in that given state. The destination state may be a name of another declared state, an anonymous state (i.e. a state declaration starting and ending with curly brackets), or a decision state. Each decision state is composed of pairs. For each pair, the first component is the name of a value from an enumeration or a boolean literal, depending on if the method returns an enumeration or a boolean value. The second component indicates to which state the method transits to depending on the return value of the method call, which may be the name of a state or an anonymous state.

Additionally, each state may optionally include a droppable transition. This is a special transition that happens implicitly when an object is no longer used, which moves the object’s state to the final state. This feature will be further explained later.

typestate Iterator {
  HasNext = {
    boolean hasNext(): <true: Next, false: end>
  }
  Next = {
    boolean hasNext(): <true: Next, false: end>,
    Object next(): HasNext
  }
}

In this example is presented a protocol for a Java iterator. This protocol has two declared states, HasNext and Next and the implicit end state. In the HasNext state, only the hasNext method is available to be called (line 3). In the Next state, both hasNext and next methods are available (lines 6 and 7). When the hasNext method is called, and if it returns true, the iterator transits to the Next state. If the method returns false, the iterator transits to the end state. When the next is called, the iterator transits to the HasNext state.

Please note that protocol files should include a "package" statement at the top just like Java classes (if they do not belong to the default package), so that the resolution of types works. An example may be found here.

@Typestate annotation

To associate a protocol with a Java class, the @Typestate annotation should be placed on top of the class declaration. The annotation accepts one string argument: the relative path from the class file to the protocol file. The .protocol extension may be omitted.

@Typestate("./protocols/Iterator.protocol")
public class Iterator { ... } 
@Typestate("./protocols/Iterator")
public class Iterator { ... }

With the protocol associated with the class, the type-checker will ensure that instances of that class follow the respective protocol.

Iterator it = new Iterator();
while (it.hasNext()) {
    it.next();
}

An example may also be found here.

Nullness checking

Null pointer errors are very common in Java. Because of this, it is crucial for the typechecker to be able to detect these errors before runtime. For every object type used in a program, the type-checker assumes the type is not nullable (contrary to the default type system of Java). If one desires that a type be nullable, one can use the @Nullable annotation. This design choice follows what other tools do (like the Nullness Checker) and we believe it reduces the amount of errors and annotations that would need to be added for current code to be accepted.

The annotation may be used before any type, in variable declarations, in field declarations, in parameter declarations and in return types of methods. Nevertheless, the @Nullable annotation is not necessary in variable declarations nor in field declarations, assuming the field is immediately initialized in the constructor and assuming it remains non-null.

The type-checker then ensures that no operations that could raise a null pointer error are performed. The only exception is that we cannot check code from external libraries, just the code of your project. To avoid potential null-pointer errors from occurring when working with libraries, we assume that methods from those libraries may return null. Nonetheless, stub files can be used to augment the types of parameters and return values in methods of interfaces. See Protocols for third-party libraries.

Additionally, the type-checker is able to refine the type of nullable values when a comparison with null is made in if statements or in the conditions of loops.

@Nullable @Ensures("Open") File tryOpening() {
  File file = new File();
  return file.open() ? file : null;
}

void main1() {
  File file = tryOpening();
  file.read(); // Error
  file.close();
}

void main2() {
  File file = tryOpening();
  if (file != null) {
    file.read(); // OK
    file.close();
  }
}

Furthermore, if a class has a protocol, we use that information to know which methods are called before other ones. This allows us to avoid reporting nullness errors if we know that an initializing method was necessarily called before another one that reads from a given field.

Linearity

By default, the tool ensures that objects with protocol are used linearly, this implies that there is only one reference occurring in memory at any given time that can be used to call methods on an object to change its state.

By default, methods of a class without protocol and methods of a class with protocol that are not mentioned in the protocol are always available to be called. We call these anytime methods. But to preserve soundness with regards to linearity, these methods cannot modify the fields of that object and cannot change the states of objects referenced by those fields.

On a shared (i.e. aliased) reference, only these kinds of methods (i.e. methods that are always available), may be called.

To ensure linear use of objects, every time a reference to an object is assigned to a local variable, field, parameter, the previous variable is given the "shared type", and the new variable is given the "linear type". In other words, methods that modify state can then only be called through the new variable, while the old variable only allows for "anytime" methods to be called.

@Requires annotation

This annotation may be used in the parameters of method declarations to indicate in which states the object pointed by the parameter is expected to be in. If this annotation is not used, the type-checker assumes that the parameter receives an aliased reference. The annotation expects a string argument or an array of strings with the names of the required states.

void readFile(@Requires("Open") File file) {
  file.read();
  file.close();
}

@Ensures annotation

This annotation may be used in the return types of method declarations. It indicates the states in which a returned object is after the method call. If this annotation is not used, the type-checker assumes that the returned reference is aliased. The annotation expects a string argument or an array of strings with the names of states.

@Ensures("Open") File newFile() {
  File file = new File();
  file.open();
  return file;
} 
@Ensures("Open") File newFile(@Requires("Init") File file) {
  file.open();
  return file;
}

Protocol completion

When working with objects whose use is expected to follow a protocol, it is important not only to ensure that method calls are performed in valid sequences, but that objects are used to completion (i.e. until they reach the final state). This ensures that the implementation is correct by preventing method calls from being forgotten and by freeing resources that are no longer necessary. For example, this can be used to ensure that the close method on a socket is called after the socket is no longer in use.

typestate Socket {
  NotConnected = {
    void connect(): Connected
  }
  Connected = {
    void send(String): Connected,
    void close(): end
  }
} 

Socket s = new Socket();
s.connect();
s.send("Hello World!"); // Error: protocol did not complete
Socket s = new Socket();
s.connect();
s.send("Hello World!");
s.close(); // OK

Droppable states

There are cases where we do not need to explicitly end the protocol of an object. To support this kind of scenario, protocol specifications support a special kind of transition. This transition represents the dropping of an object and transits it to the end state. It happens implicitly when an object is no longer used. This is similar to how the drop method is automatically called in Rust when an object goes out of scope. One key feature of this special transition is that it does not need to be defined in all states. This allows one to indicate in which states the object may be dropped. States that do not include this transition are states where the object cannot be dropped.

typestate Iterator {
  HasNext = {
    boolean hasNext(): <true: Next, false: end>,
    drop: end
  }
  Next = {
    boolean hasNext(): <true: Next, false: end>,
    Object next(): HasNext,
    drop: end
  }
}

In this example is defined a protocol for an iterator which may be dropped in any state. That is specified by the drop: end transition defined in the HasNext and Next states. This means that one may stop using the iterator if it is either in the HasNext state or in the Next state.

Subtyping

The tool also has support for subtyping. This means that you may have a class with a protocol that extends another class with another protocol and the tool will ensure that the first protocol is a subtype of the second one.

One can also create a class with protocol that extends a class without protocol. In the class without protocol, all the methods are available to be called and need to remain so in the subclass, which means that they cannot be mentioned in the protocol of the subclass. In other words, "anytime" methods should remain "anytime" in subclasses.

If a class extends another class with protocol, but does not include a @Typestate annotation, the subclass assumes by default the same protocol of its superclass.

The algorithm for supporting protocol subtyping takes inspiration from the synchronous subtyping one for session types. It builds graphs from the protocols to be checked, traverses them by firing common input/output operations and marks each encountered pair of states. Notice that, in our setting, input operations are represented by method calls, while output operations by values returned by them. We mark pairs of states if: (i) both are input states and input contravariance holds, i.e. the subtype can perform a set of input operations greater or equal to the one of the supertype, (ii) both are output states and output covariance holds, i.e. the supertype can perform a set of output operations greater or equal to the one of the subtype, (iii) both states are end states. The algorithm stops when either all reachable pairs have been marked (subtyping holds) or a pair of states does not satisfy any of the above conditions (subtyping does not hold). Since Java does not support inheritance in enumeration classes, we have to consider all enumeration values as potentially returnable and, consequently, all should be included in the protocol. Because of this, output covariance always holds (in our setting all outputs are invariant).

You may look at some examples here of classes that inherit from others.

Casts

With support for subtyping, casts need to be handled. In Java, up and down-casts may occur explicitly and up-casts may occur implicitly when assigning to local variables or fields, passing objects to parameters or returning objects. To showcase this, consider the following examples and classes with their protocols:

typestate A {
  Init = {
    void m1(): StateA
  }
  StateA = {
    void m2(): end
  }
}

typestate B {
  Init = {
    void m1(): StateB
  }
  StateB = {
    void m2(): end
  }
}

@Typestate("A")
class A {
  void m1() {}
  void m2() {}
}
@Typestate("B")
class B extends A {…}

When passing a typestate-endowed object to a method call, 3 possibilities may occur:

  • The method requires an object of the same class and in the method signature there is an @Requires annotation with the state in which the object must be when it is passed.
public static void main() {
  A a = new B();
  a.m1();
  playA(a);
}

public static void playA(@Requires("StateA") A a) {...}
  • The method requires an object of a superclass and an implicit up-cast is performed.
public static void main() {
  B b = new B();
  playA(b);
}

public static void playA(@Requires("Init") A a) {...}
  • If the method has no @Requires annotation, it expects either an aliased reference or a reference to an object that is in the end state (notice that a reference to an object that has completed its protocol can be seen as an aliased reference). You can turn a linear reference into a shared (aliased) reference by assigning it to a different variable which will get the linear reference, while the old one becomes shared. The reason why one cannot just pass a linear reference to a parameter without @Requires annotation is that one would not be able to finish the protocol. In this example one must, at first, put the object b into another variable a and then pass b to the method. Below you can find an example:
public static void main() {
  B b = new B();
  A a = b; // b becomes shared
  a.m1();
  playA(b);
}

public static void playA(A a) {...}

Protocols for third-party libraries

Since classes belonging to those third-party libraries might not be associated with protocol specifications, the tool allows one to associate protocol files with classes or interfaces in a configuration file.

The content of this configuration file follows the same syntax of .properties files, commonly used in the Java community. Each line in the file is a mapping from a key to a value. In this instance, the key is the full qualified name of a class or interface and the value is the path (relative to the configuration file) of the protocol file. An example follows.

java.util.Iterator=Iterator.protocol

To use a configuration file, add the -AconfigFile=PATH_TO_FILE option.

The tool also supports stub files (a feature already present in the Checker Framework). A stub file is Java source code that omits method bodies and allows one to write annotations for a library when the code is not available to be edited.

import jatyc.lib.Ensures;

package java.util;

public interface List<E> {
  @Ensures("HasNext") Iterator<E> iterator();
}

In this example is shown the content of a stub file which provides an annotation for the iterator method in the List interface of the standard Java library. With the use of the @Ensures annotation, we inform the type-checker that the returned iterator is a linear reference in the HasNext state.

Suppressing errors or warnings

To suppress any errors or warnings, one may use the @SuppressWarnings("all") annotation on the method or class where error/warning messages should be suppressed, an in the following example.

public class Tasks {
  @SuppressWarnings("all")
  private Object makeDescription() {
    return null;
  }
}
Clone this wiki locally