001// ***** This file is automatically generated from Bound.java.jpp 002 003package daikon.inv.unary.scalar; 004 005import daikon.*; 006import daikon.inv.*; 007 008 import daikon.inv.binary.sequenceScalar.*; 009 import daikon.inv.unary.sequence.*; 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 {@code x >= c}, where {@code c} is a constant and 026 * {@code x} is a double scalar. 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 LowerBoundFloat extends SingleFloat { 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 LowerBoundFloat 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 LowerBoundFloat 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 LowerBoundFloat 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 LowerBoundCoreFloat core; 059 060 @SuppressWarnings("nullness") // circular initialization 061 private LowerBoundFloat(PptSlice slice) { 062 super(slice); 063 assert slice != null; 064 core = new LowerBoundCoreFloat(this); 065 } 066 067 private @Prototype LowerBoundFloat() { 068 super(); 069 // do we need a core? 070 } 071 072 private static @Prototype LowerBoundFloat proto = new @Prototype LowerBoundFloat(); 073 074 /** Returns the prototype invariant for LowerBoundFloat */ 075 public static @Prototype LowerBoundFloat 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 LowerBoundFloat instantiate_dyn(@Prototype LowerBoundFloat this, PptSlice slice) { 096 return new LowerBoundFloat(slice); 097 } 098 099 @SideEffectFree 100 @Override 101 public LowerBoundFloat clone(@GuardSatisfied LowerBoundFloat this) { 102 LowerBoundFloat result = (LowerBoundFloat) super.clone(); 103 result.core = core.clone(); 104 result.core.wrapper = result; 105 return result; 106 } 107 108 public double min() { 109 return core.min(); // i.e., core.min1 110 } 111 112 @Override 113 public String repr(@GuardSatisfied LowerBoundFloat this) { 114 return "LowerBoundFloat" + varNames() + ": " 115 + core.repr(); 116 } 117 118 @SideEffectFree 119 @Override 120 public String format_using(@GuardSatisfied LowerBoundFloat this, OutputFormat format) { 121 String name = var().name_using(format); 122 PptTopLevel pptt = ppt.parent; 123 124 if ((format == OutputFormat.DAIKON) 125 || (format == OutputFormat.ESCJAVA) 126 || format.isJavaFamily() 127 || (format == OutputFormat.CSHARPCONTRACT)) { 128 129 if (PrintInvariants.dkconfig_static_const_infer) { 130 for (VarInfo vi : pptt.var_infos) { 131 // Check is static constant, and variables are comparable 132 if (vi.isStaticConstant() && VarComparability.comparable(vi, var())) { 133 // If variable is a double, then use fuzzy comparison 134 if (vi.rep_type == ProglangType.DOUBLE) { 135 Double constantVal = (Double)vi.constantValue(); 136 if (Global.fuzzy.eq(constantVal, (core.min1)) || (Double.isNaN(constantVal) && Double.isNaN( core.min1))) { 137 return name + " >= " + vi.name(); 138 } 139 } 140 // Otherwise just use the equals method 141 else { 142 Object constantVal = vi.constantValue(); 143 if (constantVal.equals(core.min1)) { 144 return name + " >= " + vi.name(); 145 } 146 } 147 } 148 } 149 } 150 151 return name + " >= " + core.min1; 152 } 153 154 if (format == OutputFormat.SIMPLIFY) { 155 156 return "(>= " + name + " " + simplify_format_double(core.min1) + ")"; 157 } 158 159 return format_unimplemented(format); 160 } 161 162 @Override 163 public InvariantStatus add_modified(double value, int count) { 164 // System.out.println("LowerBoundFloat" + varNames() + ": " 165 // + "add(" + value + ", " + modified + ", " + count + ")"); 166 167 return core.add_modified(value, count); 168 169 } 170 171 @Override 172 public InvariantStatus check_modified(double value, int count) { 173 174 return core.check(value); 175 176 } 177 178 @Override 179 public boolean enoughSamples(@GuardSatisfied LowerBoundFloat this) { 180 return core.enoughSamples(); 181 } 182 183 @Override 184 protected double computeConfidence() { 185 return core.computeConfidence(); 186 } 187 188 @Pure 189 @Override 190 public boolean isExact() { 191 return core.isExact(); 192 } 193 194 @Pure 195 @Override 196 public boolean isSameFormula(Invariant other) { 197 return core.isSameFormula(((LowerBoundFloat) other).core); 198 } 199 200 @Override 201 public boolean hasUninterestingConstant() { 202 // If the constant bound is not in some small range of interesting 203 // values (by default {-1, 0, 1, 2}), call it uninteresting. 204 if ((core.min1 < dkconfig_minimal_interesting) 205 || (core.min1 > dkconfig_maximal_interesting)) { 206 return true; 207 } 208 209 else if (core.min1 != (int)core.min1) { 210 // Non-integer bounds are uninteresting even if small. 211 return true; 212 } 213 214 return false; 215 } 216 217 @Pure 218 @Override 219 public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) { 220 VarInfo var = vis[0]; 221 if ((var.derived instanceof SequenceLength) 222 && (((SequenceLength) var.derived).shift != 0)) { 223 return new DiscardInfo(this, DiscardCode.obvious, "Bounds are preferrable over sequence lengths with no shift"); 224 } 225 226 if (var.aux.hasValue(VarInfoAux.MINIMUM_VALUE)) { 227 int minVal = var.aux.getInt(VarInfoAux.MINIMUM_VALUE); 228 if (minVal == core.min1) { 229 return new DiscardInfo(this, DiscardCode.obvious, 230 var.name() + " GTE " + core.min1 + " is already known"); 231 } 232 } 233 234 return super.isObviousStatically(vis); 235 } 236 237 @Pure 238 @Override 239 public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) { 240 DiscardInfo super_result = super.isObviousDynamically(vis); 241 if (super_result != null) { 242 return super_result; 243 } 244 245 PptTopLevel pptt = ppt.parent; 246 247 // This check always lets invariants pass through (even if it is not within 248 // the default range of (-1 to 2) if it matches a static constant 249 // As noted below, this check really doesn't belong here, but should be 250 // moved to hasUninterestingConstant() whenever that is implemented 251 if (PrintInvariants.dkconfig_static_const_infer) { 252 if (core.matchConstant()) { 253 return null; 254 } 255 } 256 257 // if the value is not in some range (like -1,0,1,2) then say that it is obvious 258 if ((core.min1 < dkconfig_minimal_interesting) 259 || (core.min1 > dkconfig_maximal_interesting)) { 260 // XXX This check doesn't really belong here. However It 261 // shouldn't get removed until hasUninterestingConstant() is 262 // suitable to be turned on everywhere by default. -SMcC 263 // if the value is not in some range (like -1,0,1,2) then say that 264 // it is obvious 265 String discardString = ""; 266 if (core.min1 < dkconfig_minimal_interesting) { 267 discardString = "MIN1="+core.min1+" is less than dkconfig_minimal_interesting==" 268 + dkconfig_minimal_interesting; 269 } else { 270 discardString = "MIN1="+core.min1+" is greater than dkconfig_maximal_interesting=="+ 271 dkconfig_maximal_interesting; 272 } 273 return new DiscardInfo(this, DiscardCode.obvious, discardString); 274 } 275 OneOfFloat oo = OneOfFloat.find(ppt); 276 if ((oo != null) && oo.enoughSamples() && oo.num_elts() > 0) { 277 assert oo.var().isCanonical(); 278 // We could also use core.min1 == oo.min_elt(), since the LowerBound 279 // will never have a core.min1 that does not appear in the OneOf. 280 if (core.min1 <= oo.min_elt()) { 281 String varName = vis[0].name(); 282 String discardString = varName + "<=" + core.min1 + " is implied by " + varName + "<=" + oo.min_elt(); 283 log("%s", discardString); 284 return new DiscardInfo(this, DiscardCode.obvious, discardString); 285 } 286 } 287 288 // NOT: "VarInfo v = var();" because we want to operate not on this 289 // object's own variables, but on the variables that were passed in. 290 VarInfo v = vis[0]; 291 292 if (v.isDerived() && (v.derived instanceof SequenceLength)) { 293 // Invariants with over sequence lengths with vshift != 0 are 294 // now no longer even instantiated. However, the commented-out 295 // assertion below would break reading old .inv files, so we'll 296 // still do the check at run time for the moment. 297 int vshift = ((SequenceLength) v.derived).shift; 298 // assert vshift == 0; 299 if (vshift == 0 && core.min1 == 0) { 300 // "size(a[]) >= 0" is obvious. 301 return new DiscardInfo(this, DiscardCode.obvious, v.name()+" >=0 is obvious"); 302 } 303 } 304 305 // For each sequence variable, if this is an obvious member/subsequence, and 306 // it has the same invariant, then this one is obvious. 307 for (int i = 0; i < pptt.var_infos.length; i++) { 308 VarInfo vi = pptt.var_infos[i]; 309 310 if (MemberFloat.isObviousMember(v, vi)) 311 { 312 PptSlice1 other_slice = pptt.findSlice(vi); 313 if (other_slice != null) { 314 EltLowerBoundFloat eb = EltLowerBoundFloat.find(other_slice); 315 if ((eb != null) 316 && eb.enoughSamples() 317 && eb.min() == min()) { 318 String otherName = other_slice.var_infos[0].name(); 319 String varName = v.name(); 320 String discardString = varName+" is a subsequence of "+otherName+" for which the invariant holds."; 321 log("%s", discardString); 322 return new DiscardInfo(this, DiscardCode.obvious, discardString); 323 } 324 } 325 } 326 } 327 328 return null; 329 } 330 331 @Pure 332 @Override 333 public boolean isExclusiveFormula(Invariant other) { 334 335 if (other instanceof UpperBoundFloat) { 336 if (min() > ((UpperBoundFloat) other).max()) { 337 return true; 338 } 339 } 340 341 if (other instanceof OneOfFloat) { 342 return other.isExclusiveFormula(this); 343 } 344 return false; 345 } 346 347 // Look up a previously instantiated invariant. 348 public static @Nullable LowerBoundFloat find(PptSlice ppt) { 349 assert ppt.arity() == 1; 350 for (Invariant inv : ppt.invs) { 351 if (inv instanceof LowerBoundFloat) { 352 return (LowerBoundFloat) inv; 353 } 354 } 355 return null; 356 } 357 358 /** 359 * Bound can merge different formulas from lower points to create a single formula at an upper 360 * point. See merge() below. 361 */ 362 @Override 363 public boolean mergeFormulasOk() { 364 return true; 365 } 366 367 /** 368 * Merge the invariants in invs to form a new invariant. Each must be a LowerBoundFloat invariant. This 369 * code finds all of the min/max values in each invariant, applies them to a new parent invariant 370 * and returns the merged invariant (if any). 371 * 372 * @param invs list of invariants to merge. The invariants must all be of the same type and should 373 * come from the children of parent_ppt. They should also all be permuted to match the 374 * variable order in parent_ppt. 375 * @param parent_ppt slice that will contain the new invariant 376 */ 377 @Override 378 public @Nullable LowerBoundFloat merge(List<Invariant> invs, PptSlice parent_ppt) { 379 380 // Create the initial parent invariant from the first child 381 LowerBoundFloat first = (LowerBoundFloat) invs.get(0); 382 LowerBoundFloat result= first.clone(); 383 result.ppt = parent_ppt; 384 385 // Loop through the rest of the child invariants 386 for (int i = 1; i < invs.size(); i++ ) { 387 LowerBoundFloat lb = (LowerBoundFloat) invs.get(i); 388 result.core.add(lb.core); 389 } 390 391 result.log("Merged '%s' from %s child invariants", result.format(),invs.size()); 392 return result; 393 } 394}