import gov.nasa.jpf.ListenerAdapter;
import gov.nasa.jpf.jvm.bytecode.INVOKEINTERFACE;
import gov.nasa.jpf.jvm.bytecode.JVMFieldInstruction;
+import gov.nasa.jpf.report.Publisher;
import gov.nasa.jpf.search.Search;
import gov.nasa.jpf.vm.*;
import gov.nasa.jpf.vm.bytecode.ReadInstruction;
// Statistics
private int numOfTransitions;
+ private int numOfUniqueTransitions;
public DPORStateReducerWithSummary(Config config, JPF jpf) {
verboseMode = config.getBoolean("printout_state_transition", false);
isNotCheckedForEventsYet = true;
mainSummary = new MainSummary();
numOfTransitions = 0;
+ numOfUniqueTransitions = 0;
nonRelevantClasses = new HashSet<>();
nonRelevantFields = new HashSet<>();
relevantFields = new HashSet<>();
public void searchFinished(Search search) {
if (verboseMode) {
out.println("\n==> DEBUG: ----------------------------------- search finished");
- out.println("\n==> DEBUG: State reduction mode : " + stateReductionMode);
- out.println("\n==> DEBUG: Number of transitions : " + numOfTransitions);
+ out.println("\n==> DEBUG: State reduction mode : " + stateReductionMode);
+ out.println("\n==> DEBUG: Number of transitions : " + numOfTransitions);
+ out.println("\n==> DEBUG: Number of unique transitions (DPOR) : " + numOfUniqueTransitions);
out.println("\n==> DEBUG: ----------------------------------- search finished" + "\n");
- fileWriter.println("==> DEBUG: State reduction mode : " + stateReductionMode);
- fileWriter.println("==> DEBUG: Number of transitions : " + numOfTransitions);
+ fileWriter.println("==> DEBUG: State reduction mode : " + stateReductionMode);
+ fileWriter.println("==> DEBUG: Number of transitions : " + numOfTransitions);
+ fileWriter.println("==> DEBUG: Number of unique transitions : " + numOfUniqueTransitions);
fileWriter.println();
fileWriter.close();
}
@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) {
- if (isNotCheckedForEventsYet) {
- // Check if this benchmark has no events
- if (nextCG instanceof IntChoiceFromSet) {
- IntChoiceFromSet icsCG = (IntChoiceFromSet) nextCG;
+ // Initialize with necessary information from the CG
+ if (nextCG instanceof IntChoiceFromSet) {
+ IntChoiceFromSet icsCG = (IntChoiceFromSet) nextCG;
+ // Tell JPF that we are performing DPOR
+ icsCG.setDpor();
+ if (!isEndOfExecution) {
+ // Check if CG has been initialized, otherwise initialize it
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;
- }
- } else {
- // Initialize with necessary information from the CG
- if (nextCG instanceof IntChoiceFromSet) {
- IntChoiceFromSet icsCG = (IntChoiceFromSet) nextCG;
- // Tell JPF that we are performing DPOR
- icsCG.setDpor();
- if (!isEndOfExecution) {
- // Check if CG has been initialized, otherwise initialize it
- Integer[] cgChoices = icsCG.getAllChoices();
- // Record the events (from choices)
- if (choices == null) {
- choices = cgChoices;
- // Make a copy of choices as reference
- refChoices = copyChoices(choices);
- // Record the max event choice (the last element of the choice array)
- maxEventChoice = choices[choices.length - 1];
- }
- icsCG.setNewValues(choices);
- icsCG.reset();
- // Use a modulo since choiceCounter is going to keep increasing
- int choiceIndex = choiceCounter % choices.length;
- icsCG.advance(choices[choiceIndex]);
- } else {
- // Set done all CGs while transitioning to a new execution
- icsCG.setDone();
+ // Record the events (from choices)
+ if (choices == null) {
+ choices = cgChoices;
+ // Make a copy of choices as reference
+ refChoices = copyChoices(choices);
+ // Record the max event choice (the last element of the choice array)
+ maxEventChoice = choices[choices.length - 1];
}
+ icsCG.setNewValues(choices);
+ icsCG.reset();
+ // Use a modulo since choiceCounter is going to keep increasing
+ int choiceIndex = choiceCounter % choices.length;
+ icsCG.advance(choices[choiceIndex]);
+ } else {
+ // Set done all CGs while transitioning to a new execution
+ icsCG.setDone();
}
}
}
exploreNextBacktrackPoints(vm, icsCG);
} else {
numOfTransitions++;
+ if (choiceCounter < choices.length) {
+ numOfUniqueTransitions++;
+ }
}
// Map state to event
mapStateToEvent(icsCG.getNextChoice());
choiceCounter++;
}
} else {
- numOfTransitions++;
+ if (currentCG instanceof IntChoiceFromSet) {
+ numOfTransitions++;
+ }
}
}
Set<Integer> eventChoicesAtStateId = mainSummary.getEventChoicesAtStateId(stateId);
for (Integer eventChoice : eventChoicesAtStateId) {
// Get the ReadWriteSet object for this event at state ID
- ReadWriteSet rwSet = mainSummary.getRWSetForEventChoiceAtState(eventChoice, stateId);
+ ReadWriteSet rwSet = mainSummary.getRWSetForEventChoiceAtState(eventChoice, stateId).getCopy();
+ // We have to first check for conflicts between the event and the current transition
+ // Push up one happens-before transition
+ int conflictEventChoice = eventChoice;
+ if (isConflictFound(eventChoice, currExecution, currChoice, rwSet)) {
+ createBacktrackingPoint(eventChoice, currExecution, currChoice);
+ // We need to extract the pushed happens-before event choice from the predecessor execution and choice
+ conflictEventChoice = currExecution.getExecutionTrace().get(currChoice).getChoice();
+ }
// 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.getCopy(), visited);
+ updateBacktrackSetDFS(currExecution, currChoice, conflictEventChoice, rwSet, visited);
}
}
}
projects / jpf-core.git / blobdiff