src/main/gov/nasa/jpf/listener/ExecTracker.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.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;
  31
  32 import java.io.PrintWriter;
  33
  34 /**
  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
  37  * 'statehBacktracked'
  38  *
  39  * NOTE - the ExecTracker is machine type agnostic
  40  */
  41
  42 public class ExecTracker extends ListenerAdapter {
  43
  44   @JPFOption(type = "Boolean", key = "et.print_insn", defaultValue = "true", comment = "print executed bytecode instructions")
  45   boolean printInsn = true;
  46
  47   @JPFOption(type = "Boolean", key = "et.print_src", defaultValue = "false", comment = "print source lines")
  48   boolean printSrc = false;
  49
  50   @JPFOption(type = "Boolean", key = "et.print_mth", defaultValue = "false", comment = "print executed method names")
  51   boolean printMth = false;
  52
  53   @JPFOption(type = "Boolean", key = "et.skip_init", defaultValue = "true", comment = "do not log execution before entering main()")
  54   boolean skipInit = false;
  55
  56   boolean showShared = false;
  57
  58   PrintWriter out;
  59   String lastLine;
  60   MethodInfo lastMi;
  61   String linePrefix;
  62
  63   boolean skip;
  64   MethodInfo miMain; // just to make init skipping more efficient
  65
  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);
  69
  70     /** @jpfoption et.print_src : boolean - print source lines (default=false). */
  71     printSrc = config.getBoolean("et.print_src", false);
  72
  73     /** @jpfoption et.print_mth : boolean - print executed method names (default=false). */
  74     printMth = config.getBoolean("et.print_mth", false);
  75
  76     /** @jpfoption et.skip_init : boolean - do not log execution before entering main() (default=true). */
  77     skipInit = config.getBoolean("et.skip_init", true);
  78
  79     showShared = config.getBoolean("et.show_shared", true);
  80
  81     if (skipInit) {
  82       skip = true;
  83     }
  84
  85     out = new PrintWriter(System.out, true);
  86   }
  87
  88   /******************************************* SearchListener interface *****/
  89
  90   @Override
  91   public void stateRestored(Search search) {
  92     int id = search.getStateId();
  93     out.println("----------------------------------- [" +
  94                        search.getDepth() + "] restored: " + id);
  95   }
  96
  97   //--- the ones we are interested in
  98   @Override
  99   public void searchStarted(Search search) {
 100     out.println("----------------------------------- search started");
 101     if (skipInit) {
 102       ThreadInfo tiCurrent = ThreadInfo.getCurrentThread();
 103       miMain = tiCurrent.getEntryMethod();
 104
 105       out.println("      [skipping static init instructions]");
 106     }
 107   }
 108
 109   @Override
 110   public void stateAdvanced(Search search) {
 111     int id = search.getStateId();
 112
 113     out.print("----------------------------------- [" +
 114                      search.getDepth() + "] forward: " + id);
 115     if (search.isNewState()) {
 116       out.print(" new");
 117     } else {
 118       out.print(" visited");
 119     }
 120
 121     if (search.isEndState()) {
 122       out.print(" end");
 123     }
 124
 125     out.println();
 126
 127     lastLine = null; // in case we report by source line
 128     lastMi = null;
 129     linePrefix = null;
 130   }
 131
 132   @Override
 133   public void stateProcessed (Search search) {
 134     int id = search.getStateId();
 135     out.println("----------------------------------- [" +
 136                        search.getDepth() + "] done: " + id);
 137   }
 138
 139   @Override
 140   public void stateBacktracked(Search search) {
 141     int id = search.getStateId();
 142
 143     lastLine = null;
 144     lastMi = null;
 145
 146     out.println("----------------------------------- [" +
 147                        search.getDepth() + "] backtrack: " + id);
 148   }
 149
 150   @Override
 151   public void searchFinished(Search search) {
 152     out.println("----------------------------------- search finished");
 153   }
 154
 155   /******************************************* VMListener interface *********/
 156
 157   @Override
 158   public void gcEnd(VM vm) {
 159     out.println("\t\t # garbage collection");
 160   }
 161
 162   //--- the ones we are interested in
 163   @Override
 164   public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
 165
 166     if (skip) {
 167       MethodInfo mi = executedInsn.getMethodInfo();
 168       if (mi == miMain) {
 169         skip = false; // start recording
 170       } else {
 171         return;  // skip
 172       }
 173     }
 174
 175     int nNoSrc = 0;
 176
 177     if (linePrefix == null) {
 178       linePrefix = Integer.toString( ti.getId()) + " : ";
 179     }
 180
 181     // that's pretty redundant to what is done in the ConsolePublisher, but we don't want
 182     // presentation functionality in Step anymore
 183     if (printSrc) {
 184       String line = executedInsn.getSourceLine();
 185       if (line != null){
 186         if (nNoSrc > 0) {
 187           out.println("            [" + nNoSrc + " insn w/o sources]");
 188         }
 189
 190         if (!line.equals(lastLine)) {
 191           out.print("            [");
 192           out.print(executedInsn.getFileLocation());
 193           out.print("] : ");
 194           out.println(line.trim());
 195         }
 196
 197         nNoSrc = 0;
 198
 199       } else { // no source
 200         nNoSrc++;
 201       }
 202
 203       lastLine = line;
 204     }
 205
 206     if (printInsn) {
 207       if (printMth) {
 208         MethodInfo mi = executedInsn.getMethodInfo();
 209         if (mi != lastMi){
 210           ClassInfo mci = mi.getClassInfo();
 211           out.print("      ");
 212           if (mci != null) {
 213             out.print(mci.getName());
 214             out.print(".");
 215           }
 216           out.println(mi.getUniqueName());
 217           lastMi = mi;
 218         }
 219       }
 220
 221       out.print( linePrefix);
 222
 223       out.printf("[%04x]   ", executedInsn.getPosition());
 224
 225       out.println( executedInsn.toPostExecString());
 226     }
 227   }
 228
 229   @Override
 230   public void threadStarted(VM vm, ThreadInfo ti) {
 231     out.println( "\t\t # thread started: " + ti.getName() + " index: " + ti.getId());
 232   }
 233
 234   @Override
 235   public void threadTerminated(VM vm, ThreadInfo ti) {
 236     out.println( "\t\t # thread terminated: " + ti.getName() + " index: " + ti.getId());
 237   }
 238
 239   @Override
 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);
 243   }
 244
 245   @Override
 246   public void choiceGeneratorAdvanced (VM vm, ChoiceGenerator<?> currentCG) {
 247     out.println("\t\t # choice: " + currentCG);
 248
 249     //vm.dumpThreadStates();
 250   }
 251
 252   @Override
 253   public void objectExposed (VM vm, ThreadInfo currentThread, ElementInfo fieldOwnerObject, ElementInfo exposedObject) {
 254     if (showShared){
 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 ";
 262         }
 263
 264         msg += " through " + ownerStatus + fieldOwnerObject;
 265       }
 266       out.println(msg);
 267     }
 268   }
 269
 270   @Override
 271   public void objectShared (VM vm, ThreadInfo currentThread, ElementInfo sharedObject) {
 272     if (showShared){
 273       out.println("\t\t # shared " + sharedObject);
 274     }
 275   }
 276
 277
 278   /****************************************** private stuff ******/
 279
 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")) {
 284           printSrc = true;
 285           args[i] = null;
 286         }
 287       }
 288     }
 289   }
 290 }
 291