2 * Copyright (C) 2014, United States Government, as represented by the
3 * Administrator of the National Aeronautics and Space Administration.
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
10 * http://www.apache.org/licenses/LICENSE-2.0.
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.
18 package gov.nasa.jpf.listener;
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;
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;
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
61 public class VarTracker extends ListenerAdapter {
63 // our matchers to determine which variables we have to report
64 StringSetMatcher includeVars = null; // means all
65 StringSetMatcher excludeVars = null; // means none
67 // filter methods from which access happens
68 MethodSpec methodSpec;
70 int maxVars; // maximum number of variables shown
72 ArrayList<VarChange> queue = new ArrayList<VarChange>();
73 ThreadInfo lastThread;
74 HashMap<String, VarStat> stat = new HashMap<String, VarStat>();
79 public VarTracker (Config config, JPF jpf){
81 includeVars = StringSetMatcher.getNonEmpty(config.getStringArray("vt.include"));
82 excludeVars = StringSetMatcher.getNonEmpty(config.getStringArray("vt.exclude",
83 new String[] {"java.*", "javax.*"} ));
85 maxVars = config.getInt("vt.max_vars", 25);
87 methodSpec = MethodSpec.createMethodSpec(config.getString("vt.methods", "!java.*.*"));
89 jpf.addPublisherExtension(ConsolePublisher.class, this);
93 public void publishPropertyViolation (Publisher publisher) {
94 PrintWriter pw = publisher.getOut();
95 publisher.publishTopicStart("field access ");
100 void print (PrintWriter pw, int n, int length) {
101 String s = Integer.toString(n);
102 int l = length - s.length();
104 for (int i=0; i<l; i++) {
111 void report (PrintWriter pw) {
113 pw.println(" change variable");
114 pw.println("---------------------------------------");
116 Collection<VarStat> values = stat.values();
117 List<VarStat> valueList = new ArrayList<VarStat>();
118 valueList.addAll(values);
119 Collections.sort(valueList);
122 for (VarStat s : valueList) {
128 print(pw, s.nChanges, 12);
135 public void stateAdvanced(Search search) {
137 if (search.isNewState()) { // don't count twice
138 int stateId = search.getStateId();
140 int depth = search.getDepth();
141 if (depth > maxDepth) maxDepth = depth;
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);
149 s = new VarStat(id, stateId);
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
155 s.lastState = stateId;
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
168 public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
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);
180 varId = ((LocalVariableInstruction) executedInsn).getVariableId();
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);
190 } else if ((executedInsn instanceof ReadInstruction) && ((JVMFieldInstruction)executedInsn).isReferenceField()){
191 varId = ((JVMFieldInstruction)executedInsn).getFieldName();
193 StackFrame frame = ti.getModifiableTopFrame();
194 frame.addOperandAttr(varId);
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);
214 varId = ((LocalVariableInstruction)executedInsn).getVariableId();
216 queueIfRelevant(ti, executedInsn, varId);
218 } else if (executedInsn instanceof WriteInstruction){
219 varId = ((WriteInstruction) executedInsn).getFieldInfo().getFullName();
220 queueIfRelevant(ti, executedInsn, varId);
224 void queueIfRelevant(ThreadInfo ti, Instruction insn, String varId){
225 if (isMethodRelevant(insn.getMethodInfo()) && isVarRelevant(varId)) {
226 queue.add(new VarChange(varId));
231 boolean isMethodRelevant (MethodInfo mi){
232 return methodSpec.matches(mi);
235 boolean isVarRelevant (String varId) {
236 if (!StringSetMatcher.isMatch(varId, includeVars, excludeVars)){
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)) {
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
259 int lastState; // this was changed in (<2do> don't think we need this)
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.
264 VarStat (String varId, int stateId) {
271 int getChangeCount () {
276 public int compareTo (VarStat other) {
277 if (other.nChanges > nChanges) {
279 } else if (other.nChanges == nChanges) {
287 // <2do> expand into types to record values
291 VarChange (String varId) {
295 String getVariableId () {