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