001// ***** This file is automatically generated from Bound.java.jpp 002 003package daikon.inv.unary.sequence; 004 005import daikon.*; 006import daikon.inv.*; 007 008 import daikon.inv.binary.twoSequence.*; 009 import daikon.inv.unary.scalar.*; 010 011import daikon.derive.unary.*; 012import daikon.inv.unary.*; 013import java.util.*; 014import org.checkerframework.checker.interning.qual.Interned; 015import org.checkerframework.checker.lock.qual.GuardSatisfied; 016import org.checkerframework.checker.nullness.qual.Nullable; 017import org.checkerframework.dataflow.qual.Pure; 018import org.checkerframework.dataflow.qual.SideEffectFree; 019import org.checkerframework.framework.qual.Unused; 020import org.plumelib.util.Intern; 021import typequals.prototype.qual.NonPrototype; 022import typequals.prototype.qual.Prototype; 023 024 /** 025 * Represents the invariant that each element of a sequence of double values is less than or 026 * equal to a constant. Prints as {@code x[] elements <= c}. 027 */ 028 029// One reason not to combine LowerBound and UpperBound into a single range 030// invariant is that they have separate justifications: one may be 031// justified when the other is not. 032@SuppressWarnings("UnnecessaryParentheses") // code generated by macros 033public class EltUpperBoundFloat extends SingleFloatSequence { 034 static final long serialVersionUID = 20030822L; 035 036 // Variables starting with dkconfig_ should only be set via the 037 // daikon.config.Configuration interface. 038 /** Boolean. True iff EltUpperBoundFloat invariants should be considered. */ 039 public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault; 040 /** 041 * Long integer. Together with the corresponding {@code maximal_interesting} parameter, 042 * specifies the range of the computed constant that is ``interesting'' --- the range that should 043 * be reported. For instance, setting {@code minimal_interesting} to -1 and 044 * {@code maximal_interesting} to 2 would only permit output of EltUpperBoundFloat invariants whose 045 * cutoff was one of (-1,0,1,2). 046 */ 047 public static long dkconfig_minimal_interesting = -1; 048 /** 049 * Long integer. Together with the corresponding {@code minimal_interesting} parameter, 050 * specifies the range of the computed constant that is ``interesting'' --- the range that should 051 * be reported. For instance, setting {@code minimal_interesting} to -1 and 052 * {@code maximal_interesting} to 2 would only permit output of EltUpperBoundFloat invariants whose 053 * cutoff was one of (-1,0,1,2). 054 */ 055 public static long dkconfig_maximal_interesting = 2; 056 057 @Unused(when=Prototype.class) 058 private UpperBoundCoreFloat core; 059 060 @SuppressWarnings("nullness") // circular initialization 061 private EltUpperBoundFloat(PptSlice slice) { 062 super(slice); 063 assert slice != null; 064 core = new UpperBoundCoreFloat(this); 065 } 066 067 private @Prototype EltUpperBoundFloat() { 068 super(); 069 // do we need a core? 070 } 071 072 private static @Prototype EltUpperBoundFloat proto = new @Prototype EltUpperBoundFloat(); 073 074 /** Returns the prototype invariant for EltUpperBoundFloat */ 075 public static @Prototype EltUpperBoundFloat get_proto() { 076 return proto; 077 } 078 079 @Override 080 public boolean enabled() { 081 return dkconfig_enabled; 082 } 083 084 @Override 085 public boolean instantiate_ok(VarInfo[] vis) { 086 087 if (!valid_types(vis)) { 088 return false; 089 } 090 091 return vis[0].file_rep_type.baseIsFloat(); 092 } 093 094 @Override 095 public EltUpperBoundFloat instantiate_dyn(@Prototype EltUpperBoundFloat this, PptSlice slice) { 096 return new EltUpperBoundFloat(slice); 097 } 098 099 @SideEffectFree 100 @Override 101 public EltUpperBoundFloat clone(@GuardSatisfied EltUpperBoundFloat this) { 102 EltUpperBoundFloat result = (EltUpperBoundFloat) super.clone(); 103 result.core = core.clone(); 104 result.core.wrapper = result; 105 return result; 106 } 107 108 public double max() { 109 return core.max(); // i.e., core.max1 110 } 111 112 @Override 113 public String repr(@GuardSatisfied EltUpperBoundFloat this) { 114 return "EltUpperBoundFloat" + varNames() + ": " 115 + core.repr(); 116 } 117 118 @SideEffectFree 119 @Override 120 public String format_using(@GuardSatisfied EltUpperBoundFloat this, OutputFormat format) { 121 122 if (format.isJavaFamily()) { 123 return format_java_family(format); 124 } 125 126 if (format == OutputFormat.DAIKON) { 127 return format_daikon(); 128 } else if (format == OutputFormat.SIMPLIFY) { 129 return format_simplify(); 130 } else if (format == OutputFormat.ESCJAVA) { 131 return format_esc(); 132 } else if (format == OutputFormat.CSHARPCONTRACT) { 133 return format_csharp_contract(); 134 } 135 136 return format_unimplemented(format); 137 } 138 // ELTLOWEr || ELTUPPEr 139 public String format_daikon(@GuardSatisfied EltUpperBoundFloat this) { 140 PptTopLevel pptt = ppt.parent; 141 String name = var().name(); 142 143 if (PrintInvariants.dkconfig_static_const_infer) { 144 for (VarInfo vi : pptt.var_infos) { 145 if (vi.isStaticConstant() && VarComparability.comparable(vi, var())) { 146 // If variable is a double, then use fuzzy comparison 147 if (vi.rep_type == ProglangType.DOUBLE) { 148 Double constantVal = (Double)vi.constantValue(); 149 if (Global.fuzzy.eq(constantVal, (core.max1)) || (Double.isNaN(constantVal) && Double.isNaN( core.max1))) { 150 return name + " <= " + vi.name(); 151 } 152 } 153 // Otherwise just use the equals method 154 else { 155 Object constantVal = vi.constantValue(); 156 if (constantVal.equals(core.max1)) { 157 return name + " <= " + vi.name(); 158 } 159 } 160 } 161 } 162 } 163 164 return var().name() + " elements <= " + core.max1; 165 } 166 167 public String format_esc(@GuardSatisfied EltUpperBoundFloat this) { 168 PptTopLevel pptt = ppt.parent; 169 170 if (PrintInvariants.dkconfig_static_const_infer) { 171 for (VarInfo vi : pptt.var_infos) { 172 if (vi.isStaticConstant() && VarComparability.comparable(vi, var())) { 173 // If variable is a double, then use fuzzy comparison 174 if (vi.rep_type == ProglangType.DOUBLE) { 175 Double constantVal = (Double)vi.constantValue(); 176 if (Global.fuzzy.eq(constantVal, (core.max1)) || (Double.isNaN(constantVal) && Double.isNaN( core.max1))) { 177 178 String[] form = VarInfo.esc_quantify(var()); 179 return form[0] + "(" + form[1] + " <= " + vi.name() + ")" + form[2]; 180 } 181 } 182 // Otherwise just use the equals method 183 else { 184 Object constantVal = vi.constantValue(); 185 if (constantVal.equals(core.max1)) { 186 187 String[] form = VarInfo.esc_quantify(var()); 188 return form[0] + "(" + form[1] + " <= " + vi.name() + ")" + form[2]; 189 } 190 } 191 } 192 } 193 } 194 195 String[] form = VarInfo.esc_quantify(var()); 196 return form[0] + "(" + form[1] + " <= " + core.max1 + ")" + form[2]; 197 } 198 199 public String format_csharp_contract(@GuardSatisfied EltUpperBoundFloat this) { 200 PptTopLevel pptt = ppt.parent; 201 202 if (PrintInvariants.dkconfig_static_const_infer) { 203 for (VarInfo vi : pptt.var_infos) { 204 if (vi.isStaticConstant() && VarComparability.comparable(vi, var())) { 205 // If variable is a double, then use fuzzy comparison 206 if (vi.rep_type == ProglangType.DOUBLE) { 207 Double constantVal = (Double)vi.constantValue(); 208 if (Global.fuzzy.eq(constantVal, (core.max1)) || (Double.isNaN(constantVal) && Double.isNaN( core.max1))) { 209 210 String[] split = var().csharp_array_split(); 211 return "Contract.ForAll(" + split[0] + ", x => x" + split[1] + " <= " + vi.name() + ")"; 212 } 213 } 214 // Otherwise just use the equals method 215 else { 216 Object constantVal = vi.constantValue(); 217 if (constantVal.equals(core.max1)) { 218 219 String[] split = var().csharp_array_split(); 220 return "Contract.ForAll(" + split[0] + ", x => x" + split[1] + " <= " + vi.name() + ")"; 221 } 222 } 223 } 224 } 225 } 226 227 String[] split = var().csharp_array_split(); 228 return "Contract.ForAll(" + split[0] + ", x => x" + split[1] + " <= " + core.max1+ ")"; 229 } 230 231 public String format_java_family(@GuardSatisfied EltUpperBoundFloat this, OutputFormat format) { 232 PptTopLevel pptt = ppt.parent; 233 234 if (PrintInvariants.dkconfig_static_const_infer) { 235 for (VarInfo vi : pptt.var_infos) { 236 if (vi.isStaticConstant() && VarComparability.comparable(vi, var())) { 237 // If variable is a double, then use fuzzy comparison 238 if (vi.rep_type == ProglangType.DOUBLE) { 239 Double constantVal = (Double)vi.constantValue(); 240 if (Global.fuzzy.eq(constantVal, (core.max1)) || (Double.isNaN(constantVal) && Double.isNaN( core.max1))) { 241 242 return "daikon.Quant.eltsLTE(" + var().name_using(format) + ", " + vi.name() + ")"; 243 } 244 } 245 // Otherwise just use the equals method 246 else { 247 Object constantVal = vi.constantValue(); 248 if (constantVal.equals(core.max1)) { 249 250 return "daikon.Quant.eltsLTE(" + var().name_using(format) + ", " + vi.name() + ")"; 251 } 252 } 253 } 254 } 255 } 256 257 return 258 "daikon.Quant.eltsLTE(" + var().name_using(format) + ", " + core.max1 + ")"; 259 260 } 261 262 public String format_simplify(@GuardSatisfied EltUpperBoundFloat this) { 263 264 String value = simplify_format_double(core.max1); 265 266 String[] form = VarInfo.simplify_quantify(var()); 267 return form[0] + "(<= " + form[1] + " " + value + ")" 268 + form[2]; 269 270 } 271 272 @Override 273 public InvariantStatus add_modified(double @Interned [] value, int count) { 274 // System.out.println("EltUpperBoundFloat" + varNames() + ": " 275 // + "add(" + value + ", " + modified + ", " + count + ")"); 276 277 boolean changed = false; 278 InvariantStatus status = InvariantStatus.NO_CHANGE; 279 for (int i = 0; i < value.length; i++) { 280 if (!changed && core.wouldChange(value[i])) { 281 changed = true; 282 status = InvariantStatus.WEAKENED; 283 } 284 if (core.add_modified(value[i], count) == InvariantStatus.FALSIFIED) { 285 return InvariantStatus.FALSIFIED; 286 } 287 } 288 return status; 289 } 290 291 @Override 292 public InvariantStatus check_modified(double @Interned [] value, int count) { 293 294 for (int i = 0; i < value.length; i++) { 295 if (core.check(value[i]) == InvariantStatus.WEAKENED) { 296 return InvariantStatus.WEAKENED; 297 } 298 } 299 return InvariantStatus.NO_CHANGE; 300 } 301 302 @Override 303 public boolean enoughSamples(@GuardSatisfied EltUpperBoundFloat this) { 304 return core.enoughSamples(); 305 } 306 307 @Override 308 protected double computeConfidence() { 309 return core.computeConfidence(); 310 } 311 312 @Pure 313 @Override 314 public boolean isExact() { 315 return core.isExact(); 316 } 317 318 @Pure 319 @Override 320 public boolean isSameFormula(Invariant other) { 321 return core.isSameFormula(((EltUpperBoundFloat) other).core); 322 } 323 324 @Override 325 public boolean hasUninterestingConstant() { 326 // If the constant bound is not in some small range of interesting 327 // values (by default {-1, 0, 1, 2}), call it uninteresting. 328 if ((core.max1 < dkconfig_minimal_interesting) 329 || (core.max1 > dkconfig_maximal_interesting)) { 330 return true; 331 } 332 333 else if (core.max1 != (int)core.max1) { 334 // Non-integer bounds are uninteresting even if small. 335 return true; 336 } 337 338 return false; 339 } 340 341 @Pure 342 @Override 343 public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) { 344 VarInfo var = vis[0]; 345 if ((var.derived instanceof SequenceLength) 346 && (((SequenceLength) var.derived).shift != 0)) { 347 return new DiscardInfo(this, DiscardCode.obvious, "Bounds are preferrable over sequence lengths with no shift"); 348 } 349 350 return super.isObviousStatically(vis); 351 } 352 353 @Pure 354 @Override 355 public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) { 356 DiscardInfo super_result = super.isObviousDynamically(vis); 357 if (super_result != null) { 358 return super_result; 359 } 360 361 PptTopLevel pptt = ppt.parent; 362 363 // This check always lets invariants pass through (even if it is not within 364 // the default range of (-1 to 2) if it matches a static constant 365 // As noted below, this check really doesn't belong here, but should be 366 // moved to hasUninterestingConstant() whenever that is implemented 367 if (PrintInvariants.dkconfig_static_const_infer) { 368 if (core.matchConstant()) { 369 return null; 370 } 371 } 372 373 // if the value is not in some range (like -1,0,1,2) then say that it is obvious 374 if ((core.max1 < dkconfig_minimal_interesting) 375 || (core.max1 > dkconfig_maximal_interesting)) { 376 // XXX This check doesn't really belong here. However It 377 // shouldn't get removed until hasUninterestingConstant() is 378 // suitable to be turned on everywhere by default. -SMcC 379 // if the value is not in some range (like -1,0,1,2) then say that 380 // it is obvious 381 String discardString = ""; 382 if (core.max1 < dkconfig_minimal_interesting) { 383 discardString = "MIN1="+core.max1+" is less than dkconfig_minimal_interesting==" 384 + dkconfig_minimal_interesting; 385 } else { 386 discardString = "MIN1="+core.max1+" is greater than dkconfig_maximal_interesting=="+ 387 dkconfig_maximal_interesting; 388 } 389 return new DiscardInfo(this, DiscardCode.obvious, discardString); 390 } 391 EltOneOfFloat oo = EltOneOfFloat.find(ppt); 392 if ((oo != null) && oo.enoughSamples() && oo.num_elts() > 0) { 393 assert oo.var().isCanonical(); 394 // We could also use core.max1 == oo.max_elt(), since the LowerBound 395 // will never have a core.max1 that does not appear in the OneOf. 396 if (core.max1 >= oo.max_elt()) { 397 String varName = vis[0].name(); 398 String discardString = varName + ">=" + core.max1 + " is implied by " + varName + ">=" + oo.max_elt(); 399 log("%s", discardString); 400 return new DiscardInfo(this, DiscardCode.obvious, discardString); 401 } 402 } 403 404 // NOT: "VarInfo v = var();" because we want to operate not on this 405 // object's own variables, but on the variables that were passed in. 406 VarInfo v = vis[0]; 407 408 // Look for the same property over a supersequence of this one. 409 for (Iterator<Invariant> inv_itor = pptt.invariants_iterator(); inv_itor.hasNext(); ) { 410 Invariant inv = inv_itor.next(); 411 if (inv == this) { 412 continue; 413 } 414 if (inv instanceof EltUpperBoundFloat) { 415 EltUpperBoundFloat other = (EltUpperBoundFloat) inv; 416 if (isSameFormula(other) 417 && SubSequenceFloat.isObviousSubSequenceDynamically(this, v, other.var())) { 418 String varName = v.name(); 419 String otherName = other.var().name(); 420 String discardString = varName + " is a subsequence of " + otherName + " for which the invariant holds."; 421 log("%s", discardString); 422 return new DiscardInfo(this, DiscardCode.obvious, discardString); 423 } 424 } 425 } 426 427 // For each sequence variable, if this is an obvious member/subsequence, and 428 // it has the same invariant, then this one is obvious. 429 for (int i = 0; i < pptt.var_infos.length; i++) { 430 VarInfo vi = pptt.var_infos[i]; 431 432 if (SubSequenceFloat.isObviousSubSequenceDynamically(this, v, vi)) 433 { 434 PptSlice1 other_slice = pptt.findSlice(vi); 435 if (other_slice != null) { 436 EltUpperBoundFloat eb = EltUpperBoundFloat.find(other_slice); 437 if ((eb != null) 438 && eb.enoughSamples() 439 && eb.max() == max()) { 440 String otherName = other_slice.var_infos[0].name(); 441 String varName = v.name(); 442 String discardString = varName+" is a subsequence of "+otherName+" for which the invariant holds."; 443 log("%s", discardString); 444 return new DiscardInfo(this, DiscardCode.obvious, discardString); 445 } 446 } 447 } 448 } 449 450 return null; 451 } 452 453 @Pure 454 @Override 455 public boolean isExclusiveFormula(Invariant other) { 456 457 // N.B. "x[] elements >= 200" is not mutually exclusive with "x[] 458 // elements <= 100"; they could both be true if x[] were always empty. 459 460 if (other instanceof OneOfFloat) { 461 return other.isExclusiveFormula(this); 462 } 463 return false; 464 } 465 466 // Look up a previously instantiated invariant. 467 public static @Nullable EltUpperBoundFloat find(PptSlice ppt) { 468 assert ppt.arity() == 1; 469 for (Invariant inv : ppt.invs) { 470 if (inv instanceof EltUpperBoundFloat) { 471 return (EltUpperBoundFloat) inv; 472 } 473 } 474 return null; 475 } 476 477 /** 478 * Bound can merge different formulas from lower points to create a single formula at an upper 479 * point. See merge() below. 480 */ 481 @Override 482 public boolean mergeFormulasOk() { 483 return true; 484 } 485 486 /** 487 * Merge the invariants in invs to form a new invariant. Each must be a EltUpperBoundFloat invariant. This 488 * code finds all of the min/max values in each invariant, applies them to a new parent invariant 489 * and returns the merged invariant (if any). 490 * 491 * @param invs list of invariants to merge. The invariants must all be of the same type and should 492 * come from the children of parent_ppt. They should also all be permuted to match the 493 * variable order in parent_ppt. 494 * @param parent_ppt slice that will contain the new invariant 495 */ 496 @Override 497 public @Nullable EltUpperBoundFloat merge(List<Invariant> invs, PptSlice parent_ppt) { 498 499 // Create the initial parent invariant from the first child 500 EltUpperBoundFloat first = (EltUpperBoundFloat) invs.get(0); 501 EltUpperBoundFloat result= first.clone(); 502 result.ppt = parent_ppt; 503 504 // Loop through the rest of the child invariants 505 for (int i = 1; i < invs.size(); i++ ) { 506 EltUpperBoundFloat lb = (EltUpperBoundFloat) invs.get(i); 507 result.core.add(lb.core); 508 } 509 510 result.log("Merged '%s' from %s child invariants", result.format(),invs.size()); 511 return result; 512 } 513}