Recording predecessors per state as opposed to per transition.
authorrtrimana <rtrimana@uci.edu>
Wed, 13 Jan 2021 20:09:43 +0000 (12:09 -0800)
committerrtrimana <rtrimana@uci.edu>
Wed, 13 Jan 2021 20:09:43 +0000 (12:09 -0800)
src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java

index 50e4061..2026793 100755 (executable)
@@ -72,9 +72,10 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
   private PriorityQueue<Integer> backtrackStateQ;                 // Heap that returns the latest state
   private Execution currentExecution;                             // Holds the information about the current execution
   private HashMap<Integer, HashSet<Integer>> doneBacktrackMap;    // Record state ID and trace already constructed
+  private MainSummary mainSummary;                                // Main summary (M) for state ID, event, and R/W set
+  private HashMap<Integer, PredecessorInfo> stateToPredInfo;      // Predecessor info indexed by state ID
   private HashMap<Integer, RestorableVMState> restorableStateMap; // Maps state IDs to the restorable state object
   private RGraph rGraph;                                          // R-Graph for past executions
-  private MainSummary mainSummary;                                // Main summary (M) for state ID, event, and R/W set
 
   // Boolean states
   private boolean isBooleanCGFlipped;
@@ -99,12 +100,13 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
       }
     }
     isBooleanCGFlipped = false;
+    mainSummary = new MainSummary();
                numOfTransitions = 0;
                nonRelevantClasses = new HashSet<>();
                nonRelevantFields = new HashSet<>();
                relevantFields = new HashSet<>();
     restorableStateMap = new HashMap<>();
-    mainSummary = new MainSummary();
+    stateToPredInfo = new HashMap<>();
     initializeStatesVariables();
   }
 
@@ -523,6 +525,48 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
     }
   }
 
+  // This class is a representation of a state.
+  // It stores the predecessors to a state.
+  // TODO: We also have stateToEventMap, restorableStateMap, and doneBacktrackMap that has state Id as HashMap key.
+  private class PredecessorInfo {
+    private HashSet<Predecessor> predecessors;  // Maps incoming events/transitions (execution and choice)
+    private HashMap<Execution, HashSet<Integer>> recordedPredecessors;
+                                                // Memorize event and choice number to not record them twice
+
+    public PredecessorInfo() {
+      predecessors = new HashSet<>();
+      recordedPredecessors = new HashMap<>();
+    }
+
+    public HashSet<Predecessor> getPredecessors() {
+      return predecessors;
+    }
+
+    private boolean isRecordedPredecessor(Execution execution, int choice) {
+      // See if we have recorded this predecessor earlier
+      HashSet<Integer> recordedChoices;
+      if (recordedPredecessors.containsKey(execution)) {
+        recordedChoices = recordedPredecessors.get(execution);
+        if (recordedChoices.contains(choice)) {
+          return true;
+        }
+      } else {
+        recordedChoices = new HashSet<>();
+        recordedPredecessors.put(execution, recordedChoices);
+      }
+      // Record the choice if we haven't seen it
+      recordedChoices.add(choice);
+
+      return false;
+    }
+
+    public void recordPredecessor(Execution execution, int choice) {
+      if (!isRecordedPredecessor(execution, choice)) {
+        predecessors.add(new Predecessor(choice, execution));
+      }
+    }
+  }
+
   // This class compactly stores transitions:
   // 1) CG,
   // 2) state ID,
@@ -532,9 +576,6 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
     private int choice;                        // Choice chosen at this transition
     private int choiceCounter;                 // Choice counter at this transition
     private Execution execution;               // The execution where this transition belongs
-    private HashSet<Predecessor> predecessors; // Maps incoming events/transitions (execution and choice)
-    private HashMap<Execution, HashSet<Integer>> recordedPredecessors;
-                                               // Memorize event and choice number to not record them twice
     private int stateId;                       // State at this transition
     private IntChoiceFromSet transitionCG;     // CG at this transition
 
@@ -542,8 +583,6 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
       choice = 0;
       choiceCounter = 0;
       execution = null;
-      predecessors = new HashSet<>();
-      recordedPredecessors = new HashMap<>();
       stateId = 0;
       transitionCG = null;
     }
@@ -560,40 +599,12 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
       return execution;
     }
 
-    public HashSet<Predecessor> getPredecessors() {
-      return predecessors;
-    }
-
     public int getStateId() {
       return stateId;
     }
 
     public IntChoiceFromSet getTransitionCG() { return transitionCG; }
 
-    private boolean isRecordedPredecessor(Execution execution, int choice) {
-      // See if we have recorded this predecessor earlier
-      HashSet<Integer> recordedChoices;
-      if (recordedPredecessors.containsKey(execution)) {
-        recordedChoices = recordedPredecessors.get(execution);
-        if (recordedChoices.contains(choice)) {
-          return true;
-        }
-      } else {
-        recordedChoices = new HashSet<>();
-        recordedPredecessors.put(execution, recordedChoices);
-      }
-      // Record the choice if we haven't seen it
-      recordedChoices.add(choice);
-
-      return false;
-    }
-
-    public void recordPredecessor(Execution execution, int choice) {
-      if (!isRecordedPredecessor(execution, choice)) {
-        predecessors.add(new Predecessor(choice, execution));
-      }
-    }
-
     public void setChoice(int cho) {
       choice = cho;
     }
@@ -606,10 +617,6 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
       execution = exec;
     }
 
-    public void setPredecessors(HashSet<Predecessor> preds) {
-      predecessors = new HashSet<>(preds);
-    }
-
     public void setStateId(int stId) {
       stateId = stId;
     }
@@ -765,14 +772,7 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
     } else {
       transition = new TransitionEvent();
       currentExecution.addTransition(transition);
-      transition.recordPredecessor(currentExecution, choiceCounter - 1);
-      // We have to check if there is a transition whose source state ID is the same
-      // If such exists, then we need to add its predecessors to the predecessor set of the current transition
-      for (TransitionEvent trans : rGraph.getReachableTransitionsAtState(stateId)) {
-        for (Predecessor pred : trans.getPredecessors()) {
-          transition.recordPredecessor(pred.getExecution(), pred.getChoice());
-        }
-      }
+      addPredecessors(stateId);
     }
     transition.setExecution(currentExecution);
     transition.setTransitionCG(icsCG);
@@ -814,16 +814,31 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
     choiceCounter = 0;
     maxEventChoice = 0;
     // Cycle tracking
-    currVisitedStates = new HashMap<>();
-    justVisitedStates = new HashSet<>();
-    prevVisitedStates = new HashSet<>();
-    stateToEventMap = new HashMap<>();
+    if (!isBooleanCGFlipped) {
+      currVisitedStates = new HashMap<>();
+      justVisitedStates = new HashSet<>();
+      prevVisitedStates = new HashSet<>();
+      stateToEventMap = new HashMap<>();
+    } else {
+      currVisitedStates.clear();
+      justVisitedStates.clear();
+      prevVisitedStates.clear();
+      stateToEventMap.clear();
+    }
     // Backtracking
-    backtrackMap = new HashMap<>();
+    if (!isBooleanCGFlipped) {
+      backtrackMap = new HashMap<>();
+    } else {
+      backtrackMap.clear();
+    }
     backtrackStateQ = new PriorityQueue<>(Collections.reverseOrder());
     currentExecution = new Execution();
     currentExecution.addTransition(new TransitionEvent()); // Always start with 1 backtrack point
-    doneBacktrackMap = new HashMap<>();
+    if (!isBooleanCGFlipped) {
+      doneBacktrackMap = new HashMap<>();
+    } else {
+      doneBacktrackMap.clear();
+    }
     rGraph = new RGraph();
     // Booleans
     isEndOfExecution = false;
@@ -853,7 +868,7 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
           updateBacktrackSetsFromGraph(stateId, currentExecution, choiceCounter - 1);
           terminate = true;
         }
-        // If frequency > 1 then this means we have visited this stateId more than once
+        // If frequency > 1 then this means we have visited this stateId more than once in the current execution
         if (currVisitedStates.containsKey(stateId) && currVisitedStates.get(stateId) > 1) {
           updateBacktrackSetsFromGraph(stateId, currentExecution, choiceCounter - 1);
         }
@@ -895,7 +910,6 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
     }
     // Add the new backtrack execution object
     TransitionEvent backtrackTransition = new TransitionEvent();
-    backtrackTransition.setPredecessors(conflictTransition.getPredecessors());
     backtrackExecList.addFirst(new BacktrackExecution(newChoiceList, backtrackTransition));
     // Add to priority queue
     if (!backtrackStateQ.contains(stateId)) {
@@ -903,6 +917,17 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
     }
   }
 
+  private void addPredecessors(int stateId) {
+    PredecessorInfo predecessorInfo;
+    if (!stateToPredInfo.containsKey(stateId)) {
+      predecessorInfo = new PredecessorInfo();
+      stateToPredInfo.put(stateId, predecessorInfo);
+    } else {  // This is a new state Id
+      predecessorInfo = stateToPredInfo.get(stateId);
+    }
+    predecessorInfo.recordPredecessor(currentExecution, choiceCounter - 1);
+  }
+
   // Analyze Read/Write accesses that are directly invoked on fields
   private void analyzeReadWriteAccesses(Instruction executedInsn, int currentChoice) {
     // Get the field info
@@ -1118,20 +1143,6 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
     return false;
   }
 
-  private ReadWriteSet getReadWriteSet(int currentChoice) {
-    // Do the analysis to get Read and Write accesses to fields
-    ReadWriteSet rwSet;
-    // We already have an entry
-    HashMap<Integer, ReadWriteSet> currReadWriteFieldsMap = currentExecution.getReadWriteFieldsMap();
-    if (currReadWriteFieldsMap.containsKey(currentChoice)) {
-      rwSet = currReadWriteFieldsMap.get(currentChoice);
-    } else { // We need to create a new entry
-      rwSet = new ReadWriteSet();
-      currReadWriteFieldsMap.put(currentChoice, rwSet);
-    }
-    return rwSet;
-  }
-
   private boolean isFieldExcluded(Instruction executedInsn) {
     // Get the field info
     FieldInfo fieldInfo = ((JVMFieldInstruction) executedInsn).getFieldInfo();
@@ -1176,6 +1187,33 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
     return false;
   }
 
+  private HashSet<Predecessor> getPredecessors(int stateId) {
+    // Get a set of predecessors for this state ID
+    HashSet<Predecessor> predecessors;
+    if (stateToPredInfo.containsKey(stateId)) {
+      PredecessorInfo predecessorInfo = stateToPredInfo.get(stateId);
+      predecessors = predecessorInfo.getPredecessors();
+    } else {
+      predecessors = new HashSet<>();
+    }
+
+    return predecessors;
+  }
+
+  private ReadWriteSet getReadWriteSet(int currentChoice) {
+    // Do the analysis to get Read and Write accesses to fields
+    ReadWriteSet rwSet;
+    // We already have an entry
+    HashMap<Integer, ReadWriteSet> currReadWriteFieldsMap = currentExecution.getReadWriteFieldsMap();
+    if (currReadWriteFieldsMap.containsKey(currentChoice)) {
+      rwSet = currReadWriteFieldsMap.get(currentChoice);
+    } else { // We need to create a new entry
+      rwSet = new ReadWriteSet();
+      currReadWriteFieldsMap.put(currentChoice, rwSet);
+    }
+    return rwSet;
+  }
+
   // Reset data structure for each new execution
   private void resetStatesForNewExecution(IntChoiceFromSet icsCG, VM vm) {
     if (choices == null || choices != icsCG.getAllChoices()) {
@@ -1184,8 +1222,8 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
       choices = icsCG.getAllChoices();
       refChoices = copyChoices(choices);
       // Clear data structures
-      currVisitedStates = new HashMap<>();
-      stateToEventMap = new HashMap<>();
+      currVisitedStates.clear();
+      stateToEventMap.clear();
       isEndOfExecution = false;
     }
   }
@@ -1244,7 +1282,7 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
     // Check the predecessors only if the set is not empty
     if (!currRWSet.isEmpty()) {
       // Explore all predecessors
-      for (Predecessor predecessor : currTrans.getPredecessors()) {
+      for (Predecessor predecessor : getPredecessors(currTrans.getStateId())) {
         // Get the predecessor (previous conflict choice)
         int predecessorChoice = predecessor.getChoice();
         Execution predecessorExecution = predecessor.getExecution();
@@ -1274,11 +1312,8 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
     if (!isEndOfExecution && choiceCounter > 1 && stateId > 0) {
       if ((currVisitedStates.containsKey(stateId) && currVisitedStates.get(stateId) > 1) ||
               prevVisitedStates.contains(stateId)) {
-        // Update reachable transitions in the graph with a predecessor
-        HashSet<TransitionEvent> reachableTransitions = rGraph.getReachableTransitionsAtState(stateId);
-        for (TransitionEvent transition : reachableTransitions) {
-          transition.recordPredecessor(currentExecution, choiceCounter - 1);
-        }
+        // Record a new predecessor for a revisited state
+        addPredecessors(stateId);
       }
     }
   }