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.LocalVariableInstruction;
  27 import gov.nasa.jpf.vm.bytecode.ReadInstruction;
  28 import gov.nasa.jpf.vm.bytecode.StoreInstruction;
  29 import gov.nasa.jpf.vm.bytecode.WriteInstruction;
  30 import gov.nasa.jpf.vm.choice.IntIntervalGenerator;
  31
  32 import java.io.PrintWriter;
  33
  34 import java.util.*;
  35
  36 // TODO: Fix for Groovy's model-checking
  37 // TODO: This is a listener created to detect device conflicts and global variable conflicts
  38 /**
  39  * Simple listener tool to track remove unwanted ChoiceGenerators that are registered
  40  * while an existing ChoiceGenerator is being explored. Multiple ChoiceGenerators of the same
  41  * type could be registered spuriously during a while(true) loop.
  42  */
  43 public class StateReducer extends ListenerAdapter {
  44
  45   private boolean debugMode;
  46   private boolean stateReductionMode;
  47   private final PrintWriter out;
  48   private String detail;
  49   private int depth;
  50   private int id;
  51   private Transition transition;
  52
  53   // Holds values that have appeared during CG advances
  54   private HashSet<Integer> cgChoiceSet;
  55   private Integer choiceUpperBound;
  56   private boolean isInitialized;
  57
  58   public StateReducer (Config config, JPF jpf) {
  59     debugMode = config.getBoolean("debug_state_transition", false);
  60     stateReductionMode = config.getBoolean("activate_state_reduction", true);
  61     if (debugMode) {
  62       out = new PrintWriter(System.out, true);
  63     } else {
  64       out = null;
  65     }
  66     detail = null;
  67     depth = 0;
  68     id = 0;
  69     transition = null;
  70     cgChoiceSet = new HashSet<>();
  71     choiceUpperBound = 0;
  72     isInitialized = false;
  73   }
  74
  75   @Override
  76   public void stateRestored(Search search) {
  77     if (debugMode) {
  78       id = search.getStateId();
  79       depth = search.getDepth();
  80       transition = search.getTransition();
  81       detail = null;
  82       out.println("\n==> DEBUG: The state is restored to state with id: " + id + " -- Transition: " + transition +
  83               " and depth: " + depth + "\n");
  84     }
  85   }
  86
  87   //--- the ones we are interested in
  88   @Override
  89   public void searchStarted(Search search) {
  90     if (debugMode) {
  91       out.println("\n==> DEBUG: ----------------------------------- search started" + "\n");
  92     }
  93   }
  94
  95   @Override
  96   public void choiceGeneratorSet (VM vm, ChoiceGenerator<?> newCG) {
  97     if (stateReductionMode) {
  98       // Initialize with necessary information from the CG
  99       if (newCG instanceof IntIntervalGenerator) {
 100         IntIntervalGenerator iigCG = (IntIntervalGenerator) newCG;
 101         // Check if CG has been initialized, otherwise initialize it
 102         if (!isInitialized) {
 103           Integer[] choices = iigCG.getChoices();
 104           // Get the upper bound from the last element of the choices
 105           choiceUpperBound = choices[choices.length - 1];
 106           isInitialized = true;
 107         } else {
 108           newCG.setDone();
 109         }
 110       }
 111     }
 112   }
 113
 114   @Override
 115   public void choiceGeneratorAdvanced (VM vm, ChoiceGenerator<?> currentCG) {
 116     if (stateReductionMode) {
 117       // Check every choice generated and make sure that all the available choices
 118       // are chosen first before repeating the same choice of value twice!
 119       if (currentCG instanceof IntIntervalGenerator) {
 120         IntIntervalGenerator iigCG = (IntIntervalGenerator) currentCG;
 121         Integer nextChoice = iigCG.getNextChoice();
 122         if (!cgChoiceSet.contains(nextChoice)) {
 123           cgChoiceSet.add(nextChoice);
 124         }
 125         // Allow reinitialization after an upper bound is hit
 126         // This means all available choices have been explored once during this iteration
 127         if (cgChoiceSet.contains(choiceUpperBound)) {
 128           isInitialized = false;
 129           cgChoiceSet.clear();
 130         }
 131       }
 132     }
 133   }
 134
 135   @Override
 136   public void stateAdvanced(Search search) {
 137     if (debugMode) {
 138       id = search.getStateId();
 139       depth = search.getDepth();
 140       transition = search.getTransition();
 141       if (search.isNewState()) {
 142         detail = "new";
 143       } else {
 144         detail = "visited";
 145       }
 146
 147       if (search.isEndState()) {
 148         out.println("\n==> DEBUG: This is the last state!\n");
 149         detail += " end";
 150       }
 151       out.println("\n==> DEBUG: The state is forwarded to state with id: " + id + " with depth: " + depth +
 152               " which is " + detail + " Transition: " + transition + "\n");
 153     }
 154   }
 155
 156   @Override
 157   public void stateBacktracked(Search search) {
 158     if (debugMode) {
 159       id = search.getStateId();
 160       depth = search.getDepth();
 161       transition = search.getTransition();
 162       detail = null;
 163
 164       out.println("\n==> DEBUG: The state is backtracked to state with id: " + id + " -- Transition: " + transition +
 165               " and depth: " + depth + "\n");
 166     }
 167   }
 168
 169   @Override
 170   public void searchFinished(Search search) {
 171     if (debugMode) {
 172       out.println("\n==> DEBUG: ----------------------------------- search finished" + "\n");
 173     }
 174   }
 175 }