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();
}
}
}
+ // 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;
}
} else {
transition = new TransitionEvent();
currentExecution.addTransition(transition);
- transition.recordPredecessor(currentExecution, choiceCounter - 1);
- // We have to check if there is a transition whose source state ID is the same
- // If such exists, then we need to add its predecessors to the predecessor set of the current transition
- for (TransitionEvent trans : rGraph.getReachableTransitionsAtState(stateId)) {
- for (Predecessor pred : trans.getPredecessors()) {
- transition.recordPredecessor(pred.getExecution(), pred.getChoice());
- }
- }
+ 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;
updateBacktrackSetsFromGraph(stateId, currentExecution, choiceCounter - 1);
terminate = true;
}
- // If frequency > 1 then this means we have visited this stateId more than once
+ // 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);
}
}
// 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;
}
}
// Check the predecessors only if the set is not empty
if (!currRWSet.isEmpty()) {
// Explore all predecessors
- for (Predecessor predecessor : currTrans.getPredecessors()) {
+ for (Predecessor predecessor : getPredecessors(currTrans.getStateId())) {
// Get the predecessor (previous conflict choice)
int predecessorChoice = predecessor.getChoice();
Execution predecessorExecution = predecessor.getExecution();
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