Adding graph traversal to find cycles; adding debug mode for ConflictTracker.

[jpf-core.git] / src / main / gov / nasa / jpf / listener / ConflictTracker.java

diff --git a/src/main/gov/nasa/jpf/listener/ConflictTracker.java b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
index 384056ee12abc750d28c340af0749361d9d1237b..791a7dad4b2d67eb3e629a74f8bfb8d5b1158384 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/ConflictTracker.java
+++ b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
@@ -27,6 +27,7 @@ import gov.nasa.jpf.vm.bytecode.LocalVariableInstruction;
 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;
 
@@ -37,11 +38,13 @@ import java.util.*;
  **/
 
 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;
@@ -54,12 +57,15 @@ public class ConflictTracker extends ListenerAdapter {
   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
@@ -124,7 +130,8 @@ public class ConflictTracker extends ListenerAdapter {
       }
 
       //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));
@@ -174,13 +181,13 @@ public class ConflictTracker extends ListenerAdapter {
     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
@@ -218,12 +225,14 @@ public class ConflictTracker extends ListenerAdapter {
   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);
     }
 
@@ -239,6 +248,8 @@ public class ConflictTracker extends ListenerAdapter {
       return transition;
     }
 
+    int getEventNumber() { return eventNumber; }
+
     ArrayList<Update> getUpdates() {
       return updates;
     }
@@ -371,6 +382,15 @@ public class ConflictTracker extends ListenerAdapter {
 
     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) {
@@ -384,7 +404,7 @@ public class ConflictTracker extends ListenerAdapter {
     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();