private PriorityQueue<Integer> backtrackStateQ; // Heap that returns the latest state
private Execution currentExecution; // Holds the information about the current execution
private HashMap<Integer, HashSet<Integer>> doneBacktrackMap; // Record state ID and trace already constructed
+ private MainSummary mainSummary; // Main summary (M) for state ID, event, and R/W set
+ private HashMap<Integer, PredecessorInfo> stateToPredInfo; // Predecessor info indexed by state ID
private HashMap<Integer, RestorableVMState> 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;
private boolean isEndOfExecution;
+ private boolean isNotCheckedForEventsYet;
// Statistics
private int numOfTransitions;
}
}
isBooleanCGFlipped = false;
- numOfTransitions = 0;
- nonRelevantClasses = new HashSet<>();
- nonRelevantFields = new HashSet<>();
- relevantFields = new HashSet<>();
- restorableStateMap = new HashMap<>();
+ isNotCheckedForEventsYet = true;
mainSummary = new MainSummary();
+ numOfTransitions = 0;
+ nonRelevantClasses = new HashSet<>();
+ nonRelevantFields = new HashSet<>();
+ relevantFields = new HashSet<>();
+ restorableStateMap = new HashMap<>();
+ stateToPredInfo = new HashMap<>();
initializeStatesVariables();
}
@Override
public void choiceGeneratorRegistered(VM vm, ChoiceGenerator<?> nextCG, ThreadInfo currentThread, Instruction executedInstruction) {
+ if (isNotCheckedForEventsYet) {
+ // Check if this benchmark has no events
+ if (nextCG instanceof IntChoiceFromSet) {
+ IntChoiceFromSet icsCG = (IntChoiceFromSet) nextCG;
+ Integer[] cgChoices = icsCG.getAllChoices();
+ if (cgChoices.length == 2 && cgChoices[0] == 0 && cgChoices[1] == -1) {
+ // This means the benchmark only has 2 choices, i.e., 0 and -1 which means that it has no events
+ stateReductionMode = false;
+ }
+ isNotCheckedForEventsYet = false;
+ }
+ }
if (stateReductionMode) {
// Initialize with necessary information from the CG
if (nextCG instanceof IntChoiceFromSet) {
public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
if (stateReductionMode) {
if (!isEndOfExecution) {
- // Has to be initialized and a integer CG
+ // Has to be initialized and it is a integer CG
ChoiceGenerator<?> cg = vm.getChoiceGenerator();
if (cg instanceof IntChoiceFromSet || cg instanceof IntIntervalGenerator) {
int currentChoice = choiceCounter - 1; // Accumulative choice w.r.t the current trace
}
}
+ // 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<Predecessor> predecessors; // Maps incoming events/transitions (execution and choice)
+ private HashMap<Execution, HashSet<Integer>> recordedPredecessors;
+ // Memorize event and choice number to not record them twice
+
+ public PredecessorInfo() {
+ predecessors = new HashSet<>();
+ recordedPredecessors = new HashMap<>();
+ }
+
+ public HashSet<Predecessor> getPredecessors() {
+ return predecessors;
+ }
+
+ private boolean isRecordedPredecessor(Execution execution, int choice) {
+ // See if we have recorded this predecessor earlier
+ HashSet<Integer> 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,
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<Predecessor> predecessors; // Maps incoming events/transitions (execution and choice)
- private HashMap<Execution, HashSet<Integer>> 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
choice = 0;
choiceCounter = 0;
execution = null;
- predecessors = new HashSet<>();
- recordedPredecessors = new HashMap<>();
stateId = 0;
transitionCG = null;
}
return execution;
}
- public HashSet<Predecessor> 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<Integer> 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;
}
execution = exec;
}
- public void setPredecessors(HashSet<Predecessor> preds) {
- predecessors = new HashSet<>(preds);
- }
-
public void setStateId(int stId) {
stateId = stId;
}
public Set<Integer> getEventChoicesAtStateId(int stateId) {
HashMap<Integer, ReadWriteSet> stateSummary = mainSummary.get(stateId);
- return stateSummary.keySet();
+ // Return a new set since this might get updated concurrently
+ return new HashSet<>(stateSummary.keySet());
}
public ReadWriteSet getRWSetForEventChoiceAtState(int eventChoice, int stateId) {
return stateSummary.get(eventChoice);
}
+ public Set<Integer> getStateIds() {
+ return mainSummary.keySet();
+ }
+
private ReadWriteSet performUnion(ReadWriteSet recordedRWSet, ReadWriteSet rwSet) {
// Combine the same write accesses and record in the recordedRWSet
HashMap<String, Integer> recordedWriteMap = recordedRWSet.getWriteMap();
} else {
transition = new TransitionEvent();
currentExecution.addTransition(transition);
- transition.recordPredecessor(currentExecution, choiceCounter - 1);
+ addPredecessors(stateId);
}
transition.setExecution(currentExecution);
transition.setTransitionCG(icsCG);
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;
// 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
boolean terminate = false;
+ Set<Integer> mainStateIds = mainSummary.getStateIds();
for(Integer stateId : justVisitedStates) {
- // We perform updates on backtrack sets for every
- if (prevVisitedStates.contains(stateId) || completeFullCycle(stateId)) {
- updateBacktrackSetsFromGraph(stateId, currentExecution, choiceCounter - 1);
- terminate = true;
- }
- // If frequency > 1 then this means we have visited this stateId more than once
- if (currVisitedStates.containsKey(stateId) && currVisitedStates.get(stateId) > 1) {
- updateBacktrackSetsFromGraph(stateId, currentExecution, choiceCounter - 1);
+ // We exclude states that are produced by other CGs that are not integer CG
+ // When we encounter these states, then we should also encounter the corresponding integer CG state ID
+ if (mainStateIds.contains(stateId)) {
+ // We perform updates on backtrack sets for every
+ if (prevVisitedStates.contains(stateId) || completeFullCycle(stateId)) {
+ updateBacktrackSetsFromGraph(stateId, currentExecution, choiceCounter - 1);
+ terminate = true;
+ }
+ // 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);
+ }
}
}
return terminate;
}
// 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)) {
}
}
+ 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
}
private void exploreNextBacktrackPoints(VM vm, IntChoiceFromSet icsCG) {
- // Check if we are reaching the end of our execution: no more backtracking points to explore
- // cgMap, backtrackMap, backtrackStateQ are updated simultaneously (checking backtrackStateQ is enough)
- if (!backtrackStateQ.isEmpty()) {
- // Set done all the other backtrack points
- for (TransitionEvent backtrackTransition : currentExecution.getExecutionTrace()) {
+ // Check if we are reaching the end of our execution: no more backtracking points to explore
+ // cgMap, backtrackMap, backtrackStateQ are updated simultaneously (checking backtrackStateQ is enough)
+ if (!backtrackStateQ.isEmpty()) {
+ // Set done all the other backtrack points
+ for (TransitionEvent backtrackTransition : currentExecution.getExecutionTrace()) {
backtrackTransition.getTransitionCG().setDone();
- }
- // Reset the next backtrack point with the latest state
- int hiStateId = backtrackStateQ.peek();
- // Restore the state first if necessary
- if (vm.getStateId() != hiStateId) {
- RestorableVMState restorableState = restorableStateMap.get(hiStateId);
- vm.restoreState(restorableState);
- }
- // Set the backtrack CG
- IntChoiceFromSet backtrackCG = (IntChoiceFromSet) vm.getChoiceGenerator();
- setBacktrackCG(hiStateId, backtrackCG);
- } else {
- // Set done this last CG (we save a few rounds)
- icsCG.setDone();
- }
- // Save all the visited states when starting a new execution of trace
- prevVisitedStates.addAll(currVisitedStates.keySet());
- // This marks a transitional period to the new CG
- isEndOfExecution = true;
+ }
+ // Reset the next backtrack point with the latest state
+ int hiStateId = backtrackStateQ.peek();
+ // Restore the state first if necessary
+ if (vm.getStateId() != hiStateId) {
+ RestorableVMState restorableState = restorableStateMap.get(hiStateId);
+ vm.restoreState(restorableState);
+ }
+ // Set the backtrack CG
+ IntChoiceFromSet backtrackCG = (IntChoiceFromSet) vm.getChoiceGenerator();
+ setBacktrackCG(hiStateId, backtrackCG);
+ } else {
+ // Set done this last CG (we save a few rounds)
+ icsCG.setDone();
+ }
+ // Save all the visited states when starting a new execution of trace
+ prevVisitedStates.addAll(currVisitedStates.keySet());
+ // This marks a transitional period to the new CG
+ isEndOfExecution = true;
}
private boolean isConflictFound(int eventChoice, Execution conflictExecution, int conflictChoice,
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<Integer, ReadWriteSet> 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();
return false;
}
+ private HashSet<Predecessor> getPredecessors(int stateId) {
+ // Get a set of predecessors for this state ID
+ HashSet<Predecessor> 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<Integer, ReadWriteSet> 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()) {
choices = icsCG.getAllChoices();
refChoices = copyChoices(choices);
// Clear data structures
- currVisitedStates = new HashMap<>();
- stateToEventMap = new HashMap<>();
+ currVisitedStates.clear();
+ stateToEventMap.clear();
isEndOfExecution = false;
}
}
return;
}
visited.add(currTrans);
- // Halt if the set is empty
- if (currRWSet.isEmpty()) {
- return;
- }
- // Explore all predecessors
- for (Predecessor predecessor : currTrans.getPredecessors()) {
- // Get the predecessor (previous conflict choice)
- int predecessorChoice = predecessor.getChoice();
- Execution predecessorExecution = predecessor.getExecution();
- // Push up one happens-before transition
- int newConflictEventChoice = conflictEventChoice;
- // Check if a conflict is found
- if (isConflictFound(conflictEventChoice, predecessorExecution, predecessorChoice, currRWSet)) {
- createBacktrackingPoint(conflictEventChoice, predecessorExecution, predecessorChoice);
- // We need to extract the pushed happens-before event choice from the predecessor execution and choice
- newConflictEventChoice = predecessorExecution.getExecutionTrace().get(predecessorChoice).getChoice();
+ // Check the predecessors only if the set is not empty
+ if (!currRWSet.isEmpty()) {
+ // Explore all predecessors
+ for (Predecessor predecessor : getPredecessors(currTrans.getStateId())) {
+ // Get the predecessor (previous conflict choice)
+ int predecessorChoice = predecessor.getChoice();
+ Execution predecessorExecution = predecessor.getExecution();
+ // Push up one happens-before transition
+ int newConflictEventChoice = conflictEventChoice;
+ // Check if a conflict is found
+ ReadWriteSet newCurrRWSet = currRWSet.getCopy();
+ if (isConflictFound(conflictEventChoice, predecessorExecution, predecessorChoice, newCurrRWSet)) {
+ createBacktrackingPoint(conflictEventChoice, predecessorExecution, predecessorChoice);
+ // We need to extract the pushed happens-before event choice from the predecessor execution and choice
+ newConflictEventChoice = predecessorExecution.getExecutionTrace().get(predecessorChoice).getChoice();
+ }
+ // Continue performing DFS if conflict is not found
+ updateBacktrackSetDFS(predecessorExecution, predecessorChoice, newConflictEventChoice,
+ newCurrRWSet, visited);
}
- // Continue performing DFS if conflict is not found
- updateBacktrackSetDFS(predecessorExecution, predecessorChoice, newConflictEventChoice,
- currRWSet, visited);
}
}
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<TransitionEvent> reachableTransitions = rGraph.getReachableTransitionsAtState(stateId);
- for (TransitionEvent transition : reachableTransitions) {
- transition.recordPredecessor(currentExecution, choiceCounter - 1);
- }
+ // Record a new predecessor for a revisited state
+ addPredecessors(stateId);
}
}
}
projects / jpf-core.git / blobdiff