Finalizing the beta version of the implementation for Groovy extension in JPF: JPF...

diff --git a/examples/Empty.groovy b/examples/Empty.groovy
index 77aec71547e62db4a099b963f6992145d4dd9926..b52e40db5e6f05549fdb65964ef6d74a2cf0029e 100644 (file)
--- a/examples/Empty.groovy
+++ b/examples/Empty.groovy
@@ -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
+++ b/examples/Racer.groovy
@@ -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) {}
+     }
+}

diff --git a/examples/Rand.groovy b/examples/Rand.groovy
index 53f483f4fe1f04b2b8d0fa7b889870507a93023d..4d6ff322829afbdd856963a698e2b22b463ac2d4 100644 (file)
--- a/examples/Rand.groovy
+++ b/examples/Rand.groovy
@@ -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)
+       }
 }
 

diff --git a/src/classes/java/lang/Class.java b/src/classes/java/lang/Class.java
index 7dd3947aae23630b8d3246a4ff35c849ed0df759..97f8e90e3ba0f68e40c6b059bc76ebbc2da03037 100644 (file)
--- a/src/classes/java/lang/Class.java
+++ b/src/classes/java/lang/Class.java
@@ -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;

diff --git a/src/classes/java/security/AllPermission.java b/src/classes/java/security/AllPermission.java
index 658c063b10b70ad69c5b338cf8d0de1c073e9d07..2c9885597f96fdd85f575e85ba1530d0b0a5b2f9 100644 (file)
--- a/src/classes/java/security/AllPermission.java
+++ b/src/classes/java/security/AllPermission.java
@@ -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
  */

diff --git a/src/classes/java/security/ProtectionDomain.java b/src/classes/java/security/ProtectionDomain.java
index 09650ab3a201ed4ff1db4e43c305e28850ef28d9..66ddad5b1c944205f174d0e0d86e0eeba373fcf6 100644 (file)
--- a/src/classes/java/security/ProtectionDomain.java
+++ b/src/classes/java/security/ProtectionDomain.java
@@ -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
  */

diff --git a/src/main/gov/nasa/jpf/vm/Types.java b/src/main/gov/nasa/jpf/vm/Types.java
index c0edb793f6b50be7e2425f34571dda6231862d6b..313e8aab7d0fb0f01027262c8ea64abc1ea0fe91 100644 (file)
--- a/src/main/gov/nasa/jpf/vm/Types.java
+++ b/src/main/gov/nasa/jpf/vm/Types.java
@@ -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;

diff --git a/src/peers/gov/nasa/jpf/vm/JPF_java_lang_Class.java b/src/peers/gov/nasa/jpf/vm/JPF_java_lang_Class.java
index 20c59e8c4b50488058315a6802d180f1c96f3fb3..ef0d782b998fb735dfa40828b1ed1c98600ace24 100644 (file)
--- a/src/peers/gov/nasa/jpf/vm/JPF_java_lang_Class.java
+++ b/src/peers/gov/nasa/jpf/vm/JPF_java_lang_Class.java
@@ -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);

diff --git a/src/peers/gov/nasa/jpf/vm/JPF_java_lang_Thread.java b/src/peers/gov/nasa/jpf/vm/JPF_java_lang_Thread.java
index 7533a9aa6d2fcb3e25cce24800e8f6bff16dd6d4..d5bfec4f1cd234031802692f9148721b8660a0b2 100644 (file)
--- a/src/peers/gov/nasa/jpf/vm/JPF_java_lang_Thread.java
+++ b/src/peers/gov/nasa/jpf/vm/JPF_java_lang_Thread.java
@@ -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);

diff --git a/src/peers/gov/nasa/jpf/vm/JPF_java_lang_reflect_Method.java b/src/peers/gov/nasa/jpf/vm/JPF_java_lang_reflect_Method.java
index 123cbbb16364d5b5ad96d41702ebe989d22f33dd..3baa1651b31a3fdbdaa777a8fa0e16d723e9f10a 100644 (file)
--- a/src/peers/gov/nasa/jpf/vm/JPF_java_lang_reflect_Method.java
+++ b/src/peers/gov/nasa/jpf/vm/JPF_java_lang_reflect_Method.java
@@ -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();

diff --git a/src/peers/gov/nasa/jpf/vm/JPF_java_util_ResourceBundle.java b/src/peers/gov/nasa/jpf/vm/JPF_java_util_ResourceBundle.java
index 9493309e5ed9e7d650736673b5b6f9016012f9d2..20fadf499d753d5ac1dbde567a16ad3ffc256d24 100644 (file)
--- a/src/peers/gov/nasa/jpf/vm/JPF_java_util_ResourceBundle.java
+++ b/src/peers/gov/nasa/jpf/vm/JPF_java_util_ResourceBundle.java
@@ -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;
-  }
+  }*/
 }