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:
020: package gov.nasa.jpf.tools;
021:
022: import gov.nasa.jpf.PropertyListenerAdapter;
023: import gov.nasa.jpf.VM;
024:
025: import gov.nasa.jpf.jvm.ElementInfo;
026: import gov.nasa.jpf.Search;
027: import gov.nasa.jpf.jvm.JVM;
028: import gov.nasa.jpf.jvm.DynamicArea;
029: import gov.nasa.jpf.JPF;
030: import gov.nasa.jpf.Config;
031: import gov.nasa.jpf.jvm.ThreadInfo;
032: import gov.nasa.jpf.util.DynamicObjectArray;
033: import gov.nasa.jpf.jvm.MethodInfo;
034: import gov.nasa.jpf.util.SourceRef;
035: import gov.nasa.jpf.jvm.ClassInfo;
036:
037: import java.util.Stack;
038: import java.util.Iterator;
039: import java.util.regex.Pattern;
040:
041: /**
042: * HeapTracker - property-listener class to check heap utilization along all
043: * execution paths (e.g. to verify heap bounds)
044: */
045: public class HeapTracker extends PropertyListenerAdapter {
046:
047: class PathStat implements Cloneable {
048: int nNew = 0;
049: int nReleased = 0;
050: int heapSize = 0; // in bytes
051:
052: public Object clone() {
053: try {
054: return super .clone();
055: } catch (CloneNotSupportedException e) {
056: return null;
057: }
058: }
059: }
060:
061: PathStat stat = new PathStat();
062: Stack pathStats = new Stack();
063:
064: DynamicObjectArray loc = new DynamicObjectArray();
065:
066: int maxState;
067: int nForward;
068: int nBacktrack;
069:
070: int nElemTotal;
071: int nGcTotal;
072: int nSharedTotal;
073: int nImmutableTotal;
074:
075: int nElemMax = Integer.MIN_VALUE;
076: int nElemMin = Integer.MAX_VALUE;
077: int nElemAv;
078:
079: int pElemSharedMax = Integer.MIN_VALUE;
080: int pElemSharedMin = Integer.MAX_VALUE;
081: int pElemSharedAv;
082:
083: int pElemImmutableMax = Integer.MIN_VALUE;
084: int pElemImmutableMin = Integer.MAX_VALUE;
085: int pElemImmutableAv;
086:
087: int nReleased;
088: int nReleasedTotal;
089: int nReleasedAv;
090: int nReleasedMax = Integer.MIN_VALUE;
091: int nReleasedMin = Integer.MAX_VALUE;
092:
093: int maxPathHeap = Integer.MIN_VALUE;
094: int maxPathNew = Integer.MIN_VALUE;
095: int maxPathReleased = Integer.MIN_VALUE;
096: int maxPathAlive = Integer.MIN_VALUE;
097:
098: int initHeap = 0;
099: int initNew = 0;
100: int initReleased = 0;
101: int initAlive = 0;
102:
103: // used as a property check
104: int maxHeapSizeLimit;
105: int maxLiveLimit;
106: boolean throwOutOfMemory = false;
107: Pattern classPattern = null;
108:
109: void updateMaxPathValues() {
110: if (stat.heapSize > maxPathHeap) {
111: maxPathHeap = stat.heapSize;
112: }
113:
114: if (stat.nNew > maxPathNew) {
115: maxPathNew = stat.nNew;
116: }
117:
118: if (stat.nReleased > maxPathReleased) {
119: maxPathReleased = stat.nReleased;
120: }
121:
122: int nAlive = stat.nNew - stat.nReleased;
123: if (nAlive > maxPathAlive) {
124: maxPathAlive = nAlive;
125: }
126: }
127:
128: public HeapTracker(Config config) {
129: maxHeapSizeLimit = config.getInt("heap.size_limit", -1);
130: maxLiveLimit = config.getInt("heap.live_limit", -1);
131: throwOutOfMemory = config.getBoolean("heap.throw_exception");
132:
133: String regEx = config.getString("heap.classes");
134: if (regEx != null) {
135: classPattern = Pattern.compile(regEx);
136: }
137: }
138:
139: /******************************************* abstract Property *****/
140:
141: /**
142: * return 'false' if property is violated
143: */
144: public boolean check(VM vm, Object arg) {
145: if (throwOutOfMemory) {
146: // in this case we don't want to stop the program, but see if it
147: // behaves gracefully - don't report a property violation
148: return true;
149: } else {
150: if ((maxHeapSizeLimit >= 0)
151: && (stat.heapSize > maxHeapSizeLimit)) {
152: return false;
153: }
154: if ((maxLiveLimit >= 0)
155: && ((stat.nNew - stat.nReleased) > maxLiveLimit)) {
156: return false;
157: }
158:
159: return true;
160: }
161: }
162:
163: public String getErrorMessage() {
164: return "heap limit exceeded: " + stat.heapSize + " > "
165: + maxHeapSizeLimit;
166: }
167:
168: /******************************************* SearchListener interface *****/
169: public void searchStarted(Search search) {
170: super .searchStarted(search);
171:
172: updateMaxPathValues();
173: pathStats.push(stat);
174:
175: initHeap = stat.heapSize;
176: initNew = stat.nNew;
177: initReleased = stat.nReleased;
178: initAlive = initNew - initReleased;
179:
180: stat = (PathStat) stat.clone();
181: }
182:
183: public void stateAdvanced(Search search) {
184:
185: if (search.isNewState()) {
186: int id = search.getStateNumber();
187:
188: if (id > maxState)
189: maxState = id;
190:
191: updateMaxPathValues();
192: pathStats.push(stat);
193: stat = (PathStat) stat.clone();
194:
195: nForward++;
196: }
197: }
198:
199: public void stateBacktracked(Search search) {
200: nBacktrack++;
201:
202: if (!pathStats.isEmpty()) {
203: stat = (PathStat) pathStats.pop();
204: }
205: }
206:
207: public void searchFinished(Search search) {
208: System.out.println("heap statistics:");
209: System.out.println(" states: " + maxState);
210: System.out.println(" forwards: " + nForward);
211: System.out.println(" backtrack: " + nBacktrack);
212: System.out.println();
213: System.out.println(" gc cycles: " + nGcTotal);
214: System.out.println();
215: System.out.println(" max Objects: " + nElemMax);
216: System.out.println(" min Objects: " + nElemMin);
217: System.out.println(" avg Objects: " + nElemAv);
218: System.out.println();
219: System.out.println(" max% shared: " + pElemSharedMax);
220: System.out.println(" min% shared: " + pElemSharedMin);
221: System.out.println(" avg% shared: " + pElemSharedAv);
222: System.out.println();
223: System.out.println(" max% immutable: " + pElemImmutableMax);
224: System.out.println(" min% immutable: " + pElemImmutableMin);
225: System.out.println(" avg% immutable: " + pElemImmutableAv);
226: System.out.println();
227: System.out.println(" max released: " + nReleasedMax);
228: System.out.println(" min released: " + nReleasedMin);
229: System.out.println(" avg released: " + nReleasedAv);
230:
231: System.out.println();
232: System.out.print(" max path heap (B): " + maxPathHeap);
233: System.out.println(" / " + (maxPathHeap - initHeap));
234: System.out.print(" max path alive: " + maxPathAlive);
235: System.out.println(" / " + (maxPathAlive - initAlive));
236: System.out.print(" max path new: " + maxPathNew);
237: System.out.println(" / " + (maxPathNew - initNew));
238: System.out.print(" max path released: " + maxPathReleased);
239: System.out.println(" / " + (maxPathReleased - initReleased));
240: }
241:
242: /******************************************* VMListener interface *********/
243: public void gcBegin(VM vm) {
244: JVM jvm = (JVM) vm;
245: /**
246: System.out.println();
247: System.out.println( "----- gc cycle: " + jvm.getDynamicArea().getGcNumber()
248: + ", state: " + jvm.getStateId());
249: **/
250: }
251:
252: public void gcEnd(VM vm) {
253: JVM jvm = (JVM) vm;
254: DynamicArea da = jvm.getDynamicArea();
255: Iterator it = da.iterator();
256:
257: int n = 0;
258: int nShared = 0;
259: int nImmutable = 0;
260:
261: while (it.hasNext()) {
262: ElementInfo ei = (ElementInfo) it.next();
263: n++;
264:
265: if (ei.isShared())
266: nShared++;
267: if (ei.isImmutable())
268: nImmutable++;
269:
270: //printElementInfo(ei);
271: }
272:
273: nElemTotal += n;
274: nGcTotal++;
275:
276: if (n > nElemMax)
277: nElemMax = n;
278: if (n < nElemMin)
279: nElemMin = n;
280:
281: int pShared = (nShared * 100) / n;
282: int pImmutable = (nImmutable * 100) / n;
283:
284: if (pShared > pElemSharedMax)
285: pElemSharedMax = pShared;
286: if (pShared < pElemSharedMin)
287: pElemSharedMin = pShared;
288:
289: nSharedTotal += nShared;
290: nImmutableTotal += nImmutable;
291:
292: pElemSharedAv = (nSharedTotal * 100) / nElemTotal;
293: pElemImmutableAv = (nImmutableTotal * 100) / nElemTotal;
294:
295: if (pImmutable > pElemImmutableMax)
296: pElemImmutableMax = pImmutable;
297: if (pImmutable < pElemImmutableMin)
298: pElemImmutableMin = pImmutable;
299:
300: nElemAv = nElemTotal / nGcTotal;
301: nReleasedAv = nReleasedTotal / nGcTotal;
302:
303: if (nReleased > nReleasedMax)
304: nReleasedMax = nReleased;
305: if (nReleased < nReleasedMin)
306: nReleasedMin = nReleased;
307:
308: nReleased = 0;
309: }
310:
311: boolean isRelevantType(ElementInfo ei) {
312: if (classPattern == null)
313: return true;
314:
315: return classPattern.matcher(ei.getClassInfo().getName())
316: .matches();
317: }
318:
319: public void objectCreated(VM vm) {
320: JVM jvm = (JVM) vm;
321: ElementInfo ei = jvm.getLastElementInfo();
322: int idx = ei.getIndex();
323: ThreadInfo ti = jvm.getLastThreadInfo();
324: int line = ti.getLine();
325: MethodInfo mi = ti.getMethod();
326: SourceRef sr = null;
327:
328: if (!isRelevantType(ei)) {
329: return;
330: }
331:
332: if (mi != null) {
333: String file = mi.getClassInfo().getSourceFileName();
334:
335: if (file != null) {
336: sr = new SourceRef(file, line);
337: } else {
338: ClassInfo ci = ti.getMethod().getClassInfo();
339: sr = new SourceRef(ci.getName(), line);
340: }
341: }
342:
343: loc.set(idx, sr);
344:
345: stat.nNew++;
346: stat.heapSize += ei.getHeapSize();
347:
348: // check if we should simulate an OutOfMemoryError
349: if (throwOutOfMemory) {
350: if (((maxHeapSizeLimit >= 0) && (stat.heapSize > maxHeapSizeLimit))
351: || ((maxLiveLimit >= 0) && ((stat.nNew - stat.nReleased) > maxLiveLimit))) {
352: DynamicArea.getHeap().setOutOfMemory(true);
353: }
354: }
355: }
356:
357: public void objectReleased(VM vm) {
358: JVM jvm = (JVM) vm;
359: ElementInfo ei = jvm.getLastElementInfo();
360:
361: if (!isRelevantType(ei)) {
362: return;
363: }
364:
365: nReleasedTotal++;
366: nReleased++;
367:
368: stat.nReleased++;
369: stat.heapSize -= ei.getHeapSize();
370: }
371:
372: /****************************************** private stuff ******/
373: private void printElementInfo(ElementInfo ei) {
374: boolean first = false;
375: ;
376:
377: System.out.print(ei.getIndex());
378: System.out.print(": ");
379: System.out.print(ei.getClassInfo().getName());
380: System.out.print(" [");
381:
382: if (ei.isShared()) {
383: System.out.print("shared");
384: first = false;
385: }
386: if (ei.isImmutable()) {
387: if (!first)
388: System.out.print(' ');
389: System.out.print("immutable");
390: }
391: System.out.print("] ");
392:
393: SourceRef sr = (SourceRef) loc.get(ei.getIndex());
394: if (sr != null) {
395: System.out.println(sr);
396: } else {
397: System.out.println("?");
398: }
399: }
400:
401: static void printUsage() {
402: System.out
403: .println("HeapTracker - a JPF listener tool to report and check heap utilization");
404: System.out
405: .println("usage: java gov.nasa.jpf.tools.HeapTracker <jpf-options> <heapTracker-options> <class>");
406: System.out
407: .println(" +heap.size_limit=<num> : report property violation if heap exceeds <num> bytes");
408: System.out
409: .println(" +heap.live_limit=<num> : report property violation if more than <num> live objects");
410: System.out
411: .println(" +heap.classes=<regEx> : only report instances of classes matching <regEx>");
412: System.out
413: .println(" +heap.throw_exception=<bool>: throw a OutOfMemoryError instead of reporting property violation");
414: }
415:
416: public static void main(String[] args) {
417: if (args.length == 0) {
418: printUsage();
419: return;
420: }
421: Config conf = JPF.createConfig(args);
422: // set own options here..
423:
424: HeapTracker listener = new HeapTracker(conf);
425:
426: JPF jpf = new JPF(conf);
427: jpf.addSearchListener(listener);
428: jpf.addVMListener(listener);
429:
430: if (listener.maxHeapSizeLimit >= 0) {
431: jpf.addSearchProperty(listener);
432: }
433:
434: jpf.run();
435: }
436: }
|