src/main/gov/nasa/jpf/vm/ChoicePoint.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.vm;
  19
  20 import gov.nasa.jpf.JPFException;
  21
  22 import java.io.File;
  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;
  29
  30 /**
  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)
  34  */
  35 public class ChoicePoint {
  36   String cgClassName;
  37   int choiceIndex;
  38   ChoicePoint next, prev;
  39
  40   ChoicePoint (String cgClassName, int choice, ChoicePoint prev) {
  41     this.cgClassName = cgClassName;
  42     this.choiceIndex = choice;
  43
  44     if (prev != null) {
  45       this.prev = prev;
  46       prev.next = this;
  47     }
  48   }
  49
  50   public String getCgClassName() {
  51     return cgClassName;
  52   }
  53
  54   public int getChoiceIndex() {
  55     return choiceIndex;
  56   }
  57
  58   public ChoicePoint getNext() {
  59     return next;
  60   }
  61
  62   public ChoicePoint getPrevious() {
  63     return prev;
  64   }
  65
  66   public static void storeTrace (String fileName,
  67                                  String sutName, String comment,
  68                                  ChoiceGenerator[] trace, boolean verbose) {
  69     int i;
  70     if (fileName != null) {
  71       try {
  72         FileWriter fw = new FileWriter(fileName);
  73         PrintWriter pw = new PrintWriter(fw);
  74
  75         if (comment != null){ // might be multi-line
  76           pw.print("/* ");
  77           pw.print(comment);
  78           pw.println(" */");
  79         }
  80
  81         // store the main app class and args here, so that we can do at least some checking
  82         pw.print( "application: ");
  83         pw.println( sutName);
  84
  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>();
  87         int clsId = 0;
  88
  89         for (i=0; i<trace.length; i++) {
  90           String cgClsName = trace[i].getClass().getName();
  91
  92           pw.print('[');
  93           pw.print(i);
  94           pw.print("] ");
  95
  96           Integer ref = map.get(cgClsName);
  97           if (ref == null) {
  98             pw.print(cgClsName);
  99             map.put(cgClsName, clsId++);
 100           } else { // us the numeric id instead
 101             pw.print('#');
 102             pw.print(ref.intValue());
 103           }
 104
 105           pw.print(" ");
 106           pw.print( trace[i].getProcessedNumberOfChoices()-1);
 107
 108           if (verbose){
 109             pw.print("  // ");
 110             pw.print(trace[i]);
 111           }
 112
 113           pw.println();
 114         }
 115
 116         pw.close();
 117         fw.close();
 118       } catch (Throwable t) {
 119         throw new JPFException(t);
 120       }
 121     }
 122   }
 123
 124   static StreamTokenizer createScanner (String fileName) {
 125     StreamTokenizer scanner = null;
 126
 127     if (fileName == null) {
 128       return null;
 129     }
 130
 131     File f = new File(fileName);
 132     if (f.exists()) {
 133       try {
 134         FileReader fr = new FileReader(f);
 135         scanner = new StreamTokenizer(fr);
 136
 137         scanner.slashSlashComments(true);
 138         scanner.slashStarComments(true);
 139
 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('\'');
 149
 150         scanner.wordChars('0','9');
 151         scanner.wordChars(':', ':');
 152         scanner.wordChars('.', '.');
 153         scanner.wordChars('#', '#');
 154
 155         scanner.nextToken();
 156       } catch (IOException iox) {
 157         throw new JPFException("cannot read tracefile: " + fileName);
 158       }
 159
 160       return scanner;
 161     } else {
 162       return null;
 163     }
 164   }
 165
 166   static void match (StreamTokenizer scanner, String s) throws IOException {
 167     if ((scanner.ttype == StreamTokenizer.TT_WORD) && (scanner.sval.equals(s))) {
 168       scanner.nextToken();
 169     } else {
 170       throw new JPFException ("tracefile error - expected " + s + ", got: " + scanner.sval);
 171     }
 172   }
 173
 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");
 179       }
 180       scanner.nextToken();
 181       return s;
 182     } else {
 183       throw new JPFException ("tracefile error - word expected, got: " + scanner.sval);
 184     }
 185   }
 186
 187   static void matchChar (StreamTokenizer scanner, char c) throws IOException {
 188     if (scanner.ttype == c) {
 189       scanner.nextToken();
 190     } else {
 191       throw new JPFException ("tracefile error - char '"
 192                               + c + "' expected, got: " + scanner.sval);
 193     }
 194   }
 195
 196   static int matchNumber (StreamTokenizer scanner) throws IOException {
 197     try {
 198       if (scanner.ttype == StreamTokenizer.TT_WORD) {
 199         int n = Integer.parseInt(scanner.sval);
 200         scanner.nextToken();
 201         return n;
 202       }
 203     } catch (NumberFormatException nfx) {}
 204
 205     throw new JPFException ("tracefile error - number expected, got: " + scanner.sval);
 206   }
 207
 208   /**
 209    * "application:" appName
 210    *  {arg}
 211    *  "["searchLevel"]" (choiceGeneratorName | '#'cgID) nChoice
 212    */
 213   public static ChoicePoint readTrace (String fileName, String sutName) {
 214     ChoicePoint firstCp = null, cp = null;
 215     StreamTokenizer scanner = createScanner(fileName);
 216
 217     if (scanner == null) {
 218       return null;
 219     }
 220
 221     try {
 222     match(scanner, "application:");
 223     match(scanner, sutName);
 224
 225     HashMap<String,String> map = new HashMap<String,String>();
 226     int clsId = 0;
 227
 228     while (scanner.ttype != StreamTokenizer.TT_EOF) {
 229       matchChar(scanner, '[');
 230       matchNumber(scanner);
 231       matchChar(scanner, ']');
 232
 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);
 238         }
 239       } else {
 240         String id = "#" + clsId++;
 241         map.put(id, cpClass);
 242       }
 243
 244       int choiceIndex = matchNumber(scanner);
 245
 246       cp = new ChoicePoint(cpClass, choiceIndex, cp);
 247       if (firstCp == null) {
 248         firstCp = cp;
 249       }
 250     }
 251     } catch (IOException iox) {
 252       throw new JPFException("tracefile read error: " + iox.getMessage());
 253     }
 254
 255     return firstCp;
 256   }
 257 }