Fixing issues: counter bugs, object ID comparison, exclusion of non-event and non...

diff --git a/src/main/gov/nasa/jpf/listener/StateReducer.java b/src/main/gov/nasa/jpf/listener/StateReducer.java
index ffeca2078d316eda1abcb806dde561fdc3d28ec5..8aa2c381c636597093e286a53480af3045af30bb 100644 (file)
--- 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
           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);
           // 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
   }
 
   // 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 class ReadWriteSet {

-    private HashSet<String> readSet;
-    private HashSet<String> writeSet;
+    private HashMap<String,Integer> readSet;
+    private HashMap<String,Integer> writeSet;

 
     public ReadWriteSet() {
 
     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) {
     }
 
     public boolean readFieldExists(String field) {

-      return readSet.contains(field);
+      return readSet.containsKey(field);

     }
 
     public boolean writeFieldExists(String 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
     // 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();
     } 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) {
     // 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) {
   @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
           // 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("<init>")) {
+            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;
+                  }
+                }

               }
             }
           }
               }
             }
           }