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