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.jvm;
020:
021: import gov.nasa.jpf.*;
022: import gov.nasa.jpf.Path;
023: import gov.nasa.jpf.util.*;
024: import gov.nasa.jpf.util.Printable;
025:
026: import java.io.PrintWriter;
027:
028: /**
029: * concrete type to store execution paths. TrailInfo corresponds to Transition,
030: * i.e. all instructions executed in the context of a vm.forward() leading
031: * into a new state
032: */
033: public class TrailInfo implements Transition, Printable { // <2do> cloneable
034:
035: private int thread;
036: private int random;
037: private Step first, last;
038: int nSteps;
039:
040: private Object annotation;
041: String output;
042:
043: static boolean showSteps; // do we report steps?
044:
045: static boolean init(Config config) {
046: showSteps = config.getBoolean("vm.report.show_steps");
047: return true;
048: }
049:
050: public TrailInfo(int t, int r) {
051: thread = t;
052: random = r;
053: }
054:
055: public String getLabel() {
056: if (last != null) {
057: return last.getLineString();
058: } else {
059: return "?";
060: }
061: }
062:
063: public void setOutput(String s) {
064: output = s;
065: }
066:
067: public void setAnnotation(Object o) {
068: annotation = o;
069: }
070:
071: public Object getAnnotation() {
072: return annotation;
073: }
074:
075: public String getOutput() {
076: return output;
077: }
078:
079: public void setRandom(int r) {
080: random = r;
081: }
082:
083: public int getRandom() {
084: return this .random;
085: }
086:
087: public Step getStep(int index) {
088: Step s;
089: int i;
090: for (i = 0, s = first; (s != null) && (i < index); i++, s = s.next)
091: ;
092: return s;
093: }
094:
095: public Step getLastStep() {
096: return last;
097: }
098:
099: public int getStepCount() {
100: return nSteps;
101: }
102:
103: public int getThread() {
104: return this .thread;
105: }
106:
107: /**
108: * @see Transition
109: */
110: public TransitionStep getTransitionStep(int index) {
111: return getStep(index);
112: }
113:
114: /**
115: * @see Transition
116: */
117: public TransitionStep getLastTransitionStep() {
118: return last;
119: }
120:
121: void addStep(Step step) {
122: if (first == null) {
123: first = step;
124: last = step;
125: } else {
126: last.next = step;
127: last = step;
128: }
129: nSteps++;
130: }
131:
132: public void printOn(PrintWriter pw) {
133: SourceRef sr = new SourceRef();
134:
135: pw.print("Thread #");
136: pw.print(thread);
137:
138: if (random != -1) {
139: pw.print(" Random #");
140: pw.print(random);
141: }
142: pw.println();
143:
144: if (showSteps) {
145: for (Step s = first; s != null; s = s.next) {
146: s.printStepOn(pw, sr, null);
147: }
148: }
149: }
150:
151: public void toXML(PrintWriter pw) {
152: if (random == -1) {
153: pw.println("\t<Step Thread=\"" + getThread() + "\">");
154: } else {
155: pw.println("\t<Step Thread=\"" + getThread()
156: + "\" Random=\"" + getRandom() + "\">");
157: }
158:
159: for (Step s = first; s != null; s = s.next) {
160: s.toXML(pw);
161: }
162:
163: pw.println("\t</Step>");
164: }
165:
166: public static void toXML(PrintWriter s, Path path) {
167: s.println("<?xml version=\"1.0\"?>");
168: s.println("<!DOCTYPE Trace [");
169:
170: s.println("\t<!ELEMENT Trace (Step+)>");
171: s.println("\t<!ATTLIST Trace");
172: s.println("\t\tHandler CDATA #REQUIRED");
173: s.println("\t\tApplication CDATA #REQUIRED");
174: s.println("\t\tMessage CDATA #IMPLIED>");
175:
176: s.println("\t<!ELEMENT Step (Instruction+,Comment*)>");
177: s.println("\t<!ATTLIST Step");
178: s.println("\t\tThread CDATA #REQUIRED ");
179: s.println("\t\tRandom CDATA \"-1\">");
180:
181: s.println("\t<!ELEMENT Instruction (EMPTY)>");
182: s.println("\t<!ATTLIST Instruction");
183: s.println("\t\tFile CDATA #REQUIRED");
184: s.println("\t\tLine CDATA #REQUIRED>");
185:
186: s.println("\t<!ELEMENT Comment (#PCDATA)>");
187: s.println("]>");
188: s.println();
189:
190: s.print("<Trace ");
191: s.print(" Handler=\"gov.nasa.jpf.jvm.JVMXMLTraceHandler\"");
192: s.print(" Application=\"");
193: s.print(JVM.getVM().getMainClassName());
194: s.println("\">");
195:
196: for (int i = 0; i < path.length(); i++) {
197: TrailInfo ti = (TrailInfo) path.get(i);
198: ti.toXML(s);
199: }
200:
201: s.println("</Trace>");
202: }
203: }
|