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.VMListener;
022: import gov.nasa.jpf.VM;
023: import gov.nasa.jpf.SearchListener;
024: import gov.nasa.jpf.jvm.JVM;
025: import gov.nasa.jpf.jvm.bytecode.Instruction;
026: import gov.nasa.jpf.Search;
027: import gov.nasa.jpf.Config;
028: import gov.nasa.jpf.JPF;
029:
030: /**
031: * simple tools to gather statistics about instructions executed by JPF.
032: * InsnCounter is mostly a VMListener that observes 'instructionExecuted'
033: */
034: public class InsnCounter implements VMListener, SearchListener {
035:
036: String[] opCodes = new String[256];
037: int[] counts = new int[256];
038: int total;
039:
040: //----------------------------------------- SearchKistener interface
041: public void searchFinished(Search search) {
042: reportStatistics();
043: }
044:
045: public void stateBacktracked(Search search) {
046: // not interested
047: }
048:
049: public void propertyViolated(Search search) {
050: // not interested
051: }
052:
053: public void searchConstraintHit(Search search) {
054: // not interested
055: }
056:
057: public void stateAdvanced(Search search) {
058: // not interested
059: }
060:
061: public void stateProcessed(Search search) {
062: // not interested
063: }
064:
065: public void searchStarted(Search search) {
066: // not interested
067: }
068:
069: public void stateRestored(Search search) {
070: // not interested
071: }
072:
073: //----------------------------------------------------- VMListener interface
074: public void instructionExecuted(VM vm) {
075: JVM jvm = (JVM) vm;
076: Instruction insn = jvm.getLastInstruction();
077: int bc = insn.getByteCode();
078:
079: if (opCodes[bc] == null) {
080: opCodes[bc] = insn.getMnemonic();
081: }
082: counts[bc]++;
083: total++;
084: }
085:
086: public void threadStarted(VM vm) {
087: // not interested
088: }
089:
090: public void threadTerminated(VM vm) {
091: // not interested
092: }
093:
094: public void objectCreated(VM vm) {
095: // not interested
096: }
097:
098: public void objectReleased(VM vm) {
099: // not interested
100: }
101:
102: public void gcBegin(VM vm) {
103: // not interested
104: }
105:
106: public void gcEnd(VM vm) {
107: // not interested
108: }
109:
110: public void classLoaded(VM vm) {
111: // not interested
112: }
113:
114: public void exceptionThrown(VM vm) {
115: // not interested
116: }
117:
118: //----------------------------------------------------- internal stuff
119: void reportStatistics() {
120: int[] sorted = getSortedCounts();
121: int i;
122:
123: for (i = 0; i < sorted.length; i++) {
124: int idx = sorted[i];
125: String opc = opCodes[idx];
126:
127: if (counts[idx] > 0) {
128: System.out.print(i);
129: System.out.print(" ");
130: System.out.print(opc);
131: System.out.print(" : ");
132: System.out.println(counts[idx]);
133: } else {
134: break;
135: }
136: }
137: }
138:
139: int[] getSortedCounts() {
140: int[] sorted = new int[256];
141: int last = -1;
142: int i, j;
143:
144: for (i = 0; i < 256; i++) {
145: int c = counts[i];
146: if (c > 0) {
147: for (j = 0; j < last; j++) {
148: if (counts[sorted[j]] < c) {
149: System.arraycopy(sorted, j, sorted, j + 1,
150: (last - j));
151: break;
152: }
153: }
154: sorted[j] = i;
155: last++;
156: }
157: }
158:
159: return sorted;
160: }
161:
162: void filterArgs(String[] args) {
163: // we don't have any yet
164: }
165:
166: public static void main(String[] args) {
167: InsnCounter listener = new InsnCounter();
168: listener.filterArgs(args);
169:
170: Config conf = JPF.createConfig(args);
171: // do own settings here
172:
173: JPF jpf = new JPF(conf);
174: jpf.addSearchListener(listener);
175: jpf.addVMListener(listener);
176:
177: jpf.run();
178: }
179: }
|