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}