001// Main routine for Daikon invariant detector 002// For documentation, see file doc/daikon.html in the distribution. 003 004package daikon; 005 006import static java.util.logging.Level.FINE; 007import static java.util.logging.Level.FINER; 008import static java.util.logging.Level.INFO; 009 010import daikon.config.Configuration; 011import daikon.derive.Derivation; 012import daikon.inv.Equality; 013import daikon.inv.Invariant; 014import daikon.inv.OutputFormat; 015import daikon.inv.binary.sequenceScalar.Member; 016import daikon.inv.binary.sequenceScalar.MemberFloat; 017import daikon.inv.binary.sequenceScalar.SeqFloatEqual; 018import daikon.inv.binary.sequenceScalar.SeqFloatGreaterEqual; 019import daikon.inv.binary.sequenceScalar.SeqFloatGreaterThan; 020import daikon.inv.binary.sequenceScalar.SeqFloatLessEqual; 021import daikon.inv.binary.sequenceScalar.SeqFloatLessThan; 022import daikon.inv.binary.sequenceScalar.SeqIntEqual; 023import daikon.inv.binary.sequenceScalar.SeqIntGreaterEqual; 024import daikon.inv.binary.sequenceScalar.SeqIntGreaterThan; 025import daikon.inv.binary.sequenceScalar.SeqIntLessEqual; 026import daikon.inv.binary.sequenceScalar.SeqIntLessThan; 027import daikon.inv.binary.sequenceString.MemberString; 028import daikon.inv.binary.twoScalar.FloatEqual; 029import daikon.inv.binary.twoScalar.FloatGreaterEqual; 030import daikon.inv.binary.twoScalar.FloatGreaterThan; 031import daikon.inv.binary.twoScalar.FloatLessEqual; 032import daikon.inv.binary.twoScalar.FloatLessThan; 033import daikon.inv.binary.twoScalar.FloatNonEqual; 034import daikon.inv.binary.twoScalar.IntEqual; 035import daikon.inv.binary.twoScalar.IntGreaterEqual; 036import daikon.inv.binary.twoScalar.IntGreaterThan; 037import daikon.inv.binary.twoScalar.IntLessEqual; 038import daikon.inv.binary.twoScalar.IntLessThan; 039import daikon.inv.binary.twoScalar.IntNonEqual; 040import daikon.inv.binary.twoScalar.LinearBinary; 041import daikon.inv.binary.twoScalar.LinearBinaryFloat; 042import daikon.inv.binary.twoScalar.NumericFloat; 043import daikon.inv.binary.twoScalar.NumericInt; 044import daikon.inv.binary.twoSequence.PairwiseFloatEqual; 045import daikon.inv.binary.twoSequence.PairwiseFloatGreaterEqual; 046import daikon.inv.binary.twoSequence.PairwiseFloatGreaterThan; 047import daikon.inv.binary.twoSequence.PairwiseFloatLessEqual; 048import daikon.inv.binary.twoSequence.PairwiseFloatLessThan; 049import daikon.inv.binary.twoSequence.PairwiseIntEqual; 050import daikon.inv.binary.twoSequence.PairwiseIntGreaterEqual; 051import daikon.inv.binary.twoSequence.PairwiseIntGreaterThan; 052import daikon.inv.binary.twoSequence.PairwiseIntLessEqual; 053import daikon.inv.binary.twoSequence.PairwiseIntLessThan; 054import daikon.inv.binary.twoSequence.PairwiseLinearBinary; 055import daikon.inv.binary.twoSequence.PairwiseLinearBinaryFloat; 056import daikon.inv.binary.twoSequence.PairwiseNumericFloat; 057import daikon.inv.binary.twoSequence.PairwiseNumericInt; 058import daikon.inv.binary.twoSequence.PairwiseString; 059import daikon.inv.binary.twoSequence.PairwiseStringEqual; 060import daikon.inv.binary.twoSequence.PairwiseStringGreaterEqual; 061import daikon.inv.binary.twoSequence.PairwiseStringGreaterThan; 062import daikon.inv.binary.twoSequence.PairwiseStringLessEqual; 063import daikon.inv.binary.twoSequence.PairwiseStringLessThan; 064import daikon.inv.binary.twoSequence.Reverse; 065import daikon.inv.binary.twoSequence.ReverseFloat; 066import daikon.inv.binary.twoSequence.SeqSeqFloatEqual; 067import daikon.inv.binary.twoSequence.SeqSeqFloatGreaterEqual; 068import daikon.inv.binary.twoSequence.SeqSeqFloatGreaterThan; 069import daikon.inv.binary.twoSequence.SeqSeqFloatLessEqual; 070import daikon.inv.binary.twoSequence.SeqSeqFloatLessThan; 071import daikon.inv.binary.twoSequence.SeqSeqIntEqual; 072import daikon.inv.binary.twoSequence.SeqSeqIntGreaterEqual; 073import daikon.inv.binary.twoSequence.SeqSeqIntGreaterThan; 074import daikon.inv.binary.twoSequence.SeqSeqIntLessEqual; 075import daikon.inv.binary.twoSequence.SeqSeqIntLessThan; 076import daikon.inv.binary.twoSequence.SeqSeqStringEqual; 077import daikon.inv.binary.twoSequence.SeqSeqStringGreaterEqual; 078import daikon.inv.binary.twoSequence.SeqSeqStringGreaterThan; 079import daikon.inv.binary.twoSequence.SeqSeqStringLessEqual; 080import daikon.inv.binary.twoSequence.SeqSeqStringLessThan; 081import daikon.inv.binary.twoSequence.SubSequence; 082import daikon.inv.binary.twoSequence.SubSequenceFloat; 083import daikon.inv.binary.twoSequence.SubSet; 084import daikon.inv.binary.twoSequence.SubSetFloat; 085import daikon.inv.binary.twoSequence.SuperSequence; 086import daikon.inv.binary.twoSequence.SuperSequenceFloat; 087import daikon.inv.binary.twoSequence.SuperSet; 088import daikon.inv.binary.twoSequence.SuperSetFloat; 089import daikon.inv.binary.twoString.StdString; 090import daikon.inv.binary.twoString.StringEqual; 091import daikon.inv.binary.twoString.StringGreaterEqual; 092import daikon.inv.binary.twoString.StringGreaterThan; 093import daikon.inv.binary.twoString.StringLessEqual; 094import daikon.inv.binary.twoString.StringLessThan; 095import daikon.inv.binary.twoString.StringNonEqual; 096import daikon.inv.ternary.threeScalar.FunctionBinary; 097import daikon.inv.ternary.threeScalar.FunctionBinaryFloat; 098import daikon.inv.ternary.threeScalar.LinearTernary; 099import daikon.inv.ternary.threeScalar.LinearTernaryFloat; 100import daikon.inv.unary.scalar.CompleteOneOfScalar; 101import daikon.inv.unary.scalar.IsPointer; 102import daikon.inv.unary.scalar.LowerBound; 103import daikon.inv.unary.scalar.LowerBoundFloat; 104import daikon.inv.unary.scalar.Modulus; 105import daikon.inv.unary.scalar.NonModulus; 106import daikon.inv.unary.scalar.NonZero; 107import daikon.inv.unary.scalar.NonZeroFloat; 108import daikon.inv.unary.scalar.OneOfFloat; 109import daikon.inv.unary.scalar.OneOfScalar; 110import daikon.inv.unary.scalar.RangeFloat; 111import daikon.inv.unary.scalar.RangeInt; 112import daikon.inv.unary.scalar.UpperBound; 113import daikon.inv.unary.scalar.UpperBoundFloat; 114import daikon.inv.unary.sequence.CommonFloatSequence; 115import daikon.inv.unary.sequence.CommonSequence; 116import daikon.inv.unary.sequence.EltLowerBound; 117import daikon.inv.unary.sequence.EltLowerBoundFloat; 118import daikon.inv.unary.sequence.EltNonZero; 119import daikon.inv.unary.sequence.EltNonZeroFloat; 120import daikon.inv.unary.sequence.EltOneOf; 121import daikon.inv.unary.sequence.EltOneOfFloat; 122import daikon.inv.unary.sequence.EltRangeFloat; 123import daikon.inv.unary.sequence.EltRangeInt; 124import daikon.inv.unary.sequence.EltUpperBound; 125import daikon.inv.unary.sequence.EltUpperBoundFloat; 126import daikon.inv.unary.sequence.EltwiseFloatEqual; 127import daikon.inv.unary.sequence.EltwiseFloatGreaterEqual; 128import daikon.inv.unary.sequence.EltwiseFloatGreaterThan; 129import daikon.inv.unary.sequence.EltwiseFloatLessEqual; 130import daikon.inv.unary.sequence.EltwiseFloatLessThan; 131import daikon.inv.unary.sequence.EltwiseIntEqual; 132import daikon.inv.unary.sequence.EltwiseIntGreaterEqual; 133import daikon.inv.unary.sequence.EltwiseIntGreaterThan; 134import daikon.inv.unary.sequence.EltwiseIntLessEqual; 135import daikon.inv.unary.sequence.EltwiseIntLessThan; 136import daikon.inv.unary.sequence.NoDuplicates; 137import daikon.inv.unary.sequence.NoDuplicatesFloat; 138import daikon.inv.unary.sequence.OneOfFloatSequence; 139import daikon.inv.unary.sequence.OneOfSequence; 140import daikon.inv.unary.sequence.SeqIndexFloatEqual; 141import daikon.inv.unary.sequence.SeqIndexFloatGreaterEqual; 142import daikon.inv.unary.sequence.SeqIndexFloatGreaterThan; 143import daikon.inv.unary.sequence.SeqIndexFloatLessEqual; 144import daikon.inv.unary.sequence.SeqIndexFloatLessThan; 145import daikon.inv.unary.sequence.SeqIndexFloatNonEqual; 146import daikon.inv.unary.sequence.SeqIndexIntEqual; 147import daikon.inv.unary.sequence.SeqIndexIntGreaterEqual; 148import daikon.inv.unary.sequence.SeqIndexIntGreaterThan; 149import daikon.inv.unary.sequence.SeqIndexIntLessEqual; 150import daikon.inv.unary.sequence.SeqIndexIntLessThan; 151import daikon.inv.unary.sequence.SeqIndexIntNonEqual; 152import daikon.inv.unary.string.CompleteOneOfString; 153import daikon.inv.unary.string.OneOfString; 154import daikon.inv.unary.string.PrintableString; 155import daikon.inv.unary.stringsequence.CommonStringSequence; 156import daikon.inv.unary.stringsequence.EltOneOfString; 157import daikon.inv.unary.stringsequence.OneOfStringSequence; 158import daikon.simplify.LemmaStack; 159import daikon.split.ContextSplitterFactory; 160import daikon.split.PptSplitter; 161import daikon.split.SpinfoFile; 162import daikon.split.Splitter; 163import daikon.split.SplitterFactory; 164import daikon.split.SplitterList; 165import daikon.suppress.NIS; 166import daikon.suppress.NIS.SuppressionProcessor; 167import gnu.getopt.Getopt; 168import gnu.getopt.LongOpt; 169import java.io.File; 170import java.io.FileInputStream; 171import java.io.IOException; 172import java.io.InputStream; 173import java.io.LineNumberReader; 174import java.lang.reflect.Field; 175import java.lang.reflect.Method; 176import java.time.LocalDateTime; 177import java.time.ZoneId; 178import java.util.ArrayList; 179import java.util.Collection; 180import java.util.ConcurrentModificationException; 181import java.util.HashSet; 182import java.util.Iterator; 183import java.util.LinkedHashMap; 184import java.util.LinkedHashSet; 185import java.util.List; 186import java.util.Map; 187import java.util.Set; 188import java.util.TreeSet; 189import java.util.concurrent.TimeUnit; 190import java.util.logging.Logger; 191import java.util.regex.Matcher; 192import java.util.regex.Pattern; 193import java.util.regex.PatternSyntaxException; 194import org.checkerframework.checker.interning.qual.Interned; 195import org.checkerframework.checker.nullness.qual.EnsuresNonNull; 196import org.checkerframework.checker.nullness.qual.KeyFor; 197import org.checkerframework.checker.nullness.qual.MonotonicNonNull; 198import org.checkerframework.checker.nullness.qual.NonNull; 199import org.checkerframework.checker.nullness.qual.Nullable; 200import org.checkerframework.checker.nullness.qual.RequiresNonNull; 201import org.checkerframework.checker.signature.qual.ClassGetName; 202import org.checkerframework.dataflow.qual.Pure; 203import org.plumelib.util.EntryReader; 204import org.plumelib.util.FilesPlume; 205import org.plumelib.util.RegexUtil; 206import org.plumelib.util.StringsPlume; 207import typequals.prototype.qual.Prototype; 208 209/** 210 * The {@link #main} method is the main entry point for the Daikon invariant detector. The {@link 211 * #mainHelper} method is the entry point, when called programmatically. 212 */ 213public final class Daikon { 214 215 private Daikon() { 216 throw new Error("do not instantiate"); 217 } 218 219 /** 220 * The amount of time to wait between updates of the progress display, measured in milliseconds. A 221 * value of -1 means do not print the progress display at all. 222 */ 223 public static int dkconfig_progress_delay = 1000; 224 225 /** The current version of Daikon. */ 226 public static final String release_version = "5.8.20"; 227 228 /** The date for the current version of Daikon. */ 229 public static final String release_date = "May 14, 2024"; 230 231 /** A description of the Daikon release (version number, date, and URL). */ 232 public static final String release_string = 233 "Daikon version " 234 + release_version 235 + ", released " 236 + release_date 237 + "; http://plse.cs.washington.edu/daikon."; 238 239 // Variables starting with dkconfig_ should only be set via the 240 // daikon.config.Configuration interface. 241 /** Boolean. Controls whether conditional program points are displayed. */ 242 public static boolean dkconfig_output_conditionals = true; 243 244 // Variables starting with dkconfig_ should only be set via the 245 // daikon.config.Configuration interface. 246 /** Boolean. Just print the total number of possible invariants and exit. */ 247 public static boolean dkconfig_calc_possible_invs; 248 249 /** 250 * Integer. Percentage of program points to process. All program points are sorted by name, and 251 * all samples for the first {@code ppt_perc} program points are processed. A percentage of 100 252 * matches all program points. 253 */ 254 public static int dkconfig_ppt_perc = 100; 255 256 /** 257 * Boolean. Controls whether or not the total samples read and processed are printed at the end of 258 * processing. 259 */ 260 public static boolean dkconfig_print_sample_totals = false; 261 262 // All these variables really need to be organized better. 263 264 public static final String lineSep = Global.lineSep; 265 266 /** 267 * Boolean. Controls whether or not processing information is printed out. Setting this variable 268 * to true also automatically sets {@code progress_delay} to -1. 269 */ 270 public static boolean dkconfig_quiet = false; 271 272 // Change this at your peril; high costs in time and space for "false", 273 // because so many more invariants get instantiated. 274 public static final boolean check_program_types = true; 275 276 // Problem with setting this to true: 277 // get no invariants over any value that can ever be missing 278 // Problem with setting this to false: 279 // due to different number of samples, isEqualityComparison is 280 // non-transitive (that is specially handled in the code) 281 public static final boolean invariants_check_canBeMissing = false; 282 283 // Specialized version for array elements; only examined if 284 // invariants_check_canBeMissing is false 285 public static final boolean invariants_check_canBeMissing_arrayelt = true; 286 287 public static final boolean disable_modbit_check_message = false; 288 289 /** 290 * Not a good idea to set this to true, as it is too easy to ignore the warnings and the modbit 291 * problem can cause an error later. 292 */ 293 public static final boolean disable_modbit_check_error = false; 294 295 /** When true, don't print textual output. */ 296 public static boolean no_text_output = false; 297 298 /** 299 * When true, show how much time each Daikon phase took. Has no effect if System.console() is not 300 * connected to a terminal. If option show-detail-progress was used, also show how much time each 301 * program point took. 302 */ 303 public static boolean show_progress = false; 304 305 /** 306 * Whether to use the "new" equality set mechanism for handling equality, using canonicals to have 307 * instantiation of invariants only over equality sets. 308 */ 309 public static boolean use_equality_optimization = true; 310 311 /** 312 * Boolean. Controls whether the Daikon optimizations (equality sets, suppressions) are undone at 313 * the end to create a more complete set of invariants. Output does not include conditional 314 * program points, implications, reflexive and partially reflexive invariants. 315 */ 316 public static boolean dkconfig_undo_opts = false; 317 318 /** 319 * Boolean. Indicates to Daikon classes and methods that the methods calls should be compatible to 320 * DaikonSimple because Daikon and DaikonSimple share methods. Default value is 'false'. 321 */ 322 public static boolean using_DaikonSimple = false; 323 324 /** 325 * If "always", then invariants are always guarded. If "never", then invariants are never guarded. 326 * If "missing", then invariants are guarded only for variables that were missing ("can be 327 * missing") in the dtrace (the observed executions). If "default", then use "missing" mode for 328 * Java output and "never" mode otherwise. 329 * 330 * <p>Guarding means adding predicates that ensure that variables can be dereferenced. For 331 * instance, if {@code a} can be null --- that is, if {@code a.b} can be nonsensical --- then the 332 * guarded version of 333 * 334 * <pre>a.b == 5</pre> 335 * 336 * is 337 * 338 * <pre>(a != null) ⇒ (a.b == 5)</pre> 339 * 340 * . 341 * 342 * <p>(To do: Some configuration option (maybe this one) should add guards for other reasons that 343 * lead to nonsensical values (@pxref{Variable names}).) <br> 344 * @cindex nonsensical values for variables, guarding 345 */ 346 // Perhaps a better default would be "missing". 347 public static @Interned String dkconfig_guardNulls = "default"; 348 349 /** 350 * Whether to associate the program points in a dataflow hierarchy, as via Nimmer's thesis. 351 * Deactivate only for languages and analyses where flow relation is nonsensical. 352 */ 353 public static boolean use_dataflow_hierarchy = true; 354 355 /** 356 * Whether to use the bottom up implementation of the dataflow hierarchy. This mechanism builds 357 * invariants initially only at the leaves of the partial order. Upper points are calculated by 358 * joining the invariants from each of their children points. 359 */ 360 // public static boolean dkconfig_df_bottom_up = true; 361 362 // When true, use the Simplify theorem prover (not part of Daikon) 363 // to locate logically redundant invariants, and flag them as 364 // redundant, so that they are removed from the printed output. 365 public static boolean suppress_redundant_invariants_with_simplify = false; 366 367 public static OutputFormat output_format = OutputFormat.DAIKON; 368 369 // When true, output numbers of values and samples (also names of variables) 370 public static boolean output_num_samples = false; 371 372 public static boolean ignore_comparability = false; 373 374 // Controls which program points/variables are used/ignored. 375 public static @Nullable Pattern ppt_regexp; 376 public static @Nullable Pattern ppt_omit_regexp; 377 public static @Nullable Pattern var_regexp; 378 public static @Nullable Pattern var_omit_regexp; 379 380 /** 381 * If set, only ppts less than ppt_max_name are included. Used by the configuration option 382 * dkconfig_ppt_percent to only work on a specified percent of the ppts. 383 */ 384 public static @Nullable String ppt_max_name = null; 385 386 // The invariants detected will be serialized and written to this 387 // file. 388 public static @Nullable File inv_file; 389 390 // Whether we want the memory monitor activated 391 private static boolean use_mem_monitor = false; 392 393 /** Whether Daikon should print its version number and date. */ 394 public static boolean noversion_output = false; 395 396 /** Whether Daikon is in its inferencing loop. Used only for assertion checks. */ 397 public static boolean isInferencing = false; 398 399 /** 400 * When true, omit certain invariants from the output {@code .inv} file. Generally these are 401 * invariants that wouldn't be printed in any case; but by default, they're retained in the {@code 402 * .inv} file in case they would be useful for later processing. (For instance, we might at some 403 * point in the future support resuming processing with more data from an {@code .inv} file). 404 * These invariants can increase the size of the {@code .inv} file, though, so when only limited 405 * further processing is needed, it can save space to omit them. 406 */ 407 public static boolean omit_from_output = false; 408 409 /** 410 * An array of flags, indexed by characters, in which a true entry means that invariants of that 411 * sort should be omitted from the output {@code .inv} file. 412 */ 413 public static boolean[] omit_types = new boolean[256]; 414 415 // Command-line options / command-line arguments 416 // These variables are public so other programs can reuse the same 417 // command-line options. 418 419 /** option help. */ 420 public static final String help_SWITCH = "help"; 421 422 // "-o" switch: file to which serialized output is written 423 /** option no-text-output. */ 424 public static final String no_text_output_SWITCH = "no_text_output"; 425 426 /** option format. */ 427 public static final String format_SWITCH = "format"; 428 429 /** option show-progress. */ 430 public static final String show_progress_SWITCH = "show_progress"; 431 432 /** option show-detail-progress. */ 433 public static final String show_detail_progress_SWITCH = "show_detail_progress"; 434 435 /** option no-show-progress. */ 436 public static final String no_show_progress_SWITCH = "no_show_progress"; 437 438 /** option noversion. */ 439 public static final String noversion_SWITCH = "noversion"; 440 441 public static final String output_num_samples_SWITCH = "output_num_samples"; 442 public static final String files_from_SWITCH = "files_from"; 443 public static final String omit_from_output_SWITCH = "omit_from_output"; 444 // Control invariant detection 445 public static final String conf_limit_SWITCH = "conf_limit"; 446 public static final String list_type_SWITCH = "list_type"; 447 public static final String user_defined_invariant_SWITCH = "user-defined-invariant"; 448 public static final String disable_all_invariants_SWITCH = "disable-all-invariants"; 449 public static final String no_dataflow_hierarchy_SWITCH = "nohierarchy"; 450 public static final String suppress_redundant_SWITCH = "suppress_redundant"; 451 // Process only part of the trace file 452 public static final String ppt_regexp_SWITCH = "ppt-select-pattern"; 453 public static final String ppt_omit_regexp_SWITCH = "ppt-omit-pattern"; 454 public static final String var_regexp_SWITCH = "var-select-pattern"; 455 public static final String var_omit_regexp_SWITCH = "var-omit-pattern"; 456 // Configuration options 457 public static final String server_SWITCH = 458 "server"; // YOAV: server mode for Daikon: reads dtrace files as they appear 459 public static final String config_SWITCH = "config"; 460 public static final String config_option_SWITCH = "config_option"; 461 // Debugging 462 public static final String debugAll_SWITCH = "debug"; 463 public static final String debug_SWITCH = "dbg"; 464 public static final String track_SWITCH = "track"; 465 public static final String disc_reason_SWITCH = "disc_reason"; 466 public static final String mem_stat_SWITCH = "mem_stat"; 467 public static final String wrap_xml_SWITCH = "wrap_xml"; 468 469 /** 470 * Regular expression that matches class names in the format expected by {@link 471 * Class#forName(String)}. 472 */ 473 // This regular expression is taken from 474 // checker-framework/checker/src/org/checkerframework/checker/signature/qual/ClassGetName.java 475 // . It's a bit too lenient since we don't need to permit arrays and 476 // primitives. 477 private static final String classGetNameRegex = 478 "(^[A-Za-z_][A-Za-z_0-9]*(\\.[A-Za-z_][A-Za-z_0-9]*)*(\\$[A-Za-z_0-9]+)*$)|^\\[+([BCDFIJSZ]|L[A-Za-z_][A-Za-z_0-9]*(\\.[A-Za-z_][A-Za-z_0-9]*)*(\\$[A-Za-z_0-9]+)*;)$"; 479 480 private static final Pattern classGetNamePattern; 481 482 static { 483 try { 484 classGetNamePattern = Pattern.compile(classGetNameRegex); 485 } catch (PatternSyntaxException e) { 486 // This shouldn't happen because classGetNameRegex is a legal regex 487 throw new Error(e); 488 } 489 } 490 491 public static @MonotonicNonNull File server_dir = 492 null; // YOAV: the directory from which we read the dtrace files 493 494 /** 495 * A PptMap (mapping from String to PptTopLevel) that contains all the program points. Set in 496 * mainHelper(). 497 */ 498 @SuppressWarnings("nullness:initialization.static.field.uninitialized") // set in mainHelper() 499 public static PptMap all_ppts; 500 501 /** current invariant (used for debugging) */ 502 public static @Nullable Invariant current_inv = null; 503 504 /* List of prototype invariants (one for each type of invariant) */ 505 public static ArrayList<@Prototype Invariant> proto_invs = new ArrayList<>(); 506 507 /** Debug tracer. */ 508 public static final Logger debugTrace = Logger.getLogger("daikon.Daikon"); 509 510 public static final Logger debugProgress = Logger.getLogger("daikon.Progress"); 511 512 public static final Logger debugEquality = Logger.getLogger("daikon.Equality"); 513 514 /** Debug tracer for ppt initialization. */ 515 public static final Logger debugInit = Logger.getLogger("daikon.init"); 516 517 /** Prints out statistics concerning equality sets, suppressions, etc. */ 518 public static final Logger debugStats = Logger.getLogger("daikon.stats"); 519 520 /** The usage message for this program. */ 521 static String usage = 522 StringsPlume.joinLines( 523 release_string, 524 // "Uses the Java port of GNU getopt, copyright (c) 1998 Aaron M. Renn", 525 // "For licensing information, see the License section of the manual.", 526 "Usage:", 527 " java daikon.Daikon [flags...] files...", 528 " Each file is a declaration file or a data trace file; the file type", 529 " is determined by the file name (containing \".decls\" or \".dtrace\").", 530 " For a list of flags, see the Daikon manual, which appears in the ", 531 " Daikon distribution and also at http://plse.cs.washington.edu/daikon/."); 532 533 /** Indicates the need for Daikon to terminate. */ 534 public abstract static class DaikonTerminationException extends RuntimeException { 535 static final long serialVersionUID = 20180729L; 536 537 protected DaikonTerminationException() { 538 super(); 539 } 540 541 protected DaikonTerminationException(String message) { 542 super(message); 543 } 544 545 protected DaikonTerminationException(Throwable e) { 546 super(e); 547 } 548 549 protected DaikonTerminationException(String message, Throwable e) { 550 super(message, e); 551 } 552 } 553 554 /** Indicates that Daikon has terminated normally. */ 555 public static class NormalTermination extends DaikonTerminationException { 556 static final long serialVersionUID = 20180729L; 557 558 public NormalTermination(String message) { 559 super(message); 560 } 561 562 public NormalTermination() { 563 super(); 564 } 565 } 566 567 /** 568 * Indicates that Daikon has terminated abnormally, indicating a bug in Daikon. Also used to 569 * indicate a situation that should not happen. 570 */ 571 public static class BugInDaikon extends DaikonTerminationException { 572 static final long serialVersionUID = 20180729L; 573 574 public BugInDaikon(String message) { 575 super(message); 576 } 577 578 public BugInDaikon(Throwable e) { 579 super(e); 580 } 581 582 public BugInDaikon(String message, Throwable e) { 583 super(message, e); 584 } 585 } 586 587 /** 588 * Indicates a user error. Thrown to indicate that main should not print a stack trace, but only 589 * print the message itself to the user. 590 * 591 * <p>Code in Daikon should throw other exceptions such as BugInDaikon in cases of a Daikon bug or 592 * a system problem (like unpredictable IOExceptions). If the string is null, then this is normal 593 * termination, not an error; no message is printed. 594 */ 595 public static class UserError extends DaikonTerminationException { 596 static final long serialVersionUID = 20050923L; 597 598 public static String error_at_line_file(LineNumberReader reader, String filename, Throwable e) { 599 String msg = e.getMessage(); 600 if (msg == null) { 601 msg = " of type " + e.getClass() + " with no detail message"; 602 } 603 return error_at_line_file(reader, filename, msg); 604 } 605 606 public static String error_at_line_file(LineNumberReader reader, String filename, String msg) { 607 if (msg == null) { 608 throw new Error("Null message supplied to error_at_line_file()"); 609 } 610 return "Error at line " + reader.getLineNumber() + " in file " + filename + ": " + msg; 611 } 612 613 /// Constructors that take a Throwable 614 615 // Requires that e.getMessage() != null. 616 public UserError(Throwable e) { 617 super(e.getMessage() == null ? e.toString() : e.getMessage(), e); 618 } 619 620 public UserError(Throwable e, String msg) { 621 super( 622 ((e.getMessage() != null && msg.contains(e.getMessage())) 623 ? msg 624 : msg + ": " + e.getMessage()), 625 e); 626 } 627 628 public UserError(Throwable e, FileIO.ParseState state) { 629 this(e, error_at_line_file(state.reader, state.filename, e)); 630 } 631 632 public UserError(Throwable e, LineNumberReader reader, String filename) { 633 this(e, error_at_line_file(reader, filename, e)); 634 } 635 636 public UserError(Throwable e, String msg, LineNumberReader reader, String filename) { 637 this(e, error_at_line_file(reader, filename, msg)); 638 } 639 640 /// Constructors that do not take a Throwable 641 642 public UserError() { 643 super(""); 644 } 645 646 public UserError(String s) { 647 super(s); 648 } 649 650 public UserError(String msg, FileIO.ParseState state) { 651 super(error_at_line_file(state.reader, state.filename, msg)); 652 } 653 654 public UserError(String msg, LineNumberReader reader, String filename) { 655 super(error_at_line_file(reader, filename, msg)); 656 } 657 // This constructor is too error-prone: it leads to throwing away 658 // subsequent args if there are not enough % directives in the string. 659 // public UserError(String format, @Nullable Object... args) { 660 // super (String.format (format, args)); 661 // } 662 } 663 664 /** A parser error that should be reported, with better context, by the caller. */ 665 public static class ParseError extends Exception { 666 static final long serialVersionUID = 20181021L; 667 668 ParseError(String s) { 669 super(s); 670 } 671 } 672 673 /** 674 * The arguments to daikon.Daikon are file names. Declaration file names end in ".decls", and data 675 * trace file names end in ".dtrace". 676 */ 677 public static void main(final String[] args) { 678 try { 679 mainHelper(args); 680 } catch (DaikonTerminationException e) { 681 handleDaikonTerminationException(e); 682 } 683 } 684 685 /** 686 * Handle DaikonTerminationExceptions. Others are left to be handled by the default handler, which 687 * prints a more informative stack trace. 688 */ 689 public static void handleDaikonTerminationException(DaikonTerminationException e) { 690 if (e instanceof NormalTermination) { 691 System.out.println(); 692 if (e.getMessage() != null) { 693 System.out.println(e.getMessage()); 694 } 695 System.exit(0); 696 } else if (e instanceof UserError) { 697 System.err.println(); 698 System.err.println(e.getMessage()); 699 if (Debug.dkconfig_show_stack_trace) { 700 e.printStackTrace(); 701 } 702 System.exit(1); 703 } else if (e instanceof BugInDaikon) { 704 System.err.println(); 705 System.err.println("Bug in Daikon. Please report."); 706 e.printStackTrace(System.err); 707 System.err.println("Bug in Daikon. Please report."); 708 System.exit(2); 709 } else { 710 // This caes should never be executed. 711 System.err.println(); 712 System.err.println("Bug in Daikon. Please report."); 713 e.printStackTrace(System.err); 714 System.err.println("Bug in Daikon. Please report."); 715 System.exit(2); 716 } 717 } 718 719 /** 720 * This does the work of {@link #main}, but it never calls System.exit, so it is appropriate to be 721 * called progrmmatically. 722 * 723 * @param args the command-line arguments 724 */ 725 @SuppressWarnings("nullness:contracts.precondition") // private field 726 public static void mainHelper(final String[] args) { 727 long startTime = System.nanoTime(); 728 long duration; 729 730 // Cleanup from any previous runs 731 cleanup(); 732 733 // Read command line options 734 FileOptions files = read_options(args, usage); 735 Set<File> decls_files = files.decls; 736 Set<String> dtrace_files = files.dtrace; 737 Set<File> spinfo_files = files.spinfo; 738 Set<File> map_files = files.map; 739 if (server_dir == null && (decls_files.size() == 0) && (dtrace_files.size() == 0)) { 740 System.out.println("No .decls or .dtrace files specified"); 741 throw new Daikon.UserError("No .decls or .dtrace files specified"); 742 } 743 744 // Never disable splitting for csharp format. 745 if (Daikon.dkconfig_undo_opts && Daikon.output_format != OutputFormat.CSHARPCONTRACT) { 746 PptSplitter.dkconfig_disable_splitting = true; 747 } 748 749 if (Daikon.dkconfig_quiet) { 750 Daikon.dkconfig_progress_delay = -1; 751 } 752 if (System.console() == null && !show_progress) { 753 // not connected to a terminal 754 Daikon.dkconfig_progress_delay = -1; 755 } 756 757 // Set up debug traces; note this comes after reading command line options. 758 LogHelper.setupLogs(Global.debugAll ? FINE : INFO); 759 760 if (!noversion_output) { 761 if (!Daikon.dkconfig_quiet) { 762 System.out.println(release_string); 763 } 764 } 765 766 // figure out which algorithm to use in NIS to process suppressions 767 if (NIS.dkconfig_suppression_processor == SuppressionProcessor.HYBRID) { 768 NIS.hybrid_method = true; 769 } else { 770 if (NIS.dkconfig_suppression_processor == SuppressionProcessor.ANTECEDENT) { 771 NIS.antecedent_method = true; 772 NIS.hybrid_method = false; 773 } else { 774 assert (NIS.dkconfig_suppression_processor == SuppressionProcessor.FALSIFIED); 775 NIS.antecedent_method = false; 776 NIS.hybrid_method = false; 777 } 778 } 779 780 // Create the list of all invariant types 781 setup_proto_invs(); 782 783 if (PrintInvariants.print_discarded_invariants) { 784 DiscReasonMap.initialize(); 785 } 786 787 fileio_progress = new FileIOProgress(); 788 fileio_progress.start(); 789 790 // Load declarations and splitters 791 load_spinfo_files(spinfo_files); 792 all_ppts = load_decls_files(decls_files); 793 load_map_files(map_files); 794 795 all_ppts.trimToSize(); 796 797 // Only for assertion checks 798 isInferencing = true; 799 800 // Infer invariants 801 process_data(all_ppts, dtrace_files); 802 isInferencing = false; 803 if (Debug.logOn()) { 804 Debug.check(all_ppts, "After process data"); 805 } 806 807 // If requested, just calculate the total number of invariants possible 808 if (dkconfig_calc_possible_invs) { 809 fileio_progress.shouldStop = true; 810 int total_invs = 0; 811 // Can't use new for syntax because the default iterator for all_ppts 812 // is not the one I want here. 813 for (PptTopLevel ppt : all_ppts.ppt_all_iterable()) { 814 System.out.printf("Processing %s with %d variables", ppt.name(), ppt.var_infos.length); 815 int inv_cnt = 0; 816 if (ppt.var_infos.length > 1600) { 817 System.out.println("Skipping, too many variables!"); 818 } else { 819 inv_cnt = ppt.getInvariants().size(); 820 System.out.println(" " + inv_cnt + " invariants"); 821 total_invs += inv_cnt; 822 } 823 } 824 System.out.println(total_invs + " invariants total"); 825 return; 826 } 827 828 if (suppress_redundant_invariants_with_simplify) { 829 suppressWithSimplify(all_ppts); 830 } 831 832 // Check that PptMap created was correct 833 all_ppts.repCheck(); 834 835 // Remove undesired invariants, if requested 836 if (omit_from_output) { 837 processOmissions(all_ppts); 838 } 839 840 debugProgress.fine(" Writing Serialized Pptmap ... "); 841 long startWriteTime = System.nanoTime(); 842 // Write serialized output - must be done before guarding invariants 843 if (inv_file != null) { 844 try { 845 FileIO.write_serialized_pptmap(all_ppts, inv_file); 846 } catch (IOException e) { 847 throw new RuntimeException("Error while writing .inv file: " + inv_file, e); 848 } 849 } 850 duration = System.nanoTime() - startWriteTime; 851 debugProgress.fine( 852 " Writing Serialized Pptmap ... done [" + TimeUnit.NANOSECONDS.toSeconds(duration) + "]"); 853 854 // if ((Daikon.dkconfig_guardNulls == "always") // interned 855 // || (Daikon.dkconfig_guardNulls == "missing")) { // interned 856 // // This side-effects the PptMap, but it has already been saved 857 // // to disk and is now being used only for printing. 858 // guardInvariants(all_ppts); 859 // } 860 861 // Debug print information about the variables 862 if (false) { 863 for (PptTopLevel ppt : all_ppts.all_ppts()) { 864 System.out.printf("Dumping variables for ppt %s%n", ppt.name()); 865 for (VarInfo vi : ppt.var_infos) { 866 System.out.printf(" vi %s%n", vi); 867 System.out.printf(" file_rep_type = %s%n", vi.file_rep_type); 868 System.out.printf(" type = %s%n", vi.type); 869 } 870 } 871 } 872 873 // print out the invariants for each program point 874 if (Daikon.dkconfig_undo_opts) { 875 // Print out the invariants for each program point (sort first) 876 for (PptTopLevel ppt : all_ppts.pptIterable()) { 877 878 // We do not need to print out program points that have not seen 879 // any samples. 880 if (ppt.num_samples() == 0) { 881 continue; 882 } 883 List<Invariant> invs = PrintInvariants.sort_invariant_list(ppt.invariants_vector()); 884 List<Invariant> filtered_invs = filter_invs(invs); 885 886 // Debugging output. Sometimes the program points actually differ in number of samples seen 887 // due to differences in how Daikon and DaikonSimple see the variable hierarchy. 888 if (false) { 889 System.out.println("===================================================="); 890 System.out.println(ppt.name()); 891 System.out.println(ppt.num_samples()); 892 893 for (Invariant inv : filtered_invs) { 894 System.out.println(inv.getClass()); 895 System.out.println(inv); 896 } 897 } 898 } 899 900 // exit the program 901 if (false) { 902 return; 903 } 904 } 905 906 // Display invariants 907 if (output_num_samples) { 908 System.out.println("The --output_num_samples debugging flag is on."); 909 System.out.println("Some of the debugging output may only make sense to Daikon programmers."); 910 } 911 912 // If they want to see discarded invariants, they probably don't 913 // want to see the true ones. 914 if (!PrintInvariants.print_discarded_invariants) { 915 PrintInvariants.print_invariants(all_ppts); 916 } else { 917 PrintInvariants.print_reasons(all_ppts); 918 } 919 920 if (output_num_samples) { 921 Global.output_statistics(); 922 } 923 if (dkconfig_print_sample_totals) { 924 System.out.println(FileIO.samples_processed + " samples processed"); 925 } 926 927 // print statistics concerning what invariants are printed 928 if (debugStats.isLoggable(FINE)) { 929 for (PptTopLevel ppt : all_ppts.ppt_all_iterable()) { 930 PrintInvariants.print_filter_stats(debugStats, ppt, all_ppts); 931 } 932 } 933 934 duration = System.nanoTime() - startTime; 935 debugProgress.fine(" Total time spent in Daikon: " + TimeUnit.NANOSECONDS.toSeconds(duration)); 936 937 // Done 938 if (!Daikon.dkconfig_quiet) { 939 System.out.println("Exiting Daikon."); 940 } 941 } 942 943 /** Cleans up static variables so that mainHelper can be called more than once. */ 944 @SuppressWarnings("nullness") // reinitialization 945 public static void cleanup() { 946 947 // Stop the thread that prints out progress information 948 if ((fileio_progress != null) && (fileio_progress.getState() != Thread.State.NEW)) { 949 fileio_progress.shouldStop = true; 950 try { 951 fileio_progress.join(2000); 952 } catch (InterruptedException e) { 953 // It's OK for a wait operation to be interrupted. 954 } 955 if (fileio_progress.getState() != Thread.State.TERMINATED) { 956 throw new BugInDaikon("Can't stop fileio_progress thead"); 957 } 958 } 959 fileio_progress = null; 960 progress = ""; 961 962 // Reset statics. Unfortunately, these must match the settings where 963 // these are declared and I don't know how to do that automatically. 964 inv_file = null; 965 no_text_output = false; 966 show_progress = false; 967 output_format = OutputFormat.DAIKON; 968 noversion_output = false; 969 output_num_samples = false; 970 omit_from_output = false; 971 omit_types = new boolean[256]; 972 use_dataflow_hierarchy = true; 973 suppress_redundant_invariants_with_simplify = false; 974 ppt_regexp = null; 975 ppt_omit_regexp = null; 976 var_regexp = null; 977 var_omit_regexp = null; 978 server_dir = null; 979 use_mem_monitor = false; 980 981 proto_invs.clear(); 982 } 983 984 // Structure for return value of read_options. 985 // Return an array of {decls, dtrace, spinfo, map} files. 986 public static class FileOptions { 987 public Set<File> decls; 988 public Set<String> dtrace; 989 public Set<File> spinfo; 990 public Set<File> map; 991 992 public FileOptions(Set<File> decls, Set<String> dtrace, Set<File> spinfo, Set<File> map) { 993 this.decls = decls; 994 this.dtrace = dtrace; 995 this.spinfo = spinfo; 996 this.map = map; 997 } 998 } 999 1000 /////////////////////////////////////////////////////////////////////////// 1001 // Read in the command line options 1002 // Return {decls, dtrace, spinfo, map} files. 1003 static FileOptions read_options(String[] args, String usage) { 1004 if (args.length == 0) { 1005 System.out.println("Error: no files supplied on command line."); 1006 System.out.println(usage); 1007 throw new Daikon.UserError(); 1008 } 1009 1010 // LinkedHashSet because it can be confusing to users if files (of the 1011 // same type) are gratuitously processed in a different order than they 1012 // were supplied on the command line. 1013 HashSet<File> decl_files = new LinkedHashSet<>(); 1014 HashSet<String> dtrace_files = new LinkedHashSet<>(); // file names or "-" or "+" 1015 HashSet<File> spinfo_files = new LinkedHashSet<>(); 1016 HashSet<File> map_files = new LinkedHashSet<>(); 1017 1018 LongOpt[] longopts = 1019 new LongOpt[] { 1020 // Control output 1021 new LongOpt(help_SWITCH, LongOpt.NO_ARGUMENT, null, 0), 1022 new LongOpt(no_text_output_SWITCH, LongOpt.NO_ARGUMENT, null, 0), 1023 new LongOpt(format_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0), 1024 new LongOpt(show_progress_SWITCH, LongOpt.NO_ARGUMENT, null, 0), 1025 new LongOpt(show_detail_progress_SWITCH, LongOpt.NO_ARGUMENT, null, 0), 1026 new LongOpt(no_show_progress_SWITCH, LongOpt.NO_ARGUMENT, null, 0), 1027 new LongOpt(noversion_SWITCH, LongOpt.NO_ARGUMENT, null, 0), 1028 new LongOpt(output_num_samples_SWITCH, LongOpt.NO_ARGUMENT, null, 0), 1029 new LongOpt(files_from_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0), 1030 new LongOpt(omit_from_output_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0), 1031 // Control invariant detection 1032 new LongOpt(conf_limit_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0), 1033 new LongOpt(list_type_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0), 1034 new LongOpt(user_defined_invariant_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0), 1035 new LongOpt(disable_all_invariants_SWITCH, LongOpt.NO_ARGUMENT, null, 0), 1036 new LongOpt(no_dataflow_hierarchy_SWITCH, LongOpt.NO_ARGUMENT, null, 0), 1037 new LongOpt(suppress_redundant_SWITCH, LongOpt.NO_ARGUMENT, null, 0), 1038 // Process only part of the trace file 1039 new LongOpt(ppt_regexp_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0), 1040 new LongOpt(ppt_omit_regexp_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0), 1041 new LongOpt(var_regexp_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0), 1042 new LongOpt(var_omit_regexp_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0), 1043 // Configuration options 1044 new LongOpt(server_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0), 1045 new LongOpt(config_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0), 1046 new LongOpt(config_option_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0), 1047 // Debugging 1048 new LongOpt(debugAll_SWITCH, LongOpt.NO_ARGUMENT, null, 0), 1049 new LongOpt(debug_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0), 1050 new LongOpt(track_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0), 1051 new LongOpt(disc_reason_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0), 1052 new LongOpt(mem_stat_SWITCH, LongOpt.NO_ARGUMENT, null, 0), 1053 }; 1054 Getopt g = new Getopt("daikon.Daikon", args, "ho:", longopts); 1055 int c; 1056 1057 while ((c = g.getopt()) != -1) { 1058 switch (c) { 1059 case 0: 1060 // got a long option 1061 String option_name = longopts[g.getLongind()].getName(); 1062 1063 // Control output 1064 if (help_SWITCH.equals(option_name)) { 1065 System.out.println(usage); 1066 throw new Daikon.NormalTermination(); 1067 } else if (no_text_output_SWITCH.equals(option_name)) { 1068 no_text_output = true; 1069 } else if (format_SWITCH.equals(option_name)) { 1070 String format_name = getOptarg(g); 1071 Daikon.output_format = OutputFormat.get(format_name); 1072 if (Daikon.output_format == null) { 1073 throw new Daikon.UserError("Unknown output format: --format " + format_name); 1074 } 1075 } else if (show_progress_SWITCH.equals(option_name)) { 1076 show_progress = true; 1077 LogHelper.setLevel("daikon.Progress", FINE); 1078 } else if (show_detail_progress_SWITCH.equals(option_name)) { 1079 show_progress = true; 1080 LogHelper.setLevel("daikon.Progress", FINER); 1081 } else if (no_show_progress_SWITCH.equals(option_name)) { 1082 show_progress = false; 1083 } else if (noversion_SWITCH.equals(option_name)) { 1084 noversion_output = true; 1085 } else if (output_num_samples_SWITCH.equals(option_name)) { 1086 output_num_samples = true; 1087 } else if (files_from_SWITCH.equals(option_name)) { 1088 String files_from_filename = getOptarg(g); 1089 try (EntryReader entryReader = new EntryReader(files_from_filename)) { 1090 for (String filename : entryReader) { 1091 // Ignore blank lines in file. 1092 if (filename.equals("")) { 1093 continue; 1094 } 1095 // This code is duplicated below outside the options loop. 1096 // These aren't "endsWith()" because there might be a suffix 1097 // on the end (eg, a date, or ".gz"). 1098 File file = new File(filename); 1099 if (!file.exists()) { 1100 throw new Daikon.UserError("File " + filename + " not found."); 1101 } 1102 if (filename.indexOf(".decls") != -1) { 1103 decl_files.add(file); 1104 } else if (filename.indexOf(".dtrace") != -1) { 1105 dtrace_files.add(filename); 1106 } else if (filename.indexOf(".spinfo") != -1) { 1107 spinfo_files.add(file); 1108 } else if (filename.indexOf(".map") != -1) { 1109 map_files.add(file); 1110 } else { 1111 throw new Daikon.UserError("Unrecognized file extension: " + filename); 1112 } 1113 } 1114 } catch (IOException e) { 1115 throw new RuntimeException( 1116 String.format("Error reading --files_from file: %s", files_from_filename)); 1117 } 1118 break; 1119 } else if (omit_from_output_SWITCH.equals(option_name)) { 1120 String f = getOptarg(g); 1121 for (int i = 0; i < f.length(); i++) { 1122 if ("0rs".indexOf(f.charAt(i)) == -1) { 1123 throw new Daikon.UserError( 1124 "omit_from_output flag letter '" + f.charAt(i) + "' is unknown"); 1125 } 1126 omit_types[f.charAt(i)] = true; 1127 } 1128 omit_from_output = true; 1129 } 1130 // Control invariant detection 1131 else if (conf_limit_SWITCH.equals(option_name)) { 1132 double limit = Double.parseDouble(getOptarg(g)); 1133 if ((limit < 0.0) || (limit > 1.0)) { 1134 throw new Daikon.UserError(conf_limit_SWITCH + " must be between [0..1]"); 1135 } 1136 Configuration.getInstance() 1137 .apply("daikon.inv.Invariant.confidence_limit", String.valueOf(limit)); 1138 } else if (list_type_SWITCH.equals(option_name)) { 1139 try { 1140 String list_type_string = getOptarg(g); 1141 ProglangType.list_implementors.add(list_type_string); 1142 } catch (Exception e) { 1143 throw new Daikon.UserError("Problem parsing " + list_type_SWITCH + " option: " + e); 1144 } 1145 break; 1146 } else if (user_defined_invariant_SWITCH.equals(option_name)) { 1147 try { 1148 String user_defined_invariant_string = getOptarg(g); 1149 Matcher m = classGetNamePattern.matcher(user_defined_invariant_string); 1150 if (!m.matches()) { 1151 throw new Daikon.UserError( 1152 "Bad argument " 1153 + user_defined_invariant_string 1154 + " for " 1155 + ppt_regexp_SWITCH 1156 + ": not in the format required by Class.getName(String)"); 1157 } 1158 @SuppressWarnings("signature") // Regex match guarantees the format of Class.getName() 1159 @ClassGetName String cname = user_defined_invariant_string; 1160 userDefinedInvariants.add(cname); 1161 } catch (Exception e) { 1162 throw new Daikon.UserError( 1163 "Problem parsing " + user_defined_invariant_SWITCH + " option: " + e); 1164 } 1165 break; 1166 } else if (disable_all_invariants_SWITCH.equals(option_name)) { 1167 // There are two possibilities: 1168 // * a given invariant class is not yet loaded, in which case 1169 // we set the default value for its dkconfig_enabled field. 1170 // * a given invariant class is already loaded, in which case 1171 // we reflectively set its dkconfig_enabled to false. 1172 1173 // Set the default for not-yet-loaded invariants. 1174 Invariant.invariantEnabledDefault = false; 1175 1176 // Get all loaded classes. This solution is from 1177 // http://stackoverflow.com/a/10261850/173852 . Alternate approach: 1178 // http://stackoverflow.com/questions/2548384/java-get-a-list-of-all-classes-loaded-in-the-jvm 1179 Field f; 1180 try { 1181 f = ClassLoader.class.getDeclaredField("classes"); 1182 } catch (NoSuchFieldException e) { 1183 throw new Daikon.BugInDaikon("Didn't find field ClassLoader.classes"); 1184 } 1185 f.setAccessible(true); 1186 Object classesAsObject; 1187 { 1188 ClassLoader cl = Thread.currentThread().getContextClassLoader(); 1189 if (cl == null) { 1190 throw new Daikon.BugInDaikon( 1191 "Need to handle when getContextClassLoader returns null"); 1192 } 1193 try { 1194 classesAsObject = f.get(cl); 1195 } catch (IllegalAccessException e) { 1196 throw new Daikon.BugInDaikon("Field ClassLoader.classes was not made accessible"); 1197 } 1198 } 1199 @SuppressWarnings({ 1200 "unchecked", // type of ClassLoader.classes field is known 1201 "nullness" // ClassLoader.classes is non-null 1202 }) 1203 @NonNull List<Class<?>> classes = (List<Class<?>>) classesAsObject; 1204 for (int i = 0; i < classes.size(); i++) { 1205 Class<?> loadedClass = classes.get(i); 1206 if (Invariant.class.isAssignableFrom(loadedClass)) { 1207 @SuppressWarnings("unchecked") // loadedClass is a subclass of Invariant 1208 Class<? extends Invariant> invType = (Class<? extends Invariant>) loadedClass; 1209 try { 1210 Field field = invType.getField("dkconfig_enabled"); 1211 if (field.getType() != Boolean.TYPE) { 1212 throw new Daikon.BugInDaikon( 1213 "Field " 1214 + invType 1215 + ".dkconfig_enabled has type " 1216 + field.getType() 1217 + " instead of boolean"); 1218 } else { 1219 setStaticField(field, false); 1220 // System.out.println( 1221 // "Set field " 1222 // + invType 1223 // + ".dkconfig_enabled to false"); 1224 } 1225 } catch (NoSuchFieldException e) { 1226 // System.out.println( 1227 // "Class " + invType + " does not have a dkconfig_enabled field"); 1228 } catch (IllegalAccessException e) { 1229 throw new Daikon.BugInDaikon( 1230 "IllegalAccessException for field " + invType + ".dkconfig_enabled"); 1231 } 1232 } 1233 } 1234 } else if (no_dataflow_hierarchy_SWITCH.equals(option_name)) { 1235 use_dataflow_hierarchy = false; 1236 } else if (suppress_redundant_SWITCH.equals(option_name)) { 1237 suppress_redundant_invariants_with_simplify = true; 1238 } 1239 1240 // Process only part of the trace file 1241 else if (ppt_regexp_SWITCH.equals(option_name)) { 1242 if (ppt_regexp != null) { 1243 throw new Daikon.UserError( 1244 "multiple --" 1245 + ppt_regexp_SWITCH 1246 + " regular expressions supplied on command line"); 1247 } 1248 String regexp_string = getOptarg(g); 1249 if (!RegexUtil.isRegex(regexp_string)) { 1250 throw new Daikon.UserError( 1251 "Bad regexp " 1252 + regexp_string 1253 + " for " 1254 + ppt_regexp_SWITCH 1255 + ": " 1256 + RegexUtil.regexError(regexp_string)); 1257 } 1258 ppt_regexp = Pattern.compile(regexp_string); 1259 break; 1260 } else if (ppt_omit_regexp_SWITCH.equals(option_name)) { 1261 if (ppt_omit_regexp != null) { 1262 throw new Daikon.UserError( 1263 "multiple --" 1264 + ppt_omit_regexp_SWITCH 1265 + " regular expressions supplied on command line"); 1266 } 1267 String regexp_string = getOptarg(g); 1268 if (!RegexUtil.isRegex(regexp_string)) { 1269 throw new Daikon.UserError( 1270 "Bad regexp " 1271 + regexp_string 1272 + " for " 1273 + ppt_omit_regexp_SWITCH 1274 + ": " 1275 + RegexUtil.regexError(regexp_string)); 1276 } 1277 ppt_omit_regexp = Pattern.compile(regexp_string); 1278 break; 1279 } else if (var_regexp_SWITCH.equals(option_name)) { 1280 if (var_regexp != null) { 1281 throw new Daikon.UserError( 1282 "multiple --" 1283 + var_regexp_SWITCH 1284 + " regular expressions supplied on command line"); 1285 } 1286 String regexp_string = getOptarg(g); 1287 if (!RegexUtil.isRegex(regexp_string)) { 1288 throw new Daikon.UserError( 1289 "Bad regexp " 1290 + regexp_string 1291 + " for " 1292 + var_regexp_SWITCH 1293 + ": " 1294 + RegexUtil.regexError(regexp_string)); 1295 } 1296 var_regexp = Pattern.compile(regexp_string); 1297 break; 1298 } else if (var_omit_regexp_SWITCH.equals(option_name)) { 1299 if (var_omit_regexp != null) { 1300 throw new Daikon.UserError( 1301 "multiple --" 1302 + var_omit_regexp_SWITCH 1303 + " regular expressions supplied on command line"); 1304 } 1305 String regexp_string = getOptarg(g); 1306 if (!RegexUtil.isRegex(regexp_string)) { 1307 throw new Daikon.UserError( 1308 "Bad regexp " 1309 + regexp_string 1310 + " for " 1311 + var_omit_regexp_SWITCH 1312 + ": " 1313 + RegexUtil.regexError(regexp_string)); 1314 } 1315 var_omit_regexp = Pattern.compile(regexp_string); 1316 break; 1317 } else if (server_SWITCH.equals(option_name)) { 1318 String input_dir = getOptarg(g); 1319 server_dir = new File(input_dir); 1320 if (!server_dir.isDirectory() || !server_dir.canRead() || !server_dir.canWrite()) { 1321 throw new RuntimeException( 1322 "Could not open config file in server directory " + server_dir); 1323 } 1324 break; 1325 1326 // Configuration options 1327 1328 } else if (config_SWITCH.equals(option_name)) { 1329 String config_file = getOptarg(g); 1330 try (InputStream stream = new FileInputStream(config_file)) { 1331 Configuration.getInstance().apply(stream); 1332 } catch (IOException e) { 1333 throw new Daikon.UserError( 1334 // Is this the only possible reason for an IOException? 1335 "Could not open config file " + config_file); 1336 } 1337 break; 1338 } else if (config_option_SWITCH.equals(option_name)) { 1339 String item = getOptarg(g); 1340 try { 1341 Configuration.getInstance().apply(item); 1342 } catch (daikon.config.Configuration.ConfigException e) { 1343 throw new Daikon.UserError(e); 1344 } 1345 break; 1346 } else if (debugAll_SWITCH.equals(option_name)) { 1347 Global.debugAll = true; 1348 } else if (debug_SWITCH.equals(option_name)) { 1349 LogHelper.setLevel(getOptarg(g), FINE); 1350 } else if (track_SWITCH.equals(option_name)) { 1351 LogHelper.setLevel("daikon.Debug", FINE); 1352 String error = Debug.add_track(getOptarg(g)); 1353 if (error != null) { 1354 throw new Daikon.UserError( 1355 "Error parsing track argument '" + getOptarg(g) + "' - " + error); 1356 } 1357 } else if (disc_reason_SWITCH.equals(option_name)) { 1358 try { 1359 PrintInvariants.discReasonSetup(getOptarg(g)); 1360 } catch (IllegalArgumentException e) { 1361 throw new Daikon.UserError(e); 1362 } 1363 } else if (mem_stat_SWITCH.equals(option_name)) { 1364 use_mem_monitor = true; 1365 } else { 1366 throw new Daikon.UserError("Unknown option " + option_name + " on command line"); 1367 } 1368 break; 1369 case 'h': 1370 System.out.println(usage); 1371 throw new Daikon.NormalTermination(); 1372 case 'o': 1373 String inv_filename = getOptarg(g); 1374 1375 if (inv_file != null) { 1376 throw new Daikon.UserError( 1377 "multiple serialization output files supplied on command line: " 1378 + inv_file 1379 + " " 1380 + inv_filename); 1381 } 1382 1383 inv_file = new File(inv_filename); 1384 1385 if (!FilesPlume.canCreateAndWrite(inv_file)) { 1386 throw new Daikon.UserError("Cannot write to serialization output file " + inv_file); 1387 } 1388 break; 1389 // 1390 case '?': 1391 // break; // getopt() already printed an error 1392 System.out.println(usage); 1393 throw new Daikon.NormalTermination(); 1394 // 1395 default: 1396 throw new Daikon.BugInDaikon("getopt() returned " + c); 1397 } 1398 } 1399 1400 // This code is duplicated above within the switch processing. 1401 // First check that all the file names are OK, so we don't do lots of 1402 // processing only to bail out at the end. 1403 for (int i = g.getOptind(); i < args.length; i++) { 1404 String filename = args[i]; 1405 if (filename.equals("-") || filename.equals("+")) { 1406 dtrace_files.add(filename); 1407 continue; 1408 } 1409 1410 File file = new File(filename); 1411 if (!file.exists()) { 1412 throw new Daikon.UserError("File " + file + " not found."); 1413 } 1414 filename = file.toString(); 1415 1416 // These aren't "endsWith()" because there might be a suffix on the end 1417 // (eg, a date or ".gz"). 1418 if (filename.indexOf(".decls") != -1) { 1419 decl_files.add(file); 1420 } else if (filename.indexOf(".dtrace") != -1) { 1421 dtrace_files.add(filename); 1422 // Always output an invariant file by default, even if none is 1423 // specified on the command line. 1424 if (inv_file == null) { 1425 String basename; 1426 // This puts the .inv file in the current directory. 1427 basename = new File(filename).getName(); 1428 // This puts the .inv file in the same directory as the .dtrace file. 1429 // basename = filename; 1430 int base_end = basename.indexOf(".dtrace"); 1431 String inv_filename = basename.substring(0, base_end) + ".inv.gz"; 1432 1433 inv_file = new File(inv_filename); 1434 if (!FilesPlume.canCreateAndWrite(inv_file)) { 1435 throw new Daikon.UserError("Cannot write to file " + inv_file); 1436 } 1437 } 1438 } else if (filename.indexOf(".spinfo") != -1) { 1439 spinfo_files.add(file); 1440 } else if (filename.indexOf(".map") != -1) { 1441 map_files.add(file); 1442 } else { 1443 throw new Daikon.UserError("Unrecognized file type: " + file); 1444 } 1445 } 1446 1447 // Set the fuzzy float comparison ratio. This needs to be done after 1448 // any configuration options (which may set the ratio) are processed. 1449 Global.fuzzy.setRelativeRatio(Invariant.dkconfig_fuzzy_ratio); 1450 1451 // Setup ppt_max_name based on the specified percentage of ppts to process 1452 if (dkconfig_ppt_perc != 100) { 1453 ppt_max_name = setup_ppt_perc(decl_files, dkconfig_ppt_perc); 1454 System.out.println("Max ppt name = " + ppt_max_name); 1455 } 1456 1457 // Validate guardNulls option 1458 PrintInvariants.validateGuardNulls(); 1459 1460 return new FileOptions(decl_files, dtrace_files, spinfo_files, map_files); 1461 } 1462 1463 /** 1464 * Set a static field to the given value. 1465 * 1466 * @param field a field; must be static 1467 * @param value the value to set the field to 1468 * @throws IllegalAccessException if {@code field} is enforcing Java language access control and 1469 * the underlying field is either inaccessible or final 1470 */ 1471 // This method exists to reduce the scope of the warning suppression. 1472 @SuppressWarnings({ 1473 "nullness:argument", // field is static, so object may be null 1474 "interning:argument" // interning is not necessary for how this method is used 1475 }) 1476 private static void setStaticField(Field field, Object value) throws IllegalAccessException { 1477 field.set(null, value); 1478 } 1479 1480 /** 1481 * Just like {@code g.getOptarg()}, but only to be called in circumstances when the programmer 1482 * knows that the return value is non-null. 1483 * 1484 * @param g a command-line argument processor 1485 * @return the value for an argument found by {@code g} 1486 */ 1487 @Pure 1488 public static String getOptarg(Getopt g) { 1489 String result = g.getOptarg(); 1490 if (result == null) { 1491 throw new Error("getOptarg returned null for " + g); 1492 } 1493 return result; 1494 } 1495 1496 /** 1497 * Invariants passed on the command line with the {@code --user_defined_invariant} option. A list 1498 * of class names in the format required by {@link Class#forName(String)}. 1499 */ 1500 private static List<@ClassGetName String> userDefinedInvariants = 1501 new ArrayList<@ClassGetName String>(); 1502 1503 /** 1504 * Creates the list of prototype invariants for all Daikon invariants. New invariants must be 1505 * added to this list. 1506 */ 1507 public static void setup_proto_invs() { 1508 1509 // Unary scalar invariants 1510 { 1511 // OneOf (OneOf.java.jpp) 1512 proto_invs.add(OneOfScalar.get_proto()); 1513 proto_invs.add(OneOfFloat.get_proto()); 1514 proto_invs.add(OneOfString.get_proto()); 1515 1516 // NonZero (NonZero.java.jpp) 1517 proto_invs.add(NonZero.get_proto()); 1518 proto_invs.add(NonZeroFloat.get_proto()); 1519 1520 proto_invs.add(IsPointer.get_proto()); 1521 1522 // Lower and Upper bound (Bound.java.jpp) 1523 proto_invs.add(LowerBound.get_proto()); 1524 proto_invs.add(LowerBoundFloat.get_proto()); 1525 proto_invs.add(UpperBound.get_proto()); 1526 proto_invs.add(UpperBoundFloat.get_proto()); 1527 1528 // Modulus and NonModulus (Modulus.java and NonModulus.java) 1529 proto_invs.add(Modulus.get_proto()); 1530 proto_invs.add(NonModulus.get_proto()); 1531 1532 // Range invariant (Range.java.jpp) 1533 proto_invs.addAll(RangeInt.get_proto_all()); 1534 proto_invs.addAll(RangeFloat.get_proto_all()); 1535 1536 // Printable String 1537 proto_invs.add(PrintableString.get_proto()); 1538 1539 // Complete One Of 1540 proto_invs.add(CompleteOneOfString.get_proto()); 1541 proto_invs.add(CompleteOneOfScalar.get_proto()); 1542 1543 // Positive (x > 0) (Postive.java). Positive is a sample invariant 1544 // that is only included as an example. 1545 // proto_invs.add (Postive.get_proto()); 1546 } 1547 1548 // Unary sequence invariants 1549 { 1550 // OneOf (OneOf.java.jpp) 1551 proto_invs.add(OneOfSequence.get_proto()); 1552 proto_invs.add(OneOfFloatSequence.get_proto()); 1553 proto_invs.add(OneOfStringSequence.get_proto()); 1554 proto_invs.add(EltOneOf.get_proto()); 1555 proto_invs.add(EltOneOfFloat.get_proto()); 1556 proto_invs.add(EltOneOfString.get_proto()); 1557 1558 // Range invariant (Range.java.jpp) 1559 proto_invs.addAll(EltRangeInt.get_proto_all()); 1560 proto_invs.addAll(EltRangeFloat.get_proto_all()); 1561 1562 // Sequence Index Comparisons (SeqIndexComparison.java.jpp) 1563 proto_invs.add(SeqIndexIntEqual.get_proto()); 1564 proto_invs.add(SeqIndexIntNonEqual.get_proto()); 1565 proto_invs.add(SeqIndexIntGreaterEqual.get_proto()); 1566 proto_invs.add(SeqIndexIntGreaterThan.get_proto()); 1567 proto_invs.add(SeqIndexIntLessEqual.get_proto()); 1568 proto_invs.add(SeqIndexIntLessThan.get_proto()); 1569 proto_invs.add(SeqIndexFloatEqual.get_proto()); 1570 proto_invs.add(SeqIndexFloatNonEqual.get_proto()); 1571 proto_invs.add(SeqIndexFloatGreaterEqual.get_proto()); 1572 proto_invs.add(SeqIndexFloatGreaterThan.get_proto()); 1573 proto_invs.add(SeqIndexFloatLessEqual.get_proto()); 1574 proto_invs.add(SeqIndexFloatLessThan.get_proto()); 1575 1576 // foreach i compare a[i] to a[i+1] (EltwiseIntComparisons.java.jpp) 1577 proto_invs.add(EltwiseIntEqual.get_proto()); 1578 proto_invs.add(EltwiseIntLessEqual.get_proto()); 1579 proto_invs.add(EltwiseIntGreaterEqual.get_proto()); 1580 proto_invs.add(EltwiseIntLessThan.get_proto()); 1581 proto_invs.add(EltwiseIntGreaterThan.get_proto()); 1582 proto_invs.add(EltwiseFloatEqual.get_proto()); 1583 proto_invs.add(EltwiseFloatLessEqual.get_proto()); 1584 proto_invs.add(EltwiseFloatGreaterEqual.get_proto()); 1585 proto_invs.add(EltwiseFloatLessThan.get_proto()); 1586 proto_invs.add(EltwiseFloatGreaterThan.get_proto()); 1587 1588 // EltNonZero (EltNonZero.java.jpp) 1589 proto_invs.add(EltNonZero.get_proto()); 1590 proto_invs.add(EltNonZeroFloat.get_proto()); 1591 1592 // No Duplicates (NoDuplicates.java.jpp) 1593 proto_invs.add(NoDuplicates.get_proto()); 1594 proto_invs.add(NoDuplicatesFloat.get_proto()); 1595 1596 // Element bounds (Bound.java.jpp) 1597 proto_invs.add(EltLowerBound.get_proto()); 1598 proto_invs.add(EltUpperBound.get_proto()); 1599 proto_invs.add(EltLowerBoundFloat.get_proto()); 1600 proto_invs.add(EltUpperBoundFloat.get_proto()); 1601 1602 // CommonSequence (CommonSequence.java.jpp) 1603 proto_invs.add(CommonSequence.get_proto()); 1604 proto_invs.add(CommonFloatSequence.get_proto()); 1605 1606 // CommonStringSequence (CommonStringSubsequence.java) 1607 proto_invs.add(CommonStringSequence.get_proto()); 1608 } 1609 1610 // Binary scalar-scalar invariants 1611 { 1612 // Int, Float, String comparisons (from IntComparisons.java.jpp) 1613 proto_invs.add(IntEqual.get_proto()); 1614 proto_invs.add(IntNonEqual.get_proto()); 1615 proto_invs.add(IntLessThan.get_proto()); 1616 proto_invs.add(IntGreaterThan.get_proto()); 1617 proto_invs.add(IntLessEqual.get_proto()); 1618 proto_invs.add(IntGreaterEqual.get_proto()); 1619 proto_invs.add(FloatEqual.get_proto()); 1620 proto_invs.add(FloatNonEqual.get_proto()); 1621 proto_invs.add(FloatLessThan.get_proto()); 1622 proto_invs.add(FloatGreaterThan.get_proto()); 1623 proto_invs.add(FloatLessEqual.get_proto()); 1624 proto_invs.add(FloatGreaterEqual.get_proto()); 1625 proto_invs.add(StringEqual.get_proto()); 1626 proto_invs.add(StringNonEqual.get_proto()); 1627 proto_invs.add(StringLessThan.get_proto()); 1628 proto_invs.add(StringGreaterThan.get_proto()); 1629 proto_invs.add(StringLessEqual.get_proto()); 1630 proto_invs.add(StringGreaterEqual.get_proto()); 1631 1632 // LinearBinary over integer/float (from LinearBinary.java.jpp) 1633 proto_invs.add(LinearBinary.get_proto()); 1634 proto_invs.add(LinearBinaryFloat.get_proto()); 1635 1636 // Numeric invariants (from Numeric.java.jpp) 1637 proto_invs.addAll(NumericInt.get_proto_all()); 1638 proto_invs.addAll(NumericFloat.get_proto_all()); 1639 1640 // Standard binary string invariants 1641 proto_invs.addAll(StdString.get_proto_all()); 1642 } 1643 1644 // Binary sequence-sequence invariants 1645 { 1646 // Numeric invariants (from Numeric.java.jpp) 1647 proto_invs.addAll(PairwiseNumericInt.get_proto_all()); 1648 proto_invs.addAll(PairwiseNumericFloat.get_proto_all()); 1649 1650 // Pairwise string invariants (also from Numeric.java.jpp) 1651 proto_invs.addAll(PairwiseString.get_proto_all()); 1652 1653 // Lexical sequence comparisons (from SeqComparison.java.jpp) 1654 proto_invs.add(SeqSeqIntEqual.get_proto()); 1655 proto_invs.add(SeqSeqIntLessThan.get_proto()); 1656 proto_invs.add(SeqSeqIntGreaterThan.get_proto()); 1657 proto_invs.add(SeqSeqIntLessEqual.get_proto()); 1658 proto_invs.add(SeqSeqIntGreaterEqual.get_proto()); 1659 proto_invs.add(SeqSeqFloatEqual.get_proto()); 1660 proto_invs.add(SeqSeqFloatLessThan.get_proto()); 1661 proto_invs.add(SeqSeqFloatGreaterThan.get_proto()); 1662 proto_invs.add(SeqSeqFloatLessEqual.get_proto()); 1663 proto_invs.add(SeqSeqFloatGreaterEqual.get_proto()); 1664 proto_invs.add(SeqSeqStringEqual.get_proto()); 1665 proto_invs.add(SeqSeqStringLessThan.get_proto()); 1666 proto_invs.add(SeqSeqStringGreaterThan.get_proto()); 1667 proto_invs.add(SeqSeqStringLessEqual.get_proto()); 1668 proto_invs.add(SeqSeqStringGreaterEqual.get_proto()); 1669 1670 // Pairwise sequence comparisons (from PairwiseIntComparison.java.jpp) 1671 proto_invs.add(PairwiseIntEqual.get_proto()); 1672 proto_invs.add(PairwiseIntLessThan.get_proto()); 1673 proto_invs.add(PairwiseIntGreaterThan.get_proto()); 1674 proto_invs.add(PairwiseIntLessEqual.get_proto()); 1675 proto_invs.add(PairwiseIntGreaterEqual.get_proto()); 1676 proto_invs.add(PairwiseFloatEqual.get_proto()); 1677 proto_invs.add(PairwiseFloatLessThan.get_proto()); 1678 proto_invs.add(PairwiseFloatGreaterThan.get_proto()); 1679 proto_invs.add(PairwiseFloatLessEqual.get_proto()); 1680 proto_invs.add(PairwiseFloatGreaterEqual.get_proto()); 1681 proto_invs.add(PairwiseStringEqual.get_proto()); 1682 proto_invs.add(PairwiseStringLessThan.get_proto()); 1683 proto_invs.add(PairwiseStringGreaterThan.get_proto()); 1684 proto_invs.add(PairwiseStringLessEqual.get_proto()); 1685 proto_invs.add(PairwiseStringGreaterEqual.get_proto()); 1686 1687 // Array Reverse (from Reverse.java.jpp) 1688 proto_invs.add(Reverse.get_proto()); 1689 proto_invs.add(ReverseFloat.get_proto()); 1690 1691 // Pairwise Linear Binary (from PairwiseLinearBinary.java.jpp) 1692 proto_invs.add(PairwiseLinearBinary.get_proto()); 1693 proto_invs.add(PairwiseLinearBinaryFloat.get_proto()); 1694 1695 // Subset and Superset (from SubSet.java.jpp) 1696 proto_invs.add(SubSet.get_proto()); 1697 proto_invs.add(SuperSet.get_proto()); 1698 proto_invs.add(SubSetFloat.get_proto()); 1699 proto_invs.add(SuperSetFloat.get_proto()); 1700 1701 // Subsequence (from SubSequence.java.jpp) 1702 proto_invs.add(SubSequence.get_proto()); 1703 proto_invs.add(SubSequenceFloat.get_proto()); 1704 proto_invs.add(SuperSequence.get_proto()); 1705 proto_invs.add(SuperSequenceFloat.get_proto()); 1706 } 1707 1708 // Binary sequence-scalar invariants 1709 { 1710 // Comparison of scalar to each array element (SeqIntComparison.java.jpp) 1711 proto_invs.add(SeqIntEqual.get_proto()); 1712 proto_invs.add(SeqIntLessThan.get_proto()); 1713 proto_invs.add(SeqIntGreaterThan.get_proto()); 1714 proto_invs.add(SeqIntLessEqual.get_proto()); 1715 proto_invs.add(SeqIntGreaterEqual.get_proto()); 1716 proto_invs.add(SeqFloatEqual.get_proto()); 1717 proto_invs.add(SeqFloatLessThan.get_proto()); 1718 proto_invs.add(SeqFloatGreaterThan.get_proto()); 1719 proto_invs.add(SeqFloatLessEqual.get_proto()); 1720 proto_invs.add(SeqFloatGreaterEqual.get_proto()); 1721 1722 // Scalar is an element of the array (Member.java.jpp) 1723 proto_invs.add(Member.get_proto()); 1724 proto_invs.add(MemberFloat.get_proto()); 1725 proto_invs.add(MemberString.get_proto()); 1726 } 1727 1728 // Ternary invariants 1729 { 1730 // FunctionBinary (FunctionBinary.java.jpp) 1731 proto_invs.addAll(FunctionBinary.get_proto_all()); 1732 proto_invs.addAll(FunctionBinaryFloat.get_proto_all()); 1733 1734 // LinearTernary (LinearTernary.java.jpp) 1735 proto_invs.add(LinearTernary.get_proto()); 1736 proto_invs.add(LinearTernaryFloat.get_proto()); 1737 } 1738 1739 // User-defined invariants 1740 for (String invariantClassName : userDefinedInvariants) { 1741 Class<?> invClass; 1742 try { 1743 invClass = Class.forName(invariantClassName); 1744 } catch (ClassNotFoundException e) { 1745 throw new Daikon.UserError( 1746 "Cannot load class " 1747 + invariantClassName 1748 + " in " 1749 + user_defined_invariant_SWITCH 1750 + " command-line argument; is it on the classpath?"); 1751 } 1752 Method get_proto_method; 1753 try { 1754 get_proto_method = invClass.getMethod("get_proto"); 1755 } catch (NoSuchMethodException e) { 1756 throw new Daikon.UserError( 1757 "No get_proto() method in user-defined invariant class " + invariantClassName); 1758 } catch (SecurityException e) { 1759 throw new Daikon.UserError( 1760 e, 1761 "SecurityException while looking up get_proto() method in user-defined invariant class " 1762 + invariantClassName); 1763 } 1764 Invariant inv; 1765 try { 1766 @SuppressWarnings("nullness") // null argument is OK because get_proto_method is static 1767 Object inv_as_object = get_proto_method.invoke(null); 1768 if (inv_as_object == null) { 1769 throw new Daikon.UserError( 1770 invariantClassName 1771 + ".get_proto() returned null but should have returned an Invariant"); 1772 } 1773 if (!(inv_as_object instanceof Invariant)) { 1774 Class<?> cls = inv_as_object.getClass(); 1775 throw new Daikon.UserError( 1776 invariantClassName 1777 + ".get_proto() returned object of the wrong type." 1778 + " It should have been a subclass of invariant, but was " 1779 + cls 1780 + ": " 1781 + inv_as_object); 1782 } 1783 inv = (Invariant) inv_as_object; 1784 } catch (Exception e) { 1785 throw new Daikon.UserError( 1786 e, "Exception while invoking " + invariantClassName + ".get_proto()"); 1787 } 1788 proto_invs.add(inv); 1789 } 1790 1791 // Remove any elements that are not enabled 1792 for (Iterator<@Prototype Invariant> i = proto_invs.iterator(); i.hasNext(); ) { 1793 @Prototype Invariant inv = i.next(); 1794 assert inv != null; 1795 if (!inv.enabled()) { 1796 i.remove(); 1797 } 1798 } 1799 } 1800 1801 /** 1802 * Creates invariants for upper program points by merging together the invariants from all of the 1803 * lower points. 1804 */ 1805 public static void createUpperPpts(PptMap all_ppts) { 1806 1807 // Process each ppt that doesn't have a parent 1808 // (mergeInvs is called on a root, and recursively processes children) 1809 for (PptTopLevel ppt : all_ppts.pptIterable()) { 1810 // System.out.printf("considering ppt %s parents: %s, children: %s%n", 1811 // ppt.name, ppt.parents, ppt.children); 1812 if (ppt.parents.size() == 0) { 1813 ppt.mergeInvs(); 1814 } 1815 } 1816 } 1817 1818 /** Setup splitters. Add orig and derived variables. Recursively call init_ppt on splits. */ 1819 public static void init_ppt(PptTopLevel ppt, PptMap all_ppts) { 1820 1821 if (!Daikon.using_DaikonSimple) { 1822 // Create orig variables and set up splitters. 1823 // This must be done before adding derived variables. 1824 // Do not add splitters to ppts that were already created by splitters! 1825 // Also, ppts created by splitters already have their orig_vars. 1826 if (!(ppt instanceof PptConditional)) { 1827 progress = "Creating orig variables and splitters for: " + ppt.name; 1828 create_orig_vars(ppt, all_ppts); 1829 setup_splitters(ppt); 1830 } 1831 } 1832 1833 // Create derived variables 1834 if (!Derivation.dkconfig_disable_derived_variables) { 1835 progress = "Creating derived variables for: " + ppt.name; 1836 ppt.create_derived_variables(); 1837 } 1838 1839 if (!Daikon.using_DaikonSimple) { 1840 // Initialize equality sets on leaf nodes 1841 setupEquality(ppt); 1842 // System.out.printf("initialized equality %s for ppt %s%n", 1843 // ppt.equality_view, ppt.name()); 1844 1845 // Recursively initialize ppts created by splitters 1846 if (ppt.has_splitters()) { 1847 for (PptConditional ppt_cond : ppt.cond_iterable()) { 1848 init_ppt(ppt_cond, all_ppts); 1849 } 1850 } 1851 } 1852 1853 if (VarInfo.assertionsEnabled()) { 1854 for (VarInfo vi : ppt.var_infos) { 1855 vi.checkRep(); 1856 } 1857 } 1858 } 1859 1860 /** Create EXIT program points as needed for EXITnn program points. */ 1861 public static void create_combined_exits(PptMap ppts) { 1862 1863 // We can't add the newly created exit Ppts directly to ppts while we 1864 // are iterating over it, so store them temporarily in this map. 1865 PptMap exit_ppts = new PptMap(); 1866 1867 for (PptTopLevel ppt : ppts.pptIterable()) { 1868 // skip unless it's an EXITnn 1869 if (!ppt.is_subexit()) { 1870 continue; 1871 } 1872 1873 PptTopLevel exitnn_ppt = ppt; 1874 PptName exit_name = ppt.ppt_name.makeExit(); 1875 PptTopLevel exit_ppt = exit_ppts.get(exit_name); 1876 1877 if (debugInit.isLoggable(FINE)) { 1878 debugInit.fine("create_combined_exits: encountered exit " + exitnn_ppt.name()); 1879 } 1880 1881 // Create the exit, if necessary 1882 if (exit_ppt == null) { 1883 // This is a hack. It should probably filter out orig and derived 1884 // vars instead of taking the first n. 1885 int len = ppt.num_tracevars + ppt.num_static_constant_vars; 1886 VarInfo[] exit_vars = new VarInfo[len]; 1887 // System.out.printf("new decl fmt = %b%n", FileIO.new_decl_format); 1888 for (int j = 0; j < len; j++) { 1889 @SuppressWarnings("interning") // about to be used in new program point 1890 @Interned VarInfo exit_var = new VarInfo(ppt.var_infos[j]); 1891 exit_vars[j] = exit_var; 1892 // System.out.printf("exitNN name '%s', exit name '%s'%n", 1893 // ppt.var_infos[j].name(), exit_vars[j].name()); 1894 exit_vars[j].varinfo_index = ppt.var_infos[j].varinfo_index; 1895 exit_vars[j].value_index = ppt.var_infos[j].value_index; 1896 // Don't inherit the entry variable's equalitySet. 1897 @SuppressWarnings("nullness") // reinitialization 1898 @NonNull Equality es = null; 1899 exit_vars[j].equalitySet = es; 1900 } 1901 1902 exit_ppt = 1903 new PptTopLevel( 1904 exit_name.getName(), 1905 PptTopLevel.PptType.EXIT, 1906 ppt.parent_relations, 1907 ppt.flags, 1908 exit_vars); 1909 1910 // exit_ppt.ppt_name.setVisibility(exitnn_name.getVisibility()); 1911 exit_ppts.add(exit_ppt); 1912 if (debugInit.isLoggable(FINE)) { 1913 debugInit.fine("create_combined_exits: created exit " + exit_name); 1914 } 1915 init_ppt(exit_ppt, ppts); 1916 } 1917 } 1918 1919 // Now add the newly created Ppts to the global map. 1920 for (PptTopLevel ppt : exit_ppts.pptIterable()) { 1921 ppts.add(ppt); 1922 } 1923 } 1924 1925 // The function filters out the reflexive invs in binary slices, 1926 // reflexive and partially reflexive invs in ternary slices 1927 // and also filters out the invariants that have not seen enough 1928 // samples in ternary slices. 1929 static List<Invariant> filter_invs(List<Invariant> invs) { 1930 List<Invariant> new_list = new ArrayList<>(); 1931 1932 for (Invariant inv : invs) { 1933 VarInfo[] vars = inv.ppt.var_infos; 1934 1935 // This check is the most non-intrusive way to filter out the invs 1936 // Filter out reflexive invariants in the binary invs 1937 if (!((inv.ppt instanceof PptSlice2) && vars[0] == vars[1])) { 1938 1939 // Filter out the reflexive and partially reflexive invs in the 1940 // ternary slices 1941 if (!((inv.ppt instanceof PptSlice3) 1942 && (vars[0] == vars[1] || vars[1] == vars[2] || vars[0] == vars[2]))) { 1943 if (inv.ppt.num_values() != 0) { 1944 1945 // filters out "warning: too few samples for 1946 // daikon.inv.ternary.threeScalar.LinearTernary invariant" 1947 if (inv.isActive()) { 1948 new_list.add(inv); 1949 } 1950 } 1951 } 1952 } 1953 } 1954 1955 return new_list; 1956 } 1957 1958 /** 1959 * Add orig() variables to the given EXIT/EXITnn point. Does nothing if exit_ppt is not an 1960 * EXIT/EXITnn. 1961 */ 1962 private static void create_orig_vars(PptTopLevel exit_ppt, PptMap ppts) { 1963 if (!exit_ppt.ppt_name.isExitPoint()) { 1964 if (VarInfo.assertionsEnabled()) { 1965 for (VarInfo vi : exit_ppt.var_infos) { 1966 try { 1967 vi.checkRep(); 1968 } catch (Throwable e) { 1969 System.err.println(); 1970 System.err.println("Error with variable " + vi + " at ppt " + exit_ppt); 1971 throw e; 1972 } 1973 } 1974 } 1975 return; 1976 } 1977 1978 if (debugInit.isLoggable(FINE)) { 1979 debugInit.fine("Doing create and relate orig vars for: " + exit_ppt.name()); 1980 } 1981 1982 PptTopLevel entry_ppt = ppts.get(exit_ppt.ppt_name.makeEnter()); 1983 if (entry_ppt == null) { 1984 throw new Daikon.UserError("exit found with no corresponding entry: " + exit_ppt.name()); 1985 } 1986 1987 // Add "orig(...)" (prestate) variables to the program point. 1988 // Don't bother to include the constants. Walk through 1989 // entry_ppt's vars. For each non-constant, put it on the 1990 // new_vis worklist after fixing its comparability information. 1991 exit_ppt.num_orig_vars = entry_ppt.num_tracevars; 1992 VarInfo[] new_vis = new VarInfo[exit_ppt.num_orig_vars]; 1993 { 1994 VarInfo[] entry_ppt_vis = entry_ppt.var_infos; 1995 int new_vis_index = 0; 1996 for (int k = 0; k < entry_ppt.num_declvars; k++) { 1997 VarInfo vi = entry_ppt_vis[k]; 1998 assert !vi.isDerived() : "Derived when making orig(): " + vi.name(); 1999 if (vi.isStaticConstant()) { 2000 continue; 2001 } 2002 VarInfo origvar = VarInfo.origVarInfo(vi); 2003 // Fix comparability 2004 VarInfo postvar = exit_ppt.find_var_by_name(vi.name()); 2005 if (postvar == null) { 2006 System.out.printf( 2007 "Looking for postvar, can't find var %s in exit of ppt %s%n", vi, exit_ppt.name()); 2008 for (VarInfo cvi : entry_ppt.var_infos) { 2009 System.out.printf(" entry var = %s%n", cvi); 2010 } 2011 for (VarInfo cvi : exit_ppt.var_infos) { 2012 System.out.printf(" exit var = %s%n", cvi); 2013 } 2014 throw new RuntimeException("this can't happen: postvar is null"); 2015 } 2016 origvar.postState = postvar; 2017 origvar.comparability = postvar.comparability.makeAlias(); 2018 2019 // add parents for override relations 2020 // exit_ppt.parents has not been loaded at this point 2021 for (VarParent pi : postvar.parents) { 2022 PptTopLevel parentppt = ppts.get(pi.parent_ppt); 2023 if (parentppt != null) { 2024 if (!parentppt.is_object() && !parentppt.is_class()) { 2025 VarInfo pvi = 2026 parentppt.find_var_by_name( 2027 pi.parent_variable == null ? postvar.name() : pi.parent_variable); 2028 if (pvi != null) { 2029 origvar.parents.add( 2030 new VarParent(pi.parent_ppt, pi.parent_relation_id, pvi.prestate_name())); 2031 } 2032 } 2033 } 2034 } 2035 2036 // Add to new_vis 2037 new_vis[new_vis_index] = origvar; 2038 new_vis_index++; 2039 // System.out.printf("adding origvar %s to ppt %s%n", origvar.name(), 2040 // exit_ppt.name()); 2041 } 2042 assert new_vis_index == exit_ppt.num_orig_vars; 2043 } 2044 exit_ppt.addVarInfos(new_vis); 2045 2046 if (VarInfo.assertionsEnabled()) { 2047 for (VarInfo vi : exit_ppt.var_infos) { 2048 try { 2049 vi.checkRep(); 2050 } catch (Throwable e) { 2051 System.err.println(); 2052 System.err.println("Error with variable " + vi + " at ppt " + exit_ppt); 2053 throw e; 2054 } 2055 } 2056 } 2057 } 2058 2059 /////////////////////////////////////////////////////////////////////////// 2060 // Read decls, dtrace, etc. files 2061 2062 /** 2063 * Load a set of decl files. 2064 * 2065 * @param decl_files the files to load 2066 * @return the PptMap for the loaded files 2067 */ 2068 @RequiresNonNull("fileio_progress") 2069 // set in mainHelper 2070 private static PptMap load_decls_files(Set<File> decl_files) { 2071 long startTime = System.nanoTime(); 2072 try { 2073 if (!Daikon.dkconfig_quiet) { 2074 System.out.print("Reading declaration files "); 2075 } 2076 PptMap all_ppts = FileIO.read_declaration_files(decl_files); 2077 if (debugTrace.isLoggable(FINE)) { 2078 debugTrace.fine("Initializing partial order"); 2079 } 2080 fileio_progress.clear(); 2081 if (!Daikon.dkconfig_quiet && decl_files.size() > 0) { 2082 System.out.print("\r(read "); 2083 System.out.print(StringsPlume.nplural(decl_files.size(), "decls file")); 2084 System.out.println(")"); 2085 } 2086 return all_ppts; 2087 } catch (IOException e) { 2088 // System.out.println(); 2089 // e.printStackTrace(); 2090 throw new Daikon.UserError(e, "Error parsing decl file"); 2091 } finally { 2092 long duration = System.nanoTime() - startTime; 2093 debugProgress.fine( 2094 "Time spent on read_declaration_files: " + TimeUnit.NANOSECONDS.toSeconds(duration)); 2095 } 2096 } 2097 2098 private static void load_spinfo_files(Set<File> spinfo_files) { 2099 if (PptSplitter.dkconfig_disable_splitting || spinfo_files.isEmpty()) { 2100 return; 2101 } 2102 long startTime = System.nanoTime(); 2103 try { 2104 System.out.print("Reading splitter info files "); 2105 create_splitters(spinfo_files); 2106 System.out.print("\r(read "); 2107 System.out.print(StringsPlume.nplural(spinfo_files.size(), "spinfo file")); 2108 System.out.print(", "); 2109 System.out.print( 2110 StringsPlume.nplural(SpinfoFile.numSplittterObjects(spinfoFiles), "splitter")); 2111 System.out.println(")"); 2112 } catch (IOException e) { 2113 System.out.println(); 2114 e.printStackTrace(); 2115 throw new Error(e); 2116 } finally { 2117 long duration = System.nanoTime() - startTime; 2118 debugProgress.fine( 2119 "Time spent on load_spinfo_files: " + TimeUnit.NANOSECONDS.toSeconds(duration)); 2120 } 2121 } 2122 2123 /** 2124 * A wrapper around {@link ContextSplitterFactory#load_mapfiles_into_splitterlist}. 2125 * 2126 * @param map_files the map files to read into SplitterList 2127 */ 2128 private static void load_map_files(Set<File> map_files) { 2129 long startTime = System.nanoTime(); 2130 if (!PptSplitter.dkconfig_disable_splitting && map_files.size() > 0) { 2131 System.out.print("Reading map (context) files "); 2132 ContextSplitterFactory.load_mapfiles_into_splitterlist( 2133 map_files, ContextSplitterFactory.dkconfig_granularity); 2134 System.out.print("\r(read "); 2135 System.out.print(StringsPlume.nplural(map_files.size(), "map (context) file")); 2136 System.out.println(")"); 2137 long duration = System.nanoTime() - startTime; 2138 debugProgress.fine( 2139 "Time spent on load_map_files: " + TimeUnit.NANOSECONDS.toSeconds(duration)); 2140 } 2141 } 2142 2143 /** 2144 * Sets up splitting on all ppts. Currently only binary splitters over boolean returns or exactly 2145 * two return statements are enabled by default (though other splitters can be defined by the 2146 * user). 2147 * 2148 * @param ppt the program point to add conditions to 2149 */ 2150 @SuppressWarnings("nullness:contracts.precondition") 2151 public static void setup_splitters(PptTopLevel ppt) { 2152 if (PptSplitter.dkconfig_disable_splitting) { 2153 return; 2154 } 2155 2156 Global.debugSplit.fine("<<enter>> setup_splitters"); 2157 2158 SplitterFactory.load_splitters(ppt, spinfoFiles); 2159 2160 Splitter[] pconds; 2161 if (SplitterList.dkconfig_all_splitters) { 2162 pconds = SplitterList.get_all(); 2163 } else { 2164 pconds = SplitterList.get(ppt.name()); 2165 } 2166 if (pconds != null) { 2167 Global.debugSplit.fine( 2168 "Got " + StringsPlume.nplural(pconds.length, "splitter") + " for " + ppt.name()); 2169 ppt.addConditions(pconds); 2170 } 2171 2172 Global.debugSplit.fine("<<exit>> setup_splitters"); 2173 } 2174 2175 /////////////////////////////////////////////////////////////////////////// 2176 // Infer invariants over the trace data 2177 2178 /** 2179 * The number of columns of progress information to display. In many Unix shells, this can be set 2180 * to an appropriate value by {@code --config_option 2181 * daikon.Daikon.progress_display_width=$COLUMNS}. 2182 */ 2183 public static int dkconfig_progress_display_width = 80; 2184 2185 /** 2186 * Human-friendly progress status message. If {@code fileio_progress} is non-null, then this is 2187 * ignored. So this is primarily for progress reports that are not IO-related. 2188 */ 2189 public static String progress = ""; 2190 2191 // Is set unconditionally in mainHelper 2192 /** Takes precedence over the progress variable. */ 2193 private static @MonotonicNonNull FileIOProgress fileio_progress = null; 2194 2195 /** Outputs FileIO progress information. Uses global variable FileIO.data_trace_state. */ 2196 public static class FileIOProgress extends Thread { 2197 public FileIOProgress() { 2198 setDaemon(true); 2199 } 2200 2201 /** 2202 * Clients should set this variable instead of calling Thread.stop(), which is deprecated. 2203 * Typically a client calls "display()" before setting this. The stopping happens later, and 2204 * calls clear() anyway. 2205 */ 2206 public boolean shouldStop = false; 2207 2208 @Override 2209 public void run() { 2210 if (dkconfig_progress_delay == -1) { 2211 return; 2212 } 2213 while (true) { 2214 if (shouldStop) { 2215 clear(); 2216 return; 2217 } 2218 display(); 2219 try { 2220 sleep(dkconfig_progress_delay); 2221 } catch (InterruptedException e) { 2222 // hmm 2223 } 2224 } 2225 } 2226 2227 /** Clear the display; good to do before printing to System.out. */ 2228 public void clear() { 2229 if (dkconfig_progress_delay == -1) { 2230 return; 2231 } 2232 // "display("");" is wrong becuase it leaves the timestamp and writes 2233 // spaces across the screen. 2234 String status = StringsPlume.rpad("", dkconfig_progress_display_width - 1); 2235 System.out.print("\r" + status); 2236 System.out.print("\r"); // return to beginning of line 2237 System.out.flush(); 2238 } 2239 2240 /** 2241 * Displays the current status. Call this if you don't want to wait until the next automatic 2242 * display. 2243 */ 2244 public void display() { 2245 if (dkconfig_progress_delay == -1) { 2246 return; 2247 } 2248 2249 String message; 2250 if (FileIO.data_trace_state != null) { 2251 message = FileIO.data_trace_state.reading_message(); 2252 } else { 2253 if (Daikon.progress == null) { 2254 message = "[no status]"; 2255 } else { 2256 message = Daikon.progress; 2257 } 2258 } 2259 display(message); 2260 } 2261 2262 /** 2263 * Displays the given message. 2264 * 2265 * @param message message to be displayed 2266 */ 2267 public void display(String message) { 2268 if (dkconfig_progress_delay == -1) { 2269 return; 2270 } 2271 String status = 2272 StringsPlume.rpad( 2273 "[" + LocalDateTime.now(ZoneId.systemDefault()) + "]: " + message, 2274 dkconfig_progress_display_width - 1); 2275 System.out.print("\r" + status); 2276 System.out.flush(); 2277 // System.out.println (status); // for debugging 2278 2279 if (debugTrace.isLoggable(FINE)) { 2280 debugTrace.fine("Free memory: " + java.lang.Runtime.getRuntime().freeMemory()); 2281 debugTrace.fine( 2282 "Used memory: " 2283 + (java.lang.Runtime.getRuntime().totalMemory() 2284 - java.lang.Runtime.getRuntime().freeMemory())); 2285 try { 2286 if (FileIO.data_trace_state != null) { 2287 debugTrace.fine("Active slices: " + FileIO.data_trace_state.all_ppts.countSlices()); 2288 } 2289 } catch (ConcurrentModificationException e) { 2290 // Because this code is a separate thread, the number of ppts 2291 // could change during countSlices. Just ignore and continue. 2292 } 2293 } 2294 } 2295 } 2296 2297 /** 2298 * The data-processing routine of the daikon engine. At this point, the decls and spinfo files 2299 * have been loaded, all of the program points have been setup, and candidate invariants have been 2300 * instantiated. This routine processes data to falsify the candidate invariants. 2301 */ 2302 @RequiresNonNull("fileio_progress") 2303 // set in mainHelper 2304 private static void process_data(PptMap all_ppts, Set<String> dtrace_files) { 2305 MemMonitor monitor = null; 2306 if (use_mem_monitor) { 2307 monitor = new MemMonitor("stat.out"); 2308 new Thread((Runnable) monitor).start(); 2309 } 2310 2311 long startTime = System.nanoTime(); 2312 2313 // Preprocessing 2314 setup_NISuppression(); 2315 2316 // Processing (actually using dtrace files) 2317 try { 2318 fileio_progress.clear(); 2319 if (!Daikon.dkconfig_quiet) { 2320 System.out.println( 2321 "Processing trace data; reading " 2322 + StringsPlume.nplural(dtrace_files.size(), "dtrace file") 2323 + ":"); 2324 } 2325 FileIO.read_data_trace_files(dtrace_files, all_ppts); 2326 // Final update, so "100%", not "99.70%", is the last thing printed. 2327 // (This doesn't seem to achieve that, though...) 2328 fileio_progress.display(); 2329 fileio_progress.shouldStop = true; 2330 fileio_progress.display(); 2331 if (!Daikon.dkconfig_quiet) { 2332 System.out.println(); 2333 } 2334 // System.out.print("Creating implications "); // XXX untested code 2335 // for (PptTopLevel ppt : all_ppts) { 2336 // System.out.print('.'); 2337 // ppt.addImplications(); 2338 // } 2339 // System.out.println(); 2340 } catch (IOException e) { 2341 // System.out.println(); 2342 // e.printStackTrace(); 2343 throw new Error(e); 2344 } finally { 2345 long duration = System.nanoTime() - startTime; 2346 debugProgress.fine( 2347 "Time spent on read_data_trace_files: " + TimeUnit.NANOSECONDS.toSeconds(duration)); 2348 } 2349 2350 if (monitor != null) { 2351 monitor.stop(); 2352 } 2353 2354 if (FileIO.dkconfig_read_samples_only) { 2355 throw new Daikon.NormalTermination( 2356 String.format("Finished reading %d samples", FileIO.samples_processed)); 2357 } 2358 2359 if (all_ppts.size() == 0) { 2360 String message = "No program point declarations were found."; 2361 if (FileIO.omitted_declarations != 0) { 2362 message += 2363 lineSep 2364 + " " 2365 + FileIO.omitted_declarations 2366 + " " 2367 + ((FileIO.omitted_declarations == 1) ? "declaration was" : "declarations were") 2368 + " omitted by regexps (e.g., --ppt-select-pattern)."; 2369 } 2370 throw new Daikon.UserError(message); 2371 } 2372 2373 // System.out.println("samples processed: " + FileIO.samples_processed); 2374 2375 int unmatched_count = FileIO.call_stack.size() + FileIO.call_hashmap.size(); 2376 if ((use_dataflow_hierarchy && FileIO.samples_processed == unmatched_count) 2377 || (FileIO.samples_processed == 0)) { 2378 throw new Daikon.UserError( 2379 "No samples found for any of " + StringsPlume.nplural(all_ppts.size(), "program point")); 2380 } 2381 2382 // ppt_stats (all_ppts); 2383 2384 // if (debugStats.isLoggable (FINE)) { 2385 // PptSliceEquality.print_equality_stats (debugStats, all_ppts); 2386 // } 2387 2388 // Print equality set info 2389 // for (PptTopLevel ppt : all_ppts.pptIterable()) { 2390 // System.out.printf("ppt: %s", ppt.name); 2391 // if ((ppt.equality_view == null) || (ppt.equality_view.invs == null)) 2392 // continue; 2393 // for (Invariant inv : ppt.equality_view.invs) { 2394 // Equality e = (Equality) inv; 2395 // System.out.printf(" equality set = %s", e); 2396 // } 2397 // } 2398 2399 // System.out.printf("printing ternary invariants"); 2400 // PrintInvariants.print_all_ternary_invs (all_ppts); 2401 // System.exit(0); 2402 2403 // Postprocessing 2404 2405 debugProgress.fine("Create Combined Exits ... "); 2406 startTime = System.nanoTime(); 2407 create_combined_exits(all_ppts); 2408 long duration = System.nanoTime() - startTime; 2409 debugProgress.fine( 2410 "Create Combined Exits ... done [" + TimeUnit.NANOSECONDS.toSeconds(duration) + "]"); 2411 2412 // Post process dynamic constants 2413 if (DynamicConstants.dkconfig_use_dynamic_constant_optimization) { 2414 debugProgress.fine("Constant Post Processing ... "); 2415 startTime = System.nanoTime(); 2416 for (PptTopLevel ppt : all_ppts.ppt_all_iterable()) { 2417 if (ppt.constants != null) { 2418 ppt.constants.post_process(); 2419 } 2420 } 2421 duration = System.nanoTime() - startTime; 2422 debugProgress.fine( 2423 "Constant Post Processing ... done [" + TimeUnit.NANOSECONDS.toSeconds(duration) + "]"); 2424 } 2425 2426 // Initialize the partial order hierarchy 2427 debugProgress.fine("Init Hierarchy ... "); 2428 startTime = System.nanoTime(); 2429 assert FileIO.new_decl_format != null 2430 : "@AssumeAssertion(nullness): read data, so new_decl_format is set"; 2431 if (FileIO.new_decl_format) { 2432 PptRelation.init_hierarchy_new(all_ppts); 2433 } else { 2434 PptRelation.init_hierarchy(all_ppts); 2435 } 2436 duration = System.nanoTime() - startTime; 2437 debugProgress.fine( 2438 "Init Hierarchy ... done [" + TimeUnit.NANOSECONDS.toSeconds(duration) + "]"); 2439 2440 // Calculate invariants at all non-leaf ppts 2441 if (use_dataflow_hierarchy) { 2442 debugProgress.fine("createUpperPpts ... "); 2443 startTime = System.nanoTime(); 2444 // calculates invariants; does not actually create any ppts 2445 createUpperPpts(all_ppts); 2446 duration = System.nanoTime() - startTime; 2447 debugProgress.fine( 2448 "createUpperPpts ... done [" + TimeUnit.NANOSECONDS.toSeconds(duration) + "]"); 2449 } 2450 2451 // Equality data for each PptTopLevel. 2452 if (Daikon.use_equality_optimization && !Daikon.dkconfig_undo_opts) { 2453 debugProgress.fine("Equality Post Process ... "); 2454 startTime = System.nanoTime(); 2455 for (PptTopLevel ppt : all_ppts.ppt_all_iterable()) { 2456 // ppt.equality_view can be null here 2457 ppt.postProcessEquality(); 2458 } 2459 duration = System.nanoTime() - startTime; 2460 debugProgress.fine( 2461 "Equality Post Process ... done [" + TimeUnit.NANOSECONDS.toSeconds(duration) + "]"); 2462 } 2463 2464 // undo optimizations; results in a more redundant but more complete 2465 // set of invariants 2466 if (Daikon.dkconfig_undo_opts) { 2467 undoOpts(all_ppts); 2468 } 2469 2470 // Debug print information about equality sets 2471 if (debugEquality.isLoggable(FINE)) { 2472 for (PptTopLevel ppt : all_ppts.ppt_all_iterable()) { 2473 debugEquality.fine(ppt.name() + ": " + ppt.equality_sets_txt()); 2474 } 2475 } 2476 2477 debugProgress.fine("Non-implication postprocessing ... done"); 2478 2479 isInferencing = false; 2480 2481 // Add implications 2482 startTime = System.nanoTime(); 2483 fileio_progress.clear(); 2484 if (!PptSplitter.dkconfig_disable_splitting) { 2485 debugProgress.fine("Adding Implications ... "); 2486 for (PptTopLevel ppt : all_ppts.pptIterable()) { 2487 // debugProgress.fine (" Adding implications for " + ppt.name); 2488 ppt.addImplications(); 2489 } 2490 duration = System.nanoTime() - startTime; 2491 debugProgress.fine( 2492 "Adding Implications ... done [" + TimeUnit.NANOSECONDS.toSeconds(duration) + "]"); 2493 } 2494 } 2495 2496 private static class Count { 2497 public int val; 2498 2499 Count(int val) { 2500 this.val = val; 2501 } 2502 } 2503 2504 /** Print out basic statistics (samples, invariants, variables, etc) about each ppt. */ 2505 public static void ppt_stats(PptMap all_ppts) { 2506 2507 int all_ppt_cnt = 0; 2508 int ppt_w_sample_cnt = 0; 2509 for (PptTopLevel ppt : all_ppts.pptIterable()) { 2510 all_ppt_cnt++; 2511 if (ppt.num_samples() == 0) { 2512 continue; 2513 } 2514 ppt_w_sample_cnt++; 2515 System.out.printf("%s%n", ppt.name()); 2516 System.out.printf(" samples = %n%d", ppt.num_samples()); 2517 System.out.printf(" invariants = %n%d", ppt.invariant_cnt()); 2518 Map<ProglangType, Count> type_map = new LinkedHashMap<>(); 2519 int leader_cnt = 0; 2520 for (VarInfo v : ppt.var_infos) { 2521 if (!v.isCanonical()) { 2522 continue; 2523 } 2524 leader_cnt++; 2525 Count cnt = type_map.computeIfAbsent(v.file_rep_type, __ -> new Count(0)); 2526 cnt.val++; 2527 } 2528 System.out.println(" vars = " + ppt.var_infos.length); 2529 System.out.println(" leaders = " + leader_cnt); 2530 for (Map.Entry<@KeyFor("type_map") ProglangType, Count> e : type_map.entrySet()) { 2531 ProglangType file_rep_type = e.getKey(); 2532 Count cnt = e.getValue(); 2533 System.out.printf(" %s = %d%n", file_rep_type, cnt.val); 2534 } 2535 } 2536 System.out.println("Total ppt count = " + all_ppt_cnt); 2537 System.out.println("PPts w/sample count = " + ppt_w_sample_cnt); 2538 } 2539 2540 /** Process the invariants with simplify to remove redundant invariants. */ 2541 private static void suppressWithSimplify(PptMap all_ppts) { 2542 System.out.print("Invoking Simplify to identify redundant invariants"); 2543 System.out.flush(); 2544 long startTime = System.nanoTime(); 2545 for (PptTopLevel ppt : all_ppts.ppt_all_iterable()) { 2546 ppt.mark_implied_via_simplify(all_ppts); 2547 System.out.print("."); 2548 System.out.flush(); 2549 } 2550 long duration = System.nanoTime() - startTime; 2551 System.out.println(TimeUnit.NANOSECONDS.toSeconds(duration)); 2552 2553 // Make sure the Simplify process and helper threads are finished 2554 LemmaStack proverStack = PptTopLevel.getProverStack(); 2555 if (proverStack != null) { 2556 proverStack.close(); 2557 } 2558 } 2559 2560 /** Initialize NIS suppression. */ 2561 @EnsuresNonNull({ 2562 "daikon.suppress.NIS.suppressor_map", 2563 "daikon.suppress.NIS.suppressor_map_suppression_count", 2564 "daikon.suppress.NIS.all_suppressions", 2565 "daikon.suppress.NIS.suppressor_proto_invs" 2566 }) 2567 public static void setup_NISuppression() { 2568 NIS.init_ni_suppression(); 2569 } 2570 2571 /** Initialize the equality sets for each variable. */ 2572 public static void setupEquality(PptTopLevel ppt) { 2573 2574 if (!Daikon.use_equality_optimization) { 2575 return; 2576 } 2577 2578 // Skip points that are not leaves. 2579 if (use_dataflow_hierarchy) { 2580 PptTopLevel p = ppt; 2581 if (ppt instanceof PptConditional) { 2582 p = ((PptConditional) ppt).parent; 2583 } 2584 2585 // Rather than defining leaves as :::GLOBAL or :::EXIT54 (numbered 2586 // exit), we define them as everything except 2587 // ::EXIT (combined), :::ENTER, :::THROWS, :::OBJECT 2588 // and :::CLASS program points. This scheme ensures that arbitrarly 2589 // named program points such as :::POINT (used by convertcsv.pl) 2590 // will be treated as leaves. 2591 if (p.ppt_name.isCombinedExitPoint() 2592 || p.ppt_name.isEnterPoint() 2593 || p.ppt_name.isThrowsPoint() 2594 || p.ppt_name.isObjectInstanceSynthetic() 2595 || p.ppt_name.isClassStaticSynthetic()) { 2596 return; 2597 } 2598 2599 if (ppt.has_splitters()) { 2600 return; 2601 } 2602 } 2603 2604 // Create the initial equality sets 2605 ppt.equality_view = new PptSliceEquality(ppt); 2606 ppt.equality_view.instantiate_invariants(); 2607 } 2608 2609 private static List<SpinfoFile> spinfoFiles = new ArrayList<>(); 2610 2611 /** 2612 * Create user-defined splitters. For each file in the input, add a SpinfoFile to the spinfoFiles 2613 * variable. 2614 */ 2615 public static void create_splitters(Set<File> spinfo_files) throws IOException { 2616 for (File filename : spinfo_files) { 2617 SpinfoFile sf = SplitterFactory.parse_spinfofile(filename); 2618 spinfoFiles.add(sf); 2619 } 2620 } 2621 2622 // /** 2623 // * Guard the invariants at all PptTopLevels. Note that this changes 2624 // * the contents of the PptTopLevels, and the changes made should 2625 // * probably not be written out to an inv file (save the file before 2626 // * this is called). 2627 // */ 2628 // public static void guardInvariants(PptMap allPpts) { 2629 // for (PptTopLevel ppt : allPpts.asCollection()) { 2630 // if (ppt.num_samples() == 0) 2631 // continue; 2632 // // Make sure isDerivedParam is set before guarding. Otherwise 2633 // // we'll never get it correct. 2634 // for (int iVarInfo = 0; 2635 // iVarInfo < ppt.var_infos.length; 2636 // iVarInfo++) { 2637 // boolean temp = 2638 // ppt.var_infos[iVarInfo].isDerivedParamAndUninteresting(); 2639 // } 2640 // 2641 // ppt.guardInvariants(); 2642 // } 2643 // } 2644 2645 /** Removed invariants as specified in omit_types. */ 2646 private static void processOmissions(PptMap allPpts) { 2647 if (omit_types['0']) { 2648 allPpts.removeUnsampled(); 2649 } 2650 for (PptTopLevel ppt : allPpts.asCollection()) { 2651 ppt.processOmissions(omit_types); 2652 } 2653 } 2654 2655 /** 2656 * Returns the ppt name, max_ppt, that corresponds to the specified percentage of ppts (presuming 2657 * that only those ppts ≤ max_ppt will be processed). 2658 */ 2659 private static @Nullable String setup_ppt_perc(Collection<File> decl_files, int ppt_perc) { 2660 2661 // Make sure the percentage is valid 2662 if ((ppt_perc < 1) || (ppt_perc > 100)) { 2663 // The number should already have been checked, so don't use UserError. 2664 throw new BugInDaikon("ppt_perc of " + ppt_perc + " is out of range 1..100"); 2665 } 2666 if (ppt_perc == 100) { 2667 return null; 2668 } 2669 2670 // Keep track of all of the ppts in a set ordered by the ppt name 2671 Set<String> ppts = new TreeSet<>(); 2672 2673 // Read all of the ppt names out of the decl files 2674 try { 2675 for (File file : decl_files) { 2676 2677 // Open the file 2678 try (LineNumberReader fp = FilesPlume.newLineNumberFileReader(file)) { 2679 2680 // Read each ppt name from the file 2681 for (String line = fp.readLine(); line != null; line = fp.readLine()) { 2682 if (line.equals("") || FileIO.isComment(line)) { 2683 continue; 2684 } 2685 if (!line.equals("DECLARE")) { 2686 continue; 2687 } 2688 // Just read "DECLARE", so next line has ppt name. 2689 String ppt_name = fp.readLine(); 2690 if (ppt_name == null) { 2691 throw new Daikon.UserError("File " + file + " terminated prematurely"); 2692 } 2693 ppts.add(ppt_name); 2694 } 2695 } 2696 } 2697 } catch (IOException e) { 2698 e.printStackTrace(); 2699 throw new Error(e); 2700 } 2701 2702 // Determine the ppt_name that matches the specified percentage. Always 2703 // return the last exit point from the method (so we don't get half the 2704 // exits from a method or enters without exits, etc) 2705 int ppt_cnt = (ppts.size() * ppt_perc) / 100; 2706 if (ppt_cnt == 0) { 2707 throw new Daikon.UserError( 2708 "ppt_perc of " + ppt_perc + "% results in processing 0 out of " + ppts.size() + " ppts"); 2709 } 2710 for (Iterator<String> i = ppts.iterator(); i.hasNext(); ) { 2711 String ppt_name = i.next(); 2712 if (--ppt_cnt <= 0) { 2713 String last_ppt_name = ppt_name; 2714 while (i.hasNext()) { 2715 ppt_name = i.next(); 2716 if ((last_ppt_name.indexOf("EXIT") != -1) && (ppt_name.indexOf("EXIT") == -1)) { 2717 return last_ppt_name; 2718 } 2719 last_ppt_name = ppt_name; 2720 } 2721 return ppt_name; 2722 } 2723 } 2724 // Execution should not reach this line 2725 throw new Error("ppt_cnt " + ppt_cnt + " ppts.size " + ppts.size()); 2726 } 2727 2728 /** 2729 * Undoes the invariants suppressed for the dynamic constant, suppression and equality set 2730 * optimizations (should yield the same invariants as the simple incremental algorithm. 2731 */ 2732 @RequiresNonNull({"daikon.suppress.NIS.all_suppressions", "daikon.suppress.NIS.suppressor_map"}) 2733 public static void undoOpts(PptMap all_ppts) { 2734 2735 // undo suppressions 2736 for (PptTopLevel ppt : all_ppts.ppt_all_iterable()) { 2737 NIS.create_suppressed_invs(ppt); 2738 } 2739 2740 // undo equality sets 2741 for (PptTopLevel ppt : all_ppts.ppt_all_iterable()) { 2742 PptSliceEquality sliceEquality = ppt.equality_view; 2743 2744 // some program points have no equality sets? 2745 if (sliceEquality == null) { 2746 // System.out.println(ppt.name); 2747 continue; 2748 } 2749 2750 // get the new leaders 2751 List<Equality> allNewInvs = new ArrayList<>(); 2752 2753 for (Invariant eq_as_inv : sliceEquality.invs) { 2754 Equality eq = (Equality) eq_as_inv; 2755 VarInfo leader = eq.leader(); 2756 List<VarInfo> vars = new ArrayList<>(); 2757 2758 for (VarInfo var : eq.getVars()) { 2759 if (!var.equals(leader)) { 2760 vars.add(var); 2761 } 2762 } 2763 2764 if (vars.size() > 0) { 2765 2766 // Create new equality sets for all of the non-equal vars 2767 List<Equality> newInvs = sliceEquality.createEqualityInvs(vars, eq); 2768 2769 // Create new slices and invariants for each new leader 2770 // copyInvsFromLeader(sliceEquality, leader, vars); 2771 sliceEquality.copyInvsFromLeader(leader, vars); 2772 2773 // Keep track of all of the new invariants created. 2774 // Add all of the new equality sets to our list 2775 allNewInvs.addAll(newInvs); 2776 } 2777 } 2778 2779 sliceEquality.invs.addAll(allNewInvs); 2780 } 2781 } 2782}