COSC6490A

This page is read only. You can view the source, but not change it. Ask your administrator if you think this is wrong.
====== Handling Native Code ======

Consider, for example, the following app.
<code java>
import java.util.Date;
                                                                                
public class Now
{
    public static void main(String[] args)
    {
        Date now = new Date();
        System.out.println(now);
    }
}
</code>
If we run JPF on this app, we get something like
<code>
JavaPathfinder v4.1 - (C) 1999-2007 RIACS/NASA Ames Research Center
 
 
====================================================== system under test
application: Now.java
 
====================================================== search started: 5/14/09 4:43 PM
 
====================================================== error #1
gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty
java.lang.UnsatisfiedLinkError: sun.misc.VM.initialize()V (no peer)
        at sun.misc.VM.<clinit>(VM.java:332)
        at java.nio.charset.Charset.atBugLevel(Charset.java:250)
        at java.nio.charset.Charset.checkName(Charset.java:272)
        at java.nio.charset.Charset.<init>(Charset.java:611)
        at sun.nio.cs.Unicode.<init>(Unicode.java:16)
        at sun.nio.cs.UTF_8.<init>(UTF_8.java:39)
        at sun.nio.cs.FastCharsetProvider.lookup(FastCharsetProvider.java:105)
        at sun.nio.cs.FastCharsetProvider.charsetForName(FastCharsetProvider.java:119)
        at java.nio.charset.Charset.lookup2(Charset.java:450)
        at java.nio.charset.Charset.lookup(Charset.java:438)
        at java.nio.charset.Charset.isSupported(Charset.java:480)
        at java.lang.StringCoding.lookupCharset(StringCoding.java:85)
        at java.lang.StringCoding.decode(StringCoding.java:165)
        at java.lang.String.<init>(String.java:444)
        at sun.util.calendar.ZoneInfoFile.getZoneAliases(ZoneInfoFile.java:777)
        at sun.util.calendar.ZoneInfo.getAliasTable(ZoneInfo.java:777)
        at sun.util.calendar.ZoneInfo.getTimeZone(ZoneInfo.java:608)
        at java.util.TimeZone.getTimeZone(TimeZone.java:469)
        at java.util.TimeZone.setDefaultZone(TimeZone.java:566)
        at java.util.TimeZone.getDefaultRef(TimeZone.java:533)
        at java.util.Date.normalize(Date.java:1176)
        at java.util.Date.toString(Date.java:1010)
        at gov.nasa.jpf.ConsoleOutputStream.println(ConsoleOutputStream.java:83)        at Now.main(Now.java:8)
 
 
====================================================== trace #1
------------------------------------------------------ transition #0 thread: 0
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>main}
      [17631 insn w/o sources]
 
====================================================== snapshot #1
thread index=0,name=main,status=RUNNING,this=java.lang.Thread@0,target=null,priority=5,lockCount=0
  owned locks:java.lang.Class@373,java.lang.Class@423,sun.nio.cs.StandardCharsets@1253,java.lang.Class@721
  call stack:
        at sun.misc.VM.<clinit>(VM.java:332)
        at java.nio.charset.Charset.atBugLevel(Charset.java:250)
        at java.nio.charset.Charset.checkName(Charset.java:272)
        at java.nio.charset.Charset.<init>(Charset.java:611)
        at sun.nio.cs.Unicode.<init>(Unicode.java:16)
        at sun.nio.cs.UTF_8.<init>(UTF_8.java:39)
        at sun.nio.cs.FastCharsetProvider.lookup(FastCharsetProvider.java:105)
        at sun.nio.cs.FastCharsetProvider.charsetForName(FastCharsetProvider.java:119)
        at java.nio.charset.Charset.lookup2(Charset.java:450)
        at java.nio.charset.Charset.lookup(Charset.java:438)
        at java.nio.charset.Charset.isSupported(Charset.java:480)
        at java.lang.StringCoding.lookupCharset(StringCoding.java:85)
        at java.lang.StringCoding.decode(StringCoding.java:165)
        at java.lang.String.<init>(String.java:444)
        at sun.util.calendar.ZoneInfoFile.getZoneAliases(ZoneInfoFile.java:777)
        at sun.util.calendar.ZoneInfo.getAliasTable(ZoneInfo.java:777)
        at sun.util.calendar.ZoneInfo.getTimeZone(ZoneInfo.java:608)
        at java.util.TimeZone.getTimeZone(TimeZone.java:469)
        at java.util.TimeZone.setDefaultZone(TimeZone.java:566)
        at java.util.TimeZone.getDefaultRef(TimeZone.java:533)
        at java.util.Date.normalize(Date.java:1176)
        at java.util.Date.toString(Date.java:1010)
        at gov.nasa.jpf.ConsoleOutputStream.println(ConsoleOutputStream.java:83)        at Now.main(Now.java:8)
 
 
====================================================== results
error #1: gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty "java.lang.UnsatisfiedLinkError: sun.misc.VM.initia..."
 
====================================================== statistics
elapsed time:       0:00:02
states:             new=0, visited=1, backtracked=0, end=0
search:             maxDepth=0, constraints=0
choice generators:  thread=1, data=0
heap:               gc=1, new=1842, free=48
instructions:       17631
max memory:         17MB
loaded code:        classes=137, methods=2029
 
====================================================== search finished: 5/14/09 4:43 PM
</code>
During the model checking of the app, JPF encounters some native code.

JPF has two ways to handle native code:
  * model class
  * native peer class

===== Model Class =====

We can model the toString method of the Date class as follows.
<code java>
package java.util;
 
/**
 * A model class for the toString method of the Date class.
 */
public class Date
{
    public String toString()
    {
        return "string representation of a Date object in the model class";
    }
}
</code>
To ensure that JPF model checks the above class, rather than the
Date class of the Java standard library, whenever the toString method
is invoked, we add the following to our jpf.properties file.
<code>
vm.bootclasspath+= ,modeldirectory
</code>
Note that modeldirectory is the directory in which the model classes can be found.  This directory contains java/util/Date.java.

If we run JPF, we get something like the following.
<code>
JavaPathfinder v4.1 - (C) 1999-2007 RIACS/NASA Ames Research Center
                                                                                
                                                                                
====================================================== system under test
application: Now.java
                                                                                
====================================================== search started: 5/14/09 4:52 PM
string representation of a Date object in the model class
                                                                                
====================================================== results
no errors detected
                                                                                
====================================================== statistics
elapsed time:       0:00:01
states:             new=1, visited=0, backtracked=0, end=1
search:             maxDepth=0, constraints=0
choice generators:  thread=1, data=0
heap:               gc=1, new=262, free=12
instructions:       2708
max memory:         10MB
loaded code:        classes=66, methods=839
                                                                                
====================================================== search finished: 5/14/09 4:52 PM
</code>

===== Model Class and Native Peer Class =====

We can also "model" the toString method by declaring it native.
<code java>
package java.util;
 
/**
 * Model class of the constructor and the toString method of the Date class.
 */
public class Date
{
    private long fastTime;
 
    public Date()
    {
        this.fastTime = System.currentTimeMillis();
    }
 
    native public String toString();
}
</code>
Note that we also model the constructor.  This is done since JPF uses the attribute fastTime internally.

Whenever JPF encounters a native method, it looks for a corresponding
native peer class.  In this case, we can use the following class.
<code java>
package gov.nasa.jpf.jvm;
 
/**
 * Native peer for the toString method of the Date class.
 */
public class JPF_java_util_Date
{
    public static int toString(MJIEnv env, int objref)
    {
        return env.newString(env.getDateObject(objref).toString());
    }
}
</code>

We have to ensure that the native peer class is part of the classpath
used by JPF and set the vm.bootclasspath appropriately for the model class.

If we run JPF, we get something like the following.
<code>
JavaPathfinder v4.1 - (C) 1999-2007 RIACS/NASA Ames Research Center
 
 
====================================================== system under test
application: Now.java
 
====================================================== search started: 5/14/09 5:02 PM
Thu May 14 17:02:54 EDT 2009
 
====================================================== results
no errors detected
 
====================================================== statistics
elapsed time:       0:00:01
states:             new=1, visited=0, backtracked=0, end=1
search:             maxDepth=0, constraints=0
choice generators:  thread=1, data=0
heap:               gc=1, new=262, free=14
instructions:       2709
max memory:         17MB
loaded code:        classes=66, methods=839
 
====================================================== search finished: 5/14/09 5:02 PM
</code>