Fixing more potential bugs for the reachability analysis.

[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 c8c780683013dca10fc1cddfde977b9053872955..104af2bd9993dd0cabb776e3e793e1a2060ba2fa 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@ -76,7 +76,8 @@ public class DPORStateReducer extends ListenerAdapter {
   private HashMap<Integer, HashSet<Integer>> conflictPairMap;     // Record conflicting events
   private HashSet<String> doneBacktrackSet;                       // Record state ID and trace already constructed
   private HashMap<Integer, ReadWriteSet> readWriteFieldsMap;      // Record fields that are accessed
-  private HashMap<Integer, RestorableState> restorableStateMap;   // Maps state IDs to the restorable state object
+  private HashMap<Integer, RestorableVMState> restorableStateMap; // Maps state IDs to the restorable state object
+  private HashMap<Integer, Integer> stateToChoiceCounterMap;      // Maps state IDs to the choice counter
 
   // Boolean states
   private boolean isBooleanCGFlipped;
@@ -365,25 +366,6 @@ public class DPORStateReducer extends ListenerAdapter {
     }
   }
 
-  // This class compactly stores: 1) restorable VM state, and 2) global choice counter
-  private class RestorableState {
-    private RestorableVMState restorableState;
-    private int choiceCounter;
-
-    public RestorableState (RestorableVMState restState, int choCtr) {
-      restorableState = restState;
-      choiceCounter = choCtr;
-    }
-
-    public RestorableVMState getRestorableState() {
-      return restorableState;
-    }
-
-    public int getChoiceCounter() {
-      return choiceCounter;
-    }
-  }
-
   // -- CONSTANTS
   private final static String DO_CALL_METHOD = "doCall";
   // We exclude fields that come from libraries (Java and Groovy), and also the infrastructure
@@ -421,7 +403,11 @@ public class DPORStateReducer extends ListenerAdapter {
     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, new RestorableState(restorableState, choiceCounter));
+    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) {
@@ -474,6 +460,7 @@ public class DPORStateReducer extends ListenerAdapter {
     conflictPairMap = new HashMap<>();
     doneBacktrackSet = new HashSet<>();
     readWriteFieldsMap = new HashMap<>();
+    stateToChoiceCounterMap = new HashMap<>();
     // Booleans
     isEndOfExecution = false;
   }
@@ -503,14 +490,14 @@ public class DPORStateReducer extends ListenerAdapter {
     // Update the state variables
     // Line 19 in the paper page 11 (see the heading note above)
     int stateId = search.getStateId();
-    currVisitedStates.add(stateId);
     // Insert state ID into the map if it is new
     if (!stateToEventMap.containsKey(stateId)) {
       HashSet<Integer> eventSet = new HashSet<>();
       stateToEventMap.put(stateId, eventSet);
     }
-    justVisitedStates.add(stateId);
     analyzeReachabilityAndCreateBacktrackPoints(search.getVM(), stateId);
+    justVisitedStates.add(stateId);
+    currVisitedStates.add(stateId);
   }
 
   // --- Functions related to Read/Write access analysis on shared fields
@@ -683,7 +670,7 @@ public class DPORStateReducer extends ListenerAdapter {
                        int hiStateId = backtrackStateQ.peek();
                        // Restore the state first if necessary
                        if (vm.getStateId() != hiStateId) {
-                               RestorableVMState restorableState = restorableStateMap.get(hiStateId).getRestorableState();
+                               RestorableVMState restorableState = restorableStateMap.get(hiStateId);
                                vm.restoreState(restorableState);
                        }
                        // Set the backtrack CG
@@ -848,21 +835,25 @@ public class DPORStateReducer extends ListenerAdapter {
   // 2) We need to analyze and find conflicts for the reachable choices/events in the cycle
   // 3) Then we create a new backtrack point for every new conflict
   private void analyzeReachabilityAndCreateBacktrackPoints(VM vm, int stateId) {
-    // Perform this analysis only when there is a state match
-    if (!vm.isNewState()) {
-      if (restorableStateMap.containsKey(stateId)) {
-        // Find the choice/event that marks the start of this cycle: first choice we explore for conflicts
-        int conflictChoice = restorableStateMap.get(stateId).getChoiceCounter();
-        int currentChoice = choiceCounter - 1;
-        // Find conflicts between choices/events in this cycle (we scan forward in the cycle, not backward)
-        while (conflictChoice < currentChoice) {
-          for (int eventCounter = conflictChoice + 1; eventCounter <= currentChoice; eventCounter++) {
-            if (isConflictFound(eventCounter, conflictChoice) && isNewConflict(conflictChoice, eventCounter)) {
-              createBacktrackingPoint(conflictChoice, eventCounter);
-            }
+    // Perform this analysis only when:
+    // 1) there is a state match,
+    // 2) this is not during a switch to a new execution,
+    // 3) at least 2 choices/events have been explored (choiceCounter > 1),
+    // 4) the matched state has been encountered in the current execution, and
+    // 5) state > 0 (state 0 is for boolean CG)
+    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
+      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)
+      while (conflictChoice < currentChoice) {
+        for (int eventCounter = conflictChoice + 1; eventCounter <= currentChoice; eventCounter++) {
+          if (isConflictFound(eventCounter, conflictChoice) && isNewConflict(conflictChoice, eventCounter)) {
+            createBacktrackingPoint(conflictChoice, eventCounter);
           }
-          conflictChoice++;
         }
+        conflictChoice++;
       }
     }
   }