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.SearchListener;
023: import gov.nasa.jpf.VMListener;
024: import gov.nasa.jpf.JPF;
025: import gov.nasa.jpf.jvm.JVM;
026: import gov.nasa.jpf.Search;
027: import gov.nasa.jpf.VM;
028: import gov.nasa.jpf.jvm.bytecode.Instruction;
029: import gov.nasa.jpf.jvm.ThreadInfo;
030: import gov.nasa.jpf.jvm.Step;
031: import java.io.PrintWriter;
032: import gov.nasa.jpf.util.SourceRef;
033:
034: /**
035: * Listener tool to monitor JPF execution. This class can be used as a drop-in
036: * replacement for JPF, which is called by ExecTracker.
037: * ExecTracker is mostly a VMListener of 'instructionExecuted' and
038: * a SearchListener of 'stateAdvanced' and 'statehBacktracked'
039: */
040: public class ExecTracker implements SearchListener, VMListener {
041: /******************************************* SearchListener interface *****/
042:
043: boolean printLines = false;
044: PrintWriter pw;
045: SourceRef lastLine;
046: String linePrefix;
047:
048: public void searchConstraintHit(Search search) {
049: }
050:
051: public void stateRestored(Search search) {
052: int id = search.getStateNumber();
053: System.out.println("--- restored: " + id);
054: }
055:
056: public void propertyViolated(Search search) {
057: }
058:
059: //--- the ones we are interested in
060: public void searchStarted(Search search) {
061: System.out.println("--- search started");
062: }
063:
064: public void stateAdvanced(Search search) {
065: int id = search.getStateNumber();
066:
067: System.out.print("--- forward: " + id);
068: if (search.isNewState()) {
069: System.out.print(" new");
070: } else {
071: System.out.print(" visited");
072: }
073:
074: if (search.isEndState()) {
075: System.out.println(" end");
076: } else {
077: System.out.println();
078: }
079:
080: lastLine = null; // in case we report by source line
081: linePrefix = null;
082: }
083:
084: public void stateProcessed(Search search) {
085: int id = search.getStateNumber();
086: System.out.println("--- done: " + id);
087: }
088:
089: public void stateBacktracked(Search search) {
090: int id = search.getStateNumber();
091:
092: System.out.println("--- backtrack: " + id);
093: }
094:
095: public void searchFinished(Search search) {
096: System.out.println("--- search finished");
097: }
098:
099: /******************************************* VMListener interface *********/
100: public void exceptionThrown(VM vm) {
101: }
102:
103: public void classLoaded(VM vm) {
104: }
105:
106: public void gcBegin(VM vm) {
107: }
108:
109: public void gcEnd(VM vm) {
110: System.out.println("\t\t\t\t # GC");
111: }
112:
113: public void objectCreated(VM vm) {
114: }
115:
116: public void objectReleased(VM vm) {
117: }
118:
119: //--- the ones we are interested in
120: public void instructionExecuted(VM vm) {
121: JVM jvm = (JVM) vm;
122: ThreadInfo ti = jvm.getLastThreadInfo();
123:
124: if (linePrefix == null) {
125: linePrefix = Integer.toString(ti.getIndex()) + " : ";
126: }
127:
128: if (printLines) {
129: if (pw == null) {
130: pw = new PrintWriter(System.out);
131: }
132: if (lastLine == null) {
133: lastLine = new SourceRef();
134: }
135: Step step = jvm.getLastStep();
136: step.printStepOn(pw, lastLine, linePrefix);
137: pw.flush();
138: } else {
139: Instruction insn = jvm.getLastInstruction();
140: System.out.print(linePrefix);
141: System.out.println(insn);
142: }
143: }
144:
145: public void threadStarted(VM vm) {
146: JVM jvm = (JVM) vm;
147: ThreadInfo ti = jvm.getLastThreadInfo();
148:
149: System.out.println("\t\t\t\t # thread started: "
150: + ti.getIndex());
151: }
152:
153: public void threadTerminated(VM vm) {
154: JVM jvm = (JVM) vm;
155: ThreadInfo ti = jvm.getLastThreadInfo();
156:
157: System.out.println("\t\t\t\t # thread terminated: "
158: + ti.getIndex());
159: }
160:
161: /****************************************** private stuff ******/
162:
163: void filterArgs(String[] args) {
164: for (int i = 0; i < args.length; i++) {
165: if (args[i].equals("-print-lines")) {
166: printLines = true;
167: args[i] = null;
168: }
169: }
170: }
171:
172: public static void main(String[] args) {
173: ExecTracker listener = new ExecTracker();
174: listener.filterArgs(args); // check and remove our own args
175:
176: Config conf = JPF.createConfig(args);
177: // do special settings here
178:
179: JPF jpf = new JPF(conf);
180: jpf.addSearchListener(listener);
181: jpf.addVMListener(listener);
182:
183: jpf.run();
184: }
185: }
|