src/main/gov/nasa/jpf/listener/ObjectTracker.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.jvm.bytecode.PUTFIELD;
  25 import gov.nasa.jpf.report.ConsolePublisher;
  26 import gov.nasa.jpf.report.Publisher;
  27 import gov.nasa.jpf.util.IntSet;
  28 import gov.nasa.jpf.util.SortedArrayIntSet;
  29 import gov.nasa.jpf.util.StateExtensionClient;
  30 import gov.nasa.jpf.util.StateExtensionListener;
  31 import gov.nasa.jpf.util.StringSetMatcher;
  32 import gov.nasa.jpf.vm.ClassInfo;
  33 import gov.nasa.jpf.vm.ElementInfo;
  34 import gov.nasa.jpf.vm.Instruction;
  35 import gov.nasa.jpf.vm.StackFrame;
  36 import gov.nasa.jpf.vm.VM;
  37 import gov.nasa.jpf.vm.ThreadInfo;
  38 import gov.nasa.jpf.vm.Types;
  39 import gov.nasa.jpf.vm.bytecode.FieldInstruction;
  40 import gov.nasa.jpf.vm.bytecode.InstanceFieldInstruction;
  41 import gov.nasa.jpf.vm.bytecode.InstanceInvokeInstruction;
  42 import gov.nasa.jpf.vm.bytecode.InvokeInstruction;
  43 import java.io.PrintWriter;
  44 import java.util.ArrayList;
  45 import java.util.Collections;
  46 import java.util.List;
  47
  48
  49 /**
  50  * listener that keeps track of all operations on objects that are specified by
  51  * reference value or types
  52  */
  53 public class ObjectTracker extends ListenerAdapter implements StateExtensionClient {
  54
  55   static class Attr {
  56     // nothing here, just a tag
  57   }
  58
  59   static final Attr ATTR = new Attr(); // we need only one
  60
  61   enum OpType { NEW, CALL, PUT, GET, FREE };
  62
  63   static class LogRecord {
  64     ElementInfo ei;
  65     ThreadInfo ti;
  66     Instruction insn;
  67     OpType opType;
  68     int stateId;
  69
  70     LogRecord prev;
  71
  72     LogRecord (OpType opType, ElementInfo ei, ThreadInfo ti, Instruction insn, LogRecord prev){
  73       this.opType = opType;
  74       this.ei = ei;
  75       this.ti = ti;
  76       this.insn = insn;
  77       this.prev = prev;
  78       this.stateId = ti.getVM().getStateId();
  79     }
  80
  81     void printOn (PrintWriter pw){
  82       if (prev != null && stateId != prev.stateId){
  83         pw.printf("----------------------------------- [%d]\n", prev.stateId + 1);
  84       }
  85
  86       pw.print(ti.getId());
  87       pw.print(": ");
  88
  89       pw.printf("%-4s ", opType.toString().toLowerCase());
  90       pw.print(ei);
  91       pw.print('.');
  92
  93       if (insn != null){
  94         if (insn instanceof FieldInstruction){
  95           FieldInstruction finsn = (FieldInstruction)insn;
  96
  97           String fname = finsn.getFieldName();
  98           pw.print(fname);
  99
 100         } else if (insn instanceof InvokeInstruction){
 101           InvokeInstruction call = (InvokeInstruction)insn;
 102
 103           String mthName = call.getInvokedMethodName();
 104
 105           pw.print( Types.getDequalifiedMethodSignature(mthName));
 106         }
 107       }
 108
 109       pw.println();
 110     }
 111   }
 112
 113   protected LogRecord log; // needs to be state restored
 114
 115   //--- log options
 116   protected StringSetMatcher includeClasses, excludeClasses; // type name patterns
 117   protected IntSet trackedRefs;
 118
 119   protected boolean logFieldAccess;
 120   protected boolean logCalls;
 121
 122
 123
 124   //--- internal stuff
 125
 126   public ObjectTracker (Config conf, JPF jpf) {
 127     includeClasses = StringSetMatcher.getNonEmpty(conf.getStringArray("ot.include"));
 128     excludeClasses = StringSetMatcher.getNonEmpty(conf.getStringArray("ot.exclude", new String[] { "*" }));
 129
 130     trackedRefs = new SortedArrayIntSet();
 131
 132     int[] refs = conf.getIntArray("ot.refs");
 133     if (refs != null){
 134       for (int i=0; i<refs.length; i++){
 135         trackedRefs.add(refs[i]);
 136       }
 137     }
 138
 139     logCalls = conf.getBoolean("ot.log_calls", true);
 140     logFieldAccess = conf.getBoolean("ot.log_fields", true);
 141
 142     registerListener(jpf);
 143     jpf.addPublisherExtension(ConsolePublisher.class, this);
 144   }
 145
 146   protected void log (OpType opType, ElementInfo ei, ThreadInfo ti, Instruction insn){
 147     log = new LogRecord( opType, ei, ti, insn,  log);
 148   }
 149
 150
 151   //--- Listener interface
 152
 153   @Override
 154   public void classLoaded (VM vm, ClassInfo ci){
 155     if (StringSetMatcher.isMatch(ci.getName(), includeClasses, excludeClasses)){
 156       ci.addAttr(ATTR);
 157     }
 158   }
 159
 160   @Override
 161   public void objectCreated (VM vm, ThreadInfo ti, ElementInfo ei) {
 162     ClassInfo ci = ei.getClassInfo();
 163     int ref = ei.getObjectRef();
 164
 165     if (ci.hasAttr(Attr.class) || trackedRefs.contains(ref)){
 166       // it's new, we don't need to call getModifiable
 167       ei.addObjectAttr(ATTR);
 168       log( OpType.NEW, ei, ti, ti.getPC());
 169     }
 170   }
 171
 172   @Override
 173   public void objectReleased (VM vm, ThreadInfo ti, ElementInfo ei) {
 174     if (ei.hasObjectAttr(Attr.class)){
 175       log( OpType.FREE, ei, ti, ti.getPC());
 176     }
 177   }
 178
 179   @Override
 180   public void instructionExecuted (VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn){
 181
 182     if (logCalls && executedInsn instanceof InstanceInvokeInstruction){
 183       if (nextInsn != executedInsn){ // otherwise we didn't enter
 184         InstanceInvokeInstruction call = (InstanceInvokeInstruction)executedInsn;
 185
 186         int ref = call.getCalleeThis(ti);
 187         ElementInfo ei = ti.getElementInfo(ref);
 188
 189         if (ei.hasObjectAttr(Attr.class)) {
 190           log( OpType.CALL, ei, ti, executedInsn);
 191         }
 192       }
 193
 194     } else if (logFieldAccess && executedInsn instanceof InstanceFieldInstruction){
 195       if (nextInsn != executedInsn){ // otherwise we didn't enter
 196         InstanceFieldInstruction finsn = (InstanceFieldInstruction) executedInsn;
 197
 198         StackFrame frame = ti.getTopFrame();
 199         int idx = finsn.getObjectSlot(frame);
 200         int ref = frame.getSlot(idx);
 201         ElementInfo ei = ti.getElementInfo(ref);
 202
 203         if (ei.hasObjectAttr(Attr.class)) {
 204           OpType op = (executedInsn instanceof PUTFIELD) ? OpType.PUT : OpType.GET;
 205           log( op, ei, ti, executedInsn);
 206         }
 207       }
 208     }
 209   }
 210
 211   //--- state store/restore
 212
 213   @Override
 214   public Object getStateExtension () {
 215     return log;
 216   }
 217
 218   @Override
 219   public void restore (Object stateExtension) {
 220     log = (LogRecord)stateExtension;
 221   }
 222
 223   @Override
 224   public void registerListener (JPF jpf) {
 225     StateExtensionListener<Number> sel = new StateExtensionListener(this);
 226     jpf.addSearchListener(sel);
 227   }
 228
 229
 230   //--- reporting
 231
 232   @Override
 233   public void publishPropertyViolation (Publisher publisher) {
 234     if (log != null){ // otherwise we don't have anything to report
 235       PrintWriter pw = publisher.getOut();
 236       publisher.publishTopicStart("ObjectTracker " + publisher.getLastErrorId());
 237       printLogOn(pw);
 238     }
 239   }
 240
 241   protected void printLogOn (PrintWriter pw){
 242     // the log can be quite long so we can't use recursion (Java does not optimize tail recursion)
 243     List<LogRecord> logRecs = new ArrayList<LogRecord>();
 244     for (LogRecord lr = log; lr != null; lr = lr.prev){
 245       logRecs.add(lr);
 246     }
 247
 248     Collections.reverse(logRecs);
 249
 250     for (LogRecord lr : logRecs){
 251       lr.printOn(pw);
 252     }
 253   }
 254 }