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