Adding more restrictions in conflict analysis: not to analyze fields from the Groovy...

[jpf-core.git] / src / main / gov / nasa / jpf / listener / StateReducer.java

diff --git a/src/main/gov/nasa/jpf/listener/StateReducer.java b/src/main/gov/nasa/jpf/listener/StateReducer.java
index 82e8cf87560a5d211b05d024b07050697d75fa0f..ffeca2078d316eda1abcb806dde561fdc3d28ec5 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/StateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/StateReducer.java
@@ -162,7 +162,7 @@ public class StateReducer extends ListenerAdapter {
     for(IntChoiceFromSet cg : cgMap.keySet()) {
       int event = cgMap.get(cg);
       LinkedList<Integer[]> choiceLists = backtrackMap.get(event);
-      if (choiceLists.peekFirst() != null) {
+      if (choiceLists != null && choiceLists.peekFirst() != null) {
         Integer[] choiceList = choiceLists.removeFirst();
         // Deploy the new choice list for this CG
         cg.setNewValues(choiceList);
@@ -363,8 +363,17 @@ public class StateReducer extends ListenerAdapter {
             !fieldClass.startsWith("sun") &&
             !fieldClass.startsWith("com") &&
             !fieldClass.startsWith("gov") &&
-            !fieldClass.startsWith("groovy")) {
-          analyzeReadWriteAccesses(executedInsn, fieldClass);
+            !fieldClass.startsWith("groovy") &&
+            // and fields generated for the Groovy library
+            !fieldClass.endsWith("stMC") &&
+            !fieldClass.endsWith("callSiteArray") &&
+            !fieldClass.endsWith("metaClass") &&
+            !fieldClass.endsWith("staticClassInfo") &&
+            !fieldClass.endsWith("__constructor__")) {
+          // Analyze only after being initialized
+          if (isInitialized) {
+            analyzeReadWriteAccesses(executedInsn, fieldClass);
+          }
         }
       }
       // Analyze conflicts from next instructions
@@ -376,7 +385,13 @@ public class StateReducer extends ListenerAdapter {
             !fieldClass.startsWith("sun") &&
             !fieldClass.startsWith("com") &&
             !fieldClass.startsWith("gov") &&
-            !fieldClass.startsWith("groovy")) {
+            !fieldClass.startsWith("groovy") &&
+            // and fields generated for the Groovy library
+            !fieldClass.endsWith("stMC") &&
+            !fieldClass.endsWith("callSiteArray") &&
+            !fieldClass.endsWith("metaClass") &&
+            !fieldClass.endsWith("staticClassInfo") &&
+            !fieldClass.endsWith("__constructor__")) {
           // Check for conflict (go backward from currentChoice and get the first conflict)
           // If the current event has conflicts with multiple events, then these will be detected
           // one by one as this recursively checks backward when backtrack set is revisited and executed.
@@ -389,8 +404,8 @@ public class StateReducer extends ListenerAdapter {
             // 1) Check for conflicts with Write fields for both Read and Write instructions
             // 2) Check for conflicts with Read fields for Write instructions
             if (((nextInsn instanceof WriteInstruction || nextInsn instanceof ReadInstruction) &&
-                    rwSet.writeFieldExists(fieldClass)) ||
-                    (nextInsn instanceof WriteInstruction && rwSet.readFieldExists(fieldClass)))   {
+                  rwSet.writeFieldExists(fieldClass)) ||
+                 (nextInsn instanceof WriteInstruction && rwSet.readFieldExists(fieldClass)))   {
               // We do not record and service the same backtrack pair/point twice!
               // If it has been serviced before, we just skip this
               if (recordConflictPair(choiceCounter, eventNumber)) {