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 PairwiseNumericFloat extends TwoSequenceFloat { 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 PairwiseNumericFloat(PptSlice ppt, boolean swap) { 042 super(ppt); 043 this.swap = swap; 044 } 045 046 protected PairwiseNumericFloat(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.baseIsFloat() || !type2.baseIsFloat()) { 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 PairwiseNumericFloat 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 PairwiseNumericFloat 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 { 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 { 117 return format_unimplemented(format); 118 } 119 120 } 121 122 if (format == OutputFormat.ESCJAVA) { 123 String[] form = VarInfo.esc_quantify(var1(), var2()); 124 fmt_str = form[0] + "(" + fmt_str + ")" + form[3]; 125 v1 = form[1]; 126 v2 = form[2]; 127 } else if (format == OutputFormat.SIMPLIFY) { 128 String[] form = VarInfo.simplify_quantify(QuantFlags.element_wise(), 129 var1(), var2()); 130 fmt_str = form[0] + " " + fmt_str + " " + form[3]; 131 v1 = form[1]; 132 v2 = form[2]; 133 } else { 134 v1 = var1().name_using(format); 135 v2 = var2().name_using(format); 136 if (format == OutputFormat.DAIKON) { 137 fmt_str += " (elementwise)"; 138 } 139 } 140 141 // Note that we do not use String.replaceAll here, because that's 142 // inseparable from the regex library, and we don't want to have to 143 // escape v1 with something like 144 // v1.replaceAll("([\\$\\\\])", "\\\\$1") 145 fmt_str = fmt_str.replace("%var1%", v1); 146 fmt_str = fmt_str.replace("%var2%", v2); 147 148 // if (false && (format == OutputFormat.DAIKON)) { 149 // fmt_str = "[" + getClass() + "]" + fmt_str + " (" 150 // + var1().get_value_info() + ", " + var2().get_value_info() + ")"; 151 // } 152 return fmt_str; 153 } 154 155 /** Calls the function specific equal check and returns the correct status. */ 156 157 @Override 158 public InvariantStatus check_modified(double[] x, double[] y, 159 int count) { 160 if (x.length != y.length) { 161 if (Debug.logOn()) { 162 log("Falsified - x length = %s y length = %s", x.length, y.length); 163 } 164 return InvariantStatus.FALSIFIED; 165 } 166 167 if (Debug.logDetail()) { 168 log("testing values %s, %s", Arrays.toString (x), 169 Arrays.toString(y)); 170 } 171 172 try { 173 for (int i = 0; i < x.length; i++) { 174 if (!eq_check(x[i], y[i])) { 175 if (Debug.logOn()) { 176 log("Falsified - x[%s]=%s y[%s]=%s", i, x[i], i, y[i]); 177 } 178 return InvariantStatus.FALSIFIED; 179 } 180 } 181 return InvariantStatus.NO_CHANGE; 182 } catch (Exception e) { 183 if (Debug.logOn()) { 184 log("Falsified - exception %s", e); 185 } 186 return InvariantStatus.FALSIFIED; 187 } 188 } 189 190 /** 191 * Checks to see if this invariant is over subsequences and if the same relationship holds over 192 * the full sequence. This is obvious if it does. For example 'x[foo..] op y[bar..]' would be 193 * obvious if 'x[] op y[]' This can't fully be handled as a suppression since a suppression needs 194 * to insure that foo == bar as well. But that is not a requirement here (the fact that 'x[] op 195 * y[]' implies that foo == bar when x[] and y[] are not missing). 196 */ 197 public @Nullable DiscardInfo is_subsequence(VarInfo[] vis) { 198 199 VarInfo v1 = var1(vis); 200 VarInfo v2 = var2(vis); 201 202 // Make sure each var is a sequence subsequence 203 if (!v1.isDerived() || !(v1.derived instanceof SequenceFloatSubsequence)) { 204 return null; 205 } 206 if (!v2.isDerived() || !(v2.derived instanceof SequenceFloatSubsequence)) { 207 return null; 208 } 209 210 @NonNull SequenceFloatSubsequence der1 = (SequenceFloatSubsequence) v1.derived; 211 @NonNull SequenceFloatSubsequence der2 = (SequenceFloatSubsequence) v2.derived; 212 213 // Both of the indices must be either from the start or up to the end. 214 // It is not necessary to check that they match in any other way since 215 // if the supersequence holds, that implies that the sequences are 216 // of the same length. Thus any subsequence that starts from the 217 // beginning or finishes at the end must end or start at the same 218 // spot (or it would have been falsified when it didn't) 219 if (der1.from_start != der2.from_start) { 220 return null; 221 } 222 223 // Look up this class over the sequence variables 224 Invariant inv = find(getClass(), der1.seqvar(), der2.seqvar()); 225 if (inv == null) { 226 return null; 227 } 228 return new DiscardInfo(this, DiscardCode.obvious, "Implied by " 229 + inv.format()); 230 } 231 232 @Pure 233 @Override 234 public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) { 235 236 DiscardInfo super_result = super.isObviousDynamically(vis); 237 if (super_result != null) { 238 return super_result; 239 } 240 241 // any elementwise relation across subsequences is made obvious by 242 // the same relation across the original sequence 243 DiscardInfo result = is_subsequence(vis); 244 if (result != null) { 245 return result; 246 } 247 248 // Check for invariant specific obvious checks. The obvious_checks 249 // method returns an array of arrays of antecedents. If all of the 250 // antecedents in an array are true, then the invariant is obvoius. 251 InvDef[][] obvious_arr = obvious_checks(vis); 252 obvious_loop: 253 for (int i = 0; i < obvious_arr.length; i++) { 254 InvDef[] antecedents = obvious_arr[i]; 255 StringBuilder why = null; 256 for (int j = 0; j < antecedents.length; j++) { 257 Invariant inv = antecedents[j].find(); 258 if (inv == null) { 259 continue obvious_loop; 260 } 261 if (why == null) { 262 why = new StringBuilder(inv.format()); 263 } else { 264 why.append(" and "); 265 why.append(inv.format()); 266 } 267 } 268 return new DiscardInfo(this, DiscardCode.obvious, "Implied by " + why); 269 } 270 271 return null; 272 } 273 274 /** 275 * Returns an invariant that is true when the size(v1) == size(v2). There are a number of 276 * possible cases for an array: 277 * 278 * <pre> 279 * x[] - entire array, size usually available as size(x[]) 280 * x[..(n-1)] - size is n 281 * x[..n] - size is n+1 282 * x[n..] - size is size(x[]) - n 283 * x[(n+1)..] - size is size(x[]) - (n+1) 284 * </pre> 285 * 286 * Each combination of the above must be considered in creating the equality invariant. Not all 287 * possibilities can be handled. Null is returned in that case. In the following table, s stands 288 * for the size 289 * 290 * <pre> 291 * x[] x[..(n-1)] x[..n] x[n..] x[(n+1)..] 292 * --------- ---------- ------ ------ ---------- 293 * y[] s(y)=s(x) s(y)=n 294 * y[..(m-1)] x m=n 295 * y[..m] x x m=n 296 * y[m..] x x x m=n ∧ 297 * s(y)=s(x) 298 * y[(m+1)..] x x x x m=n ∧ 299 * s(y)=s(x) 300 * </pre> 301 * NOTE: this is not currently used. Many (if not all) of the missing table cells above could be 302 * filled in with linear binary invariants (eg, m = n + 1). 303 */ 304 public @Nullable InvDef array_sizes_eq(VarInfo v1, VarInfo v2) { 305 306 VarInfo v1_size = get_array_size(v1); 307 VarInfo v2_size = get_array_size(v2); 308 309 // If we can find a size variable for each side build the invariant 310 if ((v1_size != null) && (v2_size != null)) { 311 return new InvDef(v1_size, v2_size, IntEqual.class); 312 } 313 314 // If either variable is not derived, there is no possible invariant 315 // (since we covered all of the direct size comparisons above) 316 if ((v1.derived == null) || (v2.derived == null)) { 317 return null; 318 } 319 320 // Get the sequence subsequence derivations 321 SequenceFloatSubsequence v1_ss = (SequenceFloatSubsequence) v1.derived; 322 SequenceFloatSubsequence v2_ss = (SequenceFloatSubsequence) v2.derived; 323 324 // If both are from_start and have the same index_shift, just compare 325 // the variables 326 if (v1_ss.from_start && v2_ss.from_start 327 && (v1_ss.index_shift == v2_ss.index_shift)) { 328 return new InvDef(v1_ss.sclvar(), v2_ss.sclvar(), IntEqual.class); 329 } 330 331 return null; 332 } 333 334 /** 335 * Returns a variable that corresponds to the size of v. Returns null if no such variable exists. 336 * 337 * There are two cases that are not handled: x[..n] with an index shift and x[n..]. 338 */ 339 public @Nullable VarInfo get_array_size(VarInfo v) { 340 341 assert v.rep_type.isArray(); 342 343 if (v.derived == null) { 344 return v.sequenceSize(); 345 } else if (v.derived instanceof SequenceFloatSubsequence) { 346 SequenceFloatSubsequence ss = (SequenceFloatSubsequence) v.derived; 347 if (ss.from_start && (ss.index_shift == -1)) { 348 return ss.sclvar(); 349 } 350 } 351 352 return null; 353 } 354 355 /** 356 * Return a format string for the specified output format. Each instance of %varN% will be 357 * replaced by the correct name for varN. 358 */ 359 public abstract String get_format_str(@GuardSatisfied PairwiseNumericFloat this, OutputFormat format); 360 361 /** Returns true if x and y don't invalidate the invariant. */ 362 public abstract boolean eq_check(double x, double y); 363 364 /** 365 * Returns an array of arrays of antecedents. If all of the antecedents in any array are true, 366 * then the invariant is obvious. 367 */ 368 public InvDef[][] obvious_checks(VarInfo[] vis) { 369 return new InvDef[][] {}; 370 } 371 372 public static List<@Prototype Invariant> get_proto_all() { 373 374 List<@Prototype Invariant> result = new ArrayList<>(); 375 376 result.add(Divides.get_proto(false)); 377 result.add(Divides.get_proto(true)); 378 result.add(Square.get_proto(false)); 379 result.add(Square.get_proto(true)); 380 381 // System.out.printf("%s get proto: %s%n", PairwiseNumericFloat.class, result); 382 return result; 383 } 384 385 // suppressor definitions, used by many of the classes below 386 protected static NISuppressor 387 388 var1_eq_0 = new NISuppressor(0, EltRangeFloat.EqualZero.class), 389 var2_eq_0 = new NISuppressor(1, EltRangeFloat.EqualZero.class), 390 var1_ge_0 = new NISuppressor(0, EltRangeFloat.GreaterEqualZero.class), 391 var2_ge_0 = new NISuppressor(1, EltRangeFloat.GreaterEqualZero.class), 392 var1_eq_1 = new NISuppressor(0, EltRangeFloat.EqualOne.class), 393 var2_eq_1 = new NISuppressor(1, EltRangeFloat.EqualOne.class), 394 var1_eq_minus_1 = new NISuppressor(0, EltRangeFloat.EqualMinusOne.class), 395 var2_eq_minus_1 = new NISuppressor(1, EltRangeFloat.EqualMinusOne.class), 396 var1_ne_0 = new NISuppressor(0, EltNonZeroFloat.class), 397 var2_ne_0 = new NISuppressor(1, EltNonZeroFloat.class), 398 var1_le_var2 = new NISuppressor(0, 1, PairwiseFloatLessEqual.class), 399 400 var1_eq_var2 = new NISuppressor(0, 1, PairwiseFloatEqual.class), 401 var2_eq_var1 = new NISuppressor(0, 1, PairwiseFloatEqual.class); 402 403 // 404 // Int and Float Numeric Invariants 405 // 406 407 /** 408 * Represents the divides without remainder invariant between corresponding elements of two sequences of double. 409 * Prints as {@code x[] % y[] == 0}. 410 */ 411 public static class Divides extends PairwiseNumericFloat { 412 // We are Serializable, so we specify a version to allow changes to 413 // method signatures without breaking serialization. If you add or 414 // remove fields, you should change this number to the current date. 415 static final long serialVersionUID = 20040113L; 416 417 protected Divides(PptSlice ppt, boolean swap) { 418 super(ppt, swap); 419 } 420 421 protected Divides(boolean swap) { 422 super(swap); 423 } 424 425 private static @Prototype Divides proto = new @Prototype Divides(false); 426 private static @Prototype Divides proto_swap = new @Prototype Divides(true); 427 428 /** Returns the prototype invariant. */ 429 public static @Prototype PairwiseNumericFloat get_proto(boolean swap) { 430 if (swap) { 431 return proto_swap; 432 } else { 433 return proto; 434 } 435 } 436 437 // Variables starting with dkconfig_ should only be set via the 438 // daikon.config.Configuration interface. 439 /** Boolean. True iff divides invariants should be considered. */ 440 public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault; 441 442 /** Returns whether or not this invariant is enabled. */ 443 @Override 444 public boolean enabled() { 445 return dkconfig_enabled; 446 } 447 448 @Override 449 protected Divides instantiate_dyn(@Prototype Divides this, PptSlice slice) { 450 return new Divides(slice, swap); 451 } 452 453 @Override 454 public String get_format_str(@GuardSatisfied Divides this, OutputFormat format) { 455 if (format == OutputFormat.SIMPLIFY) { 456 return "(EQ 0 (MOD %var1% %var2%))"; 457 } else if (format == OutputFormat.CSHARPCONTRACT) { 458 return "%var1% % %var2% == 0"; 459 } else { 460 return "%var1% % %var2% == 0"; 461 } 462 } 463 464 @Override 465 public boolean eq_check(double x, double y) { 466 return Global.fuzzy.eq(0, (x % y)); 467 } 468 469 /** 470 * This needs to be an obvious check and not a suppression for sequences because there is no 471 * consistent way to check that var1 and var2 have the same length (for derivations). 472 */ 473 @Override 474 public InvDef[][] obvious_checks(VarInfo[] vis) { 475 476 return new InvDef[][] { 477 new InvDef[] { 478 new InvDef(var2(vis), EltOneOfFloat.class, InvDef.elts_minus_one_and_plus_one_float) 479 }, 480 new InvDef[] { 481 new InvDef(var1(), EltOneOfFloat.class, InvDef.elts_zero_float) 482 } 483 }; 484 } 485 486 /** Returns a list of non-instantiating suppressions for this invariant. */ 487 @Pure 488 @Override 489 public NISuppressionSet get_ni_suppressions() { 490 if (swap) { 491 return suppressions_swap; 492 } else { 493 return suppressions; 494 } 495 } 496 497 /** definition of this invariant (the suppressee) (unswapped) */ 498 private static NISuppressee suppressee = new NISuppressee(Divides.class, false); 499 500 private static NISuppressionSet suppressions = 501 new NISuppressionSet( 502 new NISuppression[] { 503 504 // (var1 == var2) ^ (var2 != 0) ==> var1 % var2 == 0 505 new NISuppression(var1_eq_var2, var2_ne_0, suppressee), 506 507 // (var2 == var1) ^ (var1 != 0) ==> var2 % var1 == 0 508 new NISuppression(var2_eq_var1, var1_ne_0, suppressee), 509 510 }); 511 private static NISuppressionSet suppressions_swap = suppressions.swap(); 512 513 /** 514 * Returns non-null if this invariant is obvious from an existing, non-falsified linear binary 515 * invariant in the same slice as this invariant. This invariant of the form "x % y == 0" is 516 * falsified if a linear binary invariant is found of the form "a*y - 1*x + 0 == 0" 517 * 518 * @return non-null value iff this invariant is obvious from other invariants in the same slice 519 */ 520 @Pure 521 @Override 522 public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) { 523 // First call super type's method, and if it returns non-null, then 524 // this invariant is already known to be obvious, so just return 525 // whatever reason the super type returned. 526 DiscardInfo di = super.isObviousDynamically(vis); 527 if (di != null) { 528 return di; 529 } 530 531 VarInfo var1 = vis[0]; 532 VarInfo var2 = vis[1]; 533 534 // ensure that var1.varinfo_index <= var2.varinfo_index 535 if (var1.varinfo_index > var2.varinfo_index) { 536 var1 = vis[1]; 537 var2 = vis[0]; 538 } 539 540 // Find slice corresponding to these two variables. 541 // Ideally, this should always just be ppt if all 542 // falsified invariants have been removed. 543 PptSlice2 ppt2 = ppt.parent.findSlice(var1,var2); 544 545 // If no slice is found , no invariants exist to make this one obvious. 546 if (ppt2 == null) { 547 return null; 548 } 549 550 // For each invariant, check to see if it's a linear binary 551 // invariant of the form "a*y - 1*x + 0 == 0" and if so, 552 // you know this invariant of the form "x % y == 0" is obvious. 553 for(Invariant inv : ppt2.invs) { 554 555 if (inv instanceof LinearBinary) { 556 LinearBinary linv = (LinearBinary) inv; 557 558 // General form for linear binary: a*x + b*y + c == 0, 559 // but a and b can be switched with respect to vis, and either 560 // one may be negative, so instead check: 561 // - c == 0 562 // - a*b < 0 (a and b have different signs) 563 // - |a| == 1 or |b| == 1, so one will divide the other 564 // While this means that both x % y == 0 and y % x == 0, 565 // only one of these invariants will still be true at this 566 // time, and only that one will be falsified by this test. 567 if (!linv.is_false() 568 && Global.fuzzy.eq(linv.core.c, 0) 569 && linv.core.b * linv.core.a < 0 570 && (Global.fuzzy.eq(linv.core.a * linv.core.a, 1) 571 || Global.fuzzy.eq(linv.core.b * linv.core.b, 1))) { 572 return new DiscardInfo(this, DiscardCode.obvious, 573 "Linear binary invariant implies divides"); 574 } 575 } 576 } 577 578 return null; 579 } 580 581 } 582 583 /** 584 * Represents the square invariant between corresponding elements of two sequences of double. 585 * Prints as {@code x[] = y[]**2}. 586 */ 587 public static class Square extends PairwiseNumericFloat { 588 // We are Serializable, so we specify a version to allow changes to 589 // method signatures without breaking serialization. If you add or 590 // remove fields, you should change this number to the current date. 591 static final long serialVersionUID = 20040113L; 592 593 protected Square(PptSlice ppt, boolean swap) { 594 super(ppt, swap); 595 } 596 597 protected Square(boolean swap) { 598 super(swap); 599 } 600 601 private static @Prototype Square proto = new @Prototype Square(false); 602 private static @Prototype Square proto_swap = new @Prototype Square(true); 603 604 /** Returns the prototype invariant. */ 605 public static @Prototype Square get_proto(boolean swap) { 606 if (swap) { 607 return proto_swap; 608 } else { 609 return proto; 610 } 611 } 612 613 // Variables starting with dkconfig_ should only be set via the 614 // daikon.config.Configuration interface. 615 /** Boolean. True iff square invariants should be considered. */ 616 public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault; 617 618 /** Returns whether or not this invariant is enabled. */ 619 @Override 620 public boolean enabled() { 621 return dkconfig_enabled; 622 } 623 @Override 624 protected Square instantiate_dyn(@Prototype Square this, PptSlice slice) { 625 return new Square(slice, swap); 626 } 627 628 @Override 629 public String get_format_str(@GuardSatisfied Square this, OutputFormat format) { 630 if (format == OutputFormat.SIMPLIFY) { 631 return "(EQ %var1% (* %var2% %var2))"; 632 } else if (format == OutputFormat.CSHARPCONTRACT) { 633 return "%var1% == %var2%*%var2%"; 634 } else if (format.isJavaFamily()) { 635 636 return "%var1% == %var2%*%var2%"; 637 } else { 638 return "%var1% == %var2%**2"; 639 } 640 } 641 642 /** Check to see if x == y squared. */ 643 @Override 644 public boolean eq_check(double x, double y) { 645 return Global.fuzzy.eq(x, y*y); 646 } 647 648 // Note there are no NI Suppressions for Square. Two obvious 649 // suppressions are: 650 // 651 // (var2 == 1) ^ (var1 == 1) ==> var1 = var2*var2 652 // (var2 == 0) ^ (var1 == 0) ==> var1 = var2*var2 653 // 654 // But all of the antecedents would be constants, so we would 655 // never need to create this slice, so there is no reason to create 656 // these. 657 658 } 659 660 /** 661 * Represents the zero tracks invariant between 662 * corresponding elements of two sequences of double; that is, when {@code x[]} is zero, 663 * {@code y[]} is also zero. 664 * Prints as {@code x[] = 0 => y[] = 0}. 665 */ 666 public static class ZeroTrack extends PairwiseNumericFloat { 667 // We are Serializable, so we specify a version to allow changes to 668 // method signatures without breaking serialization. If you add or 669 // remove fields, you should change this number to the current date. 670 static final long serialVersionUID = 20040313L; 671 672 protected ZeroTrack(PptSlice ppt, boolean swap) { 673 super(ppt, swap); 674 } 675 676 protected @Prototype ZeroTrack(boolean swap) { 677 super(swap); 678 } 679 680 private static @Prototype ZeroTrack proto = new @Prototype ZeroTrack(false); 681 private static @Prototype ZeroTrack proto_swap = new @Prototype ZeroTrack(true); 682 683 /** Returns the prototype invariant. */ 684 public static @Prototype ZeroTrack get_proto(boolean swap) { 685 if (swap) { 686 return proto_swap; 687 } else { 688 return proto; 689 } 690 } 691 692 // Variables starting with dkconfig_ should only be set via the 693 // daikon.config.Configuration interface. 694 /** Boolean. True iff zero-track invariants should be considered. */ 695 public static boolean dkconfig_enabled = false; 696 697 /** Returns whether or not this invariant is enabled. */ 698 @Override 699 public boolean enabled() { 700 return dkconfig_enabled; 701 } 702 703 @Override 704 protected ZeroTrack instantiate_dyn(@Prototype ZeroTrack this, PptSlice slice) { 705 return new ZeroTrack(slice, swap); 706 } 707 708 @Override 709 public String get_format_str(@GuardSatisfied ZeroTrack this, OutputFormat format) { 710 if (format == OutputFormat.SIMPLIFY) { 711 return "(IMPLIES (EQ %var1% 0) (EQ %var2% 0))"; 712 } else if (format.isJavaFamily() || format == OutputFormat.CSHARPCONTRACT) { 713 return "(!(%var1% == 0)) || (%var2% == 0)"; 714 } else { 715 return "(%var1% == 0) ==> (%var2% == 0)"; 716 } 717 } 718 719 @Override 720 public boolean eq_check(double x, double y) { 721 if (x == 0) { 722 return y == 0; 723 } else { 724 return true; 725 } 726 } 727 728 /** Returns a list of non-instantiating suppressions for this invariant. */ 729 @Pure 730 @Override 731 public NISuppressionSet get_ni_suppressions() { 732 if (swap) { 733 return suppressions_swap; 734 } else { 735 return suppressions; 736 } 737 } 738 739 /** definition of this invariant (the suppressee) (unswapped) */ 740 private static NISuppressee suppressee = new NISuppressee(ZeroTrack.class, false); 741 742 private static NISuppressionSet suppressions = 743 new NISuppressionSet( 744 new NISuppression[] { 745 // (var1 == var2) ==> (var1=0 ==> var2=0) 746 new NISuppression(var1_eq_var2, suppressee), 747 // (var1 != 0) ==> (var1=0 ==> var2=0) 748 new NISuppression(var1_ne_0, suppressee), 749 // (var2 == 0) ==> (var1=0 ==> var2=0) 750 new NISuppression(var2_eq_0, suppressee), 751 }); 752 private static NISuppressionSet suppressions_swap = suppressions.swap(); 753 754 } 755 756// 757// Standard String invariants 758// 759 760}