001// ***** This file is automatically generated from Numeric.java.jpp 002 003package daikon.inv.binary.twoSequence; 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 PairwiseNumericInt extends TwoSequence { 035 036 static final long serialVersionUID = 20060609L; 037 038 protected PairwiseNumericInt(PptSlice ppt, boolean swap) { 039 super(ppt); 040 this.swap = swap; 041 } 042 043 protected PairwiseNumericInt(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.baseIsIntegral() || !type2.baseIsIntegral()) { 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 PairwiseNumericInt 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 PairwiseNumericInt 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; 089 String v2; 090 if (format.isJavaFamily()) { 091 092 v1 = var1().name_using(format); 093 v2 = var2().name_using(format); 094 if (this instanceof Divides) { 095 return "daikon.Quant.pairwiseDivides(" + v1 + ", " + v2 + ")"; 096 } else if (this instanceof Square) { 097 return "daikon.Quant.pairwiseSquare(" + v1 + ", " + v2 + ")"; 098 } else if (this instanceof BitwiseComplement) { 099 return "daikon.Quant.pairwiseBitwiseComplement(" +v1+", "+v2+ ")"; 100 } else if (this instanceof BitwiseSubset) { 101 return "daikon.Quant.pairwiseBitwiseSubset(" +v1+ ", " + v2 + ")"; 102 } else { 103 return format_unimplemented(format); 104 } 105 106 } else if (format == OutputFormat.CSHARPCONTRACT) { 107 108 v1 = var1().csharp_name(); 109 v2 = var2().csharp_name(); 110 String[] split1 = var1().csharp_array_split(); 111 String[] split2 = var2().csharp_array_split(); 112 if (this instanceof Divides) { 113 return "Contract.ForAll(0, " + split1[0] + ".Count(), i => " + split1[0] + " [i]" + split1[1] + " % " + split2[0] + "[i]" + split2[1] + " == 0)"; 114 } else if (this instanceof Square) { 115 return "Contract.ForAll(0, " + split1[0] + ".Count(), i => " + split1[0] + " [i]" + split1[1] + " == " + split2[0] + "[i]" + split2[1] + "*" + split2[0] + "[i]" + split2[1] + ")"; 116 } else if (this instanceof BitwiseComplement) { 117 return "Contract.ForAll(0, " + split1[0] + ".Count(), i => " + split1[0] + " [i]" + split1[1] + " == ~" + split2[0] + "[i]" + split2[1] + ")"; 118 } else if (this instanceof BitwiseSubset) { 119 return "Contract.ForAll(0, " + split1[0] + ".Count(), i => " + split1[0] + " [i]" + split1[1] + " == " + split1[0] + "[i]" + split1[1] + " | " + split2[0] + "[i]" + split2[1] + ")"; 120 } else { 121 return format_unimplemented(format); 122 } 123 124 } 125 126 if (format == OutputFormat.ESCJAVA) { 127 String[] form = VarInfo.esc_quantify(var1(), var2()); 128 fmt_str = form[0] + "(" + fmt_str + ")" + form[3]; 129 v1 = form[1]; 130 v2 = form[2]; 131 } else if (format == OutputFormat.SIMPLIFY) { 132 String[] form = VarInfo.simplify_quantify(QuantFlags.element_wise(), 133 var1(), var2()); 134 fmt_str = form[0] + " " + fmt_str + " " + form[3]; 135 v1 = form[1]; 136 v2 = form[2]; 137 } else { 138 v1 = var1().name_using(format); 139 v2 = var2().name_using(format); 140 if (format == OutputFormat.DAIKON) { 141 fmt_str += " (elementwise)"; 142 } 143 } 144 145 // Note that we do not use String.replaceAll here, because that's 146 // inseparable from the regex library, and we don't want to have to 147 // escape v1 with something like 148 // v1.replaceAll("([\\$\\\\])", "\\\\$1") 149 fmt_str = fmt_str.replace("%var1%", v1); 150 fmt_str = fmt_str.replace("%var2%", v2); 151 152 // if (false && (format == OutputFormat.DAIKON)) { 153 // fmt_str = "[" + getClass() + "]" + fmt_str + " (" 154 // + var1().get_value_info() + ", " + var2().get_value_info() + ")"; 155 // } 156 return fmt_str; 157 } 158 159 /** Calls the function specific equal check and returns the correct status. */ 160 161 @Override 162 public InvariantStatus check_modified(long[] x, long[] y, 163 int count) { 164 if (x.length != y.length) { 165 if (Debug.logOn()) { 166 log("Falsified - x length = %s y length = %s", x.length, y.length); 167 } 168 return InvariantStatus.FALSIFIED; 169 } 170 171 if (Debug.logDetail()) { 172 log("testing values %s, %s", Arrays.toString (x), 173 Arrays.toString(y)); 174 } 175 176 try { 177 for (int i = 0; i < x.length; i++) { 178 if (!eq_check(x[i], y[i])) { 179 if (Debug.logOn()) { 180 log("Falsified - x[%s]=%s y[%s]=%s", i, x[i], i, y[i]); 181 } 182 return InvariantStatus.FALSIFIED; 183 } 184 } 185 return InvariantStatus.NO_CHANGE; 186 } catch (Exception e) { 187 if (Debug.logOn()) { 188 log("Falsified - exception %s", e); 189 } 190 return InvariantStatus.FALSIFIED; 191 } 192 } 193 194 /** 195 * Checks to see if this invariant is over subsequences and if the same relationship holds over 196 * the full sequence. This is obvious if it does. For example 'x[foo..] op y[bar..]' would be 197 * obvious if 'x[] op y[]' This can't fully be handled as a suppression since a suppression needs 198 * to insure that foo == bar as well. But that is not a requirement here (the fact that 'x[] op 199 * y[]' implies that foo == bar when x[] and y[] are not missing). 200 */ 201 public @Nullable DiscardInfo is_subsequence(VarInfo[] vis) { 202 203 VarInfo v1 = var1(vis); 204 VarInfo v2 = var2(vis); 205 206 // Make sure each var is a sequence subsequence 207 if (!v1.isDerived() || !(v1.derived instanceof SequenceScalarSubsequence)) { 208 return null; 209 } 210 if (!v2.isDerived() || !(v2.derived instanceof SequenceScalarSubsequence)) { 211 return null; 212 } 213 214 @NonNull SequenceScalarSubsequence der1 = (SequenceScalarSubsequence) v1.derived; 215 @NonNull SequenceScalarSubsequence der2 = (SequenceScalarSubsequence) v2.derived; 216 217 // Both of the indices must be either from the start or up to the end. 218 // It is not necessary to check that they match in any other way since 219 // if the supersequence holds, that implies that the sequences are 220 // of the same length. Thus any subsequence that starts from the 221 // beginning or finishes at the end must end or start at the same 222 // spot (or it would have been falsified when it didn't) 223 if (der1.from_start != der2.from_start) { 224 return null; 225 } 226 227 // Look up this class over the sequence variables 228 Invariant inv = find(getClass(), der1.seqvar(), der2.seqvar()); 229 if (inv == null) { 230 return null; 231 } 232 return new DiscardInfo(this, DiscardCode.obvious, "Implied by " 233 + inv.format()); 234 } 235 236 @Pure 237 @Override 238 public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) { 239 240 DiscardInfo super_result = super.isObviousDynamically(vis); 241 if (super_result != null) { 242 return super_result; 243 } 244 245 // any elementwise relation across subsequences is made obvious by 246 // the same relation across the original sequence 247 DiscardInfo result = is_subsequence(vis); 248 if (result != null) { 249 return result; 250 } 251 252 // Check for invariant specific obvious checks. The obvious_checks 253 // method returns an array of arrays of antecedents. If all of the 254 // antecedents in an array are true, then the invariant is obvoius. 255 InvDef[][] obvious_arr = obvious_checks(vis); 256 obvious_loop: 257 for (int i = 0; i < obvious_arr.length; i++) { 258 InvDef[] antecedents = obvious_arr[i]; 259 StringBuilder why = null; 260 for (int j = 0; j < antecedents.length; j++) { 261 Invariant inv = antecedents[j].find(); 262 if (inv == null) { 263 continue obvious_loop; 264 } 265 if (why == null) { 266 why = new StringBuilder(inv.format()); 267 } else { 268 why.append(" and "); 269 why.append(inv.format()); 270 } 271 } 272 return new DiscardInfo(this, DiscardCode.obvious, "Implied by " + why); 273 } 274 275 return null; 276 } 277 278 /** 279 * Returns an invariant that is true when the size(v1) == size(v2). There are a number of 280 * possible cases for an array: 281 * 282 * <pre> 283 * x[] - entire array, size usually available as size(x[]) 284 * x[..(n-1)] - size is n 285 * x[..n] - size is n+1 286 * x[n..] - size is size(x[]) - n 287 * x[(n+1)..] - size is size(x[]) - (n+1) 288 * </pre> 289 * 290 * Each combination of the above must be considered in creating the equality invariant. Not all 291 * possibilities can be handled. Null is returned in that case. In the following table, s stands 292 * for the size 293 * 294 * <pre> 295 * x[] x[..(n-1)] x[..n] x[n..] x[(n+1)..] 296 * --------- ---------- ------ ------ ---------- 297 * y[] s(y)=s(x) s(y)=n 298 * y[..(m-1)] x m=n 299 * y[..m] x x m=n 300 * y[m..] x x x m=n ∧ 301 * s(y)=s(x) 302 * y[(m+1)..] x x x x m=n ∧ 303 * s(y)=s(x) 304 * </pre> 305 * NOTE: this is not currently used. Many (if not all) of the missing table cells above could be 306 * filled in with linear binary invariants (eg, m = n + 1). 307 */ 308 public @Nullable InvDef array_sizes_eq(VarInfo v1, VarInfo v2) { 309 310 VarInfo v1_size = get_array_size(v1); 311 VarInfo v2_size = get_array_size(v2); 312 313 // If we can find a size variable for each side build the invariant 314 if ((v1_size != null) && (v2_size != null)) { 315 return new InvDef(v1_size, v2_size, IntEqual.class); 316 } 317 318 // If either variable is not derived, there is no possible invariant 319 // (since we covered all of the direct size comparisons above) 320 if ((v1.derived == null) || (v2.derived == null)) { 321 return null; 322 } 323 324 // Get the sequence subsequence derivations 325 SequenceScalarSubsequence v1_ss = (SequenceScalarSubsequence) v1.derived; 326 SequenceScalarSubsequence v2_ss = (SequenceScalarSubsequence) v2.derived; 327 328 // If both are from_start and have the same index_shift, just compare 329 // the variables 330 if (v1_ss.from_start && v2_ss.from_start 331 && (v1_ss.index_shift == v2_ss.index_shift)) { 332 return new InvDef(v1_ss.sclvar(), v2_ss.sclvar(), IntEqual.class); 333 } 334 335 return null; 336 } 337 338 /** 339 * Returns a variable that corresponds to the size of v. Returns null if no such variable exists. 340 * 341 * There are two cases that are not handled: x[..n] with an index shift and x[n..]. 342 */ 343 public @Nullable VarInfo get_array_size(VarInfo v) { 344 345 assert v.rep_type.isArray(); 346 347 if (v.derived == null) { 348 return v.sequenceSize(); 349 } else if (v.derived instanceof SequenceScalarSubsequence) { 350 SequenceScalarSubsequence ss = (SequenceScalarSubsequence) v.derived; 351 if (ss.from_start && (ss.index_shift == -1)) { 352 return ss.sclvar(); 353 } 354 } 355 356 return null; 357 } 358 359 /** 360 * Return a format string for the specified output format. Each instance of %varN% will be 361 * replaced by the correct name for varN. 362 */ 363 public abstract String get_format_str(@GuardSatisfied PairwiseNumericInt this, OutputFormat format); 364 365 /** Returns true if x and y don't invalidate the invariant. */ 366 public abstract boolean eq_check(long x, long y); 367 368 /** 369 * Returns an array of arrays of antecedents. If all of the antecedents in any array are true, 370 * then the invariant is obvious. 371 */ 372 public InvDef[][] obvious_checks(VarInfo[] vis) { 373 return new InvDef[][] {}; 374 } 375 376 public static List<@Prototype Invariant> get_proto_all() { 377 378 List<@Prototype Invariant> result = new ArrayList<>(); 379 380 result.add(Divides.get_proto(false)); 381 result.add(Divides.get_proto(true)); 382 result.add(Square.get_proto(false)); 383 result.add(Square.get_proto(true)); 384 385 result.add(BitwiseComplement.get_proto()); 386 result.add(BitwiseSubset.get_proto(false)); 387 result.add(BitwiseSubset.get_proto(true)); 388 389 // System.out.printf("%s get proto: %s%n", PairwiseNumericInt.class, result); 390 return result; 391 } 392 393 // suppressor definitions, used by many of the classes below 394 protected static NISuppressor 395 396 var1_eq_0 = new NISuppressor(0, EltRangeInt.EqualZero.class), 397 var2_eq_0 = new NISuppressor(1, EltRangeInt.EqualZero.class), 398 var1_ge_0 = new NISuppressor(0, EltRangeInt.GreaterEqualZero.class), 399 var2_ge_0 = new NISuppressor(1, EltRangeInt.GreaterEqualZero.class), 400 var1_eq_1 = new NISuppressor(0, EltRangeInt.EqualOne.class), 401 var2_eq_1 = new NISuppressor(1, EltRangeInt.EqualOne.class), 402 var1_eq_minus_1 = new NISuppressor(0, EltRangeInt.EqualMinusOne.class), 403 var2_eq_minus_1 = new NISuppressor(1, EltRangeInt.EqualMinusOne.class), 404 var1_ne_0 = new NISuppressor(0, EltNonZero.class), 405 var2_ne_0 = new NISuppressor(1, EltNonZero.class), 406 var1_le_var2 = new NISuppressor(0, 1, PairwiseIntLessEqual.class), 407 408 var1_eq_var2 = new NISuppressor(0, 1, PairwiseIntEqual.class), 409 var2_eq_var1 = new NISuppressor(0, 1, PairwiseIntEqual.class); 410 411 protected static NISuppressor var2_valid_shift = 412 new NISuppressor(1, EltRangeInt.Bound0_63.class); 413 414 // 415 // Int and Float Numeric Invariants 416 // 417 418 /** 419 * Represents the divides without remainder invariant between corresponding elements of two sequences of long. 420 * Prints as {@code x[] % y[] == 0}. 421 */ 422 public static class Divides extends PairwiseNumericInt { 423 // We are Serializable, so we specify a version to allow changes to 424 // method signatures without breaking serialization. If you add or 425 // remove fields, you should change this number to the current date. 426 static final long serialVersionUID = 20040113L; 427 428 protected Divides(PptSlice ppt, boolean swap) { 429 super(ppt, swap); 430 } 431 432 protected Divides(boolean swap) { 433 super(swap); 434 } 435 436 private static @Prototype Divides proto = new @Prototype Divides(false); 437 private static @Prototype Divides proto_swap = new @Prototype Divides(true); 438 439 /** Returns the prototype invariant. */ 440 public static @Prototype PairwiseNumericInt get_proto(boolean swap) { 441 if (swap) { 442 return proto_swap; 443 } else { 444 return proto; 445 } 446 } 447 448 // Variables starting with dkconfig_ should only be set via the 449 // daikon.config.Configuration interface. 450 /** Boolean. True iff divides invariants should be considered. */ 451 public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault; 452 453 @Override 454 public boolean enabled() { 455 return dkconfig_enabled; 456 } 457 458 @Override 459 protected Divides instantiate_dyn(@Prototype Divides this, PptSlice slice) { 460 return new Divides(slice, swap); 461 } 462 463 @Override 464 public String get_format_str(@GuardSatisfied Divides this, OutputFormat format) { 465 if (format == OutputFormat.SIMPLIFY) { 466 return "(EQ 0 (MOD %var1% %var2%))"; 467 } else if (format == OutputFormat.CSHARPCONTRACT) { 468 return "%var1% % %var2% == 0"; 469 } else { 470 return "%var1% % %var2% == 0"; 471 } 472 } 473 474 @Override 475 public boolean eq_check(long x, long y) { 476 return (0 == (x % y)); 477 } 478 479 /** 480 * This needs to be an obvious check and not a suppression for sequences because there is no 481 * consistent way to check that var1 and var2 have the same length (for derivations). 482 */ 483 @Override 484 public InvDef[][] obvious_checks(VarInfo[] vis) { 485 486 return new InvDef[][] { 487 new InvDef[] { 488 new InvDef(var2(vis), EltOneOf.class, InvDef.elts_minus_one_and_plus_one) 489 }, 490 new InvDef[] { 491 new InvDef(var1(), EltOneOf.class, InvDef.elts_zero) 492 } 493 }; 494 } 495 496 /** Returns a list of non-instantiating suppressions for this invariant. */ 497 @Pure 498 @Override 499 public NISuppressionSet get_ni_suppressions() { 500 if (swap) { 501 return suppressions_swap; 502 } else { 503 return suppressions; 504 } 505 } 506 507 /** definition of this invariant (the suppressee) (unswapped) */ 508 private static NISuppressee suppressee = new NISuppressee(Divides.class, false); 509 510 private static NISuppressionSet suppressions = 511 new NISuppressionSet( 512 new NISuppression[] { 513 514 // (var1 == var2) ^ (var2 != 0) ==> var1 % var2 == 0 515 new NISuppression(var1_eq_var2, var2_ne_0, suppressee), 516 517 // (var2 == var1) ^ (var1 != 0) ==> var2 % var1 == 0 518 new NISuppression(var2_eq_var1, var1_ne_0, suppressee), 519 520 }); 521 private static NISuppressionSet suppressions_swap = suppressions.swap(); 522 523 /** 524 * Returns non-null if this invariant is obvious from an existing, non-falsified linear binary 525 * invariant in the same slice as this invariant. This invariant of the form "x % y == 0" is 526 * falsified if a linear binary invariant is found of the form "a*y - 1*x + 0 == 0" 527 * 528 * @return non-null value iff this invariant is obvious from other invariants in the same slice 529 */ 530 @Pure 531 @Override 532 public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) { 533 // First call super type's method, and if it returns non-null, then 534 // this invariant is already known to be obvious, so just return 535 // whatever reason the super type returned. 536 DiscardInfo di = super.isObviousDynamically(vis); 537 if (di != null) { 538 return di; 539 } 540 541 VarInfo var1 = vis[0]; 542 VarInfo var2 = vis[1]; 543 544 // ensure that var1.varinfo_index <= var2.varinfo_index 545 if (var1.varinfo_index > var2.varinfo_index) { 546 var1 = vis[1]; 547 var2 = vis[0]; 548 } 549 550 // Find slice corresponding to these two variables. 551 // Ideally, this should always just be ppt if all 552 // falsified invariants have been removed. 553 PptSlice2 ppt2 = ppt.parent.findSlice(var1,var2); 554 555 // If no slice is found , no invariants exist to make this one obvious. 556 if (ppt2 == null) { 557 return null; 558 } 559 560 // For each invariant, check to see if it's a linear binary 561 // invariant of the form "a*y - 1*x + 0 == 0" and if so, 562 // you know this invariant of the form "x % y == 0" is obvious. 563 for(Invariant inv : ppt2.invs) { 564 565 if (inv instanceof LinearBinary) { 566 LinearBinary linv = (LinearBinary) inv; 567 568 // General form for linear binary: a*x + b*y + c == 0, 569 // but a and b can be switched with respect to vis, and either 570 // one may be negative, so instead check: 571 // - c == 0 572 // - a*b < 0 (a and b have different signs) 573 // - |a| == 1 or |b| == 1, so one will divide the other 574 // While this means that both x % y == 0 and y % x == 0, 575 // only one of these invariants will still be true at this 576 // time, and only that one will be falsified by this test. 577 if (!linv.is_false() 578 && Global.fuzzy.eq(linv.core.c, 0) 579 && linv.core.b * linv.core.a < 0 580 && (Global.fuzzy.eq(linv.core.a * linv.core.a, 1) 581 || Global.fuzzy.eq(linv.core.b * linv.core.b, 1))) { 582 return new DiscardInfo(this, DiscardCode.obvious, 583 "Linear binary invariant implies divides"); 584 } 585 } 586 } 587 588 return null; 589 } 590 591 } 592 593 /** 594 * Represents the square invariant between corresponding elements of two sequences of long. 595 * Prints as {@code x[] = y[]**2}. 596 */ 597 public static class Square extends PairwiseNumericInt { 598 // We are Serializable, so we specify a version to allow changes to 599 // method signatures without breaking serialization. If you add or 600 // remove fields, you should change this number to the current date. 601 static final long serialVersionUID = 20040113L; 602 603 protected Square(PptSlice ppt, boolean swap) { 604 super(ppt, swap); 605 } 606 607 protected Square(boolean swap) { 608 super(swap); 609 } 610 611 private static @Prototype Square proto = new @Prototype Square(false); 612 private static @Prototype Square proto_swap = new @Prototype Square(true); 613 614 /** Returns the prototype invariant. */ 615 public static @Prototype Square get_proto(boolean swap) { 616 if (swap) { 617 return proto_swap; 618 } else { 619 return proto; 620 } 621 } 622 623 // Variables starting with dkconfig_ should only be set via the 624 // daikon.config.Configuration interface. 625 /** Boolean. True iff square invariants should be considered. */ 626 public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault; 627 628 @Override 629 public boolean enabled() { 630 return dkconfig_enabled; 631 } 632 @Override 633 protected Square instantiate_dyn(@Prototype Square this, PptSlice slice) { 634 return new Square(slice, swap); 635 } 636 637 @Override 638 public String get_format_str(@GuardSatisfied Square this, OutputFormat format) { 639 if (format == OutputFormat.SIMPLIFY) { 640 return "(EQ %var1% (* %var2% %var2))"; 641 } else if (format == OutputFormat.CSHARPCONTRACT) { 642 return "%var1% == %var2%*%var2%"; 643 } else if (format.isJavaFamily()) { 644 645 return "%var1% == %var2%*%var2%"; 646 } else { 647 return "%var1% == %var2%**2"; 648 } 649 } 650 651 /** Check to see if x == y squared. */ 652 @Override 653 public boolean eq_check(long x, long y) { 654 return (x == y*y); 655 } 656 657 // Note there are no NI Suppressions for Square. Two obvious 658 // suppressions are: 659 // 660 // (var2 == 1) ^ (var1 == 1) ==> var1 = var2*var2 661 // (var2 == 0) ^ (var1 == 0) ==> var1 = var2*var2 662 // 663 // But all of the antecedents would be constants, so we would 664 // never need to create this slice, so there is no reason to create 665 // these. 666 667 } 668 669 /** 670 * Represents the zero tracks invariant between 671 * corresponding elements of two sequences of long; that is, when {@code x[]} is zero, 672 * {@code y[]} is also zero. 673 * Prints as {@code x[] = 0 => y[] = 0}. 674 */ 675 public static class ZeroTrack extends PairwiseNumericInt { 676 // We are Serializable, so we specify a version to allow changes to 677 // method signatures without breaking serialization. If you add or 678 // remove fields, you should change this number to the current date. 679 static final long serialVersionUID = 20040313L; 680 681 protected ZeroTrack(PptSlice ppt, boolean swap) { 682 super(ppt, swap); 683 } 684 685 protected @Prototype ZeroTrack(boolean swap) { 686 super(swap); 687 } 688 689 private static @Prototype ZeroTrack proto = new @Prototype ZeroTrack(false); 690 private static @Prototype ZeroTrack proto_swap = new @Prototype ZeroTrack(true); 691 692 /** Returns the prototype invariant. */ 693 public static @Prototype ZeroTrack get_proto(boolean swap) { 694 if (swap) { 695 return proto_swap; 696 } else { 697 return proto; 698 } 699 } 700 701 // Variables starting with dkconfig_ should only be set via the 702 // daikon.config.Configuration interface. 703 /** Boolean. True iff zero-track invariants should be considered. */ 704 public static boolean dkconfig_enabled = false; 705 706 @Override 707 public boolean enabled() { 708 return dkconfig_enabled; 709 } 710 711 @Override 712 protected ZeroTrack instantiate_dyn(@Prototype ZeroTrack this, PptSlice slice) { 713 return new ZeroTrack(slice, swap); 714 } 715 716 @Override 717 public String get_format_str(@GuardSatisfied ZeroTrack this, OutputFormat format) { 718 if (format == OutputFormat.SIMPLIFY) { 719 return "(IMPLIES (EQ %var1% 0) (EQ %var2% 0))"; 720 } else if (format.isJavaFamily() || format == OutputFormat.CSHARPCONTRACT) { 721 return "(!(%var1% == 0)) || (%var2% == 0)"; 722 } else { 723 return "(%var1% == 0) ==> (%var2% == 0)"; 724 } 725 } 726 727 @Override 728 public boolean eq_check(long x, long y) { 729 if (x == 0) { 730 return y == 0; 731 } else { 732 return true; 733 } 734 } 735 736 /** Returns a list of non-instantiating suppressions for this invariant. */ 737 @Pure 738 @Override 739 public NISuppressionSet get_ni_suppressions() { 740 if (swap) { 741 return suppressions_swap; 742 } else { 743 return suppressions; 744 } 745 } 746 747 /** definition of this invariant (the suppressee) (unswapped) */ 748 private static NISuppressee suppressee = new NISuppressee(ZeroTrack.class, false); 749 750 private static NISuppressionSet suppressions = 751 new NISuppressionSet( 752 new NISuppression[] { 753 // (var1 == var2) ==> (var1=0 ==> var2=0) 754 new NISuppression(var1_eq_var2, suppressee), 755 // (var1 != 0) ==> (var1=0 ==> var2=0) 756 new NISuppression(var1_ne_0, suppressee), 757 // (var2 == 0) ==> (var1=0 ==> var2=0) 758 new NISuppression(var2_eq_0, suppressee), 759 }); 760 private static NISuppressionSet suppressions_swap = suppressions.swap(); 761 762 } 763 764 /** 765 * Represents the bitwise complement invariant between corresponding elements of two sequences of long. 766 * Prints as {@code x[] = ~y[]}. 767 */ 768 public static class BitwiseComplement extends PairwiseNumericInt { 769 // We are Serializable, so we specify a version to allow changes to 770 // method signatures without breaking serialization. If you add or 771 // remove fields, you should change this number to the current date. 772 static final long serialVersionUID = 20040113L; 773 774 protected BitwiseComplement(PptSlice ppt) { 775 super(ppt, false); 776 } 777 778 protected @Prototype BitwiseComplement() { 779 super(false); 780 } 781 782 private static @Prototype BitwiseComplement proto = new @Prototype BitwiseComplement(); 783 784 /** Returns the prototype invariant. */ 785 public static @Prototype BitwiseComplement get_proto() { 786 return proto; 787 } 788 789 // Variables starting with dkconfig_ should only be set via the 790 // daikon.config.Configuration interface. 791 /** Boolean. True iff bitwise complement invariants should be considered. */ 792 public static boolean dkconfig_enabled = false; 793 794 @Override 795 public boolean enabled() { 796 return dkconfig_enabled; 797 } 798 799 @Override 800 protected BitwiseComplement instantiate_dyn(@Prototype BitwiseComplement this, PptSlice slice) { 801 return new BitwiseComplement(slice); 802 } 803 804 @Pure 805 @Override 806 public boolean is_symmetric() { 807 return true; 808 } 809 810 @Override 811 public String get_format_str(@GuardSatisfied BitwiseComplement this, OutputFormat format) { 812 if (format == OutputFormat.SIMPLIFY) { 813 return "(EQ %var1% (~ %var2%))"; 814 } else if (format == OutputFormat.CSHARPCONTRACT) { 815 return "%var1% == ~%var2%"; 816 } else { 817 return "%var1% == ~%var2%"; 818 } 819 } 820 821 /** Check to see if x == ~y . */ 822 @Override 823 public boolean eq_check(long x, long y) { 824 return (x == ~y); 825 } 826 } 827 828 /** 829 * Represents the bitwise subset invariant between corresponding elements of two sequences of long; that is, the bits of 830 * {@code y[]} are a subset of the bits of {@code x[]}. 831 * Prints as {@code x[] = y[] | x[]}. 832 */ 833 public static class BitwiseSubset extends PairwiseNumericInt { 834 // We are Serializable, so we specify a version to allow changes to 835 // method signatures without breaking serialization. If you add or 836 // remove fields, you should change this number to the current date. 837 static final long serialVersionUID = 20040113L; 838 839 protected BitwiseSubset(PptSlice ppt, boolean swap) { 840 super(ppt, swap); 841 } 842 843 protected BitwiseSubset(boolean swap) { 844 super(swap); 845 } 846 847 private static @Prototype BitwiseSubset proto = new @Prototype BitwiseSubset(false); 848 private static @Prototype BitwiseSubset proto_swap = new @Prototype BitwiseSubset(true); 849 850 /** Returns the prototype invariant. */ 851 public static @Prototype BitwiseSubset get_proto(boolean swap) { 852 if (swap) { 853 return proto_swap; 854 } else { 855 return proto; 856 } 857 } 858 859 // Variables starting with dkconfig_ should only be set via the 860 // daikon.config.Configuration interface. 861 /** Boolean. True iff bitwise subset invariants should be considered. */ 862 public static boolean dkconfig_enabled = false; 863 864 @Override 865 public boolean enabled() { 866 return dkconfig_enabled; 867 } 868 869 @Override 870 public BitwiseSubset instantiate_dyn(@Prototype BitwiseSubset this, PptSlice slice) { 871 return new BitwiseSubset(slice, swap); 872 } 873 874 @Override 875 public String get_format_str(@GuardSatisfied BitwiseSubset this, OutputFormat format) { 876 if (format == OutputFormat.SIMPLIFY) { 877 return "(EQ %var1% (|java-bitwise-or| %var2% %var1%))"; 878 } else if (format == OutputFormat.DAIKON) { 879 return "%var2% is a bitwise subset of %var1%"; 880 } else if (format == OutputFormat.CSHARPCONTRACT) { 881 return "%var1% == (%var2% | %var1%)"; 882 } else { 883 return "%var1% == (%var2% | %var1%)"; 884 } 885 } 886 887 @Override 888 public boolean eq_check(long x, long y) { 889 return (x == (y | x)); 890 } 891 892 /** 893 * This needs to be an obvious check and not a suppression for sequences because there is no 894 * consistent way to check that var1 and var2 have the same length (for derivations). 895 */ 896 @Override 897 public InvDef[][] obvious_checks(VarInfo[] vis) { 898 899 return new InvDef[][] { 900 // suppress if var2 == 0 901 new InvDef[] {new InvDef(var2(), EltOneOf.class, InvDef.elts_zero)}, 902 // suppress if var1 == -1 (all of its bits are on) 903 new InvDef[] {new InvDef(var1(), EltOneOf.class, InvDef.elts_minus_one)} 904 }; 905 } 906 907 /** Returns a list of non-instantiating suppressions for this invariant. */ 908 @Pure 909 @Override 910 public NISuppressionSet get_ni_suppressions() { 911 if (swap) { 912 return suppressions_swap; 913 } else { 914 return suppressions; 915 } 916 } 917 918 /** definition of this invariant (the suppressee) (unswapped) */ 919 private static NISuppressee suppressee = new NISuppressee(BitwiseSubset.class, false); 920 921 private static NISuppressionSet suppressions = 922 new NISuppressionSet( 923 new NISuppression[] { 924 925 // (var1 == var2) ==> var1 = (var2 | var1) 926 new NISuppression(var1_eq_var2, suppressee), 927 928 }); 929 private static NISuppressionSet suppressions_swap = suppressions.swap(); 930 } 931 932 /** 933 * Represents the BitwiseAnd == 0 invariant between corresponding elements of two sequences of long; that is, {@code x[]} and 934 * {@code y[]} have no bits in common. 935 * Prints as {@code x[] & y[] == 0}. 936 */ 937 public static class BitwiseAndZero extends PairwiseNumericInt { 938 // We are Serializable, so we specify a version to allow changes to 939 // method signatures without breaking serialization. If you add or 940 // remove fields, you should change this number to the current date. 941 static final long serialVersionUID = 20040313L; 942 943 protected BitwiseAndZero(PptSlice ppt) { 944 super(ppt, false); 945 } 946 947 protected @Prototype BitwiseAndZero() { 948 super(false); 949 } 950 951 private static @Prototype BitwiseAndZero proto = new @Prototype BitwiseAndZero(); 952 953 /** Returns the prototype invariant. */ 954 public static @Prototype BitwiseAndZero get_proto() { 955 return proto; 956 } 957 958 // Variables starting with dkconfig_ should only be set via the 959 // daikon.config.Configuration interface. 960 /** Boolean. True iff BitwiseAndZero invariants should be considered. */ 961 public static boolean dkconfig_enabled = false; 962 963 @Override 964 public boolean enabled() { 965 return dkconfig_enabled; 966 } 967 968 @Override 969 public BitwiseAndZero instantiate_dyn(@Prototype BitwiseAndZero this, PptSlice slice) { 970 return new BitwiseAndZero(slice); 971 } 972 973 @Override 974 public String get_format_str(@GuardSatisfied BitwiseAndZero this, OutputFormat format) { 975 if (format == OutputFormat.SIMPLIFY) { 976 return "(EQ (|java-&| %var1% %var2%) 0)"; 977 } else if (format == OutputFormat.CSHARPCONTRACT) { 978 return "(%var1% & %var2%) == 0"; 979 } else { 980 return "(%var1% & %var2%) == 0"; 981 } 982 } 983 984 @Pure 985 @Override 986 public boolean is_symmetric() { 987 return true; 988 } 989 990 @Override 991 public boolean eq_check(long x, long y) { 992 return (x & y) == 0; 993 } 994 995 /** Returns a list of non-instantiating suppressions for this invariant. */ 996 @Pure 997 @Override 998 public @Nullable NISuppressionSet get_ni_suppressions() { 999 return suppressions; 1000 } 1001 1002 private static @Nullable NISuppressionSet suppressions = null; 1003 1004 } 1005 1006 /** 1007 * Represents the ShiftZero invariant between corresponding elements of two sequences of long; that is, {@code x[]} 1008 * right-shifted by {@code y[]} is always zero. 1009 * Prints as {@code x[] >> y[] = 0}. 1010 */ 1011 public static class ShiftZero extends PairwiseNumericInt { 1012 // We are Serializable, so we specify a version to allow changes to 1013 // method signatures without breaking serialization. If you add or 1014 // remove fields, you should change this number to the current date. 1015 static final long serialVersionUID = 20040313L; 1016 1017 protected ShiftZero(PptSlice ppt, boolean swap) { 1018 super(ppt, swap); 1019 } 1020 1021 protected ShiftZero(boolean swap) { 1022 super(swap); 1023 } 1024 1025 private static @Prototype ShiftZero proto = new @Prototype ShiftZero(false); 1026 private static @Prototype ShiftZero proto_swap = new @Prototype ShiftZero(true); 1027 1028 /** Returns the prototype invariant. */ 1029 public static @Prototype ShiftZero get_proto(boolean swap) { 1030 if (swap) { 1031 return proto_swap; 1032 } else { 1033 return proto; 1034 } 1035 } 1036 1037 // Variables starting with dkconfig_ should only be set via the 1038 // daikon.config.Configuration interface. 1039 /** Boolean. True iff ShiftZero invariants should be considered. */ 1040 public static boolean dkconfig_enabled = false; 1041 1042 @Override 1043 public boolean enabled() { 1044 return dkconfig_enabled; 1045 } 1046 1047 @Override 1048 protected ShiftZero instantiate_dyn(@Prototype ShiftZero this, PptSlice slice) { 1049 return new ShiftZero(slice, swap); 1050 } 1051 1052 @Override 1053 public String get_format_str(@GuardSatisfied ShiftZero this, OutputFormat format) { 1054 if (format == OutputFormat.SIMPLIFY) { 1055 return "(EQ (|java->>| %var1% %var2%) 0)"; 1056 } else if (format == OutputFormat.CSHARPCONTRACT) { 1057 return "(%var1% >> %var2% == 0)"; 1058 } else { 1059 return "(%var1% >> %var2% == 0)"; 1060 } 1061 } 1062 1063 @Override 1064 public boolean eq_check(long x, long y) { 1065 if ((y < 0) || (y > 63)) { 1066 throw new ArithmeticException("shift op (" + y + ") is out of range"); 1067 } 1068 return (x >> y) == 0; 1069 } 1070 1071 /** Returns a list of non-instantiating suppressions for this invariant. */ 1072 @Pure 1073 @Override 1074 public NISuppressionSet get_ni_suppressions() { 1075 if (swap) { 1076 return suppressions_swap; 1077 } else { 1078 return suppressions; 1079 } 1080 } 1081 1082 /** definition of this invariant (the suppressee) (unswapped) */ 1083 private static NISuppressee suppressee = new NISuppressee(ShiftZero.class, false); 1084 1085 private static NISuppressionSet suppressions = 1086 new NISuppressionSet( 1087 new NISuppression[] { 1088 // (var1>=0) ^ (var1<=var2) ^ (0<=var2<=63) ==> (var1 >> var2) == 0 1089 new NISuppression(var1_ge_0, var1_le_var2, var2_valid_shift, 1090 suppressee), 1091 }); 1092 private static NISuppressionSet suppressions_swap = suppressions.swap(); 1093 } 1094 1095// 1096// Standard String invariants 1097// 1098 1099}