Fixing a bug: restorable state has to be saved when backtrack point info is saved...

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index 54170ea00a0e119654b7d19be87d78da643f851e..8531e2cc4db5c1588ba3db63204858786fae26f8 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 gov.nasa.jpf.vm.choice.IntChoiceFromSet;
 import gov.nasa.jpf.vm.choice.IntIntervalGenerator;
 

+import java.awt.*;

 import java.io.PrintWriter;
 import java.util.*;
 
 import java.io.PrintWriter;
 import java.util.*;
 


@@ -376,7 +377,11 @@ public class DPORStateReducer extends ListenerAdapter {
       }
     }
     // Record state ID and choice/event as backtrack point
       }
     }
     // 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) {
   }
 
   private Integer[] copyChoices(Integer[] choicesToCopy) {


@@ -468,9 +473,6 @@ public class DPORStateReducer extends ListenerAdapter {
       stateToEventMap.put(stateId, eventSet);
     }
     justVisitedStates.add(stateId);
       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
   }
 
   // --- 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;
     // 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
     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();
       // 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;
     }
     if (currChoiceInd != currChoiceFromCG) {
       currentChoice = (currentChoice - currChoiceInd) + currChoiceFromCG;


@@ -595,7 +602,6 @@ public class DPORStateReducer extends ListenerAdapter {
     if (isTraceConstructed(newChoiceList, stateId)) {
       return;
     }
     if (isTraceConstructed(newChoiceList, stateId)) {
       return;
     }

-    //BacktrackPoint backtrackPoint = new BacktrackPoint(backtrackCG, newChoiceList);

     addNewBacktrackPoint(stateId, newChoiceList);
   }
 
     addNewBacktrackPoint(stateId, newChoiceList);
   }