001package daikon.test; 002 003import static java.io.StreamTokenizer.TT_WORD; 004import static java.nio.charset.StandardCharsets.UTF_8; 005import static java.util.logging.Level.FINE; 006import static java.util.logging.Level.INFO; 007import static org.junit.Assert.assertEquals; 008import static org.junit.Assert.fail; 009 010import daikon.Daikon; 011import daikon.Debug; 012import daikon.FileIO; 013import daikon.Global; 014import daikon.PptMap; 015import daikon.PptSlice; 016import daikon.PptTopLevel; 017import daikon.PrintInvariants; 018import daikon.ValueTuple; 019import daikon.VarInfo; 020import daikon.inv.Invariant; 021import gnu.getopt.Getopt; 022import gnu.getopt.LongOpt; 023import java.io.File; 024import java.io.IOException; 025import java.io.InputStream; 026import java.io.InputStreamReader; 027import java.io.LineNumberReader; 028import java.io.StreamTokenizer; 029import java.io.StringReader; 030import java.io.UncheckedIOException; 031import java.net.URL; 032import java.util.ArrayList; 033import java.util.Arrays; 034import java.util.HashSet; 035import java.util.List; 036import java.util.Set; 037import java.util.logging.Logger; 038import org.checkerframework.checker.nullness.qual.Nullable; 039import org.checkerframework.checker.signature.qual.ClassGetName; 040import org.junit.Test; 041import org.plumelib.util.StringsPlume; 042 043/** 044 * This tests Daikon's state as samples are processed. A standard decl file specifies the ppts. A 045 * sample input file specifies the samples and assertions that should be true at various points 046 * while processing. 047 * 048 * <p>The input file format is documented in the developer manual. 049 */ 050@SuppressWarnings({"nullness", "builder"}) // test code 051public class SampleTester { 052 053 public static final Logger debug = Logger.getLogger("daikon.test.SampleTester"); 054 public static final Logger debug_progress = Logger.getLogger("daikon.test.SampleTester.progress"); 055 056 static boolean first_decl = true; 057 String fname; 058 LineNumberReader fp; 059 PptMap all_ppts; 060 PptTopLevel ppt; 061 VarInfo[] vars; 062 063 /** The usage message for this program. */ 064 private static String usage = 065 StringsPlume.joinLines( 066 "Usage: java daikon.PrintInvariants [OPTION]... FILE", 067 " -h, --" + Daikon.help_SWITCH, 068 " Display this usage message", 069 " --" + Daikon.config_option_SWITCH, 070 " Specify a configuration option ", 071 " --" + Daikon.debug_SWITCH, 072 " Specify a logger to enable", 073 " --" + Daikon.track_SWITCH, 074 " Specify a class, varinfos, and ppt to debug track.", 075 " Format is class<var1,var2,var3>@ppt"); 076 077 public static void main(String[] args) throws IOException { 078 079 LongOpt[] longopts = 080 new LongOpt[] { 081 new LongOpt(Daikon.config_option_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0), 082 new LongOpt(Daikon.debugAll_SWITCH, LongOpt.NO_ARGUMENT, null, 0), 083 new LongOpt(Daikon.debug_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0), 084 new LongOpt(Daikon.track_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0), 085 }; 086 087 Getopt g = new Getopt("daikon.test.SampleTester", args, "h:", longopts); 088 int c; 089 while ((c = g.getopt()) != -1) { 090 switch (c) { 091 092 // long option 093 case 0: 094 String option_name = longopts[g.getLongind()].getName(); 095 if (Daikon.help_SWITCH.equals(option_name)) { 096 System.out.println(usage); 097 throw new Daikon.NormalTermination(); 098 099 } else if (Daikon.config_option_SWITCH.equals(option_name)) { 100 String item = Daikon.getOptarg(g); 101 daikon.config.Configuration.getInstance().apply(item); 102 break; 103 104 } else if (Daikon.debugAll_SWITCH.equals(option_name)) { 105 Global.debugAll = true; 106 107 } else if (Daikon.debug_SWITCH.equals(option_name)) { 108 daikon.LogHelper.setLevel(Daikon.getOptarg(g), FINE); 109 } else if (Daikon.track_SWITCH.equals(option_name)) { 110 daikon.LogHelper.setLevel("daikon.Debug", FINE); 111 String error = Debug.add_track(Daikon.getOptarg(g)); 112 if (error != null) { 113 throw new Daikon.UserError( 114 "Error parsing track argument '" + Daikon.getOptarg(g) + "' - " + error); 115 } 116 } else { 117 throw new RuntimeException("Unknown long option received: " + option_name); 118 } 119 break; 120 121 case 'h': 122 System.out.println(usage); 123 throw new Daikon.NormalTermination(); 124 125 case '?': 126 break; // getopt() already printed an error 127 128 default: 129 System.out.println("getopt() returned " + c); 130 break; 131 } 132 } 133 134 daikon.LogHelper.setupLogs(Global.debugAll ? FINE : INFO); 135 136 try (InputStream commands = SampleTester.class.getResourceAsStream("SampleTester.commands")) { 137 if (commands == null) { 138 fail( 139 "Input file SampleTester.commands missing." 140 + " (Should be in daikon.test and it must be within the classpath)"); 141 } 142 143 SampleTester ts = new SampleTester(); 144 ts.proc_sample_file(commands, "SampleTester.commands"); 145 System.out.println("Test Passes"); 146 } 147 } 148 149 private static @Nullable String find_file(String fname) { 150 151 URL input_file_location = ClassLoader.getSystemResource(fname); 152 153 if (input_file_location == null) { 154 return null; 155 } else { 156 return input_file_location.toExternalForm(); 157 } 158 } 159 160 /** 161 * This function is the actual function performed when this class is run through JUnit. 162 * 163 * @throws IOException if there in a problem with I/O 164 */ 165 @Test 166 public void test_samples() throws IOException { 167 168 FileIO.new_decl_format = null; 169 170 try (InputStream commands = getClass().getResourceAsStream("SampleTester.commands")) { 171 if (commands == null) { 172 fail( 173 "Input file SampleTester.commands missing." 174 + " (Should be in daikon.test and it must be within the classpath)"); 175 } 176 177 SampleTester ts = new SampleTester(); 178 ts.proc_sample_file(commands, "SampleTester.commands"); 179 } 180 } 181 182 public void proc_sample_file(InputStream commands, String filename) throws IOException { 183 184 if (PrintInvariants.dkconfig_print_inv_class) { 185 System.out.println("Warning: turning off PrintInvariants.dkconfig_print_inv_class"); 186 PrintInvariants.dkconfig_print_inv_class = false; 187 } 188 189 // Enable expected invariants 190 daikon.inv.ternary.threeScalar.FunctionBinary.dkconfig_enabled = true; 191 daikon.inv.ternary.threeScalar.FunctionBinaryFloat.dkconfig_enabled = true; 192 193 this.fname = filename; 194 fp = new LineNumberReader(new InputStreamReader(commands, UTF_8)); 195 196 for (String line = fp.readLine(); line != null; line = fp.readLine()) { 197 198 // Remove comments and skip blank lines 199 line = line.replaceAll("#.*", ""); 200 line = line.trim(); 201 if (line.length() == 0) { 202 continue; 203 } 204 205 // Get the line type and the remainder of the line 206 String[] sa = line.split(": *", 2); 207 if (sa.length != 2) parse_error("No line type specified"); 208 String ltype = sa[0].trim(); 209 String cmd = sa[1].trim(); 210 if (cmd.length() == 0) { 211 parse_error("no command specified"); 212 } 213 214 // Process the specified type of command 215 if (ltype.equals("decl")) proc_decl(cmd); 216 else if (ltype.equals("ppt")) proc_ppt(cmd); 217 else if (ltype.equals("vars")) proc_vars(cmd); 218 else if (ltype.equals("data")) proc_data(cmd, fp, filename); 219 else if (ltype.equals("assert")) proc_assert(cmd); 220 else { 221 parse_error("unknown line type: " + ltype); 222 } 223 } 224 } 225 226 /** Reads in the specified decl file and sets all_ppts accordingly. */ 227 private void proc_decl(String decl_file) throws IOException { 228 229 debug_progress.fine("Processing " + decl_file); 230 231 // Read in the specified file 232 Set<File> decl_files = new HashSet<>(1); 233 String absolute_decl_file = find_file(decl_file); 234 if (absolute_decl_file == null) { 235 fail("Decl file " + decl_file + " not found."); 236 } 237 238 if (absolute_decl_file.startsWith("file:")) { 239 absolute_decl_file = absolute_decl_file.substring(5); 240 } 241 242 decl_files.add(new File(absolute_decl_file)); 243 all_ppts = FileIO.read_declaration_files(decl_files); 244 245 // Setup everything to run 246 if (first_decl) { 247 Daikon.setup_proto_invs(); 248 Daikon.setup_NISuppression(); 249 first_decl = false; 250 } 251 252 ppt = null; 253 } 254 255 /** Looks up the specified ppt name and set ppt accordingly. */ 256 private void proc_ppt(String ppt_name) { 257 258 if (all_ppts == null) parse_error("decl file must be specified before ppt"); 259 ppt = all_ppts.get(ppt_name); 260 if (ppt == null) { 261 parse_error("ppt name " + ppt_name + " not found in decl file"); 262 } 263 vars = null; 264 } 265 266 /** 267 * Processes a variable list. Sets up the vars[] array to point to the matching variables in the 268 * ppt. The ppt must have been previously specified. 269 * 270 * @param var_names the variable names, separated by spaces 271 */ 272 private void proc_vars(String var_names) { 273 274 if (ppt == null) { 275 parse_error("ppt must be specified first"); 276 } 277 278 // Variable names are separated by blanks 279 String[] var_arr = var_names.split(" *"); 280 281 // The var array contains the variables in the ppt that correspond 282 // to each name specified 283 vars = new VarInfo[var_arr.length]; 284 285 // Loop through each variable name and find it in the variable list 286 for (int i = 0; i < var_arr.length; i++) { 287 String vname = var_arr[i]; 288 for (int j = 0; j < ppt.var_infos.length; j++) { 289 if (vname.equals(ppt.var_infos[j].name())) vars[i] = ppt.var_infos[j]; 290 } 291 if (vars[i] == null) parse_error("Variable " + vname + " not found in ppt " + ppt.name()); 292 } 293 } 294 295 /** 296 * Processes a line of sample data. There should be one item of data for each previously specified 297 * variable. Each data item is separated by spaces. Spaces cannot be included within a single item 298 * (i.e., strings and arrays can't include spaces). Missing items are indicated with a dash (-). 299 * Any variables not specifically mentioned in the variable string are set to missing as well. 300 * 301 * <p>Neither orig nor derived variables are added. 302 */ 303 private void proc_data(String data, LineNumberReader reader, String filename) { 304 305 if (vars == null) parse_error("vars must be specified before data"); 306 String[] da = data.split(" *"); 307 if (da.length != vars.length) parse_error("number of data elements doesn't match var elements"); 308 debug_progress.fine("data: " + Debug.toString(da)); 309 310 VarInfo[] vis = ppt.var_infos; 311 int vals_array_size = vis.length; 312 Object[] vals = new Object[vals_array_size]; 313 int[] mods = new int[vals_array_size]; 314 315 // initially all variables are missing 316 for (int i = 0; i < vals_array_size; i++) { 317 vals[i] = null; 318 mods[i] = ValueTuple.parseModified("2"); 319 } 320 321 // Parse and enter the specified variables, - indicates a missing value 322 for (int i = 0; i < vars.length; i++) { 323 if (da[i].equals("-")) { 324 continue; 325 } 326 VarInfo vi = vars[i]; 327 vals[vi.value_index] = vi.rep_type.parse_value(da[i], reader, filename); 328 mods[vi.value_index] = ValueTuple.parseModified("1"); 329 } 330 331 ValueTuple vt = ValueTuple.makeUninterned(vals, mods); 332 333 // We might want to add the following at some point. Certainly the 334 // derived variables. The orig variables force us to deal with matching 335 // enter and exit which I really don't want to do. Perhaps we can always 336 // give them the same value at enter and exit. Both of these calls 337 // are in FileIO 338 339 // compute_orig_variables (ppt, vt.vals, vt.mods, nonce); 340 // compute_derived_variables (ppt, vt.vals, vt.mods); 341 342 // Causes interning 343 vt = new ValueTuple(vt.vals, vt.mods); 344 345 ppt.add_bottom_up(vt, 1); 346 } 347 348 /** Requires that the StreamTokenizer has just read a word. Returns that word. */ 349 private String readString(StreamTokenizer stok) { 350 int ttype; 351 try { 352 ttype = stok.nextToken(); 353 } catch (IOException e) { 354 throw new UncheckedIOException(e); 355 } 356 if (ttype == TT_WORD || ttype == '"') { 357 return stok.sval; 358 } else if (ttype > 0) { 359 return String.valueOf((char) ttype); 360 } else { 361 throw new Error("Expected string. Got ttype = " + ttype); 362 } 363 } 364 365 /** Processes a single assertion. If the assertion is false, throws an error. */ 366 private void proc_assert(String assertion) throws IOException { 367 368 // Look for negation 369 boolean negate = false; 370 String assert_string = assertion; 371 if (assertion.indexOf('!') == 0) { 372 negate = true; 373 assert_string = assert_string.substring(1); 374 } 375 376 // Create a tokenizer over the assertion string 377 StreamTokenizer stok = new StreamTokenizer(new StringReader(assert_string)); 378 stok.commentChar('#'); 379 stok.quoteChar('"'); 380 381 int ttype; 382 383 // Get the assertion name 384 ttype = stok.nextToken(); 385 assertEquals(TT_WORD, ttype); 386 String name = stok.sval; 387 388 // Get the arguments (enclosed in parens, separated by commas) 389 String delimiter = readString(stok); 390 assertEquals("(", delimiter); 391 392 List<String> args = new ArrayList<>(10); 393 do { 394 String arg = readString(stok); 395 args.add(arg); 396 delimiter = readString(stok); 397 } while (delimiter.equals(",")); 398 if (!delimiter.equals(")")) { 399 parse_error(String.format("%s found where ')' expected", delimiter)); 400 } 401 402 // process the specific assertion 403 boolean result = false; 404 if (name.equals("inv")) { 405 result = proc_inv_assert(args); 406 if (!result && !negate) { 407 daikon.LogHelper.setLevel(debug, FINE); 408 proc_inv_assert(args); 409 } 410 } else if (name.equals("show_invs")) { 411 result = proc_show_invs_assert(args); 412 } else if (name.equals("constant")) { 413 result = proc_constant_assert(args); 414 } else { 415 parse_error("unknown assertion: " + name); 416 } 417 418 if (negate) { 419 result = !result; 420 } 421 422 if (!result) { 423 fail( 424 String.format( 425 "Assertion %s fails in file %s at line %d", assertion, fname, fp.getLineNumber())); 426 } 427 } 428 429 /** 430 * Processes an invariant existence assertion and returns true if it is found. The first argument 431 * should be the invariant class. The remaining arguments are the variables. This needs to be 432 * expanded to specify more information for invariants with state. 433 */ 434 private boolean proc_inv_assert(List<String> args) { 435 436 if ((args.size() < 2) || (args.size() > 4)) { 437 parse_error("bad argument count (" + args.size() + ") for invariant assertion"); 438 } 439 440 Class<?> cls = null; 441 String format = null; 442 443 // First argument is a classname or a quoted string 444 String arg0 = args.get(0); 445 try { 446 debug.fine("Looking for " + arg0); 447 @SuppressWarnings("signature") // user input (?); throws exception if fails 448 @ClassGetName String arg0_cgn = arg0; 449 cls = Class.forName(arg0_cgn); 450 } catch (Exception e) { 451 format = arg0; 452 debug.fine(String.format("Looking for format: '%s' in ppt %s", format, ppt)); 453 } 454 455 // Build a vis to match the specified variables 456 VarInfo[] vis = new VarInfo[args.size() - 1]; 457 for (int i = 0; i < vis.length; i++) { 458 vis[i] = ppt.find_var_by_name(args.get(i + 1)); 459 if (vis[i] == null) { 460 parse_error( 461 String.format("Variable '%s' not found at ppt %s", args.get(i + 1), ppt.name())); 462 } 463 } 464 PptSlice slice = ppt.findSlice(vis); 465 if (slice == null) { 466 return false; 467 } 468 469 // Look for a matching invariant in the slices invariant list 470 for (Invariant inv : slice.invs) { 471 if (inv.getClass() == cls) { 472 return true; 473 } 474 if ((format != null) && format.equals(inv.format())) { 475 return true; 476 } 477 debug.fine(String.format("trace %s: '%s'", inv.getClass(), inv.format())); 478 } 479 return false; 480 } 481 482 /** 483 * Prints out all of the invariants in the slice identified by the argumens (each of which should 484 * be a valid variable name for this ppt). always returns true. 485 */ 486 private boolean proc_show_invs_assert(List<String> args) { 487 488 if ((args.size() < 1) || (args.size() > 3)) { 489 parse_error("bad argument count (" + args.size() + ") for show_invs"); 490 } 491 492 // Build a vis to match the specified variables 493 VarInfo[] vis = new VarInfo[args.size()]; 494 for (int i = 0; i < vis.length; i++) { 495 vis[i] = ppt.find_var_by_name(args.get(i)); 496 if (vis[i] == null) { 497 parse_error(String.format("Variable '%s' not found at ppt %s", args.get(i), ppt.name())); 498 } 499 } 500 PptSlice slice = ppt.findSlice(vis); 501 if (slice == null) { 502 System.out.println("No invariants found for vars: " + Arrays.toString(vis)); 503 return true; 504 } 505 506 // Look for a matching invariant in the slices invariant list 507 for (Invariant inv : slice.invs) { 508 System.out.printf("found %s: %s%n", inv.getClass(), inv.format()); 509 } 510 return true; 511 } 512 513 /** 514 * The constant assertion returns true if all of its arguments are constants. 515 * 516 * @param args variables; must be non-empty 517 * @return true if all of the given variables are constants 518 */ 519 private boolean proc_constant_assert(List<String> args) { 520 521 if (args.size() < 1) { 522 parse_error("Must be at least one argument for constant assertion"); 523 } 524 525 for (String arg : args) { 526 VarInfo v = ppt.find_var_by_name(arg); 527 if (v == null) { 528 parse_error(String.format("Variable '%s' not found at ppt %s", arg, ppt.name())); 529 } 530 if (!ppt.constants.is_constant(v)) { 531 return false; 532 } 533 } 534 return true; 535 } 536 537 private void parse_error(String msg) { 538 539 fail(String.format("Error parsing %s at line %d: %s", fname, fp.getLineNumber(), msg)); 540 } 541}