Java News from Thursday, April 28, 2005

Spiral of Death

NASA (yes, that NASA) has released Java PathFinder, an open source static code analysis tool for compiled Java bytecode. "In its basic form, it is a Java Virtual Machine (JVM) that is used as an explicit state software model checker, systematically exploring all potential execution paths of a program to find violations of properties like deadlocks or unhandled exceptions. Other than traditional debuggers, JPF reports the whole execution path that leads to a defect. JPF is especially suitable to find hard-to-test concurrency defects in multithreaded programs." Unlike a lot of static analysis tools such as PMD, PathFinder is designed to check programs, not classes. It starts from the main() method, and works its way through the program from there.

PathFinder is only available in source form. You'll have to compile it yourself. There's a build.xml file, but it doesn't actually work. Some directories and thrid party libraries are missing. These need to be installed manually. One of those libraries (FastMD5) isn't even available as a JAR archive. You have to manullay build your own JAR. Furthermore it uses C code, all to do some that can be done with pure Java code and no extra libraries using the standard class library. After I finally got all the necessary libraries installed and the classpath set up so I could test PathFinder on some of my code, it promptly threw a NullPointerException:

$ java -classpath 
build/jpf:lib/xercesImpl.jar:lib/bcel.jar:lib/fastmd5.jar:
/Users/elharo/Projects/XOM/build/classes:
/Users/elharo/Projects/XOM/build/jaxen-classes 
gov.nasa.jpf.JPF  nu.xom.samples.FibonacciXML
Java Pathfinder Model Checker v3.1.2 - (C) 1999-2004 RIACS/NASA Ames Research Center

java.lang.NullPointerException
        at gov.nasa.jpf.jvm.MJIEnv.getElementInfo(MJIEnv.java:593)
        at gov.nasa.jpf.jvm.MJIEnv.getClassInfo(MJIEnv.java:580)
        at gov.nasa.jpf.jvm.ThreadInfo.printStackTrace(ThreadInfo.java:1309)
        at gov.nasa.jpf.jvm.ExceptionInfo.printOn(ExceptionInfo.java:51)
        at gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty.printOn(NoUncaughtExceptionsProperty.java:54)
        at gov.nasa.jpf.search.PropertyMulticaster.printOn(PropertyMulticaster.java:112)
        at gov.nasa.jpf.Error.printOn(Error.java:58)
        at gov.nasa.jpf.util.Debug.println(Debug.java:199)
        at gov.nasa.jpf.util.Debug.println(Debug.java:205)
        at gov.nasa.jpf.search.AbstractSearch.error(AbstractSearch.java:254)
        at gov.nasa.jpf.search.AbstractSearch.isPropertyViolated(AbstractSearch.java:137)
        at gov.nasa.jpf.search.AbstractSearch.hasPropertyTermination(AbstractSearch.java:126)
        at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:90)
        at gov.nasa.jpf.JPF.run(JPF.java:249)
        at gov.nasa.jpf.JPF.main(JPF.java:198)

This product is a lot rougher than I would have expected from NASA, especially given the fanfare with which it was announced. PathFinder is published under the NASA Open Source Agreement.


Jayasoft has released Ivy 1.0, a free Java based dependency manager, that features transitive dependencies, Ant integration, Maven compatibility, and continuous integration.