import java.util.*;
+// TODO: Fix for Groovy's model-checking
+// TODO: This is a listener created to detect device conflicts and global variable conflicts
/**
- * simple tool to log state changes
+ * Simple listener tool to track remove unwanted ChoiceGenerators that are registered
+ * while an existing ChoiceGenerator is being explored. Multiple ChoiceGenerators of the same
+ * type could be registered spuriously during a while(true) loop.
*/
public class StateReducer extends ListenerAdapter {
+ private boolean debugMode;
+ private boolean stateReductionMode;
private final PrintWriter out;
- volatile private String valueVarLock = "";
- volatile private String valueVarContact = "";
- volatile private String operation;
- volatile private String detail;
- volatile private int depth;
- volatile private int id;
- Transition transition;
- Object annotation;
- String label;
- String output;
- int stateId;
-
-
- public StateReducer (Config conf, JPF jpf) {
- out = new PrintWriter(System.out, true);
+ private String detail;
+ 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) {
+ debugMode = config.getBoolean("debug_state_transition", false);
+ stateReductionMode = config.getBoolean("activate_state_reduction", true);
+ if (debugMode) {
+ out = new PrintWriter(System.out, true);
+ } else {
+ out = null;
+ }
+ detail = null;
+ depth = 0;
+ id = 0;
+ transition = null;
+ 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
public void stateRestored(Search search) {
- id = search.getStateId();
- depth = search.getDepth();
- operation = "restored";
- transition = search.getTransition();
- if (transition != null) {
- annotation = transition.getAnnotation();
- label = transition.getLabel();
- output = transition.getOutput();
- stateId = transition.getStateId();
+ if (debugMode) {
+ id = search.getStateId();
+ depth = search.getDepth();
+ transition = search.getTransition();
+ detail = null;
+ out.println("\n==> DEBUG: The state is restored to state with id: " + id + " -- Transition: " + transition +
+ " and depth: " + depth + "\n");
}
- detail = null;
-
- out.println("\nThe state is restored to state with id: "+id+" Transition: "+transition+", with depth: "+depth+"##LockValue: "+valueVarLock+", ##ContactValue: "+valueVarContact +"\n");
}
//--- the ones we are interested in
@Override
public void searchStarted(Search search) {
- out.println("----------------------------------- search started");
+ if (debugMode) {
+ out.println("\n==> DEBUG: ----------------------------------- search started" + "\n");
+ }
}
- // Holds values that have appeared during CG advances
- private HashSet<Integer> cgChoiceSet = new HashSet<>();
- private Integer choiceUpperBound = 0;
- private boolean isInitialized = false;
-
@Override
public void choiceGeneratorSet (VM vm, ChoiceGenerator<?> newCG) {
-
- // Initialize with necessary information from the CG
- if (newCG instanceof IntIntervalGenerator) {
- IntIntervalGenerator iigCG = (IntIntervalGenerator) newCG;
- // Check if CG has been initialized, otherwise initialize it
- if (!isInitialized) {
- Integer[] choices = iigCG.getChoices();
- // Get the upper bound from the last element of the choices
- choiceUpperBound = choices[choices.length - 1];
- isInitialized = true;
- } else {
- newCG.setDone();
+ if (stateReductionMode) {
+ // Initialize with necessary information from the CG
+ if (newCG instanceof IntIntervalGenerator) {
+ IntIntervalGenerator iigCG = (IntIntervalGenerator) newCG;
+ // Check if CG has been initialized, otherwise initialize it
+ if (!isInitialized) {
+ Integer[] choices = iigCG.getChoices();
+ // Get the upper bound from the last element of the choices
+ choiceUpperBound = choices[choices.length - 1];
+ isInitialized = true;
+ } else {
+ newCG.setDone();
+ }
}
}
}
@Override
public void choiceGeneratorAdvanced (VM vm, ChoiceGenerator<?> currentCG) {
- // 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) {
- IntIntervalGenerator iigCG = (IntIntervalGenerator) currentCG;
- Integer nextChoice = iigCG.getNextChoice();
- if (!cgChoiceSet.contains(nextChoice)) {
- cgChoiceSet.add(nextChoice);
+ if (stateReductionMode) {
+ // Check for BooleanChoiceGenerator
+ if (currentCG instanceof BooleanChoiceGenerator) {
+ bCGIsAdvanced++;
}
- // Allow reinitialization after an upper bound is hit
- // This means all available choices have been explored once during this iteration
- if (cgChoiceSet.contains(choiceUpperBound)) {
- isInitialized = false;
- cgChoiceSet.clear();
+ // 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) {
+ IntIntervalGenerator iigCG = (IntIntervalGenerator) currentCG;
+ Integer nextChoice = iigCG.getNextChoice();
+ if (!cgChoiceSet.contains(nextChoice)) {
+ cgChoiceSet.add(nextChoice);
+ }
+ // Allow reinitialization after an upper bound is hit
+ // This means all available choices have been explored once during this iteration
+ 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();
+ }
+ }
}
}
}
@Override
public void stateAdvanced(Search search) {
- String theEnd = null;
- id = search.getStateId();
- depth = search.getDepth();
- operation = "forward";
- transition = search.getTransition();
- if (transition != null) {
- annotation = transition.getAnnotation();
- label = transition.getLabel();
- output = transition.getOutput();
- stateId = transition.getStateId();
- }
- if (search.isNewState()) {
- detail = "new";
- } else {
- detail = "visited";
- }
+ if (debugMode) {
+ id = search.getStateId();
+ depth = search.getDepth();
+ transition = search.getTransition();
+ if (search.isNewState()) {
+ detail = "new";
+ } else {
+ detail = "visited";
+ }
- if (search.isEndState()) {
- out.println("This is the last state!");
- theEnd = "end";
+ if (search.isEndState()) {
+ out.println("\n==> DEBUG: This is the last state!\n");
+ detail += " end";
+ }
+ out.println("\n==> DEBUG: The state is forwarded to state with id: " + id + " with depth: " + depth +
+ " which is " + detail + " Transition: " + transition + "\n");
}
+ }
- //out.println("stateId: "+stateId+", output: "+output+", label: "+label);
- out.println("\nThe state is forwarded to state with id: "+id+", with depth: "+depth+" which is "+detail+" Transition: "+transition+" state: "+"% "+theEnd+"##LockValue: "+valueVarLock+", ##ContactValue: "+valueVarContact +"\n");
+ @Override
+ public void stateBacktracked(Search search) {
+ if (debugMode) {
+ id = search.getStateId();
+ depth = search.getDepth();
+ transition = search.getTransition();
+ detail = null;
- if (search.isEndState()) {
- detail += " end";
+ out.println("\n==> DEBUG: The state is backtracked to state with id: " + id + " -- Transition: " + transition +
+ " and depth: " + depth + "\n");
}
}
@Override
- public void stateBacktracked(Search search) {
- id = search.getStateId();
- depth = search.getDepth();
- operation = "backtrack";
- transition = search.getTransition();
- if (transition != null) {
- annotation = transition.getAnnotation();
- label = transition.getLabel();
- output = transition.getOutput();
- stateId = transition.getStateId();
+ public void searchFinished(Search search) {
+ if (debugMode) {
+ out.println("\n==> DEBUG: ----------------------------------- search finished" + "\n");
}
- detail = null;
-
- out.println("\nThe state is backtracked to state with id: "+id+" Transition: "+ transition+", with depth: "+depth+"##LockValue: "+valueVarLock+", ##ContactValue: "+valueVarContact +"\n");
}
@Override
- public void searchFinished(Search search) {
- out.println("----------------------------------- search finished");
+ 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
projects / jpf-core.git / blobdiff