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.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.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   private class ReadWriteSet {
 256     private HashSet<String> readSet;
 257     private HashSet<String> writeSet;
 258
 259     public ReadWriteSet() {
 260       readSet = new HashSet<>();
 261       writeSet = new HashSet<>();
 262     }
 263
 264     public void addReadField(String field) {
 265       readSet.add(field);
 266     }
 267
 268     public void addWriteField(String field) {
 269       writeSet.add(field);
 270     }
 271
 272     public boolean readFieldExists(String field) {
 273       return readSet.contains(field);
 274     }
 275
 276     public boolean writeFieldExists(String field) {
 277       return writeSet.contains(field);
 278     }
 279   }
 280
 281   private void analyzeReadWriteAccesses(Instruction executedInsn, String fieldClass) {
 282     // Do the analysis to get Read and Write accesses to fields
 283     ReadWriteSet rwSet;
 284     // We already have an entry
 285     if (readWriteFieldsMap.containsKey(choiceCounter)) {
 286       rwSet = readWriteFieldsMap.get(choiceCounter);
 287     } else { // We need to create a new entry
 288       rwSet = new ReadWriteSet();
 289       readWriteFieldsMap.put(choiceCounter, rwSet);
 290     }
 291     // Record the field in the map
 292     if (executedInsn instanceof WriteInstruction) {
 293       rwSet.addWriteField(fieldClass);
 294     }
 295     if (executedInsn instanceof ReadInstruction) {
 296       rwSet.addReadField(fieldClass);
 297     }
 298   }
 299
 300   private boolean recordConflictPair(int currentEvent, int eventNumber) {
 301     HashSet<Integer> conflictSet;
 302     if (!conflictPairMap.containsKey(currentEvent)) {
 303       conflictSet = new HashSet<>();
 304       conflictPairMap.put(currentEvent, conflictSet);
 305     } else {
 306       conflictSet = conflictPairMap.get(currentEvent);
 307     }
 308     // If this conflict has been recorded before, we return false because
 309     // we don't want to service this backtrack point twice
 310     if (conflictSet.contains(eventNumber)) {
 311       return false;
 312     }
 313     // If it hasn't been recorded, then do otherwise
 314     conflictSet.add(eventNumber);
 315     return true;
 316   }
 317
 318   private void createBacktrackChoiceList(int currentChoice, int conflictEventNumber) {
 319
 320     int minChoice = Math.min(currentChoice, conflictEventNumber);
 321     int maxChoice = Math.max(currentChoice, conflictEventNumber);
 322     LinkedList<Integer[]> backtrackChoiceLists;
 323     // Check if we have a list for this choice number
 324     // If not we create a new one for it
 325     if (!backtrackMap.containsKey(minChoice)) {
 326       backtrackChoiceLists = new LinkedList<>();
 327       backtrackMap.put(minChoice, backtrackChoiceLists);
 328     } else {
 329       backtrackChoiceLists = backtrackMap.get(minChoice);
 330     }
 331     // TODO: The following might change depending on the POR implementation detail
 332     // Create a new list of choices for backtrack based on the current choice and conflicting event number
 333     // If we have a conflict between 1 and 3, then we create the list {3, 1, 2, 4, 5} for backtrack
 334     // The backtrack point is the CG for event number 1 and the list length is one less than the original list
 335     // (originally of length 6) since we don't start from event number 0
 336     int maxListLength = choiceUpperBound + 1;
 337     int listLength = maxListLength - minChoice;
 338     Integer[] choiceList = new Integer[listLength+1];
 339     // Put the conflicting event numbers first and reverse the order
 340     choiceList[0] = maxChoice;
 341     choiceList[1] = minChoice;
 342     // Put the rest of the event numbers into the array starting from the minimum to the upper bound
 343     for(int i = minChoice + 1, j = 2; j < listLength; i++) {
 344       if (i != maxChoice) {
 345         choiceList[j] = i;
 346         j++;
 347       }
 348     }
 349     // Set the last element to '-1' as the end of the sequence
 350     choiceList[choiceList.length - 1] = -1;
 351     backtrackChoiceLists.addLast(choiceList);
 352   }
 353
 354   @Override
 355   public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
 356     if (stateReductionMode) {
 357       // Record accesses from executed instructions
 358       if (executedInsn instanceof JVMFieldInstruction) {
 359         String fieldClass = ((JVMFieldInstruction) executedInsn).getFieldInfo().getFullName();
 360         // We don't care about libraries
 361         if (!fieldClass.startsWith("java") &&
 362             !fieldClass.startsWith("org") &&
 363             !fieldClass.startsWith("sun") &&
 364             !fieldClass.startsWith("com") &&
 365             !fieldClass.startsWith("gov") &&
 366             !fieldClass.startsWith("groovy")) {
 367           analyzeReadWriteAccesses(executedInsn, fieldClass);
 368         }
 369       }
 370       // Analyze conflicts from next instructions
 371       if (nextInsn instanceof JVMFieldInstruction) {
 372         String fieldClass = ((JVMFieldInstruction) nextInsn).getFieldInfo().getFullName();
 373         // We don't care about libraries
 374         if (!fieldClass.startsWith("java") &&
 375             !fieldClass.startsWith("org") &&
 376             !fieldClass.startsWith("sun") &&
 377             !fieldClass.startsWith("com") &&
 378             !fieldClass.startsWith("gov") &&
 379             !fieldClass.startsWith("groovy")) {
 380           // Check for conflict (go backward from currentChoice and get the first conflict)
 381           // If the current event has conflicts with multiple events, then these will be detected
 382           // one by one as this recursively checks backward when backtrack set is revisited and executed.
 383           for(int eventNumber=choiceCounter-1; eventNumber>=0; eventNumber--) {
 384             // Skip if this event number does not have any Read/Write set
 385             if (!readWriteFieldsMap.containsKey(eventNumber)) {
 386               continue;
 387             }
 388             ReadWriteSet rwSet = readWriteFieldsMap.get(eventNumber);
 389             // 1) Check for conflicts with Write fields for both Read and Write instructions
 390             // 2) Check for conflicts with Read fields for Write instructions
 391             if (((nextInsn instanceof WriteInstruction || nextInsn instanceof ReadInstruction) &&
 392                     rwSet.writeFieldExists(fieldClass)) ||
 393                     (nextInsn instanceof WriteInstruction && rwSet.readFieldExists(fieldClass)))   {
 394               // We do not record and service the same backtrack pair/point twice!
 395               // If it has been serviced before, we just skip this
 396               if (recordConflictPair(choiceCounter, eventNumber)) {
 397                 createBacktrackChoiceList(choiceCounter, eventNumber);
 398                 // Break if a conflict is found!
 399                 break;
 400               }
 401             }
 402           }
 403         }
 404       }
 405     }
 406   }
 407 }