KickJava   Java API By Example, From Geeks To Geeks.

Java > Open Source Codes > gov > nasa > jpf > tools > VarTracker


1 //
2
// Copyright (C) 2005 United States Government as represented by the
3
// Administrator of the National Aeronautics and Space Administration
4
// (NASA). All Rights Reserved.
5
//
6
// This software is distributed under the NASA Open Source Agreement
7
// (NOSA), version 1.3. The NOSA has been approved by the Open Source
8
// Initiative. See the file NOSA-1.3-JPF at the top of the distribution
9
// directory tree for the complete NOSA document.
10
//
11
// THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
12
// KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
13
// LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
14
// SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
15
// A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
16
// THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
17
// DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
18
//
19
package gov.nasa.jpf.tools;
20
21 import gov.nasa.jpf.Config;
22 import gov.nasa.jpf.VMListener;
23 import gov.nasa.jpf.SearchListener;
24 import gov.nasa.jpf.VM;
25 import gov.nasa.jpf.Search;
26 import gov.nasa.jpf.jvm.JVM;
27 import gov.nasa.jpf.jvm.bytecode.Instruction;
28 import gov.nasa.jpf.jvm.ThreadInfo;
29 import java.util.ArrayList JavaDoc;
30 import gov.nasa.jpf.jvm.bytecode.FieldInstruction;
31 import gov.nasa.jpf.jvm.ElementInfo;
32 import gov.nasa.jpf.jvm.bytecode.VariableAccessor;
33 import java.util.HashMap JavaDoc;
34 import java.util.Iterator JavaDoc;
35 import java.util.Collection JavaDoc;
36 import java.util.List JavaDoc;
37 import java.util.Collections JavaDoc;
38 import gov.nasa.jpf.JPF;
39 import gov.nasa.jpf.jvm.bytecode.StoreInstruction;
40 import gov.nasa.jpf.jvm.bytecode.ArrayStoreInstruction;
41 import gov.nasa.jpf.jvm.bytecode.GETFIELD;
42 import gov.nasa.jpf.jvm.bytecode.GETSTATIC;
43 import gov.nasa.jpf.jvm.DynamicArea;
44 import gov.nasa.jpf.jvm.bytecode.ALOAD;
45
46
47 /**
48  * simple listener tool to find out which variables (locals and fields) are
49  * changed how often and from where. This should give a good idea if a state
50  * space blows up because of some counter/timer vars, and where to apply the
51  * necessary abstractions to close/shrink it
52  */

53 public class VarTracker implements VMListener, SearchListener {
54   
55   int changeThreshold = 1;
56   boolean filterSystemVars = false;
57   String JavaDoc classFilter = null;
58   
59   ArrayList JavaDoc queue = new ArrayList JavaDoc();
60   ThreadInfo lastThread;
61   HashMap JavaDoc stat = new HashMap JavaDoc();
62   int nStates = 0;
63   int maxDepth;
64   
65   void print (int n, int length) {
66     String JavaDoc s = Integer.toString(n);
67     int l = length - s.length();
68     
69     for (int i=0; i<l; i++) {
70       System.out.print(' ');
71     }
72     
73     System.out.print(s);
74   }
75   
76   void report (String JavaDoc message) {
77     System.out.println("VarTracker results:");
78     System.out.println(" states: " + nStates);
79     System.out.println(" max depth: " + maxDepth);
80     System.out.println(" term reason: " + message);
81     System.out.println();
82     System.out.println(" minChange: " + changeThreshold);
83     System.out.println(" filterSysVars: " + filterSystemVars);
84     
85     if (classFilter != null) {
86       System.out.println(" classFilter: " + classFilter);
87     }
88     
89     System.out.println();
90     System.out.println(" change variable");
91     System.out.println("---------------------------------------");
92     
93     Collection JavaDoc values = stat.values();
94     List JavaDoc valueList = new ArrayList JavaDoc();
95     valueList.addAll(values);
96     Collections.sort(valueList);
97     
98     for (Iterator JavaDoc it = valueList.iterator(); it.hasNext();) {
99       VarStat s = (VarStat)it.next();
100       int n = s.getChangeCount();
101       
102       if (n < changeThreshold) {
103         break;
104       }
105       
106       print(s.nChanges, 12);
107       System.out.print(" ");
108       System.out.println(s.id);
109     }
110   }
111   
112   public void stateAdvanced(Search search) {
113     
114     if (search.isNewState()) { // don't count twice
115
int stateId = search.getStateNumber();
116       nStates++;
117       int depth = search.getSearchDepth();
118       if (depth > maxDepth) maxDepth = depth;
119       
120       if (!queue.isEmpty()) {
121         for (Iterator JavaDoc it = queue.iterator(); it.hasNext(); ){
122           VarChange change = (VarChange) it.next();
123             String JavaDoc id = change.getVariableId();
124             VarStat s = (VarStat)stat.get(id);
125             if (s == null) {
126               s = new VarStat(id, stateId);
127               stat.put(id, s);
128             } else {
129               // no good - we should filter during reg (think of large vectors or loop indices)
130
if (s.lastState != stateId) { // count only once per new state
131
s.nChanges++;
132                 s.lastState = stateId;
133               }
134             }
135         }
136       }
137     }
138
139     queue.clear();
140   }
141   
142   public void stateBacktracked(Search search) {
143     // nothing to do
144
}
145   
146   public void stateProcessed (Search search) {
147     // nothing to do
148
}
149   
150   public void stateRestored(Search search) {
151     // TODO
152
}
153   
154   public void propertyViolated(Search search) {
155     report("property violated");
156   }
157   
158   public void searchStarted(Search search) {
159     // nothing to do
160
}
161   
162   public void searchConstraintHit(Search search) {
163     report("search constraint hit");
164     
165     System.exit(0); // just for now, quick hack
166
}
167   
168   public void searchFinished(Search search) {
169     report("search finished");
170   }
171     
172   public void instructionExecuted(VM vm) {
173     JVM jvm = (JVM)vm;
174     Instruction insn = jvm.getLastInstruction();
175     ThreadInfo ti = jvm.getLastThreadInfo();
176     String JavaDoc varId;
177     
178     if ( ((((insn instanceof GETFIELD) || (insn instanceof GETSTATIC)))
179             && ((FieldInstruction)insn).isReferenceField()) ||
180          (insn instanceof ALOAD)) {
181       // a little extra work - we need to keep track of variable names, because
182
// we cannot easily retrieve them in a subsequent xASTORE, which follows
183
// a pattern like: ..GETFIELD.. some-stack-operations .. xASTORE
184
int objRef = ti.peek();
185       if (objRef != -1) {
186         ElementInfo ei = DynamicArea.getHeap().get(objRef);
187         if (ei.isArray()) {
188           varId = ((VariableAccessor)insn).getVariableId();
189           
190           // <2do> unfortunately, we can't filter here because we don't know yet
191
// how the array ref will be used (we would only need the attr for
192
// subsequent xASTOREs)
193
ti.setOperandAttr( varId);
194         }
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)
201
else if (insn instanceof StoreInstruction) {
202       if (insn instanceof ArrayStoreInstruction) {
203         // did we have a name for the array?
204
// stack is ".. ref idx [l]value => .."
205
Object JavaDoc attr = ti.getOperandAttr(-1);
206         if (attr != null) {
207           varId = attr.toString() + "[]";
208         } else {
209           varId = "?[]";
210         }
211       } else {
212         varId = ((VariableAccessor)insn).getVariableId();
213       }
214       
215       if (filterChange(varId)) {
216         queue.add(new VarChange(varId));
217         lastThread = ti;
218       }
219     }
220   }
221   
222   boolean filterChange (String JavaDoc varId) {
223     
224     // filter based on the field owner
225
if (filterSystemVars) {
226       if (varId.startsWith("java.")) return false;
227       if (varId.startsWith("javax.")) return false;
228       if (varId.startsWith("sun.")) return false;
229     }
230     
231     // yes, it's a bit simplistic for now..
232
if ((classFilter != null) && (!varId.startsWith(classFilter))) {
233       return false;
234     }
235     
236     // filter subsequent changes in the same transition (to avoid gazillions of
237
// VarChanges for loop variables etc.)
238
for (int i=0; i<queue.size(); i++) {
239       VarChange change = (VarChange) queue.get(i);
240       if (change.getVariableId().equals(varId)) {
241         return false;
242       }
243     }
244     
245     return true;
246   }
247   
248   public void threadStarted(VM vm) {
249     // TODO
250
}
251   
252   public void threadTerminated(VM vm) {
253     // TODO
254
}
255   
256   public void classLoaded(VM vm) {
257     // TODO
258
}
259   
260   public void objectCreated(VM vm) {
261     // TODO
262
}
263   
264   public void objectReleased(VM vm) {
265     // TODO
266
}
267   
268   public void gcBegin(VM vm) {
269     // TODO
270
}
271   
272   public void gcEnd(VM vm) {
273     // TODO
274
}
275   
276   public void exceptionThrown(VM vm) {
277     // TODO
278
}
279   
280   void filterArgs (String JavaDoc[] args) {
281     for (int i=0; i<args.length; i++) {
282       if (args[i].equals("-noSystemVars")) {
283         filterSystemVars = true;
284         args[i] = null;
285       } else if (args[i].equals("-minChange")) {
286         args[i++] = null;
287         if (i < args.length) {
288           changeThreshold = Integer.parseInt(args[i]);
289           args[i] = null;
290         }
291       } else if (args[i].equals("-classFilter")) {
292         args[i++] = null;
293         if (i < args.length) {
294           classFilter = args[i];
295           args[i] = null;
296         }
297       }
298     }
299   }
300   
301   static void printUsage () {
302     System.out.println("VarTracker - a JPF listener tool to report how often variables changed");
303     System.out.println(" at least once in every state (to detect state space holes)");
304     System.out.println("usage: java gov.nasa.jpf.tools.VarTracker <jpf-options> <varTracker-options> <class>");
305     System.out.println(" -noSystemVars : don't report system variable changes (java*)");
306     System.out.println(" -minChange <num> : don't report variables with less than <num> changes");
307     System.out.println(" -classFilter <string> : only report changes in classes starting with <string>");
308   }
309   
310   public static void main (String JavaDoc[] args) {
311     if (args.length == 0) {
312       printUsage();
313       return;
314     }
315     
316     VarTracker listener = new VarTracker();
317     listener.filterArgs(args);
318     
319     Config conf = JPF.createConfig(args);
320     // do own settings here
321

322     JPF jpf = new JPF(conf);
323     jpf.addSearchListener(listener);
324     jpf.addVMListener(listener);
325
326     jpf.run();
327   }
328 }
329
330 // <2do> expand into types to record value ranges
331
class VarStat implements Comparable JavaDoc {
332   String JavaDoc id; // class[@objRef].field || class[@objref].method.local
333
int nChanges;
334   
335   int lastState; // this was changed in (<2do> don't think we need this)
336

337   // might have more info in the future, e.g. total number of changes vs.
338
// number of states incl. this var change, source locations, threads etc.
339

340   VarStat (String JavaDoc varId, int stateId) {
341     id = varId;
342     nChanges = 1;
343     
344     lastState = stateId;
345   }
346   
347   int getChangeCount () {
348     return nChanges;
349   }
350   
351   public int compareTo (Object JavaDoc o) {
352     VarStat other = (VarStat) o;
353     
354     if (other.nChanges > nChanges) {
355       return 1;
356     } else if (other.nChanges == nChanges) {
357       return 0;
358     } else {
359       return -1;
360     }
361   }
362 }
363
364 // <2do> expand into types to record values
365
class VarChange {
366   String JavaDoc id;
367   
368   VarChange (String JavaDoc varId) {
369     id = varId;
370   }
371   
372   String JavaDoc getVariableId () {
373     return id;
374   }
375 }
376
Popular Tags