src/main/gov/nasa/jpf/listener/StateReducerEfficient.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 // TODO: ISSUES
  38 // TODO: This POR implementation, however, has some issues in that the DFS algorithm doesn't properly
  39 //       traverse the sub-graphs after resets (the CGs are ignored)
  40 /**
  41  * simple tool to log state changes
  42  */
  43 public class StateReducerEfficient extends ListenerAdapter {
  44
  45   // Debug info fields
  46   private boolean debugMode;
  47   private boolean stateReductionMode;
  48   private final PrintWriter out;
  49   volatile private String detail;
  50   volatile private int depth;
  51   volatile private int id;
  52   Transition transition;
  53
  54   // State reduction fields
  55   private Integer[] choices;
  56   private IntChoiceFromSet currCG;
  57   private int choiceCounter;
  58   private Integer choiceUpperBound;
  59   private boolean isInitialized;
  60   private HashMap<IntChoiceFromSet,Boolean> resetAfterAnalysisMap;
  61   private HashMap<IntChoiceFromSet,Integer[]> cgToParentChoicesMap;
  62   private HashMap<Integer[],HashMap<IntChoiceFromSet,Integer>> choicesToCGMap;
  63   private HashMap<Integer[],HashMap<Integer,LinkedList<Integer[]>>> choicesToBacktrackMap;
  64   private boolean isBooleanCGFlipped;
  65   // Record the mapping between event number and field accesses (Read and Write)
  66   private HashMap<Integer,ReadWriteSet> readWriteFieldsMap;
  67   // The following is the backtrack map (set) that stores all the backtrack information
  68   // e.g., event number 1 can have two backtrack sequences: {3,1,2,4,...} and {2,1,3,4,...}
  69   private HashMap<Integer,HashSet<Integer>> conflictPairMap;
  70
  71   public StateReducerEfficient (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     // TODO: TESTING
  85     choicesToCGMap = new HashMap<>();
  86     choicesToBacktrackMap = new HashMap<>();
  87     resetAfterAnalysisMap = new HashMap<>();
  88     resetAfterAnalysisMap.put(null, false);
  89     cgToParentChoicesMap = new HashMap<>();
  90     readWriteFieldsMap = new HashMap<>();
  91     conflictPairMap = new HashMap<>();
  92     choices = null;
  93     currCG = null;
  94     choiceCounter = 0;
  95     initializeStateReduction();
  96   }
  97
  98   private void initializeStateReduction() {
  99     choiceUpperBound = 0;
 100     isInitialized = false;
 101     readWriteFieldsMap.clear();
 102     conflictPairMap.clear();
 103   }
 104
 105   @Override
 106   public void stateRestored(Search search) {
 107     if (debugMode) {
 108       id = search.getStateId();
 109       depth = search.getDepth();
 110       transition = search.getTransition();
 111       detail = null;
 112       out.println("\n==> DEBUG: The state is restored to state with id: " + id + " -- Transition: " + transition +
 113               " and depth: " + depth + "\n");
 114     }
 115   }
 116
 117   //--- the ones we are interested in
 118   @Override
 119   public void searchStarted(Search search) {
 120     if (debugMode) {
 121       out.println("\n==> DEBUG: ----------------------------------- search started" + "\n");
 122     }
 123   }
 124
 125   // We map current child CG to parent CG
 126   private void insertCGToMap(int choice, IntChoiceFromSet childCG) {
 127     HashMap<IntChoiceFromSet,Integer> cgMap;
 128     if (choicesToCGMap.containsKey(choices)) {
 129       cgMap = choicesToCGMap.get(choices);
 130     } else {
 131       cgMap = new HashMap<>();
 132     }
 133     cgMap.put(childCG, choice);
 134     choicesToCGMap.put(choices,cgMap);
 135   }
 136
 137   @Override
 138   public void choiceGeneratorRegistered (VM vm, ChoiceGenerator<?> nextCG, ThreadInfo currentThread, Instruction executedInstruction) {
 139     if (stateReductionMode) {
 140       // Initialize with necessary information from the CG
 141       if (nextCG instanceof IntChoiceFromSet) {
 142         IntChoiceFromSet icsCG = (IntChoiceFromSet) nextCG;
 143         // Check if CG has been initialized, otherwise initialize it
 144         Integer[] cgChoices = null;
 145         if (!isInitialized) {
 146           if (currCG == null) { // Main
 147             cgChoices = icsCG.getAllChoices();
 148             // Get the upper bound from the last element of the choices
 149             choiceUpperBound = cgChoices.length - 1;
 150           } else { // Sub-graph
 151             cgChoices = choices;
 152             choiceUpperBound = cgChoices.length - 2;
 153           }
 154           isInitialized = true;
 155         }
 156         // Record the subsequent Integer CGs only until we hit the upper bound
 157         boolean isResetAfterAnalysis = resetAfterAnalysisMap.get(currCG);
 158         if (!isResetAfterAnalysis && choiceCounter <= choiceUpperBound) {
 159           // Update the choices of the first CG and add '-1'
 160           if (choices == null) {
 161             // All the choices are always the same so we only need to update it once
 162             choices = new Integer[cgChoices.length + 1];
 163             System.arraycopy(cgChoices, 0, choices, 0, cgChoices.length);
 164             choices[choices.length - 1] = -1;
 165           }
 166           icsCG.setNewValues(choices);
 167           icsCG.reset();
 168           // Advance the current Integer CG
 169           // This way we explore all the event numbers in the first pass
 170           icsCG.advance(choices[choiceCounter]);
 171           insertCGToMap(choices[choiceCounter], icsCG);
 172           choiceCounter++;
 173           cgToParentChoicesMap.put(icsCG, choices);
 174         } else {
 175           // Set done the subsequent CGs
 176           // We only need n CGs (n is event numbers)
 177           icsCG.setDone();
 178         }
 179       }
 180     }
 181   }
 182
 183   private void resetAllCGs() {
 184     HashMap<Integer,LinkedList<Integer[]>> currBacktrackMap = choicesToBacktrackMap.get(choices);
 185     if (currBacktrackMap == null) {
 186       return;
 187     }
 188     // Extract the event numbers that have backtrack lists
 189     Set<Integer> eventSet = currBacktrackMap.keySet();
 190     // Return if there is no conflict at all (highly unlikely)
 191     if (eventSet.isEmpty()) {
 192       return;
 193     }
 194     // Reset every CG with the first backtrack lists
 195     HashMap<IntChoiceFromSet,Integer> currCGMap = choicesToCGMap.get(choices);
 196     for(IntChoiceFromSet cg : currCGMap.keySet()) {
 197       int event = currCGMap.get(cg);
 198       LinkedList<Integer[]> choiceLists = currBacktrackMap.get(event);
 199       if (choiceLists != null && choiceLists.peekFirst() != null) {
 200         Integer[] choiceList = choiceLists.removeFirst();
 201         // Deploy the new choice list for this CG
 202         cg.setNewValues(choiceList);
 203         cg.reset();
 204       } else {
 205         cg.setDone();
 206       }
 207     }
 208   }
 209
 210   @Override
 211   public void choiceGeneratorAdvanced (VM vm, ChoiceGenerator<?> currentCG) {
 212
 213     if(stateReductionMode) {
 214       // Check the boolean CG and if it is flipped, we are resetting the analysis
 215       if (currentCG instanceof BooleanChoiceGenerator) {
 216         if (!isBooleanCGFlipped) {
 217           isBooleanCGFlipped = true;
 218         } else {
 219           choiceCounter = 0;
 220           initializeStateReduction();
 221         }
 222       }
 223       // Check every choice generated and make sure that all the available choices
 224       // are chosen first before repeating the same choice of value twice!
 225       if (currentCG instanceof IntChoiceFromSet) {
 226         IntChoiceFromSet icsCG = (IntChoiceFromSet) currentCG;
 227         // Update the current pointer to the current set of choices
 228         if (choices == null || choices != icsCG.getAllChoices()) {
 229           currCG = icsCG;
 230           choices = icsCG.getAllChoices();
 231           resetAfterAnalysisMap.put(icsCG, false);
 232           choiceCounter = 1;
 233           // Reset states for the sub-graph
 234           initializeStateReduction();
 235         }
 236         if (icsCG.getNextChoice() == -1) {
 237           // Get the current CG
 238           boolean isCurrResetAfterAnalysis = resetAfterAnalysisMap.get(currCG);
 239           // Update and reset the CG if needed (do this for the first time after the analysis)
 240           if (!isCurrResetAfterAnalysis) {
 241             resetAllCGs();
 242             resetAfterAnalysisMap.put(currCG, true);
 243           }
 244           if (!icsCG.isDone()) {
 245             // Get the CG that needs to be reset
 246             Integer[] parentChoices = cgToParentChoicesMap.get(icsCG);
 247             // Do this for every CG after finishing each backtrack list
 248             HashMap<IntChoiceFromSet, Integer> parentCGMap = choicesToCGMap.get(parentChoices);
 249             HashMap<Integer, LinkedList<Integer[]>> parentBacktrackMap = choicesToBacktrackMap.get(parentChoices);
 250             int event = parentCGMap.get(icsCG);
 251             LinkedList<Integer[]> choiceLists = parentBacktrackMap.get(event);
 252             if (choiceLists != null && choiceLists.peekFirst() != null) {
 253               Integer[] choiceList = choiceLists.removeFirst();
 254               // Deploy the new choice list for this CG
 255               icsCG.setNewValues(choiceList);
 256               icsCG.reset();
 257             } else {
 258               // Set done if this was the last backtrack list
 259               icsCG.setDone();
 260             }
 261           }
 262         }
 263       }
 264     }
 265   }
 266
 267   @Override
 268   public void stateAdvanced(Search search) {
 269     if (debugMode) {
 270       id = search.getStateId();
 271       depth = search.getDepth();
 272       transition = search.getTransition();
 273       if (search.isNewState()) {
 274         detail = "new";
 275       } else {
 276         detail = "visited";
 277       }
 278
 279       if (search.isEndState()) {
 280         out.println("\n==> DEBUG: This is the last state!\n");
 281         detail += " end";
 282       }
 283       out.println("\n==> DEBUG: The state is forwarded to state with id: " + id + " with depth: " + depth +
 284               " which is " + detail + " Transition: " + transition + "\n");
 285     }
 286   }
 287
 288   @Override
 289   public void stateBacktracked(Search search) {
 290     if (debugMode) {
 291       id = search.getStateId();
 292       depth = search.getDepth();
 293       transition = search.getTransition();
 294       detail = null;
 295
 296       out.println("\n==> DEBUG: The state is backtracked to state with id: " + id + " -- Transition: " + transition +
 297               " and depth: " + depth + "\n");
 298     }
 299   }
 300
 301   @Override
 302   public void searchFinished(Search search) {
 303     if (debugMode) {
 304       out.println("\n==> DEBUG: ----------------------------------- search finished" + "\n");
 305     }
 306   }
 307
 308   // This class compactly stores Read and Write field sets
 309   // We store the field name and its object ID
 310   // Sharing the same field means the same field name and object ID
 311   private class ReadWriteSet {
 312     private HashMap<String,Integer> readSet;
 313     private HashMap<String,Integer> writeSet;
 314
 315     public ReadWriteSet() {
 316       readSet = new HashMap<>();
 317       writeSet = new HashMap<>();
 318     }
 319
 320     public void addReadField(String field, int objectId) {
 321       readSet.put(field, objectId);
 322     }
 323
 324     public void addWriteField(String field, int objectId) {
 325       writeSet.put(field, objectId);
 326     }
 327
 328     public boolean readFieldExists(String field) {
 329       return readSet.containsKey(field);
 330     }
 331
 332     public boolean writeFieldExists(String field) {
 333       return writeSet.containsKey(field);
 334     }
 335
 336     public int readFieldObjectId(String field) {
 337       return readSet.get(field);
 338     }
 339
 340     public int writeFieldObjectId(String field) {
 341       return writeSet.get(field);
 342     }
 343   }
 344
 345   private void analyzeReadWriteAccesses(Instruction executedInsn, String fieldClass, int currentChoice) {
 346     // Do the analysis to get Read and Write accesses to fields
 347     ReadWriteSet rwSet;
 348     // We already have an entry
 349     if (readWriteFieldsMap.containsKey(choices[currentChoice])) {
 350       rwSet = readWriteFieldsMap.get(choices[currentChoice]);
 351     } else { // We need to create a new entry
 352       rwSet = new ReadWriteSet();
 353       readWriteFieldsMap.put(choices[currentChoice], rwSet);
 354     }
 355     int objectId = ((JVMFieldInstruction) executedInsn).getFieldInfo().getClassInfo().getClassObjectRef();
 356     // Record the field in the map
 357     if (executedInsn instanceof WriteInstruction) {
 358       // Exclude certain field writes because of infrastructure needs, e.g., Event class field writes
 359       for(String str : EXCLUDED_FIELDS_WRITE_INSTRUCTIONS_STARTS_WITH_LIST) {
 360         if (fieldClass.startsWith(str)) {
 361           return;
 362         }
 363       }
 364       rwSet.addWriteField(fieldClass, objectId);
 365     } else if (executedInsn instanceof ReadInstruction) {
 366       rwSet.addReadField(fieldClass, objectId);
 367     }
 368   }
 369
 370   private boolean recordConflictPair(int currentEvent, int eventNumber) {
 371     HashSet<Integer> conflictSet;
 372     if (!conflictPairMap.containsKey(currentEvent)) {
 373       conflictSet = new HashSet<>();
 374       conflictPairMap.put(currentEvent, conflictSet);
 375     } else {
 376       conflictSet = conflictPairMap.get(currentEvent);
 377     }
 378     // If this conflict has been recorded before, we return false because
 379     // we don't want to service this backtrack point twice
 380     if (conflictSet.contains(eventNumber)) {
 381       return false;
 382     }
 383     // If it hasn't been recorded, then do otherwise
 384     conflictSet.add(eventNumber);
 385     return true;
 386   }
 387
 388   private void createBacktrackChoiceList(int currentChoice, int conflictEventNumber) {
 389
 390     LinkedList<Integer[]> backtrackChoiceLists;
 391     // Create a new list of choices for backtrack based on the current choice and conflicting event number
 392     // If we have a conflict between 1 and 3, then we create the list {3, 1, 2, 4, 5} for backtrack
 393     // The backtrack point is the CG for event number 1 and the list length is one less than the original list
 394     // (originally of length 6) since we don't start from event number 0
 395     boolean isResetAfterAnalysis = resetAfterAnalysisMap.get(currCG);
 396     if (!isResetAfterAnalysis) {
 397       HashMap<Integer,LinkedList<Integer[]>> currBacktrackMap;
 398       if (!choicesToBacktrackMap.containsKey(choices)) {
 399         currBacktrackMap = new HashMap<>();
 400         choicesToBacktrackMap.put(choices, currBacktrackMap);
 401       } else {
 402         currBacktrackMap = choicesToBacktrackMap.get(choices);
 403       }
 404       // Check if we have a list for this choice number
 405       // If not we create a new one for it
 406       if (!currBacktrackMap.containsKey(conflictEventNumber)) {
 407         backtrackChoiceLists = new LinkedList<>();
 408         currBacktrackMap.put(conflictEventNumber, backtrackChoiceLists);
 409       } else {
 410         backtrackChoiceLists = currBacktrackMap.get(conflictEventNumber);
 411       }
 412       int maxListLength = choiceUpperBound + 1;
 413       int listLength = maxListLength - conflictEventNumber;
 414       Integer[] newChoiceList = new Integer[listLength + 1];
 415       // Put the conflicting event numbers first and reverse the order
 416       newChoiceList[0] = choices[currentChoice];
 417       newChoiceList[1] = choices[conflictEventNumber];
 418       // Put the rest of the event numbers into the array starting from the minimum to the upper bound
 419       for (int i = conflictEventNumber + 1, j = 2; j < listLength; i++) {
 420         if (choices[i] != choices[currentChoice]) {
 421           newChoiceList[j] = choices[i];
 422           j++;
 423         }
 424       }
 425       // Set the last element to '-1' as the end of the sequence
 426       newChoiceList[newChoiceList.length - 1] = -1;
 427       backtrackChoiceLists.addLast(newChoiceList);
 428     }
 429   }
 430
 431   // We exclude fields that come from libraries (Java and Groovy), and also the infrastructure
 432   private final static String[] EXCLUDED_FIELDS_STARTS_WITH_LIST =
 433           // Java and Groovy libraries
 434           { "java", "org", "sun", "com", "gov", "groovy"};
 435   private final static String[] EXCLUDED_FIELDS_ENDS_WITH_LIST =
 436           // Groovy library created fields
 437           {"stMC", "callSiteArray", "metaClass", "staticClassInfo", "__constructor__",
 438                   // Infrastructure
 439                   "sendEvent", "Object", "reference", "location", "app", "state", "log", "functionList", "objectList",
 440                   "eventList", "valueList", "settings", "printToConsole", "app1", "app2"};
 441   private final static String[] EXCLUDED_FIELDS_CONTAINS_LIST = {"_closure"};
 442   private final static String[] EXCLUDED_FIELDS_WRITE_INSTRUCTIONS_STARTS_WITH_LIST = {"Event"};
 443
 444   private boolean isFieldExcluded(String field) {
 445     // Check against "starts-with" list
 446     for(String str : EXCLUDED_FIELDS_STARTS_WITH_LIST) {
 447       if (field.startsWith(str)) {
 448         return true;
 449       }
 450     }
 451     // Check against "ends-with" list
 452     for(String str : EXCLUDED_FIELDS_ENDS_WITH_LIST) {
 453       if (field.endsWith(str)) {
 454         return true;
 455       }
 456     }
 457     // Check against "contains" list
 458     for(String str : EXCLUDED_FIELDS_CONTAINS_LIST) {
 459       if (field.contains(str)) {
 460         return true;
 461       }
 462     }
 463
 464     return false;
 465   }
 466
 467   @Override
 468   public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
 469     if (stateReductionMode) {
 470       if (isInitialized) {
 471         if (choiceCounter > choices.length - 1) {
 472           // We do not compute the conflicts for the choice '-1'
 473           return;
 474         }
 475         int currentChoice = choiceCounter - 1;
 476         // Record accesses from executed instructions
 477         if (executedInsn instanceof JVMFieldInstruction) {
 478           // Analyze only after being initialized
 479           String fieldClass = ((JVMFieldInstruction) executedInsn).getFieldInfo().getFullName();
 480           // We don't care about libraries
 481           if (!isFieldExcluded(fieldClass)) {
 482             analyzeReadWriteAccesses(executedInsn, fieldClass, currentChoice);
 483           }
 484         }
 485         // Analyze conflicts from next instructions
 486         if (nextInsn instanceof JVMFieldInstruction) {
 487           // The constructor is only called once when the object is initialized
 488           // It does not have shared access with other objects
 489           MethodInfo mi = nextInsn.getMethodInfo();
 490           if (!mi.getName().equals("<init>")) {
 491             String fieldClass = ((JVMFieldInstruction) nextInsn).getFieldInfo().getFullName();
 492             // We don't care about libraries
 493             if (!isFieldExcluded(fieldClass)) {
 494               // For the main graph we go down to 0, but for subgraph, we only go down to 1 since 0 contains
 495               // the reversed event
 496               // If null then it is the main graph, if not it is a sub-graph
 497               int end = currCG == null ? 0 : 1;
 498               // Check for conflict (go backward from currentChoice and get the first conflict)
 499               // If the current event has conflicts with multiple events, then these will be detected
 500               // one by one as this recursively checks backward when backtrack set is revisited and executed.
 501               for (int eventNumber = currentChoice - 1; eventNumber >= end; eventNumber--) {
 502                 // Skip if this event number does not have any Read/Write set
 503                 if (!readWriteFieldsMap.containsKey(choices[eventNumber])) {
 504                   continue;
 505                 }
 506                 ReadWriteSet rwSet = readWriteFieldsMap.get(choices[eventNumber]);
 507                 int currObjId = ((JVMFieldInstruction) nextInsn).getFieldInfo().getClassInfo().getClassObjectRef();
 508                 // 1) Check for conflicts with Write fields for both Read and Write instructions
 509                 // 2) Check for conflicts with Read fields for Write instructions
 510                 if (((nextInsn instanceof WriteInstruction || nextInsn instanceof ReadInstruction) &&
 511                         rwSet.writeFieldExists(fieldClass) && rwSet.writeFieldObjectId(fieldClass) == currObjId) ||
 512                         (nextInsn instanceof WriteInstruction && rwSet.readFieldExists(fieldClass) &&
 513                                 rwSet.readFieldObjectId(fieldClass) == currObjId)) {
 514                   // We do not record and service the same backtrack pair/point twice!
 515                   // If it has been serviced before, we just skip this
 516                   if (recordConflictPair(currentChoice, eventNumber)) {
 517                     createBacktrackChoiceList(currentChoice, eventNumber);
 518                     // Break if a conflict is found!
 519                     break;
 520                   }
 521                 }
 522               }
 523             }
 524           }
 525         }
 526       }
 527     }
 528   }
 529 }