Missing java.nio in JPF?

[Uri Klein]

Hello,

I am trying to use JPF in what seems to be a rather ambitious project.
We are trying to run the Grizzly servlet container on top of JPF and
verify some servlet code. In the process we have run into a library
missing from JPF - java.nio - and we were wondering if anyone might
have an implementation or know of someone who has ported it into JPF.

Thank you very much.

[Peter Mehlitz]

unfortunately I'm not aware of anybody modeling java.nio yet

-- Peter

[Uri Klein]

Thank you for your quick response.

If you do not mind - we have yet another problem with using JPF. They
way we believed JPF was working, was that it could access only classes
that are in its JPF classpath. However, when we run our code in
Eclipse and get error messages, the stack trace appears to suggest
that the program accesses classes that are not to be found anywhere in
the JPF classpath.

For example, despite the fact that, as you say, java.nio is not
implemented in the main distribution of JPF (or in the concurrency
package which we use as well), we get a stack trace that ends in a
method call to a java.nio class that cannot be found by JPF, but
following a few other java.nio classes on the stack. This is the stack
trace that we get:

gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty
java.lang.NoSuchMethodError: sun.misc.Unsafe.allocateMemory(J)J
at java.nio.Bits.<clinit>(Bits.java:581)
at java.nio.ByteBuffer.<init>(ByteBuffer.java:1380)
at java.nio.HeapByteBuffer.<init>(HeapByteBuffer.java:70)
at java.nio.ByteBuffer.wrap(ByteBuffer.java:367)
at java.nio.ByteBuffer.wrap(ByteBuffer.java:390)
at
com.sun.grizzly.http.SocketChannelOutputBuffer.<clinit>(SocketChannelOutputBuffer.java:
134)
at
com.sun.grizzly.http.ProcessorTask.initialize(ProcessorTask.java:506)
at
com.sun.grizzly.http.SelectorThread.rampUpProcessorTask(SelectorThread.java:
981)
at com.sun.grizzly.http.SelectorThread.run(SelectorThread.java:
1083)

Before this stack trace, we get a few warnings about orphant
NativePeer methods from the cuncurrent package.

Thank you very much,
Uri Klein

[Peter Mehlitz]

the JPF classpath automatically includes sun.boot.class.path, i.e. the standard libraries from rt.jar or classes.jar of your Java installation. This is in ClassInfo.buildModelClassPath(), and you can see it if you start with +log.fine=gov.nasa.jpf.jvm.ClassInfo

Keep in mind that most of the standard libraries are bytecode only, and we want to directly use as much of this code as possible. We only need to model classes if they either
(a) require native methods (like java.nio)
(b) interface with jpf-core mechanisms (like java.lang.Thread etc.)

The reason for (a) is that we can't account for native changes when storing/matching/restoring program state. The way such libraries are modeled depends on functionality and required properties, examples being jpf-awt (for applications using javax.swing) and jpf-net-iocache (for applications using java.net)

-- Peter