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