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