X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=blobdiff_plain;f=src%2Fmain%2Fgov%2Fnasa%2Fjpf%2Flistener%2FStateReducer.java;h=8aa2c381c636597093e286a53480af3045af30bb;hp=ffeca2078d316eda1abcb806dde561fdc3d28ec5;hb=76bdd87b5c4d921fc9949c225bb1dd22e70d7dfa;hpb=92913d69d358e98252d0278b5b96d7973566a958 diff --git a/src/main/gov/nasa/jpf/listener/StateReducer.java b/src/main/gov/nasa/jpf/listener/StateReducer.java index ffeca20..8aa2c38 100644 --- a/src/main/gov/nasa/jpf/listener/StateReducer.java +++ b/src/main/gov/nasa/jpf/listener/StateReducer.java @@ -130,7 +130,7 @@ public class StateReducer extends ListenerAdapter { isInitialized = true; } // Record the subsequent Integer CGs only until we hit the upper bound - if (choiceCounter < choiceUpperBound && !cgMap.containsValue(choiceCounter)) { + if (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); @@ -252,48 +252,58 @@ public class StateReducer extends ListenerAdapter { } // This class compactly stores Read and Write field sets + // We store the field name and its object ID + // Sharing the same field means the same field name and object ID private class ReadWriteSet { - private HashSet readSet; - private HashSet writeSet; + private HashMap readSet; + private HashMap writeSet; public ReadWriteSet() { - readSet = new HashSet<>(); - writeSet = new HashSet<>(); + readSet = new HashMap<>(); + writeSet = new HashMap<>(); } - public void addReadField(String field) { - readSet.add(field); + public void addReadField(String field, int objectId) { + readSet.put(field, objectId); } - public void addWriteField(String field) { - writeSet.add(field); + public void addWriteField(String field, int objectId) { + writeSet.put(field, objectId); } public boolean readFieldExists(String field) { - return readSet.contains(field); + return readSet.containsKey(field); } public boolean writeFieldExists(String field) { - return writeSet.contains(field); + return writeSet.containsKey(field); + } + + public int readFieldObjectId(String field) { + return readSet.get(field); + } + + public int writeFieldObjectId(String field) { + return writeSet.get(field); } } - private void analyzeReadWriteAccesses(Instruction executedInsn, String fieldClass) { + private void analyzeReadWriteAccesses(Instruction executedInsn, String fieldClass, int currentChoice) { // Do the analysis to get Read and Write accesses to fields ReadWriteSet rwSet; // We already have an entry - if (readWriteFieldsMap.containsKey(choiceCounter)) { - rwSet = readWriteFieldsMap.get(choiceCounter); + if (readWriteFieldsMap.containsKey(currentChoice)) { + rwSet = readWriteFieldsMap.get(currentChoice); } else { // We need to create a new entry rwSet = new ReadWriteSet(); - readWriteFieldsMap.put(choiceCounter, rwSet); + readWriteFieldsMap.put(currentChoice, rwSet); } + int objectId = ((JVMFieldInstruction) executedInsn).getFieldInfo().getClassInfo().getClassObjectRef(); // Record the field in the map if (executedInsn instanceof WriteInstruction) { - rwSet.addWriteField(fieldClass); - } - if (executedInsn instanceof ReadInstruction) { - rwSet.addReadField(fieldClass); + rwSet.addWriteField(fieldClass, objectId); + } else if (executedInsn instanceof ReadInstruction) { + rwSet.addReadField(fieldClass, objectId); } } @@ -354,64 +364,71 @@ public class StateReducer extends ListenerAdapter { @Override public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) { if (stateReductionMode) { - // Record accesses from executed instructions - if (executedInsn instanceof JVMFieldInstruction) { - String fieldClass = ((JVMFieldInstruction) executedInsn).getFieldInfo().getFullName(); - // We don't care about libraries - if (!fieldClass.startsWith("java") && - !fieldClass.startsWith("org") && - !fieldClass.startsWith("sun") && - !fieldClass.startsWith("com") && - !fieldClass.startsWith("gov") && - !fieldClass.startsWith("groovy") && - // and fields generated for the Groovy library - !fieldClass.endsWith("stMC") && - !fieldClass.endsWith("callSiteArray") && - !fieldClass.endsWith("metaClass") && - !fieldClass.endsWith("staticClassInfo") && - !fieldClass.endsWith("__constructor__")) { + if (isInitialized) { + int currentChoice = choiceCounter - 1; + // Record accesses from executed instructions + if (executedInsn instanceof JVMFieldInstruction) { // Analyze only after being initialized - if (isInitialized) { - analyzeReadWriteAccesses(executedInsn, fieldClass); + String fieldClass = ((JVMFieldInstruction) executedInsn).getFieldInfo().getFullName(); + // We don't care about libraries + if (!fieldClass.startsWith("java") && + !fieldClass.startsWith("org") && + !fieldClass.startsWith("sun") && + !fieldClass.startsWith("com") && + !fieldClass.startsWith("gov") && + !fieldClass.startsWith("groovy") && + // and fields generated for the Groovy library + !fieldClass.endsWith("stMC") && + !fieldClass.endsWith("callSiteArray") && + !fieldClass.endsWith("metaClass") && + !fieldClass.endsWith("staticClassInfo") && + !fieldClass.endsWith("__constructor__")) { + analyzeReadWriteAccesses(executedInsn, fieldClass, currentChoice); } } - } - // Analyze conflicts from next instructions - if (nextInsn instanceof JVMFieldInstruction) { - String fieldClass = ((JVMFieldInstruction) nextInsn).getFieldInfo().getFullName(); - // We don't care about libraries - if (!fieldClass.startsWith("java") && - !fieldClass.startsWith("org") && - !fieldClass.startsWith("sun") && - !fieldClass.startsWith("com") && - !fieldClass.startsWith("gov") && - !fieldClass.startsWith("groovy") && - // and fields generated for the Groovy library - !fieldClass.endsWith("stMC") && - !fieldClass.endsWith("callSiteArray") && - !fieldClass.endsWith("metaClass") && - !fieldClass.endsWith("staticClassInfo") && - !fieldClass.endsWith("__constructor__")) { - // 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=choiceCounter-1; eventNumber>=0; eventNumber--) { - // Skip if this event number does not have any Read/Write set - if (!readWriteFieldsMap.containsKey(eventNumber)) { - continue; - } - ReadWriteSet rwSet = readWriteFieldsMap.get(eventNumber); - // 1) Check for conflicts with Write fields for both Read and Write instructions - // 2) Check for conflicts with Read fields for Write instructions - if (((nextInsn instanceof WriteInstruction || nextInsn instanceof ReadInstruction) && - rwSet.writeFieldExists(fieldClass)) || - (nextInsn instanceof WriteInstruction && rwSet.readFieldExists(fieldClass))) { - // We do not record and service the same backtrack pair/point twice! - // If it has been serviced before, we just skip this - if (recordConflictPair(choiceCounter, eventNumber)) { - createBacktrackChoiceList(choiceCounter, eventNumber); - // Break if a conflict is found! - break; + // Analyze conflicts from next instructions + if (nextInsn instanceof JVMFieldInstruction) { + // The constructor is only called once when the object is initialized + // It does not have shared access with other objects + MethodInfo mi = nextInsn.getMethodInfo(); + if (!mi.getName().equals("")) { + String fieldClass = ((JVMFieldInstruction) nextInsn).getFieldInfo().getFullName(); + // We don't care about libraries + if (!fieldClass.startsWith("java") && + !fieldClass.startsWith("org") && + !fieldClass.startsWith("sun") && + !fieldClass.startsWith("com") && + !fieldClass.startsWith("gov") && + !fieldClass.startsWith("groovy") && + // and fields generated for the Groovy library + !fieldClass.endsWith("stMC") && + !fieldClass.endsWith("callSiteArray") && + !fieldClass.endsWith("metaClass") && + !fieldClass.endsWith("staticClassInfo") && + !fieldClass.endsWith("__constructor__")) { + // 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--) { + // Skip if this event number does not have any Read/Write set + if (!readWriteFieldsMap.containsKey(eventNumber)) { + continue; + } + ReadWriteSet rwSet = readWriteFieldsMap.get(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)) { + // 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)) { + createBacktrackChoiceList(currentChoice, eventNumber); + // Break if a conflict is found! + break; + } + } } } }