001package daikon.inv; 002 003import static daikon.tools.nullness.NullnessUtil.castNonNullDeep; 004 005import daikon.Daikon; 006import daikon.Debug; 007import daikon.FileIO; 008import daikon.PptSlice; 009import daikon.PptSlice1; 010import daikon.PptSlice2; 011import daikon.PrintInvariants; 012import daikon.ValueTuple; 013import daikon.VarComparability; 014import daikon.VarComparabilityImplicit; 015import daikon.VarInfo; 016import daikon.inv.binary.BinaryInvariant; 017import daikon.inv.filter.InvariantFilters; 018import daikon.inv.ternary.TernaryInvariant; 019import daikon.inv.unary.OneOf; 020import daikon.inv.unary.UnaryInvariant; 021import daikon.simplify.LemmaStack; 022import daikon.simplify.SimpUtil; 023import daikon.suppress.NISuppressionSet; 024import java.io.Serializable; 025import java.util.ArrayList; 026import java.util.Arrays; 027import java.util.Comparator; 028import java.util.List; 029import java.util.logging.Level; 030import java.util.logging.Logger; 031import java.util.regex.Pattern; 032import org.checkerframework.checker.formatter.qual.FormatMethod; 033import org.checkerframework.checker.initialization.qual.UnknownInitialization; 034import org.checkerframework.checker.interning.qual.UsesObjectEquals; 035import org.checkerframework.checker.lock.qual.GuardSatisfied; 036import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf; 037import org.checkerframework.checker.nullness.qual.Nullable; 038import org.checkerframework.checker.signedness.qual.UnknownSignedness; 039import org.checkerframework.dataflow.qual.Pure; 040import org.checkerframework.dataflow.qual.SideEffectFree; 041import org.checkerframework.framework.qual.Unused; 042import org.plumelib.util.ArraysPlume; 043import org.plumelib.util.CollectionsPlume; 044import org.plumelib.util.MathPlume; 045import typequals.prototype.qual.NonPrototype; 046import typequals.prototype.qual.Prototype; 047 048/** 049 * Base implementation for Invariant objects. Intended to be subclassed but not to be directly 050 * instantiated. Rules/assumptions for invariants: 051 * 052 * <p>For each program point's set of VarInfos, there exists no more than one invariant of its type. 053 * For example, between variables a and b at PptTopLevel T, there will not be two instances of 054 * invariant I(a, b). 055 */ 056@UsesObjectEquals 057@Prototype 058public abstract class Invariant implements Serializable, Cloneable // but don't YOU clone it 059{ 060 // We are Serializable, so we specify a version to allow changes to 061 // method signatures without breaking serialization. If you add or 062 // remove fields, you should change this number to the current date. 063 static final long serialVersionUID = 20040921L; 064 065 /** General debug tracer. */ 066 public static final Logger debug = Logger.getLogger("daikon.inv.Invariant"); 067 068 /** Debug tracer for printing invariants. */ 069 public static final Logger debugPrint = Logger.getLogger("daikon.print"); 070 071 /** Debug tracer for invariant flow. */ 072 public static final Logger debugFlow = Logger.getLogger("daikon.flow.flow"); 073 074 /** Debug tracer for printing equality invariants. */ 075 public static final Logger debugPrintEquality = Logger.getLogger("daikon.print.equality"); 076 077 /** Debug tracer for isWorthPrinting() checks. */ 078 public static final Logger debugIsWorthPrinting = 079 Logger.getLogger("daikon.print.isWorthPrinting"); 080 081 /** Debug tracer for guarding. */ 082 public static final Logger debugGuarding = Logger.getLogger("daikon.guard"); 083 084 /** Debug tracer for isObvious checks. */ 085 public static final Logger debugIsObvious = Logger.getLogger("daikon.inv.Invariant.isObvious"); 086 087 /** 088 * Floating-point number between 0 and 1. Invariants are displayed only if the confidence that the 089 * invariant did not occur by chance is greater than this. (May also be set via the {@code 090 * --conf_limit} command-line option to Daikon; refer to manual.) 091 */ 092 public static double dkconfig_confidence_limit = .99; 093 094 /** 095 * A boolean value. If true, Daikon's Simplify output (printed when the {@code --format simplify} 096 * flag is enabled, and used internally by {@code --suppress_redundant}) will include new 097 * predicates representing some complex relationships in invariants, such as lexical ordering 098 * among sequences. If false, some complex relationships will appear in the output as complex 099 * quantified formulas, while others will not appear at all. When enabled, Simplify may be able to 100 * make more inferences, allowing {@code --suppress_redundant} to suppress more redundant 101 * invariants, but Simplify may also run more slowly. 102 */ 103 public static boolean dkconfig_simplify_define_predicates = false; 104 105 /** 106 * Floating-point number between 0 and 0.1, representing the maximum relative difference between 107 * two floats for fuzzy comparisons. Larger values will result in floats that are relatively 108 * farther apart being treated as equal. A value of 0 essentially disables fuzzy comparisons. 109 * Specifically, if {@code abs(1 - f1/f2)} is less than or equal to this value, then the two 110 * doubles ({@code f1} and {@code f2}) will be treated as equal by Daikon. 111 */ 112 public static double dkconfig_fuzzy_ratio = 0.0001; 113 114 /** The default for dkconfig_enabled in each subclass of Invariant. */ 115 public static boolean invariantEnabledDefault = true; 116 117 /** 118 * The program point for this invariant; includes values, number of samples, VarInfos, etc. Can be 119 * null for a "prototype" invariant. 120 */ 121 @Unused(when = Prototype.class) 122 public PptSlice ppt; 123 124 // Has to be public so wrappers can read it. 125 /** 126 * True exactly if the invariant has been falsified: it is guaranteed never to hold (and should be 127 * either in the process of being destroyed or about to be destroyed). This should never be set 128 * directly; instead, call destroy(). 129 */ 130 protected boolean falsified = false; 131 132 // Whether an invariant is a guarding predicate, that is, creately solely 133 // for the purpose of ensuring invariants with variables that can be 134 // missing do not cause exceptions when tested. If this is true, then 135 // the invariant itself does not hold over the observed data. 136 public boolean isGuardingPredicate = false; 137 138 /** 139 * The probability that this could have happened by chance alone. <br> 140 * 1 = could never have happened by chance; that is, we are fully confident that this invariant is 141 * a real invariant 142 */ 143 public static final double CONFIDENCE_JUSTIFIED = 1; 144 145 /** 146 * (0..1) = greater to lesser likelihood of coincidence <br> 147 * 0 = must have happened by chance 148 */ 149 public static final double CONFIDENCE_UNJUSTIFIED = 0; 150 151 /** -1 = delete this invariant; we know it's not true */ 152 public static final double CONFIDENCE_NEVER = -1; 153 154 /** 155 * The probability that this could have happened by chance alone. <br> 156 * 0 = could never have happened by chance; that is, we are fully confident that this invariant is 157 * a real invariant 158 */ 159 public static final double PROBABILITY_JUSTIFIED = 0; 160 161 /** 162 * (0..1) = lesser to greater likelihood of coincidence <br> 163 * 1 = must have happened by chance 164 */ 165 public static final double PROBABILITY_UNJUSTIFIED = 1; 166 167 /** 3 = delete this invariant; we know it's not true */ 168 public static final double PROBABILITY_NEVER = 3; 169 170 /** 171 * Return Invariant.CONFIDENCE_JUSTIFIED if x≥goal. Return Invariant.CONFIDENCE_UNJUSTIFIED if 172 * x≤1. For intermediate inputs, the result gives confidence that grades between the two 173 * extremes. See the discussion of gradual vs. sudden confidence transitions. 174 * 175 * @param x the greater value 176 * @param goal the lesser value 177 * @return CONFIDENCE_JUSTIFIED if x≥goal, Invariant.CONFIDENCE_UNJUSTIFIED if x≤1, other 178 * values otherwise 179 */ 180 public static final double conf_is_ge(double x, double goal) { 181 if (x >= goal) { 182 return 1; 183 } 184 if (x <= 1) { 185 return 0; 186 } 187 double result = 1 - (goal - x) / (goal - 1); 188 assert 0 <= result && result <= 1 189 : "conf_is_ge: bad result = " + result + " for (x=" + x + ", goal=" + goal + ")"; 190 return result; 191 } 192 193 /** 194 * Return Invariant.PROBABILITY_JUSTIFIED if x≥goal. Return Invariant.PROBABILITY_UNJUSTIFIED 195 * if x≤1. For intermediate inputs, the result gives probability that grades between the two 196 * extremes. See the discussion of gradual vs. sudden probability transitions. 197 * 198 * @param x the greater value 199 * @param goal the lesser value 200 * @return if x≥goal: invariant.PROBABILITY_JUSTIFIED; if x≤1: 201 * Invariant.PROBABILITY_UNJUSTIFIED; otherwise: other values 202 */ 203 public static final double prob_is_ge(double x, double goal) { 204 if (x >= goal) { 205 return 0; 206 } 207 if (x <= 1) { 208 return 1; 209 } 210 double result = (goal - x) / (goal - 1); 211 assert 0 <= result && result <= 1 212 : "prob_is_ge: bad result = " + result + " for (x=" + x + ", goal=" + goal + ")"; 213 return result; 214 } 215 216 /** 217 * Return the "and" of the given confidences. This is the confidence that multiple conditions 218 * (whose confidences are given) are all satisfied. 219 * 220 * @param c1 the confidence of the first condition 221 * @param c2 the confidence of the second condition 222 * @return the "and" of the two condidences 223 */ 224 public static final double confidence_and(double c1, double c2) { 225 assert 0 <= c1 && c1 <= 1 : "confidence_and: bad c1 = " + c1; 226 assert 0 <= c2 && c2 <= 1 : "confidence_and: bad c2 = " + c2; 227 228 double result = c1 * c2; 229 230 assert 0 <= result && result <= 1 : "confidence_and: bad result = " + result; 231 return result; 232 } 233 234 /** 235 * Return the "and" of the given confidences. This is the confidence that multiple conditions 236 * (whose confidences are given) are all satisfied. 237 * 238 * @param c1 the confidence of the first condition 239 * @param c2 the confidence of the second condition 240 * @param c3 the confidence of the third condition 241 * @return the "and" of the two condidences 242 */ 243 public static final double confidence_and(double c1, double c2, double c3) { 244 assert 0 <= c1 && c1 <= 1 : "confidence_and: bad c1 = " + c1; 245 assert 0 <= c2 && c2 <= 1 : "confidence_and: bad c2 = " + c1; 246 assert 0 <= c3 && c3 <= 1 : "confidence_and: bad c3 = " + c1; 247 248 double result = c1 * c2 * c3; 249 250 assert 0 <= result && result <= 1 : "confidence_and: bad result = " + result; 251 return result; 252 } 253 254 /** 255 * Return the "or" of the given confidences. This is the confidence that at least one of multiple 256 * conditions (whose confidences are given) is satisfied. 257 * 258 * @param c1 the confidence of the first condition 259 * @param c2 the confidence of the second condition 260 * @return the "or" of the two condidences 261 */ 262 public static final double confidence_or(double c1, double c2) { 263 // Not "1-(1-c1)*(1-c2)" because that can produce a value too large; we 264 // don't want the result to be larger than the larger argument. 265 return Math.max(c1, c2); 266 } 267 268 /** 269 * Return the "and" of the given probabilities. This is the probability that multiple conditions 270 * (whose probabilities are given) are all satisfied. 271 * 272 * @param p1 the probability of the first condition 273 * @param p2 the probability of the second condition 274 * @return the "and" of the two condidences 275 */ 276 public static final double prob_and(double p1, double p2) { 277 assert 0 <= p1 && p1 <= 1 : "prob_and: bad p1 = " + p1; 278 assert 0 <= p2 && p2 <= 1 : "prob_and: bad p2 = " + p2; 279 280 // 1 - (1-p1)*(1-p2) 281 double result = p1 + p2 - p1 * p2; 282 283 assert 0 <= result && result <= 1 : "prob_and: bad result = " + result; 284 return result; 285 } 286 287 /** 288 * Return the "and" of the given probabilities. This is the probability that multiple conditions 289 * (whose probabilities are given) are all satisfied. 290 * 291 * @param p1 the probability of the first condition 292 * @param p2 the probability of the second condition 293 * @param p3 the probability of the third condition 294 * @return the "and" of the two condidences 295 */ 296 public static final double prob_and(double p1, double p2, double p3) { 297 assert 0 <= p1 && p1 <= 1 : "prob_and: bad p1 = " + p1; 298 assert 0 <= p2 && p2 <= 1 : "prob_and: bad p2 = " + p1; 299 assert 0 <= p3 && p3 <= 1 : "prob_and: bad p3 = " + p1; 300 301 double result = 1 - (1 - p1) * (1 - p2) * (1 - p3); 302 303 assert 0 <= result && result <= 1 : "prob_and: bad result = " + result; 304 return result; 305 } 306 307 /** 308 * Return the "or" of the given probabilities. This is the probability that at least one of 309 * multiple conditions (whose probabilities are given) is satisfied. 310 * 311 * @param p1 the probability of the first condition 312 * @param p2 the probability of the second condition 313 * @return the "or" of the two condidences 314 */ 315 public static final double prob_or(double p1, double p2) { 316 // Not "p1*p2" because that can produce a value too small; we don't 317 // want the result to be smaller than the smaller argument. 318 return Math.min(p1, p2); 319 } 320 321 // Subclasses should set these; Invariant never does. 322 323 /** 324 * At least this many samples are required, or else we don't report any invariant at all. (Except 325 * that OneOf invariants are treated differently.) 326 */ 327 public static final int min_mod_non_missing_samples = 5; 328 329 /** 330 * Returns true if the invariant has enough samples to have its computed constants well-formed. Is 331 * overridden in classes like LinearBinary/Ternary and Upper/LowerBound. 332 * 333 * @return true if the invariant has enough samples to have its computed constants well-formed 334 */ 335 public boolean enoughSamples(@GuardSatisfied @NonPrototype Invariant this) { 336 return true; 337 } 338 339 // The confidence routines (getConfidence and internal helper 340 // computeConfidence) use ModBitTracker information to compute 341 // justification. 342 343 // There are three confidence routines: 344 // justified() is what most clients should call 345 // getConfidence() gives the actual confidence. It used to cache 346 // results, but it does not do so any longer. 347 // computeConfidence() is an internal helper method that does the 348 // actual work, but it should not be called externally, only by 349 // getConfidence. It ignores whether the invariant is falsified. 350 351 // There are two general approaches to computing confidence 352 // when there is a threshold (such as needing to see 10 samples): 353 // * Make the confidence typically either 0 or 1, transitioning 354 // suddenly between the two as soon as the 10th sample is observed. 355 // * Make the confidence transition more gradually; for instance, each 356 // sample changes the confidence by 10%. 357 // The gradual approach has advantages and disadvantages: 358 // + Users can set the confidence limit to see invariants earlier; this 359 // is simpler than figuring out all the thresholds to set. 360 // + Tools such as the operational difference for test suite generation 361 // are assisted by knowing whether they are getting closer to 362 // justification. 363 // - The code is a bit more complicated. 364 365 /** 366 * A wrapper around getConfidence() or getConfidence(). 367 * 368 * @return true if this invariant's confidence is greater than the global confidence limit 369 */ 370 public final boolean justified(@NonPrototype Invariant this) { 371 boolean just = (!falsified && (getConfidence() >= dkconfig_confidence_limit)); 372 if (logOn()) { 373 log( 374 "justified = %s, confidence = %s, samples = %s", 375 just, getConfidence(), ppt.num_samples()); 376 } 377 return just; 378 } 379 380 // If confidence == CONFIDENCE_NEVER, then this invariant can be eliminated. 381 /** 382 * Given that this invariant has been true for all values seen so far, this method returns the 383 * confidence that that situation has occurred by chance alone. 384 * 385 * <p>Returns the probability that the observed data did not happen by chance alone. The result is 386 * a value between 0 and 1 inclusive. 0 means that this invariant could never have occurred by 387 * chance alone; we are fully confident that its truth is no coincidence. 1 means that the 388 * invariant is certainly a happenstance, so the truth of the invariant is not relevant and it 389 * should not be reported. Values between 0 and 1 give differing confidences in the invariant. The 390 * method may also return {@link #CONFIDENCE_NEVER}, meaning the invariant has been falsified. 391 * 392 * <p>An invariant is printed only if its probability of not occurring by chance alone is large 393 * enough (by default, greater than .99; see Daikon's --conf_limit command-line option. 394 * 395 * <p>As an example, consider the invariant "x!=0". If only one value, 22, has been seen for x, 396 * then the conclusion "x!=0" is not justified. But if there have been 1,000,000 values, and none 397 * of them were 0, then we may be confident that the property "x!=0" is not a coincidence. 398 * 399 * <p>This method is a wrapper around {@link #computeConfidence()}, which does the actual work. 400 * 401 * <p>Consider the invariant is 'x is even', which has a 50% chance of being true by chance for 402 * each sample. Then a reasonable body for {@link #computeConfidence} would be 403 * 404 * <pre>return 1 - Math.pow(.5, ppt.num_samples());</pre> 405 * 406 * If 5 values had been seen, then this implementation would return 31/32, which is the likelihood 407 * that all 5 values seen so far were even not purely by chance. 408 * 409 * @return confidence of this invariant 410 * @see #computeConfidence() 411 */ 412 public final double getConfidence(@NonPrototype Invariant this) { 413 assert !falsified; 414 // if (falsified) 415 // return CONFIDENCE_NEVER; 416 double result = computeConfidence(); 417 // System.out.println("getConfidence: " + getClass().getName() + " " + ppt.varNames()); 418 if (!((result == CONFIDENCE_JUSTIFIED) 419 || (result == CONFIDENCE_UNJUSTIFIED) 420 || (result == CONFIDENCE_NEVER) 421 || ((0 <= result) && (result <= 1)))) { 422 // Can't print this.repr_prob(), as it may compute the confidence! 423 System.out.println( 424 "getConfidence: " + getClass().getName() + " " + ppt.varNames() + " => " + result); 425 System.out.println(" " + this.format() + "; " + repr()); 426 } 427 assert ((0 <= result) && (result <= 1)) 428 || (result == CONFIDENCE_JUSTIFIED) 429 || (result == CONFIDENCE_UNJUSTIFIED) 430 || (result == CONFIDENCE_NEVER) 431 : "unexpected conf value: " + getClass().getName() + ": " + repr() + ", result=" + result; 432 return result; 433 } 434 435 /** 436 * This method computes the confidence that this invariant occurred by chance. Clients should call 437 * {@link #getConfidence()} instead. 438 * 439 * <p>This method need not check the value of field "falsified", as the caller does that. 440 * 441 * @return confidence of this invariant 442 * @see #getConfidence() 443 */ 444 protected abstract double computeConfidence(@NonPrototype Invariant this); 445 446 /** 447 * Subclasses should override. An exact invariant indicates that given all but one variable value, 448 * the last one can be computed. (I think that's correct, anyway.) Examples are IntComparison 449 * (when only equality is possible), LinearBinary, FunctionUnary. OneOf is treated differently, as 450 * an interface. The result of this method does not depend on whether the invariant is justified, 451 * destroyed, etc. 452 * 453 * @return true if any variable value can be computed from all the others 454 */ 455 @Pure 456 public boolean isExact(@Prototype Invariant this) { 457 return false; 458 } 459 460 // Implementations of this need to examine all the data values already 461 // in the ppt. Or, don't put too much work in the constructor and instead 462 // have the caller do that. 463 // The "ppt" argument can be null if this is a prototype invariant. 464 protected Invariant(PptSlice ppt) { 465 this.ppt = ppt; 466 } 467 468 @SuppressWarnings("nullness") // weakness in @Unused checking 469 protected @Prototype Invariant() { 470 this.ppt = null; 471 } 472 473 @SuppressWarnings("unused") 474 @Pure 475 private boolean isPrototype() { 476 return this.ppt == null; 477 } 478 479 /** 480 * Marks the invariant as falsified. Should always be called rather than just setting the flag so 481 * that we can track when this happens. 482 */ 483 public void falsify(@NonPrototype Invariant this) { 484 falsified = true; 485 if (logOn()) log("Destroyed %s", format()); 486 } 487 488 /** Clear the falsified flag. */ 489 public void clear_falsified(@NonPrototype Invariant this) { 490 falsified = false; 491 } 492 493 /** 494 * Returns whether or not this invariant has been falsified. 495 * 496 * @return true if this invariant has been falsified 497 */ 498 @Pure 499 public boolean is_false(@NonPrototype Invariant this) { 500 return falsified; 501 } 502 503 /** Do nothing special, Overridden to remove exception from declaration. */ 504 @SideEffectFree 505 @Override 506 public Invariant clone(@GuardSatisfied @NonPrototype Invariant this) { 507 try { 508 Invariant result = (Invariant) super.clone(); 509 return result; 510 } catch (CloneNotSupportedException e) { 511 throw new Error(); // can never happen 512 } 513 } 514 515 /** 516 * Make a copy of this invariant and transfer it into a new PptSlice. 517 * 518 * @param new_ppt must have the same arity and types 519 * @param permutation gives the varinfo array index mapping in the new ppt 520 * @return a copy of the invariant, on a different slice 521 */ 522 public Invariant transfer(@NonPrototype Invariant this, PptSlice new_ppt, int[] permutation) { 523 // Check some sanity conditions 524 assert new_ppt.arity() == ppt.arity(); 525 assert permutation.length == ppt.arity(); 526 for (int i = 0; i < ppt.arity(); i++) { 527 VarInfo oldvi = ppt.var_infos[i]; 528 VarInfo newvi = new_ppt.var_infos[permutation[i]]; 529 // We used to check that all 3 types were equal, but we can't do 530 // that anymore, because with equality, invariants may get 531 // transferred between old and new VarInfos of different types. 532 // They are, however, comparable 533 assert oldvi.comparableNWay(newvi); 534 } 535 536 Invariant result; 537 // Clone it 538 result = this.clone(); 539 540 // Fix up the fields 541 result.ppt = new_ppt; 542 // Let subclasses fix what they need to 543 result = result.resurrect_done(permutation); 544 545 if (logOn()) { 546 result.log( 547 "Created %s:%s via transfer from %s:%s using permutation %s old_ppt = %s new_ppt = %s", 548 result.getClass().getName(), 549 result.format(), 550 getClass().getName(), 551 format(), 552 Arrays.toString(permutation), 553 ppt, 554 new_ppt); 555 // result.log (UtilPlume.backTrace()); 556 } 557 // if (debug.isLoggable(Level.FINE)) 558 // debug.fine ("Invariant.transfer to " + new_ppt.name() + " " 559 // + result.repr()); 560 561 return result; 562 } 563 564 /** 565 * Clones the invariant and then permutes it as specified. Normally used to make child invariant 566 * match the variable order of the parent when merging invariants bottom up. 567 */ 568 public Invariant clone_and_permute(@NonPrototype Invariant this, int[] permutation) { 569 570 Invariant result = this.clone(); 571 result = result.resurrect_done(permutation); 572 573 if (logOn()) { 574 result.log( 575 "Created %s via clone_and_permute from %s using permutation %s old_ppt = %s", 576 result.format(), format(), Arrays.toString(permutation), Arrays.toString(ppt.var_infos) 577 // + " new_ppt = " + Arrays.toString (new_ppt.var_infos) 578 ); 579 } 580 581 return result; 582 } 583 584 /** 585 * Take a falsified invariant and resurrect it in a new PptSlice. 586 * 587 * @param new_ppt must have the same arity and types 588 * @param permutation gives the varinfo array index mapping 589 * @return the resurrected invariant, in a new PptSlice 590 */ 591 public Invariant resurrect(@NonPrototype Invariant this, PptSlice new_ppt, int[] permutation) { 592 // Check some sanity conditions 593 assert falsified; 594 assert new_ppt.arity() == ppt.arity(); 595 assert permutation.length == ppt.arity(); 596 for (int i = 0; i < ppt.arity(); i++) { 597 VarInfo oldvi = ppt.var_infos[i]; 598 VarInfo newvi = new_ppt.var_infos[permutation[i]]; 599 // We used to check that all 3 types were equal, but we can't do 600 // that anymore, because with equality, invariants may get 601 // resurrected between old and new VarInfos of different types. 602 // They are, however, comparable 603 assert oldvi.comparableNWay(newvi); 604 } 605 606 Invariant result; 607 // Clone it 608 result = this.clone(); 609 610 // Fix up the fields 611 result.falsified = false; 612 result.ppt = new_ppt; 613 // Let subclasses fix what they need to 614 result = result.resurrect_done(permutation); 615 616 if (logOn()) { 617 result.log( 618 "Created %s via resurrect from %s using permutation %s old_ppt = %s new_ppt = %s", 619 result.format(), 620 format(), 621 Arrays.toString(permutation), 622 Arrays.toString(ppt.var_infos), 623 Arrays.toString(new_ppt.var_infos)); 624 } 625 626 return result; 627 } 628 629 /** 630 * Returns a single VarComparability that describes the set of variables used by this invariant. 631 * Since all of the variables in an invariant must be comparable, this can usually be the 632 * comparability information for any variable. The exception is when one or more variables is 633 * always comparable (comparable to everything else). An always comparable VarComparability is 634 * returned only if all of the variables involved are always comparable. Otherwise the 635 * comparability information from one of the non always-comparable variables is returned. 636 * 637 * @return a VarComparability that describes any (and all) of this invariant's variables 638 */ 639 public VarComparability get_comparability(@NonPrototype Invariant this) { 640 641 // assert ppt != null : "class " + getClass(); 642 643 // Return the first variable that is not always-comparable 644 for (int i = 0; i < ppt.var_infos.length; i++) { 645 VarComparability vc = ppt.var_infos[i].comparability; 646 if (!vc.alwaysComparable()) { 647 return vc; 648 } 649 } 650 651 // All the variables are always-comparable, just return the first one 652 // return ppt.var_infos[0].comparability; 653 return VarComparabilityImplicit.unknown; 654 } 655 656 /** 657 * Merge the invariants in invs to form a new invariant. This implementation merely returns a 658 * clone of the first invariant in the list. This is correct for simple invariants whose equation 659 * or statistics don't depend on the actual samples seen. It should be overriden for more complex 660 * invariants (eg, bound, oneof, linearbinary, etc). 661 * 662 * @param invs list of invariants to merge. The invariants must all be of the same type and should 663 * come from the children of parent_ppt. They should also all be permuted to match the 664 * variable order in parent_ppt. 665 * @param parent_ppt slice that will contain the new invariant 666 * @return the merged invariant or null if the invariants didn't represent the same invariant 667 */ 668 public @Nullable @NonPrototype Invariant merge( 669 @Prototype Invariant this, List<@NonPrototype Invariant> invs, PptSlice parent_ppt) { 670 671 Invariant first = invs.get(0); 672 Invariant result = first.clone(); 673 result.ppt = parent_ppt; 674 result.log( 675 "Merged '%s' from %s child invariants", 676 result.format(), invs.size() /*, first.ppt.name() */); 677 678 // Make sure that each invariant was really of the same type 679 boolean assert_enabled = false; 680 assert (assert_enabled = true); 681 if (assert_enabled) { 682 Match m = new Match(result); 683 for (int i = 1; i < invs.size(); i++) { 684 assert m.equals(new Match(invs.get(i))); 685 } 686 } 687 688 return result; 689 } 690 691 /** 692 * Permutes the invariant as specified. Often creates a new invariant (with a different class). 693 * 694 * @param permutation the permutation 695 * @return the permuted invariant 696 */ 697 public @NonPrototype Invariant permute(@NonPrototype Invariant this, int[] permutation) { 698 return resurrect_done(permutation); 699 } 700 701 /** 702 * Called on the new invariant just before resurrect() returns it to allow subclasses to fix any 703 * information they might have cached from the old Ppt and VarInfos. 704 * 705 * @param permutation the permutation 706 * @return the permuted invariant 707 */ 708 protected abstract Invariant resurrect_done(@NonPrototype Invariant this, int[] permutation); 709 710 // Regrettably, I can't declare a static abstract method. 711 // // The return value is probably ignored. The new Invariant installs 712 // // itself on the PptSlice, and that's what really matters (right?). 713 // public static abstract Invariant instantiate(PptSlice ppt); 714 715 /** Return true if this invariant uses the given variable. */ 716 public boolean usesVar(@NonPrototype Invariant this, VarInfo vi) { 717 return ppt.usesVar(vi); 718 } 719 720 /** Return true if this invariant uses the given variable. */ 721 public boolean usesVar(@NonPrototype Invariant this, String name) { 722 return ppt.usesVar(name); 723 } 724 725 /** Return true if this invariant uses the given variable or any variable derived from it. */ 726 public boolean usesVarDerived(@NonPrototype Invariant this, String name) { 727 return ppt.usesVarDerived(name); 728 } 729 730 // Not used as of 1/31/2000 731 // // For use by subclasses. 732 // /** Put a string representation of the variable names in the StringBuilder. */ 733 // public void varNames(StringBuilder sb) { 734 // // sb.append(this.getClass().getName()); 735 // ppt.varNames(sb); 736 // } 737 738 /** 739 * Return a string representation of the variable names. 740 * 741 * @return a string representation of the variable names 742 */ 743 public final String varNames(@GuardSatisfied @NonPrototype Invariant this) { 744 return ppt.varNames(); 745 } 746 747 // repr()'s output should not include result of getConfidence, because 748 // repr() may be called from computeConfidence or elsewhere for 749 // debugging purposes. 750 /** 751 * For printing invariants, there are two interfaces: repr gives a low-level representation 752 * ({@link #repr_prob} also prints the confidence), and {@link #format} gives a high-level 753 * representation for user output. 754 * 755 * @return a string representation of this 756 */ 757 public String repr(@GuardSatisfied @NonPrototype Invariant this) { 758 // A better default would be to use reflection and print out all 759 // the variable names. 760 return getClass() + varNames() + ": " + format(); 761 } 762 763 /** 764 * For printing invariants, there are two interfaces: {@link #repr} gives a low-level 765 * representation (repr_prob also prints the confidence), and {@link #format} gives a high-level 766 * representation for user output. 767 * 768 * @return {@link #repr()}, but with the confidence as well 769 */ 770 public String repr_prob(@NonPrototype Invariant this) { 771 return repr() + "; confidence = " + getConfidence(); 772 } 773 774 /** 775 * Returns a high-level printed representation of the invariant, for user output. {@code format} 776 * produces normal output, while the {@link #repr} formatting routine produces low-level, detailed 777 * output for debugging, and {@link #repr_prob} also prints the confidence. 778 * 779 * @return a string representation of this 780 */ 781 // Does not respect PrintInvariants.dkconfig_print_inv_class; PrintInvariants does so. 782 // Receiver must be fully-initialized because subclasses read their fields. 783 @SideEffectFree 784 public String format(@GuardSatisfied @NonPrototype Invariant this) { 785 return format_using(OutputFormat.DAIKON); 786 } 787 788 /** 789 * Returns the class name of the invariant, for use in debugging output. Returns "" if {@link 790 * PrintInvariants#dkconfig_print_inv_class} is false. 791 * 792 * @return a string representation of the class name of the invariant, or "" 793 */ 794 public String format_classname() { 795 if (!PrintInvariants.dkconfig_print_inv_class) { 796 return ""; 797 } 798 String classname = getClass().getName(); 799 int index = classname.lastIndexOf('.'); 800 classname = classname.substring(index + 1); 801 return " [" + classname + "]"; 802 } 803 804 /** Return a printed representation of this invariant, in the given format. */ 805 @SideEffectFree 806 public abstract String format_using( 807 @GuardSatisfied @NonPrototype Invariant this, OutputFormat format); 808 809 /** 810 * Returns a conjuction of mapping the same function of our expresssions's VarInfos, in general. 811 * Subclasses may override if they are able to handle generally-inexpressible properties in 812 * special-case ways. 813 * 814 * @return conjuction of mapping the same function of our expresssions's VarInfos 815 * @see VarInfo#isValidEscExpression 816 */ 817 @Pure 818 public boolean isValidEscExpression(@NonPrototype Invariant this) { 819 for (int i = 0; i < ppt.var_infos.length; i++) { 820 if (!ppt.var_infos[i].isValidEscExpression()) { 821 return false; 822 } 823 } 824 return true; 825 } 826 827 /** A "\type(...)" construct where the "..." contains a "$". */ 828 private static Pattern anontype_pat = Pattern.compile("\\\\type\\([^\\)]*\\$"); 829 830 /** 831 * Returns true if this Invariant can be properly formatted for the given output format. 832 * 833 * @param format the expected output format 834 * @return true if this Invariant can be properly formatted for the given output format 835 */ 836 @Pure 837 public boolean isValidExpression(@NonPrototype Invariant this, OutputFormat format) { 838 if ((format == OutputFormat.ESCJAVA) && !isValidEscExpression()) { 839 return false; 840 } 841 842 String s = format_using(format); 843 844 if ((format == OutputFormat.ESCJAVA) || format.isJavaFamily()) { 845 // This list should get shorter as we improve the formatting. 846 if ((s.indexOf(" needs to be implemented: ") != -1) 847 || (s.indexOf("<<") != -1) 848 || (s.indexOf(">>") != -1) 849 || (s.indexOf("warning: ") != -1) 850 || (s.indexOf('~') != -1) 851 || (s.indexOf("\\new") != -1) 852 || (s.indexOf(".toString ") != -1) 853 || s.endsWith(".toString") 854 || (s.indexOf(".typeArray") != -1) 855 || (s.indexOf("warning: method") != -1) 856 || (s.indexOf("inexpressible") != -1) 857 || (s.indexOf("unimplemented") != -1) 858 || (s.indexOf("Infinity") != -1) 859 || anontype_pat.matcher(s).find()) { 860 return false; 861 } 862 } 863 return true; 864 } 865 866 /** 867 * Returns standard "format needs to be implemented" for the given requested format. Made public 868 * so cores can call it. 869 * 870 * @param format the requested output format 871 * @return standard "format needs to be implemented" for the given requested format 872 */ 873 public String format_unimplemented( 874 @GuardSatisfied @NonPrototype Invariant this, OutputFormat format) { 875 String classname = this.getClass().getName(); 876 return "warning: method " 877 + classname 878 + ".format(" 879 + format 880 + ")" 881 + " needs to be implemented: " 882 + format(); 883 } 884 885 /** 886 * Returns standard "too few samples for to have interesting invariant" for the requested format. 887 * For machine-readable formats, this is just "true". An optional string argument, if supplied, is 888 * a human-readable description of the invariant in its uninformative state, which will be added 889 * to the message. 890 * 891 * @param format the requested output format 892 * @return standard "too few samples for to have interesting invariant" for the requested format 893 */ 894 public String format_too_few_samples( 895 @GuardSatisfied @NonPrototype Invariant this, OutputFormat format, @Nullable String attempt) { 896 if (format == OutputFormat.SIMPLIFY) { 897 return "(AND)"; 898 } else if (format == OutputFormat.JAVA 899 || format == OutputFormat.ESCJAVA 900 || format == OutputFormat.JML 901 || format == OutputFormat.DBCJAVA) { 902 return "true"; 903 } 904 String classname = this.getClass().getName(); 905 if (attempt == null) { 906 attempt = varNames(); 907 } 908 return "warning: too few samples for " + classname + " invariant: " + attempt; 909 } 910 911 /** 912 * Convert a floating point value into the weird Modula-3-like floating point format that the 913 * Simplify tool requires. 914 * 915 * @param d the number to print 916 * @return a printed representation of the number, for Simplify 917 */ 918 public static String simplify_format_double(double d) { 919 String s = d + ""; 920 if (s.indexOf('E') != -1) { 921 // 1E6 -> 1d6 922 // 1.43E6 -> 1.43d6 923 s = s.replace('E', 'd'); 924 } else if (s.indexOf('.') != -1) { 925 // 3.14 -> 3.14d0 926 s = s + "d0"; 927 } else if (s.equals("-Infinity")) { 928 // -Infinity -> NegativeInfinity 929 s = "NegativeInfinity"; 930 } 931 // 5 -> 5 932 // NaN -> NaN 933 // Infinity -> Infinity 934 return s; 935 } 936 937 /** 938 * Conver a long integer value into a format that Simplify can use. If the value is too big, we 939 * have to print it in a weird way, then tell Simplify about its properties specially. 940 * 941 * @param l the number to print 942 * @return a printed representation of the number, for Simplify 943 */ 944 public static String simplify_format_long(long l) { 945 LemmaStack.noticeInt(l); 946 if (l > -LemmaStack.SMALL_INTEGER && l < LemmaStack.SMALL_INTEGER) { 947 // Simplify's internal numeric representation is based on 948 // (ratios of) signed 32-bit integers, so it can't be both sound 949 // and precise with respect to integer overflow. In its default 950 // configuration it crashes with an internal error when any 951 // internal computation overflows. To work around this, we print 952 // large integers in an abstract format, and then explicitly 953 // give the ordering among those values. This loses other 954 // arithmetic facts, but is good enough for the way we use it. 955 // Examples of inputs containing large integers that crash: 956 // > (BG_PUSH (< 2147483647 n)) 957 // (assertion in negative argument to GCD) 958 // > (BG_PUSH (>= x -1073741825)) 959 // > (BG_PUSH (<= x 1073741825)) 960 // > (OR) 961 // (assertion: unexpected negative value in the Simplex engine) 962 // > (BG_PUSH (EQ x 56312)) 963 // > (BG_PUSH (EQ y (* y x))) 964 // (assertion: negative denomniator in rational normalize) 965 // The value 32000 for SMALL_INTEGER is semi-empirically derived 966 // as "2**15 - some slop" in hopes of working around as many 967 // potential overflows in Simplify as possible, while still 968 // letting it do concrete arithmetic on small integers. It may 969 // be that there's no bound that would work with arbitrary 970 // formulas, but this one seems to work OK for formulas 971 // generated by Daikon. 972 return "" + l; 973 } else { 974 return SimpUtil.formatInteger(l); 975 } 976 } 977 978 /** 979 * Convert a string value into the weird |-quoted format that the Simplify tool requires. (Note 980 * that Simplify doesn't distinguish between variables, symbolic constants, and strings, so we 981 * prepend "_string_" to avoid collisions with variables and other symbols). 982 * 983 * @param s the number to print 984 * @return a printed representation of the string, for Simplify 985 */ 986 public static String simplify_format_string(String s) { 987 if (s == null) { 988 return "null"; 989 } 990 StringBuilder buf = new StringBuilder("|_string_"); 991 if (s.length() > 150) { 992 // Simplify can't handle long strings (its input routines have a 993 // 4000-character limit for |...| identifiers, but it gets an 994 // internal array overflow for ones more than about 195 995 // characters), so replace all but the beginning and end of a 996 // long string with a hashed summary. 997 int summ_length = s.length() - 100; 998 int p1 = 50 + summ_length / 4; 999 int p2 = 50 + summ_length / 2; 1000 int p3 = 50 + 3 * summ_length / 4; 1001 int p4 = 50 + summ_length; 1002 StringBuilder summ_buf = new StringBuilder(s.substring(0, 50)); 1003 summ_buf.append("..."); 1004 summ_buf.append(Integer.toHexString(s.substring(50, p1).hashCode())); 1005 summ_buf.append(Integer.toHexString(s.substring(p1, p2).hashCode())); 1006 summ_buf.append(Integer.toHexString(s.substring(p2, p3).hashCode())); 1007 summ_buf.append(Integer.toHexString(s.substring(p3, p4).hashCode())); 1008 summ_buf.append("..."); 1009 summ_buf.append(s.substring(p4)); 1010 s = summ_buf.toString(); 1011 } 1012 for (int i = 0; i < s.length(); i++) { 1013 char c = s.charAt(i); 1014 if (c == '\n') // not lineSep 1015 buf.append("\\n"); // not lineSep 1016 else if (c == '\r') buf.append("\\r"); 1017 else if (c == '\t') buf.append("\\t"); 1018 else if (c == '\f') buf.append("\\f"); 1019 else if (c == '\\') buf.append("\\\\"); 1020 else if (c == '|') buf.append("\\|"); 1021 else if (c >= ' ' && c <= '~') buf.append(c); 1022 else { 1023 buf.append("\\"); 1024 // AFAIK, Simplify doesn't glork Unicode, so lop off all but 1025 // the low 8 bits 1026 String octal = Integer.toOctalString(c & 0xff); 1027 // Also, Simplify only accepts octal escapes with exactly 3 digits 1028 while (octal.length() < 3) octal = "0" + octal; 1029 buf.append(octal); 1030 } 1031 } 1032 buf.append("|"); 1033 return buf.toString(); 1034 } 1035 1036 // This should perhaps be merged with some kind of PptSlice comparator. 1037 /** Compare based on arity, then printed representation. */ 1038 public static final class InvariantComparatorForPrinting implements Comparator<Invariant> { 1039 @Pure 1040 @Override 1041 public int compare(@NonPrototype Invariant inv1, @NonPrototype Invariant inv2) { 1042 if (inv1 == inv2) { 1043 return 0; 1044 } 1045 1046 // Guarding implications should compare as if they were without the 1047 // guarding predicate 1048 1049 if (inv1 instanceof GuardingImplication) inv1 = ((GuardingImplication) inv1).right; 1050 if (inv2 instanceof GuardingImplication) { 1051 inv2 = ((GuardingImplication) inv2).right; 1052 } 1053 1054 // Put equality invariants first 1055 if ((inv1 instanceof EqualityComparison) && !(inv2 instanceof EqualityComparison)) { 1056 return -1; 1057 } 1058 if (!(inv1 instanceof EqualityComparison) && (inv2 instanceof EqualityComparison)) { 1059 return 1; 1060 } 1061 1062 // assert inv1.ppt.parent == inv2.ppt.parent; 1063 VarInfo[] vis1 = inv1.ppt.var_infos; 1064 VarInfo[] vis2 = inv2.ppt.var_infos; 1065 int arity_cmp = vis1.length - vis2.length; 1066 if (arity_cmp != 0) { 1067 return arity_cmp; 1068 } 1069 // Comparing on variable index is wrong in general: variables of the 1070 // same name may have different indices at different program points. 1071 // However, it's safe if the invariants are from the same program 1072 // point. Also, it is nice to avoid changing the order of variables 1073 // from that of the data trace file. 1074 1075 if (inv1.ppt.parent == inv2.ppt.parent) { 1076 for (int i = 0; i < vis1.length; i++) { 1077 int tmp = vis1[i].varinfo_index - vis2[i].varinfo_index; 1078 if (tmp != 0) { 1079 return tmp; 1080 } 1081 } 1082 } else { 1083 // // Debugging 1084 // System.out.println("ICFP: different parents for " + inv1.format() + ", " + 1085 // inv2.format()); 1086 1087 for (int i = 0; i < vis1.length; i++) { 1088 String name1 = vis1[i].name(); 1089 String name2 = vis2[i].name(); 1090 if (name1.equals(name2)) { 1091 continue; 1092 } 1093 int name1in2 = inv2.ppt.parent.indexOf(name1); 1094 int name2in1 = inv1.ppt.parent.indexOf(name2); 1095 int cmp1 = (name1in2 == -1) ? 0 : vis1[i].varinfo_index - name1in2; 1096 int cmp2 = (name2in1 == -1) ? 0 : vis2[i].varinfo_index - name2in1; 1097 int cmp = MathPlume.sign(cmp1) + MathPlume.sign(cmp2); 1098 if (cmp != 0) { 1099 return cmp; 1100 } 1101 } 1102 } 1103 1104 // Sort OneOf invariants earlier than others 1105 if ((inv1 instanceof OneOf) && !(inv2 instanceof OneOf)) { 1106 return -1; 1107 } 1108 if (!(inv1 instanceof OneOf) && (inv2 instanceof OneOf)) { 1109 return 1; 1110 } 1111 1112 // System.out.println("ICFP: default rule yields " 1113 // + inv1.format().compareTo(inv2.format()) 1114 // + " for " + inv1.format() + ", " + inv2.format()); 1115 // (Actually, FileIO.new_decl_format should always be non-null here.) 1116 if (PrintInvariants.dkconfig_old_array_names 1117 && FileIO.new_decl_format != null 1118 && FileIO.new_decl_format) { 1119 return inv1.format().replace("[..]", "[]").compareTo(inv2.format().replace("[..]", "[]")); 1120 } else { 1121 return inv1.format().compareTo(inv2.format()); 1122 } 1123 } 1124 } 1125 1126 /** 1127 * Returns true iff the two invariants represent the same mathematical formula. Does not consider 1128 * the context such as variable names, confidences, sample counts, value counts, or related 1129 * quantities. As a rule of thumb, if two invariants format the same, this method returns true. 1130 * Furthermore, in many cases, if an invariant does not involve computed constants (as "x>c" 1131 * and "y=ax+b" do for constants a, b, and c), then this method vacuously returns true. 1132 * 1133 * @param other the invariant to compare to this one 1134 * @return true iff the two invariants represent the same mathematical formula. Does not consider 1135 * @exception RuntimeException if other.getClass() != this.getClass() 1136 */ 1137 public abstract boolean isSameFormula(@Prototype Invariant this, Invariant other); 1138 1139 /** 1140 * Returns whether or not it is possible to merge invariants of the same class but with different 1141 * formulas when combining invariants from lower ppts to build invariants at upper program points. 1142 * Invariants that have this characteristic (eg, bound, oneof) should override this function. Note 1143 * that invariants that can do this, normally need special merge code as well (to merge the 1144 * different formulas into a single formula at the upper point. 1145 * 1146 * @return true if invariants with different formulas can be merged 1147 */ 1148 public boolean mergeFormulasOk(@Prototype Invariant this) { 1149 return false; 1150 } 1151 1152 /** 1153 * Returns true iff the argument is the "same" invariant as this. Same, in this case, means a 1154 * matching type, formula, and variable names. 1155 * 1156 * @param inv2 the other invariant to compare to this one 1157 * @return true iff the argument is the "same" invariant as this 1158 */ 1159 @Pure 1160 public boolean isSameInvariant(@NonPrototype Invariant this, Invariant inv2) { 1161 // return isSameInvariant(inv2, defaultIsSameInvariantNameExtractor); 1162 1163 Invariant inv1 = this; 1164 1165 // Can't be the same if they aren't the same type 1166 if (!inv1.getClass().equals(inv2.getClass())) { 1167 return false; 1168 } 1169 1170 // Can't be the same if they aren't the same formula 1171 if (!inv1.isSameFormula(inv2)) { 1172 return false; 1173 } 1174 1175 // The variable names much match up, in order 1176 VarInfo[] vars1 = inv1.ppt.var_infos; 1177 VarInfo[] vars2 = inv2.ppt.var_infos; 1178 1179 // due to inv type match already 1180 assert vars1.length == vars2.length; 1181 1182 for (int i = 0; i < vars1.length; i++) { 1183 VarInfo var1 = vars1[i]; 1184 VarInfo var2 = vars2[i]; 1185 if (!var1.name().equals(var2.name())) { 1186 return false; 1187 } 1188 } 1189 1190 return true; 1191 } 1192 1193 /** 1194 * Returns true iff the two invariants represent mutually exclusive mathematical formulas -- that 1195 * is, if one of them is true, then the other must be false. This method does not consider the 1196 * context such as variable names, confidences, sample counts, value counts, or related 1197 * quantities. 1198 * 1199 * @param other the other invariant to compare to this one 1200 * @return true iff the two invariants represent mutually exclusive mathematical formulas 1201 */ 1202 @Pure 1203 public boolean isExclusiveFormula(@NonPrototype Invariant this, Invariant other) { 1204 return false; 1205 } 1206 1207 /** 1208 * Look up a previously instantiated Invariant. 1209 * 1210 * @param invclass the class of the invariant to search for 1211 * @param ppt the program point in which to look for the invariant 1212 * @return the invariant of class invclass, or null if none was found 1213 */ 1214 // This implementation should be made more efficient, because it's used in 1215 // suppression. We should somehow index invariants by their type. 1216 public static @Nullable Invariant find(Class<? extends Invariant> invclass, PptSlice ppt) { 1217 for (Invariant inv : ppt.invs) { 1218 if (inv.getClass() == invclass) { 1219 return inv; 1220 } 1221 } 1222 return null; 1223 } 1224 1225 /** 1226 * Returns the set of non-instantiating suppressions for this invariant. May return null instead 1227 * of an empty set. Should be overridden by subclasses with non-instantiating suppressions. 1228 * 1229 * @return the set of non-instantiating suppressions for this invariant 1230 */ 1231 @Pure 1232 public @Nullable NISuppressionSet get_ni_suppressions(@Prototype Invariant this) { 1233 return null; 1234 } 1235 1236 /** 1237 * Returns whether or not this invariant is ni-suppressed. 1238 * 1239 * @return true if this invariant is ni-suppressed 1240 */ 1241 @SuppressWarnings( 1242 "nullness") // tricky control flow, need to mark get_ni_suppressions as @Pure if that's true 1243 @EnsuresNonNullIf(result = true, expression = "get_ni_suppressions()") 1244 @Pure 1245 public boolean is_ni_suppressed() { 1246 1247 NISuppressionSet ss = get_ni_suppressions(); 1248 if (ss == null) { 1249 return false; 1250 } 1251 boolean suppressed = ss.suppressed(ppt); 1252 if (suppressed && Debug.logOn() && (Daikon.current_inv != null)) { 1253 Daikon.current_inv.log("inv %s suppressed: %s", format(), ss); 1254 } 1255 if (Debug.logDetail()) { 1256 log("suppressed = %s suppression set = %s", suppressed, ss); 1257 } 1258 1259 return suppressed; 1260 } 1261 1262 /////////////////////////////////////////////////////////////////////////// 1263 /// Tests about the invariant (for printing) 1264 /// 1265 1266 // DO NOT OVERRIDE. Should be declared "final", but the "final" is 1267 // omitted to allow for easier testing. 1268 @Pure 1269 public boolean isWorthPrinting(@NonPrototype Invariant this) { 1270 return InvariantFilters.defaultFilters().shouldKeep(this) == null; 1271 } 1272 1273 //////////////////////////////////////////////////////////////////////////// 1274 // Static and dynamic checks for obviousness 1275 1276 /** 1277 * Return true if this invariant is necessarily true from a fact that can be determined statically 1278 * from the decls files. (An example is being from a certain derivation.) Intended to be 1279 * overridden by subclasses. 1280 * 1281 * <p>This method is final because children of Invariant should be extending 1282 * isObviousStatically(VarInfo[]) because it is more general. 1283 */ 1284 @Pure 1285 public final @Nullable DiscardInfo isObviousStatically(@NonPrototype Invariant this) { 1286 return isObviousStatically(this.ppt.var_infos); 1287 } 1288 1289 /** 1290 * Return true if this invariant is necessarily true from a fact that can be determined statically 1291 * -- for the given varInfos rather than the varInfos of this. Conceptually, this means "is this 1292 * invariant statically obvious if its VarInfos were switched with vis?" Intended to be overridden 1293 * by subclasses. Should only do static checking. 1294 * 1295 * <p>Precondition: vis.length == this.ppt.var_infos.length 1296 * 1297 * @param vis the VarInfos this invariant is obvious over. The position and data type of the 1298 * variables is the *same* as that of this.ppt.var_infos. 1299 */ 1300 @Pure 1301 public @Nullable DiscardInfo isObviousStatically(@Prototype Invariant this, VarInfo[] vis) { 1302 return null; 1303 } 1304 1305 /** 1306 * Return true if this invariant and all equality combinations of its member variables are 1307 * necessarily true from a fact that can be determined statically (i.e., the decls files). For 1308 * example, a == b, and f(a) is obvious, but f(b) is not. In that case, this method on f(a) would 1309 * return false. If f(b) is also obvious, then this method would return true. 1310 */ 1311 // This is used because we cannot decide to non-instantiate some 1312 // invariants just because isObviousStatically is true, since some 1313 // of the member variables may be equal to non-obvious varInfos. If 1314 // we were to non-instantiate, we could not copy an invariant to the 1315 // non-obvious VarInfos should they split off from the obvious one. 1316 // Of course, it's expensive to examine every possible permutation 1317 // of VarInfos and their equality set, so a possible conservative 1318 // approximation is to simply return false. 1319 @Pure 1320 public boolean isObviousStatically_AllInEquality(@NonPrototype Invariant this) { 1321 // If the leaders aren't statically obvious, then clearly not all 1322 // combinations are. 1323 if (isObviousStatically() == null) { 1324 return false; 1325 } 1326 1327 for (int i = 0; i < ppt.var_infos.length; i++) { 1328 if (ppt.var_infos[i].equalitySet.getVars().size() > 1) { 1329 return false; 1330 } 1331 } 1332 return true; 1333 } 1334 1335 /** 1336 * Return true if this invariant and some equality combinations of its member variables are 1337 * statically obvious. For example, if a == b, and f(a) is obvious, then so is f(b). We use the 1338 * someInEquality (or least interesting) method during printing so we only print an invariant if 1339 * all its variables are interesting, since a single, static, non interesting occurance means all 1340 * the equality combinations aren't interesting. 1341 * 1342 * @return the VarInfo array that contains the VarInfos that showed this invariant to be obvious. 1343 * The contains variables that are elementwise in the same equality set as this.ppt.var_infos. 1344 * Can be null if no such assignment exists. 1345 */ 1346 @Pure 1347 public @Nullable DiscardInfo isObviousStatically_SomeInEquality(@NonPrototype Invariant this) { 1348 DiscardInfo result = isObviousStatically(); 1349 if (result != null) { 1350 return result; 1351 } 1352 return isObviousStatically_SomeInEqualityHelper( 1353 this.ppt.var_infos, new /*NNC:@MonotonicNonNull*/ VarInfo[this.ppt.var_infos.length], 0); 1354 } 1355 1356 // TODO: finish this comment. 1357 /** Recurse through vis and generate the cartesian product of ... */ 1358 @Pure 1359 protected @Nullable DiscardInfo isObviousStatically_SomeInEqualityHelper( 1360 @NonPrototype Invariant this, 1361 VarInfo[] vis, 1362 /*NNC:@MonotonicNonNull*/ VarInfo[] assigned, 1363 int position) { 1364 if (position == vis.length) { 1365 if (debugIsObvious.isLoggable(Level.FINE)) { 1366 StringBuilder sb = new StringBuilder(); 1367 sb.append(" isObviousStatically_SomeInEquality: "); 1368 for (int i = 0; i < vis.length; i++) { 1369 sb.append(assigned[i].name() + " "); 1370 } 1371 debugIsObvious.fine(sb.toString()); 1372 } 1373 1374 assigned = castNonNullDeep(assigned); // https://tinyurl.com/cfissue/986 1375 return isObviousStatically(assigned); 1376 } else { 1377 for (VarInfo vi : vis[position].get_equalitySet_vars()) { 1378 assigned[position] = vi; 1379 DiscardInfo temp = isObviousStatically_SomeInEqualityHelper(vis, assigned, position + 1); 1380 if (temp != null) { 1381 return temp; 1382 } 1383 } 1384 return null; 1385 } 1386 } 1387 1388 /** 1389 * Return true if this invariant is necessarily true from a fact that can be determined statically 1390 * (i.e., the decls files) or dynamically (after checking data). Intended not to be overriden, 1391 * because sub-classes should override isObviousStatically or isObviousDynamically. Wherever 1392 * possible, suppression, rather than this, should do the dynamic checking. 1393 */ 1394 @Pure 1395 public final @Nullable DiscardInfo isObvious(@NonPrototype Invariant this) { 1396 // Actually actually, we'll eliminate invariants as they become obvious 1397 // rather than on output; the point of this is to speed up computation. 1398 // // Actually, we do need to check isObviousDerived after all because we 1399 // // add invariants that might be obvious, but might also turn out to be 1400 // // even stronger (and so not obvious). We don't know how the invariant 1401 // // turns out until after testing it. 1402 // // // We don't need to check isObviousDerived because we won't add 1403 // // // obvious-derived invariants to lists in the first place. 1404 DiscardInfo staticResult = isObviousStatically_SomeInEquality(); 1405 if (staticResult != null) { 1406 if (debugPrint.isLoggable(Level.FINE)) debugPrint.fine(" [obvious: " + repr_prob() + " ]"); 1407 return staticResult; 1408 } else { 1409 DiscardInfo dynamicResult = isObviousDynamically_SomeInEquality(); 1410 if (dynamicResult != null) { 1411 if (debugPrint.isLoggable(Level.FINE)) { 1412 debugPrint.fine(" [obvious: " + repr_prob() + " ]"); 1413 } 1414 return dynamicResult; 1415 } else { 1416 return null; 1417 } 1418 } 1419 } 1420 1421 /** 1422 * Return non-null if this invariant is necessarily true from a fact that can be determined 1423 * dynamically (after checking data) -- for the given varInfos rather than the varInfos of this. 1424 * Conceptually, this means, "Is this invariant dynamically obvious if its VarInfos were switched 1425 * with vis?" Intended to be overriden by subclasses so they can filter invariants after checking; 1426 * the overriding method should first call "super.isObviousDynamically(vis)". Since this method is 1427 * dynamic, it should only be called after all processing. 1428 */ 1429 public @Nullable DiscardInfo isObviousDynamically(@NonPrototype Invariant this, VarInfo[] vis) { 1430 assert !Daikon.isInferencing; 1431 assert vis.length <= 3 : "Unexpected more-than-ternary invariant"; 1432 if (!ArraysPlume.noDuplicates(vis)) { 1433 log("Two or more variables are equal %s", format()); 1434 return new DiscardInfo(this, DiscardCode.obvious, "Two or more variables are equal"); 1435 } 1436 // System.out.println("Passed Invariant.isObviousDynamically(): " + format()); 1437 return null; 1438 } 1439 1440 /** 1441 * Return true if more than one of the variables in the invariant are the same variable. We create 1442 * such invariants for the purpose of equality set processing, but they aren't intended for 1443 * printing; there should be invariants with the same meaning but lower arity instead. For 1444 * instance, we don't need "x = x + x" because we have "x = 0" instead. 1445 * 1446 * <p>Actually, this isn't strictly true: we don't have an invariant "a[] is a palindrome" 1447 * corresponding to "a[] is the reverse of a[]", for instance. 1448 */ 1449 @Pure 1450 public boolean isReflexive(@NonPrototype Invariant this) { 1451 return !ArraysPlume.noDuplicates(ppt.var_infos); 1452 } 1453 1454 /** 1455 * Return true if this invariant is necessarily true from a fact that can be determined 1456 * dynamically (after checking data, based on other invariants that were inferred). Since this 1457 * method is dynamic, it should only be called after all processing. 1458 * 1459 * <p>If a test does not look up other inferred invariants (that is, it relies only on information 1460 * in the decls file), then it should be written as an isObviousStatically test, not an 1461 * isObviousDynamically test. 1462 * 1463 * <p>This method is final because subclasses should extend isObviousDynamically(VarInfo[]) since 1464 * that method is more general. 1465 */ 1466 public final @Nullable DiscardInfo isObviousDynamically(@NonPrototype Invariant this) { 1467 assert !Daikon.isInferencing; 1468 return isObviousDynamically(ppt.var_infos); 1469 } 1470 1471 /** 1472 * Return true if this invariant and some equality combinations of its member variables are 1473 * dynamically obvious. For example, a == b, and f(a) is obvious, so is f(b). We use the 1474 * someInEquality (or least interesting) method during printing so we only print an invariant if 1475 * all its variables are interesting, since a single, dynamic, non interesting occurance means all 1476 * the equality combinations aren't interesting. 1477 * 1478 * @return the VarInfo array that contains the VarInfos that showed this invariant to be obvious. 1479 * The contains variables that are elementwise in the same equality set as this.ppt.var_infos. 1480 * Can be null if no such assignment exists. 1481 */ 1482 @Pure 1483 public @Nullable DiscardInfo isObviousDynamically_SomeInEquality(@NonPrototype Invariant this) { 1484 DiscardInfo result = isObviousDynamically(); 1485 if (result != null) { 1486 return result; 1487 } 1488 return isObviousDynamically_SomeInEqualityHelper( 1489 this.ppt.var_infos, new /*NNC:@MonotonicNonNull*/ VarInfo[this.ppt.var_infos.length], 0); 1490 } 1491 1492 /** 1493 * Recurse through vis (an array of leaders) and generate the cartesian product of their equality 1494 * sets; in other words, every combination of one element from each equality set. For each such 1495 * combination, test isObviousDynamically; if any test is true, then return that combination. The 1496 * combinations are generated via recursive calls to this routine. 1497 */ 1498 protected @Nullable DiscardInfo isObviousDynamically_SomeInEqualityHelper( 1499 @NonPrototype Invariant this, VarInfo[] vis, VarInfo[] assigned, int position) { 1500 if (position == vis.length) { 1501 // base case 1502 if (debugIsObvious.isLoggable(Level.FINE)) { 1503 StringBuilder sb = new StringBuilder(); 1504 sb.append(" isObviousDynamically_SomeInEquality: "); 1505 for (int i = 0; i < vis.length; i++) { 1506 sb.append(assigned[i].name() + " "); 1507 } 1508 debugIsObvious.fine(sb.toString()); 1509 } 1510 return isObviousDynamically(assigned); 1511 } else { 1512 // recursive case 1513 for (VarInfo vi : vis[position].get_equalitySet_vars()) { 1514 assigned[position] = vi; 1515 DiscardInfo temp = isObviousDynamically_SomeInEqualityHelper(vis, assigned, position + 1); 1516 if (temp != null) { 1517 return temp; 1518 } 1519 } 1520 return null; 1521 } 1522 } 1523 1524 /** 1525 * Returns true if this invariant is only over prestate variables. 1526 * 1527 * @return true if this invariant is only over prestate variables 1528 */ 1529 @Pure 1530 public boolean isAllPrestate(@NonPrototype Invariant this) { 1531 return ppt.allPrestate(); 1532 } 1533 1534 /** 1535 * An invariant that includes an uninteresting constant (say, "size(x[]) < 237") is likely to 1536 * be an artifact of the way the program was tested, rather than a statement that would in fact 1537 * hold over all possible executions. 1538 */ 1539 public boolean hasUninterestingConstant(@NonPrototype Invariant this) { 1540 return false; 1541 } 1542 1543 // Orders invariants by class, then by variable names. If the 1544 // invariants are both of class Implication, they are ordered by 1545 // comparing the predicate, then the consequent. 1546 public static final class ClassVarnameComparator implements Comparator<Invariant> { 1547 @Pure 1548 @Override 1549 public int compare(Invariant inv1, Invariant inv2) { 1550 1551 if (inv1 instanceof Implication && inv2 instanceof Implication) { 1552 return compareImplications((Implication) inv1, (Implication) inv2); 1553 } 1554 1555 int compareClass = compareClass(inv1, inv2); 1556 if (compareClass != 0) { 1557 return compareClass; 1558 } 1559 1560 return compareVariables(inv1, inv2); 1561 } 1562 1563 // Returns 0 if the invariants are of the same class. Else, 1564 // returns the comparison of the class names. 1565 private int compareClass(Invariant inv1, Invariant inv2) { 1566 if (inv1.getClass().equals(inv2.getClass())) { 1567 if (inv1 instanceof DummyInvariant) { 1568 // This special case is needed because the other code 1569 // assumes that all invariants of a given class have the 1570 // same arity. 1571 String df1 = inv1.format(); 1572 String df2 = inv2.format(); 1573 int cmp = df1.compareTo(df2); 1574 if (cmp != 0) { 1575 return cmp; 1576 } 1577 return inv1.ppt.var_infos.length - inv2.ppt.var_infos.length; 1578 } 1579 return 0; 1580 } else { 1581 String classname1 = inv1.getClass().getName(); 1582 String classname2 = inv2.getClass().getName(); 1583 return classname1.compareTo(classname2); 1584 } 1585 } 1586 1587 // Returns 0 if the invariants have the same variable names. 1588 // Else, returns the comparison of the first variable names that 1589 // differ. Requires that the invariants be of the same class. 1590 private int compareVariables(Invariant inv1, Invariant inv2) { 1591 VarInfo[] vars1 = inv1.ppt.var_infos; 1592 VarInfo[] vars2 = inv2.ppt.var_infos; 1593 1594 // due to inv type match already 1595 assert vars1.length == vars2.length 1596 : "Bad type match: " + inv1.format() + " vs. " + inv2.format(); 1597 1598 for (int i = 0; i < vars1.length; i++) { 1599 VarInfo var1 = vars1[i]; 1600 VarInfo var2 = vars2[i]; 1601 int compare = var1.name().compareTo(var2.name()); 1602 if (compare != 0) { 1603 return compare; 1604 } 1605 } 1606 1607 // All the variable names matched 1608 return 0; 1609 } 1610 1611 private int compareImplications(Implication inv1, Implication inv2) { 1612 int comparePredicate = compare(inv1.predicate(), inv2.predicate()); 1613 if (comparePredicate != 0) { 1614 return comparePredicate; 1615 } 1616 1617 return compare(inv1.consequent(), inv2.consequent()); 1618 } 1619 } 1620 1621 /** 1622 * Orders invariants by class, then variable names, then formula. If the formulas are the same, 1623 * compares the printed representation obtained from the format() method. 1624 */ 1625 public static final class ClassVarnameFormulaComparator implements Comparator<Invariant> { 1626 1627 Comparator<Invariant> classVarnameComparator = new ClassVarnameComparator(); 1628 1629 @Pure 1630 @Override 1631 public int compare(@NonPrototype Invariant inv1, @NonPrototype Invariant inv2) { 1632 int compareClassVarname = classVarnameComparator.compare(inv1, inv2); 1633 1634 if (compareClassVarname != 0) { 1635 return compareClassVarname; 1636 } 1637 1638 if (inv1.isSameInvariant(inv2)) { 1639 return 0; 1640 } 1641 1642 int result = inv1.format().compareTo(inv2.format()); 1643 1644 // The purpose of the assertion below would seem to be to insist that 1645 // anything that doesn't return true to isSameInvariant() will not 1646 // produce the same written formula. This can happen, however, if the 1647 // variables have a different order (as in function binary), but the 1648 // swapped variables are actually the same (since we create invariants 1649 // of the form f(a, a, a) because of equality sets. 1650 // assert result != 0 1651 // : "isSameInvariant() returned false " 1652 // + "(isSameFormula returned " + inv1.isSameFormula(inv2) + ")," + lineSep 1653 // + "but format().compareTo() returned 0:" + lineSep 1654 // + " " + inv1.format() + lineSep + " " + inv1.repr() + lineSep 1655 // + " " + inv1.ppt.parent.name + lineSep 1656 // + " " + inv2.format() + lineSep + " " + inv2.repr() + lineSep 1657 // + " " + inv1.ppt.parent.name + lineSep 1658 // ; 1659 1660 return result; 1661 } 1662 } 1663 1664 /** 1665 * Class used as a key to store invariants in a MAP where their equality depends on the invariant 1666 * representing the same invariant (i.e., their class is the same) and the same internal state 1667 * (when multiple invariants with the same class are possible) 1668 * 1669 * <p>Note that this is based on the Invariant type (i.e., class) and the internal state and not 1670 * on what ppt the invariant is in or what variables it is over. Thus, invariants from different 1671 * ppts are the same if they represent the same type of invariant. 1672 */ 1673 public static class Match { 1674 1675 public Invariant inv; 1676 1677 public Match(Invariant inv) { 1678 this.inv = inv; 1679 } 1680 1681 @EnsuresNonNullIf(result = true, expression = "#1") 1682 @Pure 1683 @Override 1684 public boolean equals(@GuardSatisfied Match this, @GuardSatisfied @Nullable Object obj) { 1685 if (!(obj instanceof Match)) { 1686 return false; 1687 } 1688 1689 Match ic = (Match) obj; 1690 return ic.inv.match(inv); 1691 } 1692 1693 @Pure 1694 @Override 1695 public int hashCode(@GuardSatisfied @UnknownSignedness Match this) { 1696 return inv.getClass().hashCode(); 1697 } 1698 } 1699 1700 /** 1701 * Returns whether or not two invariants are of the same type. To be of the same type, invariants 1702 * must be of the same class. Some invariant classes represent multiple invariants (such as 1703 * FunctionBinary). They must also be the same formula. Note that invariants with different 1704 * formulas based on their samples (LinearBinary, Bounds, etc) will still match as long as the 1705 * mergeFormulaOk() method returns true. 1706 */ 1707 public boolean match(@Prototype Invariant inv) { 1708 1709 if (inv.getClass() == getClass()) { 1710 return inv.mergeFormulasOk() || isSameFormula(inv); 1711 } else { 1712 return false; 1713 } 1714 } 1715 1716 /** 1717 * Returns whether or not the invariant matches the specified state. Must be overriden by 1718 * subclasses that support this. Otherwise, it returns true only if the state is null. 1719 */ 1720 public boolean state_match(@NonPrototype Invariant this, Object state) { 1721 return (state == null); 1722 } 1723 1724 /** Create a guarding predicate for a given invariant. Returns null if no guarding is needed. */ 1725 public @Nullable @NonPrototype Invariant createGuardingPredicate(boolean install) { 1726 if (debugGuarding.isLoggable(Level.FINE)) { 1727 debugGuarding.fine("Guarding predicate being created for: "); 1728 debugGuarding.fine(" " + this.format()); 1729 } 1730 1731 // Find which VarInfos must be guarded 1732 List<VarInfo> mustBeGuarded = getGuardingList(); 1733 1734 if (mustBeGuarded.isEmpty()) { 1735 if (debugGuarding.isLoggable(Level.FINE)) { 1736 debugGuarding.fine("No guarding is needed, returning"); 1737 } 1738 return null; 1739 } 1740 1741 // This conjunction would look better if it was built up right-to-left. 1742 Invariant guardingPredicate = null; 1743 for (VarInfo vi : mustBeGuarded) { 1744 Invariant currentGuard = vi.createGuardingPredicate(install); 1745 if (currentGuard == null) { 1746 continue; 1747 } 1748 debugGuarding.fine(String.format("VarInfo %s guard is %s", vi, currentGuard)); 1749 if (guardingPredicate == null) { 1750 guardingPredicate = currentGuard; 1751 } else { 1752 guardingPredicate = new AndJoiner(ppt.parent, guardingPredicate, currentGuard); 1753 } 1754 debugGuarding.fine(String.format(" predicate so far: %s", guardingPredicate)); 1755 } 1756 1757 // If the guarding predicate has been previously constructed, return it. 1758 // Otherwise, we will return the newly constructed one. 1759 // This algorithm is inefficient. 1760 if (guardingPredicate != null) { // equivalently: mustBeGuarded.size() > 1 1761 List<Invariant> joinerViewInvs = ppt.parent.joiner_view.invs; 1762 for (Invariant currentInv : joinerViewInvs) { 1763 if (currentInv.isSameInvariant(guardingPredicate)) { 1764 return currentInv; 1765 } 1766 } 1767 } 1768 return guardingPredicate; 1769 } 1770 1771 /** 1772 * Return a list of all the variables that must be non-null in order for this invariant to be 1773 * evaluated. For instance, it this invariant is "a.b.c > d.e" (where c and e are of integer 1774 * type), then it doesn't make sense to evaluate the invariant unless "a" is non-null, "a.b" is 1775 * non-null, and "d" is non-null. So, another way to write the invariant (in "guarded" form) would 1776 * be "a != null && a.b != null && d != null && a.b.c > d.e". 1777 */ 1778 public List<VarInfo> getGuardingList(@NonPrototype Invariant this) { 1779 return getGuardingList(ppt.var_infos); 1780 } 1781 1782 /** 1783 * Returns the union of calling VarInfo.getGuardingList on each element of the argument. 1784 * 1785 * @param varInfos an array of VarInfo 1786 * @return the union of calling VarInfo.getGuardingList on each element of the argument 1787 */ 1788 public static List<VarInfo> getGuardingList(VarInfo[] varInfos) { 1789 List<VarInfo> guardingList = new ArrayList<>(); 1790 1791 for (int i = 0; i < varInfos.length; i++) { 1792 // debugGuarding.fine (varInfos[i]); 1793 guardingList.addAll(varInfos[i].getGuardingList()); 1794 // debugGuarding.fine (guardingSet.toString()); 1795 } 1796 1797 return CollectionsPlume.withoutDuplicates(guardingList); 1798 } 1799 1800 // This is called only from finally_print_the_invariants(). 1801 // Nothing is ever done with the result except print it and discard it. 1802 /** 1803 * This procedure guards one invariant and returns the resulting guarded invariant (implication), 1804 * without placing it in any slice and without modifying the original invariant. Returns null if 1805 * the invariant does not need to be guarded. 1806 */ 1807 public @Nullable @NonPrototype Invariant createGuardedInvariant(boolean install) { 1808 if (Daikon.dkconfig_guardNulls == "never") { // interned 1809 return null; 1810 } 1811 1812 if (debugGuarding.isLoggable(Level.FINE)) { 1813 debugGuarding.fine(" Trying to add guard for: " + this + "; repr = " + repr()); 1814 } 1815 if (isGuardingPredicate) { 1816 debugGuarding.fine(" Do not guard: this is a guarding predicate"); 1817 return null; 1818 } 1819 Invariant guardingPredicate = createGuardingPredicate(install); 1820 if (debugGuarding.isLoggable(Level.FINE)) { 1821 if (guardingPredicate != null) { 1822 debugGuarding.fine(" Predicate: " + guardingPredicate.format()); 1823 debugGuarding.fine(" Consequent: " + format()); 1824 } else { 1825 debugGuarding.fine(" No implication needed"); 1826 } 1827 } 1828 1829 if (guardingPredicate == null) { 1830 return null; 1831 } 1832 1833 Implication guardingImplication = 1834 GuardingImplication.makeGuardingImplication(ppt.parent, guardingPredicate, this, false); 1835 1836 if (install) { 1837 if (!ppt.parent.joiner_view.hasImplication(guardingImplication)) { 1838 ppt.parent.joiner_view.addInvariant(guardingImplication); 1839 } 1840 } 1841 return guardingImplication; 1842 } 1843 1844 /** 1845 * Instantiates (creates) an invariant of the same class on the specified slice. Must be 1846 * overridden in each class. Must be used rather than {@link #clone} so that checks in {@link 1847 * #instantiate} for reasonable invariants are done. 1848 * 1849 * <p>The implementation of this method is almost always {@code return new 1850 * <em>InvName</em>(slice);} 1851 * 1852 * @return the new invariant 1853 */ 1854 protected abstract @NonPrototype Invariant instantiate_dyn( 1855 @Prototype Invariant this, PptSlice slice); 1856 1857 /** 1858 * Returns whether or not this class of invariants is currently enabled. 1859 * 1860 * <p>Its implementation is almost always {@code return dkconfig_enabled;}. 1861 */ 1862 public abstract boolean enabled(@Prototype Invariant this); 1863 1864 /** 1865 * Returns whether or not the invariant is valid over the basic types in vis. This only checks 1866 * basic types (scalar, string, array, etc) and should match the basic superclasses of invariant 1867 * (SingleFloat, SingleScalarSequence, ThreeScalar, etc). More complex checks that depend on 1868 * variable details can be implemented in instantiate_ok(). 1869 * 1870 * @see #instantiate_ok(VarInfo[]) 1871 */ 1872 public abstract boolean valid_types(@Prototype Invariant this, VarInfo[] vis); 1873 1874 /** 1875 * Returns true if it makes sense to instantiate this invariant over the specified variables. 1876 * Checks details beyond what is provided by {@link #valid_types}. This should never be called 1877 * without calling valid_types() first (implementations should be able to presume that 1878 * valid_types() returns true). 1879 * 1880 * <p>This method does not have to be overridden; the default implementation in Invariant returns 1881 * true. 1882 * 1883 * @see #valid_types(VarInfo[]) 1884 */ 1885 public boolean instantiate_ok(@Prototype Invariant this, VarInfo[] vis) { 1886 return true; 1887 } 1888 1889 // Every Invariant is either a regular Invariant, or a "prototype" 1890 // Invariant. A prototype invariant is really a factory. The 1891 // "instantiate" method should only be called on a prototype invariant, 1892 // and many methods should only be called on non-prototype methods. 1893 // Another (arguably better, though less convenient in certain ways) 1894 // design would not represent the factory as an Invariant object. An 1895 // object never transitions at run time between being a factory/prototype 1896 // and being a normal invariant. 1897 // 1898 // Could we just use the class, such as Positive.class, as (a proxy for) 1899 // the factory? 1900 // * That would require use of reflection to call the constructor, which 1901 // is ugly. 1902 // * The factory needs at least some state is needed, for example to 1903 // distinguish between creating a division operator "a/b" vs. "b/a". 1904 // 1905 // Could the factories be represented by a separate class, unrelated in 1906 // the type hierarchy to Invariant? 1907 // * That would probably be a better design. 1908 // * instantiate_dyn would have to have more than just the single line that 1909 // it is right now; longer code is more error-prone. 1910 // * Not all the code for an invariant would be in a single class any 1911 // more; but it could still all be in the same file, for example. 1912 // * There are probably other difficulties that escape me at the moment. 1913 1914 /** 1915 * Instantiates this invariant over the specified slice. The slice must not be null and its 1916 * variables must be valid for this type of invariant. Returns null if the invariant is not 1917 * enabled or if the invariant is not reasonable over the specified variables. Otherwise returns 1918 * the new invariant. 1919 */ 1920 public @Nullable Invariant instantiate(@Prototype Invariant this, PptSlice slice) { 1921 1922 assert isPrototype(); // receiver should be a "prototype" invariant 1923 assert slice != null; 1924 if (!valid_types(slice.var_infos)) { 1925 System.out.printf("this.getClass(): %s%n", this.getClass()); 1926 System.out.printf("slice: %s%n", slice); 1927 System.out.printf( 1928 "slice.var_infos (length %d): %s%n", slice.var_infos.length, (Object) slice.var_infos); 1929 for (VarInfo vi : slice.var_infos) { 1930 System.out.printf(" var_info: %s %s%n", vi, vi.type); 1931 } 1932 } 1933 assert valid_types(slice.var_infos) 1934 : String.format("valid_types(%s) = false for %s", Arrays.toString(slice.var_infos), this); 1935 if (!enabled() || !instantiate_ok(slice.var_infos)) { 1936 return null; 1937 } 1938 Invariant inv = instantiate_dyn(slice); 1939 assert inv != null; 1940 if (inv.ppt == null) { 1941 // Avoid creating the message if the check succeeds 1942 assert inv.ppt != null : "invariant class " + inv.getClass(); 1943 } 1944 return inv; 1945 } 1946 1947 /** 1948 * Adds the specified sample to the invariant and returns the result. 1949 * 1950 * @param vt the sample to add to this invariant 1951 * @param count the number of occurrences of the sample to add to this invariant 1952 * @return the result of adding the samples to this invariant 1953 */ 1954 public InvariantStatus add_sample(@NonPrototype Invariant this, ValueTuple vt, int count) { 1955 1956 if (ppt instanceof PptSlice1) { 1957 1958 VarInfo v = ppt.var_infos[0]; 1959 UnaryInvariant unary_inv = (UnaryInvariant) this; 1960 return unary_inv.add(vt.getValue(v), vt.getModified(v), count); 1961 1962 } else if (ppt instanceof PptSlice2) { 1963 1964 VarInfo v1 = ppt.var_infos[0]; 1965 VarInfo v2 = ppt.var_infos[1]; 1966 BinaryInvariant bin_inv = (BinaryInvariant) this; 1967 return bin_inv.add_unordered(vt.getValue(v1), vt.getValue(v2), vt.getModified(v1), count); 1968 1969 } else /* must be ternary */ { 1970 1971 VarInfo v1 = ppt.var_infos[0]; 1972 VarInfo v2 = ppt.var_infos[1]; 1973 VarInfo v3 = ppt.var_infos[2]; 1974 assert (this instanceof TernaryInvariant) 1975 : "invariant '" + format() + "' in slice " + ppt.name() + " is not ternary"; 1976 TernaryInvariant ternary_inv = (TernaryInvariant) this; 1977 return ternary_inv.add( 1978 vt.getValue(v1), vt.getValue(v2), vt.getValue(v3), vt.getModified(v1), count); 1979 } 1980 } 1981 1982 /** Check the rep invariants of this. */ 1983 public void repCheck(@Prototype Invariant this) {} 1984 1985 /** 1986 * Returns whether or not the invariant is currently active. This is used to identify those 1987 * invariants that require a certain number of points before they actually do computation (eg, 1988 * LinearBinary) 1989 * 1990 * <p>This is used during suppresion. Any invariant that is not active cannot suppress another 1991 * invariant. 1992 * 1993 * @return true if this invariant is currently active 1994 */ 1995 @Pure 1996 public boolean isActive(@NonPrototype Invariant this) { 1997 return true; 1998 } 1999 2000 // TODO: The logDetail and (especially) logOn methods are misleading, 2001 // because they are static but are very often called with an instance as 2002 // the receiver, suggesting that they have something to do with the 2003 // receiver. This should be corrected. -MDE 2004 2005 /** 2006 * Returns true if detailed logging is on. Note that this check is not performed inside the 2007 * logging calls themselves, it must be performed by the caller. 2008 * 2009 * @return true if detailed logging is on 2010 * @see daikon.Debug#logDetail() 2011 * @see daikon.Debug#logOn() 2012 * @see daikon.Debug#log(Logger, Class, Ppt, String) 2013 */ 2014 public static boolean logDetail() { 2015 return Debug.logDetail(); 2016 } 2017 2018 /** 2019 * Returns whether or not logging is on. 2020 * 2021 * @see daikon.Debug#logOn() 2022 */ 2023 public static boolean logOn() { 2024 return Debug.logOn(); 2025 } 2026 2027 // Using `@link` leads to javadoc -Xdoclint:all crashing with: 2028 // "com.sun.tools.javac.code.Type$AnnotatedType cannot be cast to 2029 // com.sun.tools.javac.code.Type$ClassType" 2030 /** 2031 * Logs a description of the invariant and the specified msg via the logger as described in {@code 2032 * daikon.Debug#log(Logger, Class, Ppt, VarInfo[], String)}. 2033 * 2034 * @param log where to log the message 2035 * @param msg the message to log 2036 */ 2037 // receiver needs to be initialized because subclass implementations will read their own fields 2038 public void log(@NonPrototype Invariant this, Logger log, String msg) { 2039 2040 if (Debug.logOn()) { 2041 Debug.log(log, getClass(), ppt, msg); 2042 } 2043 } 2044 2045 // Using `@link` leads to javadoc -Xdoclint:all crashing with: 2046 // "com.sun.tools.javac.code.Type$AnnotatedType cannot be cast to 2047 // com.sun.tools.javac.code.Type$ClassType" 2048 /** 2049 * Logs a description of the invariant and the specified msg via the logger as described in {@code 2050 * daikon.Debug#log(Logger, Class, Ppt, VarInfo[], String)}. 2051 * 2052 * @param format a format string 2053 * @param args the argumnts to the format string 2054 * @return whether or not it logged anything 2055 */ 2056 @FormatMethod 2057 public boolean log( 2058 @UnknownInitialization(Invariant.class) @NonPrototype Invariant this, 2059 String format, 2060 @Nullable Object... args) { 2061 if (ppt != null) { 2062 String msg = format; 2063 if (args.length > 0) msg = String.format(format, args); 2064 return Debug.log(getClass(), ppt, msg); 2065 } else { 2066 return false; 2067 } 2068 } 2069 2070 // Receiver must be fully initialized 2071 @SideEffectFree 2072 @Override 2073 public String toString(@GuardSatisfied Invariant this) { 2074 return format(); 2075 } 2076 2077 /** 2078 * Return a string representation of the given invariants. 2079 * 2080 * @param invs the invariants to get a string representation of 2081 * @return a string representation of the given invariants 2082 */ 2083 public static String toString(@NonPrototype Invariant[] invs) { 2084 2085 ArrayList<String> strings = new ArrayList<>(invs.length); 2086 for (int i = 0; i < invs.length; i++) { 2087 if (invs[i] == null) { 2088 strings.add("null"); 2089 } else { 2090 strings.add(invs[i].format()); 2091 } 2092 } 2093 return String.join(", ", strings); 2094 } 2095 2096 /** 2097 * Used throughout Java family formatting of invariants. 2098 * 2099 * <p>Returns 2100 * 2101 * <p>"plume.FuzzyFloat.method(v1_name, v2_name)" 2102 * 2103 * <p>Where v1_name and v2_name are the properly formatted varinfos v1 and v2, under the given 2104 * format. 2105 */ 2106 // [[ This method doesn't belong here. But where? ]] 2107 public static String formatFuzzy(String method, VarInfo v1, VarInfo v2, OutputFormat format) { 2108 2109 StringBuilder results = new StringBuilder(); 2110 return results 2111 .append("daikon.Quant.fuzzy.") 2112 .append(method) 2113 .append("(") 2114 .append(v1.name_using(format)) 2115 .append(", ") 2116 .append(v2.name_using(format)) 2117 .append(")") 2118 .toString(); 2119 } 2120 2121 @SuppressWarnings("unchecked") // casting method 2122 public static Class<? extends Invariant> asInvClass(Object x) { 2123 return (Class<? extends Invariant>) x; 2124 } 2125 2126 /** 2127 * Returns true if this is an equality comparison. That is, returns true if this Invariant 2128 * satisfies the following conditions: 2129 * 2130 * <ul> 2131 * <li>the Invariant is an EqualityComparison (its relationship is =, not <, ≤, >, or 2132 * ≥). 2133 * <li>the invariant is statistically satisfied (its confidence is above the limit) 2134 * </ul> 2135 * 2136 * This does not consider PairwiseIntComparison to be an equality invariant. 2137 */ 2138 public boolean isEqualityComparison() { 2139 if (!(this instanceof EqualityComparison)) { 2140 return false; 2141 } 2142 double chance_conf = ((EqualityComparison) this).eq_confidence(); 2143 return chance_conf > Invariant.dkconfig_confidence_limit; 2144 } 2145 2146 /** 2147 * Throws an exception if this object is invalid. 2148 * 2149 * @exception RuntimeException if representation invariant on this is broken 2150 */ 2151 public void checkRep() { 2152 // very partial initial implementation 2153 for (VarInfo vi : ppt.var_infos) { 2154 vi.checkRep(); 2155 } 2156 } 2157}