Completing POR implementation with complete recursions.

diff --git a/src/main/gov/nasa/jpf/listener/StateReducer.java b/src/main/gov/nasa/jpf/listener/StateReducer.java
index 0a4c6858935b0345ed314a7c81b833e86b394275..957940f082d6514823392d3a1a0dfe61da37c948 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/StateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/StateReducer.java
@@ -17,7 +17,6 @@
  */
 package gov.nasa.jpf.listener;
 
  */
 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;
 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
   Transition transition;
 
   // State reduction fields

+  private Integer[] choices;

   private int choiceCounter;
   private Integer choiceUpperBound;
   private boolean isInitialized;
   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;
   // 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);
 
   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) {
 
   private void initializeStateReduction() {
     if (stateReductionMode) {

+      choices = null;

       choiceCounter = 0;
       choiceUpperBound = 0;
       isInitialized = false;
       choiceCounter = 0;
       choiceUpperBound = 0;
       isInitialized = false;


@@ -93,6 +96,7 @@ public class StateReducer extends ListenerAdapter {
       readWriteFieldsMap = new HashMap<>();
       backtrackMap = new HashMap<>();
       conflictPairMap = new HashMap<>();
       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
       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
         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
           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'
           // 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.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
           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();
         // Deploy the new choice list for this CG
         cg.setNewValues(choiceList);
         cg.reset();

+      } else {
+        cg.setDone();

       }
     }
   }
 
   @Override
   public void choiceGeneratorAdvanced (VM vm, ChoiceGenerator<?> currentCG) {
       }
     }
   }
 
   @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) {
     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;
       // 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;
         }
         // 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
     // 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();
     } 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
     }
     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) {
 
 
   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
     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<>();
       backtrackChoiceLists = new LinkedList<>();

-      backtrackMap.put(minChoice, backtrackChoiceLists);
+      backtrackMap.put(conflictEventNumber, backtrackChoiceLists);

     } else {
     } 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
     // 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
   }
 
   // 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__",
   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"};
 
   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) {
   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) {
         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)) {
             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.
               // 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
                 // Skip if this event number does not have any Read/Write set

-                if (!readWriteFieldsMap.containsKey(eventNumber)) {
+                if (!readWriteFieldsMap.containsKey(choices[eventNumber])) {

                   continue;
                 }
                   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) &&
                 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)) {
                   // 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)) {