001// ***** This file is automatically generated from Numeric.java.jpp 002 003package daikon.inv.binary.twoScalar; 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 NumericFloat extends TwoFloat { 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 NumericFloat(PptSlice ppt, boolean swap) { 042 super(ppt); 043 this.swap = swap; 044 } 045 046 protected NumericFloat(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.isFloat() || !type2.isFloat()) { 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 NumericFloat 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 NumericFloat 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 = var1().name_using(format); 093 String v2 = var2().name_using(format); 094 095 // Note that we do not use String.replaceAll here, because that's 096 // inseparable from the regex library, and we don't want to have to 097 // escape v1 with something like 098 // v1.replaceAll("([\\$\\\\])", "\\\\$1") 099 fmt_str = fmt_str.replace("%var1%", v1); 100 fmt_str = fmt_str.replace("%var2%", v2); 101 102 // if (false && (format == OutputFormat.DAIKON)) { 103 // fmt_str = "[" + getClass() + "]" + fmt_str + " (" 104 // + var1().get_value_info() + ", " + var2().get_value_info() + ")"; 105 // } 106 return fmt_str; 107 } 108 109 /** Calls the function specific equal check and returns the correct status. */ 110 111 @Override 112 public InvariantStatus check_modified(double x, double y, int count) { 113 114 try { 115 if (eq_check(x, y)) { 116 return InvariantStatus.NO_CHANGE; 117 } else { 118 return InvariantStatus.FALSIFIED; 119 } 120 } catch (Exception e) { 121 return InvariantStatus.FALSIFIED; 122 } 123 } 124 125 /** 126 * Checks to see if 'x[a] op y[b]' where 'x[] op y[]' and 'a == b'. Doesn't catch the case where 127 * a = b+1. 128 */ 129 public @Nullable DiscardInfo is_subscript(VarInfo[] vis) { 130 131 VarInfo v1 = var1(vis); 132 VarInfo v2 = var2(vis); 133 134 // Make sure each var is a sequence subscript 135 if (!v1.isDerived() || !(v1.derived instanceof SequenceFloatSubscript)) { 136 return null; 137 } 138 if (!v2.isDerived() || !(v2.derived instanceof SequenceFloatSubscript)) { 139 return null; 140 } 141 142 @NonNull SequenceFloatSubscript der1 = (SequenceFloatSubscript) v1.derived; 143 @NonNull SequenceFloatSubscript der2 = (SequenceFloatSubscript) v2.derived; 144 145 // Make sure the shifts match 146 if (der1.index_shift != der2.index_shift) { 147 return null; 148 } 149 150 // Look for this invariant over a sequence 151 String cstr = getClass().getName(); 152 cstr = cstr.replaceFirst("Numeric", "PairwiseNumeric"); 153 cstr = cstr.replaceFirst("twoScalar", "twoSequence"); 154 cstr = cstr.replaceFirst("twoFloat", "twoSequence"); 155 Class<? extends Invariant> pairwise_class; 156 try { 157 @SuppressWarnings("signature") // string manipulation; application invariants 158 @ClassGetName String cstr_cgn = cstr; 159 pairwise_class = asInvClass(Class.forName(cstr_cgn)); 160 } catch (Exception e) { 161 throw new Error("can't create class for " + cstr, e); 162 } 163 Invariant inv = find(pairwise_class, der1.seqvar(), der2.seqvar()); 164 if (inv == null) { 165 return null; 166 } 167 168 // Look to see if the subscripts are equal 169 Invariant subinv = find(FloatEqual.class, der1.sclvar(), der2.sclvar()); 170 if (subinv == null) { 171 return null; 172 } 173 174 return new DiscardInfo(this, DiscardCode.obvious, "Implied by " 175 + inv.format() + " and " + subinv.format()); 176 } 177 178 @Pure 179 @Override 180 public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) { 181 182 DiscardInfo super_result = super.isObviousDynamically(vis); 183 if (super_result != null) { 184 return super_result; 185 } 186 187 // any relation across subscripts is made obvious by the same 188 // relation across the original sequence if the subscripts are equal 189 DiscardInfo result = is_subscript(vis); 190 if (result != null) { 191 return result; 192 } 193 194 // Check for invariant specific obvious checks. The obvious_checks 195 // method returns an array of arrays of antecedents. If all of the 196 // antecedents in an array are true, then the invariant is obvoius. 197 InvDef[][] obvious_arr = obvious_checks(vis); 198 obvious_loop: 199 for (int i = 0; i < obvious_arr.length; i++) { 200 InvDef[] antecedents = obvious_arr[i]; 201 StringBuilder why = null; 202 for (int j = 0; j < antecedents.length; j++) { 203 Invariant inv = antecedents[j].find(); 204 if (inv == null) { 205 continue obvious_loop; 206 } 207 if (why == null) { 208 why = new StringBuilder(inv.format()); 209 } else { 210 why.append(" and "); 211 why.append(inv.format()); 212 } 213 } 214 return new DiscardInfo(this, DiscardCode.obvious, "Implied by " + why); 215 } 216 217 return null; 218 } 219 220 /** 221 * Return a format string for the specified output format. Each instance of %varN% will be 222 * replaced by the correct name for varN. 223 */ 224 public abstract String get_format_str(@GuardSatisfied NumericFloat this, OutputFormat format); 225 226 /** Returns true if x and y don't invalidate the invariant. */ 227 public abstract boolean eq_check(double x, double y); 228 229 /** 230 * Returns an array of arrays of antecedents. If all of the antecedents in any array are true, 231 * then the invariant is obvious. 232 */ 233 public InvDef[][] obvious_checks(VarInfo[] vis) { 234 return new InvDef[][] {}; 235 } 236 237 public static List<@Prototype Invariant> get_proto_all() { 238 239 List<@Prototype Invariant> result = new ArrayList<>(); 240 241 result.add(Divides.get_proto(false)); 242 result.add(Divides.get_proto(true)); 243 result.add(Square.get_proto(false)); 244 result.add(Square.get_proto(true)); 245 246 result.add(ZeroTrack.get_proto(false)); 247 result.add(ZeroTrack.get_proto(true)); 248 249 // System.out.printf("%s get proto: %s%n", NumericFloat.class, result); 250 return result; 251 } 252 253 // suppressor definitions, used by many of the classes below 254 protected static NISuppressor 255 256 var1_eq_0 = new NISuppressor(0, RangeFloat.EqualZero.class), 257 var2_eq_0 = new NISuppressor(1, RangeFloat.EqualZero.class), 258 var1_ge_0 = new NISuppressor(0, RangeFloat.GreaterEqualZero.class), 259 var2_ge_0 = new NISuppressor(1, RangeFloat.GreaterEqualZero.class), 260 var1_eq_1 = new NISuppressor(0, RangeFloat.EqualOne.class), 261 var2_eq_1 = new NISuppressor(1, RangeFloat.EqualOne.class), 262 var1_eq_minus_1 = new NISuppressor(0, RangeFloat.EqualMinusOne.class), 263 var2_eq_minus_1 = new NISuppressor(1, RangeFloat.EqualMinusOne.class), 264 var1_ne_0 = new NISuppressor(0, NonZeroFloat.class), 265 var2_ne_0 = new NISuppressor(1, NonZeroFloat.class), 266 var1_le_var2 = new NISuppressor(0, 1, FloatLessEqual.class), 267 268 var1_eq_var2 = new NISuppressor(0, 1, FloatEqual.class), 269 var2_eq_var1 = new NISuppressor(0, 1, FloatEqual.class); 270 271 // 272 // Int and Float Numeric Invariants 273 // 274 275 /** 276 * Represents the divides without remainder invariant between two double scalars. 277 * Prints as {@code x % y == 0}. 278 */ 279 public static class Divides extends NumericFloat { 280 // We are Serializable, so we specify a version to allow changes to 281 // method signatures without breaking serialization. If you add or 282 // remove fields, you should change this number to the current date. 283 static final long serialVersionUID = 20040113L; 284 285 protected Divides(PptSlice ppt, boolean swap) { 286 super(ppt, swap); 287 } 288 289 protected Divides(boolean swap) { 290 super(swap); 291 } 292 293 private static @Prototype Divides proto = new @Prototype Divides(false); 294 private static @Prototype Divides proto_swap = new @Prototype Divides(true); 295 296 /** Returns the prototype invariant. */ 297 public static @Prototype NumericFloat get_proto(boolean swap) { 298 if (swap) { 299 return proto_swap; 300 } else { 301 return proto; 302 } 303 } 304 305 // Variables starting with dkconfig_ should only be set via the 306 // daikon.config.Configuration interface. 307 /** Boolean. True iff divides invariants should be considered. */ 308 public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault; 309 310 /** Returns whether or not this invariant is enabled. */ 311 @Override 312 public boolean enabled() { 313 return dkconfig_enabled; 314 } 315 316 @Override 317 protected Divides instantiate_dyn(@Prototype Divides this, PptSlice slice) { 318 return new Divides(slice, swap); 319 } 320 321 @Override 322 public String get_format_str(@GuardSatisfied Divides this, OutputFormat format) { 323 if (format == OutputFormat.SIMPLIFY) { 324 return "(EQ 0 (MOD %var1% %var2%))"; 325 } else if (format == OutputFormat.CSHARPCONTRACT) { 326 return "%var1% % %var2% == 0"; 327 } else if (format.isJavaFamily()) { 328 return "daikon.Quant.fuzzy.eq(%var1% % %var2%, 0)"; 329 } else { 330 return "%var1% % %var2% == 0"; 331 } 332 } 333 334 @Override 335 public boolean eq_check(double x, double y) { 336 return Global.fuzzy.eq(0, (x % y)); 337 } 338 339 /** Returns a list of non-instantiating suppressions for this invariant. */ 340 @Pure 341 @Override 342 public NISuppressionSet get_ni_suppressions() { 343 if (swap) { 344 return suppressions_swap; 345 } else { 346 return suppressions; 347 } 348 } 349 350 /** definition of this invariant (the suppressee) (unswapped) */ 351 private static NISuppressee suppressee = new NISuppressee(Divides.class, false); 352 353 private static NISuppressionSet suppressions = 354 new NISuppressionSet( 355 new NISuppression[] { 356 357 // These suppressions are only valid on scalars because the length 358 // of var1 and var2 must also be the same and there is no suppressor 359 // for that. 360 361 // var2 == 1 ==> var1 % var2 == 0 362 new NISuppression(var2_eq_1, suppressee), 363 364 // var2 == -1 ==> var1 % var2 == 0 365 new NISuppression(var2_eq_minus_1, suppressee), 366 367 // (var1 == 0) ^ (var2 != 0) ==> var1 % var2 == 0 368 new NISuppression(var1_eq_0, var2_ne_0, suppressee), 369 370 // (var1 == var2) ^ (var2 != 0) ==> var1 % var2 == 0 371 new NISuppression(var1_eq_var2, var2_ne_0, suppressee), 372 373 // (var2 == var1) ^ (var1 != 0) ==> var2 % var1 == 0 374 new NISuppression(var2_eq_var1, var1_ne_0, suppressee), 375 376 }); 377 private static NISuppressionSet suppressions_swap = suppressions.swap(); 378 379 /** 380 * Returns non-null if this invariant is obvious from an existing, non-falsified linear binary 381 * invariant in the same slice as this invariant. This invariant of the form "x % y == 0" is 382 * falsified if a linear binary invariant is found of the form "a*y - 1*x + 0 == 0" 383 * 384 * @return non-null value iff this invariant is obvious from other invariants in the same slice 385 */ 386 @Pure 387 @Override 388 public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) { 389 // First call super type's method, and if it returns non-null, then 390 // this invariant is already known to be obvious, so just return 391 // whatever reason the super type returned. 392 DiscardInfo di = super.isObviousDynamically(vis); 393 if (di != null) { 394 return di; 395 } 396 397 VarInfo var1 = vis[0]; 398 VarInfo var2 = vis[1]; 399 400 // ensure that var1.varinfo_index <= var2.varinfo_index 401 if (var1.varinfo_index > var2.varinfo_index) { 402 var1 = vis[1]; 403 var2 = vis[0]; 404 } 405 406 // Find slice corresponding to these two variables. 407 // Ideally, this should always just be ppt if all 408 // falsified invariants have been removed. 409 PptSlice2 ppt2 = ppt.parent.findSlice(var1,var2); 410 411 // If no slice is found , no invariants exist to make this one obvious. 412 if (ppt2 == null) { 413 return null; 414 } 415 416 // For each invariant, check to see if it's a linear binary 417 // invariant of the form "a*y - 1*x + 0 == 0" and if so, 418 // you know this invariant of the form "x % y == 0" is obvious. 419 for(Invariant inv : ppt2.invs) { 420 421 if (inv instanceof LinearBinaryFloat) { 422 LinearBinaryFloat linv = (LinearBinaryFloat) inv; 423 424 // General form for linear binary: a*x + b*y + c == 0, 425 // but a and b can be switched with respect to vis, and either 426 // one may be negative, so instead check: 427 // - c == 0 428 // - a*b < 0 (a and b have different signs) 429 // - |a| == 1 or |b| == 1, so one will divide the other 430 // While this means that both x % y == 0 and y % x == 0, 431 // only one of these invariants will still be true at this 432 // time, and only that one will be falsified by this test. 433 if (!linv.is_false() 434 && Global.fuzzy.eq(linv.core.c, 0) 435 && linv.core.b * linv.core.a < 0 436 && (Global.fuzzy.eq(linv.core.a * linv.core.a, 1) 437 || Global.fuzzy.eq(linv.core.b * linv.core.b, 1))) { 438 return new DiscardInfo(this, DiscardCode.obvious, 439 "Linear binary invariant implies divides"); 440 } 441 } 442 } 443 444 return null; 445 } 446 447 } 448 449 /** 450 * Represents the square invariant between two double scalars. 451 * Prints as {@code x = y**2}. 452 */ 453 public static class Square extends NumericFloat { 454 // We are Serializable, so we specify a version to allow changes to 455 // method signatures without breaking serialization. If you add or 456 // remove fields, you should change this number to the current date. 457 static final long serialVersionUID = 20040113L; 458 459 protected Square(PptSlice ppt, boolean swap) { 460 super(ppt, swap); 461 } 462 463 protected Square(boolean swap) { 464 super(swap); 465 } 466 467 private static @Prototype Square proto = new @Prototype Square(false); 468 private static @Prototype Square proto_swap = new @Prototype Square(true); 469 470 /** Returns the prototype invariant. */ 471 public static @Prototype Square get_proto(boolean swap) { 472 if (swap) { 473 return proto_swap; 474 } else { 475 return proto; 476 } 477 } 478 479 // Variables starting with dkconfig_ should only be set via the 480 // daikon.config.Configuration interface. 481 /** Boolean. True iff square invariants should be considered. */ 482 public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault; 483 484 /** Returns whether or not this invariant is enabled. */ 485 @Override 486 public boolean enabled() { 487 return dkconfig_enabled; 488 } 489 @Override 490 protected Square instantiate_dyn(@Prototype Square this, PptSlice slice) { 491 return new Square(slice, swap); 492 } 493 494 @Override 495 public String get_format_str(@GuardSatisfied Square this, OutputFormat format) { 496 if (format == OutputFormat.SIMPLIFY) { 497 return "(EQ %var1% (* %var2% %var2))"; 498 } else if (format == OutputFormat.CSHARPCONTRACT) { 499 return "%var1% == %var2%*%var2%"; 500 } else if (format.isJavaFamily()) { 501 502 return "daikon.Quant.fuzzy.eq(%var1%, %var2%*%var2%)"; 503 } else { 504 return "%var1% == %var2%**2"; 505 } 506 } 507 508 /** Check to see if x == y squared. */ 509 @Override 510 public boolean eq_check(double x, double y) { 511 return Global.fuzzy.eq(x, y*y); 512 } 513 514 // Note there are no NI Suppressions for Square. Two obvious 515 // suppressions are: 516 // 517 // (var2 == 1) ^ (var1 == 1) ==> var1 = var2*var2 518 // (var2 == 0) ^ (var1 == 0) ==> var1 = var2*var2 519 // 520 // But all of the antecedents would be constants, so we would 521 // never need to create this slice, so there is no reason to create 522 // these. 523 524 } 525 526 /** 527 * Represents the zero tracks invariant between 528 * two double scalars; that is, when {@code x} is zero, 529 * {@code y} is also zero. 530 * Prints as {@code x = 0 => y = 0}. 531 */ 532 public static class ZeroTrack extends NumericFloat { 533 // We are Serializable, so we specify a version to allow changes to 534 // method signatures without breaking serialization. If you add or 535 // remove fields, you should change this number to the current date. 536 static final long serialVersionUID = 20040313L; 537 538 protected ZeroTrack(PptSlice ppt, boolean swap) { 539 super(ppt, swap); 540 } 541 542 protected @Prototype ZeroTrack(boolean swap) { 543 super(swap); 544 } 545 546 private static @Prototype ZeroTrack proto = new @Prototype ZeroTrack(false); 547 private static @Prototype ZeroTrack proto_swap = new @Prototype ZeroTrack(true); 548 549 /** Returns the prototype invariant. */ 550 public static @Prototype ZeroTrack get_proto(boolean swap) { 551 if (swap) { 552 return proto_swap; 553 } else { 554 return proto; 555 } 556 } 557 558 // Variables starting with dkconfig_ should only be set via the 559 // daikon.config.Configuration interface. 560 /** Boolean. True iff zero-track invariants should be considered. */ 561 public static boolean dkconfig_enabled = false; 562 563 /** Returns whether or not this invariant is enabled. */ 564 @Override 565 public boolean enabled() { 566 return dkconfig_enabled; 567 } 568 569 @Override 570 protected ZeroTrack instantiate_dyn(@Prototype ZeroTrack this, PptSlice slice) { 571 return new ZeroTrack(slice, swap); 572 } 573 574 @Override 575 public String get_format_str(@GuardSatisfied ZeroTrack this, OutputFormat format) { 576 if (format == OutputFormat.SIMPLIFY) { 577 return "(IMPLIES (EQ %var1% 0) (EQ %var2% 0))"; 578 } else if (format.isJavaFamily() || format == OutputFormat.CSHARPCONTRACT) { 579 return "(!(%var1% == 0)) || (%var2% == 0)"; 580 } else { 581 return "(%var1% == 0) ==> (%var2% == 0)"; 582 } 583 } 584 585 @Override 586 public boolean eq_check(double x, double y) { 587 if (x == 0) { 588 return y == 0; 589 } else { 590 return true; 591 } 592 } 593 594 /** Returns a list of non-instantiating suppressions for this invariant. */ 595 @Pure 596 @Override 597 public NISuppressionSet get_ni_suppressions() { 598 if (swap) { 599 return suppressions_swap; 600 } else { 601 return suppressions; 602 } 603 } 604 605 /** definition of this invariant (the suppressee) (unswapped) */ 606 private static NISuppressee suppressee = new NISuppressee(ZeroTrack.class, false); 607 608 private static NISuppressionSet suppressions = 609 new NISuppressionSet( 610 new NISuppression[] { 611 // (var1 == var2) ==> (var1=0 ==> var2=0) 612 new NISuppression(var1_eq_var2, suppressee), 613 // (var1 != 0) ==> (var1=0 ==> var2=0) 614 new NISuppression(var1_ne_0, suppressee), 615 // (var2 == 0) ==> (var1=0 ==> var2=0) 616 new NISuppression(var2_eq_0, suppressee), 617 }); 618 private static NISuppressionSet suppressions_swap = suppressions.swap(); 619 620 } 621 622// 623// Standard String invariants 624// 625 626}