001: //
002: // Copyright (C) 2005 United States Government as represented by the
003: // Administrator of the National Aeronautics and Space Administration
004: // (NASA). All Rights Reserved.
005: //
006: // This software is distributed under the NASA Open Source Agreement
007: // (NOSA), version 1.3. The NOSA has been approved by the Open Source
008: // Initiative. See the file NOSA-1.3-JPF at the top of the distribution
009: // directory tree for the complete NOSA document.
010: //
011: // THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
012: // KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
013: // LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
014: // SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
015: // A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
016: // THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
017: // DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
018: //
019: package gov.nasa.jpf.tools;
020:
021: import gov.nasa.jpf.Config;
022: import gov.nasa.jpf.VMListener;
023: import gov.nasa.jpf.SearchListener;
024: import gov.nasa.jpf.VM;
025: import gov.nasa.jpf.Search;
026: import gov.nasa.jpf.jvm.JVM;
027: import gov.nasa.jpf.jvm.bytecode.Instruction;
028: import gov.nasa.jpf.jvm.ThreadInfo;
029: import java.util.ArrayList;
030: import gov.nasa.jpf.jvm.bytecode.FieldInstruction;
031: import gov.nasa.jpf.jvm.ElementInfo;
032: import gov.nasa.jpf.jvm.bytecode.VariableAccessor;
033: import java.util.HashMap;
034: import java.util.Iterator;
035: import java.util.Collection;
036: import java.util.List;
037: import java.util.Collections;
038: import gov.nasa.jpf.JPF;
039: import gov.nasa.jpf.jvm.bytecode.StoreInstruction;
040: import gov.nasa.jpf.jvm.bytecode.ArrayStoreInstruction;
041: import gov.nasa.jpf.jvm.bytecode.GETFIELD;
042: import gov.nasa.jpf.jvm.bytecode.GETSTATIC;
043: import gov.nasa.jpf.jvm.DynamicArea;
044: import gov.nasa.jpf.jvm.bytecode.ALOAD;
045:
046: /**
047: * simple listener tool to find out which variables (locals and fields) are
048: * changed how often and from where. This should give a good idea if a state
049: * space blows up because of some counter/timer vars, and where to apply the
050: * necessary abstractions to close/shrink it
051: */
052: public class VarTracker implements VMListener, SearchListener {
053:
054: int changeThreshold = 1;
055: boolean filterSystemVars = false;
056: String classFilter = null;
057:
058: ArrayList queue = new ArrayList();
059: ThreadInfo lastThread;
060: HashMap stat = new HashMap();
061: int nStates = 0;
062: int maxDepth;
063:
064: void print(int n, int length) {
065: String s = Integer.toString(n);
066: int l = length - s.length();
067:
068: for (int i = 0; i < l; i++) {
069: System.out.print(' ');
070: }
071:
072: System.out.print(s);
073: }
074:
075: void report(String message) {
076: System.out.println("VarTracker results:");
077: System.out.println(" states: " + nStates);
078: System.out.println(" max depth: " + maxDepth);
079: System.out.println(" term reason: " + message);
080: System.out.println();
081: System.out.println(" minChange: "
082: + changeThreshold);
083: System.out.println(" filterSysVars: "
084: + filterSystemVars);
085:
086: if (classFilter != null) {
087: System.out.println(" classFilter: "
088: + classFilter);
089: }
090:
091: System.out.println();
092: System.out.println(" change variable");
093: System.out.println("---------------------------------------");
094:
095: Collection values = stat.values();
096: List valueList = new ArrayList();
097: valueList.addAll(values);
098: Collections.sort(valueList);
099:
100: for (Iterator it = valueList.iterator(); it.hasNext();) {
101: VarStat s = (VarStat) it.next();
102: int n = s.getChangeCount();
103:
104: if (n < changeThreshold) {
105: break;
106: }
107:
108: print(s.nChanges, 12);
109: System.out.print(" ");
110: System.out.println(s.id);
111: }
112: }
113:
114: public void stateAdvanced(Search search) {
115:
116: if (search.isNewState()) { // don't count twice
117: int stateId = search.getStateNumber();
118: nStates++;
119: int depth = search.getSearchDepth();
120: if (depth > maxDepth)
121: maxDepth = depth;
122:
123: if (!queue.isEmpty()) {
124: for (Iterator it = queue.iterator(); it.hasNext();) {
125: VarChange change = (VarChange) it.next();
126: String id = change.getVariableId();
127: VarStat s = (VarStat) stat.get(id);
128: if (s == null) {
129: s = new VarStat(id, stateId);
130: stat.put(id, s);
131: } else {
132: // no good - we should filter during reg (think of large vectors or loop indices)
133: if (s.lastState != stateId) { // count only once per new state
134: s.nChanges++;
135: s.lastState = stateId;
136: }
137: }
138: }
139: }
140: }
141:
142: queue.clear();
143: }
144:
145: public void stateBacktracked(Search search) {
146: // nothing to do
147: }
148:
149: public void stateProcessed(Search search) {
150: // nothing to do
151: }
152:
153: public void stateRestored(Search search) {
154: // TODO
155: }
156:
157: public void propertyViolated(Search search) {
158: report("property violated");
159: }
160:
161: public void searchStarted(Search search) {
162: // nothing to do
163: }
164:
165: public void searchConstraintHit(Search search) {
166: report("search constraint hit");
167:
168: System.exit(0); // just for now, quick hack
169: }
170:
171: public void searchFinished(Search search) {
172: report("search finished");
173: }
174:
175: public void instructionExecuted(VM vm) {
176: JVM jvm = (JVM) vm;
177: Instruction insn = jvm.getLastInstruction();
178: ThreadInfo ti = jvm.getLastThreadInfo();
179: String varId;
180:
181: if (((((insn instanceof GETFIELD) || (insn instanceof GETSTATIC))) && ((FieldInstruction) insn)
182: .isReferenceField())
183: || (insn instanceof ALOAD)) {
184: // a little extra work - we need to keep track of variable names, because
185: // we cannot easily retrieve them in a subsequent xASTORE, which follows
186: // a pattern like: ..GETFIELD.. some-stack-operations .. xASTORE
187: int objRef = ti.peek();
188: if (objRef != -1) {
189: ElementInfo ei = DynamicArea.getHeap().get(objRef);
190: if (ei.isArray()) {
191: varId = ((VariableAccessor) insn).getVariableId();
192:
193: // <2do> unfortunately, we can't filter here because we don't know yet
194: // how the array ref will be used (we would only need the attr for
195: // subsequent xASTOREs)
196: ti.setOperandAttr(varId);
197: }
198: }
199: }
200: // here come the changes - note that we can't update the stats right away,
201: // because we don't know yet if the state this leads into has already been
202: // visited, and we want to detect only var changes that lead to *new* states
203: // (objective is to find out why we have new states)
204: else if (insn instanceof StoreInstruction) {
205: if (insn instanceof ArrayStoreInstruction) {
206: // did we have a name for the array?
207: // stack is ".. ref idx [l]value => .."
208: Object attr = ti.getOperandAttr(-1);
209: if (attr != null) {
210: varId = attr.toString() + "[]";
211: } else {
212: varId = "?[]";
213: }
214: } else {
215: varId = ((VariableAccessor) insn).getVariableId();
216: }
217:
218: if (filterChange(varId)) {
219: queue.add(new VarChange(varId));
220: lastThread = ti;
221: }
222: }
223: }
224:
225: boolean filterChange(String varId) {
226:
227: // filter based on the field owner
228: if (filterSystemVars) {
229: if (varId.startsWith("java."))
230: return false;
231: if (varId.startsWith("javax."))
232: return false;
233: if (varId.startsWith("sun."))
234: return false;
235: }
236:
237: // yes, it's a bit simplistic for now..
238: if ((classFilter != null) && (!varId.startsWith(classFilter))) {
239: return false;
240: }
241:
242: // filter subsequent changes in the same transition (to avoid gazillions of
243: // VarChanges for loop variables etc.)
244: for (int i = 0; i < queue.size(); i++) {
245: VarChange change = (VarChange) queue.get(i);
246: if (change.getVariableId().equals(varId)) {
247: return false;
248: }
249: }
250:
251: return true;
252: }
253:
254: public void threadStarted(VM vm) {
255: // TODO
256: }
257:
258: public void threadTerminated(VM vm) {
259: // TODO
260: }
261:
262: public void classLoaded(VM vm) {
263: // TODO
264: }
265:
266: public void objectCreated(VM vm) {
267: // TODO
268: }
269:
270: public void objectReleased(VM vm) {
271: // TODO
272: }
273:
274: public void gcBegin(VM vm) {
275: // TODO
276: }
277:
278: public void gcEnd(VM vm) {
279: // TODO
280: }
281:
282: public void exceptionThrown(VM vm) {
283: // TODO
284: }
285:
286: void filterArgs(String[] args) {
287: for (int i = 0; i < args.length; i++) {
288: if (args[i].equals("-noSystemVars")) {
289: filterSystemVars = true;
290: args[i] = null;
291: } else if (args[i].equals("-minChange")) {
292: args[i++] = null;
293: if (i < args.length) {
294: changeThreshold = Integer.parseInt(args[i]);
295: args[i] = null;
296: }
297: } else if (args[i].equals("-classFilter")) {
298: args[i++] = null;
299: if (i < args.length) {
300: classFilter = args[i];
301: args[i] = null;
302: }
303: }
304: }
305: }
306:
307: static void printUsage() {
308: System.out
309: .println("VarTracker - a JPF listener tool to report how often variables changed");
310: System.out
311: .println(" at least once in every state (to detect state space holes)");
312: System.out
313: .println("usage: java gov.nasa.jpf.tools.VarTracker <jpf-options> <varTracker-options> <class>");
314: System.out
315: .println(" -noSystemVars : don't report system variable changes (java*)");
316: System.out
317: .println(" -minChange <num> : don't report variables with less than <num> changes");
318: System.out
319: .println(" -classFilter <string> : only report changes in classes starting with <string>");
320: }
321:
322: public static void main(String[] args) {
323: if (args.length == 0) {
324: printUsage();
325: return;
326: }
327:
328: VarTracker listener = new VarTracker();
329: listener.filterArgs(args);
330:
331: Config conf = JPF.createConfig(args);
332: // do own settings here
333:
334: JPF jpf = new JPF(conf);
335: jpf.addSearchListener(listener);
336: jpf.addVMListener(listener);
337:
338: jpf.run();
339: }
340: }
341:
342: // <2do> expand into types to record value ranges
343: class VarStat implements Comparable {
344: String id; // class[@objRef].field || class[@objref].method.local
345: int nChanges;
346:
347: int lastState; // this was changed in (<2do> don't think we need this)
348:
349: // might have more info in the future, e.g. total number of changes vs.
350: // number of states incl. this var change, source locations, threads etc.
351:
352: VarStat(String varId, int stateId) {
353: id = varId;
354: nChanges = 1;
355:
356: lastState = stateId;
357: }
358:
359: int getChangeCount() {
360: return nChanges;
361: }
362:
363: public int compareTo(Object o) {
364: VarStat other = (VarStat) o;
365:
366: if (other.nChanges > nChanges) {
367: return 1;
368: } else if (other.nChanges == nChanges) {
369: return 0;
370: } else {
371: return -1;
372: }
373: }
374: }
375:
376: // <2do> expand into types to record values
377: class VarChange {
378: String id;
379:
380: VarChange(String varId) {
381: id = varId;
382: }
383:
384: String getVariableId() {
385: return id;
386: }
387: }
|