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