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.vm;
20 import gov.nasa.jpf.JPFException;
23 import java.io.FileReader;
24 import java.io.FileWriter;
25 import java.io.IOException;
26 import java.io.PrintWriter;
27 import java.io.StreamTokenizer;
28 import java.util.HashMap;
31 * a little helper class that is used to replay previously stored traces
32 * (which are little more than just a list of ChoiceGenerator classnames and
33 * choiceIndex indexes stored in a previous run)
35 public class ChoicePoint {
38 ChoicePoint next, prev;
40 ChoicePoint (String cgClassName, int choice, ChoicePoint prev) {
41 this.cgClassName = cgClassName;
42 this.choiceIndex = choice;
50 public String getCgClassName() {
54 public int getChoiceIndex() {
58 public ChoicePoint getNext() {
62 public ChoicePoint getPrevious() {
66 public static void storeTrace (String fileName,
67 String sutName, String comment,
68 ChoiceGenerator[] trace, boolean verbose) {
70 if (fileName != null) {
72 FileWriter fw = new FileWriter(fileName);
73 PrintWriter pw = new PrintWriter(fw);
75 if (comment != null){ // might be multi-line
81 // store the main app class and args here, so that we can do at least some checking
82 pw.print( "application: ");
85 // keep a String->id map so that we don't have to store thousands of redundant strings
86 HashMap<String,Integer> map = new HashMap<String,Integer>();
89 for (i=0; i<trace.length; i++) {
90 String cgClsName = trace[i].getClass().getName();
96 Integer ref = map.get(cgClsName);
99 map.put(cgClsName, clsId++);
100 } else { // us the numeric id instead
102 pw.print(ref.intValue());
106 pw.print( trace[i].getProcessedNumberOfChoices()-1);
118 } catch (Throwable t) {
119 throw new JPFException(t);
124 static StreamTokenizer createScanner (String fileName) {
125 StreamTokenizer scanner = null;
127 if (fileName == null) {
131 File f = new File(fileName);
134 FileReader fr = new FileReader(f);
135 scanner = new StreamTokenizer(fr);
137 scanner.slashSlashComments(true);
138 scanner.slashStarComments(true);
140 // how silly - there is no better way to turn off parseNumbers()
141 scanner.resetSyntax();
142 scanner.wordChars('a', 'z');
143 scanner.wordChars('A', 'Z');
144 scanner.wordChars(128 + 32, 255);
145 scanner.whitespaceChars(0, ' ');
146 //scanner.commentChar('/');
147 scanner.quoteChar('"');
148 scanner.quoteChar('\'');
150 scanner.wordChars('0','9');
151 scanner.wordChars(':', ':');
152 scanner.wordChars('.', '.');
153 scanner.wordChars('#', '#');
156 } catch (IOException iox) {
157 throw new JPFException("cannot read tracefile: " + fileName);
166 static void match (StreamTokenizer scanner, String s) throws IOException {
167 if ((scanner.ttype == StreamTokenizer.TT_WORD) && (scanner.sval.equals(s))) {
170 throw new JPFException ("tracefile error - expected " + s + ", got: " + scanner.sval);
174 static String matchString (StreamTokenizer scanner) throws IOException {
175 if (scanner.ttype == StreamTokenizer.TT_WORD) {
176 String s = scanner.sval;
177 if (s.length() == 0) {
178 throw new JPFException ("tracefile error - non-empty string expected");
183 throw new JPFException ("tracefile error - word expected, got: " + scanner.sval);
187 static void matchChar (StreamTokenizer scanner, char c) throws IOException {
188 if (scanner.ttype == c) {
191 throw new JPFException ("tracefile error - char '"
192 + c + "' expected, got: " + scanner.sval);
196 static int matchNumber (StreamTokenizer scanner) throws IOException {
198 if (scanner.ttype == StreamTokenizer.TT_WORD) {
199 int n = Integer.parseInt(scanner.sval);
203 } catch (NumberFormatException nfx) {}
205 throw new JPFException ("tracefile error - number expected, got: " + scanner.sval);
209 * "application:" appName
211 * "["searchLevel"]" (choiceGeneratorName | '#'cgID) nChoice
213 public static ChoicePoint readTrace (String fileName, String sutName) {
214 ChoicePoint firstCp = null, cp = null;
215 StreamTokenizer scanner = createScanner(fileName);
217 if (scanner == null) {
222 match(scanner, "application:");
223 match(scanner, sutName);
225 HashMap<String,String> map = new HashMap<String,String>();
228 while (scanner.ttype != StreamTokenizer.TT_EOF) {
229 matchChar(scanner, '[');
230 matchNumber(scanner);
231 matchChar(scanner, ']');
233 String cpClass = matchString(scanner);
234 if (cpClass.charAt(0) == '#') { // it's a CG class id
235 cpClass = map.get(cpClass);
236 if (cpClass == null) {
237 throw new JPFException("tracefile error - unknown ChoicePoint class id: " + cpClass);
240 String id = "#" + clsId++;
241 map.put(id, cpClass);
244 int choiceIndex = matchNumber(scanner);
246 cp = new ChoicePoint(cpClass, choiceIndex, cp);
247 if (firstCp == null) {
251 } catch (IOException iox) {
252 throw new JPFException("tracefile read error: " + iox.getMessage());