001package daikon; 002 003import static daikon.FileIO.ParentRelation; 004import static daikon.PptRelation.PptRelationType; 005import static daikon.tools.nullness.NullnessUtil.castNonNullDeep; 006 007import daikon.derive.Derivation; 008import daikon.derive.binary.BinaryDerivation; 009import daikon.derive.binary.BinaryDerivationFactory; 010import daikon.derive.binary.SequenceFloatIntersectionFactory; 011import daikon.derive.binary.SequenceFloatSubscriptFactory; 012import daikon.derive.binary.SequenceFloatUnionFactory; 013import daikon.derive.binary.SequenceScalarIntersectionFactory; 014import daikon.derive.binary.SequenceScalarSubscriptFactory; 015import daikon.derive.binary.SequenceScalarUnionFactory; 016import daikon.derive.binary.SequenceStringIntersectionFactory; 017import daikon.derive.binary.SequenceStringSubscriptFactory; 018import daikon.derive.binary.SequenceStringUnionFactory; 019import daikon.derive.binary.SequencesConcatFactory; 020import daikon.derive.binary.SequencesJoinFactory; 021import daikon.derive.binary.SequencesPredicateFactory; 022import daikon.derive.ternary.SequenceFloatArbitrarySubsequenceFactory; 023import daikon.derive.ternary.SequenceScalarArbitrarySubsequenceFactory; 024import daikon.derive.ternary.SequenceStringArbitrarySubsequenceFactory; 025import daikon.derive.ternary.TernaryDerivation; 026import daikon.derive.ternary.TernaryDerivationFactory; 027import daikon.derive.unary.SequenceInitialFactory; 028import daikon.derive.unary.SequenceInitialFactoryFloat; 029import daikon.derive.unary.SequenceLengthFactory; 030import daikon.derive.unary.SequenceMinMaxSumFactory; 031import daikon.derive.unary.StringLengthFactory; 032import daikon.derive.unary.UnaryDerivation; 033import daikon.derive.unary.UnaryDerivationFactory; 034import daikon.inv.DiscardCode; 035import daikon.inv.DiscardInfo; 036import daikon.inv.Equality; 037import daikon.inv.Implication; 038import daikon.inv.Invariant; 039import daikon.inv.InvariantStatus; 040import daikon.inv.OutputFormat; 041import daikon.inv.ValueSet; 042import daikon.inv.binary.twoScalar.FloatEqual; 043import daikon.inv.binary.twoScalar.IntEqual; 044import daikon.inv.binary.twoScalar.IntGreaterEqual; 045import daikon.inv.binary.twoScalar.IntGreaterThan; 046import daikon.inv.binary.twoScalar.IntLessEqual; 047import daikon.inv.binary.twoScalar.IntLessThan; 048import daikon.inv.binary.twoSequence.SeqSeqFloatEqual; 049import daikon.inv.binary.twoSequence.SeqSeqIntEqual; 050import daikon.inv.binary.twoSequence.SeqSeqStringEqual; 051import daikon.inv.binary.twoSequence.SubSequence; 052import daikon.inv.binary.twoSequence.SubSequenceFloat; 053import daikon.inv.binary.twoSequence.SubSet; 054import daikon.inv.binary.twoSequence.SubSetFloat; 055import daikon.inv.binary.twoString.StringEqual; 056import daikon.inv.filter.InvariantFilters; 057import daikon.inv.unary.scalar.LowerBound; 058import daikon.inv.unary.scalar.LowerBoundFloat; 059import daikon.inv.unary.scalar.NonZero; 060import daikon.inv.unary.scalar.UpperBound; 061import daikon.inv.unary.scalar.UpperBoundFloat; 062import daikon.inv.unary.sequence.OneOfFloatSequence; 063import daikon.inv.unary.sequence.OneOfSequence; 064import daikon.inv.unary.stringsequence.OneOfStringSequence; 065import daikon.simplify.InvariantLemma; 066import daikon.simplify.Lemma; 067import daikon.simplify.LemmaStack; 068import daikon.simplify.SessionManager; 069import daikon.simplify.SimplifyError; 070import daikon.split.PptSplitter; 071import daikon.split.Splitter; 072import daikon.split.SplitterList; 073import daikon.split.misc.ReturnTrueSplitter; 074import daikon.suppress.NIS; 075import daikon.suppress.NISuppressionSet; 076import java.io.IOException; 077import java.io.ObjectInputStream; 078import java.text.DecimalFormat; 079import java.text.NumberFormat; 080import java.util.ArrayList; 081import java.util.Arrays; 082import java.util.BitSet; 083import java.util.Collection; 084import java.util.Collections; 085import java.util.Comparator; 086import java.util.EnumSet; 087import java.util.HashMap; 088import java.util.Iterator; 089import java.util.LinkedHashMap; 090import java.util.LinkedHashSet; 091import java.util.List; 092import java.util.Map; 093import java.util.NoSuchElementException; 094import java.util.Set; 095import java.util.StringJoiner; 096import java.util.TreeMap; 097import java.util.concurrent.TimeUnit; 098import java.util.logging.Level; 099import java.util.logging.Logger; 100import org.checkerframework.checker.initialization.qual.Initialized; 101import org.checkerframework.checker.initialization.qual.UnderInitialization; 102import org.checkerframework.checker.initialization.qual.UnknownInitialization; 103import org.checkerframework.checker.interning.qual.Interned; 104import org.checkerframework.checker.lock.qual.GuardSatisfied; 105import org.checkerframework.checker.mustcall.qual.Owning; 106import org.checkerframework.checker.nullness.qual.EnsuresNonNull; 107import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf; 108import org.checkerframework.checker.nullness.qual.KeyFor; 109import org.checkerframework.checker.nullness.qual.MonotonicNonNull; 110import org.checkerframework.checker.nullness.qual.NonNull; 111import org.checkerframework.checker.nullness.qual.Nullable; 112import org.checkerframework.checker.nullness.qual.RequiresNonNull; 113import org.checkerframework.dataflow.qual.Pure; 114import org.checkerframework.dataflow.qual.SideEffectFree; 115import org.plumelib.reflection.ReflectionPlume; 116import org.plumelib.util.CollectionsPlume; 117import org.plumelib.util.StringsPlume; 118import typequals.prototype.qual.Prototype; 119 120/** 121 * All information about a single program point. A Ppt may also represent just part of the data: see 122 * PptConditional. 123 * 124 * <p>PptTopLevel doesn't do any direct computation, instead deferring that to its views that are 125 * slices and that actually contain the invariants. 126 * 127 * <p>The data layout is as follows: 128 * 129 * <ul> 130 * <li>A PptMap is a collection of PptTopLevel objects. 131 * <li>A PptTopLevel contains PptSlice objects, one for each set of variables at the program 132 * point. For instance, if a PptTopLevel has variables a, b, and c, then it has three 133 * PptSlice1 objects (one for a; one for b; and one for c), three PptSlice2 objects (one for 134 * a,b; one for a,c; and one for b,c), and one PptSlice3 object (for a,b,c). 135 * <li>A PptSlice object contains invariants. When a sample (a tuple of variable values) is fed to 136 * a PptTopLevel, it in turn feeds it to all the slices, which feed it to all the invariants, 137 * which act on it appropriately. 138 * </ul> 139 */ 140public class PptTopLevel extends Ppt { 141 static final long serialVersionUID = 20071129L; 142 143 /** If true, print diagnostic information to standard out. */ 144 private static final boolean debugStdout = false; 145 146 // Variables starting with dkconfig_ should only be set via the 147 // daikon.config.Configuration interface. 148 /** 149 * Boolean. If true, create implications for all pairwise combinations of conditions, and all 150 * pairwise combinations of exit points. If false, create implications for only the first two 151 * conditions, and create implications only if there are exactly two exit points. 152 */ 153 public static boolean dkconfig_pairwise_implications = false; 154 155 /** 156 * Remove invariants at lower program points when a matching invariant is created at a higher 157 * program point. For experimental purposes only. 158 */ 159 public static boolean dkconfig_remove_merged_invs = false; 160 161 /** 162 * Boolean. Needed by the NIS.falsified method when keeping stats to figure out how many falsified 163 * invariants are antecedents. Only the first pass of processing with the sample is counted toward 164 * the stats. 165 */ 166 public static boolean first_pass_with_sample = true; 167 168 /** Ppt attributes (specified in decl records) */ 169 public enum PptFlags { 170 STATIC, 171 ENTER, 172 EXIT, 173 PRIVATE, 174 RETURN 175 }; 176 177 /** Attributes of this ppt. */ 178 public EnumSet<PptFlags> flags = EnumSet.noneOf(PptFlags.class); 179 180 /** 181 * Possible types of program points. POINT is a generic, non-program language point. It is the 182 * default and can be used when the others are not appropriate. 183 */ 184 public enum PptType { 185 POINT, 186 CLASS, 187 OBJECT, 188 ENTER, 189 EXIT, 190 SUBEXIT 191 } 192 193 /** Type of this program point. */ 194 public PptType type; 195 196 /** Number of invariants after equality set processing for the last sample. */ 197 public int instantiated_inv_cnt = 0; 198 199 /** Number of slices after equality set processing for the last sample. */ 200 public int instantiated_slice_cnt = 0; 201 202 /** Main debug tracer. */ 203 public static final Logger debug = Logger.getLogger("daikon.PptTopLevel"); 204 205 /** Debug tracer for instantiated slices. */ 206 public static final Logger debugInstantiate = Logger.getLogger("daikon.PptTopLevel.instantiate"); 207 208 /** Debug tracer for timing merges. */ 209 public static final Logger debugTimeMerge = Logger.getLogger("daikon.PptTopLevel.time_merge"); 210 211 /** Debug tracer for equalTo checks. */ 212 public static final Logger debugEqualTo = Logger.getLogger("daikon.PptTopLevel.equal"); 213 214 /** Debug tracer for addImplications. */ 215 public static final Logger debugAddImplications = 216 Logger.getLogger("daikon.PptTopLevel.addImplications"); 217 218 /** Debug tracer for adding and processing conditional ppts. */ 219 public static final Logger debugConditional = Logger.getLogger("daikon.PptTopLevel.conditional"); 220 221 /** Debug tracer for data flow. */ 222 public static final Logger debugFlow = Logger.getLogger("daikon.flow.flow"); 223 224 /** Debug tracer for up-merging equality sets. */ 225 public static final Logger debugMerge = Logger.getLogger("daikon.PptTopLevel.merge"); 226 227 /** Debug tracer for NIS suppression statistics. */ 228 public static final Logger debugNISStats = Logger.getLogger("daikon.PptTopLevel.NISStats"); 229 230 // public static final SimpleLog debug_varinfo = new SimpleLog(false); 231 232 // These used to appear in Ppt, were moved down to PptToplevel 233 public final String name; 234 public final PptName ppt_name; 235 236 @Pure 237 @Override 238 public String name(@GuardSatisfied @UnknownInitialization(PptTopLevel.class) PptTopLevel this) { 239 return name; 240 } 241 242 /** Permutation to swap the order of variables in a binary invariant. */ 243 private static int[] permute_swap = new int[] {1, 0}; 244 245 /** 246 * List of constant variables. Null unless 247 * DynamicConstants.dkconfig_use_dynamic_constant_optimization is set. 248 */ 249 public @MonotonicNonNull DynamicConstants constants = null; 250 251 // Invariant: num_declvars == num_tracevars + num_orig_vars 252 public int num_declvars; // number of variables in the declaration 253 public int num_tracevars; // number of variables in the trace file 254 public int num_orig_vars; // number of _orig vars 255 public int num_static_constant_vars; // these don't appear in the trace file 256 257 private int values_num_samples; 258 259 /** Keep track of which variables are valid (not missing) on each sample. */ 260 ModBitTracker mbtracker; 261 262 /** Keep track of values we have seen for each variable. */ 263 ValueSet[] value_sets; 264 265 /** 266 * All the Views (that is, slices) on this are stored as values in the HashMap. Indexed by a 267 * Arrays.asList array list of Integers holding varinfo_index values. 268 * 269 * <p>For a client to access this private variable, it should use {@link #viewsAsCollection}, 270 * {@link #views_iterable}, or {@link #views_iterator}. 271 */ 272 @SuppressWarnings("serial") 273 private Map<List<Integer>, PptSlice> views; 274 275 /** List of all of the splitters for this ppt. */ 276 // Not List because List doesn't support the trimToSize() method. 277 public @MonotonicNonNull ArrayList<PptSplitter> splitters = null; 278 279 /** 280 * Iterator for all of the conditional ppts. Returns each PptConditional from each entry in 281 * splitters. 282 */ 283 public class CondIterator implements java.util.Iterator<PptConditional> { 284 285 int splitter_index = 0; 286 int ppts_index = 0; 287 288 @Override 289 @SuppressWarnings( 290 "flowexpr.parse.error") // Checker Framework bug: splitters is a field in this class 291 @EnsuresNonNullIf(result = true, expression = "splitters") 292 public boolean hasNext(@GuardSatisfied CondIterator this) { 293 if (splitters == null) { 294 return false; 295 } 296 if (splitter_index >= splitters.size()) { 297 return false; 298 } 299 return true; 300 } 301 302 @Override 303 public PptConditional next(@GuardSatisfied CondIterator this) { 304 305 if (!hasNext()) { 306 throw new NoSuchElementException(); 307 } 308 309 PptSplitter ppt_split = splitters.get(splitter_index); 310 PptConditional ppt = (PptConditional) ppt_split.ppts[ppts_index]; 311 312 if (ppts_index < (ppt_split.ppts.length - 1)) { 313 ppts_index++; 314 } else { 315 splitter_index++; 316 ppts_index = 0; 317 } 318 return ppt; 319 } 320 321 @Override 322 public void remove(@GuardSatisfied CondIterator this) { 323 throw new UnsupportedOperationException("Remove unsupported in CondIterator"); 324 } 325 } 326 327 /** 328 * Returns an iterator over all of the PptConditionals at this ppt. 329 * 330 * @see #cond_iterable() 331 */ 332 public CondIterator cond_iterator() { 333 return new CondIterator(); 334 } 335 336 /** 337 * Returns an iterable over all of the PptConditionals at this ppt. 338 * 339 * @see #cond_iterator() 340 */ 341 public Iterable<PptConditional> cond_iterable() { 342 return CollectionsPlume.iteratorToIterable(new CondIterator()); 343 } 344 345 /** 346 * Returns whether or not this ppt has any splitters. 347 * 348 * @return whether or not this ppt has any splitters 349 */ 350 @SuppressWarnings("contracts.conditional.postcondition") // Checker Framework bug: "splitters" 351 @EnsuresNonNullIf(result = true, expression = "splitters") 352 public boolean has_splitters() { 353 return (splitters != null) && (splitters.size() > 0); 354 } 355 356 /** All children relations in the variable/ppt hierarchy. */ 357 @SuppressWarnings("serial") 358 public List<PptRelation> children = new ArrayList<>(); 359 360 /** All parent relations in the variable/ppt hierarchy. */ 361 @SuppressWarnings("serial") 362 public List<PptRelation> parents = new ArrayList<>(); 363 364 /** 365 * List of parent relations in the variable/ppt hierarchy as specified in the declaration record. 366 * These are used to build the detailed parents/children lists of PptRelation above. 367 */ 368 @SuppressWarnings("serial") 369 public List<ParentRelation> parent_relations; 370 371 /** 372 * Flag that indicates whether or not invariants have been merged from all of this ppts children 373 * to form the invariants here. Necessary because a ppt can have multiple parents and otherwise 374 * we'd needlessly merge multiple times. 375 */ 376 public boolean invariants_merged = false; 377 378 // True while we're inside an invocation of mergeInvs() on this PPT. 379 // Used to prevent calling mergeInvs() recursively on a child in such 380 // a way as to cause an infinite loop, even if there is a loop in the 381 // PPT hierarchy. 382 public boolean in_merge = false; 383 384 /** 385 * Flag that indicates whether or not invariants that are duplicated at the parent have been 386 * removed.. 387 */ 388 public boolean invariants_removed = false; 389 390 /** Contains invariants that represent a "joining" of two others: implications, and, or, etc. */ 391 @SuppressWarnings({ 392 "nullness:assignment", // field won't be used until object is initialized 393 "nullness:argument" // field won't be used until object is initialized 394 }) 395 public PptSlice0 joiner_view = new PptSlice0(this); 396 397 /** Holds Equality invariants. Never null after invariants are instantiated. */ 398 // Is set by Daikon.setupEquality (and a few other methods). Remains null if 399 // Daikon.using_DaikonSimple==true or Daikon.use_equality_optimization==false. 400 public @MonotonicNonNull PptSliceEquality equality_view; 401 402 // The redundant_invs* variables are filled in by method 403 // mark_implied_via_simplify. 404 /** Redundant invariants, except for Equality invariants. */ 405 @SuppressWarnings("serial") 406 public Set<Invariant> redundant_invs = new LinkedHashSet<>(0); 407 408 /** The canonical VarInfo for the equality. */ 409 @SuppressWarnings("serial") 410 public Set<VarInfo> redundant_invs_equality = new LinkedHashSet<>(0); 411 412 @SuppressWarnings("fields.uninitialized") // todo: initialization and helper methods 413 public PptTopLevel( 414 String name, 415 PptType type, 416 List<ParentRelation> parents, 417 EnumSet<PptFlags> flags, 418 VarInfo[] var_infos) { 419 super(var_infos); 420 421 this.name = name; 422 if (!name.contains(":::")) { 423 name += ":::" + type; 424 } 425 this.ppt_name = new PptName(name); 426 this.flags = flags; 427 this.type = type; 428 this.parent_relations = parents; 429 init_vars(); 430 } 431 432 /** Restore/Create interns when reading serialized object. */ 433 private void readObject(ObjectInputStream in) throws IOException, ClassNotFoundException { 434 in.defaultReadObject(); 435 if (name != null) { 436 try { 437 ReflectionPlume.setFinalField(this, "name", name.intern()); 438 } catch (Exception e) { 439 throw new Error("unexpected error setting name", e); 440 } 441 } 442 } 443 444 // Used by DaikonSimple, InvMap, and tests. Violates invariants. 445 @SuppressWarnings( 446 "nullness:fields.uninitialized") // violates invariants; also uses helper function 447 public PptTopLevel(String name, VarInfo[] var_infos) { 448 super(var_infos); 449 this.name = name; 450 ppt_name = new PptName(name); 451 init_vars(); 452 } 453 454 @RequiresNonNull("var_infos") 455 @EnsuresNonNull({"mbtracker", "views", "value_sets"}) 456 private void init_vars(@UnderInitialization(Ppt.class) PptTopLevel this) { 457 458 // debug_varinfo.log("initializing var_infos %s", Arrays.toString(var_infos)); 459 // debug_varinfo.tb(); 460 461 int val_idx = 0; 462 num_static_constant_vars = 0; 463 for (int i = 0; i < var_infos.length; i++) { 464 VarInfo vi = var_infos[i]; 465 vi.varinfo_index = i; 466 if (vi.is_static_constant) { 467 vi.value_index = -1; 468 num_static_constant_vars++; 469 } else { 470 vi.value_index = val_idx; 471 val_idx++; 472 } 473 } 474 for (VarInfo vi : var_infos) { 475 assert (vi.value_index == -1) || !vi.is_static_constant; 476 } 477 478 views = new LinkedHashMap<>(); 479 480 num_declvars = var_infos.length; 481 num_tracevars = val_idx; 482 num_orig_vars = 0; 483 assert num_static_constant_vars == num_declvars - num_tracevars; 484 assert num_tracevars == var_infos.length - num_static_constant_vars; 485 mbtracker = new ModBitTracker(num_tracevars); 486 /*NNC:@MonotonicNonNull*/ ValueSet[] new_value_sets = new ValueSet[num_tracevars]; 487 for (VarInfo vi : var_infos) { 488 int value_index = vi.value_index; 489 if (value_index == -1) { 490 continue; 491 } 492 assert new_value_sets[value_index] == null; 493 new_value_sets[value_index] = ValueSet.factory(vi); 494 } 495 for (ValueSet vs : new_value_sets) { 496 assert vs != null; 497 } 498 new_value_sets = castNonNullDeep(new_value_sets); // https://tinyurl.com/cfissue/986 499 value_sets = new_value_sets; 500 501 for (VarInfo vi : var_infos) { 502 // TODO: This should not be necessary, since initialization is now complete 503 @SuppressWarnings({"nullness:assignment"}) // initialization is now complete 504 @Initialized PptTopLevel initializedThis = this; 505 vi.ppt = initializedThis; 506 } 507 508 // Fix variable pointers so that they refer to the variables 509 // in this program point (they may have been cloned from a diff 510 // program point) 511 for (VarInfo vi : var_infos) { 512 vi.update_after_moving_to_new_ppt(); 513 } 514 515 // Relate the variables to one another 516 for (VarInfo vi : var_infos) { 517 vi.relate_var(); 518 } 519 } 520 521 // Appears to be used only in the memory monitor. 522 public int num_array_vars() { 523 int num_arrays = 0; 524 for (VarInfo vi : var_infos) { 525 if (vi.rep_type.isArray()) { 526 num_arrays++; 527 } 528 } 529 return num_arrays; 530 } 531 532 /** Iterate through each variable at this ppt. */ 533 public Iterator<VarInfo> var_info_iterator() { 534 return Arrays.<VarInfo>asList(var_infos).iterator(); 535 } 536 537 /** Returns the full name of the ppt. */ 538 @SideEffectFree 539 @Override 540 public String toString(@GuardSatisfied PptTopLevel this) { 541 return name(); 542 } 543 544 /** Trim the collections used here, in hopes of saving space. */ 545 @Override 546 public void trimToSize() { 547 super.trimToSize(); 548 if (splitters != null) { 549 splitters.trimToSize(); 550 } 551 } 552 553 /** The number of samples processed by this program point so far. */ 554 public int num_samples() { 555 return values_num_samples; 556 } 557 558 /** Return the number of samples where vi1 is present (not missing) */ 559 public int num_samples(VarInfo vi1) { 560 if (vi1.is_static_constant) { 561 return mbtracker.num_samples(); 562 } 563 BitSet b1 = mbtracker.get(vi1.value_index); 564 int num_slice_samples = b1.cardinality(); 565 return num_slice_samples; 566 } 567 568 /** Return the number of samples where vi1 and vi2 are both present (not missing). */ 569 public int num_samples(VarInfo vi1, VarInfo vi2) { 570 if (vi1.is_static_constant) { 571 return num_samples(vi2); 572 } 573 if (vi2.is_static_constant) { 574 return num_samples(vi1); 575 } 576 BitSet b1 = mbtracker.get(vi1.value_index); 577 BitSet b2 = mbtracker.get(vi2.value_index); 578 int num_slice_samples = CollectionsPlume.intersectionCardinality(b1, b2); 579 return num_slice_samples; 580 } 581 582 /** Return the number of samples where vi1, vi2, and vi3 are all present (not missing). */ 583 public int num_samples(VarInfo vi1, VarInfo vi2, VarInfo vi3) { 584 if (vi1.is_static_constant) { 585 return num_samples(vi2, vi3); 586 } 587 if (vi2.is_static_constant) { 588 return num_samples(vi1, vi3); 589 } 590 if (vi3.is_static_constant) { 591 return num_samples(vi1, vi2); 592 } 593 BitSet b1 = mbtracker.get(vi1.value_index); 594 BitSet b2 = mbtracker.get(vi2.value_index); 595 BitSet b3 = mbtracker.get(vi3.value_index); 596 int num_slice_samples = CollectionsPlume.intersectionCardinality(b1, b2, b3); 597 return num_slice_samples; 598 } 599 600 /** The number of distinct values that have been seen. */ 601 public int num_values(VarInfo vi1) { 602 if (vi1.is_static_constant) { 603 return 1; 604 } 605 ValueSet vs1 = value_sets[vi1.value_index]; 606 return vs1.size(); 607 } 608 609 /** 610 * An upper bound on the number of distinct pairs of values that have been seen. Note that there 611 * can't be more pairs of values than there are samples. This matters when there are very few 612 * samples due to one of the variables being missing. 613 */ 614 public int num_values(VarInfo vi1, VarInfo vi2) { 615 return Math.min(num_samples(vi1, vi2), num_values(vi1) * num_values(vi2)); 616 } 617 618 /** 619 * An upper bound on the number of distinct values over vi1, vi2, and vi3 that have been seen. 620 * Note that there can't be more pairs of values than there are samples. This matters when there 621 * are very few samples due to one of the variables being missing. 622 */ 623 public int num_values(VarInfo vi1, VarInfo vi2, VarInfo vi3) { 624 return Math.min( 625 num_samples(vi1, vi2, vi3), num_values(vi1) * num_values(vi2) * num_values(vi3)); 626 } 627 628 // Get the actual views from the HashMap 629 Collection<PptSlice> viewsAsCollection() { 630 return views.values(); 631 } 632 633 // Quick access to the number of views, since the views variable is private 634 public int numViews() { 635 return views.size(); 636 } 637 638 /////////////////////////////////////////////////////////////////////////// 639 /// Adding variables 640 /// 641 642 /** 643 * Appends the elements of vis to the var_infos array of this ppt. Method is not private so that 644 * FileIO can access it; should not be called by other classes. 645 * 646 * @param vis must not contain static constant VarInfos 647 */ 648 void addVarInfos(VarInfo[] vis) { 649 if (vis.length == 0) { 650 return; 651 } 652 int old_length = var_infos.length; 653 /*NNC:@MonotonicNonNull*/ VarInfo[] new_var_infos = new VarInfo[var_infos.length + vis.length]; 654 assert mbtracker.num_samples() == 0; 655 mbtracker = new ModBitTracker(mbtracker.num_vars() + vis.length); 656 System.arraycopy(var_infos, 0, new_var_infos, 0, old_length); 657 System.arraycopy(vis, 0, new_var_infos, old_length, vis.length); 658 new_var_infos = castNonNullDeep(new_var_infos); // https://tinyurl.com/cfissue/986 659 for (int i = old_length; i < new_var_infos.length; i++) { 660 VarInfo vi = new_var_infos[i]; 661 vi.varinfo_index = i; 662 vi.value_index = i - num_static_constant_vars; 663 vi.ppt = this; 664 } 665 var_infos = castNonNullDeep(new_var_infos); 666 int old_vs_length = value_sets.length; 667 /*NNC:@MonotonicNonNull*/ ValueSet[] new_value_sets = new ValueSet[old_vs_length + vis.length]; 668 System.arraycopy(value_sets, 0, new_value_sets, 0, old_vs_length); 669 for (int i = 0; i < vis.length; i++) { 670 new_value_sets[old_vs_length + i] = ValueSet.factory(vis[i]); 671 } 672 new_value_sets = castNonNullDeep(new_value_sets); // https://tinyurl.com/cfissue/986 673 value_sets = new_value_sets; 674 675 // Relate the variables to one another 676 for (VarInfo vi : vis) { 677 vi.relate_var(); 678 } 679 } 680 681 /////////////////////////////////////////////////////////////////////////// 682 /// Derived variables 683 /// 684 685 // This is here because I think it doesn't make sense to derive except 686 // from a PptTopLevel (and possibly a PptConditional?). Perhaps move it 687 // to another class later. 688 689 public static boolean worthDerivingFrom(VarInfo vi) { 690 691 // This prevents derivation from ever occurring on 692 // derived variables. Ought to put this under the 693 // control of the individual Derivation objects. 694 695 // System.out.println("worthDerivingFrom(" + vi.name + "): " 696 // + "derivedDepth=" + vi.derivedDepth() 697 // + ", isCanonical=" + vi.isCanonical() 698 // + ", canBeMissing=" + vi.canBeMissing); 699 return (vi.derivedDepth() < 2); 700 701 // Should add this (back) in: 702 // && !vi.always_missing() 703 // && !vi.always_equal_to_null(); 704 705 // Testing for being canonical is going to be a touch tricky when we 706 // integrate derivation and inference, because when something becomes 707 // non-canonical we'll have to go back and derive from it, etc. It's 708 // almost as if that is a new variable appearing. But it did appear in 709 // the list until it was found to be equal to another and removed from 710 // the list! I need to decide whether the time savings of not 711 // processing the non-canonical variables are worth the time and 712 // complexity of making variables non-canonical and possibly canonical 713 // again. 714 715 } 716 717 // To verify that these are all the factories of interest, do 718 // cd ~/research/invariants/daikon/derive; search -i -n 'extends.*derivationfactory' 719 720 transient UnaryDerivationFactory[] unaryDerivations = 721 new UnaryDerivationFactory[] { 722 new StringLengthFactory(), 723 new SequenceLengthFactory(), 724 new SequenceInitialFactory(), 725 new SequenceMinMaxSumFactory(), 726 new SequenceInitialFactoryFloat(), 727 }; 728 729 transient BinaryDerivationFactory[] binaryDerivations = 730 new BinaryDerivationFactory[] { 731 // subscript 732 new SequenceScalarSubscriptFactory(), 733 new SequenceFloatSubscriptFactory(), 734 new SequenceStringSubscriptFactory(), 735 // intersection 736 new SequenceScalarIntersectionFactory(), 737 new SequenceFloatIntersectionFactory(), 738 new SequenceStringIntersectionFactory(), 739 // union 740 new SequenceScalarUnionFactory(), 741 new SequenceFloatUnionFactory(), 742 new SequenceStringUnionFactory(), 743 // other 744 new SequencesConcatFactory(), 745 new SequencesJoinFactory(), 746 new SequencesPredicateFactory(), 747 }; 748 749 transient TernaryDerivationFactory[] ternaryDerivations = 750 new TernaryDerivationFactory[] { 751 new SequenceScalarArbitrarySubsequenceFactory(), 752 new SequenceStringArbitrarySubsequenceFactory(), 753 new SequenceFloatArbitrarySubsequenceFactory(), 754 }; 755 756 /** 757 * This routine creates derivations for one "pass"; that is, it adds some set of derived 758 * variables, according to the functions that are passed in. All the results involve at least one 759 * VarInfo object at an index i such that vi_index_min ≤ i < vi_index_limit (and possibly 760 * other VarInfos outside that range). 761 */ 762 private Derivation[] derive(int vi_index_min, int vi_index_limit) { 763 boolean debug_bin_possible = false; 764 765 UnaryDerivationFactory[] unary = unaryDerivations; 766 BinaryDerivationFactory[] binary = binaryDerivations; 767 TernaryDerivationFactory[] ternary = ternaryDerivations; 768 769 // optimize track logging, otherwise it really takes a lot of time 770 if (Debug.logOn()) { 771 for (int di = 0; di < binary.length; di++) { 772 BinaryDerivationFactory d = binary[di]; 773 if (Debug.class_match(d.getClass())) { 774 debug_bin_possible = true; 775 } 776 } 777 } 778 779 if (Global.debugDerive.isLoggable(Level.FINE)) { 780 Global.debugDerive.fine("Deriving one pass for ppt " + this.name); 781 Global.debugDerive.fine( 782 "vi_index_min=" 783 + vi_index_min 784 + ", vi_index_limit=" 785 + vi_index_limit 786 + ", unary.length=" 787 + unary.length 788 + ", binary.length=" 789 + binary.length 790 + ", ternary.length=" 791 + ternary.length); 792 } 793 794 Collection<Derivation> result = new ArrayList<Derivation>(); 795 796 Daikon.progress = "Creating derived variables for: " + ppt_name.toString() + " (unary)"; 797 for (int i = vi_index_min; i < vi_index_limit; i++) { 798 VarInfo vi = var_infos[i]; 799 if (Global.debugDerive.isLoggable(Level.FINE)) { 800 Global.debugDerive.fine("Unary: trying to derive from " + vi.name()); 801 } 802 if (!worthDerivingFrom(vi)) { 803 if (Global.debugDerive.isLoggable(Level.FINE)) { 804 Global.debugDerive.fine("Unary: not worth deriving from " + vi.name()); 805 } 806 continue; 807 } 808 for (int di = 0; di < unary.length; di++) { 809 UnaryDerivationFactory udf = unary[di]; 810 UnaryDerivation[] uderivs = udf.instantiate(vi); 811 if (uderivs != null) { 812 for (int udi = 0; udi < uderivs.length; udi++) { 813 UnaryDerivation uderiv = uderivs[udi]; 814 // System.out.printf("processing uderiv %s %s%n", uderiv, 815 // uderiv.getVarInfo()); 816 if (!FileIO.var_included(uderiv.getVarInfo().name())) { 817 continue; 818 } 819 result.add(uderiv); 820 } 821 } 822 } 823 } 824 825 // I want to get all pairs of variables such that at least one of the 826 // variables is under consideration, but I want to generate each such 827 // pair only once. This probably isn't the most efficient technique, 828 // but it's probably adequate and is not excessively complicated or 829 // excessively slow. 830 for (int i1 = 0; i1 < var_infos.length; i1++) { 831 VarInfo vi1 = var_infos[i1]; 832 if (!worthDerivingFrom(vi1)) { 833 if (Global.debugDerive.isLoggable(Level.FINE)) { 834 Global.debugDerive.fine("Binary first VarInfo: not worth deriving from " + vi1.name()); 835 } 836 continue; 837 } 838 // This guarantees that at least one of the variables is under 839 // consideration. 840 // target1 indicates whether the first variable is under consideration. 841 boolean target1 = (i1 >= vi_index_min) && (i1 < vi_index_limit); 842 int i2_min, i2_limit; 843 if (target1) { 844 i2_min = i1 + 1; 845 i2_limit = var_infos.length; 846 } else { 847 i2_min = Math.max(i1 + 1, vi_index_min); 848 i2_limit = vi_index_limit; 849 } 850 // if (Global.debugDerive.isLoggable(Level.FINE)) 851 // Global.debugDerive.fine ("i1=" + i1 852 // + ", i2_min=" + i2_min 853 // + ", i2_limit=" + i2_limit); 854 Daikon.progress = 855 "Creating derived variables for: " 856 + ppt_name.toString() 857 + " (binary, " 858 + vi1.name() 859 + ")"; 860 for (int i2 = i2_min; i2 < i2_limit; i2++) { 861 VarInfo vi2 = var_infos[i2]; 862 if (!worthDerivingFrom(vi2)) { 863 if (Global.debugDerive.isLoggable(Level.FINE)) { 864 Global.debugDerive.fine( 865 "Binary: not worth deriving from (" + vi1.name() + "," + vi2.name() + ")"); 866 } 867 continue; 868 } 869 for (int di = 0; di < binary.length; di++) { 870 BinaryDerivationFactory d = binary[di]; 871 if (debug_bin_possible && Debug.logOn()) { 872 Debug.log(d.getClass(), vi1.ppt, Debug.vis(vi1, vi2), "Trying Binary Derivation "); 873 } 874 BinaryDerivation[] bderivs = d.instantiate(vi1, vi2); 875 if (bderivs != null) { 876 for (int bdi = 0; bdi < bderivs.length; bdi++) { 877 BinaryDerivation bderiv = bderivs[bdi]; 878 if (!FileIO.var_included(bderiv.getVarInfo().name())) { 879 continue; 880 } 881 result.add(bderiv); 882 if (Debug.logOn()) { 883 Debug.log( 884 d.getClass(), 885 vi1.ppt, 886 Debug.vis(vi1, vi2), 887 "Created Binary Derivation " + bderiv.getVarInfo().name()); 888 } 889 } 890 } 891 } 892 } 893 } 894 895 // Ternary derivations follow the same pattern, one level deeper. 896 for (int i1 = 0; i1 < var_infos.length; i1++) { 897 VarInfo vi1 = var_infos[i1]; 898 if (vi1.isDerived()) { 899 if (Global.debugDerive.isLoggable(Level.FINE)) { 900 Global.debugDerive.fine("Ternary first VarInfo: not worth deriving from " + vi1.name()); 901 } 902 continue; 903 } 904 // This guarantees that at least one of the variables is under 905 // consideration. 906 // target1 indicates whether the first variable is under consideration. 907 boolean target1 = (i1 >= vi_index_min) && (i1 < vi_index_limit); 908 int i2_min, i2_limit; 909 if (target1) { 910 i2_min = i1 + 1; 911 i2_limit = var_infos.length; 912 } else { 913 i2_min = Math.max(i1 + 1, vi_index_min); 914 i2_limit = vi_index_limit; 915 } 916 // if (Global.debugDerive.isLoggable(Level.FINE)) 917 // Global.debugDerive.fine ("i1=" + i1 918 // + ", i2_min=" + i2_min 919 // + ", i2_limit=" + i2_limit); 920 Daikon.progress = 921 "Creating derived variables for: " 922 + ppt_name.toString() 923 + " (ternary, " 924 + vi1.name() 925 + ")"; 926 for (int i2 = i2_min; i2 < i2_limit; i2++) { 927 VarInfo vi2 = var_infos[i2]; 928 if (vi2.isDerived() 929 || !TernaryDerivationFactory.checkType(vi1, vi2) 930 || !TernaryDerivationFactory.checkComparability(vi1, vi2)) { 931 if (Global.debugDerive.isLoggable(Level.FINE)) { 932 Global.debugDerive.fine( 933 "Ternary 2nd: not worth deriving from (" + vi1.name() + "," + vi2.name() + ")"); 934 } 935 continue; 936 } 937 boolean target2 = (i2 >= vi_index_min) && (i2 < vi_index_limit); 938 int i3_min, i3_limit; 939 if (target1 || target2) { 940 i3_min = i2 + 1; 941 i3_limit = var_infos.length; 942 } else { 943 i3_min = Math.max(i2 + 1, vi_index_min); 944 i3_limit = vi_index_limit; 945 } 946 for (int i3 = i3_min; i3 < i3_limit; i3++) { 947 VarInfo vi3 = var_infos[i3]; 948 if (vi3.isDerived()) { 949 if (Global.debugDerive.isLoggable(Level.FINE)) { 950 Global.debugDerive.fine( 951 "Ternary 3rd: not worth deriving from (" 952 + vi1.name() 953 + "," 954 + vi2.name() 955 + ")" 956 + vi3.name() 957 + ")"); 958 } 959 continue; 960 } 961 for (int di = 0; di < ternary.length; di++) { 962 TernaryDerivationFactory d = ternary[di]; 963 TernaryDerivation[] tderivs = d.instantiate(vi1, vi2, vi3); 964 if (tderivs != null) { 965 for (int tdi = 0; tdi < tderivs.length; tdi++) { 966 TernaryDerivation tderiv = tderivs[tdi]; 967 if (!FileIO.var_included(tderiv.getVarInfo().name())) { 968 continue; 969 } 970 result.add(tderiv); 971 } 972 } else { 973 if (Global.debugDerive.isLoggable(Level.FINE)) { 974 Global.debugDerive.fine( 975 "Ternary instantiated but not used: " 976 + vi1.name() 977 + " " 978 + vi2.name() 979 + " " 980 + vi3.name() 981 + " "); 982 } 983 } 984 } 985 } 986 } 987 } 988 989 if (Global.debugDerive.isLoggable(Level.FINE)) { 990 Global.debugDerive.fine( 991 "Number of derived variables at program point " + this.name + ": " + result.size()); 992 String derived_vars = "Derived:"; 993 for (Iterator<Derivation> itor = result.iterator(); itor.hasNext(); ) { 994 derived_vars += " " + itor.next().getVarInfo().name(); 995 } 996 Global.debugDerive.fine(derived_vars); 997 } 998 Derivation[] result_array = result.toArray(new Derivation[0]); 999 return result_array; 1000 } 1001 1002 /** 1003 * Add the sample to the equality sets, dynamic constants, and invariants at this program point. 1004 * This version is specific to the bottom up processing mechanism. 1005 * 1006 * <p>This routine also instantiates slices/invariants on the first call for the ppt. 1007 * 1008 * @param vt the set of values for this to see 1009 * @param count the number of samples that vt represents 1010 * @return the set of all invariants weakened or falsified by this sample 1011 */ 1012 @RequiresNonNull({ 1013 "daikon.suppress.NIS.suppressor_map", 1014 "daikon.suppress.NIS.suppressor_map_suppression_count", 1015 "daikon.suppress.NIS.all_suppressions", 1016 "daikon.suppress.NIS.suppressor_proto_invs" 1017 }) 1018 public @Nullable Set<Invariant> add_bottom_up(ValueTuple vt, int count) { 1019 // Doable, but commented out for efficiency 1020 // repCheck(); 1021 1022 // Debug print some (program specific) variables 1023 if (debug.isLoggable(Level.FINE)) { 1024 System.out.println("Processing samples at " + name()); 1025 if (vt.size() > 0) { 1026 StringBuilder out = new StringBuilder(); 1027 for (int i = 0; i < vt.size(); i++) { 1028 VarInfo vi = var_infos[i]; 1029 if (!vi.name().startsWith("xx")) { 1030 continue; 1031 } 1032 out.append(String.format("%s %b %s ", vi.name(), vt.isMissing(i), vt.getValue(vi))); 1033 } 1034 System.out.printf("%s vals: %s%n", name(), out); 1035 } 1036 } 1037 1038 assert vt.size() == var_infos.length - num_static_constant_vars : name; 1039 1040 // stop early if there are no vars 1041 if (var_infos.length == 0) { 1042 assert vt.size() == 0; 1043 return null; 1044 } 1045 1046 // If there are conditional program points, add the sample there instead 1047 if (has_splitters()) { 1048 assert splitters != null; // guaranteed by call to has_splitters 1049 for (PptSplitter ppt_split : splitters) { 1050 ppt_split.add_bottom_up(vt, count); 1051 } 1052 if (Daikon.use_dataflow_hierarchy) { 1053 return null; 1054 } 1055 } 1056 1057 // If we are not using the hierarchy and this is a numbered exit, also 1058 // apply these values to the combined exit 1059 if (!Daikon.use_dataflow_hierarchy) { 1060 // System.out.println ("ppt_name = " + ppt_name); 1061 if (!(this instanceof PptConditional) && ppt_name.isNumberedExitPoint()) { 1062 PptTopLevel parent = Daikon.all_ppts.get(ppt_name.makeExit()); 1063 if (parent != null) { 1064 // System.out.println ("parent is " + parent.name()); 1065 parent.get_missingOutOfBounds(this, vt); 1066 parent.add_bottom_up(vt, count); 1067 } 1068 } 1069 } 1070 1071 if (debugNISStats.isLoggable(Level.FINE)) { 1072 NIS.clear_stats(); 1073 } 1074 1075 // Set of invariants weakened by this sample 1076 Set<Invariant> weakened_invs = new LinkedHashSet<>(); 1077 1078 // Instantiate slices and invariants if this is the first sample 1079 if (values_num_samples == 0) { 1080 debugFlow.fine(" Instantiating views for the first time"); 1081 if (!DynamicConstants.dkconfig_use_dynamic_constant_optimization) { 1082 instantiate_views_and_invariants(); 1083 } 1084 } 1085 1086 // Add the samples to all of the equality sets, breaking sets as required 1087 if (Daikon.use_equality_optimization) { 1088 assert equality_view != null 1089 : "@AssumeAssertion(nullness): dependent: non-null if use_equality_optimization==true"; 1090 weakened_invs.addAll(equality_view.add(vt, count)); 1091 } 1092 1093 // Add samples to constants, adding new invariants as required 1094 if (DynamicConstants.dkconfig_use_dynamic_constant_optimization) { 1095 if (constants == null) { 1096 constants = new DynamicConstants(this); 1097 } 1098 constants.add(vt, count); 1099 } 1100 1101 instantiated_inv_cnt = invariant_cnt(); 1102 instantiated_slice_cnt = views.size(); 1103 1104 if (debugInstantiate.isLoggable(Level.FINE) && values_num_samples == 0) { 1105 int slice1_cnt = 0; 1106 int slice2_cnt = 0; 1107 int slice3_cnt = 0; 1108 for (PptSlice slice : views_iterable()) { 1109 if (slice instanceof PptSlice1) { 1110 slice1_cnt++; 1111 } else if (slice instanceof PptSlice2) { 1112 slice2_cnt++; 1113 } else if (slice instanceof PptSlice3) { 1114 slice3_cnt++; 1115 } 1116 } 1117 System.out.println("ppt " + name()); 1118 debugInstantiate.fine("slice1 (" + slice1_cnt + ") slices"); 1119 for (PptSlice slice : views_iterable()) { 1120 if (slice instanceof PptSlice1) { 1121 debugInstantiate.fine( 1122 " : " 1123 + slice.var_infos[0].name() 1124 + ": " 1125 + slice.var_infos[0].file_rep_type 1126 + ": " 1127 + slice.var_infos[0].rep_type 1128 + ": " 1129 + slice.var_infos[0].equalitySet.shortString()); 1130 } 1131 if (debugStdout) { 1132 for (Invariant inv : slice.invs) { 1133 debugInstantiate.fine("-- invariant " + inv.format()); 1134 } 1135 } 1136 } 1137 debugInstantiate.fine("slice2 (" + slice2_cnt + ") slices"); 1138 for (PptSlice slice : views_iterable()) { 1139 if (slice instanceof PptSlice2) { 1140 debugInstantiate.fine( 1141 " : " + slice.var_infos[0].name() + " : " + slice.var_infos[1].name()); 1142 } 1143 } 1144 debugInstantiate.fine("slice3 (" + slice3_cnt + ") slices"); 1145 for (PptSlice slice : views_iterable()) { 1146 if (slice instanceof PptSlice3) { 1147 debugInstantiate.fine( 1148 " : " 1149 + slice.var_infos[0].name() 1150 + " : " 1151 + slice.var_infos[1].name() 1152 + " : " 1153 + slice.var_infos[2].name()); 1154 } 1155 } 1156 } 1157 1158 values_num_samples += count; 1159 1160 vt.checkRep(); // temporary, for debugging 1161 1162 // Keep track of what variables are present on this sample 1163 mbtracker.add(vt, count); 1164 1165 vt.checkRep(); // temporary, for debugging 1166 1167 // Keep track of the distinct values seen 1168 for (int i = 0; i < vt.vals.length; i++) { 1169 if (!vt.isMissing(i)) { 1170 Object val = vt.vals[i]; 1171 ValueSet vs = value_sets[i]; 1172 if (val == null) { // temporary, for debugging 1173 System.out.printf("Null value at index %s in ValueTuple %s, ValueSet=%s%n", i, vt, vs); 1174 } 1175 vs.add(val); 1176 } 1177 } 1178 1179 // Add the sample to each slice 1180 for (PptSlice slice : views_iterable()) { 1181 if (slice.invs.size() == 0) { 1182 continue; 1183 } 1184 weakened_invs.addAll(slice.add(vt, count)); 1185 } 1186 1187 // Create any newly unsuppressed invariants 1188 NIS.process_falsified_invs(this, vt); 1189 1190 // NIS.newly_falsified is a list of invariants that are falsified by 1191 // the current sample when using the falsified method of processing 1192 // suppressions. The newly falsified invariants are added back to 1193 // the slices so that they can be processed. Thus, the falsified method 1194 // is used iteratively, since these newly falsified invariants may 1195 // unsuppress new invariants. In the antecedents method, the problem 1196 // does not exist, because of the way that recursive suppressions are 1197 // ordered. This loop should be executed at least once, regardless of 1198 // the algorithm for processing suppressions, hence the do loop. For, 1199 // the antecedents method, the loop is executed only once because 1200 // the NIS.newly_falsified list will be empty. 1201 1202 do { 1203 // Remove any falsified invariants. Make a copy of the original slices 1204 // since NISuppressions will add new slices/invariants as others are 1205 // falsified. 1206 PptSlice[] slices = views.values().toArray(new @Nullable PptSlice[0]); 1207 for (int i = 0; i < slices.length; i++) { 1208 slices[i].remove_falsified(); 1209 } 1210 1211 // Apply the sample to any invariants created by non-instantiating 1212 // suppressions. This must happen before we remove slices without 1213 // invariants below. 1214 NIS.apply_samples(vt, count); 1215 first_pass_with_sample = false; 1216 } while (NIS.newly_falsified.size() != 0); 1217 1218 first_pass_with_sample = true; 1219 1220 // Remove slices from the list if all of their invariants have died. 1221 // (Removal requires use of old-style for loop and Iterator.) 1222 for (Iterator<PptSlice> itor = views_iterator(); itor.hasNext(); ) { 1223 PptSlice view = itor.next(); 1224 if (view.invs.size() == 0) { 1225 itor.remove(); 1226 if (Global.debugInfer.isLoggable(Level.FINE)) { 1227 Global.debugInfer.fine("add(ValueTulple,int): slice died: " + name() + view.varNames()); 1228 } 1229 } 1230 } 1231 1232 if (debugNISStats.isLoggable(Level.FINE)) { 1233 NIS.dump_stats(debugNISStats, this); 1234 } 1235 1236 // At this point, no invariant should exist that is suppressed 1237 if (Debug.dkconfig_internal_check) { 1238 for (PptSlice slice : views_iterable()) { 1239 for (Invariant inv : slice.invs) { 1240 if (inv.is_ni_suppressed()) { 1241 NISuppressionSet ss = inv.get_ni_suppressions(); 1242 assert ss != null; // guaranteed by call to is_ni_suppressed 1243 ss.suppressed(inv.ppt); 1244 System.out.printf( 1245 "suppressed: %s by suppression set %s in ppt %s", inv.format(), ss, slice); 1246 throw new Error(); 1247 } 1248 } 1249 } 1250 } 1251 1252 return weakened_invs; 1253 } 1254 1255 /** 1256 * Adds a sample to each invariant in the list. Returns the list of weakened invariants. This 1257 * should only be called when the sample has already been added to the slice containing each 1258 * invariant. Otherwise the statistics kept in the slice will be incorrect. 1259 * 1260 * @param inv_list the invariants to add the sample to 1261 * @param vt the sample 1262 * @param count how many instances of the sample to add 1263 * @return the invariants that were weakened 1264 */ 1265 public List<Invariant> inv_add(List<Invariant> inv_list, ValueTuple vt, int count) { 1266 1267 // // Slices containing these invariants 1268 // Set<PptSlice> slices = new LinkedHashSet<>(); 1269 1270 // List of invariants weakened by this sample 1271 List<Invariant> weakened_invs = new ArrayList<>(); 1272 1273 // Loop through each invariant 1274 inv_loop: 1275 for (Invariant inv : inv_list) { 1276 if (Debug.logDetail()) { 1277 inv.log("Processing in inv_add"); 1278 } 1279 1280 // Skip falsified invariants (shouldn't happen) 1281 if (inv.is_false()) { 1282 continue; 1283 } 1284 1285 // Skip any invariants with a missing variable 1286 for (int j = 0; j < inv.ppt.var_infos.length; j++) { 1287 if (inv.ppt.var_infos[j].isMissing(vt)) { 1288 continue inv_loop; 1289 } 1290 } 1291 1292 // // Add the slice containing this invariant to the set of slices 1293 // slices.add(inv.ppt); 1294 1295 // Get the values and add them to the invariant. 1296 InvariantStatus result = inv.add_sample(vt, count); 1297 1298 if (result == InvariantStatus.FALSIFIED) { 1299 inv.falsify(); 1300 weakened_invs.add(inv); 1301 } else if (result == InvariantStatus.WEAKENED) { 1302 weakened_invs.add(inv); 1303 } 1304 } 1305 1306 return weakened_invs; 1307 } 1308 1309 /** 1310 * Gets any missing out of bounds variables from the specified ppt and applies them to the 1311 * matching variable in this ppt if the variable is MISSING_NONSENSICAL. The goal is to set the 1312 * missing_array_bounds flag only if it was missing in ppt on THIS sample. 1313 * 1314 * <p>This could fail if missing_array_bounds was set on a previous sample and the 1315 * MISSING_NONSENSICAL flag is set for a different reason on this sample. This could happen with 1316 * an array in an object. 1317 * 1318 * <p>This implementation is also not particularly efficient and the variables must match exactly. 1319 * 1320 * <p>Missing out of bounds really needs to be implemented as a separate flag in the missing bits. 1321 * That would clear up all of this mess. 1322 */ 1323 public void get_missingOutOfBounds(PptTopLevel ppt, ValueTuple vt) { 1324 1325 for (int ii = 0; ii < ppt.var_infos.length; ii++) { 1326 if (ppt.var_infos[ii].missingOutOfBounds()) { 1327 int mod = vt.getModified(ppt.var_infos[ii]); 1328 if (this.var_infos[ii].derived == null) { 1329 System.out.printf( 1330 "ppt %s, ii %s, ppt.var_infos[ii] %s, this.var_infos[ii] %s%n", 1331 ppt, ii, ppt.var_infos[ii], this.var_infos[ii]); 1332 } 1333 assert this.var_infos[ii].derived != null : "@AssumeAssertion(nullness)"; 1334 if (mod == ValueTuple.MISSING_NONSENSICAL) { 1335 this.var_infos[ii].derived.missing_array_bounds = true; 1336 } 1337 } 1338 } 1339 } 1340 1341 /** Returns whether or not the specified variable is dynamically constant. */ 1342 @SuppressWarnings("contracts.conditional.postcondition") // Checker Framework bug 1343 @EnsuresNonNullIf(result = true, expression = "constants") 1344 @Pure 1345 public boolean is_constant(VarInfo v) { 1346 return (constants != null) && constants.is_constant(v); 1347 } 1348 1349 /** 1350 * Returns whether or not the specified variable is currently dynamically constant, or was a 1351 * dynamic constant at the beginning of constant processing. 1352 */ 1353 @SuppressWarnings("contracts.conditional.postcondition") // Checker Framework bug 1354 @EnsuresNonNullIf(result = true, expression = "constants") 1355 @Pure 1356 public boolean is_prev_constant(VarInfo v) { 1357 return (constants != null) && constants.is_prev_constant(v); 1358 } 1359 1360 /** Returns whether or not the specified variable has been missing for all samples seen so far. */ 1361 @SuppressWarnings("contracts.conditional.postcondition") // Checker Framework bug 1362 @EnsuresNonNullIf(result = true, expression = "constants") 1363 @Pure 1364 public boolean is_missing(VarInfo v) { 1365 return (constants != null) && constants.is_missing(v); 1366 } 1367 1368 /** 1369 * returns whether the specified variable is currently missing OR was missing at the beginning of 1370 * constants processing. 1371 */ 1372 @SuppressWarnings("contracts.conditional.postcondition") // Checker Framework bug 1373 @EnsuresNonNullIf(result = true, expression = "constants") 1374 @Pure 1375 public boolean is_prev_missing(VarInfo v) { 1376 return (constants != null) && constants.is_prev_missing(v); 1377 } 1378 1379 /** Returns the number of true invariants at this ppt. */ 1380 public int invariant_cnt() { 1381 1382 int inv_cnt = 0; 1383 1384 for (Iterator<PptSlice> j = views_iterator(); j.hasNext(); ) { 1385 PptSlice slice = j.next(); 1386 inv_cnt += slice.invs.size(); 1387 } 1388 return inv_cnt; 1389 } 1390 1391 /** Returns the number of slices that contain one or more constants. */ 1392 public int const_slice_cnt() { 1393 1394 int const_cnt = 0; 1395 1396 for (Iterator<PptSlice> j = views_iterator(); j.hasNext(); ) { 1397 PptSlice slice = j.next(); 1398 for (int i = 0; i < slice.arity(); i++) { 1399 if (is_constant(slice.var_infos[i])) { 1400 const_cnt++; 1401 break; 1402 } 1403 } 1404 } 1405 return const_cnt; 1406 } 1407 1408 /** Returns the number of invariants that contain one or more constants. */ 1409 public int const_inv_cnt() { 1410 1411 int const_cnt = 0; 1412 1413 for (Iterator<PptSlice> j = views_iterator(); j.hasNext(); ) { 1414 PptSlice slice = j.next(); 1415 for (int i = 0; i < slice.arity(); i++) { 1416 if (is_constant(slice.var_infos[i])) { 1417 const_cnt += slice.invs.size(); 1418 break; 1419 } 1420 } 1421 } 1422 return const_cnt; 1423 } 1424 1425 static class Cnt { 1426 public int cnt = 0; 1427 } 1428 1429 /** Debug print to the specified logger information about each invariant at this ppt. */ 1430 @RequiresNonNull("daikon.suppress.NIS.suppressor_map") 1431 public void debug_invs(Logger log) { 1432 1433 for (Iterator<PptSlice> i = views_iterator(); i.hasNext(); ) { 1434 PptSlice slice = i.next(); 1435 log.fine("Slice: " + slice); 1436 for (Invariant inv : slice.invs) { 1437 log.fine( 1438 "-- " 1439 + inv.format() 1440 + (NIS.is_suppressor(inv.getClass()) ? "[suppressor]" : "") 1441 + (inv.is_false() ? " [falsified]" : " ")); 1442 } 1443 } 1444 } 1445 1446 /** 1447 * Debug print to the specified logger information about each variable in this ppt. Currently only 1448 * prints integer and float information using the bound invariants. 1449 */ 1450 public void debug_unary_info(Logger log) { 1451 1452 for (Iterator<PptSlice> j = views_iterator(); j.hasNext(); ) { 1453 PptSlice slice = j.next(); 1454 if (!(slice instanceof PptSlice1)) { 1455 continue; 1456 } 1457 LowerBound lb = null; 1458 LowerBoundFloat lbf = null; 1459 UpperBound ub = null; 1460 UpperBoundFloat ubf = null; 1461 for (Invariant inv : slice.invs) { 1462 if (inv instanceof LowerBound) { 1463 lb = (LowerBound) inv; 1464 } else if (inv instanceof LowerBoundFloat) { 1465 lbf = (LowerBoundFloat) inv; 1466 } else if (inv instanceof UpperBound) { 1467 ub = (UpperBound) inv; 1468 } else if (inv instanceof UpperBoundFloat) { 1469 ubf = (UpperBoundFloat) inv; 1470 } 1471 } 1472 if ((lb != null) && (ub != null)) { 1473 log.fine(lb.min() + " <= " + slice.var_infos[0].name() + " <= " + ub.max()); 1474 } else if ((lbf != null) && (ubf != null)) { 1475 log.fine(lbf.min() + " <= " + slice.var_infos[0].name() + " <= " + ubf.max()); 1476 } else if ((lb != null) || (ub != null) || (lbf != null) || (ubf != null)) { 1477 throw new Error("This can't happen"); 1478 } 1479 } 1480 } 1481 1482 /** 1483 * Returns how many invariants there are of each invariant class. The map is from the invariant 1484 * class to an integer cnt of the number of that class. 1485 */ 1486 public Map<Class<? extends Invariant>, Cnt> invariant_cnt_by_class() { 1487 1488 Map<Class<? extends Invariant>, Cnt> inv_map = new LinkedHashMap<>(); 1489 1490 for (Iterator<PptSlice> j = views_iterator(); j.hasNext(); ) { 1491 PptSlice slice = j.next(); 1492 for (Invariant inv : slice.invs) { 1493 Cnt cnt = inv_map.computeIfAbsent(inv.getClass(), __ -> new Cnt()); 1494 cnt.cnt++; 1495 } 1496 } 1497 1498 return inv_map; 1499 } 1500 1501 /** Returns the number of slices at this ppt. */ 1502 public int slice_cnt() { 1503 return views.size(); 1504 } 1505 1506 /** Create all the derived variables. */ 1507 public void create_derived_variables() { 1508 if (debug.isLoggable(Level.FINE)) { 1509 debug.fine("create_derived_variables for " + name()); 1510 } 1511 1512 // Make ALL of the derived variables. The loop terminates 1513 // because derive() stops creating derived variables after some 1514 // depth. Within the loop, [lower..upper) need deriving from. 1515 int lower = 0; 1516 int upper = var_infos.length; 1517 while (lower < upper) { 1518 Derivation[] ders = derive(lower, upper); 1519 lower = upper; 1520 upper += ders.length; 1521 1522 List<VarInfo> vis_list = new ArrayList<>(ders.length); 1523 for (Derivation der : ders) { 1524 vis_list.add(der.getVarInfo()); 1525 } 1526 VarInfo[] vis = vis_list.toArray(new VarInfo[0]); 1527 if (Global.debugDerive.isLoggable(Level.FINE)) { 1528 for (int i = 0; i < ders.length; i++) { 1529 Global.debugDerive.fine("Derived " + vis[i].name()); 1530 } 1531 } 1532 1533 // Using addDerivedVariables(derivations) would add data too 1534 addVarInfos(vis); 1535 } 1536 assert lower == upper; 1537 assert upper == var_infos.length; 1538 1539 if (debug.isLoggable(Level.FINE)) { 1540 debug.fine("Done with create_derived_variables, " + var_infos.length + " vars"); 1541 // System.out.println(Arrays.toString(var_infos)); 1542 } 1543 } 1544 1545 /////////////////////////////////////////////////////////////////////////// 1546 /// Creating invariants 1547 /// 1548 1549 // I can't decide which loop it's more efficient to make the inner loop: 1550 // the loop over samples or the loop over slices. 1551 1552 /** Add the specified slices to this ppt. */ 1553 public void addViews(List<PptSlice> slices_vector) { 1554 if (slices_vector.isEmpty()) { 1555 return; 1556 } 1557 1558 // Don't modify the actual parameter 1559 @SuppressWarnings("unchecked") 1560 List<PptSlice> slices_vector_copy = new ArrayList<>(slices_vector); 1561 1562 // This might be a brand-new Slice, and instantiate_invariants for this 1563 // pass might not have come up with any invariants. 1564 for (Iterator<PptSlice> itor = slices_vector_copy.iterator(); itor.hasNext(); ) { 1565 PptSlice slice = itor.next(); 1566 if (slice.invs.size() == 0) { 1567 // removes the element from slices_vector_copy 1568 itor.remove(); 1569 } 1570 } 1571 1572 addSlices(slices_vector_copy); 1573 } 1574 1575 /** Add a collection of slices to the views of a PptTopLevel. */ 1576 private void addSlices(Collection<PptSlice> slices) { 1577 for (Iterator<PptSlice> i = slices.iterator(); i.hasNext(); ) { 1578 addSlice(i.next()); 1579 } 1580 } 1581 1582 /** 1583 * Given an array of VarInfos, return a List representing that array, to be used as an index in 1584 * the views hashtable. 1585 */ 1586 private List<Integer> sliceIndex(VarInfo[] vis) { 1587 List<Integer> result = new ArrayList<>(vis.length); 1588 for (int i = 0; i < vis.length; i++) { 1589 result.add(vis[i].varinfo_index); 1590 } 1591 return result; 1592 } 1593 1594 /** Add a single slice to the views variable. */ 1595 public void addSlice(PptSlice slice) { 1596 1597 // System.out.printf("Adding slice %s to ppt %s%n", slice, this); 1598 1599 // Make sure the slice doesn't already exist (should never happen) 1600 PptSlice cslice = findSlice(slice.var_infos); 1601 if (cslice != null) { 1602 System.out.println("Trying to add slice " + slice); 1603 System.out.println("but, slice " + cslice + " already exists"); 1604 for (Invariant inv : cslice.invs) { 1605 System.out.println(" -- inv " + inv); 1606 } 1607 throw new Error(); 1608 } 1609 1610 // Make sure that the slice is valid (they are not always valid) 1611 // slice.repCheck(); 1612 1613 views.put(sliceIndex(slice.var_infos), slice); 1614 if (Debug.logOn()) { 1615 slice.log("Adding slice"); 1616 } 1617 } 1618 1619 /** Remove a slice from this PptTopLevel. */ 1620 public void removeSlice(PptSlice slice) { 1621 Object o = views.remove(sliceIndex(slice.var_infos)); 1622 assert o != null; 1623 } 1624 1625 /** Remove a list of invariants. */ 1626 public void remove_invs(List<Invariant> rm_list) { 1627 for (Invariant inv : rm_list) { 1628 inv.ppt.removeInvariant(inv); 1629 } 1630 } 1631 1632 /** 1633 * Returns the unary slice over v. Returns null if the slice doesn't exist (which can occur if all 1634 * of its invariants were falsified). 1635 */ 1636 public @Nullable PptSlice1 findSlice(VarInfo v) { 1637 return (PptSlice1) findSlice(new VarInfo[] {v}); 1638 } 1639 1640 /** 1641 * Returns the binary slice over v1 and v2. Returns null if the slice doesn't exist (which can 1642 * occur if all of its invariants were falsified). 1643 */ 1644 public @Nullable PptSlice2 findSlice(VarInfo v1, VarInfo v2) { 1645 assert v1.varinfo_index <= v2.varinfo_index; 1646 return (PptSlice2) findSlice(new VarInfo[] {v1, v2}); 1647 } 1648 1649 /** 1650 * Like findSlice, but it is not required that the variables be supplied in order of 1651 * varinfo_index. 1652 */ 1653 public @Nullable PptSlice2 findSlice_unordered(VarInfo v1, VarInfo v2) { 1654 // assert v1.varinfo_index != v2.varinfo_index; 1655 if (v1.varinfo_index < v2.varinfo_index) { 1656 return findSlice(v1, v2); 1657 } else { 1658 return findSlice(v2, v1); 1659 } 1660 } 1661 1662 /** 1663 * Returns the ternary slice over v1, v2, and v3. Returns null if the slice doesn't exist (which 1664 * can occur if all of its invariants were falsified). 1665 */ 1666 public @Nullable PptSlice3 findSlice(VarInfo v1, VarInfo v2, VarInfo v3) { 1667 assert v1.varinfo_index <= v2.varinfo_index; 1668 assert v2.varinfo_index <= v3.varinfo_index; 1669 return (PptSlice3) findSlice(new VarInfo[] {v1, v2, v3}); 1670 } 1671 1672 /** 1673 * Like findSlice, but it is not required that the variables be supplied in order of 1674 * varinfo_index. 1675 */ 1676 public @Nullable PptSlice3 findSlice_unordered(VarInfo v1, VarInfo v2, VarInfo v3) { 1677 // bubble sort is easier than 3 levels of if-then-else 1678 VarInfo tmp; 1679 if (v1.varinfo_index > v2.varinfo_index) { 1680 tmp = v2; 1681 v2 = v1; 1682 v1 = tmp; 1683 } 1684 if (v2.varinfo_index > v3.varinfo_index) { 1685 tmp = v3; 1686 v3 = v2; 1687 v2 = tmp; 1688 } 1689 if (v1.varinfo_index > v2.varinfo_index) { 1690 tmp = v2; 1691 v2 = v1; 1692 v1 = tmp; 1693 } 1694 return findSlice(v1, v2, v3); 1695 } 1696 1697 /** Find a pptSlice without an assumed ordering. */ 1698 public @Nullable PptSlice findSlice_unordered(VarInfo[] vis) { 1699 switch (vis.length) { 1700 case 1: 1701 return findSlice(vis[0]); 1702 case 2: 1703 return findSlice_unordered(vis[0], vis[1]); 1704 case 3: 1705 return findSlice_unordered(vis[0], vis[1], vis[2]); 1706 default: 1707 throw new RuntimeException("Bad length " + vis.length); 1708 } 1709 } 1710 1711 /** Find a pptSlice with an assumed ordering. */ 1712 public @Nullable PptSlice findSlice(VarInfo[] vis) { 1713 if (vis.length > 3) { 1714 throw new RuntimeException("Bad length " + vis.length); 1715 } 1716 return views.get(sliceIndex(vis)); 1717 } 1718 1719 /** 1720 * Returns the invariant in the slice specified by vis that matches the specified class. If the 1721 * slice or the invariant does not exist, returns null. 1722 */ 1723 public @Nullable Invariant find_inv_by_class(VarInfo[] vis, Class<? extends Invariant> cls) { 1724 1725 PptSlice slice = findSlice(vis); 1726 if (slice == null) { 1727 return null; 1728 } 1729 return slice.find_inv_by_class(cls); 1730 } 1731 1732 /** 1733 * Searches for all of the invariants that that provide an exact value for v. Intuitively those 1734 * are invariants of the form 'v = equation'. For example: 'v = 63' or 'v = x * y' The 1735 * implementation is a little iffy -- each invariant over v is examined and it matches iff it is 1736 * exact and its daikon format starts with 'v ='. 1737 * 1738 * @return list of matching invariants or null if no matching invariants are found 1739 */ 1740 public @Nullable List<Invariant> find_assignment_inv(VarInfo v) { 1741 1742 List<Invariant> assignment_invs = null; 1743 1744 String start = v.name() + " ="; 1745 for (PptSlice slice : views.values()) { 1746 1747 // Skip slices that don't use v 1748 if (!slice.usesVar(v)) { 1749 continue; 1750 } 1751 1752 // Skip slices that use v in more than one slot (eg, v = v/1) 1753 int cnt = 0; 1754 for (VarInfo vi : slice.var_infos) { 1755 if (vi == v) { 1756 cnt++; 1757 } 1758 } 1759 if (cnt > 1) { 1760 continue; 1761 } 1762 1763 // Look for exact assignments 1764 for (Invariant inv : slice.invs) { 1765 // System.out.printf("considering invariant %s, exact = %b%n", 1766 // inv.format(), inv.isExact()); 1767 if (inv.isExact() && inv.format_using(OutputFormat.DAIKON).startsWith(start)) { 1768 if (assignment_invs == null) { 1769 assignment_invs = new ArrayList<Invariant>(); 1770 } 1771 assignment_invs.add(inv); 1772 } 1773 } 1774 } 1775 1776 return assignment_invs; 1777 } 1778 1779 /** 1780 * Looks up the slice for v1. If the slice does not exist, one is created (but not added into the 1781 * list of slices for this ppt). 1782 */ 1783 @SuppressWarnings("all:purity") // caching 1784 @Pure 1785 public PptSlice get_temp_slice(VarInfo v) { 1786 1787 PptSlice slice = findSlice(v); 1788 if (slice == null) { 1789 slice = new PptSlice1(this, v); 1790 } 1791 1792 return slice; 1793 } 1794 1795 /** 1796 * Looks up the slice for v1 and v2. They do not have to be in order. If the slice does not exist, 1797 * one is created (but not added into the list of slices for this ppt). 1798 */ 1799 @SuppressWarnings("all:purity") // caching 1800 @Pure 1801 public PptSlice get_temp_slice(VarInfo v1, VarInfo v2) { 1802 1803 PptSlice slice = findSlice_unordered(v1, v2); 1804 if (slice == null) { 1805 if (v1.varinfo_index <= v2.varinfo_index) { 1806 slice = new PptSlice2(this, v1, v2); 1807 } else { 1808 slice = new PptSlice2(this, v2, v1); 1809 } 1810 } 1811 1812 return slice; 1813 } 1814 1815 /** 1816 * If the prototype invariant is true over the specified variable returns DiscardInfo indicating 1817 * that the prototype invariant implies imp_inv. Otherwise returns null. 1818 */ 1819 public @Nullable DiscardInfo check_implied( 1820 Invariant imp_inv, VarInfo v, @Prototype Invariant proto) { 1821 1822 // If there is no proto invariant, we can't look for it. This happens 1823 // if the invariant is not enabled. 1824 if (proto == null) { 1825 return null; 1826 } 1827 1828 // Get the slice and instantiate the possible antecedent over it 1829 PptSlice slice = get_temp_slice(v); 1830 Invariant antecedent_inv = proto.instantiate(slice); 1831 if (antecedent_inv == null) { 1832 return null; 1833 } 1834 1835 // Check to see if the antecedent is true 1836 if (slice.is_inv_true(antecedent_inv)) { 1837 return new DiscardInfo(imp_inv, DiscardCode.obvious, "Implied by " + antecedent_inv.format()); 1838 } 1839 1840 return null; 1841 } 1842 1843 /** 1844 * If the proto invariant is true over the leader of the specified variable returns DiscardInfo 1845 * indicating that the proto invariant implies imp_inv. Otherwise returns null. 1846 */ 1847 public @Nullable DiscardInfo check_implied_canonical( 1848 Invariant imp_inv, VarInfo v, @Prototype Invariant proto) { 1849 1850 VarInfo leader = v.canonicalRep(); 1851 1852 DiscardInfo di = check_implied(imp_inv, leader, proto); 1853 if (di == null) { 1854 return null; 1855 } 1856 1857 // Build a new discardString that includes the variable equality 1858 String reason = di.discardString(); 1859 if (leader != v) { 1860 reason += " and (" + leader + "==" + v + ")"; 1861 } 1862 1863 return new DiscardInfo(imp_inv, DiscardCode.obvious, reason); 1864 } 1865 1866 /** 1867 * If the prototype invariant is true over the specified variables returns DiscardInfo indicating 1868 * that the prototype invariant implies imp_inv. Otherwise returns null. 1869 */ 1870 public @Nullable DiscardInfo check_implied( 1871 Invariant imp_inv, VarInfo v1, VarInfo v2, @Prototype Invariant proto) { 1872 1873 // If there is no prototype invariant, we can't look for it. This happens 1874 // if the invariant is not enabled. 1875 if (proto == null) { 1876 return null; 1877 } 1878 1879 // Get the slice and instantiate the possible antecedent over it 1880 PptSlice slice = get_temp_slice(v1, v2); 1881 Invariant antecedent_inv = proto.instantiate(slice); 1882 if (antecedent_inv == null) { 1883 return null; 1884 } 1885 1886 // Permute the antecedent if necessary 1887 if (v1.varinfo_index > v2.varinfo_index) { 1888 antecedent_inv = antecedent_inv.permute(permute_swap); 1889 } 1890 1891 // Check to see if the antecedent is true 1892 if (slice.is_inv_true(antecedent_inv)) { 1893 return new DiscardInfo(imp_inv, DiscardCode.obvious, "Implied by " + antecedent_inv.format()); 1894 } 1895 1896 return null; 1897 } 1898 1899 public boolean check_implied(DiscardInfo di, VarInfo v1, VarInfo v2, @Prototype Invariant proto) { 1900 1901 DiscardInfo di2 = check_implied(di.inv, v1, v2, proto); 1902 if (di2 == null) { 1903 return false; 1904 } 1905 1906 di.add_implied(di2.discardString()); 1907 return true; 1908 } 1909 1910 /** 1911 * If the prototype invariant is true over the leader of each specified variables returns 1912 * DiscardInfo indicating that the prototype invariant implies imp_inv. Otherwise returns null. 1913 */ 1914 public @Nullable DiscardInfo check_implied_canonical( 1915 Invariant imp_inv, VarInfo v1, VarInfo v2, @Prototype Invariant proto) { 1916 1917 VarInfo leader1 = v1.canonicalRep(); 1918 VarInfo leader2 = v2.canonicalRep(); 1919 1920 DiscardInfo di = check_implied(imp_inv, leader1, leader2, proto); 1921 if (di == null) { 1922 return null; 1923 } 1924 1925 // If the variables match the leader, the current reason is good 1926 if ((leader1 == v1) && (leader2 == v2)) { 1927 return di; 1928 } 1929 1930 // Build a new discardString that includes the variable equality 1931 String reason = di.discardString(); 1932 if (leader1 != v1) { 1933 reason += " and (" + leader1 + "==" + v1 + ")"; 1934 } 1935 if (leader2 != v2) { 1936 reason += " and (" + leader2 + "==" + v2 + ")"; 1937 } 1938 1939 return new DiscardInfo(imp_inv, DiscardCode.obvious, reason); 1940 } 1941 1942 public boolean check_implied_canonical( 1943 DiscardInfo di, VarInfo v1, VarInfo v2, @Prototype Invariant proto) { 1944 1945 DiscardInfo di2 = check_implied_canonical(di.inv, v1, v2, proto); 1946 if (di2 == null) { 1947 return false; 1948 } 1949 1950 di.add_implied(di2.discardString()); 1951 return true; 1952 } 1953 1954 /** Returns whether or not v1 is a subset of v2. */ 1955 @SuppressWarnings("all:purity") // side effects to local state 1956 @Pure 1957 public boolean is_subset(VarInfo v1, VarInfo v2) { 1958 1959 // Find the slice for v1 and v2. If no slice exists, create it, 1960 // but don't add it to the slices for this ppt. It only exists 1961 // as a temporary home for the invariant we are looking for below. 1962 PptSlice slice = get_temp_slice(v1, v2); 1963 1964 // Create the invariant we are looking for 1965 Invariant inv = null; 1966 if ((v1.rep_type == ProglangType.INT_ARRAY)) { 1967 assert v2.rep_type == ProglangType.INT_ARRAY; 1968 inv = SubSet.get_proto().instantiate(slice); 1969 } else if (v1.rep_type == ProglangType.DOUBLE_ARRAY) { 1970 assert v2.rep_type == ProglangType.DOUBLE_ARRAY; 1971 inv = SubSetFloat.get_proto().instantiate(slice); 1972 } 1973 1974 if (inv == null) { 1975 return false; 1976 } 1977 1978 // If the varinfos are out of order swap 1979 if (v1.varinfo_index > v2.varinfo_index) { 1980 inv = inv.permute(permute_swap); 1981 } 1982 1983 // Look for the invariant 1984 return slice.is_inv_true(inv); 1985 } 1986 1987 /** Returns whether or not v1 is always non-zero. */ 1988 @SuppressWarnings("all:purity") // caching 1989 @Pure 1990 public boolean is_nonzero(VarInfo v) { 1991 1992 // find the slice for v. If the slice doesn't exist, the non-zero 1993 // invariant can't exist 1994 PptSlice slice = findSlice(v.canonicalRep()); 1995 if (slice == null) { 1996 // System.out.printf("No slice for variable %s [leader %s]%n", v, 1997 // v.canonicalRep()); 1998 return false; 1999 } 2000 2001 // Get a prototype of the invariant we are looking for 2002 @Prototype Invariant proto = NonZero.get_proto(); 2003 if (proto == null) { 2004 return false; 2005 } 2006 2007 Invariant inv = proto.instantiate(slice); 2008 if (inv == null) { 2009 return false; 2010 } 2011 2012 // Debug print the other invariants in this slice. 2013 // if (!slice.is_inv_true(inv)) { 2014 // System.out.printf("%d invariants for variable %s in ppt %s%n", slice.invs.size(), v, 2015 // name()); 2016 // for (Invariant other_inv : slice.invs) { 2017 // System.out.printf("Invariant %s in ppt %s%n", other_inv.format(), name()); 2018 // } 2019 // } 2020 2021 return slice.is_inv_true(inv); 2022 } 2023 2024 /** 2025 * Returns whether or not the specified variables are equal (ie, an equality invariant exists 2026 * between them). 2027 */ 2028 @Pure 2029 public boolean is_equal(VarInfo v1, VarInfo v2) { 2030 2031 // System.out.printf("checking equality on %s and %s%n", v1, v2); 2032 2033 // Check for leaders, not variables 2034 v1 = v1.canonicalRep(); 2035 v2 = v2.canonicalRep(); 2036 2037 // Find the slice for v1 and v2. If the slice doesn't exist, 2038 // the variables can't be equal 2039 PptSlice slice = findSlice_unordered(v1, v2); 2040 if (slice == null) { 2041 // System.out.printf("No slide for %s and %s%n", v1, v2); 2042 return false; 2043 } 2044 2045 // Get a prototype of the invariant we are looking for 2046 @Prototype Invariant proto; 2047 if (v1.rep_type.isScalar()) { 2048 assert v2.rep_type.isScalar() 2049 : String.format("v1 %s rep %s, v2 %s rep %s", v1, v1.rep_type, v2, v2.rep_type); 2050 proto = IntEqual.get_proto(); 2051 } else if (v1.rep_type.isFloat()) { 2052 assert v2.rep_type.isFloat(); 2053 proto = FloatEqual.get_proto(); 2054 } else if (v1.rep_type == ProglangType.STRING) { 2055 assert v2.rep_type == ProglangType.STRING; 2056 proto = StringEqual.get_proto(); 2057 } else if ((v1.rep_type == ProglangType.INT_ARRAY)) { 2058 assert v2.rep_type == ProglangType.INT_ARRAY; 2059 proto = SeqSeqIntEqual.get_proto(); 2060 } else if (v1.rep_type == ProglangType.DOUBLE_ARRAY) { 2061 assert v2.rep_type == ProglangType.DOUBLE_ARRAY; 2062 proto = SeqSeqFloatEqual.get_proto(); 2063 } else if ((v1.rep_type == ProglangType.STRING_ARRAY)) { 2064 assert v2.rep_type == ProglangType.STRING_ARRAY; 2065 proto = SeqSeqStringEqual.get_proto(); 2066 } else { 2067 throw new Error("unexpected type " + v1.rep_type); 2068 } 2069 assert proto != null; 2070 assert proto.valid_types(slice.var_infos); 2071 2072 // Return whether or not the invariant is true in the slice 2073 Invariant inv = proto.instantiate(slice); 2074 // System.out.printf("invariant = %s", inv); 2075 if (inv == null) { 2076 return false; 2077 } 2078 return slice.is_inv_true(inv); 2079 } 2080 2081 /** 2082 * Returns true if (v1+v1_shift) ≤ (v2+v2_shift) is known to be true. Returns false otherwise. 2083 * Integers only. 2084 */ 2085 @Pure 2086 public boolean is_less_equal(VarInfo v1, int v1_shift, VarInfo v2, int v2_shift) { 2087 2088 assert v1.ppt == this; 2089 assert v2.ppt == this; 2090 assert v1.file_rep_type.isIntegral(); 2091 assert v2.file_rep_type.isIntegral(); 2092 2093 Invariant inv = null; 2094 PptSlice slice = null; 2095 if (v1.varinfo_index <= v2.varinfo_index) { 2096 slice = findSlice(v1, v2); 2097 if (slice != null) { 2098 if (v1_shift <= v2_shift) { 2099 inv = IntLessEqual.get_proto().instantiate(slice); 2100 } else if (v1_shift == (v2_shift + 1)) { 2101 inv = IntLessThan.get_proto().instantiate(slice); 2102 } else { // no invariant over v1 and v2 shows ((v1 + 2) <= v2) 2103 } 2104 } 2105 } else { 2106 slice = findSlice(v2, v1); 2107 if (slice != null) { 2108 if (v1_shift <= v2_shift) { 2109 inv = IntGreaterEqual.get_proto().instantiate(slice); 2110 } else if (v1_shift == (v2_shift + 1)) { 2111 inv = IntGreaterThan.get_proto().instantiate(slice); 2112 } else { // no invariant over v1 and v2 shows ((v2 + 2) <= v1) 2113 } 2114 } 2115 } 2116 2117 @SuppressWarnings("nullness") // dependent: if inv is non-null, then slice is non-null 2118 boolean found = (inv != null) && slice.is_inv_true(inv); 2119 if (debugStdout) { 2120 System.out.printf( 2121 "Looking for %s [%d] <= %s [%d] in ppt %s%n", 2122 v1.name(), v1_shift, v2.name(), v2_shift, this.name()); 2123 System.out.printf( 2124 "Searched for invariant %s, found = %b", (inv == null) ? "null" : inv.format(), found); 2125 } 2126 return found; 2127 } 2128 2129 /** 2130 * Returns true if v1 is known to be a subsequence of v2. This is true if the subsequence 2131 * invariant exists or if it it suppressed. 2132 */ 2133 @Pure 2134 public boolean is_subsequence(VarInfo v1, VarInfo v2) { 2135 2136 // Find the slice for v1 and v2. If no slice exists, create it, 2137 // but don't add it to the slices for this ppt. It only exists 2138 // as a temporary home for the invariant we are looking for below. 2139 PptSlice slice = get_temp_slice(v1, v2); 2140 2141 // Create the invariant we are looking for. 2142 Invariant inv = null; 2143 if ((v1.rep_type == ProglangType.INT_ARRAY)) { 2144 assert v2.rep_type == ProglangType.INT_ARRAY; 2145 inv = SubSequence.get_proto().instantiate(slice); 2146 } else if (v1.rep_type == ProglangType.DOUBLE_ARRAY) { 2147 assert v2.rep_type == ProglangType.DOUBLE_ARRAY; 2148 inv = SubSequenceFloat.get_proto().instantiate(slice); 2149 } else { 2150 throw new Error("unexpected type " + v1.rep_type); 2151 } 2152 2153 if (inv == null) { 2154 return false; 2155 } 2156 2157 // If the varinfos are out of order swap 2158 if (v1.varinfo_index > v2.varinfo_index) { 2159 inv = inv.permute(permute_swap); 2160 } 2161 2162 return slice.is_inv_true(inv); 2163 } 2164 2165 /** Returns true if varr is empty. Supports ints, doubles, and strings. */ 2166 @Pure 2167 public boolean is_empty(VarInfo varr) { 2168 2169 // Find the slice for varr. If no slice exists, create it, but 2170 // don't add it to the slices for this ppt. It only exists as a 2171 // temporary home for the invariant we are looking for below. 2172 PptSlice slice = findSlice(varr); 2173 if (slice == null) { 2174 slice = new PptSlice1(this, varr); 2175 } 2176 2177 // Create a one of invariant with an empty array as its only 2178 // value. 2179 Invariant inv = null; 2180 if ((varr.rep_type == ProglangType.INT_ARRAY)) { 2181 OneOfSequence oos = (OneOfSequence) OneOfSequence.get_proto().instantiate(slice); 2182 if (oos != null) { 2183 long[] @Interned [] one_of = new long[] @Interned [] {new long @Interned [0]}; 2184 oos.set_one_of_val(one_of); 2185 inv = oos; 2186 } 2187 } else if (varr.rep_type == ProglangType.DOUBLE_ARRAY) { 2188 OneOfFloatSequence oos = 2189 (OneOfFloatSequence) OneOfFloatSequence.get_proto().instantiate(slice); 2190 if (oos != null) { 2191 double[] @Interned [] one_of = new double[] @Interned [] {new double @Interned [0]}; 2192 oos.set_one_of_val(one_of); 2193 inv = oos; 2194 } 2195 } else if (varr.rep_type == ProglangType.STRING_ARRAY) { 2196 OneOfStringSequence oos = 2197 (OneOfStringSequence) OneOfStringSequence.get_proto().instantiate(slice); 2198 if (oos != null) { 2199 @Interned String[] @Interned [] one_of = 2200 new @Interned String[] @Interned [] {new @Interned String @Interned [0]}; 2201 oos.set_one_of_val(one_of); 2202 inv = oos; 2203 } 2204 } 2205 2206 if (inv == null) { 2207 return false; 2208 } 2209 2210 return slice.is_inv_true(inv); 2211 } 2212 2213 /** 2214 * This function creates all the views (and thus candidate invariants), but does not check those 2215 * invariants. We create NO views over static constant variables, but everything else is fair 2216 * game. We don't create views over variables which have a higher (controlling) view. This 2217 * function does NOT cause invariants over the new views to be checked (but it does create 2218 * invariants). 2219 */ 2220 2221 // Note that some slightly inefficient code has been added to aid 2222 // in debugging. When creating binary and ternary views and debugging 2223 // is on, the outer loops will not terminate prematurely on inappropriate 2224 // (i.e., non-canonical) variables. This allows explicit debug statements 2225 // for each possible combination, simplifying determining why certain 2226 // slices were not created. 2227 2228 public void instantiate_views_and_invariants() { 2229 2230 if (debug.isLoggable(Level.FINE)) { 2231 debug.fine("instantiate_views_and_invariants for " + name()); 2232 } 2233 2234 // used only for debugging 2235 int old_num_vars = var_infos.length; 2236 int old_num_views = views.size(); 2237 boolean debug_on = debug.isLoggable(Level.FINE); 2238 2239 // / 1. all unary views 2240 2241 // Unary slices/invariants. 2242 List<PptSlice> unary_views = new ArrayList<>(var_infos.length); 2243 for (int i = 0; i < var_infos.length; i++) { 2244 VarInfo vi = var_infos[i]; 2245 2246 if (Debug.logOn()) { 2247 Debug.log(getClass(), this, Debug.vis(vi), " Instantiate Slice, ok=" + is_slice_ok(vi)); 2248 } 2249 2250 // we do not call is_var_ok_unary on vi here because 2251 // is_slice_ok does the same thing 2252 if (!is_slice_ok(vi)) { 2253 continue; 2254 } 2255 2256 // Eventually, add back in this test as "if constant and no 2257 // comparability info exists" then continue. 2258 // if (vi.isStaticConstant()) continue; 2259 2260 PptSlice1 slice1 = new PptSlice1(this, vi); 2261 slice1.instantiate_invariants(); 2262 2263 if (Debug.logOn() || debug_on) { 2264 Debug.log(debug, getClass(), slice1, "Created unary slice"); 2265 } 2266 unary_views.add(slice1); 2267 } 2268 addViews(unary_views); 2269 unary_views = null; 2270 2271 // / 2. all binary views 2272 2273 // Binary slices/invariants. 2274 List<PptSlice> binary_views = new ArrayList<>(); 2275 for (int i1 = 0; i1 < var_infos.length; i1++) { 2276 VarInfo var1 = var_infos[i1]; 2277 2278 if (!is_var_ok_binary(var1)) { 2279 continue; 2280 } 2281 2282 // Eventually, add back in this test as "if constant and no 2283 // comparability info exists" then continue. 2284 // if (var1.isStaticConstant()) continue; 2285 2286 for (int i2 = i1; i2 < var_infos.length; i2++) { 2287 VarInfo var2 = var_infos[i2]; 2288 2289 if (!is_var_ok_binary(var2)) { 2290 continue; 2291 } 2292 2293 // Eventually, add back in this test as "if constant and no 2294 // comparability info exists" then continue. 2295 // if (var2.isStaticConstant()) continue; 2296 if (!is_slice_ok(var1, var2)) { 2297 if (Debug.logOn() || debug_on) { 2298 Debug.log( 2299 debug, 2300 getClass(), 2301 this, 2302 Debug.vis(var1, var2), 2303 "Binary slice not created, is_slice_ok == false"); 2304 } 2305 continue; 2306 } 2307 PptSlice2 slice2 = new PptSlice2(this, var1, var2); 2308 if (Debug.logOn() || debug_on) { 2309 Debug.log(debug, getClass(), slice2, "Creating binary slice"); 2310 } 2311 2312 slice2.instantiate_invariants(); 2313 binary_views.add(slice2); 2314 } 2315 } 2316 addViews(binary_views); 2317 binary_views = null; 2318 2319 // 3. all ternary views 2320 if (Global.debugInfer.isLoggable(Level.FINE)) { 2321 Global.debugInfer.fine("Trying ternary slices for " + this.name()); 2322 } 2323 2324 List<PptSlice> ternary_views = new ArrayList<>(); 2325 for (int i1 = 0; i1 < var_infos.length; i1++) { 2326 VarInfo var1 = var_infos[i1]; 2327 if (!is_var_ok_ternary(var1)) { 2328 continue; 2329 } 2330 2331 // Eventually, add back in this test as "if constant and no 2332 // comparability info exists" then continue. 2333 // if (var1.isStaticConstant()) continue; 2334 2335 for (int i2 = i1; i2 < var_infos.length; i2++) { 2336 VarInfo var2 = var_infos[i2]; 2337 2338 if (!is_var_ok_ternary(var2)) { 2339 continue; 2340 } 2341 2342 // Eventually, add back in this test as "if constant and no 2343 // comparability info exists" then continue. 2344 // if (var2.isStaticConstant()) continue; 2345 2346 for (int i3 = i2; i3 < var_infos.length; i3++) { 2347 2348 VarInfo var3 = var_infos[i3]; 2349 2350 if (!is_var_ok_ternary(var3)) { 2351 continue; 2352 } 2353 2354 if (!is_slice_ok(var1, var2, var3)) { 2355 continue; 2356 } 2357 2358 PptSlice3 slice3 = new PptSlice3(this, var1, var2, var3); 2359 slice3.instantiate_invariants(); 2360 if (Debug.logOn() || debug_on) { 2361 Debug.log(debug, getClass(), slice3, "Created Ternary Slice"); 2362 } 2363 ternary_views.add(slice3); 2364 } 2365 } 2366 } 2367 addViews(ternary_views); 2368 2369 if (debug.isLoggable(Level.FINE)) { 2370 debug.fine(views.size() - old_num_views + " new views for " + name()); 2371 } 2372 2373 if (debug.isLoggable(Level.FINE)) { 2374 debug.fine("Done with instantiate_views_and_invariants"); 2375 } 2376 2377 // This method didn't add any new variables. 2378 assert old_num_vars == var_infos.length; 2379 repCheck(); 2380 } 2381 2382 /** 2383 * Returns whether the variable should be involved in an unary slice. The variable must be a 2384 * leader, not a constant, and not always missing. 2385 */ 2386 @Pure 2387 private boolean is_var_ok_unary(VarInfo var) { 2388 2389 if (DynamicConstants.dkconfig_use_dynamic_constant_optimization && constants == null) { 2390 return false; 2391 } 2392 2393 if (is_constant(var)) { 2394 return false; 2395 } 2396 2397 if (is_missing(var)) { 2398 return false; 2399 } 2400 2401 if (!var.isCanonical()) { 2402 return false; 2403 } 2404 2405 if (PrintInvariants.dkconfig_static_const_infer && var.is_static_constant) { 2406 return false; 2407 } 2408 2409 return true; 2410 } 2411 2412 /** 2413 * Returns whether the variable should be involved in a binary slice. The variable must be a 2414 * leader and not always missing. The function allows early termination when looking at 2415 * combinations of variables for creating slices. For example, if variable x is not suitable for 2416 * binary slices, then we do not need to look at x with any other variable in a binary slice (fail 2417 * fast). 2418 */ 2419 @Pure 2420 private boolean is_var_ok_binary(VarInfo var) { 2421 2422 if (DynamicConstants.dkconfig_use_dynamic_constant_optimization && constants == null) { 2423 return false; 2424 } 2425 2426 if (is_missing(var)) { 2427 return false; 2428 } 2429 2430 if (!var.isCanonical()) { 2431 return false; 2432 } 2433 2434 if (PrintInvariants.dkconfig_static_const_infer && var.is_static_constant) { 2435 return false; 2436 } 2437 2438 return true; 2439 } 2440 2441 /** 2442 * Returns whether the variable should be involved in a ternary slice. In addition to the 2443 * requirements of variables in the binary slices, for ternary slices, the variable must be an 2444 * integer or float and must not be an array. The function allows early termination when looking 2445 * at combinations of variables for creating slices. For example, if variable x is not suitable 2446 * for binary slices, then we do not need to look at x with any other variable in a binary slice 2447 * (fail fast). 2448 * 2449 * @see #is_var_ok_binary(VarInfo) 2450 */ 2451 @Pure 2452 private boolean is_var_ok_ternary(VarInfo var) { 2453 if (DynamicConstants.dkconfig_use_dynamic_constant_optimization && constants == null) { 2454 return false; 2455 } 2456 2457 if (!is_var_ok_binary(var)) { 2458 return false; 2459 } 2460 2461 // arrays are not allowed in ternary invariants 2462 if (var.rep_type.isArray()) { 2463 return false; 2464 } 2465 2466 // For now, variable must be integral or float 2467 if (!var.file_rep_type.isIntegral() && !var.file_rep_type.isFloat()) { 2468 return false; 2469 } 2470 2471 if (PrintInvariants.dkconfig_static_const_infer && var.is_static_constant) { 2472 return false; 2473 } 2474 2475 return true; 2476 } 2477 2478 /** Returns whether or not the specified slice should be created. */ 2479 @Pure 2480 public boolean is_slice_ok(VarInfo[] vis, int arity) { 2481 if (arity == 1) { 2482 return is_slice_ok(vis[0]); 2483 } else if (arity == 2) { 2484 return is_slice_ok(vis[0], vis[1]); 2485 } else { 2486 return is_slice_ok(vis[0], vis[1], vis[2]); 2487 } 2488 } 2489 2490 /** 2491 * Returns whether or not the specified unary slice should be created. The slice should not be 2492 * created if the variable does not meet qualifications for the unary slice. 2493 * 2494 * @see #is_var_ok_unary(VarInfo) 2495 */ 2496 @Pure 2497 public boolean is_slice_ok(VarInfo var1) { 2498 2499 return is_var_ok_unary(var1); 2500 } 2501 2502 /** 2503 * Returns whether or not the specified binary slice should be created. The slice should not be 2504 * created if any of the following are true: 2505 * 2506 * <p>- One of the variables does not meet qualifications for the binary slice - Variables are not 2507 * compatible - Both variables are constant. 2508 * 2509 * @see #is_var_ok_binary(VarInfo) 2510 */ 2511 @Pure 2512 public boolean is_slice_ok(VarInfo var1, VarInfo var2) { 2513 2514 if (!is_var_ok_binary(var1) || !is_var_ok_binary(var2)) { 2515 return false; 2516 } 2517 2518 // Check to see if the new slice would be over all constants 2519 if (is_constant(var1) && is_constant(var2)) { 2520 return false; 2521 } 2522 2523 if (!(var1.compatible(var2) 2524 || (var1.type.isArray() && var1.eltsCompatible(var2)) 2525 || (var2.type.isArray() && var2.eltsCompatible(var1)))) { 2526 // System.out.printf("is_slice_ok(%s, %s): variables not compatible%n", 2527 // var1, var2); 2528 return false; 2529 } 2530 2531 // Don't create a slice with the same variables if the equality 2532 // set only contains 1 variable 2533 // This is not turned on for now since suppressions need invariants 2534 // of the form a == a even when a is the only item in the set. 2535 if (false) { 2536 if ((var1 == var2) && (var1.get_equalitySet_size() == 1)) { 2537 return false; 2538 } 2539 } 2540 2541 return true; 2542 } 2543 2544 /** 2545 * Returns whether or not the specified ternary slice should be created by checking the variables' 2546 * qualifications. In addition, The slice should not be created if any of the following are true: 2547 * 2548 * <ul> 2549 * <li>One of the variables does not meet qualifications for the ternary slice 2550 * <li>All of the vars are constants 2551 * <li>Any var is not (integral or float) 2552 * <li>Each var is the same and its equality set has only two variables 2553 * <li>Two of the vars are the same and its equality has only one variable. (This last one is 2554 * currently disabled as x = func(x,y) might still be interesting even if x is the same.) 2555 * </ul> 2556 * 2557 * @see #is_var_ok_ternary(VarInfo) 2558 */ 2559 @Pure 2560 public boolean is_slice_ok(VarInfo v1, VarInfo v2, VarInfo v3) { 2561 2562 Debug dlog = null; 2563 if (Debug.logOn() || debug.isLoggable(Level.FINE)) { 2564 dlog = new Debug(getClass(), this, Debug.vis(v1, v2, v3)); 2565 } 2566 2567 if (!is_var_ok_ternary(v1) || !is_var_ok_ternary(v2) || !is_var_ok_ternary(v3)) { 2568 return false; 2569 } 2570 2571 // At least one variable must not be a constant 2572 if (is_constant(v1) && is_constant(v2) && is_constant(v3)) { 2573 return false; 2574 } 2575 2576 // Vars must be compatible 2577 if (!v1.compatible(v2) || !v1.compatible(v3) || !v2.compatible(v3)) { 2578 if (dlog != null) { 2579 dlog.log(debug, "Ternary slice not created, vars not compatible"); 2580 } 2581 return false; 2582 } 2583 2584 // Don't create a reflexive slice (all vars the same) if there are 2585 // only two vars in the equality set 2586 if ((v1 == v2) && (v2 == v3) && (v1.get_equalitySet_size() <= 2)) { 2587 return false; 2588 } 2589 2590 // Don't create a partially reflexive slice (two vars the same) if there 2591 // is only one variable in its equality set 2592 if (false) { 2593 if (((v1 == v2) || (v1 == v3)) && (v1.get_equalitySet_size() == 1)) { 2594 return false; 2595 } 2596 if ((v2 == v3) && (v2.get_equalitySet_size() == 1)) { 2597 return false; 2598 } 2599 } 2600 2601 return true; 2602 } 2603 2604 /** 2605 * Determines whether the order of the variables in vis is a valid permutation (i.e., their 2606 * varinfo_index's are ordered). Null elements are ignored (and an all-null list is OK). 2607 */ 2608 public boolean vis_order_ok(VarInfo[] vis) { 2609 2610 VarInfo prev = vis[0]; 2611 for (int i = 1; i < vis.length; i++) { 2612 if ((prev != null) && (vis[i] != null)) { 2613 if (vis[i].varinfo_index < prev.varinfo_index) { 2614 return false; 2615 } 2616 } 2617 if (vis[i] != null) { 2618 prev = vis[i]; 2619 } 2620 } 2621 return true; 2622 } 2623 2624 /** 2625 * Return a slice that contains the given VarInfos (creating if needed). It is incumbent on the 2626 * caller that the slice be either filled with one or more invariants, or else removed from the 2627 * views collection. 2628 * 2629 * <p>When the arity of the slice is known, call one of the overloaded definitions of 2630 * get_or_instantiate_slice that takes (one or more) VarInfo arguments; they are more efficient. 2631 * 2632 * @param vis array of VarInfo objects; is not used internally (so the same value can be passed in 2633 * repeatedly). Can be unsorted. 2634 */ 2635 public PptSlice get_or_instantiate_slice(VarInfo[] vis) { 2636 switch (vis.length) { 2637 case 1: 2638 return get_or_instantiate_slice(vis[0]); 2639 case 2: 2640 return get_or_instantiate_slice(vis[0], vis[1]); 2641 case 3: 2642 return get_or_instantiate_slice(vis[0], vis[1], vis[2]); 2643 default: 2644 throw new IllegalArgumentException("bad length = " + vis.length); 2645 } 2646 } 2647 2648 /** 2649 * Return a slice that contains the given VarInfos (creating if needed). It is incumbent on the 2650 * caller that the slice be either filled with one or more invariants, or else removed from the 2651 * views collection. 2652 */ 2653 public PptSlice get_or_instantiate_slice(VarInfo vi) { 2654 PptSlice result = findSlice(vi); 2655 if (result != null) { 2656 return result; 2657 } 2658 2659 // We may do inference over static constants 2660 // assert ! vi.isStaticConstant(); 2661 result = new PptSlice1(this, vi); 2662 2663 addSlice(result); 2664 return result; 2665 } 2666 2667 /** 2668 * Return a slice that contains the given VarInfos (creating if needed). It is incumbent on the 2669 * caller that the slice be either filled with one or more invariants, or else removed from the 2670 * views collection. 2671 */ 2672 public PptSlice get_or_instantiate_slice(VarInfo v1, VarInfo v2) { 2673 VarInfo tmp; 2674 if (v1.varinfo_index > v2.varinfo_index) { 2675 tmp = v2; 2676 v2 = v1; 2677 v1 = tmp; 2678 } 2679 2680 PptSlice result = findSlice(v1, v2); 2681 if (result != null) { 2682 return result; 2683 } 2684 2685 // We may do inference over static constants 2686 // assert ! v1.isStaticConstant(); 2687 // assert ! v2.isStaticConstant(); 2688 result = new PptSlice2(this, v1, v2); 2689 2690 addSlice(result); 2691 return result; 2692 } 2693 2694 /** 2695 * Return a slice that contains the given VarInfos (creating if needed). It is incumbent on the 2696 * caller that the slice be either filled with one or more invariants, or else removed from the 2697 * views collection. 2698 */ 2699 public PptSlice get_or_instantiate_slice(VarInfo v1, VarInfo v2, VarInfo v3) { 2700 VarInfo tmp; 2701 if (v1.varinfo_index > v2.varinfo_index) { 2702 tmp = v2; 2703 v2 = v1; 2704 v1 = tmp; 2705 } 2706 if (v2.varinfo_index > v3.varinfo_index) { 2707 tmp = v3; 2708 v3 = v2; 2709 v2 = tmp; 2710 } 2711 if (v1.varinfo_index > v2.varinfo_index) { 2712 tmp = v2; 2713 v2 = v1; 2714 v1 = tmp; 2715 } 2716 2717 PptSlice result = findSlice(v1, v2, v3); 2718 if (result != null) { 2719 return result; 2720 } 2721 2722 // We may do inference over static constants 2723 // assert ! v1.isStaticConstant(); 2724 // assert ! v2.isStaticConstant(); 2725 // assert ! v3.isStaticConstant(); 2726 result = new PptSlice3(this, v1, v2, v3); 2727 2728 addSlice(result); 2729 return result; 2730 } 2731 2732 /////////////////////////////////////////////////////////////////////////// 2733 /// Creating conditioned views 2734 /// 2735 2736 // This static region can't appear in PptConditional, lest it never get 2737 // called. PptConditional isn't instantiated unless it needs to be, but 2738 // it doesn't need to be unless we run this static region! 2739 static { 2740 if (!PptSplitter.dkconfig_disable_splitting) { 2741 SplitterList.put( 2742 ".*", 2743 new Splitter[] { 2744 new ReturnTrueSplitter(), 2745 }); 2746 } 2747 } 2748 2749 public void addConditions(Splitter[] splits) { 2750 2751 debugConditional.fine( 2752 "Applying " 2753 + StringsPlume.nplural(((splits == null) ? 0 : splits.length), "split") 2754 + " to " 2755 + name()); 2756 2757 if ((splits == null) || (splits.length == 0)) { 2758 debugConditional.fine("No splits for " + name()); 2759 return; 2760 } 2761 2762 // Create a Conditional ppt for each side of each splitter 2763 splitters = new ArrayList<PptSplitter>(splits.length); 2764 for (int ii = 0; ii < splits.length; ii++) { 2765 PptSplitter ppt_split = new PptSplitter(this, splits[ii]); 2766 if (!ppt_split.splitter_valid()) { 2767 debugConditional.fine( 2768 "Splitter (" 2769 + ((ppt_split.splitter == null) ? "[no class]" : ppt_split.splitter.getClass()) 2770 + ") not valid: " 2771 + ppt_split.ppts[0].name); 2772 continue; 2773 } 2774 splitters.add(ppt_split); 2775 if (debugConditional.isLoggable(Level.FINE)) { 2776 debugConditional.fine("Added PptSplitter: " + ppt_split); 2777 } 2778 } 2779 } 2780 2781 @Pure 2782 public static @Nullable LemmaStack getProverStack() { 2783 return proverStack; 2784 } 2785 2786 /** 2787 * Given conditional program points (and invariants detected over them), create implications. 2788 * Configuration variable "pairwise_implications" controls whether all or only the first two 2789 * conditional program points are considered. 2790 */ 2791 @SuppressWarnings("nullness:contracts.precondition") // private field 2792 public void addImplications() { 2793 2794 if (PptSplitter.dkconfig_disable_splitting) { 2795 return; 2796 } 2797 2798 // Will this code be a problem at a parent point if one of its children 2799 // has no samples and thus no implications? 2800 if (num_samples() == 0) { 2801 return; 2802 } 2803 2804 // Add implications from each splitter 2805 if (splitters != null) { 2806 for (PptSplitter ppt_split : splitters) { 2807 ppt_split.add_implications(); 2808 } 2809 } 2810 2811 // If this is a combined exit point with two individual exits, create 2812 // implications from the two exit points 2813 if (ppt_name.isCombinedExitPoint()) { 2814 // System.out.printf("Considering ppt %s [%d children]%n", name(), 2815 // children.size()); 2816 List<PptTopLevel> exit_points = new ArrayList<>(); 2817 for (PptRelation rel : children) { 2818 if (rel.getRelationType() == PptRelationType.EXIT_EXITNN) { 2819 exit_points.add(rel.child); 2820 } 2821 } 2822 // System.out.printf("exit point count = %d%n", exit_points.size()); 2823 if (exit_points.size() == 2) { 2824 PptTopLevel ppt1 = exit_points.get(0); 2825 PptTopLevel ppt2 = exit_points.get(1); 2826 PptSplitter ppt_split = new PptSplitter(this, ppt2, ppt1); 2827 ppt_split.add_implications(); 2828 } 2829 } 2830 } 2831 2832 /////////////////////////////////////////////////////////////////////////// 2833 /// Post processing after data trace files are read (but before printing) 2834 /// 2835 2836 /** 2837 * Two things: a) convert Equality invariants into normal IntEqual type for filtering, printing, 2838 * etc. b) Pivot uninteresting parameter VarInfos so that each equality set contains only the 2839 * interesting one. 2840 */ 2841 public void postProcessEquality() { 2842 if (debugEqualTo.isLoggable(Level.FINE)) { 2843 debugEqualTo.fine("PostProcessingEquality for: " + this.name()); 2844 } 2845 if (num_samples() == 0) { 2846 return; 2847 } 2848 2849 assert equality_view != null : "ppt = " + ppt_name + " children = " + children; 2850 assert equality_view != null : "@AssumeAssertion(nullness): application invariant"; 2851 List<Invariant> equalityInvs = equality_view.invs; 2852 2853 // Pivot invariants to new equality leaders if needed, if old 2854 // leaders would prevent printing. 2855 for (Invariant inv : equalityInvs) { 2856 ((Equality) inv).pivot(); 2857 } 2858 2859 // Now pivot the other invariants 2860 Collection<PptSlice> slices = viewsAsCollection(); 2861 List<PptSlice> pivoted = new ArrayList<>(); 2862 2863 // PptSlice newSlice = slice.cloneAndInvs(leader, newLeader); 2864 2865 // Pivot each pptSlice so that each of its VarInfos map back to 2866 // their leaders. 2867 if (debugEqualTo.isLoggable(Level.FINE)) { 2868 debugEqualTo.fine(" Doing cloneAllPivots: "); 2869 } 2870 for (Iterator<PptSlice> iSlices = slices.iterator(); iSlices.hasNext(); ) { 2871 PptSlice slice = iSlices.next(); 2872 boolean needPivoting = false; 2873 for (int i = 0; i < slice.arity(); i++) { 2874 if (slice.var_infos[i].canonicalRep() != slice.var_infos[i]) { 2875 needPivoting = true; 2876 } 2877 } 2878 if (!needPivoting) { 2879 continue; 2880 } 2881 List<VarInfo> newVis_list = new ArrayList<>(slice.arity()); 2882 for (VarInfo vi : slice.var_infos) { 2883 newVis_list.add(vi.canonicalRep()); 2884 } 2885 VarInfo[] newVis = newVis_list.toArray(new VarInfo[0]); 2886 PptSlice newSlice = slice.cloneAndPivot(newVis); 2887 if (slice != newSlice) { 2888 pivoted.add(newSlice); 2889 iSlices.remove(); // Because the key is now wrong 2890 } 2891 } 2892 2893 // Add in the removed slices 2894 for (PptSlice oPivoted : pivoted) { 2895 addSlice(oPivoted); // Make the key right again 2896 if (debugEqualTo.isLoggable(Level.FINE)) { 2897 debugEqualTo.fine(" Readded: " + oPivoted); 2898 } 2899 } 2900 2901 // Add specific equality invariants for each member of the 2902 // equality set 2903 for (Invariant inv : equalityInvs) { 2904 ((Equality) inv).postProcess(); 2905 } 2906 } 2907 2908 /////////////////////////////////////////////////////////////////////////// 2909 /// Locating implied (same) invariants via the Simplify theorem-prover 2910 /// 2911 2912 /** 2913 * Created upon first use, then saved. Do not eagerly initialize, because doing so runs Simplify 2914 * (which crashes if Simplify is not installed). 2915 */ 2916 private static @Owning @MonotonicNonNull LemmaStack proverStack = null; 2917 2918 /** 2919 * Interface used by mark_implied_via_simplify to determine what invariants should be considered 2920 * during the logical redundancy tests. 2921 */ 2922 public static interface SimplifyInclusionTester { 2923 public boolean include(Invariant inv); 2924 } 2925 2926 /** 2927 * Use the Simplify theorem prover to flag invariants that are logically implied by others. 2928 * Considers only invariants that pass isWorthPrinting. 2929 * 2930 * @param all_ppts all the program points 2931 */ 2932 @SuppressWarnings("nullness") // reinitialization if error occurs 2933 public void mark_implied_via_simplify(PptMap all_ppts) { 2934 try { 2935 if (proverStack == null) { 2936 proverStack = new LemmaStack(); 2937 } 2938 markImpliedViaSimplify_int( 2939 new SimplifyInclusionTester() { 2940 @Override 2941 public boolean include(Invariant inv) { 2942 return InvariantFilters.defaultFilters().shouldKeep(inv) == null; 2943 } 2944 }); 2945 } catch (SimplifyError e) { 2946 if (proverStack != null) { 2947 proverStack.close(); 2948 } 2949 proverStack = null; 2950 } 2951 } 2952 2953 /** 2954 * Returns true if there was a problem with Simplify formatting (such as the invariant not having 2955 * a Simplify representation). 2956 */ 2957 public static boolean format_simplify_problem(String s) { 2958 return ((s.indexOf("Simplify not implemented") >= 0) 2959 || (s.indexOf("format(OutputFormat:Simplify)") >= 0) 2960 || (s.indexOf("format_simplify") >= 0)); 2961 } 2962 2963 /** 2964 * Use the Simplify theorem prover to flag invariants that are logically implied by others. Uses 2965 * the provided test interface to determine if an invariant is within the domain of inspection. 2966 * 2967 * @param test the predicate about whether an invariant is relevant 2968 */ 2969 @RequiresNonNull("proverStack") 2970 private void markImpliedViaSimplify_int(SimplifyInclusionTester test) throws SimplifyError { 2971 SessionManager.debugln("Simplify checking " + ppt_name); 2972 2973 // Create the list of invariants from this ppt which are 2974 // expressible in Simplify 2975 Invariant[] invs; 2976 { 2977 // Replace pairwise equality with an equivalence set 2978 List<Invariant> all_noeq = invariants_vector(); 2979 Collections.sort(all_noeq, icfp); 2980 List<Invariant> all = InvariantFilters.addEqualityInvariants(all_noeq); 2981 Collections.sort(all, icfp); 2982 List<Invariant> printing = new ArrayList<>(); 2983 for (Invariant inv : all) { 2984 if (test.include(inv)) { // think: inv.isWorthPrinting() 2985 String fmt = inv.format_using(OutputFormat.SIMPLIFY); 2986 if (!format_simplify_problem(fmt)) { 2987 // If format_simplify is not defined for this invariant, don't 2988 // confuse Simplify with the error message 2989 printing.add(inv); 2990 } 2991 } 2992 } 2993 invs = printing.toArray(new Invariant[0]); 2994 } 2995 2996 // For efficiency, bail if we don't have any invariants to mark as implied 2997 if (invs.length == 0) { 2998 return; 2999 } 3000 3001 // Come up with a "desirability" ordering of the printing and 3002 // expressible invariants, so that we can remove the least 3003 // desirable first. For now just use the ICFP. 3004 Arrays.sort(invs, icfp); 3005 3006 // Debugging 3007 if (Global.debugSimplify.isLoggable(Level.FINE)) { 3008 Global.debugSimplify.fine("Sorted invs:"); 3009 for (int i = 0; i < invs.length; i++) { 3010 Global.debugSimplify.fine(" " + invs[i].format()); 3011 } 3012 for (int i = 0; i < invs.length - 1; i++) { 3013 int cmp = icfp.compare(invs[i], invs[i + 1]); 3014 Global.debugSimplify.fine("cmp(" + i + "," + (i + 1) + ") = " + cmp); 3015 int rev_cmp = icfp.compare(invs[i + 1], invs[i]); 3016 Global.debugSimplify.fine("cmp(" + (i + 1) + "," + i + ") = " + rev_cmp); 3017 assert rev_cmp >= 0; 3018 } 3019 } 3020 3021 // The below two paragraphs of code (whose end result is to 3022 // compute "background") should be changed to use the VarInfo 3023 // partial ordering to determine background invariants, instead of 3024 // the (now deprecated) controlling_ppts relationship. 3025 3026 // Form the closure of the controllers; each element is a Ppt 3027 Set<PptTopLevel> closure = new LinkedHashSet<>(); 3028 { 3029 Set<PptTopLevel> working = new LinkedHashSet<>(); 3030 while (!working.isEmpty()) { 3031 PptTopLevel ppt = working.iterator().next(); 3032 working.remove(ppt); 3033 closure.add(ppt); 3034 } 3035 } 3036 3037 // Create the conjunction of the closures' invariants to form a 3038 // background environment for the prover. Ignore implications, 3039 // since in the current scheme, implications came from controlled 3040 // program points, and we don't necessarily want to lose the 3041 // unconditional version of the invariant at the conditional ppt. 3042 for (PptTopLevel ppt : closure) { 3043 List<Invariant> invs_vec = ppt.invariants_vector(); 3044 Collections.sort(invs_vec, icfp); 3045 for (Invariant inv : InvariantFilters.addEqualityInvariants(invs_vec)) { 3046 if (inv instanceof Implication) { 3047 continue; 3048 } 3049 if (!test.include(inv)) { // think: !inv.isWorthPrinting() 3050 continue; 3051 } 3052 String fmt = inv.format_using(OutputFormat.SIMPLIFY); 3053 if (format_simplify_problem(fmt)) { 3054 // If format_simplify is not defined for this invariant, don't 3055 // confuse Simplify with the error message 3056 continue; 3057 } 3058 // We could also consider testing if the controlling invariant 3059 // was removed by Simplify, but what would the point be? Also, 3060 // these "intermediate goals" might help out Simplify. 3061 proverStack.pushLemma(new InvariantLemma(inv)); 3062 3063 // If this is the :::OBJECT ppt, also restate all of them in 3064 // orig terms, since the conditions also held upon entry. 3065 if (ppt.ppt_name.isObjectInstanceSynthetic()) { 3066 proverStack.pushLemma(InvariantLemma.makeLemmaAddOrig(inv)); 3067 } 3068 } 3069 } 3070 3071 if (proverStack.checkForContradiction() == 'T') { 3072 if (LemmaStack.dkconfig_remove_contradictions) { 3073 System.err.println( 3074 "Warning: " + ppt_name + " background is contradictory, removing some parts"); 3075 proverStack.removeContradiction(); 3076 } else { 3077 System.err.println("Warning: " + ppt_name + " background is contradictory, giving up"); 3078 return; 3079 } 3080 } 3081 3082 int backgroundMark = proverStack.markLevel(); 3083 3084 /*NNC:@MonotonicNonNull*/ InvariantLemma[] lemmas = new InvariantLemma[invs.length]; 3085 for (int i = 0; i < invs.length; i++) { 3086 lemmas[i] = new InvariantLemma(invs[i]); 3087 } 3088 lemmas = castNonNullDeep(lemmas); // https://tinyurl.com/cfissue/986 3089 boolean[] present = new boolean[lemmas.length]; 3090 Arrays.fill(present, 0, present.length, true); 3091 for (int checking = invs.length - 1; checking >= 0; checking--) { 3092 StringJoiner bg = new StringJoiner(" ", "(", ")"); 3093 bg.add("AND"); 3094 for (int i = 0; i < present.length; i++) { 3095 if (present[i] && (i != checking)) { 3096 // format_using(OutputFormat.SIMPLIFY) is guaranteed to return 3097 // a sensible result for invariants in invs[]. 3098 bg.add(invs[i].format_using(OutputFormat.SIMPLIFY)); 3099 } 3100 } 3101 3102 // Debugging 3103 if (Global.debugSimplify.isLoggable(Level.FINE)) { 3104 SessionManager.debugln("Background:"); 3105 for (int i = 0; i < present.length; i++) { 3106 if (present[i] && (i != checking)) { 3107 SessionManager.debugln(" " + invs[i].format()); 3108 } 3109 } 3110 } 3111 } 3112 3113 for (int i = 0; i < invs.length; i++) { 3114 proverStack.pushLemma(lemmas[i]); 3115 } 3116 3117 // If the background is necessarily false, we are in big trouble 3118 if (proverStack.checkForContradiction() == 'T') { 3119 // Uncomment to punt on contradictions 3120 if (!LemmaStack.dkconfig_remove_contradictions) { 3121 System.err.println("Warning: " + ppt_name + " invariants are contradictory, giving up"); 3122 if (LemmaStack.dkconfig_print_contradictions) { 3123 LemmaStack.printLemmas(System.err, proverStack.minimizeContradiction()); 3124 } 3125 } 3126 System.err.println("Warning: " + ppt_name + " invariants are contradictory, axing some"); 3127 Map<Lemma, Integer> demerits = new TreeMap<>(); 3128 int worstWheel = 0; 3129 do { 3130 // But try to recover anyway 3131 List<Lemma> problems = proverStack.minimizeContradiction(); 3132 if (LemmaStack.dkconfig_print_contradictions) { 3133 System.err.println("Minimal set:"); 3134 LemmaStack.printLemmas(System.err, proverStack.minimizeContradiction()); 3135 System.err.println(); 3136 } 3137 if (problems.size() == 0) { 3138 System.err.println("Warning: removal failed, punting"); 3139 return; 3140 } 3141 for (Lemma problem : problems) { 3142 if (demerits.containsKey(problem)) { 3143 demerits.put(problem, demerits.get(problem).intValue() + 1); 3144 } else { 3145 demerits.put(problem, 1); 3146 } 3147 } 3148 int max_demerits = -1; 3149 List<Lemma> worst = new ArrayList<>(); 3150 for (Map.Entry<@KeyFor("demerits") Lemma, Integer> ent : demerits.entrySet()) { 3151 int value = ent.getValue().intValue(); 3152 if (value == max_demerits) { 3153 worst.add(ent.getKey()); 3154 } else if (value > max_demerits) { 3155 max_demerits = value; 3156 worst = new ArrayList<Lemma>(); 3157 worst.add(ent.getKey()); 3158 } 3159 } 3160 int offsetFromEnd = worstWheel % worst.size(); 3161 worstWheel = (3 * worstWheel + 1) % 10000019; 3162 int index = worst.size() - 1 - offsetFromEnd; 3163 Lemma bad = worst.get(index); 3164 demerits.remove(bad); 3165 proverStack.popToMark(backgroundMark); 3166 boolean isInvariant = false; 3167 for (int i = 0; i < lemmas.length; i++) { 3168 @SuppressWarnings("interning") // list membership 3169 boolean isBad = (lemmas[i] == bad); 3170 if (isBad) { 3171 present[i] = false; 3172 isInvariant = true; 3173 } else if (present[i]) { 3174 proverStack.pushLemma(lemmas[i]); 3175 } 3176 } 3177 if (!isInvariant) { 3178 proverStack.removeLemma(bad); 3179 } 3180 if (LemmaStack.dkconfig_print_contradictions) { 3181 System.err.println("Removing " + bad.summarize()); 3182 } else if (Daikon.no_text_output && Daikon.show_progress) { 3183 System.err.print("x"); 3184 } 3185 } while (proverStack.checkForContradiction() == 'T'); 3186 } 3187 3188 proverStack.popToMark(backgroundMark); 3189 3190 flagRedundantRecursive(lemmas, present, 0, lemmas.length - 1); 3191 3192 proverStack.clear(); 3193 } 3194 3195 /** 3196 * Go though an array of invariants, marking those that can be proved as consequences of others as 3197 * redundant. 3198 * 3199 * @param start first index to check, inclusive 3200 * @param end last index to check, inclusive 3201 */ 3202 @RequiresNonNull("proverStack") 3203 private void flagRedundantRecursive( 3204 InvariantLemma[] lemmas, boolean[] present, int start, int end) throws SimplifyError { 3205 assert start <= end; 3206 3207 if (start == end) { 3208 // Base case: check a single invariant 3209 int checking = start; 3210 if (proverStack.checkLemma(lemmas[checking]) == 'T') { 3211 // System.err.println("-------------------------"); 3212 // System.err.println(lemmas[checking].summarize() + 3213 // " is redundant because of"); 3214 // LemmaStack.printLemmas(System.err, 3215 // proverStack.minimizeProof(lemmas[checking])); 3216 flagRedundant(lemmas[checking].invariant); 3217 present[checking] = false; 3218 } 3219 SessionManager.debugln( 3220 (present[checking] ? "UNIQUE" : "REDUNDANT") + " " + lemmas[checking].summarize()); 3221 } else { 3222 // Recursive case: divide and conquer 3223 int first_half_end = (start + end) / 2; 3224 int second_half_start = first_half_end + 1; 3225 int mark = proverStack.markLevel(); 3226 // First, assume the first half and check the second half 3227 for (int i = start; i <= first_half_end; i++) { 3228 if (present[i]) { 3229 proverStack.pushLemma(lemmas[i]); 3230 } 3231 } 3232 flagRedundantRecursive(lemmas, present, second_half_start, end); 3233 proverStack.popToMark(mark); 3234 // Now, assume what's left of the second half, and check the 3235 // first half. 3236 for (int i = second_half_start; i <= end; i++) { 3237 if (present[i]) { 3238 proverStack.pushLemma(lemmas[i]); 3239 } 3240 } 3241 flagRedundantRecursive(lemmas, present, start, first_half_end); 3242 proverStack.popToMark(mark); 3243 } 3244 } 3245 3246 /** Mark an invariant as redundant. */ 3247 private void flagRedundant(Invariant inv) { 3248 if (inv instanceof Equality) { 3249 // Equality is not represented with a permanent invariant 3250 // object, so store the canonical variable instead. 3251 redundant_invs_equality.add(((Equality) inv).leader()); 3252 } else { 3253 redundant_invs.add(inv); 3254 } 3255 } 3256 3257 /////////////////////////////////////////////////////////////////////////// 3258 /// Parameter VarInfo processing 3259 /// 3260 3261 /** Cached VarInfos that are parameter variables. */ 3262 @SuppressWarnings("serial") 3263 private @MonotonicNonNull Set<VarInfo> paramVars = null; 3264 3265 /** Returns variables in this Ppt that are parameters. */ 3266 @Pure 3267 public Set<VarInfo> getParamVars() { 3268 if (paramVars != null) { 3269 return paramVars; 3270 } 3271 3272 paramVars = new LinkedHashSet<VarInfo>(); 3273 for (VarInfo var : var_infos) { 3274 if (var.isParam() && !var.isPrestate()) { 3275 paramVars.add(var); 3276 } 3277 } 3278 return paramVars; 3279 } 3280 3281 /////////////////////////////////////////////////////////////////////////// 3282 /// Printing invariants 3283 /// 3284 3285 /** 3286 * Return a List of all the invariants for the program point. Also consider using views_iterator() 3287 * instead. You can't modify the result of this. 3288 */ 3289 public List<Invariant> getInvariants() { 3290 List<Invariant> result = new ArrayList<>(); 3291 for (Iterator<Iterator<Invariant>> itor = new ViewsIteratorIterator(this); itor.hasNext(); ) { 3292 for (Iterator<Invariant> itor2 = itor.next(); itor2.hasNext(); ) { 3293 result.add(itor2.next()); 3294 } 3295 } 3296 return Collections.unmodifiableList(result); 3297 } 3298 3299 /** ArrayList version of {@link #getInvariants()}. */ 3300 public List<Invariant> invariants_vector() { 3301 return new ArrayList<Invariant>(getInvariants()); 3302 } 3303 3304 /** 3305 * For some clients, this method may be more efficient than getInvariants. 3306 * 3307 * @see #views_iterable() 3308 */ 3309 public Iterator<PptSlice> views_iterator() { 3310 // assertion only true when guarding invariants 3311 // assert views.contains(joiner_view); 3312 return viewsAsCollection().iterator(); 3313 } 3314 3315 /** 3316 * For some clients, this method may be more efficient than getInvariants. 3317 * 3318 * @see #views_iterator() 3319 */ 3320 public Iterable<PptSlice> views_iterable() { 3321 // assertion only true when guarding invariants 3322 // assert views.contains(joiner_view); 3323 return viewsAsCollection(); 3324 } 3325 3326 /** Iterate over all of the invariants at this ppt (but not any implications). */ 3327 public Iterator<Invariant> invariants_iterator() { 3328 return new CollectionsPlume.MergedIterator<Invariant>(views_iterator_iterator()); 3329 } 3330 3331 /** An iterator whose elements are themselves iterators that return invariants. */ 3332 private Iterator<Iterator<Invariant>> views_iterator_iterator() { 3333 return new ViewsIteratorIterator(this); 3334 } 3335 3336 /** An iterator whose elements are themselves iterators that return invariants. */ 3337 public static final class ViewsIteratorIterator implements Iterator<Iterator<Invariant>> { 3338 Iterator<PptSlice> vitor; 3339 @Nullable Iterator<Invariant> implication_iterator; 3340 3341 public ViewsIteratorIterator(PptTopLevel ppt) { 3342 vitor = ppt.views_iterator(); 3343 implication_iterator = ppt.joiner_view.invs.iterator(); 3344 } 3345 3346 @Override 3347 public boolean hasNext(@GuardSatisfied ViewsIteratorIterator this) { 3348 return vitor.hasNext() || (implication_iterator != null); 3349 } 3350 3351 @Override 3352 public Iterator<Invariant> next(@GuardSatisfied ViewsIteratorIterator this) { 3353 if (vitor.hasNext()) { 3354 return vitor.next().invs.iterator(); 3355 } else { 3356 if (implication_iterator == null) { 3357 throw new NoSuchElementException(); 3358 } 3359 Iterator<Invariant> tmp = implication_iterator; 3360 implication_iterator = null; 3361 return tmp; 3362 } 3363 } 3364 3365 @Override 3366 public void remove(@GuardSatisfied ViewsIteratorIterator this) { 3367 throw new UnsupportedOperationException(); 3368 } 3369 } 3370 3371 /** 3372 * Simplify the names of variables before printing them. For example, "orig(a[post(i)])" might 3373 * change into "orig(a[i+1])". We might want to switch off this behavior, depending on various 3374 * heuristics. We'll have to try it and see which output we like best. In any case, we have to do 3375 * this for ESC output, since ESC doesn't have anything like post(). 3376 */ 3377 public void simplify_variable_names() { 3378 for (VarInfo vi : var_infos) { 3379 // String original = vi.name(); 3380 vi.simplify_expression(); 3381 // if (!original.equals (vi.name())) 3382 // System.out.printf("modified var from %s to %s%n", original, 3383 // vi.name()); 3384 } 3385 } 3386 3387 public static final Comparator<Invariant> icfp = new Invariant.InvariantComparatorForPrinting(); 3388 3389 static Comparator<PptSlice> arityVarnameComparator = new PptSlice.ArityVarnameComparator(); 3390 3391 ///////////////////////////////////////////////////////////////////////////// 3392 ///// Invariant guarding 3393 3394 // /** This function guards all of the invariants in a PptTopLevel */ 3395 // public void guardInvariants() { 3396 // // To avoid concurrent modification exceptions using arrays 3397 // Object[] viewArray = viewsAsCollection().toArray(); 3398 // for (int i = 0; i < viewArray.length; i++) { 3399 // PptSlice currentView = (PptSlice) viewArray[i]; 3400 // currentView.guardInvariants(true); 3401 // } 3402 // 3403 // // Commented this code out because conditional views are not slices. 3404 // // It is not clear what this is trying to accomplish 3405 // // Object viewCondArray[] = views_cond.toArray(); 3406 // // for (int i = 0; i < viewCondArray.length; i++) { 3407 // // PptSlice currentCondView = (PptSlice)viewCondArray[i]; 3408 // // currentCondView.guardInvariants(); 3409 // // } 3410 // // This is a version changed to use the new conditional ppt iterator. 3411 // // But the elements are still not slices! 3412 // // for (Iterator<PptSlice> i = cond_iterator(); i.hasNext(); ) { 3413 // // PptSlice currentCondView = i.next(); 3414 // // currentCondView.guardInvariants(); 3415 // // } 3416 // 3417 // // System.out.println("Ppt name: " + name()); 3418 // // System.out.println("Number of invs in joiner_view: " + joiner_view.invs.size()); 3419 // } 3420 3421 /** Remove invariants that are marked for omission in omitTypes. */ 3422 public void processOmissions(boolean[] omitTypes) { 3423 // Avoid concurrent modification exceptions using arrays 3424 Collection<PptSlice> viewsAsCollection = viewsAsCollection(); 3425 PptSlice[] viewArray = viewsAsCollection.toArray(new PptSlice[0]); 3426 for (PptSlice currentView : viewArray) { 3427 currentView.processOmissions(omitTypes); 3428 } 3429 for (PptConditional currentCondView : cond_iterable()) { 3430 currentCondView.processOmissions(omitTypes); 3431 } 3432 } 3433 3434 /** Check the rep invariants of this. Throw an Error if not okay. */ 3435 public void repCheck() { 3436 // System.out.printf("repCheck of %s%n", name()); 3437 // Check that the hashing of 'views' is working correctly. This 3438 // should really be beneath the abstraction layer of the hash 3439 // table, but it isn't because Java can't enforce the immutability 3440 // of the keys. In particular, we got into trouble in the past 3441 // when the keys had pointers to VarInfos which themselves 3442 // indirectly pointed back to us. If the serializer found the 3443 // VarInfo before it found us, the VarInfo would be in-progress at 3444 // the time the HashMap was serialized. At the point when When the 3445 // PptTopLevel was unserialized, the VarInfo pointers in the keys 3446 // would be null, causing them to have a different hashCode than 3447 // they should. When the VarInfo was fully unserialized, the key's 3448 // hashCode then changed to the correct one, messing up the 3449 // indexing in a hard-to-debug way. -SMcC 3450 for (List<Integer> this_key : views.keySet()) { 3451 assert views.containsKey(this_key); 3452 } 3453 3454 // System.out.printf("equality for %s = %s%n", this, equality_view); 3455 3456 // We could check a lot more than just that slices are okay. For 3457 // example, we could ensure that flow graph is correct. 3458 for (PptSlice slice : viewsAsCollection()) { 3459 slice.repCheck(); 3460 } 3461 if (equality_view != null) { 3462 equality_view.repCheck(); 3463 } 3464 3465 // This should only be true while processing the hierarchy. Normally 3466 // repcheck isn't called there. 3467 assert in_merge == false : this; 3468 3469 // check variables for some possible errors 3470 for (VarInfo vi : var_infos) { 3471 vi.var_check(); 3472 } 3473 } 3474 3475 /** Debug method to display all slices. */ 3476 public String debugSlices() { 3477 StringBuilder result = new StringBuilder(); 3478 result.append("Slices for: " + this.ppt_name); 3479 for (PptSlice slice : viewsAsCollection()) { 3480 result.append(Global.lineSep + slice.toString()); 3481 } 3482 return result.toString(); 3483 } 3484 3485 /** Debug method to print children (in the partial order) recursively. */ 3486 public void debug_print_tree(Logger l, int indent, @Nullable PptRelation parent_rel) { 3487 3488 // Calculate the indentation 3489 String indent_str = ""; 3490 for (int i = 0; i < indent; i++) { 3491 indent_str += "-- "; 3492 } 3493 3494 // Get the type of the parent relation 3495 String rel_type = ""; 3496 if (parent_rel != null) { 3497 rel_type = parent_rel.getRelationType().toString(); 3498 } 3499 3500 // Calculate the variable relationships 3501 String var_rel = "[]"; 3502 if (parent_rel != null) { 3503 var_rel = "[" + parent_rel.parent_to_child_var_string() + "]"; 3504 } 3505 3506 // Put out this item 3507 l.fine( 3508 String.format( 3509 // Version that outputs the hash code too: 3510 // "%s %s [%s]: %s: %d: %s", 3511 // indent_str, ppt_name, System.identityHashCode(this), rel_type, num_samples(), 3512 // var_rel)); 3513 "%s %s: %s: %d: %s", indent_str, ppt_name, rel_type, num_samples(), var_rel)); 3514 3515 // Put out each slice. 3516 if (debugStdout) { 3517 for (Iterator<PptSlice> i = views_iterator(); i.hasNext(); ) { 3518 PptSlice cslice = i.next(); 3519 l.fine(indent_str + "++ " + cslice); 3520 for (VarInfo vi : cslice.var_infos) { 3521 assert vi.isCanonical() : vi; 3522 } 3523 } 3524 } 3525 3526 // Put out children if this is the primary relationship. Limiting 3527 // this to primary relations simplifies the tree for viewing while 3528 // not leaving anything out. 3529 if ((parent_rel == null) || parent_rel.is_primary() || (Daikon.ppt_regexp != null)) { 3530 for (Iterator<PptRelation> i = children.iterator(); i.hasNext(); ) { 3531 i.next().debug_print_tree(l, indent + 1); 3532 } 3533 } 3534 } 3535 3536 /** 3537 * Returns a string version of all of the equality sets for this ppt. The string is of the form 3538 * [a,b], [c,d] where a,b and c,d are each in an equality set. Should be used only for debugging. 3539 */ 3540 public String equality_sets_txt() { 3541 3542 if (equality_view == null) { 3543 return "null"; 3544 } 3545 3546 StringJoiner out = new StringJoiner(", "); 3547 for (Invariant inv : equality_view.invs) { 3548 Equality e = (Equality) inv; 3549 Set<VarInfo> vars = e.getVars(); 3550 StringJoiner set_str = new StringJoiner(","); 3551 for (VarInfo v : vars) { 3552 String name = v.name(); 3553 if (v.missingOutOfBounds()) { 3554 name += "{MOB}"; 3555 } 3556 set_str.add(name); 3557 } 3558 out.add("[" + set_str + "]"); 3559 } 3560 3561 return out.toString(); 3562 } 3563 3564 /** Returns whether or not the specified variable in this ppt has any parents. */ 3565 public boolean has_parent(VarInfo v) { 3566 3567 for (PptRelation rel : parents) { 3568 if (rel.parentVar(v) != null) { 3569 return true; 3570 } 3571 } 3572 3573 return false; 3574 } 3575 3576 /** 3577 * Recursively merge invariants from children to create an invariant list at this ppt. 3578 * 3579 * <p>First, equality sets are created for this ppt. These are the intersection of the equality 3580 * sets from each child. Then create unary, binary, and ternary slices for each combination of 3581 * equality sets and build the invariants for each slice. 3582 */ 3583 public void mergeInvs() { 3584 3585 if (Daikon.debugProgress.isLoggable(Level.FINER)) { 3586 // String hashCode = String.format(" [%s]", System.identityHashCode(this)); 3587 String hashCode = ""; 3588 Daikon.debugProgress.finer( 3589 String.format( 3590 "Merging ppt %s%s with %d children, %d parents, %d variables", 3591 name, hashCode, children.size(), parents.size(), var_infos.length)); 3592 } 3593 3594 // If we don't have any children, there is nothing to do. 3595 if (children.size() == 0) { 3596 assert equality_view != null : "children.size() == 0 and equality_view == null for " + this; 3597 return; 3598 } 3599 3600 // If this has already been done (because this ppt has multiple parents) 3601 // there is nothing to do. 3602 if (invariants_merged) { 3603 assert equality_view != null : this; 3604 return; 3605 } 3606 3607 in_merge = true; 3608 3609 // First do this for any children. 3610 for (PptRelation rel : children) { 3611 // System.out.printf("merging child %s[%s], its in_merge = %b%n", 3612 // rel.child, System.identityHashCode(rel.child), 3613 // rel.child.in_merge); 3614 if (!rel.child.in_merge) { 3615 rel.child.mergeInvs(); 3616 } 3617 } 3618 3619 if (debugMerge.isLoggable(Level.FINE)) { 3620 debugMerge.fine("Processing ppt " + name()); 3621 } 3622 3623 long startTime = System.nanoTime(); 3624 if (debugTimeMerge.isLoggable(Level.FINE)) { 3625 if (children.size() == 1) { 3626 debugTimeMerge.fine( 3627 "Timing merge of 1 child (" + children.get(0).child.name + " under ppt " + name); 3628 } else { 3629 debugTimeMerge.fine("Timing merge of " + children.size() + " children under ppt " + name); 3630 } 3631 } 3632 3633 // Number of samples here is the sum of all of the child samples, presuming 3634 // there are some variable relationships with the child (note that 3635 // some ppt relationships such as constructor ENTER ppts to their 3636 // object ppts do not have any variable relationships). 3637 for (PptRelation rel : children) { 3638 if (rel.size() > 0) { 3639 values_num_samples += rel.child.values_num_samples; 3640 } 3641 } 3642 3643 // Merge any always missing variables from the children 3644 if (DynamicConstants.dkconfig_use_dynamic_constant_optimization) { 3645 assert constants == null : this; 3646 constants = new DynamicConstants(this); 3647 constants.merge(); 3648 } 3649 3650 // Merge the ModBitTracker. 3651 // We'll reuse one dummy ValueTuple throughout, side-effecting its mods 3652 // array. 3653 if (debugStdout) { 3654 System.out.printf("in ppt %s%n", name()); 3655 System.out.printf(" num_tracevars = %d%n", num_tracevars); 3656 System.out.printf(" mbtracker.num_vars() = %d%n", mbtracker.num_vars()); 3657 for (int ii = 0; ii < var_infos.length; ii++) { 3658 System.out.printf( 3659 " Variable %s, index = %d%n", var_infos[ii], var_infos[ii].value_index); 3660 } 3661 } 3662 int num_tracevars = mbtracker.num_vars(); 3663 // warning: shadows field of same name 3664 @Nullable Object[] vals = new Object[num_tracevars]; 3665 int[] mods = new int[num_tracevars]; 3666 ValueTuple vt = ValueTuple.makeUninterned(vals, mods); 3667 for (PptRelation rel : children) { 3668 ModBitTracker child_mbtracker = rel.child.mbtracker; 3669 int child_mbsize = child_mbtracker.num_samples(); 3670 // System.out.println("mergeInvs child #" + children.indexOf(rel) + "=" + rel.child.name() + " 3671 // has size " + child_mbsize + " for " + name()); 3672 for (int sampno = 0; sampno < child_mbsize; sampno++) { 3673 Arrays.fill(mods, ValueTuple.MISSING_FLOW); 3674 for (int j = 0; j < var_infos.length; j++) { 3675 VarInfo parent_vi = var_infos[j]; 3676 VarInfo child_vi = rel.childVar(parent_vi); 3677 if ((child_vi != null) && (child_vi.value_index != -1)) { 3678 if (child_mbtracker.get(child_vi.value_index, sampno)) { 3679 mods[parent_vi.value_index] = ValueTuple.MODIFIED; 3680 } 3681 } 3682 } 3683 mbtracker.add(vt, 1); 3684 } 3685 } 3686 3687 // Merge the ValueSets. 3688 for (PptRelation rel : children) { 3689 3690 for (int j = 0; j < var_infos.length; j++) { 3691 VarInfo parent_vi = var_infos[j]; 3692 VarInfo child_vi = rel.childVar(parent_vi); 3693 if (child_vi != null) { 3694 assert parent_vi.ppt == this; 3695 if (parent_vi.value_index == -1) { 3696 continue; 3697 } 3698 ValueSet parent_vs = value_sets[parent_vi.value_index]; 3699 ValueSet child_vs = rel.child.value_sets[child_vi.value_index]; 3700 parent_vs.add(child_vs); 3701 } 3702 } 3703 } 3704 3705 // Merge information stored in the VarInfo objects themselves. 3706 // Currently just the "canBeMissing" field, which is needed by 3707 // guarding, and the flag that marks missing-out-of-bounds 3708 // derived variables 3709 for (PptRelation rel : children) { 3710 // This approach doesn't work correctly for the OBJECT_USER 3711 // relation case, because obj.field could be missing in a user PPT 3712 // when obj is null, but shouldn't be missing in the OBJECT PPT, 3713 // since "this" is always present for object invariants. 3714 // For the moment, just punt on this case, to match the previous 3715 // behavior. 3716 if (rel.getRelationType() == PptRelationType.USER) { 3717 continue; 3718 } 3719 for (int j = 0; j < var_infos.length; j++) { 3720 VarInfo parent_vi = var_infos[j]; 3721 VarInfo child_vi = rel.childVar(parent_vi); 3722 if (child_vi != null) { 3723 parent_vi.canBeMissing |= child_vi.canBeMissing; 3724 if (parent_vi.derived != null && child_vi.derived != null) { 3725 parent_vi.derived.missing_array_bounds |= child_vi.derived.missing_array_bounds; 3726 } 3727 } 3728 } 3729 } 3730 3731 // Create the (empty) equality view for this ppt 3732 assert (equality_view == null) : name() + ": " + equality_view; 3733 equality_view = new PptSliceEquality(this); 3734 3735 // Get all of the binary relationships from the first child's 3736 // equality sets. 3737 Map<VarInfo.Pair, VarInfo.Pair> equalityPairs = null; // a set of pairs, represented as a map 3738 int first_child = 0; // the index of the first child with num_samples() > 0 3739 for (first_child = 0; first_child < children.size(); first_child++) { 3740 PptRelation c1 = children.get(first_child); 3741 debugMerge.fine("looking at " + c1.child.name() + " " + c1.child.num_samples()); 3742 if (c1.child.num_samples() > 0) { 3743 // System.out.printf("First child equality set: %s%n", 3744 // c1.child.equality_view); 3745 equalityPairs = c1.get_child_equalities_as_parent(); 3746 if (debugMerge.isLoggable(Level.FINE)) { 3747 debugMerge.fine("Found equality pairs via " + c1); 3748 for (VarInfo.Pair vp : equalityPairs.keySet()) { 3749 debugMerge.fine("-- " + vp); 3750 } 3751 } 3752 break; 3753 } 3754 } 3755 if (equalityPairs == null) { 3756 equality_view.instantiate_invariants(); 3757 invariants_merged = true; 3758 in_merge = false; 3759 return; 3760 } 3761 3762 // Loop through the remaining children, intersecting the equal 3763 // variables and incrementing the sample count as we go. 3764 for (int i = first_child + 1; i < children.size(); i++) { 3765 PptRelation rel = children.get(i); 3766 if (rel.child.num_samples() == 0) { 3767 continue; 3768 } 3769 Map<VarInfo.Pair, VarInfo.Pair> eq_new = rel.get_child_equalities_as_parent(); 3770 // Cannot use foreach loop, due to desire to remove from equalityPairs. 3771 for (Iterator<VarInfo.@KeyFor("equalityPairs") Pair> j = equalityPairs.keySet().iterator(); 3772 j.hasNext(); ) { 3773 VarInfo.Pair curpair = j.next(); 3774 VarInfo.Pair newpair = eq_new.get(curpair); 3775 if (newpair == null) { 3776 // Equivalent to equalityPairs.remove(...), but that could throw a 3777 // ConcurrentModificationException, so must remove via the iterator. 3778 j.remove(); 3779 } else { 3780 curpair.samples += newpair.samples; 3781 } 3782 } 3783 } 3784 3785 // Build actual equality sets that match the pairs we found 3786 Set<VarInfo.Pair> equalityPairs_keySet = equalityPairs.keySet(); 3787 equality_view.instantiate_from_pairs(equalityPairs_keySet); 3788 if (debugMerge.isLoggable(Level.FINE)) { 3789 debugMerge.fine("Built equality sets "); 3790 for (Invariant inv : equality_view.invs) { 3791 Equality e = (Equality) inv; 3792 debugMerge.fine("-- " + e.shortString()); 3793 } 3794 } 3795 3796 // System.out.printf("New equality set = %s%n", equality_view); 3797 3798 if (debugTimeMerge.isLoggable(Level.FINE)) { 3799 long duration = System.nanoTime() - startTime; 3800 debugTimeMerge.fine( 3801 " equality sets etc time = " + TimeUnit.NANOSECONDS.toSeconds(duration) + "s"); 3802 startTime = System.nanoTime(); 3803 } 3804 3805 // Merge the invariants 3806 if (children.size() == 1) { 3807 merge_invs_one_child(); 3808 } else { 3809 merge_invs_multiple_children(); 3810 } 3811 3812 if (debugTimeMerge.isLoggable(Level.FINE)) { 3813 long duration = System.nanoTime() - startTime; 3814 debugTimeMerge.fine( 3815 " merge invariants time = " + TimeUnit.NANOSECONDS.toSeconds(duration) + "s"); 3816 startTime = System.nanoTime(); 3817 } 3818 3819 // Merge the conditionals 3820 merge_conditionals(); 3821 if (debugTimeMerge.isLoggable(Level.FINE)) { 3822 long duration = System.nanoTime() - startTime; 3823 debugTimeMerge.fine( 3824 " conditionals time = " + TimeUnit.NANOSECONDS.toSeconds(duration) + "s"); 3825 } 3826 3827 // Mark this ppt as merged, so we don't process it multiple times 3828 invariants_merged = true; 3829 in_merge = false; 3830 3831 // Remove any child invariants that now exist here 3832 if (dkconfig_remove_merged_invs) { 3833 for (PptRelation rel : children) { 3834 rel.child.remove_child_invs(rel); 3835 } 3836 } 3837 if (debugTimeMerge.isLoggable(Level.FINE)) { 3838 long duration = System.nanoTime() - startTime; 3839 debugTimeMerge.fine( 3840 " removing child invs time = " + TimeUnit.NANOSECONDS.toSeconds(duration) + "s"); 3841 } 3842 3843 // Remove the relations since we don't need it anymore 3844 if (dkconfig_remove_merged_invs) { 3845 for (PptRelation rel : children) { 3846 rel.child.parents.remove(rel); 3847 } 3848 children = new ArrayList<PptRelation>(0); 3849 } 3850 } 3851 3852 /** 3853 * Merges the invariants from multiple children. NI suppression is handled by first creating all 3854 * of the suppressed invariants in each of the children, performing the merge, and then removing 3855 * them. 3856 */ 3857 @SuppressWarnings("nullness:contracts.precondition") // private field 3858 @RequiresNonNull("equality_view") 3859 public void merge_invs_multiple_children() { 3860 3861 // Debug print ppt and children 3862 if (debugStdout) { 3863 System.out.printf("Merging invariants for ppt %s%n", this); 3864 for (PptRelation rel : children) { 3865 System.out.printf("child: %s%n", rel); 3866 } 3867 } 3868 3869 // There shouldn't be any slices when we start 3870 assert views.size() == 0; 3871 3872 // Create an array of leaders to build slices over 3873 List<VarInfo> non_missing_leaders = new ArrayList<>(equality_view.invs.size()); 3874 for (Invariant inv : equality_view.invs) { 3875 VarInfo l = ((Equality) inv).leader(); 3876 if (l.missingOutOfBounds()) { 3877 continue; 3878 } 3879 if (constants != null && constants.is_missing(l)) { 3880 // System.out.printf("skipping leader %s in ppt %s, always missing%n", 3881 // l, name()); 3882 continue; 3883 } 3884 non_missing_leaders.add(l); 3885 } 3886 VarInfo[] leaders = non_missing_leaders.toArray(new VarInfo[0]); 3887 3888 // Create any invariants in the children which are NI-suppressed and 3889 // remember the list for each child. The same ppt can be a child 3890 // more than once (with different variable relations), but we only 3891 // need to created the suppressed invariants once. 3892 Map<PptTopLevel, List<Invariant>> suppressed_invs = new LinkedHashMap<>(); 3893 for (PptRelation rel : children) { 3894 PptTopLevel child = rel.child; 3895 if (child.num_samples() == 0) { 3896 continue; 3897 } 3898 if (suppressed_invs.get(child) != null) { 3899 continue; 3900 } 3901 suppressed_invs.put(child, NIS.create_suppressed_invs(child)); 3902 } 3903 3904 // Create unary views and related invariants 3905 List<PptSlice> unary_slices = new ArrayList<>(); 3906 for (int i = 0; i < leaders.length; i++) { 3907 PptSlice1 slice1 = new PptSlice1(this, leaders[i]); 3908 slice1.merge_invariants(); 3909 unary_slices.add(slice1); 3910 } 3911 addSlices(unary_slices); 3912 if (debugMerge.isLoggable(Level.FINE)) { 3913 debug_print_slice_info(debugMerge, "unary", unary_slices); 3914 } 3915 3916 // Create binary views and related invariants 3917 List<PptSlice> binary_slices = new ArrayList<>(); 3918 for (int i = 0; i < leaders.length; i++) { 3919 for (int j = i; j < leaders.length; j++) { 3920 if (!is_slice_ok(leaders[i], leaders[j])) { 3921 continue; 3922 } 3923 PptSlice2 slice2 = new PptSlice2(this, leaders[i], leaders[j]); 3924 3925 slice2.merge_invariants(); 3926 if (slice2.invs.size() > 0) { 3927 binary_slices.add(slice2); 3928 } 3929 } 3930 } 3931 addSlices(binary_slices); 3932 if (debugMerge.isLoggable(Level.FINE)) { 3933 debug_print_slice_info(debugMerge, "binary", binary_slices); 3934 } 3935 3936 // Create ternary views and related invariants. Since there 3937 // are no ternary array invariants, those slices don't need to 3938 // be created. 3939 List<PptSlice> ternary_slices = new ArrayList<>(); 3940 for (int i = 0; i < leaders.length; i++) { 3941 if (leaders[i].rep_type.isArray()) { 3942 continue; 3943 } 3944 for (int j = i; j < leaders.length; j++) { 3945 if (leaders[j].rep_type.isArray()) { 3946 continue; 3947 } 3948 if (!leaders[i].compatible(leaders[j])) { 3949 continue; 3950 } 3951 for (int k = j; k < leaders.length; k++) { 3952 if (!is_slice_ok(leaders[i], leaders[j], leaders[k])) { 3953 continue; 3954 } 3955 PptSlice3 slice3 = new PptSlice3(this, leaders[i], leaders[j], leaders[k]); 3956 3957 slice3.merge_invariants(); 3958 3959 if (slice3.invs.size() > 0) { 3960 ternary_slices.add(slice3); 3961 } 3962 } 3963 } 3964 } 3965 addSlices(ternary_slices); 3966 if (debugMerge.isLoggable(Level.FINE)) { 3967 debug_print_slice_info(debugMerge, "ternary", ternary_slices); 3968 } 3969 3970 // Remove any merged invariants that are suppressed 3971 NIS.remove_suppressed_invs(this); 3972 3973 // Remove the NI suppressed invariants in the children that we 3974 // previously created 3975 for (Map.Entry<@KeyFor("suppressed_invs") PptTopLevel, List<Invariant>> entry : 3976 suppressed_invs.entrySet()) { 3977 PptTopLevel child = entry.getKey(); 3978 List<Invariant> suppressed_list = entry.getValue(); 3979 child.remove_invs(suppressed_list); 3980 } 3981 } 3982 3983 /** 3984 * Merges one child. Since there is only one child, the merge is trivial. Just copy each invariant 3985 * to the parent. 3986 */ 3987 public void merge_invs_one_child() { 3988 3989 if (debugStdout) { 3990 System.out.printf("merge_invs_one_child " + this); 3991 } 3992 3993 assert views.size() == 0; 3994 assert children.size() == 1; 3995 3996 PptRelation rel = children.get(0); 3997 3998 // Loop through each slice 3999 for (Iterator<PptSlice> i = rel.child.views_iterator(); i.hasNext(); ) { 4000 PptSlice cslice = i.next(); 4001 4002 // System.out.printf("Processing slice %s%n", cslice); 4003 4004 // Matching parent variable info. Skip this slice if there isn't a 4005 // match for each variable (such as with an enter-exit relation). 4006 VarInfo[] pvis = parent_vis(rel, cslice); 4007 if (pvis == null) { 4008 continue; 4009 } 4010 VarInfo[] pvis_sorted = pvis.clone(); 4011 Arrays.sort(pvis_sorted, VarInfo.IndexComparator.getInstance()); 4012 4013 // Create the parent slice 4014 PptSlice pslice; 4015 if (pvis.length == 1) { 4016 pslice = new PptSlice1(this, pvis_sorted[0]); 4017 } else if (pvis.length == 2) { 4018 pslice = new PptSlice2(this, pvis_sorted[0], pvis_sorted[1]); 4019 } else { 4020 pslice = new PptSlice3(this, pvis_sorted[0], pvis_sorted[1], pvis_sorted[2]); 4021 } 4022 addSlice(pslice); 4023 4024 // Build the permute from the child to the parent slice 4025 int[] permute = build_permute(pvis, pvis_sorted); 4026 4027 // Copy each child invariant to the parent 4028 for (Invariant child_inv : cslice.invs) { 4029 Invariant parent_inv = child_inv.clone_and_permute(permute); 4030 parent_inv.ppt = pslice; 4031 pslice.invs.add(parent_inv); 4032 if (Debug.logOn()) { 4033 parent_inv.log("Added %s to %s", parent_inv.format(), pslice); 4034 } 4035 } 4036 } 4037 } 4038 4039 /** 4040 * Creates a list of parent variables (i.e., variables at the parent program point) that matches 4041 * slice. Returns null if any of the variables don't have a corresponding parent variables. 4042 * 4043 * <p>The corresponding parent variable can match ANY of the members of an equality set. For 4044 * example, suppose that the child is EXIT with variable A, with equality set members {A, 4045 * orig(A)}; and suppose that this child is matched against ENTER. A does not have a relation 4046 * (since it is a post value), but orig(A) does have a relation. 4047 * 4048 * <p>Note that there are cases where this is not exactly correct. If you wanted to get all of the 4049 * invariants over A where A is an equality set with B, and A and B were in different equality 4050 * sets at the parent, the invariants true at A in the child are the union of those true at A and 4051 * B at the parent. 4052 */ 4053 public VarInfo @Nullable [] parent_vis(PptRelation rel, PptSlice slice) { 4054 4055 /*NNC:@MonotonicNonNull*/ VarInfo[] pvis = new VarInfo[slice.var_infos.length]; 4056 for (int j = 0; j < slice.var_infos.length; j++) { 4057 VarInfo sliceVar = slice.var_infos[j]; 4058 VarInfo cv = null; // child variable: a variable equal to sliceVar that has a parent 4059 VarInfo pv = null; // parent variable: cv's parent 4060 for (Iterator<VarInfo> k = sliceVar.equalitySet.getVars().iterator(); k.hasNext(); ) { 4061 cv = k.next(); 4062 pv = rel.parentVar(cv); 4063 if (pv != null) { 4064 break; 4065 } 4066 } 4067 if (pv == null) { 4068 return null; 4069 } 4070 assert cv != null : "@AssumeAssertion(nullness): if pv is non-null, cv must be non-null"; 4071 4072 // Make sure that the parent equality set is a subset of the child equality set. 4073 boolean assert_enabled = false; 4074 assert (assert_enabled = true); 4075 if (assert_enabled) { 4076 for (VarInfo test_pv : pv.equalitySet.getVars()) { 4077 @SuppressWarnings("nullness") 4078 @NonNull VarInfo test_cv = rel.childVar(test_pv); 4079 if (test_cv.canonicalRep() != cv.canonicalRep()) { 4080 System.out.println("pv.equalitySet = " + pv.equalitySet); 4081 System.out.println("cv.equalitySet = " + cv.equalitySet); 4082 throw new Error( 4083 "parent variable " 4084 + test_pv 4085 + " child " 4086 + test_cv 4087 + " is not in the same child equality set as " 4088 + cv); 4089 } 4090 } 4091 } 4092 if (!pv.isCanonical()) { 4093 pv = pv.canonicalRep(); 4094 } 4095 pvis[j] = pv; 4096 4097 // assert !pv.missingOutOfBounds(); 4098 } 4099 pvis = castNonNullDeep(pvis); // https://tinyurl.com/cfissue/986 4100 return pvis; 4101 } 4102 4103 /** 4104 * Merges the conditionals from the children of this ppt to this ppt. Only conditionals that exist 4105 * at each child and whose splitting condition is valid here can be merged. 4106 */ 4107 public void merge_conditionals() { 4108 4109 debugConditional.fine("attempting merge conditional for " + name()); 4110 4111 // If there are no children, there is nothing to do 4112 if (children.size() == 0) { 4113 return; 4114 } 4115 4116 // If there are no splitters there is nothing to do 4117 if (!has_splitters()) { 4118 return; 4119 } 4120 4121 if (debugConditional.isLoggable(Level.FINE)) { 4122 debugConditional.fine("Merge conditional for " + name()); 4123 for (PptRelation rel : children) { 4124 debugConditional.fine("child: " + rel); 4125 } 4126 } 4127 4128 // Merge the conditional points 4129 for (PptConditional ppt_cond : cond_iterable()) { 4130 if (debugConditional.isLoggable(Level.FINE)) { 4131 debugConditional.fine("Merge invariants for conditional " + ppt_cond.name()); 4132 for (PptRelation rel : ppt_cond.children) { 4133 debugConditional.fine("child relation: " + rel); 4134 debugConditional.fine("child equality set = " + rel.child.equality_sets_txt()); 4135 } 4136 } 4137 ppt_cond.mergeInvs(); 4138 debugConditional.fine("After merge, equality set = " + ppt_cond.equality_sets_txt()); 4139 } 4140 } 4141 4142 /** 4143 * Cleans up the ppt so that its invariants can be merged from other ppts. Not normally necessary 4144 * unless the merge is taking place over multiple ppts maps based on different data. This allows a 4145 * ppt to have its invariants recalculated. 4146 */ 4147 @SuppressWarnings("nullness") // reinitialization 4148 public void clean_for_merge() { 4149 equality_view = null; 4150 for (int i = 0; i < var_infos.length; i++) { 4151 var_infos[i].equalitySet = null; 4152 } 4153 views = new HashMap<>(); 4154 // parents = new ArrayList(); 4155 // children = new ArrayList(); 4156 invariants_merged = false; 4157 in_merge = false; 4158 constants = null; 4159 mbtracker = new ModBitTracker(mbtracker.num_vars()); 4160 remove_implications(); 4161 values_num_samples = 0; 4162 } 4163 4164 /** 4165 * Remove the equality invariants added during equality post processing. These are not over 4166 * leaders and can cause problems in some uses of the ppt. In particular, they cause problems 4167 * during merging. 4168 */ 4169 public void remove_equality_invariants() { 4170 4171 List<PptSlice> slices_to_remove = new ArrayList<>(); 4172 for (PptSlice slice : viewsAsCollection()) { 4173 if (slice.var_infos.length != 2) { 4174 continue; 4175 } 4176 if (slice.var_infos[0].isCanonical() && slice.var_infos[1].isCanonical()) { 4177 continue; 4178 } 4179 assert slice.var_infos[0].canonicalRep() == slice.var_infos[1].canonicalRep() : slice; 4180 slices_to_remove.add(slice); 4181 } 4182 for (PptSlice slice : slices_to_remove) { 4183 removeSlice(slice); 4184 } 4185 } 4186 4187 /** 4188 * Remove all of the implications from this program point. Can be used when recalculating 4189 * implications. Actually removes the entire joiner_view. 4190 */ 4191 public void remove_implications() { 4192 joiner_view = new PptSlice0(this); 4193 } 4194 4195 /** 4196 * Removes any invariant in this ppt which has a matching invariant in the parent (as specified in 4197 * the relation). Done to save space. Only safe when all processing of this child is complete 4198 * (i.e., all of the parents of this child must have been merged). 4199 * 4200 * <p>Another interesting problem arises with this code. As currently set up, it won't process 4201 * combined exit points (which often have two parents), but it will process enter points. Once the 4202 * enter point is removed, it can no longer parent filter the combined exit point. 4203 * 4204 * <p>Also, the dynamic obvious code doesn't work anymore (because it is missing the appropriate 4205 * invariants). This could be fixed by changing dynamic obvious to search up the tree (blecho!). 4206 * Fix this by only doing this for ppts whose parent only has one child. 4207 */ 4208 public void remove_child_invs(PptRelation rel) { 4209 4210 // For now, only do this for ppts with only one parent 4211 // if (parents.size() != 1) 4212 // return; 4213 4214 // Only do this for ppts whose children have also been removed 4215 for (PptRelation crel : children) { 4216 if (!crel.child.invariants_removed) { 4217 // System.out.println ("Rel " + rel + "has not had its child invs rm"); 4218 return; 4219 } 4220 } 4221 4222 // Only do this for ppts whose parent only has one child 4223 // if (rel.parent.children.size() != 1) 4224 // return; 4225 4226 System.out.println("Removing child invariants at " + name()); 4227 4228 List<PptSlice> slices_to_remove = new ArrayList<>(); 4229 4230 // Loop through each slice 4231 for (Iterator<PptSlice> i = views_iterator(); i.hasNext(); ) { 4232 PptSlice slice = i.next(); 4233 4234 // Build the varlist for the parent. If any variables are not present in 4235 // the parent, skip this slice 4236 VarInfo[] pvis = parent_vis(rel, slice); 4237 if (pvis == null) { 4238 continue; 4239 } 4240 VarInfo[] pvis_sorted = pvis.clone(); 4241 Arrays.sort(pvis_sorted, VarInfo.IndexComparator.getInstance()); 4242 4243 // Find the parent slice. If it doesn't exist, there is nothing to do 4244 PptSlice pslice = rel.parent.findSlice(pvis_sorted); 4245 if (pslice == null) { 4246 continue; 4247 } 4248 4249 // Build the permute from child to parent 4250 int[] permute = build_permute(pvis_sorted, pvis); 4251 4252 // Remove any invariant that is also present in the parent 4253 for (Iterator<Invariant> j = slice.invs.iterator(); j.hasNext(); ) { 4254 Invariant orig_inv = j.next(); 4255 Invariant inv = orig_inv.clone_and_permute(permute); 4256 Invariant pinv = pslice.find_inv_exact(inv); 4257 if (pinv != null) { 4258 j.remove(); 4259 // System.out.println ("Removed " + orig_inv + " @" + name() 4260 // + " parent inv " + pinv + " @" + rel.parent); 4261 } 4262 } 4263 4264 // If all of the invariants in a slice were removed, note it for removal 4265 if (slice.invs.size() == 0) { 4266 slices_to_remove.add(slice); 4267 } 4268 } 4269 4270 // Remove all of the slices with 0 invariants 4271 System.out.println(" Removed " + slices_to_remove.size() + " slices of " + numViews()); 4272 for (PptSlice slice : slices_to_remove) { 4273 // System.out.println ("Removing Slice " + slice); 4274 removeSlice(slice); 4275 } 4276 4277 invariants_removed = true; 4278 } 4279 4280 /** Builds a permutation from vis1 to vis2. The result is vis1[i] = vis2[permute[i]]. */ 4281 public static int[] build_permute(VarInfo[] vis1, VarInfo[] vis2) { 4282 4283 int[] permute = new int[vis1.length]; 4284 boolean[] matched = new boolean[vis1.length]; 4285 Arrays.fill(matched, false); 4286 4287 for (int j = 0; j < vis1.length; j++) { 4288 for (int k = 0; k < vis2.length; k++) { 4289 if ((vis1[j] == vis2[k]) && !matched[k]) { 4290 permute[j] = k; 4291 matched[k] = true; // don't match the same one twice 4292 break; 4293 } 4294 } 4295 } 4296 4297 // Check results 4298 for (int j = 0; j < vis1.length; j++) { 4299 assert vis1[j] == vis2[permute[j]]; 4300 } 4301 4302 return permute; 4303 } 4304 4305 /** Debug print slice/inv count information to the specified logger. */ 4306 public void debug_print_slice_info(Logger log, String descr, List<PptSlice> slices) { 4307 4308 int inv_cnt = 0; 4309 for (PptSlice slice : slices) { 4310 inv_cnt += slice.invs.size(); 4311 } 4312 log.fine(slices.size() + descr + " slices with " + inv_cnt + " invariants"); 4313 } 4314 4315 /** 4316 * Create an equality invariant over the specified variables. Samples should be the number of 4317 * samples for the slice over v1 and v2. The slice should not already exist. 4318 */ 4319 public PptSlice create_equality_inv(VarInfo v1, VarInfo v2, int samples) { 4320 4321 ProglangType rep = v1.rep_type; 4322 boolean rep_is_scalar = rep.isScalar(); 4323 boolean rep_is_float = rep.isFloat(); 4324 4325 assert findSlice_unordered(v1, v2) == null; 4326 PptSlice newSlice = get_or_instantiate_slice(v1, v2); 4327 4328 Invariant invEquals = null; 4329 4330 // This is almost directly copied from PptSlice2's instantiation 4331 // of factories 4332 if (rep_is_scalar) { 4333 invEquals = IntEqual.get_proto().instantiate(newSlice); 4334 } else if ((rep == ProglangType.STRING)) { 4335 invEquals = StringEqual.get_proto().instantiate(newSlice); 4336 } else if ((rep == ProglangType.INT_ARRAY)) { 4337 invEquals = SeqSeqIntEqual.get_proto().instantiate(newSlice); 4338 } else if ((rep == ProglangType.STRING_ARRAY)) { 4339 // JHP commented out to see what diffs are coming from here (5/3/3) 4340 // invEquals = SeqComparisonString.instantiate (newSlice, true); 4341 // if (invEquals != null) { 4342 // ((SeqComparisonString) invEquals).can_be_eq = true; 4343 // } 4344 // debugPostProcess.fine (" seqStringEqual"); 4345 } else if (rep_is_float) { 4346 invEquals = FloatEqual.get_proto().instantiate(newSlice); 4347 } else if (rep == ProglangType.DOUBLE_ARRAY) { 4348 invEquals = SeqSeqFloatEqual.get_proto().instantiate(newSlice); 4349 } 4350 4351 if (invEquals != null) { 4352 newSlice.addInvariant(invEquals); 4353 } else { 4354 if (newSlice.invs.size() == 0) { 4355 newSlice.parent.removeSlice(newSlice); 4356 } 4357 } 4358 return newSlice; 4359 } 4360 4361 /** Stores various statistics about a ppt. */ 4362 public static class Stats { 4363 4364 /** sample count. */ 4365 public int sample_cnt = 0; 4366 4367 /** number of equality sets. */ 4368 public int set_cnt = 0; 4369 4370 /** total number of variables in all equality sets. */ 4371 public int var_cnt = 0; 4372 4373 /** time (milliseconds) to process this sample. */ 4374 public int time = 0; 4375 4376 /** additional memory (bytes) allocated to processing this sample. */ 4377 public long memory = 0; 4378 4379 /** number of invariants. */ 4380 public int inv_cnt = 0; 4381 4382 /** number of slices. */ 4383 public int slice_cnt = 0; 4384 4385 /** number of instantiated invariants before the sample is applied. */ 4386 public int instantiated_inv_cnt = 0; 4387 4388 /** number of instantiated slices. */ 4389 public int instantiated_slice_cnt = 0; 4390 4391 /** program point of the stat. */ 4392 // Initialized by the set() method. 4393 public @MonotonicNonNull PptTopLevel ppt; 4394 4395 int const_slice_cnt = 0; 4396 int const_inv_cnt = 0; 4397 int constant_leader_cnt = 0; 4398 public static boolean cnt_inv_classes = false; 4399 // non-null if cnt_inv_classes is true 4400 @Nullable Map<Class<? extends Invariant>, Cnt> inv_map = null; 4401 public static boolean show_invs = false; 4402 public static boolean show_tern_slices = false; 4403 4404 /** 4405 * Sets each of the stats from the current info in ppt and the specified time (msecs) and memory 4406 * (bytes). 4407 */ 4408 @EnsuresNonNull("this.ppt") 4409 void set(PptTopLevel ppt, int time, int memory) { 4410 set_cnt = 0; 4411 var_cnt = 0; 4412 if (ppt.equality_view != null) { 4413 for (Invariant inv : ppt.equality_view.invs) { 4414 set_cnt++; 4415 Equality e = (Equality) inv; 4416 Collection<VarInfo> vars = e.getVars(); 4417 var_cnt += vars.size(); 4418 } 4419 } 4420 this.ppt = ppt; 4421 sample_cnt = ppt.num_samples(); 4422 slice_cnt = ppt.slice_cnt(); 4423 const_slice_cnt = ppt.const_slice_cnt(); 4424 const_inv_cnt = ppt.const_inv_cnt(); 4425 inv_cnt = ppt.invariant_cnt(); 4426 instantiated_slice_cnt = ppt.instantiated_slice_cnt; 4427 instantiated_inv_cnt = ppt.instantiated_inv_cnt; 4428 if (ppt.constants != null) { 4429 constant_leader_cnt = ppt.constants.constant_leader_cnt(); 4430 } 4431 this.time = time; 4432 this.memory = memory; 4433 4434 if (cnt_inv_classes) { 4435 inv_map = ppt.invariant_cnt_by_class(); 4436 } 4437 } 4438 4439 static void dump_header(Logger log) { 4440 4441 log.fine( 4442 "Program Point : Sample Cnt: Equality Cnt : Var Cnt : " 4443 + " Vars/Equality : Const Slice Cnt : " 4444 + " Slice / Inv Cnt : Instan Slice / Inv Cnt " 4445 + " Memory (bytes) : Time (msecs) "); 4446 } 4447 4448 @RequiresNonNull("ppt") 4449 void dump(Logger log) { 4450 4451 DecimalFormat dfmt = new DecimalFormat(); 4452 dfmt.setMaximumFractionDigits(2); 4453 dfmt.setGroupingSize(3); 4454 dfmt.setGroupingUsed(true); 4455 4456 double vars_per_eq = 0; 4457 if (set_cnt > 0) { 4458 vars_per_eq = (double) var_cnt / set_cnt; 4459 } 4460 4461 log.fine( 4462 ppt.name() 4463 + " : " 4464 + sample_cnt 4465 + " : " 4466 + set_cnt 4467 + " (" 4468 + constant_leader_cnt 4469 + " con) : " 4470 + var_cnt 4471 + " : " 4472 + dfmt.format(vars_per_eq) 4473 + " : " 4474 + const_slice_cnt 4475 + "/" 4476 + const_inv_cnt 4477 + " : " 4478 + slice_cnt 4479 + "/" 4480 + inv_cnt 4481 + " : " 4482 + instantiated_slice_cnt 4483 + "/" 4484 + instantiated_inv_cnt 4485 + " : " 4486 + memory 4487 + ": " 4488 + time); 4489 if (cnt_inv_classes) { 4490 assert inv_map != null : "@AssumeAssertion(nullness) : dependent: cnt_inv_classes is true"; 4491 for (Class<? extends Invariant> inv_class : inv_map.keySet()) { 4492 @SuppressWarnings("nullness") // limited side effects don't affect inv_map field 4493 Cnt cnt = inv_map.get(inv_class); 4494 log.fine(" : " + inv_class + ": " + cnt.cnt); 4495 } 4496 } 4497 4498 if (show_invs) { 4499 for (Iterator<PptSlice> j = ppt.views_iterator(); j.hasNext(); ) { 4500 PptSlice slice = j.next(); 4501 for (Invariant inv : slice.invs) { 4502 String falsify = ""; 4503 if (inv.is_false()) { 4504 falsify = "(falsified) "; 4505 } 4506 log.fine(" : " + falsify + inv.format()); 4507 } 4508 } 4509 } 4510 4511 if (show_tern_slices) { 4512 for (Iterator<PptSlice> j = ppt.views_iterator(); j.hasNext(); ) { 4513 PptSlice slice = j.next(); 4514 StringBuilder sb = new StringBuilder(); 4515 for (int k = 0; k < slice.arity(); k++) { 4516 VarInfo v = slice.var_infos[k]; 4517 sb.append( 4518 v.name() + "/" + v.equalitySet.getVars().size() + "/" + v.file_rep_type + " "); 4519 } 4520 log.fine(": " + sb.toString() + ": " + slice.invs.size()); 4521 } 4522 } 4523 } 4524 } 4525 4526 /** 4527 * Print statistics concerning equality sets over the entire set of ppts to the specified logger. 4528 */ 4529 public static void print_equality_stats(Logger log, PptMap all_ppts) { 4530 4531 if (!log.isLoggable(Level.FINE)) { 4532 return; 4533 } 4534 4535 boolean show_details = true; 4536 4537 NumberFormat dfmt = NumberFormat.getInstance(); 4538 dfmt.setMaximumFractionDigits(2); 4539 // double equality_set_cnt = 0; 4540 // double vars_cnt = 0; 4541 // double total_sample_cnt = 0; 4542 Map<PptTopLevel, List<Stats>> stats_map = Global.stats_map; 4543 4544 Stats.dump_header(debug); 4545 for (PptTopLevel ppt : all_ppts.pptIterable()) { 4546 List<Stats> slist = stats_map.get(ppt); 4547 if (slist == null) { 4548 continue; 4549 } 4550 int sample_cnt; 4551 int time = 0; 4552 double avg_equality_cnt = 0; 4553 double avg_var_cnt = 0; 4554 double avg_vars_per_equality = 0; 4555 double avg_inv_cnt = 0; 4556 int instantiated_inv_cnt = 0; 4557 int slice_cnt = 0; 4558 int instantiated_slice_cnt = 0; 4559 long memory = 0; 4560 sample_cnt = slist.size(); 4561 // total_sample_cnt += sample_cnt; 4562 for (Stats stats : slist) { 4563 avg_equality_cnt += stats.set_cnt; 4564 avg_var_cnt += stats.var_cnt; 4565 // equality_set_cnt += stats.set_cnt; 4566 // vars_cnt += stats.var_cnt; 4567 time += stats.time; 4568 avg_inv_cnt += stats.inv_cnt; 4569 slice_cnt += stats.slice_cnt; 4570 instantiated_inv_cnt += stats.instantiated_inv_cnt; 4571 instantiated_slice_cnt += stats.instantiated_slice_cnt; 4572 memory += stats.memory; 4573 } 4574 avg_equality_cnt = avg_equality_cnt / sample_cnt; 4575 avg_var_cnt = avg_var_cnt / sample_cnt; 4576 4577 if (avg_equality_cnt > 0) { 4578 avg_vars_per_equality = avg_var_cnt / avg_equality_cnt; 4579 } 4580 log.fine( 4581 ppt.name() 4582 + " : " 4583 + sample_cnt 4584 + " : " 4585 + dfmt.format(avg_equality_cnt) 4586 + " : " 4587 + dfmt.format(avg_var_cnt) 4588 + " : " 4589 + dfmt.format(avg_vars_per_equality) 4590 + " : " 4591 + dfmt.format((double) slice_cnt / sample_cnt) 4592 + "/" 4593 + dfmt.format(avg_inv_cnt / sample_cnt) 4594 + " : " 4595 + dfmt.format((double) instantiated_slice_cnt / sample_cnt) 4596 + "/" 4597 + dfmt.format((double) instantiated_inv_cnt / sample_cnt) 4598 + ": " 4599 + dfmt.format((double) memory / sample_cnt) 4600 + ": " 4601 + dfmt.format((double) time / sample_cnt)); 4602 if (show_details) { 4603 double avg_time = (double) time / sample_cnt; 4604 for (int j = 0; j < slist.size(); j++) { 4605 Stats stats = slist.get(j); 4606 double vars_per_eq = 0; 4607 if (stats.set_cnt > 0) { 4608 vars_per_eq = (double) stats.var_cnt / stats.set_cnt; 4609 } 4610 if ((j == (slist.size() - 1)) || (stats.time > (2 * avg_time))) { 4611 log.fine( 4612 " : " 4613 + j 4614 + " : " 4615 + stats.set_cnt 4616 + " : " 4617 + stats.var_cnt 4618 + " : " 4619 + dfmt.format(vars_per_eq) 4620 + " : " 4621 + stats.slice_cnt 4622 + "/" 4623 + stats.inv_cnt 4624 + " : " 4625 + stats.instantiated_slice_cnt 4626 + "/" 4627 + stats.instantiated_inv_cnt 4628 + " : " 4629 + stats.memory 4630 + ": " 4631 + stats.time); 4632 } 4633 } 4634 } 4635 } 4636 } 4637 4638 /** sets the sample count. */ 4639 void set_sample_number(int val) { 4640 values_num_samples = val; 4641 } 4642 4643 /** Increments the number of samples processed by the program point by 1. */ 4644 public void incSampleNumber() { 4645 values_num_samples++; 4646 } 4647 4648 /** Is this is an exit ppt (combined or specific)? */ 4649 @Pure 4650 public boolean is_exit() { 4651 if (type != null) { 4652 return (type == PptType.EXIT) || (type == PptType.SUBEXIT); 4653 } else { 4654 return ppt_name.isExitPoint(); 4655 } 4656 } 4657 4658 /** 4659 * Returns true if this is an enter ppt. 4660 * 4661 * @return true if this is an enter ppt 4662 */ 4663 @Pure 4664 public boolean is_enter() { 4665 if (type != null) { 4666 return (type == PptType.ENTER); 4667 } else { 4668 return ppt_name.isEnterPoint(); 4669 } 4670 } 4671 4672 /** Is this a combined exit point? */ 4673 @Pure 4674 public boolean is_combined_exit() { 4675 if (type != null) { 4676 return (type == PptType.EXIT); 4677 } else { 4678 return ppt_name.isCombinedExitPoint(); 4679 } 4680 } 4681 4682 /** Is this a numbered (specific) exit point? */ 4683 @Pure 4684 public boolean is_subexit() { 4685 if (type != null) { 4686 return (type == PptType.SUBEXIT); 4687 } else { 4688 return ppt_name.isExitPoint() && !ppt_name.isCombinedExitPoint(); 4689 } 4690 } 4691 4692 /** Is this a ppt that represents an object? */ 4693 @Pure 4694 public boolean is_object() { 4695 if (type != null) { 4696 return (type == PptType.OBJECT); 4697 } else { 4698 return ppt_name.isObjectInstanceSynthetic(); 4699 } 4700 } 4701 4702 /** Is this a ppt that represents a class? */ 4703 @EnsuresNonNullIf(result = true, expression = "type") 4704 @Pure 4705 public boolean is_class() { 4706 return (type != null && type == PptType.CLASS); 4707 } 4708 4709 public String var_names() { 4710 return Arrays.toString(var_infos); 4711 } 4712}