private HashSet<String> doneBacktrackSet; // Record state ID and trace already constructed
private HashMap<Integer, RestorableVMState> restorableStateMap; // Maps state IDs to the restorable state object
private HashMap<Integer, Integer> stateToChoiceCounterMap; // Maps state IDs to the choice counter
- private HashMap<Integer, ArrayList<ReachableTrace>> rGraph; // Create a reachability graph
+ //private HashMap<Integer, ArrayList<ReachableTrace>> rGraph; // Create a reachability graph
+ private HashMap<Integer, ArrayList<Execution>> rGraph; // Create a reachability graph for past executions
// Boolean states
private boolean isBooleanCGFlipped;
}
}
-
-
// This class stores a compact representation of a reachability graph for past executions
- private class ReachableTrace {
- private ArrayList<BacktrackPoint> pastBacktrackPointList;
- private HashMap<Integer, ReadWriteSet> pastReadWriteFieldsMap;
-
- public ReachableTrace(ArrayList<BacktrackPoint> btrackPointList,
- HashMap<Integer, ReadWriteSet> rwFieldsMap) {
- pastBacktrackPointList = btrackPointList;
- pastReadWriteFieldsMap = rwFieldsMap;
- }
-
- public ArrayList<BacktrackPoint> getPastBacktrackPointList() {
- return pastBacktrackPointList;
- }
-
- public HashMap<Integer, ReadWriteSet> getPastReadWriteFieldsMap() {
- return pastReadWriteFieldsMap;
- }
- }
+// private class ReachableTrace {
+// private ArrayList<BacktrackPoint> pastBacktrackPointList;
+// private HashMap<Integer, ReadWriteSet> pastReadWriteFieldsMap;
+//
+// public ReachableTrace(ArrayList<BacktrackPoint> btrackPointList,
+// HashMap<Integer, ReadWriteSet> rwFieldsMap) {
+// pastBacktrackPointList = btrackPointList;
+// pastReadWriteFieldsMap = rwFieldsMap;
+// }
+//
+// public ArrayList<BacktrackPoint> getPastBacktrackPointList() {
+// return pastBacktrackPointList;
+// }
+//
+// public HashMap<Integer, ReadWriteSet> getPastReadWriteFieldsMap() {
+// return pastReadWriteFieldsMap;
+// }
+// }
// -- CONSTANTS
private final static String DO_CALL_METHOD = "doCall";
}
// 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();
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:
}
}
+ 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<Execution> 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
HashSet<Integer> 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<ReachableTrace> 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);
}
}
}
// 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<Integer, ReadWriteSet> pastRWFieldsMap = pastExecution.getReadWriteFieldsMap();
ArrayList<BacktrackPoint> pastTrace = pastExecution.getExecutionTrace();
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<String> 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<String> 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<BacktrackPoint> executionTrace = execution.getExecutionTrace();
+ HashMap<Integer, ReadWriteSet> 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<String> 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<String> 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
// 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!
// Update the backtrack sets in a previous execution
private void updateBacktrackSetsInPreviousExecution(int stateId) {
-// // Don't check a past trace twice!
-// HashSet<ReachableTrace> checkedTrace = new HashSet<>();
-// // Don't check the same event twice for a revisited state
-// HashMap<Integer, HashSet<Integer>> checkedStateIdAndChoice = new HashMap<>();
-// // Get sorted reachable state IDs
-// ArrayList<Integer> 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<ReachableTrace> 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<BacktrackPoint> pastBacktrackPointList = rTrace.getPastBacktrackPointList();
-// HashMap<Integer, ReadWriteSet> 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<Execution> checkedTrace = new HashSet<>();
+ // Don't check the same event twice for a revisited state
+ HashMap<Integer, HashSet<Integer>> checkedStateIdAndChoice = new HashMap<>();
+ // Get sorted reachable state IDs
+ ArrayList<Integer> 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<Execution> 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<BacktrackPoint> pastExecutionTrace = rExecution.getExecutionTrace();
+ HashMap<Integer, ReadWriteSet> 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<BacktrackPoint> currentTrace = currentExecution.getExecutionTrace();
+ HashMap<Integer, ReadWriteSet> 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);
+ }
+ }
+ }
}
}
projects / jpf-core.git / blobdiff