From: rtrimana <rtrimana@uci.edu>
Date: Fri, 28 Jun 2019 18:39:38 +0000 (-0700)
Subject: Finalizing the beta version of the implementation for Groovy extension in JPF: JPF...
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=8407476b0dce3b2c1d1a5093d55df109aa7f9789;p=jpf-core.git
Finalizing the beta version of the implementation for Groovy extension in JPF: JPF now runs Groovy-compiled bytecode.
---
diff --git a/examples/Empty.groovy b/examples/Empty.groovy
index 77aec71..b52e40d 100644
--- 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
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 53f483f..4d6ff32 100644
--- 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 7dd3947..97f8e90 100644
--- 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 658c063..2c98855 100644
--- 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 09650ab..66ddad5 100644
--- 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 c0edb79..313e8aa 100644
--- 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 20c59e8..ef0d782 100644
--- 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 7533a9a..d5bfec4 100644
--- 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 123cbbb..3baa165 100644
--- 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 9493309..20fadf4 100644
--- 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;
- }
+ }*/
}