private int depth;
private int id;
private Transition transition;
-
+ private HashSet<String> conflictSet;
+ private HashSet<String> appSet;
+ // Holds the event value numbers that execute write instructions
+ private HashSet<Integer> writeEventNumberSet;
// Holds values that have appeared during CG advances
private HashSet<Integer> cgChoiceSet;
private Integer choiceUpperBound;
private boolean isInitialized;
+ private int currentChoice;
+ // Records how many times BooleanChoiceGenerator has been advanced
+ private int bCGIsAdvanced;
+ // Records how many times we have looped through all the event numbers (IntIntervalGenerator)
+ private int iiCGIsLooped;
+
+ // Constants to determine when to start reducing states
+ private final int BOOLEAN_CG_ADVANCED_THRESHOLD = 2;
+ private final int INTEGER_CG_ADVANCED_THRESHOLD = 50;
- public StateReducer (Config config, JPF jpf) {
+ public StateReducer (Config config) {
debugMode = config.getBoolean("debug_state_transition", false);
stateReductionMode = config.getBoolean("activate_state_reduction", true);
if (debugMode) {
cgChoiceSet = new HashSet<>();
choiceUpperBound = 0;
isInitialized = false;
+ conflictSet = new HashSet<>();
+ String[] conflictVars = config.getStringArray("variables");
+ // We are not tracking anything if it is null
+ if (conflictVars != null) {
+ for (String var : conflictVars) {
+ conflictSet.add(var);
+ }
+ }
+ appSet = new HashSet<>();
+ String[] apps = config.getStringArray("apps");
+ // We are not tracking anything if it is null
+ if (apps != null) {
+ for (String var : apps) {
+ appSet.add(var);
+ }
+ }
+ currentChoice = 0;
+ writeEventNumberSet = new HashSet<>();
+ bCGIsAdvanced = 0;
+ iiCGIsLooped = 0;
}
@Override
@Override
public void choiceGeneratorAdvanced (VM vm, ChoiceGenerator<?> currentCG) {
if (stateReductionMode) {
+ // Check for BooleanChoiceGenerator
+ if (currentCG instanceof BooleanChoiceGenerator) {
+ bCGIsAdvanced++;
+ }
// Check every choice generated and make sure that all the available choices
// are chosen first before repeating the same choice of value twice!
if (currentCG instanceof IntIntervalGenerator) {
if (cgChoiceSet.contains(choiceUpperBound)) {
isInitialized = false;
cgChoiceSet.clear();
+ iiCGIsLooped++;
+ }
+ // Record the current choice
+ currentChoice = iigCG.getNextChoice();
+ // Start reducing (advancing) if the thresholds are passed
+ if (iiCGIsLooped >= INTEGER_CG_ADVANCED_THRESHOLD &&
+ bCGIsAdvanced >= BOOLEAN_CG_ADVANCED_THRESHOLD) {
+ if (!writeEventNumberSet.contains(currentChoice)) {
+ iigCG.advance();
+ }
}
}
}
out.println("\n==> DEBUG: ----------------------------------- search finished" + "\n");
}
}
+
+ @Override
+ public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
+ // CASE #1: Detecting variable write-after-write conflict
+ if (executedInsn instanceof WriteInstruction) {
+ // Check for write-after-write conflict
+ String varId = ((WriteInstruction) executedInsn).getFieldInfo().getFullName();
+ for(String var : conflictSet) {
+ if (varId.contains(var)) {
+ String writer = getWriter(ti.getStack());
+ // Just return if the writer is not one of the listed apps in the .jpf file
+ if (writer == null)
+ return;
+
+ // Stores event number that executes WriteInstruction
+ if (!writeEventNumberSet.contains(currentChoice)) {
+ writeEventNumberSet.add(currentChoice);
+ }
+ }
+ }
+ }
+ }
+
+ // Find the variable writer
+ // It should be one of the apps listed in the .jpf file
+ private String getWriter(List<StackFrame> sfList) {
+ // Start looking from the top of the stack backward
+ for(int i=sfList.size()-1; i>=0; i--) {
+ MethodInfo mi = sfList.get(i).getMethodInfo();
+ if(!mi.isJPFInternal()) {
+ String method = mi.getStackTraceName();
+ // Check against the apps in the appSet
+ for(String app : appSet) {
+ // There is only one writer at a time but we need to always
+ // check all the potential writers in the list
+ if (method.contains(app)) {
+ return app;
+ }
+ }
+ }
+ }
+
+ return null;
+ }
}
\ No newline at end of file