From 10ed69b94bee3bb11581d43aa884f667e240ff15 Mon Sep 17 00:00:00 2001 From: rtrimana Date: Thu, 14 May 2020 16:36:02 -0700 Subject: [PATCH] Adjusting support methods for reachability analysis with the new algorithm; untested yet. --- .../nasa/jpf/listener/DPORStateReducer.java | 286 ++++++++---------- 1 file changed, 130 insertions(+), 156 deletions(-) diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java index bf06232..ee61c19 100644 --- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java +++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java @@ -80,7 +80,8 @@ 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 + private HashMap> rGraph; // Create a reachability graph for past executions // Boolean states private boolean isBooleanCGFlipped; @@ -442,27 +443,25 @@ 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; - } - } +// 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"; @@ -498,7 +497,6 @@ public class DPORStateReducer extends ListenerAdapter { } // Record state ID and choice/event as backtrack point int stateId = vm.getStateId(); -// backtrackPointList.add(new BacktrackPoint(icsCG, stateId, refChoices[choiceIndex])); currentExecution.addBacktrackPoint(new BacktrackPoint(icsCG, stateId, refChoices[choiceIndex])); // Store restorable state object for this state (always store the latest) RestorableVMState restorableState = vm.getRestorableState(); @@ -512,7 +510,7 @@ public class DPORStateReducer extends ListenerAdapter { return copyOfChoices; } - // --- Functions related to cycle detection + // --- Functions related to cycle detection and reachability graph // Detect cycles in the current execution/trace // We terminate the execution iff: @@ -569,6 +567,23 @@ public class DPORStateReducer extends ListenerAdapter { } } + private void saveExecutionToRGraph(int stateId) { + // Save execution state into the reachability graph only if + // (1) It is not a revisited state from a past execution, or + // (2) It is just a new backtracking point + if (!prevVisitedStates.contains(stateId) || + choiceCounter <= 1) { + ArrayList reachableExecutions; + if (!prevVisitedStates.contains(stateId)) { + reachableExecutions = new ArrayList<>(); + rGraph.put(stateId, reachableExecutions); + } else { + reachableExecutions = rGraph.get(stateId); + } + reachableExecutions.add(currentExecution); + } + } + private boolean terminateCurrentExecution() { // 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 @@ -589,25 +604,9 @@ public class DPORStateReducer extends ListenerAdapter { HashSet eventSet = new HashSet<>(); stateToEventMap.put(stateId, eventSet); } - // Save execution state into the Reachability only if - // (1) It is not a revisited state from a past execution, or - // (2) It is just a new backtracking point - // TODO: New algorithm -/* if (!prevVisitedStates.contains(stateId) || - choiceCounter <= 1) { - ReachableTrace reachableTrace= new - ReachableTrace(backtrackPointList, readWriteFieldsMap); - ArrayList rTrace; - if (!prevVisitedStates.contains(stateId)) { - rTrace = new ArrayList<>(); - rGraph.put(stateId, rTrace); - } else { - rTrace = rGraph.get(stateId); - } - rTrace.add(reachableTrace); - } + saveExecutionToRGraph(stateId); stateToChoiceCounterMap.put(stateId, choiceCounter); - analyzeReachabilityAndCreateBacktrackPoints(search.getVM(), stateId);*/ + analyzeReachabilityAndCreateBacktrackPoints(search.getVM(), stateId); justVisitedStates.add(stateId); currVisitedStates.add(stateId); } @@ -835,15 +834,15 @@ public class DPORStateReducer extends ListenerAdapter { } } // Check if a conflict is found - if (isConflictFound(nextInsn, pastChoice, execution, currentChoice, fieldClass)) { + if (isConflictFound(nextInsn, fieldClass, currentChoice, pastChoice, execution)) { createBacktrackingPoint(currentChoice, pastChoice, execution); break; // Stop at the first found conflict } } } - private boolean isConflictFound(Instruction nextInsn, int pastChoice, Execution pastExecution, - int currentChoice, String fieldClass) { + private boolean isConflictFound(Instruction nextInsn, String fieldClass, int currentChoice, + int pastChoice, Execution pastExecution) { HashMap pastRWFieldsMap = pastExecution.getReadWriteFieldsMap(); ArrayList pastTrace = pastExecution.getExecutionTrace(); @@ -867,64 +866,39 @@ public class DPORStateReducer extends ListenerAdapter { return false; } - // 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) || -// currActualChoice == backtrackPointList.get(eventCounter).getChoice()) { -// return false; -// } -// // Current R/W set -// ReadWriteSet currRWSet = readWriteFieldsMap.get(currentChoice); -// // R/W set of choice/event that may have a potential conflict -// ReadWriteSet evtRWSet = readWriteFieldsMap.get(eventCounter); -// // Check for conflicts with Read and Write fields for Write instructions -// Set currWriteSet = currRWSet.getWriteSet(); -// for(String writeField : currWriteSet) { -// int currObjId = currRWSet.writeFieldObjectId(writeField); -// if ((evtRWSet.readFieldExists(writeField) && evtRWSet.readFieldObjectId(writeField) == currObjId) || -// (evtRWSet.writeFieldExists(writeField) && evtRWSet.writeFieldObjectId(writeField) == currObjId)) { -// return true; -// } -// } -// // Check for conflicts with Write fields for Read instructions -// Set currReadSet = currRWSet.getReadSet(); -// for(String readField : currReadSet) { -// int currObjId = currRWSet.readFieldObjectId(readField); -// if (evtRWSet.writeFieldExists(readField) && evtRWSet.writeFieldObjectId(readField) == currObjId) { -// return true; -// } -// } -// // Return false if no conflict is found -// return false; -// } + private boolean isConflictFound(int currentChoice, int reachableEvent, Execution execution) { -// private boolean isConflictFound(Instruction nextInsn, int eventCounter, int currentChoice, String fieldClass) { -// -// int actualCurrCho = currentChoice % refChoices.length; -// // 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) || -// choices[actualCurrCho] == backtrackPointList.get(eventCounter).getChoice()) { -// return false; -// } -// ReadWriteSet rwSet = readWriteFieldsMap.get(eventCounter); -// int currObjId = ((JVMFieldInstruction) nextInsn).getFieldInfo().getClassInfo().getClassObjectRef(); -// // Check for conflicts with Write fields for both Read and Write instructions -// if (((nextInsn instanceof WriteInstruction || nextInsn instanceof ReadInstruction) && -// rwSet.writeFieldExists(fieldClass) && rwSet.writeFieldObjectId(fieldClass) == currObjId) || -// (nextInsn instanceof WriteInstruction && rwSet.readFieldExists(fieldClass) && -// rwSet.readFieldObjectId(fieldClass) == currObjId)) { -// return true; -// } -// return false; -// } + ArrayList executionTrace = execution.getExecutionTrace(); + HashMap execRWFieldsMap = execution.getReadWriteFieldsMap(); + // Skip if this event does not have any Read/Write set or the two events are basically the same event (number) + if (!execRWFieldsMap.containsKey(reachableEvent) || + executionTrace.get(currentChoice).getChoice() == executionTrace.get(reachableEvent).getChoice()) { + return false; + } + // Current R/W set + ReadWriteSet currRWSet = execRWFieldsMap.get(currentChoice); + // R/W set of choice/event that may have a potential conflict + ReadWriteSet evtRWSet = execRWFieldsMap.get(reachableEvent); + // Check for conflicts with Read and Write fields for Write instructions + Set currWriteSet = currRWSet.getWriteSet(); + for(String writeField : currWriteSet) { + int currObjId = currRWSet.writeFieldObjectId(writeField); + if ((evtRWSet.readFieldExists(writeField) && evtRWSet.readFieldObjectId(writeField) == currObjId) || + (evtRWSet.writeFieldExists(writeField) && evtRWSet.writeFieldObjectId(writeField) == currObjId)) { + return true; + } + } + // Check for conflicts with Write fields for Read instructions + Set currReadSet = currRWSet.getReadSet(); + for(String readField : currReadSet) { + int currObjId = currRWSet.readFieldObjectId(readField); + if (evtRWSet.writeFieldExists(readField) && evtRWSet.writeFieldObjectId(readField) == currObjId) { + return true; + } + } + // Return false if no conflict is found + return false; + } private ReadWriteSet getReadWriteSet(int currentChoice) { // Do the analysis to get Read and Write accesses to fields @@ -1059,19 +1033,18 @@ public class DPORStateReducer extends ListenerAdapter { // 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 -// int conflictChoice = stateToChoiceCounterMap.get(stateId); -// int currentChoice = choiceCounter - 1; -// // 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, false)) { -//// && isNewConflict(conflictChoice, eventCounter)) { -// createBacktrackingPoint(conflictChoice, eventCounter, false); -// } -// } -// conflictChoice++; -// } + // Find the choice/event that marks the start of this cycle: first choice we explore for conflicts + int currentChoice = stateToChoiceCounterMap.get(stateId); + int cycleEndChoice = choiceCounter - 1; + // Find conflicts between choices/events in this cycle (we scan forward in the cycle, not backward) + while (currentChoice < cycleEndChoice) { + for (int reachableEvent = currentChoice + 1; reachableEvent <= cycleEndChoice; reachableEvent++) { + if (isConflictFound(currentChoice, reachableEvent, currentExecution)) { + createBacktrackingPoint(currentChoice, reachableEvent, currentExecution); + } + } + currentChoice++; + } } // TODO: OPTIMIZATION! @@ -1098,47 +1071,48 @@ public class DPORStateReducer extends ListenerAdapter { // Update the backtrack sets in a previous execution private void updateBacktrackSetsInPreviousExecution(int stateId) { -// // Don't check a past trace twice! -// HashSet checkedTrace = new HashSet<>(); -// // Don't check the same event twice for a revisited state -// HashMap> checkedStateIdAndChoice = new HashMap<>(); -// // Get sorted reachable state IDs -// ArrayList reachableStateIds = getReachableStateIds(rGraph.keySet(), stateId); -// // Iterate from this state ID until the biggest state ID -// for(Integer stId : reachableStateIds) { -// // Find the right reachability graph object that contains the stateId -// ArrayList rTraces = rGraph.get(stId); -// for (ReachableTrace rTrace : rTraces) { -// if (!checkedTrace.contains(rTrace)) { -// // Find the choice/event that marks the start of the subtrace from the previous execution -// ArrayList pastBacktrackPointList = rTrace.getPastBacktrackPointList(); -// HashMap pastReadWriteFieldsMap = rTrace.getPastReadWriteFieldsMap(); -// int pastConfChoice = getPastConflictChoice(stId, pastBacktrackPointList); -// int conflictChoice = choiceCounter; -// // Iterate from the starting point until the end of the past execution trace -// while (pastConfChoice < pastBacktrackPointList.size() - 1) { // BacktrackPoint list always has a surplus of 1 -// // Get the info of the event from the past execution trace -// BacktrackPoint confBtrackPoint = pastBacktrackPointList.get(pastConfChoice); -// if (isNotChecked(checkedStateIdAndChoice, confBtrackPoint)) { -// ReadWriteSet rwSet = pastReadWriteFieldsMap.get(pastConfChoice); -// // Append this event to the current list and map -// backtrackPointList.add(confBtrackPoint); -// readWriteFieldsMap.put(choiceCounter, rwSet); -// for (int eventCounter = conflictChoice - 1; eventCounter >= 0; eventCounter--) { -// if (isConflictFound(eventCounter, conflictChoice, true)) { -// && isNewConflict(conflictChoice, eventCounter)) { -// createBacktrackingPoint(conflictChoice, eventCounter, true); -// } -// } -// // Remove this event to replace it with a new one -// backtrackPointList.remove(backtrackPointList.size() - 1); -// readWriteFieldsMap.remove(choiceCounter); -// } -// pastConfChoice++; -// } -// checkedTrace.add(rTrace); -// } -// } -// } + // Don't check a past trace twice! + HashSet checkedTrace = new HashSet<>(); + // Don't check the same event twice for a revisited state + HashMap> checkedStateIdAndChoice = new HashMap<>(); + // Get sorted reachable state IDs + ArrayList reachableStateIds = getReachableStateIds(rGraph.keySet(), stateId); + // Iterate from this state ID until the biggest state ID + for(Integer stId : reachableStateIds) { + // Find the right reachability graph object that contains the stateId + ArrayList rExecutions = rGraph.get(stId); + for (Execution rExecution : rExecutions) { + if (!checkedTrace.contains(rExecution)) { + // Find the choice/event that marks the start of the subtrace from the previous execution + ArrayList pastExecutionTrace = rExecution.getExecutionTrace(); + HashMap pastReadWriteFieldsMap = rExecution.getReadWriteFieldsMap(); + int pastConfChoice = getPastConflictChoice(stId, pastExecutionTrace); + int conflictChoice = choiceCounter; + // Iterate from the starting point until the end of the past execution trace + 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 (isNotChecked(checkedStateIdAndChoice, confBtrackPoint)) { + ReadWriteSet rwSet = pastReadWriteFieldsMap.get(pastConfChoice); + // Append this event to the current list and map + ArrayList currentTrace = currentExecution.getExecutionTrace(); + HashMap currRWFieldsMap = currentExecution.getReadWriteFieldsMap(); + currentTrace.add(confBtrackPoint); + currRWFieldsMap.put(choiceCounter, rwSet); + for (int pastChoice = conflictChoice - 1; pastChoice >= 0; pastChoice--) { + if (isConflictFound(conflictChoice, pastChoice, rExecution)) { + createBacktrackingPoint(conflictChoice, pastChoice, rExecution); + } + } + // Remove this event to replace it with a new one + currentTrace.remove(currentTrace.size() - 1); + currRWFieldsMap.remove(choiceCounter); + } + pastConfChoice++; + } + checkedTrace.add(rExecution); + } + } + } } } -- 2.34.1