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