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.18"; 227 228 /** The date for the current version of Daikon. */ 229 public static final String release_date = "June 23, 2023"; 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) System.out.println(release_string); 762 } 763 764 // figure out which algorithm to use in NIS to process suppressions 765 if (NIS.dkconfig_suppression_processor == SuppressionProcessor.HYBRID) { 766 NIS.hybrid_method = true; 767 } else { 768 if (NIS.dkconfig_suppression_processor == SuppressionProcessor.ANTECEDENT) { 769 NIS.antecedent_method = true; 770 NIS.hybrid_method = false; 771 } else { 772 assert (NIS.dkconfig_suppression_processor == SuppressionProcessor.FALSIFIED); 773 NIS.antecedent_method = false; 774 NIS.hybrid_method = false; 775 } 776 } 777 778 // Create the list of all invariant types 779 setup_proto_invs(); 780 781 if (PrintInvariants.print_discarded_invariants) { 782 DiscReasonMap.initialize(); 783 } 784 785 fileio_progress = new FileIOProgress(); 786 fileio_progress.start(); 787 788 // Load declarations and splitters 789 load_spinfo_files(spinfo_files); 790 all_ppts = load_decls_files(decls_files); 791 load_map_files(map_files); 792 793 all_ppts.trimToSize(); 794 795 // Only for assertion checks 796 isInferencing = true; 797 798 // Infer invariants 799 process_data(all_ppts, dtrace_files); 800 isInferencing = false; 801 if (Debug.logOn()) { 802 Debug.check(all_ppts, "After process data"); 803 } 804 805 // If requested, just calculate the total number of invariants possible 806 if (dkconfig_calc_possible_invs) { 807 fileio_progress.shouldStop = true; 808 int total_invs = 0; 809 // Can't use new for syntax because the default iterator for all_ppts 810 // is not the one I want here. 811 for (PptTopLevel ppt : all_ppts.ppt_all_iterable()) { 812 System.out.printf("Processing %s with %d variables", ppt.name(), ppt.var_infos.length); 813 int inv_cnt = 0; 814 if (ppt.var_infos.length > 1600) { 815 System.out.println("Skipping, too many variables!"); 816 } else { 817 inv_cnt = ppt.getInvariants().size(); 818 System.out.println(" " + inv_cnt + " invariants"); 819 total_invs += inv_cnt; 820 } 821 } 822 System.out.println(total_invs + " invariants total"); 823 return; 824 } 825 826 if (suppress_redundant_invariants_with_simplify) { 827 suppressWithSimplify(all_ppts); 828 } 829 830 // Check that PptMap created was correct 831 all_ppts.repCheck(); 832 833 // Remove undesired invariants, if requested 834 if (omit_from_output) { 835 processOmissions(all_ppts); 836 } 837 838 debugProgress.fine(" Writing Serialized Pptmap ... "); 839 long startWriteTime = System.nanoTime(); 840 // Write serialized output - must be done before guarding invariants 841 if (inv_file != null) { 842 try { 843 FileIO.write_serialized_pptmap(all_ppts, inv_file); 844 } catch (IOException e) { 845 throw new RuntimeException("Error while writing .inv file: " + inv_file, e); 846 } 847 } 848 duration = System.nanoTime() - startWriteTime; 849 debugProgress.fine( 850 " Writing Serialized Pptmap ... done [" + TimeUnit.NANOSECONDS.toSeconds(duration) + "]"); 851 852 // if ((Daikon.dkconfig_guardNulls == "always") // interned 853 // || (Daikon.dkconfig_guardNulls == "missing")) { // interned 854 // // This side-effects the PptMap, but it has already been saved 855 // // to disk and is now being used only for printing. 856 // guardInvariants(all_ppts); 857 // } 858 859 // Debug print information about the variables 860 if (false) { 861 for (PptTopLevel ppt : all_ppts.all_ppts()) { 862 System.out.printf("Dumping variables for ppt %s%n", ppt.name()); 863 for (VarInfo vi : ppt.var_infos) { 864 System.out.printf(" vi %s%n", vi); 865 System.out.printf(" file_rep_type = %s%n", vi.file_rep_type); 866 System.out.printf(" type = %s%n", vi.type); 867 } 868 } 869 } 870 871 // print out the invariants for each program point 872 if (Daikon.dkconfig_undo_opts) { 873 // Print out the invariants for each program point (sort first) 874 for (PptTopLevel ppt : all_ppts.pptIterable()) { 875 876 // We do not need to print out program points that have not seen 877 // any samples. 878 if (ppt.num_samples() == 0) { 879 continue; 880 } 881 List<Invariant> invs = PrintInvariants.sort_invariant_list(ppt.invariants_vector()); 882 List<Invariant> filtered_invs = filter_invs(invs); 883 884 // Debugging output. Sometimes the program points actually differ in number of samples seen 885 // due to differences in how Daikon and DaikonSimple see the variable hierarchy. 886 if (false) { 887 System.out.println("===================================================="); 888 System.out.println(ppt.name()); 889 System.out.println(ppt.num_samples()); 890 891 for (Invariant inv : filtered_invs) { 892 System.out.println(inv.getClass()); 893 System.out.println(inv); 894 } 895 } 896 } 897 898 // exit the program 899 if (false) { 900 return; 901 } 902 } 903 904 // Display invariants 905 if (output_num_samples) { 906 System.out.println("The --output_num_samples debugging flag is on."); 907 System.out.println("Some of the debugging output may only make sense to Daikon programmers."); 908 } 909 910 // If they want to see discarded invariants, they probably don't 911 // want to see the true ones. 912 if (!PrintInvariants.print_discarded_invariants) { 913 PrintInvariants.print_invariants(all_ppts); 914 } else { 915 PrintInvariants.print_reasons(all_ppts); 916 } 917 918 if (output_num_samples) { 919 Global.output_statistics(); 920 } 921 if (dkconfig_print_sample_totals) { 922 System.out.println(FileIO.samples_processed + " samples processed"); 923 } 924 925 // print statistics concerning what invariants are printed 926 if (debugStats.isLoggable(FINE)) { 927 for (PptTopLevel ppt : all_ppts.ppt_all_iterable()) { 928 PrintInvariants.print_filter_stats(debugStats, ppt, all_ppts); 929 } 930 } 931 932 duration = System.nanoTime() - startTime; 933 debugProgress.fine(" Total time spent in Daikon: " + TimeUnit.NANOSECONDS.toSeconds(duration)); 934 935 // Done 936 if (!Daikon.dkconfig_quiet) { 937 System.out.println("Exiting Daikon."); 938 } 939 } 940 941 /** Cleans up static variables so that mainHelper can be called more than once. */ 942 @SuppressWarnings("nullness") // reinitialization 943 public static void cleanup() { 944 945 // Stop the thread that prints out progress information 946 if ((fileio_progress != null) && (fileio_progress.getState() != Thread.State.NEW)) { 947 fileio_progress.shouldStop = true; 948 try { 949 fileio_progress.join(2000); 950 } catch (InterruptedException e) { 951 // It's OK for a wait operation to be interrupted. 952 } 953 if (fileio_progress.getState() != Thread.State.TERMINATED) { 954 throw new BugInDaikon("Can't stop fileio_progress thead"); 955 } 956 } 957 fileio_progress = null; 958 progress = ""; 959 960 // Reset statics. Unfortunately, these must match the settings where 961 // these are declared and I don't know how to do that automatically. 962 inv_file = null; 963 no_text_output = false; 964 show_progress = false; 965 output_format = OutputFormat.DAIKON; 966 noversion_output = false; 967 output_num_samples = false; 968 omit_from_output = false; 969 omit_types = new boolean[256]; 970 use_dataflow_hierarchy = true; 971 suppress_redundant_invariants_with_simplify = false; 972 ppt_regexp = null; 973 ppt_omit_regexp = null; 974 var_regexp = null; 975 var_omit_regexp = null; 976 server_dir = null; 977 use_mem_monitor = false; 978 979 proto_invs.clear(); 980 } 981 982 // Structure for return value of read_options. 983 // Return an array of {decls, dtrace, spinfo, map} files. 984 public static class FileOptions { 985 public Set<File> decls; 986 public Set<String> dtrace; 987 public Set<File> spinfo; 988 public Set<File> map; 989 990 public FileOptions(Set<File> decls, Set<String> dtrace, Set<File> spinfo, Set<File> map) { 991 this.decls = decls; 992 this.dtrace = dtrace; 993 this.spinfo = spinfo; 994 this.map = map; 995 } 996 } 997 998 /////////////////////////////////////////////////////////////////////////// 999 // Read in the command line options 1000 // Return {decls, dtrace, spinfo, map} files. 1001 static FileOptions read_options(String[] args, String usage) { 1002 if (args.length == 0) { 1003 System.out.println("Error: no files supplied on command line."); 1004 System.out.println(usage); 1005 throw new Daikon.UserError(); 1006 } 1007 1008 // LinkedHashSet because it can be confusing to users if files (of the 1009 // same type) are gratuitously processed in a different order than they 1010 // were supplied on the command line. 1011 HashSet<File> decl_files = new LinkedHashSet<>(); 1012 HashSet<String> dtrace_files = new LinkedHashSet<>(); // file names or "-" or "+" 1013 HashSet<File> spinfo_files = new LinkedHashSet<>(); 1014 HashSet<File> map_files = new LinkedHashSet<>(); 1015 1016 LongOpt[] longopts = 1017 new LongOpt[] { 1018 // Control output 1019 new LongOpt(help_SWITCH, LongOpt.NO_ARGUMENT, null, 0), 1020 new LongOpt(no_text_output_SWITCH, LongOpt.NO_ARGUMENT, null, 0), 1021 new LongOpt(format_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0), 1022 new LongOpt(show_progress_SWITCH, LongOpt.NO_ARGUMENT, null, 0), 1023 new LongOpt(show_detail_progress_SWITCH, LongOpt.NO_ARGUMENT, null, 0), 1024 new LongOpt(no_show_progress_SWITCH, LongOpt.NO_ARGUMENT, null, 0), 1025 new LongOpt(noversion_SWITCH, LongOpt.NO_ARGUMENT, null, 0), 1026 new LongOpt(output_num_samples_SWITCH, LongOpt.NO_ARGUMENT, null, 0), 1027 new LongOpt(files_from_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0), 1028 new LongOpt(omit_from_output_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0), 1029 // Control invariant detection 1030 new LongOpt(conf_limit_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0), 1031 new LongOpt(list_type_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0), 1032 new LongOpt(user_defined_invariant_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0), 1033 new LongOpt(disable_all_invariants_SWITCH, LongOpt.NO_ARGUMENT, null, 0), 1034 new LongOpt(no_dataflow_hierarchy_SWITCH, LongOpt.NO_ARGUMENT, null, 0), 1035 new LongOpt(suppress_redundant_SWITCH, LongOpt.NO_ARGUMENT, null, 0), 1036 // Process only part of the trace file 1037 new LongOpt(ppt_regexp_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0), 1038 new LongOpt(ppt_omit_regexp_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0), 1039 new LongOpt(var_regexp_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0), 1040 new LongOpt(var_omit_regexp_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0), 1041 // Configuration options 1042 new LongOpt(server_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0), 1043 new LongOpt(config_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0), 1044 new LongOpt(config_option_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0), 1045 // Debugging 1046 new LongOpt(debugAll_SWITCH, LongOpt.NO_ARGUMENT, null, 0), 1047 new LongOpt(debug_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0), 1048 new LongOpt(track_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0), 1049 new LongOpt(disc_reason_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0), 1050 new LongOpt(mem_stat_SWITCH, LongOpt.NO_ARGUMENT, null, 0), 1051 }; 1052 Getopt g = new Getopt("daikon.Daikon", args, "ho:", longopts); 1053 int c; 1054 1055 while ((c = g.getopt()) != -1) { 1056 switch (c) { 1057 case 0: 1058 // got a long option 1059 String option_name = longopts[g.getLongind()].getName(); 1060 1061 // Control output 1062 if (help_SWITCH.equals(option_name)) { 1063 System.out.println(usage); 1064 throw new Daikon.NormalTermination(); 1065 } else if (no_text_output_SWITCH.equals(option_name)) { 1066 no_text_output = true; 1067 } else if (format_SWITCH.equals(option_name)) { 1068 String format_name = getOptarg(g); 1069 Daikon.output_format = OutputFormat.get(format_name); 1070 if (Daikon.output_format == null) { 1071 throw new Daikon.UserError("Unknown output format: --format " + format_name); 1072 } 1073 } else if (show_progress_SWITCH.equals(option_name)) { 1074 show_progress = true; 1075 LogHelper.setLevel("daikon.Progress", FINE); 1076 } else if (show_detail_progress_SWITCH.equals(option_name)) { 1077 show_progress = true; 1078 LogHelper.setLevel("daikon.Progress", FINER); 1079 } else if (no_show_progress_SWITCH.equals(option_name)) { 1080 show_progress = false; 1081 } else if (noversion_SWITCH.equals(option_name)) { 1082 noversion_output = true; 1083 } else if (output_num_samples_SWITCH.equals(option_name)) { 1084 output_num_samples = true; 1085 } else if (files_from_SWITCH.equals(option_name)) { 1086 String files_from_filename = getOptarg(g); 1087 try (EntryReader entryReader = new EntryReader(files_from_filename)) { 1088 for (String filename : entryReader) { 1089 // Ignore blank lines in file. 1090 if (filename.equals("")) { 1091 continue; 1092 } 1093 // This code is duplicated below outside the options loop. 1094 // These aren't "endsWith()" because there might be a suffix 1095 // on the end (eg, a date, or ".gz"). 1096 File file = new File(filename); 1097 if (!file.exists()) { 1098 throw new Daikon.UserError("File " + filename + " not found."); 1099 } 1100 if (filename.indexOf(".decls") != -1) { 1101 decl_files.add(file); 1102 } else if (filename.indexOf(".dtrace") != -1) { 1103 dtrace_files.add(filename); 1104 } else if (filename.indexOf(".spinfo") != -1) { 1105 spinfo_files.add(file); 1106 } else if (filename.indexOf(".map") != -1) { 1107 map_files.add(file); 1108 } else { 1109 throw new Daikon.UserError("Unrecognized file extension: " + filename); 1110 } 1111 } 1112 } catch (IOException e) { 1113 throw new RuntimeException( 1114 String.format("Error reading --files_from file: %s", files_from_filename)); 1115 } 1116 break; 1117 } else if (omit_from_output_SWITCH.equals(option_name)) { 1118 String f = getOptarg(g); 1119 for (int i = 0; i < f.length(); i++) { 1120 if ("0rs".indexOf(f.charAt(i)) == -1) { 1121 throw new Daikon.UserError( 1122 "omit_from_output flag letter '" + f.charAt(i) + "' is unknown"); 1123 } 1124 omit_types[f.charAt(i)] = true; 1125 } 1126 omit_from_output = true; 1127 } 1128 // Control invariant detection 1129 else if (conf_limit_SWITCH.equals(option_name)) { 1130 double limit = Double.parseDouble(getOptarg(g)); 1131 if ((limit < 0.0) || (limit > 1.0)) { 1132 throw new Daikon.UserError(conf_limit_SWITCH + " must be between [0..1]"); 1133 } 1134 Configuration.getInstance() 1135 .apply("daikon.inv.Invariant.confidence_limit", String.valueOf(limit)); 1136 } else if (list_type_SWITCH.equals(option_name)) { 1137 try { 1138 String list_type_string = getOptarg(g); 1139 ProglangType.list_implementors.add(list_type_string); 1140 } catch (Exception e) { 1141 throw new Daikon.UserError("Problem parsing " + list_type_SWITCH + " option: " + e); 1142 } 1143 break; 1144 } else if (user_defined_invariant_SWITCH.equals(option_name)) { 1145 try { 1146 String user_defined_invariant_string = getOptarg(g); 1147 Matcher m = classGetNamePattern.matcher(user_defined_invariant_string); 1148 if (!m.matches()) { 1149 throw new Daikon.UserError( 1150 "Bad argument " 1151 + user_defined_invariant_string 1152 + " for " 1153 + ppt_regexp_SWITCH 1154 + ": not in the format required by Class.getName(String)"); 1155 } 1156 @SuppressWarnings("signature") // Regex match guarantees the format of Class.getName() 1157 @ClassGetName String cname = user_defined_invariant_string; 1158 userDefinedInvariants.add(cname); 1159 } catch (Exception e) { 1160 throw new Daikon.UserError( 1161 "Problem parsing " + user_defined_invariant_SWITCH + " option: " + e); 1162 } 1163 break; 1164 } else if (disable_all_invariants_SWITCH.equals(option_name)) { 1165 // There are two possibilities: 1166 // * a given invariant class is not yet loaded, in which case 1167 // we set the default value for its dkconfig_enabled field. 1168 // * a given invariant class is already loaded, in which case 1169 // we reflectively set its dkconfig_enabled to false. 1170 1171 // Set the default for not-yet-loaded invariants. 1172 Invariant.invariantEnabledDefault = false; 1173 1174 // Get all loaded classes. This solution is from 1175 // http://stackoverflow.com/a/10261850/173852 . Alternate approach: 1176 // http://stackoverflow.com/questions/2548384/java-get-a-list-of-all-classes-loaded-in-the-jvm 1177 Field f; 1178 try { 1179 f = ClassLoader.class.getDeclaredField("classes"); 1180 } catch (NoSuchFieldException e) { 1181 throw new Daikon.BugInDaikon("Didn't find field ClassLoader.classes"); 1182 } 1183 f.setAccessible(true); 1184 Object classesAsObject; 1185 { 1186 ClassLoader cl = Thread.currentThread().getContextClassLoader(); 1187 if (cl == null) { 1188 throw new Daikon.BugInDaikon( 1189 "Need to handle when getContextClassLoader returns null"); 1190 } 1191 try { 1192 classesAsObject = f.get(cl); 1193 } catch (IllegalAccessException e) { 1194 throw new Daikon.BugInDaikon("Field ClassLoader.classes was not made accessible"); 1195 } 1196 } 1197 @SuppressWarnings({ 1198 "unchecked", // type of ClassLoader.classes field is known 1199 "nullness" // ClassLoader.classes is non-null 1200 }) 1201 @NonNull List<Class<?>> classes = (List<Class<?>>) classesAsObject; 1202 for (int i = 0; i < classes.size(); i++) { 1203 Class<?> loadedClass = classes.get(i); 1204 if (Invariant.class.isAssignableFrom(loadedClass)) { 1205 @SuppressWarnings("unchecked") // loadedClass is a subclass of Invariant 1206 Class<? extends Invariant> invType = (Class<? extends Invariant>) loadedClass; 1207 try { 1208 Field field = invType.getField("dkconfig_enabled"); 1209 if (field.getType() != Boolean.TYPE) { 1210 throw new Daikon.BugInDaikon( 1211 "Field " 1212 + invType 1213 + ".dkconfig_enabled has type " 1214 + field.getType() 1215 + " instead of boolean"); 1216 } else { 1217 setStaticField(field, false); 1218 // System.out.println( 1219 // "Set field " 1220 // + invType 1221 // + ".dkconfig_enabled to false"); 1222 } 1223 } catch (NoSuchFieldException e) { 1224 // System.out.println( 1225 // "Class " + invType + " does not have a dkconfig_enabled field"); 1226 } catch (IllegalAccessException e) { 1227 throw new Daikon.BugInDaikon( 1228 "IllegalAccessException for field " + invType + ".dkconfig_enabled"); 1229 } 1230 } 1231 } 1232 } else if (no_dataflow_hierarchy_SWITCH.equals(option_name)) { 1233 use_dataflow_hierarchy = false; 1234 } else if (suppress_redundant_SWITCH.equals(option_name)) { 1235 suppress_redundant_invariants_with_simplify = true; 1236 } 1237 1238 // Process only part of the trace file 1239 else if (ppt_regexp_SWITCH.equals(option_name)) { 1240 if (ppt_regexp != null) { 1241 throw new Daikon.UserError( 1242 "multiple --" 1243 + ppt_regexp_SWITCH 1244 + " regular expressions supplied on command line"); 1245 } 1246 String regexp_string = getOptarg(g); 1247 if (!RegexUtil.isRegex(regexp_string)) { 1248 throw new Daikon.UserError( 1249 "Bad regexp " 1250 + regexp_string 1251 + " for " 1252 + ppt_regexp_SWITCH 1253 + ": " 1254 + RegexUtil.regexError(regexp_string)); 1255 } 1256 ppt_regexp = Pattern.compile(regexp_string); 1257 break; 1258 } else if (ppt_omit_regexp_SWITCH.equals(option_name)) { 1259 if (ppt_omit_regexp != null) { 1260 throw new Daikon.UserError( 1261 "multiple --" 1262 + ppt_omit_regexp_SWITCH 1263 + " regular expressions supplied on command line"); 1264 } 1265 String regexp_string = getOptarg(g); 1266 if (!RegexUtil.isRegex(regexp_string)) { 1267 throw new Daikon.UserError( 1268 "Bad regexp " 1269 + regexp_string 1270 + " for " 1271 + ppt_omit_regexp_SWITCH 1272 + ": " 1273 + RegexUtil.regexError(regexp_string)); 1274 } 1275 ppt_omit_regexp = Pattern.compile(regexp_string); 1276 break; 1277 } else if (var_regexp_SWITCH.equals(option_name)) { 1278 if (var_regexp != null) { 1279 throw new Daikon.UserError( 1280 "multiple --" 1281 + var_regexp_SWITCH 1282 + " regular expressions supplied on command line"); 1283 } 1284 String regexp_string = getOptarg(g); 1285 if (!RegexUtil.isRegex(regexp_string)) { 1286 throw new Daikon.UserError( 1287 "Bad regexp " 1288 + regexp_string 1289 + " for " 1290 + var_regexp_SWITCH 1291 + ": " 1292 + RegexUtil.regexError(regexp_string)); 1293 } 1294 var_regexp = Pattern.compile(regexp_string); 1295 break; 1296 } else if (var_omit_regexp_SWITCH.equals(option_name)) { 1297 if (var_omit_regexp != null) { 1298 throw new Daikon.UserError( 1299 "multiple --" 1300 + var_omit_regexp_SWITCH 1301 + " regular expressions supplied on command line"); 1302 } 1303 String regexp_string = getOptarg(g); 1304 if (!RegexUtil.isRegex(regexp_string)) { 1305 throw new Daikon.UserError( 1306 "Bad regexp " 1307 + regexp_string 1308 + " for " 1309 + var_omit_regexp_SWITCH 1310 + ": " 1311 + RegexUtil.regexError(regexp_string)); 1312 } 1313 var_omit_regexp = Pattern.compile(regexp_string); 1314 break; 1315 } else if (server_SWITCH.equals(option_name)) { 1316 String input_dir = getOptarg(g); 1317 server_dir = new File(input_dir); 1318 if (!server_dir.isDirectory() || !server_dir.canRead() || !server_dir.canWrite()) { 1319 throw new RuntimeException( 1320 "Could not open config file in server directory " + server_dir); 1321 } 1322 break; 1323 1324 // Configuration options 1325 1326 } else if (config_SWITCH.equals(option_name)) { 1327 String config_file = getOptarg(g); 1328 try (InputStream stream = new FileInputStream(config_file)) { 1329 Configuration.getInstance().apply(stream); 1330 } catch (IOException e) { 1331 throw new Daikon.UserError( 1332 // Is this the only possible reason for an IOException? 1333 "Could not open config file " + config_file); 1334 } 1335 break; 1336 } else if (config_option_SWITCH.equals(option_name)) { 1337 String item = getOptarg(g); 1338 try { 1339 Configuration.getInstance().apply(item); 1340 } catch (daikon.config.Configuration.ConfigException e) { 1341 throw new Daikon.UserError(e); 1342 } 1343 break; 1344 } else if (debugAll_SWITCH.equals(option_name)) { 1345 Global.debugAll = true; 1346 } else if (debug_SWITCH.equals(option_name)) { 1347 LogHelper.setLevel(getOptarg(g), FINE); 1348 } else if (track_SWITCH.equals(option_name)) { 1349 LogHelper.setLevel("daikon.Debug", FINE); 1350 String error = Debug.add_track(getOptarg(g)); 1351 if (error != null) { 1352 throw new Daikon.UserError( 1353 "Error parsing track argument '" + getOptarg(g) + "' - " + error); 1354 } 1355 } else if (disc_reason_SWITCH.equals(option_name)) { 1356 try { 1357 PrintInvariants.discReasonSetup(getOptarg(g)); 1358 } catch (IllegalArgumentException e) { 1359 throw new Daikon.UserError(e); 1360 } 1361 } else if (mem_stat_SWITCH.equals(option_name)) { 1362 use_mem_monitor = true; 1363 } else { 1364 throw new Daikon.UserError("Unknown option " + option_name + " on command line"); 1365 } 1366 break; 1367 case 'h': 1368 System.out.println(usage); 1369 throw new Daikon.NormalTermination(); 1370 case 'o': 1371 String inv_filename = getOptarg(g); 1372 1373 if (inv_file != null) { 1374 throw new Daikon.UserError( 1375 "multiple serialization output files supplied on command line: " 1376 + inv_file 1377 + " " 1378 + inv_filename); 1379 } 1380 1381 inv_file = new File(inv_filename); 1382 1383 if (!FilesPlume.canCreateAndWrite(inv_file)) { 1384 throw new Daikon.UserError("Cannot write to serialization output file " + inv_file); 1385 } 1386 break; 1387 // 1388 case '?': 1389 // break; // getopt() already printed an error 1390 System.out.println(usage); 1391 throw new Daikon.NormalTermination(); 1392 // 1393 default: 1394 throw new Daikon.BugInDaikon("getopt() returned " + c); 1395 } 1396 } 1397 1398 // This code is duplicated above within the switch processing. 1399 // First check that all the file names are OK, so we don't do lots of 1400 // processing only to bail out at the end. 1401 for (int i = g.getOptind(); i < args.length; i++) { 1402 String filename = args[i]; 1403 if (filename.equals("-") || filename.equals("+")) { 1404 dtrace_files.add(filename); 1405 continue; 1406 } 1407 1408 File file = new File(filename); 1409 if (!file.exists()) { 1410 throw new Daikon.UserError("File " + file + " not found."); 1411 } 1412 filename = file.toString(); 1413 1414 // These aren't "endsWith()" because there might be a suffix on the end 1415 // (eg, a date or ".gz"). 1416 if (filename.indexOf(".decls") != -1) { 1417 decl_files.add(file); 1418 } else if (filename.indexOf(".dtrace") != -1) { 1419 dtrace_files.add(filename); 1420 // Always output an invariant file by default, even if none is 1421 // specified on the command line. 1422 if (inv_file == null) { 1423 String basename; 1424 // This puts the .inv file in the current directory. 1425 basename = new File(filename).getName(); 1426 // This puts the .inv file in the same directory as the .dtrace file. 1427 // basename = filename; 1428 int base_end = basename.indexOf(".dtrace"); 1429 String inv_filename = basename.substring(0, base_end) + ".inv.gz"; 1430 1431 inv_file = new File(inv_filename); 1432 if (!FilesPlume.canCreateAndWrite(inv_file)) { 1433 throw new Daikon.UserError("Cannot write to file " + inv_file); 1434 } 1435 } 1436 } else if (filename.indexOf(".spinfo") != -1) { 1437 spinfo_files.add(file); 1438 } else if (filename.indexOf(".map") != -1) { 1439 map_files.add(file); 1440 } else { 1441 throw new Daikon.UserError("Unrecognized file type: " + file); 1442 } 1443 } 1444 1445 // Set the fuzzy float comparison ratio. This needs to be done after 1446 // any configuration options (which may set the ratio) are processed. 1447 Global.fuzzy.setRelativeRatio(Invariant.dkconfig_fuzzy_ratio); 1448 1449 // Setup ppt_max_name based on the specified percentage of ppts to process 1450 if (dkconfig_ppt_perc != 100) { 1451 ppt_max_name = setup_ppt_perc(decl_files, dkconfig_ppt_perc); 1452 System.out.println("Max ppt name = " + ppt_max_name); 1453 } 1454 1455 // Validate guardNulls option 1456 PrintInvariants.validateGuardNulls(); 1457 1458 return new FileOptions(decl_files, dtrace_files, spinfo_files, map_files); 1459 } 1460 1461 /** 1462 * Set a static field to the given value. 1463 * 1464 * @param field a field; must be static 1465 * @param value the value to set the field to 1466 * @throws IllegalAccessException if {@code field} is enforcing Java language access control and 1467 * the underlying field is either inaccessible or final. 1468 */ 1469 // This method exists to reduce the scope of the warning suppression. 1470 @SuppressWarnings({ 1471 "nullness:argument", // field is static, so object may be null 1472 "interning:argument" // interning is not necessary for how this method is used 1473 }) 1474 private static void setStaticField(Field field, Object value) throws IllegalAccessException { 1475 field.set(null, value); 1476 } 1477 1478 /** 1479 * Just like {@code g.getOptarg()}, but only to be called in circumstances when the programmer 1480 * knows that the return value is non-null. 1481 * 1482 * @param g a command-line argument processor 1483 * @return the value for an argument found by {@code g} 1484 */ 1485 @Pure 1486 public static String getOptarg(Getopt g) { 1487 String result = g.getOptarg(); 1488 if (result == null) { 1489 throw new Error("getOptarg returned null for " + g); 1490 } 1491 return result; 1492 } 1493 1494 /** 1495 * Invariants passed on the command line with the {@code --user_defined_invariant} option. A list 1496 * of class names in the format required by {@link Class#forName(String)}. 1497 */ 1498 private static List<@ClassGetName String> userDefinedInvariants = 1499 new ArrayList<@ClassGetName String>(); 1500 1501 /** 1502 * Creates the list of prototype invariants for all Daikon invariants. New invariants must be 1503 * added to this list. 1504 */ 1505 public static void setup_proto_invs() { 1506 1507 // Unary scalar invariants 1508 { 1509 // OneOf (OneOf.java.jpp) 1510 proto_invs.add(OneOfScalar.get_proto()); 1511 proto_invs.add(OneOfFloat.get_proto()); 1512 proto_invs.add(OneOfString.get_proto()); 1513 1514 // NonZero (NonZero.java.jpp) 1515 proto_invs.add(NonZero.get_proto()); 1516 proto_invs.add(NonZeroFloat.get_proto()); 1517 1518 proto_invs.add(IsPointer.get_proto()); 1519 1520 // Lower and Upper bound (Bound.java.jpp) 1521 proto_invs.add(LowerBound.get_proto()); 1522 proto_invs.add(LowerBoundFloat.get_proto()); 1523 proto_invs.add(UpperBound.get_proto()); 1524 proto_invs.add(UpperBoundFloat.get_proto()); 1525 1526 // Modulus and NonModulus (Modulus.java and NonModulus.java) 1527 proto_invs.add(Modulus.get_proto()); 1528 proto_invs.add(NonModulus.get_proto()); 1529 1530 // Range invariant (Range.java.jpp) 1531 proto_invs.addAll(RangeInt.get_proto_all()); 1532 proto_invs.addAll(RangeFloat.get_proto_all()); 1533 1534 // Printable String 1535 proto_invs.add(PrintableString.get_proto()); 1536 1537 // Complete One Of 1538 proto_invs.add(CompleteOneOfString.get_proto()); 1539 proto_invs.add(CompleteOneOfScalar.get_proto()); 1540 1541 // Positive (x > 0) (Postive.java). Positive is a sample invariant 1542 // that is only included as an example. 1543 // proto_invs.add (Postive.get_proto()); 1544 } 1545 1546 // Unary sequence invariants 1547 { 1548 // OneOf (OneOf.java.jpp) 1549 proto_invs.add(OneOfSequence.get_proto()); 1550 proto_invs.add(OneOfFloatSequence.get_proto()); 1551 proto_invs.add(OneOfStringSequence.get_proto()); 1552 proto_invs.add(EltOneOf.get_proto()); 1553 proto_invs.add(EltOneOfFloat.get_proto()); 1554 proto_invs.add(EltOneOfString.get_proto()); 1555 1556 // Range invariant (Range.java.jpp) 1557 proto_invs.addAll(EltRangeInt.get_proto_all()); 1558 proto_invs.addAll(EltRangeFloat.get_proto_all()); 1559 1560 // Sequence Index Comparisons (SeqIndexComparison.java.jpp) 1561 proto_invs.add(SeqIndexIntEqual.get_proto()); 1562 proto_invs.add(SeqIndexIntNonEqual.get_proto()); 1563 proto_invs.add(SeqIndexIntGreaterEqual.get_proto()); 1564 proto_invs.add(SeqIndexIntGreaterThan.get_proto()); 1565 proto_invs.add(SeqIndexIntLessEqual.get_proto()); 1566 proto_invs.add(SeqIndexIntLessThan.get_proto()); 1567 proto_invs.add(SeqIndexFloatEqual.get_proto()); 1568 proto_invs.add(SeqIndexFloatNonEqual.get_proto()); 1569 proto_invs.add(SeqIndexFloatGreaterEqual.get_proto()); 1570 proto_invs.add(SeqIndexFloatGreaterThan.get_proto()); 1571 proto_invs.add(SeqIndexFloatLessEqual.get_proto()); 1572 proto_invs.add(SeqIndexFloatLessThan.get_proto()); 1573 1574 // foreach i compare a[i] to a[i+1] (EltwiseIntComparisons.java.jpp) 1575 proto_invs.add(EltwiseIntEqual.get_proto()); 1576 proto_invs.add(EltwiseIntLessEqual.get_proto()); 1577 proto_invs.add(EltwiseIntGreaterEqual.get_proto()); 1578 proto_invs.add(EltwiseIntLessThan.get_proto()); 1579 proto_invs.add(EltwiseIntGreaterThan.get_proto()); 1580 proto_invs.add(EltwiseFloatEqual.get_proto()); 1581 proto_invs.add(EltwiseFloatLessEqual.get_proto()); 1582 proto_invs.add(EltwiseFloatGreaterEqual.get_proto()); 1583 proto_invs.add(EltwiseFloatLessThan.get_proto()); 1584 proto_invs.add(EltwiseFloatGreaterThan.get_proto()); 1585 1586 // EltNonZero (EltNonZero.java.jpp) 1587 proto_invs.add(EltNonZero.get_proto()); 1588 proto_invs.add(EltNonZeroFloat.get_proto()); 1589 1590 // No Duplicates (NoDuplicates.java.jpp) 1591 proto_invs.add(NoDuplicates.get_proto()); 1592 proto_invs.add(NoDuplicatesFloat.get_proto()); 1593 1594 // Element bounds (Bound.java.jpp) 1595 proto_invs.add(EltLowerBound.get_proto()); 1596 proto_invs.add(EltUpperBound.get_proto()); 1597 proto_invs.add(EltLowerBoundFloat.get_proto()); 1598 proto_invs.add(EltUpperBoundFloat.get_proto()); 1599 1600 // CommonSequence (CommonSequence.java.jpp) 1601 proto_invs.add(CommonSequence.get_proto()); 1602 proto_invs.add(CommonFloatSequence.get_proto()); 1603 1604 // CommonStringSequence (CommonStringSubsequence.java) 1605 proto_invs.add(CommonStringSequence.get_proto()); 1606 } 1607 1608 // Binary scalar-scalar invariants 1609 { 1610 // Int, Float, String comparisons (from IntComparisons.java.jpp) 1611 proto_invs.add(IntEqual.get_proto()); 1612 proto_invs.add(IntNonEqual.get_proto()); 1613 proto_invs.add(IntLessThan.get_proto()); 1614 proto_invs.add(IntGreaterThan.get_proto()); 1615 proto_invs.add(IntLessEqual.get_proto()); 1616 proto_invs.add(IntGreaterEqual.get_proto()); 1617 proto_invs.add(FloatEqual.get_proto()); 1618 proto_invs.add(FloatNonEqual.get_proto()); 1619 proto_invs.add(FloatLessThan.get_proto()); 1620 proto_invs.add(FloatGreaterThan.get_proto()); 1621 proto_invs.add(FloatLessEqual.get_proto()); 1622 proto_invs.add(FloatGreaterEqual.get_proto()); 1623 proto_invs.add(StringEqual.get_proto()); 1624 proto_invs.add(StringNonEqual.get_proto()); 1625 proto_invs.add(StringLessThan.get_proto()); 1626 proto_invs.add(StringGreaterThan.get_proto()); 1627 proto_invs.add(StringLessEqual.get_proto()); 1628 proto_invs.add(StringGreaterEqual.get_proto()); 1629 1630 // LinearBinary over integer/float (from LinearBinary.java.jpp) 1631 proto_invs.add(LinearBinary.get_proto()); 1632 proto_invs.add(LinearBinaryFloat.get_proto()); 1633 1634 // Numeric invariants (from Numeric.java.jpp) 1635 proto_invs.addAll(NumericInt.get_proto_all()); 1636 proto_invs.addAll(NumericFloat.get_proto_all()); 1637 1638 // Standard binary string invariants 1639 proto_invs.addAll(StdString.get_proto_all()); 1640 } 1641 1642 // Binary sequence-sequence invariants 1643 { 1644 // Numeric invariants (from Numeric.java.jpp) 1645 proto_invs.addAll(PairwiseNumericInt.get_proto_all()); 1646 proto_invs.addAll(PairwiseNumericFloat.get_proto_all()); 1647 1648 // Pairwise string invariants (also from Numeric.java.jpp) 1649 proto_invs.addAll(PairwiseString.get_proto_all()); 1650 1651 // Lexical sequence comparisons (from SeqComparison.java.jpp) 1652 proto_invs.add(SeqSeqIntEqual.get_proto()); 1653 proto_invs.add(SeqSeqIntLessThan.get_proto()); 1654 proto_invs.add(SeqSeqIntGreaterThan.get_proto()); 1655 proto_invs.add(SeqSeqIntLessEqual.get_proto()); 1656 proto_invs.add(SeqSeqIntGreaterEqual.get_proto()); 1657 proto_invs.add(SeqSeqFloatEqual.get_proto()); 1658 proto_invs.add(SeqSeqFloatLessThan.get_proto()); 1659 proto_invs.add(SeqSeqFloatGreaterThan.get_proto()); 1660 proto_invs.add(SeqSeqFloatLessEqual.get_proto()); 1661 proto_invs.add(SeqSeqFloatGreaterEqual.get_proto()); 1662 proto_invs.add(SeqSeqStringEqual.get_proto()); 1663 proto_invs.add(SeqSeqStringLessThan.get_proto()); 1664 proto_invs.add(SeqSeqStringGreaterThan.get_proto()); 1665 proto_invs.add(SeqSeqStringLessEqual.get_proto()); 1666 proto_invs.add(SeqSeqStringGreaterEqual.get_proto()); 1667 1668 // Pairwise sequence comparisons (from PairwiseIntComparison.java.jpp) 1669 proto_invs.add(PairwiseIntEqual.get_proto()); 1670 proto_invs.add(PairwiseIntLessThan.get_proto()); 1671 proto_invs.add(PairwiseIntGreaterThan.get_proto()); 1672 proto_invs.add(PairwiseIntLessEqual.get_proto()); 1673 proto_invs.add(PairwiseIntGreaterEqual.get_proto()); 1674 proto_invs.add(PairwiseFloatEqual.get_proto()); 1675 proto_invs.add(PairwiseFloatLessThan.get_proto()); 1676 proto_invs.add(PairwiseFloatGreaterThan.get_proto()); 1677 proto_invs.add(PairwiseFloatLessEqual.get_proto()); 1678 proto_invs.add(PairwiseFloatGreaterEqual.get_proto()); 1679 proto_invs.add(PairwiseStringEqual.get_proto()); 1680 proto_invs.add(PairwiseStringLessThan.get_proto()); 1681 proto_invs.add(PairwiseStringGreaterThan.get_proto()); 1682 proto_invs.add(PairwiseStringLessEqual.get_proto()); 1683 proto_invs.add(PairwiseStringGreaterEqual.get_proto()); 1684 1685 // Array Reverse (from Reverse.java.jpp) 1686 proto_invs.add(Reverse.get_proto()); 1687 proto_invs.add(ReverseFloat.get_proto()); 1688 1689 // Pairwise Linear Binary (from PairwiseLinearBinary.java.jpp) 1690 proto_invs.add(PairwiseLinearBinary.get_proto()); 1691 proto_invs.add(PairwiseLinearBinaryFloat.get_proto()); 1692 1693 // Subset and Superset (from SubSet.java.jpp) 1694 proto_invs.add(SubSet.get_proto()); 1695 proto_invs.add(SuperSet.get_proto()); 1696 proto_invs.add(SubSetFloat.get_proto()); 1697 proto_invs.add(SuperSetFloat.get_proto()); 1698 1699 // Subsequence (from SubSequence.java.jpp) 1700 proto_invs.add(SubSequence.get_proto()); 1701 proto_invs.add(SubSequenceFloat.get_proto()); 1702 proto_invs.add(SuperSequence.get_proto()); 1703 proto_invs.add(SuperSequenceFloat.get_proto()); 1704 } 1705 1706 // Binary sequence-scalar invariants 1707 { 1708 // Comparison of scalar to each array element (SeqIntComparison.java.jpp) 1709 proto_invs.add(SeqIntEqual.get_proto()); 1710 proto_invs.add(SeqIntLessThan.get_proto()); 1711 proto_invs.add(SeqIntGreaterThan.get_proto()); 1712 proto_invs.add(SeqIntLessEqual.get_proto()); 1713 proto_invs.add(SeqIntGreaterEqual.get_proto()); 1714 proto_invs.add(SeqFloatEqual.get_proto()); 1715 proto_invs.add(SeqFloatLessThan.get_proto()); 1716 proto_invs.add(SeqFloatGreaterThan.get_proto()); 1717 proto_invs.add(SeqFloatLessEqual.get_proto()); 1718 proto_invs.add(SeqFloatGreaterEqual.get_proto()); 1719 1720 // Scalar is an element of the array (Member.java.jpp) 1721 proto_invs.add(Member.get_proto()); 1722 proto_invs.add(MemberFloat.get_proto()); 1723 proto_invs.add(MemberString.get_proto()); 1724 } 1725 1726 // Ternary invariants 1727 { 1728 // FunctionBinary (FunctionBinary.java.jpp) 1729 proto_invs.addAll(FunctionBinary.get_proto_all()); 1730 proto_invs.addAll(FunctionBinaryFloat.get_proto_all()); 1731 1732 // LinearTernary (LinearTernary.java.jpp) 1733 proto_invs.add(LinearTernary.get_proto()); 1734 proto_invs.add(LinearTernaryFloat.get_proto()); 1735 } 1736 1737 // User-defined invariants 1738 for (String invariantClassName : userDefinedInvariants) { 1739 Class<?> invClass; 1740 try { 1741 invClass = Class.forName(invariantClassName); 1742 } catch (ClassNotFoundException e) { 1743 throw new Daikon.UserError( 1744 "Cannot load class " 1745 + invariantClassName 1746 + " in " 1747 + user_defined_invariant_SWITCH 1748 + " command-line argument; is it on the classpath?"); 1749 } 1750 Method get_proto_method; 1751 try { 1752 get_proto_method = invClass.getMethod("get_proto"); 1753 } catch (NoSuchMethodException e) { 1754 throw new Daikon.UserError( 1755 "No get_proto() method in user-defined invariant class " + invariantClassName); 1756 } catch (SecurityException e) { 1757 throw new Daikon.UserError( 1758 e, 1759 "SecurityException while looking up get_proto() method in user-defined invariant class " 1760 + invariantClassName); 1761 } 1762 Invariant inv; 1763 try { 1764 @SuppressWarnings("nullness") // null argument is OK because get_proto_method is static 1765 Object inv_as_object = get_proto_method.invoke(null); 1766 if (inv_as_object == null) { 1767 throw new Daikon.UserError( 1768 invariantClassName 1769 + ".get_proto() returned null but should have returned an Invariant"); 1770 } 1771 if (!(inv_as_object instanceof Invariant)) { 1772 Class<?> cls = inv_as_object.getClass(); 1773 throw new Daikon.UserError( 1774 invariantClassName 1775 + ".get_proto() returned object of the wrong type." 1776 + " It should have been a subclass of invariant, but was " 1777 + cls 1778 + ": " 1779 + inv_as_object); 1780 } 1781 inv = (Invariant) inv_as_object; 1782 } catch (Exception e) { 1783 throw new Daikon.UserError( 1784 e, "Exception while invoking " + invariantClassName + ".get_proto()"); 1785 } 1786 proto_invs.add(inv); 1787 } 1788 1789 // Remove any elements that are not enabled 1790 for (Iterator<@Prototype Invariant> i = proto_invs.iterator(); i.hasNext(); ) { 1791 @Prototype Invariant inv = i.next(); 1792 assert inv != null; 1793 if (!inv.enabled()) i.remove(); 1794 } 1795 } 1796 1797 /** 1798 * Creates invariants for upper program points by merging together the invariants from all of the 1799 * lower points. 1800 */ 1801 public static void createUpperPpts(PptMap all_ppts) { 1802 1803 // Process each ppt that doesn't have a parent 1804 // (mergeInvs is called on a root, and recursively processes children) 1805 for (PptTopLevel ppt : all_ppts.pptIterable()) { 1806 // System.out.printf("considering ppt %s parents: %s, children: %s%n", 1807 // ppt.name, ppt.parents, ppt.children); 1808 if (ppt.parents.size() == 0) { 1809 ppt.mergeInvs(); 1810 } 1811 } 1812 } 1813 1814 /** Setup splitters. Add orig and derived variables. Recursively call init_ppt on splits. */ 1815 public static void init_ppt(PptTopLevel ppt, PptMap all_ppts) { 1816 1817 if (!Daikon.using_DaikonSimple) { 1818 // Create orig variables and set up splitters. 1819 // This must be done before adding derived variables. 1820 // Do not add splitters to ppts that were already created by splitters! 1821 // Also, ppts created by splitters already have their orig_vars. 1822 if (!(ppt instanceof PptConditional)) { 1823 progress = "Creating orig variables and splitters for: " + ppt.name; 1824 create_orig_vars(ppt, all_ppts); 1825 setup_splitters(ppt); 1826 } 1827 } 1828 1829 // Create derived variables 1830 if (!Derivation.dkconfig_disable_derived_variables) { 1831 progress = "Creating derived variables for: " + ppt.name; 1832 ppt.create_derived_variables(); 1833 } 1834 1835 if (!Daikon.using_DaikonSimple) { 1836 // Initialize equality sets on leaf nodes 1837 setupEquality(ppt); 1838 // System.out.printf("initialized equality %s for ppt %s%n", 1839 // ppt.equality_view, ppt.name()); 1840 1841 // Recursively initialize ppts created by splitters 1842 if (ppt.has_splitters()) { 1843 for (PptConditional ppt_cond : ppt.cond_iterable()) { 1844 init_ppt(ppt_cond, all_ppts); 1845 } 1846 } 1847 } 1848 1849 if (VarInfo.assertionsEnabled()) { 1850 for (VarInfo vi : ppt.var_infos) { 1851 vi.checkRep(); 1852 } 1853 } 1854 } 1855 1856 /** Create EXIT program points as needed for EXITnn program points. */ 1857 public static void create_combined_exits(PptMap ppts) { 1858 1859 // We can't add the newly created exit Ppts directly to ppts while we 1860 // are iterating over it, so store them temporarily in this map. 1861 PptMap exit_ppts = new PptMap(); 1862 1863 for (PptTopLevel ppt : ppts.pptIterable()) { 1864 // skip unless it's an EXITnn 1865 if (!ppt.is_subexit()) { 1866 continue; 1867 } 1868 1869 PptTopLevel exitnn_ppt = ppt; 1870 PptName exit_name = ppt.ppt_name.makeExit(); 1871 PptTopLevel exit_ppt = exit_ppts.get(exit_name); 1872 1873 if (debugInit.isLoggable(FINE)) { 1874 debugInit.fine("create_combined_exits: encountered exit " + exitnn_ppt.name()); 1875 } 1876 1877 // Create the exit, if necessary 1878 if (exit_ppt == null) { 1879 // This is a hack. It should probably filter out orig and derived 1880 // vars instead of taking the first n. 1881 int len = ppt.num_tracevars + ppt.num_static_constant_vars; 1882 VarInfo[] exit_vars = new VarInfo[len]; 1883 // System.out.printf("new decl fmt = %b%n", FileIO.new_decl_format); 1884 for (int j = 0; j < len; j++) { 1885 @SuppressWarnings("interning") // about to be used in new program point 1886 @Interned VarInfo exit_var = new VarInfo(ppt.var_infos[j]); 1887 exit_vars[j] = exit_var; 1888 // System.out.printf("exitNN name '%s', exit name '%s'%n", 1889 // ppt.var_infos[j].name(), exit_vars[j].name()); 1890 exit_vars[j].varinfo_index = ppt.var_infos[j].varinfo_index; 1891 exit_vars[j].value_index = ppt.var_infos[j].value_index; 1892 // Don't inherit the entry variable's equalitySet. 1893 @SuppressWarnings("nullness") // reinitialization 1894 @NonNull Equality es = null; 1895 exit_vars[j].equalitySet = es; 1896 } 1897 1898 exit_ppt = 1899 new PptTopLevel( 1900 exit_name.getName(), 1901 PptTopLevel.PptType.EXIT, 1902 ppt.parent_relations, 1903 ppt.flags, 1904 exit_vars); 1905 1906 // exit_ppt.ppt_name.setVisibility(exitnn_name.getVisibility()); 1907 exit_ppts.add(exit_ppt); 1908 if (debugInit.isLoggable(FINE)) { 1909 debugInit.fine("create_combined_exits: created exit " + exit_name); 1910 } 1911 init_ppt(exit_ppt, ppts); 1912 } 1913 } 1914 1915 // Now add the newly created Ppts to the global map. 1916 for (PptTopLevel ppt : exit_ppts.pptIterable()) { 1917 ppts.add(ppt); 1918 } 1919 } 1920 1921 // The function filters out the reflexive invs in binary slices, 1922 // reflexive and partially reflexive invs in ternary slices 1923 // and also filters out the invariants that have not seen enough 1924 // samples in ternary slices. 1925 static List<Invariant> filter_invs(List<Invariant> invs) { 1926 List<Invariant> new_list = new ArrayList<>(); 1927 1928 for (Invariant inv : invs) { 1929 VarInfo[] vars = inv.ppt.var_infos; 1930 1931 // This check is the most non-intrusive way to filter out the invs 1932 // Filter out reflexive invariants in the binary invs 1933 if (!((inv.ppt instanceof PptSlice2) && vars[0] == vars[1])) { 1934 1935 // Filter out the reflexive and partially reflexive invs in the 1936 // ternary slices 1937 if (!((inv.ppt instanceof PptSlice3) 1938 && (vars[0] == vars[1] || vars[1] == vars[2] || vars[0] == vars[2]))) { 1939 if (inv.ppt.num_values() != 0) { 1940 1941 // filters out "warning: too few samples for 1942 // daikon.inv.ternary.threeScalar.LinearTernary invariant" 1943 if (inv.isActive()) { 1944 new_list.add(inv); 1945 } 1946 } 1947 } 1948 } 1949 } 1950 1951 return new_list; 1952 } 1953 1954 /** 1955 * Add orig() variables to the given EXIT/EXITnn point. Does nothing if exit_ppt is not an 1956 * EXIT/EXITnn. 1957 */ 1958 private static void create_orig_vars(PptTopLevel exit_ppt, PptMap ppts) { 1959 if (!exit_ppt.ppt_name.isExitPoint()) { 1960 if (VarInfo.assertionsEnabled()) { 1961 for (VarInfo vi : exit_ppt.var_infos) { 1962 try { 1963 vi.checkRep(); 1964 } catch (Throwable e) { 1965 System.err.println(); 1966 System.err.println("Error with variable " + vi + " at ppt " + exit_ppt); 1967 throw e; 1968 } 1969 } 1970 } 1971 return; 1972 } 1973 1974 if (debugInit.isLoggable(FINE)) { 1975 debugInit.fine("Doing create and relate orig vars for: " + exit_ppt.name()); 1976 } 1977 1978 PptTopLevel entry_ppt = ppts.get(exit_ppt.ppt_name.makeEnter()); 1979 if (entry_ppt == null) { 1980 throw new Daikon.UserError("exit found with no corresponding entry: " + exit_ppt.name()); 1981 } 1982 1983 // Add "orig(...)" (prestate) variables to the program point. 1984 // Don't bother to include the constants. Walk through 1985 // entry_ppt's vars. For each non-constant, put it on the 1986 // new_vis worklist after fixing its comparability information. 1987 exit_ppt.num_orig_vars = entry_ppt.num_tracevars; 1988 VarInfo[] new_vis = new VarInfo[exit_ppt.num_orig_vars]; 1989 { 1990 VarInfo[] entry_ppt_vis = entry_ppt.var_infos; 1991 int new_vis_index = 0; 1992 for (int k = 0; k < entry_ppt.num_declvars; k++) { 1993 VarInfo vi = entry_ppt_vis[k]; 1994 assert !vi.isDerived() : "Derived when making orig(): " + vi.name(); 1995 if (vi.isStaticConstant()) { 1996 continue; 1997 } 1998 VarInfo origvar = VarInfo.origVarInfo(vi); 1999 // Fix comparability 2000 VarInfo postvar = exit_ppt.find_var_by_name(vi.name()); 2001 if (postvar == null) { 2002 System.out.printf( 2003 "Looking for postvar, can't find var %s in exit of ppt %s%n", vi, exit_ppt.name()); 2004 for (VarInfo cvi : entry_ppt.var_infos) { 2005 System.out.printf(" entry var = %s%n", cvi); 2006 } 2007 for (VarInfo cvi : exit_ppt.var_infos) { 2008 System.out.printf(" exit var = %s%n", cvi); 2009 } 2010 throw new RuntimeException("this can't happen: postvar is null"); 2011 } 2012 origvar.postState = postvar; 2013 origvar.comparability = postvar.comparability.makeAlias(); 2014 2015 // add parents for override relations 2016 // exit_ppt.parents has not been loaded at this point 2017 for (VarParent pi : postvar.parents) { 2018 PptTopLevel parentppt = ppts.get(pi.parent_ppt); 2019 if (parentppt != null) { 2020 if (!parentppt.is_object() && !parentppt.is_class()) { 2021 VarInfo pvi = 2022 parentppt.find_var_by_name( 2023 pi.parent_variable == null ? postvar.name() : pi.parent_variable); 2024 if (pvi != null) { 2025 origvar.parents.add( 2026 new VarParent(pi.parent_ppt, pi.parent_relation_id, pvi.prestate_name())); 2027 } 2028 } 2029 } 2030 } 2031 2032 // Add to new_vis 2033 new_vis[new_vis_index] = origvar; 2034 new_vis_index++; 2035 // System.out.printf("adding origvar %s to ppt %s%n", origvar.name(), 2036 // exit_ppt.name()); 2037 } 2038 assert new_vis_index == exit_ppt.num_orig_vars; 2039 } 2040 exit_ppt.addVarInfos(new_vis); 2041 2042 if (VarInfo.assertionsEnabled()) { 2043 for (VarInfo vi : exit_ppt.var_infos) { 2044 try { 2045 vi.checkRep(); 2046 } catch (Throwable e) { 2047 System.err.println(); 2048 System.err.println("Error with variable " + vi + " at ppt " + exit_ppt); 2049 throw e; 2050 } 2051 } 2052 } 2053 } 2054 2055 /////////////////////////////////////////////////////////////////////////// 2056 // Read decls, dtrace, etc. files 2057 2058 /** 2059 * Load a set of decl files. 2060 * 2061 * @param decl_files the files to load 2062 * @return the PptMap for the loaded files 2063 */ 2064 @RequiresNonNull("fileio_progress") 2065 // set in mainHelper 2066 private static PptMap load_decls_files(Set<File> decl_files) { 2067 long startTime = System.nanoTime(); 2068 try { 2069 if (!Daikon.dkconfig_quiet) { 2070 System.out.print("Reading declaration files "); 2071 } 2072 PptMap all_ppts = FileIO.read_declaration_files(decl_files); 2073 if (debugTrace.isLoggable(FINE)) { 2074 debugTrace.fine("Initializing partial order"); 2075 } 2076 fileio_progress.clear(); 2077 if (!Daikon.dkconfig_quiet && decl_files.size() > 0) { 2078 System.out.print("\r(read "); 2079 System.out.print(StringsPlume.nplural(decl_files.size(), "decls file")); 2080 System.out.println(")"); 2081 } 2082 return all_ppts; 2083 } catch (IOException e) { 2084 // System.out.println(); 2085 // e.printStackTrace(); 2086 throw new Daikon.UserError(e, "Error parsing decl file"); 2087 } finally { 2088 long duration = System.nanoTime() - startTime; 2089 debugProgress.fine( 2090 "Time spent on read_declaration_files: " + TimeUnit.NANOSECONDS.toSeconds(duration)); 2091 } 2092 } 2093 2094 private static void load_spinfo_files(Set<File> spinfo_files) { 2095 if (PptSplitter.dkconfig_disable_splitting || spinfo_files.isEmpty()) { 2096 return; 2097 } 2098 long startTime = System.nanoTime(); 2099 try { 2100 System.out.print("Reading splitter info files "); 2101 create_splitters(spinfo_files); 2102 System.out.print("\r(read "); 2103 System.out.print(StringsPlume.nplural(spinfo_files.size(), "spinfo file")); 2104 System.out.print(", "); 2105 System.out.print( 2106 StringsPlume.nplural(SpinfoFile.numSplittterObjects(spinfoFiles), "splitter")); 2107 System.out.println(")"); 2108 } catch (IOException e) { 2109 System.out.println(); 2110 e.printStackTrace(); 2111 throw new Error(e); 2112 } finally { 2113 long duration = System.nanoTime() - startTime; 2114 debugProgress.fine( 2115 "Time spent on load_spinfo_files: " + TimeUnit.NANOSECONDS.toSeconds(duration)); 2116 } 2117 } 2118 2119 /** 2120 * A wrapper around {@link ContextSplitterFactory#load_mapfiles_into_splitterlist}. 2121 * 2122 * @param map_files the map files to read into SplitterList 2123 */ 2124 private static void load_map_files(Set<File> map_files) { 2125 long startTime = System.nanoTime(); 2126 if (!PptSplitter.dkconfig_disable_splitting && map_files.size() > 0) { 2127 System.out.print("Reading map (context) files "); 2128 ContextSplitterFactory.load_mapfiles_into_splitterlist( 2129 map_files, ContextSplitterFactory.dkconfig_granularity); 2130 System.out.print("\r(read "); 2131 System.out.print(StringsPlume.nplural(map_files.size(), "map (context) file")); 2132 System.out.println(")"); 2133 long duration = System.nanoTime() - startTime; 2134 debugProgress.fine( 2135 "Time spent on load_map_files: " + TimeUnit.NANOSECONDS.toSeconds(duration)); 2136 } 2137 } 2138 2139 /** 2140 * Sets up splitting on all ppts. Currently only binary splitters over boolean returns or exactly 2141 * two return statements are enabled by default (though other splitters can be defined by the 2142 * user). 2143 * 2144 * @param ppt the program point to add conditions to 2145 */ 2146 @SuppressWarnings("nullness:contracts.precondition") 2147 public static void setup_splitters(PptTopLevel ppt) { 2148 if (PptSplitter.dkconfig_disable_splitting) { 2149 return; 2150 } 2151 2152 Global.debugSplit.fine("<<enter>> setup_splitters"); 2153 2154 SplitterFactory.load_splitters(ppt, spinfoFiles); 2155 2156 Splitter[] pconds; 2157 if (SplitterList.dkconfig_all_splitters) { 2158 pconds = SplitterList.get_all(); 2159 } else { 2160 pconds = SplitterList.get(ppt.name()); 2161 } 2162 if (pconds != null) { 2163 Global.debugSplit.fine( 2164 "Got " + StringsPlume.nplural(pconds.length, "splitter") + " for " + ppt.name()); 2165 ppt.addConditions(pconds); 2166 } 2167 2168 Global.debugSplit.fine("<<exit>> setup_splitters"); 2169 } 2170 2171 /////////////////////////////////////////////////////////////////////////// 2172 // Infer invariants over the trace data 2173 2174 /** 2175 * The number of columns of progress information to display. In many Unix shells, this can be set 2176 * to an appropriate value by {@code --config_option 2177 * daikon.Daikon.progress_display_width=$COLUMNS}. 2178 */ 2179 public static int dkconfig_progress_display_width = 80; 2180 2181 /** 2182 * Human-friendly progress status message. If {@code fileio_progress} is non-null, then this is 2183 * ignored. So this is primarily for progress reports that are not IO-related. 2184 */ 2185 public static String progress = ""; 2186 2187 // Is set unconditionally in mainHelper 2188 /** Takes precedence over the progress variable. */ 2189 private static @MonotonicNonNull FileIOProgress fileio_progress = null; 2190 2191 /** Outputs FileIO progress information. Uses global variable FileIO.data_trace_state. */ 2192 public static class FileIOProgress extends Thread { 2193 public FileIOProgress() { 2194 setDaemon(true); 2195 } 2196 2197 /** 2198 * Clients should set this variable instead of calling Thread.stop(), which is deprecated. 2199 * Typically a client calls "display()" before setting this. The stopping happens later, and 2200 * calls clear() anyway. 2201 */ 2202 public boolean shouldStop = false; 2203 2204 @Override 2205 public void run() { 2206 if (dkconfig_progress_delay == -1) { 2207 return; 2208 } 2209 while (true) { 2210 if (shouldStop) { 2211 clear(); 2212 return; 2213 } 2214 display(); 2215 try { 2216 sleep(dkconfig_progress_delay); 2217 } catch (InterruptedException e) { 2218 // hmm 2219 } 2220 } 2221 } 2222 2223 /** Clear the display; good to do before printing to System.out. */ 2224 public void clear() { 2225 if (dkconfig_progress_delay == -1) { 2226 return; 2227 } 2228 // "display("");" is wrong becuase it leaves the timestamp and writes 2229 // spaces across the screen. 2230 String status = StringsPlume.rpad("", dkconfig_progress_display_width - 1); 2231 System.out.print("\r" + status); 2232 System.out.print("\r"); // return to beginning of line 2233 System.out.flush(); 2234 } 2235 2236 /** 2237 * Displays the current status. Call this if you don't want to wait until the next automatic 2238 * display. 2239 */ 2240 public void display() { 2241 if (dkconfig_progress_delay == -1) { 2242 return; 2243 } 2244 2245 String message; 2246 if (FileIO.data_trace_state != null) { 2247 message = FileIO.data_trace_state.reading_message(); 2248 } else { 2249 if (Daikon.progress == null) { 2250 message = "[no status]"; 2251 } else { 2252 message = Daikon.progress; 2253 } 2254 } 2255 display(message); 2256 } 2257 2258 /** 2259 * Displays the given message. 2260 * 2261 * @param message message to be displayed 2262 */ 2263 public void display(String message) { 2264 if (dkconfig_progress_delay == -1) { 2265 return; 2266 } 2267 String status = 2268 StringsPlume.rpad( 2269 "[" + LocalDateTime.now(ZoneId.systemDefault()) + "]: " + message, 2270 dkconfig_progress_display_width - 1); 2271 System.out.print("\r" + status); 2272 System.out.flush(); 2273 // System.out.println (status); // for debugging 2274 2275 if (debugTrace.isLoggable(FINE)) { 2276 debugTrace.fine("Free memory: " + java.lang.Runtime.getRuntime().freeMemory()); 2277 debugTrace.fine( 2278 "Used memory: " 2279 + (java.lang.Runtime.getRuntime().totalMemory() 2280 - java.lang.Runtime.getRuntime().freeMemory())); 2281 try { 2282 if (FileIO.data_trace_state != null) { 2283 debugTrace.fine("Active slices: " + FileIO.data_trace_state.all_ppts.countSlices()); 2284 } 2285 } catch (ConcurrentModificationException e) { 2286 // Because this code is a separate thread, the number of ppts 2287 // could change during countSlices. Just ignore and continue. 2288 } 2289 } 2290 } 2291 } 2292 2293 /** 2294 * The data-processing routine of the daikon engine. At this point, the decls and spinfo files 2295 * have been loaded, all of the program points have been setup, and candidate invariants have been 2296 * instantiated. This routine processes data to falsify the candidate invariants. 2297 */ 2298 @RequiresNonNull("fileio_progress") 2299 // set in mainHelper 2300 private static void process_data(PptMap all_ppts, Set<String> dtrace_files) { 2301 MemMonitor monitor = null; 2302 if (use_mem_monitor) { 2303 monitor = new MemMonitor("stat.out"); 2304 new Thread((Runnable) monitor).start(); 2305 } 2306 2307 long startTime = System.nanoTime(); 2308 2309 // Preprocessing 2310 setup_NISuppression(); 2311 2312 // Processing (actually using dtrace files) 2313 try { 2314 fileio_progress.clear(); 2315 if (!Daikon.dkconfig_quiet) { 2316 System.out.println( 2317 "Processing trace data; reading " 2318 + StringsPlume.nplural(dtrace_files.size(), "dtrace file") 2319 + ":"); 2320 } 2321 FileIO.read_data_trace_files(dtrace_files, all_ppts); 2322 // Final update, so "100%", not "99.70%", is the last thing printed. 2323 // (This doesn't seem to achieve that, though...) 2324 fileio_progress.display(); 2325 fileio_progress.shouldStop = true; 2326 fileio_progress.display(); 2327 if (!Daikon.dkconfig_quiet) { 2328 System.out.println(); 2329 } 2330 // System.out.print("Creating implications "); // XXX untested code 2331 // for (PptTopLevel ppt : all_ppts) { 2332 // System.out.print('.'); 2333 // ppt.addImplications(); 2334 // } 2335 // System.out.println(); 2336 } catch (IOException e) { 2337 // System.out.println(); 2338 // e.printStackTrace(); 2339 throw new Error(e); 2340 } finally { 2341 long duration = System.nanoTime() - startTime; 2342 debugProgress.fine( 2343 "Time spent on read_data_trace_files: " + TimeUnit.NANOSECONDS.toSeconds(duration)); 2344 } 2345 2346 if (monitor != null) { 2347 monitor.stop(); 2348 } 2349 2350 if (FileIO.dkconfig_read_samples_only) { 2351 throw new Daikon.NormalTermination( 2352 String.format("Finished reading %d samples", FileIO.samples_processed)); 2353 } 2354 2355 if (all_ppts.size() == 0) { 2356 String message = "No program point declarations were found."; 2357 if (FileIO.omitted_declarations != 0) { 2358 message += 2359 lineSep 2360 + " " 2361 + FileIO.omitted_declarations 2362 + " " 2363 + ((FileIO.omitted_declarations == 1) ? "declaration was" : "declarations were") 2364 + " omitted by regexps (e.g., --ppt-select-pattern)."; 2365 } 2366 throw new Daikon.UserError(message); 2367 } 2368 2369 // System.out.println("samples processed: " + FileIO.samples_processed); 2370 2371 int unmatched_count = FileIO.call_stack.size() + FileIO.call_hashmap.size(); 2372 if ((use_dataflow_hierarchy && FileIO.samples_processed == unmatched_count) 2373 || (FileIO.samples_processed == 0)) { 2374 throw new Daikon.UserError( 2375 "No samples found for any of " + StringsPlume.nplural(all_ppts.size(), "program point")); 2376 } 2377 2378 // ppt_stats (all_ppts); 2379 2380 // if (debugStats.isLoggable (FINE)) { 2381 // PptSliceEquality.print_equality_stats (debugStats, all_ppts); 2382 // } 2383 2384 // Print equality set info 2385 // for (PptTopLevel ppt : all_ppts.pptIterable()) { 2386 // System.out.printf("ppt: %s", ppt.name); 2387 // if ((ppt.equality_view == null) || (ppt.equality_view.invs == null)) 2388 // continue; 2389 // for (Invariant inv : ppt.equality_view.invs) { 2390 // Equality e = (Equality) inv; 2391 // System.out.printf(" equality set = %s", e); 2392 // } 2393 // } 2394 2395 // System.out.printf("printing ternary invariants"); 2396 // PrintInvariants.print_all_ternary_invs (all_ppts); 2397 // System.exit(0); 2398 2399 // Postprocessing 2400 2401 debugProgress.fine("Create Combined Exits ... "); 2402 startTime = System.nanoTime(); 2403 create_combined_exits(all_ppts); 2404 long duration = System.nanoTime() - startTime; 2405 debugProgress.fine( 2406 "Create Combined Exits ... done [" + TimeUnit.NANOSECONDS.toSeconds(duration) + "]"); 2407 2408 // Post process dynamic constants 2409 if (DynamicConstants.dkconfig_use_dynamic_constant_optimization) { 2410 debugProgress.fine("Constant Post Processing ... "); 2411 startTime = System.nanoTime(); 2412 for (PptTopLevel ppt : all_ppts.ppt_all_iterable()) { 2413 if (ppt.constants != null) ppt.constants.post_process(); 2414 } 2415 duration = System.nanoTime() - startTime; 2416 debugProgress.fine( 2417 "Constant Post Processing ... done [" + TimeUnit.NANOSECONDS.toSeconds(duration) + "]"); 2418 } 2419 2420 // Initialize the partial order hierarchy 2421 debugProgress.fine("Init Hierarchy ... "); 2422 startTime = System.nanoTime(); 2423 assert FileIO.new_decl_format != null 2424 : "@AssumeAssertion(nullness): read data, so new_decl_format is set"; 2425 if (FileIO.new_decl_format) { 2426 PptRelation.init_hierarchy_new(all_ppts); 2427 } else { 2428 PptRelation.init_hierarchy(all_ppts); 2429 } 2430 duration = System.nanoTime() - startTime; 2431 debugProgress.fine( 2432 "Init Hierarchy ... done [" + TimeUnit.NANOSECONDS.toSeconds(duration) + "]"); 2433 2434 // Calculate invariants at all non-leaf ppts 2435 if (use_dataflow_hierarchy) { 2436 debugProgress.fine("createUpperPpts ... "); 2437 startTime = System.nanoTime(); 2438 // calculates invariants; does not actually create any ppts 2439 createUpperPpts(all_ppts); 2440 duration = System.nanoTime() - startTime; 2441 debugProgress.fine( 2442 "createUpperPpts ... done [" + TimeUnit.NANOSECONDS.toSeconds(duration) + "]"); 2443 } 2444 2445 // Equality data for each PptTopLevel. 2446 if (Daikon.use_equality_optimization && !Daikon.dkconfig_undo_opts) { 2447 debugProgress.fine("Equality Post Process ... "); 2448 startTime = System.nanoTime(); 2449 for (PptTopLevel ppt : all_ppts.ppt_all_iterable()) { 2450 // ppt.equality_view can be null here 2451 ppt.postProcessEquality(); 2452 } 2453 duration = System.nanoTime() - startTime; 2454 debugProgress.fine( 2455 "Equality Post Process ... done [" + TimeUnit.NANOSECONDS.toSeconds(duration) + "]"); 2456 } 2457 2458 // undo optimizations; results in a more redundant but more complete 2459 // set of invariants 2460 if (Daikon.dkconfig_undo_opts) { 2461 undoOpts(all_ppts); 2462 } 2463 2464 // Debug print information about equality sets 2465 if (debugEquality.isLoggable(FINE)) { 2466 for (PptTopLevel ppt : all_ppts.ppt_all_iterable()) { 2467 debugEquality.fine(ppt.name() + ": " + ppt.equality_sets_txt()); 2468 } 2469 } 2470 2471 debugProgress.fine("Non-implication postprocessing ... done"); 2472 2473 isInferencing = false; 2474 2475 // Add implications 2476 startTime = System.nanoTime(); 2477 fileio_progress.clear(); 2478 if (!PptSplitter.dkconfig_disable_splitting) { 2479 debugProgress.fine("Adding Implications ... "); 2480 for (PptTopLevel ppt : all_ppts.pptIterable()) { 2481 // debugProgress.fine (" Adding implications for " + ppt.name); 2482 ppt.addImplications(); 2483 } 2484 duration = System.nanoTime() - startTime; 2485 debugProgress.fine( 2486 "Adding Implications ... done [" + TimeUnit.NANOSECONDS.toSeconds(duration) + "]"); 2487 } 2488 } 2489 2490 private static class Count { 2491 public int val; 2492 2493 Count(int val) { 2494 this.val = val; 2495 } 2496 } 2497 2498 /** Print out basic statistics (samples, invariants, variables, etc) about each ppt. */ 2499 public static void ppt_stats(PptMap all_ppts) { 2500 2501 int all_ppt_cnt = 0; 2502 int ppt_w_sample_cnt = 0; 2503 for (PptTopLevel ppt : all_ppts.pptIterable()) { 2504 all_ppt_cnt++; 2505 if (ppt.num_samples() == 0) { 2506 continue; 2507 } 2508 ppt_w_sample_cnt++; 2509 System.out.printf("%s%n", ppt.name()); 2510 System.out.printf(" samples = %n%d", ppt.num_samples()); 2511 System.out.printf(" invariants = %n%d", ppt.invariant_cnt()); 2512 Map<ProglangType, Count> type_map = new LinkedHashMap<>(); 2513 int leader_cnt = 0; 2514 for (VarInfo v : ppt.var_infos) { 2515 if (!v.isCanonical()) { 2516 continue; 2517 } 2518 leader_cnt++; 2519 Count cnt = type_map.computeIfAbsent(v.file_rep_type, __ -> new Count(0)); 2520 cnt.val++; 2521 } 2522 System.out.println(" vars = " + ppt.var_infos.length); 2523 System.out.println(" leaders = " + leader_cnt); 2524 for (Map.Entry<@KeyFor("type_map") ProglangType, Count> e : type_map.entrySet()) { 2525 ProglangType file_rep_type = e.getKey(); 2526 Count cnt = e.getValue(); 2527 System.out.printf(" %s = %d%n", file_rep_type, cnt.val); 2528 } 2529 } 2530 System.out.println("Total ppt count = " + all_ppt_cnt); 2531 System.out.println("PPts w/sample count = " + ppt_w_sample_cnt); 2532 } 2533 2534 /** Process the invariants with simplify to remove redundant invariants. */ 2535 private static void suppressWithSimplify(PptMap all_ppts) { 2536 System.out.print("Invoking Simplify to identify redundant invariants"); 2537 System.out.flush(); 2538 long startTime = System.nanoTime(); 2539 for (PptTopLevel ppt : all_ppts.ppt_all_iterable()) { 2540 ppt.mark_implied_via_simplify(all_ppts); 2541 System.out.print("."); 2542 System.out.flush(); 2543 } 2544 long duration = System.nanoTime() - startTime; 2545 System.out.println(TimeUnit.NANOSECONDS.toSeconds(duration)); 2546 2547 // Make sure the Simplify process and helper threads are finished 2548 LemmaStack proverStack = PptTopLevel.getProverStack(); 2549 if (proverStack != null) { 2550 proverStack.close(); 2551 } 2552 } 2553 2554 /** Initialize NIS suppression. */ 2555 @EnsuresNonNull({ 2556 "daikon.suppress.NIS.suppressor_map", 2557 "daikon.suppress.NIS.suppressor_map_suppression_count", 2558 "daikon.suppress.NIS.all_suppressions", 2559 "daikon.suppress.NIS.suppressor_proto_invs" 2560 }) 2561 public static void setup_NISuppression() { 2562 NIS.init_ni_suppression(); 2563 } 2564 2565 /** Initialize the equality sets for each variable. */ 2566 public static void setupEquality(PptTopLevel ppt) { 2567 2568 if (!Daikon.use_equality_optimization) { 2569 return; 2570 } 2571 2572 // Skip points that are not leaves. 2573 if (use_dataflow_hierarchy) { 2574 PptTopLevel p = ppt; 2575 if (ppt instanceof PptConditional) { 2576 p = ((PptConditional) ppt).parent; 2577 } 2578 2579 // Rather than defining leaves as :::GLOBAL or :::EXIT54 (numbered 2580 // exit), we define them as everything except 2581 // ::EXIT (combined), :::ENTER, :::THROWS, :::OBJECT 2582 // and :::CLASS program points. This scheme ensures that arbitrarly 2583 // named program points such as :::POINT (used by convertcsv.pl) 2584 // will be treated as leaves. 2585 if (p.ppt_name.isCombinedExitPoint() 2586 || p.ppt_name.isEnterPoint() 2587 || p.ppt_name.isThrowsPoint() 2588 || p.ppt_name.isObjectInstanceSynthetic() 2589 || p.ppt_name.isClassStaticSynthetic()) { 2590 return; 2591 } 2592 2593 if (ppt.has_splitters()) { 2594 return; 2595 } 2596 } 2597 2598 // Create the initial equality sets 2599 ppt.equality_view = new PptSliceEquality(ppt); 2600 ppt.equality_view.instantiate_invariants(); 2601 } 2602 2603 private static List<SpinfoFile> spinfoFiles = new ArrayList<>(); 2604 2605 /** 2606 * Create user-defined splitters. For each file in the input, add a SpinfoFile to the spinfoFiles 2607 * variable. 2608 */ 2609 public static void create_splitters(Set<File> spinfo_files) throws IOException { 2610 for (File filename : spinfo_files) { 2611 SpinfoFile sf = SplitterFactory.parse_spinfofile(filename); 2612 spinfoFiles.add(sf); 2613 } 2614 } 2615 2616 // /** 2617 // * Guard the invariants at all PptTopLevels. Note that this changes 2618 // * the contents of the PptTopLevels, and the changes made should 2619 // * probably not be written out to an inv file (save the file before 2620 // * this is called). 2621 // */ 2622 // public static void guardInvariants(PptMap allPpts) { 2623 // for (PptTopLevel ppt : allPpts.asCollection()) { 2624 // if (ppt.num_samples() == 0) 2625 // continue; 2626 // // Make sure isDerivedParam is set before guarding. Otherwise 2627 // // we'll never get it correct. 2628 // for (int iVarInfo = 0; 2629 // iVarInfo < ppt.var_infos.length; 2630 // iVarInfo++) { 2631 // boolean temp = 2632 // ppt.var_infos[iVarInfo].isDerivedParamAndUninteresting(); 2633 // } 2634 // 2635 // ppt.guardInvariants(); 2636 // } 2637 // } 2638 2639 /** Removed invariants as specified in omit_types. */ 2640 private static void processOmissions(PptMap allPpts) { 2641 if (omit_types['0']) allPpts.removeUnsampled(); 2642 for (PptTopLevel ppt : allPpts.asCollection()) { 2643 ppt.processOmissions(omit_types); 2644 } 2645 } 2646 2647 /** 2648 * Returns the ppt name, max_ppt, that corresponds to the specified percentage of ppts (presuming 2649 * that only those ppts ≤ max_ppt will be processed). 2650 */ 2651 private static @Nullable String setup_ppt_perc(Collection<File> decl_files, int ppt_perc) { 2652 2653 // Make sure the percentage is valid 2654 if ((ppt_perc < 1) || (ppt_perc > 100)) { 2655 // The number should already have been checked, so don't use UserError. 2656 throw new BugInDaikon("ppt_perc of " + ppt_perc + " is out of range 1..100"); 2657 } 2658 if (ppt_perc == 100) { 2659 return null; 2660 } 2661 2662 // Keep track of all of the ppts in a set ordered by the ppt name 2663 Set<String> ppts = new TreeSet<>(); 2664 2665 // Read all of the ppt names out of the decl files 2666 try { 2667 for (File file : decl_files) { 2668 2669 // Open the file 2670 try (LineNumberReader fp = FilesPlume.newLineNumberFileReader(file)) { 2671 2672 // Read each ppt name from the file 2673 for (String line = fp.readLine(); line != null; line = fp.readLine()) { 2674 if (line.equals("") || FileIO.isComment(line)) { 2675 continue; 2676 } 2677 if (!line.equals("DECLARE")) { 2678 continue; 2679 } 2680 // Just read "DECLARE", so next line has ppt name. 2681 String ppt_name = fp.readLine(); 2682 if (ppt_name == null) { 2683 throw new Daikon.UserError("File " + file + " terminated prematurely"); 2684 } 2685 ppts.add(ppt_name); 2686 } 2687 } 2688 } 2689 } catch (IOException e) { 2690 e.printStackTrace(); 2691 throw new Error(e); 2692 } 2693 2694 // Determine the ppt_name that matches the specified percentage. Always 2695 // return the last exit point from the method (so we don't get half the 2696 // exits from a method or enters without exits, etc) 2697 int ppt_cnt = (ppts.size() * ppt_perc) / 100; 2698 if (ppt_cnt == 0) { 2699 throw new Daikon.UserError( 2700 "ppt_perc of " + ppt_perc + "% results in processing 0 out of " + ppts.size() + " ppts"); 2701 } 2702 for (Iterator<String> i = ppts.iterator(); i.hasNext(); ) { 2703 String ppt_name = i.next(); 2704 if (--ppt_cnt <= 0) { 2705 String last_ppt_name = ppt_name; 2706 while (i.hasNext()) { 2707 ppt_name = i.next(); 2708 if ((last_ppt_name.indexOf("EXIT") != -1) && (ppt_name.indexOf("EXIT") == -1)) { 2709 return last_ppt_name; 2710 } 2711 last_ppt_name = ppt_name; 2712 } 2713 return ppt_name; 2714 } 2715 } 2716 // Execution should not reach this line 2717 throw new Error("ppt_cnt " + ppt_cnt + " ppts.size " + ppts.size()); 2718 } 2719 2720 /** 2721 * Undoes the invariants suppressed for the dynamic constant, suppression and equality set 2722 * optimizations (should yield the same invariants as the simple incremental algorithm. 2723 */ 2724 @RequiresNonNull({"daikon.suppress.NIS.all_suppressions", "daikon.suppress.NIS.suppressor_map"}) 2725 public static void undoOpts(PptMap all_ppts) { 2726 2727 // undo suppressions 2728 for (PptTopLevel ppt : all_ppts.ppt_all_iterable()) { 2729 NIS.create_suppressed_invs(ppt); 2730 } 2731 2732 // undo equality sets 2733 for (PptTopLevel ppt : all_ppts.ppt_all_iterable()) { 2734 PptSliceEquality sliceEquality = ppt.equality_view; 2735 2736 // some program points have no equality sets? 2737 if (sliceEquality == null) { 2738 // System.out.println(ppt.name); 2739 continue; 2740 } 2741 2742 // get the new leaders 2743 List<Equality> allNewInvs = new ArrayList<>(); 2744 2745 for (Invariant eq_as_inv : sliceEquality.invs) { 2746 Equality eq = (Equality) eq_as_inv; 2747 VarInfo leader = eq.leader(); 2748 List<VarInfo> vars = new ArrayList<>(); 2749 2750 for (VarInfo var : eq.getVars()) { 2751 if (!var.equals(leader)) { 2752 vars.add(var); 2753 } 2754 } 2755 2756 if (vars.size() > 0) { 2757 2758 // Create new equality sets for all of the non-equal vars 2759 List<Equality> newInvs = sliceEquality.createEqualityInvs(vars, eq); 2760 2761 // Create new slices and invariants for each new leader 2762 // copyInvsFromLeader(sliceEquality, leader, vars); 2763 sliceEquality.copyInvsFromLeader(leader, vars); 2764 2765 // Keep track of all of the new invariants created. 2766 // Add all of the new equality sets to our list 2767 allNewInvs.addAll(newInvs); 2768 } 2769 } 2770 2771 sliceEquality.invs.addAll(allNewInvs); 2772 } 2773 } 2774}