src/main/gov/nasa/jpf/listener/StateReducer.java

   1 /*
   2  * Copyright (C) 2014, United States Government, as represented by the
   3  * Administrator of the National Aeronautics and Space Administration.
   4  * All rights reserved.
   5  *
   6  * The Java Pathfinder core (jpf-core) platform is licensed under the
   7  * Apache License, Version 2.0 (the "License"); you may not use this file except
   8  * in compliance with the License. You may obtain a copy of the License at
   9  *
  10  *        http://www.apache.org/licenses/LICENSE-2.0.
  11  *
  12  * Unless required by applicable law or agreed to in writing, software
  13  * distributed under the License is distributed on an "AS IS" BASIS,
  14  * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
  15  * See the License for the specific language governing permissions and
  16  * limitations under the License.
  17  */
  18 package gov.nasa.jpf.listener;
  19
  20 import gov.nasa.jpf.Config;
  21 import gov.nasa.jpf.JPF;
  22 import gov.nasa.jpf.ListenerAdapter;
  23 import gov.nasa.jpf.search.Search;
  24 import gov.nasa.jpf.jvm.bytecode.*;
  25 import gov.nasa.jpf.vm.*;
  26 import gov.nasa.jpf.vm.bytecode.ReadInstruction;
  27 import gov.nasa.jpf.vm.bytecode.WriteInstruction;
  28 import gov.nasa.jpf.vm.choice.IntChoiceFromSet;
  29
  30 import java.io.PrintWriter;
  31
  32 import java.util.*;
  33
  34 // TODO: Fix for Groovy's model-checking
  35 // TODO: This is a setter to change the values of the ChoiceGenerator to implement POR
  36 /**
  37  * simple tool to log state changes
  38  */
  39 public class StateReducer extends ListenerAdapter {
  40
  41   // Debug info fields
  42   private boolean debugMode;
  43   private boolean stateReductionMode;
  44   private final PrintWriter out;
  45   volatile private String detail;
  46   volatile private int depth;
  47   volatile private int id;
  48   Transition transition;
  49
  50   // State reduction fields
  51   private Integer[] choices;
  52   private IntChoiceFromSet currCG;
  53   private int choiceCounter;
  54   private Integer choiceUpperBound;
  55   private Integer maxUpperBound;
  56   private boolean isInitialized;
  57   private boolean isResetAfterAnalysis;
  58   private boolean isBooleanCGFlipped;
  59   private HashMap<IntChoiceFromSet, Integer> cgMap;
  60   // Record the mapping between event number and field accesses (Read and Write)
  61   private HashMap<Integer, ReadWriteSet> readWriteFieldsMap;
  62   // The following is the backtrack map (set) that stores all the backtrack information
  63   // e.g., event number 1 can have two backtrack sequences: {3,1,2,4,...} and {2,1,3,4,...}
  64   private HashMap<Integer, LinkedList<Integer[]>> backtrackMap;
  65   // Stores explored backtrack lists in the form of HashSet of Strings
  66   private HashSet<String> backtrackSet;
  67   private HashMap<Integer, HashSet<Integer>> conflictPairMap;
  68   // Map choicelist with start index
  69 //  private HashMap<Integer[],Integer> choiceListStartIndexMap;
  70
  71   public StateReducer(Config config, JPF jpf) {
  72     debugMode = config.getBoolean("debug_state_transition", false);
  73     stateReductionMode = config.getBoolean("activate_state_reduction", true);
  74     if (debugMode) {
  75       out = new PrintWriter(System.out, true);
  76     } else {
  77       out = null;
  78     }
  79     detail = null;
  80     depth = 0;
  81     id = 0;
  82     transition = null;
  83     isBooleanCGFlipped = false;
  84     initializeStateReduction();
  85   }
  86
  87   private void initializeStateReduction() {
  88     if (stateReductionMode) {
  89       choices = null;
  90       currCG = null;
  91       choiceCounter = 0;
  92       choiceUpperBound = 0;
  93       maxUpperBound = 0;
  94       isInitialized = false;
  95       isResetAfterAnalysis = false;
  96       cgMap = new HashMap<>();
  97       readWriteFieldsMap = new HashMap<>();
  98       backtrackMap = new HashMap<>();
  99       backtrackSet = new HashSet<>();
 100       conflictPairMap = new HashMap<>();
 101     }
 102   }
 103
 104   @Override
 105   public void stateRestored(Search search) {
 106     if (debugMode) {
 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   //--- the ones we are interested in
 117   @Override
 118   public void searchStarted(Search search) {
 119     if (debugMode) {
 120       out.println("\n==> DEBUG: ----------------------------------- search started" + "\n");
 121     }
 122   }
 123
 124   @Override
 125   public void choiceGeneratorRegistered(VM vm, ChoiceGenerator<?> nextCG, ThreadInfo currentThread, Instruction executedInstruction) {
 126     if (stateReductionMode) {
 127       // Initialize with necessary information from the CG
 128       if (nextCG instanceof IntChoiceFromSet) {
 129         IntChoiceFromSet icsCG = (IntChoiceFromSet) nextCG;
 130         // Check if CG has been initialized, otherwise initialize it
 131         Integer[] cgChoices = icsCG.getAllChoices();
 132         if (!isInitialized) {
 133           // Get the upper bound from the last element of the choices
 134           choiceUpperBound = cgChoices[cgChoices.length - 1];
 135           isInitialized = true;
 136         }
 137         // Record the subsequent Integer CGs only until we hit the upper bound
 138         if (!isResetAfterAnalysis && choiceCounter <= choiceUpperBound && !cgMap.containsValue(choiceCounter)) {
 139           // Update the choices of the first CG and add '-1'
 140           if (choices == null) {
 141             // Initialize backtrack set that stores all the explored backtrack lists
 142             maxUpperBound = cgChoices.length;
 143             // All the choices are always the same so we only need to update it once
 144             choices = new Integer[cgChoices.length + 1];
 145             System.arraycopy(cgChoices, 0, choices, 0, cgChoices.length);
 146             choices[choices.length - 1] = -1;
 147             String firstChoiceListString = buildStringFromChoiceList(choices);
 148             backtrackSet.add(firstChoiceListString);
 149           }
 150           icsCG.setNewValues(choices);
 151           icsCG.reset();
 152           // Advance the current Integer CG
 153           // This way we explore all the event numbers in the first pass
 154           icsCG.advance(choices[choiceCounter]);
 155           cgMap.put(icsCG, choices[choiceCounter]);
 156           choiceCounter++;
 157         } else {
 158           // Set done the subsequent CGs
 159           // We only need n CGs (n is event numbers)
 160           icsCG.setDone();
 161         }
 162       }
 163     }
 164   }
 165
 166   private void resetAllCGs() {
 167     // Extract the event numbers that have backtrack lists
 168     Set<Integer> eventSet = backtrackMap.keySet();
 169     // Return if there is no conflict at all (highly unlikely)
 170     if (eventSet.isEmpty()) {
 171       return;
 172     }
 173     // Reset every CG with the first backtrack lists
 174     for (IntChoiceFromSet cg : cgMap.keySet()) {
 175       int event = cgMap.get(cg);
 176       LinkedList<Integer[]> choiceLists = backtrackMap.get(event);
 177       if (choiceLists != null && choiceLists.peekFirst() != null) {
 178         Integer[] choiceList = choiceLists.removeFirst();
 179         // Deploy the new choice list for this CG
 180         cg.setNewValues(choiceList);
 181         cg.reset();
 182       } else {
 183         cg.setDone();
 184       }
 185     }
 186   }
 187
 188   @Override
 189   public void choiceGeneratorAdvanced(VM vm, ChoiceGenerator<?> currentCG) {
 190
 191     if (stateReductionMode) {
 192       // Check the boolean CG and if it is flipped, we are resetting the analysis
 193       if (currentCG instanceof BooleanChoiceGenerator) {
 194         if (!isBooleanCGFlipped) {
 195           isBooleanCGFlipped = true;
 196         } else {
 197           initializeStateReduction();
 198         }
 199       }
 200       // Check every choice generated and make sure that all the available choices
 201       // are chosen first before repeating the same choice of value twice!
 202       if (currentCG instanceof IntChoiceFromSet) {
 203         IntChoiceFromSet icsCG = (IntChoiceFromSet) currentCG;
 204         // Update the current pointer to the current set of choices
 205         if (choices == null || choices != icsCG.getAllChoices()) {
 206           currCG = icsCG;
 207           choices = icsCG.getAllChoices();
 208           // Reset a few things for the sub-graph
 209           conflictPairMap.clear();
 210           readWriteFieldsMap.clear();
 211           choiceCounter = 0;
 212         }
 213         // Traverse the sub-graphs
 214         if (isResetAfterAnalysis) {
 215           // Advance choice counter for sub-graphs
 216           choiceCounter++;
 217           // Do this for every CG after finishing each backtrack list
 218           if (icsCG.getNextChoice() == -1) {
 219             int event = cgMap.get(icsCG);
 220             LinkedList<Integer[]> choiceLists = backtrackMap.get(event);
 221             if (choiceLists != null && choiceLists.peekFirst() != null) {
 222               Integer[] choiceList = choiceLists.removeFirst();
 223               // Deploy the new choice list for this CG
 224               icsCG.setNewValues(choiceList);
 225               icsCG.reset();
 226             } else {
 227               // Set done if this was the last backtrack list
 228               icsCG.setDone();
 229             }
 230           }
 231         }
 232         // Update and reset the CG if needed (do this for the first time after the analysis)
 233         if (!isResetAfterAnalysis && icsCG.getNextChoice() == -1) {
 234           resetAllCGs();
 235           isResetAfterAnalysis = true;
 236         }
 237       }
 238     }
 239   }
 240
 241   @Override
 242   public void stateAdvanced(Search search) {
 243     if (debugMode) {
 244       id = search.getStateId();
 245       depth = search.getDepth();
 246       transition = search.getTransition();
 247       if (search.isNewState()) {
 248         detail = "new";
 249       } else {
 250         detail = "visited";
 251       }
 252
 253       if (search.isEndState()) {
 254         out.println("\n==> DEBUG: This is the last state!\n");
 255         detail += " end";
 256       }
 257       out.println("\n==> DEBUG: The state is forwarded to state with id: " + id + " with depth: " + depth +
 258               " which is " + detail + " Transition: " + transition + "\n");
 259     }
 260   }
 261
 262   @Override
 263   public void stateBacktracked(Search search) {
 264     if (debugMode) {
 265       id = search.getStateId();
 266       depth = search.getDepth();
 267       transition = search.getTransition();
 268       detail = null;
 269
 270       out.println("\n==> DEBUG: The state is backtracked to state with id: " + id + " -- Transition: " + transition +
 271               " and depth: " + depth + "\n");
 272     }
 273   }
 274
 275   @Override
 276   public void searchFinished(Search search) {
 277     if (debugMode) {
 278       out.println("\n==> DEBUG: ----------------------------------- search finished" + "\n");
 279     }
 280   }
 281
 282   // This class compactly stores Read and Write field sets
 283   // We store the field name and its object ID
 284   // Sharing the same field means the same field name and object ID
 285   private class ReadWriteSet {
 286     private HashMap<String, Integer> readSet;
 287     private HashMap<String, Integer> writeSet;
 288
 289     public ReadWriteSet() {
 290       readSet = new HashMap<>();
 291       writeSet = new HashMap<>();
 292     }
 293
 294     public void addReadField(String field, int objectId) {
 295       readSet.put(field, objectId);
 296     }
 297
 298     public void addWriteField(String field, int objectId) {
 299       writeSet.put(field, objectId);
 300     }
 301
 302     public boolean readFieldExists(String field) {
 303       return readSet.containsKey(field);
 304     }
 305
 306     public boolean writeFieldExists(String field) {
 307       return writeSet.containsKey(field);
 308     }
 309
 310     public int readFieldObjectId(String field) {
 311       return readSet.get(field);
 312     }
 313
 314     public int writeFieldObjectId(String field) {
 315       return writeSet.get(field);
 316     }
 317   }
 318
 319   private void analyzeReadWriteAccesses(Instruction executedInsn, String fieldClass, int currentChoice) {
 320     // Do the analysis to get Read and Write accesses to fields
 321     ReadWriteSet rwSet;
 322     // We already have an entry
 323     if (readWriteFieldsMap.containsKey(choices[currentChoice])) {
 324       rwSet = readWriteFieldsMap.get(choices[currentChoice]);
 325     } else { // We need to create a new entry
 326       rwSet = new ReadWriteSet();
 327       readWriteFieldsMap.put(choices[currentChoice], rwSet);
 328     }
 329     int objectId = ((JVMFieldInstruction) executedInsn).getFieldInfo().getClassInfo().getClassObjectRef();
 330     // Record the field in the map
 331     if (executedInsn instanceof WriteInstruction) {
 332       // Exclude certain field writes because of infrastructure needs, e.g., Event class field writes
 333       for (String str : EXCLUDED_FIELDS_WRITE_INSTRUCTIONS_STARTS_WITH_LIST) {
 334         if (fieldClass.startsWith(str)) {
 335           return;
 336         }
 337       }
 338       rwSet.addWriteField(fieldClass, objectId);
 339     } else if (executedInsn instanceof ReadInstruction) {
 340       rwSet.addReadField(fieldClass, objectId);
 341     }
 342   }
 343
 344   private boolean recordConflictPair(int currentEvent, int eventNumber) {
 345     HashSet<Integer> conflictSet;
 346     if (!conflictPairMap.containsKey(currentEvent)) {
 347       conflictSet = new HashSet<>();
 348       conflictPairMap.put(currentEvent, conflictSet);
 349     } else {
 350       conflictSet = conflictPairMap.get(currentEvent);
 351     }
 352     // If this conflict has been recorded before, we return false because
 353     // we don't want to service this backtrack point twice
 354     if (conflictSet.contains(eventNumber)) {
 355       return false;
 356     }
 357     // If it hasn't been recorded, then do otherwise
 358     conflictSet.add(eventNumber);
 359     return true;
 360   }
 361
 362   private String buildStringFromChoiceList(Integer[] newChoiceList) {
 363
 364     // When we see a choice list shorter than the upper bound, e.g., [3,2] for choices 0,1,2, and 3,
 365     //  then we have to pad the beginning before we store it, because [3,2] actually means [0,1,3,2]
 366     // First, calculate the difference between this choice list and the upper bound
 367     //  The actual list doesn't include '-1' at the end
 368     int actualListLength = newChoiceList.length - 1;
 369     int diff = maxUpperBound - actualListLength;
 370     StringBuilder sb = new StringBuilder();
 371     // Pad the beginning if necessary
 372     for (int i = 0; i < diff; i++) {
 373       sb.append(i);
 374     }
 375     // Then continue with the actual choice list
 376     // We don't include the '-1' at the end
 377     for (int i = 0; i < newChoiceList.length - 1; i++) {
 378       sb.append(newChoiceList[i]);
 379     }
 380     return sb.toString();
 381   }
 382
 383   private void checkAndAddBacktrackList(LinkedList<Integer[]> backtrackChoiceLists, Integer[] newChoiceList) {
 384
 385     String newChoiceListString = buildStringFromChoiceList(newChoiceList);
 386     // Add only if we haven't seen this combination before
 387     if (!backtrackSet.contains(newChoiceListString)) {
 388       backtrackSet.add(newChoiceListString);
 389       backtrackChoiceLists.addLast(newChoiceList);
 390     }
 391   }
 392
 393   private void createBacktrackChoiceList(int currentChoice, int conflictEventNumber) {
 394
 395     LinkedList<Integer[]> backtrackChoiceLists;
 396     // Create a new list of choices for backtrack based on the current choice and conflicting event number
 397     // If we have a conflict between 1 and 3, then we create the list {3, 1, 2, 4, 5} for backtrack
 398     // The backtrack point is the CG for event number 1 and the list length is one less than the original list
 399     // (originally of length 6) since we don't start from event number 0
 400     if (!isResetAfterAnalysis) {
 401       // Check if we have a list for this choice number
 402       // If not we create a new one for it
 403       if (!backtrackMap.containsKey(conflictEventNumber)) {
 404         backtrackChoiceLists = new LinkedList<>();
 405         backtrackMap.put(conflictEventNumber, backtrackChoiceLists);
 406       } else {
 407         backtrackChoiceLists = backtrackMap.get(conflictEventNumber);
 408       }
 409       int maxListLength = choiceUpperBound + 1;
 410       int listLength = maxListLength - conflictEventNumber;
 411       Integer[] newChoiceList = new Integer[listLength + 1];
 412       // Put the conflicting event numbers first and reverse the order
 413       newChoiceList[0] = choices[currentChoice];
 414       newChoiceList[1] = choices[conflictEventNumber];
 415       // Put the rest of the event numbers into the array starting from the minimum to the upper bound
 416       for (int i = conflictEventNumber + 1, j = 2; j < listLength; i++) {
 417         if (choices[i] != choices[currentChoice]) {
 418           newChoiceList[j] = choices[i];
 419           j++;
 420         }
 421       }
 422       // Set the last element to '-1' as the end of the sequence
 423       newChoiceList[newChoiceList.length - 1] = -1;
 424       checkAndAddBacktrackList(backtrackChoiceLists, newChoiceList);
 425       // The start index for the recursion is always 1 (from the main branch)
 426     } else { // This is a sub-graph
 427       // There is a case/bug that after a re-initialization, currCG is not yet initialized
 428       if (currCG != null) {
 429         int backtrackListIndex = cgMap.get(currCG);
 430         backtrackChoiceLists = backtrackMap.get(backtrackListIndex);
 431         int listLength = choices.length;
 432         Integer[] newChoiceList = new Integer[listLength];
 433         // Copy everything before the conflict number
 434         for (int i = 0; i < conflictEventNumber; i++) {
 435           newChoiceList[i] = choices[i];
 436         }
 437         // Put the conflicting events
 438         newChoiceList[conflictEventNumber] = choices[currentChoice];
 439         newChoiceList[conflictEventNumber + 1] = choices[conflictEventNumber];
 440         // Copy the rest
 441         for (int i = conflictEventNumber + 1, j = conflictEventNumber + 2; j < listLength - 1; i++) {
 442           if (choices[i] != choices[currentChoice]) {
 443             newChoiceList[j] = choices[i];
 444             j++;
 445           }
 446         }
 447         // Set the last element to '-1' as the end of the sequence
 448         newChoiceList[newChoiceList.length - 1] = -1;
 449         checkAndAddBacktrackList(backtrackChoiceLists, newChoiceList);
 450       }
 451     }
 452   }
 453
 454   // We exclude fields that come from libraries (Java and Groovy), and also the infrastructure
 455   private final static String[] EXCLUDED_FIELDS_STARTS_WITH_LIST =
 456           // Java and Groovy libraries
 457           { "java", "org", "sun", "com", "gov", "groovy"};
 458   private final static String[] EXCLUDED_FIELDS_ENDS_WITH_LIST =
 459           // Groovy library created fields
 460           {"stMC", "callSiteArray", "metaClass", "staticClassInfo", "__constructor__",
 461                   // Infrastructure
 462                   "sendEvent", "Object", "reference", "location", "app", "state", "log", "functionList", "objectList",
 463                   "eventList", "valueList", "settings", "printToConsole", "app1", "app2"};
 464   private final static String[] EXCLUDED_FIELDS_CONTAINS_LIST = {"_closure"};
 465   private final static String[] EXCLUDED_FIELDS_WRITE_INSTRUCTIONS_STARTS_WITH_LIST = {"Event"};
 466
 467   private boolean isFieldExcluded(String field) {
 468     // Check against "starts-with" list
 469     for(String str : EXCLUDED_FIELDS_STARTS_WITH_LIST) {
 470       if (field.startsWith(str)) {
 471         return true;
 472       }
 473     }
 474     // Check against "ends-with" list
 475     for(String str : EXCLUDED_FIELDS_ENDS_WITH_LIST) {
 476       if (field.endsWith(str)) {
 477         return true;
 478       }
 479     }
 480     // Check against "contains" list
 481     for(String str : EXCLUDED_FIELDS_CONTAINS_LIST) {
 482       if (field.contains(str)) {
 483         return true;
 484       }
 485     }
 486
 487     return false;
 488   }
 489
 490   @Override
 491   public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
 492     if (stateReductionMode) {
 493       if (isInitialized) {
 494         if (choiceCounter > choices.length - 1) {
 495           // We do not compute the conflicts for the choice '-1'
 496           return;
 497         }
 498         int currentChoice = choiceCounter - 1;
 499         // Record accesses from executed instructions
 500         if (executedInsn instanceof JVMFieldInstruction) {
 501           // Analyze only after being initialized
 502           String fieldClass = ((JVMFieldInstruction) executedInsn).getFieldInfo().getFullName();
 503           // We don't care about libraries
 504           if (!isFieldExcluded(fieldClass)) {
 505             analyzeReadWriteAccesses(executedInsn, fieldClass, currentChoice);
 506           }
 507         }
 508         // Analyze conflicts from next instructions
 509         if (nextInsn instanceof JVMFieldInstruction) {
 510           // The constructor is only called once when the object is initialized
 511           // It does not have shared access with other objects
 512           MethodInfo mi = nextInsn.getMethodInfo();
 513           if (!mi.getName().equals("<init>")) {
 514             String fieldClass = ((JVMFieldInstruction) nextInsn).getFieldInfo().getFullName();
 515             // We don't care about libraries
 516             if (!isFieldExcluded(fieldClass)) {
 517               // For the main graph we go down to 0, but for subgraph, we only go down to 1 since 0 contains
 518               // the reversed event
 519 //              int end = !isResetAfterAnalysis ? 0 : choiceListStartIndexMap.get(choices);
 520               // Check for conflict (go backward from currentChoice and get the first conflict)
 521               // If the current event has conflicts with multiple events, then these will be detected
 522               // one by one as this recursively checks backward when backtrack set is revisited and executed.
 523 //              for (int eventNumber = currentChoice - 1; eventNumber >= end; eventNumber--) {
 524               for (int eventNumber = currentChoice - 1; eventNumber >= 0; eventNumber--) {
 525                 // Skip if this event number does not have any Read/Write set
 526                 if (!readWriteFieldsMap.containsKey(choices[eventNumber])) {
 527                   continue;
 528                 }
 529                 ReadWriteSet rwSet = readWriteFieldsMap.get(choices[eventNumber]);
 530                 int currObjId = ((JVMFieldInstruction) nextInsn).getFieldInfo().getClassInfo().getClassObjectRef();
 531                 // 1) Check for conflicts with Write fields for both Read and Write instructions
 532                 if (((nextInsn instanceof WriteInstruction || nextInsn instanceof ReadInstruction) &&
 533                         rwSet.writeFieldExists(fieldClass) && rwSet.writeFieldObjectId(fieldClass) == currObjId) ||
 534                         (nextInsn instanceof WriteInstruction && rwSet.readFieldExists(fieldClass) &&
 535                                 rwSet.readFieldObjectId(fieldClass) == currObjId)) {
 536                   // We do not record and service the same backtrack pair/point twice!
 537                   // If it has been serviced before, we just skip this
 538                   if (recordConflictPair(currentChoice, eventNumber)) {
 539                     createBacktrackChoiceList(currentChoice, eventNumber);
 540                     // Break if a conflict is found!
 541                     break;
 542                   }
 543                 }
 544               }
 545             }
 546           }
 547         }
 548       }
 549     }
 550   }
 551 }