From 886e73644b1bac38152584c3234a826fddb53bc5 Mon Sep 17 00:00:00 2001 From: rtrimana Date: Tue, 5 Nov 2019 13:40:48 -0800 Subject: [PATCH] Completing POR implementation with complete recursions. --- .../gov/nasa/jpf/listener/StateReducer.java | 167 ++++++++++++------ 1 file changed, 110 insertions(+), 57 deletions(-) diff --git a/src/main/gov/nasa/jpf/listener/StateReducer.java b/src/main/gov/nasa/jpf/listener/StateReducer.java index 0a4c685..957940f 100644 --- a/src/main/gov/nasa/jpf/listener/StateReducer.java +++ b/src/main/gov/nasa/jpf/listener/StateReducer.java @@ -17,7 +17,6 @@ */ package gov.nasa.jpf.listener; -import com.sun.org.apache.xpath.internal.operations.Bool; import gov.nasa.jpf.Config; import gov.nasa.jpf.JPF; import gov.nasa.jpf.ListenerAdapter; @@ -54,6 +53,7 @@ public class StateReducer extends ListenerAdapter { Transition transition; // State reduction fields + private Integer[] choices; private int choiceCounter; private Integer choiceUpperBound; private boolean isInitialized; @@ -66,6 +66,8 @@ public class StateReducer extends ListenerAdapter { // e.g., event number 1 can have two backtrack sequences: {3,1,2,4,...} and {2,1,3,4,...} private HashMap> backtrackMap; private HashMap> conflictPairMap; + // Map choicelist with start index + private HashMap choiceListStartIndexMap; public StateReducer (Config config, JPF jpf) { debugMode = config.getBoolean("debug_state_transition", false); @@ -85,6 +87,7 @@ public class StateReducer extends ListenerAdapter { private void initializeStateReduction() { if (stateReductionMode) { + choices = null; choiceCounter = 0; choiceUpperBound = 0; isInitialized = false; @@ -93,6 +96,7 @@ public class StateReducer extends ListenerAdapter { readWriteFieldsMap = new HashMap<>(); backtrackMap = new HashMap<>(); conflictPairMap = new HashMap<>(); + choiceListStartIndexMap = new HashMap<>(); } } @@ -123,24 +127,27 @@ public class StateReducer extends ListenerAdapter { if (nextCG instanceof IntChoiceFromSet) { IntChoiceFromSet icsCG = (IntChoiceFromSet) nextCG; // Check if CG has been initialized, otherwise initialize it - Object[] choices = icsCG.getAllChoices(); + Integer[] cgChoices = icsCG.getAllChoices(); if (!isInitialized) { // Get the upper bound from the last element of the choices - choiceUpperBound = (Integer) choices[choices.length - 1]; + choiceUpperBound = (Integer) cgChoices[cgChoices.length - 1]; isInitialized = true; } // Record the subsequent Integer CGs only until we hit the upper bound - if (choiceCounter <= choiceUpperBound && !cgMap.containsValue(choiceCounter)) { + if (!isResetAfterAnalysis && choiceCounter <= choiceUpperBound && !cgMap.containsValue(choiceCounter)) { // Update the choices of the first CG and add '-1' - Integer[] newChoices = new Integer[choices.length + 1]; - System.arraycopy(choices, 0, newChoices, 0, choices.length); - newChoices[newChoices.length - 1] = -1; - icsCG.setNewValues(newChoices); + if (choices == null) { + // All the choices are always the same so we only need to update it once + choices = new Integer[cgChoices.length + 1]; + System.arraycopy(cgChoices, 0, choices, 0, cgChoices.length); + choices[choices.length - 1] = -1; + } + icsCG.setNewValues(choices); icsCG.reset(); // Advance the current Integer CG // This way we explore all the event numbers in the first pass - icsCG.advance(choiceCounter); - cgMap.put(icsCG, choiceCounter); + icsCG.advance(choices[choiceCounter]); + cgMap.put(icsCG, choices[choiceCounter]); choiceCounter++; } else { // Set done the subsequent CGs @@ -167,13 +174,15 @@ public class StateReducer extends ListenerAdapter { // Deploy the new choice list for this CG cg.setNewValues(choiceList); cg.reset(); + } else { + cg.setDone(); } } } @Override public void choiceGeneratorAdvanced (VM vm, ChoiceGenerator currentCG) { - + if(stateReductionMode) { // Check the boolean CG and if it is flipped, we are resetting the analysis if (currentCG instanceof BooleanChoiceGenerator) { @@ -187,25 +196,39 @@ public class StateReducer extends ListenerAdapter { // are chosen first before repeating the same choice of value twice! if (currentCG instanceof IntChoiceFromSet) { IntChoiceFromSet icsCG = (IntChoiceFromSet) currentCG; + // Update the current pointer to the current set of choices + if (choices == null || choices != icsCG.getAllChoices()) { + choiceListStartIndexMap.remove(choices); + choices = icsCG.getAllChoices(); + // Reset a few things for the sub-graph + conflictPairMap = new HashMap<>(); + readWriteFieldsMap = new HashMap<>(); + choiceCounter = 0; + } + // Traverse the sub-graphs + if (isResetAfterAnalysis) { + // Advance choice counter for sub-graphs + choiceCounter++; + // Do this for every CG after finishing each backtrack list + if (icsCG.getNextChoice() == -1) { + int event = cgMap.get(icsCG); + LinkedList choiceLists = backtrackMap.get(event); + if (choiceLists != null && choiceLists.peekFirst() != null) { + Integer[] choiceList = choiceLists.removeFirst(); + // Deploy the new choice list for this CG + icsCG.setNewValues(choiceList); + icsCG.reset(); + } else { + // Set done if this was the last backtrack list + icsCG.setDone(); + } + } + } // Update and reset the CG if needed (do this for the first time after the analysis) if (!isResetAfterAnalysis && icsCG.getNextChoice() == -1) { resetAllCGs(); isResetAfterAnalysis = true; } - // Do this for every CG after finishing each backtrack list - if (isResetAfterAnalysis && icsCG.getNextChoice() == -1) { - int event = cgMap.get(icsCG); - LinkedList choiceLists = backtrackMap.get(event); - if (choiceLists != null && choiceLists.peekFirst() != null) { - Integer[] choiceList = choiceLists.removeFirst(); - // Deploy the new choice list for this CG - icsCG.setNewValues(choiceList); - icsCG.reset(); - } else { - // Set done if this was the last backtrack list - icsCG.setDone(); - } - } } } } @@ -292,11 +315,11 @@ public class StateReducer extends ListenerAdapter { // Do the analysis to get Read and Write accesses to fields ReadWriteSet rwSet; // We already have an entry - if (readWriteFieldsMap.containsKey(currentChoice)) { - rwSet = readWriteFieldsMap.get(currentChoice); + if (readWriteFieldsMap.containsKey(choices[currentChoice])) { + rwSet = readWriteFieldsMap.get(choices[currentChoice]); } else { // We need to create a new entry rwSet = new ReadWriteSet(); - readWriteFieldsMap.put(currentChoice, rwSet); + readWriteFieldsMap.put(choices[currentChoice], rwSet); } int objectId = ((JVMFieldInstruction) executedInsn).getFieldInfo().getClassInfo().getClassObjectRef(); // Record the field in the map @@ -333,38 +356,61 @@ public class StateReducer extends ListenerAdapter { private void createBacktrackChoiceList(int currentChoice, int conflictEventNumber) { - int minChoice = Math.min(currentChoice, conflictEventNumber); - int maxChoice = Math.max(currentChoice, conflictEventNumber); LinkedList backtrackChoiceLists; // Check if we have a list for this choice number // If not we create a new one for it - if (!backtrackMap.containsKey(minChoice)) { + if (!backtrackMap.containsKey(conflictEventNumber)) { backtrackChoiceLists = new LinkedList<>(); - backtrackMap.put(minChoice, backtrackChoiceLists); + backtrackMap.put(conflictEventNumber, backtrackChoiceLists); } else { - backtrackChoiceLists = backtrackMap.get(minChoice); + backtrackChoiceLists = backtrackMap.get(conflictEventNumber); } - // TODO: The following might change depending on the POR implementation detail // Create a new list of choices for backtrack based on the current choice and conflicting event number // If we have a conflict between 1 and 3, then we create the list {3, 1, 2, 4, 5} for backtrack // The backtrack point is the CG for event number 1 and the list length is one less than the original list // (originally of length 6) since we don't start from event number 0 - int maxListLength = choiceUpperBound + 1; - int listLength = maxListLength - minChoice; - Integer[] choiceList = new Integer[listLength+1]; - // Put the conflicting event numbers first and reverse the order - choiceList[0] = maxChoice; - choiceList[1] = minChoice; - // Put the rest of the event numbers into the array starting from the minimum to the upper bound - for(int i = minChoice + 1, j = 2; j < listLength; i++) { - if (i != maxChoice) { - choiceList[j] = i; - j++; + if (!isResetAfterAnalysis) { + int maxListLength = choiceUpperBound + 1; + int listLength = maxListLength - conflictEventNumber; + Integer[] newChoiceList = new Integer[listLength + 1]; + // Put the conflicting event numbers first and reverse the order + newChoiceList[0] = choices[currentChoice]; + newChoiceList[1] = choices[conflictEventNumber]; + // Put the rest of the event numbers into the array starting from the minimum to the upper bound + for (int i = conflictEventNumber + 1, j = 2; j < listLength; i++) { + if (choices[i] != choices[currentChoice]) { + newChoiceList[j] = choices[i]; + j++; + } + } + // Set the last element to '-1' as the end of the sequence + newChoiceList[newChoiceList.length - 1] = -1; + backtrackChoiceLists.addLast(newChoiceList); + // The start index for the recursion is always 1 (from the main branch) + choiceListStartIndexMap.put(newChoiceList, 1); + } else { // This is a sub-graph + int listLength = choices.length; + Integer[] newChoiceList = new Integer[listLength]; + // Copy everything before the conflict number + for(int i = 0; i < conflictEventNumber; i++) { + newChoiceList[i] = choices[i]; } + // Put the conflicting events + newChoiceList[conflictEventNumber] = choices[currentChoice]; + newChoiceList[conflictEventNumber + 1] = choices[conflictEventNumber]; + // Copy the rest + for(int i = conflictEventNumber + 1, j = conflictEventNumber + 2; j < listLength - 1; i++) { + if (choices[i] != choices[currentChoice]) { + newChoiceList[j] = choices[i]; + j++; + } + } + // Set the last element to '-1' as the end of the sequence + newChoiceList[newChoiceList.length - 1] = -1; + backtrackChoiceLists.addLast(newChoiceList); + // For the sub-graph the start index depends on the conflicting event number + choiceListStartIndexMap.put(newChoiceList, conflictEventNumber + 1); } - // Set the last element to '-1' as the end of the sequence - choiceList[choiceList.length - 1] = -1; - backtrackChoiceLists.addLast(choiceList); } // We exclude fields that come from libraries (Java and Groovy), and also the infrastructure @@ -374,9 +420,9 @@ public class StateReducer extends ListenerAdapter { private final static String[] EXCLUDED_FIELDS_ENDS_WITH_LIST = // Groovy library created fields {"stMC", "callSiteArray", "metaClass", "staticClassInfo", "__constructor__", - // Infrastructure - "sendEvent", "Object", "reference", "location", "app", "state", "log", "functionList", "objectList", - "eventList", "valueList", "settings", "printToConsole", "app1", "app2"}; + // Infrastructure + "sendEvent", "Object", "reference", "location", "app", "state", "log", "functionList", "objectList", + "eventList", "valueList", "settings", "printToConsole", "app1", "app2"}; private final static String[] EXCLUDED_FIELDS_CONTAINS_LIST = {"_closure"}; private final static String[] EXCLUDED_FIELDS_WRITE_INSTRUCTIONS_STARTS_WITH_LIST = {"Event"}; @@ -407,6 +453,10 @@ public class StateReducer extends ListenerAdapter { public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) { if (stateReductionMode) { if (isInitialized) { + if (choiceCounter > choices.length - 1) { + // We do not compute the conflicts for the choice '-1' + return; + } int currentChoice = choiceCounter - 1; // Record accesses from executed instructions if (executedInsn instanceof JVMFieldInstruction) { @@ -426,21 +476,24 @@ public class StateReducer extends ListenerAdapter { String fieldClass = ((JVMFieldInstruction) nextInsn).getFieldInfo().getFullName(); // We don't care about libraries if (!isFieldExcluded(fieldClass)) { + // For the main graph we go down to 0, but for subgraph, we only go down to 1 since 0 contains + // the reversed event + int end = !isResetAfterAnalysis ? 0 : choiceListStartIndexMap.get(choices); // Check for conflict (go backward from currentChoice and get the first conflict) // If the current event has conflicts with multiple events, then these will be detected // one by one as this recursively checks backward when backtrack set is revisited and executed. - for (int eventNumber = currentChoice - 1; eventNumber >= 0; eventNumber--) { + for (int eventNumber = currentChoice - 1; eventNumber >= end; eventNumber--) { // Skip if this event number does not have any Read/Write set - if (!readWriteFieldsMap.containsKey(eventNumber)) { + if (!readWriteFieldsMap.containsKey(choices[eventNumber])) { continue; } - ReadWriteSet rwSet = readWriteFieldsMap.get(eventNumber); + ReadWriteSet rwSet = readWriteFieldsMap.get(choices[eventNumber]); int currObjId = ((JVMFieldInstruction) nextInsn).getFieldInfo().getClassInfo().getClassObjectRef(); // 1) Check for conflicts with Write fields for both Read and Write instructions if (((nextInsn instanceof WriteInstruction || nextInsn instanceof ReadInstruction) && - rwSet.writeFieldExists(fieldClass) && rwSet.writeFieldObjectId(fieldClass) == currObjId) || - (nextInsn instanceof WriteInstruction && rwSet.readFieldExists(fieldClass) && - rwSet.readFieldObjectId(fieldClass) == currObjId)) { + rwSet.writeFieldExists(fieldClass) && rwSet.writeFieldObjectId(fieldClass) == currObjId) || + (nextInsn instanceof WriteInstruction && rwSet.readFieldExists(fieldClass) && + rwSet.readFieldObjectId(fieldClass) == currObjId)) { // We do not record and service the same backtrack pair/point twice! // If it has been serviced before, we just skip this if (recordConflictPair(currentChoice, eventNumber)) { -- 2.34.1