e03135454330bf21df98cb80db167cfc819fd8de
[jpf-core.git] / src / main / gov / nasa / jpf / listener / StateReducer.java
1 /*
2  * Copyright (C) 2014, United States Government, as represented by the
3  * Administrator of the National Aeronautics and Space Administration.
4  * All rights reserved.
5  *
6  * The Java Pathfinder core (jpf-core) platform is licensed under the
7  * Apache License, Version 2.0 (the "License"); you may not use this file except
8  * in compliance with the License. You may obtain a copy of the License at
9  *
10  *        http://www.apache.org/licenses/LICENSE-2.0.
11  *
12  * Unless required by applicable law or agreed to in writing, software
13  * distributed under the License is distributed on an "AS IS" BASIS,
14  * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
15  * See the License for the specific language governing permissions and
16  * limitations under the License.
17  */
18 package gov.nasa.jpf.listener;
19
20 import gov.nasa.jpf.Config;
21 import gov.nasa.jpf.JPF;
22 import gov.nasa.jpf.ListenerAdapter;
23 import gov.nasa.jpf.search.Search;
24 import gov.nasa.jpf.jvm.bytecode.*;
25 import gov.nasa.jpf.vm.*;
26 import gov.nasa.jpf.vm.bytecode.ReadInstruction;
27 import gov.nasa.jpf.vm.bytecode.WriteInstruction;
28 import gov.nasa.jpf.vm.choice.IntChoiceFromSet;
29
30 import java.io.PrintWriter;
31
32 import java.util.*;
33
34 // TODO: Fix for Groovy's model-checking
35 // TODO: This is a setter to change the values of the ChoiceGenerator to implement POR
36 /**
37  * Simple tool to log state changes.
38  *
39  * This DPOR implementation is augmented by the algorithm presented in this SPIN paper:
40  * http://spinroot.com/spin/symposia/ws08/spin2008_submission_33.pdf
41  *
42  * The algorithm is presented on page 11 of the paper. Basically, we create a graph G
43  * (i.e., visible operation dependency graph)
44  * that maps inter-related threads/sub-programs that trigger state changes.
45  * The key to this approach is that we evaluate graph G in every iteration/recursion to
46  * only update the backtrack sets of the threads/sub-programs that are reachable in graph G
47  * from the currently running thread/sub-program.
48  */
49 public class StateReducer extends ListenerAdapter {
50
51   // Debug info fields
52   private boolean debugMode;
53   private boolean stateReductionMode;
54   private final PrintWriter out;
55   private String detail;
56   private int depth;
57   private int id;
58   private Transition transition;
59
60   // State reduction fields
61   private Integer[] choices;
62   private Integer[] refChoices;
63   private IntChoiceFromSet currCG;
64   private int choiceCounter;
65   private Integer choiceUpperBound;
66   private Integer maxUpperBound;
67   private boolean isInitialized;
68   private boolean isResetAfterAnalysis;
69   private boolean isBooleanCGFlipped;
70   private HashMap<IntChoiceFromSet, Integer> cgMap;
71   // Record the mapping between event number and field accesses (Read and Write)
72   private HashMap<Integer, ReadWriteSet> readWriteFieldsMap;
73   // The following is the backtrack map (set) that stores all the backtrack information
74   // e.g., event number 1 can have two backtrack sequences: {3,1,2,4,...} and {2,1,3,4,...}
75   private HashMap<Integer, LinkedList<Integer[]>> backtrackMap;
76   // Stores explored backtrack lists in the form of HashSet of Strings
77   private HashSet<String> backtrackSet;
78   private HashMap<Integer, HashSet<Integer>> conflictPairMap;
79
80   // Map that represents graph G
81   // (i.e., visible operation dependency graph (VOD Graph)
82   private HashMap<Integer, HashSet<Integer>> vodGraphMap;
83   // Set that represents hash table H
84   // (i.e., hash table that records encountered states)
85   // VOD graph is updated when the state has not yet been seen
86   // Current state
87   private HashSet<Integer> justVisitedStates;
88   // Previous choice number
89   private int prevChoiceValue;
90   // HashSet that stores references to unused CGs
91   private HashSet<IntChoiceFromSet> unusedCG;
92
93   //private HashMap<Integer, ConflictTracker.Node> stateGraph;
94   private HashMap<Integer, HashSet<Integer>> stateToEventMap;
95   // Map state to event
96   // Visited states in the previous and current executions/traces for terminating condition
97   private HashSet<Integer> prevVisitedStates;
98   private HashSet<Integer> currVisitedStates;
99
100   public StateReducer(Config config, JPF jpf) {
101     debugMode = config.getBoolean("debug_state_transition", false);
102     stateReductionMode = config.getBoolean("activate_state_reduction", true);
103     if (debugMode) {
104       out = new PrintWriter(System.out, true);
105     } else {
106       out = null;
107     }
108     detail = null;
109     depth = 0;
110     id = 0;
111     transition = null;
112     isBooleanCGFlipped = false;
113     vodGraphMap = new HashMap<>();
114     justVisitedStates = new HashSet<>();
115     prevChoiceValue = -1;
116     cgMap = new HashMap<>();
117     readWriteFieldsMap = new HashMap<>();
118     backtrackMap = new HashMap<>();
119     backtrackSet = new HashSet<>();
120     conflictPairMap = new HashMap<>();
121     unusedCG = new HashSet<>();
122     stateToEventMap = new HashMap<>();
123     prevVisitedStates = new HashSet<>();
124     currVisitedStates = new HashSet<>();
125     initializeStateReduction();
126   }
127
128   private void initializeStateReduction() {
129     if (stateReductionMode) {
130       choices = null;
131       refChoices = null;
132       currCG = null;
133       choiceCounter = 0;
134       choiceUpperBound = 0;
135       maxUpperBound = 0;
136       isInitialized = false;
137       isResetAfterAnalysis = false;
138       cgMap.clear();
139       resetReadWriteAnalysis();
140       backtrackMap.clear();
141       backtrackSet.clear();
142     }
143   }
144
145   @Override
146   public void stateRestored(Search search) {
147     if (debugMode) {
148       id = search.getStateId();
149       depth = search.getDepth();
150       transition = search.getTransition();
151       detail = null;
152       out.println("\n==> DEBUG: The state is restored to state with id: " + id + " -- Transition: " + transition +
153               " and depth: " + depth + "\n");
154     }
155   }
156
157   //--- the ones we are interested in
158   @Override
159   public void searchStarted(Search search) {
160     if (debugMode) {
161       out.println("\n==> DEBUG: ----------------------------------- search started" + "\n");
162     }
163   }
164
165   private void resetReadWriteAnalysis() {
166     // Reset the following data structure when the choice counter reaches 0 again
167     conflictPairMap.clear();
168     readWriteFieldsMap.clear();
169   }
170
171   private IntChoiceFromSet setNewCG(IntChoiceFromSet icsCG) {
172     icsCG.setNewValues(choices);
173     icsCG.reset();
174     // Use a modulo since choiceCounter is going to keep increasing
175     int choiceIndex = choiceCounter % choices.length;
176     icsCG.advance(choices[choiceIndex]);
177     if (choiceIndex == 0) {
178       resetReadWriteAnalysis();
179     }
180     return icsCG;
181   }
182
183   private Integer[] copyChoices(Integer[] choicesToCopy) {
184
185     Integer[] copyOfChoices = new Integer[choicesToCopy.length];
186     System.arraycopy(choicesToCopy, 0, copyOfChoices, 0, choicesToCopy.length);
187     return copyOfChoices;
188   }
189
190   private void continueExecutingThisTrace(IntChoiceFromSet icsCG) {
191     // We repeat the same trace if a state match is not found yet
192     IntChoiceFromSet setCG = setNewCG(icsCG);
193     unusedCG.add(setCG);
194   }
195
196   private void initializeChoiceGenerators(IntChoiceFromSet icsCG, Integer[] cgChoices) {
197     if (choiceCounter <= choiceUpperBound && !cgMap.containsValue(choiceCounter)) {
198       // Update the choices of the first CG and add '-1'
199       if (choices == null) {
200         // Initialize backtrack set that stores all the explored backtrack lists
201         maxUpperBound = cgChoices.length;
202         // All the choices are always the same so we only need to update it once
203         // Get the choice array and final choice in the array
204         choices = cgChoices;
205         // Make a copy of choices as reference
206         refChoices = copyChoices(choices);
207         String firstChoiceListString = buildStringFromChoiceList(choices);
208         backtrackSet.add(firstChoiceListString);
209       }
210       IntChoiceFromSet setCG = setNewCG(icsCG);
211       cgMap.put(setCG, refChoices[choiceCounter]);
212     } else {
213       continueExecutingThisTrace(icsCG);
214     }
215   }
216
217   private void manageChoiceGeneratorsInSubsequentTraces(IntChoiceFromSet icsCG) {
218     // If this is the first iteration of the trace then set other CGs done
219     if (choiceCounter <= choiceUpperBound) {
220       icsCG.setDone();
221     } else {
222       // If this is the subsequent iterations of the trace then set up new CGs to continue the execution
223       continueExecutingThisTrace(icsCG);
224     }
225   }
226
227   @Override
228   public void choiceGeneratorRegistered(VM vm, ChoiceGenerator<?> nextCG, ThreadInfo currentThread, Instruction executedInstruction) {
229     if (stateReductionMode) {
230       // Initialize with necessary information from the CG
231       if (nextCG instanceof IntChoiceFromSet) {
232         IntChoiceFromSet icsCG = (IntChoiceFromSet) nextCG;
233         // Check if CG has been initialized, otherwise initialize it
234         Integer[] cgChoices = icsCG.getAllChoices();
235         if (!isInitialized) {
236           // Get the upper bound from the last element of the choices
237           choiceUpperBound = cgChoices[cgChoices.length - 1];
238           isInitialized = true;
239         }
240         // Record the subsequent Integer CGs only until we hit the upper bound
241         if (!isResetAfterAnalysis) {
242           initializeChoiceGenerators(icsCG, cgChoices);
243         } else {
244           // Set new CGs to done so that the search algorithm explores the existing CGs
245           //icsCG.setDone();
246           manageChoiceGeneratorsInSubsequentTraces(icsCG);
247         }
248         choiceCounter++;
249       }
250     }
251   }
252
253   private void setDoneUnusedCG() {
254     // Set done every CG in the unused CG set
255     for (IntChoiceFromSet cg : unusedCG) {
256       cg.setDone();
257     }
258     unusedCG.clear();
259   }
260
261   private void resetAllCGs() {
262     // Extract the event numbers that have backtrack lists
263     Set<Integer> eventSet = backtrackMap.keySet();
264     // Return if there is no conflict at all (highly unlikely)
265     if (eventSet.isEmpty()) {
266       // Set every CG to done!
267       for (IntChoiceFromSet cg : cgMap.keySet()) {
268         cg.setDone();
269       }
270       return;
271     }
272     // Reset every CG with the first backtrack lists
273     for (IntChoiceFromSet cg : cgMap.keySet()) {
274       int event = cgMap.get(cg);
275       LinkedList<Integer[]> choiceLists = backtrackMap.get(event);
276       if (choiceLists != null && choiceLists.peekFirst() != null) {
277         Integer[] choiceList = choiceLists.removeFirst();
278         // Deploy the new choice list for this CG
279         cg.setNewValues(choiceList);
280         cg.reset();
281       } else {
282         cg.setDone();
283       }
284     }
285     setDoneUnusedCG();
286     saveVisitedStates();
287   }
288
289   // Detect cycles in the current execution/trace
290   // We terminate the execution iff:
291   // (1) the state has been visited in the current execution
292   // (2) the state has one or more cycles that involve all the events
293   // With simple approach we only need to check for a re-visited state.
294   // Basically, we have to check that we have executed all events between two occurrences of such state.
295   private boolean containsCyclesWithAllEvents(int stId) {
296
297     HashSet<Integer> visitedEvents = stateToEventMap.get(stId);
298     boolean containsCyclesWithAllEvts = false;
299     if (checkIfAllEventsInvolved(visitedEvents)) {
300       containsCyclesWithAllEvts = true;
301     }
302
303     return containsCyclesWithAllEvts;
304   }
305
306   private boolean checkIfAllEventsInvolved(HashSet<Integer> visitedEvents) {
307
308     // Check if this set contains all the event choices
309     // If not then this is not the terminating condition
310     for(int i=0; i<=choiceUpperBound; i++) {
311       if (!visitedEvents.contains(i)) {
312         return false;
313       }
314     }
315     return true;
316   }
317
318   private void saveVisitedStates() {
319     // CG is being reset
320     // Save all the visited states
321     prevVisitedStates.addAll(currVisitedStates);
322     currVisitedStates.clear();
323   }
324
325   private void updateChoicesForNewExecution(IntChoiceFromSet icsCG) {
326     if (choices == null || choices != icsCG.getAllChoices()) {
327       currCG = icsCG;
328       choices = icsCG.getAllChoices();
329       refChoices = copyChoices(choices);
330       // Reset a few things for the sub-graph
331       resetReadWriteAnalysis();
332       choiceCounter = 0;
333     }
334   }
335
336   private void exploreNextBacktrackSets(IntChoiceFromSet icsCG) {
337     // Traverse the sub-graphs
338     if (isResetAfterAnalysis) {
339       // Do this for every CG after finishing each backtrack list
340       // We try to update the CG with a backtrack list if the state has been visited multiple times
341       //if ((icsCG.getNextChoice() == -1 || choiceCounter > 1) && cgMap.containsKey(icsCG)) {
342       //if ((!icsCG.hasMoreChoices() || choiceCounter > 1) && cgMap.containsKey(icsCG)) {
343       if (choiceCounter > 1 && cgMap.containsKey(icsCG)) {
344         int event = cgMap.get(icsCG);
345         LinkedList<Integer[]> choiceLists = backtrackMap.get(event);
346         if (choiceLists != null && choiceLists.peekFirst() != null) {
347           Integer[] choiceList = choiceLists.removeFirst();
348           // Deploy the new choice list for this CG
349           icsCG.setNewValues(choiceList);
350           icsCG.reset();
351         } else {
352           // Set done if this was the last backtrack list
353           icsCG.setDone();
354         }
355         setDoneUnusedCG();
356         saveVisitedStates();
357       }
358     } else {
359       // Update and reset the CG if needed (do this for the first time after the analysis)
360       // Start backtracking if this is a visited state and it is not a repeating state
361       resetAllCGs();
362       isResetAfterAnalysis = true;
363     }
364   }
365
366   private void checkAndEnforceFairScheduling(IntChoiceFromSet icsCG) {
367     // Check the next choice and if the value is not the same as the expected then force the expected value
368     int choiceIndex = (choiceCounter - 1) % refChoices.length;
369     if (choices[choiceIndex] != icsCG.getNextChoiceIndex()) {
370       int expectedChoice = refChoices[choiceIndex];
371       int currCGIndex = icsCG.getNextChoiceIndex();
372       if ((currCGIndex >= 0) && (currCGIndex < refChoices.length)) {
373         icsCG.setChoice(currCGIndex, expectedChoice);
374       }
375     }
376   }
377
378   private boolean terminateCurrentExecution() {
379     // We need to check all the states that have just been visited
380     // Often a transition (choice/event) can result into forwarding/backtracking to a number of states
381     for(Integer stateId : justVisitedStates) {
382       if (prevVisitedStates.contains(stateId) || containsCyclesWithAllEvents(stateId)) {
383         return true;
384       }
385     }
386     return false;
387   }
388
389   @Override
390   public void choiceGeneratorAdvanced(VM vm, ChoiceGenerator<?> currentCG) {
391
392     if (stateReductionMode) {
393       // Check the boolean CG and if it is flipped, we are resetting the analysis
394       if (currentCG instanceof BooleanChoiceGenerator) {
395         if (!isBooleanCGFlipped) {
396           isBooleanCGFlipped = true;
397         } else {
398           initializeStateReduction();
399         }
400       }
401       // Check every choice generated and make sure that all the available choices
402       // are chosen first before repeating the same choice of value twice!
403       if (currentCG instanceof IntChoiceFromSet) {
404         IntChoiceFromSet icsCG = (IntChoiceFromSet) currentCG;
405         // Update the current pointer to the current set of choices
406         updateChoicesForNewExecution(icsCG);
407         // Check if we have seen this state or this state contains cycles that involve all events
408         if (terminateCurrentExecution()) {
409           exploreNextBacktrackSets(icsCG);
410         }
411         justVisitedStates.clear();
412         // If we don't see a fair scheduling of events/choices then we have to enforce it
413         checkAndEnforceFairScheduling(icsCG);
414         // Update the VOD graph always with the latest
415         updateVODGraph(icsCG.getNextChoice());
416       }
417     }
418   }
419
420   private void updateVODGraph(int currChoiceValue) {
421     // Update the graph when we have the current choice value
422     HashSet<Integer> choiceSet;
423     if (vodGraphMap.containsKey(prevChoiceValue)) {
424       // If the key already exists, just retrieve it
425       choiceSet = vodGraphMap.get(prevChoiceValue);
426     } else {
427       // Create a new entry
428       choiceSet = new HashSet<>();
429       vodGraphMap.put(prevChoiceValue, choiceSet);
430     }
431     choiceSet.add(currChoiceValue);
432     prevChoiceValue = currChoiceValue;
433   }
434
435   private void mapStateToEvent(Search search, int stateId) {
436     // Insert state ID and event choice into the map
437     HashSet<Integer> eventSet;
438     if (stateToEventMap.containsKey(stateId)) {
439       eventSet = stateToEventMap.get(stateId);
440     } else {
441       eventSet = new HashSet<>();
442       stateToEventMap.put(stateId, eventSet);
443     }
444     eventSet.add(prevChoiceValue);
445   }
446
447   private void updateStateInfo(Search search) {
448     if (stateReductionMode) {
449       // Update the state variables
450       // Line 19 in the paper page 11 (see the heading note above)
451       int stateId = search.getStateId();
452       currVisitedStates.add(stateId);
453       mapStateToEvent(search, stateId);
454       justVisitedStates.add(stateId);
455     }
456   }
457
458   @Override
459   public void stateAdvanced(Search search) {
460     if (debugMode) {
461       id = search.getStateId();
462       depth = search.getDepth();
463       transition = search.getTransition();
464       if (search.isNewState()) {
465         detail = "new";
466       } else {
467         detail = "visited";
468       }
469
470       if (search.isEndState()) {
471         out.println("\n==> DEBUG: This is the last state!\n");
472         detail += " end";
473       }
474       out.println("\n==> DEBUG: The state is forwarded to state with id: " + id + " with depth: " + depth +
475               " which is " + detail + " Transition: " + transition + "\n");
476     }
477     updateStateInfo(search);
478   }
479
480   @Override
481   public void stateBacktracked(Search search) {
482     if (debugMode) {
483       id = search.getStateId();
484       depth = search.getDepth();
485       transition = search.getTransition();
486       detail = null;
487
488       out.println("\n==> DEBUG: The state is backtracked to state with id: " + id + " -- Transition: " + transition +
489               " and depth: " + depth + "\n");
490     }
491     updateStateInfo(search);
492   }
493
494   @Override
495   public void searchFinished(Search search) {
496     if (debugMode) {
497       out.println("\n==> DEBUG: ----------------------------------- search finished" + "\n");
498     }
499   }
500
501   // This class compactly stores Read and Write field sets
502   // We store the field name and its object ID
503   // Sharing the same field means the same field name and object ID
504   private class ReadWriteSet {
505     private HashMap<String, Integer> readSet;
506     private HashMap<String, Integer> writeSet;
507
508     public ReadWriteSet() {
509       readSet = new HashMap<>();
510       writeSet = new HashMap<>();
511     }
512
513     public void addReadField(String field, int objectId) {
514       readSet.put(field, objectId);
515     }
516
517     public void addWriteField(String field, int objectId) {
518       writeSet.put(field, objectId);
519     }
520
521     public boolean readFieldExists(String field) {
522       return readSet.containsKey(field);
523     }
524
525     public boolean writeFieldExists(String field) {
526       return writeSet.containsKey(field);
527     }
528
529     public int readFieldObjectId(String field) {
530       return readSet.get(field);
531     }
532
533     public int writeFieldObjectId(String field) {
534       return writeSet.get(field);
535     }
536   }
537
538   private void analyzeReadWriteAccesses(Instruction executedInsn, String fieldClass, int currentChoice) {
539     // Do the analysis to get Read and Write accesses to fields
540     ReadWriteSet rwSet;
541     // We already have an entry
542     if (readWriteFieldsMap.containsKey(refChoices[currentChoice])) {
543       rwSet = readWriteFieldsMap.get(refChoices[currentChoice]);
544     } else { // We need to create a new entry
545       rwSet = new ReadWriteSet();
546       readWriteFieldsMap.put(refChoices[currentChoice], rwSet);
547     }
548     int objectId = ((JVMFieldInstruction) executedInsn).getFieldInfo().getClassInfo().getClassObjectRef();
549     // Record the field in the map
550     if (executedInsn instanceof WriteInstruction) {
551       // Exclude certain field writes because of infrastructure needs, e.g., Event class field writes
552       for (String str : EXCLUDED_FIELDS_WRITE_INSTRUCTIONS_STARTS_WITH_LIST) {
553         if (fieldClass.startsWith(str)) {
554           return;
555         }
556       }
557       rwSet.addWriteField(fieldClass, objectId);
558     } else if (executedInsn instanceof ReadInstruction) {
559       rwSet.addReadField(fieldClass, objectId);
560     }
561   }
562
563   private boolean recordConflictPair(int currentEvent, int eventNumber) {
564     HashSet<Integer> conflictSet;
565     if (!conflictPairMap.containsKey(currentEvent)) {
566       conflictSet = new HashSet<>();
567       conflictPairMap.put(currentEvent, conflictSet);
568     } else {
569       conflictSet = conflictPairMap.get(currentEvent);
570     }
571     // If this conflict has been recorded before, we return false because
572     // we don't want to service this backtrack point twice
573     if (conflictSet.contains(eventNumber)) {
574       return false;
575     }
576     // If it hasn't been recorded, then do otherwise
577     conflictSet.add(eventNumber);
578     return true;
579   }
580
581   private String buildStringFromChoiceList(Integer[] newChoiceList) {
582
583     // When we see a choice list shorter than the upper bound, e.g., [3,2] for choices 0,1,2, and 3,
584     //  then we have to pad the beginning before we store it, because [3,2] actually means [0,1,3,2]
585     // First, calculate the difference between this choice list and the upper bound
586     //  The actual list doesn't include '-1' at the end
587     int actualListLength = newChoiceList.length - 1;
588     int diff = maxUpperBound - actualListLength;
589     StringBuilder sb = new StringBuilder();
590     // Pad the beginning if necessary
591     for (int i = 0; i < diff; i++) {
592       sb.append(i);
593     }
594     // Then continue with the actual choice list
595     // We don't include the '-1' at the end
596     for (int i = 0; i < newChoiceList.length - 1; i++) {
597       sb.append(newChoiceList[i]);
598     }
599     return sb.toString();
600   }
601
602   private void checkAndAddBacktrackList(LinkedList<Integer[]> backtrackChoiceLists, Integer[] newChoiceList) {
603
604     String newChoiceListString = buildStringFromChoiceList(newChoiceList);
605     // Add only if we haven't seen this combination before
606     if (!backtrackSet.contains(newChoiceListString)) {
607       backtrackSet.add(newChoiceListString);
608       backtrackChoiceLists.addLast(newChoiceList);
609     }
610   }
611
612   private void createBacktrackChoiceList(int currentChoice, int conflictEventNumber) {
613
614     LinkedList<Integer[]> backtrackChoiceLists;
615     // Create a new list of choices for backtrack based on the current choice and conflicting event number
616     // If we have a conflict between 1 and 3, then we create the list {3, 1, 2, 4, 5} for backtrack
617     // The backtrack point is the CG for event number 1 and the list length is one less than the original list
618     // (originally of length 6) since we don't start from event number 0
619     if (!isResetAfterAnalysis) {
620       // Check if we have a list for this choice number
621       // If not we create a new one for it
622       if (!backtrackMap.containsKey(conflictEventNumber)) {
623         backtrackChoiceLists = new LinkedList<>();
624         backtrackMap.put(conflictEventNumber, backtrackChoiceLists);
625       } else {
626         backtrackChoiceLists = backtrackMap.get(conflictEventNumber);
627       }
628       int maxListLength = choiceUpperBound + 1;
629       int listLength = maxListLength - conflictEventNumber;
630       Integer[] newChoiceList = new Integer[listLength];
631       // Put the conflicting event numbers first and reverse the order
632       newChoiceList[0] = refChoices[currentChoice];
633       newChoiceList[1] = refChoices[conflictEventNumber];
634       // Put the rest of the event numbers into the array starting from the minimum to the upper bound
635       for (int i = conflictEventNumber + 1, j = 2; j < listLength; i++) {
636         if (refChoices[i] != refChoices[currentChoice]) {
637           newChoiceList[j] = refChoices[i];
638           j++;
639         }
640       }
641       checkAndAddBacktrackList(backtrackChoiceLists, newChoiceList);
642       // The start index for the recursion is always 1 (from the main branch)
643     } else { // This is a sub-graph
644       // There is a case/bug that after a re-initialization, currCG is not yet initialized
645       if (currCG != null && cgMap.containsKey(currCG)) {
646         int backtrackListIndex = cgMap.get(currCG);
647         backtrackChoiceLists = backtrackMap.get(backtrackListIndex);
648         int listLength = refChoices.length;
649         Integer[] newChoiceList = new Integer[listLength];
650         // Copy everything before the conflict number
651         for (int i = 0; i < conflictEventNumber; i++) {
652           newChoiceList[i] = refChoices[i];
653         }
654         // Put the conflicting events
655         newChoiceList[conflictEventNumber] = refChoices[currentChoice];
656         newChoiceList[conflictEventNumber + 1] = refChoices[conflictEventNumber];
657         // Copy the rest
658         for (int i = conflictEventNumber + 1, j = conflictEventNumber + 2; j < listLength - 1; i++) {
659           if (refChoices[i] != refChoices[currentChoice]) {
660             newChoiceList[j] = refChoices[i];
661             j++;
662           }
663         }
664         checkAndAddBacktrackList(backtrackChoiceLists, newChoiceList);
665       }
666     }
667   }
668
669   // We exclude fields that come from libraries (Java and Groovy), and also the infrastructure
670   private final static String[] EXCLUDED_FIELDS_STARTS_WITH_LIST =
671           // Java and Groovy libraries
672           { "java", "org", "sun", "com", "gov", "groovy"};
673   private final static String[] EXCLUDED_FIELDS_ENDS_WITH_LIST =
674           // Groovy library created fields
675           {"stMC", "callSiteArray", "metaClass", "staticClassInfo", "__constructor__",
676                   // Infrastructure
677                   "sendEvent", "Object", "reference", "location", "app", "state", "log", "functionList", "objectList",
678                   "eventList", "valueList", "settings", "printToConsole", "app1", "app2"};
679   private final static String[] EXCLUDED_FIELDS_CONTAINS_LIST = {"_closure"};
680   private final static String[] EXCLUDED_FIELDS_WRITE_INSTRUCTIONS_STARTS_WITH_LIST = {"Event"};
681
682   private boolean isFieldExcluded(String field) {
683     // Check against "starts-with" list
684     for(String str : EXCLUDED_FIELDS_STARTS_WITH_LIST) {
685       if (field.startsWith(str)) {
686         return true;
687       }
688     }
689     // Check against "ends-with" list
690     for(String str : EXCLUDED_FIELDS_ENDS_WITH_LIST) {
691       if (field.endsWith(str)) {
692         return true;
693       }
694     }
695     // Check against "contains" list
696     for(String str : EXCLUDED_FIELDS_CONTAINS_LIST) {
697       if (field.contains(str)) {
698         return true;
699       }
700     }
701
702     return false;
703   }
704
705   // This method checks whether a choice is reachable in the VOD graph from a reference choice
706   // This is a BFS search
707   private boolean isReachableInVODGraph(int checkedChoice, int referenceChoice) {
708     // Record visited choices as we search in the graph
709     HashSet<Integer> visitedChoice = new HashSet<>();
710     visitedChoice.add(referenceChoice);
711     LinkedList<Integer> nodesToVisit = new LinkedList<>();
712     // If the state doesn't advance as the threads/sub-programs are executed (basically there is no new state),
713     // there is a chance that the graph doesn't have new nodes---thus this check will return a null.
714     if (vodGraphMap.containsKey(referenceChoice)) {
715       nodesToVisit.addAll(vodGraphMap.get(referenceChoice));
716       while(!nodesToVisit.isEmpty()) {
717         int currChoice = nodesToVisit.getFirst();
718         if (currChoice == checkedChoice) {
719           return true;
720         }
721         if (visitedChoice.contains(currChoice)) {
722           // If there is a loop then we don't find it
723           return false;
724         }
725         // Continue searching
726         visitedChoice.add(currChoice);
727         HashSet<Integer> currChoiceNextNodes = vodGraphMap.get(currChoice);
728         if (currChoiceNextNodes != null) {
729           // Add only if there is a mapping for next nodes
730           for (Integer nextNode : currChoiceNextNodes) {
731             // Skip cycles
732             if (nextNode == currChoice) {
733               continue;
734             }
735             nodesToVisit.addLast(nextNode);
736           }
737         }
738       }
739     }
740     return false;
741   }
742
743   @Override
744   public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
745     if (stateReductionMode) {
746       if (isInitialized) {
747         int currentChoice = (choiceCounter % refChoices.length) - 1;
748         if (currentChoice < 0) {
749           // We do not compute the conflicts for the choice '-1'
750           return;
751         }
752         // Record accesses from executed instructions
753         if (executedInsn instanceof JVMFieldInstruction) {
754           // Analyze only after being initialized
755           String fieldClass = ((JVMFieldInstruction) executedInsn).getFieldInfo().getFullName();
756           // We don't care about libraries
757           if (!isFieldExcluded(fieldClass)) {
758             analyzeReadWriteAccesses(executedInsn, fieldClass, currentChoice);
759           }
760         }
761         // Analyze conflicts from next instructions
762         if (nextInsn instanceof JVMFieldInstruction) {
763           // The constructor is only called once when the object is initialized
764           // It does not have shared access with other objects
765           MethodInfo mi = nextInsn.getMethodInfo();
766           if (!mi.getName().equals("<init>")) {
767             String fieldClass = ((JVMFieldInstruction) nextInsn).getFieldInfo().getFullName();
768             // We don't care about libraries
769             if (!isFieldExcluded(fieldClass)) {
770               // Check for conflict (go backward from currentChoice and get the first conflict)
771               // If the current event has conflicts with multiple events, then these will be detected
772               // one by one as this recursively checks backward when backtrack set is revisited and executed.
773               for (int eventNumber = currentChoice - 1; eventNumber >= 0; eventNumber--) {
774                 // Skip if this event number does not have any Read/Write set
775                 if (!readWriteFieldsMap.containsKey(refChoices[eventNumber])) {
776                   continue;
777                 }
778                 ReadWriteSet rwSet = readWriteFieldsMap.get(refChoices[eventNumber]);
779                 int currObjId = ((JVMFieldInstruction) nextInsn).getFieldInfo().getClassInfo().getClassObjectRef();
780                 // 1) Check for conflicts with Write fields for both Read and Write instructions
781                 if (((nextInsn instanceof WriteInstruction || nextInsn instanceof ReadInstruction) &&
782                         rwSet.writeFieldExists(fieldClass) && rwSet.writeFieldObjectId(fieldClass) == currObjId) ||
783                         (nextInsn instanceof WriteInstruction && rwSet.readFieldExists(fieldClass) &&
784                                 rwSet.readFieldObjectId(fieldClass) == currObjId)) {
785                   // We do not record and service the same backtrack pair/point twice!
786                   // If it has been serviced before, we just skip this
787                   if (recordConflictPair(currentChoice, eventNumber)) {
788                     // Lines 4-8 of the algorithm in the paper page 11 (see the heading note above)
789                     if (vm.isNewState() || isReachableInVODGraph(refChoices[currentChoice], refChoices[currentChoice-1])) {
790                       createBacktrackChoiceList(currentChoice, eventNumber);
791                       // Break if a conflict is found!
792                       break;
793                     }
794                   }
795                 }
796               }
797             }
798           }
799         }
800       }
801     }
802   }
803 }