Fixing a bug: need to get the right choice/event number for IntIntervalGenerator...
authorrtrimana <rtrimana@uci.edu>
Tue, 19 May 2020 16:38:08 +0000 (09:38 -0700)
committerrtrimana <rtrimana@uci.edu>
Tue, 19 May 2020 16:38:08 +0000 (09:38 -0700)
src/main/gov/nasa/jpf/listener/DPORStateReducer.java

index f4b5923..bc42a46 100644 (file)
@@ -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 HashMap<Integer, ArrayList<ReachableTrace>> rGraph;     // Create a reachability graph
   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 {
-    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() {
+      cgToChoiceMap = new HashMap<>();
       executionTrace = new ArrayList<>();
       parentChoice = -1;
       parent = null;
@@ -373,10 +374,18 @@ public class DPORStateReducer extends ListenerAdapter {
       executionTrace.add(newBacktrackPoint);
     }
 
+    public void clearCGToChoiceMap() {
+      cgToChoiceMap = null;
+    }
+
     public ArrayList<BacktrackPoint> getExecutionTrace() {
       return executionTrace;
     }
 
+    public int getChoiceFromCG(IntChoiceFromSet icsCG) {
+      return cgToChoiceMap.get(icsCG);
+    }
+
     public int getParentChoice() {
       return parentChoice;
     }
@@ -389,6 +398,10 @@ public class DPORStateReducer extends ListenerAdapter {
       return readWriteFieldsMap;
     }
 
+    public void mapCGToChoice(IntChoiceFromSet icsCG, int choice) {
+      cgToChoiceMap.put(icsCG, choice);
+    }
+
     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
@@ -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]));
+    currentExecution.mapCGToChoice(icsCG, choiceCounter);
     // 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()
-    int currChoiceInd = currentChoice % refChoices.length;
-    int currChoiceFromCG = currChoiceInd;
     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();
       }
-      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;
   }
@@ -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;
-    // 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
@@ -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) ||
-            //choices[actualChoice] == pastTrace.get(pastChoice).getChoice()) {
             currTrace.get(currentChoice).getChoice() == pastTrace.get(pastChoice).getChoice()) {
       return false;
     }
@@ -924,6 +904,7 @@ public class DPORStateReducer extends ListenerAdapter {
     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!
@@ -942,6 +923,7 @@ public class DPORStateReducer extends ListenerAdapter {
     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
@@ -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);
@@ -970,6 +953,8 @@ public class DPORStateReducer extends ListenerAdapter {
       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()) {
@@ -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
-  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();
@@ -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
@@ -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);
-      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();
@@ -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<>();