Fixing a bug: java LinkedList needs removeFirst(), not getFirst() to get and remove...

[jpf-core.git] / src / main / gov / nasa / jpf / listener / DPORStateReducer.java

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index 54170ea00a0e119654b7d19be87d78da643f851e..d8133e397a43c38622abbd0f64577ba64ccbffaa 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@ -28,6 +28,7 @@ import gov.nasa.jpf.vm.bytecode.WriteInstruction;
 import gov.nasa.jpf.vm.choice.IntChoiceFromSet;
 import gov.nasa.jpf.vm.choice.IntIntervalGenerator;
 
+import java.awt.*;
 import java.io.PrintWriter;
 import java.util.*;
 
@@ -73,7 +74,7 @@ public class DPORStateReducer extends ListenerAdapter {
   private PriorityQueue<Integer> backtrackStateQ;                 // Heap that returns the latest state
   private ArrayList<BacktrackPoint> backtrackPointList;           // Record backtrack points (CG, state Id, and choice)
   private HashMap<Integer, HashSet<Integer>> conflictPairMap;     // Record conflicting events
-  private HashSet<String> doneBacktrackSet;                       // Record state ID and trace that are done
+  private HashSet<String> doneBacktrackSet;                       // Record state ID and trace already constructed
   private HashMap<Integer, ReadWriteSet> readWriteFieldsMap;      // Record fields that are accessed
   private HashMap<Integer, RestorableVMState> restorableStateMap; // Maps state IDs to the restorable state object
 
@@ -376,7 +377,11 @@ public class DPORStateReducer extends ListenerAdapter {
       }
     }
     // Record state ID and choice/event as backtrack point
-    backtrackPointList.add(new BacktrackPoint(icsCG, vm.getStateId(), refChoices[choiceIndex]));
+    int stateId = vm.getStateId();
+    backtrackPointList.add(new BacktrackPoint(icsCG, stateId, refChoices[choiceIndex]));
+    // Store restorable state object for this state (always store the latest)
+    RestorableVMState restorableState = vm.getRestorableState();
+    restorableStateMap.put(stateId, restorableState);
   }
 
   private Integer[] copyChoices(Integer[] choicesToCopy) {
@@ -468,9 +473,6 @@ public class DPORStateReducer extends ListenerAdapter {
       stateToEventMap.put(stateId, eventSet);
     }
     justVisitedStates.add(stateId);
-    // Store restorable state object for this state (always store the latest)
-    RestorableVMState restorableState = search.getVM().getRestorableState();
-    restorableStateMap.put(stateId, restorableState);
   }
 
   // --- Functions related to Read/Write access analysis on shared fields
@@ -555,15 +557,20 @@ public class DPORStateReducer extends ListenerAdapter {
     // 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 = 0;
+    int currChoiceFromCG = currChoiceInd;
     ChoiceGenerator<?> currentCG = vm.getChoiceGenerator();
     // This is the main event CG
-    if (currentCG instanceof IntChoiceFromSet) {
-      currChoiceFromCG = currChoiceInd;
-    } else {
+    if (currentCG instanceof IntIntervalGenerator) {
       // This is the interval CG used in device handlers
       ChoiceGenerator<?> parentCG = ((IntIntervalGenerator) currentCG).getPreviousChoiceGenerator();
-      currChoiceFromCG = ((IntChoiceFromSet) parentCG).getNextChoiceIndex();
+      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;
@@ -592,10 +599,9 @@ public class DPORStateReducer extends ListenerAdapter {
     // Get the backtrack CG for this backtrack point
     int stateId = backtrackPointList.get(confEvtNum).getStateId();
     // Check if this trace has been done starting from this state
-    if (isTraceConstructed(newChoiceList, stateId)) {
+    if (isTraceAlreadyConstructed(newChoiceList, stateId)) {
       return;
     }
-    //BacktrackPoint backtrackPoint = new BacktrackPoint(backtrackCG, newChoiceList);
     addNewBacktrackPoint(stateId, newChoiceList);
   }
 
@@ -721,14 +727,16 @@ public class DPORStateReducer extends ListenerAdapter {
     return true;
   }
 
-  private boolean isTraceConstructed(Integer[] choiceList, int stateId) {
-    // Concatenate state ID and trace in a string, e.g., "1:10234"
+  private boolean isTraceAlreadyConstructed(Integer[] choiceList, 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!
+    // This is the optimized version because after we execute, e.g., the trace 1:10234, we don't need to try
+    // another trace that starts with event 1 at state 1, e.g., the trace 1:13024
+    // The second time this event 1 is explored, it will generate the same state as the first one
     StringBuilder sb = new StringBuilder();
     sb.append(stateId);
     sb.append(':');
-    for(Integer choice : choiceList) {
-      sb.append(choice);
-    }
+    sb.append(choiceList[0]);
     // Check if the trace has been constructed as a backtrack point for this state
     if (doneBacktrackSet.contains(sb.toString())) {
       return true;
@@ -784,12 +792,12 @@ public class DPORStateReducer extends ListenerAdapter {
     if (vodGraphMap.containsKey(prevEvent)) {
       nodesToVisit.addAll(vodGraphMap.get(prevEvent));
       while(!nodesToVisit.isEmpty()) {
-        int choice = nodesToVisit.getFirst();
+        int choice = nodesToVisit.removeFirst();
         if (choice == currEvent) {
           return true;
         }
-        if (visitedChoice.contains(choice)) { // If there is a loop then we don't find it
-          return false;
+        if (visitedChoice.contains(choice)) { // If there is a loop then just continue the exploration
+          continue;
         }
         // Continue searching
         visitedChoice.add(choice);