From: rtrimana Date: Sat, 2 May 2020 15:25:49 +0000 (-0700) Subject: Fixing bugs: state to reachability graph map has to be updated for every new state... X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=commitdiff_plain;h=7d77b55b15ce4ebad33c8b5d2591ce701401bd7c Fixing bugs: state to reachability graph map has to be updated for every new state in the stateAdvanced method. --- diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java index 4645d2c..37ae774 100644 --- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java +++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java @@ -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 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 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 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 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 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= 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