Differences

This shows you the differences between two versions of the page.

--- jpf-native:start [2009/05/14 20:42] – franck
+++ jpf-native:start [2009/05/14 21:03] (current) – franck
@@ Line 1: / Line 1: @@
 ====== Handling Native Code ======
-JPF has two ways to handle native code:
-  * model class
-  * native peer class
 Consider, for example, the following app.
@@ Line 17: / Line 13: @@
     }
 }
+</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>