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