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