Fixing a bug: completing reachability graph with missing past traces.

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index 37ae7744dbdc0e3f92e0126624a6b5f0c04c655c..885add3e489bf49126c388171fc51811bad1d4af 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@ -82,7 +82,7 @@ public class DPORStateReducer extends ListenerAdapter {
   private HashMap<Integer, ReadWriteSet> readWriteFieldsMap;      // Record fields that are accessed
   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
-  private HashMap<Integer, ReachabilityGraph> stateToRGraph;      // Maps state IDs to a ReachabilityGraph
+  private HashMap<Integer, ArrayList<ReachableTrace>> rGraph;     // Create a reachability graph
 
   // Boolean states
   private boolean isBooleanCGFlipped;
@@ -387,11 +387,11 @@ public class DPORStateReducer extends ListenerAdapter {
   }
 
   // This class stores a compact representation of a reachability graph for past executions
-  private class ReachabilityGraph {
+  private class ReachableTrace {
     private ArrayList<BacktrackPoint> pastBacktrackPointList;
     private HashMap<Integer, ReadWriteSet> pastReadWriteFieldsMap;
 
-    public ReachabilityGraph(ArrayList<BacktrackPoint> btrackPointList,
+    public ReachableTrace(ArrayList<BacktrackPoint> btrackPointList,
                              HashMap<Integer, ReadWriteSet> rwFieldsMap) {
       pastBacktrackPointList = btrackPointList;
       pastReadWriteFieldsMap = rwFieldsMap;
@@ -497,7 +497,7 @@ public class DPORStateReducer extends ListenerAdapter {
     doneBacktrackSet = new HashSet<>();
     readWriteFieldsMap = new HashMap<>();
     stateToChoiceCounterMap = new HashMap<>();
-    stateToRGraph = new HashMap<>();
+    rGraph = new HashMap<>();
     // Booleans
     isEndOfExecution = false;
   }
@@ -532,11 +532,21 @@ public class DPORStateReducer extends ListenerAdapter {
       HashSet<Integer> eventSet = new HashSet<>();
       stateToEventMap.put(stateId, eventSet);
     }
-    // Save execution state into the map
-    if (!prevVisitedStates.contains(stateId)) {
-      ReachabilityGraph reachabilityGraph = new
-              ReachabilityGraph(backtrackPointList, readWriteFieldsMap);
-      stateToRGraph.put(stateId, reachabilityGraph);
+    // Save execution state into the Reachability only if
+    // (1) It is not a revisited state from a past execution, or
+    // (2) It is just a new backtracking point
+    if (!prevVisitedStates.contains(stateId) ||
+            choiceCounter <= 1) {
+      ReachableTrace reachableTrace= new
+              ReachableTrace(backtrackPointList, readWriteFieldsMap);
+      ArrayList<ReachableTrace> rTrace;
+      if (!prevVisitedStates.contains(stateId)) {
+        rTrace = new ArrayList<>();
+        rGraph.put(stateId, rTrace);
+      } else {
+        rTrace = rGraph.get(stateId);
+      }
+      rTrace.add(reachableTrace);
     }
     stateToChoiceCounterMap.put(stateId, choiceCounter);
     analyzeReachabilityAndCreateBacktrackPoints(search.getVM(), stateId);
@@ -928,18 +938,18 @@ public class DPORStateReducer extends ListenerAdapter {
     return pastConfChoice;
   }
 
-  // Save the information from this execution for future reachability analysis
-//  private void saveExecutionInfo() {
-//    Set<Integer> states = stateToChoiceCounterMap.keySet();
-//    // Map all the states visited in this execution to the same ReachabilityGraph object for fast access
-//    for(Integer state : states) {
-//      if (!prevVisitedStates.contains(state)) {
-//        ReachabilityGraph reachabilityGraph = new
-//                ReachabilityGraph(backtrackPointList, readWriteFieldsMap);
-//        stateToRGraph.put(state, reachabilityGraph);
-//      }
-//    }
-//  }
+  // Get a sorted list of reachable state IDs starting from the input stateId
+  private ArrayList<Integer> getReachableStateIds(Set<Integer> stateIds, int stateId) {
+    // Only include state IDs equal or greater than the input stateId: these are reachable states
+    ArrayList<Integer> sortedStateIds = new ArrayList<>();
+    for(Integer stId : stateIds) {
+      if (stId >= stateId) {
+        sortedStateIds.add(stId);
+      }
+    }
+    Collections.sort(sortedStateIds);
+    return sortedStateIds;
+  }
 
   // Update the backtrack sets in the cycle
   private void updateBacktrackSetsInCycle(int stateId) {
@@ -957,32 +967,70 @@ public class DPORStateReducer extends ListenerAdapter {
     }
   }
 
+  // TODO: OPTIMIZATION!
+  // Check and make sure that state ID and choice haven't been explored for this trace
+  private boolean isNotChecked(HashMap<Integer, HashSet<Integer>> checkedStateIdAndChoice,
+                               BacktrackPoint backtrackPoint) {
+    int stateId = backtrackPoint.getStateId();
+    int choice = backtrackPoint.getChoice();
+    HashSet<Integer> choiceSet;
+    if (checkedStateIdAndChoice.containsKey(stateId)) {
+      choiceSet = checkedStateIdAndChoice.get(stateId);
+      if (choiceSet.contains(choice)) {
+        // State ID and choice found. It has been checked!
+        return false;
+      }
+    } else {
+      choiceSet = new HashSet<>();
+      checkedStateIdAndChoice.put(stateId, choiceSet);
+    }
+    choiceSet.add(choice);
+
+    return true;
+  }
+
   // Update the backtrack sets in a previous execution
   private void updateBacktrackSetsInPreviousExecution(int stateId) {
-    // Find the right ReachabilityGraph object that contains the stateId
-    ReachabilityGraph rGraph = stateToRGraph.get(stateId);
-    // Find the choice/event that marks the start of the subtrace from the previous execution
-    ArrayList<BacktrackPoint> pastBacktrackPointList = rGraph.getPastBacktrackPointList();
-    HashMap<Integer, ReadWriteSet> pastReadWriteFieldsMap = rGraph.getPastReadWriteFieldsMap();
-    int pastConfChoice = getPastConflictChoice(stateId, pastBacktrackPointList);
-    int conflictChoice = choiceCounter;
-    // Iterate from the starting point until the end of the past execution trace
-    while (pastConfChoice < pastBacktrackPointList.size() - 1) {  // BacktrackPoint list always has a surplus of 1
-      // Get the info of the event from the past execution trace
-      BacktrackPoint confBtrackPoint = pastBacktrackPointList.get(pastConfChoice);
-      ReadWriteSet rwSet = pastReadWriteFieldsMap.get(pastConfChoice);
-      // Append this event to the current list and map
-      backtrackPointList.add(confBtrackPoint);
-      readWriteFieldsMap.put(choiceCounter, rwSet);
-      for (int eventCounter = conflictChoice - 1; eventCounter >= 0; eventCounter--) {
-        if (isConflictFound(eventCounter, conflictChoice, true) && isNewConflict(conflictChoice, eventCounter)) {
-          createBacktrackingPoint(conflictChoice, eventCounter, true);
+    // Don't check a past trace twice!
+    HashSet<ReachableTrace> checkedTrace = new HashSet<>();
+    // Don't check the same event twice for a revisited state
+    HashMap<Integer, HashSet<Integer>> checkedStateIdAndChoice = new HashMap<>();
+    // Get sorted reachable state IDs
+    ArrayList<Integer> reachableStateIds = getReachableStateIds(rGraph.keySet(), stateId);
+    // Iterate from this state ID until the biggest state ID
+    for(Integer stId : reachableStateIds) {
+      // Find the right reachability graph object that contains the stateId
+      ArrayList<ReachableTrace> rTraces = rGraph.get(stId);
+      for (ReachableTrace rTrace : rTraces) {
+        if (!checkedTrace.contains(rTrace)) {
+          // Find the choice/event that marks the start of the subtrace from the previous execution
+          ArrayList<BacktrackPoint> pastBacktrackPointList = rTrace.getPastBacktrackPointList();
+          HashMap<Integer, ReadWriteSet> pastReadWriteFieldsMap = rTrace.getPastReadWriteFieldsMap();
+          int pastConfChoice = getPastConflictChoice(stId, pastBacktrackPointList);
+          int conflictChoice = choiceCounter;
+          // Iterate from the starting point until the end of the past execution trace
+          while (pastConfChoice < pastBacktrackPointList.size() - 1) {  // BacktrackPoint list always has a surplus of 1
+            // Get the info of the event from the past execution trace
+            BacktrackPoint confBtrackPoint = pastBacktrackPointList.get(pastConfChoice);
+            if (isNotChecked(checkedStateIdAndChoice, confBtrackPoint)) {
+              ReadWriteSet rwSet = pastReadWriteFieldsMap.get(pastConfChoice);
+              // Append this event to the current list and map
+              backtrackPointList.add(confBtrackPoint);
+              readWriteFieldsMap.put(choiceCounter, rwSet);
+              for (int eventCounter = conflictChoice - 1; eventCounter >= 0; eventCounter--) {
+                if (isConflictFound(eventCounter, conflictChoice, true) && isNewConflict(conflictChoice, eventCounter)) {
+                  createBacktrackingPoint(conflictChoice, eventCounter, true);
+                }
+              }
+              // Remove this event to replace it with a new one
+              backtrackPointList.remove(backtrackPointList.size() - 1);
+              readWriteFieldsMap.remove(choiceCounter);
+            }
+            pastConfChoice++;
+          }
+          checkedTrace.add(rTrace);
         }
       }
-      // Remove this event to replace it with a new one
-      backtrackPointList.remove(backtrackPointList.size() - 1);
-      readWriteFieldsMap.remove(choiceCounter);
-      pastConfChoice++;
     }
   }
 }