001// ***** This file is automatically generated from Range.java.jpp 002 003package daikon.inv.unary.scalar; 004 005import org.checkerframework.dataflow.qual.Pure; 006import org.checkerframework.checker.lock.qual.GuardSatisfied; 007import org.checkerframework.dataflow.qual.SideEffectFree; 008import org.checkerframework.checker.interning.qual.Interned; 009import org.checkerframework.checker.nullness.qual.Nullable; 010import daikon.*; 011import daikon.Quantify.QuantFlags; 012import daikon.derive.unary.*; 013import daikon.inv.*; 014import daikon.inv.binary.sequenceScalar.*; 015import daikon.inv.unary.sequence.*; 016import java.util.*; 017import java.util.logging.Level; 018import java.util.logging.Logger; 019import org.plumelib.util.Intern; 020import org.plumelib.util.UtilPlume; 021import typequals.prototype.qual.NonPrototype; 022import typequals.prototype.qual.Prototype; 023 024/** 025 * Baseclass for unary range based invariants. Each invariant is a special stateless version of 026 * bound or oneof. For example EqualZero, BooleanVal, etc). These are never printed, but are used 027 * internally as suppressors for ni-suppressions. 028 * 029 * Each specific invariant is implemented in a subclass (typically in this file). 030 */ 031 032public abstract class RangeFloat extends SingleFloat { 033 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 = 20040311L; 038 039 protected RangeFloat(PptSlice ppt) { 040 super(ppt); 041 } 042 043 protected @Prototype RangeFloat() { 044 super(); 045 } 046 047 /** 048 * Check that instantiation is ok. The type must be integral 049 * (not boolean or hash code). 050 */ 051 @Override 052 public boolean instantiate_ok(VarInfo[] vis) { 053 054 if (!valid_types(vis)) { 055 return false; 056 } 057 058 if (!vis[0].file_rep_type.baseIsFloat()) { 059 return false; 060 } 061 062 return true; 063 } 064 065 /** 066 * Returns a string in the specified format that describes the invariant. 067 * 068 * The generic format string is obtained from the subclass specific get_format_str(). Instances of 069 * %var1% are replaced by the variable name in the specified format. 070 */ 071 @SideEffectFree 072 @Override 073 public String format_using(@GuardSatisfied RangeFloat this, OutputFormat format) { 074 075 String fmt_str = get_format_str(format); 076 077 VarInfo var1 = ppt.var_infos[0]; 078 String v1 = null; 079 080 if (v1 == null) { 081 v1 = var1.name_using(format); 082 } 083 084 fmt_str = fmt_str.replace("%var1%", v1); 085 return fmt_str; 086 } 087 088 @Override 089 public InvariantStatus check_modified(double x, int count) { 090 if (eq_check(x)) { 091 return InvariantStatus.NO_CHANGE; 092 } else { 093 return InvariantStatus.FALSIFIED; 094 } 095 } 096 097 @Override 098 public InvariantStatus add_modified(double x, int count) { 099 return check_modified(x, count); 100 } 101 102 @Override 103 protected double computeConfidence() { 104 return CONFIDENCE_JUSTIFIED; 105 } 106 107 @Pure 108 @Override 109 public boolean isSameFormula(Invariant other) { 110 assert other.getClass() == getClass(); 111 return true; 112 } 113 @Pure 114 @Override 115 public boolean isExclusiveFormula(Invariant other) { 116 return false; 117 } 118 119 /** 120 * All range invariants except Even and PowerOfTwo are obvious since they represented by some 121 * version of OneOf or Bound. 122 */ 123 @Pure 124 @Override 125 public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) { 126 127 return new DiscardInfo(this, DiscardCode.obvious, 128 "Implied by Oneof or Bound"); 129 } 130 131 /** 132 * Looks for a OneOf invariant over vis. Used by Even and PowerOfTwo to dynamically suppress those 133 * invariants if a OneOf exists. 134 */ 135 protected @Nullable OneOfFloat find_oneof(VarInfo[] vis) { 136 return (OneOfFloat) ppt.parent.find_inv_by_class(vis, OneOfFloat.class); 137 } 138 139 /** 140 * Return a format string for the specified output format. Each instance of %varN% will be 141 * replaced by the correct name for varN. 142 */ 143 public abstract String get_format_str(@GuardSatisfied RangeFloat this, OutputFormat format); 144 145 /** Returns true if x and y don't invalidate the invariant. */ 146 public abstract boolean eq_check(double x); 147 148 /** 149 * Returns a list of prototypes of all of the range 150 * invariants. 151 */ 152 public static List<@Prototype Invariant> get_proto_all() { 153 154 List<@Prototype Invariant> result = new ArrayList<>(); 155 result.add(EqualZero.get_proto()); 156 result.add(EqualOne.get_proto()); 157 result.add(EqualMinusOne.get_proto()); 158 result.add(GreaterEqualZero.get_proto()); 159 result.add(GreaterEqual64.get_proto()); 160 161 return result; 162 } 163 164 /** 165 * Internal invariant representing double scalars that are equal to zero. Used for 166 * non-instantiating suppressions. Will never print since OneOf accomplishes the same thing. 167 */ 168 public static class EqualZero extends RangeFloat { 169 170 // We are Serializable, so we specify a version to allow changes to 171 // method signatures without breaking serialization. If you add or 172 // remove fields, you should change this number to the current date. 173 static final long serialVersionUID = 20040113L; 174 175 protected EqualZero(PptSlice ppt) { 176 super(ppt); 177 } 178 179 protected @Prototype EqualZero() { 180 super(); 181 } 182 183 private static @Prototype EqualZero proto = new @Prototype EqualZero(); 184 185 /** returns the prototype invariant */ 186 public static @Prototype EqualZero get_proto() { 187 return proto; 188 } 189 190 /** Returns whether or not this invariant is enabled. */ 191 @Override 192 public boolean enabled() { 193 return OneOfFloat.dkconfig_enabled; 194 } 195 196 /** instantiates the invariant on the specified slice */ 197 @Override 198 public EqualZero instantiate_dyn(@Prototype EqualZero this, PptSlice slice) { 199 return new EqualZero(slice); 200 } 201 202 @Override 203 public String get_format_str(@GuardSatisfied EqualZero this, OutputFormat format) { 204 if (format == OutputFormat.SIMPLIFY) { 205 return "(EQ 0 %var1%)"; 206 } else { 207 return "%var1% == 0"; 208 } 209 } 210 211 @Override 212 public boolean eq_check(double x) { 213 return x == 0; 214 } 215 } 216 217 /** 218 * Internal invariant representing double scalars that are equal to one. Used for 219 * non-instantiating suppressions. Will never print since OneOf accomplishes the same thing. 220 */ 221 public static class EqualOne extends RangeFloat { 222 223 // We are Serializable, so we specify a version to allow changes to 224 // method signatures without breaking serialization. If you add or 225 // remove fields, you should change this number to the current date. 226 static final long serialVersionUID = 20040113L; 227 228 protected EqualOne(PptSlice ppt) { 229 super(ppt); 230 } 231 232 protected @Prototype EqualOne() { 233 super(); 234 } 235 236 private static @Prototype EqualOne proto = new @Prototype EqualOne(); 237 238 /** returns the prototype invariant */ 239 public static @Prototype EqualOne get_proto() { 240 return proto; 241 } 242 243 /** Returns whether or not this invariant is enabled. */ 244 @Override 245 public boolean enabled() { 246 return OneOfFloat.dkconfig_enabled; 247 } 248 249 /** instantiates the invariant on the specified slice */ 250 @Override 251 public EqualOne instantiate_dyn(@Prototype EqualOne this, PptSlice slice) { 252 return new EqualOne(slice); 253 } 254 255 @Override 256 public String get_format_str(@GuardSatisfied EqualOne this, OutputFormat format) { 257 if (format == OutputFormat.SIMPLIFY) { 258 return "(EQ 1 %var1%)"; 259 } else { 260 return "%var1% == 1"; 261 } 262 } 263 264 @Override 265 public boolean eq_check(double x) { 266 return x == 1; 267 } 268 } 269 270 /** 271 * Internal invariant representing double scalars that are equal to minus one. Used for 272 * non-instantiating suppressions. Will never print since OneOf accomplishes the same thing. 273 */ 274 public static class EqualMinusOne extends RangeFloat { 275 276 // We are Serializable, so we specify a version to allow changes to 277 // method signatures without breaking serialization. If you add or 278 // remove fields, you should change this number to the current date. 279 static final long serialVersionUID = 20040824L; 280 281 protected EqualMinusOne(PptSlice ppt) { 282 super(ppt); 283 } 284 285 protected @Prototype EqualMinusOne() { 286 super(); 287 } 288 289 private static @Prototype EqualMinusOne proto = new @Prototype EqualMinusOne(); 290 291 /** returns the prototype invariant */ 292 public static @Prototype EqualMinusOne get_proto() { 293 return proto; 294 } 295 296 /** Returns whether or not this invariant is enabled. */ 297 @Override 298 public boolean enabled() { 299 return OneOfFloat.dkconfig_enabled; 300 } 301 302 /** instantiates the invariant on the specified slice */ 303 @Override 304 public EqualMinusOne instantiate_dyn(@Prototype EqualMinusOne this, PptSlice slice) { 305 return new EqualMinusOne(slice); 306 } 307 308 @Override 309 public String get_format_str(@GuardSatisfied EqualMinusOne this, OutputFormat format) { 310 if (format == OutputFormat.SIMPLIFY) { 311 return "(EQ -1 %var1%)"; 312 } else { 313 return "%var1% == -1"; 314 } 315 } 316 317 @Override 318 public boolean eq_check(double x) { 319 return x == -1; 320 } 321 } 322 323 /** 324 * Internal invariant representing double scalars that are greater than or equal to 0. Used 325 * for non-instantiating suppressions. Will never print since Bound accomplishes the same thing. 326 */ 327 public static class GreaterEqualZero extends RangeFloat { 328 329 // We are Serializable, so we specify a version to allow changes to 330 // method signatures without breaking serialization. If you add or 331 // remove fields, you should change this number to the current date. 332 static final long serialVersionUID = 20040113L; 333 334 protected GreaterEqualZero(PptSlice ppt) { 335 super(ppt); 336 } 337 338 protected @Prototype GreaterEqualZero() { 339 super(); 340 } 341 342 private static @Prototype GreaterEqualZero proto = new @Prototype GreaterEqualZero(); 343 344 /** returns the prototype invariant */ 345 public static @Prototype GreaterEqualZero get_proto() { 346 return proto; 347 } 348 349 /** Returns whether or not this invariant is enabled. */ 350 @Override 351 public boolean enabled() { 352 return LowerBoundFloat.dkconfig_enabled; 353 } 354 355 /** instantiates the invariant on the specified slice */ 356 @Override 357 public GreaterEqualZero instantiate_dyn(@Prototype GreaterEqualZero this, PptSlice slice) { 358 return new GreaterEqualZero(slice); 359 } 360 361 @Override 362 public String get_format_str(@GuardSatisfied GreaterEqualZero this, OutputFormat format) { 363 if (format == OutputFormat.SIMPLIFY) { 364 return "(>= %var1% 0)"; 365 } else { 366 return "%var1% >= 0"; 367 } 368 } 369 370 @Override 371 public boolean eq_check(double x) { 372 return x >= 0; 373 } 374 } 375 376 /** 377 * Internal invariant representing double scalars that are greater than or equal to 64. Used 378 * for non-instantiating suppressions. Will never print since Bound accomplishes the same thing. 379 */ 380 public static class GreaterEqual64 extends RangeFloat { 381 382 // We are Serializable, so we specify a version to allow changes to 383 // method signatures without breaking serialization. If you add or 384 // remove fields, you should change this number to the current date. 385 static final long serialVersionUID = 20040113L; 386 387 protected GreaterEqual64(PptSlice ppt) { 388 super(ppt); 389 } 390 391 protected @Prototype GreaterEqual64() { 392 super(); 393 } 394 395 private static @Prototype GreaterEqual64 proto = new @Prototype GreaterEqual64(); 396 397 /** returns the prototype invariant */ 398 public static @Prototype GreaterEqual64 get_proto() { 399 return proto; 400 } 401 402 /** Returns whether or not this invariant is enabled. */ 403 @Override 404 public boolean enabled() { 405 return LowerBoundFloat.dkconfig_enabled; 406 } 407 408 /** instantiates the invariant on the specified slice */ 409 @Override 410 public GreaterEqual64 instantiate_dyn(@Prototype GreaterEqual64 this, PptSlice slice) { 411 return new GreaterEqual64(slice); 412 } 413 414 @Override 415 public String get_format_str(@GuardSatisfied GreaterEqual64 this, OutputFormat format) { 416 if (format == OutputFormat.SIMPLIFY) { 417 return "(>= %var1% 64)"; 418 } else { 419 return "%var1% >= 64"; 420 } 421 } 422 423 @Override 424 public boolean eq_check(double x) { 425 return x >= 64; 426 } 427 } 428 429}