Generate a new RestorableVMState object only when it's still not available in the...

[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 ef0994cbdeba690d46c526b1016c54a488bc09dc..363bc4b1247dad9bb06c25e00cee67bdb10b3240 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@ -196,6 +196,8 @@ public class DPORStateReducer extends ListenerAdapter {
       // Initialize with necessary information from the CG
       if (nextCG instanceof IntChoiceFromSet) {
         IntChoiceFromSet icsCG = (IntChoiceFromSet) nextCG;
+        // Tell JPF that we are performing DPOR
+        icsCG.setDpor();
         if (!isEndOfExecution) {
           // Check if CG has been initialized, otherwise initialize it
           Integer[] cgChoices = icsCG.getAllChoices();
@@ -352,6 +354,10 @@ public class DPORStateReducer extends ListenerAdapter {
       return executionTrace.get(0);
     }
 
+    public TransitionEvent getLastTransition() {
+      return executionTrace.get(executionTrace.size() - 1);
+    }
+
     public HashMap<Integer, ReadWriteSet> getReadWriteFieldsMap() {
       return readWriteFieldsMap;
     }
@@ -421,6 +427,12 @@ public class DPORStateReducer extends ListenerAdapter {
     }
 
     public HashSet<TransitionEvent> getReachableTransitionsAtState(int stateId) {
+      if (!graph.containsKey(stateId)) {
+        // This is a loop from a transition to itself, so just return the current transition
+        HashSet<TransitionEvent> transitionSet = new HashSet<>();
+        transitionSet.add(currentExecution.getLastTransition());
+        return transitionSet;
+      }
       return graph.get(stateId);
     }
 
@@ -428,7 +440,11 @@ public class DPORStateReducer extends ListenerAdapter {
       HashSet<TransitionEvent> reachableTransitions = new HashSet<>();
       // All transitions from states higher than the given state ID (until the highest state ID) are reachable
       for(int stId = stateId; stId <= hiStateId; stId++) {
-        reachableTransitions.addAll(graph.get(stId));
+        // We might encounter state IDs from the first round of Boolean CG
+        // The second round of Boolean CG should consider these new states
+        if (graph.containsKey(stId)) {
+          reachableTransitions.addAll(graph.get(stId));
+        }
       }
       return reachableTransitions;
     }
@@ -636,8 +652,10 @@ public class DPORStateReducer extends ListenerAdapter {
     }
     currentExecution.mapCGToChoice(icsCG, choiceCounter);
     // Store restorable state object for this state (always store the latest)
-    RestorableVMState restorableState = vm.getRestorableState();
-    restorableStateMap.put(stateId, restorableState);
+    if (!restorableStateMap.containsKey(stateId)) {
+      RestorableVMState restorableState = vm.getRestorableState();
+      restorableStateMap.put(stateId, restorableState);
+    }
   }
 
   private TransitionEvent setupTransition(IntChoiceFromSet icsCG, int stateId, int choiceIndex) {
@@ -1155,7 +1173,8 @@ public class DPORStateReducer extends ListenerAdapter {
               pushedExecution, pushedChoice, currRWSet, visited);
     }
     // Remove the transition after being explored
-    visited.remove(confTrans);
+    // TODO: Seems to cause a lot of loops---commented out for now
+    //visited.remove(confTrans);
   }
 
   // --- Functions related to the reachability analysis when there is a state match