src/main/gov/nasa/jpf/listener/PathOutputMonitor.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 package gov.nasa.jpf.listener;
  19
  20 import gov.nasa.jpf.Config;
  21 import gov.nasa.jpf.JPF;
  22 import gov.nasa.jpf.PropertyListenerAdapter;
  23 import gov.nasa.jpf.report.ConsolePublisher;
  24 import gov.nasa.jpf.report.Publisher;
  25 import gov.nasa.jpf.search.Search;
  26 import gov.nasa.jpf.vm.VM;
  27 import gov.nasa.jpf.vm.Path;
  28 import gov.nasa.jpf.vm.Transition;
  29
  30 import java.io.BufferedReader;
  31 import java.io.File;
  32 import java.io.FileNotFoundException;
  33 import java.io.FileReader;
  34 import java.io.IOException;
  35 import java.io.PrintWriter;
  36 import java.io.StringReader;
  37 import java.io.StringWriter;
  38 import java.util.ArrayList;
  39 import java.util.HashSet;
  40 import java.util.Iterator;
  41 import java.util.List;
  42 import java.util.logging.Logger;
  43 import java.util.regex.Matcher;
  44 import java.util.regex.Pattern;
  45 import java.util.regex.PatternSyntaxException;
  46
  47 /**
  48  * listener that monitors path output, matching it against specifications
  49  * supplied as text files. Per default, this uses simple line-by-line
  50  * regular expression matching, also supporting prefixes by means of
  51  * special ". . ." ellipsis patterns. Each file can contain a number of
  52  * path output specs, separated by "~~~~~" lines.
  53  *
  54  *  The major purpose of this listener is to verify JPF state spaces,
  55  *  but it can also be used as a functional property
  56  */
  57 public class PathOutputMonitor extends PropertyListenerAdapter {
  58
  59   static final String SEPARATOR = "~~~";
  60   static final String ELLIPSIS = "...";
  61
  62   static Logger log = JPF.getLogger("gov.nasa.jpf.listener.PathOutputMonitor");
  63
  64   public interface PathOutputSpec {
  65     boolean add (String spec);
  66     boolean matches (String[] output);
  67     void printOn (PrintWriter pw);
  68     boolean isEmpty();
  69   }
  70
  71   static class VerbatimOutputSpec implements PathOutputSpec {
  72     ArrayList<String> patterns = new ArrayList<String>();
  73
  74     @Override
  75           public boolean add (String spec) {
  76       patterns.add(spec);
  77       return true;
  78     }
  79
  80     @Override
  81           public boolean matches (String[] output) {
  82       if ((output != null) && (output.length > 0)) {
  83         Iterator<String> it = patterns.iterator();
  84         for (String line : output) {
  85           if (it.hasNext()) {
  86             String p = it.next();
  87             if (!p.equals(line)){
  88               return false;
  89             }
  90           } else {
  91             return false;
  92           }
  93         }
  94
  95         return !it.hasNext();
  96
  97       } else {
  98         return patterns.isEmpty();
  99       }
 100     }
 101
 102     // sometimes, duck typing would be nice..
 103
 104     @Override
 105           public void printOn (PrintWriter pw) {
 106       for (String p : patterns) {
 107         pw.println(p.toString());
 108       }
 109     }
 110
 111     @Override
 112     public boolean isEmpty(){
 113       return patterns.isEmpty();
 114     }
 115   }
 116
 117   // simple regular expression matchers (could be a more sophisticated parser)
 118   static class RegexOutputSpec implements PathOutputSpec {
 119     ArrayList<Pattern> patterns = new ArrayList<Pattern>();
 120
 121     @Override
 122           public boolean add (String spec) {
 123       try {
 124         Pattern p = Pattern.compile(spec);
 125         patterns.add(p);
 126       } catch (PatternSyntaxException psx) {
 127         return false;
 128       }
 129
 130       return true;
 131     }
 132
 133     @Override
 134           public boolean matches (String[] output) {
 135
 136       if ((output != null) && (output.length > 0)) {
 137         Iterator<Pattern> it = patterns.iterator();
 138         for (String line : output) {
 139           if (it.hasNext()) {
 140             Pattern p = it.next();
 141
 142             if (p.toString().equals(ELLIPSIS)) {
 143               return true;
 144             }
 145
 146             Matcher m = p.matcher(line);
 147             if (!m.matches()) {
 148               return false;
 149             }
 150           } else {
 151             return false;
 152           }
 153         }
 154
 155         return (!it.hasNext() || it.next().toString().equals(ELLIPSIS));
 156
 157       } else { // no output
 158         return patterns.isEmpty();
 159       }
 160     }
 161
 162     @Override
 163           public void printOn (PrintWriter pw) {
 164       for (Pattern p : patterns) {
 165         pw.println(p.toString());
 166       }
 167     }
 168
 169     @Override
 170     public boolean isEmpty(){
 171       return patterns.isEmpty();
 172     }
 173   }
 174
 175   //---- our instance data
 176   VM vm;
 177
 178   //--- this is where we store the outputs (line-wise)
 179   // <2do> not very space efficient
 180   List<String[]> pathOutputs = new ArrayList<String[]>();
 181
 182   //--- config options
 183   Class<? extends PathOutputSpec> psClass;
 184   boolean printOutput;
 185   boolean deferOutput;
 186   List<PathOutputSpec> anySpecs, allSpecs, noneSpecs;
 187
 188   //--- keep track of property violations
 189   String errorMsg;
 190   List<PathOutputSpec> violatedSpecs;
 191   String[] offendingOutput;
 192
 193
 194   public PathOutputMonitor (Config config, JPF jpf) {
 195     vm = jpf.getVM();
 196     vm.storePathOutput();
 197
 198     jpf.addPublisherExtension(ConsolePublisher.class, this);
 199
 200     printOutput = config.getBoolean("pom.print_output", true);
 201     deferOutput = config.getBoolean("pom.defer_output", true);
 202
 203     psClass = config.getClass("pom.output_spec.class", PathOutputSpec.class);
 204
 205     if (psClass == null) {
 206       psClass = RegexOutputSpec.class;
 207     }
 208
 209     anySpecs = loadSpecs(config, "pom.any");
 210     allSpecs = loadSpecs(config, "pom.all");
 211     noneSpecs = loadSpecs(config, "pom.none");
 212
 213     violatedSpecs = new ArrayList<PathOutputSpec>();
 214   }
 215
 216
 217   List<PathOutputSpec> loadSpecs(Config conf, String key) {
 218     String spec = conf.getString(key);
 219     if (spec != null) {
 220       if (spec.startsWith("\"")){ // spec is in-situ content (convenience method for test classes)
 221         spec = spec.substring(1, spec.length()-1);
 222         BufferedReader br = new BufferedReader( new StringReader(spec));
 223         return readPathPatterns(br);
 224
 225       } else { // spec is pathname of output sepc file
 226         File file = new File(spec);
 227         try {
 228           BufferedReader br = new BufferedReader( new FileReader(file));
 229           return readPathPatterns(br);
 230
 231         } catch (FileNotFoundException fnfx){
 232           log.warning("pattern file not found: " + spec);
 233         }
 234       }
 235     }
 236
 237     return null;
 238   }
 239
 240   PathOutputSpec createPathOutputSpec() {
 241     try {
 242       return psClass.newInstance();
 243     } catch (Throwable t) {
 244       log.severe("cannot instantiate PathoutputSpec class: " + t.getMessage());
 245       return null;
 246     }
 247   }
 248
 249
 250
 251   List<PathOutputSpec> readPathPatterns (BufferedReader br){
 252     ArrayList<PathOutputSpec> results = new ArrayList<PathOutputSpec>();
 253
 254     // prefix pattern goes into file
 255
 256     try {
 257       PathOutputSpec ps = createPathOutputSpec();
 258
 259       int lineno = 0;
 260       for (String line=br.readLine(); true; line = br.readLine()) {
 261         if (line == null) {
 262           results.add(ps);
 263           break;
 264         }
 265         lineno++;
 266
 267         if (line.startsWith(SEPARATOR)) {
 268           results.add(ps);
 269           ps = createPathOutputSpec();
 270         } else {
 271           ps.add(line);
 272         }
 273       }
 274
 275       br.close();
 276     } catch (FileNotFoundException fnfx) {
 277       return null;
 278     } catch (IOException e) {
 279       e.printStackTrace();
 280     }
 281
 282     return results;
 283   }
 284
 285   String[] getLines (String output) {
 286     ArrayList<String> lines = new ArrayList<String>();
 287     BufferedReader br = new BufferedReader(new StringReader(output));
 288     try {
 289       for (String line = br.readLine(); line != null; line = br.readLine()) {
 290         lines.add(line);
 291       }
 292     } catch (IOException iox) {
 293       iox.printStackTrace();
 294     }
 295
 296     return lines.toArray(new String[lines.size()]);
 297   }
 298
 299   boolean matchesAny (List<PathOutputSpec> outputSpecs, String[] lines) {
 300     for (PathOutputSpec ps : outputSpecs) {
 301       if (ps.matches(lines)) {
 302         return true;
 303       }
 304     }
 305
 306     errorMsg = "unmatched output";
 307     offendingOutput = lines;
 308
 309     return false;
 310   }
 311
 312   boolean matchesNone (List<PathOutputSpec> outputSpecs, String[] lines) {
 313     for (PathOutputSpec ps : outputSpecs) {
 314       if (ps.matches(lines)) {
 315         errorMsg = "illegal output (matching inverse spec)";
 316         offendingOutput = lines;
 317         violatedSpecs.add(ps);
 318
 319         return false;
 320       }
 321     }
 322
 323     return true;
 324   }
 325
 326   boolean matchesAll (List<PathOutputSpec> outputSpecs, List<String[]> outputs) {
 327     HashSet<PathOutputSpec> unmatched = new HashSet<PathOutputSpec>();
 328     unmatched.addAll(outputSpecs);
 329
 330     for (String[] lines : outputs) {
 331       for (PathOutputSpec ps : outputSpecs) {
 332         if (ps.matches(lines)) {
 333            unmatched.remove(ps);
 334           if (unmatched.isEmpty()) {
 335             return true;
 336           }
 337         }
 338       }
 339     }
 340
 341     errorMsg = "unmatched specs (" + unmatched.size() + ')';
 342     for (PathOutputSpec ps : unmatched) {
 343       violatedSpecs.add(ps);
 344     }
 345
 346     return false;
 347   }
 348
 349
 350   //----------- the listener interface
 351
 352   @Override
 353   public boolean check(Search search, VM vm) {
 354     return (errorMsg == null);
 355   }
 356
 357   @Override
 358   public String getErrorMessage () {
 359     StringWriter sw = new StringWriter();
 360     PrintWriter pw = new PrintWriter(sw);
 361
 362     pw.println(errorMsg);
 363
 364     if (offendingOutput != null) {
 365       pw.println("offending output:");
 366       for (String line : offendingOutput) {
 367         pw.println(line);
 368       }
 369     }
 370
 371     if (!violatedSpecs.isEmpty()) {
 372       pw.println("violated specs:");
 373       for (PathOutputSpec ps : violatedSpecs) {
 374         ps.printOn(pw);
 375         pw.println(SEPARATOR);
 376       }
 377
 378     }
 379
 380     String s = sw.toString();
 381     pw.close();
 382
 383     return s;
 384   }
 385
 386   @Override
 387   public void reset () {
 388     errorMsg = null;
 389     violatedSpecs.clear();
 390     offendingOutput = null;
 391   }
 392
 393   @Override
 394   public void stateAdvanced(Search search) {
 395     if (search.isEndState()) {
 396
 397       Path path = vm.getPath();
 398       if (path.hasOutput()) {
 399         StringBuilder sb = null;
 400
 401         if (deferOutput || (noneSpecs != null)) {
 402           sb = new StringBuilder();
 403           for (Transition t : path) {
 404             String s = t.getOutput();
 405             if (s != null){
 406               sb.append(s);
 407             }
 408           }
 409         }
 410
 411         String[] lines = getLines(sb.toString());
 412
 413         if (deferOutput) {
 414           pathOutputs.add(lines);
 415
 416         } else if (printOutput){
 417           for (Transition t : path) {
 418             String s = t.getOutput();
 419             if (s != null){
 420               System.out.print(s); // <2do> don't use System.out
 421             }
 422           }
 423         }
 424
 425         // check safety properties
 426         if (noneSpecs != null && !matchesNone(noneSpecs, lines)) {
 427            log.warning("pom.none violated");
 428         }
 429         if (anySpecs != null && !matchesAny(anySpecs, lines)) {
 430           log.warning("pom.any violated");
 431        }
 432
 433       }
 434     }
 435   }
 436
 437   @Override
 438   public void searchFinished (Search search) {
 439     if (allSpecs != null && !matchesAll(allSpecs, pathOutputs)) {
 440       log.warning("pom.all violated");
 441       search.error(this);
 442     }
 443   }
 444
 445   @Override
 446   public void publishFinished (Publisher publisher) {
 447
 448     if (printOutput) {
 449       PrintWriter pw = publisher.getOut();
 450       publisher.publishTopicStart("path outputs");
 451       for (String[] output : pathOutputs) {
 452         for (String line : output) {
 453           pw.println(line);
 454         }
 455         pw.println(SEPARATOR);
 456       }
 457     }
 458   }
 459
 460 }