2 * Copyright (C) 2014, United States Government, as represented by the
3 * Administrator of the National Aeronautics and Space Administration.
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
10 * http://www.apache.org/licenses/LICENSE-2.0.
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.
19 package gov.nasa.jpf.listener;
21 import gov.nasa.jpf.Config;
22 import gov.nasa.jpf.JPF;
23 import gov.nasa.jpf.ListenerAdapter;
24 import gov.nasa.jpf.report.ConsolePublisher;
25 import gov.nasa.jpf.report.Publisher;
26 import gov.nasa.jpf.report.PublisherExtension;
27 import gov.nasa.jpf.search.Search;
28 import gov.nasa.jpf.vm.ChoiceGenerator;
29 import gov.nasa.jpf.vm.VM;
30 import gov.nasa.jpf.vm.SystemState;
32 import java.io.FileNotFoundException;
33 import java.io.PrintWriter;
36 * generic choice tracker tool, to produce a list of choice values that
37 * can be used to create readable replay scripts etc.
39 public class ChoiceTracker extends ListenerAdapter implements PublisherExtension {
41 enum Format { CG, CHOICE };
47 protected PrintWriter pw;
49 boolean isReportExtension;
52 Format format = Format.CHOICE;
55 // <2do> hardwired type specific tracker for use with some shells - check if
56 // we can get rid of it
57 public ChoiceTracker (JPF jpf, String traceFileName, Class<?> cgClass){
58 config = jpf.getConfig();
60 search = jpf.getSearch();
62 cgClasses = new Class<?>[1];
63 cgClasses[0] = cgClass;
66 pw = new PrintWriter(traceFileName);
67 } catch (FileNotFoundException fnfx) {
68 System.err.println("cannot write choice trace to file: " + traceFileName);
69 pw = new PrintWriter(System.out);
73 public ChoiceTracker (Config config, JPF jpf) {
76 search = jpf.getSearch();
78 String fname = config.getString("choice.trace");
80 isReportExtension = true;
81 jpf.addPublisherExtension(ConsolePublisher.class, this);
82 // pw is going to be set later
85 pw = new PrintWriter(fname);
86 } catch (FileNotFoundException fnfx) {
87 System.err.println("cannot write choice trace to file: " + fname);
88 pw = new PrintWriter(System.out);
92 excludes = config.getStringArray("choice.exclude");
93 cgClasses = config.getClasses("choice.class");
95 format = config.getEnum("choice.format", Format.values(), Format.CG);
96 showLocation = config.getBoolean("choice.show_location", true);
99 public void setExcludes (String... ex) {
103 boolean isRelevantCG (ChoiceGenerator cg){
104 if (cgClasses == null){
107 for (Class<?> cls : cgClasses){
108 if (cls.isAssignableFrom(cg.getClass())){
118 public void propertyViolated (Search search) {
120 if (!isReportExtension) {
122 pw.print("// application: ");
123 pw.println( search.getVM().getSUTDescription());
125 if (cgClasses == null) {
126 pw.println("// trace over all CG classes");
128 pw.print("// trace over CG types: ");
129 for (Class<?> cls : cgClasses){
130 pw.print(cls.getName());
136 pw.println("//------------------------- choice trace");
139 pw.println("//------------------------- end choice trace");
144 void printChoices () {
146 SystemState ss = vm.getSystemState();
147 ChoiceGenerator<?>[] cgStack = ss.getChoiceGenerators();
150 for (ChoiceGenerator<?> cg : cgStack) {
151 if (isRelevantCG(cg) && !cg.isDone()){
153 Object choice = cg.getNextChoice();
154 if (choice == null) {
157 if (excludes != null) {
158 for (String e : excludes) {
159 if (choice.toString().startsWith(e)) {
170 line = choice.toString();
171 if (line.startsWith("gov.nasa.jpf.vm.")){
172 line = line.substring(17);
176 line = cg.toString();
177 if (line.startsWith("gov.nasa.jpf.vm.choice.")){
178 line = line.substring(24);
184 pw.print(String.format("%4d: ", i++));
189 String loc = cg.getSourceLocation();
202 //--- the PublisherExtension interface
205 public void publishPropertyViolation (Publisher publisher) {
206 pw = publisher.getOut();
207 publisher.publishTopicStart("choice trace " + publisher.getLastErrorId());