001package daikon.tools;
002
003import static java.util.logging.Level.FINE;
004import static java.util.logging.Level.INFO;
005
006import daikon.Daikon;
007import daikon.Debug;
008import daikon.FileIO;
009import daikon.Global;
010import daikon.PptConditional;
011import daikon.PptMap;
012import daikon.PptSlice;
013import daikon.PptTopLevel;
014import daikon.ValueTuple;
015import daikon.VarInfo;
016import daikon.inv.Invariant;
017import daikon.inv.InvariantStatus;
018import daikon.inv.filter.InvariantFilters;
019import daikon.split.PptSplitter;
020import gnu.getopt.*;
021import java.io.File;
022import java.io.FileNotFoundException;
023import java.io.FileOutputStream;
024import java.io.IOException;
025import java.io.OptionalDataException;
026import java.io.PrintStream;
027import java.io.StreamCorruptedException;
028import java.util.ArrayList;
029import java.util.HashSet;
030import java.util.LinkedHashMap;
031import java.util.LinkedHashSet;
032import java.util.List;
033import java.util.Map;
034import java.util.logging.Logger;
035import org.checkerframework.checker.mustcall.qual.Owning;
036import org.checkerframework.checker.nullness.qual.Nullable;
037import org.checkerframework.checker.nullness.qual.RequiresNonNull;
038import org.plumelib.util.StringsPlume;
039
040/**
041 * InvariantChecker reads an invariant file and trace file. It prints errors for any invariants that
042 * are violated by the trace file.
043 */
044public class InvariantChecker {
045  private InvariantChecker() {
046    throw new Error("do not instantiate");
047  }
048
049  public static final Logger debug = Logger.getLogger("daikon.tools.InvariantChecker");
050
051  public static final Logger debug_detail = Logger.getLogger("daikon.tools.InvariantCheckerDetail");
052
053  private static final String output_SWITCH = "output";
054  private static final String dir_SWITCH = "dir";
055  private static final String conf_SWITCH = "conf";
056  private static final String filter_SWITCH = "filter";
057  private static final String verbose_SWITCH = "verbose";
058
059  /** The usage message for this program. */
060  private static String usage =
061      StringsPlume.joinLines(
062          "Usage: java daikon.InvariantChecker [OPTION]... <inv_file> <dtrace_file>",
063          "  -h, --" + Daikon.help_SWITCH,
064          "      Display this usage message",
065          "  --" + output_SWITCH + " output file",
066          "  --" + conf_SWITCH,
067          "      Checks only invariants that are above the default confidence level",
068          "  --" + filter_SWITCH,
069          "      Checks only invariants that are not filtered by the default filters",
070          "  --" + dir_SWITCH + " directory with invariant and dtrace files",
071          "      We output how many invariants failed for each invariant file. We check for"
072              + " failure against any sample in any dtrace file.",
073          "  --" + verbose_SWITCH + " print all failing samples",
074          "  --" + Daikon.config_option_SWITCH + " config_var=val",
075          "      Sets the specified configuration variable.  ",
076          "  --" + Daikon.debugAll_SWITCH,
077          "      Turns on all debug flags (voluminous output)",
078          "  --" + Daikon.debug_SWITCH + " logger",
079          "      Turns on the specified debug logger",
080          "  --" + Daikon.track_SWITCH + " class<var1,var2,var3>@ppt",
081          "      Print debug info on the specified invariant class, vars, and ppt");
082
083  public static List<String> dtrace_files = new ArrayList<>();
084  static @Owning PrintStream output_stream = System.out;
085  static int error_cnt = 0;
086  static int sample_cnt = 0;
087
088  static @Nullable File dir_file; // Yoav added
089  static boolean doFilter;
090  static boolean doConf;
091  static boolean quiet = true;
092  static HashSet<Invariant> failedInvariants = new HashSet<>(); // Yoav added
093  static HashSet<Invariant> testedInvariants = new HashSet<>(); // Yoav added
094  static HashSet<Invariant> activeInvariants = new HashSet<>(); // Yoav added
095  static LinkedHashSet<String> outputComma = new LinkedHashSet<>(); // Yoav added
096
097  public static void main(String[] args)
098      throws FileNotFoundException,
099          StreamCorruptedException,
100          OptionalDataException,
101          IOException,
102          ClassNotFoundException {
103    try {
104      if (args.length == 0) {
105        throw new Daikon.UserError(usage);
106      }
107      mainHelper(args);
108    } catch (Daikon.DaikonTerminationException e) {
109      Daikon.handleDaikonTerminationException(e);
110    }
111  }
112
113  /**
114   * This does the work of {@link #main(String[])}, but it never calls System.exit, so it is
115   * appropriate to be called progrmmatically.
116   *
117   * @param args command-line arguments, like those of {@link #main}
118   */
119  public static void mainHelper(final String[] args)
120      throws FileNotFoundException,
121          StreamCorruptedException,
122          OptionalDataException,
123          IOException,
124          ClassNotFoundException {
125    daikon.LogHelper.setupLogs(INFO);
126
127    LongOpt[] longopts =
128        new LongOpt[] {
129          new LongOpt(Daikon.config_option_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0),
130          new LongOpt(output_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0),
131          new LongOpt(dir_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0),
132          new LongOpt(conf_SWITCH, LongOpt.NO_ARGUMENT, null, 0),
133          new LongOpt(filter_SWITCH, LongOpt.NO_ARGUMENT, null, 0),
134          new LongOpt(verbose_SWITCH, LongOpt.NO_ARGUMENT, null, 0),
135          new LongOpt(Daikon.debugAll_SWITCH, LongOpt.NO_ARGUMENT, null, 0),
136          new LongOpt(Daikon.debug_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0),
137          new LongOpt(Daikon.ppt_regexp_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0),
138          new LongOpt(Daikon.track_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0),
139        };
140    Getopt g = new Getopt("daikon.tools.InvariantChecker", args, "h", longopts);
141    int c;
142    while ((c = g.getopt()) != -1) {
143      switch (c) {
144        case 0:
145          // got a long option
146          String option_name = longopts[g.getLongind()].getName();
147          if (Daikon.help_SWITCH.equals(option_name)) {
148            System.out.println(usage);
149            throw new Daikon.NormalTermination();
150          } else if (conf_SWITCH.equals(option_name)) {
151            doConf = true;
152          } else if (filter_SWITCH.equals(option_name)) {
153            doFilter = true;
154          } else if (verbose_SWITCH.equals(option_name)) {
155            quiet = false;
156          } else if (dir_SWITCH.equals(option_name)) {
157            dir_file = new File(Daikon.getOptarg(g));
158            if (!dir_file.exists() || !dir_file.isDirectory()) {
159              throw new Daikon.UserError("Error reading the directory " + dir_file);
160            }
161
162          } else if (output_SWITCH.equals(option_name)) {
163            File output_file = new File(Daikon.getOptarg(g));
164            output_stream = new PrintStream(new FileOutputStream(output_file));
165          } else if (Daikon.config_option_SWITCH.equals(option_name)) {
166            String item = Daikon.getOptarg(g);
167            daikon.config.Configuration.getInstance().apply(item);
168            break;
169          } else if (Daikon.debugAll_SWITCH.equals(option_name)) {
170            Global.debugAll = true;
171          } else if (Daikon.debug_SWITCH.equals(option_name)) {
172            daikon.LogHelper.setLevel(Daikon.getOptarg(g), FINE);
173          } else if (Daikon.track_SWITCH.equals(option_name)) {
174            daikon.LogHelper.setLevel("daikon.Debug", FINE);
175            String error = Debug.add_track(Daikon.getOptarg(g));
176            if (error != null) {
177              throw new Daikon.UserError(
178                  "Error parsing track argument '" + Daikon.getOptarg(g) + "' - " + error);
179            }
180          } else {
181            throw new RuntimeException("Unknown long option received: " + option_name);
182          }
183          break;
184        case 'h':
185          System.out.println(usage);
186          throw new Daikon.NormalTermination();
187        case '?':
188          break; // getopt() already printed an error
189        default:
190          System.out.println("getopt() returned " + c);
191          break;
192      }
193    }
194
195    {
196      File inv_file = null;
197
198      // Loop through each filename specified
199      for (int i = g.getOptind(); i < args.length; i++) {
200
201        // Get the file and make sure it exists
202        File file = new File(args[i]);
203        if (!file.exists()) {
204          throw new Error("File " + file + " not found.");
205        }
206
207        // These aren't "endsWith()" because there might be a suffix on the end
208        // (eg, a date).
209        String filename = file.toString();
210        if (filename.indexOf(".inv") != -1) {
211          if (inv_file != null) {
212            throw new Daikon.UserError("multiple inv files specified" + Global.lineSep + usage);
213          }
214          inv_file = file;
215        } else if (filename.indexOf(".dtrace") != -1) {
216          dtrace_files.add(filename);
217        } else {
218          throw new Error("Unrecognized argument: " + file);
219        }
220      }
221      if (dir_file == null) {
222        if (inv_file == null) {
223          throw new Daikon.UserError("No inv file specified" + Global.lineSep + usage);
224        }
225        checkInvariants(inv_file);
226        return;
227      }
228    }
229
230    // Yoav additions:
231    File[] filesInDir = dir_file.listFiles();
232    if (filesInDir == null || filesInDir.length == 0) {
233      throw new Daikon.UserError(
234          "The directory " + dir_file + " is empty" + Global.lineSep + usage);
235    }
236    ArrayList<File> invariants = new ArrayList<>();
237    for (File f : filesInDir) {
238      if (f.toString().indexOf(".inv") != -1) {
239        invariants.add(f);
240      }
241    }
242    if (invariants.size() == 0) {
243      throw new Daikon.UserError(
244          "Did not find any invariant files in the directory " + dir_file + Global.lineSep + usage);
245    }
246    ArrayList<File> dtraces = new ArrayList<>();
247    for (File f : filesInDir) {
248      if (f.toString().indexOf(".dtrace") != -1) {
249        dtraces.add(f);
250      }
251    }
252    if (dtraces.size() == 0) {
253      throw new Daikon.UserError(
254          "Did not find any dtrace files in the directory " + dir_file + Global.lineSep + usage);
255    }
256
257    System.out.println(
258        "Collecting data for invariants files " + invariants + " and dtrace files " + dtraces);
259
260    dtrace_files.clear();
261    for (File dtrace : dtraces) {
262      dtrace_files.add(dtrace.toString());
263    }
264
265    String commaLine = "";
266    for (File inFile : invariants) {
267      String name = inFile.getName().replace(".inv", "").replace(".gz", "");
268      commaLine += "," + name;
269    }
270    outputComma.add(commaLine);
271
272    commaLine = "";
273    for (File inFile : invariants) {
274      File inv_file = inFile;
275      failedInvariants.clear();
276      testedInvariants.clear();
277      error_cnt = 0;
278
279      output_stream =
280          new PrintStream(
281              new FileOutputStream(
282                  inFile.toString().replace(".inv", "").replace(".gz", "")
283                      + ".false-positives.txt"));
284      checkInvariants(inv_file);
285      output_stream.close();
286
287      int failedCount = failedInvariants.size();
288      int testedCount = testedInvariants.size();
289      String percent = toPercentage(failedCount, testedCount);
290      commaLine += "," + percent;
291    }
292    outputComma.add(commaLine);
293
294    System.out.println();
295    for (String output : outputComma) {
296      System.out.println(output);
297    }
298  }
299
300  private static String toPercentage(int portion, int total) {
301    double s = portion * 100;
302    return String.format("%.2f", s / total) + "%";
303  }
304
305  private static void checkInvariants(File inv_file) throws IOException {
306    // Read the invariant file
307    PptMap ppts = FileIO.read_serialized_pptmap(inv_file, true);
308
309    // Yoav: make sure we have unique invariants
310    InvariantFilters fi = InvariantFilters.defaultFilters();
311    // Set<String> allInvariantsStr = new HashSet<>();
312    // Set<Invariant> allInvariants = new HashSet<>();
313    for (PptTopLevel ppt : ppts.all_ppts()) {
314      for (PptSlice slice : ppt.views_iterable()) {
315        for (Invariant inv : slice.invs) {
316          if (doConf && inv.getConfidence() < Invariant.dkconfig_confidence_limit) {
317            // System.out.printf("inv ignored (conf): %s:%s%n", inv.ppt.name(),
318            //                   inv.format());
319            continue;
320          }
321
322          if (doFilter && fi.shouldKeep(inv) == null) {
323            // System.out.printf("inv ignored (filter): %s:%s%n",
324            //                     inv.ppt.name(), inv.format());
325            continue;
326          }
327          activeInvariants.add(inv);
328
329          // String n = invariant2str(ppt, inv);
330          // if (!allInvariants.contains(inv) && allInvariantsStr.contains(n)) {
331          //   throw new
332          //     Daikon.UserError("Two invariants have the same ppt.name+inv.rep:"+n);
333          // }
334          // allInvariants.add(inv);
335          // allInvariantsStr.add(n);
336        }
337      }
338    }
339
340    // Read and process the data trace files
341    FileIO.Processor processor = new InvariantCheckProcessor();
342
343    Daikon.FileIOProgress progress = new Daikon.FileIOProgress();
344    progress.start();
345    progress.clear();
346    FileIO.read_data_trace_files(dtrace_files, ppts, processor, false);
347    progress.shouldStop = true;
348    System.out.println();
349    System.out.printf(
350        "%s: %,d errors found in %,d samples (%s)%n",
351        inv_file, error_cnt, sample_cnt, toPercentage(error_cnt, sample_cnt));
352    int failedCount = failedInvariants.size();
353    int testedCount = testedInvariants.size();
354    String percent = toPercentage(failedCount, testedCount);
355    System.out.println(
356        inv_file
357            + ": "
358            + failedCount
359            + " false positives, out of "
360            + testedCount
361            + ", which is "
362            + percent
363            + ".");
364    if (false) {
365      for (Invariant inv : failedInvariants) {
366        System.out.printf("+%s:%s%n", inv.ppt.name(), inv.format());
367      }
368    }
369  }
370
371  /** Class to track matching ppt and its values. */
372  static final class EnterCall {
373
374    public PptTopLevel ppt;
375    public ValueTuple vt;
376
377    public EnterCall(PptTopLevel ppt, ValueTuple vt) {
378
379      this.ppt = ppt;
380      this.vt = vt;
381    }
382  }
383
384  public static class InvariantCheckProcessor extends FileIO.Processor {
385
386    Map<Integer, EnterCall> call_map = new LinkedHashMap<>();
387
388    /**
389     * process the sample by checking it against each existing invariant and issuing an error if any
390     * invariant is falsified or weakened.
391     */
392    @RequiresNonNull("daikon.FileIO.data_trace_state")
393    @Override
394    public void process_sample(
395        PptMap all_ppts, PptTopLevel ppt, ValueTuple vt, @Nullable Integer nonce) {
396
397      debug.fine("processing sample from: " + ppt.name);
398
399      // Add orig and derived variables
400      FileIO.compute_orig_variables(ppt, vt.vals, vt.mods, nonce);
401      FileIO.compute_derived_variables(ppt, vt.vals, vt.mods);
402
403      // Intern the sample
404      vt = new ValueTuple(vt.vals, vt.mods);
405
406      // If this is an enter point, just remember it for later
407      if (ppt.ppt_name.isEnterPoint()) {
408        assert nonce != null : "@AssumeAssertion(nullness): nonce exists for enter & exit points";
409        if (dir_file != null) {
410          // Yoav: I had to do a hack to handle the case that several dtrace files are concatenated
411          // together, and Sung's dtrace files have unterminated calls, and when concatenating two
412          // files you can have the same nonce.
413          // So I have to remove the nonce found from the call_map.
414          call_map.remove(nonce);
415        } else {
416          assert call_map.get(nonce) == null;
417        }
418        call_map.put(nonce, new EnterCall(ppt, vt));
419        debug.fine("Skipping enter sample");
420        return;
421      }
422
423      // If this is an exit point, process the saved enter point
424      if (ppt.ppt_name.isExitPoint()) {
425        assert nonce != null : "@AssumeAssertion(nullness): nonce exists for enter & exit points";
426        EnterCall ec = call_map.get(nonce);
427        if (ec != null) {
428          call_map.remove(nonce);
429          debug.fine("Processing enter sample from " + ec.ppt.name);
430          add(ec.ppt, ec.vt, all_ppts);
431        } else { // didn't find the enter
432          if (!quiet) {
433            System.out.printf("couldn't find enter for nonce %d at ppt %s%n", nonce, ppt.name());
434          }
435          return;
436        }
437      }
438
439      add(ppt, vt, all_ppts);
440    }
441
442    @RequiresNonNull("daikon.FileIO.data_trace_state")
443    private void add(PptTopLevel ppt, ValueTuple vt, PptMap all_ppts) {
444      // Add the sample to any splitters
445      if (ppt.has_splitters()) {
446        assert ppt.splitters != null; // because ppt.has_splitters() = true
447        for (PptSplitter ppt_split : ppt.splitters) {
448          PptConditional ppt_cond = ppt_split.choose_conditional(vt);
449          if (ppt_cond != null) {
450            add(ppt_cond, vt, all_ppts);
451          } else {
452            debug.fine(": sample doesn't pick conditional");
453          }
454        }
455      }
456
457      // if this is a numbered exit, apply to the combined exit as well
458      if (!(ppt instanceof PptConditional) && ppt.ppt_name.isNumberedExitPoint()) {
459        PptTopLevel parent = all_ppts.get(ppt.ppt_name.makeExit());
460        if (parent != null) {
461          parent.get_missingOutOfBounds(ppt, vt);
462          add(parent, vt, all_ppts);
463        }
464      }
465
466      // If the point has no variables, skip it
467      if (ppt.var_infos.length == 0) {
468        return;
469      }
470
471      // We should have received sample here before, or there is nothing to check.
472      // Yoav added: It can be that the different dtrace and inv files have different program points
473      // if (false && ppt.num_samples() <= 0) {
474      //   assert ppt.num_samples() > 0
475      //       : "ppt " + ppt.name + " has 0 samples and " + ppt.var_infos.length + " variables";
476      // }
477
478      // Loop through each slice
479      slice_loop:
480      for (PptSlice slice : ppt.views_iterable()) {
481        if (debug_detail.isLoggable(FINE)) {
482          debug_detail.fine(
483              ": processing slice " + slice + "vars: " + Debug.toString(slice.var_infos, vt));
484        }
485
486        // If any variables are missing, skip this slice
487        for (int j = 0; j < slice.var_infos.length; j++) {
488          VarInfo v = slice.var_infos[j];
489          if (v.isMissing(vt)) {
490            if (debug_detail.isLoggable(FINE)) {
491              debug_detail.fine(": : Skipping slice, " + v.name() + " missing");
492            }
493            continue slice_loop;
494          }
495          if (v.missingOutOfBounds()) {
496            if (debug_detail.isLoggable(FINE)) {
497              debug.fine(": : Skipping slice, " + v.name() + " out of bounds");
498            }
499            continue slice_loop;
500          }
501        }
502
503        // Loop through each invariant
504        for (Invariant inv : slice.invs) {
505          if (debug_detail.isLoggable(FINE)) {
506            debug_detail.fine(": : Processing invariant: " + inv);
507          }
508          if (!inv.isActive()) {
509            if (debug_detail.isLoggable(FINE)) {
510              debug_detail.fine(": : skipped non-active " + inv);
511            }
512            continue;
513          }
514
515          // Yoav added
516          if (!activeInvariants.contains(inv)) {
517            // System.out.printf("skipping invariant %s:%s%n", inv.ppt.name(),
518            //                   inv.format());
519            continue;
520          }
521
522          // String invRep = invariant2str(ppt, inv);
523          testedInvariants.add(inv);
524
525          // Store string representation of original invariant for verbose mode
526          String invRep = quiet ? null : inv.format();
527
528          InvariantStatus status = inv.add_sample(vt, 1);
529          sample_cnt++;
530          if (status != InvariantStatus.NO_CHANGE) {
531            if (!quiet) {
532              output_stream.println(
533                  "At ppt "
534                      + ppt.name
535                      + ", Invariant '"
536                      + invRep
537                      + "' invalidated by sample "
538                      + Debug.toString(slice.var_infos, vt)
539                      + "at line "
540                      + FileIO.get_linenum()
541                      + " in file "
542                      + FileIO.data_trace_state.filename);
543            }
544            failedInvariants.add(inv);
545            activeInvariants.remove(inv);
546            error_cnt++;
547          }
548        }
549      }
550    }
551  }
552
553  @SuppressWarnings("UnusedMethod") // for debugging (which is currently commented out)
554  private static String invariant2str(PptTopLevel ppt, Invariant inv) {
555    return ppt.name + " == " + inv.repr() + inv.getClass() + inv.varNames() + ": " + inv.format();
556  }
557}