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