001// ***** This file is automatically generated from IntComparisons.java.jpp 002 003package daikon.inv.binary.twoScalar; 004 005import daikon.*; 006import daikon.derive.binary.*; 007import daikon.derive.unary.*; 008import daikon.inv.*; 009import daikon.inv.binary.twoScalar.*; 010import daikon.inv.binary.twoSequence.*; 011import daikon.inv.unary.scalar.*; 012import daikon.inv.unary.sequence.*; 013import daikon.inv.unary.string.*; 014import daikon.suppress.*; 015import java.util.*; 016import java.util.logging.Level; 017import java.util.logging.Logger; 018import org.checkerframework.checker.interning.qual.Interned; 019import org.checkerframework.checker.lock.qual.GuardSatisfied; 020import org.checkerframework.checker.nullness.qual.NonNull; 021import org.checkerframework.checker.nullness.qual.Nullable; 022import org.checkerframework.dataflow.qual.Pure; 023import org.checkerframework.dataflow.qual.SideEffectFree; 024import org.plumelib.util.Intern; 025import typequals.prototype.qual.NonPrototype; 026import typequals.prototype.qual.Prototype; 027 028/** 029 * Represents an invariant of == between two double scalars. Prints as {@code x == y}. 030 */ 031public final class FloatEqual extends TwoFloat implements EqualityComparison { 032 033 // We are Serializable, so we specify a version to allow changes to 034 // method signatures without breaking serialization. If you add or 035 // remove fields, you should change this number to the current date. 036 static final long serialVersionUID = 20030822L; 037 038 // Variables starting with dkconfig_ should only be set via the 039 // daikon.config.Configuration interface. 040 /** Boolean. True iff FloatEqual invariants should be considered. */ 041 public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault; 042 043 public static final Logger debug = Logger.getLogger("daikon.inv.binary.twoScalar.FloatEqual"); 044 045 FloatEqual(PptSlice ppt) { 046 super(ppt); 047 } 048 049 @Prototype FloatEqual() { 050 super(); 051 } 052 053 private static @Prototype FloatEqual proto = new @Prototype FloatEqual(); 054 055 /** Returns the prototype invariant for FloatEqual */ 056 public static @Prototype FloatEqual get_proto() { 057 return proto; 058 } 059 060 /** Returns whether or not this invariant is enabled. */ 061 @Override 062 public boolean enabled() { 063 return dkconfig_enabled; 064 } 065 066 /** Returns whether or not the specified var types are valid for FloatEqual */ 067 @Override 068 public boolean instantiate_ok(VarInfo[] vis) { 069 070 if (!valid_types(vis)) { 071 return false; 072 } 073 074 return true; 075 } 076 077 /** Instantiate an invariant on the specified slice. */ 078 @Override 079 protected FloatEqual instantiate_dyn(@Prototype FloatEqual this, PptSlice slice) { 080 081 return new FloatEqual(slice); 082 } 083 084 @Pure 085 public boolean is_equality_inv() { 086 return true; 087 } 088 089 @Override 090 protected Invariant resurrect_done_swapped() { 091 092 // we don't care if things swap; we have symmetry 093 return this; 094 } 095 096 @Pure 097 @Override 098 public boolean is_symmetric() { 099 return true; 100 } 101 102 // JHP: this should be removed in favor of checks in PptTopLevel 103 // such as is_equal, is_lessequal, etc. 104 // Look up a previously instantiated FloatEqual relationship. 105 // Should this implementation be made more efficient? 106 public static @Nullable FloatEqual find(PptSlice ppt) { 107 assert ppt.arity() == 2; 108 for (Invariant inv : ppt.invs) { 109 if (inv instanceof FloatEqual) { 110 return (FloatEqual) inv; 111 } 112 } 113 114 // If the invariant is suppressed, create it 115 if ((suppressions != null) && suppressions.suppressed(ppt)) { 116 FloatEqual inv = proto.instantiate_dyn(ppt); 117 // System.out.printf("%s is suppressed in ppt %s%n", inv.format(), ppt.name()); 118 return inv; 119 } 120 121 return null; 122 } 123 124 @Override 125 public String repr(@GuardSatisfied FloatEqual this) { 126 return "FloatEqual" + varNames(); 127 } 128 129 @SideEffectFree 130 @Override 131 public String format_using(@GuardSatisfied FloatEqual this, OutputFormat format) { 132 133 String var1name = var1().name_using(format); 134 String var2name = var2().name_using(format); 135 136 if ((format == OutputFormat.DAIKON) || (format == OutputFormat.ESCJAVA)) { 137 String comparator = "=="; 138 return var1name + " " + comparator + " " + var2name; 139 } 140 141 if (format == OutputFormat.CSHARPCONTRACT) { 142 143 String comparator = "=="; 144 return var1name + " " + comparator + " " + var2name; 145 } 146 147 if (format.isJavaFamily()) { 148 149 return Invariant.formatFuzzy("eq", var1(), var2(), format); 150 151 } 152 153 if (format == OutputFormat.SIMPLIFY) { 154 155 String comparator = "EQ"; 156 157 return "(" 158 + comparator 159 + " " 160 + var1().simplifyFixup(var1name) 161 + " " 162 + var2().simplifyFixup(var2name) 163 + ")"; 164 } 165 166 return format_unimplemented(format); 167 } 168 169 @Override 170 public InvariantStatus check_modified(double v1, double v2, int count) { 171 if (!Global.fuzzy.eq(v1, v2)) { 172 return InvariantStatus.FALSIFIED; 173 } 174 return InvariantStatus.NO_CHANGE; 175 } 176 177 @Override 178 public InvariantStatus add_modified(double v1, double v2, int count) { 179 if (logDetail() || debug.isLoggable(Level.FINE)) { 180 log( 181 debug, 182 "add_modified (" + v1 + ", " + v2 + ", ppt.num_values = " + ppt.num_values() + ")"); 183 } 184 if ((logOn() || debug.isLoggable(Level.FINE)) 185 && check_modified(v1, v2, count) == InvariantStatus.FALSIFIED) 186 log(debug, "destroy in add_modified (" + v1 + ", " + v2 + ", " + count + ")"); 187 188 return check_modified(v1, v2, count); 189 } 190 191 // This is very tricky, because whether two variables are equal should 192 // presumably be transitive, but it's not guaranteed to be so when using 193 // this method and not dropping out all variables whose values are ever 194 // missing. 195 @Override 196 protected double computeConfidence() { 197 // Should perhaps check number of samples and be unjustified if too few 198 // samples. 199 200 // We MUST check if we have seen samples; otherwise we get 201 // undesired transitivity with missing values. 202 if (ppt.num_samples() == 0) { 203 return Invariant.CONFIDENCE_UNJUSTIFIED; 204 } 205 206 // It's an equality invariant. I ought to use the actual ranges somehow. 207 // Actually, I can't even use this .5 test because it can make 208 // equality non-transitive. 209 // return Math.pow(.5, num_values()); 210 return Invariant.CONFIDENCE_JUSTIFIED; 211 212 } 213 214 @Override 215 public boolean enoughSamples(@GuardSatisfied FloatEqual this) { 216 return ppt.num_samples() > 0; 217 } 218 219 // For Comparison interface, which is satisfied only by exact equalities. 220 @Override 221 public double eq_confidence() { 222 if (isExact()) { 223 return getConfidence(); 224 } else { 225 return Invariant.CONFIDENCE_NEVER; 226 } 227 } 228 229 @Pure 230 @Override 231 public boolean isExact() { 232 233 return true; 234 } 235 236 // // Temporary, for debugging 237 // public void destroy() { 238 // if (debug.isLoggable(Level.FINE)) { 239 // System.out.println("FloatEqual.destroy(" + ppt.name() + ")"); 240 // System.out.println(repr()); 241 // (new Error()).printStackTrace(); 242 // } 243 // super.destroy(); 244 // } 245 246 @Override 247 public InvariantStatus add( 248 @Interned Object v1, @Interned Object v2, int mod_index, int count) { 249 if (debug.isLoggable(Level.FINE)) { 250 debug.fine( 251 "FloatEqual" 252 + ppt.varNames() 253 + ".add(" 254 + v1 255 + "," 256 + v2 257 + ", mod_index=" 258 + mod_index 259 + "), count=" 260 + count 261 + ")"); 262 } 263 return super.add(v1, v2, mod_index, count); 264 } 265 266 @Pure 267 @Override 268 public boolean isSameFormula(Invariant other) { 269 return true; 270 } 271 272 @Pure 273 @Override 274 public boolean isExclusiveFormula(Invariant other) { 275 276 // Also ought to check against LinearBinary, etc. 277 278 if ((other instanceof FloatLessThan) 279 || (other instanceof FloatGreaterThan) 280 || (other instanceof FloatNonEqual)) { 281 return true; 282 } 283 284 return false; 285 } 286 287 @Override 288 public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) { 289 final VarInfo var1 = vis[0]; 290 final VarInfo var2 = vis[1]; 291 292 // If A.minvalue==A.maxvalue==B.minvalue==B.maxvalue, then 293 // there's nothing to see here. 294 if (var1.aux.hasValue(VarInfoAux.MINIMUM_VALUE) 295 && var1.aux.hasValue(VarInfoAux.MAXIMUM_VALUE) 296 && var2.aux.hasValue(VarInfoAux.MINIMUM_VALUE) 297 && var2.aux.hasValue(VarInfoAux.MAXIMUM_VALUE)) { 298 @SuppressWarnings("all:argument") // EnsuresKeyFor for multiple maps; also https://tinyurl.com/cfissue/2586 299 int minA = var1.aux.getInt(VarInfoAux.MINIMUM_VALUE), 300 maxA = var1.aux.getInt(VarInfoAux.MAXIMUM_VALUE), 301 minB = var2.aux.getInt(VarInfoAux.MINIMUM_VALUE), 302 maxB = var2.aux.getInt(VarInfoAux.MAXIMUM_VALUE); 303 304 if (minA == maxA && maxA == minB && minB == maxB) { 305 return new DiscardInfo( 306 this, DiscardCode.obvious, var1.name() + " == " + var2.name() + " is already known"); 307 } 308 } 309 310 return super.isObviousStatically(vis); 311 } 312 313 /** 314 * Since this invariant can be a postProcessed equality, we have to handle isObvious especially to 315 * avoid circular isObvious relations. We only check if this.ppt.var_infos imply obviousness 316 * rather than the cartesian product on the equality set. 317 */ 318 @Pure 319 @Override 320 public @Nullable DiscardInfo isObviousStatically_SomeInEquality() { 321 if (var1().equalitySet == var2().equalitySet) { 322 return isObviousStatically(this.ppt.var_infos); 323 } else { 324 return super.isObviousStatically_SomeInEquality(); 325 } 326 } 327 328 /** 329 * Since this invariant can be a postProcessed equality, we have to handle isObvious especially to 330 * avoid circular isObvious relations. We only check if this.ppt.var_infos imply obviousness 331 * rather than the cartesian product on the equality set. 332 */ 333 @Pure 334 @Override 335 public @Nullable DiscardInfo isObviousDynamically_SomeInEquality() { 336 if (var1().equalitySet == var2().equalitySet) { 337 return isObviousDynamically(this.ppt.var_infos); 338 } else { 339 return super.isObviousDynamically_SomeInEquality(); 340 } 341 } 342 343 @Pure 344 @Override 345 public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) { 346 347 // JHP: We might consider adding a check over bounds. If 348 // x < c and y > c then we know that x < y. Similarly for 349 // x > c and y < c. We could also substitute oneof for 350 // one or both of the bound checks. 351 352 DiscardInfo super_result = super.isObviousDynamically(vis); 353 if (super_result != null) { 354 return super_result; 355 } 356 357 VarInfo var1 = vis[0]; 358 VarInfo var2 = vis[1]; 359 360 // a+c=b+c is implied, because a=b must have also been reported. 361 if (var1.is_add() && var2.is_add() && (var1.get_add_amount() == var2.get_add_amount())) { 362 return new DiscardInfo( 363 this, DiscardCode.obvious, 364 "Invariants of the form a+c==b+c are implied since a==b is reported."); 365 } 366 367 @SuppressWarnings("UnusedVariable") // generated code, variable is sometimes used 368 DiscardInfo di; 369 370 // Check for the same invariant over enclosing arrays 371 di = pairwise_implies(vis); 372 if (di != null) { 373 return di; 374 } 375 376 // Check for size(A[]) == Size(B[]) where A[] == B[] 377 di = array_eq_implies(vis); 378 if (di != null) { 379 return di; 380 } 381 382 { // Sequence length tests 383 SequenceLength sl1 = null; 384 if (var1.isDerived() && (var1.derived instanceof SequenceLength)) { 385 sl1 = (SequenceLength) var1.derived; 386 } 387 SequenceLength sl2 = null; 388 if (var2.isDerived() && (var2.derived instanceof SequenceLength)) { 389 sl2 = (SequenceLength) var2.derived; 390 } 391 392 // "size(a)-1 cmp size(b)-1" is never even instantiated; 393 // use "size(a) cmp size(b)" instead. 394 395 // This might never get invoked, as equality is printed out specially. 396 VarInfo s1 = (sl1 == null) ? null : sl1.base; 397 VarInfo s2 = (sl2 == null) ? null : sl2.base; 398 if ((s1 != null) && (s2 != null) && (s1.equalitySet == s2.equalitySet)) { 399 // lengths of equal arrays being compared 400 String n1 = var1.name(); 401 String n2 = var2.name(); 402 return new DiscardInfo( 403 this, 404 DiscardCode.obvious, 405 n1 + " and " + n2 + " are equal arrays, so equal size is implied"); 406 } 407 408 } 409 410 return null; 411 } // isObviousDynamically 412 413 /** 414 * If both variables are subscripts and the underlying arrays have the same invariant, then this 415 * invariant is implied: 416 * 417 * <pre>(x[] op y[]) ^ (i == j) ⇒ (x[i] op y[j])</pre> 418 */ 419 private @Nullable DiscardInfo pairwise_implies(VarInfo[] vis) { 420 421 VarInfo v1 = vis[0]; 422 VarInfo v2 = vis[1]; 423 424 // Make sure v1 and v2 are SequenceFloatSubscript with the same shift 425 if (!v1.isDerived() || !(v1.derived instanceof SequenceFloatSubscript)) { 426 return null; 427 } 428 if (!v2.isDerived() || !(v2.derived instanceof SequenceFloatSubscript)) { 429 return null; 430 } 431 @NonNull SequenceFloatSubscript der1 = (SequenceFloatSubscript) v1.derived; 432 @NonNull SequenceFloatSubscript der2 = (SequenceFloatSubscript) v2.derived; 433 if (der1.index_shift != der2.index_shift) { 434 return null; 435 } 436 437 // Make sure that the indices are equal 438 if (!ppt.parent.is_equal(der1.sclvar().canonicalRep(), der2.sclvar().canonicalRep())) { 439 return null; 440 } 441 442 // See if the same relationship holds over the arrays 443 Invariant proto = PairwiseFloatEqual.get_proto(); 444 DiscardInfo di = ppt.parent.check_implied_canonical(this, der1.seqvar(), der2.seqvar(), proto); 445 return di; 446 } 447 448 /** 449 * If the equality is between two array size variables, check to see if the underlying arrays are 450 * equal: 451 * 452 * <pre>(x[] = y[]) ⇒ size(x[]) = size(y[])</pre> 453 */ 454 private @Nullable DiscardInfo array_eq_implies(VarInfo[] vis) { 455 456 // Make sure v1 and v2 are size(array) with the same shift 457 VarInfo v1 = vis[0]; 458 if (!v1.isDerived() || !(v1.derived instanceof SequenceLength)) { 459 return null; 460 } 461 VarInfo v2 = vis[1]; 462 if (!v2.isDerived() || !(v2.derived instanceof SequenceLength)) { 463 return null; 464 } 465 if (!v1.derived.isSameFormula(v2.derived)) { 466 return null; 467 } 468 469 VarInfo seqvar1 = v1.derived.getBase(0); 470 VarInfo seqvar2 = v2.derived.getBase(0); 471 if (ppt.parent.is_equal(seqvar1, seqvar2)) { 472 return new DiscardInfo( 473 this, 474 DiscardCode.obvious, 475 "Implied by " 476 + seqvar1 477 + " == " 478 + seqvar2 479 + " and " 480 + var1() 481 + " == " 482 + v1 483 + " and " 484 + var2() 485 + " == " 486 + v2); 487 } 488 489 return null; 490 } 491 492 /** NI suppressions, initialized in get_ni_suppressions() */ 493 private static @Nullable NISuppressionSet suppressions = null; 494 495 /** Returns the non-instantiating suppressions for this invariant. */ 496 @Pure 497 @Override 498 public @Nullable NISuppressionSet get_ni_suppressions() { 499 return null; 500 } 501 502}