Further excluding infrastructure/library field accesses.

diff --git a/src/main/gov/nasa/jpf/listener/StateReducer.java b/src/main/gov/nasa/jpf/listener/StateReducer.java
index 8aa2c381c636597093e286a53480af3045af30bb..0a4c6858935b0345ed314a7c81b833e86b394275 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/StateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/StateReducer.java
@@ -196,7 +196,7 @@ public class StateReducer extends ListenerAdapter {
         if (isResetAfterAnalysis && icsCG.getNextChoice() == -1) {
           int event = cgMap.get(icsCG);
           LinkedList<Integer[]> choiceLists = backtrackMap.get(event);
         if (isResetAfterAnalysis && icsCG.getNextChoice() == -1) {
           int event = cgMap.get(icsCG);
           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
             icsCG.setNewValues(choiceList);
             Integer[] choiceList = choiceLists.removeFirst();
             // Deploy the new choice list for this CG
             icsCG.setNewValues(choiceList);


@@ -301,6 +301,12 @@ public class StateReducer extends ListenerAdapter {
     int objectId = ((JVMFieldInstruction) executedInsn).getFieldInfo().getClassInfo().getClassObjectRef();
     // Record the field in the map
     if (executedInsn instanceof WriteInstruction) {
     int objectId = ((JVMFieldInstruction) executedInsn).getFieldInfo().getClassInfo().getClassObjectRef();
     // Record the field in the map
     if (executedInsn instanceof WriteInstruction) {

+      // Exclude certain field writes because of infrastructure needs, e.g., Event class field writes
+      for(String str : EXCLUDED_FIELDS_WRITE_INSTRUCTIONS_STARTS_WITH_LIST) {
+        if (fieldClass.startsWith(str)) {
+          return;
+        }
+      }

       rwSet.addWriteField(fieldClass, objectId);
     } else if (executedInsn instanceof ReadInstruction) {
       rwSet.addReadField(fieldClass, objectId);
       rwSet.addWriteField(fieldClass, objectId);
     } else if (executedInsn instanceof ReadInstruction) {
       rwSet.addReadField(fieldClass, objectId);


@@ -361,6 +367,42 @@ public class StateReducer extends ListenerAdapter {
     backtrackChoiceLists.addLast(choiceList);
   }
 
     backtrackChoiceLists.addLast(choiceList);
   }
 

+  // We exclude fields that come from libraries (Java and Groovy), and also the infrastructure
+  private final static String[] EXCLUDED_FIELDS_STARTS_WITH_LIST =
+          // Java and Groovy libraries
+          { "java", "org", "sun", "com", "gov", "groovy"};
+  private final static String[] EXCLUDED_FIELDS_ENDS_WITH_LIST =
+          // Groovy library created fields
+          {"stMC", "callSiteArray", "metaClass", "staticClassInfo", "__constructor__",
+          // Infrastructure
+          "sendEvent", "Object", "reference", "location", "app", "state", "log", "functionList", "objectList",
+          "eventList", "valueList", "settings", "printToConsole", "app1", "app2"};
+  private final static String[] EXCLUDED_FIELDS_CONTAINS_LIST = {"_closure"};
+  private final static String[] EXCLUDED_FIELDS_WRITE_INSTRUCTIONS_STARTS_WITH_LIST = {"Event"};
+
+  private boolean isFieldExcluded(String field) {
+    // Check against "starts-with" list
+    for(String str : EXCLUDED_FIELDS_STARTS_WITH_LIST) {
+      if (field.startsWith(str)) {
+        return true;
+      }
+    }
+    // Check against "ends-with" list
+    for(String str : EXCLUDED_FIELDS_ENDS_WITH_LIST) {
+      if (field.endsWith(str)) {
+        return true;
+      }
+    }
+    // Check against "contains" list
+    for(String str : EXCLUDED_FIELDS_CONTAINS_LIST) {
+      if (field.contains(str)) {
+        return true;
+      }
+    }
+
+    return false;
+  }
+

   @Override
   public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
     if (stateReductionMode) {
   @Override
   public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
     if (stateReductionMode) {


@@ -371,18 +413,7 @@ public class StateReducer extends ListenerAdapter {
           // Analyze only after being initialized
           String fieldClass = ((JVMFieldInstruction) executedInsn).getFieldInfo().getFullName();
           // We don't care about libraries
           // Analyze only after being initialized
           String fieldClass = ((JVMFieldInstruction) executedInsn).getFieldInfo().getFullName();
           // We don't care about libraries

-          if (!fieldClass.startsWith("java") &&
-              !fieldClass.startsWith("org") &&
-              !fieldClass.startsWith("sun") &&
-              !fieldClass.startsWith("com") &&
-              !fieldClass.startsWith("gov") &&
-              !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__")) {
+          if (!isFieldExcluded(fieldClass)) {

             analyzeReadWriteAccesses(executedInsn, fieldClass, currentChoice);
           }
         }
             analyzeReadWriteAccesses(executedInsn, fieldClass, currentChoice);
           }
         }


@@ -394,18 +425,7 @@ public class StateReducer extends ListenerAdapter {
           if (!mi.getName().equals("<init>")) {
             String fieldClass = ((JVMFieldInstruction) nextInsn).getFieldInfo().getFullName();
             // We don't care about libraries
           if (!mi.getName().equals("<init>")) {
             String fieldClass = ((JVMFieldInstruction) nextInsn).getFieldInfo().getFullName();
             // We don't care about libraries

-            if (!fieldClass.startsWith("java") &&
-                !fieldClass.startsWith("org") &&
-                !fieldClass.startsWith("sun") &&
-                !fieldClass.startsWith("com") &&
-                !fieldClass.startsWith("gov") &&
-                !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__")) {
+            if (!isFieldExcluded(fieldClass)) {

               // 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.
               // 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.