From 3e0a2fe1baa5e2530e75452524afdedba8045126 Mon Sep 17 00:00:00 2001 From: rtrimana Date: Wed, 15 Apr 2020 12:11:07 -0700 Subject: [PATCH] Fixing more potential bugs for the reachability analysis. --- main.jpf | 6 +++--- .../gov/nasa/jpf/listener/DPORStateReducer.java | 14 ++++++++++---- 2 files changed, 13 insertions(+), 7 deletions(-) diff --git a/main.jpf b/main.jpf index 81a40dc..4c3f7d9 100644 --- a/main.jpf +++ b/main.jpf @@ -9,8 +9,8 @@ target = main ##listener=gov.nasa.jpf.listener.ConflictTrackerOld,gov.nasa.jpf.listener.StateReducer ##listener=gov.nasa.jpf.listener.ConflictTrackerOld,gov.nasa.jpf.listener.DPORStateReducer #listener=gov.nasa.jpf.listener.ConflictTrackerOld -listener=gov.nasa.jpf.listener.DPORStateReducer -#listener=gov.nasa.jpf.listener.DPORStateReducer,gov.nasa.jpf.listener.ConflictTrackerOld +#listener=gov.nasa.jpf.listener.DPORStateReducer +listener=gov.nasa.jpf.listener.DPORStateReducer,gov.nasa.jpf.listener.ConflictTrackerOld # Potentially conflicting variables # Alarms @@ -44,7 +44,7 @@ apps=App1,App2 # Debug mode for ConflictTracker # We do not report any conflicts if the value is true -debug_mode=true +#debug_mode=true # Debug mode for StateReducer printout_state_transition=true diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java index 0c513f2..104af2b 100644 --- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java +++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java @@ -490,14 +490,14 @@ public class DPORStateReducer extends ListenerAdapter { // Update the state variables // Line 19 in the paper page 11 (see the heading note above) int stateId = search.getStateId(); - currVisitedStates.add(stateId); // Insert state ID into the map if it is new if (!stateToEventMap.containsKey(stateId)) { HashSet eventSet = new HashSet<>(); stateToEventMap.put(stateId, eventSet); } - justVisitedStates.add(stateId); analyzeReachabilityAndCreateBacktrackPoints(search.getVM(), stateId); + justVisitedStates.add(stateId); + currVisitedStates.add(stateId); } // --- Functions related to Read/Write access analysis on shared fields @@ -835,8 +835,14 @@ public class DPORStateReducer extends ListenerAdapter { // 2) We need to analyze and find conflicts for the reachable choices/events in the cycle // 3) Then we create a new backtrack point for every new conflict private void analyzeReachabilityAndCreateBacktrackPoints(VM vm, int stateId) { - // Perform this analysis only when there is a state match and state > 0 (state 0 is for boolean CG) - if (!vm.isNewState() && (stateId > 0)) { + // Perform this analysis only when: + // 1) there is a state match, + // 2) this is not during a switch to a new execution, + // 3) at least 2 choices/events have been explored (choiceCounter > 1), + // 4) the matched state has been encountered in the current execution, and + // 5) state > 0 (state 0 is for boolean CG) + if (!vm.isNewState() && !isEndOfExecution && choiceCounter > 1 && + currVisitedStates.contains(stateId) && (stateId > 0)) { // Find the choice/event that marks the start of this cycle: first choice we explore for conflicts int conflictChoice = stateToChoiceCounterMap.get(stateId); int currentChoice = choiceCounter - 1; -- 2.34.1