001// ***** This file is automatically generated from FunctionBinary.java.jpp 002// ***** (and files it recursively includes). 003 004package daikon.inv.ternary.threeScalar; 005 006import daikon.*; 007import daikon.derive.unary.*; 008import daikon.inv.*; 009import daikon.inv.binary.twoScalar.*; 010import daikon.inv.unary.scalar.*; 011import daikon.suppress.*; 012import java.lang.reflect.*; 013import java.util.*; 014import java.util.logging.Logger; 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.plumelib.util.ArraysPlume; 020import org.plumelib.util.MathPlume; 021import typequals.prototype.qual.NonPrototype; 022import typequals.prototype.qual.Prototype; 023 024/** 025 * Base class for each of the FunctionBinaryFloat functions and permutatons. Most of the work is done 026 * here. The subclasses basically define the function and return information describing the function 027 * and permutation to these methods. 028 */ 029@SuppressWarnings("UnusedVariable") // generated code, complex rules for when var is used 030public abstract class FunctionBinaryFloat extends ThreeFloat { 031 // We are Serializable, so we specify a version to allow changes to 032 // method signatures without breaking serialization. If you add or 033 // remove fields, you should change this number to the current date. 034 static final long serialVersionUID = 20031030L; 035 036 /** Boolean. True if FunctionBinaryFloat invariants should be considered. */ 037 public static boolean dkconfig_enabled = false; 038 039 public static Logger debug = 040 Logger.getLogger("daikon.inv.ternary.threeScalar.#CLASSNAME"); 041 042 static final int[][] var_indices; 043 static { 044 var_indices = new int[7][]; 045 var_indices[1] = new int[] { 0, 1, 2 }; 046 var_indices[2] = new int[] { 1, 0, 2 }; 047 var_indices[3] = new int[] { 2, 0, 1 }; 048 var_indices[4] = new int[] { 0, 2, 1 }; 049 var_indices[5] = new int[] { 1, 2, 0 }; 050 var_indices[6] = new int[] { 2, 1, 0 }; 051 } 052 053 protected FunctionBinaryFloat(PptSlice ppt) { 054 super(ppt); 055 } 056 057 protected @Prototype FunctionBinaryFloat() { 058 super(); 059 } 060 061 /** returns whether or not this invariant is enabled */ 062 @Override 063 public boolean enabled() { 064 return dkconfig_enabled; 065 } 066 067 /** FunctionBinaryFloat is only valid on isFloat() types. */ 068 @Override 069 public boolean instantiate_ok(VarInfo[] vis) { 070 071 if (!valid_types(vis)) { 072 return false; 073 } 074 075 // Make sure that each variable is integral (not boolean or hashcode) 076 if (!vis[0].file_rep_type.isFloat() 077 || !vis[1].file_rep_type.isFloat() 078 || !vis[2].file_rep_type.isFloat()) 079 return false; 080 081 return true; 082 } 083 084 // check_modified relies on func having no side effects. 085 abstract double func(double arg1, double arg2); 086 @Pure 087 abstract boolean is_symmetric(); 088 abstract String[] get_method_name(@GuardSatisfied FunctionBinaryFloat this); 089 abstract int get_var_order(@GuardSatisfied FunctionBinaryFloat this); 090 abstract void set_function_id(int function_id); 091 abstract int get_function_id(); 092 093 /** 094 * Map from function name (eg, MultiplyLong, MinimumFloat) to an array of instances (one for each 095 * valid permutation) for that function. 096 */ 097 private static Map<String,@Prototype FunctionBinaryFloat[]> functions = new LinkedHashMap<>(); 098 099 /** 100 * A list indexed by function number to an array of instances (one for each valid permutation) for 101 * that function. The array is the same one as is stored in the functions Map. This provides a 102 * faster access mechanism once we have the function id (which are calculated the first time 103 * through). 104 */ 105 private static List<@Prototype FunctionBinaryFloat[]> func_list = new ArrayList<>(); 106 107 private static void build_func_list() { 108 109 // Reflection seems to confuse clover 110 ///CLOVER:OFF 111 112 // Build the map of functions to array of instances for that function 113 debug.fine("Processing FunctionBinaryFloat"); 114 functions = new LinkedHashMap<>(); 115 @SuppressWarnings("unchecked") 116 Class<@Prototype FunctionBinaryFloat>[] subclasses = (Class<@Prototype FunctionBinaryFloat>[]) FunctionBinaryFloat.class.getDeclaredClasses(); 117 for (int ii = 0; ii < subclasses.length; ii++) { 118 Class<@Prototype FunctionBinaryFloat> subc = subclasses[ii]; 119 String function = subc.getName(); 120 if (function.indexOf("CLOVER") >= 0) { 121 continue; 122 } 123 function = function.replaceFirst(".*FunctionBinary\\$", ""); 124 function = function.replaceFirst("_.*", ""); 125 if (function.equals("SubClass")) { 126 continue; 127 } 128 @Prototype FunctionBinaryFloat[] fb_arr = functions.get(function); 129 if (fb_arr == null) { 130 fb_arr = new @Prototype FunctionBinaryFloat[7]; 131 functions.put(function, fb_arr); 132 func_list.add(fb_arr); 133 } 134 int func_id = func_list.indexOf(fb_arr); 135 @SuppressWarnings({"nonprototype"}) 136 @Prototype FunctionBinaryFloat fb; 137 try { 138 Constructor<@Prototype FunctionBinaryFloat> con = subc.getDeclaredConstructor(new Class<?>[] {}); 139 fb = con.newInstance(new Object[] {}); 140 } catch (Exception e) { 141 throw new Error(" can't create instance for " + subc.getName() 142 + ": '" + e + "' ii = " + ii); 143 } 144 assert fb_arr[fb.get_var_order()] == null; 145 fb_arr[fb.get_var_order()] = fb; 146 fb.set_function_id(func_id); 147 debug.fine("Adding " + function + " " + fb.getClass().getName() 148 + " " + fb.get_var_order() + " " + fb.get_function_id()); 149 } 150 ///CLOVER:ON 151 } 152 153 /** Returns a list of all of the FunctionBinaryFloat prototype invariants. */ 154 public static List<@Prototype Invariant> get_proto_all() { 155 156 List<@Prototype Invariant> result = new ArrayList<>(); 157 158 // If this is the first call 159 if (functions.isEmpty()) { 160 build_func_list(); 161 } 162 163 // Get the proto invariant for all of the subclasses and return them 164 for (@Prototype FunctionBinaryFloat[] fb_arr : func_list) { 165 for (int jj = 1; jj < fb_arr.length; jj++) { 166 @Prototype FunctionBinaryFloat fb = fb_arr[jj]; 167 if (fb != null) { 168 result.add(fb); 169 } 170 } 171 } 172 return result; 173 } 174 175 /** Permuted result var. */ 176 public VarInfo resultVar() { 177 return ppt.var_infos[var_indices[get_var_order()][0]]; 178 } 179 180 /** Permuted arg1 var. */ 181 public VarInfo argVar1() { 182 return ppt.var_infos[var_indices[get_var_order()][1]]; 183 } 184 185 /** Permuted arg2 var. */ 186 public VarInfo argVar2() { 187 return ppt.var_infos[var_indices[get_var_order()][2]]; 188 } 189 190 /** 191 * Apply the specified sample to the function, returning the result. The caller is responsible 192 * for permuting the arguments. 193 */ 194 public InvariantStatus check_ordered(double result, double arg1, 195 double arg2, int count) { 196 // This implementation relies on func having no side effects. 197 try { 198 if (!Global.fuzzy.eq(result, func(arg1, arg2))) { 199 return InvariantStatus.FALSIFIED; 200 } 201 } catch (Exception e) { 202 return InvariantStatus.FALSIFIED; 203 } 204 return InvariantStatus.NO_CHANGE; 205 } 206 207 /** 208 * Apply the specified sample to the function, returning the result. The caller is responsible 209 * for permuting the arguments. 210 */ 211 public InvariantStatus add_ordered(double result, double arg1, 212 double arg2, int count) { 213 return check_ordered(result, arg1, arg2, count); 214 } 215 216 /** 217 * Reorganize our already-seen state as if the variables had shifted order underneath us 218 * (re-arrangement given by the permutation). We accomplish this by returning the class that 219 * corresponds to the new permutation. 220 */ 221 @Override 222 protected Invariant resurrect_done(int[] permutation) { 223 224 assert permutation.length == 3; 225 assert ArraysPlume.fnIsPermutation(permutation); 226 227 int[] new_order = new int[3]; 228 int[] old_order = var_indices[get_var_order()]; 229 230 // "permutation" is a permutation on the var_info array. old_order 231 // was the permutation that took the formatted invariant to the 232 // var_info array, so old_order^-1 is the permutation from the 233 // var_info array to the old formatted invariant. We want to find 234 // a new_order so that when we first do "permutation", then 235 // apply the new permutation from the var_info array to the 236 // formatted invariant, we get the same formatted invariant. 237 // What we want, then. is: 238 // new_order^-1 o permutation = old_order^-1 239 // rearranging, this is equivalent to 240 // new_order = permutation o old_order 241 new_order[0] = permutation[old_order[0]]; 242 new_order[1] = permutation[old_order[1]]; 243 new_order[2] = permutation[old_order[2]]; 244 245 // Force symmetric functions into a canonical form so that 246 // we can match them when necessary and they always print the same. 247 // For example, order of 0, 1, 2 and 0, 2, 1 represent the same 248 // invariant for a symmetric function. This forces them to always 249 // be represented as 0, 1, 2 250 if (is_symmetric()) { 251 if (new_order[2] < new_order[1]) { 252 int tmp = new_order[2]; 253 new_order[2] = new_order[1]; 254 new_order[1] = tmp; 255 } 256 } 257 258 // Look for the new order in the list of possible orders 259 int var_order = -1; 260 for (int i = 0; i < var_indices.length; i++) { 261 if (Arrays.equals(new_order, var_indices[i])) { 262 var_order = i; 263 break; 264 } 265 } 266 assert var_order != -1; 267 268 // If the var order hasn't changed, we don't need to do anything 269 if (var_order == get_var_order()) { 270 return this; 271 } 272 273 // Find the class that corresponds to the new order 274 if (functions.isEmpty()) { 275 build_func_list(); 276 } 277 int func_id = get_function_id(); 278 @Prototype FunctionBinaryFloat[] fb_arr = func_list.get(func_id); 279 assert fb_arr != null; 280 for (int ii = 0; ii < fb_arr.length; ii++) { 281 if ((fb_arr[ii] != null) && (fb_arr[ii].get_var_order() == var_order)) { 282 return fb_arr[ii].instantiate_dyn(ppt); 283 } 284 } 285 286 throw new Error("Could not find new ordering"); 287 } 288 289 @Override 290 public String repr(@GuardSatisfied FunctionBinaryFloat this) { 291 return format(); 292 } 293 294 @SideEffectFree 295 @Override 296 public String format_using(@GuardSatisfied FunctionBinaryFloat this, OutputFormat format) { 297 if (format == OutputFormat.SIMPLIFY) { 298 return format_simplify(); 299 } 300 if (format == OutputFormat.CSHARPCONTRACT) { 301 return format_csharp_contract(); 302 } 303 304 int var_order = get_var_order(); 305 String[] methodname = get_method_name(); 306 307 VarInfo argresultvi = ppt.var_infos[var_indices[var_order][0]]; 308 VarInfo arg1vi = ppt.var_infos[var_indices[var_order][1]]; 309 VarInfo arg2vi = ppt.var_infos[var_indices[var_order][2]]; 310 311 String argresult_name = argresultvi.name_using(format); 312 String arg1_name = arg1vi.name_using(format); 313 String arg2_name = arg2vi.name_using(format); 314 315 if (format == OutputFormat.DAIKON) { 316 return argresult_name + " == (" + methodname[0] + arg1_name 317 + methodname[1] + arg2_name + methodname[2] + ")"; 318 } 319 320 if (format.isJavaFamily()) { 321 if (methodname[1].equals(" || ") || methodname[1].equals(" && ")) { 322 return "(" + argresult_name + " != 0) == ((" + methodname[0] + arg1_name + " != 0)" 323 + methodname[1] + "(" + arg2_name + methodname[2] + " != 0))"; 324 } else { 325 return argresult_name + " == (" + methodname[0] + arg1_name 326 + methodname[1] + arg2_name + methodname[2] + ")"; 327 } 328 } 329 330 return format_unimplemented(format); 331 } 332 333 public String format_simplify(@GuardSatisfied FunctionBinaryFloat this) { 334 int var_order = get_var_order(); 335 String[] methodname = get_method_name(); 336 VarInfo[] vis = ppt.var_infos; 337 338 String result = vis[var_indices[var_order][0]].simplifyFixedupName(); 339 String arg1 = vis[var_indices[var_order][1]].simplifyFixedupName(); 340 String arg2 = vis[var_indices[var_order][2]].simplifyFixedupName(); 341 String func = null; 342 if (methodname[1].equals(" * ")) { 343 func = "*"; 344 } else if (methodname[1].equals(" | ")) { 345 func = "|java-bitwise-or|"; 346 } else if (methodname[1].equals(" || ")) { 347 func = "|java-logical-or|"; 348 } else if (methodname[1].equals(", ")) { 349 if (methodname[0].equals("java.lang.Math.min(")) { 350 func = "min"; 351 } else if (methodname[0].equals("java.lang.Math.max(")) { 352 func = "max"; 353 } else if (methodname[0].equals("org.plumelib.util.MathPlume.gcd(")) { 354 func = "gcd"; 355 } else if (methodname[0].equals("java.lang.Math.pow(")) { 356 func = "pow"; 357 } else if (methodname[0].equals("org.plumelib.util.MathPlume.logicalXor(")) { 358 func = "|java-logical-xor|"; 359 } 360 } else { 361 assert methodname[0].equals(""); 362 assert methodname[2].equals(""); 363 func = "|java-" + methodname[1].trim() + "|"; 364 } 365 if (func == null) { 366 return "format_simplify_contract() doesn't know function " + methodname[0] + "-" 367 + methodname[1] + "-" + methodname[2]; 368 } 369 return "(EQ " + result + " (" + func + " " + arg1 + " " + arg2 + "))"; 370 } 371 372 public String format_csharp_contract(@GuardSatisfied FunctionBinaryFloat this) { 373 int var_order = get_var_order(); 374 String[] methodname = get_method_name(); 375 376 VarInfo argresultvi = ppt.var_infos[var_indices[var_order][0]]; 377 VarInfo arg1vi = ppt.var_infos[var_indices[var_order][1]]; 378 VarInfo arg2vi = ppt.var_infos[var_indices[var_order][2]]; 379 String result = argresultvi.csharp_name(); 380 String arg1 = arg1vi.csharp_name(); 381 String arg2 = arg2vi.csharp_name(); 382 String operator = null; 383 384 if (methodname[1].equals(" * ")) { 385 operator = "*"; 386 } else if (methodname[1].equals(" | ")) { 387 operator = "|"; 388 } else if (methodname[1].equals(" & ")) { 389 operator = "&"; 390 } else if (methodname[1].equals(" / ")) { 391 operator = "/"; 392 } else if (methodname[1].equals(" ^ ")) { 393 operator = "^"; 394 } else if (methodname[1].equals(" % ")) { 395 operator = "%"; 396 } else if (methodname[1].equals(" && ")) { 397 operator = "&&"; 398 } else if (methodname[1].equals(" || ")) { 399 operator = "||"; 400 } else if (methodname[1].equals(" >> ")) { 401 operator = ">>"; 402 } else if (methodname[1].equals(" >>> ")) { 403 return result + " == " + arg1 + ".UnsignedRightShift(" + arg2 + ")"; 404 //return result + " == CSharpDaikonLib.Extensions.UnsignedRightShift(" + arg1 + ", " + arg2 + ")"; 405 } else if (methodname[1].equals(" << ")) { 406 operator = "<<"; 407 } 408 409 if (operator != null) { 410 return result + " == (" + arg1 + " " + operator + " " + arg2 + ")"; 411 } 412 413 String func = null; 414 if (methodname[1].equals(", ")) { 415 if (methodname[0].equals("java.lang.Math.min(")) { 416 func = "Math.Min"; 417 } else if (methodname[0].equals("java.lang.Math.max(")) { 418 func = "Math.Max"; 419 } else if (methodname[0].equals("org.plumelib.util.MathPlume.gcd(")) { 420 return result + " == CSharpDaikonLib.Extensions.GCD(" + arg1 + ", " + arg2 + ")"; 421 } else if (methodname[0].equals("java.lang.Math.pow(")) { 422 return result + " == " + arg1 + ".Pow(" + arg2 + ")"; 423 } else if (methodname[0].equals("org.plumelib.util.MathPlume.logicalXor(")) { 424 return result + " == (" + arg1 + " ^ " + arg2 + ")"; 425 } 426 } else { 427 assert methodname[0].equals(""); 428 assert methodname[2].equals(""); 429 func = "|" + methodname[1].trim() + "|"; 430 } 431 432 if (func == null) { 433 return "format_csharp_contract() doesn't know function " + methodname[0] + "-" + methodname[1] + "-" + methodname[2]; 434 } 435 return result + " == " + func + "(" + arg1 + ", " + arg2 + ")"; 436 } 437 438 // If our classes match, we must match 439 @Pure 440 @Override 441 public boolean isSameFormula(Invariant other) { 442 return true; 443 } 444 @Override 445 public double computeConfidence() { 446 if (logOn()) { 447 VarInfo v1 = ppt.var_infos[0]; 448 VarInfo v2 = ppt.var_infos[1]; 449 VarInfo v3 = ppt.var_infos[2]; 450 log("computeConfidence(%s: num_values = %s, num_values(%s)=%s, num_values(%s)=%s, num_values(%s)=%s", 451 format(), ppt.num_values(), 452 v1.name(), ppt.parent.num_values(v1), 453 v2.name(), ppt.parent.num_values(v2), 454 v3.name(), ppt.parent.num_values(v3)); 455 } 456 return Invariant.conf_is_ge(ppt.num_values(), 5); 457 } 458 459 /** If the arg is a sequence size, return the sequence; otherwise return null. */ 460 private @Nullable VarInfo sized_sequence(VarInfo size) { 461 if (size.derived instanceof SequenceLength) { 462 return ((SequenceLength)size.derived).base; 463 } 464 return null; 465 } 466 467 @Pure 468 @Override 469 public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) { 470 471 DiscardInfo super_result = super.isObviousDynamically(vis); 472 if (super_result != null) { 473 return super_result; 474 } 475 476 // Discard if any two of the three variables are the sizes of the 477 // same arrays. 478 VarInfo arr1 = sized_sequence(vis[0]); 479 VarInfo arr2 = sized_sequence(vis[1]); 480 VarInfo arr3 = sized_sequence(vis[2]); 481 if (((arr1 != null) && (arr1 == arr2)) 482 || ((arr1 != null) && (arr1 == arr3)) 483 || ((arr2 != null) && (arr2 == arr3))) { 484 return new DiscardInfo(this, DiscardCode.obvious, 485 "two are sizes of same array: " 486 + vis[0].name() + " " 487 + vis[1].name() + " " 488 + vis[2].name()); 489 } 490 491 return null; 492 } 493 494 // default is that it is not this function, overriden in the subclass 495 @Pure 496 public boolean isMultiply() { 497 return false; 498 } 499 500/** 501 * Represents the invariant {@code x = Multiply(y, z)} over three double 502 * scalars. 503 */ 504public static class MultiplyDouble_xyz extends FunctionBinaryFloat { 505 // We are Serializable, so we specify a version to allow changes to 506 // method signatures without breaking serialization. If you add or 507 // remove fields, you should change this number to the current date. 508 static final long serialVersionUID = 20031030L; 509 510 private static @Prototype MultiplyDouble_xyz proto = new @Prototype MultiplyDouble_xyz (); 511 512 /** Returns the prototype invariant for MultiplyDouble_xyz */ 513 public static @Prototype MultiplyDouble_xyz get_proto() { 514 return proto; 515 } 516 517 /** instantiate an invariant on the specified slice */ 518 @Override 519 protected MultiplyDouble_xyz instantiate_dyn(@Prototype MultiplyDouble_xyz this, PptSlice slice) { 520 return new MultiplyDouble_xyz (slice); 521 } 522 523 private MultiplyDouble_xyz (PptSlice slice) { 524 super(slice); 525 } 526 527 public @Prototype MultiplyDouble_xyz () { 528 super(); 529 } 530 531 private static String[] method_name = new String[] {"", " * ", ""}; 532 533 @Override 534 public String[] get_method_name(@GuardSatisfied MultiplyDouble_xyz this) { 535 return method_name; 536 } 537 538 private static int function_id = -1; 539 540 @Override 541 public int get_function_id() { 542 return function_id; 543 } 544 545 @Override 546 public void set_function_id(int function_id) { 547 assert MultiplyDouble_xyz.function_id == -1; 548 MultiplyDouble_xyz.function_id = function_id; 549 } 550 551 private static int var_order = 1; 552 553 @Override 554 public int get_var_order(@GuardSatisfied MultiplyDouble_xyz this) { 555 return var_order; 556 } 557 558 @Pure 559 @Override 560 public boolean is_symmetric() { 561 562 return true; 563 } 564 565 @Override 566 567 public double func(double y, double z) { 568 569 return y * z; 570 } 571 572 @Override 573 public InvariantStatus check_modified(double x, double y, 574 double z, int count) { 575 return check_ordered(x, y, z, count); 576 } 577 578 @Override 579 public InvariantStatus add_modified(double x, double y, 580 double z, int count) { 581 if (Debug.logDetail()) { 582 log("result=%s, arg1=%s, arg2=%s", x, y, z); 583 } 584 return add_ordered(x, y, z, count); 585 } 586 587 @Pure 588 @Override 589 public boolean isMultiply() { 590 return true; 591 } 592 593 @Pure 594 @Override 595 public boolean isExact() { 596 return true; 597 } 598 599 /** Returns a list of non-instantiating suppressions for this invariant. */ 600 @Pure 601 @Override 602 public @Nullable NISuppressionSet get_ni_suppressions() { 603 if (NIS.dkconfig_enabled && dkconfig_enabled) { 604 return suppressions; 605 } else { 606 return null; 607 } 608 } 609 610 /** definition of this invariant (the suppressee) */ 611 private static NISuppressee suppressee = new NISuppressee(MultiplyDouble_xyz.class, 3); 612 613 // suppressor definitions (used below) 614 private static NISuppressor result_eq_arg1 = 615 new NISuppressor(0, 1, FloatEqual.class); 616 private static NISuppressor result_eq_arg2 = 617 new NISuppressor(0, 2, FloatEqual.class); 618 private static NISuppressor arg1_eq_arg2 = 619 new NISuppressor(1, 2, FloatEqual.class); 620 621 private static NISuppressor result_lt_arg1 = 622 new NISuppressor(0, 1, FloatLessThan.class); 623 private static NISuppressor result_lt_arg2 = 624 new NISuppressor(0, 2, FloatLessThan.class); 625 private static NISuppressor arg1_lt_arg2 = 626 new NISuppressor(1, 2, FloatLessThan.class); 627 private static NISuppressor arg2_lt_arg1 = 628 new NISuppressor(2, 1, FloatLessThan.class); 629 630 private static NISuppressor result_le_arg1 = 631 new NISuppressor(0, 1, FloatLessEqual.class); 632 private static NISuppressor result_le_arg2 = 633 new NISuppressor(0, 2, FloatLessEqual.class); 634 private static NISuppressor arg1_le_arg2 = 635 new NISuppressor(1, 2, FloatLessEqual.class); 636 private static NISuppressor arg2_le_arg1 = 637 new NISuppressor(2, 1, FloatLessEqual.class); 638 639 private static NISuppressor result_track0_arg1 = 640 new NISuppressor(0, 1, NumericInt.ZeroTrack.class); 641 private static NISuppressor result_track0_arg2 = 642 new NISuppressor(0, 2, NumericInt.ZeroTrack.class); 643 private static NISuppressor arg1_track0_arg2 = 644 new NISuppressor(1, 2, NumericInt.ZeroTrack.class); 645 private static NISuppressor arg1_track0_result = 646 new NISuppressor(1, 0, NumericInt.ZeroTrack.class); 647 private static NISuppressor arg2_track0_result = 648 new NISuppressor(2, 0, NumericInt.ZeroTrack.class); 649 private static NISuppressor arg2_track0_arg1 = 650 new NISuppressor(2, 1, NumericInt.ZeroTrack.class); 651 652 private static NISuppressor result_eq_1 = 653 new NISuppressor(0, RangeFloat.EqualOne.class); 654 private static NISuppressor arg1_eq_1 = 655 new NISuppressor(1, RangeFloat.EqualOne.class); 656 private static NISuppressor arg2_eq_1 = 657 new NISuppressor(2, RangeFloat.EqualOne.class); 658 659 private static NISuppressor result_eq_0 = 660 new NISuppressor(0, RangeFloat.EqualZero.class); 661 private static NISuppressor arg1_eq_0 = 662 new NISuppressor(1, RangeFloat.EqualZero.class); 663 private static NISuppressor arg2_eq_0 = 664 new NISuppressor(2, RangeFloat.EqualZero.class); 665 666 private static NISuppressor result_ne_0 = 667 new NISuppressor(0, NonZeroFloat.class); 668 private static NISuppressor arg1_ne_0 = 669 new NISuppressor(1, NonZeroFloat.class); 670 private static NISuppressor arg2_ne_0 = 671 new NISuppressor(2, NonZeroFloat.class); 672 673 private static NISuppressor result_ge_0 = 674 new NISuppressor(0, RangeFloat.GreaterEqualZero.class); 675 private static NISuppressor arg1_ge_0 = 676 new NISuppressor(1, RangeFloat.GreaterEqualZero.class); 677 private static NISuppressor arg2_ge_0 = 678 new NISuppressor(2, RangeFloat.GreaterEqualZero.class); 679 680 private static NISuppressor result_ge_64 = 681 new NISuppressor(0, RangeInt.GreaterEqual64.class); 682 private static NISuppressor arg1_ge_64 = 683 new NISuppressor(1, RangeInt.GreaterEqual64.class); 684 private static NISuppressor arg2_ge_64 = 685 new NISuppressor(2, RangeInt.GreaterEqual64.class); 686 687 private static NISuppressionSet suppressions = 688 new NISuppressionSet( 689 new NISuppression[] { 690 691 // (r == 0) && (y == 0) ==> r = y * z 692 new NISuppression(result_eq_0, arg1_eq_0, suppressee), 693 694 // (r == 0) && (z == 0) ==> r = y * z 695 new NISuppression(result_eq_0, arg2_eq_0, suppressee), 696 697 // (r == y) && (z == 1) ==> r = y * z 698 new NISuppression(result_eq_arg1, arg2_eq_1, suppressee), 699 700 // (r == z) && (y == 1) ==> r = y * z 701 new NISuppression(result_eq_arg2, arg1_eq_1, suppressee), 702 703 }); 704 705 // Create a suppression factory for functionBinary 706 707} 708 709/** 710 * Represents the invariant {@code y = Multiply(x, z)} over three double 711 * scalars. 712 */ 713public static class MultiplyDouble_yxz extends FunctionBinaryFloat { 714 // We are Serializable, so we specify a version to allow changes to 715 // method signatures without breaking serialization. If you add or 716 // remove fields, you should change this number to the current date. 717 static final long serialVersionUID = 20031030L; 718 719 private static @Prototype MultiplyDouble_yxz proto = new @Prototype MultiplyDouble_yxz (); 720 721 /** Returns the prototype invariant for MultiplyDouble_yxz */ 722 public static @Prototype MultiplyDouble_yxz get_proto() { 723 return proto; 724 } 725 726 /** instantiate an invariant on the specified slice */ 727 @Override 728 protected MultiplyDouble_yxz instantiate_dyn(@Prototype MultiplyDouble_yxz this, PptSlice slice) { 729 return new MultiplyDouble_yxz (slice); 730 } 731 732 private MultiplyDouble_yxz (PptSlice slice) { 733 super(slice); 734 } 735 736 public @Prototype MultiplyDouble_yxz () { 737 super(); 738 } 739 740 private static String[] method_name = new String[] {"", " * ", ""}; 741 742 @Override 743 public String[] get_method_name(@GuardSatisfied MultiplyDouble_yxz this) { 744 return method_name; 745 } 746 747 private static int function_id = -1; 748 749 @Override 750 public int get_function_id() { 751 return function_id; 752 } 753 754 @Override 755 public void set_function_id(int function_id) { 756 assert MultiplyDouble_yxz.function_id == -1; 757 MultiplyDouble_yxz.function_id = function_id; 758 } 759 760 private static int var_order = 2; 761 762 @Override 763 public int get_var_order(@GuardSatisfied MultiplyDouble_yxz this) { 764 return var_order; 765 } 766 767 @Pure 768 @Override 769 public boolean is_symmetric() { 770 771 return true; 772 } 773 774 @Override 775 776 public double func(double x, double z) { 777 778 return x * z; 779 } 780 781 @Override 782 public InvariantStatus check_modified(double x, double y, 783 double z, int count) { 784 return check_ordered(y, x, z, count); 785 } 786 787 @Override 788 public InvariantStatus add_modified(double x, double y, 789 double z, int count) { 790 if (Debug.logDetail()) { 791 log("result=%s, arg1=%s, arg2=%s", y, x, z); 792 } 793 return add_ordered(y, x, z, count); 794 } 795 796 @Pure 797 @Override 798 public boolean isMultiply() { 799 return true; 800 } 801 802 @Pure 803 @Override 804 public boolean isExact() { 805 return true; 806 } 807 808 /** Returns a list of non-instantiating suppressions for this invariant. */ 809 @Pure 810 @Override 811 public @Nullable NISuppressionSet get_ni_suppressions() { 812 if (NIS.dkconfig_enabled && dkconfig_enabled) { 813 return suppressions; 814 } else { 815 return null; 816 } 817 } 818 819 /** definition of this invariant (the suppressee) */ 820 private static NISuppressee suppressee = new NISuppressee(MultiplyDouble_yxz.class, 3); 821 822 // suppressor definitions (used below) 823 private static NISuppressor result_eq_arg1 = 824 new NISuppressor(1, 0, FloatEqual.class); 825 private static NISuppressor result_eq_arg2 = 826 new NISuppressor(1, 2, FloatEqual.class); 827 private static NISuppressor arg1_eq_arg2 = 828 new NISuppressor(0, 2, FloatEqual.class); 829 830 private static NISuppressor result_lt_arg1 = 831 new NISuppressor(1, 0, FloatLessThan.class); 832 private static NISuppressor result_lt_arg2 = 833 new NISuppressor(1, 2, FloatLessThan.class); 834 private static NISuppressor arg1_lt_arg2 = 835 new NISuppressor(0, 2, FloatLessThan.class); 836 private static NISuppressor arg2_lt_arg1 = 837 new NISuppressor(2, 0, FloatLessThan.class); 838 839 private static NISuppressor result_le_arg1 = 840 new NISuppressor(1, 0, FloatLessEqual.class); 841 private static NISuppressor result_le_arg2 = 842 new NISuppressor(1, 2, FloatLessEqual.class); 843 private static NISuppressor arg1_le_arg2 = 844 new NISuppressor(0, 2, FloatLessEqual.class); 845 private static NISuppressor arg2_le_arg1 = 846 new NISuppressor(2, 0, FloatLessEqual.class); 847 848 private static NISuppressor result_track0_arg1 = 849 new NISuppressor(1, 0, NumericInt.ZeroTrack.class); 850 private static NISuppressor result_track0_arg2 = 851 new NISuppressor(1, 2, NumericInt.ZeroTrack.class); 852 private static NISuppressor arg1_track0_arg2 = 853 new NISuppressor(0, 2, NumericInt.ZeroTrack.class); 854 private static NISuppressor arg1_track0_result = 855 new NISuppressor(0, 1, NumericInt.ZeroTrack.class); 856 private static NISuppressor arg2_track0_result = 857 new NISuppressor(2, 1, NumericInt.ZeroTrack.class); 858 private static NISuppressor arg2_track0_arg1 = 859 new NISuppressor(2, 0, NumericInt.ZeroTrack.class); 860 861 private static NISuppressor result_eq_1 = 862 new NISuppressor(1, RangeFloat.EqualOne.class); 863 private static NISuppressor arg1_eq_1 = 864 new NISuppressor(0, RangeFloat.EqualOne.class); 865 private static NISuppressor arg2_eq_1 = 866 new NISuppressor(2, RangeFloat.EqualOne.class); 867 868 private static NISuppressor result_eq_0 = 869 new NISuppressor(1, RangeFloat.EqualZero.class); 870 private static NISuppressor arg1_eq_0 = 871 new NISuppressor(0, RangeFloat.EqualZero.class); 872 private static NISuppressor arg2_eq_0 = 873 new NISuppressor(2, RangeFloat.EqualZero.class); 874 875 private static NISuppressor result_ne_0 = 876 new NISuppressor(1, NonZeroFloat.class); 877 private static NISuppressor arg1_ne_0 = 878 new NISuppressor(0, NonZeroFloat.class); 879 private static NISuppressor arg2_ne_0 = 880 new NISuppressor(2, NonZeroFloat.class); 881 882 private static NISuppressor result_ge_0 = 883 new NISuppressor(1, RangeFloat.GreaterEqualZero.class); 884 private static NISuppressor arg1_ge_0 = 885 new NISuppressor(0, RangeFloat.GreaterEqualZero.class); 886 private static NISuppressor arg2_ge_0 = 887 new NISuppressor(2, RangeFloat.GreaterEqualZero.class); 888 889 private static NISuppressor result_ge_64 = 890 new NISuppressor(1, RangeInt.GreaterEqual64.class); 891 private static NISuppressor arg1_ge_64 = 892 new NISuppressor(0, RangeInt.GreaterEqual64.class); 893 private static NISuppressor arg2_ge_64 = 894 new NISuppressor(2, RangeInt.GreaterEqual64.class); 895 896 private static NISuppressionSet suppressions = 897 new NISuppressionSet( 898 new NISuppression[] { 899 900 // (r == 0) && (x == 0) ==> r = x * z 901 new NISuppression(result_eq_0, arg1_eq_0, suppressee), 902 903 // (r == 0) && (z == 0) ==> r = x * z 904 new NISuppression(result_eq_0, arg2_eq_0, suppressee), 905 906 // (r == x) && (z == 1) ==> r = x * z 907 new NISuppression(result_eq_arg1, arg2_eq_1, suppressee), 908 909 // (r == z) && (x == 1) ==> r = x * z 910 new NISuppression(result_eq_arg2, arg1_eq_1, suppressee), 911 912 }); 913 914 // Create a suppression factory for functionBinary 915 916} 917 918/** 919 * Represents the invariant {@code z = Multiply(x, y)} over three double 920 * scalars. 921 */ 922public static class MultiplyDouble_zxy extends FunctionBinaryFloat { 923 // We are Serializable, so we specify a version to allow changes to 924 // method signatures without breaking serialization. If you add or 925 // remove fields, you should change this number to the current date. 926 static final long serialVersionUID = 20031030L; 927 928 private static @Prototype MultiplyDouble_zxy proto = new @Prototype MultiplyDouble_zxy (); 929 930 /** Returns the prototype invariant for MultiplyDouble_zxy */ 931 public static @Prototype MultiplyDouble_zxy get_proto() { 932 return proto; 933 } 934 935 /** instantiate an invariant on the specified slice */ 936 @Override 937 protected MultiplyDouble_zxy instantiate_dyn(@Prototype MultiplyDouble_zxy this, PptSlice slice) { 938 return new MultiplyDouble_zxy (slice); 939 } 940 941 private MultiplyDouble_zxy (PptSlice slice) { 942 super(slice); 943 } 944 945 public @Prototype MultiplyDouble_zxy () { 946 super(); 947 } 948 949 private static String[] method_name = new String[] {"", " * ", ""}; 950 951 @Override 952 public String[] get_method_name(@GuardSatisfied MultiplyDouble_zxy this) { 953 return method_name; 954 } 955 956 private static int function_id = -1; 957 958 @Override 959 public int get_function_id() { 960 return function_id; 961 } 962 963 @Override 964 public void set_function_id(int function_id) { 965 assert MultiplyDouble_zxy.function_id == -1; 966 MultiplyDouble_zxy.function_id = function_id; 967 } 968 969 private static int var_order = 3; 970 971 @Override 972 public int get_var_order(@GuardSatisfied MultiplyDouble_zxy this) { 973 return var_order; 974 } 975 976 @Pure 977 @Override 978 public boolean is_symmetric() { 979 980 return true; 981 } 982 983 @Override 984 985 public double func(double x, double y) { 986 987 return x * y; 988 } 989 990 @Override 991 public InvariantStatus check_modified(double x, double y, 992 double z, int count) { 993 return check_ordered(z, x, y, count); 994 } 995 996 @Override 997 public InvariantStatus add_modified(double x, double y, 998 double z, int count) { 999 if (Debug.logDetail()) { 1000 log("result=%s, arg1=%s, arg2=%s", z, x, y); 1001 } 1002 return add_ordered(z, x, y, count); 1003 } 1004 1005 @Pure 1006 @Override 1007 public boolean isMultiply() { 1008 return true; 1009 } 1010 1011 @Pure 1012 @Override 1013 public boolean isExact() { 1014 return true; 1015 } 1016 1017 /** Returns a list of non-instantiating suppressions for this invariant. */ 1018 @Pure 1019 @Override 1020 public @Nullable NISuppressionSet get_ni_suppressions() { 1021 if (NIS.dkconfig_enabled && dkconfig_enabled) { 1022 return suppressions; 1023 } else { 1024 return null; 1025 } 1026 } 1027 1028 /** definition of this invariant (the suppressee) */ 1029 private static NISuppressee suppressee = new NISuppressee(MultiplyDouble_zxy.class, 3); 1030 1031 // suppressor definitions (used below) 1032 private static NISuppressor result_eq_arg1 = 1033 new NISuppressor(2, 0, FloatEqual.class); 1034 private static NISuppressor result_eq_arg2 = 1035 new NISuppressor(2, 1, FloatEqual.class); 1036 private static NISuppressor arg1_eq_arg2 = 1037 new NISuppressor(0, 1, FloatEqual.class); 1038 1039 private static NISuppressor result_lt_arg1 = 1040 new NISuppressor(2, 0, FloatLessThan.class); 1041 private static NISuppressor result_lt_arg2 = 1042 new NISuppressor(2, 1, FloatLessThan.class); 1043 private static NISuppressor arg1_lt_arg2 = 1044 new NISuppressor(0, 1, FloatLessThan.class); 1045 private static NISuppressor arg2_lt_arg1 = 1046 new NISuppressor(1, 0, FloatLessThan.class); 1047 1048 private static NISuppressor result_le_arg1 = 1049 new NISuppressor(2, 0, FloatLessEqual.class); 1050 private static NISuppressor result_le_arg2 = 1051 new NISuppressor(2, 1, FloatLessEqual.class); 1052 private static NISuppressor arg1_le_arg2 = 1053 new NISuppressor(0, 1, FloatLessEqual.class); 1054 private static NISuppressor arg2_le_arg1 = 1055 new NISuppressor(1, 0, FloatLessEqual.class); 1056 1057 private static NISuppressor result_track0_arg1 = 1058 new NISuppressor(2, 0, NumericInt.ZeroTrack.class); 1059 private static NISuppressor result_track0_arg2 = 1060 new NISuppressor(2, 1, NumericInt.ZeroTrack.class); 1061 private static NISuppressor arg1_track0_arg2 = 1062 new NISuppressor(0, 1, NumericInt.ZeroTrack.class); 1063 private static NISuppressor arg1_track0_result = 1064 new NISuppressor(0, 2, NumericInt.ZeroTrack.class); 1065 private static NISuppressor arg2_track0_result = 1066 new NISuppressor(1, 2, NumericInt.ZeroTrack.class); 1067 private static NISuppressor arg2_track0_arg1 = 1068 new NISuppressor(1, 0, NumericInt.ZeroTrack.class); 1069 1070 private static NISuppressor result_eq_1 = 1071 new NISuppressor(2, RangeFloat.EqualOne.class); 1072 private static NISuppressor arg1_eq_1 = 1073 new NISuppressor(0, RangeFloat.EqualOne.class); 1074 private static NISuppressor arg2_eq_1 = 1075 new NISuppressor(1, RangeFloat.EqualOne.class); 1076 1077 private static NISuppressor result_eq_0 = 1078 new NISuppressor(2, RangeFloat.EqualZero.class); 1079 private static NISuppressor arg1_eq_0 = 1080 new NISuppressor(0, RangeFloat.EqualZero.class); 1081 private static NISuppressor arg2_eq_0 = 1082 new NISuppressor(1, RangeFloat.EqualZero.class); 1083 1084 private static NISuppressor result_ne_0 = 1085 new NISuppressor(2, NonZeroFloat.class); 1086 private static NISuppressor arg1_ne_0 = 1087 new NISuppressor(0, NonZeroFloat.class); 1088 private static NISuppressor arg2_ne_0 = 1089 new NISuppressor(1, NonZeroFloat.class); 1090 1091 private static NISuppressor result_ge_0 = 1092 new NISuppressor(2, RangeFloat.GreaterEqualZero.class); 1093 private static NISuppressor arg1_ge_0 = 1094 new NISuppressor(0, RangeFloat.GreaterEqualZero.class); 1095 private static NISuppressor arg2_ge_0 = 1096 new NISuppressor(1, RangeFloat.GreaterEqualZero.class); 1097 1098 private static NISuppressor result_ge_64 = 1099 new NISuppressor(2, RangeInt.GreaterEqual64.class); 1100 private static NISuppressor arg1_ge_64 = 1101 new NISuppressor(0, RangeInt.GreaterEqual64.class); 1102 private static NISuppressor arg2_ge_64 = 1103 new NISuppressor(1, RangeInt.GreaterEqual64.class); 1104 1105 private static NISuppressionSet suppressions = 1106 new NISuppressionSet( 1107 new NISuppression[] { 1108 1109 // (r == 0) && (x == 0) ==> r = x * y 1110 new NISuppression(result_eq_0, arg1_eq_0, suppressee), 1111 1112 // (r == 0) && (y == 0) ==> r = x * y 1113 new NISuppression(result_eq_0, arg2_eq_0, suppressee), 1114 1115 // (r == x) && (y == 1) ==> r = x * y 1116 new NISuppression(result_eq_arg1, arg2_eq_1, suppressee), 1117 1118 // (r == y) && (x == 1) ==> r = x * y 1119 new NISuppression(result_eq_arg2, arg1_eq_1, suppressee), 1120 1121 }); 1122 1123 // Create a suppression factory for functionBinary 1124 1125} 1126 1127 // #define EQUALITY_MIN_MAX_SUPPRESS 1128 1129 // default is that it is not this function, overriden in the subclass 1130 @Pure 1131 public boolean isMinimum() { 1132 return false; 1133 } 1134 1135/** 1136 * Represents the invariant {@code x = Minimum(y, z)} over three double 1137 * scalars. 1138 */ 1139public static class MinimumDouble_xyz extends FunctionBinaryFloat { 1140 // We are Serializable, so we specify a version to allow changes to 1141 // method signatures without breaking serialization. If you add or 1142 // remove fields, you should change this number to the current date. 1143 static final long serialVersionUID = 20031030L; 1144 1145 private static @Prototype MinimumDouble_xyz proto = new @Prototype MinimumDouble_xyz (); 1146 1147 /** Returns the prototype invariant for MinimumDouble_xyz */ 1148 public static @Prototype MinimumDouble_xyz get_proto() { 1149 return proto; 1150 } 1151 1152 /** instantiate an invariant on the specified slice */ 1153 @Override 1154 protected MinimumDouble_xyz instantiate_dyn(@Prototype MinimumDouble_xyz this, PptSlice slice) { 1155 return new MinimumDouble_xyz (slice); 1156 } 1157 1158 private MinimumDouble_xyz (PptSlice slice) { 1159 super(slice); 1160 } 1161 1162 public @Prototype MinimumDouble_xyz () { 1163 super(); 1164 } 1165 1166 private static String[] method_name = new String[] {"java.lang.Math.min(", ", ", ")"}; 1167 1168 @Override 1169 public String[] get_method_name(@GuardSatisfied MinimumDouble_xyz this) { 1170 return method_name; 1171 } 1172 1173 private static int function_id = -1; 1174 1175 @Override 1176 public int get_function_id() { 1177 return function_id; 1178 } 1179 1180 @Override 1181 public void set_function_id(int function_id) { 1182 assert MinimumDouble_xyz.function_id == -1; 1183 MinimumDouble_xyz.function_id = function_id; 1184 } 1185 1186 private static int var_order = 1; 1187 1188 @Override 1189 public int get_var_order(@GuardSatisfied MinimumDouble_xyz this) { 1190 return var_order; 1191 } 1192 1193 @Pure 1194 @Override 1195 public boolean is_symmetric() { 1196 1197 return true; 1198 } 1199 1200 @Override 1201 1202 public double func(double y, double z) { 1203 1204 return Math.min(y, z); 1205 } 1206 1207 @Override 1208 public InvariantStatus check_modified(double x, double y, 1209 double z, int count) { 1210 return check_ordered(x, y, z, count); 1211 } 1212 1213 @Override 1214 public InvariantStatus add_modified(double x, double y, 1215 double z, int count) { 1216 if (Debug.logDetail()) { 1217 log("result=%s, arg1=%s, arg2=%s", x, y, z); 1218 } 1219 return add_ordered(x, y, z, count); 1220 } 1221 1222 @Pure 1223 @Override 1224 public boolean isMinimum() { 1225 return true; 1226 } 1227 1228 /** Returns a list of non-instantiating suppressions for this invariant. */ 1229 @Pure 1230 @Override 1231 public @Nullable NISuppressionSet get_ni_suppressions() { 1232 if (NIS.dkconfig_enabled && dkconfig_enabled) { 1233 return suppressions; 1234 } else { 1235 return null; 1236 } 1237 } 1238 1239 /** definition of this invariant (the suppressee) */ 1240 private static NISuppressee suppressee = new NISuppressee(MinimumDouble_xyz.class, 3); 1241 1242 // suppressor definitions (used below) 1243 private static NISuppressor result_eq_arg1 = 1244 new NISuppressor(0, 1, FloatEqual.class); 1245 private static NISuppressor result_eq_arg2 = 1246 new NISuppressor(0, 2, FloatEqual.class); 1247 private static NISuppressor arg1_eq_arg2 = 1248 new NISuppressor(1, 2, FloatEqual.class); 1249 1250 private static NISuppressor result_lt_arg1 = 1251 new NISuppressor(0, 1, FloatLessThan.class); 1252 private static NISuppressor result_lt_arg2 = 1253 new NISuppressor(0, 2, FloatLessThan.class); 1254 private static NISuppressor arg1_lt_arg2 = 1255 new NISuppressor(1, 2, FloatLessThan.class); 1256 private static NISuppressor arg2_lt_arg1 = 1257 new NISuppressor(2, 1, FloatLessThan.class); 1258 1259 private static NISuppressor result_le_arg1 = 1260 new NISuppressor(0, 1, FloatLessEqual.class); 1261 private static NISuppressor result_le_arg2 = 1262 new NISuppressor(0, 2, FloatLessEqual.class); 1263 private static NISuppressor arg1_le_arg2 = 1264 new NISuppressor(1, 2, FloatLessEqual.class); 1265 private static NISuppressor arg2_le_arg1 = 1266 new NISuppressor(2, 1, FloatLessEqual.class); 1267 1268 private static NISuppressor result_track0_arg1 = 1269 new NISuppressor(0, 1, NumericInt.ZeroTrack.class); 1270 private static NISuppressor result_track0_arg2 = 1271 new NISuppressor(0, 2, NumericInt.ZeroTrack.class); 1272 private static NISuppressor arg1_track0_arg2 = 1273 new NISuppressor(1, 2, NumericInt.ZeroTrack.class); 1274 private static NISuppressor arg1_track0_result = 1275 new NISuppressor(1, 0, NumericInt.ZeroTrack.class); 1276 private static NISuppressor arg2_track0_result = 1277 new NISuppressor(2, 0, NumericInt.ZeroTrack.class); 1278 private static NISuppressor arg2_track0_arg1 = 1279 new NISuppressor(2, 1, NumericInt.ZeroTrack.class); 1280 1281 private static NISuppressor result_eq_1 = 1282 new NISuppressor(0, RangeFloat.EqualOne.class); 1283 private static NISuppressor arg1_eq_1 = 1284 new NISuppressor(1, RangeFloat.EqualOne.class); 1285 private static NISuppressor arg2_eq_1 = 1286 new NISuppressor(2, RangeFloat.EqualOne.class); 1287 1288 private static NISuppressor result_eq_0 = 1289 new NISuppressor(0, RangeFloat.EqualZero.class); 1290 private static NISuppressor arg1_eq_0 = 1291 new NISuppressor(1, RangeFloat.EqualZero.class); 1292 private static NISuppressor arg2_eq_0 = 1293 new NISuppressor(2, RangeFloat.EqualZero.class); 1294 1295 private static NISuppressor result_ne_0 = 1296 new NISuppressor(0, NonZeroFloat.class); 1297 private static NISuppressor arg1_ne_0 = 1298 new NISuppressor(1, NonZeroFloat.class); 1299 private static NISuppressor arg2_ne_0 = 1300 new NISuppressor(2, NonZeroFloat.class); 1301 1302 private static NISuppressor result_ge_0 = 1303 new NISuppressor(0, RangeFloat.GreaterEqualZero.class); 1304 private static NISuppressor arg1_ge_0 = 1305 new NISuppressor(1, RangeFloat.GreaterEqualZero.class); 1306 private static NISuppressor arg2_ge_0 = 1307 new NISuppressor(2, RangeFloat.GreaterEqualZero.class); 1308 1309 private static NISuppressor result_ge_64 = 1310 new NISuppressor(0, RangeInt.GreaterEqual64.class); 1311 private static NISuppressor arg1_ge_64 = 1312 new NISuppressor(1, RangeInt.GreaterEqual64.class); 1313 private static NISuppressor arg2_ge_64 = 1314 new NISuppressor(2, RangeInt.GreaterEqual64.class); 1315 1316 private static NISuppressionSet suppressions = 1317 new NISuppressionSet( 1318 new NISuppression[] { 1319 1320 // (x == y) && (y <= z) ==> r = min(y, z) 1321 new NISuppression(result_eq_arg1, arg1_le_arg2, suppressee), 1322 1323 // (x == z) && (z <= y) ==> r = min(y, z) 1324 new NISuppression(result_eq_arg2, arg2_le_arg1, suppressee), 1325 1326 }); 1327 1328 // Create a suppression factory for functionBinary 1329 1330} 1331 1332/** 1333 * Represents the invariant {@code y = Minimum(x, z)} over three double 1334 * scalars. 1335 */ 1336public static class MinimumDouble_yxz extends FunctionBinaryFloat { 1337 // We are Serializable, so we specify a version to allow changes to 1338 // method signatures without breaking serialization. If you add or 1339 // remove fields, you should change this number to the current date. 1340 static final long serialVersionUID = 20031030L; 1341 1342 private static @Prototype MinimumDouble_yxz proto = new @Prototype MinimumDouble_yxz (); 1343 1344 /** Returns the prototype invariant for MinimumDouble_yxz */ 1345 public static @Prototype MinimumDouble_yxz get_proto() { 1346 return proto; 1347 } 1348 1349 /** instantiate an invariant on the specified slice */ 1350 @Override 1351 protected MinimumDouble_yxz instantiate_dyn(@Prototype MinimumDouble_yxz this, PptSlice slice) { 1352 return new MinimumDouble_yxz (slice); 1353 } 1354 1355 private MinimumDouble_yxz (PptSlice slice) { 1356 super(slice); 1357 } 1358 1359 public @Prototype MinimumDouble_yxz () { 1360 super(); 1361 } 1362 1363 private static String[] method_name = new String[] {"java.lang.Math.min(", ", ", ")"}; 1364 1365 @Override 1366 public String[] get_method_name(@GuardSatisfied MinimumDouble_yxz this) { 1367 return method_name; 1368 } 1369 1370 private static int function_id = -1; 1371 1372 @Override 1373 public int get_function_id() { 1374 return function_id; 1375 } 1376 1377 @Override 1378 public void set_function_id(int function_id) { 1379 assert MinimumDouble_yxz.function_id == -1; 1380 MinimumDouble_yxz.function_id = function_id; 1381 } 1382 1383 private static int var_order = 2; 1384 1385 @Override 1386 public int get_var_order(@GuardSatisfied MinimumDouble_yxz this) { 1387 return var_order; 1388 } 1389 1390 @Pure 1391 @Override 1392 public boolean is_symmetric() { 1393 1394 return true; 1395 } 1396 1397 @Override 1398 1399 public double func(double x, double z) { 1400 1401 return Math.min(x, z); 1402 } 1403 1404 @Override 1405 public InvariantStatus check_modified(double x, double y, 1406 double z, int count) { 1407 return check_ordered(y, x, z, count); 1408 } 1409 1410 @Override 1411 public InvariantStatus add_modified(double x, double y, 1412 double z, int count) { 1413 if (Debug.logDetail()) { 1414 log("result=%s, arg1=%s, arg2=%s", y, x, z); 1415 } 1416 return add_ordered(y, x, z, count); 1417 } 1418 1419 @Pure 1420 @Override 1421 public boolean isMinimum() { 1422 return true; 1423 } 1424 1425 /** Returns a list of non-instantiating suppressions for this invariant. */ 1426 @Pure 1427 @Override 1428 public @Nullable NISuppressionSet get_ni_suppressions() { 1429 if (NIS.dkconfig_enabled && dkconfig_enabled) { 1430 return suppressions; 1431 } else { 1432 return null; 1433 } 1434 } 1435 1436 /** definition of this invariant (the suppressee) */ 1437 private static NISuppressee suppressee = new NISuppressee(MinimumDouble_yxz.class, 3); 1438 1439 // suppressor definitions (used below) 1440 private static NISuppressor result_eq_arg1 = 1441 new NISuppressor(1, 0, FloatEqual.class); 1442 private static NISuppressor result_eq_arg2 = 1443 new NISuppressor(1, 2, FloatEqual.class); 1444 private static NISuppressor arg1_eq_arg2 = 1445 new NISuppressor(0, 2, FloatEqual.class); 1446 1447 private static NISuppressor result_lt_arg1 = 1448 new NISuppressor(1, 0, FloatLessThan.class); 1449 private static NISuppressor result_lt_arg2 = 1450 new NISuppressor(1, 2, FloatLessThan.class); 1451 private static NISuppressor arg1_lt_arg2 = 1452 new NISuppressor(0, 2, FloatLessThan.class); 1453 private static NISuppressor arg2_lt_arg1 = 1454 new NISuppressor(2, 0, FloatLessThan.class); 1455 1456 private static NISuppressor result_le_arg1 = 1457 new NISuppressor(1, 0, FloatLessEqual.class); 1458 private static NISuppressor result_le_arg2 = 1459 new NISuppressor(1, 2, FloatLessEqual.class); 1460 private static NISuppressor arg1_le_arg2 = 1461 new NISuppressor(0, 2, FloatLessEqual.class); 1462 private static NISuppressor arg2_le_arg1 = 1463 new NISuppressor(2, 0, FloatLessEqual.class); 1464 1465 private static NISuppressor result_track0_arg1 = 1466 new NISuppressor(1, 0, NumericInt.ZeroTrack.class); 1467 private static NISuppressor result_track0_arg2 = 1468 new NISuppressor(1, 2, NumericInt.ZeroTrack.class); 1469 private static NISuppressor arg1_track0_arg2 = 1470 new NISuppressor(0, 2, NumericInt.ZeroTrack.class); 1471 private static NISuppressor arg1_track0_result = 1472 new NISuppressor(0, 1, NumericInt.ZeroTrack.class); 1473 private static NISuppressor arg2_track0_result = 1474 new NISuppressor(2, 1, NumericInt.ZeroTrack.class); 1475 private static NISuppressor arg2_track0_arg1 = 1476 new NISuppressor(2, 0, NumericInt.ZeroTrack.class); 1477 1478 private static NISuppressor result_eq_1 = 1479 new NISuppressor(1, RangeFloat.EqualOne.class); 1480 private static NISuppressor arg1_eq_1 = 1481 new NISuppressor(0, RangeFloat.EqualOne.class); 1482 private static NISuppressor arg2_eq_1 = 1483 new NISuppressor(2, RangeFloat.EqualOne.class); 1484 1485 private static NISuppressor result_eq_0 = 1486 new NISuppressor(1, RangeFloat.EqualZero.class); 1487 private static NISuppressor arg1_eq_0 = 1488 new NISuppressor(0, RangeFloat.EqualZero.class); 1489 private static NISuppressor arg2_eq_0 = 1490 new NISuppressor(2, RangeFloat.EqualZero.class); 1491 1492 private static NISuppressor result_ne_0 = 1493 new NISuppressor(1, NonZeroFloat.class); 1494 private static NISuppressor arg1_ne_0 = 1495 new NISuppressor(0, NonZeroFloat.class); 1496 private static NISuppressor arg2_ne_0 = 1497 new NISuppressor(2, NonZeroFloat.class); 1498 1499 private static NISuppressor result_ge_0 = 1500 new NISuppressor(1, RangeFloat.GreaterEqualZero.class); 1501 private static NISuppressor arg1_ge_0 = 1502 new NISuppressor(0, RangeFloat.GreaterEqualZero.class); 1503 private static NISuppressor arg2_ge_0 = 1504 new NISuppressor(2, RangeFloat.GreaterEqualZero.class); 1505 1506 private static NISuppressor result_ge_64 = 1507 new NISuppressor(1, RangeInt.GreaterEqual64.class); 1508 private static NISuppressor arg1_ge_64 = 1509 new NISuppressor(0, RangeInt.GreaterEqual64.class); 1510 private static NISuppressor arg2_ge_64 = 1511 new NISuppressor(2, RangeInt.GreaterEqual64.class); 1512 1513 private static NISuppressionSet suppressions = 1514 new NISuppressionSet( 1515 new NISuppression[] { 1516 1517 // (y == x) && (x <= z) ==> r = min(x, z) 1518 new NISuppression(result_eq_arg1, arg1_le_arg2, suppressee), 1519 1520 // (y == z) && (z <= x) ==> r = min(x, z) 1521 new NISuppression(result_eq_arg2, arg2_le_arg1, suppressee), 1522 1523 }); 1524 1525 // Create a suppression factory for functionBinary 1526 1527} 1528 1529/** 1530 * Represents the invariant {@code z = Minimum(x, y)} over three double 1531 * scalars. 1532 */ 1533public static class MinimumDouble_zxy extends FunctionBinaryFloat { 1534 // We are Serializable, so we specify a version to allow changes to 1535 // method signatures without breaking serialization. If you add or 1536 // remove fields, you should change this number to the current date. 1537 static final long serialVersionUID = 20031030L; 1538 1539 private static @Prototype MinimumDouble_zxy proto = new @Prototype MinimumDouble_zxy (); 1540 1541 /** Returns the prototype invariant for MinimumDouble_zxy */ 1542 public static @Prototype MinimumDouble_zxy get_proto() { 1543 return proto; 1544 } 1545 1546 /** instantiate an invariant on the specified slice */ 1547 @Override 1548 protected MinimumDouble_zxy instantiate_dyn(@Prototype MinimumDouble_zxy this, PptSlice slice) { 1549 return new MinimumDouble_zxy (slice); 1550 } 1551 1552 private MinimumDouble_zxy (PptSlice slice) { 1553 super(slice); 1554 } 1555 1556 public @Prototype MinimumDouble_zxy () { 1557 super(); 1558 } 1559 1560 private static String[] method_name = new String[] {"java.lang.Math.min(", ", ", ")"}; 1561 1562 @Override 1563 public String[] get_method_name(@GuardSatisfied MinimumDouble_zxy this) { 1564 return method_name; 1565 } 1566 1567 private static int function_id = -1; 1568 1569 @Override 1570 public int get_function_id() { 1571 return function_id; 1572 } 1573 1574 @Override 1575 public void set_function_id(int function_id) { 1576 assert MinimumDouble_zxy.function_id == -1; 1577 MinimumDouble_zxy.function_id = function_id; 1578 } 1579 1580 private static int var_order = 3; 1581 1582 @Override 1583 public int get_var_order(@GuardSatisfied MinimumDouble_zxy this) { 1584 return var_order; 1585 } 1586 1587 @Pure 1588 @Override 1589 public boolean is_symmetric() { 1590 1591 return true; 1592 } 1593 1594 @Override 1595 1596 public double func(double x, double y) { 1597 1598 return Math.min(x, y); 1599 } 1600 1601 @Override 1602 public InvariantStatus check_modified(double x, double y, 1603 double z, int count) { 1604 return check_ordered(z, x, y, count); 1605 } 1606 1607 @Override 1608 public InvariantStatus add_modified(double x, double y, 1609 double z, int count) { 1610 if (Debug.logDetail()) { 1611 log("result=%s, arg1=%s, arg2=%s", z, x, y); 1612 } 1613 return add_ordered(z, x, y, count); 1614 } 1615 1616 @Pure 1617 @Override 1618 public boolean isMinimum() { 1619 return true; 1620 } 1621 1622 /** Returns a list of non-instantiating suppressions for this invariant. */ 1623 @Pure 1624 @Override 1625 public @Nullable NISuppressionSet get_ni_suppressions() { 1626 if (NIS.dkconfig_enabled && dkconfig_enabled) { 1627 return suppressions; 1628 } else { 1629 return null; 1630 } 1631 } 1632 1633 /** definition of this invariant (the suppressee) */ 1634 private static NISuppressee suppressee = new NISuppressee(MinimumDouble_zxy.class, 3); 1635 1636 // suppressor definitions (used below) 1637 private static NISuppressor result_eq_arg1 = 1638 new NISuppressor(2, 0, FloatEqual.class); 1639 private static NISuppressor result_eq_arg2 = 1640 new NISuppressor(2, 1, FloatEqual.class); 1641 private static NISuppressor arg1_eq_arg2 = 1642 new NISuppressor(0, 1, FloatEqual.class); 1643 1644 private static NISuppressor result_lt_arg1 = 1645 new NISuppressor(2, 0, FloatLessThan.class); 1646 private static NISuppressor result_lt_arg2 = 1647 new NISuppressor(2, 1, FloatLessThan.class); 1648 private static NISuppressor arg1_lt_arg2 = 1649 new NISuppressor(0, 1, FloatLessThan.class); 1650 private static NISuppressor arg2_lt_arg1 = 1651 new NISuppressor(1, 0, FloatLessThan.class); 1652 1653 private static NISuppressor result_le_arg1 = 1654 new NISuppressor(2, 0, FloatLessEqual.class); 1655 private static NISuppressor result_le_arg2 = 1656 new NISuppressor(2, 1, FloatLessEqual.class); 1657 private static NISuppressor arg1_le_arg2 = 1658 new NISuppressor(0, 1, FloatLessEqual.class); 1659 private static NISuppressor arg2_le_arg1 = 1660 new NISuppressor(1, 0, FloatLessEqual.class); 1661 1662 private static NISuppressor result_track0_arg1 = 1663 new NISuppressor(2, 0, NumericInt.ZeroTrack.class); 1664 private static NISuppressor result_track0_arg2 = 1665 new NISuppressor(2, 1, NumericInt.ZeroTrack.class); 1666 private static NISuppressor arg1_track0_arg2 = 1667 new NISuppressor(0, 1, NumericInt.ZeroTrack.class); 1668 private static NISuppressor arg1_track0_result = 1669 new NISuppressor(0, 2, NumericInt.ZeroTrack.class); 1670 private static NISuppressor arg2_track0_result = 1671 new NISuppressor(1, 2, NumericInt.ZeroTrack.class); 1672 private static NISuppressor arg2_track0_arg1 = 1673 new NISuppressor(1, 0, NumericInt.ZeroTrack.class); 1674 1675 private static NISuppressor result_eq_1 = 1676 new NISuppressor(2, RangeFloat.EqualOne.class); 1677 private static NISuppressor arg1_eq_1 = 1678 new NISuppressor(0, RangeFloat.EqualOne.class); 1679 private static NISuppressor arg2_eq_1 = 1680 new NISuppressor(1, RangeFloat.EqualOne.class); 1681 1682 private static NISuppressor result_eq_0 = 1683 new NISuppressor(2, RangeFloat.EqualZero.class); 1684 private static NISuppressor arg1_eq_0 = 1685 new NISuppressor(0, RangeFloat.EqualZero.class); 1686 private static NISuppressor arg2_eq_0 = 1687 new NISuppressor(1, RangeFloat.EqualZero.class); 1688 1689 private static NISuppressor result_ne_0 = 1690 new NISuppressor(2, NonZeroFloat.class); 1691 private static NISuppressor arg1_ne_0 = 1692 new NISuppressor(0, NonZeroFloat.class); 1693 private static NISuppressor arg2_ne_0 = 1694 new NISuppressor(1, NonZeroFloat.class); 1695 1696 private static NISuppressor result_ge_0 = 1697 new NISuppressor(2, RangeFloat.GreaterEqualZero.class); 1698 private static NISuppressor arg1_ge_0 = 1699 new NISuppressor(0, RangeFloat.GreaterEqualZero.class); 1700 private static NISuppressor arg2_ge_0 = 1701 new NISuppressor(1, RangeFloat.GreaterEqualZero.class); 1702 1703 private static NISuppressor result_ge_64 = 1704 new NISuppressor(2, RangeInt.GreaterEqual64.class); 1705 private static NISuppressor arg1_ge_64 = 1706 new NISuppressor(0, RangeInt.GreaterEqual64.class); 1707 private static NISuppressor arg2_ge_64 = 1708 new NISuppressor(1, RangeInt.GreaterEqual64.class); 1709 1710 private static NISuppressionSet suppressions = 1711 new NISuppressionSet( 1712 new NISuppression[] { 1713 1714 // (z == x) && (x <= y) ==> r = min(x, y) 1715 new NISuppression(result_eq_arg1, arg1_le_arg2, suppressee), 1716 1717 // (z == y) && (y <= x) ==> r = min(x, y) 1718 new NISuppression(result_eq_arg2, arg2_le_arg1, suppressee), 1719 1720 }); 1721 1722 // Create a suppression factory for functionBinary 1723 1724} 1725 1726 // #define EQUALITY_MIN_MAX_SUPPRESS 1727 1728 // default is that it is not this function, overriden in the subclass 1729 @Pure 1730 public boolean isMaximum() { 1731 return false; 1732 } 1733 1734/** 1735 * Represents the invariant {@code x = Maximum(y, z)} over three double 1736 * scalars. 1737 */ 1738public static class MaximumDouble_xyz extends FunctionBinaryFloat { 1739 // We are Serializable, so we specify a version to allow changes to 1740 // method signatures without breaking serialization. If you add or 1741 // remove fields, you should change this number to the current date. 1742 static final long serialVersionUID = 20031030L; 1743 1744 private static @Prototype MaximumDouble_xyz proto = new @Prototype MaximumDouble_xyz (); 1745 1746 /** Returns the prototype invariant for MaximumDouble_xyz */ 1747 public static @Prototype MaximumDouble_xyz get_proto() { 1748 return proto; 1749 } 1750 1751 /** instantiate an invariant on the specified slice */ 1752 @Override 1753 protected MaximumDouble_xyz instantiate_dyn(@Prototype MaximumDouble_xyz this, PptSlice slice) { 1754 return new MaximumDouble_xyz (slice); 1755 } 1756 1757 private MaximumDouble_xyz (PptSlice slice) { 1758 super(slice); 1759 } 1760 1761 public @Prototype MaximumDouble_xyz () { 1762 super(); 1763 } 1764 1765 private static String[] method_name = new String[] {"java.lang.Math.max(", ", ", ")"}; 1766 1767 @Override 1768 public String[] get_method_name(@GuardSatisfied MaximumDouble_xyz this) { 1769 return method_name; 1770 } 1771 1772 private static int function_id = -1; 1773 1774 @Override 1775 public int get_function_id() { 1776 return function_id; 1777 } 1778 1779 @Override 1780 public void set_function_id(int function_id) { 1781 assert MaximumDouble_xyz.function_id == -1; 1782 MaximumDouble_xyz.function_id = function_id; 1783 } 1784 1785 private static int var_order = 1; 1786 1787 @Override 1788 public int get_var_order(@GuardSatisfied MaximumDouble_xyz this) { 1789 return var_order; 1790 } 1791 1792 @Pure 1793 @Override 1794 public boolean is_symmetric() { 1795 1796 return true; 1797 } 1798 1799 @Override 1800 1801 public double func(double y, double z) { 1802 1803 return Math.max(y, z); 1804 } 1805 1806 @Override 1807 public InvariantStatus check_modified(double x, double y, 1808 double z, int count) { 1809 return check_ordered(x, y, z, count); 1810 } 1811 1812 @Override 1813 public InvariantStatus add_modified(double x, double y, 1814 double z, int count) { 1815 if (Debug.logDetail()) { 1816 log("result=%s, arg1=%s, arg2=%s", x, y, z); 1817 } 1818 return add_ordered(x, y, z, count); 1819 } 1820 1821 @Pure 1822 @Override 1823 public boolean isMaximum() { 1824 return true; 1825 } 1826 1827 /** Returns a list of non-instantiating suppressions for this invariant. */ 1828 @Pure 1829 @Override 1830 public @Nullable NISuppressionSet get_ni_suppressions() { 1831 if (NIS.dkconfig_enabled && dkconfig_enabled) { 1832 return suppressions; 1833 } else { 1834 return null; 1835 } 1836 } 1837 1838 /** definition of this invariant (the suppressee) */ 1839 private static NISuppressee suppressee = new NISuppressee(MaximumDouble_xyz.class, 3); 1840 1841 // suppressor definitions (used below) 1842 private static NISuppressor result_eq_arg1 = 1843 new NISuppressor(0, 1, FloatEqual.class); 1844 private static NISuppressor result_eq_arg2 = 1845 new NISuppressor(0, 2, FloatEqual.class); 1846 private static NISuppressor arg1_eq_arg2 = 1847 new NISuppressor(1, 2, FloatEqual.class); 1848 1849 private static NISuppressor result_lt_arg1 = 1850 new NISuppressor(0, 1, FloatLessThan.class); 1851 private static NISuppressor result_lt_arg2 = 1852 new NISuppressor(0, 2, FloatLessThan.class); 1853 private static NISuppressor arg1_lt_arg2 = 1854 new NISuppressor(1, 2, FloatLessThan.class); 1855 private static NISuppressor arg2_lt_arg1 = 1856 new NISuppressor(2, 1, FloatLessThan.class); 1857 1858 private static NISuppressor result_le_arg1 = 1859 new NISuppressor(0, 1, FloatLessEqual.class); 1860 private static NISuppressor result_le_arg2 = 1861 new NISuppressor(0, 2, FloatLessEqual.class); 1862 private static NISuppressor arg1_le_arg2 = 1863 new NISuppressor(1, 2, FloatLessEqual.class); 1864 private static NISuppressor arg2_le_arg1 = 1865 new NISuppressor(2, 1, FloatLessEqual.class); 1866 1867 private static NISuppressor result_track0_arg1 = 1868 new NISuppressor(0, 1, NumericInt.ZeroTrack.class); 1869 private static NISuppressor result_track0_arg2 = 1870 new NISuppressor(0, 2, NumericInt.ZeroTrack.class); 1871 private static NISuppressor arg1_track0_arg2 = 1872 new NISuppressor(1, 2, NumericInt.ZeroTrack.class); 1873 private static NISuppressor arg1_track0_result = 1874 new NISuppressor(1, 0, NumericInt.ZeroTrack.class); 1875 private static NISuppressor arg2_track0_result = 1876 new NISuppressor(2, 0, NumericInt.ZeroTrack.class); 1877 private static NISuppressor arg2_track0_arg1 = 1878 new NISuppressor(2, 1, NumericInt.ZeroTrack.class); 1879 1880 private static NISuppressor result_eq_1 = 1881 new NISuppressor(0, RangeFloat.EqualOne.class); 1882 private static NISuppressor arg1_eq_1 = 1883 new NISuppressor(1, RangeFloat.EqualOne.class); 1884 private static NISuppressor arg2_eq_1 = 1885 new NISuppressor(2, RangeFloat.EqualOne.class); 1886 1887 private static NISuppressor result_eq_0 = 1888 new NISuppressor(0, RangeFloat.EqualZero.class); 1889 private static NISuppressor arg1_eq_0 = 1890 new NISuppressor(1, RangeFloat.EqualZero.class); 1891 private static NISuppressor arg2_eq_0 = 1892 new NISuppressor(2, RangeFloat.EqualZero.class); 1893 1894 private static NISuppressor result_ne_0 = 1895 new NISuppressor(0, NonZeroFloat.class); 1896 private static NISuppressor arg1_ne_0 = 1897 new NISuppressor(1, NonZeroFloat.class); 1898 private static NISuppressor arg2_ne_0 = 1899 new NISuppressor(2, NonZeroFloat.class); 1900 1901 private static NISuppressor result_ge_0 = 1902 new NISuppressor(0, RangeFloat.GreaterEqualZero.class); 1903 private static NISuppressor arg1_ge_0 = 1904 new NISuppressor(1, RangeFloat.GreaterEqualZero.class); 1905 private static NISuppressor arg2_ge_0 = 1906 new NISuppressor(2, RangeFloat.GreaterEqualZero.class); 1907 1908 private static NISuppressor result_ge_64 = 1909 new NISuppressor(0, RangeInt.GreaterEqual64.class); 1910 private static NISuppressor arg1_ge_64 = 1911 new NISuppressor(1, RangeInt.GreaterEqual64.class); 1912 private static NISuppressor arg2_ge_64 = 1913 new NISuppressor(2, RangeInt.GreaterEqual64.class); 1914 1915 private static NISuppressionSet suppressions = 1916 new NISuppressionSet( 1917 new NISuppression[] { 1918 1919 // (r == y) && (z <= y) ==> r = max(y, z) 1920 new NISuppression(result_eq_arg1, arg2_le_arg1, suppressee), 1921 1922 // (r == z) && (y <= z) ==> r = max(y, z) 1923 new NISuppression(result_eq_arg2, arg1_le_arg2, suppressee), 1924 1925 }); 1926 1927 // Create a suppression factory for functionBinary 1928 1929} 1930 1931/** 1932 * Represents the invariant {@code y = Maximum(x, z)} over three double 1933 * scalars. 1934 */ 1935public static class MaximumDouble_yxz extends FunctionBinaryFloat { 1936 // We are Serializable, so we specify a version to allow changes to 1937 // method signatures without breaking serialization. If you add or 1938 // remove fields, you should change this number to the current date. 1939 static final long serialVersionUID = 20031030L; 1940 1941 private static @Prototype MaximumDouble_yxz proto = new @Prototype MaximumDouble_yxz (); 1942 1943 /** Returns the prototype invariant for MaximumDouble_yxz */ 1944 public static @Prototype MaximumDouble_yxz get_proto() { 1945 return proto; 1946 } 1947 1948 /** instantiate an invariant on the specified slice */ 1949 @Override 1950 protected MaximumDouble_yxz instantiate_dyn(@Prototype MaximumDouble_yxz this, PptSlice slice) { 1951 return new MaximumDouble_yxz (slice); 1952 } 1953 1954 private MaximumDouble_yxz (PptSlice slice) { 1955 super(slice); 1956 } 1957 1958 public @Prototype MaximumDouble_yxz () { 1959 super(); 1960 } 1961 1962 private static String[] method_name = new String[] {"java.lang.Math.max(", ", ", ")"}; 1963 1964 @Override 1965 public String[] get_method_name(@GuardSatisfied MaximumDouble_yxz this) { 1966 return method_name; 1967 } 1968 1969 private static int function_id = -1; 1970 1971 @Override 1972 public int get_function_id() { 1973 return function_id; 1974 } 1975 1976 @Override 1977 public void set_function_id(int function_id) { 1978 assert MaximumDouble_yxz.function_id == -1; 1979 MaximumDouble_yxz.function_id = function_id; 1980 } 1981 1982 private static int var_order = 2; 1983 1984 @Override 1985 public int get_var_order(@GuardSatisfied MaximumDouble_yxz this) { 1986 return var_order; 1987 } 1988 1989 @Pure 1990 @Override 1991 public boolean is_symmetric() { 1992 1993 return true; 1994 } 1995 1996 @Override 1997 1998 public double func(double x, double z) { 1999 2000 return Math.max(x, z); 2001 } 2002 2003 @Override 2004 public InvariantStatus check_modified(double x, double y, 2005 double z, int count) { 2006 return check_ordered(y, x, z, count); 2007 } 2008 2009 @Override 2010 public InvariantStatus add_modified(double x, double y, 2011 double z, int count) { 2012 if (Debug.logDetail()) { 2013 log("result=%s, arg1=%s, arg2=%s", y, x, z); 2014 } 2015 return add_ordered(y, x, z, count); 2016 } 2017 2018 @Pure 2019 @Override 2020 public boolean isMaximum() { 2021 return true; 2022 } 2023 2024 /** Returns a list of non-instantiating suppressions for this invariant. */ 2025 @Pure 2026 @Override 2027 public @Nullable NISuppressionSet get_ni_suppressions() { 2028 if (NIS.dkconfig_enabled && dkconfig_enabled) { 2029 return suppressions; 2030 } else { 2031 return null; 2032 } 2033 } 2034 2035 /** definition of this invariant (the suppressee) */ 2036 private static NISuppressee suppressee = new NISuppressee(MaximumDouble_yxz.class, 3); 2037 2038 // suppressor definitions (used below) 2039 private static NISuppressor result_eq_arg1 = 2040 new NISuppressor(1, 0, FloatEqual.class); 2041 private static NISuppressor result_eq_arg2 = 2042 new NISuppressor(1, 2, FloatEqual.class); 2043 private static NISuppressor arg1_eq_arg2 = 2044 new NISuppressor(0, 2, FloatEqual.class); 2045 2046 private static NISuppressor result_lt_arg1 = 2047 new NISuppressor(1, 0, FloatLessThan.class); 2048 private static NISuppressor result_lt_arg2 = 2049 new NISuppressor(1, 2, FloatLessThan.class); 2050 private static NISuppressor arg1_lt_arg2 = 2051 new NISuppressor(0, 2, FloatLessThan.class); 2052 private static NISuppressor arg2_lt_arg1 = 2053 new NISuppressor(2, 0, FloatLessThan.class); 2054 2055 private static NISuppressor result_le_arg1 = 2056 new NISuppressor(1, 0, FloatLessEqual.class); 2057 private static NISuppressor result_le_arg2 = 2058 new NISuppressor(1, 2, FloatLessEqual.class); 2059 private static NISuppressor arg1_le_arg2 = 2060 new NISuppressor(0, 2, FloatLessEqual.class); 2061 private static NISuppressor arg2_le_arg1 = 2062 new NISuppressor(2, 0, FloatLessEqual.class); 2063 2064 private static NISuppressor result_track0_arg1 = 2065 new NISuppressor(1, 0, NumericInt.ZeroTrack.class); 2066 private static NISuppressor result_track0_arg2 = 2067 new NISuppressor(1, 2, NumericInt.ZeroTrack.class); 2068 private static NISuppressor arg1_track0_arg2 = 2069 new NISuppressor(0, 2, NumericInt.ZeroTrack.class); 2070 private static NISuppressor arg1_track0_result = 2071 new NISuppressor(0, 1, NumericInt.ZeroTrack.class); 2072 private static NISuppressor arg2_track0_result = 2073 new NISuppressor(2, 1, NumericInt.ZeroTrack.class); 2074 private static NISuppressor arg2_track0_arg1 = 2075 new NISuppressor(2, 0, NumericInt.ZeroTrack.class); 2076 2077 private static NISuppressor result_eq_1 = 2078 new NISuppressor(1, RangeFloat.EqualOne.class); 2079 private static NISuppressor arg1_eq_1 = 2080 new NISuppressor(0, RangeFloat.EqualOne.class); 2081 private static NISuppressor arg2_eq_1 = 2082 new NISuppressor(2, RangeFloat.EqualOne.class); 2083 2084 private static NISuppressor result_eq_0 = 2085 new NISuppressor(1, RangeFloat.EqualZero.class); 2086 private static NISuppressor arg1_eq_0 = 2087 new NISuppressor(0, RangeFloat.EqualZero.class); 2088 private static NISuppressor arg2_eq_0 = 2089 new NISuppressor(2, RangeFloat.EqualZero.class); 2090 2091 private static NISuppressor result_ne_0 = 2092 new NISuppressor(1, NonZeroFloat.class); 2093 private static NISuppressor arg1_ne_0 = 2094 new NISuppressor(0, NonZeroFloat.class); 2095 private static NISuppressor arg2_ne_0 = 2096 new NISuppressor(2, NonZeroFloat.class); 2097 2098 private static NISuppressor result_ge_0 = 2099 new NISuppressor(1, RangeFloat.GreaterEqualZero.class); 2100 private static NISuppressor arg1_ge_0 = 2101 new NISuppressor(0, RangeFloat.GreaterEqualZero.class); 2102 private static NISuppressor arg2_ge_0 = 2103 new NISuppressor(2, RangeFloat.GreaterEqualZero.class); 2104 2105 private static NISuppressor result_ge_64 = 2106 new NISuppressor(1, RangeInt.GreaterEqual64.class); 2107 private static NISuppressor arg1_ge_64 = 2108 new NISuppressor(0, RangeInt.GreaterEqual64.class); 2109 private static NISuppressor arg2_ge_64 = 2110 new NISuppressor(2, RangeInt.GreaterEqual64.class); 2111 2112 private static NISuppressionSet suppressions = 2113 new NISuppressionSet( 2114 new NISuppression[] { 2115 2116 // (r == x) && (z <= x) ==> r = max(x, z) 2117 new NISuppression(result_eq_arg1, arg2_le_arg1, suppressee), 2118 2119 // (r == z) && (x <= z) ==> r = max(x, z) 2120 new NISuppression(result_eq_arg2, arg1_le_arg2, suppressee), 2121 2122 }); 2123 2124 // Create a suppression factory for functionBinary 2125 2126} 2127 2128/** 2129 * Represents the invariant {@code z = Maximum(x, y)} over three double 2130 * scalars. 2131 */ 2132public static class MaximumDouble_zxy extends FunctionBinaryFloat { 2133 // We are Serializable, so we specify a version to allow changes to 2134 // method signatures without breaking serialization. If you add or 2135 // remove fields, you should change this number to the current date. 2136 static final long serialVersionUID = 20031030L; 2137 2138 private static @Prototype MaximumDouble_zxy proto = new @Prototype MaximumDouble_zxy (); 2139 2140 /** Returns the prototype invariant for MaximumDouble_zxy */ 2141 public static @Prototype MaximumDouble_zxy get_proto() { 2142 return proto; 2143 } 2144 2145 /** instantiate an invariant on the specified slice */ 2146 @Override 2147 protected MaximumDouble_zxy instantiate_dyn(@Prototype MaximumDouble_zxy this, PptSlice slice) { 2148 return new MaximumDouble_zxy (slice); 2149 } 2150 2151 private MaximumDouble_zxy (PptSlice slice) { 2152 super(slice); 2153 } 2154 2155 public @Prototype MaximumDouble_zxy () { 2156 super(); 2157 } 2158 2159 private static String[] method_name = new String[] {"java.lang.Math.max(", ", ", ")"}; 2160 2161 @Override 2162 public String[] get_method_name(@GuardSatisfied MaximumDouble_zxy this) { 2163 return method_name; 2164 } 2165 2166 private static int function_id = -1; 2167 2168 @Override 2169 public int get_function_id() { 2170 return function_id; 2171 } 2172 2173 @Override 2174 public void set_function_id(int function_id) { 2175 assert MaximumDouble_zxy.function_id == -1; 2176 MaximumDouble_zxy.function_id = function_id; 2177 } 2178 2179 private static int var_order = 3; 2180 2181 @Override 2182 public int get_var_order(@GuardSatisfied MaximumDouble_zxy this) { 2183 return var_order; 2184 } 2185 2186 @Pure 2187 @Override 2188 public boolean is_symmetric() { 2189 2190 return true; 2191 } 2192 2193 @Override 2194 2195 public double func(double x, double y) { 2196 2197 return Math.max(x, y); 2198 } 2199 2200 @Override 2201 public InvariantStatus check_modified(double x, double y, 2202 double z, int count) { 2203 return check_ordered(z, x, y, count); 2204 } 2205 2206 @Override 2207 public InvariantStatus add_modified(double x, double y, 2208 double z, int count) { 2209 if (Debug.logDetail()) { 2210 log("result=%s, arg1=%s, arg2=%s", z, x, y); 2211 } 2212 return add_ordered(z, x, y, count); 2213 } 2214 2215 @Pure 2216 @Override 2217 public boolean isMaximum() { 2218 return true; 2219 } 2220 2221 /** Returns a list of non-instantiating suppressions for this invariant. */ 2222 @Pure 2223 @Override 2224 public @Nullable NISuppressionSet get_ni_suppressions() { 2225 if (NIS.dkconfig_enabled && dkconfig_enabled) { 2226 return suppressions; 2227 } else { 2228 return null; 2229 } 2230 } 2231 2232 /** definition of this invariant (the suppressee) */ 2233 private static NISuppressee suppressee = new NISuppressee(MaximumDouble_zxy.class, 3); 2234 2235 // suppressor definitions (used below) 2236 private static NISuppressor result_eq_arg1 = 2237 new NISuppressor(2, 0, FloatEqual.class); 2238 private static NISuppressor result_eq_arg2 = 2239 new NISuppressor(2, 1, FloatEqual.class); 2240 private static NISuppressor arg1_eq_arg2 = 2241 new NISuppressor(0, 1, FloatEqual.class); 2242 2243 private static NISuppressor result_lt_arg1 = 2244 new NISuppressor(2, 0, FloatLessThan.class); 2245 private static NISuppressor result_lt_arg2 = 2246 new NISuppressor(2, 1, FloatLessThan.class); 2247 private static NISuppressor arg1_lt_arg2 = 2248 new NISuppressor(0, 1, FloatLessThan.class); 2249 private static NISuppressor arg2_lt_arg1 = 2250 new NISuppressor(1, 0, FloatLessThan.class); 2251 2252 private static NISuppressor result_le_arg1 = 2253 new NISuppressor(2, 0, FloatLessEqual.class); 2254 private static NISuppressor result_le_arg2 = 2255 new NISuppressor(2, 1, FloatLessEqual.class); 2256 private static NISuppressor arg1_le_arg2 = 2257 new NISuppressor(0, 1, FloatLessEqual.class); 2258 private static NISuppressor arg2_le_arg1 = 2259 new NISuppressor(1, 0, FloatLessEqual.class); 2260 2261 private static NISuppressor result_track0_arg1 = 2262 new NISuppressor(2, 0, NumericInt.ZeroTrack.class); 2263 private static NISuppressor result_track0_arg2 = 2264 new NISuppressor(2, 1, NumericInt.ZeroTrack.class); 2265 private static NISuppressor arg1_track0_arg2 = 2266 new NISuppressor(0, 1, NumericInt.ZeroTrack.class); 2267 private static NISuppressor arg1_track0_result = 2268 new NISuppressor(0, 2, NumericInt.ZeroTrack.class); 2269 private static NISuppressor arg2_track0_result = 2270 new NISuppressor(1, 2, NumericInt.ZeroTrack.class); 2271 private static NISuppressor arg2_track0_arg1 = 2272 new NISuppressor(1, 0, NumericInt.ZeroTrack.class); 2273 2274 private static NISuppressor result_eq_1 = 2275 new NISuppressor(2, RangeFloat.EqualOne.class); 2276 private static NISuppressor arg1_eq_1 = 2277 new NISuppressor(0, RangeFloat.EqualOne.class); 2278 private static NISuppressor arg2_eq_1 = 2279 new NISuppressor(1, RangeFloat.EqualOne.class); 2280 2281 private static NISuppressor result_eq_0 = 2282 new NISuppressor(2, RangeFloat.EqualZero.class); 2283 private static NISuppressor arg1_eq_0 = 2284 new NISuppressor(0, RangeFloat.EqualZero.class); 2285 private static NISuppressor arg2_eq_0 = 2286 new NISuppressor(1, RangeFloat.EqualZero.class); 2287 2288 private static NISuppressor result_ne_0 = 2289 new NISuppressor(2, NonZeroFloat.class); 2290 private static NISuppressor arg1_ne_0 = 2291 new NISuppressor(0, NonZeroFloat.class); 2292 private static NISuppressor arg2_ne_0 = 2293 new NISuppressor(1, NonZeroFloat.class); 2294 2295 private static NISuppressor result_ge_0 = 2296 new NISuppressor(2, RangeFloat.GreaterEqualZero.class); 2297 private static NISuppressor arg1_ge_0 = 2298 new NISuppressor(0, RangeFloat.GreaterEqualZero.class); 2299 private static NISuppressor arg2_ge_0 = 2300 new NISuppressor(1, RangeFloat.GreaterEqualZero.class); 2301 2302 private static NISuppressor result_ge_64 = 2303 new NISuppressor(2, RangeInt.GreaterEqual64.class); 2304 private static NISuppressor arg1_ge_64 = 2305 new NISuppressor(0, RangeInt.GreaterEqual64.class); 2306 private static NISuppressor arg2_ge_64 = 2307 new NISuppressor(1, RangeInt.GreaterEqual64.class); 2308 2309 private static NISuppressionSet suppressions = 2310 new NISuppressionSet( 2311 new NISuppression[] { 2312 2313 // (r == x) && (y <= x) ==> r = max(x, y) 2314 new NISuppression(result_eq_arg1, arg2_le_arg1, suppressee), 2315 2316 // (r == y) && (x <= y) ==> r = max(x, y) 2317 new NISuppression(result_eq_arg2, arg1_le_arg2, suppressee), 2318 2319 }); 2320 2321 // Create a suppression factory for functionBinary 2322 2323} 2324 2325 // default is that it is not this function, overriden in the subclass 2326 @Pure 2327 public boolean isDivision() { 2328 return false; 2329 } 2330 2331/** 2332 * Represents the invariant {@code x = Division(y, z)} over three double 2333 * scalars. 2334 */ 2335public static class DivisionDouble_xyz extends FunctionBinaryFloat { 2336 // We are Serializable, so we specify a version to allow changes to 2337 // method signatures without breaking serialization. If you add or 2338 // remove fields, you should change this number to the current date. 2339 static final long serialVersionUID = 20031030L; 2340 2341 private static @Prototype DivisionDouble_xyz proto = new @Prototype DivisionDouble_xyz (); 2342 2343 /** Returns the prototype invariant for DivisionDouble_xyz */ 2344 public static @Prototype DivisionDouble_xyz get_proto() { 2345 return proto; 2346 } 2347 2348 /** instantiate an invariant on the specified slice */ 2349 @Override 2350 protected DivisionDouble_xyz instantiate_dyn(@Prototype DivisionDouble_xyz this, PptSlice slice) { 2351 return new DivisionDouble_xyz (slice); 2352 } 2353 2354 private DivisionDouble_xyz (PptSlice slice) { 2355 super(slice); 2356 } 2357 2358 public @Prototype DivisionDouble_xyz () { 2359 super(); 2360 } 2361 2362 private static String[] method_name = new String[] {"", " / ", ""}; 2363 2364 @Override 2365 public String[] get_method_name(@GuardSatisfied DivisionDouble_xyz this) { 2366 return method_name; 2367 } 2368 2369 private static int function_id = -1; 2370 2371 @Override 2372 public int get_function_id() { 2373 return function_id; 2374 } 2375 2376 @Override 2377 public void set_function_id(int function_id) { 2378 assert DivisionDouble_xyz.function_id == -1; 2379 DivisionDouble_xyz.function_id = function_id; 2380 } 2381 2382 private static int var_order = 1; 2383 2384 @Override 2385 public int get_var_order(@GuardSatisfied DivisionDouble_xyz this) { 2386 return var_order; 2387 } 2388 2389 @Pure 2390 @Override 2391 public boolean is_symmetric() { 2392 2393 return false; 2394 } 2395 2396 @Override 2397 2398 public double func(double y, double z) { 2399 2400 return (y / z); 2401 } 2402 2403 @Override 2404 public InvariantStatus check_modified(double x, double y, 2405 double z, int count) { 2406 return check_ordered(x, y, z, count); 2407 } 2408 2409 @Override 2410 public InvariantStatus add_modified(double x, double y, 2411 double z, int count) { 2412 if (Debug.logDetail()) { 2413 log("result=%s, arg1=%s, arg2=%s", x, y, z); 2414 } 2415 return add_ordered(x, y, z, count); 2416 } 2417 2418 @Pure 2419 @Override 2420 public boolean isDivision() { 2421 return true; 2422 } 2423 2424 @Pure 2425 @Override 2426 public boolean isExact() { 2427 return true; 2428 } 2429 2430 /** Returns a list of non-instantiating suppressions for this invariant. */ 2431 @Pure 2432 @Override 2433 public @Nullable NISuppressionSet get_ni_suppressions() { 2434 if (NIS.dkconfig_enabled && dkconfig_enabled) { 2435 return suppressions; 2436 } else { 2437 return null; 2438 } 2439 } 2440 2441 /** definition of this invariant (the suppressee) */ 2442 private static NISuppressee suppressee = new NISuppressee(DivisionDouble_xyz.class, 3); 2443 2444 // suppressor definitions (used below) 2445 private static NISuppressor result_eq_arg1 = 2446 new NISuppressor(0, 1, FloatEqual.class); 2447 private static NISuppressor result_eq_arg2 = 2448 new NISuppressor(0, 2, FloatEqual.class); 2449 private static NISuppressor arg1_eq_arg2 = 2450 new NISuppressor(1, 2, FloatEqual.class); 2451 2452 private static NISuppressor result_lt_arg1 = 2453 new NISuppressor(0, 1, FloatLessThan.class); 2454 private static NISuppressor result_lt_arg2 = 2455 new NISuppressor(0, 2, FloatLessThan.class); 2456 private static NISuppressor arg1_lt_arg2 = 2457 new NISuppressor(1, 2, FloatLessThan.class); 2458 private static NISuppressor arg2_lt_arg1 = 2459 new NISuppressor(2, 1, FloatLessThan.class); 2460 2461 private static NISuppressor result_le_arg1 = 2462 new NISuppressor(0, 1, FloatLessEqual.class); 2463 private static NISuppressor result_le_arg2 = 2464 new NISuppressor(0, 2, FloatLessEqual.class); 2465 private static NISuppressor arg1_le_arg2 = 2466 new NISuppressor(1, 2, FloatLessEqual.class); 2467 private static NISuppressor arg2_le_arg1 = 2468 new NISuppressor(2, 1, FloatLessEqual.class); 2469 2470 private static NISuppressor result_track0_arg1 = 2471 new NISuppressor(0, 1, NumericInt.ZeroTrack.class); 2472 private static NISuppressor result_track0_arg2 = 2473 new NISuppressor(0, 2, NumericInt.ZeroTrack.class); 2474 private static NISuppressor arg1_track0_arg2 = 2475 new NISuppressor(1, 2, NumericInt.ZeroTrack.class); 2476 private static NISuppressor arg1_track0_result = 2477 new NISuppressor(1, 0, NumericInt.ZeroTrack.class); 2478 private static NISuppressor arg2_track0_result = 2479 new NISuppressor(2, 0, NumericInt.ZeroTrack.class); 2480 private static NISuppressor arg2_track0_arg1 = 2481 new NISuppressor(2, 1, NumericInt.ZeroTrack.class); 2482 2483 private static NISuppressor result_eq_1 = 2484 new NISuppressor(0, RangeFloat.EqualOne.class); 2485 private static NISuppressor arg1_eq_1 = 2486 new NISuppressor(1, RangeFloat.EqualOne.class); 2487 private static NISuppressor arg2_eq_1 = 2488 new NISuppressor(2, RangeFloat.EqualOne.class); 2489 2490 private static NISuppressor result_eq_0 = 2491 new NISuppressor(0, RangeFloat.EqualZero.class); 2492 private static NISuppressor arg1_eq_0 = 2493 new NISuppressor(1, RangeFloat.EqualZero.class); 2494 private static NISuppressor arg2_eq_0 = 2495 new NISuppressor(2, RangeFloat.EqualZero.class); 2496 2497 private static NISuppressor result_ne_0 = 2498 new NISuppressor(0, NonZeroFloat.class); 2499 private static NISuppressor arg1_ne_0 = 2500 new NISuppressor(1, NonZeroFloat.class); 2501 private static NISuppressor arg2_ne_0 = 2502 new NISuppressor(2, NonZeroFloat.class); 2503 2504 private static NISuppressor result_ge_0 = 2505 new NISuppressor(0, RangeFloat.GreaterEqualZero.class); 2506 private static NISuppressor arg1_ge_0 = 2507 new NISuppressor(1, RangeFloat.GreaterEqualZero.class); 2508 private static NISuppressor arg2_ge_0 = 2509 new NISuppressor(2, RangeFloat.GreaterEqualZero.class); 2510 2511 private static NISuppressor result_ge_64 = 2512 new NISuppressor(0, RangeInt.GreaterEqual64.class); 2513 private static NISuppressor arg1_ge_64 = 2514 new NISuppressor(1, RangeInt.GreaterEqual64.class); 2515 private static NISuppressor arg2_ge_64 = 2516 new NISuppressor(2, RangeInt.GreaterEqual64.class); 2517 2518 private static NISuppressionSet suppressions = 2519 new NISuppressionSet( 2520 new NISuppression[] { 2521 2522 // (y == z) && (z != 0) && (r == 1) 2523 new NISuppression(arg1_eq_arg2, arg2_ne_0, result_eq_1, suppressee), 2524 2525 // (r == y) && (z == 1) ==> r = y / z 2526 new NISuppression(result_eq_arg1, arg2_eq_1, suppressee), 2527 }); 2528 2529 // Create a suppression factory for functionBinary 2530 2531} 2532 2533/** 2534 * Represents the invariant {@code y = Division(x, z)} over three double 2535 * scalars. 2536 */ 2537public static class DivisionDouble_yxz extends FunctionBinaryFloat { 2538 // We are Serializable, so we specify a version to allow changes to 2539 // method signatures without breaking serialization. If you add or 2540 // remove fields, you should change this number to the current date. 2541 static final long serialVersionUID = 20031030L; 2542 2543 private static @Prototype DivisionDouble_yxz proto = new @Prototype DivisionDouble_yxz (); 2544 2545 /** Returns the prototype invariant for DivisionDouble_yxz */ 2546 public static @Prototype DivisionDouble_yxz get_proto() { 2547 return proto; 2548 } 2549 2550 /** instantiate an invariant on the specified slice */ 2551 @Override 2552 protected DivisionDouble_yxz instantiate_dyn(@Prototype DivisionDouble_yxz this, PptSlice slice) { 2553 return new DivisionDouble_yxz (slice); 2554 } 2555 2556 private DivisionDouble_yxz (PptSlice slice) { 2557 super(slice); 2558 } 2559 2560 public @Prototype DivisionDouble_yxz () { 2561 super(); 2562 } 2563 2564 private static String[] method_name = new String[] {"", " / ", ""}; 2565 2566 @Override 2567 public String[] get_method_name(@GuardSatisfied DivisionDouble_yxz this) { 2568 return method_name; 2569 } 2570 2571 private static int function_id = -1; 2572 2573 @Override 2574 public int get_function_id() { 2575 return function_id; 2576 } 2577 2578 @Override 2579 public void set_function_id(int function_id) { 2580 assert DivisionDouble_yxz.function_id == -1; 2581 DivisionDouble_yxz.function_id = function_id; 2582 } 2583 2584 private static int var_order = 2; 2585 2586 @Override 2587 public int get_var_order(@GuardSatisfied DivisionDouble_yxz this) { 2588 return var_order; 2589 } 2590 2591 @Pure 2592 @Override 2593 public boolean is_symmetric() { 2594 2595 return false; 2596 } 2597 2598 @Override 2599 2600 public double func(double x, double z) { 2601 2602 return (x / z); 2603 } 2604 2605 @Override 2606 public InvariantStatus check_modified(double x, double y, 2607 double z, int count) { 2608 return check_ordered(y, x, z, count); 2609 } 2610 2611 @Override 2612 public InvariantStatus add_modified(double x, double y, 2613 double z, int count) { 2614 if (Debug.logDetail()) { 2615 log("result=%s, arg1=%s, arg2=%s", y, x, z); 2616 } 2617 return add_ordered(y, x, z, count); 2618 } 2619 2620 @Pure 2621 @Override 2622 public boolean isDivision() { 2623 return true; 2624 } 2625 2626 @Pure 2627 @Override 2628 public boolean isExact() { 2629 return true; 2630 } 2631 2632 /** Returns a list of non-instantiating suppressions for this invariant. */ 2633 @Pure 2634 @Override 2635 public @Nullable NISuppressionSet get_ni_suppressions() { 2636 if (NIS.dkconfig_enabled && dkconfig_enabled) { 2637 return suppressions; 2638 } else { 2639 return null; 2640 } 2641 } 2642 2643 /** definition of this invariant (the suppressee) */ 2644 private static NISuppressee suppressee = new NISuppressee(DivisionDouble_yxz.class, 3); 2645 2646 // suppressor definitions (used below) 2647 private static NISuppressor result_eq_arg1 = 2648 new NISuppressor(1, 0, FloatEqual.class); 2649 private static NISuppressor result_eq_arg2 = 2650 new NISuppressor(1, 2, FloatEqual.class); 2651 private static NISuppressor arg1_eq_arg2 = 2652 new NISuppressor(0, 2, FloatEqual.class); 2653 2654 private static NISuppressor result_lt_arg1 = 2655 new NISuppressor(1, 0, FloatLessThan.class); 2656 private static NISuppressor result_lt_arg2 = 2657 new NISuppressor(1, 2, FloatLessThan.class); 2658 private static NISuppressor arg1_lt_arg2 = 2659 new NISuppressor(0, 2, FloatLessThan.class); 2660 private static NISuppressor arg2_lt_arg1 = 2661 new NISuppressor(2, 0, FloatLessThan.class); 2662 2663 private static NISuppressor result_le_arg1 = 2664 new NISuppressor(1, 0, FloatLessEqual.class); 2665 private static NISuppressor result_le_arg2 = 2666 new NISuppressor(1, 2, FloatLessEqual.class); 2667 private static NISuppressor arg1_le_arg2 = 2668 new NISuppressor(0, 2, FloatLessEqual.class); 2669 private static NISuppressor arg2_le_arg1 = 2670 new NISuppressor(2, 0, FloatLessEqual.class); 2671 2672 private static NISuppressor result_track0_arg1 = 2673 new NISuppressor(1, 0, NumericInt.ZeroTrack.class); 2674 private static NISuppressor result_track0_arg2 = 2675 new NISuppressor(1, 2, NumericInt.ZeroTrack.class); 2676 private static NISuppressor arg1_track0_arg2 = 2677 new NISuppressor(0, 2, NumericInt.ZeroTrack.class); 2678 private static NISuppressor arg1_track0_result = 2679 new NISuppressor(0, 1, NumericInt.ZeroTrack.class); 2680 private static NISuppressor arg2_track0_result = 2681 new NISuppressor(2, 1, NumericInt.ZeroTrack.class); 2682 private static NISuppressor arg2_track0_arg1 = 2683 new NISuppressor(2, 0, NumericInt.ZeroTrack.class); 2684 2685 private static NISuppressor result_eq_1 = 2686 new NISuppressor(1, RangeFloat.EqualOne.class); 2687 private static NISuppressor arg1_eq_1 = 2688 new NISuppressor(0, RangeFloat.EqualOne.class); 2689 private static NISuppressor arg2_eq_1 = 2690 new NISuppressor(2, RangeFloat.EqualOne.class); 2691 2692 private static NISuppressor result_eq_0 = 2693 new NISuppressor(1, RangeFloat.EqualZero.class); 2694 private static NISuppressor arg1_eq_0 = 2695 new NISuppressor(0, RangeFloat.EqualZero.class); 2696 private static NISuppressor arg2_eq_0 = 2697 new NISuppressor(2, RangeFloat.EqualZero.class); 2698 2699 private static NISuppressor result_ne_0 = 2700 new NISuppressor(1, NonZeroFloat.class); 2701 private static NISuppressor arg1_ne_0 = 2702 new NISuppressor(0, NonZeroFloat.class); 2703 private static NISuppressor arg2_ne_0 = 2704 new NISuppressor(2, NonZeroFloat.class); 2705 2706 private static NISuppressor result_ge_0 = 2707 new NISuppressor(1, RangeFloat.GreaterEqualZero.class); 2708 private static NISuppressor arg1_ge_0 = 2709 new NISuppressor(0, RangeFloat.GreaterEqualZero.class); 2710 private static NISuppressor arg2_ge_0 = 2711 new NISuppressor(2, RangeFloat.GreaterEqualZero.class); 2712 2713 private static NISuppressor result_ge_64 = 2714 new NISuppressor(1, RangeInt.GreaterEqual64.class); 2715 private static NISuppressor arg1_ge_64 = 2716 new NISuppressor(0, RangeInt.GreaterEqual64.class); 2717 private static NISuppressor arg2_ge_64 = 2718 new NISuppressor(2, RangeInt.GreaterEqual64.class); 2719 2720 private static NISuppressionSet suppressions = 2721 new NISuppressionSet( 2722 new NISuppression[] { 2723 2724 // (x == z) && (z != 0) && (r == 1) 2725 new NISuppression(arg1_eq_arg2, arg2_ne_0, result_eq_1, suppressee), 2726 2727 // (r == x) && (z == 1) ==> r = x / z 2728 new NISuppression(result_eq_arg1, arg2_eq_1, suppressee), 2729 }); 2730 2731 // Create a suppression factory for functionBinary 2732 2733} 2734 2735/** 2736 * Represents the invariant {@code z = Division(x, y)} over three double 2737 * scalars. 2738 */ 2739public static class DivisionDouble_zxy extends FunctionBinaryFloat { 2740 // We are Serializable, so we specify a version to allow changes to 2741 // method signatures without breaking serialization. If you add or 2742 // remove fields, you should change this number to the current date. 2743 static final long serialVersionUID = 20031030L; 2744 2745 private static @Prototype DivisionDouble_zxy proto = new @Prototype DivisionDouble_zxy (); 2746 2747 /** Returns the prototype invariant for DivisionDouble_zxy */ 2748 public static @Prototype DivisionDouble_zxy get_proto() { 2749 return proto; 2750 } 2751 2752 /** instantiate an invariant on the specified slice */ 2753 @Override 2754 protected DivisionDouble_zxy instantiate_dyn(@Prototype DivisionDouble_zxy this, PptSlice slice) { 2755 return new DivisionDouble_zxy (slice); 2756 } 2757 2758 private DivisionDouble_zxy (PptSlice slice) { 2759 super(slice); 2760 } 2761 2762 public @Prototype DivisionDouble_zxy () { 2763 super(); 2764 } 2765 2766 private static String[] method_name = new String[] {"", " / ", ""}; 2767 2768 @Override 2769 public String[] get_method_name(@GuardSatisfied DivisionDouble_zxy this) { 2770 return method_name; 2771 } 2772 2773 private static int function_id = -1; 2774 2775 @Override 2776 public int get_function_id() { 2777 return function_id; 2778 } 2779 2780 @Override 2781 public void set_function_id(int function_id) { 2782 assert DivisionDouble_zxy.function_id == -1; 2783 DivisionDouble_zxy.function_id = function_id; 2784 } 2785 2786 private static int var_order = 3; 2787 2788 @Override 2789 public int get_var_order(@GuardSatisfied DivisionDouble_zxy this) { 2790 return var_order; 2791 } 2792 2793 @Pure 2794 @Override 2795 public boolean is_symmetric() { 2796 2797 return false; 2798 } 2799 2800 @Override 2801 2802 public double func(double x, double y) { 2803 2804 return (x / y); 2805 } 2806 2807 @Override 2808 public InvariantStatus check_modified(double x, double y, 2809 double z, int count) { 2810 return check_ordered(z, x, y, count); 2811 } 2812 2813 @Override 2814 public InvariantStatus add_modified(double x, double y, 2815 double z, int count) { 2816 if (Debug.logDetail()) { 2817 log("result=%s, arg1=%s, arg2=%s", z, x, y); 2818 } 2819 return add_ordered(z, x, y, count); 2820 } 2821 2822 @Pure 2823 @Override 2824 public boolean isDivision() { 2825 return true; 2826 } 2827 2828 @Pure 2829 @Override 2830 public boolean isExact() { 2831 return true; 2832 } 2833 2834 /** Returns a list of non-instantiating suppressions for this invariant. */ 2835 @Pure 2836 @Override 2837 public @Nullable NISuppressionSet get_ni_suppressions() { 2838 if (NIS.dkconfig_enabled && dkconfig_enabled) { 2839 return suppressions; 2840 } else { 2841 return null; 2842 } 2843 } 2844 2845 /** definition of this invariant (the suppressee) */ 2846 private static NISuppressee suppressee = new NISuppressee(DivisionDouble_zxy.class, 3); 2847 2848 // suppressor definitions (used below) 2849 private static NISuppressor result_eq_arg1 = 2850 new NISuppressor(2, 0, FloatEqual.class); 2851 private static NISuppressor result_eq_arg2 = 2852 new NISuppressor(2, 1, FloatEqual.class); 2853 private static NISuppressor arg1_eq_arg2 = 2854 new NISuppressor(0, 1, FloatEqual.class); 2855 2856 private static NISuppressor result_lt_arg1 = 2857 new NISuppressor(2, 0, FloatLessThan.class); 2858 private static NISuppressor result_lt_arg2 = 2859 new NISuppressor(2, 1, FloatLessThan.class); 2860 private static NISuppressor arg1_lt_arg2 = 2861 new NISuppressor(0, 1, FloatLessThan.class); 2862 private static NISuppressor arg2_lt_arg1 = 2863 new NISuppressor(1, 0, FloatLessThan.class); 2864 2865 private static NISuppressor result_le_arg1 = 2866 new NISuppressor(2, 0, FloatLessEqual.class); 2867 private static NISuppressor result_le_arg2 = 2868 new NISuppressor(2, 1, FloatLessEqual.class); 2869 private static NISuppressor arg1_le_arg2 = 2870 new NISuppressor(0, 1, FloatLessEqual.class); 2871 private static NISuppressor arg2_le_arg1 = 2872 new NISuppressor(1, 0, FloatLessEqual.class); 2873 2874 private static NISuppressor result_track0_arg1 = 2875 new NISuppressor(2, 0, NumericInt.ZeroTrack.class); 2876 private static NISuppressor result_track0_arg2 = 2877 new NISuppressor(2, 1, NumericInt.ZeroTrack.class); 2878 private static NISuppressor arg1_track0_arg2 = 2879 new NISuppressor(0, 1, NumericInt.ZeroTrack.class); 2880 private static NISuppressor arg1_track0_result = 2881 new NISuppressor(0, 2, NumericInt.ZeroTrack.class); 2882 private static NISuppressor arg2_track0_result = 2883 new NISuppressor(1, 2, NumericInt.ZeroTrack.class); 2884 private static NISuppressor arg2_track0_arg1 = 2885 new NISuppressor(1, 0, NumericInt.ZeroTrack.class); 2886 2887 private static NISuppressor result_eq_1 = 2888 new NISuppressor(2, RangeFloat.EqualOne.class); 2889 private static NISuppressor arg1_eq_1 = 2890 new NISuppressor(0, RangeFloat.EqualOne.class); 2891 private static NISuppressor arg2_eq_1 = 2892 new NISuppressor(1, RangeFloat.EqualOne.class); 2893 2894 private static NISuppressor result_eq_0 = 2895 new NISuppressor(2, RangeFloat.EqualZero.class); 2896 private static NISuppressor arg1_eq_0 = 2897 new NISuppressor(0, RangeFloat.EqualZero.class); 2898 private static NISuppressor arg2_eq_0 = 2899 new NISuppressor(1, RangeFloat.EqualZero.class); 2900 2901 private static NISuppressor result_ne_0 = 2902 new NISuppressor(2, NonZeroFloat.class); 2903 private static NISuppressor arg1_ne_0 = 2904 new NISuppressor(0, NonZeroFloat.class); 2905 private static NISuppressor arg2_ne_0 = 2906 new NISuppressor(1, NonZeroFloat.class); 2907 2908 private static NISuppressor result_ge_0 = 2909 new NISuppressor(2, RangeFloat.GreaterEqualZero.class); 2910 private static NISuppressor arg1_ge_0 = 2911 new NISuppressor(0, RangeFloat.GreaterEqualZero.class); 2912 private static NISuppressor arg2_ge_0 = 2913 new NISuppressor(1, RangeFloat.GreaterEqualZero.class); 2914 2915 private static NISuppressor result_ge_64 = 2916 new NISuppressor(2, RangeInt.GreaterEqual64.class); 2917 private static NISuppressor arg1_ge_64 = 2918 new NISuppressor(0, RangeInt.GreaterEqual64.class); 2919 private static NISuppressor arg2_ge_64 = 2920 new NISuppressor(1, RangeInt.GreaterEqual64.class); 2921 2922 private static NISuppressionSet suppressions = 2923 new NISuppressionSet( 2924 new NISuppression[] { 2925 2926 // (x == y) && (y != 0) && (r == 1) 2927 new NISuppression(arg1_eq_arg2, arg2_ne_0, result_eq_1, suppressee), 2928 2929 // (r == x) && (y == 1) ==> r = x / y 2930 new NISuppression(result_eq_arg1, arg2_eq_1, suppressee), 2931 }); 2932 2933 // Create a suppression factory for functionBinary 2934 2935} 2936 2937/** 2938 * Represents the invariant {@code x = Division(z, y)} over three double 2939 * scalars. 2940 */ 2941public static class DivisionDouble_xzy extends FunctionBinaryFloat { 2942 // We are Serializable, so we specify a version to allow changes to 2943 // method signatures without breaking serialization. If you add or 2944 // remove fields, you should change this number to the current date. 2945 static final long serialVersionUID = 20031030L; 2946 2947 private static @Prototype DivisionDouble_xzy proto = new @Prototype DivisionDouble_xzy (); 2948 2949 /** Returns the prototype invariant for DivisionDouble_xzy */ 2950 public static @Prototype DivisionDouble_xzy get_proto() { 2951 return proto; 2952 } 2953 2954 /** instantiate an invariant on the specified slice */ 2955 @Override 2956 protected DivisionDouble_xzy instantiate_dyn(@Prototype DivisionDouble_xzy this, PptSlice slice) { 2957 return new DivisionDouble_xzy (slice); 2958 } 2959 2960 private DivisionDouble_xzy (PptSlice slice) { 2961 super(slice); 2962 } 2963 2964 public @Prototype DivisionDouble_xzy () { 2965 super(); 2966 } 2967 2968 private static String[] method_name = new String[] {"", " / ", ""}; 2969 2970 @Override 2971 public String[] get_method_name(@GuardSatisfied DivisionDouble_xzy this) { 2972 return method_name; 2973 } 2974 2975 private static int function_id = -1; 2976 2977 @Override 2978 public int get_function_id() { 2979 return function_id; 2980 } 2981 2982 @Override 2983 public void set_function_id(int function_id) { 2984 assert DivisionDouble_xzy.function_id == -1; 2985 DivisionDouble_xzy.function_id = function_id; 2986 } 2987 2988 private static int var_order = 4; 2989 2990 @Override 2991 public int get_var_order(@GuardSatisfied DivisionDouble_xzy this) { 2992 return var_order; 2993 } 2994 2995 @Pure 2996 @Override 2997 public boolean is_symmetric() { 2998 2999 return false; 3000 } 3001 3002 @Override 3003 3004 public double func(double z, double y) { 3005 3006 return (z / y); 3007 } 3008 3009 @Override 3010 public InvariantStatus check_modified(double x, double y, 3011 double z, int count) { 3012 return check_ordered(x, z, y, count); 3013 } 3014 3015 @Override 3016 public InvariantStatus add_modified(double x, double y, 3017 double z, int count) { 3018 if (Debug.logDetail()) { 3019 log("result=%s, arg1=%s, arg2=%s", x, z, y); 3020 } 3021 return add_ordered(x, z, y, count); 3022 } 3023 3024 @Pure 3025 @Override 3026 public boolean isDivision() { 3027 return true; 3028 } 3029 3030 @Pure 3031 @Override 3032 public boolean isExact() { 3033 return true; 3034 } 3035 3036 /** Returns a list of non-instantiating suppressions for this invariant. */ 3037 @Pure 3038 @Override 3039 public @Nullable NISuppressionSet get_ni_suppressions() { 3040 if (NIS.dkconfig_enabled && dkconfig_enabled) { 3041 return suppressions; 3042 } else { 3043 return null; 3044 } 3045 } 3046 3047 /** definition of this invariant (the suppressee) */ 3048 private static NISuppressee suppressee = new NISuppressee(DivisionDouble_xzy.class, 3); 3049 3050 // suppressor definitions (used below) 3051 private static NISuppressor result_eq_arg1 = 3052 new NISuppressor(0, 2, FloatEqual.class); 3053 private static NISuppressor result_eq_arg2 = 3054 new NISuppressor(0, 1, FloatEqual.class); 3055 private static NISuppressor arg1_eq_arg2 = 3056 new NISuppressor(2, 1, FloatEqual.class); 3057 3058 private static NISuppressor result_lt_arg1 = 3059 new NISuppressor(0, 2, FloatLessThan.class); 3060 private static NISuppressor result_lt_arg2 = 3061 new NISuppressor(0, 1, FloatLessThan.class); 3062 private static NISuppressor arg1_lt_arg2 = 3063 new NISuppressor(2, 1, FloatLessThan.class); 3064 private static NISuppressor arg2_lt_arg1 = 3065 new NISuppressor(1, 2, FloatLessThan.class); 3066 3067 private static NISuppressor result_le_arg1 = 3068 new NISuppressor(0, 2, FloatLessEqual.class); 3069 private static NISuppressor result_le_arg2 = 3070 new NISuppressor(0, 1, FloatLessEqual.class); 3071 private static NISuppressor arg1_le_arg2 = 3072 new NISuppressor(2, 1, FloatLessEqual.class); 3073 private static NISuppressor arg2_le_arg1 = 3074 new NISuppressor(1, 2, FloatLessEqual.class); 3075 3076 private static NISuppressor result_track0_arg1 = 3077 new NISuppressor(0, 2, NumericInt.ZeroTrack.class); 3078 private static NISuppressor result_track0_arg2 = 3079 new NISuppressor(0, 1, NumericInt.ZeroTrack.class); 3080 private static NISuppressor arg1_track0_arg2 = 3081 new NISuppressor(2, 1, NumericInt.ZeroTrack.class); 3082 private static NISuppressor arg1_track0_result = 3083 new NISuppressor(2, 0, NumericInt.ZeroTrack.class); 3084 private static NISuppressor arg2_track0_result = 3085 new NISuppressor(1, 0, NumericInt.ZeroTrack.class); 3086 private static NISuppressor arg2_track0_arg1 = 3087 new NISuppressor(1, 2, NumericInt.ZeroTrack.class); 3088 3089 private static NISuppressor result_eq_1 = 3090 new NISuppressor(0, RangeFloat.EqualOne.class); 3091 private static NISuppressor arg1_eq_1 = 3092 new NISuppressor(2, RangeFloat.EqualOne.class); 3093 private static NISuppressor arg2_eq_1 = 3094 new NISuppressor(1, RangeFloat.EqualOne.class); 3095 3096 private static NISuppressor result_eq_0 = 3097 new NISuppressor(0, RangeFloat.EqualZero.class); 3098 private static NISuppressor arg1_eq_0 = 3099 new NISuppressor(2, RangeFloat.EqualZero.class); 3100 private static NISuppressor arg2_eq_0 = 3101 new NISuppressor(1, RangeFloat.EqualZero.class); 3102 3103 private static NISuppressor result_ne_0 = 3104 new NISuppressor(0, NonZeroFloat.class); 3105 private static NISuppressor arg1_ne_0 = 3106 new NISuppressor(2, NonZeroFloat.class); 3107 private static NISuppressor arg2_ne_0 = 3108 new NISuppressor(1, NonZeroFloat.class); 3109 3110 private static NISuppressor result_ge_0 = 3111 new NISuppressor(0, RangeFloat.GreaterEqualZero.class); 3112 private static NISuppressor arg1_ge_0 = 3113 new NISuppressor(2, RangeFloat.GreaterEqualZero.class); 3114 private static NISuppressor arg2_ge_0 = 3115 new NISuppressor(1, RangeFloat.GreaterEqualZero.class); 3116 3117 private static NISuppressor result_ge_64 = 3118 new NISuppressor(0, RangeInt.GreaterEqual64.class); 3119 private static NISuppressor arg1_ge_64 = 3120 new NISuppressor(2, RangeInt.GreaterEqual64.class); 3121 private static NISuppressor arg2_ge_64 = 3122 new NISuppressor(1, RangeInt.GreaterEqual64.class); 3123 3124 private static NISuppressionSet suppressions = 3125 new NISuppressionSet( 3126 new NISuppression[] { 3127 3128 // (z == y) && (y != 0) && (r == 1) 3129 new NISuppression(arg1_eq_arg2, arg2_ne_0, result_eq_1, suppressee), 3130 3131 // (r == z) && (y == 1) ==> r = z / y 3132 new NISuppression(result_eq_arg1, arg2_eq_1, suppressee), 3133 }); 3134 3135 // Create a suppression factory for functionBinary 3136 3137} 3138 3139/** 3140 * Represents the invariant {@code y = Division(z, x)} over three double 3141 * scalars. 3142 */ 3143public static class DivisionDouble_yzx extends FunctionBinaryFloat { 3144 // We are Serializable, so we specify a version to allow changes to 3145 // method signatures without breaking serialization. If you add or 3146 // remove fields, you should change this number to the current date. 3147 static final long serialVersionUID = 20031030L; 3148 3149 private static @Prototype DivisionDouble_yzx proto = new @Prototype DivisionDouble_yzx (); 3150 3151 /** Returns the prototype invariant for DivisionDouble_yzx */ 3152 public static @Prototype DivisionDouble_yzx get_proto() { 3153 return proto; 3154 } 3155 3156 /** instantiate an invariant on the specified slice */ 3157 @Override 3158 protected DivisionDouble_yzx instantiate_dyn(@Prototype DivisionDouble_yzx this, PptSlice slice) { 3159 return new DivisionDouble_yzx (slice); 3160 } 3161 3162 private DivisionDouble_yzx (PptSlice slice) { 3163 super(slice); 3164 } 3165 3166 public @Prototype DivisionDouble_yzx () { 3167 super(); 3168 } 3169 3170 private static String[] method_name = new String[] {"", " / ", ""}; 3171 3172 @Override 3173 public String[] get_method_name(@GuardSatisfied DivisionDouble_yzx this) { 3174 return method_name; 3175 } 3176 3177 private static int function_id = -1; 3178 3179 @Override 3180 public int get_function_id() { 3181 return function_id; 3182 } 3183 3184 @Override 3185 public void set_function_id(int function_id) { 3186 assert DivisionDouble_yzx.function_id == -1; 3187 DivisionDouble_yzx.function_id = function_id; 3188 } 3189 3190 private static int var_order = 5; 3191 3192 @Override 3193 public int get_var_order(@GuardSatisfied DivisionDouble_yzx this) { 3194 return var_order; 3195 } 3196 3197 @Pure 3198 @Override 3199 public boolean is_symmetric() { 3200 3201 return false; 3202 } 3203 3204 @Override 3205 3206 public double func(double z, double x) { 3207 3208 return (z / x); 3209 } 3210 3211 @Override 3212 public InvariantStatus check_modified(double x, double y, 3213 double z, int count) { 3214 return check_ordered(y, z, x, count); 3215 } 3216 3217 @Override 3218 public InvariantStatus add_modified(double x, double y, 3219 double z, int count) { 3220 if (Debug.logDetail()) { 3221 log("result=%s, arg1=%s, arg2=%s", y, z, x); 3222 } 3223 return add_ordered(y, z, x, count); 3224 } 3225 3226 @Pure 3227 @Override 3228 public boolean isDivision() { 3229 return true; 3230 } 3231 3232 @Pure 3233 @Override 3234 public boolean isExact() { 3235 return true; 3236 } 3237 3238 /** Returns a list of non-instantiating suppressions for this invariant. */ 3239 @Pure 3240 @Override 3241 public @Nullable NISuppressionSet get_ni_suppressions() { 3242 if (NIS.dkconfig_enabled && dkconfig_enabled) { 3243 return suppressions; 3244 } else { 3245 return null; 3246 } 3247 } 3248 3249 /** definition of this invariant (the suppressee) */ 3250 private static NISuppressee suppressee = new NISuppressee(DivisionDouble_yzx.class, 3); 3251 3252 // suppressor definitions (used below) 3253 private static NISuppressor result_eq_arg1 = 3254 new NISuppressor(1, 2, FloatEqual.class); 3255 private static NISuppressor result_eq_arg2 = 3256 new NISuppressor(1, 0, FloatEqual.class); 3257 private static NISuppressor arg1_eq_arg2 = 3258 new NISuppressor(2, 0, FloatEqual.class); 3259 3260 private static NISuppressor result_lt_arg1 = 3261 new NISuppressor(1, 2, FloatLessThan.class); 3262 private static NISuppressor result_lt_arg2 = 3263 new NISuppressor(1, 0, FloatLessThan.class); 3264 private static NISuppressor arg1_lt_arg2 = 3265 new NISuppressor(2, 0, FloatLessThan.class); 3266 private static NISuppressor arg2_lt_arg1 = 3267 new NISuppressor(0, 2, FloatLessThan.class); 3268 3269 private static NISuppressor result_le_arg1 = 3270 new NISuppressor(1, 2, FloatLessEqual.class); 3271 private static NISuppressor result_le_arg2 = 3272 new NISuppressor(1, 0, FloatLessEqual.class); 3273 private static NISuppressor arg1_le_arg2 = 3274 new NISuppressor(2, 0, FloatLessEqual.class); 3275 private static NISuppressor arg2_le_arg1 = 3276 new NISuppressor(0, 2, FloatLessEqual.class); 3277 3278 private static NISuppressor result_track0_arg1 = 3279 new NISuppressor(1, 2, NumericInt.ZeroTrack.class); 3280 private static NISuppressor result_track0_arg2 = 3281 new NISuppressor(1, 0, NumericInt.ZeroTrack.class); 3282 private static NISuppressor arg1_track0_arg2 = 3283 new NISuppressor(2, 0, NumericInt.ZeroTrack.class); 3284 private static NISuppressor arg1_track0_result = 3285 new NISuppressor(2, 1, NumericInt.ZeroTrack.class); 3286 private static NISuppressor arg2_track0_result = 3287 new NISuppressor(0, 1, NumericInt.ZeroTrack.class); 3288 private static NISuppressor arg2_track0_arg1 = 3289 new NISuppressor(0, 2, NumericInt.ZeroTrack.class); 3290 3291 private static NISuppressor result_eq_1 = 3292 new NISuppressor(1, RangeFloat.EqualOne.class); 3293 private static NISuppressor arg1_eq_1 = 3294 new NISuppressor(2, RangeFloat.EqualOne.class); 3295 private static NISuppressor arg2_eq_1 = 3296 new NISuppressor(0, RangeFloat.EqualOne.class); 3297 3298 private static NISuppressor result_eq_0 = 3299 new NISuppressor(1, RangeFloat.EqualZero.class); 3300 private static NISuppressor arg1_eq_0 = 3301 new NISuppressor(2, RangeFloat.EqualZero.class); 3302 private static NISuppressor arg2_eq_0 = 3303 new NISuppressor(0, RangeFloat.EqualZero.class); 3304 3305 private static NISuppressor result_ne_0 = 3306 new NISuppressor(1, NonZeroFloat.class); 3307 private static NISuppressor arg1_ne_0 = 3308 new NISuppressor(2, NonZeroFloat.class); 3309 private static NISuppressor arg2_ne_0 = 3310 new NISuppressor(0, NonZeroFloat.class); 3311 3312 private static NISuppressor result_ge_0 = 3313 new NISuppressor(1, RangeFloat.GreaterEqualZero.class); 3314 private static NISuppressor arg1_ge_0 = 3315 new NISuppressor(2, RangeFloat.GreaterEqualZero.class); 3316 private static NISuppressor arg2_ge_0 = 3317 new NISuppressor(0, RangeFloat.GreaterEqualZero.class); 3318 3319 private static NISuppressor result_ge_64 = 3320 new NISuppressor(1, RangeInt.GreaterEqual64.class); 3321 private static NISuppressor arg1_ge_64 = 3322 new NISuppressor(2, RangeInt.GreaterEqual64.class); 3323 private static NISuppressor arg2_ge_64 = 3324 new NISuppressor(0, RangeInt.GreaterEqual64.class); 3325 3326 private static NISuppressionSet suppressions = 3327 new NISuppressionSet( 3328 new NISuppression[] { 3329 3330 // (z == x) && (x != 0) && (r == 1) 3331 new NISuppression(arg1_eq_arg2, arg2_ne_0, result_eq_1, suppressee), 3332 3333 // (r == z) && (x == 1) ==> r = z / x 3334 new NISuppression(result_eq_arg1, arg2_eq_1, suppressee), 3335 }); 3336 3337 // Create a suppression factory for functionBinary 3338 3339} 3340 3341/** 3342 * Represents the invariant {@code z = Division(y, x)} over three double 3343 * scalars. 3344 */ 3345public static class DivisionDouble_zyx extends FunctionBinaryFloat { 3346 // We are Serializable, so we specify a version to allow changes to 3347 // method signatures without breaking serialization. If you add or 3348 // remove fields, you should change this number to the current date. 3349 static final long serialVersionUID = 20031030L; 3350 3351 private static @Prototype DivisionDouble_zyx proto = new @Prototype DivisionDouble_zyx (); 3352 3353 /** Returns the prototype invariant for DivisionDouble_zyx */ 3354 public static @Prototype DivisionDouble_zyx get_proto() { 3355 return proto; 3356 } 3357 3358 /** instantiate an invariant on the specified slice */ 3359 @Override 3360 protected DivisionDouble_zyx instantiate_dyn(@Prototype DivisionDouble_zyx this, PptSlice slice) { 3361 return new DivisionDouble_zyx (slice); 3362 } 3363 3364 private DivisionDouble_zyx (PptSlice slice) { 3365 super(slice); 3366 } 3367 3368 public @Prototype DivisionDouble_zyx () { 3369 super(); 3370 } 3371 3372 private static String[] method_name = new String[] {"", " / ", ""}; 3373 3374 @Override 3375 public String[] get_method_name(@GuardSatisfied DivisionDouble_zyx this) { 3376 return method_name; 3377 } 3378 3379 private static int function_id = -1; 3380 3381 @Override 3382 public int get_function_id() { 3383 return function_id; 3384 } 3385 3386 @Override 3387 public void set_function_id(int function_id) { 3388 assert DivisionDouble_zyx.function_id == -1; 3389 DivisionDouble_zyx.function_id = function_id; 3390 } 3391 3392 private static int var_order = 6; 3393 3394 @Override 3395 public int get_var_order(@GuardSatisfied DivisionDouble_zyx this) { 3396 return var_order; 3397 } 3398 3399 @Pure 3400 @Override 3401 public boolean is_symmetric() { 3402 3403 return false; 3404 } 3405 3406 @Override 3407 3408 public double func(double y, double x) { 3409 3410 return (y / x); 3411 } 3412 3413 @Override 3414 public InvariantStatus check_modified(double x, double y, 3415 double z, int count) { 3416 return check_ordered(z, y, x, count); 3417 } 3418 3419 @Override 3420 public InvariantStatus add_modified(double x, double y, 3421 double z, int count) { 3422 if (Debug.logDetail()) { 3423 log("result=%s, arg1=%s, arg2=%s", z, y, x); 3424 } 3425 return add_ordered(z, y, x, count); 3426 } 3427 3428 @Pure 3429 @Override 3430 public boolean isDivision() { 3431 return true; 3432 } 3433 3434 @Pure 3435 @Override 3436 public boolean isExact() { 3437 return true; 3438 } 3439 3440 /** Returns a list of non-instantiating suppressions for this invariant. */ 3441 @Pure 3442 @Override 3443 public @Nullable NISuppressionSet get_ni_suppressions() { 3444 if (NIS.dkconfig_enabled && dkconfig_enabled) { 3445 return suppressions; 3446 } else { 3447 return null; 3448 } 3449 } 3450 3451 /** definition of this invariant (the suppressee) */ 3452 private static NISuppressee suppressee = new NISuppressee(DivisionDouble_zyx.class, 3); 3453 3454 // suppressor definitions (used below) 3455 private static NISuppressor result_eq_arg1 = 3456 new NISuppressor(2, 1, FloatEqual.class); 3457 private static NISuppressor result_eq_arg2 = 3458 new NISuppressor(2, 0, FloatEqual.class); 3459 private static NISuppressor arg1_eq_arg2 = 3460 new NISuppressor(1, 0, FloatEqual.class); 3461 3462 private static NISuppressor result_lt_arg1 = 3463 new NISuppressor(2, 1, FloatLessThan.class); 3464 private static NISuppressor result_lt_arg2 = 3465 new NISuppressor(2, 0, FloatLessThan.class); 3466 private static NISuppressor arg1_lt_arg2 = 3467 new NISuppressor(1, 0, FloatLessThan.class); 3468 private static NISuppressor arg2_lt_arg1 = 3469 new NISuppressor(0, 1, FloatLessThan.class); 3470 3471 private static NISuppressor result_le_arg1 = 3472 new NISuppressor(2, 1, FloatLessEqual.class); 3473 private static NISuppressor result_le_arg2 = 3474 new NISuppressor(2, 0, FloatLessEqual.class); 3475 private static NISuppressor arg1_le_arg2 = 3476 new NISuppressor(1, 0, FloatLessEqual.class); 3477 private static NISuppressor arg2_le_arg1 = 3478 new NISuppressor(0, 1, FloatLessEqual.class); 3479 3480 private static NISuppressor result_track0_arg1 = 3481 new NISuppressor(2, 1, NumericInt.ZeroTrack.class); 3482 private static NISuppressor result_track0_arg2 = 3483 new NISuppressor(2, 0, NumericInt.ZeroTrack.class); 3484 private static NISuppressor arg1_track0_arg2 = 3485 new NISuppressor(1, 0, NumericInt.ZeroTrack.class); 3486 private static NISuppressor arg1_track0_result = 3487 new NISuppressor(1, 2, NumericInt.ZeroTrack.class); 3488 private static NISuppressor arg2_track0_result = 3489 new NISuppressor(0, 2, NumericInt.ZeroTrack.class); 3490 private static NISuppressor arg2_track0_arg1 = 3491 new NISuppressor(0, 1, NumericInt.ZeroTrack.class); 3492 3493 private static NISuppressor result_eq_1 = 3494 new NISuppressor(2, RangeFloat.EqualOne.class); 3495 private static NISuppressor arg1_eq_1 = 3496 new NISuppressor(1, RangeFloat.EqualOne.class); 3497 private static NISuppressor arg2_eq_1 = 3498 new NISuppressor(0, RangeFloat.EqualOne.class); 3499 3500 private static NISuppressor result_eq_0 = 3501 new NISuppressor(2, RangeFloat.EqualZero.class); 3502 private static NISuppressor arg1_eq_0 = 3503 new NISuppressor(1, RangeFloat.EqualZero.class); 3504 private static NISuppressor arg2_eq_0 = 3505 new NISuppressor(0, RangeFloat.EqualZero.class); 3506 3507 private static NISuppressor result_ne_0 = 3508 new NISuppressor(2, NonZeroFloat.class); 3509 private static NISuppressor arg1_ne_0 = 3510 new NISuppressor(1, NonZeroFloat.class); 3511 private static NISuppressor arg2_ne_0 = 3512 new NISuppressor(0, NonZeroFloat.class); 3513 3514 private static NISuppressor result_ge_0 = 3515 new NISuppressor(2, RangeFloat.GreaterEqualZero.class); 3516 private static NISuppressor arg1_ge_0 = 3517 new NISuppressor(1, RangeFloat.GreaterEqualZero.class); 3518 private static NISuppressor arg2_ge_0 = 3519 new NISuppressor(0, RangeFloat.GreaterEqualZero.class); 3520 3521 private static NISuppressor result_ge_64 = 3522 new NISuppressor(2, RangeInt.GreaterEqual64.class); 3523 private static NISuppressor arg1_ge_64 = 3524 new NISuppressor(1, RangeInt.GreaterEqual64.class); 3525 private static NISuppressor arg2_ge_64 = 3526 new NISuppressor(0, RangeInt.GreaterEqual64.class); 3527 3528 private static NISuppressionSet suppressions = 3529 new NISuppressionSet( 3530 new NISuppression[] { 3531 3532 // (y == x) && (x != 0) && (r == 1) 3533 new NISuppression(arg1_eq_arg2, arg2_ne_0, result_eq_1, suppressee), 3534 3535 // (r == y) && (x == 1) ==> r = y / x 3536 new NISuppression(result_eq_arg1, arg2_eq_1, suppressee), 3537 }); 3538 3539 // Create a suppression factory for functionBinary 3540 3541} 3542 3543 // default is that it is not this function, overriden in the subclass 3544 @Pure 3545 public boolean isPower() { 3546 return false; 3547 } 3548 3549/** 3550 * Represents the invariant {@code x = Power(y, z)} over three double 3551 * scalars. 3552 */ 3553public static class PowerDouble_xyz extends FunctionBinaryFloat { 3554 // We are Serializable, so we specify a version to allow changes to 3555 // method signatures without breaking serialization. If you add or 3556 // remove fields, you should change this number to the current date. 3557 static final long serialVersionUID = 20031030L; 3558 3559 private static @Prototype PowerDouble_xyz proto = new @Prototype PowerDouble_xyz (); 3560 3561 /** Returns the prototype invariant for PowerDouble_xyz */ 3562 public static @Prototype PowerDouble_xyz get_proto() { 3563 return proto; 3564 } 3565 3566 /** instantiate an invariant on the specified slice */ 3567 @Override 3568 protected PowerDouble_xyz instantiate_dyn(@Prototype PowerDouble_xyz this, PptSlice slice) { 3569 return new PowerDouble_xyz (slice); 3570 } 3571 3572 private PowerDouble_xyz (PptSlice slice) { 3573 super(slice); 3574 } 3575 3576 public @Prototype PowerDouble_xyz () { 3577 super(); 3578 } 3579 3580 private static String[] method_name = new String[] {"java.lang.Math.pow(", ", ", ")"}; 3581 3582 @Override 3583 public String[] get_method_name(@GuardSatisfied PowerDouble_xyz this) { 3584 return method_name; 3585 } 3586 3587 private static int function_id = -1; 3588 3589 @Override 3590 public int get_function_id() { 3591 return function_id; 3592 } 3593 3594 @Override 3595 public void set_function_id(int function_id) { 3596 assert PowerDouble_xyz.function_id == -1; 3597 PowerDouble_xyz.function_id = function_id; 3598 } 3599 3600 private static int var_order = 1; 3601 3602 @Override 3603 public int get_var_order(@GuardSatisfied PowerDouble_xyz this) { 3604 return var_order; 3605 } 3606 3607 @Pure 3608 @Override 3609 public boolean is_symmetric() { 3610 3611 return false; 3612 } 3613 3614 @Override 3615 3616 public double func(double y, double z) { 3617 3618 return Math.pow(y, z); 3619 } 3620 3621 @Override 3622 public InvariantStatus check_modified(double x, double y, 3623 double z, int count) { 3624 return check_ordered(x, y, z, count); 3625 } 3626 3627 @Override 3628 public InvariantStatus add_modified(double x, double y, 3629 double z, int count) { 3630 if (Debug.logDetail()) { 3631 log("result=%s, arg1=%s, arg2=%s", x, y, z); 3632 } 3633 return add_ordered(x, y, z, count); 3634 } 3635 3636 @Pure 3637 @Override 3638 public boolean isPower() { 3639 return true; 3640 } 3641 3642 @Pure 3643 @Override 3644 public boolean isExact() { 3645 return true; 3646 } 3647 3648 /** Returns a list of non-instantiating suppressions for this invariant. */ 3649 @Pure 3650 @Override 3651 public @Nullable NISuppressionSet get_ni_suppressions() { 3652 if (NIS.dkconfig_enabled && dkconfig_enabled) { 3653 return suppressions; 3654 } else { 3655 return null; 3656 } 3657 } 3658 3659 /** definition of this invariant (the suppressee) */ 3660 private static NISuppressee suppressee = new NISuppressee(PowerDouble_xyz.class, 3); 3661 3662 // suppressor definitions (used below) 3663 private static NISuppressor result_eq_arg1 = 3664 new NISuppressor(0, 1, FloatEqual.class); 3665 private static NISuppressor result_eq_arg2 = 3666 new NISuppressor(0, 2, FloatEqual.class); 3667 private static NISuppressor arg1_eq_arg2 = 3668 new NISuppressor(1, 2, FloatEqual.class); 3669 3670 private static NISuppressor result_lt_arg1 = 3671 new NISuppressor(0, 1, FloatLessThan.class); 3672 private static NISuppressor result_lt_arg2 = 3673 new NISuppressor(0, 2, FloatLessThan.class); 3674 private static NISuppressor arg1_lt_arg2 = 3675 new NISuppressor(1, 2, FloatLessThan.class); 3676 private static NISuppressor arg2_lt_arg1 = 3677 new NISuppressor(2, 1, FloatLessThan.class); 3678 3679 private static NISuppressor result_le_arg1 = 3680 new NISuppressor(0, 1, FloatLessEqual.class); 3681 private static NISuppressor result_le_arg2 = 3682 new NISuppressor(0, 2, FloatLessEqual.class); 3683 private static NISuppressor arg1_le_arg2 = 3684 new NISuppressor(1, 2, FloatLessEqual.class); 3685 private static NISuppressor arg2_le_arg1 = 3686 new NISuppressor(2, 1, FloatLessEqual.class); 3687 3688 private static NISuppressor result_track0_arg1 = 3689 new NISuppressor(0, 1, NumericInt.ZeroTrack.class); 3690 private static NISuppressor result_track0_arg2 = 3691 new NISuppressor(0, 2, NumericInt.ZeroTrack.class); 3692 private static NISuppressor arg1_track0_arg2 = 3693 new NISuppressor(1, 2, NumericInt.ZeroTrack.class); 3694 private static NISuppressor arg1_track0_result = 3695 new NISuppressor(1, 0, NumericInt.ZeroTrack.class); 3696 private static NISuppressor arg2_track0_result = 3697 new NISuppressor(2, 0, NumericInt.ZeroTrack.class); 3698 private static NISuppressor arg2_track0_arg1 = 3699 new NISuppressor(2, 1, NumericInt.ZeroTrack.class); 3700 3701 private static NISuppressor result_eq_1 = 3702 new NISuppressor(0, RangeFloat.EqualOne.class); 3703 private static NISuppressor arg1_eq_1 = 3704 new NISuppressor(1, RangeFloat.EqualOne.class); 3705 private static NISuppressor arg2_eq_1 = 3706 new NISuppressor(2, RangeFloat.EqualOne.class); 3707 3708 private static NISuppressor result_eq_0 = 3709 new NISuppressor(0, RangeFloat.EqualZero.class); 3710 private static NISuppressor arg1_eq_0 = 3711 new NISuppressor(1, RangeFloat.EqualZero.class); 3712 private static NISuppressor arg2_eq_0 = 3713 new NISuppressor(2, RangeFloat.EqualZero.class); 3714 3715 private static NISuppressor result_ne_0 = 3716 new NISuppressor(0, NonZeroFloat.class); 3717 private static NISuppressor arg1_ne_0 = 3718 new NISuppressor(1, NonZeroFloat.class); 3719 private static NISuppressor arg2_ne_0 = 3720 new NISuppressor(2, NonZeroFloat.class); 3721 3722 private static NISuppressor result_ge_0 = 3723 new NISuppressor(0, RangeFloat.GreaterEqualZero.class); 3724 private static NISuppressor arg1_ge_0 = 3725 new NISuppressor(1, RangeFloat.GreaterEqualZero.class); 3726 private static NISuppressor arg2_ge_0 = 3727 new NISuppressor(2, RangeFloat.GreaterEqualZero.class); 3728 3729 private static NISuppressor result_ge_64 = 3730 new NISuppressor(0, RangeInt.GreaterEqual64.class); 3731 private static NISuppressor arg1_ge_64 = 3732 new NISuppressor(1, RangeInt.GreaterEqual64.class); 3733 private static NISuppressor arg2_ge_64 = 3734 new NISuppressor(2, RangeInt.GreaterEqual64.class); 3735 3736 // Note that any suppression that doesn't limit z to valid exponents 3737 // (>= 0), must check for valid exponents as well (so that the invariant 3738 // is correctly destroyed on invalid exponents) 3739 // 3740 // Note also that pow(0,0) == 1 and pow(0,x), where (x > 0), == 0 3741 // Another interesting artificat of pow is that for any even base, any 3742 // exponent >= 64 will yield a result of 0. For example, pow(10,256) == 0 3743 // (at least for integers) 3744 3745 private static NISuppressionSet suppressions = 3746 new NISuppressionSet( 3747 new NISuppression[] { 3748 3749 // (r == 1) && (z == 0) ==> r = pow (y, z) 3750 new NISuppression(result_eq_1, arg2_eq_0, suppressee), 3751 3752 // (r == 1) && (y == 1) && (z >= 0) ==> r = pow (y, z) 3753 new NISuppression(result_eq_1, arg1_eq_1, arg2_ge_0, suppressee), 3754 3755 // (r == 0) && (y == 0) && (z > 0) 3756 new NISuppression(result_eq_0, arg1_eq_0, arg2_ne_0, arg2_ge_0, 3757 suppressee), 3758 3759 // (r == y) && (z == 1) ==> r = pow (y, z) 3760 new NISuppression(result_eq_arg1, arg2_eq_1, suppressee), 3761 3762 }); 3763 3764 // Create a suppression factory for functionBinary 3765 3766} 3767 3768/** 3769 * Represents the invariant {@code y = Power(x, z)} over three double 3770 * scalars. 3771 */ 3772public static class PowerDouble_yxz extends FunctionBinaryFloat { 3773 // We are Serializable, so we specify a version to allow changes to 3774 // method signatures without breaking serialization. If you add or 3775 // remove fields, you should change this number to the current date. 3776 static final long serialVersionUID = 20031030L; 3777 3778 private static @Prototype PowerDouble_yxz proto = new @Prototype PowerDouble_yxz (); 3779 3780 /** Returns the prototype invariant for PowerDouble_yxz */ 3781 public static @Prototype PowerDouble_yxz get_proto() { 3782 return proto; 3783 } 3784 3785 /** instantiate an invariant on the specified slice */ 3786 @Override 3787 protected PowerDouble_yxz instantiate_dyn(@Prototype PowerDouble_yxz this, PptSlice slice) { 3788 return new PowerDouble_yxz (slice); 3789 } 3790 3791 private PowerDouble_yxz (PptSlice slice) { 3792 super(slice); 3793 } 3794 3795 public @Prototype PowerDouble_yxz () { 3796 super(); 3797 } 3798 3799 private static String[] method_name = new String[] {"java.lang.Math.pow(", ", ", ")"}; 3800 3801 @Override 3802 public String[] get_method_name(@GuardSatisfied PowerDouble_yxz this) { 3803 return method_name; 3804 } 3805 3806 private static int function_id = -1; 3807 3808 @Override 3809 public int get_function_id() { 3810 return function_id; 3811 } 3812 3813 @Override 3814 public void set_function_id(int function_id) { 3815 assert PowerDouble_yxz.function_id == -1; 3816 PowerDouble_yxz.function_id = function_id; 3817 } 3818 3819 private static int var_order = 2; 3820 3821 @Override 3822 public int get_var_order(@GuardSatisfied PowerDouble_yxz this) { 3823 return var_order; 3824 } 3825 3826 @Pure 3827 @Override 3828 public boolean is_symmetric() { 3829 3830 return false; 3831 } 3832 3833 @Override 3834 3835 public double func(double x, double z) { 3836 3837 return Math.pow(x, z); 3838 } 3839 3840 @Override 3841 public InvariantStatus check_modified(double x, double y, 3842 double z, int count) { 3843 return check_ordered(y, x, z, count); 3844 } 3845 3846 @Override 3847 public InvariantStatus add_modified(double x, double y, 3848 double z, int count) { 3849 if (Debug.logDetail()) { 3850 log("result=%s, arg1=%s, arg2=%s", y, x, z); 3851 } 3852 return add_ordered(y, x, z, count); 3853 } 3854 3855 @Pure 3856 @Override 3857 public boolean isPower() { 3858 return true; 3859 } 3860 3861 @Pure 3862 @Override 3863 public boolean isExact() { 3864 return true; 3865 } 3866 3867 /** Returns a list of non-instantiating suppressions for this invariant. */ 3868 @Pure 3869 @Override 3870 public @Nullable NISuppressionSet get_ni_suppressions() { 3871 if (NIS.dkconfig_enabled && dkconfig_enabled) { 3872 return suppressions; 3873 } else { 3874 return null; 3875 } 3876 } 3877 3878 /** definition of this invariant (the suppressee) */ 3879 private static NISuppressee suppressee = new NISuppressee(PowerDouble_yxz.class, 3); 3880 3881 // suppressor definitions (used below) 3882 private static NISuppressor result_eq_arg1 = 3883 new NISuppressor(1, 0, FloatEqual.class); 3884 private static NISuppressor result_eq_arg2 = 3885 new NISuppressor(1, 2, FloatEqual.class); 3886 private static NISuppressor arg1_eq_arg2 = 3887 new NISuppressor(0, 2, FloatEqual.class); 3888 3889 private static NISuppressor result_lt_arg1 = 3890 new NISuppressor(1, 0, FloatLessThan.class); 3891 private static NISuppressor result_lt_arg2 = 3892 new NISuppressor(1, 2, FloatLessThan.class); 3893 private static NISuppressor arg1_lt_arg2 = 3894 new NISuppressor(0, 2, FloatLessThan.class); 3895 private static NISuppressor arg2_lt_arg1 = 3896 new NISuppressor(2, 0, FloatLessThan.class); 3897 3898 private static NISuppressor result_le_arg1 = 3899 new NISuppressor(1, 0, FloatLessEqual.class); 3900 private static NISuppressor result_le_arg2 = 3901 new NISuppressor(1, 2, FloatLessEqual.class); 3902 private static NISuppressor arg1_le_arg2 = 3903 new NISuppressor(0, 2, FloatLessEqual.class); 3904 private static NISuppressor arg2_le_arg1 = 3905 new NISuppressor(2, 0, FloatLessEqual.class); 3906 3907 private static NISuppressor result_track0_arg1 = 3908 new NISuppressor(1, 0, NumericInt.ZeroTrack.class); 3909 private static NISuppressor result_track0_arg2 = 3910 new NISuppressor(1, 2, NumericInt.ZeroTrack.class); 3911 private static NISuppressor arg1_track0_arg2 = 3912 new NISuppressor(0, 2, NumericInt.ZeroTrack.class); 3913 private static NISuppressor arg1_track0_result = 3914 new NISuppressor(0, 1, NumericInt.ZeroTrack.class); 3915 private static NISuppressor arg2_track0_result = 3916 new NISuppressor(2, 1, NumericInt.ZeroTrack.class); 3917 private static NISuppressor arg2_track0_arg1 = 3918 new NISuppressor(2, 0, NumericInt.ZeroTrack.class); 3919 3920 private static NISuppressor result_eq_1 = 3921 new NISuppressor(1, RangeFloat.EqualOne.class); 3922 private static NISuppressor arg1_eq_1 = 3923 new NISuppressor(0, RangeFloat.EqualOne.class); 3924 private static NISuppressor arg2_eq_1 = 3925 new NISuppressor(2, RangeFloat.EqualOne.class); 3926 3927 private static NISuppressor result_eq_0 = 3928 new NISuppressor(1, RangeFloat.EqualZero.class); 3929 private static NISuppressor arg1_eq_0 = 3930 new NISuppressor(0, RangeFloat.EqualZero.class); 3931 private static NISuppressor arg2_eq_0 = 3932 new NISuppressor(2, RangeFloat.EqualZero.class); 3933 3934 private static NISuppressor result_ne_0 = 3935 new NISuppressor(1, NonZeroFloat.class); 3936 private static NISuppressor arg1_ne_0 = 3937 new NISuppressor(0, NonZeroFloat.class); 3938 private static NISuppressor arg2_ne_0 = 3939 new NISuppressor(2, NonZeroFloat.class); 3940 3941 private static NISuppressor result_ge_0 = 3942 new NISuppressor(1, RangeFloat.GreaterEqualZero.class); 3943 private static NISuppressor arg1_ge_0 = 3944 new NISuppressor(0, RangeFloat.GreaterEqualZero.class); 3945 private static NISuppressor arg2_ge_0 = 3946 new NISuppressor(2, RangeFloat.GreaterEqualZero.class); 3947 3948 private static NISuppressor result_ge_64 = 3949 new NISuppressor(1, RangeInt.GreaterEqual64.class); 3950 private static NISuppressor arg1_ge_64 = 3951 new NISuppressor(0, RangeInt.GreaterEqual64.class); 3952 private static NISuppressor arg2_ge_64 = 3953 new NISuppressor(2, RangeInt.GreaterEqual64.class); 3954 3955 // Note that any suppression that doesn't limit z to valid exponents 3956 // (>= 0), must check for valid exponents as well (so that the invariant 3957 // is correctly destroyed on invalid exponents) 3958 // 3959 // Note also that pow(0,0) == 1 and pow(0,x), where (x > 0), == 0 3960 // Another interesting artificat of pow is that for any even base, any 3961 // exponent >= 64 will yield a result of 0. For example, pow(10,256) == 0 3962 // (at least for integers) 3963 3964 private static NISuppressionSet suppressions = 3965 new NISuppressionSet( 3966 new NISuppression[] { 3967 3968 // (r == 1) && (z == 0) ==> r = pow (x, z) 3969 new NISuppression(result_eq_1, arg2_eq_0, suppressee), 3970 3971 // (r == 1) && (x == 1) && (z >= 0) ==> r = pow (x, z) 3972 new NISuppression(result_eq_1, arg1_eq_1, arg2_ge_0, suppressee), 3973 3974 // (r == 0) && (x == 0) && (z > 0) 3975 new NISuppression(result_eq_0, arg1_eq_0, arg2_ne_0, arg2_ge_0, 3976 suppressee), 3977 3978 // (r == x) && (z == 1) ==> r = pow (x, z) 3979 new NISuppression(result_eq_arg1, arg2_eq_1, suppressee), 3980 3981 }); 3982 3983 // Create a suppression factory for functionBinary 3984 3985} 3986 3987/** 3988 * Represents the invariant {@code z = Power(x, y)} over three double 3989 * scalars. 3990 */ 3991public static class PowerDouble_zxy extends FunctionBinaryFloat { 3992 // We are Serializable, so we specify a version to allow changes to 3993 // method signatures without breaking serialization. If you add or 3994 // remove fields, you should change this number to the current date. 3995 static final long serialVersionUID = 20031030L; 3996 3997 private static @Prototype PowerDouble_zxy proto = new @Prototype PowerDouble_zxy (); 3998 3999 /** Returns the prototype invariant for PowerDouble_zxy */ 4000 public static @Prototype PowerDouble_zxy get_proto() { 4001 return proto; 4002 } 4003 4004 /** instantiate an invariant on the specified slice */ 4005 @Override 4006 protected PowerDouble_zxy instantiate_dyn(@Prototype PowerDouble_zxy this, PptSlice slice) { 4007 return new PowerDouble_zxy (slice); 4008 } 4009 4010 private PowerDouble_zxy (PptSlice slice) { 4011 super(slice); 4012 } 4013 4014 public @Prototype PowerDouble_zxy () { 4015 super(); 4016 } 4017 4018 private static String[] method_name = new String[] {"java.lang.Math.pow(", ", ", ")"}; 4019 4020 @Override 4021 public String[] get_method_name(@GuardSatisfied PowerDouble_zxy this) { 4022 return method_name; 4023 } 4024 4025 private static int function_id = -1; 4026 4027 @Override 4028 public int get_function_id() { 4029 return function_id; 4030 } 4031 4032 @Override 4033 public void set_function_id(int function_id) { 4034 assert PowerDouble_zxy.function_id == -1; 4035 PowerDouble_zxy.function_id = function_id; 4036 } 4037 4038 private static int var_order = 3; 4039 4040 @Override 4041 public int get_var_order(@GuardSatisfied PowerDouble_zxy this) { 4042 return var_order; 4043 } 4044 4045 @Pure 4046 @Override 4047 public boolean is_symmetric() { 4048 4049 return false; 4050 } 4051 4052 @Override 4053 4054 public double func(double x, double y) { 4055 4056 return Math.pow(x, y); 4057 } 4058 4059 @Override 4060 public InvariantStatus check_modified(double x, double y, 4061 double z, int count) { 4062 return check_ordered(z, x, y, count); 4063 } 4064 4065 @Override 4066 public InvariantStatus add_modified(double x, double y, 4067 double z, int count) { 4068 if (Debug.logDetail()) { 4069 log("result=%s, arg1=%s, arg2=%s", z, x, y); 4070 } 4071 return add_ordered(z, x, y, count); 4072 } 4073 4074 @Pure 4075 @Override 4076 public boolean isPower() { 4077 return true; 4078 } 4079 4080 @Pure 4081 @Override 4082 public boolean isExact() { 4083 return true; 4084 } 4085 4086 /** Returns a list of non-instantiating suppressions for this invariant. */ 4087 @Pure 4088 @Override 4089 public @Nullable NISuppressionSet get_ni_suppressions() { 4090 if (NIS.dkconfig_enabled && dkconfig_enabled) { 4091 return suppressions; 4092 } else { 4093 return null; 4094 } 4095 } 4096 4097 /** definition of this invariant (the suppressee) */ 4098 private static NISuppressee suppressee = new NISuppressee(PowerDouble_zxy.class, 3); 4099 4100 // suppressor definitions (used below) 4101 private static NISuppressor result_eq_arg1 = 4102 new NISuppressor(2, 0, FloatEqual.class); 4103 private static NISuppressor result_eq_arg2 = 4104 new NISuppressor(2, 1, FloatEqual.class); 4105 private static NISuppressor arg1_eq_arg2 = 4106 new NISuppressor(0, 1, FloatEqual.class); 4107 4108 private static NISuppressor result_lt_arg1 = 4109 new NISuppressor(2, 0, FloatLessThan.class); 4110 private static NISuppressor result_lt_arg2 = 4111 new NISuppressor(2, 1, FloatLessThan.class); 4112 private static NISuppressor arg1_lt_arg2 = 4113 new NISuppressor(0, 1, FloatLessThan.class); 4114 private static NISuppressor arg2_lt_arg1 = 4115 new NISuppressor(1, 0, FloatLessThan.class); 4116 4117 private static NISuppressor result_le_arg1 = 4118 new NISuppressor(2, 0, FloatLessEqual.class); 4119 private static NISuppressor result_le_arg2 = 4120 new NISuppressor(2, 1, FloatLessEqual.class); 4121 private static NISuppressor arg1_le_arg2 = 4122 new NISuppressor(0, 1, FloatLessEqual.class); 4123 private static NISuppressor arg2_le_arg1 = 4124 new NISuppressor(1, 0, FloatLessEqual.class); 4125 4126 private static NISuppressor result_track0_arg1 = 4127 new NISuppressor(2, 0, NumericInt.ZeroTrack.class); 4128 private static NISuppressor result_track0_arg2 = 4129 new NISuppressor(2, 1, NumericInt.ZeroTrack.class); 4130 private static NISuppressor arg1_track0_arg2 = 4131 new NISuppressor(0, 1, NumericInt.ZeroTrack.class); 4132 private static NISuppressor arg1_track0_result = 4133 new NISuppressor(0, 2, NumericInt.ZeroTrack.class); 4134 private static NISuppressor arg2_track0_result = 4135 new NISuppressor(1, 2, NumericInt.ZeroTrack.class); 4136 private static NISuppressor arg2_track0_arg1 = 4137 new NISuppressor(1, 0, NumericInt.ZeroTrack.class); 4138 4139 private static NISuppressor result_eq_1 = 4140 new NISuppressor(2, RangeFloat.EqualOne.class); 4141 private static NISuppressor arg1_eq_1 = 4142 new NISuppressor(0, RangeFloat.EqualOne.class); 4143 private static NISuppressor arg2_eq_1 = 4144 new NISuppressor(1, RangeFloat.EqualOne.class); 4145 4146 private static NISuppressor result_eq_0 = 4147 new NISuppressor(2, RangeFloat.EqualZero.class); 4148 private static NISuppressor arg1_eq_0 = 4149 new NISuppressor(0, RangeFloat.EqualZero.class); 4150 private static NISuppressor arg2_eq_0 = 4151 new NISuppressor(1, RangeFloat.EqualZero.class); 4152 4153 private static NISuppressor result_ne_0 = 4154 new NISuppressor(2, NonZeroFloat.class); 4155 private static NISuppressor arg1_ne_0 = 4156 new NISuppressor(0, NonZeroFloat.class); 4157 private static NISuppressor arg2_ne_0 = 4158 new NISuppressor(1, NonZeroFloat.class); 4159 4160 private static NISuppressor result_ge_0 = 4161 new NISuppressor(2, RangeFloat.GreaterEqualZero.class); 4162 private static NISuppressor arg1_ge_0 = 4163 new NISuppressor(0, RangeFloat.GreaterEqualZero.class); 4164 private static NISuppressor arg2_ge_0 = 4165 new NISuppressor(1, RangeFloat.GreaterEqualZero.class); 4166 4167 private static NISuppressor result_ge_64 = 4168 new NISuppressor(2, RangeInt.GreaterEqual64.class); 4169 private static NISuppressor arg1_ge_64 = 4170 new NISuppressor(0, RangeInt.GreaterEqual64.class); 4171 private static NISuppressor arg2_ge_64 = 4172 new NISuppressor(1, RangeInt.GreaterEqual64.class); 4173 4174 // Note that any suppression that doesn't limit y to valid exponents 4175 // (>= 0), must check for valid exponents as well (so that the invariant 4176 // is correctly destroyed on invalid exponents) 4177 // 4178 // Note also that pow(0,0) == 1 and pow(0,x), where (x > 0), == 0 4179 // Another interesting artificat of pow is that for any even base, any 4180 // exponent >= 64 will yield a result of 0. For example, pow(10,256) == 0 4181 // (at least for integers) 4182 4183 private static NISuppressionSet suppressions = 4184 new NISuppressionSet( 4185 new NISuppression[] { 4186 4187 // (r == 1) && (y == 0) ==> r = pow (x, y) 4188 new NISuppression(result_eq_1, arg2_eq_0, suppressee), 4189 4190 // (r == 1) && (x == 1) && (y >= 0) ==> r = pow (x, y) 4191 new NISuppression(result_eq_1, arg1_eq_1, arg2_ge_0, suppressee), 4192 4193 // (r == 0) && (x == 0) && (y > 0) 4194 new NISuppression(result_eq_0, arg1_eq_0, arg2_ne_0, arg2_ge_0, 4195 suppressee), 4196 4197 // (r == x) && (y == 1) ==> r = pow (x, y) 4198 new NISuppression(result_eq_arg1, arg2_eq_1, suppressee), 4199 4200 }); 4201 4202 // Create a suppression factory for functionBinary 4203 4204} 4205 4206/** 4207 * Represents the invariant {@code x = Power(z, y)} over three double 4208 * scalars. 4209 */ 4210public static class PowerDouble_xzy extends FunctionBinaryFloat { 4211 // We are Serializable, so we specify a version to allow changes to 4212 // method signatures without breaking serialization. If you add or 4213 // remove fields, you should change this number to the current date. 4214 static final long serialVersionUID = 20031030L; 4215 4216 private static @Prototype PowerDouble_xzy proto = new @Prototype PowerDouble_xzy (); 4217 4218 /** Returns the prototype invariant for PowerDouble_xzy */ 4219 public static @Prototype PowerDouble_xzy get_proto() { 4220 return proto; 4221 } 4222 4223 /** instantiate an invariant on the specified slice */ 4224 @Override 4225 protected PowerDouble_xzy instantiate_dyn(@Prototype PowerDouble_xzy this, PptSlice slice) { 4226 return new PowerDouble_xzy (slice); 4227 } 4228 4229 private PowerDouble_xzy (PptSlice slice) { 4230 super(slice); 4231 } 4232 4233 public @Prototype PowerDouble_xzy () { 4234 super(); 4235 } 4236 4237 private static String[] method_name = new String[] {"java.lang.Math.pow(", ", ", ")"}; 4238 4239 @Override 4240 public String[] get_method_name(@GuardSatisfied PowerDouble_xzy this) { 4241 return method_name; 4242 } 4243 4244 private static int function_id = -1; 4245 4246 @Override 4247 public int get_function_id() { 4248 return function_id; 4249 } 4250 4251 @Override 4252 public void set_function_id(int function_id) { 4253 assert PowerDouble_xzy.function_id == -1; 4254 PowerDouble_xzy.function_id = function_id; 4255 } 4256 4257 private static int var_order = 4; 4258 4259 @Override 4260 public int get_var_order(@GuardSatisfied PowerDouble_xzy this) { 4261 return var_order; 4262 } 4263 4264 @Pure 4265 @Override 4266 public boolean is_symmetric() { 4267 4268 return false; 4269 } 4270 4271 @Override 4272 4273 public double func(double z, double y) { 4274 4275 return Math.pow(z, y); 4276 } 4277 4278 @Override 4279 public InvariantStatus check_modified(double x, double y, 4280 double z, int count) { 4281 return check_ordered(x, z, y, count); 4282 } 4283 4284 @Override 4285 public InvariantStatus add_modified(double x, double y, 4286 double z, int count) { 4287 if (Debug.logDetail()) { 4288 log("result=%s, arg1=%s, arg2=%s", x, z, y); 4289 } 4290 return add_ordered(x, z, y, count); 4291 } 4292 4293 @Pure 4294 @Override 4295 public boolean isPower() { 4296 return true; 4297 } 4298 4299 @Pure 4300 @Override 4301 public boolean isExact() { 4302 return true; 4303 } 4304 4305 /** Returns a list of non-instantiating suppressions for this invariant. */ 4306 @Pure 4307 @Override 4308 public @Nullable NISuppressionSet get_ni_suppressions() { 4309 if (NIS.dkconfig_enabled && dkconfig_enabled) { 4310 return suppressions; 4311 } else { 4312 return null; 4313 } 4314 } 4315 4316 /** definition of this invariant (the suppressee) */ 4317 private static NISuppressee suppressee = new NISuppressee(PowerDouble_xzy.class, 3); 4318 4319 // suppressor definitions (used below) 4320 private static NISuppressor result_eq_arg1 = 4321 new NISuppressor(0, 2, FloatEqual.class); 4322 private static NISuppressor result_eq_arg2 = 4323 new NISuppressor(0, 1, FloatEqual.class); 4324 private static NISuppressor arg1_eq_arg2 = 4325 new NISuppressor(2, 1, FloatEqual.class); 4326 4327 private static NISuppressor result_lt_arg1 = 4328 new NISuppressor(0, 2, FloatLessThan.class); 4329 private static NISuppressor result_lt_arg2 = 4330 new NISuppressor(0, 1, FloatLessThan.class); 4331 private static NISuppressor arg1_lt_arg2 = 4332 new NISuppressor(2, 1, FloatLessThan.class); 4333 private static NISuppressor arg2_lt_arg1 = 4334 new NISuppressor(1, 2, FloatLessThan.class); 4335 4336 private static NISuppressor result_le_arg1 = 4337 new NISuppressor(0, 2, FloatLessEqual.class); 4338 private static NISuppressor result_le_arg2 = 4339 new NISuppressor(0, 1, FloatLessEqual.class); 4340 private static NISuppressor arg1_le_arg2 = 4341 new NISuppressor(2, 1, FloatLessEqual.class); 4342 private static NISuppressor arg2_le_arg1 = 4343 new NISuppressor(1, 2, FloatLessEqual.class); 4344 4345 private static NISuppressor result_track0_arg1 = 4346 new NISuppressor(0, 2, NumericInt.ZeroTrack.class); 4347 private static NISuppressor result_track0_arg2 = 4348 new NISuppressor(0, 1, NumericInt.ZeroTrack.class); 4349 private static NISuppressor arg1_track0_arg2 = 4350 new NISuppressor(2, 1, NumericInt.ZeroTrack.class); 4351 private static NISuppressor arg1_track0_result = 4352 new NISuppressor(2, 0, NumericInt.ZeroTrack.class); 4353 private static NISuppressor arg2_track0_result = 4354 new NISuppressor(1, 0, NumericInt.ZeroTrack.class); 4355 private static NISuppressor arg2_track0_arg1 = 4356 new NISuppressor(1, 2, NumericInt.ZeroTrack.class); 4357 4358 private static NISuppressor result_eq_1 = 4359 new NISuppressor(0, RangeFloat.EqualOne.class); 4360 private static NISuppressor arg1_eq_1 = 4361 new NISuppressor(2, RangeFloat.EqualOne.class); 4362 private static NISuppressor arg2_eq_1 = 4363 new NISuppressor(1, RangeFloat.EqualOne.class); 4364 4365 private static NISuppressor result_eq_0 = 4366 new NISuppressor(0, RangeFloat.EqualZero.class); 4367 private static NISuppressor arg1_eq_0 = 4368 new NISuppressor(2, RangeFloat.EqualZero.class); 4369 private static NISuppressor arg2_eq_0 = 4370 new NISuppressor(1, RangeFloat.EqualZero.class); 4371 4372 private static NISuppressor result_ne_0 = 4373 new NISuppressor(0, NonZeroFloat.class); 4374 private static NISuppressor arg1_ne_0 = 4375 new NISuppressor(2, NonZeroFloat.class); 4376 private static NISuppressor arg2_ne_0 = 4377 new NISuppressor(1, NonZeroFloat.class); 4378 4379 private static NISuppressor result_ge_0 = 4380 new NISuppressor(0, RangeFloat.GreaterEqualZero.class); 4381 private static NISuppressor arg1_ge_0 = 4382 new NISuppressor(2, RangeFloat.GreaterEqualZero.class); 4383 private static NISuppressor arg2_ge_0 = 4384 new NISuppressor(1, RangeFloat.GreaterEqualZero.class); 4385 4386 private static NISuppressor result_ge_64 = 4387 new NISuppressor(0, RangeInt.GreaterEqual64.class); 4388 private static NISuppressor arg1_ge_64 = 4389 new NISuppressor(2, RangeInt.GreaterEqual64.class); 4390 private static NISuppressor arg2_ge_64 = 4391 new NISuppressor(1, RangeInt.GreaterEqual64.class); 4392 4393 // Note that any suppression that doesn't limit y to valid exponents 4394 // (>= 0), must check for valid exponents as well (so that the invariant 4395 // is correctly destroyed on invalid exponents) 4396 // 4397 // Note also that pow(0,0) == 1 and pow(0,x), where (x > 0), == 0 4398 // Another interesting artificat of pow is that for any even base, any 4399 // exponent >= 64 will yield a result of 0. For example, pow(10,256) == 0 4400 // (at least for integers) 4401 4402 private static NISuppressionSet suppressions = 4403 new NISuppressionSet( 4404 new NISuppression[] { 4405 4406 // (r == 1) && (y == 0) ==> r = pow (z, y) 4407 new NISuppression(result_eq_1, arg2_eq_0, suppressee), 4408 4409 // (r == 1) && (z == 1) && (y >= 0) ==> r = pow (z, y) 4410 new NISuppression(result_eq_1, arg1_eq_1, arg2_ge_0, suppressee), 4411 4412 // (r == 0) && (z == 0) && (y > 0) 4413 new NISuppression(result_eq_0, arg1_eq_0, arg2_ne_0, arg2_ge_0, 4414 suppressee), 4415 4416 // (r == z) && (y == 1) ==> r = pow (z, y) 4417 new NISuppression(result_eq_arg1, arg2_eq_1, suppressee), 4418 4419 }); 4420 4421 // Create a suppression factory for functionBinary 4422 4423} 4424 4425/** 4426 * Represents the invariant {@code y = Power(z, x)} over three double 4427 * scalars. 4428 */ 4429public static class PowerDouble_yzx extends FunctionBinaryFloat { 4430 // We are Serializable, so we specify a version to allow changes to 4431 // method signatures without breaking serialization. If you add or 4432 // remove fields, you should change this number to the current date. 4433 static final long serialVersionUID = 20031030L; 4434 4435 private static @Prototype PowerDouble_yzx proto = new @Prototype PowerDouble_yzx (); 4436 4437 /** Returns the prototype invariant for PowerDouble_yzx */ 4438 public static @Prototype PowerDouble_yzx get_proto() { 4439 return proto; 4440 } 4441 4442 /** instantiate an invariant on the specified slice */ 4443 @Override 4444 protected PowerDouble_yzx instantiate_dyn(@Prototype PowerDouble_yzx this, PptSlice slice) { 4445 return new PowerDouble_yzx (slice); 4446 } 4447 4448 private PowerDouble_yzx (PptSlice slice) { 4449 super(slice); 4450 } 4451 4452 public @Prototype PowerDouble_yzx () { 4453 super(); 4454 } 4455 4456 private static String[] method_name = new String[] {"java.lang.Math.pow(", ", ", ")"}; 4457 4458 @Override 4459 public String[] get_method_name(@GuardSatisfied PowerDouble_yzx this) { 4460 return method_name; 4461 } 4462 4463 private static int function_id = -1; 4464 4465 @Override 4466 public int get_function_id() { 4467 return function_id; 4468 } 4469 4470 @Override 4471 public void set_function_id(int function_id) { 4472 assert PowerDouble_yzx.function_id == -1; 4473 PowerDouble_yzx.function_id = function_id; 4474 } 4475 4476 private static int var_order = 5; 4477 4478 @Override 4479 public int get_var_order(@GuardSatisfied PowerDouble_yzx this) { 4480 return var_order; 4481 } 4482 4483 @Pure 4484 @Override 4485 public boolean is_symmetric() { 4486 4487 return false; 4488 } 4489 4490 @Override 4491 4492 public double func(double z, double x) { 4493 4494 return Math.pow(z, x); 4495 } 4496 4497 @Override 4498 public InvariantStatus check_modified(double x, double y, 4499 double z, int count) { 4500 return check_ordered(y, z, x, count); 4501 } 4502 4503 @Override 4504 public InvariantStatus add_modified(double x, double y, 4505 double z, int count) { 4506 if (Debug.logDetail()) { 4507 log("result=%s, arg1=%s, arg2=%s", y, z, x); 4508 } 4509 return add_ordered(y, z, x, count); 4510 } 4511 4512 @Pure 4513 @Override 4514 public boolean isPower() { 4515 return true; 4516 } 4517 4518 @Pure 4519 @Override 4520 public boolean isExact() { 4521 return true; 4522 } 4523 4524 /** Returns a list of non-instantiating suppressions for this invariant. */ 4525 @Pure 4526 @Override 4527 public @Nullable NISuppressionSet get_ni_suppressions() { 4528 if (NIS.dkconfig_enabled && dkconfig_enabled) { 4529 return suppressions; 4530 } else { 4531 return null; 4532 } 4533 } 4534 4535 /** definition of this invariant (the suppressee) */ 4536 private static NISuppressee suppressee = new NISuppressee(PowerDouble_yzx.class, 3); 4537 4538 // suppressor definitions (used below) 4539 private static NISuppressor result_eq_arg1 = 4540 new NISuppressor(1, 2, FloatEqual.class); 4541 private static NISuppressor result_eq_arg2 = 4542 new NISuppressor(1, 0, FloatEqual.class); 4543 private static NISuppressor arg1_eq_arg2 = 4544 new NISuppressor(2, 0, FloatEqual.class); 4545 4546 private static NISuppressor result_lt_arg1 = 4547 new NISuppressor(1, 2, FloatLessThan.class); 4548 private static NISuppressor result_lt_arg2 = 4549 new NISuppressor(1, 0, FloatLessThan.class); 4550 private static NISuppressor arg1_lt_arg2 = 4551 new NISuppressor(2, 0, FloatLessThan.class); 4552 private static NISuppressor arg2_lt_arg1 = 4553 new NISuppressor(0, 2, FloatLessThan.class); 4554 4555 private static NISuppressor result_le_arg1 = 4556 new NISuppressor(1, 2, FloatLessEqual.class); 4557 private static NISuppressor result_le_arg2 = 4558 new NISuppressor(1, 0, FloatLessEqual.class); 4559 private static NISuppressor arg1_le_arg2 = 4560 new NISuppressor(2, 0, FloatLessEqual.class); 4561 private static NISuppressor arg2_le_arg1 = 4562 new NISuppressor(0, 2, FloatLessEqual.class); 4563 4564 private static NISuppressor result_track0_arg1 = 4565 new NISuppressor(1, 2, NumericInt.ZeroTrack.class); 4566 private static NISuppressor result_track0_arg2 = 4567 new NISuppressor(1, 0, NumericInt.ZeroTrack.class); 4568 private static NISuppressor arg1_track0_arg2 = 4569 new NISuppressor(2, 0, NumericInt.ZeroTrack.class); 4570 private static NISuppressor arg1_track0_result = 4571 new NISuppressor(2, 1, NumericInt.ZeroTrack.class); 4572 private static NISuppressor arg2_track0_result = 4573 new NISuppressor(0, 1, NumericInt.ZeroTrack.class); 4574 private static NISuppressor arg2_track0_arg1 = 4575 new NISuppressor(0, 2, NumericInt.ZeroTrack.class); 4576 4577 private static NISuppressor result_eq_1 = 4578 new NISuppressor(1, RangeFloat.EqualOne.class); 4579 private static NISuppressor arg1_eq_1 = 4580 new NISuppressor(2, RangeFloat.EqualOne.class); 4581 private static NISuppressor arg2_eq_1 = 4582 new NISuppressor(0, RangeFloat.EqualOne.class); 4583 4584 private static NISuppressor result_eq_0 = 4585 new NISuppressor(1, RangeFloat.EqualZero.class); 4586 private static NISuppressor arg1_eq_0 = 4587 new NISuppressor(2, RangeFloat.EqualZero.class); 4588 private static NISuppressor arg2_eq_0 = 4589 new NISuppressor(0, RangeFloat.EqualZero.class); 4590 4591 private static NISuppressor result_ne_0 = 4592 new NISuppressor(1, NonZeroFloat.class); 4593 private static NISuppressor arg1_ne_0 = 4594 new NISuppressor(2, NonZeroFloat.class); 4595 private static NISuppressor arg2_ne_0 = 4596 new NISuppressor(0, NonZeroFloat.class); 4597 4598 private static NISuppressor result_ge_0 = 4599 new NISuppressor(1, RangeFloat.GreaterEqualZero.class); 4600 private static NISuppressor arg1_ge_0 = 4601 new NISuppressor(2, RangeFloat.GreaterEqualZero.class); 4602 private static NISuppressor arg2_ge_0 = 4603 new NISuppressor(0, RangeFloat.GreaterEqualZero.class); 4604 4605 private static NISuppressor result_ge_64 = 4606 new NISuppressor(1, RangeInt.GreaterEqual64.class); 4607 private static NISuppressor arg1_ge_64 = 4608 new NISuppressor(2, RangeInt.GreaterEqual64.class); 4609 private static NISuppressor arg2_ge_64 = 4610 new NISuppressor(0, RangeInt.GreaterEqual64.class); 4611 4612 // Note that any suppression that doesn't limit x to valid exponents 4613 // (>= 0), must check for valid exponents as well (so that the invariant 4614 // is correctly destroyed on invalid exponents) 4615 // 4616 // Note also that pow(0,0) == 1 and pow(0,x), where (x > 0), == 0 4617 // Another interesting artificat of pow is that for any even base, any 4618 // exponent >= 64 will yield a result of 0. For example, pow(10,256) == 0 4619 // (at least for integers) 4620 4621 private static NISuppressionSet suppressions = 4622 new NISuppressionSet( 4623 new NISuppression[] { 4624 4625 // (r == 1) && (x == 0) ==> r = pow (z, x) 4626 new NISuppression(result_eq_1, arg2_eq_0, suppressee), 4627 4628 // (r == 1) && (z == 1) && (x >= 0) ==> r = pow (z, x) 4629 new NISuppression(result_eq_1, arg1_eq_1, arg2_ge_0, suppressee), 4630 4631 // (r == 0) && (z == 0) && (x > 0) 4632 new NISuppression(result_eq_0, arg1_eq_0, arg2_ne_0, arg2_ge_0, 4633 suppressee), 4634 4635 // (r == z) && (x == 1) ==> r = pow (z, x) 4636 new NISuppression(result_eq_arg1, arg2_eq_1, suppressee), 4637 4638 }); 4639 4640 // Create a suppression factory for functionBinary 4641 4642} 4643 4644/** 4645 * Represents the invariant {@code z = Power(y, x)} over three double 4646 * scalars. 4647 */ 4648public static class PowerDouble_zyx extends FunctionBinaryFloat { 4649 // We are Serializable, so we specify a version to allow changes to 4650 // method signatures without breaking serialization. If you add or 4651 // remove fields, you should change this number to the current date. 4652 static final long serialVersionUID = 20031030L; 4653 4654 private static @Prototype PowerDouble_zyx proto = new @Prototype PowerDouble_zyx (); 4655 4656 /** Returns the prototype invariant for PowerDouble_zyx */ 4657 public static @Prototype PowerDouble_zyx get_proto() { 4658 return proto; 4659 } 4660 4661 /** instantiate an invariant on the specified slice */ 4662 @Override 4663 protected PowerDouble_zyx instantiate_dyn(@Prototype PowerDouble_zyx this, PptSlice slice) { 4664 return new PowerDouble_zyx (slice); 4665 } 4666 4667 private PowerDouble_zyx (PptSlice slice) { 4668 super(slice); 4669 } 4670 4671 public @Prototype PowerDouble_zyx () { 4672 super(); 4673 } 4674 4675 private static String[] method_name = new String[] {"java.lang.Math.pow(", ", ", ")"}; 4676 4677 @Override 4678 public String[] get_method_name(@GuardSatisfied PowerDouble_zyx this) { 4679 return method_name; 4680 } 4681 4682 private static int function_id = -1; 4683 4684 @Override 4685 public int get_function_id() { 4686 return function_id; 4687 } 4688 4689 @Override 4690 public void set_function_id(int function_id) { 4691 assert PowerDouble_zyx.function_id == -1; 4692 PowerDouble_zyx.function_id = function_id; 4693 } 4694 4695 private static int var_order = 6; 4696 4697 @Override 4698 public int get_var_order(@GuardSatisfied PowerDouble_zyx this) { 4699 return var_order; 4700 } 4701 4702 @Pure 4703 @Override 4704 public boolean is_symmetric() { 4705 4706 return false; 4707 } 4708 4709 @Override 4710 4711 public double func(double y, double x) { 4712 4713 return Math.pow(y, x); 4714 } 4715 4716 @Override 4717 public InvariantStatus check_modified(double x, double y, 4718 double z, int count) { 4719 return check_ordered(z, y, x, count); 4720 } 4721 4722 @Override 4723 public InvariantStatus add_modified(double x, double y, 4724 double z, int count) { 4725 if (Debug.logDetail()) { 4726 log("result=%s, arg1=%s, arg2=%s", z, y, x); 4727 } 4728 return add_ordered(z, y, x, count); 4729 } 4730 4731 @Pure 4732 @Override 4733 public boolean isPower() { 4734 return true; 4735 } 4736 4737 @Pure 4738 @Override 4739 public boolean isExact() { 4740 return true; 4741 } 4742 4743 /** Returns a list of non-instantiating suppressions for this invariant. */ 4744 @Pure 4745 @Override 4746 public @Nullable NISuppressionSet get_ni_suppressions() { 4747 if (NIS.dkconfig_enabled && dkconfig_enabled) { 4748 return suppressions; 4749 } else { 4750 return null; 4751 } 4752 } 4753 4754 /** definition of this invariant (the suppressee) */ 4755 private static NISuppressee suppressee = new NISuppressee(PowerDouble_zyx.class, 3); 4756 4757 // suppressor definitions (used below) 4758 private static NISuppressor result_eq_arg1 = 4759 new NISuppressor(2, 1, FloatEqual.class); 4760 private static NISuppressor result_eq_arg2 = 4761 new NISuppressor(2, 0, FloatEqual.class); 4762 private static NISuppressor arg1_eq_arg2 = 4763 new NISuppressor(1, 0, FloatEqual.class); 4764 4765 private static NISuppressor result_lt_arg1 = 4766 new NISuppressor(2, 1, FloatLessThan.class); 4767 private static NISuppressor result_lt_arg2 = 4768 new NISuppressor(2, 0, FloatLessThan.class); 4769 private static NISuppressor arg1_lt_arg2 = 4770 new NISuppressor(1, 0, FloatLessThan.class); 4771 private static NISuppressor arg2_lt_arg1 = 4772 new NISuppressor(0, 1, FloatLessThan.class); 4773 4774 private static NISuppressor result_le_arg1 = 4775 new NISuppressor(2, 1, FloatLessEqual.class); 4776 private static NISuppressor result_le_arg2 = 4777 new NISuppressor(2, 0, FloatLessEqual.class); 4778 private static NISuppressor arg1_le_arg2 = 4779 new NISuppressor(1, 0, FloatLessEqual.class); 4780 private static NISuppressor arg2_le_arg1 = 4781 new NISuppressor(0, 1, FloatLessEqual.class); 4782 4783 private static NISuppressor result_track0_arg1 = 4784 new NISuppressor(2, 1, NumericInt.ZeroTrack.class); 4785 private static NISuppressor result_track0_arg2 = 4786 new NISuppressor(2, 0, NumericInt.ZeroTrack.class); 4787 private static NISuppressor arg1_track0_arg2 = 4788 new NISuppressor(1, 0, NumericInt.ZeroTrack.class); 4789 private static NISuppressor arg1_track0_result = 4790 new NISuppressor(1, 2, NumericInt.ZeroTrack.class); 4791 private static NISuppressor arg2_track0_result = 4792 new NISuppressor(0, 2, NumericInt.ZeroTrack.class); 4793 private static NISuppressor arg2_track0_arg1 = 4794 new NISuppressor(0, 1, NumericInt.ZeroTrack.class); 4795 4796 private static NISuppressor result_eq_1 = 4797 new NISuppressor(2, RangeFloat.EqualOne.class); 4798 private static NISuppressor arg1_eq_1 = 4799 new NISuppressor(1, RangeFloat.EqualOne.class); 4800 private static NISuppressor arg2_eq_1 = 4801 new NISuppressor(0, RangeFloat.EqualOne.class); 4802 4803 private static NISuppressor result_eq_0 = 4804 new NISuppressor(2, RangeFloat.EqualZero.class); 4805 private static NISuppressor arg1_eq_0 = 4806 new NISuppressor(1, RangeFloat.EqualZero.class); 4807 private static NISuppressor arg2_eq_0 = 4808 new NISuppressor(0, RangeFloat.EqualZero.class); 4809 4810 private static NISuppressor result_ne_0 = 4811 new NISuppressor(2, NonZeroFloat.class); 4812 private static NISuppressor arg1_ne_0 = 4813 new NISuppressor(1, NonZeroFloat.class); 4814 private static NISuppressor arg2_ne_0 = 4815 new NISuppressor(0, NonZeroFloat.class); 4816 4817 private static NISuppressor result_ge_0 = 4818 new NISuppressor(2, RangeFloat.GreaterEqualZero.class); 4819 private static NISuppressor arg1_ge_0 = 4820 new NISuppressor(1, RangeFloat.GreaterEqualZero.class); 4821 private static NISuppressor arg2_ge_0 = 4822 new NISuppressor(0, RangeFloat.GreaterEqualZero.class); 4823 4824 private static NISuppressor result_ge_64 = 4825 new NISuppressor(2, RangeInt.GreaterEqual64.class); 4826 private static NISuppressor arg1_ge_64 = 4827 new NISuppressor(1, RangeInt.GreaterEqual64.class); 4828 private static NISuppressor arg2_ge_64 = 4829 new NISuppressor(0, RangeInt.GreaterEqual64.class); 4830 4831 // Note that any suppression that doesn't limit x to valid exponents 4832 // (>= 0), must check for valid exponents as well (so that the invariant 4833 // is correctly destroyed on invalid exponents) 4834 // 4835 // Note also that pow(0,0) == 1 and pow(0,x), where (x > 0), == 0 4836 // Another interesting artificat of pow is that for any even base, any 4837 // exponent >= 64 will yield a result of 0. For example, pow(10,256) == 0 4838 // (at least for integers) 4839 4840 private static NISuppressionSet suppressions = 4841 new NISuppressionSet( 4842 new NISuppression[] { 4843 4844 // (r == 1) && (x == 0) ==> r = pow (y, x) 4845 new NISuppression(result_eq_1, arg2_eq_0, suppressee), 4846 4847 // (r == 1) && (y == 1) && (x >= 0) ==> r = pow (y, x) 4848 new NISuppression(result_eq_1, arg1_eq_1, arg2_ge_0, suppressee), 4849 4850 // (r == 0) && (y == 0) && (x > 0) 4851 new NISuppression(result_eq_0, arg1_eq_0, arg2_ne_0, arg2_ge_0, 4852 suppressee), 4853 4854 // (r == y) && (x == 1) ==> r = pow (y, x) 4855 new NISuppression(result_eq_arg1, arg2_eq_1, suppressee), 4856 4857 }); 4858 4859 // Create a suppression factory for functionBinary 4860 4861} 4862 4863}