Source code

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