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