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