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;
}
}
isBooleanCGFlipped = false;
+ mainSummary = new MainSummary();
numOfTransitions = 0;
nonRelevantClasses = new HashSet<>();
nonRelevantFields = new HashSet<>();
relevantFields = new HashSet<>();
restorableStateMap = new HashMap<>();
- mainSummary = new MainSummary();
+ stateToPredInfo = new HashMap<>();
initializeStatesVariables();
}
// Explore the next backtrack point:
// 1) if we have seen this state or this state contains cycles that involve all events, and
// 2) after the current CG is advanced at least once
- if (terminateCurrentExecution() && choiceCounter > 0) {
+ if (choiceCounter > 0 && terminateCurrentExecution()) {
exploreNextBacktrackPoints(vm, icsCG);
} else {
numOfTransitions++;
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();
// If the state Id has existed, find the event choice:
// 1) If the event choice has not existed, insert the ReadWriteSet object
// 2) If the event choice has existed, perform union between the two ReadWriteSet objects
- HashMap<Integer, ReadWriteSet> stateSummary;
- if (!mainSummary.containsKey(stateId)) {
- stateSummary = new HashMap<>();
- stateSummary.put(eventChoice, rwSet.getCopy());
- mainSummary.put(stateId, stateSummary);
- } else {
- stateSummary = mainSummary.get(stateId);
- if (!stateSummary.containsKey(eventChoice)) {
+ if (!rwSet.isEmpty()) {
+ HashMap<Integer, ReadWriteSet> stateSummary;
+ if (!mainSummary.containsKey(stateId)) {
+ stateSummary = new HashMap<>();
stateSummary.put(eventChoice, rwSet.getCopy());
+ mainSummary.put(stateId, stateSummary);
} else {
- rwSet = performUnion(stateSummary.get(eventChoice), rwSet);
+ stateSummary = mainSummary.get(stateId);
+ if (!stateSummary.containsKey(eventChoice)) {
+ stateSummary.put(eventChoice, rwSet.getCopy());
+ } else {
+ rwSet = performUnion(stateSummary.get(eventChoice), rwSet);
+ }
}
}
return rwSet;
} 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
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;
}
}
private void updateBacktrackSetDFS(Execution execution, int currentChoice, int conflictEventChoice,
ReadWriteSet currRWSet, HashSet<TransitionEvent> visited) {
- // Halt when we have found the first read/write conflicts for all memory locations
- if (currRWSet.isEmpty()) {
- return;
- }
TransitionEvent currTrans = execution.getExecutionTrace().get(currentChoice);
// Record this transition into the state summary of main summary
currRWSet = mainSummary.updateStateSummary(currTrans.getStateId(), conflictEventChoice, currRWSet);
return;
}
visited.add(currTrans);
- // 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);
}
}
}
// Memorize visited TransitionEvent object while performing backward DFS to avoid getting caught up in a cycle
HashSet<TransitionEvent> visited = new HashSet<>();
// Update the backtrack sets recursively
- updateBacktrackSetDFS(currExecution, currChoice, eventChoice, rwSet, visited);
+ updateBacktrackSetDFS(currExecution, currChoice, eventChoice, rwSet.getCopy(), visited);
}
}
}
projects / jpf-core.git / blobdiff