Explored trace needs to be constructed and modified as there are predecessor branches.
[jpf-core.git] / src / main / gov / nasa / jpf / listener / DPORStateReducer.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 import gov.nasa.jpf.vm.choice.IntIntervalGenerator;
30
31 import java.io.FileWriter;
32 import java.io.PrintWriter;
33 import java.lang.reflect.Field;
34 import java.util.*;
35 import java.util.logging.Logger;
36 import java.io.IOException;
37
38 /**
39  * This a DPOR implementation for event-driven applications with loops that create cycles of state matching
40  * In this new DPOR algorithm/implementation, each run is terminated iff:
41  * - we find a state that matches a state in a previous run, or
42  * - we have a matched state in the current run that consists of cycles that contain all choices/events.
43  */
44 public class DPORStateReducer extends ListenerAdapter {
45
46   // Information printout fields for verbose mode
47   private boolean verboseMode;
48   private boolean stateReductionMode;
49   private final PrintWriter out;
50   private PrintWriter fileWriter;
51   private String detail;
52   private int depth;
53   private int id;
54   private Transition transition;
55
56   // DPOR-related fields
57   // Basic information
58   private Integer[] choices;
59   private Integer[] refChoices; // Second reference to a copy of choices (choices may be modified for fair scheduling)
60   private int choiceCounter;
61   private int maxEventChoice;
62   // Data structure to track the events seen by each state to track cycles (containing all events) for termination
63   private HashSet<Integer> currVisitedStates;   // States being visited in the current execution
64   private HashSet<Integer> justVisitedStates;   // States just visited in the previous choice/event
65   private HashSet<Integer> prevVisitedStates;   // States visited in the previous execution
66   private HashSet<ClassInfo> nonRelevantClasses;// Class info objects of non-relevant classes
67   private HashSet<FieldInfo> nonRelevantFields; // Field info objects of non-relevant fields
68   private HashSet<FieldInfo> relevantFields;    // Field info objects of relevant fields
69   private HashMap<Integer, HashSet<Integer>> stateToEventMap;
70   // Data structure to analyze field Read/Write accesses and conflicts
71   private HashMap<Integer, LinkedList<BacktrackExecution>> backtrackMap;  // Track created backtracking points
72   private PriorityQueue<Integer> backtrackStateQ;                 // Heap that returns the latest state
73   private Execution currentExecution;                             // Holds the information about the current execution
74   private HashSet<String> doneBacktrackSet;                       // Record state ID and trace already constructed
75   private HashMap<Integer, RestorableVMState> restorableStateMap; // Maps state IDs to the restorable state object
76   private RGraph rGraph;                                          // R-Graph for past executions
77
78   // Boolean states
79   private boolean isBooleanCGFlipped;
80   private boolean isEndOfExecution;
81
82   // Statistics
83   private int numOfConflicts;
84   private int numOfTransitions;
85         
86   public DPORStateReducer(Config config, JPF jpf) {
87     verboseMode = config.getBoolean("printout_state_transition", false);
88     stateReductionMode = config.getBoolean("activate_state_reduction", true);
89     if (verboseMode) {
90       out = new PrintWriter(System.out, true);
91     } else {
92       out = null;
93     }
94     String outputFile = config.getString("file_output");
95     if (!outputFile.isEmpty()) {
96       try {
97         fileWriter = new PrintWriter(new FileWriter(outputFile, true), true);
98       } catch (IOException e) {
99       }
100     }
101     isBooleanCGFlipped = false;
102                 numOfConflicts = 0;
103                 numOfTransitions = 0;
104                 nonRelevantClasses = new HashSet<>();
105                 nonRelevantFields = new HashSet<>();
106                 relevantFields = new HashSet<>();
107     restorableStateMap = new HashMap<>();
108     initializeStatesVariables();
109   }
110
111   @Override
112   public void stateRestored(Search search) {
113     if (verboseMode) {
114       id = search.getStateId();
115       depth = search.getDepth();
116       transition = search.getTransition();
117       detail = null;
118       out.println("\n==> DEBUG: The state is restored to state with id: " + id + " -- Transition: " + transition +
119               " and depth: " + depth + "\n");
120     }
121   }
122
123   @Override
124   public void searchStarted(Search search) {
125     if (verboseMode) {
126       out.println("\n==> DEBUG: ----------------------------------- search started" + "\n");
127     }
128   }
129
130   @Override
131   public void stateAdvanced(Search search) {
132     if (verboseMode) {
133       id = search.getStateId();
134       depth = search.getDepth();
135       transition = search.getTransition();
136       if (search.isNewState()) {
137         detail = "new";
138       } else {
139         detail = "visited";
140       }
141
142       if (search.isEndState()) {
143         out.println("\n==> DEBUG: This is the last state!\n");
144         detail += " end";
145       }
146       out.println("\n==> DEBUG: The state is forwarded to state with id: " + id + " with depth: " + depth +
147               " which is " + detail + " Transition: " + transition + "\n");
148     }
149     if (stateReductionMode) {
150       updateStateInfo(search);
151     }
152   }
153
154   @Override
155   public void stateBacktracked(Search search) {
156     if (verboseMode) {
157       id = search.getStateId();
158       depth = search.getDepth();
159       transition = search.getTransition();
160       detail = null;
161
162       out.println("\n==> DEBUG: The state is backtracked to state with id: " + id + " -- Transition: " + transition +
163               " and depth: " + depth + "\n");
164     }
165     if (stateReductionMode) {
166       updateStateInfo(search);
167     }
168   }
169
170   static Logger log = JPF.getLogger("report");
171
172   @Override
173   public void searchFinished(Search search) {
174     if (stateReductionMode) {
175       // Number of conflicts = first trace + subsequent backtrack points
176       numOfConflicts += 1 + doneBacktrackSet.size();
177     }
178     if (verboseMode) {
179       out.println("\n==> DEBUG: ----------------------------------- search finished");
180       out.println("\n==> DEBUG: State reduction mode  : " + stateReductionMode);
181       out.println("\n==> DEBUG: Number of conflicts   : " + numOfConflicts);
182       out.println("\n==> DEBUG: Number of transitions : " + numOfTransitions);
183       out.println("\n==> DEBUG: ----------------------------------- search finished" + "\n");
184
185       fileWriter.println("==> DEBUG: State reduction mode  : " + stateReductionMode);
186       fileWriter.println("==> DEBUG: Number of conflicts   : " + numOfConflicts);
187       fileWriter.println("==> DEBUG: Number of transitions : " + numOfTransitions);
188       fileWriter.println();
189       fileWriter.close();
190     }
191   }
192
193   @Override
194   public void choiceGeneratorRegistered(VM vm, ChoiceGenerator<?> nextCG, ThreadInfo currentThread, Instruction executedInstruction) {
195     if (stateReductionMode) {
196       // Initialize with necessary information from the CG
197       if (nextCG instanceof IntChoiceFromSet) {
198         IntChoiceFromSet icsCG = (IntChoiceFromSet) nextCG;
199         if (!isEndOfExecution) {
200           // Check if CG has been initialized, otherwise initialize it
201           Integer[] cgChoices = icsCG.getAllChoices();
202           // Record the events (from choices)
203           if (choices == null) {
204             choices = cgChoices;
205             // Make a copy of choices as reference
206             refChoices = copyChoices(choices);
207             // Record the max event choice (the last element of the choice array)
208             maxEventChoice = choices[choices.length - 1];
209           }
210           icsCG.setNewValues(choices);
211           icsCG.reset();
212           // Use a modulo since choiceCounter is going to keep increasing
213           int choiceIndex = choiceCounter % choices.length;
214           icsCG.advance(choices[choiceIndex]);
215         } else {
216           // Set done all CGs while transitioning to a new execution
217           icsCG.setDone();
218         }
219       }
220     }
221   }
222
223   @Override
224   public void choiceGeneratorAdvanced(VM vm, ChoiceGenerator<?> currentCG) {
225     if (stateReductionMode) {
226       // Check the boolean CG and if it is flipped, we are resetting the analysis
227       if (currentCG instanceof BooleanChoiceGenerator) {
228         if (!isBooleanCGFlipped) {
229           isBooleanCGFlipped = true;
230         } else {
231           // Number of conflicts = first trace + subsequent backtrack points
232           numOfConflicts = 1 + doneBacktrackSet.size();
233           // Allocate new objects for data structure when the boolean is flipped from "false" to "true"
234           initializeStatesVariables();
235         }
236       }
237       // Check every choice generated and ensure fair scheduling!
238       if (currentCG instanceof IntChoiceFromSet) {
239         IntChoiceFromSet icsCG = (IntChoiceFromSet) currentCG;
240         // If this is a new CG then we need to update data structures
241         resetStatesForNewExecution(icsCG, vm);
242         // If we don't see a fair scheduling of events/choices then we have to enforce it
243         ensureFairSchedulingAndSetupTransition(icsCG, vm);
244         // Update backtrack set of an executed event (transition): one transition before this one
245         updateBacktrackSet(currentExecution, choiceCounter - 1);
246         // Explore the next backtrack point:
247         // 1) if we have seen this state or this state contains cycles that involve all events, and
248         // 2) after the current CG is advanced at least once
249         if (terminateCurrentExecution() && choiceCounter > 0) {
250           exploreNextBacktrackPoints(vm, icsCG);
251         } else {
252           numOfTransitions++;
253         }
254         // Map state to event
255         mapStateToEvent(icsCG.getNextChoice());
256         justVisitedStates.clear();
257         choiceCounter++;
258       }
259     } else {
260       numOfTransitions++;
261     }
262   }
263
264   @Override
265   public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
266     if (stateReductionMode) {
267       if (!isEndOfExecution) {
268         // Has to be initialized and a integer CG
269         ChoiceGenerator<?> cg = vm.getChoiceGenerator();
270         if (cg instanceof IntChoiceFromSet || cg instanceof IntIntervalGenerator) {
271           int currentChoice = choiceCounter - 1;  // Accumulative choice w.r.t the current trace
272           if (currentChoice < 0) { // If choice is -1 then skip
273             return;
274           }
275           currentChoice = checkAndAdjustChoice(currentChoice, vm);
276           // Record accesses from executed instructions
277           if (executedInsn instanceof JVMFieldInstruction) {
278             // We don't care about libraries
279             if (!isFieldExcluded(executedInsn)) {
280               analyzeReadWriteAccesses(executedInsn, currentChoice);
281             }
282           } else if (executedInsn instanceof INVOKEINTERFACE) {
283             // Handle the read/write accesses that occur through iterators
284             analyzeReadWriteAccesses(executedInsn, ti, currentChoice);
285           }
286         }
287       }
288     }
289   }
290
291
292   // == HELPERS
293
294   // -- INNER CLASSES
295
296   // This class compactly stores backtrack execution:
297   // 1) backtrack choice list, and
298   // 2) first backtrack point (linking with predecessor execution)
299   private class BacktrackExecution {
300     private Integer[] choiceList;
301     private TransitionEvent firstTransition;
302
303     public BacktrackExecution(Integer[] choList, TransitionEvent fTransition) {
304       choiceList = choList;
305       firstTransition = fTransition;
306     }
307
308     public Integer[] getChoiceList() {
309       return choiceList;
310     }
311
312     public TransitionEvent getFirstTransition() {
313       return firstTransition;
314     }
315   }
316
317   // This class stores a representation of an execution
318   // TODO: We can modify this class to implement some optimization (e.g., clock-vector)
319   // TODO: We basically need to keep track of:
320   // TODO:    (1) last read/write access to each memory location
321   // TODO:    (2) last state with two or more incoming events/transitions
322   private class Execution {
323     private HashMap<IntChoiceFromSet, Integer> cgToChoiceMap;   // Map between CG to choice numbers for O(1) access
324     private ArrayList<TransitionEvent> executionTrace;          // The BacktrackPoint objects of this execution
325     private boolean isNew;                                      // Track if this is the first time it is accessed
326     private HashMap<Integer, ReadWriteSet> readWriteFieldsMap;  // Record fields that are accessed
327
328     public Execution() {
329       cgToChoiceMap = new HashMap<>();
330       executionTrace = new ArrayList<>();
331       isNew = true;
332       readWriteFieldsMap = new HashMap<>();
333     }
334
335     public void addTransition(TransitionEvent newBacktrackPoint) {
336       executionTrace.add(newBacktrackPoint);
337     }
338
339     public void clearCGToChoiceMap() {
340       cgToChoiceMap = null;
341     }
342
343     public int getChoiceFromCG(IntChoiceFromSet icsCG) {
344       return cgToChoiceMap.get(icsCG);
345     }
346
347     public ArrayList<TransitionEvent> getExecutionTrace() {
348       return executionTrace;
349     }
350
351     public TransitionEvent getFirstTransition() {
352       return executionTrace.get(0);
353     }
354
355     public HashMap<Integer, ReadWriteSet> getReadWriteFieldsMap() {
356       return readWriteFieldsMap;
357     }
358
359     public boolean isNew() {
360       if (isNew) {
361         // Right after this is accessed, it is no longer new
362         isNew = false;
363         return true;
364       }
365       return false;
366     }
367
368     public void mapCGToChoice(IntChoiceFromSet icsCG, int choice) {
369       cgToChoiceMap.put(icsCG, choice);
370     }
371   }
372
373   // This class compactly stores a predecessor
374   // 1) a predecessor execution
375   // 2) the predecessor choice in that predecessor execution
376   private class Predecessor {
377     private int choice;           // Predecessor choice
378     private Execution execution;  // Predecessor execution
379
380     public Predecessor(int predChoice, Execution predExec) {
381       choice = predChoice;
382       execution = predExec;
383     }
384
385     public int getChoice() {
386       return choice;
387     }
388
389     public Execution getExecution() {
390       return execution;
391     }
392   }
393
394   // This class represents a R-Graph (in the paper it is a state transition graph R)
395   // This implementation stores reachable transitions from and connects with past executions
396   private class RGraph {
397     private int hiStateId;                                     // Maximum state Id
398     private HashMap<Integer, HashSet<TransitionEvent>> graph;  // Reachable transitions from past executions
399
400     public RGraph() {
401       hiStateId = 0;
402       graph = new HashMap<>();
403     }
404
405     public void addReachableTransition(int stateId, TransitionEvent transition) {
406       HashSet<TransitionEvent> transitionSet;
407       if (graph.containsKey(stateId)) {
408         transitionSet = graph.get(stateId);
409       } else {
410         transitionSet = new HashSet<>();
411         graph.put(stateId, transitionSet);
412       }
413       // Insert into the set if it does not contain it yet
414       if (!transitionSet.contains(transition)) {
415         transitionSet.add(transition);
416       }
417       // Update highest state ID
418       if (hiStateId < stateId) {
419         hiStateId = stateId;
420       }
421     }
422
423     public HashSet<TransitionEvent> getReachableTransitionsAtState(int stateId) {
424       return graph.get(stateId);
425     }
426
427     public HashSet<TransitionEvent> getReachableTransitions(int stateId) {
428       HashSet<TransitionEvent> reachableTransitions = new HashSet<>();
429       // All transitions from states higher than the given state ID (until the highest state ID) are reachable
430       for(int stId = stateId; stId <= hiStateId; stId++) {
431         reachableTransitions.addAll(graph.get(stId));
432       }
433       return reachableTransitions;
434     }
435   }
436
437   // This class compactly stores Read and Write field sets
438   // We store the field name and its object ID
439   // Sharing the same field means the same field name and object ID
440   private class ReadWriteSet {
441     private HashMap<String, Integer> readMap;
442     private HashMap<String, Integer> writeMap;
443
444     public ReadWriteSet() {
445       readMap = new HashMap<>();
446       writeMap = new HashMap<>();
447     }
448
449     public void addReadField(String field, int objectId) {
450       readMap.put(field, objectId);
451     }
452
453     public void addWriteField(String field, int objectId) {
454       writeMap.put(field, objectId);
455     }
456
457     public void removeReadField(String field) {
458       readMap.remove(field);
459     }
460
461     public void removeWriteField(String field) {
462       writeMap.remove(field);
463     }
464
465     public boolean isEmpty() {
466       return readMap.isEmpty() && writeMap.isEmpty();
467     }
468
469     public ReadWriteSet getCopy() {
470       ReadWriteSet copyRWSet = new ReadWriteSet();
471       // Copy the maps in the set into the new object copy
472       copyRWSet.setReadMap(new HashMap<>(this.getReadMap()));
473       copyRWSet.setWriteMap(new HashMap<>(this.getWriteMap()));
474       return copyRWSet;
475     }
476
477     public Set<String> getReadSet() {
478       return readMap.keySet();
479     }
480
481     public Set<String> getWriteSet() {
482       return writeMap.keySet();
483     }
484
485     public boolean readFieldExists(String field) {
486       return readMap.containsKey(field);
487     }
488
489     public boolean writeFieldExists(String field) {
490       return writeMap.containsKey(field);
491     }
492
493     public int readFieldObjectId(String field) {
494       return readMap.get(field);
495     }
496
497     public int writeFieldObjectId(String field) {
498       return writeMap.get(field);
499     }
500
501     private HashMap<String, Integer> getReadMap() {
502       return readMap;
503     }
504
505     private HashMap<String, Integer> getWriteMap() {
506       return writeMap;
507     }
508
509     private void setReadMap(HashMap<String, Integer> rMap) {
510       readMap = rMap;
511     }
512
513     private void setWriteMap(HashMap<String, Integer> wMap) {
514       writeMap = wMap;
515     }
516   }
517
518   // This class compactly stores transitions:
519   // 1) CG,
520   // 2) state ID,
521   // 3) choice,
522   // 4) predecessors (for backward DFS).
523   private class TransitionEvent {
524     private int choice;                        // Choice chosen at this transition
525     private int choiceCounter;                 // Choice counter at this transition
526     private Execution execution;               // The execution where this transition belongs
527     private HashSet<Predecessor> predecessors; // Maps incoming events/transitions (execution and choice)
528     private int stateId;                       // State at this transition
529     private IntChoiceFromSet transitionCG;     // CG at this transition
530
531     public TransitionEvent() {
532       choice = 0;
533       choiceCounter = 0;
534       execution = null;
535       predecessors = new HashSet<>();
536       stateId = 0;
537       transitionCG = null;
538     }
539
540     public int getChoice() {
541       return choice;
542     }
543
544     public int getChoiceCounter() {
545       return choiceCounter;
546     }
547
548     public Execution getExecution() {
549       return execution;
550     }
551
552     public HashSet<Predecessor> getPredecessors() {
553       return predecessors;
554     }
555
556     public int getStateId() {
557       return stateId;
558     }
559
560     public IntChoiceFromSet getTransitionCG() { return transitionCG; }
561
562     public void recordPredecessor(Execution execution, int choice) {
563       predecessors.add(new Predecessor(choice, execution));
564     }
565
566     public void setChoice(int cho) {
567       choice = cho;
568     }
569
570     public void setChoiceCounter(int choCounter) {
571       choiceCounter = choCounter;
572     }
573
574     public void setExecution(Execution exec) {
575       execution = exec;
576     }
577
578     public void setPredecessors(HashSet<Predecessor> preds) {
579       predecessors = new HashSet<>(preds);
580     }
581
582     public void setStateId(int stId) {
583       stateId = stId;
584     }
585
586     public void setTransitionCG(IntChoiceFromSet cg) {
587       transitionCG = cg;
588     }
589   }
590
591   // -- CONSTANTS
592   private final static String DO_CALL_METHOD = "doCall";
593   // We exclude fields that come from libraries (Java and Groovy), and also the infrastructure
594   private final static String[] EXCLUDED_FIELDS_CONTAINS_LIST = {"_closure"};
595   private final static String[] EXCLUDED_FIELDS_ENDS_WITH_LIST =
596           // Groovy library created fields
597           {"stMC", "callSiteArray", "metaClass", "staticClassInfo", "__constructor__",
598           // Infrastructure
599           "sendEvent", "Object", "reference", "location", "app", "state", "log", "functionList", "objectList",
600           "eventList", "valueList", "settings", "printToConsole", "app1", "app2"};
601   private final static String[] EXCLUDED_FIELDS_STARTS_WITH_LIST =
602           // Java and Groovy libraries
603           { "java", "org", "sun", "com", "gov", "groovy"};
604   private final static String[] EXCLUDED_FIELDS_READ_WRITE_INSTRUCTIONS_STARTS_WITH_LIST = {"Event"};
605   private final static String GET_PROPERTY_METHOD =
606           "invokeinterface org.codehaus.groovy.runtime.callsite.CallSite.callGetProperty";
607   private final static String GROOVY_CALLSITE_LIB = "org.codehaus.groovy.runtime.callsite";
608   private final static String JAVA_INTEGER = "int";
609   private final static String JAVA_STRING_LIB = "java.lang.String";
610
611   // -- FUNCTIONS
612   private Integer[] copyChoices(Integer[] choicesToCopy) {
613
614     Integer[] copyOfChoices = new Integer[choicesToCopy.length];
615     System.arraycopy(choicesToCopy, 0, copyOfChoices, 0, choicesToCopy.length);
616     return copyOfChoices;
617   }
618
619   private void ensureFairSchedulingAndSetupTransition(IntChoiceFromSet icsCG, VM vm) {
620     // Check the next choice and if the value is not the same as the expected then force the expected value
621     int choiceIndex = choiceCounter % refChoices.length;
622     int nextChoice = icsCG.getNextChoice();
623     if (refChoices[choiceIndex] != nextChoice) {
624       int expectedChoice = refChoices[choiceIndex];
625       int currCGIndex = icsCG.getNextChoiceIndex();
626       if ((currCGIndex >= 0) && (currCGIndex < refChoices.length)) {
627         icsCG.setChoice(currCGIndex, expectedChoice);
628       }
629     }
630     // Get state ID and associate it with this transition
631     int stateId = vm.getStateId();
632     TransitionEvent transition = setupTransition(icsCG, stateId, choiceIndex);
633     // Add new transition to the current execution and map it in R-Graph
634     for (Integer stId : justVisitedStates) {  // Map this transition to all the previously passed states
635       rGraph.addReachableTransition(stId, transition);
636     }
637     currentExecution.mapCGToChoice(icsCG, choiceCounter);
638     // Store restorable state object for this state (always store the latest)
639     RestorableVMState restorableState = vm.getRestorableState();
640     restorableStateMap.put(stateId, restorableState);
641   }
642
643   private TransitionEvent setupTransition(IntChoiceFromSet icsCG, int stateId, int choiceIndex) {
644     // Get a new transition
645     TransitionEvent transition;
646     if (currentExecution.isNew()) {
647       // We need to handle the first transition differently because this has a predecessor execution
648       transition = currentExecution.getFirstTransition();
649     } else {
650       transition = new TransitionEvent();
651       currentExecution.addTransition(transition);
652       transition.recordPredecessor(currentExecution, choiceCounter - 1);
653     }
654     transition.setExecution(currentExecution);
655     transition.setTransitionCG(icsCG);
656     transition.setStateId(stateId);
657     transition.setChoice(refChoices[choiceIndex]);
658     transition.setChoiceCounter(choiceCounter);
659
660     return transition;
661   }
662
663   // --- Functions related to cycle detection and reachability graph
664
665   // Detect cycles in the current execution/trace
666   // We terminate the execution iff:
667   // (1) the state has been visited in the current execution
668   // (2) the state has one or more cycles that involve all the events
669   // With simple approach we only need to check for a re-visited state.
670   // Basically, we have to check that we have executed all events between two occurrences of such state.
671   private boolean completeFullCycle(int stId) {
672     // False if the state ID hasn't been recorded
673     if (!stateToEventMap.containsKey(stId)) {
674       return false;
675     }
676     HashSet<Integer> visitedEvents = stateToEventMap.get(stId);
677     // Check if this set contains all the event choices
678     // If not then this is not the terminating condition
679     for(int i=0; i<=maxEventChoice; i++) {
680       if (!visitedEvents.contains(i)) {
681         return false;
682       }
683     }
684     return true;
685   }
686
687   private void initializeStatesVariables() {
688     // DPOR-related
689     choices = null;
690     refChoices = null;
691     choiceCounter = 0;
692     maxEventChoice = 0;
693     // Cycle tracking
694     currVisitedStates = new HashSet<>();
695     justVisitedStates = new HashSet<>();
696     prevVisitedStates = new HashSet<>();
697     stateToEventMap = new HashMap<>();
698     // Backtracking
699     backtrackMap = new HashMap<>();
700     backtrackStateQ = new PriorityQueue<>(Collections.reverseOrder());
701     currentExecution = new Execution();
702     currentExecution.addTransition(new TransitionEvent()); // Always start with 1 backtrack point
703     doneBacktrackSet = new HashSet<>();
704     rGraph = new RGraph();
705     // Booleans
706     isEndOfExecution = false;
707   }
708
709   private void mapStateToEvent(int nextChoiceValue) {
710     // Update all states with this event/choice
711     // This means that all past states now see this transition
712     Set<Integer> stateSet = stateToEventMap.keySet();
713     for(Integer stateId : stateSet) {
714       HashSet<Integer> eventSet = stateToEventMap.get(stateId);
715       eventSet.add(nextChoiceValue);
716     }
717   }
718
719   private boolean terminateCurrentExecution() {
720     // We need to check all the states that have just been visited
721     // Often a transition (choice/event) can result into forwarding/backtracking to a number of states
722     for(Integer stateId : justVisitedStates) {
723       if (prevVisitedStates.contains(stateId) || completeFullCycle(stateId)) {
724         return true;
725       }
726     }
727     return false;
728   }
729
730   private void updateStateInfo(Search search) {
731     // Update the state variables
732     int stateId = search.getStateId();
733     // Insert state ID into the map if it is new
734     if (!stateToEventMap.containsKey(stateId)) {
735       HashSet<Integer> eventSet = new HashSet<>();
736       stateToEventMap.put(stateId, eventSet);
737     }
738     analyzeReachabilityAndCreateBacktrackPoints(search.getVM(), stateId);
739     justVisitedStates.add(stateId);
740     if (!prevVisitedStates.contains(stateId)) {
741       // It is a currently visited states if the state has not been seen in previous executions
742       currVisitedStates.add(stateId);
743     }
744   }
745
746   // --- Functions related to Read/Write access analysis on shared fields
747
748   private void addNewBacktrackPoint(int stateId, Integer[] newChoiceList, TransitionEvent conflictTransition) {
749     // Insert backtrack point to the right state ID
750     LinkedList<BacktrackExecution> backtrackExecList;
751     if (backtrackMap.containsKey(stateId)) {
752       backtrackExecList = backtrackMap.get(stateId);
753     } else {
754       backtrackExecList = new LinkedList<>();
755       backtrackMap.put(stateId, backtrackExecList);
756     }
757     // Add the new backtrack execution object
758     TransitionEvent backtrackTransition = new TransitionEvent();
759     backtrackTransition.setPredecessors(conflictTransition.getPredecessors());
760     backtrackExecList.addFirst(new BacktrackExecution(newChoiceList, backtrackTransition));
761     // Add to priority queue
762     if (!backtrackStateQ.contains(stateId)) {
763       backtrackStateQ.add(stateId);
764     }
765   }
766
767   // Analyze Read/Write accesses that are directly invoked on fields
768   private void analyzeReadWriteAccesses(Instruction executedInsn, int currentChoice) {
769     // Get the field info
770     FieldInfo fieldInfo = ((JVMFieldInstruction) executedInsn).getFieldInfo();
771     // Analyze only after being initialized
772     String fieldClass = fieldInfo.getFullName();
773     // Do the analysis to get Read and Write accesses to fields
774     ReadWriteSet rwSet = getReadWriteSet(currentChoice);
775     int objectId = fieldInfo.getClassInfo().getClassObjectRef();
776     // Record the field in the map
777     if (executedInsn instanceof WriteInstruction) {
778       // We first check the non-relevant fields set
779       if (!nonRelevantFields.contains(fieldInfo)) {
780         // Exclude certain field writes because of infrastructure needs, e.g., Event class field writes
781         for (String str : EXCLUDED_FIELDS_READ_WRITE_INSTRUCTIONS_STARTS_WITH_LIST) {
782           if (fieldClass.startsWith(str)) {
783             nonRelevantFields.add(fieldInfo);
784             return;
785           }
786         }
787       } else {
788         // If we have this field in the non-relevant fields set then we return right away
789         return;
790       }
791       rwSet.addWriteField(fieldClass, objectId);
792     } else if (executedInsn instanceof ReadInstruction) {
793       rwSet.addReadField(fieldClass, objectId);
794     }
795   }
796
797   // Analyze Read accesses that are indirect (performed through iterators)
798   // These accesses are marked by certain bytecode instructions, e.g., INVOKEINTERFACE
799   private void analyzeReadWriteAccesses(Instruction instruction, ThreadInfo ti, int currentChoice) {
800     // Get method name
801     INVOKEINTERFACE insn = (INVOKEINTERFACE) instruction;
802     if (insn.toString().startsWith(GET_PROPERTY_METHOD) &&
803             insn.getMethodInfo().getName().equals(DO_CALL_METHOD)) {
804       // Extract info from the stack frame
805       StackFrame frame = ti.getTopFrame();
806       int[] frameSlots = frame.getSlots();
807       // Get the Groovy callsite library at index 0
808       ElementInfo eiCallsite = VM.getVM().getHeap().get(frameSlots[0]);
809       if (!eiCallsite.getClassInfo().getName().startsWith(GROOVY_CALLSITE_LIB)) {
810         return;
811       }
812       // Get the iterated object whose property is accessed
813       ElementInfo eiAccessObj = VM.getVM().getHeap().get(frameSlots[1]);
814       if (eiAccessObj == null) {
815         return;
816       }
817       // We exclude library classes (they start with java, org, etc.) and some more
818       ClassInfo classInfo = eiAccessObj.getClassInfo();
819       String objClassName = classInfo.getName();
820       // Check if this class info is part of the non-relevant classes set already
821       if (!nonRelevantClasses.contains(classInfo)) {
822         if (excludeThisForItStartsWith(EXCLUDED_FIELDS_READ_WRITE_INSTRUCTIONS_STARTS_WITH_LIST, objClassName) ||
823                 excludeThisForItStartsWith(EXCLUDED_FIELDS_STARTS_WITH_LIST, objClassName)) {
824           nonRelevantClasses.add(classInfo);
825           return;
826         }
827       } else {
828         // If it is part of the non-relevant classes set then return immediately
829         return;
830       }
831       // Extract fields from this object and put them into the read write
832       int numOfFields = eiAccessObj.getNumberOfFields();
833       for(int i=0; i<numOfFields; i++) {
834         FieldInfo fieldInfo = eiAccessObj.getFieldInfo(i);
835         if (fieldInfo.getType().equals(JAVA_STRING_LIB) || fieldInfo.getType().equals(JAVA_INTEGER)) {
836           String fieldClass = fieldInfo.getFullName();
837           ReadWriteSet rwSet = getReadWriteSet(currentChoice);
838           int objectId = fieldInfo.getClassInfo().getClassObjectRef();
839           // Record the field in the map
840           rwSet.addReadField(fieldClass, objectId);
841         }
842       }
843     }
844   }
845
846   private int checkAndAdjustChoice(int currentChoice, VM vm) {
847     // If current choice is not the same, then this is caused by the firing of IntIntervalGenerator
848     // for certain method calls in the infrastructure, e.g., eventSince()
849     ChoiceGenerator<?> currentCG = vm.getChoiceGenerator();
850     // This is the main event CG
851     if (currentCG instanceof IntIntervalGenerator) {
852       // This is the interval CG used in device handlers
853       ChoiceGenerator<?> parentCG = ((IntIntervalGenerator) currentCG).getPreviousChoiceGenerator();
854       // Iterate until we find the IntChoiceFromSet CG
855       while (!(parentCG instanceof IntChoiceFromSet)) {
856         parentCG = ((IntIntervalGenerator) parentCG).getPreviousChoiceGenerator();
857       }
858       // Find the choice related to the IntIntervalGenerator CG from the map
859       currentChoice = currentExecution.getChoiceFromCG((IntChoiceFromSet) parentCG);
860     }
861     return currentChoice;
862   }
863
864   private void createBacktrackingPoint(Execution execution, int currentChoice,
865                                        Execution conflictExecution, int conflictChoice) {
866     // Create a new list of choices for backtrack based on the current choice and conflicting event number
867     // E.g. if we have a conflict between 1 and 3, then we create the list {3, 1, 0, 2}
868     // for the original set {0, 1, 2, 3}
869     Integer[] newChoiceList = new Integer[refChoices.length];
870     ArrayList<TransitionEvent> currentTrace = execution.getExecutionTrace();
871     ArrayList<TransitionEvent> conflictTrace = conflictExecution.getExecutionTrace();
872     int currChoice = currentTrace.get(currentChoice).getChoice();
873     int stateId = conflictTrace.get(conflictChoice).getStateId();
874     // Check if this trace has been done from this state
875     if (isTraceAlreadyConstructed(currChoice, stateId)) {
876       return;
877     }
878     // Put the conflicting event numbers first and reverse the order
879     newChoiceList[0] = currChoice;
880     // Put the rest of the event numbers into the array starting from the minimum to the upper bound
881     for (int i = 0, j = 1; i < refChoices.length; i++) {
882       if (refChoices[i] != newChoiceList[0]) {
883         newChoiceList[j] = refChoices[i];
884         j++;
885       }
886     }
887     // Predecessor of the new backtrack point is the same as the conflict point's
888     addNewBacktrackPoint(stateId, newChoiceList, conflictTrace.get(conflictChoice));
889   }
890
891   private boolean excludeThisForItContains(String[] excludedStrings, String className) {
892     for (String excludedField : excludedStrings) {
893       if (className.contains(excludedField)) {
894         return true;
895       }
896     }
897     return false;
898   }
899
900   private boolean excludeThisForItEndsWith(String[] excludedStrings, String className) {
901     for (String excludedField : excludedStrings) {
902       if (className.endsWith(excludedField)) {
903         return true;
904       }
905     }
906     return false;
907   }
908
909   private boolean excludeThisForItStartsWith(String[] excludedStrings, String className) {
910     for (String excludedField : excludedStrings) {
911       if (className.startsWith(excludedField)) {
912         return true;
913       }
914     }
915     return false;
916   }
917
918   private void exploreNextBacktrackPoints(VM vm, IntChoiceFromSet icsCG) {
919                 // Check if we are reaching the end of our execution: no more backtracking points to explore
920                 // cgMap, backtrackMap, backtrackStateQ are updated simultaneously (checking backtrackStateQ is enough)
921                 if (!backtrackStateQ.isEmpty()) {
922                         // Set done all the other backtrack points
923                         for (TransitionEvent backtrackTransition : currentExecution.getExecutionTrace()) {
924         backtrackTransition.getTransitionCG().setDone();
925                         }
926                         // Reset the next backtrack point with the latest state
927                         int hiStateId = backtrackStateQ.peek();
928                         // Restore the state first if necessary
929                         if (vm.getStateId() != hiStateId) {
930                                 RestorableVMState restorableState = restorableStateMap.get(hiStateId);
931                                 vm.restoreState(restorableState);
932                         }
933                         // Set the backtrack CG
934                         IntChoiceFromSet backtrackCG = (IntChoiceFromSet) vm.getChoiceGenerator();
935                         setBacktrackCG(hiStateId, backtrackCG);
936                 } else {
937                         // Set done this last CG (we save a few rounds)
938                         icsCG.setDone();
939                 }
940                 // Save all the visited states when starting a new execution of trace
941                 prevVisitedStates.addAll(currVisitedStates);
942                 // This marks a transitional period to the new CG
943                 isEndOfExecution = true;
944   }
945
946   private boolean isConflictFound(Execution execution, int reachableChoice, Execution conflictExecution, int conflictChoice,
947                                   ReadWriteSet currRWSet) {
948     ArrayList<TransitionEvent> executionTrace = execution.getExecutionTrace();
949     ArrayList<TransitionEvent> conflictTrace = conflictExecution.getExecutionTrace();
950     HashMap<Integer, ReadWriteSet> confRWFieldsMap = conflictExecution.getReadWriteFieldsMap();
951     // Skip if this event does not have any Read/Write set or the two events are basically the same event (number)
952     if (!confRWFieldsMap.containsKey(conflictChoice) ||
953             executionTrace.get(reachableChoice).getChoice() == conflictTrace.get(conflictChoice).getChoice()) {
954       return false;
955     }
956     // R/W set of choice/event that may have a potential conflict
957     ReadWriteSet confRWSet = confRWFieldsMap.get(conflictChoice);
958     // Check for conflicts with Read and Write fields for Write instructions
959     Set<String> currWriteSet = currRWSet.getWriteSet();
960     for(String writeField : currWriteSet) {
961       int currObjId = currRWSet.writeFieldObjectId(writeField);
962       if ((confRWSet.readFieldExists(writeField) && confRWSet.readFieldObjectId(writeField) == currObjId) ||
963           (confRWSet.writeFieldExists(writeField) && confRWSet.writeFieldObjectId(writeField) == currObjId)) {
964         // Remove this from the write set as we are tracking per memory location
965         currRWSet.removeWriteField(writeField);
966         return true;
967       }
968     }
969     // Check for conflicts with Write fields for Read instructions
970     Set<String> currReadSet = currRWSet.getReadSet();
971     for(String readField : currReadSet) {
972       int currObjId = currRWSet.readFieldObjectId(readField);
973       if (confRWSet.writeFieldExists(readField) && confRWSet.writeFieldObjectId(readField) == currObjId) {
974         // Remove this from the read set as we are tracking per memory location
975         currRWSet.removeReadField(readField);
976         return true;
977       }
978     }
979     // Return false if no conflict is found
980     return false;
981   }
982
983   private ReadWriteSet getReadWriteSet(int currentChoice) {
984     // Do the analysis to get Read and Write accesses to fields
985     ReadWriteSet rwSet;
986     // We already have an entry
987     HashMap<Integer, ReadWriteSet> currReadWriteFieldsMap = currentExecution.getReadWriteFieldsMap();
988     if (currReadWriteFieldsMap.containsKey(currentChoice)) {
989       rwSet = currReadWriteFieldsMap.get(currentChoice);
990     } else { // We need to create a new entry
991       rwSet = new ReadWriteSet();
992       currReadWriteFieldsMap.put(currentChoice, rwSet);
993     }
994     return rwSet;
995   }
996
997   private boolean isFieldExcluded(Instruction executedInsn) {
998     // Get the field info
999     FieldInfo fieldInfo = ((JVMFieldInstruction) executedInsn).getFieldInfo();
1000     // Check if the non-relevant fields set already has it
1001     if (nonRelevantFields.contains(fieldInfo)) {
1002       return true;
1003     }
1004     // Check if the relevant fields set already has it
1005     if (relevantFields.contains(fieldInfo)) {
1006       return false;
1007     }
1008     // Analyze only after being initialized
1009     String field = fieldInfo.getFullName();
1010     // Check against "starts-with", "ends-with", and "contains" list
1011     if (excludeThisForItStartsWith(EXCLUDED_FIELDS_STARTS_WITH_LIST, field) ||
1012             excludeThisForItEndsWith(EXCLUDED_FIELDS_ENDS_WITH_LIST, field) ||
1013             excludeThisForItContains(EXCLUDED_FIELDS_CONTAINS_LIST, field)) {
1014       nonRelevantFields.add(fieldInfo);
1015       return true;
1016     }
1017     relevantFields.add(fieldInfo);
1018     return false;
1019   }
1020
1021   // Check if this trace is already constructed
1022   private boolean isTraceAlreadyConstructed(int firstChoice, int stateId) {
1023     // Concatenate state ID and only the first event in the string, e.g., "1:1 for the trace 10234 at state 1"
1024     // TODO: THIS IS AN OPTIMIZATION!
1025     // This is the optimized version because after we execute, e.g., the trace 1:10234, we don't need to try
1026     // another trace that starts with event 1 at state 1, e.g., the trace 1:13024
1027     // The second time this event 1 is explored, it will generate the same state as the first one
1028     StringBuilder sb = new StringBuilder();
1029     sb.append(stateId);
1030     sb.append(':');
1031     sb.append(firstChoice);
1032     // Check if the trace has been constructed as a backtrack point for this state
1033     if (doneBacktrackSet.contains(sb.toString())) {
1034       return true;
1035     }
1036     doneBacktrackSet.add(sb.toString());
1037     return false;
1038   }
1039
1040   // Reset data structure for each new execution
1041   private void resetStatesForNewExecution(IntChoiceFromSet icsCG, VM vm) {
1042     if (choices == null || choices != icsCG.getAllChoices()) {
1043       // Reset state variables
1044       choiceCounter = 0;
1045       choices = icsCG.getAllChoices();
1046       refChoices = copyChoices(choices);
1047       // Clear data structures
1048       currVisitedStates = new HashSet<>();
1049       stateToEventMap = new HashMap<>();
1050       isEndOfExecution = false;
1051     }
1052   }
1053
1054   // Set a backtrack point for a particular state
1055   private void setBacktrackCG(int stateId, IntChoiceFromSet backtrackCG) {
1056     // Set a backtrack CG based on a state ID
1057     LinkedList<BacktrackExecution> backtrackExecutions = backtrackMap.get(stateId);
1058     BacktrackExecution backtrackExecution = backtrackExecutions.removeLast();
1059     backtrackCG.setNewValues(backtrackExecution.getChoiceList());  // Get the last from the queue
1060     backtrackCG.setStateId(stateId);
1061     backtrackCG.reset();
1062     // Update current execution with this new execution
1063     Execution newExecution = new Execution();
1064     TransitionEvent firstTransition = backtrackExecution.getFirstTransition();
1065     newExecution.addTransition(firstTransition);
1066     // Try to free some memory since this map is only used for the current execution
1067     currentExecution.clearCGToChoiceMap();
1068     currentExecution = newExecution;
1069     // Remove from the queue if we don't have more backtrack points for that state
1070     if (backtrackExecutions.isEmpty()) {
1071       backtrackMap.remove(stateId);
1072       backtrackStateQ.remove(stateId);
1073     }
1074   }
1075
1076   // Update backtrack sets
1077   // 1) recursively, and
1078   // 2) track accesses per memory location (per shared variable/field)
1079   private void updateBacktrackSet(Execution execution, int currentChoice) {
1080     // Copy ReadWriteSet object
1081     HashMap<Integer, ReadWriteSet> currRWFieldsMap = execution.getReadWriteFieldsMap();
1082     ReadWriteSet currRWSet = currRWFieldsMap.get(currentChoice);
1083     if (currRWSet == null) {
1084       return;
1085     }
1086     currRWSet = currRWSet.getCopy();
1087     // Memorize visited TransitionEvent object while performing backward DFS to avoid getting caught up in a cycle
1088     HashSet<TransitionEvent> visited = new HashSet<>();
1089     // Update backtrack set recursively
1090     // TODO: The following is the call to the original version of the method
1091 //    updateBacktrackSetRecursive(execution, currentChoice, execution, currentChoice, currRWSet, visited);
1092     // TODO: The following is the call to the version of the method with pushing up happens-before transitions
1093     updateBacktrackSetRecursive(execution, currentChoice, execution, currentChoice, execution, currentChoice, currRWSet, visited);
1094   }
1095
1096 //  TODO: This is the original version of the recursive method
1097 //  private void updateBacktrackSetRecursive(Execution execution, int currentChoice,
1098 //                                           Execution conflictExecution, int conflictChoice,
1099 //                                           ReadWriteSet currRWSet, HashSet<TransitionEvent> visited) {
1100 //    // Halt when we have found the first read/write conflicts for all memory locations
1101 //    if (currRWSet.isEmpty()) {
1102 //      return;
1103 //    }
1104 //    TransitionEvent confTrans = conflictExecution.getExecutionTrace().get(conflictChoice);
1105 //    // Halt when we have visited this transition (in a cycle)
1106 //    if (visited.contains(confTrans)) {
1107 //      return;
1108 //    }
1109 //    visited.add(confTrans);
1110 //    // Explore all predecessors
1111 //    for (Predecessor predecessor : confTrans.getPredecessors()) {
1112 //      // Get the predecessor (previous conflict choice)
1113 //      conflictChoice = predecessor.getChoice();
1114 //      conflictExecution = predecessor.getExecution();
1115 //      // Check if a conflict is found
1116 //      if (isConflictFound(execution, currentChoice, conflictExecution, conflictChoice, currRWSet)) {
1117 //        createBacktrackingPoint(execution, currentChoice, conflictExecution, conflictChoice);
1118 //      }
1119 //      // Continue performing DFS if conflict is not found
1120 //      updateBacktrackSetRecursive(execution, currentChoice, conflictExecution, conflictChoice, currRWSet, visited);
1121 //    }
1122 //  }
1123
1124   // TODO: This is the version of the method with pushing up happens-before transitions
1125   private void updateBacktrackSetRecursive(Execution execution, int currentChoice,
1126                                            Execution conflictExecution, int conflictChoice,
1127                                            Execution hbExecution, int hbChoice,
1128                                            ReadWriteSet currRWSet, HashSet<TransitionEvent> visited) {
1129     // Halt when we have found the first read/write conflicts for all memory locations
1130     if (currRWSet.isEmpty()) {
1131       return;
1132     }
1133     TransitionEvent confTrans = conflictExecution.getExecutionTrace().get(conflictChoice);
1134     // Halt when we have visited this transition (in a cycle)
1135     if (visited.contains(confTrans)) {
1136       return;
1137     }
1138     visited.add(confTrans);
1139     // Explore all predecessors
1140     for (Predecessor predecessor : confTrans.getPredecessors()) {
1141       // Get the predecessor (previous conflict choice)
1142       conflictChoice = predecessor.getChoice();
1143       conflictExecution = predecessor.getExecution();
1144       // Push up one happens-before transition
1145       int pushedChoice = hbChoice;
1146       Execution pushedExecution = hbExecution;
1147       // Check if a conflict is found
1148       if (isConflictFound(execution, currentChoice, conflictExecution, conflictChoice, currRWSet)) {
1149         createBacktrackingPoint(pushedExecution, pushedChoice, conflictExecution, conflictChoice);
1150         pushedChoice = conflictChoice;
1151         pushedExecution = conflictExecution;
1152       }
1153       // Continue performing DFS if conflict is not found
1154       updateBacktrackSetRecursive(execution, currentChoice, conflictExecution, conflictChoice,
1155               pushedExecution, pushedChoice, currRWSet, visited);
1156     }
1157     // Remove the transition after being explored
1158     visited.remove(confTrans);
1159   }
1160
1161   // --- Functions related to the reachability analysis when there is a state match
1162
1163   private void analyzeReachabilityAndCreateBacktrackPoints(VM vm, int stateId) {
1164     // Perform this analysis only when:
1165     // 1) this is not during a switch to a new execution,
1166     // 2) at least 2 choices/events have been explored (choiceCounter > 1),
1167     // 3) state > 0 (state 0 is for boolean CG)
1168     if (!isEndOfExecution && choiceCounter > 1 && stateId > 0) {
1169       if (currVisitedStates.contains(stateId) || prevVisitedStates.contains(stateId)) {
1170         // Update reachable transitions in the graph with a predecessor
1171         HashSet<TransitionEvent> reachableTransitions = rGraph.getReachableTransitionsAtState(stateId);
1172         for(TransitionEvent transition : reachableTransitions) {
1173           transition.recordPredecessor(currentExecution, choiceCounter - 1);
1174         }
1175         updateBacktrackSetsFromPreviousExecution(stateId);
1176       }
1177     }
1178   }
1179
1180   // Update the backtrack sets from previous executions
1181   private void updateBacktrackSetsFromPreviousExecution(int stateId) {
1182     // Collect all the reachable transitions from R-Graph
1183     HashSet<TransitionEvent> reachableTransitions = rGraph.getReachableTransitions(stateId);
1184     for(TransitionEvent transition : reachableTransitions) {
1185       Execution execution = transition.getExecution();
1186       int currentChoice = transition.getChoiceCounter();
1187       updateBacktrackSet(execution, currentChoice);
1188     }
1189   }
1190 }