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