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