src/main/gov/nasa/jpf/listener/ChoiceTracker.java

   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
  19 package gov.nasa.jpf.listener;
  20
  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;
  31
  32 import java.io.FileNotFoundException;
  33 import java.io.PrintWriter;
  34
  35 /**
  36  * generic choice tracker tool, to produce a list of choice values that
  37  * can be used to create readable replay scripts etc.
  38  */
  39 public class ChoiceTracker extends ListenerAdapter implements PublisherExtension {
  40
  41   enum Format { CG, CHOICE };
  42
  43   Config config;
  44   VM vm;
  45   Search search;
  46
  47   protected PrintWriter pw;
  48   Class<?>[] cgClasses;
  49   boolean isReportExtension;
  50
  51   boolean showLocation;
  52   Format format = Format.CHOICE;
  53   String[] excludes;
  54
  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();
  59     vm = jpf.getVM();
  60     search = jpf.getSearch();
  61
  62     cgClasses = new Class<?>[1];
  63     cgClasses[0] = cgClass;
  64
  65     try {
  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);
  70     }
  71   }
  72
  73   public ChoiceTracker (Config config, JPF jpf) {
  74     this.config = config;
  75     vm = jpf.getVM();
  76     search = jpf.getSearch();
  77
  78     String fname = config.getString("choice.trace");
  79     if (fname == null) {
  80       isReportExtension = true;
  81       jpf.addPublisherExtension(ConsolePublisher.class, this);
  82       // pw is going to be set later
  83     } else {
  84       try {
  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);
  89       }
  90     }
  91
  92     excludes = config.getStringArray("choice.exclude");
  93     cgClasses = config.getClasses("choice.class");
  94
  95     format = config.getEnum("choice.format", Format.values(), Format.CG);
  96     showLocation = config.getBoolean("choice.show_location", true);
  97   }
  98
  99   public void setExcludes (String... ex) {
 100     excludes=ex;
 101   }
 102
 103   boolean isRelevantCG (ChoiceGenerator cg){
 104     if (cgClasses == null){
 105       return true;
 106     } else {
 107       for (Class<?> cls : cgClasses){
 108         if (cls.isAssignableFrom(cg.getClass())){
 109           return true;
 110         }
 111       }
 112
 113       return false;
 114     }
 115   }
 116
 117   @Override
 118   public void propertyViolated (Search search) {
 119
 120     if (!isReportExtension) {
 121
 122       pw.print("// application: ");
 123       pw.println( search.getVM().getSUTDescription());
 124
 125       if (cgClasses == null) {
 126         pw.println("// trace over all CG classes");
 127       } else {
 128         pw.print("// trace over CG types: ");
 129         for (Class<?> cls : cgClasses){
 130           pw.print(cls.getName());
 131           pw.print(' ');
 132         }
 133         pw.println();
 134       }
 135
 136       pw.println("//------------------------- choice trace");
 137       printChoices();
 138
 139       pw.println("//------------------------- end choice trace");
 140       pw.flush();
 141     }
 142   }
 143
 144   void printChoices () {
 145     int i = 0;
 146     SystemState ss = vm.getSystemState();
 147     ChoiceGenerator<?>[] cgStack = ss.getChoiceGenerators();
 148
 149     nextChoice:
 150     for (ChoiceGenerator<?> cg : cgStack) {
 151       if (isRelevantCG(cg) && !cg.isDone()){
 152
 153         Object choice = cg.getNextChoice();
 154         if (choice == null) {
 155           continue;
 156         } else {
 157           if (excludes != null) {
 158             for (String e : excludes) {
 159               if (choice.toString().startsWith(e)) {
 160                 continue nextChoice;
 161               }
 162             }
 163           }
 164         }
 165
 166         String line = null;
 167
 168         switch (format){
 169           case CHOICE:
 170             line = choice.toString();
 171             if (line.startsWith("gov.nasa.jpf.vm.")){
 172               line = line.substring(17);
 173             }
 174             break;
 175           case CG:
 176             line = cg.toString();
 177             if (line.startsWith("gov.nasa.jpf.vm.choice.")){
 178               line = line.substring(24);
 179             }
 180             break;
 181         }
 182
 183         if (line != null){
 184           pw.print(String.format("%4d: ", i++));
 185
 186           pw.print(line);
 187
 188           if (showLocation) {
 189             String loc = cg.getSourceLocation();
 190             if (loc != null) {
 191               pw.println();
 192               pw.print(" \tat ");
 193               pw.print(loc);
 194             }
 195           }
 196           pw.println();
 197         }
 198       }
 199     }
 200   }
 201
 202   //--- the PublisherExtension interface
 203
 204   @Override
 205   public void publishPropertyViolation (Publisher publisher) {
 206     pw = publisher.getOut();
 207     publisher.publishTopicStart("choice trace " + publisher.getLastErrorId());
 208     printChoices();
 209   }
 210
 211 }