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 { 332 return "%var1% % %var2% == 0"; 333 } 334 } 335 336 @Override 337 public boolean eq_check(long x, long y) { 338 return (0 == (x % y)); 339 } 340 341 /** Returns a list of non-instantiating suppressions for this invariant. */ 342 @Pure 343 @Override 344 public NISuppressionSet get_ni_suppressions() { 345 if (swap) { 346 return suppressions_swap; 347 } else { 348 return suppressions; 349 } 350 } 351 352 /** definition of this invariant (the suppressee) (unswapped) */ 353 private static NISuppressee suppressee = new NISuppressee(Divides.class, false); 354 355 private static NISuppressionSet suppressions = 356 new NISuppressionSet( 357 new NISuppression[] { 358 359 // These suppressions are only valid on scalars because the length 360 // of var1 and var2 must also be the same and there is no suppressor 361 // for that. 362 363 // var2 == 1 ==> var1 % var2 == 0 364 new NISuppression(var2_eq_1, suppressee), 365 366 // var2 == -1 ==> var1 % var2 == 0 367 new NISuppression(var2_eq_minus_1, suppressee), 368 369 // (var1 == 0) ^ (var2 != 0) ==> var1 % var2 == 0 370 new NISuppression(var1_eq_0, var2_ne_0, suppressee), 371 372 // (var1 == var2) ^ (var2 != 0) ==> var1 % var2 == 0 373 new NISuppression(var1_eq_var2, var2_ne_0, suppressee), 374 375 // (var2 == var1) ^ (var1 != 0) ==> var2 % var1 == 0 376 new NISuppression(var2_eq_var1, var1_ne_0, suppressee), 377 378 }); 379 private static NISuppressionSet suppressions_swap = suppressions.swap(); 380 381 /** 382 * Returns non-null if this invariant is obvious from an existing, non-falsified linear binary 383 * invariant in the same slice as this invariant. This invariant of the form "x % y == 0" is 384 * falsified if a linear binary invariant is found of the form "a*y - 1*x + 0 == 0" 385 * 386 * @return non-null value iff this invariant is obvious from other invariants in the same slice 387 */ 388 @Pure 389 @Override 390 public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) { 391 // First call super type's method, and if it returns non-null, then 392 // this invariant is already known to be obvious, so just return 393 // whatever reason the super type returned. 394 DiscardInfo di = super.isObviousDynamically(vis); 395 if (di != null) { 396 return di; 397 } 398 399 VarInfo var1 = vis[0]; 400 VarInfo var2 = vis[1]; 401 402 // ensure that var1.varinfo_index <= var2.varinfo_index 403 if (var1.varinfo_index > var2.varinfo_index) { 404 var1 = vis[1]; 405 var2 = vis[0]; 406 } 407 408 // Find slice corresponding to these two variables. 409 // Ideally, this should always just be ppt if all 410 // falsified invariants have been removed. 411 PptSlice2 ppt2 = ppt.parent.findSlice(var1,var2); 412 413 // If no slice is found , no invariants exist to make this one obvious. 414 if (ppt2 == null) { 415 return null; 416 } 417 418 // For each invariant, check to see if it's a linear binary 419 // invariant of the form "a*y - 1*x + 0 == 0" and if so, 420 // you know this invariant of the form "x % y == 0" is obvious. 421 for(Invariant inv : ppt2.invs) { 422 423 if (inv instanceof LinearBinary) { 424 LinearBinary linv = (LinearBinary) inv; 425 426 // General form for linear binary: a*x + b*y + c == 0, 427 // but a and b can be switched with respect to vis, and either 428 // one may be negative, so instead check: 429 // - c == 0 430 // - a*b < 0 (a and b have different signs) 431 // - |a| == 1 or |b| == 1, so one will divide the other 432 // While this means that both x % y == 0 and y % x == 0, 433 // only one of these invariants will still be true at this 434 // time, and only that one will be falsified by this test. 435 if (!linv.is_false() 436 && Global.fuzzy.eq(linv.core.c, 0) 437 && linv.core.b * linv.core.a < 0 438 && (Global.fuzzy.eq(linv.core.a * linv.core.a, 1) 439 || Global.fuzzy.eq(linv.core.b * linv.core.b, 1))) { 440 return new DiscardInfo(this, DiscardCode.obvious, 441 "Linear binary invariant implies divides"); 442 } 443 } 444 } 445 446 return null; 447 } 448 449 } 450 451 /** 452 * Represents the square invariant between two long scalars. 453 * Prints as {@code x = y**2}. 454 */ 455 public static class Square extends NumericInt { 456 // We are Serializable, so we specify a version to allow changes to 457 // method signatures without breaking serialization. If you add or 458 // remove fields, you should change this number to the current date. 459 static final long serialVersionUID = 20040113L; 460 461 protected Square(PptSlice ppt, boolean swap) { 462 super(ppt, swap); 463 } 464 465 protected Square(boolean swap) { 466 super(swap); 467 } 468 469 private static @Prototype Square proto = new @Prototype Square(false); 470 private static @Prototype Square proto_swap = new @Prototype Square(true); 471 472 /** Returns the prototype invariant. */ 473 public static @Prototype Square get_proto(boolean swap) { 474 if (swap) { 475 return proto_swap; 476 } else { 477 return proto; 478 } 479 } 480 481 // Variables starting with dkconfig_ should only be set via the 482 // daikon.config.Configuration interface. 483 /** Boolean. True iff square invariants should be considered. */ 484 public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault; 485 486 @Override 487 public boolean enabled() { 488 return dkconfig_enabled; 489 } 490 @Override 491 protected Square instantiate_dyn(@Prototype Square this, PptSlice slice) { 492 return new Square(slice, swap); 493 } 494 495 @Override 496 public String get_format_str(@GuardSatisfied Square this, OutputFormat format) { 497 if (format == OutputFormat.SIMPLIFY) { 498 return "(EQ %var1% (* %var2% %var2))"; 499 } else if (format == OutputFormat.CSHARPCONTRACT) { 500 return "%var1% == %var2%*%var2%"; 501 } else if (format.isJavaFamily()) { 502 503 return "%var1% == %var2%*%var2%"; 504 } else { 505 return "%var1% == %var2%**2"; 506 } 507 } 508 509 /** Check to see if x == y squared. */ 510 @Override 511 public boolean eq_check(long x, long y) { 512 return (x == y*y); 513 } 514 515 // Note there are no NI Suppressions for Square. Two obvious 516 // suppressions are: 517 // 518 // (var2 == 1) ^ (var1 == 1) ==> var1 = var2*var2 519 // (var2 == 0) ^ (var1 == 0) ==> var1 = var2*var2 520 // 521 // But all of the antecedents would be constants, so we would 522 // never need to create this slice, so there is no reason to create 523 // these. 524 525 } 526 527 /** 528 * Represents the zero tracks invariant between 529 * two long scalars; that is, when {@code x} is zero, 530 * {@code y} is also zero. 531 * Prints as {@code x = 0 => y = 0}. 532 */ 533 public static class ZeroTrack extends NumericInt { 534 // We are Serializable, so we specify a version to allow changes to 535 // method signatures without breaking serialization. If you add or 536 // remove fields, you should change this number to the current date. 537 static final long serialVersionUID = 20040313L; 538 539 protected ZeroTrack(PptSlice ppt, boolean swap) { 540 super(ppt, swap); 541 } 542 543 protected @Prototype ZeroTrack(boolean swap) { 544 super(swap); 545 } 546 547 private static @Prototype ZeroTrack proto = new @Prototype ZeroTrack(false); 548 private static @Prototype ZeroTrack proto_swap = new @Prototype ZeroTrack(true); 549 550 /** Returns the prototype invariant. */ 551 public static @Prototype ZeroTrack get_proto(boolean swap) { 552 if (swap) { 553 return proto_swap; 554 } else { 555 return proto; 556 } 557 } 558 559 // Variables starting with dkconfig_ should only be set via the 560 // daikon.config.Configuration interface. 561 /** Boolean. True iff zero-track invariants should be considered. */ 562 public static boolean dkconfig_enabled = false; 563 564 @Override 565 public boolean enabled() { 566 return dkconfig_enabled; 567 } 568 569 @Override 570 protected ZeroTrack instantiate_dyn(@Prototype ZeroTrack this, PptSlice slice) { 571 return new ZeroTrack(slice, swap); 572 } 573 574 @Override 575 public String get_format_str(@GuardSatisfied ZeroTrack this, OutputFormat format) { 576 if (format == OutputFormat.SIMPLIFY) { 577 return "(IMPLIES (EQ %var1% 0) (EQ %var2% 0))"; 578 } else if (format.isJavaFamily() || format == OutputFormat.CSHARPCONTRACT) { 579 return "(!(%var1% == 0)) || (%var2% == 0)"; 580 } else { 581 return "(%var1% == 0) ==> (%var2% == 0)"; 582 } 583 } 584 585 @Override 586 public boolean eq_check(long x, long y) { 587 if (x == 0) { 588 return y == 0; 589 } else { 590 return true; 591 } 592 } 593 594 /** Returns a list of non-instantiating suppressions for this invariant. */ 595 @Pure 596 @Override 597 public NISuppressionSet get_ni_suppressions() { 598 if (swap) { 599 return suppressions_swap; 600 } else { 601 return suppressions; 602 } 603 } 604 605 /** definition of this invariant (the suppressee) (unswapped) */ 606 private static NISuppressee suppressee = new NISuppressee(ZeroTrack.class, false); 607 608 private static NISuppressionSet suppressions = 609 new NISuppressionSet( 610 new NISuppression[] { 611 // (var1 == var2) ==> (var1=0 ==> var2=0) 612 new NISuppression(var1_eq_var2, suppressee), 613 // (var1 != 0) ==> (var1=0 ==> var2=0) 614 new NISuppression(var1_ne_0, suppressee), 615 // (var2 == 0) ==> (var1=0 ==> var2=0) 616 new NISuppression(var2_eq_0, suppressee), 617 }); 618 private static NISuppressionSet suppressions_swap = suppressions.swap(); 619 620 } 621 622 /** 623 * Represents the bitwise complement invariant between two long scalars. 624 * Prints as {@code x = ~y}. 625 */ 626 public static class BitwiseComplement extends NumericInt { 627 // We are Serializable, so we specify a version to allow changes to 628 // method signatures without breaking serialization. If you add or 629 // remove fields, you should change this number to the current date. 630 static final long serialVersionUID = 20040113L; 631 632 protected BitwiseComplement(PptSlice ppt) { 633 super(ppt, false); 634 } 635 636 protected @Prototype BitwiseComplement() { 637 super(false); 638 } 639 640 private static @Prototype BitwiseComplement proto = new @Prototype BitwiseComplement(); 641 642 /** Returns the prototype invariant. */ 643 public static @Prototype BitwiseComplement get_proto() { 644 return proto; 645 } 646 647 // Variables starting with dkconfig_ should only be set via the 648 // daikon.config.Configuration interface. 649 /** Boolean. True iff bitwise complement invariants should be considered. */ 650 public static boolean dkconfig_enabled = false; 651 652 @Override 653 public boolean enabled() { 654 return dkconfig_enabled; 655 } 656 657 @Override 658 protected BitwiseComplement instantiate_dyn(@Prototype BitwiseComplement this, PptSlice slice) { 659 return new BitwiseComplement(slice); 660 } 661 662 @Pure 663 @Override 664 public boolean is_symmetric() { 665 return true; 666 } 667 668 @Override 669 public String get_format_str(@GuardSatisfied BitwiseComplement this, OutputFormat format) { 670 if (format == OutputFormat.SIMPLIFY) { 671 return "(EQ %var1% (~ %var2%))"; 672 } else { 673 return "%var1% == ~%var2%"; 674 } 675 } 676 677 /** Check to see if x == ~y . */ 678 @Override 679 public boolean eq_check(long x, long y) { 680 return (x == ~y); 681 } 682 } 683 684 /** 685 * Represents the bitwise subset invariant between two long scalars; that is, the bits of 686 * {@code y} are a subset of the bits of {@code x}. 687 * Prints as {@code x = y | x}. 688 */ 689 public static class BitwiseSubset extends NumericInt { 690 // We are Serializable, so we specify a version to allow changes to 691 // method signatures without breaking serialization. If you add or 692 // remove fields, you should change this number to the current date. 693 static final long serialVersionUID = 20040113L; 694 695 protected BitwiseSubset(PptSlice ppt, boolean swap) { 696 super(ppt, swap); 697 } 698 699 protected BitwiseSubset(boolean swap) { 700 super(swap); 701 } 702 703 private static @Prototype BitwiseSubset proto = new @Prototype BitwiseSubset(false); 704 private static @Prototype BitwiseSubset proto_swap = new @Prototype BitwiseSubset(true); 705 706 /** Returns the prototype invariant. */ 707 public static @Prototype BitwiseSubset get_proto(boolean swap) { 708 if (swap) { 709 return proto_swap; 710 } else { 711 return proto; 712 } 713 } 714 715 // Variables starting with dkconfig_ should only be set via the 716 // daikon.config.Configuration interface. 717 /** Boolean. True iff bitwise subset invariants should be considered. */ 718 public static boolean dkconfig_enabled = false; 719 720 @Override 721 public boolean enabled() { 722 return dkconfig_enabled; 723 } 724 725 @Override 726 public BitwiseSubset instantiate_dyn(@Prototype BitwiseSubset this, PptSlice slice) { 727 return new BitwiseSubset(slice, swap); 728 } 729 730 @Override 731 public String get_format_str(@GuardSatisfied BitwiseSubset this, OutputFormat format) { 732 if (format == OutputFormat.SIMPLIFY) { 733 return "(EQ %var1% (|java-bitwise-or| %var2% %var1%))"; 734 } else if (format == OutputFormat.DAIKON) { 735 return "%var2% is a bitwise subset of %var1%"; 736 } else { 737 return "%var1% == (%var2% | %var1%)"; 738 } 739 } 740 741 @Override 742 public boolean eq_check(long x, long y) { 743 return (x == (y | x)); 744 } 745 746 /** Returns a list of non-instantiating suppressions for this invariant. */ 747 @Pure 748 @Override 749 public NISuppressionSet get_ni_suppressions() { 750 if (swap) { 751 return suppressions_swap; 752 } else { 753 return suppressions; 754 } 755 } 756 757 /** definition of this invariant (the suppressee) (unswapped) */ 758 private static NISuppressee suppressee = new NISuppressee(BitwiseSubset.class, false); 759 760 private static NISuppressionSet suppressions = 761 new NISuppressionSet( 762 new NISuppression[] { 763 764 // (var2 == 0) ==> var1 = (var2 | var1) 765 new NISuppression(var2_eq_0, suppressee), 766 767 // (var1 == -1) ==> var1 = (var2 | var1) 768 new NISuppression(var1_eq_minus_1, suppressee), 769 770 // (var1 == var2) ==> var1 = (var2 | var1) 771 new NISuppression(var1_eq_var2, suppressee), 772 773 }); 774 private static NISuppressionSet suppressions_swap = suppressions.swap(); 775 } 776 777 /** 778 * Represents the BitwiseAnd == 0 invariant between two long scalars; that is, {@code x} and 779 * {@code y} have no bits in common. 780 * Prints as {@code x & y == 0}. 781 */ 782 public static class BitwiseAndZero extends NumericInt { 783 // We are Serializable, so we specify a version to allow changes to 784 // method signatures without breaking serialization. If you add or 785 // remove fields, you should change this number to the current date. 786 static final long serialVersionUID = 20040313L; 787 788 protected BitwiseAndZero(PptSlice ppt) { 789 super(ppt, false); 790 } 791 792 protected @Prototype BitwiseAndZero() { 793 super(false); 794 } 795 796 private static @Prototype BitwiseAndZero proto = new @Prototype BitwiseAndZero(); 797 798 /** Returns the prototype invariant. */ 799 public static @Prototype BitwiseAndZero get_proto() { 800 return proto; 801 } 802 803 // Variables starting with dkconfig_ should only be set via the 804 // daikon.config.Configuration interface. 805 /** Boolean. True iff BitwiseAndZero invariants should be considered. */ 806 public static boolean dkconfig_enabled = false; 807 808 @Override 809 public boolean enabled() { 810 return dkconfig_enabled; 811 } 812 813 @Override 814 public BitwiseAndZero instantiate_dyn(@Prototype BitwiseAndZero this, PptSlice slice) { 815 return new BitwiseAndZero(slice); 816 } 817 818 @Override 819 public String get_format_str(@GuardSatisfied BitwiseAndZero this, OutputFormat format) { 820 if (format == OutputFormat.SIMPLIFY) { 821 return "(EQ (|java-&| %var1% %var2%) 0)"; 822 } else { 823 return "(%var1% & %var2%) == 0"; 824 } 825 } 826 827 @Pure 828 @Override 829 public boolean is_symmetric() { 830 return true; 831 } 832 833 @Override 834 public boolean eq_check(long x, long y) { 835 return (x & y) == 0; 836 } 837 838 /** Returns a list of non-instantiating suppressions for this invariant. */ 839 @Pure 840 @Override 841 public @Nullable NISuppressionSet get_ni_suppressions() { 842 return suppressions; 843 } 844 845 /** definition of this invariant (the suppressee) (unswapped) */ 846 private static NISuppressee suppressee = new NISuppressee(BitwiseAndZero.class, 2); 847 848 private static NISuppressionSet suppressions = 849 new NISuppressionSet( 850 new NISuppression[] { 851 // (var1 == 0) ==> (var1 & var2) == 0 852 new NISuppression(var1_eq_0, suppressee), 853 854 // (var2 == 0) ==> (var1 & var2) == 0 855 new NISuppression(var2_eq_0, suppressee), 856 }); 857 858 } 859 860 /** 861 * Represents the ShiftZero invariant between two long scalars; that is, {@code x} 862 * right-shifted by {@code y} is always zero. 863 * Prints as {@code x >> y = 0}. 864 */ 865 public static class ShiftZero extends NumericInt { 866 // We are Serializable, so we specify a version to allow changes to 867 // method signatures without breaking serialization. If you add or 868 // remove fields, you should change this number to the current date. 869 static final long serialVersionUID = 20040313L; 870 871 protected ShiftZero(PptSlice ppt, boolean swap) { 872 super(ppt, swap); 873 } 874 875 protected ShiftZero(boolean swap) { 876 super(swap); 877 } 878 879 private static @Prototype ShiftZero proto = new @Prototype ShiftZero(false); 880 private static @Prototype ShiftZero proto_swap = new @Prototype ShiftZero(true); 881 882 /** Returns the prototype invariant. */ 883 public static @Prototype ShiftZero get_proto(boolean swap) { 884 if (swap) { 885 return proto_swap; 886 } else { 887 return proto; 888 } 889 } 890 891 // Variables starting with dkconfig_ should only be set via the 892 // daikon.config.Configuration interface. 893 /** Boolean. True iff ShiftZero invariants should be considered. */ 894 public static boolean dkconfig_enabled = false; 895 896 @Override 897 public boolean enabled() { 898 return dkconfig_enabled; 899 } 900 901 @Override 902 protected ShiftZero instantiate_dyn(@Prototype ShiftZero this, PptSlice slice) { 903 return new ShiftZero(slice, swap); 904 } 905 906 @Override 907 public String get_format_str(@GuardSatisfied ShiftZero this, OutputFormat format) { 908 if (format == OutputFormat.SIMPLIFY) { 909 return "(EQ (|java->>| %var1% %var2%) 0)"; 910 } else { 911 return "(%var1% >> %var2% == 0)"; 912 } 913 } 914 915 @Override 916 public boolean eq_check(long x, long y) { 917 if ((y < 0) || (y > 63)) { 918 throw new ArithmeticException("shift op (" + y + ") is out of range"); 919 } 920 return (x >> y) == 0; 921 } 922 923 /** Returns a list of non-instantiating suppressions for this invariant. */ 924 @Pure 925 @Override 926 public NISuppressionSet get_ni_suppressions() { 927 if (swap) { 928 return suppressions_swap; 929 } else { 930 return suppressions; 931 } 932 } 933 934 /** definition of this invariant (the suppressee) (unswapped) */ 935 private static NISuppressee suppressee = new NISuppressee(ShiftZero.class, false); 936 937 private static NISuppressionSet suppressions = 938 new NISuppressionSet( 939 new NISuppression[] { 940 // (var1>=0) ^ (var1<=var2) ^ (0<=var2<=63) ==> (var1 >> var2) == 0 941 new NISuppression(var1_ge_0, var1_le_var2, var2_valid_shift, 942 suppressee), 943 }); 944 private static NISuppressionSet suppressions_swap = suppressions.swap(); 945 } 946 947// 948// Standard String invariants 949// 950 951}