Making field exclusion checks more efficient.

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index 93fbca772c1ea9d0f0ec169e323885caf88d97dc..f6903824fc2a9ec388f538b71a44498aefe54420 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@ -30,6 +30,7 @@ import gov.nasa.jpf.vm.choice.IntIntervalGenerator;
 
 import java.io.FileWriter;
 import java.io.PrintWriter;
+import java.lang.reflect.Field;
 import java.util.*;
 import java.util.logging.Logger;
 import java.io.IOException;
@@ -59,9 +60,12 @@ public class DPORStateReducer extends ListenerAdapter {
   private int choiceCounter;
   private int maxEventChoice;
   // Data structure to track the events seen by each state to track cycles (containing all events) for termination
-  private HashSet<Integer> currVisitedStates; // States being visited in the current execution
-  private HashSet<Integer> justVisitedStates; // States just visited in the previous choice/event
-  private HashSet<Integer> prevVisitedStates; // States visited in the previous execution
+  private HashSet<Integer> currVisitedStates;   // States being visited in the current execution
+  private HashSet<Integer> justVisitedStates;   // States just visited in the previous choice/event
+  private HashSet<Integer> prevVisitedStates;   // States visited in the previous execution
+  private HashSet<ClassInfo> nonRelevantClasses;// Class info objects of non-relevant classes
+  private HashSet<FieldInfo> nonRelevantFields; // Field info objects of non-relevant fields
+  private HashSet<FieldInfo> relevantFields;    // Field info objects of relevant fields
   private HashMap<Integer, HashSet<Integer>> stateToEventMap;
   // Data structure to analyze field Read/Write accesses and conflicts
   private HashMap<Integer, LinkedList<BacktrackExecution>> backtrackMap;  // Track created backtracking points
@@ -97,6 +101,9 @@ public class DPORStateReducer extends ListenerAdapter {
     isBooleanCGFlipped = false;
                numOfConflicts = 0;
                numOfTransitions = 0;
+               nonRelevantClasses = new HashSet<>();
+               nonRelevantFields = new HashSet<>();
+               relevantFields = new HashSet<>();
     restorableStateMap = new HashMap<>();
     initializeStatesVariables();
   }
@@ -268,11 +275,9 @@ public class DPORStateReducer extends ListenerAdapter {
           currentChoice = checkAndAdjustChoice(currentChoice, vm);
           // Record accesses from executed instructions
           if (executedInsn instanceof JVMFieldInstruction) {
-            // Analyze only after being initialized
-            String fieldClass = ((JVMFieldInstruction) executedInsn).getFieldInfo().getFullName();
             // We don't care about libraries
-            if (!isFieldExcluded(fieldClass)) {
-              analyzeReadWriteAccesses(executedInsn, fieldClass, currentChoice);
+            if (!isFieldExcluded(executedInsn)) {
+              analyzeReadWriteAccesses(executedInsn, currentChoice);
             }
           } else if (executedInsn instanceof INVOKEINTERFACE) {
             // Handle the read/write accesses that occur through iterators
@@ -775,17 +780,28 @@ public class DPORStateReducer extends ListenerAdapter {
   }
 
   // Analyze Read/Write accesses that are directly invoked on fields
-  private void analyzeReadWriteAccesses(Instruction executedInsn, String fieldClass, int currentChoice) {
+  private void analyzeReadWriteAccesses(Instruction executedInsn, int currentChoice) {
+    // Get the field info
+    FieldInfo fieldInfo = ((JVMFieldInstruction) executedInsn).getFieldInfo();
+    // Analyze only after being initialized
+    String fieldClass = fieldInfo.getFullName();
     // Do the analysis to get Read and Write accesses to fields
     ReadWriteSet rwSet = getReadWriteSet(currentChoice);
-    int objectId = ((JVMFieldInstruction) executedInsn).getFieldInfo().getClassInfo().getClassObjectRef();
+    int objectId = fieldInfo.getClassInfo().getClassObjectRef();
     // Record the field in the map
     if (executedInsn instanceof WriteInstruction) {
-      // Exclude certain field writes because of infrastructure needs, e.g., Event class field writes
-      for (String str : EXCLUDED_FIELDS_READ_WRITE_INSTRUCTIONS_STARTS_WITH_LIST) {
-        if (fieldClass.startsWith(str)) {
-          return;
+      // We first check the non-relevant fields set
+      if (!nonRelevantFields.contains(fieldInfo)) {
+        // Exclude certain field writes because of infrastructure needs, e.g., Event class field writes
+        for (String str : EXCLUDED_FIELDS_READ_WRITE_INSTRUCTIONS_STARTS_WITH_LIST) {
+          if (fieldClass.startsWith(str)) {
+            nonRelevantFields.add(fieldInfo);
+            return;
+          }
         }
+      } else {
+        // If we have this field in the non-relevant fields set then we return right away
+        return;
       }
       rwSet.addWriteField(fieldClass, objectId);
     } else if (executedInsn instanceof ReadInstruction) {
@@ -814,9 +830,17 @@ public class DPORStateReducer extends ListenerAdapter {
         return;
       }
       // We exclude library classes (they start with java, org, etc.) and some more
-      String objClassName = eiAccessObj.getClassInfo().getName();
-      if (excludeThisForItStartsWith(EXCLUDED_FIELDS_STARTS_WITH_LIST, objClassName) ||
-          excludeThisForItStartsWith(EXCLUDED_FIELDS_READ_WRITE_INSTRUCTIONS_STARTS_WITH_LIST, objClassName)) {
+      ClassInfo classInfo = eiAccessObj.getClassInfo();
+      String objClassName = classInfo.getName();
+      // Check if this class info is part of the non-relevant classes set already
+      if (!nonRelevantClasses.contains(classInfo)) {
+        if (excludeThisForItStartsWith(EXCLUDED_FIELDS_READ_WRITE_INSTRUCTIONS_STARTS_WITH_LIST, objClassName) ||
+                excludeThisForItStartsWith(EXCLUDED_FIELDS_STARTS_WITH_LIST, objClassName)) {
+          nonRelevantClasses.add(classInfo);
+          return;
+        }
+      } else {
+        // If it is part of the non-relevant classes set then return immediately
         return;
       }
       // Extract fields from this object and put them into the read write
@@ -985,14 +1009,27 @@ public class DPORStateReducer extends ListenerAdapter {
     return rwSet;
   }
 
-  private boolean isFieldExcluded(String field) {
+  private boolean isFieldExcluded(Instruction executedInsn) {
+    // Get the field info
+    FieldInfo fieldInfo = ((JVMFieldInstruction) executedInsn).getFieldInfo();
+    // Check if the non-relevant fields set already has it
+    if (nonRelevantFields.contains(fieldInfo)) {
+      return true;
+    }
+    // Check if the relevant fields set already has it
+    if (relevantFields.contains(fieldInfo)) {
+      return false;
+    }
+    // Analyze only after being initialized
+    String field = fieldInfo.getFullName();
     // Check against "starts-with", "ends-with", and "contains" list
     if (excludeThisForItStartsWith(EXCLUDED_FIELDS_STARTS_WITH_LIST, field) ||
             excludeThisForItEndsWith(EXCLUDED_FIELDS_ENDS_WITH_LIST, field) ||
             excludeThisForItContains(EXCLUDED_FIELDS_CONTAINS_LIST, field)) {
+      nonRelevantFields.add(fieldInfo);
       return true;
     }
-
+    relevantFields.add(fieldInfo);
     return false;
   }