001// ***** This file is automatically generated from Range.java.jpp 002 003package daikon.inv.unary.scalar; 004 005import org.checkerframework.dataflow.qual.Pure; 006import org.checkerframework.checker.lock.qual.GuardSatisfied; 007import org.checkerframework.dataflow.qual.SideEffectFree; 008import org.checkerframework.checker.interning.qual.Interned; 009import org.checkerframework.checker.nullness.qual.Nullable; 010import daikon.*; 011import daikon.Quantify.QuantFlags; 012import daikon.derive.unary.*; 013import daikon.inv.*; 014import daikon.inv.binary.sequenceScalar.*; 015import daikon.inv.unary.sequence.*; 016import java.util.*; 017import java.util.logging.Level; 018import java.util.logging.Logger; 019import org.plumelib.util.Intern; 020import org.plumelib.util.UtilPlume; 021import typequals.prototype.qual.NonPrototype; 022import typequals.prototype.qual.Prototype; 023 024/** 025 * Baseclass for unary range based invariants. Each invariant is a special stateless version of 026 * bound or oneof. For example EqualZero, BooleanVal, etc). These are never printed, but are used 027 * internally as suppressors for ni-suppressions. 028 * 029 * Each specific invariant is implemented in a subclass (typically in this file). 030 */ 031 032public abstract class RangeInt extends SingleScalar { 033 034 // We are Serializable, so we specify a version to allow changes to 035 // method signatures without breaking serialization. If you add or 036 // remove fields, you should change this number to the current date. 037 static final long serialVersionUID = 20040311L; 038 039 protected RangeInt(PptSlice ppt) { 040 super(ppt); 041 } 042 043 protected @Prototype RangeInt() { 044 super(); 045 } 046 047 /** 048 * Check that instantiation is ok. The type must be integral 049 * (not boolean or hash code). 050 */ 051 @Override 052 public boolean instantiate_ok(VarInfo[] vis) { 053 054 if (!valid_types(vis)) { 055 return false; 056 } 057 058 if (!vis[0].file_rep_type.baseIsIntegral()) { 059 return false; 060 } 061 062 return true; 063 } 064 065 /** 066 * Returns a string in the specified format that describes the invariant. 067 * 068 * The generic format string is obtained from the subclass specific get_format_str(). Instances of 069 * %var1% are replaced by the variable name in the specified format. 070 */ 071 @SideEffectFree 072 @Override 073 public String format_using(@GuardSatisfied RangeInt this, OutputFormat format) { 074 075 String fmt_str = get_format_str(format); 076 077 VarInfo var1 = ppt.var_infos[0]; 078 String v1 = null; 079 080 if (v1 == null) { 081 v1 = var1.name_using(format); 082 } 083 084 fmt_str = fmt_str.replace("%var1%", v1); 085 return fmt_str; 086 } 087 088 @Override 089 public InvariantStatus check_modified(long x, int count) { 090 if (eq_check(x)) { 091 return InvariantStatus.NO_CHANGE; 092 } else { 093 return InvariantStatus.FALSIFIED; 094 } 095 } 096 097 @Override 098 public InvariantStatus add_modified(long x, int count) { 099 return check_modified(x, count); 100 } 101 102 @Override 103 protected double computeConfidence() { 104 return CONFIDENCE_JUSTIFIED; 105 } 106 107 @Pure 108 @Override 109 public boolean isSameFormula(Invariant other) { 110 assert other.getClass() == getClass(); 111 return true; 112 } 113 @Pure 114 @Override 115 public boolean isExclusiveFormula(Invariant other) { 116 return false; 117 } 118 119 /** 120 * All range invariants except Even and PowerOfTwo are obvious since they represented by some 121 * version of OneOf or Bound. 122 */ 123 @Pure 124 @Override 125 public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) { 126 127 return new DiscardInfo(this, DiscardCode.obvious, 128 "Implied by Oneof or Bound"); 129 } 130 131 /** 132 * Looks for a OneOf invariant over vis. Used by Even and PowerOfTwo to dynamically suppress those 133 * invariants if a OneOf exists. 134 */ 135 protected @Nullable OneOfScalar find_oneof(VarInfo[] vis) { 136 return (OneOfScalar) ppt.parent.find_inv_by_class(vis, OneOfScalar.class); 137 } 138 139 /** 140 * Return a format string for the specified output format. Each instance of %varN% will be 141 * replaced by the correct name for varN. 142 */ 143 public abstract String get_format_str(@GuardSatisfied RangeInt this, OutputFormat format); 144 145 /** Returns true if x and y don't invalidate the invariant. */ 146 public abstract boolean eq_check(long x); 147 148 /** 149 * Returns a list of prototypes of all of the range 150 * invariants. 151 */ 152 public static List<@Prototype Invariant> get_proto_all() { 153 154 List<@Prototype Invariant> result = new ArrayList<>(); 155 result.add(EqualZero.get_proto()); 156 result.add(EqualOne.get_proto()); 157 result.add(EqualMinusOne.get_proto()); 158 result.add(GreaterEqualZero.get_proto()); 159 result.add(GreaterEqual64.get_proto()); 160 161 result.add(BooleanVal.get_proto()); 162 result.add(PowerOfTwo.get_proto()); 163 result.add(Even.get_proto()); 164 result.add(Bound0_63.get_proto()); 165 166 return result; 167 } 168 169 /** 170 * Internal invariant representing long scalars that are equal to zero. Used for 171 * non-instantiating suppressions. Will never print since OneOf accomplishes the same thing. 172 */ 173 public static class EqualZero extends RangeInt { 174 175 // We are Serializable, so we specify a version to allow changes to 176 // method signatures without breaking serialization. If you add or 177 // remove fields, you should change this number to the current date. 178 static final long serialVersionUID = 20040113L; 179 180 protected EqualZero(PptSlice ppt) { 181 super(ppt); 182 } 183 184 protected @Prototype EqualZero() { 185 super(); 186 } 187 188 private static @Prototype EqualZero proto = new @Prototype EqualZero(); 189 190 /** returns the prototype invariant */ 191 public static @Prototype EqualZero get_proto() { 192 return proto; 193 } 194 195 /** Returns whether or not this invariant is enabled. */ 196 @Override 197 public boolean enabled() { 198 return OneOfScalar.dkconfig_enabled; 199 } 200 201 /** instantiates the invariant on the specified slice */ 202 @Override 203 public EqualZero instantiate_dyn(@Prototype EqualZero this, PptSlice slice) { 204 return new EqualZero(slice); 205 } 206 207 @Override 208 public String get_format_str(@GuardSatisfied EqualZero this, OutputFormat format) { 209 if (format == OutputFormat.SIMPLIFY) { 210 return "(EQ 0 %var1%)"; 211 } else { 212 return "%var1% == 0"; 213 } 214 } 215 216 @Override 217 public boolean eq_check(long x) { 218 return x == 0; 219 } 220 } 221 222 /** 223 * Internal invariant representing long scalars that are equal to one. Used for 224 * non-instantiating suppressions. Will never print since OneOf accomplishes the same thing. 225 */ 226 public static class EqualOne extends RangeInt { 227 228 // We are Serializable, so we specify a version to allow changes to 229 // method signatures without breaking serialization. If you add or 230 // remove fields, you should change this number to the current date. 231 static final long serialVersionUID = 20040113L; 232 233 protected EqualOne(PptSlice ppt) { 234 super(ppt); 235 } 236 237 protected @Prototype EqualOne() { 238 super(); 239 } 240 241 private static @Prototype EqualOne proto = new @Prototype EqualOne(); 242 243 /** returns the prototype invariant */ 244 public static @Prototype EqualOne get_proto() { 245 return proto; 246 } 247 248 /** Returns whether or not this invariant is enabled. */ 249 @Override 250 public boolean enabled() { 251 return OneOfScalar.dkconfig_enabled; 252 } 253 254 /** instantiates the invariant on the specified slice */ 255 @Override 256 public EqualOne instantiate_dyn(@Prototype EqualOne this, PptSlice slice) { 257 return new EqualOne(slice); 258 } 259 260 @Override 261 public String get_format_str(@GuardSatisfied EqualOne this, OutputFormat format) { 262 if (format == OutputFormat.SIMPLIFY) { 263 return "(EQ 1 %var1%)"; 264 } else { 265 return "%var1% == 1"; 266 } 267 } 268 269 @Override 270 public boolean eq_check(long x) { 271 return x == 1; 272 } 273 } 274 275 /** 276 * Internal invariant representing long scalars that are equal to minus one. Used for 277 * non-instantiating suppressions. Will never print since OneOf accomplishes the same thing. 278 */ 279 public static class EqualMinusOne extends RangeInt { 280 281 // We are Serializable, so we specify a version to allow changes to 282 // method signatures without breaking serialization. If you add or 283 // remove fields, you should change this number to the current date. 284 static final long serialVersionUID = 20040824L; 285 286 protected EqualMinusOne(PptSlice ppt) { 287 super(ppt); 288 } 289 290 protected @Prototype EqualMinusOne() { 291 super(); 292 } 293 294 private static @Prototype EqualMinusOne proto = new @Prototype EqualMinusOne(); 295 296 /** returns the prototype invariant */ 297 public static @Prototype EqualMinusOne get_proto() { 298 return proto; 299 } 300 301 /** Returns whether or not this invariant is enabled. */ 302 @Override 303 public boolean enabled() { 304 return OneOfScalar.dkconfig_enabled; 305 } 306 307 /** instantiates the invariant on the specified slice */ 308 @Override 309 public EqualMinusOne instantiate_dyn(@Prototype EqualMinusOne this, PptSlice slice) { 310 return new EqualMinusOne(slice); 311 } 312 313 @Override 314 public String get_format_str(@GuardSatisfied EqualMinusOne this, OutputFormat format) { 315 if (format == OutputFormat.SIMPLIFY) { 316 return "(EQ -1 %var1%)"; 317 } else { 318 return "%var1% == -1"; 319 } 320 } 321 322 @Override 323 public boolean eq_check(long x) { 324 return x == -1; 325 } 326 } 327 328 /** 329 * Internal invariant representing long scalars that are greater than or equal to 0. Used 330 * for non-instantiating suppressions. Will never print since Bound accomplishes the same thing. 331 */ 332 public static class GreaterEqualZero extends RangeInt { 333 334 // We are Serializable, so we specify a version to allow changes to 335 // method signatures without breaking serialization. If you add or 336 // remove fields, you should change this number to the current date. 337 static final long serialVersionUID = 20040113L; 338 339 protected GreaterEqualZero(PptSlice ppt) { 340 super(ppt); 341 } 342 343 protected @Prototype GreaterEqualZero() { 344 super(); 345 } 346 347 private static @Prototype GreaterEqualZero proto = new @Prototype GreaterEqualZero(); 348 349 /** returns the prototype invariant */ 350 public static @Prototype GreaterEqualZero get_proto() { 351 return proto; 352 } 353 354 /** Returns whether or not this invariant is enabled. */ 355 @Override 356 public boolean enabled() { 357 return LowerBound.dkconfig_enabled; 358 } 359 360 /** instantiates the invariant on the specified slice */ 361 @Override 362 public GreaterEqualZero instantiate_dyn(@Prototype GreaterEqualZero this, PptSlice slice) { 363 return new GreaterEqualZero(slice); 364 } 365 366 @Override 367 public String get_format_str(@GuardSatisfied GreaterEqualZero this, OutputFormat format) { 368 if (format == OutputFormat.SIMPLIFY) { 369 return "(>= %var1% 0)"; 370 } else { 371 return "%var1% >= 0"; 372 } 373 } 374 375 @Override 376 public boolean eq_check(long x) { 377 return x >= 0; 378 } 379 } 380 381 /** 382 * Internal invariant representing long scalars that are greater than or equal to 64. Used 383 * for non-instantiating suppressions. Will never print since Bound accomplishes the same thing. 384 */ 385 public static class GreaterEqual64 extends RangeInt { 386 387 // We are Serializable, so we specify a version to allow changes to 388 // method signatures without breaking serialization. If you add or 389 // remove fields, you should change this number to the current date. 390 static final long serialVersionUID = 20040113L; 391 392 protected GreaterEqual64(PptSlice ppt) { 393 super(ppt); 394 } 395 396 protected @Prototype GreaterEqual64() { 397 super(); 398 } 399 400 private static @Prototype GreaterEqual64 proto = new @Prototype GreaterEqual64(); 401 402 /** returns the prototype invariant */ 403 public static @Prototype GreaterEqual64 get_proto() { 404 return proto; 405 } 406 407 /** Returns whether or not this invariant is enabled. */ 408 @Override 409 public boolean enabled() { 410 return LowerBound.dkconfig_enabled; 411 } 412 413 /** instantiates the invariant on the specified slice */ 414 @Override 415 public GreaterEqual64 instantiate_dyn(@Prototype GreaterEqual64 this, PptSlice slice) { 416 return new GreaterEqual64(slice); 417 } 418 419 @Override 420 public String get_format_str(@GuardSatisfied GreaterEqual64 this, OutputFormat format) { 421 if (format == OutputFormat.SIMPLIFY) { 422 return "(>= %var1% 64)"; 423 } else { 424 return "%var1% >= 64"; 425 } 426 } 427 428 @Override 429 public boolean eq_check(long x) { 430 return x >= 64; 431 } 432 } 433 434 /** 435 * Internal invariant representing longs whose values are always 0 or 1. Used for 436 * non-instantiating suppressions. Will never print since OneOf accomplishes the same thing. 437 */ 438 public static class BooleanVal extends RangeInt { 439 440 // We are Serializable, so we specify a version to allow changes to 441 // method signatures without breaking serialization. If you add or 442 // remove fields, you should change this number to the current date. 443 static final long serialVersionUID = 20040113L; 444 445 protected BooleanVal(PptSlice ppt) { 446 super(ppt); 447 } 448 449 protected @Prototype BooleanVal() { 450 super(); 451 } 452 453 private static @Prototype BooleanVal proto = new @Prototype BooleanVal(); 454 455 /** returns the prototype invariant */ 456 public static @Prototype BooleanVal get_proto() { 457 return proto; 458 } 459 460 /** Returns whether or not this invariant is enabled. */ 461 @Override 462 public boolean enabled() { 463 return LowerBound.dkconfig_enabled && UpperBound.dkconfig_enabled; 464 } 465 466 /** instantiates the invariant on the specified slice */ 467 @Override 468 public BooleanVal instantiate_dyn(@Prototype BooleanVal this, PptSlice slice) { 469 return new BooleanVal(slice); 470 } 471 472 @Override 473 public String get_format_str(@GuardSatisfied BooleanVal this, OutputFormat format) { 474 if (format == OutputFormat.SIMPLIFY) { 475 return "(OR (EQ 0 %var1%) (EQ 1 %var1%))"; 476 } else { 477 return "%var1% is boolean"; 478 } 479 } 480 481 @Override 482 public boolean eq_check(long x) { 483 return (x == 0) || (x == 1); 484 } 485 } 486 487 /** 488 * Invariant representing longs whose values are always a power of 2 (exactly one bit is set). 489 * Used for non-instantiating suppressions. Since this is not covered by the Bound or OneOf 490 * invariants it is printed. Prints as {@code x is a power of 2}. 491 */ 492 public static class PowerOfTwo extends RangeInt { 493 494 // We are Serializable, so we specify a version to allow changes to 495 // method signatures without breaking serialization. If you add or 496 // remove fields, you should change this number to the current date. 497 static final long serialVersionUID = 20040113L; 498 499 /** Boolean. True if PowerOfTwo invariants should be considered. */ 500 public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault; 501 502 protected PowerOfTwo(PptSlice ppt) { 503 super(ppt); 504 } 505 506 protected @Prototype PowerOfTwo() { 507 super(); 508 } 509 510 private static @Prototype PowerOfTwo proto = new @Prototype PowerOfTwo(); 511 512 /** returns the prototype invariant */ 513 public static @Prototype PowerOfTwo get_proto() { 514 return proto; 515 } 516 517 /** returns whether or not this invariant is enabled */ 518 @Override 519 public boolean enabled() { 520 return dkconfig_enabled; 521 } 522 523 /** instantiates the invariant on the specified slice */ 524 @Override 525 public PowerOfTwo instantiate_dyn(@Prototype PowerOfTwo this, PptSlice slice) { 526 return new PowerOfTwo(slice); 527 } 528 529 @Override 530 public String get_format_str(@GuardSatisfied PowerOfTwo this, OutputFormat format) { 531 if (format == OutputFormat.SIMPLIFY) { 532 return "(EXISTS (p) (EQ %var1% (pow 2 p)))"; 533 } 534 if (format == OutputFormat.JAVA) { 535 return "daikon.tools.runtimechecker.Runtime.isPowerOfTwo(%var1%)"; 536 } 537 if (format == OutputFormat.CSHARPCONTRACT) { 538 return "%var1%.IsPowerOfTwo()"; 539 } else { 540 return "%var1% is a power of 2"; 541 } 542 } 543 544 /** 545 * Returns true if x is a power of 2 (has one bit on). The check is to and x with itself - 546 * 1. The theory is that if there are multiple bits turned on, at least one of those bits is 547 * unmodified by a subtract operation and thus the bitwise-and be non-zero. There is probably a 548 * more elegant way to do this. 549 */ 550 @Override 551 public boolean eq_check(long x) { 552 return (x >= 1) && ((x & (x - 1)) == 0); 553 } 554 555 /** 556 * Since PowerOfTwo is not covered by Bound or OneOf, it is not obvious 557 * (and should thus be printed). 558 */ 559 @Pure 560 @Override 561 public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) { 562 563 OneOfScalar oneof = find_oneof(vis); 564 if (oneof != null) { 565 return new DiscardInfo(this, DiscardCode.obvious, "Implied by Oneof"); 566 } 567 568 return null; 569 } 570 571 } 572 573 /** 574 * Invariant representing longs whose values are always even. Used for non-instantiating 575 * suppressions. Since this is not covered by the Bound or OneOf invariants it is printed. Prints 576 * as {@code x is even}. 577 */ 578 public static class Even extends RangeInt { 579 580 // We are Serializable, so we specify a version to allow changes to 581 // method signatures without breaking serialization. If you add or 582 // remove fields, you should change this number to the current date. 583 static final long serialVersionUID = 20040113L; 584 585 /** Boolean. True if Even invariants should be considered. */ 586 public static boolean dkconfig_enabled = false; 587 588 protected Even(PptSlice ppt) { 589 super(ppt); 590 } 591 592 protected @Prototype Even() { 593 super(); 594 } 595 596 private static @Prototype Even proto = new @Prototype Even(); 597 598 /** returns the prototype invariant */ 599 public static @Prototype Even get_proto() { 600 return proto; 601 } 602 603 /** returns whether or not this invariant is enabled */ 604 @Override 605 public boolean enabled() { 606 return dkconfig_enabled; 607 } 608 609 /** instantiates the invariant on the specified slice */ 610 @Override 611 public Even instantiate_dyn(@Prototype Even this, PptSlice slice) { 612 return new Even(slice); 613 } 614 615 @Override 616 public String get_format_str(@GuardSatisfied Even this, OutputFormat format) { 617 if (format == OutputFormat.SIMPLIFY) { 618 return "(EQ (MOD %var1% 2) 0)"; 619 } 620 if (format == OutputFormat.CSHARPCONTRACT) { 621 return "%var1% % 2 == 0"; 622 } else { 623 return "%var1% is even"; 624 } 625 } 626 627 @Override 628 public boolean eq_check(long x) { 629 return (x & 1) == 0; 630 } 631 632 /** 633 * Since Even is not covered by Bound or OneOf, it is not obvious 634 * (and should thus be printed). 635 */ 636 @Pure 637 @Override 638 public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) { 639 // If there is a oneof, it implies this 640 OneOfScalar oneof = find_oneof(vis); 641 if (oneof != null) { 642 return new DiscardInfo(this, DiscardCode.obvious, "Implied by Oneof"); 643 } 644 645 return null; 646 } 647 } 648 649 /** 650 * Internal invariant representing longs whose values are between 0 and 63. Used for 651 * non-instantiating suppressions. Will never print since Bound accomplishes the same thing. 652 */ 653 public static class Bound0_63 extends RangeInt { 654 655 // We are Serializable, so we specify a version to allow changes to 656 // method signatures without breaking serialization. If you add or 657 // remove fields, you should change this number to the current date. 658 static final long serialVersionUID = 20040113L; 659 660 protected Bound0_63(PptSlice ppt) { 661 super(ppt); 662 } 663 664 protected @Prototype Bound0_63() { 665 super(); 666 } 667 668 private static @Prototype Bound0_63 proto = new @Prototype Bound0_63(); 669 670 /** returns the prototype invariant */ 671 public static @Prototype Bound0_63 get_proto() { 672 return proto; 673 } 674 675 /** Returns whether or not this invariant is enabled. */ 676 @Override 677 public boolean enabled() { 678 return LowerBound.dkconfig_enabled && UpperBound.dkconfig_enabled; 679 } 680 681 /** instantiates the invariant on the specified slice */ 682 @Override 683 public Bound0_63 instantiate_dyn(@Prototype Bound0_63 this, PptSlice slice) { 684 return new Bound0_63(slice); 685 } 686 687 @Override 688 public String get_format_str(@GuardSatisfied Bound0_63 this, OutputFormat format) { 689 if (format == OutputFormat.SIMPLIFY) { 690 return "(AND (>= %var1% 0) (>= 63 %var1%))"; 691 } else { 692 return "0 <= %var1% <= 63"; 693 } 694 } 695 696 @Override 697 public boolean eq_check(long x) { 698 return (x >= 0) && (x <= 63); 699 } 700 } 701 702}