Mercurial > hg > Members > kono > jpf-core
view src/main/gov/nasa/jpf/report/ConsolePublisher.java @ 0:61d41facf527
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 |
line wrap: on
line source
/* * Copyright (C) 2014, United States Government, as represented by the * Administrator of the National Aeronautics and Space Administration. * All rights reserved. * * The Java Pathfinder core (jpf-core) platform is licensed under the * Apache License, Version 2.0 (the "License"); you may not use this file except * in compliance with the License. You may obtain a copy of the License at * * http://www.apache.org/licenses/LICENSE-2.0. * * Unless required by applicable law or agreed to in writing, software * distributed under the License is distributed on an "AS IS" BASIS, * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. * See the License for the specific language governing permissions and * limitations under the License. */ package gov.nasa.jpf.report; import gov.nasa.jpf.Config; import gov.nasa.jpf.Error; import gov.nasa.jpf.util.Left; import gov.nasa.jpf.vm.ClassInfo; import gov.nasa.jpf.vm.ClassLoaderInfo; import gov.nasa.jpf.vm.Instruction; import gov.nasa.jpf.vm.VM; import gov.nasa.jpf.vm.MethodInfo; import gov.nasa.jpf.vm.Path; import gov.nasa.jpf.vm.Step; import gov.nasa.jpf.vm.Transition; import java.io.FileNotFoundException; import java.io.FileOutputStream; import java.io.PrintWriter; import java.util.List; import java.util.Map; import java.util.Set; import java.util.TreeMap; public class ConsolePublisher extends Publisher { // output destinations String fileName; FileOutputStream fos; String port; // the various degrees of information for program traces protected boolean showCG; protected boolean showSteps; protected boolean showLocation; protected boolean showSource; protected boolean showMethod; protected boolean showCode; public ConsolePublisher(Config conf, Reporter reporter) { super(conf, reporter); // options controlling the output destination fileName = conf.getString("report.console.file"); port = conf.getString("report.console.port"); // options controlling what info should be included in a trace showCG = conf.getBoolean("report.console.show_cg", true); showSteps = conf.getBoolean("report.console.show_steps", true); showLocation = conf.getBoolean("report.console.show_location", true); showSource = conf.getBoolean("report.console.show_source", true); showMethod = conf.getBoolean("report.console.show_method", false); showCode = conf.getBoolean("report.console.show_code", false); } @Override public String getName() { return "console"; } @Override protected void openChannel(){ if (fileName != null) { try { fos = new FileOutputStream(fileName); out = new PrintWriter( fos); } catch (FileNotFoundException x) { // fall back to System.out } } else if (port != null) { // <2do> } if (out == null){ out = new PrintWriter(System.out, true); } } @Override protected void closeChannel() { if (fos != null){ out.close(); } } @Override public void publishTopicStart (String topic) { out.println(); out.print("====================================================== "); out.println(topic); } @Override public void publishTopicEnd (String topic) { // nothing here } @Override public void publishStart() { super.publishStart(); if (startItems.length > 0){ // only report if we have output for this phase publishTopicStart("search started: " + formatDTG(reporter.getStartDate())); } } @Override public void publishFinished() { super.publishFinished(); if (finishedItems.length > 0){ // only report if we have output for this phase publishTopicStart("search finished: " + formatDTG(reporter.getFinishedDate())); } } @Override protected void publishJPF() { out.println(reporter.getJPFBanner()); out.println(); } @Override protected void publishDTG() { out.println("started: " + reporter.getStartDate()); } @Override protected void publishUser() { out.println("user: " + reporter.getUser()); } @Override protected void publishJPFConfig() { publishTopicStart("JPF configuration"); TreeMap<Object,Object> map = conf.asOrderedMap(); Set<Map.Entry<Object,Object>> eSet = map.entrySet(); for (Object src : conf.getSources()){ out.print("property source: "); out.println(conf.getSourceName(src)); } out.println("properties:"); for (Map.Entry<Object,Object> e : eSet) { out.println(" " + e.getKey() + "=" + e.getValue()); } } @Override protected void publishPlatform() { publishTopicStart("platform"); out.println("hostname: " + reporter.getHostName()); out.println("arch: " + reporter.getArch()); out.println("os: " + reporter.getOS()); out.println("java: " + reporter.getJava()); } @Override protected void publishSuT() { publishTopicStart("system under test"); out.println( reporter.getSuT()); } @Override protected void publishError() { Error e = reporter.getCurrentError(); publishTopicStart("error " + e.getId()); out.println(e.getDescription()); String s = e.getDetails(); if (s != null) { out.println(s); } } @Override protected void publishConstraint() { String constraint = reporter.getLastSearchConstraint(); publishTopicStart("search constraint"); out.println(constraint); // not much info here yet } @Override protected void publishResult() { List<Error> errors = reporter.getErrors(); publishTopicStart("results"); if (errors.isEmpty()) { out.println("no errors detected"); } else { for (Error e : errors) { out.print("error #"); out.print(e.getId()); out.print(": "); out.print(e.getDescription()); String s = e.getDetails(); if (s != null) { s = s.replace('\n', ' '); s = s.replace('\t', ' '); s = s.replace('\r', ' '); out.print(" \""); if (s.length() > 50){ out.print(s.substring(0,50)); out.print("..."); } else { out.print(s); } out.print('"'); } out.println(); } } } /** * this is done as part of the property violation reporting, i.e. * we have an error */ @Override protected void publishTrace() { Path path = reporter.getPath(); int i=0; if (path.size() == 0) { return; // nothing to publish } publishTopicStart("trace " + reporter.getCurrentErrorId()); for (Transition t : path) { out.print("------------------------------------------------------ "); out.println("transition #" + i++ + " thread: " + t.getThreadIndex()); if (showCG){ out.println(t.getChoiceGenerator()); } if (showSteps) { String lastLine = null; MethodInfo lastMi = null; int nNoSrc=0; for (Step s : t) { if (showSource) { String line = s.getLineString(); if (line != null) { if (!line.equals(lastLine)) { if (nNoSrc > 0){ out.println(" [" + nNoSrc + " insn w/o sources]"); } out.print(" "); if (showLocation) { out.print(Left.format(s.getLocationString(),30)); out.print(" : "); } out.println(line.trim()); nNoSrc = 0; } } else { // no source nNoSrc++; } lastLine = line; } if (showCode) { Instruction insn = s.getInstruction(); if (showMethod){ MethodInfo mi = insn.getMethodInfo(); if (mi != lastMi) { ClassInfo mci = mi.getClassInfo(); out.print(" "); if (mci != null) { out.print(mci.getName()); out.print("."); } out.println(mi.getUniqueName()); lastMi = mi; } } out.print(" "); out.println(insn); } } if (showSource && !showCode && (nNoSrc > 0)) { out.println(" [" + nNoSrc + " insn w/o sources]"); } } } } @Override protected void publishOutput() { Path path = reporter.getPath(); if (path.size() == 0) { return; // nothing to publish } publishTopicStart("output " + reporter.getCurrentErrorId()); if (path.hasOutput()) { for (Transition t : path) { String s = t.getOutput(); if (s != null){ out.print(s); } } } else { out.println("no output"); } } @Override protected void publishSnapshot() { VM vm = reporter.getVM(); // not so nice - we have to delegate this since it's using a lot of internals, and is also // used in debugging publishTopicStart("snapshot " + reporter.getCurrentErrorId()); if (vm.getPathLength() > 0) { vm.printLiveThreadStatus(out); } else { out.println("initial program state"); } } public static final String STATISTICS_TOPIC = "statistics"; // this is useful if somebody wants to monitor progress from a specialized ConsolePublisher public synchronized void printStatistics (PrintWriter pw){ publishTopicStart( STATISTICS_TOPIC); printStatistics( pw, reporter); } // this can be used outside a publisher, to show the same info public static void printStatistics (PrintWriter pw, Reporter reporter){ Statistics stat = reporter.getStatistics(); pw.println("elapsed time: " + formatHMS(reporter.getElapsedTime())); pw.println("states: new=" + stat.newStates + ",visited=" + stat.visitedStates + ",backtracked=" + stat.backtracked + ",end=" + stat.endStates); pw.println("search: maxDepth=" + stat.maxDepth + ",constraints=" + stat.constraints); pw.println("choice generators: thread=" + stat.threadCGs + " (signal=" + stat.signalCGs + ",lock=" + stat.monitorCGs + ",sharedRef=" + stat.sharedAccessCGs + ",threadApi=" + stat.threadApiCGs + ",reschedule=" + stat.breakTransitionCGs + "), data=" + stat.dataCGs); pw.println("heap: " + "new=" + stat.nNewObjects + ",released=" + stat.nReleasedObjects + ",maxLive=" + stat.maxLiveObjects + ",gcCycles=" + stat.gcCycles); pw.println("instructions: " + stat.insns); pw.println("max memory: " + (stat.maxUsed >> 20) + "MB"); pw.println("loaded code: classes=" + ClassLoaderInfo.getNumberOfLoadedClasses() + ",methods=" + MethodInfo.getNumberOfLoadedMethods()); } @Override public void publishStatistics() { printStatistics(out); } }