001// ***** This file is automatically generated from LinearBinaryCore.java.jpp 002 003package daikon.inv.binary.twoScalar; 004 005import org.checkerframework.dataflow.qual.Pure; 006import org.checkerframework.checker.lock.qual.GuardSatisfied; 007import org.checkerframework.dataflow.qual.SideEffectFree; 008import org.checkerframework.checker.nullness.qual.Nullable; 009import daikon.*; 010import daikon.inv.*; 011import java.io.Serializable; 012import java.util.*; 013import java.util.logging.Level; 014import java.util.logging.Logger; 015import org.plumelib.util.MathPlume; 016 017public final class LinearBinaryCoreFloat implements Serializable, Cloneable { 018 // We are Serializable, so we specify a version to allow changes to 019 // method signatures without breaking serialization. If you add or 020 // remove fields, you should change this number to the current date. 021 static final long serialVersionUID = 20030822L; 022 023 /** Debug tracer. */ 024 public static final Logger debug = 025 Logger.getLogger("daikon.inv.binary.twoScalar.LinearBinaryCoreFloat"); 026 027 /** This invariant represents ax + by + c = 0; the first argument is x, second is y. */ 028 public double a = 0, b = 0, c = 0; 029 030 public double min_x, min_y, max_x, max_y; 031 public double min_a, max_a, min_b, max_b, min_c, max_c; 032 033 public Invariant wrapper; 034 035 // The number of distinct values (not samples) observed. 036 public int values_seen = 0; 037 038 // We delay computation of a, b and c until we have seen several pairs so 039 // that we can compute a, b and c based on a far-separated pair. We reduce 040 // the likelihood of roundoff error by getting 4 points, then choosing 041 // the two that are furthest apart in order to compute a, b and c. 042 static final int MINPAIRS = 4; 043 044 public double[] x_cache = new double[MINPAIRS]; 045 public double[] y_cache = new double[MINPAIRS]; 046 047 @SuppressWarnings("fields.uninitialized") // delayed initialization 048 public LinearBinaryCoreFloat(Invariant wrapper) { 049 this.wrapper = wrapper; 050 } 051 052 @SideEffectFree 053 @Override 054 public LinearBinaryCoreFloat clone(@GuardSatisfied LinearBinaryCoreFloat this) { 055 try { 056 LinearBinaryCoreFloat result = (LinearBinaryCoreFloat) super.clone(); 057 if (x_cache != null) { 058 result.x_cache = x_cache.clone(); 059 } 060 if (y_cache != null) { 061 result.y_cache = y_cache.clone(); 062 } 063 return result; 064 } catch (CloneNotSupportedException e) { 065 throw new Error(); // can't happen 066 } 067 } 068 069// There is no more need for swap because the equation is in standard form. 070 public void swap() { 071 // was a swap 072 if (values_seen < MINPAIRS) { 073 } else { 074 if (a == 0) { 075 // can't swap horizontal line into vertical, but if a was 0, 076 // then we might as well falsify ourselves because this is just 077 // a constant 078 values_seen = Integer.MAX_VALUE; 079 a = 0; 080 b = 0; 081 c = 0; 082 } else { 083 // since the equation is already in standard form, just guarantee that the x coefficient is positive 084 085 if (b < 0) { 086 a = -b; 087 b = -a; 088 c = -c; 089 } 090 } 091 } 092 093 // swap the value caches 094 double[] tmp = x_cache; 095 x_cache = y_cache; 096 y_cache = tmp; 097 098 // swap min_x/min_y and max_x/max_y 099 double tmp_val = max_x; 100 max_x = max_y; 101 max_y = tmp_val; 102 tmp_val = min_x; 103 min_x = min_y; 104 min_y = tmp_val; 105 } 106 107 /** 108 * Returns whether or not the invariant is currently active. We become active after MINPAIRS 109 * values have been seen and a line calculated. Before that, a and b are uninitialized. 110 */ 111 @Pure 112 public boolean isActive() { 113 return values_seen >= MINPAIRS; 114 } 115 116 /** 117 * LinearBinary can't be flowed because it keeps samples to build the line. These sample can't be 118 * flowed from ppt to ppt (since they probably didn't occur at the lower ppt). 119 */ 120 @Pure 121 public boolean isFlowable() { 122 return false; 123 } 124 125 // Note that this method is relatively inconsistent with respect to 126 // differing ordering of the points. It will always give exactly the 127 // same answer with points that are delivered in the same order, but 128 // it can calculate different a/b and change whether or not it even 129 // finds a line with a different order. Current code always guarantees 130 // that the points arrive in the same order (I think). 131 public InvariantStatus add_modified(double x, double y, int count) { 132 if (values_seen < MINPAIRS) { 133 if (debug.isLoggable(Level.FINE)) { 134 debug.fine("min point: " + wrapper.ppt.name() + ": " + x + ", " + y); 135 } 136 // We delay computation of a and b until we have seen several pairs 137 // so that we can compute a and b based on a far-separated pair. If 138 // the points in a pair are nearby, then roundoff errors in the 139 // computation of the slope can be non-negligible. 140 141 for (int i = 0; i < values_seen; i++) { 142 if ((x_cache[i] == x) && (y_cache[i] == y)) { 143 return InvariantStatus.NO_CHANGE; 144 } 145 } 146 x_cache[values_seen] = x; 147 y_cache[values_seen] = y; 148 values_seen++; 149 if (values_seen == MINPAIRS) { 150 // Find the most separated pair. 151 int[] sep_indices = maxsep_indices(); 152 int max_i = sep_indices[0]; 153 int max_j = sep_indices[1]; 154 155 // Set a, b and c based on that pair 156 if (max_i == -1) { 157 values_seen--; 158 wrapper.log("falsified, max_i = -1"); 159 return InvariantStatus.FALSIFIED; 160 } 161 // remember the min and max pairs 162 if (x_cache[max_i] < x_cache[max_j]) { 163 // swap max_i and max_j 164 int tmp = max_i; 165 max_i = max_j; 166 max_j = tmp; 167 } 168 min_x = x_cache[max_i]; 169 min_y = y_cache[max_i]; 170 max_x = x_cache[max_j]; 171 max_y = y_cache[max_j]; 172 173 // calculate a, b and c for this pair and remember them as min/max a,b,c 174 if (set_bi_linear(min_x, max_x, min_y, max_y) == InvariantStatus.FALSIFIED) { 175 values_seen--; 176 wrapper.log("falsified, no set_bi_linear"); 177 return InvariantStatus.FALSIFIED; 178 } 179 min_a = a; 180 max_a = a; 181 min_b = b; 182 max_b = b; 183 min_c = c; 184 max_c = c; 185 if (debug.isLoggable(Level.FINE)) { 186 debug.fine( 187 wrapper.ppt.name() + ": Initial a (" + a + ") and b (" + b + ") and c (" + c + ")"); 188 } 189 190 // Check all values against a, b, and c. 191 if (Global.fuzzy.eq(a, 0)) { 192 wrapper.log("falsified, a == 0"); 193 values_seen--; 194 return InvariantStatus.FALSIFIED; 195 } 196 197 for (int i = 0; i < MINPAIRS; i++) { 198 // if the point is close enough in either x or y it is close enough 199 // The double check is used because lines with different slopes may 200 // indicate an unreasonably high x or y diff when the actual point 201 // is very close. It would probably be better to calculate the 202 // actual distance from the line, but it would be unclear what to 203 // compare this to (average or X and Y?). This seems like a 204 // reasonable compromise. 205 if (!Global.fuzzy.eq(-b * y_cache[i], a * x_cache[i] + c) 206 && !Global.fuzzy.eq(x_cache[i], (-b * y_cache[i] - c) / a)) { 207 if (debug.isLoggable(Level.FINE)) { 208 debug.fine( 209 "Suppressing LinearBinaryCoreFloat (" 210 + wrapper.format() 211 + ") at index " 212 + i 213 + ": " 214 + y_cache[i] 215 + " != " 216 + a 217 + "*" 218 + x_cache[i] 219 + "+" 220 + b); 221 debug.fine(" "); 222 } 223 values_seen--; 224 wrapper.log("falsified, point in cache doesn't match"); 225 return InvariantStatus.FALSIFIED; 226 } 227 } 228 } 229 } else { 230 // Check the new value against a and b. (See previous explanation for double 231 // EQUAL check.) 232 if (!Global.fuzzy.eq(y, (-c - a * x)/b) && !Global.fuzzy.eq(x, (-c - b * y)/ a)) { 233 // see if this new point is off one end or the other 234 if (x < min_x) { 235 min_x = x; 236 min_y = y; 237 } else if (x > max_x) { 238 max_x = x; 239 max_y = y; 240 } 241 242 double delta_x = max_x - min_x; 243 // should be fixed in the future to permit vertical lines 244 if (Global.fuzzy.eq(delta_x, 0)) { 245 return InvariantStatus.FALSIFIED; 246 } 247 248 // calculate a new a, b, c possibly using a new end point 249 250 double[] res = new double[3]; 251 boolean ok = find_bi_linear(min_x, max_x, min_y, max_y, res); 252 double new_a = 0; 253 double new_b = 0; 254 double new_c = 0; 255 if (ok) { 256 new_a = res[0]; 257 new_b = res[1]; 258 new_c = res[2]; 259 } 260 261 // if the a or b is a new min/max remember it. 262 if (new_a < min_a) min_a = new_a; 263 if (new_a > max_a) max_a = new_a; 264 if (new_b < min_b) min_b = new_b; 265 if (new_b > max_b) max_b = new_b; 266 if (new_c < min_c) min_c = new_c; 267 if (new_c > max_c) max_c = new_c; 268 269 // pick a new a, b, c as the average of their endpoints 270 new_a = (min_a + max_a) / 2; 271 new_b = (min_b + max_b) / 2; 272 new_c = (min_c + max_c) / 2; 273 if (debug.isLoggable(Level.FINE)) { 274 debug.fine(wrapper.ppt.name() + ": Trying new a (" + new_a 275 + ") and b (" + new_b + ")"); 276 } 277 278 // if the new a, b, c are 'equal' to min/max a, b, c and 279 // this point fits, then this new equation is good enough both 280 // for existing points and the new point. 281 282 if (Global.fuzzy.eq(new_a, min_a) 283 && Global.fuzzy.eq(new_a, max_a) 284 && Global.fuzzy.eq(new_b, min_b) 285 && Global.fuzzy.eq(new_b, max_b) 286 && Global.fuzzy.eq(new_c, min_c) 287 && Global.fuzzy.eq(new_c, max_c) 288 && Global.fuzzy.eq(-new_b * y, new_a * x + new_c)) { 289 a = new_a; 290 b = new_b; 291 c = new_c; 292 if (debug.isLoggable(Level.FINE)) { 293 debug.fine( 294 wrapper.ppt.name() + ": New a (" + a + ") and b (" + b + ") and c (" + c + ")"); 295 } 296 } else { 297 if (debug.isLoggable(Level.FINE)) { 298 debug.fine("Suppressing LinearBinaryCoreFloat (" 299 + wrapper.format() + ") at new value: " 300 + a + " * x + " + b + " * y + " + c + " != 0"); 301// + y + " != " + a + "*" + x + "+" + b); 302 } 303 return InvariantStatus.FALSIFIED; 304 } 305 //??? wrapper.destroyAndFlow(); 306 //??? return; 307 } 308 } 309 return InvariantStatus.NO_CHANGE; 310 } 311 312 /** 313 * Returns a 2-element int array of the indices of the most separated pair of points between the 314 * points represented by x_array and y_array. Requires that x_array and y_array are the same 315 * length. 316 */ 317 static int[] maxsep_point(double[] x_array, double[] y_array) { 318 // Find the most separated pair. 319 // Do I really need to check in two dimensions, or would one be enough? 320 321 assert x_array.length == y_array.length; 322 323 // indices of the most-separated pair of points 324 int max_i = -1; 325 int max_j = -1; 326 // (square of the) distance between the most separated pair 327 double max_separation = 0; 328 for (int i = 0; i < x_array.length - 1; i++) { 329 for (int j = i + 1; j < x_array.length; j++) { 330 // not long, lest we get wraparound 331 double xsep = x_array[i] - x_array[j]; 332 double ysep = y_array[i] - y_array[j]; 333 double separation = xsep * xsep + ysep * ysep; 334 335 // Roundoff error might result in 0. 336 // assert separation > 0; 337 338 if (separation > max_separation) { 339 max_separation = separation; 340 max_i = i; 341 max_j = j; 342 } 343 } 344 } 345 return new int[] {max_i, max_j}; 346 } 347 /** 348 * Returns a 2-element int array of the indices of the most separated pair of points between the 349 * points within this. 350 */ 351 int[] maxsep_indices() { 352 return maxsep_point(x_cache, y_cache); 353 } 354 355 // /** 356 // * Given ((x0,y0),(x1,y1)), finds a and b such that y = ax + b. 357 // * Places a and b (if they exist) into result at indexes 0 and 1 358 // * respectively. 359 // * @return true if such an a and b exist. 360 // */ 361 /** 362 * Given ((x0,y0),(x1,y1)), finds a,b and c such that ax + by + c = 0. Places a, b and c (if they 363 * exist) into result at indexes 0, 1 and 2 respectively. 364 * 365 * @return true if such an a and b exist 366 */ 367 private static boolean find_bi_linear( 368 double x0, double x1, double y0, double y1, double[] result) { 369 if (x1 - x0 == 0) { // not "x0 == x1", due to roundoff 370 // x being constant would have been discovered elsewhere (and this 371 // invariant would not have been instantiated). 372 return false; 373 } 374 if (y1 - y0 == 0) { // not "y0 == y1", due to roundoff 375 // y being constant would have been discovered elsewhere (and this 376 // invariant would not have been instantiated). 377 return false; 378 } 379 380 double i_var = y1 - y0; 381 double j_var = x0 - x1; 382 double Stand_const = y0 * x1 - x0 * y1; 383 384 // Put the coefficients in lowest terms by dividing by the gcd. 385 // If the gcd is 1, no harm done -- divide by 1. 386 // Type is double to ensure floating-point division. 387 double myGCD = MathPlume.gcd(MathPlume.gcd(i_var, j_var), Stand_const); 388 double standard_i_var = i_var / myGCD; 389 double standard_j_var = j_var / myGCD; 390 double standard_Stand_const = Stand_const / myGCD; 391 392 // Ensure postive x coefficient by negating if "x" term is negative. 393 if (i_var < 0) { 394 standard_i_var = -standard_i_var; 395 standard_j_var = -standard_j_var; 396 standard_Stand_const = -standard_Stand_const; 397 } 398 399 result[0] = standard_i_var; 400 result[1] = standard_j_var; 401 result[2] = standard_Stand_const; 402 403 return true; 404 } 405 406 /** Given ((x0,y0),(x1,y1)), set a, b and c such that ax + by + c = 0. */ 407 private InvariantStatus set_bi_linear(double x0, double x1, double y0, double y1) { 408 double[] AandBandC = new double[3]; 409 if (!find_bi_linear(x0, x1, y0, y1, AandBandC)) { 410 if (debug.isLoggable(Level.FINE)) { 411 debug.fine("Suppressing LinearBinaryCoreFloat due to equal x values: (" + x0 + "," + y0 + "), (" + x1 + "," + y1 + ")"); 412 } 413 return InvariantStatus.FALSIFIED; 414 } 415 a = AandBandC[0]; 416 b = AandBandC[1]; 417 c = AandBandC[2]; 418 wrapper.log("x0=%s, x1=%s, y0=%s, y1=%s", x0, x1, y0, y1); 419 wrapper.log("a=%s, b=%s, c=%s", a, b, c); 420 return InvariantStatus.NO_CHANGE; 421 } 422 423 public boolean enoughSamples(@GuardSatisfied LinearBinaryCoreFloat this) { 424 return values_seen >= MINPAIRS; 425 } 426 427 public double computeConfidence() { 428 return Invariant.conf_is_ge(values_seen, MINPAIRS); 429 } 430 431 public String repr(@GuardSatisfied LinearBinaryCoreFloat this) { 432 return "LinearBinaryCoreFloat" + wrapper.varNames() + ": a=" + a 433 + ",b=" + b 434 + ",c=" + c 435 + ",values_seen=" + values_seen; 436 } 437 438 // Format one term of an equation. 439 // Variable "first" indicates whether this is the leading term 440 // Variable "varname" is the name of the variable; may be null 441 // for the constant term. 442 public static String formatTerm(double coeff, @Nullable String varname, boolean first) { 443 double ncoeff = coeff; 444 445 if (ncoeff == 0) { 446 return ""; 447 } 448 String sign; 449 if (ncoeff < 0) { 450 if (first) { 451 sign = "- "; 452 } else { 453 sign = " - "; 454 } 455 } else if (first) { 456 sign = ""; 457 } else { 458 sign = " + "; 459 } 460 461 //we want to ensure that the positive value is used because the sign has already been determined 462 String coeff_string = 463 (ncoeff == (int)ncoeff) ? "" + Math.abs((int)ncoeff) : "" + Math.abs(ncoeff); 464 if (varname == null) { 465 return sign + coeff_string; 466 } 467 if (ncoeff == 1 || ncoeff == -1) { 468 return sign + varname; 469 } else { 470 return sign + coeff_string + " * " + varname; 471 } 472 } 473 474 @SideEffectFree 475 public String format_using( 476 OutputFormat format, String vix, String viy, double u, double v, double w) { 477 478 // recall that a, b, c in the linear binary equation means ax + by + c = 0; 479 if (u == 0 && v == 0 && w == 0) { 480 return wrapper.format_too_few_samples(format, "0 * " + vix + "+ 0 * " + viy + " + 0 == 0"); 481 } 482 483 if (format.isJavaFamily()) { 484 485 return "daikon.Quant.fuzzy.eq(0, " 486 + formatTerm(u, vix, true) 487 + formatTerm(v, viy, false) 488 + formatTerm(w, null, false) 489 + ")"; 490 491 } 492 493 if ((format == OutputFormat.DAIKON) 494 || (format == OutputFormat.ESCJAVA) 495 || (format == OutputFormat.CSHARPCONTRACT)) { 496 String eq = " == "; 497 return formatTerm(u, vix, true) 498 + formatTerm(v, viy, false) 499 + formatTerm(w, null, false) 500 + eq 501 + "0"; 502 } 503 504 if (format == OutputFormat.SIMPLIFY) { 505 return format_simplify(vix, viy, u, v, w); 506 } 507 throw new Error("Unknown OutputFormat: " + format); 508 } 509 510 public static String format_simplify(String str_x, String str_y, double a, double b, double c) { 511 512 int ia = (int) a; 513 int ib = (int) b; 514 int ic = (int) c; 515 516 String str_a, str_b, str_c; 517 if (ia == a && ib == b && ic == c) { 518 // integer 519 str_a = Invariant.simplify_format_long(ia); 520 str_b = Invariant.simplify_format_long(ib); 521 str_c = Invariant.simplify_format_long(ic); 522 } else { 523 // floating point; probably not very useful 524 str_a = Invariant.simplify_format_double(a); 525 str_b = Invariant.simplify_format_double(b); 526 str_c = Invariant.simplify_format_double(c); 527 } 528 529 // ax + by + c = 0 530 531 String str_ax = (a == 1.0) ? str_x : "(* " + str_a + " " + str_x + ")"; 532 String str_by = (b == 1.0) ? str_y : "(* " + str_b + " " + str_y + ")"; 533 String str_axby = "(+ " + str_ax + " " + str_by + ")"; 534 String str_axpc = (c == 0.0) ? str_axby : "(+ " + str_axby + " " + str_c + ")"; 535 536 return "(EQ 0 " + str_axpc + ")"; 537 } 538 539 @SideEffectFree 540 public String format_using(OutputFormat format, String xname, String yname) { 541 String result = format_using(format, xname, yname, a, b, c); 542 if (result != null) { 543 return result; 544 } else { 545 return wrapper.format_unimplemented(format); 546 } 547 } 548 549 // Format as "x = cy+d" instead of as "y = ax+b". [now that we print in standard format, is 550 // there a point to this method? 551 public String format_reversed_using(OutputFormat format, String xname, String yname) { 552 assert a == 1 || a == -1; 553 return format_using(format, yname, xname, b, a, c); 554 } 555 556 /** 557 * In general, we can't merge formulas, but we can merge invariants with too few samples to have 558 * formed a line with invariants with enough samples. And those will appear to have different 559 * formulas. 560 */ 561 public boolean mergeFormulasOk() { 562 return true; 563 } 564 565 /** 566 * Merge the linear binary cores in cores to form a new core. Any core in the list that has seen 567 * enough points to define a line, must define the same line. Any cores that have not yet seen 568 * enough points, will have each of their points applied to that invariant. The merged core is 569 * returned. Null is returned if the cores don't describe the same line 570 * 571 * @param cores list of LinearBinary cores to merge. They should all be permuted to match the 572 * variable order in ppt. 573 */ 574 public @Nullable LinearBinaryCoreFloat merge(List<LinearBinaryCoreFloat> cores, Invariant wrapper) { 575 576 // Look for any active lines. All must define the same line 577 LinearBinaryCoreFloat result = null; 578 for (LinearBinaryCoreFloat c : cores) { 579 if (!c.isActive()) { 580 continue; 581 } 582 if (result == null) { 583 result = c.clone(); 584 } else { 585 if (!Global.fuzzy.eq(result.a, c.a) 586 || !Global.fuzzy.eq(result.b, c.b) 587 || !Global.fuzzy.eq(result.c, c.c)) { 588 return null; 589 } 590 } 591 } 592 593 // If no active lines were found, created an empty core 594 if (result == null) { 595 result = new LinearBinaryCoreFloat(wrapper); 596 } else { 597 result.wrapper = wrapper; 598 } 599 600 // Merge in any points from non-active cores 601 for (LinearBinaryCoreFloat c : cores) { 602 if (c.isActive()) { 603 continue; 604 } 605 for (int j = 0; j < c.values_seen; j++) { 606 if (result.add_modified(c.x_cache[j], c.y_cache[j], 1) == InvariantStatus.FALSIFIED) { 607 // if (wrapper.falsified) 608 return null; 609 } 610 } 611 } 612 613 return result; 614 } 615 616 @Pure 617 public boolean isSameFormula(LinearBinaryCoreFloat other) { 618 boolean thisMeaningless = values_seen < MINPAIRS; 619 boolean otherMeaningless = other.values_seen < MINPAIRS; 620 621 if (thisMeaningless && otherMeaningless) { 622 return true; 623 } else { 624 return (values_seen >= MINPAIRS) 625 && (other.values_seen >= MINPAIRS) 626 && (a == other.a) 627 && (b == other.b) 628 && (c == other.c); 629 } 630 } 631 632 @Pure 633 public boolean isExclusiveFormula(LinearBinaryCoreFloat other) { 634 if ((values_seen < MINPAIRS) || (other.values_seen < MINPAIRS)) { 635 return false; 636 } 637 638 return (-a / b == -other.a / other.b) && (-c / b != -other.c / other.b); 639 } 640}