001// ***** This file is automatically generated from PptSlice.java.jpp 002 003package daikon; 004 005import static daikon.tools.nullness.NullnessUtil.castNonNullDeep; 006 007import daikon.inv.*; 008 009import daikon.inv.ternary.*; 010import daikon.inv.ternary.threeScalar.*; 011 012import daikon.suppress.*; 013import java.util.*; 014import java.util.logging.Level; 015import java.util.logging.Logger; 016import org.checkerframework.checker.initialization.qual.UnknownInitialization; 017import org.checkerframework.checker.interning.qual.Interned; 018import org.checkerframework.checker.lock.qual.GuardSatisfied; 019import org.checkerframework.checker.nullness.qual.MonotonicNonNull; 020import org.checkerframework.checker.nullness.qual.NonNull; 021import org.plumelib.util.ArraysPlume; 022import org.plumelib.util.Intern; 023import typequals.prototype.qual.Prototype; 024import typequals.prototype.qual.NonPrototype; 025 026/** Contains all of the invariants over a particular set of 3 variables. */ 027public final class PptSlice3 extends PptSlice { 028 // We are Serializable, so we specify a version to allow changes to 029 // method signatures without breaking serialization. If you add or 030 // remove fields, you should change this number to the current date. 031 static final long serialVersionUID = 20040921L; 032 033 /** Debug tracer. */ 034 public static final Logger debugSpecific = Logger.getLogger("daikon.PptSlice3"); 035 036 public static final Logger debugMerge = Logger.getLogger("daikon.PptSlice.merge"); 037 038 /** Create a new PptSlice3. The var_infos must be in varinfo_index order. */ 039 public PptSlice3(PptTopLevel parent, VarInfo[] var_infos) { 040 041 super(parent, var_infos); 042 assert var_infos.length == 3; 043 044 if (debug.isLoggable(Level.FINE) || debugSpecific.isLoggable(Level.FINE)) { 045 debug.info("Created PptSlice3 " + this.name()); 046 } 047 if (Debug.logOn()) { 048 Debug.log(getClass(), this, "Created"); 049 } 050 } 051 052 PptSlice3(PptTopLevel parent, VarInfo var_info1, VarInfo var_info2, VarInfo var_info3) { 053 this(parent, new VarInfo[] {var_info1, var_info2, var_info3}); 054 } 055 056 @Override 057 public final int arity( 058 @UnknownInitialization(PptSlice.class) PptSlice3 this) { 059 return 3; 060 } 061 /** 062 * Creates all of the invariants that are appropriate for this slice. No invariants are 063 * created unless the variables in the slice are compatible. If the variables are compatible, 064 * invariants that match the type of the slices variables are created. 065 */ 066 @Override 067 public void instantiate_invariants() { 068 instantiate_invariants(Daikon.proto_invs); 069 } 070 071 /** 072 * Creates all of the invariants that are appropriate for this slice based on the list of 073 * invariants passed in. No invariants are created unless the variables in the slice are 074 * compatible. If the variables are compatible, invariants that match the type of the slices 075 * variables are created. 076 */ 077 public void instantiate_invariants(List<@Prototype Invariant> proto_invs) { 078 079 if (Debug.logOn()) { 080 log("instantiate invariants"); 081 } 082 083 // Do nothing if the variables aren't compatible 084 085 VarInfo v1 = var_infos[0]; 086 VarInfo v2 = var_infos[1]; 087 VarInfo v3 = var_infos[2]; 088 if (!v1.compatible(v2)) { 089 return; 090 } 091 if (!v2.compatible(v3)) { 092 return; 093 } 094 assert v1.compatible(v3); 095 096 // Instantiate each invariant that is valid over those types 097 for (@Prototype Invariant proto : proto_invs) { 098 099 // Skip invariant if the types are not appropriate 100 if (!proto.valid_types(var_infos) || !proto.instantiate_ok(var_infos)) { 101 // Debug.log (proto.getClass(), this, "not created-types not valid"); 102 continue; 103 } 104 105 // Skip invariant if it is suppressed. Note that this will work 106 // even though we haven't instantiated all of the invariants for this 107 // slice yet because it will check constant values. 108 NISuppressionSet ss = proto.get_ni_suppressions(); 109 if (NIS.dkconfig_enabled && (ss != null) && !ss.is_instantiate_ok(this)) { 110 if (Debug.logOn()) // avoid stringify if not logging 111 Debug.log(proto.getClass(), this, "not created - suppressed " + ss); 112 continue; 113 } 114 115 // Instantiate the invariant and add it to the list. Null should 116 // never be returned because we check instantiate_ok() above and 117 // only enabled invariants are in this list. 118 @SuppressWarnings("nullness") // application invariant, see comment above 119 @NonNull Invariant inv = proto.instantiate(this); 120 addInvariant(inv); 121 if (Debug.logOn()) { 122 inv.log("Created invariant %s ss = %s", inv.format(), ss); 123 } 124 } 125 } 126 127 // These accessors are for abstract methods declared in Ppt 128 /** Returns the number of (non-missing) samples observed at this slice. */ 129 @Override 130 public int num_samples(@UnknownInitialization @GuardSatisfied PptSlice3 this) { 131 if (parent == null || var_infos == null) { // handle not-yet-initialized slices 132 return 0; 133 } 134 // return an approximation 135 136 int num_slice_samples = parent.num_samples(var_infos[0], var_infos[1], 137 var_infos[2]); 138 139 return num_slice_samples; 140 } 141 142 /** 143 * Returns an upper bound on the number of distinct values observed at this slice. This is not the 144 * number of samples observed. 145 */ 146 @Override 147 public int num_values() { 148 // return an approximation 149 150 int num_values = parent.num_values(var_infos[0], var_infos[1], 151 var_infos[2]); 152 153 return num_values; 154 } 155 156 /** 157 * This procedure accepts a sample (a ValueTuple), extracts the values from it, casts them to the 158 * proper types, and passes them along to the invariants proper. (The invariants accept typed 159 * values rather than a ValueTuple that encapsulates objects of any type whatever.) 160 */ 161 @Override 162 public List<Invariant> add(ValueTuple full_vt, int count) { 163 164 assert invs.size() > 0; 165 for (Invariant inv : invs) { 166 assert inv != null; 167 } 168 169 VarInfo vi1 = var_infos[0]; 170 VarInfo vi2 = var_infos[1]; 171 VarInfo vi3 = var_infos[2]; 172 173 // If any var has encountered out of array bounds values, 174 // stop all invariants in this slice. The presumption here is that 175 // an index out of bounds implies that the derived variable (eg a[i]) 176 // doesn't really make any sense (essentially that i is not a valid 177 // index for a). Invariants on the derived variable are thus not 178 // relevant 179 for (int i = 0; i < var_infos.length; i++) { 180 if (var_infos[i].missingOutOfBounds()) { 181 List<Invariant> result = new ArrayList<>(); 182 for (Invariant inv : invs) { 183 if (PrintInvariants.print_discarded_invariants) { 184 DiscReasonMap.put( 185 inv, 186 DiscardCode.bad_sample, 187 var_infos[i].name() + " array index was out of bounds"); 188 } 189 inv.falsify(); 190 result.add(inv); 191 if (Invariant.logOn()) { 192 inv.log("destroyed because %s array index out of bounds", var_infos[i].name()); 193 } 194 } 195 if (VarInfo.debugMissing.isLoggable(Level.FINE)) { 196 VarInfo.debugMissing.fine( 197 "Removing slice " 198 + this 199 + " because var " 200 + var_infos[i].name() 201 + " array index out of bounds"); 202 } 203 return result; 204 } 205 } 206 207 int mod1 = full_vt.getModified(vi1); 208 if (mod1 == ValueTuple.MISSING_FLOW || mod1 == ValueTuple.MISSING_NONSENSICAL) { 209 return emptyInvList; 210 } 211 212 if (mod1 == ValueTuple.STATIC_CONSTANT) { 213 assert vi1.is_static_constant; 214 mod1 = ((num_samples() == 0) ? ValueTuple.MODIFIED : ValueTuple.UNMODIFIED); 215 } 216 217 int mod2 = full_vt.getModified(vi2); 218 if (mod2 == ValueTuple.MISSING_FLOW || mod2 == ValueTuple.MISSING_NONSENSICAL) { 219 return emptyInvList; 220 } 221 if (mod2 == ValueTuple.STATIC_CONSTANT) { 222 assert vi2.is_static_constant; 223 mod2 = ((num_samples() == 0) 224 ? ValueTuple.MODIFIED : ValueTuple.UNMODIFIED); 225 } 226 227 int mod3 = full_vt.getModified(vi3); 228 if (mod3 == ValueTuple.MISSING_FLOW || mod3 == ValueTuple.MISSING_NONSENSICAL) { 229 return emptyInvList; 230 } 231 if (mod3 == ValueTuple.STATIC_CONSTANT) { 232 assert vi3.is_static_constant; 233 mod3 = ((num_samples() == 0) ? ValueTuple.MODIFIED : ValueTuple.UNMODIFIED); 234 } 235 236 Object val1 = full_vt.getValue(vi1); 237 assert Intern.isInterned(val1) : "obj " + val1 + " class " + val1.getClass(); 238 239 Object val2 = full_vt.getValue(vi2); 240 assert Intern.isInterned(val2); 241 242 Object val3 = full_vt.getValue(vi3); 243 assert Intern.isInterned(val3); 244 245 // Supply the new values to all the invariant objects. 246 assert (mod1 == vi1.getModified(full_vt)) 247 || ((vi1.getModified(full_vt) == ValueTuple.STATIC_CONSTANT) 248 && ((mod1 == ValueTuple.UNMODIFIED) || (mod1 == ValueTuple.MODIFIED))); 249 250 List<Invariant> weakened_invs = add_val_bu(val1, val2, val3, mod1, mod2, 251 mod3, count); 252 253 return weakened_invs; 254 } 255 256 public List<Invariant> add_val_bu(@Interned Object val1, @Interned Object val2, @Interned Object val3, 257 int mod1, int mod2, int mod3, int count) { 258 259 assert (mod1 != ValueTuple.MISSING_FLOW 260 && mod1 != ValueTuple.MISSING_NONSENSICAL) 261 && (mod2 != ValueTuple.MISSING_FLOW 262 && mod2 != ValueTuple.MISSING_NONSENSICAL) 263 && (mod3 != ValueTuple.MISSING_FLOW 264 && mod3 != ValueTuple.MISSING_NONSENSICAL); 265 266 List<Invariant> result = new ArrayList<>(); 267 for (Invariant invariant : invs) { 268 TernaryInvariant inv = (TernaryInvariant) invariant; 269 if (inv.is_false()) { 270 continue; 271 } 272 InvariantStatus status = inv.add(val1, val2, val3, mod1, count); 273 if (status == InvariantStatus.FALSIFIED) { 274 inv.falsify(); 275 result.add(inv); 276 } else if (status == InvariantStatus.WEAKENED) { 277 result.add(inv); 278 } 279 if (PrintInvariants.print_discarded_invariants && inv.is_false()) { 280 // Currently there are no ternary invariants with arrays, but if 281 // there are in the future, I don't want this to break. 282 DiscReasonMap.put(inv, DiscardCode.bad_sample, 283 "Falsified from sample: " + var_infos[0].name() + " = " 284 + Debug.toString(val1) 285 + "," + var_infos[1].name() + " = " 286 + Debug.toString(val2) 287 + "," + var_infos[2].name() + " = " 288 + Debug.toString(val3)); 289 } 290 } 291 return result; 292 } 293 294 @Override 295 public void addInvariant(Invariant invariant) { 296 assert invariant != null; 297 // assert invariant.ppt == this; 298 299 if (Debug.dkconfig_internal_check) { 300 // Don't add a check here to ensure that the invairant is not suppressed 301 // in some cases (see NIS.apply_samples), a suppressed invariant is 302 // added and them later removed when the suppression is found 303 // if (invariant.is_ni_suppressed()) { 304 // System.out.printf("suppressed invariant %s is being added to ppt %s " 305 // + "with %d samples%n", invariant.format(), this, 306 // this.num_samples()); 307 // NISuppressionSet ss = invariant.get_ni_suppressions(); 308 // ss.suppressed (invariant.ppt); 309 // System.out.printf("suppression = %s%n", ss); 310 // throw new Error(); 311 // } 312 } 313 314 invs.add(invariant); 315 Global.instantiated_invariants++; 316 if (Invariant.logOn()) { 317 invariant.log("Instantiated %s", invariant.format()); 318 } 319 } 320 321 /** 322 * Copy invariants from this slice to a new slice over the variables argNewVarInfos. The new slice 323 * should not already exist. 324 */ 325 @Override 326 protected PptSlice cloneAndPivot(VarInfo[] argNewVarInfos) { 327 328 // Sort the VarInfos by var_index and build a matching permutation 329 // from the current order to the new order 330 VarInfo[] vis_sorted = argNewVarInfos.clone(); 331 Arrays.sort(vis_sorted, VarInfo.IndexComparator.getInstance()); 332 int[] permutation = PptTopLevel.build_permute(argNewVarInfos, vis_sorted); 333 334 // Assert sorted 335 for (int i = 0; i < 3 - 1; i++) { 336 assert vis_sorted[i].varinfo_index <= vis_sorted[i + 1].varinfo_index; 337 } 338 339 assert ArraysPlume.fnIsPermutation(permutation); 340 // Assert that the permutation represents the rearrangement 341 for (int i = 0; i < 3; i++) { 342 // the variable that used to be at position "i" is now found at 343 // position permutation[i]. 344 VarInfo oldvi = argNewVarInfos[i]; 345 VarInfo newvi = vis_sorted[permutation[i]]; 346 assert oldvi == newvi; 347 } 348 349 // The new slice should not already exist. 350 assert parent.findSlice(vis_sorted) == null; 351 352 // Why not just clone? Because then index order wouldn't be 353 // preserved 354 PptSlice3 result = new PptSlice3(this.parent, vis_sorted); 355 356 // re-parent the invariants and copy them out. 357 List<Invariant> newInvs = new ArrayList<>(); 358 for (Invariant inv : invs) { 359 assert inv.ppt == this; 360 Invariant newInv = inv.transfer(result, permutation); 361 newInvs.add(newInv); 362 assert newInv != inv; 363 assert newInv.ppt == result; 364 assert inv.ppt == this; 365 } 366 367 if (Debug.logOn()) { 368 result.log( 369 "Copied " 370 + newInvs.size() 371 + " invariants from " 372 + this.name() 373 + " with " 374 + invs.size() 375 + " invariants"); 376 } 377 result.invs.addAll(newInvs); 378 if (PptSliceEquality.debug.isLoggable(Level.FINE)) { 379 PptSliceEquality.debug.fine("cloneAndPivot: newInvs " + invs); 380 } 381 return result; 382 } 383 384 /** 385 * Creates invariants at this ppt by merging invariants from each of its children. An invariant 386 * must exist at each of the children in order for it to be created here (at the parent). 387 * Additionally, some invariants have state information that must be merged. This is done by the 388 * invariant itself. 389 * 390 * <p>The basic steps are: 391 * 392 * <ol> 393 * <li>Find all of the child invariants. These are the invariants in the matching slice of each 394 * child. 395 * <li>For each invariant class, build a list of all of the invariants of that class. Note that 396 * some invariant classes (eg, functionBinary) contain distinct invariants, each of which 397 * must be merged separately. See Invariant.Match for more information concerning what makes 398 * an invariant the 'same' 399 * <li>Each invariant that is found at each of the children is then merged to possibly create a 400 * parent invariant. 401 * </ol> 402 */ 403 public void merge_invariants() { 404 405 if (debugMerge.isLoggable(Level.FINE)) { 406 debugMerge.fine("merging invs for " + name()); 407 } 408 409 // List of all invariants found over all of the children 410 List<Invariant> all_invs = new ArrayList<>(); 411 412 // Keep count of the number of valid children processed. An invariant 413 // must be found at each valid child in order to exist at the parent. 414 // A valid child is one that has received samples and has a corresponding 415 // variable for each parent variable 416 int valid_child_count = 0; 417 418 // Loop through all of the children of our top level parent 419 child_loop: 420 for (PptRelation rel : parent.children) { 421 PptTopLevel ppt = rel.child; 422 423 // Skip any children that have not seen any samples 424 if (ppt.num_samples() == 0) { 425 if (debugMerge.isLoggable(Level.FINE)) { 426 debugMerge.fine("-- slice ignored (no samples) " + ppt.name()); 427 } 428 continue; 429 } 430 431 // Child variable info 432 /*NNC:@MonotonicNonNull*/ VarInfo[] cvis = new VarInfo[var_infos.length]; 433 /*NNC:@MonotonicNonNull*/ VarInfo[] cvis_sorted = new VarInfo[var_infos.length]; 434 435 // Build the corresponding array of VarInfos for the child. If any 436 // of the vars don't exist in this child, skip the child (since we 437 // won't have data for each variable). 438 for (int j = 0; j < var_infos.length; j++) { 439 VarInfo pv = var_infos[j]; 440 VarInfo cv = rel.childVar(pv); 441 if (cv == null) { 442 continue child_loop; 443 } 444 cvis[j] = cv.canonicalRep(); 445 cvis_sorted[j] = cv.canonicalRep(); 446 } 447 448 cvis = castNonNullDeep(cvis); // https://tinyurl.com/cfissue/986 449 cvis_sorted = castNonNullDeep(cvis_sorted); // https://tinyurl.com/cfissue/986 450 451 // If any of the child variables have always been missing, this 452 // particular slice in the child received no samples. If dynamic 453 // constants are enabled, the slice will have never been created. 454 // These slices can be skipped unless they contain a missing out of 455 // bound var. Out of bounds variables destroy all invariants in 456 // the slice (since the variable is deemed to be nonsensical) 457 if (slice_missing(ppt, cvis)) { 458 if (debugMerge.isLoggable(Level.FINE)) { 459 debugMerge.fine( 460 "-- slice ignored (missing) " + ppt.name() + " vars " + Arrays.toString(cvis_sorted)); 461 } 462 continue; 463 } 464 465 // The child variables must be sorted by their index (in the child) 466 Arrays.sort(cvis_sorted, VarInfo.IndexComparator.getInstance()); 467 468 // Keep track of the number of valid children 469 valid_child_count++; 470 471 // Find the corresponding slice. If the slice does not exist or 472 // has no invariants, there can be no invariants to merge (since 473 // invariants must exist at each child to exist at the parent) 474 PptSlice3 cslice = (PptSlice3) ppt.findSlice(cvis_sorted); 475 if ((cslice == null) || (cslice.invs.size() == 0)) { 476 if (Debug.logOn()) { 477 this.log( 478 "slice not found " 479 + ppt.name() 480 + " " 481 + Arrays.toString(cvis_sorted) 482 + " num_samples= " 483 + ppt.num_samples() 484 + " ppt.constants = " 485 + ppt.constants); 486 } 487 if (debugMerge.isLoggable(Level.FINE)) { 488 debugMerge.fine( 489 "-- slice not found " + ppt.name() + " vars " + Arrays.toString(cvis_sorted)); 490 } 491 return; 492 } 493 494 // // Update sample count info 495 // mod_samples += cslice.mod_samples; 496 // unmod_samples += cslice.unmod_samples; 497 498 // Build the permutation array from child to parent slice 499 int[] permute = PptTopLevel.build_permute(cvis_sorted, cvis); 500 501 // Debug print child vars and permute to parent 502 if (debugMerge.isLoggable(Level.FINE)) { 503 debugMerge.fine("-- Processing child " + ppt.name() + " (" + rel.getRelationType() + ")"); 504 debugMerge.fine("-- -- child vars = " + Arrays.toString(cvis_sorted)); 505 debugMerge.fine("-- -- parent vars = " + Arrays.toString(var_infos)); 506 debugMerge.fine("-- -- permute = " + Arrays.toString(permute)); 507 } 508 509 // Add each invariant (permuted to match the parent varinfos) 510 // to our list of invariants. 511 for (Invariant orig_inv : cslice.invs) { 512 Invariant inv = orig_inv.clone_and_permute(permute); 513 all_invs.add(inv); 514 if (Invariant.logOn()) { 515 /*NNC:@MonotonicNonNull*/ VarInfo[] child_vars = new VarInfo[var_infos.length]; 516 for (int k = 0; k < var_infos.length; k++) { 517 VarInfo pv = var_infos[k]; 518 @SuppressWarnings("nullness") 519 @NonNull VarInfo cv = rel.childVar(pv); 520 assert cv != null; 521 child_vars[k] = cv.canonicalRep(); 522 } 523 child_vars = castNonNullDeep(child_vars); // https://tinyurl.com/cfissue/986 524 orig_inv.log("org inv"); 525 inv.log( 526 "Created %s from %s using permute %s cvis_sorted = %s cvis = %s for ppt %s", 527 inv, 528 orig_inv, 529 Arrays.toString(permute), 530 Arrays.toString(cvis_sorted), 531 Arrays.toString(child_vars), 532 parent.name()); 533 } 534 } 535 } 536 537 log("Found " + all_invs.size() + " invariants to merge"); 538 if (debugMerge.isLoggable(Level.FINE) && (valid_child_count == 0)) { 539 debugMerge.fine("-- No valid children found"); 540 } 541 542 // For each invariant found, find the list of invariants of the 543 // same type (type corresponds basically but not exactly to the 544 // invariants class) and add the invariant to that list. 545 // Invariant.Match.equals() defines if two invariants are of the 546 // same 'type' for the purpose of merging invariants. 547 Map<Invariant.Match, List<Invariant>> inv_map = 548 new LinkedHashMap<>(); 549 for (Invariant inv : all_invs) { 550 Invariant.Match imatch = new Invariant.Match(inv); 551 List<Invariant> invs = inv_map.get(imatch); 552 if (Invariant.logOn()) { 553 inv.log("Adding %s to %s invs list %s", inv.format(), name(), invs); 554 } 555 if (invs == null) { 556 invs = new ArrayList<Invariant>(); 557 inv_map.put(imatch, invs); 558 } 559 invs.add(inv); 560 } 561 562 // Attempt to create a parent invariant for each invariant that 563 // appeared at each valid child. Note that some invariants will 564 // not exist at the parent even if they exist at each child (eg, 565 // LinearBinary) 566 for (List<Invariant> child_invs : inv_map.values()) { 567 if (child_invs.size() > valid_child_count) { 568 // this shouldn't happen 569 System.out.println( 570 "Found " 571 + child_invs.size() 572 + " invariants at " 573 + name() 574 + " (" 575 + valid_child_count 576 + " children)"); 577 for (Invariant child_inv : child_invs) { 578 System.out.printf( 579 "-- Invariant = '%s' [%s] @%s%n", 580 child_inv.repr(), child_inv.getClass(), child_inv.ppt); 581 } 582 assert child_invs.size() <= valid_child_count; 583 } 584 if (child_invs.size() == valid_child_count) { 585 Invariant first = child_invs.get(0); 586 if (Debug.logOn()) { 587 first.log("Attempting merge of %s invariants into ppt %s", child_invs.size(), name()); 588 } 589 Invariant parent_inv = first.merge(child_invs, this); 590 if (parent_inv != null) { 591 invs.add(parent_inv); 592 if (Debug.logOn()) { 593 parent_inv.log("Merge successful of %s into %s", parent_inv.format(), name()); 594 } 595 } 596 } else { 597 if (Debug.logOn()) { 598 Invariant inv = child_invs.get(0); 599 inv.log( 600 "Not merging invariant into %s, Found %s child invariants in %s children", 601 name(), child_invs.size(), valid_child_count); 602 } 603 } 604 } 605 } 606 607 /** 608 * Returns whether or not the slice is missing due to having one or more of its variables always 609 * missing. This returns true only for missing flow and/or missing nonsensical. Out of Bounds is 610 * treated differently since it destroys all of its invariants. 611 */ 612 private boolean slice_missing(PptTopLevel ppt, VarInfo[] vis) { 613 614 if (ppt.constants != null) { 615 616 if ((ppt.constants.is_missing(vis[0]) 617 || ppt.constants.is_missing(vis[1]) 618 || ppt.constants.is_missing(vis[2])) 619 && !vis[0].missingOutOfBounds() 620 && !vis[1].missingOutOfBounds() 621 && !vis[2].missingOutOfBounds()) { 622 return true; 623 } 624 625 } 626 return false; 627 } 628}