2 * Copyright (C) 2014, United States Government, as represented by the
3 * Administrator of the National Aeronautics and Space Administration.
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
10 * http://www.apache.org/licenses/LICENSE-2.0.
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.
19 package gov.nasa.jpf.listener;
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;
35 import java.util.Random;
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
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")
57 public class ChoiceSelector extends ListenerAdapter {
60 boolean singleChoice = true;
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;;
66 StringSetMatcher calls; // .. when any of the methods is called
67 boolean callSeen = true;
69 int startDepth; // .. when reaching this depth
70 boolean depthReached = true;
72 // set if we replay a trace
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
78 boolean searchAfterTrace;
81 public ChoiceSelector (Config config, JPF jpf) {
82 random = new Random( config.getInt("choice.seed", 42));
84 threadSet = StringSetMatcher.getNonEmpty(config.getStringArray("choice.threads"));
85 if (threadSet != null) {
89 calls = StringSetMatcher.getNonEmpty(config.getStringArray("choice.calls"));
92 startDepth = config.getInt("choice.depth", -1);
93 if (startDepth != -1) {
97 // if nothing was specified, we just do single choice (simulation)
98 if ((threadSet == null) && (calls == null) && (startDepth == -1)) {
101 depthReached = false;
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);
110 void checkSingleChoiceCond() {
111 singleChoice = !(depthReached && callSeen && threadsAlive);
115 public void choiceGeneratorAdvanced (VM vm, ChoiceGenerator<?> currentCG) {
116 int n = currentCG.getTotalNumberOfChoices();
118 if (trace != null) { // this is a replay
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();
125 int choiceIndex = trace.getChoiceIndex();
126 currentCG.select(choiceIndex);
131 int r = random.nextInt(n);
132 currentCG.select(r); // sets it done, so we never backtrack into it
139 public void threadStarted(VM vm, ThreadInfo ti) {
140 if (singleChoice && (threadSet != null)) {
141 String tname = ti.getName();
142 if (threadSet.matchesAny( tname)){
144 checkSingleChoiceCond();
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();
155 if (calls.matchesAny(mthName)){
157 checkSingleChoiceCond();
164 public void stateAdvanced(Search search) {
167 // there is no backtracking or restoring as long as we replay
168 trace = trace.getNext();
171 search.getVM().setTraceReplay(false);
172 if (searchAfterTrace){
173 singleChoice = false;
178 if (singleChoice && !depthReached && (startDepth >= 0)) {
179 if (search.getDepth() == startDepth) {
181 checkSingleChoiceCond();