Fixing a bug: mapping state to event has to be done after the execution termination...

[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 0c513f21372d531a3d5b59754bb1de3445010380..12bd44ff802e2547e86e1e22856f32ff6e31c6bf 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@ -228,8 +228,6 @@ public class DPORStateReducer extends ListenerAdapter {
         resetStatesForNewExecution(icsCG, vm);
         // If we don't see a fair scheduling of events/choices then we have to enforce it
         fairSchedulingAndBacktrackPoint(icsCG, vm);
-        // Map state to event
-        mapStateToEvent(icsCG.getNextChoice());
         // Explore the next backtrack point: 
         // 1) if we have seen this state or this state contains cycles that involve all events, and
         // 2) after the current CG is advanced at least once
@@ -238,6 +236,8 @@ public class DPORStateReducer extends ListenerAdapter {
         } else {
           numOfTransitions++;
         }
+        // Map state to event
+        mapStateToEvent(icsCG.getNextChoice());
         justVisitedStates.clear();
         choiceCounter++;
       }
@@ -404,10 +404,6 @@ public class DPORStateReducer extends ListenerAdapter {
     // Store restorable state object for this state (always store the latest)
     RestorableVMState restorableState = vm.getRestorableState();
     restorableStateMap.put(stateId, restorableState);
-    // Map multiple state IDs to a choice counter
-    for (Integer stId : justVisitedStates) {
-      stateToChoiceCounterMap.put(stId, choiceCounter);
-    }
   }
 
   private Integer[] copyChoices(Integer[] choicesToCopy) {
@@ -490,14 +486,15 @@ public class DPORStateReducer extends ListenerAdapter {
     // Update the state variables
     // Line 19 in the paper page 11 (see the heading note above)
     int stateId = search.getStateId();
-    currVisitedStates.add(stateId);
     // Insert state ID into the map if it is new
     if (!stateToEventMap.containsKey(stateId)) {
       HashSet<Integer> eventSet = new HashSet<>();
       stateToEventMap.put(stateId, eventSet);
     }
-    justVisitedStates.add(stateId);
+    stateToChoiceCounterMap.put(stateId, choiceCounter);
     analyzeReachabilityAndCreateBacktrackPoints(search.getVM(), stateId);
+    justVisitedStates.add(stateId);
+    currVisitedStates.add(stateId);
   }
 
   // --- Functions related to Read/Write access analysis on shared fields
@@ -588,6 +585,10 @@ public class DPORStateReducer extends ListenerAdapter {
     if (currentCG instanceof IntIntervalGenerator) {
       // This is the interval CG used in device handlers
       ChoiceGenerator<?> parentCG = ((IntIntervalGenerator) currentCG).getPreviousChoiceGenerator();
+      // Iterate until we find the IntChoiceFromSet CG
+      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++) {
@@ -835,8 +836,14 @@ public class DPORStateReducer extends ListenerAdapter {
   // 2) We need to analyze and find conflicts for the reachable choices/events in the cycle
   // 3) Then we create a new backtrack point for every new conflict
   private void analyzeReachabilityAndCreateBacktrackPoints(VM vm, int stateId) {
-    // Perform this analysis only when there is a state match and state > 0 (state 0 is for boolean CG)
-    if (!vm.isNewState() && (stateId > 0)) {
+    // Perform this analysis only when:
+    // 1) there is a state match,
+    // 2) this is not during a switch to a new execution,
+    // 3) at least 2 choices/events have been explored (choiceCounter > 1),
+    // 4) the matched state has been encountered in the current execution, and
+    // 5) state > 0 (state 0 is for boolean CG)
+    if (!vm.isNewState() && !isEndOfExecution && choiceCounter > 1 &&
+            currVisitedStates.contains(stateId) && (stateId > 0)) {
       // Find the choice/event that marks the start of this cycle: first choice we explore for conflicts
       int conflictChoice = stateToChoiceCounterMap.get(stateId);
       int currentChoice = choiceCounter - 1;