From 8407476b0dce3b2c1d1a5093d55df109aa7f9789 Mon Sep 17 00:00:00 2001 From: rtrimana Date: Fri, 28 Jun 2019 11:39:38 -0700 Subject: [PATCH] Finalizing the beta version of the implementation for Groovy extension in JPF: JPF now runs Groovy-compiled bytecode. --- examples/Empty.groovy | 2 +- examples/Racer.groovy | 24 +++++++++++++++++++ examples/Rand.groovy | 19 +++++++++------ src/classes/java/lang/Class.java | 20 ++++------------ src/classes/java/security/AllPermission.java | 1 + .../java/security/ProtectionDomain.java | 1 + src/main/gov/nasa/jpf/vm/Types.java | 2 -- .../gov/nasa/jpf/vm/JPF_java_lang_Class.java | 5 ++-- .../gov/nasa/jpf/vm/JPF_java_lang_Thread.java | 1 - .../jpf/vm/JPF_java_lang_reflect_Method.java | 1 - .../jpf/vm/JPF_java_util_ResourceBundle.java | 5 +++- 11 files changed, 51 insertions(+), 30 deletions(-) create mode 100644 examples/Racer.groovy 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 implements Serializable, GenericDeclaration, Type, A public native TypeVariable>[] 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 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 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 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; - } + }*/ } -- 2.34.1