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