Completing POR implementation with complete recursions.
[jpf-core.git] / src / main / gov / nasa / jpf / listener / StateReducer.java
index 0a4c685..957940f 100644 (file)
@@ -17,7 +17,6 @@
  */
 package gov.nasa.jpf.listener;
 
-import com.sun.org.apache.xpath.internal.operations.Bool;
 import gov.nasa.jpf.Config;
 import gov.nasa.jpf.JPF;
 import gov.nasa.jpf.ListenerAdapter;
@@ -54,6 +53,7 @@ public class StateReducer extends ListenerAdapter {
   Transition transition;
 
   // State reduction fields
+  private Integer[] choices;
   private int choiceCounter;
   private Integer choiceUpperBound;
   private boolean isInitialized;
@@ -66,6 +66,8 @@ public class StateReducer extends ListenerAdapter {
   // e.g., event number 1 can have two backtrack sequences: {3,1,2,4,...} and {2,1,3,4,...}
   private HashMap<Integer,LinkedList<Integer[]>> backtrackMap;
   private HashMap<Integer,HashSet<Integer>> conflictPairMap;
+  // Map choicelist with start index
+  private HashMap<Integer[],Integer> choiceListStartIndexMap;
 
   public StateReducer (Config config, JPF jpf) {
     debugMode = config.getBoolean("debug_state_transition", false);
@@ -85,6 +87,7 @@ public class StateReducer extends ListenerAdapter {
 
   private void initializeStateReduction() {
     if (stateReductionMode) {
+      choices = null;
       choiceCounter = 0;
       choiceUpperBound = 0;
       isInitialized = false;
@@ -93,6 +96,7 @@ public class StateReducer extends ListenerAdapter {
       readWriteFieldsMap = new HashMap<>();
       backtrackMap = new HashMap<>();
       conflictPairMap = new HashMap<>();
+      choiceListStartIndexMap = new HashMap<>();
     }
   }
 
@@ -123,24 +127,27 @@ public class StateReducer extends ListenerAdapter {
       if (nextCG instanceof IntChoiceFromSet) {
         IntChoiceFromSet icsCG = (IntChoiceFromSet) nextCG;
         // Check if CG has been initialized, otherwise initialize it
-        Object[] choices = icsCG.getAllChoices();
+        Integer[] cgChoices = icsCG.getAllChoices();
         if (!isInitialized) {
           // Get the upper bound from the last element of the choices
-          choiceUpperBound = (Integer) choices[choices.length - 1];
+          choiceUpperBound = (Integer) cgChoices[cgChoices.length - 1];
           isInitialized = true;
         }
         // Record the subsequent Integer CGs only until we hit the upper bound
-        if (choiceCounter <= choiceUpperBound && !cgMap.containsValue(choiceCounter)) {
+        if (!isResetAfterAnalysis && choiceCounter <= choiceUpperBound && !cgMap.containsValue(choiceCounter)) {
           // Update the choices of the first CG and add '-1'
-          Integer[] newChoices = new Integer[choices.length + 1];
-          System.arraycopy(choices, 0, newChoices, 0, choices.length);
-          newChoices[newChoices.length - 1] = -1;
-          icsCG.setNewValues(newChoices);
+          if (choices == null) {
+            // All the choices are always the same so we only need to update it once
+            choices = new Integer[cgChoices.length + 1];
+            System.arraycopy(cgChoices, 0, choices, 0, cgChoices.length);
+            choices[choices.length - 1] = -1;
+          }
+          icsCG.setNewValues(choices);
           icsCG.reset();
           // Advance the current Integer CG
           // This way we explore all the event numbers in the first pass
-          icsCG.advance(choiceCounter);
-          cgMap.put(icsCG, choiceCounter);
+          icsCG.advance(choices[choiceCounter]);
+          cgMap.put(icsCG, choices[choiceCounter]);
           choiceCounter++;
         } else {
           // Set done the subsequent CGs
@@ -167,13 +174,15 @@ public class StateReducer extends ListenerAdapter {
         // Deploy the new choice list for this CG
         cg.setNewValues(choiceList);
         cg.reset();
+      } else {
+        cg.setDone();
       }
     }
   }
 
   @Override
   public void choiceGeneratorAdvanced (VM vm, ChoiceGenerator<?> currentCG) {
-               
+
     if(stateReductionMode) {
       // Check the boolean CG and if it is flipped, we are resetting the analysis
       if (currentCG instanceof BooleanChoiceGenerator) {
@@ -187,25 +196,39 @@ public class StateReducer extends ListenerAdapter {
       // are chosen first before repeating the same choice of value twice!
       if (currentCG instanceof IntChoiceFromSet) {
         IntChoiceFromSet icsCG = (IntChoiceFromSet) currentCG;
+        // Update the current pointer to the current set of choices
+        if (choices == null || choices != icsCG.getAllChoices()) {
+          choiceListStartIndexMap.remove(choices);
+          choices = icsCG.getAllChoices();
+          // Reset a few things for the sub-graph
+          conflictPairMap = new HashMap<>();
+          readWriteFieldsMap = new HashMap<>();
+          choiceCounter = 0;
+        }
+        // Traverse the sub-graphs
+        if (isResetAfterAnalysis) {
+          // Advance choice counter for sub-graphs
+          choiceCounter++;
+          // Do this for every CG after finishing each backtrack list
+          if (icsCG.getNextChoice() == -1) {
+            int event = cgMap.get(icsCG);
+            LinkedList<Integer[]> choiceLists = backtrackMap.get(event);
+            if (choiceLists != null && choiceLists.peekFirst() != null) {
+              Integer[] choiceList = choiceLists.removeFirst();
+              // Deploy the new choice list for this CG
+              icsCG.setNewValues(choiceList);
+              icsCG.reset();
+            } else {
+              // Set done if this was the last backtrack list
+              icsCG.setDone();
+            }
+          }
+        }
         // Update and reset the CG if needed (do this for the first time after the analysis)
         if (!isResetAfterAnalysis && icsCG.getNextChoice() == -1) {
           resetAllCGs();
           isResetAfterAnalysis = true;
         }
-        // Do this for every CG after finishing each backtrack list
-        if (isResetAfterAnalysis && icsCG.getNextChoice() == -1) {
-          int event = cgMap.get(icsCG);
-          LinkedList<Integer[]> choiceLists = backtrackMap.get(event);
-          if (choiceLists != null && choiceLists.peekFirst() != null) {
-            Integer[] choiceList = choiceLists.removeFirst();
-            // Deploy the new choice list for this CG
-            icsCG.setNewValues(choiceList);
-            icsCG.reset();
-          } else {
-            // Set done if this was the last backtrack list
-            icsCG.setDone();
-          }
-        }
       }
     }
   }
@@ -292,11 +315,11 @@ public class StateReducer extends ListenerAdapter {
     // Do the analysis to get Read and Write accesses to fields
     ReadWriteSet rwSet;
     // We already have an entry
-    if (readWriteFieldsMap.containsKey(currentChoice)) {
-      rwSet = readWriteFieldsMap.get(currentChoice);
+    if (readWriteFieldsMap.containsKey(choices[currentChoice])) {
+      rwSet = readWriteFieldsMap.get(choices[currentChoice]);
     } else { // We need to create a new entry
       rwSet = new ReadWriteSet();
-      readWriteFieldsMap.put(currentChoice, rwSet);
+      readWriteFieldsMap.put(choices[currentChoice], rwSet);
     }
     int objectId = ((JVMFieldInstruction) executedInsn).getFieldInfo().getClassInfo().getClassObjectRef();
     // Record the field in the map
@@ -333,38 +356,61 @@ public class StateReducer extends ListenerAdapter {
 
   private void createBacktrackChoiceList(int currentChoice, int conflictEventNumber) {
 
-    int minChoice = Math.min(currentChoice, conflictEventNumber);
-    int maxChoice = Math.max(currentChoice, conflictEventNumber);
     LinkedList<Integer[]> backtrackChoiceLists;
     // Check if we have a list for this choice number
     // If not we create a new one for it
-    if (!backtrackMap.containsKey(minChoice)) {
+    if (!backtrackMap.containsKey(conflictEventNumber)) {
       backtrackChoiceLists = new LinkedList<>();
-      backtrackMap.put(minChoice, backtrackChoiceLists);
+      backtrackMap.put(conflictEventNumber, backtrackChoiceLists);
     } else {
-      backtrackChoiceLists = backtrackMap.get(minChoice);
+      backtrackChoiceLists = backtrackMap.get(conflictEventNumber);
     }
-    // TODO: The following might change depending on the POR implementation detail
     // Create a new list of choices for backtrack based on the current choice and conflicting event number
     // If we have a conflict between 1 and 3, then we create the list {3, 1, 2, 4, 5} for backtrack
     // The backtrack point is the CG for event number 1 and the list length is one less than the original list
     // (originally of length 6) since we don't start from event number 0
-    int maxListLength = choiceUpperBound + 1;
-    int listLength = maxListLength - minChoice;
-    Integer[] choiceList = new Integer[listLength+1];
-    // Put the conflicting event numbers first and reverse the order
-    choiceList[0] = maxChoice;
-    choiceList[1] = minChoice;
-    // Put the rest of the event numbers into the array starting from the minimum to the upper bound
-    for(int i = minChoice + 1, j = 2; j < listLength; i++) {
-      if (i != maxChoice) {
-        choiceList[j] = i;
-        j++;
+    if (!isResetAfterAnalysis) {
+      int maxListLength = choiceUpperBound + 1;
+      int listLength = maxListLength - conflictEventNumber;
+      Integer[] newChoiceList = new Integer[listLength + 1];
+      // Put the conflicting event numbers first and reverse the order
+      newChoiceList[0] = choices[currentChoice];
+      newChoiceList[1] = choices[conflictEventNumber];
+      // Put the rest of the event numbers into the array starting from the minimum to the upper bound
+      for (int i = conflictEventNumber + 1, j = 2; j < listLength; i++) {
+        if (choices[i] != choices[currentChoice]) {
+          newChoiceList[j] = choices[i];
+          j++;
+        }
+      }
+      // Set the last element to '-1' as the end of the sequence
+      newChoiceList[newChoiceList.length - 1] = -1;
+      backtrackChoiceLists.addLast(newChoiceList);
+      // The start index for the recursion is always 1 (from the main branch)
+      choiceListStartIndexMap.put(newChoiceList, 1);
+    } else { // This is a sub-graph
+      int listLength = choices.length;
+      Integer[] newChoiceList = new Integer[listLength];
+      // Copy everything before the conflict number
+      for(int i = 0; i < conflictEventNumber; i++) {
+        newChoiceList[i] = choices[i];
       }
+      // Put the conflicting events
+      newChoiceList[conflictEventNumber] = choices[currentChoice];
+      newChoiceList[conflictEventNumber + 1] = choices[conflictEventNumber];
+      // Copy the rest
+      for(int i = conflictEventNumber + 1, j = conflictEventNumber + 2; j < listLength - 1; i++) {
+        if (choices[i] != choices[currentChoice]) {
+          newChoiceList[j] = choices[i];
+          j++;
+        }
+      }
+      // Set the last element to '-1' as the end of the sequence
+      newChoiceList[newChoiceList.length - 1] = -1;
+      backtrackChoiceLists.addLast(newChoiceList);
+      // For the sub-graph the start index depends on the conflicting event number
+      choiceListStartIndexMap.put(newChoiceList, conflictEventNumber + 1);
     }
-    // Set the last element to '-1' as the end of the sequence
-    choiceList[choiceList.length - 1] = -1;
-    backtrackChoiceLists.addLast(choiceList);
   }
 
   // We exclude fields that come from libraries (Java and Groovy), and also the infrastructure
@@ -374,9 +420,9 @@ public class StateReducer extends ListenerAdapter {
   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"};
+                  // 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"};
 
@@ -407,6 +453,10 @@ public class StateReducer extends ListenerAdapter {
   public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
     if (stateReductionMode) {
       if (isInitialized) {
+        if (choiceCounter > choices.length - 1) {
+          // We do not compute the conflicts for the choice '-1'
+          return;
+        }
         int currentChoice = choiceCounter - 1;
         // Record accesses from executed instructions
         if (executedInsn instanceof JVMFieldInstruction) {
@@ -426,21 +476,24 @@ public class StateReducer extends ListenerAdapter {
             String fieldClass = ((JVMFieldInstruction) nextInsn).getFieldInfo().getFullName();
             // We don't care about libraries
             if (!isFieldExcluded(fieldClass)) {
+              // For the main graph we go down to 0, but for subgraph, we only go down to 1 since 0 contains
+              // the reversed event
+              int end = !isResetAfterAnalysis ? 0 : choiceListStartIndexMap.get(choices);
               // 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.
-              for (int eventNumber = currentChoice - 1; eventNumber >= 0; eventNumber--) {
+              for (int eventNumber = currentChoice - 1; eventNumber >= end; eventNumber--) {
                 // Skip if this event number does not have any Read/Write set
-                if (!readWriteFieldsMap.containsKey(eventNumber)) {
+                if (!readWriteFieldsMap.containsKey(choices[eventNumber])) {
                   continue;
                 }
-                ReadWriteSet rwSet = readWriteFieldsMap.get(eventNumber);
+                ReadWriteSet rwSet = readWriteFieldsMap.get(choices[eventNumber]);
                 int currObjId = ((JVMFieldInstruction) nextInsn).getFieldInfo().getClassInfo().getClassObjectRef();
                 // 1) Check for conflicts with Write fields for both Read and Write instructions
                 if (((nextInsn instanceof WriteInstruction || nextInsn instanceof ReadInstruction) &&
-                      rwSet.writeFieldExists(fieldClass) && rwSet.writeFieldObjectId(fieldClass) == currObjId) ||
-                     (nextInsn instanceof WriteInstruction && rwSet.readFieldExists(fieldClass) &&
-                      rwSet.readFieldObjectId(fieldClass) == currObjId)) {
+                        rwSet.writeFieldExists(fieldClass) && rwSet.writeFieldObjectId(fieldClass) == currObjId) ||
+                        (nextInsn instanceof WriteInstruction && rwSet.readFieldExists(fieldClass) &&
+                                rwSet.readFieldObjectId(fieldClass) == currObjId)) {
                   // We do not record and service the same backtrack pair/point twice!
                   // If it has been serviced before, we just skip this
                   if (recordConflictPair(currentChoice, eventNumber)) {