Mercurial > hg > Members > kono > jpf-core
view src/main/gov/nasa/jpf/listener/VarTracker.java @ 25:3517702bd768
added class name to warning for ambiguous native methods (without MJI signatures)
fixed VarTracker, which was utterly unaware of new instruction type hierarchy.
added JVMArrayElementInstruction.get{Array/Index}Attr(ti) since listeners most
likely use attrs which otherwise would have to be retrieved/cached in
executeInstruction() notifications (e.g. variable name for array)
fixed ReadInstruction, which somehow extended StoreInstruction
author | Peter Mehlitz <pcmehlitz@gmail.com> |
---|---|
date | Wed, 22 Apr 2015 15:54:26 -0700 |
parents | 61d41facf527 |
children |
line wrap: on
line source
/* * Copyright (C) 2014, United States Government, as represented by the * Administrator of the National Aeronautics and Space Administration. * All rights reserved. * * The Java Pathfinder core (jpf-core) platform is licensed under the * Apache License, Version 2.0 (the "License"); you may not use this file except * in compliance with the License. You may obtain a copy of the License at * * http://www.apache.org/licenses/LICENSE-2.0. * * Unless required by applicable law or agreed to in writing, software * distributed under the License is distributed on an "AS IS" BASIS, * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. * See the License for the specific language governing permissions and * limitations under the License. */ package gov.nasa.jpf.listener; import gov.nasa.jpf.Config; import gov.nasa.jpf.JPF; import gov.nasa.jpf.ListenerAdapter; import gov.nasa.jpf.jvm.bytecode.ALOAD; import gov.nasa.jpf.jvm.bytecode.ArrayStoreInstruction; import gov.nasa.jpf.jvm.bytecode.JVMFieldInstruction; import gov.nasa.jpf.jvm.bytecode.GETFIELD; import gov.nasa.jpf.jvm.bytecode.GETSTATIC; import gov.nasa.jpf.vm.bytecode.ReadInstruction; import gov.nasa.jpf.vm.bytecode.StoreInstruction; import gov.nasa.jpf.vm.bytecode.LocalVariableInstruction; import gov.nasa.jpf.report.ConsolePublisher; import gov.nasa.jpf.report.Publisher; import gov.nasa.jpf.search.Search; import gov.nasa.jpf.util.MethodSpec; import gov.nasa.jpf.util.StringSetMatcher; import gov.nasa.jpf.vm.ElementInfo; import gov.nasa.jpf.vm.Instruction; import gov.nasa.jpf.vm.MJIEnv; import gov.nasa.jpf.vm.VM; import gov.nasa.jpf.vm.MethodInfo; import gov.nasa.jpf.vm.StackFrame; import gov.nasa.jpf.vm.ThreadInfo; import gov.nasa.jpf.vm.bytecode.WriteInstruction; import java.io.PrintWriter; import java.util.ArrayList; import java.util.Collection; import java.util.Collections; import java.util.HashMap; import java.util.Iterator; import java.util.List; /** * simple listener tool to find out which variables (locals and fields) are * changed how often and from where. This should give a good idea if a state * space blows up because of some counter/timer vars, and where to apply the * necessary abstractions to close/shrink it * */ public class VarTracker extends ListenerAdapter { // our matchers to determine which variables we have to report StringSetMatcher includeVars = null; // means all StringSetMatcher excludeVars = null; // means none // filter methods from which access happens MethodSpec methodSpec; int maxVars; // maximum number of variables shown ArrayList<VarChange> queue = new ArrayList<VarChange>(); ThreadInfo lastThread; HashMap<String, VarStat> stat = new HashMap<String, VarStat>(); int nStates = 0; int maxDepth; public VarTracker (Config config, JPF jpf){ includeVars = StringSetMatcher.getNonEmpty(config.getStringArray("vt.include")); excludeVars = StringSetMatcher.getNonEmpty(config.getStringArray("vt.exclude", new String[] {"java.*", "javax.*"} )); maxVars = config.getInt("vt.max_vars", 25); methodSpec = MethodSpec.createMethodSpec(config.getString("vt.methods", "!java.*.*")); jpf.addPublisherExtension(ConsolePublisher.class, this); } @Override public void publishPropertyViolation (Publisher publisher) { PrintWriter pw = publisher.getOut(); publisher.publishTopicStart("field access "); report(pw); } void print (PrintWriter pw, int n, int length) { String s = Integer.toString(n); int l = length - s.length(); for (int i=0; i<l; i++) { pw.print(' '); } pw.print(s); } void report (PrintWriter pw) { pw.println(); pw.println(" change variable"); pw.println("---------------------------------------"); Collection<VarStat> values = stat.values(); List<VarStat> valueList = new ArrayList<VarStat>(); valueList.addAll(values); Collections.sort(valueList); int n = 0; for (VarStat s : valueList) { if (n++ > maxVars) { break; } print(pw, s.nChanges, 12); pw.print(" "); pw.println(s.id); } } @Override public void stateAdvanced(Search search) { if (search.isNewState()) { // don't count twice int stateId = search.getStateId(); nStates++; int depth = search.getDepth(); if (depth > maxDepth) maxDepth = depth; if (!queue.isEmpty()) { for (Iterator<VarChange> it = queue.iterator(); it.hasNext(); ){ VarChange change = it.next(); String id = change.getVariableId(); VarStat s = stat.get(id); if (s == null) { s = new VarStat(id, stateId); stat.put(id, s); } else { // no good - we should filter during reg (think of large vectors or loop indices) if (s.lastState != stateId) { // count only once per new state s.nChanges++; s.lastState = stateId; } } } } } queue.clear(); } // <2do> - general purpose listeners should not use types such as String for storing // attributes, there is no good way to make sure you retrieve your own attributes @Override public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) { String varId; if (executedInsn instanceof ALOAD) { // a little extra work - we need to keep track of variable names, because // we cannot easily retrieve them in a subsequent xASTORE, which follows // a pattern like: ..GETFIELD.. some-stack-operations .. xASTORE StackFrame frame = ti.getTopFrame(); int objRef = frame.peek(); if (objRef != MJIEnv.NULL) { ElementInfo ei = ti.getElementInfo(objRef); if (ei.isArray()) { varId = ((LocalVariableInstruction) executedInsn).getVariableId(); // <2do> unfortunately, we can't filter here because we don't know yet // how the array ref will be used (we would only need the attr for // subsequent xASTOREs) frame = ti.getModifiableTopFrame(); frame.addOperandAttr(varId); } } } else if ((executedInsn instanceof ReadInstruction) && ((JVMFieldInstruction)executedInsn).isReferenceField()){ varId = ((JVMFieldInstruction)executedInsn).getFieldName(); StackFrame frame = ti.getModifiableTopFrame(); frame.addOperandAttr(varId); // here come the changes - note that we can't update the stats right away, // because we don't know yet if the state this leads into has already been // visited, and we want to detect only var changes that lead to *new* states // (objective is to find out why we have new states). Note that variable // changes do not necessarily contribute to the state hash (@FilterField) } else if (executedInsn instanceof StoreInstruction) { if (executedInsn instanceof ArrayStoreInstruction) { // did we have a name for the array? // stack is ".. ref idx [l]value => .." // <2do> String is not a good attribute type to retrieve Object attr = ((ArrayStoreInstruction)executedInsn).getArrayOperandAttr(ti); if (attr != null) { varId = attr + "[]"; } else { varId = "?[]"; } } else { varId = ((LocalVariableInstruction)executedInsn).getVariableId(); } queueIfRelevant(ti, executedInsn, varId); } else if (executedInsn instanceof WriteInstruction){ varId = ((WriteInstruction) executedInsn).getFieldInfo().getFullName(); queueIfRelevant(ti, executedInsn, varId); } } void queueIfRelevant(ThreadInfo ti, Instruction insn, String varId){ if (isMethodRelevant(insn.getMethodInfo()) && isVarRelevant(varId)) { queue.add(new VarChange(varId)); lastThread = ti; } } boolean isMethodRelevant (MethodInfo mi){ return methodSpec.matches(mi); } boolean isVarRelevant (String varId) { if (!StringSetMatcher.isMatch(varId, includeVars, excludeVars)){ return false; } // filter subsequent changes in the same transition (to avoid gazillions of // VarChanges for loop variables etc.) // <2do> this is very inefficient - improve for (int i=0; i<queue.size(); i++) { VarChange change = queue.get(i); if (change.getVariableId().equals(varId)) { return false; } } return true; } } // <2do> expand into types to record value ranges class VarStat implements Comparable<VarStat> { String id; // class[@objRef].field || class[@objref].method.local int nChanges; int lastState; // this was changed in (<2do> don't think we need this) // might have more info in the future, e.g. total number of changes vs. // number of states incl. this var change, source locations, threads etc. VarStat (String varId, int stateId) { id = varId; nChanges = 1; lastState = stateId; } int getChangeCount () { return nChanges; } @Override public int compareTo (VarStat other) { if (other.nChanges > nChanges) { return 1; } else if (other.nChanges == nChanges) { return 0; } else { return -1; } } } // <2do> expand into types to record values class VarChange { String id; VarChange (String varId) { id = varId; } String getVariableId () { return id; } }