Fixing a bug in ClassLoader.defineClass(); basically this method has to still return...
authorrtrimana <rtrimana@uci.edu>
Tue, 16 Jul 2019 20:22:12 +0000 (13:22 -0700)
committerrtrimana <rtrimana@uci.edu>
Tue, 16 Jul 2019 20:22:12 +0000 (13:22 -0700)
examples/SunClassLoader.java
jpf.properties
src/examples/Racer.java
src/peers/gov/nasa/jpf/vm/JPF_java_lang_ClassLoader.java

index 7d022c65a9a15ccac930e3d3ed1ac47b7307ef0d..49b8117c96fb7756806e3afcc24c619d59d816e8 100644 (file)
@@ -28,6 +28,7 @@ public class SunClassLoader extends ClassLoader implements Opcodes {
     protected void define(byte[] bytes, final String name) {
         //knownClasses.put(name, defineClass(name, bytes, 0, bytes.length));
         Class cls = defineClass(name, bytes, 0, bytes.length);
+        //Class cls2 = defineClass(name, bytes, 0, bytes.length);
     }
 
     protected final Map<String,Class> knownClasses = new HashMap<String,Class>();
@@ -36,6 +37,6 @@ public class SunClassLoader extends ClassLoader implements Opcodes {
         SunClassLoader sun = new SunClassLoader();
         sun.loadMagic();
         
-        Class cls = sun.loadClass("java/lang/Object");
+        //Class cls = sun.loadClass("java/lang/Object");
     }
 }
index f4f093d2f30fcef24ca6e17326c757b7afaecfe4..8942678621075358076c951d93d9c4ceb0cebc50 100644 (file)
@@ -22,6 +22,7 @@ jpf-core.native_classpath=\
 
 jpf-core.classpath=\
   ${jpf-core}/build/jpf-classes.jar;\
+  ${jpf-core}/build/asm-7.1.jar;\
   ${jpf-core}/build/examples
 
 jpf-core.sourcepath=\
@@ -419,7 +420,7 @@ listener.gov.nasa.jpf.Const=gov.nasa.jpf.tools.ConstChecker
 ### PreciseRaceDetector
 
 # we don't check for races in standard libraries
-race.exclude=java.*,javax.*,groovy.*,org.*
+race.exclude=java.*,javax.*
 
 
 ############################### 5. test part #############################
index 227cfab422f067fe0a02d1a189367c6fedeff61f..c53bb4827695d9f1a660c58d18c5b3b7d8930d0b 100644 (file)
  * limitations under the License.
  */
 
-public class Racer implements Runnable {\r
-\r
-     int d = 42;\r
-\r
+public class Racer implements Runnable {
+
+     int d = 42;
+
      @Override
-       public void run () {\r
-          doSomething(1001);                   // (1)\r
-          d = 0;                               // (2)\r
-     }\r
-\r
-     public static void main (String[] args){\r
-          Racer racer = new Racer();\r
-          Thread t = new Thread(racer);\r
-          t.start();\r
-\r
-          doSomething(1000);                   // (3)\r
-          int c = 420 / racer.d;               // (4)\r
-          System.out.println(c);\r
-     }\r
-     \r
-     static void doSomething (int n) {\r
-          // not very interesting..\r
-          try { Thread.sleep(n); } catch (InterruptedException ix) {}\r
-     }\r
-}\r
+       public void run () {
+          doSomething(1001);                   // (1)
+          d = 0;                               // (2)
+     }
+
+     public static void main (String[] args){
+          Racer racer = new Racer();
+          Thread t = new Thread(racer);
+          t.start();
+
+          doSomething(1000);                   // (3)
+          int c = 420 / racer.d;               // (4)
+          System.out.println(c);
+     }
+     
+     static void doSomething (int n) {
+          // not very interesting..
+          try { Thread.sleep(n); } catch (InterruptedException ix) {}
+     }
+}
index f6eb53da9107e9c4da02e1eafc46f908a1f86273..cfea25c6ae1db7995ba1247ae0ee44086e013943 100644 (file)
@@ -143,9 +143,10 @@ public class JPF_java_lang_ClassLoader extends NativePeer {
     ClassLoaderInfo cl = env.getClassLoaderInfo(objRef);
 
     // determine whether that the corresponding class is already defined by this
-    // classloader, if so, just return the already defined class!
+    // classloader, if so, this attempt is invalid, and loading throws a LinkageError
     if (cl.getDefinedClassInfo(cname) != null) {  // attempt to define twice
-      return cl.getDefinedClassInfo(cname).getClassObjectRef();
+      env.throwException("java.lang.LinkageError");
+      return MJIEnv.NULL;
     }
         
     byte[] buffer = env.getByteArrayObject(bufferRef);
@@ -180,8 +181,16 @@ public class JPF_java_lang_ClassLoader extends NativePeer {
 
     int sysObjRef = env.getSystemClassLoaderInfo().getClassLoaderObjectRef();
     if (objRef != sysObjRef) {
-      return defineClass0__Ljava_lang_String_2_3BII__Ljava_lang_Class_2
-              (env, sysObjRef, nameRef, bufferRef, offset, length);
+      // Check if this class has been defined in the SystemClassLoader
+      ClassLoaderInfo cl = env.getSystemClassLoaderInfo();
+      String cname = env.getStringObject(nameRef);
+      if (cl.getDefinedClassInfo(cname) != null) {
+        ClassInfo ci = cl.getResolvedClassInfo(cname);
+        return ci.getClassObjectRef();
+      } else {
+        return defineClass0__Ljava_lang_String_2_3BII__Ljava_lang_Class_2
+                (env, sysObjRef, nameRef, bufferRef, offset, length);
+      }
     }
     env.throwException("java.lang.ClassNotFoundException");
     return MJIEnv.NULL;