Mercurial > hg > Members > kono > jpf-core

comparison src/main/gov/nasa/jpf/listener/VarTracker.java @ 0:61d41facf527

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