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 FloatGreaterThan extends TwoFloat { 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 FloatGreaterThan 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.FloatGreaterThan"); 041 042 FloatGreaterThan(PptSlice ppt) { 043 super(ppt); 044 } 045 046 @Prototype FloatGreaterThan() { 047 super(); 048 } 049 050 private static @Prototype FloatGreaterThan proto = new @Prototype FloatGreaterThan(); 051 052 /** Returns the prototype invariant for FloatGreaterThan. */ 053 public static @Prototype FloatGreaterThan 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 FloatGreaterThan. */ 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 FloatGreaterThan instantiate_dyn(@Prototype FloatGreaterThan this, PptSlice slice) { 075 076 return new FloatGreaterThan(slice); 077 } 078 079 @Override 080 protected Invariant resurrect_done_swapped() { 081 082 // we have no non-static member data, so we only need care about our type 083 // As of now, the constructor chain is side-effect free; 084 // let's hope it stays that way. 085 FloatLessThan result = new FloatLessThan(ppt); 086 return result; 087 } 088 089 /** Returns the class that corresponds to this class with its variable order swapped. */ 090 public static Class<? extends Invariant> swap_class() { 091 return FloatLessThan.class; 092 } 093 094 // JHP: this should be removed in favor of checks in PptTopLevel 095 // such as is_equal, is_lessequal, etc. 096 // Look up a previously instantiated FloatGreaterThan relationship. 097 // Should this implementation be made more efficient? 098 public static @Nullable FloatGreaterThan find(PptSlice ppt) { 099 assert ppt.arity() == 2; 100 for (Invariant inv : ppt.invs) { 101 if (inv instanceof FloatGreaterThan) { 102 return (FloatGreaterThan) inv; 103 } 104 } 105 106 // If the invariant is suppressed, create it 107 if ((suppressions != null) && suppressions.suppressed(ppt)) { 108 FloatGreaterThan inv = proto.instantiate_dyn(ppt); 109 // System.out.printf("%s is suppressed in ppt %s%n", inv.format(), ppt.name()); 110 return inv; 111 } 112 113 return null; 114 } 115 116 @Override 117 public String repr(@GuardSatisfied FloatGreaterThan this) { 118 return "FloatGreaterThan" + varNames(); 119 } 120 121 @SideEffectFree 122 @Override 123 public String format_using(@GuardSatisfied FloatGreaterThan this, OutputFormat format) { 124 125 String var1name = var1().name_using(format); 126 String var2name = var2().name_using(format); 127 128 if ((format == OutputFormat.DAIKON) || (format == OutputFormat.ESCJAVA)) { 129 String comparator = ">"; 130 return var1name + " " + comparator + " " + var2name; 131 } 132 133 if (format == OutputFormat.CSHARPCONTRACT) { 134 135 String comparator = ">"; 136 return var1name + " " + comparator + " " + var2name; 137 } 138 139 if (format.isJavaFamily()) { 140 141 return Invariant.formatFuzzy("gt", var1(), var2(), format); 142 143 } 144 145 if (format == OutputFormat.SIMPLIFY) { 146 147 String comparator = ">"; 148 149 return "(" 150 + comparator 151 + " " 152 + var1().simplifyFixup(var1name) 153 + " " 154 + var2().simplifyFixup(var2name) 155 + ")"; 156 } 157 158 return format_unimplemented(format); 159 } 160 161 @Override 162 public InvariantStatus check_modified(double v1, double v2, int count) { 163 if (!Global.fuzzy.gt(v1, v2)) { 164 return InvariantStatus.FALSIFIED; 165 } 166 return InvariantStatus.NO_CHANGE; 167 } 168 169 @Override 170 public InvariantStatus add_modified(double v1, double v2, int count) { 171 if (logDetail() || debug.isLoggable(Level.FINE)) { 172 log( 173 debug, 174 "add_modified (" + v1 + ", " + v2 + ", ppt.num_values = " + ppt.num_values() + ")"); 175 } 176 if ((logOn() || debug.isLoggable(Level.FINE)) 177 && check_modified(v1, v2, count) == InvariantStatus.FALSIFIED) 178 log(debug, "destroy in add_modified (" + v1 + ", " + v2 + ", " + count + ")"); 179 180 return check_modified(v1, v2, count); 181 } 182 183 // This is very tricky, because whether two variables are equal should 184 // presumably be transitive, but it's not guaranteed to be so when using 185 // this method and not dropping out all variables whose values are ever 186 // missing. 187 @Override 188 protected double computeConfidence() { 189 // Should perhaps check number of samples and be unjustified if too few 190 // samples. 191 192 // // The reason for this multiplication is that there might be only a 193 // // very few possible values. Example: towers of hanoi has only 6 194 // // possible (pegA, pegB) pairs. 195 // return 1 - (Math.pow(.5, ppt.num_values()) 196 // * Math.pow(.99, ppt.num_mod_samples())); 197 return 1 - Math.pow(.5, ppt.num_samples()); 198 } 199 200 @Pure 201 @Override 202 public boolean isExact() { 203 204 return false; 205 } 206 207 // // Temporary, for debugging 208 // public void destroy() { 209 // if (debug.isLoggable(Level.FINE)) { 210 // System.out.println("FloatGreaterThan.destroy(" + ppt.name() + ")"); 211 // System.out.println(repr()); 212 // (new Error()).printStackTrace(); 213 // } 214 // super.destroy(); 215 // } 216 217 @Override 218 public InvariantStatus add( 219 @Interned Object v1, @Interned Object v2, int mod_index, int count) { 220 if (debug.isLoggable(Level.FINE)) { 221 debug.fine( 222 "FloatGreaterThan" 223 + ppt.varNames() 224 + ".add(" 225 + v1 226 + "," 227 + v2 228 + ", mod_index=" 229 + mod_index 230 + "), count=" 231 + count 232 + ")"); 233 } 234 return super.add(v1, v2, mod_index, count); 235 } 236 237 @Pure 238 @Override 239 public boolean isSameFormula(Invariant other) { 240 return true; 241 } 242 243 @Pure 244 @Override 245 public boolean isExclusiveFormula(Invariant other) { 246 247 // Also ought to check against LinearBinary, etc. 248 249 if ((other instanceof FloatLessThan) 250 || (other instanceof FloatLessEqual) 251 || (other instanceof FloatEqual)) 252 return true; 253 254 return false; 255 } 256 257 @Override 258 public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) { 259 final VarInfo var1 = vis[0]; 260 final VarInfo var2 = vis[1]; 261 262 if (var1.aux.hasValue(VarInfoAux.MINIMUM_VALUE) 263 && var2.aux.hasValue(VarInfoAux.MAXIMUM_VALUE)) { 264 int maxB = var2.aux.getInt(VarInfoAux.MAXIMUM_VALUE), 265 minA = var1.aux.getInt(VarInfoAux.MINIMUM_VALUE); 266 267 if (minA > maxB) { 268 return new DiscardInfo( 269 this, 270 DiscardCode.obvious, 271 var1.name() + " DISCARD_OP " + var2.name() + " is already known"); 272 } 273 } 274 275 return super.isObviousStatically(vis); 276 } 277 278 @Pure 279 @Override 280 public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) { 281 282 // JHP: We might consider adding a check over bounds. If 283 // x < c and y > c then we know that x < y. Similarly for 284 // x > c and y < c. We could also substitute oneof for 285 // one or both of the bound checks. 286 287 DiscardInfo super_result = super.isObviousDynamically(vis); 288 if (super_result != null) { 289 return super_result; 290 } 291 292 VarInfo var1 = vis[0]; 293 VarInfo var2 = vis[1]; 294 295 @SuppressWarnings("UnusedVariable") // generated code, variable is sometimes used 296 DiscardInfo di; 297 298 // Check for the same invariant over enclosing arrays 299 di = pairwise_implies(vis); 300 if (di != null) { 301 return di; 302 } 303 304 // Check for a linear binary that implies > or < 305 di = lb_implies(vis); 306 if (di != null) { 307 return di; 308 } 309 310 { // Sequence length tests 311 SequenceLength sl1 = null; 312 if (var1.isDerived() && (var1.derived instanceof SequenceLength)) { 313 sl1 = (SequenceLength) var1.derived; 314 } 315 SequenceLength sl2 = null; 316 if (var2.isDerived() && (var2.derived instanceof SequenceLength)) { 317 sl2 = (SequenceLength) var2.derived; 318 } 319 320 // "size(a)-1 cmp size(b)-1" is never even instantiated; 321 // use "size(a) cmp size(b)" instead. 322 323 // This might never get invoked, as equality is printed out specially. 324 VarInfo s1 = (sl1 == null) ? null : sl1.base; 325 VarInfo s2 = (sl2 == null) ? null : sl2.base; 326 if ((s1 != null) && (s2 != null) && (s1.equalitySet == s2.equalitySet)) { 327 // lengths of equal arrays being compared 328 String n1 = var1.name(); 329 String n2 = var2.name(); 330 return new DiscardInfo( 331 this, 332 DiscardCode.obvious, 333 n1 + " and " + n2 + " are equal arrays, so equal size is implied"); 334 } 335 336 if ((sl1 != null) && (sl1.shift == 0)) { 337 // "size(a) > x" ("size(a) >= x" would be more informative) 338 String discardString = 339 "Invariants of the form size(a)-1 > x are suppressed since size(a) >= x is preferred"; 340 return new DiscardInfo(this, DiscardCode.obvious, discardString); 341 } else if ((sl2 != null) && (sl2.shift == -1)) { 342 // "x > size(a)-1" ("x >= size(a)" would be more informative) 343 String discardString = 344 "Invariants of the form x > size(a)-1 are suppressed sinec x >= size(a) is preferred"; 345 return new DiscardInfo(this, DiscardCode.obvious, discardString); 346 } 347 348 } 349 350 return null; 351 } // isObviousDynamically 352 353 /** 354 * Checks to see if there is a linear binary relationship between the variables that implies > 355 * or < 356 * 357 * <pre> 358 * a * x + b * y + c == 0 359 * 360 * (y = (-a/b)*x + (-c/b) ^ (-a/b == 1) ^ (-c/b > 0) ⇒ y > x 361 * (y = (-a/b)*x + (-c/b) ^ (-a/b == 1) ^ (-c/b < 0) ⇒ y < x 362 * </pre> 363 * 364 * Returns null if this is not true. Appropriate DiscardInfo otherwise. 365 */ 366 //old 367 // * (y = ax + b) ^ (a == 1) ^ (b > 0) ==> y > x 368 // * (y = ax + b) ^ (a == 1) ^ (b < 0) ==> y < x 369 370 private @Nullable DiscardInfo lb_implies(VarInfo[] vis) { 371 372 // Look for a linear binary invariant over the same variables 373 LinearBinaryFloat lb = (LinearBinaryFloat) ppt.parent.find_inv_by_class 374 (vis, LinearBinaryFloat.class); 375 if ((lb == null) || !lb.isActive()) { 376 return null; 377 } 378 379 // Only 'a == 1' implies a less than or greater than relationship 380 if (-lb.core.a / lb.core.b != 1.0) { 381 return null; 382 } 383 384 // The b coefficient determines less than or greater than 385 if (Global.fuzzy.gt(-lb.core.c / lb.core.b, 0)) { 386 return null; 387 } 388 389 return new DiscardInfo(this, DiscardCode.obvious, "implied by " + lb.format()); 390 } 391 392 /** 393 * If both variables are subscripts and the underlying arrays have the same invariant, then this 394 * invariant is implied: 395 * 396 * <pre>(x[] op y[]) ^ (i == j) ⇒ (x[i] op y[j])</pre> 397 */ 398 private @Nullable DiscardInfo pairwise_implies(VarInfo[] vis) { 399 400 VarInfo v1 = vis[0]; 401 VarInfo v2 = vis[1]; 402 403 // Make sure v1 and v2 are SequenceFloatSubscript with the same shift 404 if (!v1.isDerived() || !(v1.derived instanceof SequenceFloatSubscript)) { 405 return null; 406 } 407 if (!v2.isDerived() || !(v2.derived instanceof SequenceFloatSubscript)) { 408 return null; 409 } 410 @NonNull SequenceFloatSubscript der1 = (SequenceFloatSubscript) v1.derived; 411 @NonNull SequenceFloatSubscript der2 = (SequenceFloatSubscript) v2.derived; 412 if (der1.index_shift != der2.index_shift) { 413 return null; 414 } 415 416 // Make sure that the indices are equal 417 if (!ppt.parent.is_equal(der1.sclvar().canonicalRep(), der2.sclvar().canonicalRep())) { 418 return null; 419 } 420 421 // See if the same relationship holds over the arrays 422 Invariant proto = PairwiseFloatGreaterThan.get_proto(); 423 DiscardInfo di = ppt.parent.check_implied_canonical(this, der1.seqvar(), der2.seqvar(), proto); 424 return di; 425 } 426 427 /** NI suppressions, initialized in get_ni_suppressions() */ 428 private static @Nullable NISuppressionSet suppressions = null; 429 430 /** Returns the non-instantiating suppressions for this invariant. */ 431 @Pure 432 @Override 433 public @Nullable NISuppressionSet get_ni_suppressions() { 434 return null; 435 } 436 437}