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;
public class DPORStateReducerWithSummary extends ListenerAdapter {
// Information printout fields for verbose mode
+ private long startTime;
+ private long timeout;
private boolean verboseMode;
private boolean stateReductionMode;
private final PrintWriter out;
private HashSet<ClassInfo> nonRelevantClasses;// Class info objects of non-relevant classes
private HashSet<FieldInfo> nonRelevantFields; // Field info objects of non-relevant fields
private HashSet<FieldInfo> relevantFields; // Field info objects of relevant fields
- private HashMap<Integer, HashSet<Integer>> stateToEventMap;
+ private HashMap<Integer, HashSet<Integer>> stateToEventMap; // Map state ID to events
// Data structure to analyze field Read/Write accesses and conflicts
private HashMap<Integer, LinkedList<BacktrackExecution>> backtrackMap; // Track created backtracking points
private PriorityQueue<Integer> backtrackStateQ; // Heap that returns the latest state
// Boolean states
private boolean isBooleanCGFlipped;
private boolean isEndOfExecution;
+ private boolean isNotCheckedForEventsYet;
// Statistics
private int numOfTransitions;
+ private HashMap<Integer, HashSet<Integer>> stateToUniqueTransMap;
public DPORStateReducerWithSummary(Config config, JPF jpf) {
verboseMode = config.getBoolean("printout_state_transition", false);
}
}
isBooleanCGFlipped = false;
+ isNotCheckedForEventsYet = true;
mainSummary = new MainSummary();
- numOfTransitions = 0;
- nonRelevantClasses = new HashSet<>();
- nonRelevantFields = new HashSet<>();
- relevantFields = new HashSet<>();
+ numOfTransitions = 0;
+ nonRelevantClasses = new HashSet<>();
+ nonRelevantFields = new HashSet<>();
+ relevantFields = new HashSet<>();
restorableStateMap = new HashMap<>();
stateToPredInfo = new HashMap<>();
+ stateToUniqueTransMap = new HashMap<>();
initializeStatesVariables();
+
+ // Timeout input from config is in minutes, so we need to convert into millis
+ timeout = config.getInt("timeout", 0) * 60 * 1000;
+ startTime = System.currentTimeMillis();
}
@Override
@Override
public void searchFinished(Search search) {
if (verboseMode) {
+ int summaryOfUniqueTransitions = summarizeUniqueTransitions();
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);
+ if (choices != null) {
+ out.println("\n==> DEBUG: Number of events : " + choices.length);
+ } else {
+ // Without DPOR we don't have choices being assigned with a CG
+ out.println("\n==> DEBUG: Number of events : 0");
+ }
+ out.println("\n==> DEBUG: Number of transitions : " + numOfTransitions);
+ out.println("\n==> DEBUG: Number of unique transitions (DPOR) : " + summaryOfUniqueTransitions);
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);
+ if (choices != null) {
+ fileWriter.println("==> DEBUG: Number of events : " + choices.length);
+ } else {
+ // Without DPOR we don't have choices being assigned with a CG
+ fileWriter.println("==> DEBUG: Number of events : 0");
+ }
+ fileWriter.println("==> DEBUG: Number of transitions : " + numOfTransitions);
+ fileWriter.println("==> DEBUG: Number of unique transitions (DPOR) : " + summaryOfUniqueTransitions);
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) {
// Initialize with necessary information from the CG
if (nextCG instanceof IntChoiceFromSet) {
if (choiceCounter > 0 && terminateCurrentExecution()) {
exploreNextBacktrackPoints(vm, icsCG);
} else {
+ // We only count IntChoiceFromSet CGs
numOfTransitions++;
+ countUniqueTransitions(vm.getStateId(), icsCG.getNextChoice());
}
// Map state to event
mapStateToEvent(icsCG.getNextChoice());
choiceCounter++;
}
} else {
- numOfTransitions++;
+ // We only count IntChoiceFromSet CGs
+ if (currentCG instanceof IntChoiceFromSet) {
+ numOfTransitions++;
+ }
}
}
@Override
public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
+ // Check the timeout
+ if (timeout > 0) {
+ if (System.currentTimeMillis() - startTime > timeout) {
+ StringBuilder sbTimeOut = new StringBuilder();
+ sbTimeOut.append("Execution timeout: " + (timeout / (60 * 1000)) + " minutes have passed!");
+ Instruction nextIns = ti.createAndThrowException("java.lang.RuntimeException", sbTimeOut.toString());
+ ti.setNextPC(nextIns);
+ }
+ }
+
if (stateReductionMode) {
if (!isEndOfExecution) {
// Has to be initialized and it is a integer CG
return transition;
}
+ // --- Functions related to statistics counting
+ // Count unique state IDs
+ private void countUniqueTransitions(int stateId, int nextChoiceValue) {
+ HashSet<Integer> events;
+ // Get the set of events
+ if (!stateToUniqueTransMap.containsKey(stateId)) {
+ events = new HashSet<>();
+ stateToUniqueTransMap.put(stateId, events);
+ } else {
+ events = stateToUniqueTransMap.get(stateId);
+ }
+ // Insert the event
+ if (!events.contains(nextChoiceValue)) {
+ events.add(nextChoiceValue);
+ }
+ }
+
+ // Summarize unique state IDs
+ private int summarizeUniqueTransitions() {
+ // Just count the set size of each of entry map and sum them up
+ int numOfUniqueTransitions = 0;
+ for (Map.Entry<Integer,HashSet<Integer>> entry : stateToUniqueTransMap.entrySet()) {
+ numOfUniqueTransitions = numOfUniqueTransitions + entry.getValue().size();
+ }
+
+ return numOfUniqueTransitions;
+ }
+
// --- Functions related to cycle detection and reachability graph
// Detect cycles in the current execution/trace
}
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,
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