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 { 468 return "%var1% % %var2% == 0"; 469 } 470 } 471 472 @Override 473 public boolean eq_check(long x, long y) { 474 return (0 == (x % y)); 475 } 476 477 /** 478 * This needs to be an obvious check and not a suppression for sequences because there is no 479 * consistent way to check that var1 and var2 have the same length (for derivations). 480 */ 481 @Override 482 public InvDef[][] obvious_checks(VarInfo[] vis) { 483 484 return new InvDef[][] { 485 new InvDef[] { 486 new InvDef(var2(vis), EltOneOf.class, InvDef.elts_minus_one_and_plus_one) 487 }, 488 new InvDef[] { 489 new InvDef(var1(), EltOneOf.class, InvDef.elts_zero) 490 } 491 }; 492 } 493 494 /** Returns a list of non-instantiating suppressions for this invariant. */ 495 @Pure 496 @Override 497 public NISuppressionSet get_ni_suppressions() { 498 if (swap) { 499 return suppressions_swap; 500 } else { 501 return suppressions; 502 } 503 } 504 505 /** definition of this invariant (the suppressee) (unswapped) */ 506 private static NISuppressee suppressee = new NISuppressee(Divides.class, false); 507 508 private static NISuppressionSet suppressions = 509 new NISuppressionSet( 510 new NISuppression[] { 511 512 // (var1 == var2) ^ (var2 != 0) ==> var1 % var2 == 0 513 new NISuppression(var1_eq_var2, var2_ne_0, suppressee), 514 515 // (var2 == var1) ^ (var1 != 0) ==> var2 % var1 == 0 516 new NISuppression(var2_eq_var1, var1_ne_0, suppressee), 517 518 }); 519 private static NISuppressionSet suppressions_swap = suppressions.swap(); 520 521 /** 522 * Returns non-null if this invariant is obvious from an existing, non-falsified linear binary 523 * invariant in the same slice as this invariant. This invariant of the form "x % y == 0" is 524 * falsified if a linear binary invariant is found of the form "a*y - 1*x + 0 == 0" 525 * 526 * @return non-null value iff this invariant is obvious from other invariants in the same slice 527 */ 528 @Pure 529 @Override 530 public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) { 531 // First call super type's method, and if it returns non-null, then 532 // this invariant is already known to be obvious, so just return 533 // whatever reason the super type returned. 534 DiscardInfo di = super.isObviousDynamically(vis); 535 if (di != null) { 536 return di; 537 } 538 539 VarInfo var1 = vis[0]; 540 VarInfo var2 = vis[1]; 541 542 // ensure that var1.varinfo_index <= var2.varinfo_index 543 if (var1.varinfo_index > var2.varinfo_index) { 544 var1 = vis[1]; 545 var2 = vis[0]; 546 } 547 548 // Find slice corresponding to these two variables. 549 // Ideally, this should always just be ppt if all 550 // falsified invariants have been removed. 551 PptSlice2 ppt2 = ppt.parent.findSlice(var1,var2); 552 553 // If no slice is found , no invariants exist to make this one obvious. 554 if (ppt2 == null) { 555 return null; 556 } 557 558 // For each invariant, check to see if it's a linear binary 559 // invariant of the form "a*y - 1*x + 0 == 0" and if so, 560 // you know this invariant of the form "x % y == 0" is obvious. 561 for(Invariant inv : ppt2.invs) { 562 563 if (inv instanceof LinearBinary) { 564 LinearBinary linv = (LinearBinary) inv; 565 566 // General form for linear binary: a*x + b*y + c == 0, 567 // but a and b can be switched with respect to vis, and either 568 // one may be negative, so instead check: 569 // - c == 0 570 // - a*b < 0 (a and b have different signs) 571 // - |a| == 1 or |b| == 1, so one will divide the other 572 // While this means that both x % y == 0 and y % x == 0, 573 // only one of these invariants will still be true at this 574 // time, and only that one will be falsified by this test. 575 if (!linv.is_false() 576 && Global.fuzzy.eq(linv.core.c, 0) 577 && linv.core.b * linv.core.a < 0 578 && (Global.fuzzy.eq(linv.core.a * linv.core.a, 1) 579 || Global.fuzzy.eq(linv.core.b * linv.core.b, 1))) { 580 return new DiscardInfo(this, DiscardCode.obvious, 581 "Linear binary invariant implies divides"); 582 } 583 } 584 } 585 586 return null; 587 } 588 589 } 590 591 /** 592 * Represents the square invariant between corresponding elements of two sequences of long. 593 * Prints as {@code x[] = y[]**2}. 594 */ 595 public static class Square extends PairwiseNumericInt { 596 // We are Serializable, so we specify a version to allow changes to 597 // method signatures without breaking serialization. If you add or 598 // remove fields, you should change this number to the current date. 599 static final long serialVersionUID = 20040113L; 600 601 protected Square(PptSlice ppt, boolean swap) { 602 super(ppt, swap); 603 } 604 605 protected Square(boolean swap) { 606 super(swap); 607 } 608 609 private static @Prototype Square proto = new @Prototype Square(false); 610 private static @Prototype Square proto_swap = new @Prototype Square(true); 611 612 /** Returns the prototype invariant. */ 613 public static @Prototype Square get_proto(boolean swap) { 614 if (swap) { 615 return proto_swap; 616 } else { 617 return proto; 618 } 619 } 620 621 // Variables starting with dkconfig_ should only be set via the 622 // daikon.config.Configuration interface. 623 /** Boolean. True iff square invariants should be considered. */ 624 public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault; 625 626 @Override 627 public boolean enabled() { 628 return dkconfig_enabled; 629 } 630 @Override 631 protected Square instantiate_dyn(@Prototype Square this, PptSlice slice) { 632 return new Square(slice, swap); 633 } 634 635 @Override 636 public String get_format_str(@GuardSatisfied Square this, OutputFormat format) { 637 if (format == OutputFormat.SIMPLIFY) { 638 return "(EQ %var1% (* %var2% %var2))"; 639 } else if (format == OutputFormat.CSHARPCONTRACT) { 640 return "%var1% == %var2%*%var2%"; 641 } else if (format.isJavaFamily()) { 642 643 return "%var1% == %var2%*%var2%"; 644 } else { 645 return "%var1% == %var2%**2"; 646 } 647 } 648 649 /** Check to see if x == y squared. */ 650 @Override 651 public boolean eq_check(long x, long y) { 652 return (x == y*y); 653 } 654 655 // Note there are no NI Suppressions for Square. Two obvious 656 // suppressions are: 657 // 658 // (var2 == 1) ^ (var1 == 1) ==> var1 = var2*var2 659 // (var2 == 0) ^ (var1 == 0) ==> var1 = var2*var2 660 // 661 // But all of the antecedents would be constants, so we would 662 // never need to create this slice, so there is no reason to create 663 // these. 664 665 } 666 667 /** 668 * Represents the zero tracks invariant between 669 * corresponding elements of two sequences of long; that is, when {@code x[]} is zero, 670 * {@code y[]} is also zero. 671 * Prints as {@code x[] = 0 => y[] = 0}. 672 */ 673 public static class ZeroTrack extends PairwiseNumericInt { 674 // We are Serializable, so we specify a version to allow changes to 675 // method signatures without breaking serialization. If you add or 676 // remove fields, you should change this number to the current date. 677 static final long serialVersionUID = 20040313L; 678 679 protected ZeroTrack(PptSlice ppt, boolean swap) { 680 super(ppt, swap); 681 } 682 683 protected @Prototype ZeroTrack(boolean swap) { 684 super(swap); 685 } 686 687 private static @Prototype ZeroTrack proto = new @Prototype ZeroTrack(false); 688 private static @Prototype ZeroTrack proto_swap = new @Prototype ZeroTrack(true); 689 690 /** Returns the prototype invariant. */ 691 public static @Prototype ZeroTrack get_proto(boolean swap) { 692 if (swap) { 693 return proto_swap; 694 } else { 695 return proto; 696 } 697 } 698 699 // Variables starting with dkconfig_ should only be set via the 700 // daikon.config.Configuration interface. 701 /** Boolean. True iff zero-track invariants should be considered. */ 702 public static boolean dkconfig_enabled = false; 703 704 @Override 705 public boolean enabled() { 706 return dkconfig_enabled; 707 } 708 709 @Override 710 protected ZeroTrack instantiate_dyn(@Prototype ZeroTrack this, PptSlice slice) { 711 return new ZeroTrack(slice, swap); 712 } 713 714 @Override 715 public String get_format_str(@GuardSatisfied ZeroTrack this, OutputFormat format) { 716 if (format == OutputFormat.SIMPLIFY) { 717 return "(IMPLIES (EQ %var1% 0) (EQ %var2% 0))"; 718 } else if (format.isJavaFamily() || format == OutputFormat.CSHARPCONTRACT) { 719 return "(!(%var1% == 0)) || (%var2% == 0)"; 720 } else { 721 return "(%var1% == 0) ==> (%var2% == 0)"; 722 } 723 } 724 725 @Override 726 public boolean eq_check(long x, long y) { 727 if (x == 0) { 728 return y == 0; 729 } else { 730 return true; 731 } 732 } 733 734 /** Returns a list of non-instantiating suppressions for this invariant. */ 735 @Pure 736 @Override 737 public NISuppressionSet get_ni_suppressions() { 738 if (swap) { 739 return suppressions_swap; 740 } else { 741 return suppressions; 742 } 743 } 744 745 /** definition of this invariant (the suppressee) (unswapped) */ 746 private static NISuppressee suppressee = new NISuppressee(ZeroTrack.class, false); 747 748 private static NISuppressionSet suppressions = 749 new NISuppressionSet( 750 new NISuppression[] { 751 // (var1 == var2) ==> (var1=0 ==> var2=0) 752 new NISuppression(var1_eq_var2, suppressee), 753 // (var1 != 0) ==> (var1=0 ==> var2=0) 754 new NISuppression(var1_ne_0, suppressee), 755 // (var2 == 0) ==> (var1=0 ==> var2=0) 756 new NISuppression(var2_eq_0, suppressee), 757 }); 758 private static NISuppressionSet suppressions_swap = suppressions.swap(); 759 760 } 761 762 /** 763 * Represents the bitwise complement invariant between corresponding elements of two sequences of long. 764 * Prints as {@code x[] = ~y[]}. 765 */ 766 public static class BitwiseComplement extends PairwiseNumericInt { 767 // We are Serializable, so we specify a version to allow changes to 768 // method signatures without breaking serialization. If you add or 769 // remove fields, you should change this number to the current date. 770 static final long serialVersionUID = 20040113L; 771 772 protected BitwiseComplement(PptSlice ppt) { 773 super(ppt, false); 774 } 775 776 protected @Prototype BitwiseComplement() { 777 super(false); 778 } 779 780 private static @Prototype BitwiseComplement proto = new @Prototype BitwiseComplement(); 781 782 /** Returns the prototype invariant. */ 783 public static @Prototype BitwiseComplement get_proto() { 784 return proto; 785 } 786 787 // Variables starting with dkconfig_ should only be set via the 788 // daikon.config.Configuration interface. 789 /** Boolean. True iff bitwise complement invariants should be considered. */ 790 public static boolean dkconfig_enabled = false; 791 792 @Override 793 public boolean enabled() { 794 return dkconfig_enabled; 795 } 796 797 @Override 798 protected BitwiseComplement instantiate_dyn(@Prototype BitwiseComplement this, PptSlice slice) { 799 return new BitwiseComplement(slice); 800 } 801 802 @Pure 803 @Override 804 public boolean is_symmetric() { 805 return true; 806 } 807 808 @Override 809 public String get_format_str(@GuardSatisfied BitwiseComplement this, OutputFormat format) { 810 if (format == OutputFormat.SIMPLIFY) { 811 return "(EQ %var1% (~ %var2%))"; 812 } else { 813 return "%var1% == ~%var2%"; 814 } 815 } 816 817 /** Check to see if x == ~y . */ 818 @Override 819 public boolean eq_check(long x, long y) { 820 return (x == ~y); 821 } 822 } 823 824 /** 825 * Represents the bitwise subset invariant between corresponding elements of two sequences of long; that is, the bits of 826 * {@code y[]} are a subset of the bits of {@code x[]}. 827 * Prints as {@code x[] = y[] | x[]}. 828 */ 829 public static class BitwiseSubset extends PairwiseNumericInt { 830 // We are Serializable, so we specify a version to allow changes to 831 // method signatures without breaking serialization. If you add or 832 // remove fields, you should change this number to the current date. 833 static final long serialVersionUID = 20040113L; 834 835 protected BitwiseSubset(PptSlice ppt, boolean swap) { 836 super(ppt, swap); 837 } 838 839 protected BitwiseSubset(boolean swap) { 840 super(swap); 841 } 842 843 private static @Prototype BitwiseSubset proto = new @Prototype BitwiseSubset(false); 844 private static @Prototype BitwiseSubset proto_swap = new @Prototype BitwiseSubset(true); 845 846 /** Returns the prototype invariant. */ 847 public static @Prototype BitwiseSubset get_proto(boolean swap) { 848 if (swap) { 849 return proto_swap; 850 } else { 851 return proto; 852 } 853 } 854 855 // Variables starting with dkconfig_ should only be set via the 856 // daikon.config.Configuration interface. 857 /** Boolean. True iff bitwise subset invariants should be considered. */ 858 public static boolean dkconfig_enabled = false; 859 860 @Override 861 public boolean enabled() { 862 return dkconfig_enabled; 863 } 864 865 @Override 866 public BitwiseSubset instantiate_dyn(@Prototype BitwiseSubset this, PptSlice slice) { 867 return new BitwiseSubset(slice, swap); 868 } 869 870 @Override 871 public String get_format_str(@GuardSatisfied BitwiseSubset this, OutputFormat format) { 872 if (format == OutputFormat.SIMPLIFY) { 873 return "(EQ %var1% (|java-bitwise-or| %var2% %var1%))"; 874 } else if (format == OutputFormat.DAIKON) { 875 return "%var2% is a bitwise subset of %var1%"; 876 } else { 877 return "%var1% == (%var2% | %var1%)"; 878 } 879 } 880 881 @Override 882 public boolean eq_check(long x, long y) { 883 return (x == (y | x)); 884 } 885 886 /** 887 * This needs to be an obvious check and not a suppression for sequences because there is no 888 * consistent way to check that var1 and var2 have the same length (for derivations). 889 */ 890 @Override 891 public InvDef[][] obvious_checks(VarInfo[] vis) { 892 893 return new InvDef[][] { 894 // suppress if var2 == 0 895 new InvDef[] {new InvDef(var2(), EltOneOf.class, InvDef.elts_zero)}, 896 // suppress if var1 == -1 (all of its bits are on) 897 new InvDef[] {new InvDef(var1(), EltOneOf.class, InvDef.elts_minus_one)} 898 }; 899 } 900 901 /** Returns a list of non-instantiating suppressions for this invariant. */ 902 @Pure 903 @Override 904 public NISuppressionSet get_ni_suppressions() { 905 if (swap) { 906 return suppressions_swap; 907 } else { 908 return suppressions; 909 } 910 } 911 912 /** definition of this invariant (the suppressee) (unswapped) */ 913 private static NISuppressee suppressee = new NISuppressee(BitwiseSubset.class, false); 914 915 private static NISuppressionSet suppressions = 916 new NISuppressionSet( 917 new NISuppression[] { 918 919 // (var1 == var2) ==> var1 = (var2 | var1) 920 new NISuppression(var1_eq_var2, suppressee), 921 922 }); 923 private static NISuppressionSet suppressions_swap = suppressions.swap(); 924 } 925 926 /** 927 * Represents the BitwiseAnd == 0 invariant between corresponding elements of two sequences of long; that is, {@code x[]} and 928 * {@code y[]} have no bits in common. 929 * Prints as {@code x[] & y[] == 0}. 930 */ 931 public static class BitwiseAndZero extends PairwiseNumericInt { 932 // We are Serializable, so we specify a version to allow changes to 933 // method signatures without breaking serialization. If you add or 934 // remove fields, you should change this number to the current date. 935 static final long serialVersionUID = 20040313L; 936 937 protected BitwiseAndZero(PptSlice ppt) { 938 super(ppt, false); 939 } 940 941 protected @Prototype BitwiseAndZero() { 942 super(false); 943 } 944 945 private static @Prototype BitwiseAndZero proto = new @Prototype BitwiseAndZero(); 946 947 /** Returns the prototype invariant. */ 948 public static @Prototype BitwiseAndZero get_proto() { 949 return proto; 950 } 951 952 // Variables starting with dkconfig_ should only be set via the 953 // daikon.config.Configuration interface. 954 /** Boolean. True iff BitwiseAndZero invariants should be considered. */ 955 public static boolean dkconfig_enabled = false; 956 957 @Override 958 public boolean enabled() { 959 return dkconfig_enabled; 960 } 961 962 @Override 963 public BitwiseAndZero instantiate_dyn(@Prototype BitwiseAndZero this, PptSlice slice) { 964 return new BitwiseAndZero(slice); 965 } 966 967 @Override 968 public String get_format_str(@GuardSatisfied BitwiseAndZero this, OutputFormat format) { 969 if (format == OutputFormat.SIMPLIFY) { 970 return "(EQ (|java-&| %var1% %var2%) 0)"; 971 } else { 972 return "(%var1% & %var2%) == 0"; 973 } 974 } 975 976 @Pure 977 @Override 978 public boolean is_symmetric() { 979 return true; 980 } 981 982 @Override 983 public boolean eq_check(long x, long y) { 984 return (x & y) == 0; 985 } 986 987 /** Returns a list of non-instantiating suppressions for this invariant. */ 988 @Pure 989 @Override 990 public @Nullable NISuppressionSet get_ni_suppressions() { 991 return suppressions; 992 } 993 994 private static @Nullable NISuppressionSet suppressions = null; 995 996 } 997 998 /** 999 * Represents the ShiftZero invariant between corresponding elements of two sequences of long; that is, {@code x[]} 1000 * right-shifted by {@code y[]} is always zero. 1001 * Prints as {@code x[] >> y[] = 0}. 1002 */ 1003 public static class ShiftZero extends PairwiseNumericInt { 1004 // We are Serializable, so we specify a version to allow changes to 1005 // method signatures without breaking serialization. If you add or 1006 // remove fields, you should change this number to the current date. 1007 static final long serialVersionUID = 20040313L; 1008 1009 protected ShiftZero(PptSlice ppt, boolean swap) { 1010 super(ppt, swap); 1011 } 1012 1013 protected ShiftZero(boolean swap) { 1014 super(swap); 1015 } 1016 1017 private static @Prototype ShiftZero proto = new @Prototype ShiftZero(false); 1018 private static @Prototype ShiftZero proto_swap = new @Prototype ShiftZero(true); 1019 1020 /** Returns the prototype invariant. */ 1021 public static @Prototype ShiftZero get_proto(boolean swap) { 1022 if (swap) { 1023 return proto_swap; 1024 } else { 1025 return proto; 1026 } 1027 } 1028 1029 // Variables starting with dkconfig_ should only be set via the 1030 // daikon.config.Configuration interface. 1031 /** Boolean. True iff ShiftZero invariants should be considered. */ 1032 public static boolean dkconfig_enabled = false; 1033 1034 @Override 1035 public boolean enabled() { 1036 return dkconfig_enabled; 1037 } 1038 1039 @Override 1040 protected ShiftZero instantiate_dyn(@Prototype ShiftZero this, PptSlice slice) { 1041 return new ShiftZero(slice, swap); 1042 } 1043 1044 @Override 1045 public String get_format_str(@GuardSatisfied ShiftZero this, OutputFormat format) { 1046 if (format == OutputFormat.SIMPLIFY) { 1047 return "(EQ (|java->>| %var1% %var2%) 0)"; 1048 } else { 1049 return "(%var1% >> %var2% == 0)"; 1050 } 1051 } 1052 1053 @Override 1054 public boolean eq_check(long x, long y) { 1055 if ((y < 0) || (y > 63)) { 1056 throw new ArithmeticException("shift op (" + y + ") is out of range"); 1057 } 1058 return (x >> y) == 0; 1059 } 1060 1061 /** Returns a list of non-instantiating suppressions for this invariant. */ 1062 @Pure 1063 @Override 1064 public NISuppressionSet get_ni_suppressions() { 1065 if (swap) { 1066 return suppressions_swap; 1067 } else { 1068 return suppressions; 1069 } 1070 } 1071 1072 /** definition of this invariant (the suppressee) (unswapped) */ 1073 private static NISuppressee suppressee = new NISuppressee(ShiftZero.class, false); 1074 1075 private static NISuppressionSet suppressions = 1076 new NISuppressionSet( 1077 new NISuppression[] { 1078 // (var1>=0) ^ (var1<=var2) ^ (0<=var2<=63) ==> (var1 >> var2) == 0 1079 new NISuppression(var1_ge_0, var1_le_var2, var2_valid_shift, 1080 suppressee), 1081 }); 1082 private static NISuppressionSet suppressions_swap = suppressions.swap(); 1083 } 1084 1085// 1086// Standard String invariants 1087// 1088 1089}