Source code

001package daikon;
002
003import static java.util.logging.Level.FINE;
004import static java.util.logging.Level.INFO;
005
006import daikon.split.PptSplitter;
007import daikon.suppress.NIS;
008import gnu.getopt.Getopt;
009import gnu.getopt.LongOpt;
010import java.io.File;
011import java.io.FileNotFoundException;
012import java.io.IOException;
013import java.io.OptionalDataException;
014import java.io.StreamCorruptedException;
015import java.util.ArrayList;
016import java.util.List;
017import java.util.Set;
018import java.util.TreeSet;
019import java.util.concurrent.TimeUnit;
020import java.util.logging.Logger;
021import org.checkerframework.checker.nullness.qual.Nullable;
022import org.plumelib.util.FilesPlume;
023import org.plumelib.util.StringsPlume;
024
025/**
026 * Merges invariants from multiple invariant files into a single invariant file. It does this by
027 * forming a hierarchy over the ppts from each invariant file and using the normal hierarchy merging
028 * code to merge the invariants.
029 *
030 * <p>The ppts from each invariant file are merged to create a single ppt map that contains the ppts
031 * from all of the files. At each leaf of the merged map, a hierarchy is formed to the ppts from
032 * each of the input files.
033 */
034public final class MergeInvariants {
035  private MergeInvariants() {
036    throw new Error("do not instantiate");
037  }
038
039  /** Debug logger. */
040  public static final Logger debug = Logger.getLogger("daikon.MergeInvariants");
041
042  /** Progress logger. */
043  public static final Logger debugProgress = Logger.getLogger("daikon.MergeInvariants.progress");
044
045  /** The file in which to produce output; if null, the results are printed. */
046  public static @Nullable File output_inv_file;
047
048  /** The usage message for this program. */
049  private static String usage =
050      StringsPlume.joinLines(
051          "Usage: java daikon.MergeInvariants [OPTION]... FILE",
052          "  -h, --" + Daikon.help_SWITCH,
053          "      Display this usage message",
054          "  --" + Daikon.config_option_SWITCH,
055          "      Specify a configuration option ",
056          "  --" + Daikon.debug_SWITCH,
057          "      Specify a logger to enable",
058          "  --" + Daikon.track_SWITCH,
059          "      Specify a class, varinfos, and ppt to debug track.  Format"
060              + "is class<var1,var2,var3>@ppt",
061          "   -o ",
062          "      Specify an output inv file.  If not specified, the results are printed");
063
064  public static void main(final String[] args)
065      throws FileNotFoundException,
066          StreamCorruptedException,
067          OptionalDataException,
068          IOException,
069          ClassNotFoundException {
070    try {
071      mainHelper(args);
072    } catch (Daikon.DaikonTerminationException e) {
073      Daikon.handleDaikonTerminationException(e);
074    }
075  }
076
077  /**
078   * This does the work of {@link #main(String[])}, but it never calls System.exit, so it is
079   * appropriate to be called progrmmatically.
080   *
081   * @param args the command-line arguments
082   * @throws FileNotFoundException if a file cannot be found
083   * @throws StreamCorruptedException if a stream is corrupted
084   * @throws OptionalDataException if there is a serialization problem
085   * @throws IOException if there is trouble with I/O
086   * @throws ClassNotFoundException if a class cannot be found
087   */
088  @SuppressWarnings("nullness:contracts.precondition") // private field
089  public static void mainHelper(String[] args)
090      throws FileNotFoundException,
091          StreamCorruptedException,
092          OptionalDataException,
093          IOException,
094          ClassNotFoundException {
095
096    daikon.LogHelper.setupLogs(INFO);
097
098    LongOpt[] longopts =
099        new LongOpt[] {
100          new LongOpt(Daikon.help_SWITCH, LongOpt.NO_ARGUMENT, null, 0),
101          new LongOpt(Daikon.config_option_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0),
102          new LongOpt(Daikon.debugAll_SWITCH, LongOpt.NO_ARGUMENT, null, 0),
103          new LongOpt(Daikon.debug_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0),
104          new LongOpt(Daikon.track_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0),
105        };
106
107    Getopt g = new Getopt("daikon.MergeInvariants", args, "ho:", longopts);
108    int c;
109    while ((c = g.getopt()) != -1) {
110      switch (c) {
111
112          // long option
113        case 0:
114          String option_name = longopts[g.getLongind()].getName();
115          if (Daikon.help_SWITCH.equals(option_name)) {
116            System.out.println(usage);
117            throw new Daikon.NormalTermination();
118          } else if (Daikon.config_option_SWITCH.equals(option_name)) {
119            String item = Daikon.getOptarg(g);
120            daikon.config.Configuration.getInstance().apply(item);
121            break;
122
123          } else if (Daikon.debugAll_SWITCH.equals(option_name)) {
124            Global.debugAll = true;
125
126          } else if (Daikon.debug_SWITCH.equals(option_name)) {
127            LogHelper.setLevel(Daikon.getOptarg(g), FINE);
128          } else if (Daikon.track_SWITCH.equals(option_name)) {
129            LogHelper.setLevel("daikon.Debug", FINE);
130            String error = Debug.add_track(Daikon.getOptarg(g));
131            if (error != null) {
132              throw new Daikon.UserError(
133                  "Error parsing track argument '" + Daikon.getOptarg(g) + "' - " + error);
134            }
135          } else {
136            throw new Daikon.UserError("Unknown long option received: " + option_name);
137          }
138          break;
139
140        case 'h':
141          System.out.println(usage);
142          throw new Daikon.NormalTermination();
143
144        case 'o':
145          String output_inv_filename = Daikon.getOptarg(g);
146
147          if (output_inv_file != null) {
148            throw new Daikon.UserError(
149                "multiple serialization output files supplied on command line: "
150                    + output_inv_file
151                    + " "
152                    + output_inv_filename);
153          }
154
155          output_inv_file = new File(output_inv_filename);
156
157          if (!FilesPlume.canCreateAndWrite(output_inv_file)) {
158            throw new Daikon.UserError(
159                "Cannot write to serialization output file " + output_inv_file);
160          }
161          break;
162
163        case '?':
164          break; // getopt() already printed an error
165
166        default:
167          System.out.println("getopt() returned " + c);
168          break;
169      }
170    }
171
172    daikon.LogHelper.setupLogs(Global.debugAll ? FINE : INFO);
173
174    List<File> inv_files = new ArrayList<>();
175    File decl_file = null;
176    Set<File> splitter_files = new TreeSet<>();
177
178    // Get each file specified
179    for (int i = g.getOptind(); i < args.length; i++) {
180      File file = new File(args[i]);
181      if (!file.exists()) {
182        throw new Daikon.UserError("File " + file + " not found.");
183      }
184      if (file.toString().indexOf(".inv") != -1) {
185        inv_files.add(file);
186      } else if (file.toString().indexOf(".decls") != -1) {
187        if (decl_file != null) {
188          throw new Daikon.UserError("Only one decl file may be specified");
189        }
190        decl_file = file;
191      } else if (file.toString().indexOf(".spinfo") != -1) {
192        splitter_files.add(file);
193      } else {
194        throw new Daikon.UserError("Unrecognized file type: " + file);
195      }
196    }
197
198    // Make sure at least two files were specified
199    if (inv_files.size() < 2) {
200      throw new Daikon.UserError(
201          "Provided "
202              + StringsPlume.nplural(inv_files.size(), "inv file")
203              + " but needs at least two");
204    }
205
206    // Setup the default for guarding
207    PrintInvariants.validateGuardNulls();
208
209    // Initialize the prototype invariants and NI suppressions
210    Daikon.setup_proto_invs();
211    NIS.init_ni_suppression();
212
213    // Read in each of the specified maps
214    List<PptMap> pptmaps = new ArrayList<>();
215    for (File file : inv_files) {
216      debugProgress.fine("Processing " + file);
217      PptMap ppts = FileIO.read_serialized_pptmap(file, true);
218      ppts.repCheck();
219      pptmaps.add(ppts);
220      Debug.check(ppts, "After initial reading of " + file);
221    }
222
223    // Merged ppt map (result of merging each specified inv file)
224    PptMap merge_ppts = null;
225
226    // if no decls file was specified
227    if (decl_file == null) {
228      if (splitter_files.size() > 0) {
229        throw new Daikon.UserError(".spinfo files may only be specified along with a .decls file");
230      }
231
232      // Read in each of the maps again to build a template that contains all
233      // of the program points from each map.
234      for (File file : inv_files) {
235        debugProgress.fine("Reading " + file + " as merge template");
236        if (merge_ppts == null) {
237          merge_ppts = FileIO.read_serialized_pptmap(file, true);
238        } else {
239          PptMap pmap = FileIO.read_serialized_pptmap(file, true);
240          for (PptTopLevel ppt : pmap.pptIterable()) {
241            if (merge_ppts.containsName(ppt.name())) {
242              // System.out.printf("Not adding ppt %s from %s%n", ppt, file);
243              continue;
244            }
245            merge_ppts.add(ppt);
246            // System.out.printf("Adding ppt %s from %s%n", ppt, file);
247
248            // Make sure that the parents of this ppt are already in
249            // the map.  This will be true if all possible children of
250            // any ppt are always included in the same invariant file.
251            // For example, all possible enter/exit points should be
252            // included with each object point.  This is true for Chicory
253            // as long as ppt filtering didn't remove some ppts.
254            for (PptRelation rel : ppt.parents) {
255              assert merge_ppts.get(rel.parent.name()) == rel.parent : ppt + " - " + rel;
256            }
257          }
258        }
259      }
260      assert merge_ppts != null
261          : "@AssumeAssertion(nullness): inv_files is non-empty, so for-loop body executed";
262
263      // Remove all of the slices, equality sets, to start
264      debugProgress.fine("Cleaning ppt map in preparation for merge");
265      for (PptTopLevel ppt : merge_ppts.ppt_all_iterable()) {
266        ppt.clean_for_merge();
267      }
268
269    } else {
270
271      // Build the result pptmap from the specific decls file
272      debugProgress.fine("Building result ppt map from decls file");
273      Daikon.create_splitters(splitter_files);
274      List<File> decl_files = new ArrayList<>();
275      decl_files.add(decl_file);
276      merge_ppts = FileIO.read_declaration_files(decl_files);
277      merge_ppts.trimToSize();
278      PptRelation.init_hierarchy(merge_ppts);
279    }
280
281    // Create a hierarchy between the merge exitNN points and the
282    // corresponding points in each of the specified maps.  This
283    // should only be created at the exitNN points (i.e., the leaves)
284    // so that the normal processing will create the invariants at
285    // upper points.
286    debugProgress.fine("Building hierarchy between leaves of the maps");
287    for (PptTopLevel ppt : merge_ppts.pptIterable()) {
288
289      // Skip everything that is not a final exit point
290      if (!ppt.ppt_name.isExitPoint()) {
291        assert ppt.children.size() > 0 : ppt;
292        continue;
293      }
294      if (ppt.ppt_name.isCombinedExitPoint()) {
295        assert ppt.children.size() > 0 : ppt;
296        continue;
297      }
298
299      // System.out.printf("Including ppt %s, %d children%n", ppt,
300      //                   ppt.children.size());
301
302      // Splitters should not have any children to begin with
303      if (ppt.has_splitters()) {
304        assert ppt.splitters != null; // because ppt.has_splitters() = true
305        for (PptSplitter ppt_split : ppt.splitters) {
306          for (PptTopLevel p : ppt_split.ppts) {
307            assert p.children.size() == 0 : p;
308          }
309        }
310      }
311
312      // Loop over each of the input ppt maps, looking for the same ppt
313      for (int j = 0; j < pptmaps.size(); j++) {
314        PptMap pmap = pptmaps.get(j);
315        PptTopLevel child = pmap.get(ppt.name());
316        // System.out.printf("found child %s from pmap %d%n", child, j);
317        if (child == null) {
318          continue;
319        }
320        if (child.equality_view == null) {
321          System.out.println(
322              "equality_view == null in child ppt: "
323                  + child.name()
324                  + " ("
325                  + inv_files.get(j)
326                  + ")");
327        } else if (child.equality_view.invs == null) {
328          System.out.println(
329              "equality_view.invs == null in child ppt: "
330                  + child.name()
331                  + " ("
332                  + inv_files.get(j)
333                  + ")"
334                  + " samples = "
335                  + child.num_samples());
336        }
337
338        // Remove the equality invariants added during equality post
339        // processing.  These are not over leaders and will cause problems
340        // in the merge
341        child.remove_equality_invariants();
342        child.in_merge = false;
343
344        // Remove implications, they don't merge correctly
345        child.remove_implications();
346
347        // If the ppt has splitters, attach the child's splitters to the
348        // splitters.  Don't attach the ppt itself, as its invariants can
349        // be built from the invariants in the splitters.
350        if (ppt.has_splitters()) {
351          assert ppt.splitters != null; // because ppt.has_splitters() = true
352          setup_conditional_merge(ppt, child);
353        } else {
354          PptRelation.newMergeChildRel(ppt, child);
355        }
356      }
357
358      // Make sure at least one child was found
359      assert ppt.children.size() > 0 : ppt;
360      if (ppt.has_splitters()) {
361        assert ppt.splitters != null; // because ppt.has_splitters() = true
362        for (PptSplitter ppt_split : ppt.splitters) {
363          for (PptTopLevel p : ppt_split.ppts) {
364            assert p.children.size() > 0 : p;
365          }
366        }
367      }
368    }
369
370    // Check the resulting PptMap for consistency
371    merge_ppts.repCheck();
372
373    // Debug print the hierarchy is a more readable manner
374    if (debug.isLoggable(FINE)) {
375      debug.fine("PPT Hierarchy");
376      for (PptTopLevel ppt : merge_ppts.pptIterable()) {
377        if (ppt.parents.size() == 0) {
378          ppt.debug_print_tree(debug, 0, null);
379        }
380      }
381    }
382
383    // Merge the invariants
384    debugProgress.fine("Merging invariants");
385    Daikon.createUpperPpts(merge_ppts);
386
387    // Equality post processing
388    debugProgress.fine("Equality Post Processing");
389    for (PptTopLevel ppt : merge_ppts.ppt_all_iterable()) {
390      ppt.postProcessEquality();
391    }
392
393    // Implications
394    long startTime = System.nanoTime();
395    // System.out.println("Creating implications ");
396    debugProgress.fine("Adding Implications ... ");
397    for (PptTopLevel ppt : merge_ppts.pptIterable()) {
398      if (ppt.num_samples() > 0) {
399        ppt.addImplications();
400      }
401    }
402    long duration = System.nanoTime() - startTime;
403    debugProgress.fine("Time spent in implications: " + TimeUnit.NANOSECONDS.toSeconds(duration));
404
405    // Remove the PptRelation links so that when the file is written
406    // out it only includes the new information
407    for (PptTopLevel ppt : merge_ppts.pptIterable()) {
408      if (!ppt.ppt_name.isExitPoint()) {
409        continue;
410      }
411      if (ppt.ppt_name.isCombinedExitPoint()) {
412        continue;
413      }
414      ppt.children.clear();
415      for (PptConditional cond : ppt.cond_iterable()) {
416        cond.children.clear();
417      }
418    }
419
420    // Write serialized output
421    debugProgress.fine("Writing Output");
422    if (output_inv_file != null) {
423      try {
424        FileIO.write_serialized_pptmap(merge_ppts, output_inv_file);
425      } catch (IOException e) {
426        throw new RuntimeException(
427            "Error while writing .inv file '" + output_inv_file + "': " + e.toString());
428      }
429    } else {
430      // Print the invariants
431      PrintInvariants.print_invariants(merge_ppts);
432    }
433  }
434
435  /**
436   * Ses up the specified relation beteween each of the conditionals in ppt and the matching
437   * conditionals in child. Each must have the same number of splitters setup in the same order. The
438   * splitter match can't be checked because splitters can't be read back in.
439   */
440  private static void setup_conditional_merge(PptTopLevel ppt, PptTopLevel child) {
441
442    // Both ppt and child should have splitters
443    if (ppt.has_splitters() != child.has_splitters()) {
444      throw new Error(
445          "Merge ppt "
446              + ppt.name
447              + (ppt.has_splitters() ? " has " : "doesn't have ")
448              + "splitters, but child ppt "
449              + child.name
450              + (child.has_splitters() ? " does" : " doesn't"));
451    }
452
453    // Nothing to do if there are no splitters here
454    if (!ppt.has_splitters()) {
455      return;
456    }
457
458    assert child.splitters != null
459        : "@AssumeAssertion(nullness): correlated: ppt.has_splitters() == child.has_splitters(),"
460            + " and ppt.has_splitters() == true";
461
462    // Both ppt and child should have the same number of splitters
463    if (ppt.splitters.size() != child.splitters.size()) {
464      throw new Error(
465          "Merge ppt "
466              + ppt.name
467              + " has "
468              + ((ppt.splitters.size() > child.splitters.size()) ? "more" : "fewer")
469              + " splitters ("
470              + ppt.splitters.size()
471              + ") than child ppt "
472              + child.name
473              + " ("
474              + child.splitters.size()
475              + ")");
476    }
477
478    // Create a relation from each conditional ppt to its corresponding
479    // conditional ppt in the child.
480    for (int ii = 0; ii < ppt.splitters.size(); ii++) {
481      PptSplitter ppt_split = ppt.splitters.get(ii);
482      PptSplitter child_split = child.splitters.get(ii);
483      for (int jj = 0; jj < ppt_split.ppts.length; jj++) {
484        child_split.ppts[jj].remove_equality_invariants();
485        child_split.ppts[jj].in_merge = false;
486        PptRelation.newMergeChildRel(ppt_split.ppts[jj], child_split.ppts[jj]);
487      }
488    }
489  }
490}