KickJava   Java API By Example, From Geeks To Geeks.

Java > Open Source Codes > gov > nasa > jpf > tools > ExecTracker


1 //
2 // Copyright (C) 2005 United States Government as represented by the
3 // Administrator of the National Aeronautics and Space Administration
4 // (NASA). All Rights Reserved.
5 //
6 // This software is distributed under the NASA Open Source Agreement
7 // (NOSA), version 1.3. The NOSA has been approved by the Open Source
8 // Initiative. See the file NOSA-1.3-JPF at the top of the distribution
9 // directory tree for the complete NOSA document.
10 //
11 // THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
12 // KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
13 // LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
14 // SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
15 // A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
16 // THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
17 // DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
18 //
19 package gov.nasa.jpf.tools;
20
21 import gov.nasa.jpf.Config;
22 import gov.nasa.jpf.SearchListener;
23 import gov.nasa.jpf.VMListener;
24 import gov.nasa.jpf.JPF;
25 import gov.nasa.jpf.jvm.JVM;
26 import gov.nasa.jpf.Search;
27 import gov.nasa.jpf.VM;
28 import gov.nasa.jpf.jvm.bytecode.Instruction;
29 import gov.nasa.jpf.jvm.ThreadInfo;
30 import gov.nasa.jpf.jvm.Step;
31 import java.io.PrintWriter JavaDoc;
32 import gov.nasa.jpf.util.SourceRef;
33
34 /**
35  * Listener tool to monitor JPF execution. This class can be used as a drop-in
36  * replacement for JPF, which is called by ExecTracker.
37  * ExecTracker is mostly a VMListener of 'instructionExecuted' and
38  * a SearchListener of 'stateAdvanced' and 'statehBacktracked'
39  */
40 public class ExecTracker implements SearchListener, VMListener {
41   /******************************************* SearchListener interface *****/
42     
43   boolean printLines = false;
44   PrintWriter JavaDoc pw;
45   SourceRef lastLine;
46   String JavaDoc linePrefix;
47   
48   public void searchConstraintHit(Search search) {
49   }
50   
51   public void stateRestored(Search search) {
52     int id = search.getStateNumber();
53     System.out.println("--- restored: " + id);
54   }
55     
56   public void propertyViolated(Search search) {
57   }
58
59   //--- the ones we are interested in
60 public void searchStarted(Search search) {
61     System.out.println("--- search started");
62   }
63
64   public void stateAdvanced(Search search) {
65     int id = search.getStateNumber();
66     
67     System.out.print("--- forward: " + id );
68     if (search.isNewState()) {
69       System.out.print(" new");
70     } else {
71       System.out.print(" visited");
72     }
73     
74     if (search.isEndState()) {
75       System.out.println(" end");
76     } else {
77       System.out.println();
78     }
79     
80     lastLine = null; // in case we report by source line
81 linePrefix = null;
82   }
83
84   public void stateProcessed (Search search) {
85     int id = search.getStateNumber();
86     System.out.println("--- done: " + id);
87   }
88
89   public void stateBacktracked(Search search) {
90     int id = search.getStateNumber();
91     
92     System.out.println("--- backtrack: " + id);
93   }
94   
95   public void searchFinished(Search search) {
96     System.out.println("--- search finished");
97   }
98
99   /******************************************* 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 JavaDoc(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: " + ti.getIndex());
150   }
151
152   public void threadTerminated(VM vm) {
153     JVM jvm = (JVM)vm;
154     ThreadInfo ti = jvm.getLastThreadInfo();
155     
156     System.out.println( "\t\t\t\t # thread terminated: " + ti.getIndex());
157   }
158
159   /****************************************** private stuff ******/
160
161   void filterArgs (String JavaDoc[] args) {
162     for (int i=0; i<args.length; i++) {
163       if (args[i].equals("-print-lines")) {
164         printLines = true;
165         args[i] = null;
166       }
167     }
168   }
169   
170   public static void main (String JavaDoc[] args) {
171     ExecTracker listener = new ExecTracker();
172     listener.filterArgs(args); // check and remove our own args
173
174     Config conf = JPF.createConfig(args);
175     // do special settings here
176
177     JPF jpf = new JPF(conf);
178     jpf.addSearchListener(listener);
179     jpf.addVMListener(listener);
180
181     jpf.run();
182   }
183 }
184
185
Popular Tags