Slight changes for safeguard.

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

diff --git a/src/main/gov/nasa/jpf/listener/StateReducer.java b/src/main/gov/nasa/jpf/listener/StateReducer.java
index 2194ff160d3074b2a9325a2c75cab2b97f2d0d1f..e67ee1344385da875aef611ad1e49cfc2436b8d7 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/StateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/StateReducer.java
@@ -87,6 +87,8 @@ public class StateReducer extends ListenerAdapter {
   private HashSet<Integer> visitedStateSet;
   // Current state
   private int stateId;
+  // Previous choice number
+  private int prevChoiceValue;
 
   public StateReducer(Config config, JPF jpf) {
     debugMode = config.getBoolean("debug_state_transition", false);
@@ -104,6 +106,12 @@ public class StateReducer extends ListenerAdapter {
     vodGraphMap = new HashMap<>();
     visitedStateSet = new HashSet<>();
     stateId = -1;
+    prevChoiceValue = -1;
+    cgMap = new HashMap<>();
+    readWriteFieldsMap = new HashMap<>();
+    backtrackMap = new HashMap<>();
+    backtrackSet = new HashSet<>();
+    conflictPairMap = new HashMap<>();
     initializeStateReduction();
   }
 
@@ -116,11 +124,11 @@ public class StateReducer extends ListenerAdapter {
       maxUpperBound = 0;
       isInitialized = false;
       isResetAfterAnalysis = false;
-      cgMap = new HashMap<>();
-      readWriteFieldsMap = new HashMap<>();
-      backtrackMap = new HashMap<>();
-      backtrackSet = new HashSet<>();
-      conflictPairMap = new HashMap<>();
+      cgMap.clear();
+      readWriteFieldsMap.clear();
+      backtrackMap.clear();
+      backtrackSet.clear();
+      conflictPairMap.clear();
     }
   }
 
@@ -239,16 +247,18 @@ public class StateReducer extends ListenerAdapter {
           choiceCounter++;
           // Do this for every CG after finishing each backtrack list
           if (icsCG.getNextChoice() == -1 || visitedStateSet.contains(stateId)) {
-            int event = cgMap.get(icsCG);
-            LinkedList<Integer[]> choiceLists = backtrackMap.get(event);
-            if (choiceLists != null && choiceLists.peekFirst() != null) {
-              Integer[] choiceList = choiceLists.removeFirst();
-              // Deploy the new choice list for this CG
-              icsCG.setNewValues(choiceList);
-              icsCG.reset();
-            } else {
-              // Set done if this was the last backtrack list
-              icsCG.setDone();
+            if (cgMap.containsKey(icsCG)) {
+              int event = cgMap.get(icsCG);
+              LinkedList<Integer[]> choiceLists = backtrackMap.get(event);
+              if (choiceLists != null && choiceLists.peekFirst() != null) {
+                Integer[] choiceList = choiceLists.removeFirst();
+                // Deploy the new choice list for this CG
+                icsCG.setNewValues(choiceList);
+                icsCG.reset();
+              } else {
+                // Set done if this was the last backtrack list
+                icsCG.setDone();
+              }
             }
           }
         }
@@ -297,17 +307,14 @@ public class StateReducer extends ListenerAdapter {
     if (stateReductionMode) {
       // Update vodGraph
       int currChoice = choiceCounter - 1;
-      int prevChoice = currChoice - 1;
-      if (currChoice < 0) {
-        // Current choice has to be at least 0 (initial case can be -1)
-        visitedStateSet.add(stateId);
+      if (currChoice < 0 || currChoice > choices.length - 1 || choices[currChoice] == -1 || prevChoiceValue == choices[currChoice]) {
+        // Handle all corner cases (e.g., out of bound values)
         return;
       }
-      // Current choice and previous choice values could be -1 (since we use -1 as the end-of-array condition)
-      int currChoiceValue = (choices[currChoice] == -1) ? 0 : choices[currChoice];
       // When current choice is 0, previous choice could be -1
-      int prevChoiceValue = (prevChoice == -1) ? -1 : choices[prevChoice];
-      updateVODGraph(prevChoiceValue, currChoiceValue);
+      updateVODGraph(prevChoiceValue, choices[currChoice]);
+      // Current choice becomes previous choice in the next iteration
+      prevChoiceValue = choices[currChoice];
       // Line 19 in the paper page 11 (see the heading note above)
       stateId = search.getStateId();
       // Add state ID into the visited state set
@@ -481,7 +488,7 @@ public class StateReducer extends ListenerAdapter {
       // The start index for the recursion is always 1 (from the main branch)
     } else { // This is a sub-graph
       // There is a case/bug that after a re-initialization, currCG is not yet initialized
-      if (currCG != null) {
+      if (currCG != null && cgMap.containsKey(currCG)) {
         int backtrackListIndex = cgMap.get(currCG);
         backtrackChoiceLists = backtrackMap.get(backtrackListIndex);
         int listLength = choices.length;