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.
18 package gov.nasa.jpf.listener;
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;
30 import java.io.BufferedReader;
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;
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.
54 * The major purpose of this listener is to verify JPF state spaces,
55 * but it can also be used as a functional property
57 public class PathOutputMonitor extends PropertyListenerAdapter {
59 static final String SEPARATOR = "~~~";
60 static final String ELLIPSIS = "...";
62 static Logger log = JPF.getLogger("gov.nasa.jpf.listener.PathOutputMonitor");
64 public interface PathOutputSpec {
65 boolean add (String spec);
66 boolean matches (String[] output);
67 void printOn (PrintWriter pw);
71 static class VerbatimOutputSpec implements PathOutputSpec {
72 ArrayList<String> patterns = new ArrayList<String>();
75 public boolean add (String spec) {
81 public boolean matches (String[] output) {
82 if ((output != null) && (output.length > 0)) {
83 Iterator<String> it = patterns.iterator();
84 for (String line : output) {
98 return patterns.isEmpty();
102 // sometimes, duck typing would be nice..
105 public void printOn (PrintWriter pw) {
106 for (String p : patterns) {
107 pw.println(p.toString());
112 public boolean isEmpty(){
113 return patterns.isEmpty();
117 // simple regular expression matchers (could be a more sophisticated parser)
118 static class RegexOutputSpec implements PathOutputSpec {
119 ArrayList<Pattern> patterns = new ArrayList<Pattern>();
122 public boolean add (String spec) {
124 Pattern p = Pattern.compile(spec);
126 } catch (PatternSyntaxException psx) {
134 public boolean matches (String[] output) {
136 if ((output != null) && (output.length > 0)) {
137 Iterator<Pattern> it = patterns.iterator();
138 for (String line : output) {
140 Pattern p = it.next();
142 if (p.toString().equals(ELLIPSIS)) {
146 Matcher m = p.matcher(line);
155 return (!it.hasNext() || it.next().toString().equals(ELLIPSIS));
157 } else { // no output
158 return patterns.isEmpty();
163 public void printOn (PrintWriter pw) {
164 for (Pattern p : patterns) {
165 pw.println(p.toString());
170 public boolean isEmpty(){
171 return patterns.isEmpty();
175 //---- our instance data
178 //--- this is where we store the outputs (line-wise)
179 // <2do> not very space efficient
180 List<String[]> pathOutputs = new ArrayList<String[]>();
183 Class<? extends PathOutputSpec> psClass;
186 List<PathOutputSpec> anySpecs, allSpecs, noneSpecs;
188 //--- keep track of property violations
190 List<PathOutputSpec> violatedSpecs;
191 String[] offendingOutput;
194 public PathOutputMonitor (Config config, JPF jpf) {
196 vm.storePathOutput();
198 jpf.addPublisherExtension(ConsolePublisher.class, this);
200 printOutput = config.getBoolean("pom.print_output", true);
201 deferOutput = config.getBoolean("pom.defer_output", true);
203 psClass = config.getClass("pom.output_spec.class", PathOutputSpec.class);
205 if (psClass == null) {
206 psClass = RegexOutputSpec.class;
209 anySpecs = loadSpecs(config, "pom.any");
210 allSpecs = loadSpecs(config, "pom.all");
211 noneSpecs = loadSpecs(config, "pom.none");
213 violatedSpecs = new ArrayList<PathOutputSpec>();
217 List<PathOutputSpec> loadSpecs(Config conf, String key) {
218 String spec = conf.getString(key);
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);
225 } else { // spec is pathname of output sepc file
226 File file = new File(spec);
228 BufferedReader br = new BufferedReader( new FileReader(file));
229 return readPathPatterns(br);
231 } catch (FileNotFoundException fnfx){
232 log.warning("pattern file not found: " + spec);
240 PathOutputSpec createPathOutputSpec() {
242 return psClass.newInstance();
243 } catch (Throwable t) {
244 log.severe("cannot instantiate PathoutputSpec class: " + t.getMessage());
251 List<PathOutputSpec> readPathPatterns (BufferedReader br){
252 ArrayList<PathOutputSpec> results = new ArrayList<PathOutputSpec>();
254 // prefix pattern goes into file
257 PathOutputSpec ps = createPathOutputSpec();
260 for (String line=br.readLine(); true; line = br.readLine()) {
267 if (line.startsWith(SEPARATOR)) {
269 ps = createPathOutputSpec();
276 } catch (FileNotFoundException fnfx) {
278 } catch (IOException e) {
285 String[] getLines (String output) {
286 ArrayList<String> lines = new ArrayList<String>();
287 BufferedReader br = new BufferedReader(new StringReader(output));
289 for (String line = br.readLine(); line != null; line = br.readLine()) {
292 } catch (IOException iox) {
293 iox.printStackTrace();
296 return lines.toArray(new String[lines.size()]);
299 boolean matchesAny (List<PathOutputSpec> outputSpecs, String[] lines) {
300 for (PathOutputSpec ps : outputSpecs) {
301 if (ps.matches(lines)) {
306 errorMsg = "unmatched output";
307 offendingOutput = lines;
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);
326 boolean matchesAll (List<PathOutputSpec> outputSpecs, List<String[]> outputs) {
327 HashSet<PathOutputSpec> unmatched = new HashSet<PathOutputSpec>();
328 unmatched.addAll(outputSpecs);
330 for (String[] lines : outputs) {
331 for (PathOutputSpec ps : outputSpecs) {
332 if (ps.matches(lines)) {
333 unmatched.remove(ps);
334 if (unmatched.isEmpty()) {
341 errorMsg = "unmatched specs (" + unmatched.size() + ')';
342 for (PathOutputSpec ps : unmatched) {
343 violatedSpecs.add(ps);
350 //----------- the listener interface
353 public boolean check(Search search, VM vm) {
354 return (errorMsg == null);
358 public String getErrorMessage () {
359 StringWriter sw = new StringWriter();
360 PrintWriter pw = new PrintWriter(sw);
362 pw.println(errorMsg);
364 if (offendingOutput != null) {
365 pw.println("offending output:");
366 for (String line : offendingOutput) {
371 if (!violatedSpecs.isEmpty()) {
372 pw.println("violated specs:");
373 for (PathOutputSpec ps : violatedSpecs) {
375 pw.println(SEPARATOR);
380 String s = sw.toString();
387 public void reset () {
389 violatedSpecs.clear();
390 offendingOutput = null;
394 public void stateAdvanced(Search search) {
395 if (search.isEndState()) {
397 Path path = vm.getPath();
398 if (path.hasOutput()) {
399 StringBuilder sb = null;
401 if (deferOutput || (noneSpecs != null)) {
402 sb = new StringBuilder();
403 for (Transition t : path) {
404 String s = t.getOutput();
411 String[] lines = getLines(sb.toString());
414 pathOutputs.add(lines);
416 } else if (printOutput){
417 for (Transition t : path) {
418 String s = t.getOutput();
420 System.out.print(s); // <2do> don't use System.out
425 // check safety properties
426 if (noneSpecs != null && !matchesNone(noneSpecs, lines)) {
427 log.warning("pom.none violated");
429 if (anySpecs != null && !matchesAny(anySpecs, lines)) {
430 log.warning("pom.any violated");
438 public void searchFinished (Search search) {
439 if (allSpecs != null && !matchesAll(allSpecs, pathOutputs)) {
440 log.warning("pom.all violated");
446 public void publishFinished (Publisher publisher) {
449 PrintWriter pw = publisher.getOut();
450 publisher.publishTopicStart("path outputs");
451 for (String[] output : pathOutputs) {
452 for (String line : output) {
455 pw.println(SEPARATOR);