X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=blobdiff_plain;f=src%2Fmain%2Fgov%2Fnasa%2Fjpf%2Flistener%2FDPORStateReducer.java;h=f6903824fc2a9ec388f538b71a44498aefe54420;hp=93fbca772c1ea9d0f0ec169e323885caf88d97dc;hb=899f4a49b5d96061d6cc942a7ce26e8ec8958fa2;hpb=37a78390e068b24e9e12b6292b4b8852955b0f0f diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java index 93fbca7..f690382 100644 --- 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 currVisitedStates; // States being visited in the current execution - private HashSet justVisitedStates; // States just visited in the previous choice/event - private HashSet prevVisitedStates; // States visited in the previous execution + private HashSet currVisitedStates; // States being visited in the current execution + private HashSet justVisitedStates; // States just visited in the previous choice/event + private HashSet prevVisitedStates; // States visited in the previous execution + private HashSet nonRelevantClasses;// Class info objects of non-relevant classes + private HashSet nonRelevantFields; // Field info objects of non-relevant fields + private HashSet relevantFields; // Field info objects of relevant fields private HashMap> stateToEventMap; // Data structure to analyze field Read/Write accesses and conflicts private HashMap> 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; }