001// ***** This file is automatically generated from Numeric.java.jpp 002 003package daikon.inv.binary.twoScalar; 004 005import org.checkerframework.checker.lock.qual.GuardSatisfied; 006import org.checkerframework.checker.nullness.qual.NonNull; 007import org.checkerframework.checker.nullness.qual.Nullable; 008import org.checkerframework.checker.signature.qual.ClassGetName; 009import org.checkerframework.dataflow.qual.Pure; 010import org.checkerframework.dataflow.qual.SideEffectFree; 011import static daikon.inv.Invariant.asInvClass; 012 013import daikon.*; 014import daikon.Quantify.QuantFlags; 015import daikon.derive.binary.*; 016import daikon.inv.*; 017import daikon.inv.binary.twoScalar.*; 018import daikon.inv.binary.twoString.*; 019import daikon.inv.unary.scalar.*; 020import daikon.inv.unary.sequence.*; 021import daikon.suppress.*; 022import java.util.*; 023import org.plumelib.util.UtilPlume; 024import typequals.prototype.qual.NonPrototype; 025import typequals.prototype.qual.Prototype; 026 027/** 028 * Baseclass for binary numeric invariants. 029 * 030 * Each specific invariant is implemented in a subclass (typically, in this file). The subclass must 031 * provide the methods instantiate(), check(), and format(). Symmetric functions should define 032 * is_symmetric() to return true. 033 */ 034public abstract class NumericInt extends TwoScalar { 035 036 // We are Serializable, so we specify a version to allow changes to 037 // method signatures without breaking serialization. If you add or 038 // remove fields, you should change this number to the current date. 039 static final long serialVersionUID = 20060609L; 040 041 protected NumericInt(PptSlice ppt, boolean swap) { 042 super(ppt); 043 this.swap = swap; 044 } 045 046 protected NumericInt(boolean swap) { 047 super(); 048 this.swap = swap; 049 } 050 051 /** Returns true if it is ok to instantiate a numeric invariant over the specified slice. */ 052 @Override 053 public boolean instantiate_ok(VarInfo[] vis) { 054 055 ProglangType type1 = vis[0].file_rep_type; 056 ProglangType type2 = vis[1].file_rep_type; 057 if (!type1.isIntegral() || !type2.isIntegral()) { 058 return false; 059 } 060 061 return true; 062 } 063 064 @Pure 065 @Override 066 public boolean isExact() { 067 return true; 068 } 069 070 @Override 071 public String repr(@GuardSatisfied NumericInt this) { 072 return getClass().getSimpleName() + ": " + format() 073 + (swap ? " [swapped]" : " [unswapped]"); 074 } 075 076 /** 077 * Returns a string in the specified format that describes the invariant. 078 * 079 * The generic format string is obtained from the subclass specific get_format_str(). Instances of 080 * %varN% are replaced by the variable name in the specified format. 081 */ 082 @SideEffectFree 083 @Override 084 public String format_using(@GuardSatisfied NumericInt this, OutputFormat format) { 085 086 if (ppt == null) { 087 return String.format("proto ppt [class %s] format %s", getClass(), 088 get_format_str(format)); 089 } 090 String fmt_str = get_format_str(format); 091 092 String v1 = var1().name_using(format); 093 String v2 = var2().name_using(format); 094 095 // Note that we do not use String.replaceAll here, because that's 096 // inseparable from the regex library, and we don't want to have to 097 // escape v1 with something like 098 // v1.replaceAll("([\\$\\\\])", "\\\\$1") 099 fmt_str = fmt_str.replace("%var1%", v1); 100 fmt_str = fmt_str.replace("%var2%", v2); 101 102 // if (false && (format == OutputFormat.DAIKON)) { 103 // fmt_str = "[" + getClass() + "]" + fmt_str + " (" 104 // + var1().get_value_info() + ", " + var2().get_value_info() + ")"; 105 // } 106 return fmt_str; 107 } 108 109 /** Calls the function specific equal check and returns the correct status. */ 110 111 @Override 112 public InvariantStatus check_modified(long x, long y, int count) { 113 114 try { 115 if (eq_check(x, y)) { 116 return InvariantStatus.NO_CHANGE; 117 } else { 118 return InvariantStatus.FALSIFIED; 119 } 120 } catch (Exception e) { 121 return InvariantStatus.FALSIFIED; 122 } 123 } 124 125 /** 126 * Checks to see if 'x[a] op y[b]' where 'x[] op y[]' and 'a == b'. Doesn't catch the case where 127 * a = b+1. 128 */ 129 public @Nullable DiscardInfo is_subscript(VarInfo[] vis) { 130 131 VarInfo v1 = var1(vis); 132 VarInfo v2 = var2(vis); 133 134 // Make sure each var is a sequence subscript 135 if (!v1.isDerived() || !(v1.derived instanceof SequenceScalarSubscript)) { 136 return null; 137 } 138 if (!v2.isDerived() || !(v2.derived instanceof SequenceScalarSubscript)) { 139 return null; 140 } 141 142 @NonNull SequenceScalarSubscript der1 = (SequenceScalarSubscript) v1.derived; 143 @NonNull SequenceScalarSubscript der2 = (SequenceScalarSubscript) v2.derived; 144 145 // Make sure the shifts match 146 if (der1.index_shift != der2.index_shift) { 147 return null; 148 } 149 150 // Look for this invariant over a sequence 151 String cstr = getClass().getName(); 152 cstr = cstr.replaceFirst("Numeric", "PairwiseNumeric"); 153 cstr = cstr.replaceFirst("twoScalar", "twoSequence"); 154 cstr = cstr.replaceFirst("twoFloat", "twoSequence"); 155 Class<? extends Invariant> pairwise_class; 156 try { 157 @SuppressWarnings("signature") // string manipulation; application invariants 158 @ClassGetName String cstr_cgn = cstr; 159 pairwise_class = asInvClass(Class.forName(cstr_cgn)); 160 } catch (Exception e) { 161 throw new Error("can't create class for " + cstr, e); 162 } 163 Invariant inv = find(pairwise_class, der1.seqvar(), der2.seqvar()); 164 if (inv == null) { 165 return null; 166 } 167 168 // Look to see if the subscripts are equal 169 Invariant subinv = find(IntEqual.class, der1.sclvar(), der2.sclvar()); 170 if (subinv == null) { 171 return null; 172 } 173 174 return new DiscardInfo(this, DiscardCode.obvious, "Implied by " 175 + inv.format() + " and " + subinv.format()); 176 } 177 178 @Pure 179 @Override 180 public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) { 181 182 DiscardInfo super_result = super.isObviousDynamically(vis); 183 if (super_result != null) { 184 return super_result; 185 } 186 187 // any relation across subscripts is made obvious by the same 188 // relation across the original sequence if the subscripts are equal 189 DiscardInfo result = is_subscript(vis); 190 if (result != null) { 191 return result; 192 } 193 194 // Check for invariant specific obvious checks. The obvious_checks 195 // method returns an array of arrays of antecedents. If all of the 196 // antecedents in an array are true, then the invariant is obvoius. 197 InvDef[][] obvious_arr = obvious_checks(vis); 198 obvious_loop: 199 for (int i = 0; i < obvious_arr.length; i++) { 200 InvDef[] antecedents = obvious_arr[i]; 201 StringBuilder why = null; 202 for (int j = 0; j < antecedents.length; j++) { 203 Invariant inv = antecedents[j].find(); 204 if (inv == null) { 205 continue obvious_loop; 206 } 207 if (why == null) { 208 why = new StringBuilder(inv.format()); 209 } else { 210 why.append(" and "); 211 why.append(inv.format()); 212 } 213 } 214 return new DiscardInfo(this, DiscardCode.obvious, "Implied by " + why); 215 } 216 217 return null; 218 } 219 220 /** 221 * Return a format string for the specified output format. Each instance of %varN% will be 222 * replaced by the correct name for varN. 223 */ 224 public abstract String get_format_str(@GuardSatisfied NumericInt this, OutputFormat format); 225 226 /** Returns true if x and y don't invalidate the invariant. */ 227 public abstract boolean eq_check(long x, long y); 228 229 /** 230 * Returns an array of arrays of antecedents. If all of the antecedents in any array are true, 231 * then the invariant is obvious. 232 */ 233 public InvDef[][] obvious_checks(VarInfo[] vis) { 234 return new InvDef[][] {}; 235 } 236 237 public static List<@Prototype Invariant> get_proto_all() { 238 239 List<@Prototype Invariant> result = new ArrayList<>(); 240 241 result.add(Divides.get_proto(false)); 242 result.add(Divides.get_proto(true)); 243 result.add(Square.get_proto(false)); 244 result.add(Square.get_proto(true)); 245 246 result.add(BitwiseComplement.get_proto()); 247 result.add(BitwiseSubset.get_proto(false)); 248 result.add(BitwiseSubset.get_proto(true)); 249 250 result.add(ZeroTrack.get_proto(false)); 251 result.add(ZeroTrack.get_proto(true)); 252 253 result.add(BitwiseAndZero.get_proto()); 254 result.add(ShiftZero.get_proto(false)); 255 result.add(ShiftZero.get_proto(true)); 256 257 // System.out.printf("%s get proto: %s%n", NumericInt.class, result); 258 return result; 259 } 260 261 // suppressor definitions, used by many of the classes below 262 protected static NISuppressor 263 264 var1_eq_0 = new NISuppressor(0, RangeInt.EqualZero.class), 265 var2_eq_0 = new NISuppressor(1, RangeInt.EqualZero.class), 266 var1_ge_0 = new NISuppressor(0, RangeInt.GreaterEqualZero.class), 267 var2_ge_0 = new NISuppressor(1, RangeInt.GreaterEqualZero.class), 268 var1_eq_1 = new NISuppressor(0, RangeInt.EqualOne.class), 269 var2_eq_1 = new NISuppressor(1, RangeInt.EqualOne.class), 270 var1_eq_minus_1 = new NISuppressor(0, RangeInt.EqualMinusOne.class), 271 var2_eq_minus_1 = new NISuppressor(1, RangeInt.EqualMinusOne.class), 272 var1_ne_0 = new NISuppressor(0, NonZero.class), 273 var2_ne_0 = new NISuppressor(1, NonZero.class), 274 var1_le_var2 = new NISuppressor(0, 1, IntLessEqual.class), 275 276 var1_eq_var2 = new NISuppressor(0, 1, IntEqual.class), 277 var2_eq_var1 = new NISuppressor(0, 1, IntEqual.class); 278 279 protected static NISuppressor var2_valid_shift = 280 new NISuppressor(1, RangeInt.Bound0_63.class); 281 282 // 283 // Int and Float Numeric Invariants 284 // 285 286 /** 287 * Represents the divides without remainder invariant between two long scalars. 288 * Prints as {@code x % y == 0}. 289 */ 290 public static class Divides extends NumericInt { 291 // We are Serializable, so we specify a version to allow changes to 292 // method signatures without breaking serialization. If you add or 293 // remove fields, you should change this number to the current date. 294 static final long serialVersionUID = 20040113L; 295 296 protected Divides(PptSlice ppt, boolean swap) { 297 super(ppt, swap); 298 } 299 300 protected Divides(boolean swap) { 301 super(swap); 302 } 303 304 private static @Prototype Divides proto = new @Prototype Divides(false); 305 private static @Prototype Divides proto_swap = new @Prototype Divides(true); 306 307 /** Returns the prototype invariant. */ 308 public static @Prototype NumericInt get_proto(boolean swap) { 309 if (swap) { 310 return proto_swap; 311 } else { 312 return proto; 313 } 314 } 315 316 // Variables starting with dkconfig_ should only be set via the 317 // daikon.config.Configuration interface. 318 /** Boolean. True iff divides invariants should be considered. */ 319 public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault; 320 321 /** Returns whether or not this invariant is enabled. */ 322 @Override 323 public boolean enabled() { 324 return dkconfig_enabled; 325 } 326 327 @Override 328 protected Divides instantiate_dyn(@Prototype Divides this, PptSlice slice) { 329 return new Divides(slice, swap); 330 } 331 332 @Override 333 public String get_format_str(@GuardSatisfied Divides this, OutputFormat format) { 334 if (format == OutputFormat.SIMPLIFY) { 335 return "(EQ 0 (MOD %var1% %var2%))"; 336 } else if (format == OutputFormat.CSHARPCONTRACT) { 337 return "%var1% % %var2% == 0"; 338 } else { 339 return "%var1% % %var2% == 0"; 340 } 341 } 342 343 @Override 344 public boolean eq_check(long x, long y) { 345 return (0 == (x % y)); 346 } 347 348 /** Returns a list of non-instantiating suppressions for this invariant. */ 349 @Pure 350 @Override 351 public NISuppressionSet get_ni_suppressions() { 352 if (swap) { 353 return suppressions_swap; 354 } else { 355 return suppressions; 356 } 357 } 358 359 /** definition of this invariant (the suppressee) (unswapped) */ 360 private static NISuppressee suppressee = new NISuppressee(Divides.class, false); 361 362 private static NISuppressionSet suppressions = 363 new NISuppressionSet( 364 new NISuppression[] { 365 366 // These suppressions are only valid on scalars because the length 367 // of var1 and var2 must also be the same and there is no suppressor 368 // for that. 369 370 // var2 == 1 ==> var1 % var2 == 0 371 new NISuppression(var2_eq_1, suppressee), 372 373 // var2 == -1 ==> var1 % var2 == 0 374 new NISuppression(var2_eq_minus_1, suppressee), 375 376 // (var1 == 0) ^ (var2 != 0) ==> var1 % var2 == 0 377 new NISuppression(var1_eq_0, var2_ne_0, suppressee), 378 379 // (var1 == var2) ^ (var2 != 0) ==> var1 % var2 == 0 380 new NISuppression(var1_eq_var2, var2_ne_0, suppressee), 381 382 // (var2 == var1) ^ (var1 != 0) ==> var2 % var1 == 0 383 new NISuppression(var2_eq_var1, var1_ne_0, suppressee), 384 385 }); 386 private static NISuppressionSet suppressions_swap = suppressions.swap(); 387 388 /** 389 * Returns non-null if this invariant is obvious from an existing, non-falsified linear binary 390 * invariant in the same slice as this invariant. This invariant of the form "x % y == 0" is 391 * falsified if a linear binary invariant is found of the form "a*y - 1*x + 0 == 0" 392 * 393 * @return non-null value iff this invariant is obvious from other invariants in the same slice 394 */ 395 @Pure 396 @Override 397 public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) { 398 // First call super type's method, and if it returns non-null, then 399 // this invariant is already known to be obvious, so just return 400 // whatever reason the super type returned. 401 DiscardInfo di = super.isObviousDynamically(vis); 402 if (di != null) { 403 return di; 404 } 405 406 VarInfo var1 = vis[0]; 407 VarInfo var2 = vis[1]; 408 409 // ensure that var1.varinfo_index <= var2.varinfo_index 410 if (var1.varinfo_index > var2.varinfo_index) { 411 var1 = vis[1]; 412 var2 = vis[0]; 413 } 414 415 // Find slice corresponding to these two variables. 416 // Ideally, this should always just be ppt if all 417 // falsified invariants have been removed. 418 PptSlice2 ppt2 = ppt.parent.findSlice(var1,var2); 419 420 // If no slice is found , no invariants exist to make this one obvious. 421 if (ppt2 == null) { 422 return null; 423 } 424 425 // For each invariant, check to see if it's a linear binary 426 // invariant of the form "a*y - 1*x + 0 == 0" and if so, 427 // you know this invariant of the form "x % y == 0" is obvious. 428 for(Invariant inv : ppt2.invs) { 429 430 if (inv instanceof LinearBinary) { 431 LinearBinary linv = (LinearBinary) inv; 432 433 // General form for linear binary: a*x + b*y + c == 0, 434 // but a and b can be switched with respect to vis, and either 435 // one may be negative, so instead check: 436 // - c == 0 437 // - a*b < 0 (a and b have different signs) 438 // - |a| == 1 or |b| == 1, so one will divide the other 439 // While this means that both x % y == 0 and y % x == 0, 440 // only one of these invariants will still be true at this 441 // time, and only that one will be falsified by this test. 442 if (!linv.is_false() 443 && Global.fuzzy.eq(linv.core.c, 0) 444 && linv.core.b * linv.core.a < 0 445 && (Global.fuzzy.eq(linv.core.a * linv.core.a, 1) 446 || Global.fuzzy.eq(linv.core.b * linv.core.b, 1))) { 447 return new DiscardInfo(this, DiscardCode.obvious, 448 "Linear binary invariant implies divides"); 449 } 450 } 451 } 452 453 return null; 454 } 455 456 } 457 458 /** 459 * Represents the square invariant between two long scalars. 460 * Prints as {@code x = y**2}. 461 */ 462 public static class Square extends NumericInt { 463 // We are Serializable, so we specify a version to allow changes to 464 // method signatures without breaking serialization. If you add or 465 // remove fields, you should change this number to the current date. 466 static final long serialVersionUID = 20040113L; 467 468 protected Square(PptSlice ppt, boolean swap) { 469 super(ppt, swap); 470 } 471 472 protected Square(boolean swap) { 473 super(swap); 474 } 475 476 private static @Prototype Square proto = new @Prototype Square(false); 477 private static @Prototype Square proto_swap = new @Prototype Square(true); 478 479 /** Returns the prototype invariant. */ 480 public static @Prototype Square get_proto(boolean swap) { 481 if (swap) { 482 return proto_swap; 483 } else { 484 return proto; 485 } 486 } 487 488 // Variables starting with dkconfig_ should only be set via the 489 // daikon.config.Configuration interface. 490 /** Boolean. True iff square invariants should be considered. */ 491 public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault; 492 493 /** Returns whether or not this invariant is enabled. */ 494 @Override 495 public boolean enabled() { 496 return dkconfig_enabled; 497 } 498 @Override 499 protected Square instantiate_dyn(@Prototype Square this, PptSlice slice) { 500 return new Square(slice, swap); 501 } 502 503 @Override 504 public String get_format_str(@GuardSatisfied Square this, OutputFormat format) { 505 if (format == OutputFormat.SIMPLIFY) { 506 return "(EQ %var1% (* %var2% %var2))"; 507 } else if (format == OutputFormat.CSHARPCONTRACT) { 508 return "%var1% == %var2%*%var2%"; 509 } else if (format.isJavaFamily()) { 510 511 return "%var1% == %var2%*%var2%"; 512 } else { 513 return "%var1% == %var2%**2"; 514 } 515 } 516 517 /** Check to see if x == y squared. */ 518 @Override 519 public boolean eq_check(long x, long y) { 520 return (x == y*y); 521 } 522 523 // Note there are no NI Suppressions for Square. Two obvious 524 // suppressions are: 525 // 526 // (var2 == 1) ^ (var1 == 1) ==> var1 = var2*var2 527 // (var2 == 0) ^ (var1 == 0) ==> var1 = var2*var2 528 // 529 // But all of the antecedents would be constants, so we would 530 // never need to create this slice, so there is no reason to create 531 // these. 532 533 } 534 535 /** 536 * Represents the zero tracks invariant between 537 * two long scalars; that is, when {@code x} is zero, 538 * {@code y} is also zero. 539 * Prints as {@code x = 0 => y = 0}. 540 */ 541 public static class ZeroTrack extends NumericInt { 542 // We are Serializable, so we specify a version to allow changes to 543 // method signatures without breaking serialization. If you add or 544 // remove fields, you should change this number to the current date. 545 static final long serialVersionUID = 20040313L; 546 547 protected ZeroTrack(PptSlice ppt, boolean swap) { 548 super(ppt, swap); 549 } 550 551 protected @Prototype ZeroTrack(boolean swap) { 552 super(swap); 553 } 554 555 private static @Prototype ZeroTrack proto = new @Prototype ZeroTrack(false); 556 private static @Prototype ZeroTrack proto_swap = new @Prototype ZeroTrack(true); 557 558 /** Returns the prototype invariant. */ 559 public static @Prototype ZeroTrack get_proto(boolean swap) { 560 if (swap) { 561 return proto_swap; 562 } else { 563 return proto; 564 } 565 } 566 567 // Variables starting with dkconfig_ should only be set via the 568 // daikon.config.Configuration interface. 569 /** Boolean. True iff zero-track invariants should be considered. */ 570 public static boolean dkconfig_enabled = false; 571 572 /** Returns whether or not this invariant is enabled. */ 573 @Override 574 public boolean enabled() { 575 return dkconfig_enabled; 576 } 577 578 @Override 579 protected ZeroTrack instantiate_dyn(@Prototype ZeroTrack this, PptSlice slice) { 580 return new ZeroTrack(slice, swap); 581 } 582 583 @Override 584 public String get_format_str(@GuardSatisfied ZeroTrack this, OutputFormat format) { 585 if (format == OutputFormat.SIMPLIFY) { 586 return "(IMPLIES (EQ %var1% 0) (EQ %var2% 0))"; 587 } else if (format.isJavaFamily() || format == OutputFormat.CSHARPCONTRACT) { 588 return "(!(%var1% == 0)) || (%var2% == 0)"; 589 } else { 590 return "(%var1% == 0) ==> (%var2% == 0)"; 591 } 592 } 593 594 @Override 595 public boolean eq_check(long x, long y) { 596 if (x == 0) { 597 return y == 0; 598 } else { 599 return true; 600 } 601 } 602 603 /** Returns a list of non-instantiating suppressions for this invariant. */ 604 @Pure 605 @Override 606 public NISuppressionSet get_ni_suppressions() { 607 if (swap) { 608 return suppressions_swap; 609 } else { 610 return suppressions; 611 } 612 } 613 614 /** definition of this invariant (the suppressee) (unswapped) */ 615 private static NISuppressee suppressee = new NISuppressee(ZeroTrack.class, false); 616 617 private static NISuppressionSet suppressions = 618 new NISuppressionSet( 619 new NISuppression[] { 620 // (var1 == var2) ==> (var1=0 ==> var2=0) 621 new NISuppression(var1_eq_var2, suppressee), 622 // (var1 != 0) ==> (var1=0 ==> var2=0) 623 new NISuppression(var1_ne_0, suppressee), 624 // (var2 == 0) ==> (var1=0 ==> var2=0) 625 new NISuppression(var2_eq_0, suppressee), 626 }); 627 private static NISuppressionSet suppressions_swap = suppressions.swap(); 628 629 } 630 631 /** 632 * Represents the bitwise complement invariant between two long scalars. 633 * Prints as {@code x = ~y}. 634 */ 635 public static class BitwiseComplement extends NumericInt { 636 // We are Serializable, so we specify a version to allow changes to 637 // method signatures without breaking serialization. If you add or 638 // remove fields, you should change this number to the current date. 639 static final long serialVersionUID = 20040113L; 640 641 protected BitwiseComplement(PptSlice ppt) { 642 super(ppt, false); 643 } 644 645 protected @Prototype BitwiseComplement() { 646 super(false); 647 } 648 649 private static @Prototype BitwiseComplement proto = new @Prototype BitwiseComplement(); 650 651 /** Returns the prototype invariant. */ 652 public static @Prototype BitwiseComplement get_proto() { 653 return proto; 654 } 655 656 // Variables starting with dkconfig_ should only be set via the 657 // daikon.config.Configuration interface. 658 /** Boolean. True iff bitwise complement invariants should be considered. */ 659 public static boolean dkconfig_enabled = false; 660 661 /** Returns whether or not this invariant is enabled. */ 662 @Override 663 public boolean enabled() { 664 return dkconfig_enabled; 665 } 666 667 @Override 668 protected BitwiseComplement instantiate_dyn(@Prototype BitwiseComplement this, PptSlice slice) { 669 return new BitwiseComplement(slice); 670 } 671 672 @Pure 673 @Override 674 public boolean is_symmetric() { 675 return true; 676 } 677 678 @Override 679 public String get_format_str(@GuardSatisfied BitwiseComplement this, OutputFormat format) { 680 if (format == OutputFormat.SIMPLIFY) { 681 return "(EQ %var1% (~ %var2%))"; 682 } else if (format == OutputFormat.CSHARPCONTRACT) { 683 return "%var1% == ~%var2%"; 684 } else { 685 return "%var1% == ~%var2%"; 686 } 687 } 688 689 /** Check to see if x == ~y . */ 690 @Override 691 public boolean eq_check(long x, long y) { 692 return (x == ~y); 693 } 694 } 695 696 /** 697 * Represents the bitwise subset invariant between two long scalars; that is, the bits of 698 * {@code y} are a subset of the bits of {@code x}. 699 * Prints as {@code x = y | x}. 700 */ 701 public static class BitwiseSubset extends NumericInt { 702 // We are Serializable, so we specify a version to allow changes to 703 // method signatures without breaking serialization. If you add or 704 // remove fields, you should change this number to the current date. 705 static final long serialVersionUID = 20040113L; 706 707 protected BitwiseSubset(PptSlice ppt, boolean swap) { 708 super(ppt, swap); 709 } 710 711 protected BitwiseSubset(boolean swap) { 712 super(swap); 713 } 714 715 private static @Prototype BitwiseSubset proto = new @Prototype BitwiseSubset(false); 716 private static @Prototype BitwiseSubset proto_swap = new @Prototype BitwiseSubset(true); 717 718 /** Returns the prototype invariant. */ 719 public static @Prototype BitwiseSubset get_proto(boolean swap) { 720 if (swap) { 721 return proto_swap; 722 } else { 723 return proto; 724 } 725 } 726 727 // Variables starting with dkconfig_ should only be set via the 728 // daikon.config.Configuration interface. 729 /** Boolean. True iff bitwise subset invariants should be considered. */ 730 public static boolean dkconfig_enabled = false; 731 732 /** Returns whether or not this invariant is enabled. */ 733 @Override 734 public boolean enabled() { 735 return dkconfig_enabled; 736 } 737 738 @Override 739 public BitwiseSubset instantiate_dyn(@Prototype BitwiseSubset this, PptSlice slice) { 740 return new BitwiseSubset(slice, swap); 741 } 742 743 @Override 744 public String get_format_str(@GuardSatisfied BitwiseSubset this, OutputFormat format) { 745 if (format == OutputFormat.SIMPLIFY) { 746 return "(EQ %var1% (|java-bitwise-or| %var2% %var1%))"; 747 } else if (format == OutputFormat.DAIKON) { 748 return "%var2% is a bitwise subset of %var1%"; 749 } else if (format == OutputFormat.CSHARPCONTRACT) { 750 return "%var1% == (%var2% | %var1%)"; 751 } else { 752 return "%var1% == (%var2% | %var1%)"; 753 } 754 } 755 756 @Override 757 public boolean eq_check(long x, long y) { 758 return (x == (y | x)); 759 } 760 761 /** Returns a list of non-instantiating suppressions for this invariant. */ 762 @Pure 763 @Override 764 public NISuppressionSet get_ni_suppressions() { 765 if (swap) { 766 return suppressions_swap; 767 } else { 768 return suppressions; 769 } 770 } 771 772 /** definition of this invariant (the suppressee) (unswapped) */ 773 private static NISuppressee suppressee = new NISuppressee(BitwiseSubset.class, false); 774 775 private static NISuppressionSet suppressions = 776 new NISuppressionSet( 777 new NISuppression[] { 778 779 // (var2 == 0) ==> var1 = (var2 | var1) 780 new NISuppression(var2_eq_0, suppressee), 781 782 // (var1 == -1) ==> var1 = (var2 | var1) 783 new NISuppression(var1_eq_minus_1, suppressee), 784 785 // (var1 == var2) ==> var1 = (var2 | var1) 786 new NISuppression(var1_eq_var2, suppressee), 787 788 }); 789 private static NISuppressionSet suppressions_swap = suppressions.swap(); 790 } 791 792 /** 793 * Represents the BitwiseAnd == 0 invariant between two long scalars; that is, {@code x} and 794 * {@code y} have no bits in common. 795 * Prints as {@code x & y == 0}. 796 */ 797 public static class BitwiseAndZero extends NumericInt { 798 // We are Serializable, so we specify a version to allow changes to 799 // method signatures without breaking serialization. If you add or 800 // remove fields, you should change this number to the current date. 801 static final long serialVersionUID = 20040313L; 802 803 protected BitwiseAndZero(PptSlice ppt) { 804 super(ppt, false); 805 } 806 807 protected @Prototype BitwiseAndZero() { 808 super(false); 809 } 810 811 private static @Prototype BitwiseAndZero proto = new @Prototype BitwiseAndZero(); 812 813 /** Returns the prototype invariant. */ 814 public static @Prototype BitwiseAndZero get_proto() { 815 return proto; 816 } 817 818 // Variables starting with dkconfig_ should only be set via the 819 // daikon.config.Configuration interface. 820 /** Boolean. True iff BitwiseAndZero invariants should be considered. */ 821 public static boolean dkconfig_enabled = false; 822 823 /** Returns whether or not this invariant is enabled. */ 824 @Override 825 public boolean enabled() { 826 return dkconfig_enabled; 827 } 828 829 @Override 830 public BitwiseAndZero instantiate_dyn(@Prototype BitwiseAndZero this, PptSlice slice) { 831 return new BitwiseAndZero(slice); 832 } 833 834 @Override 835 public String get_format_str(@GuardSatisfied BitwiseAndZero this, OutputFormat format) { 836 if (format == OutputFormat.SIMPLIFY) { 837 return "(EQ (|java-&| %var1% %var2%) 0)"; 838 } else if (format == OutputFormat.CSHARPCONTRACT) { 839 return "(%var1% & %var2%) == 0"; 840 } else { 841 return "(%var1% & %var2%) == 0"; 842 } 843 } 844 845 @Pure 846 @Override 847 public boolean is_symmetric() { 848 return true; 849 } 850 851 @Override 852 public boolean eq_check(long x, long y) { 853 return (x & y) == 0; 854 } 855 856 /** Returns a list of non-instantiating suppressions for this invariant. */ 857 @Pure 858 @Override 859 public @Nullable NISuppressionSet get_ni_suppressions() { 860 return suppressions; 861 } 862 863 /** definition of this invariant (the suppressee) (unswapped) */ 864 private static NISuppressee suppressee = new NISuppressee(BitwiseAndZero.class, 2); 865 866 private static NISuppressionSet suppressions = 867 new NISuppressionSet( 868 new NISuppression[] { 869 // (var1 == 0) ==> (var1 & var2) == 0 870 new NISuppression(var1_eq_0, suppressee), 871 872 // (var2 == 0) ==> (var1 & var2) == 0 873 new NISuppression(var2_eq_0, suppressee), 874 }); 875 876 } 877 878 /** 879 * Represents the ShiftZero invariant between two long scalars; that is, {@code x} 880 * right-shifted by {@code y} is always zero. 881 * Prints as {@code x >> y = 0}. 882 */ 883 public static class ShiftZero extends NumericInt { 884 // We are Serializable, so we specify a version to allow changes to 885 // method signatures without breaking serialization. If you add or 886 // remove fields, you should change this number to the current date. 887 static final long serialVersionUID = 20040313L; 888 889 protected ShiftZero(PptSlice ppt, boolean swap) { 890 super(ppt, swap); 891 } 892 893 protected ShiftZero(boolean swap) { 894 super(swap); 895 } 896 897 private static @Prototype ShiftZero proto = new @Prototype ShiftZero(false); 898 private static @Prototype ShiftZero proto_swap = new @Prototype ShiftZero(true); 899 900 /** Returns the prototype invariant. */ 901 public static @Prototype ShiftZero get_proto(boolean swap) { 902 if (swap) { 903 return proto_swap; 904 } else { 905 return proto; 906 } 907 } 908 909 // Variables starting with dkconfig_ should only be set via the 910 // daikon.config.Configuration interface. 911 /** Boolean. True iff ShiftZero invariants should be considered. */ 912 public static boolean dkconfig_enabled = false; 913 914 /** Returns whether or not this invariant is enabled. */ 915 @Override 916 public boolean enabled() { 917 return dkconfig_enabled; 918 } 919 920 @Override 921 protected ShiftZero instantiate_dyn(@Prototype ShiftZero this, PptSlice slice) { 922 return new ShiftZero(slice, swap); 923 } 924 925 @Override 926 public String get_format_str(@GuardSatisfied ShiftZero this, OutputFormat format) { 927 if (format == OutputFormat.SIMPLIFY) { 928 return "(EQ (|java->>| %var1% %var2%) 0)"; 929 } else if (format == OutputFormat.CSHARPCONTRACT) { 930 return "(%var1% >> %var2% == 0)"; 931 } else { 932 return "(%var1% >> %var2% == 0)"; 933 } 934 } 935 936 @Override 937 public boolean eq_check(long x, long y) { 938 if ((y < 0) || (y > 63)) { 939 throw new ArithmeticException("shift op (" + y + ") is out of range"); 940 } 941 return (x >> y) == 0; 942 } 943 944 /** Returns a list of non-instantiating suppressions for this invariant. */ 945 @Pure 946 @Override 947 public NISuppressionSet get_ni_suppressions() { 948 if (swap) { 949 return suppressions_swap; 950 } else { 951 return suppressions; 952 } 953 } 954 955 /** definition of this invariant (the suppressee) (unswapped) */ 956 private static NISuppressee suppressee = new NISuppressee(ShiftZero.class, false); 957 958 private static NISuppressionSet suppressions = 959 new NISuppressionSet( 960 new NISuppression[] { 961 // (var1>=0) ^ (var1<=var2) ^ (0<=var2<=63) ==> (var1 >> var2) == 0 962 new NISuppression(var1_ge_0, var1_le_var2, var2_valid_shift, 963 suppressee), 964 }); 965 private static NISuppressionSet suppressions_swap = suppressions.swap(); 966 } 967 968// 969// Standard String invariants 970// 971 972}