From: rtrimana <rtrimana@uci.edu>
Date: Thu, 9 Apr 2020 22:57:06 +0000 (-0700)
Subject: Fixing a bug: restorable state has to be saved when backtrack point info is saved... 
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=commitdiff_plain;h=2c85b3bb2b21786f8eb76be7fd4eb7dc22d95e4b;hp=ebcf259b97ccf4d66fe75b59a5ebd36fadda4ddd

Fixing a bug: restorable state has to be saved when backtrack point info is saved to get the appropriate CG type when restoring.
---

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index 54170ea..8531e2c 100644
--- 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.*;
 
@@ -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;
@@ -595,7 +602,6 @@ public class DPORStateReducer extends ListenerAdapter {
     if (isTraceConstructed(newChoiceList, stateId)) {
       return;
     }
-    //BacktrackPoint backtrackPoint = new BacktrackPoint(backtrackCG, newChoiceList);
     addNewBacktrackPoint(stateId, newChoiceList);
   }