src/main/gov/nasa/jpf/listener/TraceStorer.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.jvm.bytecode.JVMInvokeInstruction;
  24 import gov.nasa.jpf.search.Search;
  25 import gov.nasa.jpf.util.StringSetMatcher;
  26 import gov.nasa.jpf.vm.Instruction;
  27 import gov.nasa.jpf.vm.VM;
  28 import gov.nasa.jpf.vm.ThreadInfo;
  29
  30 /**
  31  * tool to save traces upon various conditions like
  32  *  - property violation
  33  *  - call of a certain method
  34  *  - reaching a certain search depth
  35  *  - creating a certain thread
  36  */
  37 public class TraceStorer extends ListenerAdapter {
  38
  39   int nTrace = 1;
  40
  41   String traceFileName;
  42
  43   // do we store to the same file? (i.e. overwrite previously stored traces)
  44   // if set to 'true', store all traces (in <traceFileName>.n)
  45   boolean storeMultiple;
  46
  47   // do we want to terminate after first store, even if it's triggered by a
  48   // property violation?
  49   boolean terminateOnStore;
  50
  51   boolean storeOnConstraintHit;
  52
  53   // search depth at what we store the tace
  54   int storeDepth;
  55
  56   // calls that should trigger a store
  57   StringSetMatcher storeCalls;
  58
  59   // thread starts that should trigger a store
  60   StringSetMatcher storeThreads;
  61
  62   // do we want verbose output
  63   boolean verbose;
  64
  65   Search search;
  66   VM vm;
  67
  68   public TraceStorer (Config config, JPF jpf){
  69
  70     traceFileName = config.getString("trace.file", "trace");
  71     storeMultiple = config.getBoolean("trace.multiple", false);
  72     storeDepth = config.getInt("trace.depth", Integer.MAX_VALUE);
  73     verbose = config.getBoolean("trace.verbose", false);
  74
  75     terminateOnStore = config.getBoolean("trace.terminate", false);
  76     storeOnConstraintHit = config.getBoolean("trace.store_constraint", false);
  77
  78     storeCalls = StringSetMatcher.getNonEmpty(config.getStringArray("trace.store_calls"));
  79     storeThreads = StringSetMatcher.getNonEmpty(config.getStringArray("trace.store_threads"));
  80
  81     vm = jpf.getVM();
  82     search = jpf.getSearch();
  83   }
  84
  85   void storeTrace(String reason) {
  86     String fname = traceFileName;
  87
  88     if (storeMultiple){
  89       fname = fname  + '.' + nTrace++;
  90     }
  91
  92     vm.storeTrace(fname, reason, verbose); // <2do> maybe some comment would be in order
  93   }
  94
  95   @Override
  96   public void propertyViolated (Search search){
  97     // Ok, this is unconditional
  98     storeTrace("violated property: " + search.getLastError().getDetails());
  99
 100     // no need to terminate (and we don't want to interfere with search.multiple_errors)
 101   }
 102
 103   @Override
 104   public void stateAdvanced (Search search){
 105     if (search.getDepth() == storeDepth){
 106       storeTrace("search depth reached: " + storeDepth);
 107       checkSearchTermination();
 108     }
 109   }
 110
 111   @Override
 112   public void searchConstraintHit (Search search){
 113     if (storeOnConstraintHit){
 114       storeTrace("search constraint hit: " + search.getLastSearchConstraint());
 115     }
 116   }
 117
 118   @Override
 119   public void instructionExecuted (VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn){
 120     if (storeCalls != null){
 121       if (executedInsn instanceof JVMInvokeInstruction) {
 122         JVMInvokeInstruction iinsn = (JVMInvokeInstruction)executedInsn;
 123         String clsName = iinsn.getInvokedMethodClassName();
 124         String mthName = iinsn.getInvokedMethodName();
 125         String mn = clsName + '.' + mthName;
 126
 127         if (storeCalls.matchesAny(mn)){
 128           storeTrace("call: " + mn);
 129           checkVMTermination(ti);
 130         }
 131       }
 132     }
 133   }
 134
 135   @Override
 136   public void threadStarted(VM vm, ThreadInfo ti) {
 137     if (storeThreads != null){
 138       String tname = ti.getName();
 139       if (storeThreads.matchesAny( tname)){
 140         storeTrace("thread started: " + tname);
 141         checkVMTermination(ti);
 142       }
 143     }
 144   }
 145
 146   boolean checkVMTermination(ThreadInfo ti) {
 147     if (terminateOnStore){
 148       ti.breakTransition("storeTraceTermination");
 149       search.terminate();
 150       return true;
 151     }
 152
 153     return false;
 154   }
 155
 156   boolean checkSearchTermination() {
 157     if (terminateOnStore){
 158       search.terminate();
 159       return true;
 160     }
 161
 162     return false;
 163   }
 164 }