Mercurial > hg > Members > kono > jpf-core
view src/main/gov/nasa/jpf/listener/VarTracker.java @ 0:61d41facf527
initial v8 import (history reset)
author | Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> |
---|---|
date | Fri, 23 Jan 2015 10:14:01 -0800 |
parents | |
children | 3517702bd768 |
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.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 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 GETFIELD) || (executedInsn instanceof GETSTATIC))) && ((JVMFieldInstruction)executedInsn).isReferenceField()) || (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); } } } // 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) 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 StackFrame frame = ti.getTopFrame(); String attr = frame.getOperandAttr(1, String.class); if (attr != null) { varId = attr + "[]"; } else { varId = "?[]"; } } else { varId = ((LocalVariableInstruction)executedInsn).getVariableId(); } if (isMethodRelevant(executedInsn.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; } }