Terse Systems

I’ve liked the idea of program verification since I first saw it, way back in Z. Program Verification has been around since Hoare’s paper in 1969, but it’s never really caught on. I suspect part of the reason is that it was expressed through things like Z.

This is a pity, because verification such a simple, beautiful idea that it’s popped up in multiple different ways, from Design by Contract to Defensive Programming to Unit Testing to Assertions to Static Code Analysis. They take different attitudes, but look for the same results – testing the code in a single method or class such that invalid input is rejected and any hidden bugs are made visible. And the faster you find bugs, the easier it is to fix them.

In this particular case, I wanted to find possible NullPointerException. Dereferencing a null pointer is one of the classic mistakes that most people make in their first program. It’s still incredibly easy to make. It’s also incredibly easy to prevent. There are only so many ways to get a reference.

NPE can come from parameters:

public void foo(String pNull) {
   pNull.trim();
}

String mNull = null;
public void foo() {


mNull.trim();


}

public void foo() {


getNull().trim();


}

If you check all your references, NPE cannot happen in your code. All you have to do is read through the code and think “could this be null here?”

So it made sense that if there were simple checks that could be applied, I could find or make a tool to verify that a program could not suffer from NPE.

I’ve been using PMD to find bugs in code. I ran up against the limits of PMD when I tried to write a rule that would trace variables for NPE. PMD generates an abstract syntax tree of code. Although it can recognize patterns of code, it doesn’t know that a variable referenced in one pattern is the same variable in the other pattern. I could have added that functionality, but I figured there must be tools which tracked the flow and state of variables in a method and could determine if they were null or not.

And there are. They’re called Data Flow Analysis tools. But some of them cost serious money, and some of them consume outrageous amounts of CPU time. (JTest and Excelsior FlawDetector, respectively.) So I started at looking at Design by Contract tools to see if I could at least prevent null parameter values from being passed to a method through preconditions.

I’ve looked at DBC tools repeatedly throughout the years, but they’ve always seemed too jerry-rigged to use in production systems. Things like iContract, jContractor, and JMSAssert. They always felt strangely unfinished, more like proofs of concept than actual tools. And they were old – untouched in years or more. (Jass looks like the exception, though I haven’t tried it myself.)

I found JML this time around. This is a DBC language designed for use in Java. It feels like a real, solid tool. Unlike Z, it uses a Java-like syntax, and hides the formal specification language under the covers. It supports post conditions on exceptional states, i.e. mandating that an exception must contain a non-null message. It can even define state modelling variables, so that a JavaBean property variable can be proved to be non-null after its mutator is called. It’s supported by several applications and has an active base of researchers who are finding new and interesting ways to exploit JML to say things about dynamic program state that weren’t possible before. The PDF tutorial is available here.

The suite of tools provided with JML encompasses jmlc (a compiler that adds run-time assertions to the compiled bytecode automatically), jmlunit (generates unit tests from the JML annotations), jmldoc (adds JML annotations to the javadoc, although you’d think that just specifying a doclet would be adequate), and finally escjava2 (extended static checker). Of these, the extended static checker is the most interesting.

The extended static checker (ESC), although it’s mentioned as part of JML has actually been through a long history spanning ten years. The first version was written to check Modula-3. Then there was a version to check Java, which used a limited subset of JML. Finally, there’s a second version of ESC which has been rewritten to integrate better with JML. This latest version, if it has an official name, is ESC/Java 2 [edit: mistyped this as ESC2/Java], which I’m abbreviating as ESC2. I mention this up front because many of the papers will mention ESC/Java, which is the older version written by the Compaq Research Center.

ESC2 does exactly what I want – it reads the source code of a program and points out every place that a null variable could exist. It will also test the JML pre and post conditions to see if it can prove the theorum is always true. If you call methods from a class library or JAR file, you can provide a specification file which will provide ESC2 with assurances that the external methods to the class cannot return null.

Here’s an example:

public void foo() {


getString().trim();


}

will be flagged by ESC2 automatically

Warning: Possible null dereference (Null)
   getString().trim();


    ^

unless you specify

/ ensures \result != null; /
  public String getString() { ... }

to the source code or the specification file.

The downside is that you have to add these annotations everywhere, or add null checks which make the annotations unnecessary. I think it’s safer to write the null checks anyway, because JML annotations will only work in situations where someone is using the JML toolkit. That puts more weight on the organization to use the toolkit in their build process, and if they don’t… well, your code will still die with NPE when someone else’s code passes a null parameter into your method, and the fact that it’s got some javadoc saying you shouldn’t do that is going to be no consolation when they call you at 2 in the morning.

JML opens up methods of programming that weren’t there before. With JML, I can write the assertions first, generate the unit tests from JML, and prove the assertions correct with ESC2. Without starting the program. Not only that, anyone else who interacts with my code can test their code against mine without even reading the javadoc and know that it’s covered against basic errors.

And I can tag methods I know to be buggy so that the bugs will be caught by JML. For example:

public void foo() {
  StringTokenizer st = new StringTokenizer(null);
}

This code won’t trigger any ESC2 warnings, but StringTokenizer has a bug which will cause NPE here. But I can tag StringTokenizer with JML to prevent this bug from ever being reached.

Because ESC2 has a common base in JML, it can be used with other programs that produce JML. Daikon is a tool which will look at a dynamically running program and try to find invariants and preconditions for a set of classes. It will output those constraints as JML, and ESC2 can then be used to check them. Here’s the paper on the result. (Note that he’s using ESC, not ESC2, so some of the limitations may no longer apply.)

There’s even an empirical evaluation of Daikon, ESC and Houdini (an annotation assistant that’s not publically available, so don’t bother trying to find it) which determines how useful these tools are in practice – the upshot seems to be that it works, but that it helps to have an annotation assistant and a fast computer when checking code. You may want to read Hacknot’s post on how studies can be skewed to the expected result before taking this too seriously.

Now for the bad news. ESC2 is still very clearly academic software, and is still in Alpha [edit: although, given the amount of JML in it, it’s probably higher quality than most other alpha software]. The [edit: installation] documentation in the binary release is unclear. There’s no Ant task. The ESC2 command line options have very little explanation. There’s a bug in resolving String invariants. Also, ESC2 doesn’t actually solve theorums itself – it generates theorem statements and passes them to another program called Simplify.

Simplify is actually written in Modula-3, is distributed as a binary executable, and is currently unmaintained. When I ran ESC2 on an ATG Dynamo project, ESC2 managed to crash Simplify twice by feeding it some hugely complex theorums.

That being said, this is one seriously kick ass tool just for the NPE detection alone. With some extra integration and some more build support, ESC2 could bring coding standards to a whole new level.