Fixing bugs: capturing object accesses (read/write) in iterators.

diff --git a/src/main/gov/nasa/jpf/listener/StateReducer.java b/src/main/gov/nasa/jpf/listener/StateReducer.java
index 94b78f8ea866da2629abb0a01463c51a88c894b0..78f1fed2237a3352556a1e6594525b8b86ed9c8e 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/StateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/StateReducer.java
@@ -557,14 +557,7 @@ public class StateReducer extends ListenerAdapter {
 
   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(refChoices[currentChoice])) {
-      rwSet = readWriteFieldsMap.get(refChoices[currentChoice]);
-    } else { // We need to create a new entry
-      rwSet = new ReadWriteSet();
-      readWriteFieldsMap.put(refChoices[currentChoice], rwSet);
-    }
+    ReadWriteSet rwSet = getReadWriteSet(currentChoice);
     int objectId = ((JVMFieldInstruction) executedInsn).getFieldInfo().getClassInfo().getClassObjectRef();
     // Record the field in the map
     if (executedInsn instanceof WriteInstruction) {
@@ -691,9 +684,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"};
 
@@ -770,6 +763,64 @@ public class StateReducer extends ListenerAdapter {
     }
   }
 
+  private final static String GROOVY_CALLSITE_LIB = "org.codehaus.groovy.runtime.callsite";
+  private final static String JAVA_STRING_LIB = "java.lang.String";
+  private final static String JAVA_INTEGER = "int";
+  private final static String DO_CALL_METHOD = "doCall";
+  private final static String GET_PROPERTY_METHOD =
+          "invokeinterface org.codehaus.groovy.runtime.callsite.CallSite.callGetProperty";
+  private final static String[] EXCLUDED_FIELDS_ITERATOR = {"java.util.LinkedHashMap"};
+
+  private ReadWriteSet getReadWriteSet(int currentChoice) {
+    // Do the analysis to get Read and Write accesses to fields
+    ReadWriteSet rwSet;
+    // We already have an entry
+    if (readWriteFieldsMap.containsKey(refChoices[currentChoice])) {
+      rwSet = readWriteFieldsMap.get(refChoices[currentChoice]);
+    } else { // We need to create a new entry
+      rwSet = new ReadWriteSet();
+      readWriteFieldsMap.put(refChoices[currentChoice], rwSet);
+    }
+    return rwSet;
+  }
+
+  private void analyzeReadWriteAccesses(Instruction instruction, ThreadInfo ti, int currentChoice) {
+    // Get method name
+    INVOKEINTERFACE insn = (INVOKEINTERFACE) instruction;
+    if (insn.toString().startsWith(GET_PROPERTY_METHOD) &&
+            insn.getMethodInfo().getName().equals(DO_CALL_METHOD)) {
+      // Extract info from the stack frame
+      StackFrame frame = ti.getTopFrame();
+      int[] frameSlots = frame.getSlots();
+      // Get the Groovy callsite library at index 0
+      ElementInfo eiCallsite = VM.getVM().getHeap().get(frameSlots[0]);
+      if (!eiCallsite.getClassInfo().getName().startsWith(GROOVY_CALLSITE_LIB)) {
+        return;
+      }
+      // Get the iterated object whose property is accessed
+      ElementInfo eiAccessObj = VM.getVM().getHeap().get(frameSlots[1]);
+      // TODO: MIGHT NEED TO EXCLUDE OTHER UNRELATED OBJECTS!
+      for (String excludedField : EXCLUDED_FIELDS_ITERATOR) {
+        if (eiAccessObj.getClassInfo().getName().startsWith(excludedField)) {
+          return;
+        }
+      }
+      // Extract fields from this object and put them into the read write
+      int numOfFields = eiAccessObj.getNumberOfFields();
+      for(int i=0; i<numOfFields; i++) {
+        FieldInfo fieldInfo = eiAccessObj.getFieldInfo(i);
+        if (fieldInfo.getType().equals(JAVA_STRING_LIB) || fieldInfo.getType().equals(JAVA_INTEGER)) {
+          String fieldClass = fieldInfo.getFullName();
+          ReadWriteSet rwSet = getReadWriteSet(currentChoice);
+          int objectId = fieldInfo.getClassInfo().getClassObjectRef();
+          // Record the field in the map
+          rwSet.addReadField(fieldClass, objectId);
+        }
+      }
+
+    }
+  }
+
   @Override
   public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
     if (stateReductionMode) {
@@ -788,6 +839,9 @@ public class StateReducer extends ListenerAdapter {
           if (!isFieldExcluded(fieldClass)) {
             analyzeReadWriteAccesses(executedInsn, fieldClass, currentChoice);
           }
+        } else if (executedInsn instanceof INVOKEINTERFACE) {
+          // Handle the read/write accesses that occur through iterators
+          analyzeReadWriteAccesses(executedInsn, ti, currentChoice);
         }
         // Analyze conflicts from next instructions
         if (nextInsn instanceof JVMFieldInstruction) {