JavaCOP Tutorial

Contact Shane Markstrum (smarkstr at cs dot ucla dot edu) with any questions or comments.

How to run JavaCOP as an extensible type checking compiler

Using JavaCOP is as easy as using javac. In fact, JavaCOP is simply an extension of the OpenJDK version of javac. This tutorial will teach you how to run JavaCOP using the C shell scripts that we provide. To learn how to run JavaCOP by directly invoking java and javac, you can read our scripts, or take a look at this older tutorial.

First Steps:

Obtain a copy of the JavaCOP jar and the JavaCOP scripts (jcopc and javacop), which can be found on the JavaCOP SourceForge site.
Set the $JCOPJAR to the full path to the JavaCOP jar in your C shell environment. Below is an example line from a .cshrc file.
```
setenv JCOPJAR /home/smarkstr/libraries/JavaCop.jar
```
Verify that your environment variable is maintained in a fresh C shell environment.
```
echo 'echo $JCOPJAR' | csh -t
/home/smarkstr/libraries/JavaCop.jar
```
You're ready to start using JavaCOP!

Compiling JavaCOP Rules

If you are eager to start type checking Java programs with JavaCOP, then this section is optional so long as you download NonnullRules.jar. Skip to next section

This section will teach you how to go from a JavaCOP rule file to a compiled JavaCOP checker which can be utilized by the JavaCOP Compiler. If you are interested in learning how to develop rules, you can visit the rule development section.

Obtain a copy of the JavaCOP Repository from the JavaCOP SourceForge site and untar it. Go to the javacop/examples/nonnull directory. The directory should contain two subdirectories (javacop and tests) and the file Nonnull.jcop.
Nonnull.jcop is the file that contains the rule specification for a flow-sensitive non-null checker. To compile this into a Java class for use with JavaCOP compiler, you will use the jcopc script. The jcopc script takes in the name of the rules to be compiled (e.g., Nonnull) and any number of javac options after it. Since the Nonnull rules specify the package javacop.nonnull, the -d . option needs to be specified to place the generated class file in the examples/nonnull/javacop/nonnull directory.
```
prompt> jcopc Nonnull -d .
done
```
At this point, there should now be one new Java file in the examples/nonnull directory: Nonnull.java. In the examples/nonnull/javacop/nonnull directory, you should have four Java class files: Nonnull.class, Nonnull$1.class, NonNullFlowFacts.class, RawTypesFlowFacts.class. If compilation has succeeded, then you now have a working copy of the flow-sensitive non-null type checker. This checker can now be used by JavaCOP to type check Java programs. The next section will go into further details of how to type check Java programs.

Type Checking Java Files

At this point, you should have either a jar file or directory structure containing the classes for the flow-sensitive type checker which you can specify on the classpath of an invocation of the javacop script. For the remainder of this part of the tutorial, the placeholder NonnullRules.jar will be used to represent this classpath entry, such as:

prompt> javacop -jcp NonnullRules.jar ...

To type check Java files using JavaCOP, you will use the javacop script. The javacop script has the following usage, where the -jcp flag indicates classpath information containing compiled JavaCOP rules and rules are specified by their qualified Java class name:
```
javacop [-jcp paths] rules [javac_options] java_files
```
Before you can type check a Java file, you will need a file that exercises the pluggable type system which you will load. In this case, we will make a very simple Java class that has one field annoted as non-null and which assigns into that field a new Object instance. Save this class as TutorialClass.java
```
import javacop.annotations.Nonnull;

public class TutorialClass {

	@Nonnull Object f;
	
	public TutorialClass() {
		f = new Object();
	}
}
```

Now, if you run the javacop script to compile TutorialClass.java and pass javacop.nonnull.Nonnull as the first argument, it should compile without an error.

javacop -jcp NonnullRules.jar javacop.nonnull.Nonnull TutorialClass.java
Loading constraints class: javacop.nonnull.Nonnull
Done, loaded 1 constraint sets.

To create an error in TutorialClass, change the line
```
f = new Object();
```
to the line
```
f = null;
```

Now, rerun javacop and it will report an error.

javacop -jcp NonnullRules.jar javacop.nonnull.Nonnull TutorialClass.java
Loading constraints class: javacop.nonnull.Nonnull
Done, loaded 1 constraint sets.
TutorialClass.java:8: Nonnull: Using possibly null value where a @Nonnull value is expected
                f = null;
                    ^
1 error

That's all there is to using JavaCOP. It can act as a javac replacement in your toolchain, or as a supplementary tool. The JavaCOP compiler is based on the OpenJDK compiler, which is currently at version 1.7. To run any classes compiled with JavaCOP, you will need to target the compilation to a version of Java compatible with your java executable.

Developing JavaCOP rules

JavaCOP is not only a set of pluggable type checking utilities, but also a declarative language for writing pluggable type systems. In this portion of the tutorial, you will learn how to build a set of rules for a simple non-null type system. While this type system will not exercise every aspect of the JavaCOP language, it will provide insight into using the basic JavaCOP building blocks. For a more complete understanding of the features of the JavaCOP language, you should refer to the (currently non-existent) JavaCOP language manual.

At this point, it is expected that you are familiar with using the jcopc and javacop tools. If you are unfamiliar with these scripts, you should first read the scripts tutorial and ensure that the JavaCOP libraries and scripts are accessible in your programming environment.

Let's move on to the motivating example which will show how you can use a pluggable type system to provide some assurance that you will not generate unexpected NullPointerExceptions.

Motivating Example: A List Data Structure

When developing a library or data structure which is meant to be used in multiple places, you want more assurance that these reused components are bug-free. The goal for this section of the tutorial is for you to create a pluggable type system which ensures that a list data structure will not generate a NullPointerException. The example class for this tutorial is shown below and can be downloaded here.

public class List {

    protected Node root = new EmptyNode();

    public void insert(T t) {
	root = root.insert(t);
    }
}

interface Node {
    Node insert(T t);
}

class DataNode implements Node {
    protected T value;
    protected Node next;

    public DataNode(T value, Node next) {
	this.value = value;
	this.next = next;
    }

    public Node insert(T t) {
	next = next.insert(t);
	return this;
    }
}

class EmptyNode implements Node {

    public Node insert(T t) {
	return new DataNode(t, this);
    }

}

This List class has very simple functionality. The root field points to the head of the chain of Nodes which contain the values stored in the list. The only method which the class contains is the insert method, which simply delegates to the insert method of the root node. As a result, any value inserted in a List object will be stored in whatever manner the Nodes dictate.

There are also two implementations of the Node interface: DataNode and EmptyNode. A DataNode acts as the main link in a List and stores a value. Calling insert on a DataNode will cause it to delegate that call to its next field and store the result as the updated next reference. An EmptyNode is meant to act as the sentinel value of a List. Calling insert on an EmptyNode instance will return a new DataNode object which contains the provided value t, thus extending the list.

The First JavaCOP Rule - Null Dereference Checking

The first step to verifying non-nullness properties of the List class is to create a new JavaCOP program. For the purpose of this tutorial, you should create a new file called NonnullRules.jcop and open it in your favorite editing program. An empty file, however, is not going to do you any good, so let's create a rule that defines a discipline on dereferences in a program.

Check programs with the `rule` declaration

In particular, one important property of a non-null type system is to verify that dereferences at runtime will not generate NullPointerExceptions. One very conservative type system that is guaranteed to have this property is a type system that disallows any explicit dereferences (i.e., there are no dots in the program). To check this proprety, you need to define a rule in JavaCOP. This is done as a top level declaration in the JavaCOP file using the rule construct. Add the declaration below to your NonnullRules.jcop file.

rule nonnullDerefs(JCFieldAccess d){

}

You can break down this declaration into five main components:

The leading keyword: rule
The name of the rule: nonnullDerefs
The type of node in the abstract syntax tree where it will be enforced: JCFieldAccess (i.e., explicit dereferences)
A variable for accessing information about the abstract syntax tree node: d
The body of the rule

The type of AST node to visit is the most crucial aspect of the rule signature, as this provides the point at which rules will be checked. Since JavaCOP is built as an extension of the OpenJDK javac, you need to use the internal javac AST nodes in order to do type checking at the appropriate places in your Java programs. Some of the names of these nodes may be counterintuitive, such as JCFieldAccess in the example matching all places in the code where a dot is encounted, including method calls invoked on expressions. While JCTree will match any node, a brief overview of some of the other AST node names can be found in the AST quick reference guide.

Program constraits via the `require` statement

At this stage, you have a JavaCOP rule that you can use to type check your program, but as it has an empty body, it will always succeed. You need to specify some checks to perform on your Java program in order to guarantee the behavior you want. These checks come in the form of program constraints specified by a require statement, which takes a boolean expression clause as its parameter. Change your nonnullDerefs to include the require statement inserted below.

rule nonnullDerefs(JCFieldAccess d){
    require(false):warning(d, "Possible null dereference!");
}

This rule will now fail everytime an explicit dereference is found in a Java program. In particular, it will print a warning to the screen every time for every dotted expression. Note that in the body of a rule declaration, every statement may be associated with either a warning or error message that specifies where in the AST the failure occured (e.g., d) and a String expression that provides a user-specified failure message.

At this point, you are ready to compile your first JavaCOP file and use it to type check the List class. Save your NonnullRules.jcop file and use the jcopc script to compile it into NonnullRules.class. Then use the javacop script with the compiled rules to type check List.java.

prompt> jcopc NonnullRules
Done

prompt> javacop NonnullRules List.java
Loading constraints class: NonnullRules
Done, loaded 1 constraint sets.
List.java:6: warning: NonnullRules: Possible null dereference!
        root = root.insert(t);
                   ^
List.java:19: warning: NonnullRules: Possible null dereference!
        this.value = value;
            ^
List.java:20: warning: NonnullRules: Possible null dereference!
        this.next = next;
            ^
List.java:24: warning: NonnullRules: Possible null dereference!
        next = next.insert(t);
                   ^
4 warnings

Type checking List.java now prints out four warning for the places that might have null dereferences in the program. However, this result is less than satisfying, because it means that users of this type system will have to manually inspect each of these results to verify that there is no error. Moreover, it is clear without even looking at the program that two of these warnings are spurious: the this reference in Java is always guaranteed to be non-null.

Predicate definition with the `declare` declaration

To resolve this issue, you need to make the require statement's boolean clause indicate which kinds of Java expressions are known to be non-null. You could simply enumerate all the cases with the || operator, but the definition of what should and should not be treated as non-null is bound to be needed in multiple places in a non-null type system. Instead, you should define a boolean predicate that returns true if a Java expression should be considered non-null. In JavaCOP, such predicates are defined using the declare declaration. Add the following predicate definitions to your NonnullRules.jcop file.

declare defNonnull(JCIdent i){
    require(i.fullName.equals("this") || i.fullName.equals("super"));
}

declare defNonnull(JCNewClass c){
    require(true);
}

Predicate declaration signatures are the same as method signatures in Java, although they do not support primitive or generic types. HOwever, one key difference is that multiple declarations can be given for the same predicate. In the example above, you have two definitions of the predicate defNonnull. This means the predicate will be satisfied if any predicate declaration is satisfied (i.e., the predicate is the logical disjunction of the declarations). In this case, if the defNonnull predicate will be satisfied if it is checked on a Java new expression or an identifier with either the name this or super. The predicate can be further expanded by adding new declarations.

To incorporate this new predicate into your nonnullDerefs rule, change the body of the rule to the one shown below.

rule nonnullDerefs(JCFieldAccess d){
    require(defNonnull(d.selected)):warning(d, "Possible null dereference!");
}

Now, your nonnullDerefs rule will be satisfied if it sees a dereference of a known non-null entity, as defined by the defNonnull predicate. In this case, the two dereferences of this that you saw previously should now satisfy the rule and no longer generate a warning. Recompile your NonnullRules.jcop file and use it to type check List.java.

prompt> jcopc NonnullRules
Done

prompt> javacop NonnullRules List.java
Loading constraints class: NonnullRules
Done, loaded 1 constraint sets.
List.java:7: warning: NonnullRules: Possible null dereference!
        root = root.insert(t);
                   ^
List.java:25: warning: NonnullRules: Possible null dereference!
        next = next.insert(t);
                   ^
2 warnings

As expected, you now only have two places in List.java that are generating warnings. Without further information, though, JavaCOP will not be able to reason about these other two explicit dereferences. In the next section, you will use Java metadata to introduce non-null annotations into your Java program for which you can write JavaCOP rules to reason.

Java annotations introduce pluggable type qualifiers

At this point, there are a few more Java constructs and expressions which you can add to defNonnull, but they will not help to get rid of the warnings that are being generated when type checking List.java. To handle this situation, you want to add more documentation to your program to indicate that these fields should be considered non-null. To do this, you can use the Java metadata framework and decorate your program with annotations. In particular, you can create a @Nonnull annotation which will indicate that variables, parameters, and fields have a non-null type and methods return non-null types.

These annotations are very simple, such as the one shown below.

package myrules;

public @interface Nonnull { }

If you compile this annotation and put the class in the appropriate package directory, you can now use it in your Java programs. Annotations can be used in declarations just as you would use any other modifier such as public or static. In particular, you can now declare that the root field of List, and the next field of DataNode are @Nonnull. Don't forgot to include the annotation just like you would include another interface or class, or Java will complain! Your class should now look similar to this class.

If you recompile this class with your NonnullRules type checker, you will notice that just adding the annotations to Java does not cause the type checker to instantly recognize that these additions relate to the non-null type checker. But this makes sense, because there is no reason why you had to use the name @Nonnull. You could have called it @NonNull, started non-null variable names with two capital Ns, or decided to use a non-null-by-default semantics and added a @Nullable annotation instead. All of these are valid ways to introduce non-null types into a program. So, what you need to do at this point is augment your NonnullRules type checker to reason about the @Nonnull annotation that you created.

To add this functionality, you will define a new predicate hasNonnullAnnot which will be satisfied if it is checked on a program entity which has the @Nonnull annotation.

declare hasNonnullAnnot(Symbol s){
  require(s.hasAnnotation("myrules.Nonnull"));
}

declare hasNonnullAnnot(JCTree t){
  require(t.holdsSymbol && hasNonnullAnnot(t.getSymbol));
}

Now, the first thing you might notice about this predicate definition is that the first declaration matches Symbol. I will not go into great detail about this type here, but a Symbol object is a separate tree hierarchy in the compiler which contains information about declarations, such as type information and members. This information is also the same information that is recoverable from bytecode. Since annotations are always added at declarations in Java 7.0 (and earlier), this is the best and most direct place to look for annotations on source code or bytecode.

The second declaration utilizes the first declaration, but with a caveat: only declared entities can safely be tested for annotations. If the JCTree is a declared entity, then it is tested for the annotation and the predicate is satisfied if the annotation is found. If the holdsSymbol guard is not checked here, then the result of t.getSymbol might be null, which would result in a null pointer exception -- the exact thing we are trying to avoid in our Java code!

This predicate can now be incorporated into the defNonnull predicate to determine if a Java expression is non-null.

declare defNonnull(JCTree t){
  require(hasNonnullAnnot(t));
}

Using this new set of rules to test your List class now results in no warnings! But you're not done yet unless you trust that the @Nonnull annoations are being used correctly. What you want to do next is actually use JavaCOP to ensure that null values are not actually being stored in variables and fields declared with @Nonnull. This is the focus of the next section.

Checking deeper properties of the type system

In this section, we will create more rules that use the predicates we previously defined. These rules will ensure that the first rule we developed actually prevents null dereferences.

Rule: Assignments to `@Nonnull` reference

Here, we will make sure that updates to the fields and locals with the @Nonnull annotation do not violate the non-null discipline we have established so that unexpected null pointer exceptions are avoided. The following rule says that at an assignment statement, if the left hand side reference claims to be @Nonnull, then the right hand side expression must be a non-null value.

rule nonnullAssign(JCAssign a){
  where(hasNonnullAnnot(a.lhs)){
    require(defNonnull(a.rhs)):warning(a, "Possible assignment of null value to @Nonnull reference!");
  }
}

Rule: `@Nonnull` return statements

rule nonnullReturn(JCReturn r){
  where(hasNonnullAnnot(r.enclMethod)){
    require(defNonnull(r.expr)):warning(r, "Possible return of null value from @Nonnull method!");
  }
}

Overriding Rule: @Nonnull information flow

rule nonnullFlow(a <<: b){
  where(hasNonnullAnnot(b)){
    require(defNonnull(a)):warning(a, "Using possibly null value where a @Nonnull value is expected!");
  }
}

Rule: `@Nonnull` reference initialization

rule nonnullInit(JCVariableDecl v){
  where(hasNonnullAnnot(v)){
    require(Expr e; v => [^^ ^* = e]):warning(a, "@Nonnull fields and locals must be initialized!");
  }
}

More to come!

How to use the JavaCOP runtime framework

Hopefully coming Soon!