src/main/gov/nasa/jpf/listener/ChoiceSelector.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
  19 package gov.nasa.jpf.listener;
  20
  21 import gov.nasa.jpf.Config;
  22 import gov.nasa.jpf.JPF;
  23 import gov.nasa.jpf.ListenerAdapter;
  24 import gov.nasa.jpf.annotation.JPFOption;
  25 import gov.nasa.jpf.annotation.JPFOptions;
  26 import gov.nasa.jpf.jvm.bytecode.JVMInvokeInstruction;
  27 import gov.nasa.jpf.search.Search;
  28 import gov.nasa.jpf.util.StringSetMatcher;
  29 import gov.nasa.jpf.vm.ChoiceGenerator;
  30 import gov.nasa.jpf.vm.ChoicePoint;
  31 import gov.nasa.jpf.vm.Instruction;
  32 import gov.nasa.jpf.vm.VM;
  33 import gov.nasa.jpf.vm.ThreadInfo;
  34
  35 import java.util.Random;
  36
  37 /**
  38  * this is a listener that only executes single choices until it detects
  39  * that it should start to search. If nothing is specified, this is pretty
  40  * much a simulator that randomly picks choices. Otherwise the user can
  41  * give it any combination of
  42  *  - a set of thread names
  43  *  - a set of method names
  44  *  - a start search depth
  45  * to turn on the search. If more than one condition is given, all have to be
  46  * satisfied
  47  */
  48
  49 @JPFOptions({
  50   @JPFOption(type = "Int", key = "choice.seed", defaultValue= "42", comment = ""),
  51   @JPFOption(type = "StringArray", key = "choice.threads", defaultValue = "", comment="start search, when all threads in the set are active"),
  52   @JPFOption(type = "StringArray", key = "choice.calls", defaultValue = "", comment = "start search, when any of the methods is called"),
  53   @JPFOption(type = "Int", key = "choice.depth", defaultValue = "-1", comment = "start search, when reaching this depth"),
  54   @JPFOption(type = "String", key = "choice.use_trace", defaultValue ="", comment = ""),
  55   @JPFOption(type = "Boolean", key = "choice.search_after_trace", defaultValue = "true", comment="start search, when reaching the end of the stored trace")
  56 })
  57 public class ChoiceSelector extends ListenerAdapter {
  58
  59   Random random;
  60   boolean singleChoice = true;
  61
  62   // those are our singleChoice end conditions (i.e. where we start the search)
  63   StringSetMatcher threadSet; // we start when all threads in the set are active
  64   boolean threadsAlive = true;;
  65
  66   StringSetMatcher calls; // .. when any of the methods is called
  67   boolean callSeen = true;
  68
  69   int startDepth; // .. when reaching this depth
  70   boolean depthReached = true;
  71
  72   // set if we replay a trace
  73   ChoicePoint trace;
  74
  75   // start the search when reaching the end of the stored trace. If not set,
  76   // the listener will just randomly select single choices once the trace
  77   // got processed
  78   boolean searchAfterTrace;
  79
  80
  81   public ChoiceSelector (Config config, JPF jpf) {
  82     random = new Random( config.getInt("choice.seed", 42));
  83
  84     threadSet = StringSetMatcher.getNonEmpty(config.getStringArray("choice.threads"));
  85     if (threadSet != null) {
  86       threadsAlive = false;
  87     }
  88
  89     calls = StringSetMatcher.getNonEmpty(config.getStringArray("choice.calls"));
  90     callSeen = false;
  91
  92     startDepth = config.getInt("choice.depth", -1);
  93     if (startDepth != -1) {
  94       depthReached = false;
  95     }
  96
  97     // if nothing was specified, we just do single choice (simulation)
  98     if ((threadSet == null) && (calls == null) && (startDepth == -1)) {
  99       threadsAlive = false;
 100       callSeen = false;
 101       depthReached = false;
 102     }
 103
 104     VM vm = jpf.getVM();
 105     trace = ChoicePoint.readTrace(config.getString("choice.use_trace"), vm.getSUTName());
 106     searchAfterTrace = config.getBoolean("choice.search_after_trace", true);
 107     vm.setTraceReplay(trace != null);
 108   }
 109
 110   void checkSingleChoiceCond() {
 111     singleChoice = !(depthReached && callSeen && threadsAlive);
 112   }
 113
 114   @Override
 115   public void choiceGeneratorAdvanced (VM vm, ChoiceGenerator<?> currentCG) {
 116     int n = currentCG.getTotalNumberOfChoices();
 117
 118     if (trace != null) { // this is a replay
 119
 120       // <2do> maybe that should just be a warning, and then a single choice
 121       assert currentCG.getClass().getName().equals(trace.getCgClassName()) :
 122         "wrong choice generator class, expecting: " + trace.getCgClassName()
 123         + ", read: " + currentCG.getClass().getName();
 124
 125       int choiceIndex = trace.getChoiceIndex();
 126       currentCG.select(choiceIndex);
 127
 128     } else {
 129       if (singleChoice) {
 130         if (n > 1) {
 131           int r = random.nextInt(n);
 132           currentCG.select(r); // sets it done, so we never backtrack into it
 133         }
 134       }
 135     }
 136   }
 137
 138   @Override
 139   public void threadStarted(VM vm, ThreadInfo ti) {
 140     if (singleChoice && (threadSet != null)) {
 141       String tname = ti.getName();
 142       if (threadSet.matchesAny( tname)){
 143         threadsAlive = true;
 144         checkSingleChoiceCond();
 145       }
 146     }
 147   }
 148
 149   @Override
 150   public void executeInstruction(VM vm, ThreadInfo ti, Instruction insnToExecute) {
 151     if (singleChoice && !callSeen && (calls != null)) {
 152       if (insnToExecute instanceof JVMInvokeInstruction) {
 153         String mthName = ((JVMInvokeInstruction)insnToExecute).getInvokedMethod(ti).getBaseName();
 154
 155         if (calls.matchesAny(mthName)){
 156           callSeen = true;
 157           checkSingleChoiceCond();
 158         }
 159       }
 160     }
 161   }
 162
 163   @Override
 164   public void stateAdvanced(Search search) {
 165
 166     if (trace != null) {
 167       // there is no backtracking or restoring as long as we replay
 168       trace = trace.getNext();
 169
 170       if (trace == null){
 171         search.getVM().setTraceReplay(false);
 172         if (searchAfterTrace){
 173           singleChoice = false;
 174         }
 175       }
 176
 177     } else {
 178       if (singleChoice && !depthReached && (startDepth >= 0)) {
 179         if (search.getDepth() == startDepth) {
 180           depthReached = true;
 181           checkSingleChoiceCond();
 182         }
 183       }
 184     }
 185   }
 186
 187 }