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