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.PropertyListenerAdapter;
23 import gov.nasa.jpf.report.ConsolePublisher;
24 import gov.nasa.jpf.report.Publisher;
25 import gov.nasa.jpf.search.Search;
26 import gov.nasa.jpf.util.DynamicObjectArray;
27 import gov.nasa.jpf.util.Misc;
28 import gov.nasa.jpf.util.SourceRef;
29 import gov.nasa.jpf.util.StringSetMatcher;
30 import gov.nasa.jpf.vm.ClassInfo;
31 import gov.nasa.jpf.vm.ElementInfo;
32 import gov.nasa.jpf.vm.Heap;
33 import gov.nasa.jpf.vm.VM;
34 import gov.nasa.jpf.vm.MethodInfo;
35 import gov.nasa.jpf.vm.ThreadInfo;
37 import java.io.PrintWriter;
38 import java.util.ArrayList;
39 import java.util.Comparator;
40 import java.util.HashMap;
42 import java.util.Stack;
45 * HeapTracker - property-listener class to check heap utilization along all
46 * execution paths (e.g. to verify heap bounds)
48 public class HeapTracker extends PropertyListenerAdapter {
50 static class PathStat implements Cloneable {
53 int heapSize = 0; // in bytes
56 public Object clone() {
59 } catch (CloneNotSupportedException e) {
65 static class TypeStat {
70 TypeStat (String typeName){
71 this.typeName = typeName;
75 PathStat stat = new PathStat();
76 Stack<PathStat> pathStats = new Stack<PathStat>();
78 DynamicObjectArray<SourceRef> loc = new DynamicObjectArray<SourceRef>();
80 HashMap<String,TypeStat> typeStat = new HashMap<String,TypeStat>();
91 int nElemMax = Integer.MIN_VALUE;
92 int nElemMin = Integer.MAX_VALUE;
95 int pElemSharedMax = Integer.MIN_VALUE;
96 int pElemSharedMin = Integer.MAX_VALUE;
99 int pElemImmutableMax = Integer.MIN_VALUE;
100 int pElemImmutableMin = Integer.MAX_VALUE;
101 int pElemImmutableAv;
106 int nReleasedMax = Integer.MIN_VALUE;
107 int nReleasedMin = Integer.MAX_VALUE;
109 int maxPathHeap = Integer.MIN_VALUE;
110 int maxPathNew = Integer.MIN_VALUE;
111 int maxPathReleased = Integer.MIN_VALUE;
112 int maxPathAlive = Integer.MIN_VALUE;
116 int initReleased = 0;
120 boolean showTypeStats;
123 // used as a property check
124 int maxHeapSizeLimit;
126 boolean throwOutOfMemory = false;
128 StringSetMatcher includes, excludes;
130 void updateMaxPathValues() {
131 if (stat.heapSize > maxPathHeap) {
132 maxPathHeap = stat.heapSize;
135 if (stat.nNew > maxPathNew) {
136 maxPathNew = stat.nNew;
139 if (stat.nReleased > maxPathReleased) {
140 maxPathReleased = stat.nReleased;
143 int nAlive = stat.nNew - stat.nReleased;
144 if (nAlive > maxPathAlive) {
145 maxPathAlive = nAlive;
149 void allocTypeStats (ElementInfo ei) {
150 String typeName = ei.getClassInfo().getName();
151 TypeStat ts = typeStat.get(typeName);
153 ts = new TypeStat(typeName);
154 typeStat.put(typeName, ts);
159 void releaseTypeStats (ElementInfo ei) {
160 String typeName = ei.getClassInfo().getName();
161 TypeStat ts = typeStat.get(typeName);
168 public HeapTracker (Config config, JPF jpf) {
169 maxHeapSizeLimit = config.getInt("heap.size_limit", -1);
170 maxLiveLimit = config.getInt("heap.live_limit", -1);
171 throwOutOfMemory = config.getBoolean("heap.throw_exception");
172 showTypeStats = config.getBoolean("heap.show_types");
173 maxTypesShown = config.getInt("heap.max_types", 20);
175 includes = StringSetMatcher.getNonEmpty(config.getStringArray("heap.include"));
176 excludes = StringSetMatcher.getNonEmpty(config.getStringArray("heap.exclude"));
178 jpf.addPublisherExtension(ConsolePublisher.class, this);
181 /******************************************* abstract Property *****/
184 * return 'false' if property is violated
187 public boolean check (Search search, VM vm) {
188 if (throwOutOfMemory) {
189 // in this case we don't want to stop the program, but see if it
190 // behaves gracefully - don't report a property violation
193 if ((maxHeapSizeLimit >= 0) && (stat.heapSize > maxHeapSizeLimit)) {
196 if ((maxLiveLimit >=0) && ((stat.nNew - stat.nReleased) > maxLiveLimit)) {
205 public String getErrorMessage () {
206 return "heap limit exceeded: " + stat.heapSize + " > " + maxHeapSizeLimit;
209 /******************************************* SearchListener interface *****/
211 public void searchStarted(Search search) {
212 super.searchStarted(search);
214 updateMaxPathValues();
215 pathStats.push(stat);
217 initHeap = stat.heapSize;
219 initReleased = stat.nReleased;
220 initAlive = initNew - initReleased;
222 stat = (PathStat)stat.clone();
226 public void stateAdvanced(Search search) {
228 if (search.isNewState()) {
229 int id = search.getStateId();
231 if (id > maxState) maxState = id;
233 updateMaxPathValues();
234 pathStats.push(stat);
235 stat = (PathStat)stat.clone();
242 public void stateBacktracked(Search search) {
245 if (!pathStats.isEmpty()){
246 stat = pathStats.pop();
250 /******************************************* PublisherExtension interface ****/
252 public void publishFinished (Publisher publisher) {
253 PrintWriter pw = publisher.getOut();
254 publisher.publishTopicStart("heap statistics");
256 pw.println("heap statistics:");
257 pw.println(" states: " + maxState);
258 pw.println(" forwards: " + nForward);
259 pw.println(" backtrack: " + nBacktrack);
261 pw.println(" gc cycles: " + nGcTotal);
263 pw.println(" max Objects: " + nElemMax);
264 pw.println(" min Objects: " + nElemMin);
265 pw.println(" avg Objects: " + nElemAv);
267 pw.println(" max% shared: " + pElemSharedMax);
268 pw.println(" min% shared: " + pElemSharedMin);
269 pw.println(" avg% shared: " + pElemSharedAv);
271 pw.println(" max% immutable: " + pElemImmutableMax);
272 pw.println(" min% immutable: " + pElemImmutableMin);
273 pw.println(" avg% immutable: " + pElemImmutableAv);
275 pw.println(" max released: " + nReleasedMax);
276 pw.println(" min released: " + nReleasedMin);
277 pw.println(" avg released: " + nReleasedAv);
280 pw.print( " max path heap (B): " + maxPathHeap);
281 pw.println(" / " + (maxPathHeap - initHeap));
282 pw.print( " max path alive: " + maxPathAlive);
283 pw.println(" / " + (maxPathAlive - initAlive));
284 pw.print( " max path new: " + maxPathNew);
285 pw.println(" / " + (maxPathNew - initNew));
286 pw.print( " max path released: " + maxPathReleased);
287 pw.println(" / " + (maxPathReleased - initReleased));
291 pw.println(" type allocation statistics:");
293 ArrayList<Map.Entry<String,TypeStat>> list =
294 Misc.createSortedEntryList(typeStat, new Comparator<Map.Entry<String,TypeStat>>() {
296 public int compare (Map.Entry<String,TypeStat> e1,
297 Map.Entry<String,TypeStat> e2) {
298 return Integer.signum(e1.getValue().nAlloc - e2.getValue().nAlloc);
302 for (Map.Entry<String,TypeStat> e : list) {
303 TypeStat ts = e.getValue();
305 pw.print(String.format("%1$9d : ", ts.nAlloc));
306 pw.println(ts.typeName);
308 if (i++ > maxTypesShown) {
317 /******************************************* VMListener interface *********/
319 public void gcBegin(VM vm) {
321 System.out.println();
322 System.out.println( "----- gc cycle: " + vm.getDynamicArea().getGcNumber()
323 + ", state: " + vm.getStateId());
328 public void gcEnd(VM vm) {
329 Heap heap = vm.getHeap();
335 for (ElementInfo ei : heap.liveObjects()) {
338 if (ei.isShared()) nShared++;
339 if (ei.isImmutable()) nImmutable++;
341 //printElementInfo(ei);
347 if (n > nElemMax) nElemMax = n;
348 if (n < nElemMin) nElemMin = n;
350 int pShared = (nShared * 100) / n;
351 int pImmutable = (nImmutable * 100) / n;
353 if (pShared > pElemSharedMax) pElemSharedMax = pShared;
354 if (pShared < pElemSharedMin) pElemSharedMin = pShared;
356 nSharedTotal += nShared;
357 nImmutableTotal += nImmutable;
359 pElemSharedAv = (nSharedTotal * 100) / nElemTotal;
360 pElemImmutableAv = (nImmutableTotal * 100) / nElemTotal;
362 if (pImmutable > pElemImmutableMax) pElemImmutableMax = pImmutable;
363 if (pImmutable < pElemImmutableMin) pElemImmutableMin = pImmutable;
365 nElemAv = nElemTotal / nGcTotal;
366 nReleasedAv = nReleasedTotal / nGcTotal;
368 if (nReleased > nReleasedMax) nReleasedMax = nReleased;
369 if (nReleased < nReleasedMin) nReleasedMin = nReleased;
374 boolean isRelevantType (ElementInfo ei) {
375 String clsName = ei.getClassInfo().getName();
376 return StringSetMatcher.isMatch(clsName, includes, excludes);
380 public void objectCreated(VM vm, ThreadInfo ti, ElementInfo ei) {
381 int idx = ei.getObjectRef();
382 int line = ti.getLine();
383 MethodInfo mi = ti.getTopFrameMethodInfo();
386 if (!isRelevantType(ei)) {
391 ClassInfo mci = mi.getClassInfo();
393 String file = mci.getSourceFileName();
395 sr = new SourceRef(file, line);
397 sr = new SourceRef(mci.getName(), line);
402 // means references with null loc are from synthetic methods
406 stat.heapSize += ei.getHeapSize();
408 // update the type statistics
414 // check if we should simulate an OutOfMemoryError
415 if (throwOutOfMemory) {
416 if (((maxHeapSizeLimit >=0) && (stat.heapSize > maxHeapSizeLimit)) ||
417 ((maxLiveLimit >=0) && ((stat.nNew - stat.nReleased) > maxLiveLimit))){
418 vm.getHeap().setOutOfMemory(true);
424 public void objectReleased(VM vm, ThreadInfo ti, ElementInfo ei) {
426 if (!isRelevantType(ei)) {
434 releaseTypeStats(ei);
438 stat.heapSize -= ei.getHeapSize();
441 /****************************************** private stuff ******/
442 protected void printElementInfo(ElementInfo ei) {
443 boolean first = false;
445 System.out.print( ei.getObjectRef());
446 System.out.print( ": ");
447 System.out.print( ei.getClassInfo().getName());
448 System.out.print( " [");
451 System.out.print( "shared");
454 if (ei.isImmutable()) {
455 if (!first) System.out.print(' ');
456 System.out.print( "immutable");
458 System.out.print( "] ");
460 SourceRef sr = loc.get(ei.getObjectRef());
462 System.out.println(sr);
464 System.out.println("?");
469 static void printUsage () {
470 System.out.println("HeapTracker - a JPF listener tool to report and check heap utilization");
471 System.out.println("usage: java gov.nasa.jpf.tools.HeapTracker <jpf-options> <heapTracker-options> <class>");
472 System.out.println(" +heap.size_limit=<num> : report property violation if heap exceeds <num> bytes");
473 System.out.println(" +heap.live_limit=<num> : report property violation if more than <num> live objects");
474 System.out.println(" +heap.classes=<regEx> : only report instances of classes matching <regEx>");
475 System.out.println(" +heap.throw_exception=<bool>: throw a OutOfMemoryError instead of reporting property violation");