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.
18 package gov.nasa.jpf.listener;
20 import gov.nasa.jpf.Config;
21 import gov.nasa.jpf.ListenerAdapter;
22 import gov.nasa.jpf.annotation.JPFOption;
23 import gov.nasa.jpf.search.Search;
24 import gov.nasa.jpf.vm.ChoiceGenerator;
25 import gov.nasa.jpf.vm.ClassInfo;
26 import gov.nasa.jpf.vm.ElementInfo;
27 import gov.nasa.jpf.vm.Instruction;
28 import gov.nasa.jpf.vm.VM;
29 import gov.nasa.jpf.vm.MethodInfo;
30 import gov.nasa.jpf.vm.ThreadInfo;
32 import java.io.PrintWriter;
35 * Listener tool to monitor JPF execution. This class can be used as a drop-in replacement for JPF, which is called by
36 * ExecTracker. ExecTracker is mostly a VMListener of 'instructionExecuted' and a SearchListener of 'stateAdvanced' and
39 * NOTE - the ExecTracker is machine type agnostic
42 public class ExecTracker extends ListenerAdapter {
44 @JPFOption(type = "Boolean", key = "et.print_insn", defaultValue = "true", comment = "print executed bytecode instructions")
45 boolean printInsn = true;
47 @JPFOption(type = "Boolean", key = "et.print_src", defaultValue = "false", comment = "print source lines")
48 boolean printSrc = false;
50 @JPFOption(type = "Boolean", key = "et.print_mth", defaultValue = "false", comment = "print executed method names")
51 boolean printMth = false;
53 @JPFOption(type = "Boolean", key = "et.skip_init", defaultValue = "true", comment = "do not log execution before entering main()")
54 boolean skipInit = false;
56 boolean showShared = false;
64 MethodInfo miMain; // just to make init skipping more efficient
66 public ExecTracker (Config config) {
67 /** @jpfoption et.print_insn : boolean - print executed bytecode instructions (default=true). */
68 printInsn = config.getBoolean("et.print_insn", true);
70 /** @jpfoption et.print_src : boolean - print source lines (default=false). */
71 printSrc = config.getBoolean("et.print_src", false);
73 /** @jpfoption et.print_mth : boolean - print executed method names (default=false). */
74 printMth = config.getBoolean("et.print_mth", false);
76 /** @jpfoption et.skip_init : boolean - do not log execution before entering main() (default=true). */
77 skipInit = config.getBoolean("et.skip_init", true);
79 showShared = config.getBoolean("et.show_shared", true);
85 out = new PrintWriter(System.out, true);
88 /******************************************* SearchListener interface *****/
91 public void stateRestored(Search search) {
92 int id = search.getStateId();
93 out.println("----------------------------------- [" +
94 search.getDepth() + "] restored: " + id);
97 //--- the ones we are interested in
99 public void searchStarted(Search search) {
100 out.println("----------------------------------- search started");
102 ThreadInfo tiCurrent = ThreadInfo.getCurrentThread();
103 miMain = tiCurrent.getEntryMethod();
105 out.println(" [skipping static init instructions]");
110 public void stateAdvanced(Search search) {
111 int id = search.getStateId();
113 out.print("----------------------------------- [" +
114 search.getDepth() + "] forward: " + id);
115 if (search.isNewState()) {
118 out.print(" visited");
121 if (search.isEndState()) {
127 lastLine = null; // in case we report by source line
133 public void stateProcessed (Search search) {
134 int id = search.getStateId();
135 out.println("----------------------------------- [" +
136 search.getDepth() + "] done: " + id);
140 public void stateBacktracked(Search search) {
141 int id = search.getStateId();
146 out.println("----------------------------------- [" +
147 search.getDepth() + "] backtrack: " + id);
151 public void searchFinished(Search search) {
152 out.println("----------------------------------- search finished");
155 /******************************************* VMListener interface *********/
158 public void gcEnd(VM vm) {
159 out.println("\t\t # garbage collection");
162 //--- the ones we are interested in
164 public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
167 MethodInfo mi = executedInsn.getMethodInfo();
169 skip = false; // start recording
177 if (linePrefix == null) {
178 linePrefix = Integer.toString( ti.getId()) + " : ";
181 // that's pretty redundant to what is done in the ConsolePublisher, but we don't want
182 // presentation functionality in Step anymore
184 String line = executedInsn.getSourceLine();
187 out.println(" [" + nNoSrc + " insn w/o sources]");
190 if (!line.equals(lastLine)) {
192 out.print(executedInsn.getFileLocation());
194 out.println(line.trim());
199 } else { // no source
208 MethodInfo mi = executedInsn.getMethodInfo();
210 ClassInfo mci = mi.getClassInfo();
213 out.print(mci.getName());
216 out.println(mi.getUniqueName());
221 out.print( linePrefix);
223 out.printf("[%04x] ", executedInsn.getPosition());
225 out.println( executedInsn.toPostExecString());
230 public void threadStarted(VM vm, ThreadInfo ti) {
231 out.println( "\t\t # thread started: " + ti.getName() + " index: " + ti.getId());
235 public void threadTerminated(VM vm, ThreadInfo ti) {
236 out.println( "\t\t # thread terminated: " + ti.getName() + " index: " + ti.getId());
240 public void exceptionThrown (VM vm, ThreadInfo ti, ElementInfo ei) {
241 MethodInfo mi = ti.getTopFrameMethodInfo();
242 out.println("\t\t\t\t # exception: " + ei + " in " + mi);
246 public void choiceGeneratorAdvanced (VM vm, ChoiceGenerator<?> currentCG) {
247 out.println("\t\t # choice: " + currentCG);
249 //vm.dumpThreadStates();
253 public void objectExposed (VM vm, ThreadInfo currentThread, ElementInfo fieldOwnerObject, ElementInfo exposedObject) {
255 String msg = "\t\t # exposed " + exposedObject;
256 if (fieldOwnerObject != null){
257 String ownerStatus = "";
258 if (fieldOwnerObject.isShared()){
259 ownerStatus = "shared ";
260 } else if (fieldOwnerObject.isExposed()){
261 ownerStatus = "exposed ";
264 msg += " through " + ownerStatus + fieldOwnerObject;
271 public void objectShared (VM vm, ThreadInfo currentThread, ElementInfo sharedObject) {
273 out.println("\t\t # shared " + sharedObject);
278 /****************************************** private stuff ******/
280 void filterArgs (String[] args) {
281 for (int i=0; i<args.length; i++) {
282 if (args[i] != null) {
283 if (args[i].equals("-print-lines")) {