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