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