Source code

001package daikon.diff;
002
003import static java.util.logging.Level.FINE;
004import static java.util.logging.Level.INFO;
005
006import daikon.Daikon;
007import daikon.FileIO;
008import daikon.Ppt;
009import daikon.PptConditional;
010import daikon.PptMap;
011import daikon.PptTopLevel;
012import daikon.inv.Invariant;
013import gnu.getopt.Getopt;
014import gnu.getopt.LongOpt;
015import java.io.File;
016import java.io.FileNotFoundException;
017import java.io.IOException;
018import java.io.OptionalDataException;
019import java.io.StreamCorruptedException;
020import java.lang.reflect.InvocationTargetException;
021import java.util.ArrayList;
022import java.util.Collections;
023import java.util.Comparator;
024import java.util.Iterator;
025import java.util.List;
026import java.util.NavigableSet;
027import java.util.TreeSet;
028import java.util.logging.Logger;
029import org.checkerframework.checker.initialization.qual.UnknownInitialization;
030import org.checkerframework.checker.nullness.qual.EnsuresNonNull;
031import org.checkerframework.checker.nullness.qual.Nullable;
032import org.checkerframework.checker.signature.qual.ClassGetName;
033import org.plumelib.util.CollectionsPlume;
034import org.plumelib.util.FilesPlume;
035import org.plumelib.util.MPair;
036import org.plumelib.util.OrderedPairIterator;
037import org.plumelib.util.StringsPlume;
038
039/**
040 * Diff is the main class for the invariant diff program. The invariant diff program outputs the
041 * differences between two sets of invariants.
042 *
043 * <p>The following is a high-level description of the program. Each input file contains a
044 * serialized PptMap or InvMap. PptMap and InvMap are similar structures, in that they both map
045 * program points to invariants. However, PptMaps are much more complicated than InvMaps. PptMaps
046 * are output by Daikon, and InvMaps are output by this program.
047 *
048 * <p>First, if either input is a PptMap, it is converted to an InvMap. Next, the two InvMaps are
049 * combined to form a tree. The tree is exactly three levels deep. The first level contains the
050 * root, which holds no data. Each node in the second level is a pair of Ppts, and each node in the
051 * third level is a pair of Invariants. The tree is constructed by pairing the corresponding Ppts
052 * and Invariants in the two PptMaps. Finally, the tree is traversed via the Visitor pattern to
053 * produce output. The Visitor pattern makes it easy to extend the program, simply by writing a new
054 * Visitor.
055 */
056public final class Diff {
057
058  /** Debug logger. */
059  public static final Logger debug = Logger.getLogger("daikon.diff.Diff");
060
061  /** The usage message for this program. */
062  private static String usage =
063      StringsPlume.joinLines(
064          "Usage:",
065          "    java daikon.diff.Diff [flags...] file1 [file2]",
066          "  file1 and file2 are serialized invariants produced by Daikon.",
067          "  If file2 is not specified, file1 is compared with the empty set.",
068          "  For a list of flags, see the Daikon manual, which appears in the ",
069          "  Daikon distribution and also at http://plse.cs.washington.edu/daikon/.");
070
071  /** The long command line options. */
072  private static final String HELP_SWITCH = "help";
073
074  private static final String INV_SORT_COMPARATOR1_SWITCH = "invSortComparator1";
075  private static final String INV_SORT_COMPARATOR2_SWITCH = "invSortComparator2";
076  private static final String INV_PAIR_COMPARATOR_SWITCH = "invPairComparator";
077  private static final String IGNORE_UNJUSTIFIED_SWITCH = "ignore_unjustified";
078  private static final String IGNORE_NUMBERED_EXITS_SWITCH = "ignore_exitNN";
079
080  /** Determine which ppts should be paired together in the tree. */
081  private static final Comparator<PptTopLevel> PPT_COMPARATOR = new Ppt.NameComparator();
082
083  /**
084   * Comparators to sort the sets of invs, and to combine the two sets into the pair tree. Can be
085   * overriden by command-line options.
086   */
087  private Comparator<Invariant> invSortComparator1;
088
089  private Comparator<Invariant> invSortComparator2;
090  private Comparator<Invariant> invPairComparator;
091
092  private boolean examineAllPpts;
093  private boolean ignoreNumberedExits;
094
095  public Diff() {
096    this(false, false);
097  }
098
099  public Diff(boolean examineAllPpts) {
100    this(examineAllPpts, false);
101  }
102
103  public Diff(boolean examineAllPpts, Comparator<Invariant> c) {
104    this(examineAllPpts, false);
105    setAllInvComparators(c);
106  }
107
108  public Diff(boolean examineAllPpts, boolean ignoreNumberedExits) {
109    this.examineAllPpts = examineAllPpts;
110    this.ignoreNumberedExits = ignoreNumberedExits;
111    setAllInvComparators(new Invariant.ClassVarnameComparator());
112  }
113
114  public Diff(
115      boolean examineAllPpts,
116      boolean ignoreNumberedExits,
117      @Nullable @ClassGetName String invSortComparator1Classname,
118      @Nullable @ClassGetName String invSortComparator2Classname,
119      @Nullable @ClassGetName String invPairComparatorClassname,
120      Comparator<Invariant> defaultComparator)
121      throws ClassNotFoundException,
122          IllegalAccessException,
123          InstantiationException,
124          InvocationTargetException,
125          NoSuchMethodException {
126    this.examineAllPpts = examineAllPpts;
127    this.ignoreNumberedExits = ignoreNumberedExits;
128    this.invSortComparator1 = selectComparator(invSortComparator1Classname, defaultComparator);
129    this.invSortComparator2 = selectComparator(invSortComparator2Classname, defaultComparator);
130    this.invPairComparator = selectComparator(invPairComparatorClassname, defaultComparator);
131  }
132
133  /**
134   * Read two PptMap or InvMap objects from their respective files. Convert the PptMaps to InvMaps
135   * as necessary, and diff the InvMaps.
136   */
137  public static void main(String[] args)
138      throws FileNotFoundException,
139          StreamCorruptedException,
140          OptionalDataException,
141          IOException,
142          ClassNotFoundException,
143          IllegalAccessException,
144          InstantiationException,
145          InvocationTargetException,
146          NoSuchMethodException {
147    try {
148      mainHelper(args);
149    } catch (Daikon.DaikonTerminationException e) {
150      daikon.Daikon.handleDaikonTerminationException(e);
151    }
152  }
153
154  /**
155   * This does the work of {@link #main(String[])}, but it never calls System.exit, so it is
156   * appropriate to be called progrmmatically.
157   */
158  public static void mainHelper(final String[] args)
159      throws FileNotFoundException,
160          StreamCorruptedException,
161          OptionalDataException,
162          IOException,
163          ClassNotFoundException,
164          InstantiationException,
165          IllegalAccessException,
166          InvocationTargetException,
167          NoSuchMethodException {
168    daikon.LogHelper.setupLogs(INFO);
169
170    boolean printDiff = false;
171    boolean printAll = false;
172    boolean includeUnjustified = true;
173    boolean stats = false;
174    boolean tabSeparatedStats = false;
175    boolean minus = false;
176    boolean xor = false;
177    boolean union = false;
178    boolean examineAllPpts = false;
179    boolean ignoreNumberedExits = false;
180    boolean printEmptyPpts = false;
181    boolean verbose = false;
182    boolean continuousJustification = false;
183    boolean logging = false;
184    File outputFile = null;
185    @ClassGetName String invSortComparator1Classname = null;
186    @ClassGetName String invSortComparator2Classname = null;
187    @ClassGetName String invPairComparatorClassname = null;
188
189    boolean optionSelected = false;
190
191    daikon.LogHelper.setupLogs(INFO);
192    //     daikon.LogHelper.setLevel ("daikon.diff", FINE);
193
194    LongOpt[] longOpts =
195        new LongOpt[] {
196          new LongOpt(HELP_SWITCH, LongOpt.NO_ARGUMENT, null, 0),
197          new LongOpt(INV_SORT_COMPARATOR1_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0),
198          new LongOpt(INV_SORT_COMPARATOR2_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0),
199          new LongOpt(INV_PAIR_COMPARATOR_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0),
200          new LongOpt(IGNORE_UNJUSTIFIED_SWITCH, LongOpt.NO_ARGUMENT, null, 0),
201          new LongOpt(IGNORE_NUMBERED_EXITS_SWITCH, LongOpt.NO_ARGUMENT, null, 0),
202        };
203
204    Getopt g =
205        new Getopt(
206            "daikon.diff.Diff", args,
207            "Hhyduastmxno:jzpevl", longOpts);
208    int c;
209    while ((c = g.getopt()) != -1) {
210      switch (c) {
211        case 0:
212          // got a long option
213          String optionName = longOpts[g.getLongind()].getName();
214          if (Daikon.help_SWITCH.equals(optionName)) {
215            System.out.println(usage);
216            throw new Daikon.NormalTermination();
217          } else if (INV_SORT_COMPARATOR1_SWITCH.equals(optionName)) {
218            if (invSortComparator1Classname != null) {
219              throw new Error(
220                  "multiple --"
221                      + INV_SORT_COMPARATOR1_SWITCH
222                      + " classnames supplied on command line");
223            }
224            @SuppressWarnings("signature") // user input, should be checked
225            @ClassGetName String cgn = Daikon.getOptarg(g);
226            invSortComparator1Classname = cgn;
227          } else if (INV_SORT_COMPARATOR2_SWITCH.equals(optionName)) {
228            if (invSortComparator2Classname != null) {
229              throw new Error(
230                  "multiple --"
231                      + INV_SORT_COMPARATOR2_SWITCH
232                      + " classnames supplied on command line");
233            }
234            @SuppressWarnings("signature") // user input, should be checked
235            @ClassGetName String cgn = Daikon.getOptarg(g);
236            invSortComparator2Classname = cgn;
237          } else if (INV_PAIR_COMPARATOR_SWITCH.equals(optionName)) {
238            if (invPairComparatorClassname != null) {
239              throw new Error(
240                  "multiple --"
241                      + INV_PAIR_COMPARATOR_SWITCH
242                      + " classnames supplied on command line");
243            }
244            @SuppressWarnings("signature") // user input, should be checked
245            @ClassGetName String cgn = Daikon.getOptarg(g);
246            invPairComparatorClassname = cgn;
247          } else if (IGNORE_UNJUSTIFIED_SWITCH.equals(optionName)) {
248            optionSelected = true;
249            includeUnjustified = false;
250            break;
251          } else if (IGNORE_NUMBERED_EXITS_SWITCH.equals(optionName)) {
252            ignoreNumberedExits = true;
253            break;
254          } else {
255            throw new RuntimeException("Unknown long option received: " + optionName);
256          }
257          break;
258        case 'h':
259          System.out.println(usage);
260          throw new Daikon.NormalTermination();
261        case 'H':
262          PrintAllVisitor.HUMAN_OUTPUT = true;
263          break;
264        case 'y': // included for legacy code
265          optionSelected = true;
266          includeUnjustified = false;
267          break;
268        case 'd':
269          optionSelected = true;
270          printDiff = true;
271          break;
272        case 'a':
273          optionSelected = true;
274          printAll = true;
275          break;
276        case 's':
277          optionSelected = true;
278          stats = true;
279          break;
280        case 't':
281          optionSelected = true;
282          tabSeparatedStats = true;
283          break;
284        case 'm':
285          optionSelected = true;
286          minus = true;
287          break;
288        case 'x':
289          optionSelected = true;
290          xor = true;
291          break;
292        case 'n':
293          optionSelected = true;
294          union = true;
295          break;
296        case 'o':
297          if (outputFile != null) {
298            throw new Error("multiple output files supplied on command line");
299          }
300          String outputFilename = Daikon.getOptarg(g);
301          outputFile = new File(outputFilename);
302          if (!FilesPlume.canCreateAndWrite(outputFile)) {
303            throw new Error("Cannot write to file " + outputFile);
304          }
305          break;
306        case 'j':
307          continuousJustification = true;
308          break;
309        case 'p':
310          examineAllPpts = true;
311          break;
312        case 'e':
313          printEmptyPpts = true;
314          break;
315        case 'v':
316          verbose = true;
317          break;
318        case 'l':
319          logging = true;
320          break;
321        case '?':
322          // getopt() already printed an error
323          System.out.println(usage);
324          throw new Daikon.UserError("Bad argument");
325        default:
326          System.out.println("getopt() returned " + c);
327          break;
328      }
329    }
330
331    // Turn on the defaults
332    if (!optionSelected) {
333      printDiff = true;
334    }
335
336    if (logging) {
337      System.err.println("Invariant Diff: Starting Log");
338    }
339
340    if (logging) {
341      System.err.println("Invariant Diff: Creating Diff Object");
342    }
343
344    Comparator<Invariant> defaultComparator;
345    if (minus || xor || union) {
346      defaultComparator = new Invariant.ClassVarnameFormulaComparator();
347    } else {
348      defaultComparator = new Invariant.ClassVarnameComparator();
349    }
350
351    // Set the comparators based on the command-line options
352
353    Diff diff =
354        new Diff(
355            examineAllPpts,
356            ignoreNumberedExits,
357            invSortComparator1Classname,
358            invSortComparator2Classname,
359            invPairComparatorClassname,
360            defaultComparator);
361
362    if (!diff.invSortComparator1
363            .getClass()
364            .toString()
365            .equals(diff.invSortComparator2.getClass().toString())
366        || !diff.invSortComparator1
367            .getClass()
368            .toString()
369            .equals(diff.invPairComparator.getClass().toString())) {
370      System.out.println("You are using different comparators to sort or pair up invariants.");
371      System.out.println("This may cause misalignment of invariants and may cause Diff to");
372      System.out.println("work incorectly.  Make sure you know what you are doing!");
373    }
374
375    // The index of the first non-option argument -- the name of the
376    // first file
377    int firstFileIndex = g.getOptind();
378    int numFiles = args.length - firstFileIndex;
379
380    InvMap invMap1 = null;
381    InvMap invMap2 = null;
382
383    if (logging) {
384      System.err.println("Invariant Diff: Reading Files");
385    }
386
387    if (numFiles == 1) {
388      String filename1 = args[firstFileIndex];
389      invMap1 = diff.readInvMap(new File(filename1));
390      invMap2 = new InvMap();
391    } else if (numFiles == 2) {
392      String filename1 = args[firstFileIndex];
393      String filename2 = args[firstFileIndex + 1];
394      invMap1 = diff.readInvMap(new File(filename1));
395      invMap2 = diff.readInvMap(new File(filename2));
396    } else if (numFiles > 2) {
397
398      // The new stuff that allows multiple files -LL
399
400      PptMap[] mapAr = new PptMap[numFiles];
401      int j = 0;
402      for (int i = firstFileIndex; i < args.length; i++) {
403        String fileName = args[i];
404        mapAr[j++] = FileIO.read_serialized_pptmap(new File(fileName), false);
405      }
406
407      // Cascade a lot of the different invariants into one map,
408      // and then put them into map1, map2
409
410      // Initialize it all
411      MultiDiffVisitor v1 = new MultiDiffVisitor(mapAr[0]);
412
413      for (int i = 1; i < mapAr.length; i++) {
414        RootNode root = diff.diffPptMap(mapAr[i], v1.currMap, includeUnjustified);
415        root.accept(v1);
416      }
417
418      // now take the final result for the MultiDiffVisitor
419      // and use it along side a null empty map
420      // PptMap map1 = v1.currMap;
421
422      v1.printAll();
423      return;
424    } else {
425      System.out.println(usage);
426      throw new Daikon.NormalTermination();
427    }
428
429    if (logging) {
430      System.err.println("Invariant Diff: Creating Tree");
431    }
432
433    if (logging) {
434      System.err.println("Invariant Diff: Visiting Tree");
435    }
436
437    RootNode root = diff.diffInvMap(invMap1, invMap2, includeUnjustified);
438
439    if (stats) {
440      DetailedStatisticsVisitor v = new DetailedStatisticsVisitor(continuousJustification);
441      root.accept(v);
442      System.out.print(v.format());
443    }
444
445    if (tabSeparatedStats) {
446      DetailedStatisticsVisitor v = new DetailedStatisticsVisitor(continuousJustification);
447      root.accept(v);
448      System.out.print(v.repr());
449    }
450
451    if (printDiff) {
452      PrintDifferingInvariantsVisitor v =
453          new PrintDifferingInvariantsVisitor(System.out, verbose, printEmptyPpts);
454      root.accept(v);
455    }
456
457    if (printAll) {
458      PrintAllVisitor v = new PrintAllVisitor(System.out, verbose, printEmptyPpts);
459      root.accept(v);
460    }
461
462    if (minus) {
463      if (outputFile != null) {
464        MinusVisitor v = new MinusVisitor();
465        root.accept(v);
466        FilesPlume.writeObject(v.getResult(), outputFile);
467        // System.out.println("Output written to: " + outputFile);
468      } else {
469        throw new Error("no output file specified on command line");
470      }
471    }
472
473    if (xor) {
474      if (outputFile != null) {
475        XorVisitor v = new XorVisitor();
476        root.accept(v);
477        InvMap resultMap = v.getResult();
478        FilesPlume.writeObject(resultMap, outputFile);
479        if (debug.isLoggable(FINE)) {
480          debug.fine("Result: " + resultMap.toString());
481        }
482
483        // System.out.println("Output written to: " + outputFile);
484      } else {
485        throw new Error("no output file specified on command line");
486      }
487    }
488
489    if (union) {
490      if (outputFile != null) {
491        UnionVisitor v = new UnionVisitor();
492        root.accept(v);
493        FilesPlume.writeObject(v.getResult(), outputFile);
494        // System.out.println("Output written to: " + outputFile);
495      } else {
496        throw new Error("no output file specified on command line");
497      }
498    }
499
500    if (logging) {
501      System.err.println("Invariant Diff: Ending Log");
502    }
503
504    // finished; return (and end program)
505  }
506
507  /**
508   * Reads an InvMap from a file that contains a serialized InvMap or PptMap.
509   *
510   * @param file a file
511   * @return an InvMap read from the file
512   * @throws IOException if there is trouble reading the file
513   * @throws ClassNotFoundException if an object in the serialized file has an unloadable class
514   */
515  private InvMap readInvMap(File file) throws IOException, ClassNotFoundException {
516    Object o = FilesPlume.readObject(file);
517    if (o instanceof InvMap) {
518      return (InvMap) o;
519    } else {
520      PptMap pptMap = FileIO.read_serialized_pptmap(file, false);
521      return convertToInvMap(pptMap);
522    }
523  }
524
525  /**
526   * Extracts the PptTopLevel and Invariants out of a pptMap, and places them into an InvMap. Maps
527   * PptTopLevel to a List of Invariants. The InvMap is a cleaner representation than the PptMap,
528   * and it allows us to more easily manipulate the contents. The InvMap contains exactly the
529   * elements contained in the PptMap. Conditional program points are also added as keys. Filtering
530   * is done when creating the pair tree. The ppts in the InvMap must be sorted, but the invariants
531   * need not be sorted.
532   */
533  public InvMap convertToInvMap(PptMap pptMap) {
534    InvMap map = new InvMap();
535
536    // Created sorted set of top level ppts, possibly including
537    // conditional ppts
538    NavigableSet<PptTopLevel> ppts = new TreeSet<>(PPT_COMPARATOR);
539    ppts.addAll(pptMap.asCollection());
540
541    for (PptTopLevel ppt : ppts) {
542      if (ignoreNumberedExits && ppt.ppt_name.isNumberedExitPoint()) {
543        continue;
544      }
545
546      // List<Invariant> invs = ppt.getInvariants();
547      List<Invariant> invs = CollectionsPlume.sortList(ppt.getInvariants(), PptTopLevel.icfp);
548      map.put(ppt, invs);
549      if (examineAllPpts) {
550        // Add conditional ppts
551        for (PptConditional pptCond : ppt.cond_iterable()) {
552          List<Invariant> invsCond =
553              CollectionsPlume.sortList(pptCond.getInvariants(), PptTopLevel.icfp);
554          // List<Invariant> invsCond = pptCond.getInvariants();
555          map.put(pptCond, invsCond);
556        }
557      }
558    }
559    return map;
560  }
561
562  /**
563   * Returns a pair tree of corresponding program points, and corresponding invariants at each
564   * program point. This tree can be walked to determine differences between the sets of invariants.
565   * Calls diffInvMap and asks to include all justified invariants.
566   */
567  public RootNode diffInvMap(InvMap map1, InvMap map2) {
568    return diffInvMap(map1, map2, true);
569  }
570
571  /**
572   * Returns a pair tree of corresponding program points, and corresponding invariants at each
573   * program point. This tree can be walked to determine differences between the sets of invariants.
574   * The tree consists of the invariants in map1 and map2. If includeUnjustified is true, the
575   * unjustified invariants are included.
576   */
577  public RootNode diffInvMap(InvMap map1, InvMap map2, boolean includeUnjustified) {
578    RootNode root = new RootNode();
579
580    Iterator<MPair<@Nullable PptTopLevel, @Nullable PptTopLevel>> opi =
581        new OrderedPairIterator<PptTopLevel>(
582            map1.pptSortedIterator(PPT_COMPARATOR),
583            map2.pptSortedIterator(PPT_COMPARATOR),
584            PPT_COMPARATOR);
585    while (opi.hasNext()) {
586      MPair<@Nullable PptTopLevel, @Nullable PptTopLevel> ppts = opi.next();
587      PptTopLevel ppt1 = ppts.first;
588      PptTopLevel ppt2 = ppts.second;
589      if (shouldAdd(ppt1) || shouldAdd(ppt2)) {
590        PptNode node = diffPptTopLevel(ppt1, ppt2, map1, map2, includeUnjustified);
591        root.add(node);
592      }
593    }
594
595    return root;
596  }
597
598  /**
599   * Diffs two PptMaps by converting them to InvMaps. Provided for compatibiliy with legacy code.
600   * Calls diffPptMap and asks to include all invariants.
601   */
602  public RootNode diffPptMap(PptMap pptMap1, PptMap pptMap2) {
603    return diffPptMap(pptMap1, pptMap2, true);
604  }
605
606  /**
607   * Diffs two PptMaps by converting them to InvMaps. Provided for compatibiliy with legacy code. If
608   * includeUnjustified is true, the unjustified invariants are included.
609   */
610  public RootNode diffPptMap(PptMap pptMap1, PptMap pptMap2, boolean includeUnjustified) {
611    InvMap map1 = convertToInvMap(pptMap1);
612    InvMap map2 = convertToInvMap(pptMap2);
613    return diffInvMap(map1, map2, includeUnjustified);
614  }
615
616  /** Returns true if the program point should be added to the tree, false otherwise. */
617  private boolean shouldAdd(@Nullable PptTopLevel ppt) {
618    if (examineAllPpts) {
619      return true;
620    } else {
621      if (ppt == null) {
622        return false;
623      } else if (ppt.ppt_name.isEnterPoint()) {
624        return true;
625      } else if (ppt.ppt_name.isCombinedExitPoint()) {
626        return true;
627      } else {
628        return false;
629      }
630    }
631  }
632
633  /**
634   * Takes a pair of corresponding top-level program points and maps, and returns a tree of the
635   * corresponding invariants. Either of the program points may be null. If includeUnjustied is
636   * true, the unjustified invariants are included.
637   */
638  private PptNode diffPptTopLevel(
639      @Nullable PptTopLevel ppt1,
640      @Nullable PptTopLevel ppt2,
641      InvMap map1,
642      InvMap map2,
643      boolean includeUnjustified) {
644    PptNode pptNode = new PptNode(ppt1, ppt2);
645
646    assert ppt1 == null || ppt2 == null || PPT_COMPARATOR.compare(ppt1, ppt2) == 0
647        : "Program points do not correspond";
648
649    List<Invariant> invs1;
650    if (ppt1 != null) {
651      invs1 = map1.get(ppt1);
652      Collections.sort(invs1, invSortComparator1);
653    } else {
654      invs1 = new ArrayList<Invariant>();
655    }
656
657    List<Invariant> invs2;
658    if (ppt2 != null) {
659      invs2 = map2.get(ppt2);
660      Collections.sort(invs2, invSortComparator2);
661    } else {
662      invs2 = new ArrayList<Invariant>();
663    }
664
665    Iterator<MPair<@Nullable Invariant, @Nullable Invariant>> opi =
666        new OrderedPairIterator<Invariant>(invs1.iterator(), invs2.iterator(), invPairComparator);
667    while (opi.hasNext()) {
668      MPair<@Nullable Invariant, @Nullable Invariant> invariants = opi.next();
669      Invariant inv1 = invariants.first;
670      Invariant inv2 = invariants.second;
671      if (!includeUnjustified) {
672        if ((inv1 != null) && !inv1.justified()) {
673          inv1 = null;
674        }
675        if ((inv2 != null) && !inv2.justified()) {
676          inv2 = null;
677        }
678      }
679      if ((inv1 != null) || (inv2 != null)) {
680        InvNode invNode = new InvNode(inv1, inv2);
681        pptNode.add(invNode);
682      }
683    }
684
685    return pptNode;
686  }
687
688  /** Use the comparator for sorting both sets and creating the pair tree. */
689  @EnsuresNonNull({"invSortComparator1", "invSortComparator2", "invPairComparator"})
690  public void setAllInvComparators(@UnknownInitialization Diff this, Comparator<Invariant> c) {
691    setInvSortComparator1(c);
692    setInvSortComparator2(c);
693    setInvPairComparator(c);
694  }
695
696  /**
697   * If the classname is non-null, returns the comparator named by the classname. Else, returns the
698   * default.
699   */
700  private static Comparator<Invariant> selectComparator(
701      @Nullable @ClassGetName String classname, Comparator<Invariant> defaultComparator)
702      throws ClassNotFoundException,
703          IllegalAccessException,
704          InstantiationException,
705          InvocationTargetException,
706          NoSuchMethodException {
707
708    if (classname != null) {
709      Class<?> cls = Class.forName(classname);
710      @SuppressWarnings("unchecked")
711      Comparator<Invariant> cmp =
712          (Comparator<Invariant>) cls.getDeclaredConstructor().newInstance();
713      return cmp;
714    } else {
715      return defaultComparator;
716    }
717  }
718
719  /** Use the comparator for sorting the first set. */
720  @EnsuresNonNull("invSortComparator1")
721  public void setInvSortComparator1(@UnknownInitialization Diff this, Comparator<Invariant> c) {
722    invSortComparator1 = c;
723  }
724
725  /** Use the comparator for sorting the second set. */
726  @EnsuresNonNull("invSortComparator2")
727  public void setInvSortComparator2(@UnknownInitialization Diff this, Comparator<Invariant> c) {
728    invSortComparator2 = c;
729  }
730
731  /** Use the comparator for creating the pair tree. */
732  @EnsuresNonNull("invPairComparator")
733  public void setInvPairComparator(@UnknownInitialization Diff this, Comparator<Invariant> c) {
734    invPairComparator = c;
735  }
736}