From 149f8d9e0d9cc78662abc4e42db3ac2c177b6811 Mon Sep 17 00:00:00 2001 From: rtrimana Date: Fri, 27 Mar 2020 15:55:00 -0700 Subject: [PATCH] Re-checking and cleaning up the code: most likely still have a bug in re-ordering the two apps. --- .../gov/nasa/jpf/listener/StateReducer.java | 159 +++++++++++------- .../nasa/jpf/vm/choice/IntChoiceFromSet.java | 7 - 2 files changed, 96 insertions(+), 70 deletions(-) diff --git a/src/main/gov/nasa/jpf/listener/StateReducer.java b/src/main/gov/nasa/jpf/listener/StateReducer.java index e031354..91c0b11 100644 --- a/src/main/gov/nasa/jpf/listener/StateReducer.java +++ b/src/main/gov/nasa/jpf/listener/StateReducer.java @@ -26,7 +26,9 @@ import gov.nasa.jpf.vm.*; import gov.nasa.jpf.vm.bytecode.ReadInstruction; import gov.nasa.jpf.vm.bytecode.WriteInstruction; import gov.nasa.jpf.vm.choice.IntChoiceFromSet; +import gov.nasa.jpf.vm.choice.IntIntervalGenerator; +import java.awt.*; import java.io.PrintWriter; import java.util.*; @@ -139,6 +141,9 @@ public class StateReducer extends ListenerAdapter { resetReadWriteAnalysis(); backtrackMap.clear(); backtrackSet.clear(); + stateToEventMap.clear(); + prevVisitedStates.clear(); + currVisitedStates.clear(); } } @@ -188,9 +193,9 @@ public class StateReducer extends ListenerAdapter { } private void continueExecutingThisTrace(IntChoiceFromSet icsCG) { - // We repeat the same trace if a state match is not found yet - IntChoiceFromSet setCG = setNewCG(icsCG); - unusedCG.add(setCG); + // We repeat the same trace if a state match is not found yet + IntChoiceFromSet setCG = setNewCG(icsCG); + unusedCG.add(setCG); } private void initializeChoiceGenerators(IntChoiceFromSet icsCG, Integer[] cgChoices) { @@ -245,7 +250,6 @@ public class StateReducer extends ListenerAdapter { //icsCG.setDone(); manageChoiceGeneratorsInSubsequentTraces(icsCG); } - choiceCounter++; } } } @@ -259,6 +263,8 @@ public class StateReducer extends ListenerAdapter { } private void resetAllCGs() { + + isResetAfterAnalysis = true; // Extract the event numbers that have backtrack lists Set eventSet = backtrackMap.keySet(); // Return if there is no conflict at all (highly unlikely) @@ -294,6 +300,10 @@ public class StateReducer extends ListenerAdapter { // Basically, we have to check that we have executed all events between two occurrences of such state. private boolean containsCyclesWithAllEvents(int stId) { + // False if the state ID hasn't been recorded + if (!stateToEventMap.containsKey(stId)) { + return false; + } HashSet visitedEvents = stateToEventMap.get(stId); boolean containsCyclesWithAllEvts = false; if (checkIfAllEventsInvolved(visitedEvents)) { @@ -333,14 +343,61 @@ public class StateReducer extends ListenerAdapter { } } + private void checkAndEnforceFairScheduling(IntChoiceFromSet icsCG) { + // Check the next choice and if the value is not the same as the expected then force the expected value + int choiceIndex = choiceCounter % refChoices.length; + int nextChoice = icsCG.getNextChoice(); + if (refChoices[choiceIndex] != nextChoice) { + int expectedChoice = refChoices[choiceIndex]; + int currCGIndex = icsCG.getNextChoiceIndex(); + if ((currCGIndex >= 0) && (currCGIndex < refChoices.length)) { + icsCG.setChoice(currCGIndex, expectedChoice); + } + } + } + + private void mapStateToEvent(int nextChoiceValue) { + // Update all states with this event/choice + // This means that all past states now see this transition + Set stateSet = stateToEventMap.keySet(); + for(Integer stateId : stateSet) { + HashSet eventSet = stateToEventMap.get(stateId); + eventSet.add(nextChoiceValue); + } + } + + private void updateVODGraph(int currChoiceValue) { + // Update the graph when we have the current choice value + HashSet choiceSet; + if (vodGraphMap.containsKey(prevChoiceValue)) { + // If the key already exists, just retrieve it + choiceSet = vodGraphMap.get(prevChoiceValue); + } else { + // Create a new entry + choiceSet = new HashSet<>(); + vodGraphMap.put(prevChoiceValue, choiceSet); + } + choiceSet.add(currChoiceValue); + prevChoiceValue = currChoiceValue; + } + + private boolean terminateCurrentExecution() { + // We need to check all the states that have just been visited + // Often a transition (choice/event) can result into forwarding/backtracking to a number of states + for(Integer stateId : justVisitedStates) { + if (prevVisitedStates.contains(stateId) || containsCyclesWithAllEvents(stateId)) { + return true; + } + } + return false; + } + private void exploreNextBacktrackSets(IntChoiceFromSet icsCG) { // Traverse the sub-graphs if (isResetAfterAnalysis) { // Do this for every CG after finishing each backtrack list // We try to update the CG with a backtrack list if the state has been visited multiple times - //if ((icsCG.getNextChoice() == -1 || choiceCounter > 1) && cgMap.containsKey(icsCG)) { - //if ((!icsCG.hasMoreChoices() || choiceCounter > 1) && cgMap.containsKey(icsCG)) { - if (choiceCounter > 1 && cgMap.containsKey(icsCG)) { + if (icsCG.getNextChoiceIndex() > 0 && cgMap.containsKey(icsCG)) { int event = cgMap.get(icsCG); LinkedList choiceLists = backtrackMap.get(event); if (choiceLists != null && choiceLists.peekFirst() != null) { @@ -359,37 +416,16 @@ public class StateReducer extends ListenerAdapter { // Update and reset the CG if needed (do this for the first time after the analysis) // Start backtracking if this is a visited state and it is not a repeating state resetAllCGs(); - isResetAfterAnalysis = true; } } - private void checkAndEnforceFairScheduling(IntChoiceFromSet icsCG) { - // Check the next choice and if the value is not the same as the expected then force the expected value - int choiceIndex = (choiceCounter - 1) % refChoices.length; - if (choices[choiceIndex] != icsCG.getNextChoiceIndex()) { - int expectedChoice = refChoices[choiceIndex]; - int currCGIndex = icsCG.getNextChoiceIndex(); - if ((currCGIndex >= 0) && (currCGIndex < refChoices.length)) { - icsCG.setChoice(currCGIndex, expectedChoice); - } - } - } - - private boolean terminateCurrentExecution() { - // We need to check all the states that have just been visited - // Often a transition (choice/event) can result into forwarding/backtracking to a number of states - for(Integer stateId : justVisitedStates) { - if (prevVisitedStates.contains(stateId) || containsCyclesWithAllEvents(stateId)) { - return true; - } - } - return false; - } - @Override public void choiceGeneratorAdvanced(VM vm, ChoiceGenerator currentCG) { if (stateReductionMode) { + if (vm.getNextChoiceGenerator() instanceof BooleanChoiceGenerator) { + System.out.println("Next CG is a booleanCG"); + } // Check the boolean CG and if it is flipped, we are resetting the analysis if (currentCG instanceof BooleanChoiceGenerator) { if (!isBooleanCGFlipped) { @@ -404,44 +440,28 @@ public class StateReducer extends ListenerAdapter { IntChoiceFromSet icsCG = (IntChoiceFromSet) currentCG; // Update the current pointer to the current set of choices updateChoicesForNewExecution(icsCG); + // If we don't see a fair scheduling of events/choices then we have to enforce it + checkAndEnforceFairScheduling(icsCG); + // Map state to event + mapStateToEvent(icsCG.getNextChoice()); + // Update the VOD graph always with the latest + updateVODGraph(icsCG.getNextChoice()); // Check if we have seen this state or this state contains cycles that involve all events if (terminateCurrentExecution()) { exploreNextBacktrackSets(icsCG); } justVisitedStates.clear(); - // If we don't see a fair scheduling of events/choices then we have to enforce it - checkAndEnforceFairScheduling(icsCG); - // Update the VOD graph always with the latest - updateVODGraph(icsCG.getNextChoice()); + choiceCounter++; } } } - private void updateVODGraph(int currChoiceValue) { - // Update the graph when we have the current choice value - HashSet choiceSet; - if (vodGraphMap.containsKey(prevChoiceValue)) { - // If the key already exists, just retrieve it - choiceSet = vodGraphMap.get(prevChoiceValue); - } else { - // Create a new entry - choiceSet = new HashSet<>(); - vodGraphMap.put(prevChoiceValue, choiceSet); - } - choiceSet.add(currChoiceValue); - prevChoiceValue = currChoiceValue; - } - - private void mapStateToEvent(Search search, int stateId) { - // Insert state ID and event choice into the map - HashSet eventSet; - if (stateToEventMap.containsKey(stateId)) { - eventSet = stateToEventMap.get(stateId); - } else { - eventSet = new HashSet<>(); + private void checkAndRecordNewState(int stateId) { + // Insert state ID into the map if it is new + if (!stateToEventMap.containsKey(stateId)) { + HashSet eventSet = new HashSet<>(); stateToEventMap.put(stateId, eventSet); } - eventSet.add(prevChoiceValue); } private void updateStateInfo(Search search) { @@ -450,7 +470,7 @@ public class StateReducer extends ListenerAdapter { // Line 19 in the paper page 11 (see the heading note above) int stateId = search.getStateId(); currVisitedStates.add(stateId); - mapStateToEvent(search, stateId); + checkAndRecordNewState(stateId); justVisitedStates.add(stateId); } } @@ -740,13 +760,26 @@ public class StateReducer extends ListenerAdapter { return false; } + private int getCurrentChoice(VM vm) { + ChoiceGenerator currentCG = vm.getChoiceGenerator(); + // This is the main event CG + if (currentCG instanceof IntChoiceFromSet) { + return ((IntChoiceFromSet) currentCG).getNextChoiceIndex(); + } else { + // This is the interval CG used in device handlers + ChoiceGenerator parentCG = ((IntIntervalGenerator) currentCG).getPreviousChoiceGenerator(); + return ((IntChoiceFromSet) parentCG).getNextChoiceIndex(); + } + } + @Override public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) { if (stateReductionMode) { - if (isInitialized) { - int currentChoice = (choiceCounter % refChoices.length) - 1; - if (currentChoice < 0) { - // We do not compute the conflicts for the choice '-1' + // Has to be initialized and a integer CG + ChoiceGenerator cg = vm.getChoiceGenerator(); + if (isInitialized && (cg instanceof IntChoiceFromSet || cg instanceof IntIntervalGenerator)) { + int currentChoice = getCurrentChoice(vm); + if (currentChoice < 0) { // If choice is -1 then skip return; } // Record accesses from executed instructions diff --git a/src/main/gov/nasa/jpf/vm/choice/IntChoiceFromSet.java b/src/main/gov/nasa/jpf/vm/choice/IntChoiceFromSet.java index eb2f33b..be11436 100644 --- a/src/main/gov/nasa/jpf/vm/choice/IntChoiceFromSet.java +++ b/src/main/gov/nasa/jpf/vm/choice/IntChoiceFromSet.java @@ -68,13 +68,6 @@ public class IntChoiceFromSet extends IntChoiceFromList { count = -1; } - // TODO: Fix for Groovy's model-checking - // TODO: This is a setter to change the values of the ChoiceGenerator to implement POR - @Override - public void setNewValues(Integer[] vals) { - values = vals; - } - @Override public Integer[] getAllChoices() { return values; -- 2.34.1