Adding graph traversal to find cycles; adding debug mode for ConflictTracker.
authorrtrimana <rtrimana@uci.edu>
Thu, 19 Mar 2020 18:14:58 +0000 (11:14 -0700)
committerrtrimana <rtrimana@uci.edu>
Thu, 19 Mar 2020 18:14:58 +0000 (11:14 -0700)
main.jpf
src/main/gov/nasa/jpf/listener/ConflictTracker.java
src/main/gov/nasa/jpf/listener/StateReducer.java

index 35b5ea4..9ce7d13 100644 (file)
--- a/main.jpf
+++ b/main.jpf
@@ -6,11 +6,11 @@ target = main
 #listener=gov.nasa.jpf.listener.StateReducerOld
 #listener=gov.nasa.jpf.listener.VariableConflictTracker,gov.nasa.jpf.listener.StateReducer
 #listener=gov.nasa.jpf.listener.ConflictTracker,gov.nasa.jpf.listener.StateReducer
+listener=gov.nasa.jpf.listener.ConflictTracker
 
 #listener=gov.nasa.jpf.listener.ConflictTracker,gov.nasa.jpf.listener.StateReducerClean
-#listener=gov.nasa.jpf.listener.ConflictTracker
 #listener=gov.nasa.jpf.listener.StateReducerClean
-listener=gov.nasa.jpf.listener.StateReducer
+#listener=gov.nasa.jpf.listener.StateReducer
 
 # Potentially conflicting variables
 # Alarms
@@ -41,11 +41,12 @@ variables=currentLock
 # Potentially conflicting apps (we default to App1 and App2 for now)
 apps=App1,App2
 
-# Tracking the location.mode variable conflict
-#track_location_var_conflict=true
+# Debug mode for ConflictTracker
+# We do not report any conflicts if the value is true
+debug_mode=true
 
 # Debug mode for StateReducer
-debug_state_transition=true
+#debug_state_transition=true
 #activate_state_reduction=true
 
 # Timeout in minutes (default is 0 which means no timeout)
index 384056e..791a7da 100644 (file)
@@ -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();
index 71eaf32..ec2fe98 100644 (file)
@@ -52,10 +52,10 @@ public class StateReducer extends ListenerAdapter {
   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;
@@ -75,8 +75,6 @@ public class StateReducer extends ListenerAdapter {
   // 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)
@@ -86,15 +84,17 @@ public class StateReducer extends ListenerAdapter {
   // 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);
@@ -110,7 +110,6 @@ public class StateReducer extends ListenerAdapter {
     isBooleanCGFlipped = false;
     vodGraphMap = new HashMap<>();
     stateId = -1;
-    prevStateId = -1;
     prevChoiceValue = -1;
     cgMap = new HashMap<>();
     readWriteFieldsMap = new HashMap<>();
@@ -118,7 +117,10 @@ public class StateReducer extends ListenerAdapter {
     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();
   }
 
@@ -241,24 +243,50 @@ public class StateReducer extends ListenerAdapter {
     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
@@ -286,11 +314,9 @@ public class StateReducer extends ListenerAdapter {
           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
@@ -316,12 +342,14 @@ public class StateReducer extends ListenerAdapter {
             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)) {
@@ -335,13 +363,6 @@ public class StateReducer extends ListenerAdapter {
     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) {
@@ -368,15 +389,11 @@ public class StateReducer extends ListenerAdapter {
       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
@@ -384,7 +401,8 @@ public class StateReducer extends ListenerAdapter {
       // 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);
     }
   }
 
@@ -397,8 +415,6 @@ public class StateReducer extends ListenerAdapter {
       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();