Adjusting support methods for reachability analysis with the new algorithm; untested...
authorrtrimana <rtrimana@uci.edu>
Thu, 14 May 2020 23:36:02 +0000 (16:36 -0700)
committerrtrimana <rtrimana@uci.edu>
Thu, 14 May 2020 23:36:02 +0000 (16:36 -0700)
src/main/gov/nasa/jpf/listener/DPORStateReducer.java

index bf06232..ee61c19 100644 (file)
@@ -80,7 +80,8 @@ public class DPORStateReducer extends ListenerAdapter {
   private HashSet<String> doneBacktrackSet;                       // Record state ID and trace already constructed
   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, ArrayList<ReachableTrace>> rGraph;     // Create a reachability graph
+  //private HashMap<Integer, ArrayList<ReachableTrace>> rGraph;     // Create a reachability graph
+  private HashMap<Integer, ArrayList<Execution>> rGraph;          // Create a reachability graph for past executions
 
   // Boolean states
   private boolean isBooleanCGFlipped;
@@ -442,27 +443,25 @@ public class DPORStateReducer extends ListenerAdapter {
     }
   }
 
-
-
   // This class stores a compact representation of a reachability graph for past executions
-  private class ReachableTrace {
-    private ArrayList<BacktrackPoint> pastBacktrackPointList;
-    private HashMap<Integer, ReadWriteSet> pastReadWriteFieldsMap;
-
-    public ReachableTrace(ArrayList<BacktrackPoint> btrackPointList,
-                             HashMap<Integer, ReadWriteSet> rwFieldsMap) {
-      pastBacktrackPointList = btrackPointList;
-      pastReadWriteFieldsMap = rwFieldsMap;
-    }
-
-    public ArrayList<BacktrackPoint> getPastBacktrackPointList() {
-      return pastBacktrackPointList;
-    }
-
-    public HashMap<Integer, ReadWriteSet> getPastReadWriteFieldsMap() {
-      return pastReadWriteFieldsMap;
-    }
-  }
+//  private class ReachableTrace {
+//    private ArrayList<BacktrackPoint> pastBacktrackPointList;
+//    private HashMap<Integer, ReadWriteSet> pastReadWriteFieldsMap;
+//
+//    public ReachableTrace(ArrayList<BacktrackPoint> btrackPointList,
+//                             HashMap<Integer, ReadWriteSet> rwFieldsMap) {
+//      pastBacktrackPointList = btrackPointList;
+//      pastReadWriteFieldsMap = rwFieldsMap;
+//    }
+//
+//    public ArrayList<BacktrackPoint> getPastBacktrackPointList() {
+//      return pastBacktrackPointList;
+//    }
+//
+//    public HashMap<Integer, ReadWriteSet> getPastReadWriteFieldsMap() {
+//      return pastReadWriteFieldsMap;
+//    }
+//  }
 
   // -- CONSTANTS
   private final static String DO_CALL_METHOD = "doCall";
@@ -498,7 +497,6 @@ public class DPORStateReducer extends ListenerAdapter {
     }
     // Record state ID and choice/event as backtrack point
     int stateId = vm.getStateId();
-//    backtrackPointList.add(new BacktrackPoint(icsCG, stateId, refChoices[choiceIndex]));
     currentExecution.addBacktrackPoint(new BacktrackPoint(icsCG, stateId, refChoices[choiceIndex]));
     // Store restorable state object for this state (always store the latest)
     RestorableVMState restorableState = vm.getRestorableState();
@@ -512,7 +510,7 @@ public class DPORStateReducer extends ListenerAdapter {
     return copyOfChoices;
   }
 
-  // --- Functions related to cycle detection
+  // --- Functions related to cycle detection and reachability graph
 
   // Detect cycles in the current execution/trace
   // We terminate the execution iff:
@@ -569,6 +567,23 @@ public class DPORStateReducer extends ListenerAdapter {
     }
   }
 
+  private void saveExecutionToRGraph(int stateId) {
+    // Save execution state into the reachability graph 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) {
+      ArrayList<Execution> reachableExecutions;
+      if (!prevVisitedStates.contains(stateId)) {
+        reachableExecutions = new ArrayList<>();
+        rGraph.put(stateId, reachableExecutions);
+      } else {
+        reachableExecutions = rGraph.get(stateId);
+      }
+      reachableExecutions.add(currentExecution);
+    }
+  }
+
   private boolean terminateCurrentExecution() {
     // We need to check all the states that have just been visited
     // Often a transition (choice/event) can result into forwarding/backtracking to a number of states
@@ -589,25 +604,9 @@ public class DPORStateReducer extends ListenerAdapter {
       HashSet<Integer> eventSet = new HashSet<>();
       stateToEventMap.put(stateId, eventSet);
     }
-    // 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
-    // TODO: New algorithm
-/*    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);
-    }
+    saveExecutionToRGraph(stateId);
     stateToChoiceCounterMap.put(stateId, choiceCounter);
-    analyzeReachabilityAndCreateBacktrackPoints(search.getVM(), stateId);*/
+    analyzeReachabilityAndCreateBacktrackPoints(search.getVM(), stateId);
     justVisitedStates.add(stateId);
     currVisitedStates.add(stateId);
   }
@@ -835,15 +834,15 @@ public class DPORStateReducer extends ListenerAdapter {
         }
       }
       // Check if a conflict is found
-      if (isConflictFound(nextInsn, pastChoice, execution, currentChoice, fieldClass)) {
+      if (isConflictFound(nextInsn, fieldClass, currentChoice, pastChoice, execution)) {
         createBacktrackingPoint(currentChoice, pastChoice, execution);
         break;  // Stop at the first found conflict
       }
     }
   }
 
-  private boolean isConflictFound(Instruction nextInsn, int pastChoice, Execution pastExecution,
-                                  int currentChoice, String fieldClass) {
+  private boolean isConflictFound(Instruction nextInsn, String fieldClass, int currentChoice,
+                                  int pastChoice, Execution pastExecution) {
 
     HashMap<Integer, ReadWriteSet> pastRWFieldsMap = pastExecution.getReadWriteFieldsMap();
     ArrayList<BacktrackPoint> pastTrace = pastExecution.getExecutionTrace();
@@ -867,64 +866,39 @@ public class DPORStateReducer extends ListenerAdapter {
     return false;
   }
 
-  //  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) ||
-//            currActualChoice == backtrackPointList.get(eventCounter).getChoice()) {
-//      return false;
-//    }
-//    // Current R/W set
-//    ReadWriteSet currRWSet = readWriteFieldsMap.get(currentChoice);
-//    // R/W set of choice/event that may have a potential conflict
-//    ReadWriteSet evtRWSet = readWriteFieldsMap.get(eventCounter);
-//    // Check for conflicts with Read and Write fields for Write instructions
-//    Set<String> currWriteSet = currRWSet.getWriteSet();
-//    for(String writeField : currWriteSet) {
-//      int currObjId = currRWSet.writeFieldObjectId(writeField);
-//      if ((evtRWSet.readFieldExists(writeField) && evtRWSet.readFieldObjectId(writeField) == currObjId) ||
-//          (evtRWSet.writeFieldExists(writeField) && evtRWSet.writeFieldObjectId(writeField) == currObjId)) {
-//        return true;
-//      }
-//    }
-//    // Check for conflicts with Write fields for Read instructions
-//    Set<String> currReadSet = currRWSet.getReadSet();
-//    for(String readField : currReadSet) {
-//      int currObjId = currRWSet.readFieldObjectId(readField);
-//      if (evtRWSet.writeFieldExists(readField) && evtRWSet.writeFieldObjectId(readField) == currObjId) {
-//        return true;
-//      }
-//    }
-//    // Return false if no conflict is found
-//    return false;
-//  }
+  private boolean isConflictFound(int currentChoice, int reachableEvent, Execution execution) {
 
-//  private boolean isConflictFound(Instruction nextInsn, int eventCounter, int currentChoice, String fieldClass) {
-//
-//    int actualCurrCho = currentChoice % refChoices.length;
-//    // 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) ||
-//         choices[actualCurrCho] == backtrackPointList.get(eventCounter).getChoice()) {
-//      return false;
-//    }
-//    ReadWriteSet rwSet = readWriteFieldsMap.get(eventCounter);
-//    int currObjId = ((JVMFieldInstruction) nextInsn).getFieldInfo().getClassInfo().getClassObjectRef();
-//    // Check for conflicts with Write fields for both Read and Write instructions
-//    if (((nextInsn instanceof WriteInstruction || nextInsn instanceof ReadInstruction) &&
-//          rwSet.writeFieldExists(fieldClass) && rwSet.writeFieldObjectId(fieldClass) == currObjId) ||
-//         (nextInsn instanceof WriteInstruction && rwSet.readFieldExists(fieldClass) &&
-//          rwSet.readFieldObjectId(fieldClass) == currObjId)) {
-//      return true;
-//    }
-//    return false;
-//  }
+    ArrayList<BacktrackPoint> executionTrace = execution.getExecutionTrace();
+    HashMap<Integer, ReadWriteSet> execRWFieldsMap = execution.getReadWriteFieldsMap();
+    // Skip if this event does not have any Read/Write set or the two events are basically the same event (number)
+    if (!execRWFieldsMap.containsKey(reachableEvent) ||
+            executionTrace.get(currentChoice).getChoice() == executionTrace.get(reachableEvent).getChoice()) {
+      return false;
+    }
+    // Current R/W set
+    ReadWriteSet currRWSet = execRWFieldsMap.get(currentChoice);
+    // R/W set of choice/event that may have a potential conflict
+    ReadWriteSet evtRWSet = execRWFieldsMap.get(reachableEvent);
+    // Check for conflicts with Read and Write fields for Write instructions
+    Set<String> currWriteSet = currRWSet.getWriteSet();
+    for(String writeField : currWriteSet) {
+      int currObjId = currRWSet.writeFieldObjectId(writeField);
+      if ((evtRWSet.readFieldExists(writeField) && evtRWSet.readFieldObjectId(writeField) == currObjId) ||
+              (evtRWSet.writeFieldExists(writeField) && evtRWSet.writeFieldObjectId(writeField) == currObjId)) {
+        return true;
+      }
+    }
+    // Check for conflicts with Write fields for Read instructions
+    Set<String> currReadSet = currRWSet.getReadSet();
+    for(String readField : currReadSet) {
+      int currObjId = currRWSet.readFieldObjectId(readField);
+      if (evtRWSet.writeFieldExists(readField) && evtRWSet.writeFieldObjectId(readField) == currObjId) {
+        return true;
+      }
+    }
+    // Return false if no conflict is found
+    return false;
+  }
 
   private ReadWriteSet getReadWriteSet(int currentChoice) {
     // Do the analysis to get Read and Write accesses to fields
@@ -1059,19 +1033,18 @@ public class DPORStateReducer extends ListenerAdapter {
 
   // 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
-//    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, false)) {
-////          && isNewConflict(conflictChoice, eventCounter)) {
-//          createBacktrackingPoint(conflictChoice, eventCounter, false);
-//        }
-//      }
-//      conflictChoice++;
-//    }
+    // Find the choice/event that marks the start of this cycle: first choice we explore for conflicts
+    int currentChoice = stateToChoiceCounterMap.get(stateId);
+    int cycleEndChoice = choiceCounter - 1;
+    // Find conflicts between choices/events in this cycle (we scan forward in the cycle, not backward)
+    while (currentChoice < cycleEndChoice) {
+      for (int reachableEvent = currentChoice + 1; reachableEvent <= cycleEndChoice; reachableEvent++) {
+        if (isConflictFound(currentChoice, reachableEvent, currentExecution)) {
+          createBacktrackingPoint(currentChoice, reachableEvent, currentExecution);
+        }
+      }
+      currentChoice++;
+    }
   }
 
   // TODO: OPTIMIZATION!
@@ -1098,47 +1071,48 @@ public class DPORStateReducer extends ListenerAdapter {
 
   // Update the backtrack sets in a previous execution
   private void updateBacktrackSetsInPreviousExecution(int stateId) {
-//    // 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);
-//        }
-//      }
-//    }
+    // Don't check a past trace twice!
+    HashSet<Execution> 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<Execution> rExecutions = rGraph.get(stId);
+      for (Execution rExecution : rExecutions) {
+        if (!checkedTrace.contains(rExecution)) {
+          // Find the choice/event that marks the start of the subtrace from the previous execution
+          ArrayList<BacktrackPoint> pastExecutionTrace = rExecution.getExecutionTrace();
+          HashMap<Integer, ReadWriteSet> pastReadWriteFieldsMap = rExecution.getReadWriteFieldsMap();
+          int pastConfChoice = getPastConflictChoice(stId, pastExecutionTrace);
+          int conflictChoice = choiceCounter;
+          // Iterate from the starting point until the end of the past execution trace
+          while (pastConfChoice < pastExecutionTrace.size() - 1) {  // BacktrackPoint list always has a surplus of 1
+            // Get the info of the event from the past execution trace
+            BacktrackPoint confBtrackPoint = pastExecutionTrace.get(pastConfChoice);
+            if (isNotChecked(checkedStateIdAndChoice, confBtrackPoint)) {
+              ReadWriteSet rwSet = pastReadWriteFieldsMap.get(pastConfChoice);
+              // Append this event to the current list and map
+              ArrayList<BacktrackPoint> currentTrace = currentExecution.getExecutionTrace();
+              HashMap<Integer, ReadWriteSet> currRWFieldsMap = currentExecution.getReadWriteFieldsMap();
+              currentTrace.add(confBtrackPoint);
+              currRWFieldsMap.put(choiceCounter, rwSet);
+              for (int pastChoice = conflictChoice - 1; pastChoice >= 0; pastChoice--) {
+                if (isConflictFound(conflictChoice, pastChoice, rExecution)) {
+                  createBacktrackingPoint(conflictChoice, pastChoice, rExecution);
+                }
+              }
+              // Remove this event to replace it with a new one
+              currentTrace.remove(currentTrace.size() - 1);
+              currRWFieldsMap.remove(choiceCounter);
+            }
+            pastConfChoice++;
+          }
+          checkedTrace.add(rExecution);
+        }
+      }
+    }
   }
 }