src/main/gov/nasa/jpf/listener/VarTracker.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.ALOAD;
  24 import gov.nasa.jpf.jvm.bytecode.ArrayStoreInstruction;
  25 import gov.nasa.jpf.jvm.bytecode.JVMFieldInstruction;
  26 import gov.nasa.jpf.jvm.bytecode.GETFIELD;
  27 import gov.nasa.jpf.jvm.bytecode.GETSTATIC;
  28 import gov.nasa.jpf.vm.bytecode.ReadInstruction;
  29 import gov.nasa.jpf.vm.bytecode.StoreInstruction;
  30 import gov.nasa.jpf.vm.bytecode.LocalVariableInstruction;
  31 import gov.nasa.jpf.report.ConsolePublisher;
  32 import gov.nasa.jpf.report.Publisher;
  33 import gov.nasa.jpf.search.Search;
  34 import gov.nasa.jpf.util.MethodSpec;
  35 import gov.nasa.jpf.util.StringSetMatcher;
  36 import gov.nasa.jpf.vm.ElementInfo;
  37 import gov.nasa.jpf.vm.Instruction;
  38 import gov.nasa.jpf.vm.MJIEnv;
  39 import gov.nasa.jpf.vm.VM;
  40 import gov.nasa.jpf.vm.MethodInfo;
  41 import gov.nasa.jpf.vm.StackFrame;
  42 import gov.nasa.jpf.vm.ThreadInfo;
  43 import gov.nasa.jpf.vm.bytecode.WriteInstruction;
  44
  45 import java.io.PrintWriter;
  46 import java.util.ArrayList;
  47 import java.util.Collection;
  48 import java.util.Collections;
  49 import java.util.HashMap;
  50 import java.util.Iterator;
  51 import java.util.List;
  52
  53
  54 /**
  55  * simple listener tool to find out which variables (locals and fields) are
  56  * changed how often and from where. This should give a good idea if a state
  57  * space blows up because of some counter/timer vars, and where to apply the
  58  * necessary abstractions to close/shrink it
  59  *
  60  */
  61 public class VarTracker extends ListenerAdapter {
  62
  63   // our matchers to determine which variables we have to report
  64   StringSetMatcher includeVars = null; //  means all
  65   StringSetMatcher excludeVars = null; //  means none
  66
  67   // filter methods from which access happens
  68   MethodSpec methodSpec;
  69
  70   int maxVars; // maximum number of variables shown
  71
  72   ArrayList<VarChange> queue = new ArrayList<VarChange>();
  73   ThreadInfo lastThread;
  74   HashMap<String, VarStat> stat = new HashMap<String, VarStat>();
  75   int nStates = 0;
  76   int maxDepth;
  77
  78
  79   public VarTracker (Config config, JPF jpf){
  80
  81     includeVars = StringSetMatcher.getNonEmpty(config.getStringArray("vt.include"));
  82     excludeVars = StringSetMatcher.getNonEmpty(config.getStringArray("vt.exclude",
  83             new String[] {"java.*", "javax.*"} ));
  84
  85     maxVars = config.getInt("vt.max_vars", 25);
  86
  87     methodSpec = MethodSpec.createMethodSpec(config.getString("vt.methods", "!java.*.*"));
  88
  89     jpf.addPublisherExtension(ConsolePublisher.class, this);
  90   }
  91
  92   @Override
  93   public void publishPropertyViolation (Publisher publisher) {
  94     PrintWriter pw = publisher.getOut();
  95     publisher.publishTopicStart("field access ");
  96
  97     report(pw);
  98   }
  99
 100   void print (PrintWriter pw, int n, int length) {
 101     String s = Integer.toString(n);
 102     int l = length - s.length();
 103
 104     for (int i=0; i<l; i++) {
 105       pw.print(' ');
 106     }
 107
 108     pw.print(s);
 109   }
 110
 111   void report (PrintWriter pw) {
 112     pw.println();
 113     pw.println("      change    variable");
 114     pw.println("---------------------------------------");
 115
 116     Collection<VarStat> values = stat.values();
 117     List<VarStat> valueList = new ArrayList<VarStat>();
 118     valueList.addAll(values);
 119     Collections.sort(valueList);
 120
 121     int n = 0;
 122     for (VarStat s : valueList) {
 123
 124       if (n++ > maxVars) {
 125         break;
 126       }
 127
 128       print(pw, s.nChanges, 12);
 129       pw.print("    ");
 130       pw.println(s.id);
 131     }
 132   }
 133
 134   @Override
 135   public void stateAdvanced(Search search) {
 136
 137     if (search.isNewState()) { // don't count twice
 138       int stateId = search.getStateId();
 139       nStates++;
 140       int depth = search.getDepth();
 141       if (depth > maxDepth) maxDepth = depth;
 142
 143       if (!queue.isEmpty()) {
 144         for (Iterator<VarChange> it = queue.iterator(); it.hasNext(); ){
 145           VarChange change = it.next();
 146             String id = change.getVariableId();
 147             VarStat s = stat.get(id);
 148             if (s == null) {
 149               s = new VarStat(id, stateId);
 150               stat.put(id, s);
 151             } else {
 152               // no good - we should filter during reg (think of large vectors or loop indices)
 153               if (s.lastState != stateId) { // count only once per new state
 154                 s.nChanges++;
 155                 s.lastState = stateId;
 156               }
 157             }
 158         }
 159       }
 160     }
 161
 162     queue.clear();
 163   }
 164
 165   // <2do> - general purpose listeners should not use types such as String for storing
 166   // attributes, there is no good way to make sure you retrieve your own attributes
 167   @Override
 168   public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
 169     String varId;
 170
 171     if (executedInsn instanceof ALOAD) {
 172       // a little extra work - we need to keep track of variable names, because
 173       // we cannot easily retrieve them in a subsequent xASTORE, which follows
 174       // a pattern like:  ..GETFIELD.. some-stack-operations .. xASTORE
 175       StackFrame frame = ti.getTopFrame();
 176       int objRef = frame.peek();
 177       if (objRef != MJIEnv.NULL) {
 178         ElementInfo ei = ti.getElementInfo(objRef);
 179         if (ei.isArray()) {
 180           varId = ((LocalVariableInstruction) executedInsn).getVariableId();
 181
 182           // <2do> unfortunately, we can't filter here because we don't know yet
 183           // how the array ref will be used (we would only need the attr for
 184           // subsequent xASTOREs)
 185           frame = ti.getModifiableTopFrame();
 186           frame.addOperandAttr(varId);
 187         }
 188       }
 189
 190     } else if ((executedInsn instanceof ReadInstruction) && ((JVMFieldInstruction)executedInsn).isReferenceField()){
 191       varId = ((JVMFieldInstruction)executedInsn).getFieldName();
 192
 193       StackFrame frame = ti.getModifiableTopFrame();
 194       frame.addOperandAttr(varId);
 195
 196
 197     // here come the changes - note that we can't update the stats right away,
 198     // because we don't know yet if the state this leads into has already been
 199     // visited, and we want to detect only var changes that lead to *new* states
 200     // (objective is to find out why we have new states). Note that variable
 201     // changes do not necessarily contribute to the state hash (@FilterField)
 202   } else if (executedInsn instanceof StoreInstruction) {
 203       if (executedInsn instanceof ArrayStoreInstruction) {
 204         // did we have a name for the array?
 205         // stack is ".. ref idx [l]value => .."
 206         // <2do> String is not a good attribute type to retrieve
 207         Object attr = ((ArrayStoreInstruction)executedInsn).getArrayOperandAttr(ti);
 208         if (attr != null) {
 209           varId = attr + "[]";
 210         } else {
 211           varId = "?[]";
 212         }
 213       } else {
 214         varId = ((LocalVariableInstruction)executedInsn).getVariableId();
 215       }
 216       queueIfRelevant(ti, executedInsn, varId);
 217
 218     } else if (executedInsn instanceof WriteInstruction){
 219       varId = ((WriteInstruction) executedInsn).getFieldInfo().getFullName();
 220       queueIfRelevant(ti, executedInsn, varId);
 221     }
 222   }
 223
 224   void queueIfRelevant(ThreadInfo ti, Instruction insn, String varId){
 225     if (isMethodRelevant(insn.getMethodInfo()) && isVarRelevant(varId)) {
 226       queue.add(new VarChange(varId));
 227       lastThread = ti;
 228     }
 229   }
 230
 231   boolean isMethodRelevant (MethodInfo mi){
 232     return methodSpec.matches(mi);
 233   }
 234
 235   boolean isVarRelevant (String varId) {
 236     if (!StringSetMatcher.isMatch(varId, includeVars, excludeVars)){
 237       return false;
 238     }
 239
 240     // filter subsequent changes in the same transition (to avoid gazillions of
 241     // VarChanges for loop variables etc.)
 242     // <2do> this is very inefficient - improve
 243     for (int i=0; i<queue.size(); i++) {
 244       VarChange change = queue.get(i);
 245       if (change.getVariableId().equals(varId)) {
 246         return false;
 247       }
 248     }
 249
 250     return true;
 251   }
 252 }
 253
 254 // <2do> expand into types to record value ranges
 255 class VarStat implements Comparable<VarStat> {
 256   String id;               // class[@objRef].field || class[@objref].method.local
 257   int nChanges;
 258
 259   int lastState;           // this was changed in (<2do> don't think we need this)
 260
 261   // might have more info in the future, e.g. total number of changes vs.
 262   // number of states incl. this var change, source locations, threads etc.
 263
 264   VarStat (String varId, int stateId) {
 265     id = varId;
 266     nChanges = 1;
 267
 268     lastState = stateId;
 269   }
 270
 271   int getChangeCount () {
 272     return nChanges;
 273   }
 274
 275   @Override
 276   public int compareTo (VarStat other) {
 277     if (other.nChanges > nChanges) {
 278       return 1;
 279     } else if (other.nChanges == nChanges) {
 280       return 0;
 281     } else {
 282       return -1;
 283     }
 284   }
 285 }
 286
 287 // <2do> expand into types to record values
 288 class VarChange {
 289   String id;
 290
 291   VarChange (String varId) {
 292     id = varId;
 293   }
 294
 295   String getVariableId () {
 296     return id;
 297   }
 298 }