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