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 UpperBoundFloat 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 UpperBoundFloat 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 UpperBoundFloat 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 UpperBoundFloat 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 UpperBoundFloat(PptSlice slice) { 062 super(slice); 063 assert slice != null; 064 core = new UpperBoundCoreFloat(this); 065 } 066 067 private @Prototype UpperBoundFloat() { 068 super(); 069 // do we need a core? 070 } 071 072 private static @Prototype UpperBoundFloat proto = new @Prototype UpperBoundFloat(); 073 074 /** Returns the prototype invariant for UpperBoundFloat */ 075 public static @Prototype UpperBoundFloat 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 UpperBoundFloat instantiate_dyn(@Prototype UpperBoundFloat this, PptSlice slice) { 096 return new UpperBoundFloat(slice); 097 } 098 099 @SideEffectFree 100 @Override 101 public UpperBoundFloat clone(@GuardSatisfied UpperBoundFloat this) { 102 UpperBoundFloat result = (UpperBoundFloat) 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 UpperBoundFloat this) { 114 return "UpperBoundFloat" + varNames() + ": " 115 + core.repr(); 116 } 117 118 @SideEffectFree 119 @Override 120 public String format_using(@GuardSatisfied UpperBoundFloat 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.max1)) || (Double.isNaN(constantVal) && Double.isNaN( core.max1))) { 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.max1)) { 144 return name + " <= " + vi.name(); 145 } 146 } 147 } 148 } 149 } 150 151 return name + " <= " + core.max1; 152 } 153 154 if (format == OutputFormat.SIMPLIFY) { 155 156 return "(<= " + name + " " + simplify_format_double(core.max1) + ")"; 157 } 158 159 return format_unimplemented(format); 160 } 161 162 @Override 163 public InvariantStatus add_modified(double value, int count) { 164 // System.out.println("UpperBoundFloat" + 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 UpperBoundFloat 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(((UpperBoundFloat) 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.max1 < dkconfig_minimal_interesting) 205 || (core.max1 > dkconfig_maximal_interesting)) { 206 return true; 207 } 208 209 else if (core.max1 != (int)core.max1) { 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.MAXIMUM_VALUE)) { 227 int minVal = var.aux.getInt(VarInfoAux.MAXIMUM_VALUE); 228 if (minVal == core.max1) { 229 return new DiscardInfo(this, DiscardCode.obvious, 230 var.name() + " GTE " + core.max1 + " 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.max1 < dkconfig_minimal_interesting) 259 || (core.max1 > 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.max1 < dkconfig_minimal_interesting) { 267 discardString = "MIN1="+core.max1+" is less than dkconfig_minimal_interesting==" 268 + dkconfig_minimal_interesting; 269 } else { 270 discardString = "MIN1="+core.max1+" 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.max1 == oo.max_elt(), since the LowerBound 279 // will never have a core.max1 that does not appear in the OneOf. 280 if (core.max1 >= oo.max_elt()) { 281 String varName = vis[0].name(); 282 String discardString = varName + ">=" + core.max1 + " is implied by " + varName + ">=" + oo.max_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 // For each sequence variable, if this is an obvious member/subsequence, and 293 // it has the same invariant, then this one is obvious. 294 for (int i = 0; i < pptt.var_infos.length; i++) { 295 VarInfo vi = pptt.var_infos[i]; 296 297 if (MemberFloat.isObviousMember(v, vi)) 298 { 299 PptSlice1 other_slice = pptt.findSlice(vi); 300 if (other_slice != null) { 301 EltUpperBoundFloat eb = EltUpperBoundFloat.find(other_slice); 302 if ((eb != null) 303 && eb.enoughSamples() 304 && eb.max() == max()) { 305 String otherName = other_slice.var_infos[0].name(); 306 String varName = v.name(); 307 String discardString = varName+" is a subsequence of "+otherName+" for which the invariant holds."; 308 log("%s", discardString); 309 return new DiscardInfo(this, DiscardCode.obvious, discardString); 310 } 311 } 312 } 313 } 314 315 return null; 316 } 317 318 @Pure 319 @Override 320 public boolean isExclusiveFormula(Invariant other) { 321 322 if (other instanceof LowerBoundFloat) { 323 if (max() < ((LowerBoundFloat) other).min()) { 324 return true; 325 } 326 } 327 328 if (other instanceof OneOfFloat) { 329 return other.isExclusiveFormula(this); 330 } 331 return false; 332 } 333 334 // Look up a previously instantiated invariant. 335 public static @Nullable UpperBoundFloat find(PptSlice ppt) { 336 assert ppt.arity() == 1; 337 for (Invariant inv : ppt.invs) { 338 if (inv instanceof UpperBoundFloat) { 339 return (UpperBoundFloat) inv; 340 } 341 } 342 return null; 343 } 344 345 /** 346 * Bound can merge different formulas from lower points to create a single formula at an upper 347 * point. See merge() below. 348 */ 349 @Override 350 public boolean mergeFormulasOk() { 351 return true; 352 } 353 354 /** 355 * Merge the invariants in invs to form a new invariant. Each must be a UpperBoundFloat invariant. This 356 * code finds all of the min/max values in each invariant, applies them to a new parent invariant 357 * and returns the merged invariant (if any). 358 * 359 * @param invs list of invariants to merge. The invariants must all be of the same type and should 360 * come from the children of parent_ppt. They should also all be permuted to match the 361 * variable order in parent_ppt. 362 * @param parent_ppt slice that will contain the new invariant 363 */ 364 @Override 365 public @Nullable UpperBoundFloat merge(List<Invariant> invs, PptSlice parent_ppt) { 366 367 // Create the initial parent invariant from the first child 368 UpperBoundFloat first = (UpperBoundFloat) invs.get(0); 369 UpperBoundFloat result= first.clone(); 370 result.ppt = parent_ppt; 371 372 // Loop through the rest of the child invariants 373 for (int i = 1; i < invs.size(); i++ ) { 374 UpperBoundFloat lb = (UpperBoundFloat) invs.get(i); 375 result.core.add(lb.core); 376 } 377 378 result.log("Merged '%s' from %s child invariants", result.format(),invs.size()); 379 return result; 380 } 381}