X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2Fmain%2Fgov%2Fnasa%2Fjpf%2Flistener%2FDPORStateReducerWithSummary.java;fp=src%2Fmain%2Fgov%2Fnasa%2Fjpf%2Flistener%2FDPORStateReducerWithSummary.java;h=2026793494c74c2871a31a99a15856049326c2c5;hb=2491e80a7fdfc1a732836e568d6e075b51dbe443;hp=50e4061d936c74db7ec53aa37cb2298b8c1acef1;hpb=d7f927a163c3cf8f1ca1e136433ac3d52f6c0f54;p=jpf-core.git diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java b/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java index 50e4061..2026793 100755 --- a/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java +++ b/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java @@ -72,9 +72,10 @@ public class DPORStateReducerWithSummary extends ListenerAdapter { private PriorityQueue backtrackStateQ; // Heap that returns the latest state private Execution currentExecution; // Holds the information about the current execution private HashMap> doneBacktrackMap; // Record state ID and trace already constructed + private MainSummary mainSummary; // Main summary (M) for state ID, event, and R/W set + private HashMap stateToPredInfo; // Predecessor info indexed by state ID private HashMap 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 predecessors; // Maps incoming events/transitions (execution and choice) + private HashMap> recordedPredecessors; + // Memorize event and choice number to not record them twice + + public PredecessorInfo() { + predecessors = new HashSet<>(); + recordedPredecessors = new HashMap<>(); + } + + public HashSet getPredecessors() { + return predecessors; + } + + private boolean isRecordedPredecessor(Execution execution, int choice) { + // See if we have recorded this predecessor earlier + HashSet 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 predecessors; // Maps incoming events/transitions (execution and choice) - private HashMap> 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 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 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 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 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 getPredecessors(int stateId) { + // Get a set of predecessors for this state ID + HashSet 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 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 reachableTransitions = rGraph.getReachableTransitionsAtState(stateId); - for (TransitionEvent transition : reachableTransitions) { - transition.recordPredecessor(currentExecution, choiceCounter - 1); - } + // Record a new predecessor for a revisited state + addPredecessors(stateId); } } }