Finalizing the beta version of the implementation for Groovy extension in JPF: JPF...
authorrtrimana <rtrimana@uci.edu>
Fri, 28 Jun 2019 18:39:38 +0000 (11:39 -0700)
committerrtrimana <rtrimana@uci.edu>
Fri, 28 Jun 2019 18:39:38 +0000 (11:39 -0700)
examples/Empty.groovy
examples/Racer.groovy [new file with mode: 0644]
examples/Rand.groovy
src/classes/java/lang/Class.java
src/classes/java/security/AllPermission.java
src/classes/java/security/ProtectionDomain.java
src/main/gov/nasa/jpf/vm/Types.java
src/peers/gov/nasa/jpf/vm/JPF_java_lang_Class.java
src/peers/gov/nasa/jpf/vm/JPF_java_lang_Thread.java
src/peers/gov/nasa/jpf/vm/JPF_java_lang_reflect_Method.java
src/peers/gov/nasa/jpf/vm/JPF_java_util_ResourceBundle.java

index 77aec71..b52e40d 100644 (file)
@@ -9,7 +9,7 @@ class Empty {
                //int result = x + y;
                //return result;
                println "installed() is called!"
-               //initialize()
+               initialize()
        }
 
        // This function is where you initialize callbacks for event listeners
diff --git a/examples/Racer.groovy b/examples/Racer.groovy
new file mode 100644 (file)
index 0000000..e8df2f8
--- /dev/null
@@ -0,0 +1,24 @@
+class Racer implements Runnable {
+     int d = 42
+
+     public void run () {
+          doSomething(1001)
+          d = 0                              // (1)
+     }
+
+     static void main (String[] args){
+          Racer racer = new Racer()
+          Thread t = new Thread(racer)
+          t.start()
+
+          doSomething(1000)
+          int c = 420 / racer.d              // (2)
+          println c
+     }
+     
+     def doSomething (int n) {
+          try { 
+               Thread.sleep(n) 
+          } catch (InterruptedException ix) {}
+     }
+}
index 53f483f..4d6ff32 100644 (file)
@@ -1,10 +1,15 @@
-int rand = Math.random()*10
+class Rand {
+       static void main (String[] args) {
+               println("Groovy model-checking")
+               Random random = new Random(42);
+       
+               int a = random.nextInt(2)
+               int b = random.nextInt(3)
+               println("a=" + a)
+               println("  b=" + b)
 
-if (rand < 5) {
-       //println "rand is less than 5: "
-       System.out.println(rand)
-} else {
-       //println "rand is greater than or equal to 5: "
-       System.out.println(rand)
+               int c = a/(b+a -2)
+               println("    c=" + c)
+       }
 }
 
index 7dd3947..97f8e90 100644 (file)
@@ -275,14 +275,13 @@ public final class Class<T> implements Serializable, GenericDeclaration, Type, A
   public native TypeVariable<Class<T>>[] getTypeParameters();
 
   public native Type getGenericSuperclass();
-  /*public Type getGenericSuperclass() {
-    throw new UnsupportedOperationException();
-  }*/
 
   public native Type[] getGenericInterfaces();
-  /*public Type[] getGenericInterfaces() {
-    throw new UnsupportedOperationException();
-  }*/
+
+  public native java.security.ProtectionDomain getProtectionDomain();
+
+  transient ClassValue.ClassValueMap classValueMap;
+  // TODO: Fix for Groovy's model-checking
 
   public Object[] getSigners() {
     throw new UnsupportedOperationException();
@@ -331,12 +330,6 @@ public final class Class<T> implements Serializable, GenericDeclaration, Type, A
     throw new UnsupportedOperationException();
   }
 
-  // TODO: Fix for Groovy's model-checking
-  public native java.security.ProtectionDomain getProtectionDomain();
-  /*public java.security.ProtectionDomain getProtectionDomain() {
-    throw new UnsupportedOperationException();
-  }*/
-
   void setProtectionDomain0(java.security.ProtectionDomain pd) {
     pd = null;  // Get rid of IDE warning 
     throw new UnsupportedOperationException();
@@ -351,9 +344,6 @@ public final class Class<T> implements Serializable, GenericDeclaration, Type, A
     throw new UnsupportedOperationException();
   }
 
-  // TODO: Fix for Groovy's model-checking
-  transient ClassValue.ClassValueMap classValueMap;
-
   public boolean isSynthetic (){
     final int SYNTHETIC = 0x00001000;
     return (getModifiers() & SYNTHETIC) != 0;
index 658c063..2c98855 100644 (file)
@@ -21,6 +21,7 @@ import java.util.Enumeration;
 import sun.security.util.SecurityConstants;
 
 // TODO: Fix for Groovy's model-checking
+// TODO: This model class is a placeholder for future implementation
 /**
  * MJI model class for java.security.AllPermission library abstraction
  */
index 09650ab..66ddad5 100644 (file)
@@ -24,6 +24,7 @@ import sun.security.util.Debug;
 import sun.security.util.SecurityConstants;
 
 // TODO: Fix for Groovy's model-checking
+// TODO: This model class is a placeholder for future implementation
 /**
  * MJI model class for java.security.ProtectionDomain library abstraction
  */
index c0edb79..313e8aa 100644 (file)
@@ -1211,7 +1211,6 @@ public class Types {
     return arrTypeVarNames;
   }
 
-  // TODO: Fix for Groovy's model-checking
   public static String[] getParameterizedTypes(String signature) {
     int pos = signature.indexOf('<', 0);
     if (pos == -1)
@@ -1311,7 +1310,6 @@ public class Types {
     }
 
     String cleanSig = signature.replaceAll("\\+|-", "");
-    // This kind of signature should be a repetition of its class' type parameter, e.g., TT for Class<T>
     if (cleanSig.length()%2 != 0) {
       // This is probably a class, e.g., +java.lang.Class
       return signature;
index 20c59e8..ef0d782 100644 (file)
@@ -161,7 +161,6 @@ public class JPF_java_lang_Class extends NativePeer {
     return typeVarRef;
   }
 
-  // TODO: Fix for Groovy's model-checking
   @MJI
   public int getGenericSuperclass____Ljava_lang_reflect_Type_2 (MJIEnv env, int robj){
     ClassInfo ci = env.getReferredClassInfo( robj);
@@ -251,7 +250,9 @@ public class JPF_java_lang_Class extends NativePeer {
     ClassInfo pdci = cli.getResolvedClassInfo("java.security.ProtectionDomain");
 
     int proDomRef = MJIEnv.NULL;
-    /* TODO: Defer the following to future implementations
+    /*
+    TODO: Defer the following to future implementations
+    TODO: Currently Groovy runs well without actually instantiating a ProtectionDomain object properly
     int proDomRef = env.newObject(pdci);
     ElementInfo ei = env.getModifiableElementInfo(proDomRef);
     ei.setReferenceField("codesource", MJIEnv.NULL);
index 7533a9a..d5bfec4 100644 (file)
@@ -43,7 +43,6 @@ public class JPF_java_lang_Thread extends NativePeer {
                          int objRef, int groupRef, int runnableRef, int nameRef, long stackSize) {
     VM vm = env.getVM();
 
-    // TODO: Fix for Groovy's model-checking
     // we only need to create the ThreadInfo - its initialization will take care
     // of proper linkage to the java.lang.Thread object (objRef)
     vm.createThreadInfo( objRef, groupRef, runnableRef, nameRef);
index 123cbbb..3baa165 100644 (file)
@@ -319,7 +319,6 @@ public class JPF_java_lang_reflect_Method extends NativePeer {
     return retRef;
   }
   // TODO: Fix for Groovy's model-checking
-  // TODO: We have been able to only register the generic class and not yet the parameterized types
 
   int getExceptionTypes(MJIEnv env, MethodInfo mi) {
     ThreadInfo ti = env.getThreadInfo();
index 9493309..20fadf4 100644 (file)
@@ -33,6 +33,9 @@ import java.util.List;
  */
 public class JPF_java_util_ResourceBundle extends NativePeer {
 
+  /*
+  TODO: Fix for Groovy's model-checking
+  TODO: We comment this out to suppress warnings
   @MJI
   public int getClassContext_____3Ljava_lang_Class_2 (MJIEnv env, int clsRef){
     ThreadInfo ti = env.getThreadInfo();
@@ -49,5 +52,5 @@ public class JPF_java_util_ResourceBundle extends NativePeer {
     }
 
     return aRef;
-  }
+  }*/
 }