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