Fixing bugs: the main one is to create a local copy of the set that contains accesses...

[jpf-core.git] / src / main / gov / nasa / jpf / listener / DPORStateReducerWithSummary.java

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java b/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java
index 39616d97fef3025d072ae95a3c0b339e5b32b5fc..50e4061d936c74db7ec53aa37cb2298b8c1acef1 100755 (executable)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java
@@ -259,7 +259,7 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
   public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
     if (stateReductionMode) {
       if (!isEndOfExecution) {
-        // Has to be initialized and a integer CG
+        // Has to be initialized and it is a integer CG
         ChoiceGenerator<?> cg = vm.getChoiceGenerator();
         if (cg instanceof IntChoiceFromSet || cg instanceof IntIntervalGenerator) {
           int currentChoice = choiceCounter - 1;  // Accumulative choice w.r.t the current trace
@@ -632,7 +632,8 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
 
     public Set<Integer> getEventChoicesAtStateId(int stateId) {
       HashMap<Integer, ReadWriteSet> stateSummary = mainSummary.get(stateId);
-      return stateSummary.keySet();
+      // Return a new set since this might get updated concurrently
+      return new HashSet<>(stateSummary.keySet());
     }
 
     public ReadWriteSet getRWSetForEventChoiceAtState(int eventChoice, int stateId) {
@@ -640,6 +641,10 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
       return stateSummary.get(eventChoice);
     }
 
+    public Set<Integer> getStateIds() {
+      return mainSummary.keySet();
+    }
+
     private ReadWriteSet performUnion(ReadWriteSet recordedRWSet, ReadWriteSet rwSet) {
       // Combine the same write accesses and record in the recordedRWSet
       HashMap<String, Integer> recordedWriteMap = recordedRWSet.getWriteMap();
@@ -761,6 +766,13 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
       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());
+        }
+      }
     }
     transition.setExecution(currentExecution);
     transition.setTransitionCG(icsCG);
@@ -831,15 +843,20 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
     // 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
     boolean terminate = false;
+    Set<Integer> mainStateIds = mainSummary.getStateIds();
     for(Integer stateId : justVisitedStates) {
-      // We perform updates on backtrack sets for every
-      if (prevVisitedStates.contains(stateId) || completeFullCycle(stateId)) {
-        updateBacktrackSetsFromGraph(stateId, currentExecution, choiceCounter - 1);
-        terminate = true;
-      }
-      // If frequency > 1 then this means we have visited this stateId more than once
-      if (currVisitedStates.containsKey(stateId) && currVisitedStates.get(stateId) > 1) {
-        updateBacktrackSetsFromGraph(stateId, currentExecution, choiceCounter - 1);
+      // We exclude states that are produced by other CGs that are not integer CG
+      // When we encounter these states, then we should also encounter the corresponding integer CG state ID
+      if (mainStateIds.contains(stateId)) {
+        // We perform updates on backtrack sets for every
+        if (prevVisitedStates.contains(stateId) || completeFullCycle(stateId)) {
+          updateBacktrackSetsFromGraph(stateId, currentExecution, choiceCounter - 1);
+          terminate = true;
+        }
+        // If frequency > 1 then this means we have visited this stateId more than once
+        if (currVisitedStates.containsKey(stateId) && currVisitedStates.get(stateId) > 1) {
+          updateBacktrackSetsFromGraph(stateId, currentExecution, choiceCounter - 1);
+        }
       }
     }
     return terminate;
@@ -1224,26 +1241,26 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
       return;
     }
     visited.add(currTrans);
-    // Halt if the set is empty
-    if (currRWSet.isEmpty()) {
-      return;
-    }
-    // Explore all predecessors
-    for (Predecessor predecessor : currTrans.getPredecessors()) {
-      // Get the predecessor (previous conflict choice)
-      int predecessorChoice = predecessor.getChoice();
-      Execution predecessorExecution = predecessor.getExecution();
-      // Push up one happens-before transition
-      int newConflictEventChoice = conflictEventChoice;
-      // Check if a conflict is found
-      if (isConflictFound(conflictEventChoice, predecessorExecution, predecessorChoice, currRWSet)) {
-        createBacktrackingPoint(conflictEventChoice, predecessorExecution, predecessorChoice);
-        // We need to extract the pushed happens-before event choice from the predecessor execution and choice
-        newConflictEventChoice = predecessorExecution.getExecutionTrace().get(predecessorChoice).getChoice();
+    // Check the predecessors only if the set is not empty
+    if (!currRWSet.isEmpty()) {
+      // Explore all predecessors
+      for (Predecessor predecessor : currTrans.getPredecessors()) {
+        // Get the predecessor (previous conflict choice)
+        int predecessorChoice = predecessor.getChoice();
+        Execution predecessorExecution = predecessor.getExecution();
+        // Push up one happens-before transition
+        int newConflictEventChoice = conflictEventChoice;
+        // Check if a conflict is found
+        ReadWriteSet newCurrRWSet = currRWSet.getCopy();
+        if (isConflictFound(conflictEventChoice, predecessorExecution, predecessorChoice, newCurrRWSet)) {
+          createBacktrackingPoint(conflictEventChoice, predecessorExecution, predecessorChoice);
+          // We need to extract the pushed happens-before event choice from the predecessor execution and choice
+          newConflictEventChoice = predecessorExecution.getExecutionTrace().get(predecessorChoice).getChoice();
+        }
+        // Continue performing DFS if conflict is not found
+        updateBacktrackSetDFS(predecessorExecution, predecessorChoice, newConflictEventChoice,
+                newCurrRWSet, visited);
       }
-      // Continue performing DFS if conflict is not found
-      updateBacktrackSetDFS(predecessorExecution, predecessorChoice, newConflictEventChoice,
-              currRWSet, visited);
     }
   }