import gov.nasa.jpf.vm.bytecode.ReadInstruction;
import gov.nasa.jpf.vm.bytecode.StoreInstruction;
import gov.nasa.jpf.vm.bytecode.WriteInstruction;
+import gov.nasa.jpf.vm.choice.IntChoiceFromSet;
import java.io.PrintWriter;
**/
public class ConflictTracker extends ListenerAdapter {
+ // Public graph: to allow the StateReducer class to access it
+ public static final HashMap<Integer, Node> nodes = new HashMap<Integer, Node>(); // Nodes of a graph
+ // Private
private final PrintWriter out;
private final HashSet<String> conflictSet = new HashSet<String>(); // Variables we want to track
private final HashSet<String> appSet = new HashSet<String>(); // Apps we want to find their conflicts
private final HashSet<String> manualSet = new HashSet<String>(); // Writer classes with manual inputs to detect direct-direct(No Conflict) interactions
- private final HashMap<Integer, Node> nodes = new HashMap<Integer, Node>(); // Nodes of a graph
private HashSet<Transition> transitions = new HashSet<Transition>();
private ArrayList<Update> currUpdates = new ArrayList<Update>();
private long timeout;
private int id;
private boolean manual = false;
private boolean conflictFound = false;
+ private int currentEvent = -1;
+ private boolean debugMode = false;
private final String SET_LOCATION_METHOD = "setLocationMode";
private final String LOCATION_VAR = "locationMode";
public ConflictTracker(Config config, JPF jpf) {
out = new PrintWriter(System.out, true);
+ debugMode = config.getBoolean("debug_mode", false);
String[] conflictVars = config.getStringArray("variables");
// We are not tracking anything if it is null
}
//Check for conflict with the appropriate update set if we are not a manual transition
- if (confupdates != null && !u.isManual()) {
+ //If this is debug mode, then we do not report any conflicts
+ if (!debugMode && confupdates != null && !u.isManual()) {
for(Update u2: confupdates) {
if (conflicts(u, u2)) {
//throw new RuntimeException(createErrorMessage(u, u2));
return message;
}
- Edge createEdge(Node parent, Node current, Transition transition) {
+ Edge createEdge(Node parent, Node current, Transition transition, int evtNum) {
//Check if this transition is explored. If so, just skip everything
if (transitions.contains(transition))
return null;
//Create edge
- Edge e = new Edge(parent, current, transition, currUpdates);
+ Edge e = new Edge(parent, current, transition, evtNum, currUpdates);
parent.addOutEdge(e);
//Mark transition as explored
static class Edge {
Node source, destination;
Transition transition;
+ int eventNumber;
ArrayList<Update> updates = new ArrayList<Update>();
- Edge(Node src, Node dst, Transition t, ArrayList<Update> _updates) {
+ Edge(Node src, Node dst, Transition t, int evtNum, ArrayList<Update> _updates) {
this.source = src;
this.destination = dst;
this.transition = t;
+ this.eventNumber = evtNum;
this.updates.addAll(_updates);
}
return transition;
}
+ int getEventNumber() { return eventNumber; }
+
ArrayList<Update> getUpdates() {
return updates;
}
System.out.println("}");
}
+
+ @Override
+ public void choiceGeneratorAdvanced(VM vm, ChoiceGenerator<?> currentCG) {
+
+ if (currentCG instanceof IntChoiceFromSet) {
+ IntChoiceFromSet icsCG = (IntChoiceFromSet) currentCG;
+ currentEvent = icsCG.getNextChoice();
+ }
+ }
@Override
public void stateAdvanced(Search search) {
Node currentNode = getNode(id);
// Create an edge based on the current transition
- Edge newEdge = createEdge(parentNode, currentNode, transition);
+ Edge newEdge = createEdge(parentNode, currentNode, transition, currentEvent);
// Reset the temporary variables and flags
currUpdates.clear();
private boolean debugMode;
private boolean stateReductionMode;
private final PrintWriter out;
- volatile private String detail;
- volatile private int depth;
- volatile private int id;
- Transition transition;
+ private String detail;
+ private int depth;
+ private int id;
+ private Transition transition;
// State reduction fields
private Integer[] choices;
// Stores explored backtrack lists in the form of HashSet of Strings
private HashSet<String> backtrackSet;
private HashMap<Integer, HashSet<Integer>> conflictPairMap;
- // Map choicelist with start index
- // private HashMap<Integer[],Integer> choiceListStartIndexMap;
// Map that represents graph G
// (i.e., visible operation dependency graph (VOD Graph)
// VOD graph is updated when the state has not yet been seen
// Current state
private int stateId;
- // Previous state
- private int prevStateId;
// Previous choice number
private int prevChoiceValue;
- // Counter for a visited state
- private HashMap<Integer, Integer> visitedStateCounter;
// HashSet that stores references to unused CGs
private HashSet<IntChoiceFromSet> unusedCG;
+ // Reference to the state graph in the ConflictTracker class
+ private HashMap<Integer, ConflictTracker.Node> stateGraph;
+ // Visited states in the previous and current executions/traces for terminating condition
+ private HashSet<Integer> prevVisitedStates;
+ private HashSet<Integer> currVisitedStates;
+
public StateReducer(Config config, JPF jpf) {
debugMode = config.getBoolean("debug_state_transition", false);
stateReductionMode = config.getBoolean("activate_state_reduction", true);
isBooleanCGFlipped = false;
vodGraphMap = new HashMap<>();
stateId = -1;
- prevStateId = -1;
prevChoiceValue = -1;
cgMap = new HashMap<>();
readWriteFieldsMap = new HashMap<>();
backtrackSet = new HashSet<>();
conflictPairMap = new HashMap<>();
unusedCG = new HashSet<>();
- visitedStateCounter = new HashMap<>();
+ // TODO: We are assuming that the StateReducer is always used together with the ConflictTracker
+ stateGraph = ConflictTracker.nodes;
+ prevVisitedStates = new HashSet<>();
+ currVisitedStates = new HashSet<>();
initializeStateReduction();
}
unusedCG.clear();
}
- private void incrementVisitedStateCounter(int stId) {
- // Increment counter for this state ID
- if (visitedStateCounter.containsKey(stId)) {
- int stateCount = visitedStateCounter.get(stId);
- visitedStateCounter.put(stId, stateCount + 1);
+ // Detect cycles in the current execution/trace
+ // We terminate the execution iff:
+ // (1) the state has been visited in the current execution
+ // (2) the state has one or more cycles that involve all the events
+ private boolean containsCyclesWithAllEvents(int stId) {
+
+ HashSet<Integer> visitedEvents = new HashSet<>();
+ boolean containsCyclesWithAllEvts = false;
+ ConflictTracker.Node currNode = stateGraph.get(stId);
+ for(ConflictTracker.Edge edge : currNode.getOutEdges()) {
+ dfsFindCycles(edge.getDst(), visitedEvents, new HashSet<>());
+ }
+ if (checkIfAllEventsInvolved(visitedEvents)) {
+ containsCyclesWithAllEvts = true;
+ }
+
+ return containsCyclesWithAllEvts;
+ }
+
+ private void dfsFindCycles(ConflictTracker.Node currNode, HashSet<Integer> visitedEvents,
+ HashSet<Integer> visitingEvents) {
+
+ // Stop when there is a cycle and record all the events
+ if (visitingEvents.contains(currNode.getId())) {
+ visitedEvents.addAll(visitingEvents);
} else {
- // If we have seen it then the frequency is 2
- visitedStateCounter.put(stId, 2);
+ for(ConflictTracker.Edge edge : currNode.getOutEdges()) {
+ visitingEvents.add(edge.getEventNumber());
+ dfsFindCycles(edge.getDst(), visitedEvents, visitingEvents);
+ visitingEvents.remove(edge.getEventNumber());
+ }
}
}
- private boolean isVisitedMultipleTimes(int stId) {
- // Return true if the state has been visited more than once
- if (visitedStateCounter.containsKey(stId) &&
- visitedStateCounter.get(stId) > 1) {
- return true;
+ private boolean checkIfAllEventsInvolved(HashSet<Integer> visitedEvents) {
+
+ // Check if this set contains all the event choices
+ // If not then this is not the terminating condition
+ for(int i=0; i<=choiceUpperBound; i++) {
+ if (!visitedEvents.contains(i)) {
+ return false;
+ }
}
- return false;
+ return true;
}
@Override
readWriteFieldsMap.clear();
choiceCounter = 0;
}
- if (!vm.isNewState()) {
- incrementVisitedStateCounter(stateId);
- }
- // Check if we have seen this state and it's not looping back to itself
- if (prevStateId != -1 && stateId != prevStateId && isVisitedMultipleTimes(stateId)) {
+ // Check if we have seen this state or this state contains cycles that involve all events
+// if (prevStateId != -1 && stateId != prevStateId && isVisitedMultipleTimes(stateId)) {
+ if (prevVisitedStates.contains(stateId) || containsCyclesWithAllEvents(stateId)) {
// Traverse the sub-graphs
if (isResetAfterAnalysis) {
// Advance choice counter for sub-graphs
resetAllCGs();
isResetAfterAnalysis = true;
}
+ // Save all the visited states
+ prevVisitedStates.addAll(currVisitedStates);
}
}
}
}
- public void updateVODGraph(int prevChoice, int currChoice) {
+ private void updateVODGraph(int prevChoice, int currChoice) {
HashSet<Integer> choiceSet;
if (vodGraphMap.containsKey(prevChoice)) {
choiceSet.add(currChoice);
}
- private void updateStateId(Search search) {
- // Saving the previous state
- prevStateId = stateId;
- // Line 19 in the paper page 11 (see the heading note above)
- stateId = search.getStateId();
- }
-
@Override
public void stateAdvanced(Search search) {
if (debugMode) {
currChoice = currChoice >= 0 ? currChoice % (choices.length -1) : currChoice;
if (currChoice < 0 || choices[currChoice] == -1 ||
prevChoiceValue == choices[currChoice]) {
-// || currChoice > choices.length - 1 || choices[currChoice] == -1 ||
-// prevChoiceValue == choices[currChoice]) {
-// // When current choice is 0, previous choice could be -1
+ // When current choice is 0, previous choice could be -1
// updateVODGraph(prevChoiceValue, choices[currChoice]);
-// // Current choice becomes previous choice in the next iteration
-// prevChoiceValue = choices[currChoice];
// Update the state ID variables
- updateStateId(search);
- // Handle all corner cases (e.g., out of bound values)
+ stateId = search.getStateId();
+ currVisitedStates.add(stateId);
return;
}
// When current choice is 0, previous choice could be -1
// Current choice becomes previous choice in the next iteration
prevChoiceValue = choices[currChoice];
// Update the state ID variables
- updateStateId(search);
+ stateId = search.getStateId();
+ currVisitedStates.add(stateId);
}
}
detail = null;
// Update the state variables
- // Saving the previous state
- prevStateId = stateId;
// Line 19 in the paper page 11 (see the heading note above)
stateId = search.getStateId();
projects / jpf-core.git / commitdiff