Fixing bugs: state to reachability graph map has to be updated for every new state...
authorrtrimana <rtrimana@uci.edu>
Sat, 2 May 2020 15:25:49 +0000 (08:25 -0700)
committerrtrimana <rtrimana@uci.edu>
Sat, 2 May 2020 15:25:49 +0000 (08:25 -0700)
src/main/gov/nasa/jpf/listener/DPORStateReducer.java

index 4645d2c..37ae774 100644 (file)
@@ -252,7 +252,6 @@ public class DPORStateReducer extends ListenerAdapter {
         // 1) if we have seen this state or this state contains cycles that involve all events, and
         // 2) after the current CG is advanced at least once
         if (terminateCurrentExecution() && choiceCounter > 0) {
-          saveExecutionInfo();
           exploreNextBacktrackPoints(vm, icsCG);
         } else {
           numOfTransitions++;
@@ -303,7 +302,7 @@ public class DPORStateReducer extends ListenerAdapter {
                   // Check and record a backtrack set for just once!
                   if (isConflictFound(nextInsn, eventCounter, currentChoice, fieldClass) &&
                       isNewConflict(currentChoice, eventCounter)) {
-                    createBacktrackingPoint(currentChoice, eventCounter);
+                    createBacktrackingPoint(currentChoice, eventCounter, false);
                   }
                 }
               }
@@ -533,6 +532,12 @@ 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);
+    }
     stateToChoiceCounterMap.put(stateId, choiceCounter);
     analyzeReachabilityAndCreateBacktrackPoints(search.getVM(), stateId);
     justVisitedStates.add(stateId);
@@ -646,15 +651,21 @@ public class DPORStateReducer extends ListenerAdapter {
     return currentChoice;
   }
 
-  private void createBacktrackingPoint(int currentChoice, int confEvtNum) {
+  private void createBacktrackingPoint(int currentChoice, int confEvtNum, boolean isPastTrace) {
 
     // Create a new list of choices for backtrack based on the current choice and conflicting event number
     // E.g. if we have a conflict between 1 and 3, then we create the list {3, 1, 0, 2}
     // for the original set {0, 1, 2, 3}
     Integer[] newChoiceList = new Integer[refChoices.length];
     // Put the conflicting event numbers first and reverse the order
-    // We use the actual choices here in case they have been modified/adjusted by the fair scheduling method
-    newChoiceList[0] = backtrackPointList.get(currentChoice).getChoice();
+    if (isPastTrace) {
+      // For past trace we get the choice/event from the list
+      newChoiceList[0] = backtrackPointList.get(currentChoice).getChoice();
+    } else {
+      // We use the actual choices here in case they have been modified/adjusted by the fair scheduling method
+      int actualCurrCho = currentChoice % refChoices.length;
+      newChoiceList[0] = choices[actualCurrCho];
+    }
     newChoiceList[1] = backtrackPointList.get(confEvtNum).getChoice();
     // Put the rest of the event numbers into the array starting from the minimum to the upper bound
     for (int i = 0, j = 2; i < refChoices.length; i++) {
@@ -742,11 +753,18 @@ public class DPORStateReducer extends ListenerAdapter {
     return rwSet;
   }
 
-  private boolean isConflictFound(int eventCounter, int currentChoice) {
+  private boolean isConflictFound(int eventCounter, int currentChoice, boolean isPastTrace) {
 
+    int currActualChoice;
+    if (isPastTrace) {
+      currActualChoice = backtrackPointList.get(currentChoice).getChoice();
+    } else {
+      int actualCurrCho = currentChoice % refChoices.length;
+      currActualChoice = choices[actualCurrCho];
+    }
     // Skip if this event does not have any Read/Write set or the two events are basically the same event (number)
     if (!readWriteFieldsMap.containsKey(eventCounter) ||
-            backtrackPointList.get(currentChoice).getChoice() == backtrackPointList.get(eventCounter).getChoice()) {
+            currActualChoice == backtrackPointList.get(eventCounter).getChoice()) {
       return false;
     }
     // Current R/W set
@@ -894,19 +912,35 @@ public class DPORStateReducer extends ListenerAdapter {
     }
   }
 
-  // Save the information from this execution for future reachability analysis
-  private void saveExecutionInfo() {
-    Set<Integer> states = stateToChoiceCounterMap.keySet();
-    ReachabilityGraph reachabilityGraph = new
-            ReachabilityGraph(backtrackPointList, readWriteFieldsMap);
-    // Map all the states visited in this execution to the same ReachabilityGraph object for fast access
-    for(Integer state : states) {
-      if (!prevVisitedStates.contains(state)) {
-        stateToRGraph.put(state, reachabilityGraph);
+  // Get the start event for the past execution trace when there is a state matched from a past execution
+  private int getPastConflictChoice(int stateId, ArrayList<BacktrackPoint> pastBacktrackPointList) {
+    // Iterate and find the first occurrence of the state ID
+    // It is guaranteed that a choice should be found because the state ID is in the list
+    int pastConfChoice = 0;
+    for(int i = 0; i<pastBacktrackPointList.size(); i++) {
+      BacktrackPoint backtrackPoint = pastBacktrackPointList.get(i);
+      int stId = backtrackPoint.getStateId();
+      if (stId == stateId) {
+        pastConfChoice = i;
+        break;
       }
     }
+    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);
+//      }
+//    }
+//  }
+
   // Update the backtrack sets in the cycle
   private void updateBacktrackSetsInCycle(int stateId) {
     // Find the choice/event that marks the start of this cycle: first choice we explore for conflicts
@@ -915,29 +949,14 @@ public class DPORStateReducer extends ListenerAdapter {
     // 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);
+        if (isConflictFound(eventCounter, conflictChoice, false) && isNewConflict(conflictChoice, eventCounter)) {
+          createBacktrackingPoint(conflictChoice, eventCounter, false);
         }
       }
       conflictChoice++;
     }
   }
 
-  private int getPastConflictChoice(int stateId, ArrayList<BacktrackPoint> pastBacktrackPointList) {
-    // Iterate and find the first occurrence of the state ID
-    // It is guaranteed that a choice should be found because the state ID is in the list
-    int pastConfChoice = 0;
-    for(int i = 0; i<pastBacktrackPointList.size(); i++) {
-      BacktrackPoint backtrackPoint = pastBacktrackPointList.get(i);
-      int stId = backtrackPoint.getStateId();
-      if (stId == stateId) {
-        pastConfChoice = i;
-        break;
-      }
-    }
-    return pastConfChoice;
-  }
-
   // Update the backtrack sets in a previous execution
   private void updateBacktrackSetsInPreviousExecution(int stateId) {
     // Find the right ReachabilityGraph object that contains the stateId
@@ -956,8 +975,8 @@ public class DPORStateReducer extends ListenerAdapter {
       backtrackPointList.add(confBtrackPoint);
       readWriteFieldsMap.put(choiceCounter, rwSet);
       for (int eventCounter = conflictChoice - 1; eventCounter >= 0; eventCounter--) {
-        if (isConflictFound(eventCounter, conflictChoice) && isNewConflict(conflictChoice, eventCounter)) {
-          createBacktrackingPoint(conflictChoice, eventCounter);
+        if (isConflictFound(eventCounter, conflictChoice, true) && isNewConflict(conflictChoice, eventCounter)) {
+          createBacktrackingPoint(conflictChoice, eventCounter, true);
         }
       }
       // Remove this event to replace it with a new one