Fixing a bug: in the second round of boolean CG, we might encounter states in the...

[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 fe4132f5386075d7cebb42ec467677a047bdfecb..3e387a95e3234d82c4b482aab56b02e9b3fb2b8f 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@ -196,6 +196,8 @@ public class DPORStateReducer extends ListenerAdapter {
       // Initialize with necessary information from the CG
       if (nextCG instanceof IntChoiceFromSet) {
         IntChoiceFromSet icsCG = (IntChoiceFromSet) nextCG;
+        // Tell JPF that we are performing DPOR
+        icsCG.setDpor();
         if (!isEndOfExecution) {
           // Check if CG has been initialized, otherwise initialize it
           Integer[] cgChoices = icsCG.getAllChoices();
@@ -324,14 +326,12 @@ public class DPORStateReducer extends ListenerAdapter {
     private ArrayList<TransitionEvent> executionTrace;          // The BacktrackPoint objects of this execution
     private boolean isNew;                                      // Track if this is the first time it is accessed
     private HashMap<Integer, ReadWriteSet> readWriteFieldsMap;  // Record fields that are accessed
-    private HashMap<Integer, TransitionEvent> stateToTransitionMap;  // For O(1) access to backtrack point
 
     public Execution() {
       cgToChoiceMap = new HashMap<>();
       executionTrace = new ArrayList<>();
       isNew = true;
       readWriteFieldsMap = new HashMap<>();
-      stateToTransitionMap = new HashMap<>();
     }
 
     public void addTransition(TransitionEvent newBacktrackPoint) {
@@ -354,16 +354,12 @@ public class DPORStateReducer extends ListenerAdapter {
       return executionTrace.get(0);
     }
 
-    public HashMap<Integer, ReadWriteSet> getReadWriteFieldsMap() {
-      return readWriteFieldsMap;
+    public TransitionEvent getLastTransition() {
+      return executionTrace.get(executionTrace.size() - 1);
     }
 
-    public TransitionEvent getTransitionFromState(int stateId) {
-      if (stateToTransitionMap.containsKey(stateId)) {
-        return stateToTransitionMap.get(stateId);
-      }
-      // Return the latest transition for unseen states (that have just been encountered in this transition)
-      return executionTrace.get(executionTrace.size() - 1);
+    public HashMap<Integer, ReadWriteSet> getReadWriteFieldsMap() {
+      return readWriteFieldsMap;
     }
 
     public boolean isNew() {
@@ -378,10 +374,6 @@ public class DPORStateReducer extends ListenerAdapter {
     public void mapCGToChoice(IntChoiceFromSet icsCG, int choice) {
       cgToChoiceMap.put(icsCG, choice);
     }
-
-    public void mapStateToTransition(int stateId, TransitionEvent transition) {
-      stateToTransitionMap.put(stateId, transition);
-    }
   }
 
   // This class compactly stores a predecessor
@@ -435,6 +427,12 @@ public class DPORStateReducer extends ListenerAdapter {
     }
 
     public HashSet<TransitionEvent> getReachableTransitionsAtState(int stateId) {
+      if (!graph.containsKey(stateId)) {
+        // This is a loop from a transition to itself, so just return the current transition
+        HashSet<TransitionEvent> transitionSet = new HashSet<>();
+        transitionSet.add(currentExecution.getLastTransition());
+        return transitionSet;
+      }
       return graph.get(stateId);
     }
 
@@ -442,7 +440,11 @@ public class DPORStateReducer extends ListenerAdapter {
       HashSet<TransitionEvent> reachableTransitions = new HashSet<>();
       // All transitions from states higher than the given state ID (until the highest state ID) are reachable
       for(int stId = stateId; stId <= hiStateId; stId++) {
-        reachableTransitions.addAll(graph.get(stId));
+        // We might encounter state IDs from the first round of Boolean CG
+        // The second round of Boolean CG should consider these new states
+        if (graph.containsKey(stId)) {
+          reachableTransitions.addAll(graph.get(stId));
+        }
       }
       return reachableTransitions;
     }
@@ -647,7 +649,6 @@ public class DPORStateReducer extends ListenerAdapter {
     // Add new transition to the current execution and map it in R-Graph
     for (Integer stId : justVisitedStates) {  // Map this transition to all the previously passed states
       rGraph.addReachableTransition(stId, transition);
-      currentExecution.mapStateToTransition(stId, transition);
     }
     currentExecution.mapCGToChoice(icsCG, choiceCounter);
     // Store restorable state object for this state (always store the latest)
@@ -1169,6 +1170,9 @@ public class DPORStateReducer extends ListenerAdapter {
       updateBacktrackSetRecursive(execution, currentChoice, conflictExecution, conflictChoice,
               pushedExecution, pushedChoice, currRWSet, visited);
     }
+    // Remove the transition after being explored
+    // TODO: Seems to cause a lot of loops---commented out for now
+    //visited.remove(confTrans);
   }
 
   // --- Functions related to the reachability analysis when there is a state match
@@ -1179,13 +1183,8 @@ public class DPORStateReducer extends ListenerAdapter {
     // 2) at least 2 choices/events have been explored (choiceCounter > 1),
     // 3) state > 0 (state 0 is for boolean CG)
     if (!isEndOfExecution && choiceCounter > 1 && stateId > 0) {
-      if (currVisitedStates.contains(stateId)) {
-        // Get the backtrack point from the current execution
-        TransitionEvent transition = currentExecution.getTransitionFromState(stateId);
-        transition.recordPredecessor(currentExecution, choiceCounter - 1);
-        updateBacktrackSetsFromPreviousExecution(stateId);
-      } else if (prevVisitedStates.contains(stateId)) { // We visit a state in a previous execution
-        // Update past executions with a predecessor
+      if (currVisitedStates.contains(stateId) || 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);