Mercurial > hg > Members > kono > jpf-core

comparison src/main/gov/nasa/jpf/report/ConsolePublisher.java @ 0:61d41facf527

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
initial v8 import (history reset)
author Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
date Fri, 23 Jan 2015 10:14:01 -0800
parents
children 6774e2e08d37
comparison
equal deleted inserted replaced
-1:000000000000 0:61d41facf527
1 /*
2 * Copyright (C) 2014, United States Government, as represented by the
3 * Administrator of the National Aeronautics and Space Administration.
4 * All rights reserved.
5 *
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
9 *
10 * http://www.apache.org/licenses/LICENSE-2.0.
11 *
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.
17 */
18 package gov.nasa.jpf.report;
19
20 import gov.nasa.jpf.Config;
21 import gov.nasa.jpf.Error;
22 import gov.nasa.jpf.util.Left;
23 import gov.nasa.jpf.vm.ClassInfo;
24 import gov.nasa.jpf.vm.ClassLoaderInfo;
25 import gov.nasa.jpf.vm.Instruction;
26 import gov.nasa.jpf.vm.VM;
27 import gov.nasa.jpf.vm.MethodInfo;
28 import gov.nasa.jpf.vm.Path;
29 import gov.nasa.jpf.vm.Step;
30 import gov.nasa.jpf.vm.Transition;
31
32 import java.io.FileNotFoundException;
33 import java.io.FileOutputStream;
34 import java.io.PrintWriter;
35 import java.util.List;
36 import java.util.Map;
37 import java.util.Set;
38 import java.util.TreeMap;
39
40 public class ConsolePublisher extends Publisher {
41
42 // output destinations
43 String fileName;
44 FileOutputStream fos;
45
46 String port;
47
48 // the various degrees of information for program traces
49 protected boolean showCG;
50 protected boolean showSteps;
51 protected boolean showLocation;
52 protected boolean showSource;
53 protected boolean showMethod;
54 protected boolean showCode;
55
56 public ConsolePublisher(Config conf, Reporter reporter) {
57 super(conf, reporter);
58
59 // options controlling the output destination
60 fileName = conf.getString("report.console.file");
61 port = conf.getString("report.console.port");
62
63 // options controlling what info should be included in a trace
64 showCG = conf.getBoolean("report.console.show_cg", true);
65 showSteps = conf.getBoolean("report.console.show_steps", true);
66 showLocation = conf.getBoolean("report.console.show_location", true);
67 showSource = conf.getBoolean("report.console.show_source", true);
68 showMethod = conf.getBoolean("report.console.show_method", false);
69 showCode = conf.getBoolean("report.console.show_code", false);
70 }
71
72 @Override
73 public String getName() {
74 return "console";
75 }
76
77 @Override
78 protected void openChannel(){
79
80 if (fileName != null) {
81 try {
82 fos = new FileOutputStream(fileName);
83 out = new PrintWriter( fos);
84 } catch (FileNotFoundException x) {
85 // fall back to System.out
86 }
87 } else if (port != null) {
88 // <2do>
89 }
90
91 if (out == null){
92 out = new PrintWriter(System.out, true);
93 }
94 }
95
96 @Override
97 protected void closeChannel() {
98 if (fos != null){
99 out.close();
100 }
101 }
102
103 @Override
104 public void publishTopicStart (String topic) {
105 out.println();
106 out.print("====================================================== ");
107 out.println(topic);
108 }
109
110 @Override
111 public void publishTopicEnd (String topic) {
112 // nothing here
113 }
114
115 @Override
116 public void publishStart() {
117 super.publishStart();
118
119 if (startItems.length > 0){ // only report if we have output for this phase
120 publishTopicStart("search started: " + formatDTG(reporter.getStartDate()));
121 }
122 }
123
124 @Override
125 public void publishFinished() {
126 super.publishFinished();
127
128 if (finishedItems.length > 0){ // only report if we have output for this phase
129 publishTopicStart("search finished: " + formatDTG(reporter.getFinishedDate()));
130 }
131 }
132
133 @Override
134 protected void publishJPF() {
135 out.println(reporter.getJPFBanner());
136 out.println();
137 }
138
139 @Override
140 protected void publishDTG() {
141 out.println("started: " + reporter.getStartDate());
142 }
143
144 @Override
145 protected void publishUser() {
146 out.println("user: " + reporter.getUser());
147 }
148
149 @Override
150 protected void publishJPFConfig() {
151 publishTopicStart("JPF configuration");
152
153 TreeMap<Object,Object> map = conf.asOrderedMap();
154 Set<Map.Entry<Object,Object>> eSet = map.entrySet();
155
156 for (Object src : conf.getSources()){
157 out.print("property source: ");
158 out.println(conf.getSourceName(src));
159 }
160
161 out.println("properties:");
162 for (Map.Entry<Object,Object> e : eSet) {
163 out.println(" " + e.getKey() + "=" + e.getValue());
164 }
165 }
166
167 @Override
168 protected void publishPlatform() {
169 publishTopicStart("platform");
170 out.println("hostname: " + reporter.getHostName());
171 out.println("arch: " + reporter.getArch());
172 out.println("os: " + reporter.getOS());
173 out.println("java: " + reporter.getJava());
174 }
175
176
177 @Override
178 protected void publishSuT() {
179 publishTopicStart("system under test");
180 out.println( reporter.getSuT());
181 }
182
183 @Override
184 protected void publishError() {
185 Error e = reporter.getCurrentError();
186
187 publishTopicStart("error " + e.getId());
188 out.println(e.getDescription());
189
190 String s = e.getDetails();
191 if (s != null) {
192 out.println(s);
193 }
194
195 }
196
197 @Override
198 protected void publishConstraint() {
199 String constraint = reporter.getLastSearchConstraint();
200 publishTopicStart("search constraint");
201 out.println(constraint); // not much info here yet
202 }
203
204 @Override
205 protected void publishResult() {
206 List<Error> errors = reporter.getErrors();
207
208 publishTopicStart("results");
209
210 if (errors.isEmpty()) {
211 out.println("no errors detected");
212 } else {
213 for (Error e : errors) {
214 out.print("error #");
215 out.print(e.getId());
216 out.print(": ");
217 out.print(e.getDescription());
218
219 String s = e.getDetails();
220 if (s != null) {
221 s = s.replace('\n', ' ');
222 s = s.replace('\t', ' ');
223 s = s.replace('\r', ' ');
224 out.print(" \"");
225 if (s.length() > 50){
226 out.print(s.substring(0,50));
227 out.print("...");
228 } else {
229 out.print(s);
230 }
231 out.print('"');
232 }
233
234 out.println();
235 }
236 }
237 }
238
239 /**
240 * this is done as part of the property violation reporting, i.e.
241 * we have an error
242 */
243 @Override
244 protected void publishTrace() {
245 Path path = reporter.getPath();
246 int i=0;
247
248 if (path.size() == 0) {
249 return; // nothing to publish
250 }
251
252 publishTopicStart("trace " + reporter.getCurrentErrorId());
253
254 for (Transition t : path) {
255 out.print("------------------------------------------------------ ");
256 out.println("transition #" + i++ + " thread: " + t.getThreadIndex());
257
258 if (showCG){
259 out.println(t.getChoiceGenerator());
260 }
261
262 if (showSteps) {
263 String lastLine = null;
264 MethodInfo lastMi = null;
265 int nNoSrc=0;
266
267 for (Step s : t) {
268 if (showSource) {
269 String line = s.getLineString();
270 if (line != null) {
271 if (!line.equals(lastLine)) {
272 if (nNoSrc > 0){
273 out.println(" [" + nNoSrc + " insn w/o sources]");
274 }
275
276 out.print(" ");
277 if (showLocation) {
278 out.print(Left.format(s.getLocationString(),30));
279 out.print(" : ");
280 }
281 out.println(line.trim());
282 nNoSrc = 0;
283
284 }
285 } else { // no source
286 nNoSrc++;
287 }
288
289 lastLine = line;
290 }
291
292 if (showCode) {
293 Instruction insn = s.getInstruction();
294 if (showMethod){
295 MethodInfo mi = insn.getMethodInfo();
296 if (mi != lastMi) {
297 ClassInfo mci = mi.getClassInfo();
298 out.print(" ");
299 if (mci != null) {
300 out.print(mci.getName());
301 out.print(".");
302 }
303 out.println(mi.getUniqueName());
304 lastMi = mi;
305 }
306 }
307 out.print(" ");
308 out.println(insn);
309 }
310 }
311
312 if (showSource && !showCode && (nNoSrc > 0)) {
313 out.println(" [" + nNoSrc + " insn w/o sources]");
314 }
315 }
316 }
317 }
318
319 @Override
320 protected void publishOutput() {
321 Path path = reporter.getPath();
322
323 if (path.size() == 0) {
324 return; // nothing to publish
325 }
326
327 publishTopicStart("output " + reporter.getCurrentErrorId());
328
329 if (path.hasOutput()) {
330 for (Transition t : path) {
331 String s = t.getOutput();
332 if (s != null){
333 out.print(s);
334 }
335 }
336 } else {
337 out.println("no output");
338 }
339 }
340
341 @Override
342 protected void publishSnapshot() {
343 VM vm = reporter.getVM();
344
345 // not so nice - we have to delegate this since it's using a lot of internals, and is also
346 // used in debugging
347 publishTopicStart("snapshot " + reporter.getCurrentErrorId());
348
349 if (vm.getPathLength() > 0) {
350 vm.printLiveThreadStatus(out);
351 } else {
352 out.println("initial program state");
353 }
354 }
355
356 public static final String STATISTICS_TOPIC = "statistics";
357
358 // this is useful if somebody wants to monitor progress from a specialized ConsolePublisher
359 public synchronized void printStatistics (PrintWriter pw){
360 publishTopicStart( STATISTICS_TOPIC);
361 printStatistics( pw, reporter);
362 }
363
364 // this can be used outside a publisher, to show the same info
365 public static void printStatistics (PrintWriter pw, Reporter reporter){
366 Statistics stat = reporter.getStatistics();
367
368 pw.println("elapsed time: " + formatHMS(reporter.getElapsedTime()));
369 pw.println("states: new=" + stat.newStates + ",visited=" + stat.visitedStates
370 + ",backtracked=" + stat.backtracked + ",end=" + stat.endStates);
371 pw.println("search: maxDepth=" + stat.maxDepth + ",constraints=" + stat.constraints);
372 pw.println("choice generators: thread=" + stat.threadCGs
373 + " (signal=" + stat.signalCGs + ",lock=" + stat.monitorCGs + ",sharedRef=" + stat.sharedAccessCGs
374 + ",threadApi=" + stat.threadApiCGs + ",reschedule=" + stat.breakTransitionCGs
375 + "), data=" + stat.dataCGs);
376 pw.println("heap: " + "new=" + stat.nNewObjects
377 + ",released=" + stat.nReleasedObjects
378 + ",maxLive=" + stat.maxLiveObjects
379 + ",gcCycles=" + stat.gcCycles);
380 pw.println("instructions: " + stat.insns);
381 pw.println("max memory: " + (stat.maxUsed >> 20) + "MB");
382
383 pw.println("loaded code: classes=" + ClassLoaderInfo.getNumberOfLoadedClasses() + ",methods="
384 + MethodInfo.getNumberOfLoadedMethods());
385 }
386
387 @Override
388 public void publishStatistics() {
389 printStatistics(out);
390 }
391
392 }