From: rtrimana Date: Thu, 19 Mar 2020 18:14:58 +0000 (-0700) Subject: Adding graph traversal to find cycles; adding debug mode for ConflictTracker. X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=commitdiff_plain;h=aeacdb3b4f77671a80702048907d8cf83f789e5b Adding graph traversal to find cycles; adding debug mode for ConflictTracker. --- diff --git a/main.jpf b/main.jpf index 35b5ea4..9ce7d13 100644 --- 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) diff --git a/src/main/gov/nasa/jpf/listener/ConflictTracker.java b/src/main/gov/nasa/jpf/listener/ConflictTracker.java index 384056e..791a7da 100644 --- 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 nodes = new HashMap(); // Nodes of a graph + // Private private final PrintWriter out; private final HashSet conflictSet = new HashSet(); // Variables we want to track private final HashSet appSet = new HashSet(); // Apps we want to find their conflicts private final HashSet manualSet = new HashSet(); // Writer classes with manual inputs to detect direct-direct(No Conflict) interactions - private final HashMap nodes = new HashMap(); // Nodes of a graph private HashSet transitions = new HashSet(); private ArrayList currUpdates = new ArrayList(); 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 updates = new ArrayList(); - Edge(Node src, Node dst, Transition t, ArrayList _updates) { + Edge(Node src, Node dst, Transition t, int evtNum, ArrayList _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 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(); diff --git a/src/main/gov/nasa/jpf/listener/StateReducer.java b/src/main/gov/nasa/jpf/listener/StateReducer.java index 71eaf32..ec2fe98 100644 --- a/src/main/gov/nasa/jpf/listener/StateReducer.java +++ b/src/main/gov/nasa/jpf/listener/StateReducer.java @@ -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 backtrackSet; private HashMap> conflictPairMap; - // Map choicelist with start index - // private HashMap 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 visitedStateCounter; // HashSet that stores references to unused CGs private HashSet unusedCG; + // Reference to the state graph in the ConflictTracker class + private HashMap stateGraph; + // Visited states in the previous and current executions/traces for terminating condition + private HashSet prevVisitedStates; + private HashSet 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 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 visitedEvents, + HashSet 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 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 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();