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<Execution>> rGraph; // Create a reachability graph for past executions
// Boolean states
// This class stores a representation of the execution graph node
private class Execution {
- private ArrayList<BacktrackPoint> executionTrace; // The BacktrackPoint objects of this execution
+ private HashMap<IntChoiceFromSet, Integer> cgToChoiceMap; // Map between CG to choice numbers for O(1) access
+ private ArrayList<BacktrackPoint> 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<Integer, ReadWriteSet> readWriteFieldsMap; // Record fields that are accessed
public Execution() {
+ cgToChoiceMap = new HashMap<>();
executionTrace = new ArrayList<>();
parentChoice = -1;
parent = null;
executionTrace.add(newBacktrackPoint);
}
+ public void clearCGToChoiceMap() {
+ cgToChoiceMap = null;
+ }
+
public ArrayList<BacktrackPoint> getExecutionTrace() {
return executionTrace;
}
+ public int getChoiceFromCG(IntChoiceFromSet icsCG) {
+ return cgToChoiceMap.get(icsCG);
+ }
+
public int getParentChoice() {
return parentChoice;
}
return readWriteFieldsMap;
}
+ public void mapCGToChoice(IntChoiceFromSet icsCG, int choice) {
+ cgToChoiceMap.put(icsCG, choice);
+ }
+
public void setParentChoice(int parChoice) {
parentChoice = parChoice;
}
}
}
- // 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;
-// }
-// }
-
// -- CONSTANTS
private final static String DO_CALL_METHOD = "doCall";
// We exclude fields that come from libraries (Java and Groovy), and also the infrastructure
// 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);
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) {
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<refChoices.length; i++) {
- if (actualEvtNum == refChoices[i]) {
- currChoiceFromCG = i;
- break;
- }
- }
- }
- if (currChoiceInd != currChoiceFromCG) {
- currentChoice = (currentChoice - currChoiceInd) + currChoiceFromCG;
+ // Find the choice related to the IntIntervalGenerator CG from the map
+ currentChoice = currentExecution.getChoiceFromCG((IntChoiceFromSet) parentCG);
}
return currentChoice;
}
private void findFirstConflictAndCreateBacktrackPoint(int currentChoice, Instruction nextInsn, String fieldClass) {
// Check for conflict (go backward from current choice and get the first conflict)
Execution execution = currentExecution;
- // Actual choice of the current execution trace
- //int actualChoice = currentChoice % refChoices.length;
// Choice/event we want to check for conflict against (start from actual choice)
int pastChoice = currentChoice;
// Perform backward DFS through the execution graph
ArrayList<BacktrackPoint> 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;
}
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!
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
}
}
+ // 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<BacktrackExecution> backtrackExecutions = backtrackMap.get(stateId);
ArrayList<BacktrackPoint> 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()) {
// TODO: OPTIMIZATION!
// Check and make sure that state ID and choice haven't been explored for this trace
- private boolean alreadyChecked(HashSet<String> checkedStateIdAndChoice, BacktrackPoint backtrackPoint) {
+ private boolean isAlreadyChecked(HashSet<String> checkedStateIdAndChoice, BacktrackPoint backtrackPoint) {
int stateId = backtrackPoint.getStateId();
int choice = backtrackPoint.getChoice();
StringBuilder sb = new StringBuilder();
}
}
+ // Update the backtrack sets in a previous execution
private void updateBacktrackSetsInPreviousExecution(Execution rExecution, int stateId,
HashSet<String> checkedStateIdAndChoice) {
// Find the choice/event that marks the start of the subtrace from the previous execution
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<BacktrackPoint> currentTrace = currentExecution.getExecutionTrace();
}
}
- // 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<Execution> checkedTrace = new HashSet<>();
projects / jpf-core.git / commitdiff