From: rtrimana Date: Tue, 19 May 2020 16:38:08 +0000 (-0700) Subject: Fixing a bug: need to get the right choice/event number for IntIntervalGenerator... X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=commitdiff_plain;h=ae8659b84395cdfa6accc01091d38a92ad9364c7;hp=c4889f13b870dd32124a09d1b840cb3ce4f66a99 Fixing a bug: need to get the right choice/event number for IntIntervalGenerator CGs. --- diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java index f4b5923..bc42a46 100644 --- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java +++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java @@ -80,7 +80,6 @@ public class DPORStateReducer extends ListenerAdapter { private HashSet doneBacktrackSet; // Record state ID and trace already constructed private HashMap restorableStateMap; // Maps state IDs to the restorable state object private HashMap stateToChoiceCounterMap; // Maps state IDs to the choice counter - //private HashMap> rGraph; // Create a reachability graph private HashMap> rGraph; // Create a reachability graph for past executions // Boolean states @@ -357,12 +356,14 @@ public class DPORStateReducer extends ListenerAdapter { // This class stores a representation of the execution graph node private class Execution { - private ArrayList executionTrace; // The BacktrackPoint objects of this execution + private HashMap cgToChoiceMap; // Map between CG to choice numbers for O(1) access + private ArrayList executionTrace; // The BacktrackPoint objects of this execution private int parentChoice; // The parent's choice that leads to this execution private Execution parent; // Store the parent for backward DFS to find conflicts private HashMap readWriteFieldsMap; // Record fields that are accessed public Execution() { + cgToChoiceMap = new HashMap<>(); executionTrace = new ArrayList<>(); parentChoice = -1; parent = null; @@ -373,10 +374,18 @@ public class DPORStateReducer extends ListenerAdapter { executionTrace.add(newBacktrackPoint); } + public void clearCGToChoiceMap() { + cgToChoiceMap = null; + } + public ArrayList getExecutionTrace() { return executionTrace; } + public int getChoiceFromCG(IntChoiceFromSet icsCG) { + return cgToChoiceMap.get(icsCG); + } + public int getParentChoice() { return parentChoice; } @@ -389,6 +398,10 @@ public class DPORStateReducer extends ListenerAdapter { return readWriteFieldsMap; } + public void mapCGToChoice(IntChoiceFromSet icsCG, int choice) { + cgToChoiceMap.put(icsCG, choice); + } + public void setParentChoice(int parChoice) { parentChoice = parChoice; } @@ -443,26 +456,6 @@ public class DPORStateReducer extends ListenerAdapter { } } - // This class stores a compact representation of a reachability graph for past executions -// private class ReachableTrace { -// private ArrayList pastBacktrackPointList; -// private HashMap pastReadWriteFieldsMap; -// -// public ReachableTrace(ArrayList btrackPointList, -// HashMap rwFieldsMap) { -// pastBacktrackPointList = btrackPointList; -// pastReadWriteFieldsMap = rwFieldsMap; -// } -// -// public ArrayList getPastBacktrackPointList() { -// return pastBacktrackPointList; -// } -// -// public HashMap getPastReadWriteFieldsMap() { -// return pastReadWriteFieldsMap; -// } -// } - // -- CONSTANTS private final static String DO_CALL_METHOD = "doCall"; // We exclude fields that come from libraries (Java and Groovy), and also the infrastructure @@ -498,6 +491,7 @@ public class DPORStateReducer extends ListenerAdapter { // Record state ID and choice/event as backtrack point int stateId = vm.getStateId(); currentExecution.addBacktrackPoint(new BacktrackPoint(icsCG, stateId, refChoices[choiceIndex])); + currentExecution.mapCGToChoice(icsCG, choiceCounter); // Store restorable state object for this state (always store the latest) RestorableVMState restorableState = vm.getRestorableState(); restorableStateMap.put(stateId, restorableState); @@ -696,8 +690,6 @@ public class DPORStateReducer extends ListenerAdapter { private int checkAndAdjustChoice(int currentChoice, VM vm) { // If current choice is not the same, then this is caused by the firing of IntIntervalGenerator // for certain method calls in the infrastructure, e.g., eventSince() - int currChoiceInd = currentChoice % refChoices.length; - int currChoiceFromCG = currChoiceInd; ChoiceGenerator currentCG = vm.getChoiceGenerator(); // This is the main event CG if (currentCG instanceof IntIntervalGenerator) { @@ -707,17 +699,8 @@ public class DPORStateReducer extends ListenerAdapter { while (!(parentCG instanceof IntChoiceFromSet)) { parentCG = ((IntIntervalGenerator) parentCG).getPreviousChoiceGenerator(); } - int actualEvtNum = ((IntChoiceFromSet) parentCG).getNextChoice(); - // Find the index of the event/choice in refChoices - for (int i = 0; i currTrace = currentExecution.getExecutionTrace(); // Skip if this event does not have any Read/Write set or the two events are basically the same event (number) if (!pastRWFieldsMap.containsKey(pastChoice) || - //choices[actualChoice] == pastTrace.get(pastChoice).getChoice()) { currTrace.get(currentChoice).getChoice() == pastTrace.get(pastChoice).getChoice()) { return false; } @@ -924,6 +904,7 @@ public class DPORStateReducer extends ListenerAdapter { return false; } + // Check if this trace is already constructed private boolean isTraceAlreadyConstructed(int firstChoice, int stateId) { // Concatenate state ID and only the first event in the string, e.g., "1:1 for the trace 10234 at state 1" // TODO: THIS IS AN OPTIMIZATION! @@ -942,6 +923,7 @@ public class DPORStateReducer extends ListenerAdapter { return false; } + // Reset data structure for each new execution private void resetStatesForNewExecution(IntChoiceFromSet icsCG, VM vm) { if (choices == null || choices != icsCG.getAllChoices()) { // Reset state variables @@ -956,6 +938,7 @@ public class DPORStateReducer extends ListenerAdapter { } } + // Set a backtrack point for a particular state private void setBacktrackCG(int stateId, IntChoiceFromSet backtrackCG) { // Set a backtrack CG based on a state ID LinkedList backtrackExecutions = backtrackMap.get(stateId); @@ -970,6 +953,8 @@ public class DPORStateReducer extends ListenerAdapter { ArrayList parentTrace = newExecution.getParent().getExecutionTrace(); newExecution.setParentChoice(parentTrace.size() - 1); } + // Try to free some memory since this map is only used for the current execution + currentExecution.clearCGToChoiceMap(); currentExecution = newExecution; // Remove from the queue if we don't have more backtrack points for that state if (backtrackExecutions.isEmpty()) { @@ -982,7 +967,7 @@ public class DPORStateReducer extends ListenerAdapter { // TODO: OPTIMIZATION! // Check and make sure that state ID and choice haven't been explored for this trace - private boolean alreadyChecked(HashSet checkedStateIdAndChoice, BacktrackPoint backtrackPoint) { + private boolean isAlreadyChecked(HashSet checkedStateIdAndChoice, BacktrackPoint backtrackPoint) { int stateId = backtrackPoint.getStateId(); int choice = backtrackPoint.getChoice(); StringBuilder sb = new StringBuilder(); @@ -1064,6 +1049,7 @@ public class DPORStateReducer extends ListenerAdapter { } } + // Update the backtrack sets in a previous execution private void updateBacktrackSetsInPreviousExecution(Execution rExecution, int stateId, HashSet checkedStateIdAndChoice) { // Find the choice/event that marks the start of the subtrace from the previous execution @@ -1075,7 +1061,7 @@ public class DPORStateReducer extends ListenerAdapter { while (pastConfChoice < pastExecutionTrace.size() - 1) { // BacktrackPoint list always has a surplus of 1 // Get the info of the event from the past execution trace BacktrackPoint confBtrackPoint = pastExecutionTrace.get(pastConfChoice); - if (!alreadyChecked(checkedStateIdAndChoice, confBtrackPoint)) { + if (!isAlreadyChecked(checkedStateIdAndChoice, confBtrackPoint)) { ReadWriteSet rwSet = pastReadWriteFieldsMap.get(pastConfChoice); // Append this event to the current list and map ArrayList currentTrace = currentExecution.getExecutionTrace(); @@ -1095,7 +1081,7 @@ public class DPORStateReducer extends ListenerAdapter { } } - // Update the backtrack sets in a previous execution + // Update the backtrack sets in previous executions private void updateBacktrackSetsInPreviousExecutions(int stateId) { // Don't check a past trace twice! HashSet checkedTrace = new HashSet<>();