Fixing a bug: need to get the right choice/event number for IntIntervalGenerator...

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index f4b5923..bc42a46 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@ -80,7 +80,6 @@ public class DPORStateReducer extends ListenerAdapter {
   private HashSet<String> doneBacktrackSet;                       // Record state ID and trace already constructed
   private HashMap<Integer, RestorableVMState> restorableStateMap; // Maps state IDs to the restorable state object
   private HashMap<Integer, Integer> stateToChoiceCounterMap;      // Maps state IDs to the choice counter
   private HashSet<String> doneBacktrackSet;                       // Record state ID and trace already constructed
   private HashMap<Integer, RestorableVMState> restorableStateMap; // Maps state IDs to the restorable state object
   private HashMap<Integer, Integer> stateToChoiceCounterMap;      // Maps state IDs to the choice counter

-  //private HashMap<Integer, ArrayList<ReachableTrace>> rGraph;     // Create a reachability graph

   private HashMap<Integer, ArrayList<Execution>> rGraph;          // Create a reachability graph for past executions
 
   // Boolean states
   private HashMap<Integer, ArrayList<Execution>> rGraph;          // Create a reachability graph for past executions
 
   // Boolean states


@@ -357,12 +356,14 @@ public class DPORStateReducer extends ListenerAdapter {
 
   // This class stores a representation of the execution graph node
   private class Execution {
 
   // This class stores a representation of the execution graph node
   private class Execution {

-    private ArrayList<BacktrackPoint> executionTrace;            // The BacktrackPoint objects of this execution
+    private HashMap<IntChoiceFromSet, Integer> cgToChoiceMap;   // Map between CG to choice numbers for O(1) access
+    private ArrayList<BacktrackPoint> executionTrace;           // The BacktrackPoint objects of this execution

     private int parentChoice;                                   // The parent's choice that leads to this execution
     private Execution parent;                                   // Store the parent for backward DFS to find conflicts
     private HashMap<Integer, ReadWriteSet> readWriteFieldsMap;  // Record fields that are accessed
 
     public Execution() {
     private int parentChoice;                                   // The parent's choice that leads to this execution
     private Execution parent;                                   // Store the parent for backward DFS to find conflicts
     private HashMap<Integer, ReadWriteSet> readWriteFieldsMap;  // Record fields that are accessed
 
     public Execution() {

+      cgToChoiceMap = new HashMap<>();

       executionTrace = new ArrayList<>();
       parentChoice = -1;
       parent = null;
       executionTrace = new ArrayList<>();
       parentChoice = -1;
       parent = null;


@@ -373,10 +374,18 @@ public class DPORStateReducer extends ListenerAdapter {
       executionTrace.add(newBacktrackPoint);
     }
 
       executionTrace.add(newBacktrackPoint);
     }
 

+    public void clearCGToChoiceMap() {
+      cgToChoiceMap = null;
+    }
+

     public ArrayList<BacktrackPoint> getExecutionTrace() {
       return executionTrace;
     }
 
     public ArrayList<BacktrackPoint> getExecutionTrace() {
       return executionTrace;
     }
 

+    public int getChoiceFromCG(IntChoiceFromSet icsCG) {
+      return cgToChoiceMap.get(icsCG);
+    }
+

     public int getParentChoice() {
       return parentChoice;
     }
     public int getParentChoice() {
       return parentChoice;
     }


@@ -389,6 +398,10 @@ public class DPORStateReducer extends ListenerAdapter {
       return readWriteFieldsMap;
     }
 
       return readWriteFieldsMap;
     }
 

+    public void mapCGToChoice(IntChoiceFromSet icsCG, int choice) {
+      cgToChoiceMap.put(icsCG, choice);
+    }
+

     public void setParentChoice(int parChoice) {
       parentChoice = parChoice;
     }
     public void setParentChoice(int parChoice) {
       parentChoice = parChoice;
     }


@@ -443,26 +456,6 @@ public class DPORStateReducer extends ListenerAdapter {
     }
   }
 
     }
   }
 

-  // This class stores a compact representation of a reachability graph for past executions
-//  private class ReachableTrace {
-//    private ArrayList<BacktrackPoint> pastBacktrackPointList;
-//    private HashMap<Integer, ReadWriteSet> pastReadWriteFieldsMap;
-//
-//    public ReachableTrace(ArrayList<BacktrackPoint> btrackPointList,
-//                             HashMap<Integer, ReadWriteSet> rwFieldsMap) {
-//      pastBacktrackPointList = btrackPointList;
-//      pastReadWriteFieldsMap = rwFieldsMap;
-//    }
-//
-//    public ArrayList<BacktrackPoint> getPastBacktrackPointList() {
-//      return pastBacktrackPointList;
-//    }
-//
-//    public HashMap<Integer, ReadWriteSet> getPastReadWriteFieldsMap() {
-//      return pastReadWriteFieldsMap;
-//    }
-//  }
-

   // -- CONSTANTS
   private final static String DO_CALL_METHOD = "doCall";
   // We exclude fields that come from libraries (Java and Groovy), and also the infrastructure
   // -- CONSTANTS
   private final static String DO_CALL_METHOD = "doCall";
   // We exclude fields that come from libraries (Java and Groovy), and also the infrastructure


@@ -498,6 +491,7 @@ public class DPORStateReducer extends ListenerAdapter {
     // Record state ID and choice/event as backtrack point
     int stateId = vm.getStateId();
     currentExecution.addBacktrackPoint(new BacktrackPoint(icsCG, stateId, refChoices[choiceIndex]));
     // Record state ID and choice/event as backtrack point
     int stateId = vm.getStateId();
     currentExecution.addBacktrackPoint(new BacktrackPoint(icsCG, stateId, refChoices[choiceIndex]));

+    currentExecution.mapCGToChoice(icsCG, choiceCounter);

     // Store restorable state object for this state (always store the latest)
     RestorableVMState restorableState = vm.getRestorableState();
     restorableStateMap.put(stateId, restorableState);
     // Store restorable state object for this state (always store the latest)
     RestorableVMState restorableState = vm.getRestorableState();
     restorableStateMap.put(stateId, restorableState);


@@ -696,8 +690,6 @@ public class DPORStateReducer extends ListenerAdapter {
   private int checkAndAdjustChoice(int currentChoice, VM vm) {
     // If current choice is not the same, then this is caused by the firing of IntIntervalGenerator
     // for certain method calls in the infrastructure, e.g., eventSince()
   private int checkAndAdjustChoice(int currentChoice, VM vm) {
     // If current choice is not the same, then this is caused by the firing of IntIntervalGenerator
     // for certain method calls in the infrastructure, e.g., eventSince()

-    int currChoiceInd = currentChoice % refChoices.length;
-    int currChoiceFromCG = currChoiceInd;

     ChoiceGenerator<?> currentCG = vm.getChoiceGenerator();
     // This is the main event CG
     if (currentCG instanceof IntIntervalGenerator) {
     ChoiceGenerator<?> currentCG = vm.getChoiceGenerator();
     // This is the main event CG
     if (currentCG instanceof IntIntervalGenerator) {


@@ -707,17 +699,8 @@ public class DPORStateReducer extends ListenerAdapter {
       while (!(parentCG instanceof IntChoiceFromSet)) {
         parentCG = ((IntIntervalGenerator) parentCG).getPreviousChoiceGenerator();
       }
       while (!(parentCG instanceof IntChoiceFromSet)) {
         parentCG = ((IntIntervalGenerator) parentCG).getPreviousChoiceGenerator();
       }

-      int actualEvtNum = ((IntChoiceFromSet) parentCG).getNextChoice();
-      // Find the index of the event/choice in refChoices
-      for (int i = 0; i<refChoices.length; i++) {
-        if (actualEvtNum == refChoices[i]) {
-          currChoiceFromCG = i;
-          break;
-        }
-      }
-    }
-    if (currChoiceInd != currChoiceFromCG) {
-      currentChoice = (currentChoice - currChoiceInd) + currChoiceFromCG;
+      // Find the choice related to the IntIntervalGenerator CG from the map
+      currentChoice = currentExecution.getChoiceFromCG((IntChoiceFromSet) parentCG);

     }
     return currentChoice;
   }
     }
     return currentChoice;
   }


@@ -810,8 +793,6 @@ public class DPORStateReducer extends ListenerAdapter {
   private void findFirstConflictAndCreateBacktrackPoint(int currentChoice, Instruction nextInsn, String fieldClass) {
     // Check for conflict (go backward from current choice and get the first conflict)
     Execution execution = currentExecution;
   private void findFirstConflictAndCreateBacktrackPoint(int currentChoice, Instruction nextInsn, String fieldClass) {
     // Check for conflict (go backward from current choice and get the first conflict)
     Execution execution = currentExecution;

-    // Actual choice of the current execution trace
-    //int actualChoice = currentChoice % refChoices.length;

     // Choice/event we want to check for conflict against (start from actual choice)
     int pastChoice = currentChoice;
     // Perform backward DFS through the execution graph
     // Choice/event we want to check for conflict against (start from actual choice)
     int pastChoice = currentChoice;
     // Perform backward DFS through the execution graph


@@ -848,7 +829,6 @@ public class DPORStateReducer extends ListenerAdapter {
     ArrayList<BacktrackPoint> currTrace = currentExecution.getExecutionTrace();
     // Skip if this event does not have any Read/Write set or the two events are basically the same event (number)
     if (!pastRWFieldsMap.containsKey(pastChoice) ||
     ArrayList<BacktrackPoint> currTrace = currentExecution.getExecutionTrace();
     // Skip if this event does not have any Read/Write set or the two events are basically the same event (number)
     if (!pastRWFieldsMap.containsKey(pastChoice) ||

-            //choices[actualChoice] == pastTrace.get(pastChoice).getChoice()) {

             currTrace.get(currentChoice).getChoice() == pastTrace.get(pastChoice).getChoice()) {
       return false;
     }
             currTrace.get(currentChoice).getChoice() == pastTrace.get(pastChoice).getChoice()) {
       return false;
     }


@@ -924,6 +904,7 @@ public class DPORStateReducer extends ListenerAdapter {
     return false;
   }
 
     return false;
   }
 

+  // Check if this trace is already constructed

   private boolean isTraceAlreadyConstructed(int firstChoice, int stateId) {
     // Concatenate state ID and only the first event in the string, e.g., "1:1 for the trace 10234 at state 1"
     // TODO: THIS IS AN OPTIMIZATION!
   private boolean isTraceAlreadyConstructed(int firstChoice, int stateId) {
     // Concatenate state ID and only the first event in the string, e.g., "1:1 for the trace 10234 at state 1"
     // TODO: THIS IS AN OPTIMIZATION!


@@ -942,6 +923,7 @@ public class DPORStateReducer extends ListenerAdapter {
     return false;
   }
 
     return false;
   }
 

+  // Reset data structure for each new execution

   private void resetStatesForNewExecution(IntChoiceFromSet icsCG, VM vm) {
     if (choices == null || choices != icsCG.getAllChoices()) {
       // Reset state variables
   private void resetStatesForNewExecution(IntChoiceFromSet icsCG, VM vm) {
     if (choices == null || choices != icsCG.getAllChoices()) {
       // Reset state variables


@@ -956,6 +938,7 @@ public class DPORStateReducer extends ListenerAdapter {
     }
   }
 
     }
   }
 

+  // Set a backtrack point for a particular state

   private void setBacktrackCG(int stateId, IntChoiceFromSet backtrackCG) {
     // Set a backtrack CG based on a state ID
     LinkedList<BacktrackExecution> backtrackExecutions = backtrackMap.get(stateId);
   private void setBacktrackCG(int stateId, IntChoiceFromSet backtrackCG) {
     // Set a backtrack CG based on a state ID
     LinkedList<BacktrackExecution> backtrackExecutions = backtrackMap.get(stateId);


@@ -970,6 +953,8 @@ public class DPORStateReducer extends ListenerAdapter {
       ArrayList<BacktrackPoint> parentTrace = newExecution.getParent().getExecutionTrace();
       newExecution.setParentChoice(parentTrace.size() - 1);
     }
       ArrayList<BacktrackPoint> parentTrace = newExecution.getParent().getExecutionTrace();
       newExecution.setParentChoice(parentTrace.size() - 1);
     }

+    // Try to free some memory since this map is only used for the current execution
+    currentExecution.clearCGToChoiceMap();

     currentExecution = newExecution;
     // Remove from the queue if we don't have more backtrack points for that state
     if (backtrackExecutions.isEmpty()) {
     currentExecution = newExecution;
     // Remove from the queue if we don't have more backtrack points for that state
     if (backtrackExecutions.isEmpty()) {


@@ -982,7 +967,7 @@ public class DPORStateReducer extends ListenerAdapter {
 
   // TODO: OPTIMIZATION!
   // Check and make sure that state ID and choice haven't been explored for this trace
 
   // TODO: OPTIMIZATION!
   // Check and make sure that state ID and choice haven't been explored for this trace

-  private boolean alreadyChecked(HashSet<String> checkedStateIdAndChoice, BacktrackPoint backtrackPoint) {
+  private boolean isAlreadyChecked(HashSet<String> checkedStateIdAndChoice, BacktrackPoint backtrackPoint) {

     int stateId = backtrackPoint.getStateId();
     int choice = backtrackPoint.getChoice();
     StringBuilder sb = new StringBuilder();
     int stateId = backtrackPoint.getStateId();
     int choice = backtrackPoint.getChoice();
     StringBuilder sb = new StringBuilder();


@@ -1064,6 +1049,7 @@ public class DPORStateReducer extends ListenerAdapter {
     }
   }
 
     }
   }
 

+  // Update the backtrack sets in a previous execution

   private void updateBacktrackSetsInPreviousExecution(Execution rExecution, int stateId,
                                                       HashSet<String> checkedStateIdAndChoice) {
     // Find the choice/event that marks the start of the subtrace from the previous execution
   private void updateBacktrackSetsInPreviousExecution(Execution rExecution, int stateId,
                                                       HashSet<String> checkedStateIdAndChoice) {
     // Find the choice/event that marks the start of the subtrace from the previous execution


@@ -1075,7 +1061,7 @@ public class DPORStateReducer extends ListenerAdapter {
     while (pastConfChoice < pastExecutionTrace.size() - 1) {  // BacktrackPoint list always has a surplus of 1
       // Get the info of the event from the past execution trace
       BacktrackPoint confBtrackPoint = pastExecutionTrace.get(pastConfChoice);
     while (pastConfChoice < pastExecutionTrace.size() - 1) {  // BacktrackPoint list always has a surplus of 1
       // Get the info of the event from the past execution trace
       BacktrackPoint confBtrackPoint = pastExecutionTrace.get(pastConfChoice);

-      if (!alreadyChecked(checkedStateIdAndChoice, confBtrackPoint)) {
+      if (!isAlreadyChecked(checkedStateIdAndChoice, confBtrackPoint)) {

         ReadWriteSet rwSet = pastReadWriteFieldsMap.get(pastConfChoice);
         // Append this event to the current list and map
         ArrayList<BacktrackPoint> currentTrace = currentExecution.getExecutionTrace();
         ReadWriteSet rwSet = pastReadWriteFieldsMap.get(pastConfChoice);
         // Append this event to the current list and map
         ArrayList<BacktrackPoint> currentTrace = currentExecution.getExecutionTrace();


@@ -1095,7 +1081,7 @@ public class DPORStateReducer extends ListenerAdapter {
     }
   }
 
     }
   }
 

-  // Update the backtrack sets in a previous execution
+  // Update the backtrack sets in previous executions

   private void updateBacktrackSetsInPreviousExecutions(int stateId) {
     // Don't check a past trace twice!
     HashSet<Execution> checkedTrace = new HashSet<>();
   private void updateBacktrackSetsInPreviousExecutions(int stateId) {
     // Don't check a past trace twice!
     HashSet<Execution> checkedTrace = new HashSet<>();