From: rtrimana <rtrimana@uci.edu>
Date: Wed, 15 Apr 2020 23:34:11 +0000 (-0700)
Subject: Fixing more bugs with the reachability analysis.
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=commitdiff_plain;h=c540b2eddfd5b18a25070d2f85bfe94de3f535c5;hp=3e0a2fe1baa5e2530e75452524afdedba8045126

Fixing more bugs with the reachability analysis.
---

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index 104af2b..26dd6bd 100644
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@ -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) {
@@ -495,6 +491,7 @@ public class DPORStateReducer extends ListenerAdapter {
       HashSet<Integer> eventSet = new HashSet<>();
       stateToEventMap.put(stateId, eventSet);
     }
+    stateToChoiceCounterMap.put(stateId, choiceCounter);
     analyzeReachabilityAndCreateBacktrackPoints(search.getVM(), stateId);
     justVisitedStates.add(stateId);
     currVisitedStates.add(stateId);
@@ -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++) {
@@ -844,6 +845,9 @@ public class DPORStateReducer extends ListenerAdapter {
     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
+      if (stateToChoiceCounterMap.get(stateId) == null) {
+        System.out.println();
+      }
       int conflictChoice = stateToChoiceCounterMap.get(stateId);
       int currentChoice = choiceCounter - 1;
       // Find conflicts between choices/events in this cycle (we scan forward in the cycle, not backward)