001// ***** This file is automatically generated from OneOf.java.jpp 002 003package daikon.inv.unary.sequence; 004 005import daikon.*; 006import daikon.inv.*; 007import daikon.inv.unary.OneOf; 008 009import java.io.*; 010import java.util.logging.Logger; 011import java.util.logging.Level; 012import java.util.*; 013 014import org.checkerframework.checker.initialization.qual.Initialized; 015import org.checkerframework.checker.interning.qual.Interned; 016import org.checkerframework.checker.lock.qual.GuardSatisfied; 017import org.checkerframework.checker.nullness.qual.NonNull; 018import org.checkerframework.checker.nullness.qual.Nullable; 019import org.checkerframework.dataflow.qual.Pure; 020import org.checkerframework.dataflow.qual.SideEffectFree; 021import org.checkerframework.framework.qual.Unused; 022import daikon.SignaturesUtil; 023import org.plumelib.reflection.Signatures; 024import org.plumelib.util.ArraysPlume; 025import org.plumelib.util.Intern; 026import org.plumelib.util.StringsPlume; 027import org.plumelib.util.UtilPlume; 028import typequals.prototype.qual.NonPrototype; 029import typequals.prototype.qual.Prototype; 030 031// This subsumes an "exact" invariant that says the value is always exactly 032// a specific value. Do I want to make that a separate invariant 033// nonetheless? Probably not, as this will simplify implication and such. 034 035 /** 036 * Represents double[] variables that take on only a few distinct values. Prints as either 037 * {@code x == c} (when there is only one value) or as {@code x one of {c1, c2, c3}} 038 * (when there are multiple values). 039 040 */ 041 042@SuppressWarnings("UnnecessaryParentheses") // generated code, parentheses are sometimes needed 043public final class OneOfFloatSequence extends SingleFloatSequence implements OneOf { 044 static final long serialVersionUID = 20030822L; 045 046 /** Debugging logger. */ 047 public static final Logger debug = 048 Logger.getLogger(OneOfFloatSequence.class.getName()); 049 050 // Variables starting with dkconfig_ should only be set via the 051 // daikon.config.Configuration interface. 052 /** Boolean. True iff OneOf invariants should be considered. */ 053 public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault; 054 055 /** 056 * Positive integer. Specifies the maximum set size for this type of invariant (x is one of 057 * {@code size} items). 058 */ 059 060 public static int dkconfig_size = 3; 061 062 // Probably needs to keep its own list of the values, and number of each seen. 063 // (That depends on the slice; maybe not until the slice is cleared out. 064 // But so few values is cheap, so this is quite fine for now and long-term.) 065 066 @Unused(when=Prototype.class) 067 private double[] @Interned [] elts; 068 @Unused(when=Prototype.class) 069 private int num_elts; 070 071 @Prototype OneOfFloatSequence() { 072 super(); 073 } 074 075 OneOfFloatSequence(PptSlice slice) { 076 super(slice); 077 078 // Elements are interned, so can test with == (except that NaN != NaN) 079 // (in the general online case, it's not worth interning). 080 elts = new double[dkconfig_size] @Interned []; 081 082 num_elts = 0; 083 084 // var() is initialized by the super constructor 085 assert var().is_array() : 086 String.format("In %s constructor, var %s (type=%s, rep_type=%s) should be an array", 087 "OneOfSequenceFloat", var().name(), var().type, var().rep_type); 088 089 } 090 091 private static @Prototype OneOfFloatSequence proto = new @Prototype OneOfFloatSequence(); 092 093 /** Returns the prototype invariant for OneOfFloatSequence */ 094 public static @Prototype OneOfFloatSequence get_proto() { 095 return proto; 096 } 097 098 @Override 099 public boolean enabled() { 100 return dkconfig_enabled; 101 } 102 103 @Override 104 public OneOfFloatSequence instantiate_dyn(@Prototype OneOfFloatSequence this, PptSlice slice) { 105 return new OneOfFloatSequence(slice); 106 } 107 108 @Pure 109 public boolean is_boolean(@GuardSatisfied OneOfFloatSequence this) { 110 return var().file_rep_type.elementType() == ProglangType.BOOLEAN; 111 } 112 @Pure 113 public boolean is_hashcode(@GuardSatisfied OneOfFloatSequence this) { 114 return var().file_rep_type.elementType() == ProglangType.HASHCODE; 115 } 116 117 @SideEffectFree 118 @Override 119 public OneOfFloatSequence clone(@GuardSatisfied OneOfFloatSequence this) { 120 OneOfFloatSequence result = (OneOfFloatSequence) super.clone(); 121 result.elts = elts.clone(); 122 123 for (int i = 0; i < num_elts; i++) { 124 result.elts[i] = Intern.intern(elts[i].clone()); 125 } 126 127 result.num_elts = this.num_elts; 128 return result; 129 } 130 131 @Override 132 public int num_elts() { 133 return num_elts; 134 } 135 136 @Override 137 public Object elt() { 138 return elt(0); 139 } 140 141 public Object elt(int index) { 142 if (num_elts <= index) { 143 throw new Error("Represents " + num_elts + " elements, index " + index + " not valid"); 144 } 145 146 return elts[index]; 147 } 148 149 static Comparator<double[]> comparator = ArraysPlume.DoubleArrayComparatorLexical.it; 150 151 private void sort_rep(@GuardSatisfied OneOfFloatSequence this) { 152 Arrays.sort(elts, 0, num_elts , comparator); 153 } 154 155 public double @Interned [] min_elt() { 156 if (num_elts == 0) { 157 throw new Error("Represents no elements"); 158 } 159 sort_rep(); 160 return elts[0]; 161 } 162 163 public double @Interned [] max_elt() { 164 if (num_elts == 0) { 165 throw new Error("Represents no elements"); 166 } 167 sort_rep(); 168 return elts[num_elts - 1]; 169 } 170 171 // Assumes the other array is already sorted 172 public boolean compare_rep(int num_other_elts, double[] @Interned [] other_elts) { 173 if (num_elts != num_other_elts) { 174 return false; 175 } 176 sort_rep(); 177 for (int i = 0; i < num_elts; i++) { 178 if (!((elts[i]) == (other_elts[i]))) { // elements are interned 179 return false; 180 } 181 } 182 return true; 183 } 184 185 private String subarray_rep(@GuardSatisfied OneOfFloatSequence this) { 186 // Not so efficient an implementation, but simple; 187 // and how often will we need to print this anyway? 188 sort_rep(); 189 StringJoiner sj = new StringJoiner(", ", "{ ", " }"); 190 for (int i = 0; i < num_elts; i++) { 191 192 sj.add(Arrays.toString(elts[i])); 193 194 } 195 return sj.toString(); 196 } 197 198 @Override 199 public String repr(@GuardSatisfied OneOfFloatSequence this) { 200 return "OneOfSequenceFloat" + varNames() + ": falsified=" + falsified 201 + ", num_elts=" + num_elts 202 + ", elts=" + subarray_rep(); 203 } 204 205 @SideEffectFree 206 @Override 207 public String format_using(@GuardSatisfied OneOfFloatSequence this, OutputFormat format) { 208 sort_rep(); 209 210 if (format.isJavaFamily()) { 211 return format_java_family(format); 212 } 213 214 if (format == OutputFormat.DAIKON) { 215 return format_daikon(); 216 } else if (format == OutputFormat.SIMPLIFY) { 217 return format_simplify(); 218 } else if (format == OutputFormat.ESCJAVA) { 219 String result = format_esc(); 220 return result; 221 } else if (format == OutputFormat.CSHARPCONTRACT) { 222 return format_csharp_contract(); 223 } else { 224 return format_unimplemented(format); 225 } 226 } 227 228 public String format_daikon(@GuardSatisfied OneOfFloatSequence this) { 229 String varname = var().name(); 230 if (num_elts == 1) { 231 232 return varname + " == " + Arrays.toString(elts[0]); 233 } else { 234 return varname + " one of " + subarray_rep(); 235 } 236 } 237 238 public String format_esc(@GuardSatisfied OneOfFloatSequence this) { 239 sort_rep(); 240 241 String result; 242 243 String length = null; 244 String forall = null; 245 246 if (length == null) { 247 if (forall == null) { 248 return format_unimplemented(OutputFormat.ESCJAVA); // "needs to be implemented" 249 } else { 250 result = forall; 251 } 252 } else { 253 if (forall == null) { 254 result = length; 255 } else { 256 result = "(" + length + ") && (" + forall + ")"; 257 } 258 } 259 260 return result; 261 } 262 263public String format_csharp_contract(@GuardSatisfied OneOfFloatSequence this) { 264 265 @NonNull @Initialized String result; 266 267 result = "(\"oneOf.java.jpp: SEQUENCE unimplemented\" != null)"; // "interned" 268 269 return result; 270 } 271 272 public String format_java_family(@GuardSatisfied OneOfFloatSequence this, OutputFormat format) { 273 274 String result; 275 276 // Setting up the name of the unary variable 277 String varname = var().name_using(format); 278 279 result = ""; 280 for (int i = 0; i < num_elts; i++) { 281 if (i != 0) { 282 result += " || "; 283 } 284 285 String seq = "new double[] { "; 286 287 for (int j = 0 ; j < elts[i].length ; j++) { 288 if (j != 0) { seq += ", "; } 289 seq = seq + (Double.isNaN(elts[i][j]) ? "Double.NaN" : String.valueOf(elts[i][j])); 290 } 291 seq += " }"; 292 293 result += "daikon.Quant.pairwiseEqual(" + varname + ", " + seq + ")"; 294 } 295 296 return result; 297 } 298 299 public String format_simplify(@GuardSatisfied OneOfFloatSequence this) { 300 301 sort_rep(); 302 303 String result; 304 305 StringBuilder resultBuf = new StringBuilder(); 306 for (int i = 0; i < num_elts; i++) { 307 double @Interned [] seq = elts[i]; 308 String offset = null; 309 String contents = null; 310 String[] bounds_name; 311 String length = var().get_simplify_size_name(); 312 // if ((length == null) && var().name.isApplySizeSafe()) 313 // System.out.printf("var %s, type %s, is_array %b%n", var().name(), 314 // var().type, var().type.isArray()); 315 if (length != null) { 316 length = "(EQ " + length + " "+ simplify_format_long(seq.length) + ")"; 317 } else if ((bounds_name = var().get_simplify_slice_bounds()) != null) { 318 String size = "(+ 1 (- " + bounds_name[1] +" " + bounds_name[0] + "))"; 319 length = "(EQ " + size + " " + simplify_format_long(seq.length) + ")"; 320 offset = bounds_name[0]; 321 } 322 323 { 324 StringBuilder contentsBuf = new StringBuilder(); 325 for (int j = 0; j < seq.length; j++) { 326 if (j + 3 < seq.length 327 && (((seq[j]) == ( seq[j + 1])) || (Double.isNaN(seq[j]) &&Double.isNaN( seq[j + 1]))) 328 && (((seq[j]) == ( seq[j + 2])) || (Double.isNaN(seq[j]) &&Double.isNaN( seq[j + 2]))) 329 && (((seq[j]) == ( seq[j + 3])) || (Double.isNaN(seq[j]) &&Double.isNaN( seq[j + 3])))) { 330 // Compress a sequence of adjacent values 331 int k = j + 4; 332 for (; k < seq.length; k++) { 333 if (!(((seq[j]) == ( seq[k])) || (Double.isNaN(seq[j]) &&Double.isNaN( seq[k])))) { 334 break; 335 } 336 } 337 k--; 338 String index_name = VarInfo.get_simplify_free_index(var()); 339 String cond_left, cond_right; 340 if (offset == null) { 341 cond_left = "(<= " + j + " " + index_name + ")"; 342 cond_right = "(<= " + index_name + " " + k + ")"; 343 } else { 344 cond_left = "(<= (+ " + offset + " " + j + ") " 345 + index_name + ")"; 346 cond_right = "(>= (+ " + offset + " " + k + ") " 347 + index_name + ")"; 348 } 349 String cond = "(AND " + cond_left + " " + cond_right + ")"; 350 String nth = var().get_simplify_selectNth(index_name, true, 0); 351 String eq = "(EQ " + nth + " " + simplify_format_double(seq[j]) + ")"; 352 String implies = "(IMPLIES " + cond + " " + eq + ")"; 353 String forall = "(FORALL (" + index_name + ") " + implies + ")"; 354 contentsBuf.append(" " + forall); 355 j = k; 356 } else { 357 // Output a single value 358 String nth = var().get_simplify_selectNth_lower(j); 359 if (nth == null) { 360 String classname = this.getClass().toString().substring(6); 361 result = "warning: method " + classname 362 + ".format_simplify() needs to fix selectNth(): " + format(); 363 return result; 364 } 365 String value = simplify_format_double(seq[j]); 366 contentsBuf.append(" (EQ " + nth + " " + value + ")"); 367 // if (nth.contains ("--orig__a")) 368 // System.out.printf("regular orig__a%n"); 369 370 } 371 } 372 if (seq.length > 1) { 373 contents = "(AND " + contentsBuf.toString() + ")"; 374 } else if (seq.length == 1) { 375 contents = contentsBuf.toString().substring(1); 376 } else if (seq.length == 0) { 377 contents = null; // back from "" 378 } 379 } 380 if (length == null && contents == null) { 381 resultBuf.append(" "); 382 } else if (length == null && contents != null) { 383 resultBuf.append(" " + contents); 384 } else if (length != null && contents == null) { 385 resultBuf.append(" " + length); 386 } else { 387 assert length != null && contents != null; 388 resultBuf.append(" (AND " + length + " " + contents + ")"); 389 } 390 391 } 392 if (num_elts > 1) { 393 result = "(OR" + resultBuf.toString() + ")"; 394 } else if (num_elts == 1) { 395 // chop leading space 396 result = resultBuf.toString().substring(1); 397 } else if (num_elts == 0) { 398 return format_too_few_samples(OutputFormat.SIMPLIFY, null); 399 } else { 400 throw new Error("this can't happen"); 401 // result = null; 402 } 403 if (result.trim().equals("")) { 404 result = "format_simplify() failed on a weird OneOf"; 405 } 406 407 if (result.indexOf("format_simplify") == -1) { 408 daikon.simplify.SimpUtil.assert_well_formed(result); 409 } 410 return result; 411 } 412 413 @Override 414 public InvariantStatus add_modified(double @Interned [] a, int count) { 415 return runValue(a, count, true); 416 } 417 418 @Override 419 public InvariantStatus check_modified(double @Interned [] a, int count) { 420 return runValue(a, count, false); 421 } 422 423 private InvariantStatus runValue(double @Interned [] v, int count, boolean mutate) { 424 InvariantStatus status; 425 if (mutate) { 426 status = add_mod_elem(v, count); 427 } else { 428 status = check_mod_elem(v, count); 429 } 430 if (status == InvariantStatus.FALSIFIED) { 431 if (logOn() && mutate) { 432 StringBuilder eltString = new StringBuilder(); 433 for (int i = 0; i < num_elts; i++) { 434 eltString.append(Arrays.toString(elts[i]) + " "); 435 } 436 log("destroyed on sample %s previous vals = {%s} num_elts = %s", 437 Arrays.toString(v), eltString, num_elts); 438 } 439 return InvariantStatus.FALSIFIED; 440 } 441 return status; 442 } 443 444 /** 445 * Adds a single sample to the invariant. Returns 446 * the appropriate InvariantStatus from the result 447 * of adding the sample to this. 448 */ 449 public InvariantStatus add_mod_elem(double @Interned [] v, int count) { 450 InvariantStatus status = check_mod_elem(v, count); 451 if (status == InvariantStatus.WEAKENED) { 452 elts[num_elts] = v; 453 num_elts++; 454 } 455 return status; 456 } 457 458 /** 459 * Checks a single sample to the invariant. Returns 460 * the appropriate InvariantStatus from the result 461 * of adding the sample to this. 462 */ 463 public InvariantStatus check_mod_elem(double @Interned [] v, int count) { 464 465 // Look for v in our list of previously seen values. If it's 466 // found, we're all set. 467 for (int i = 0; i < num_elts; i++) { 468 // if (logDetail()) 469 // log ("add_modified (" + v + ")"); 470 if (((elts[i]) == ( v))) { 471 return InvariantStatus.NO_CHANGE; 472 } 473 } 474 475 if (num_elts == dkconfig_size) { 476 return InvariantStatus.FALSIFIED; 477 } 478 479 return InvariantStatus.WEAKENED; 480 } 481 482 @Override 483 protected double computeConfidence() { 484 // This is not ideal. 485 if (num_elts == 0) { 486 return Invariant.CONFIDENCE_UNJUSTIFIED; 487 } else { 488 return Invariant.CONFIDENCE_JUSTIFIED; 489 } 490 } 491 492 @Pure 493 @Override 494 public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) { 495 // Static constants are necessarily OneOf precisely one value. 496 // This removes static constants from the output, which might not be 497 // desirable if the user doesn't know their actual value. 498 if (vis[0].isStaticConstant()) { 499 assert num_elts <= 1; 500 return new DiscardInfo(this, DiscardCode.obvious, vis[0].name() + " is a static constant."); 501 } 502 return super.isObviousStatically(vis); 503 } 504 505 @Override 506 public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) { 507 DiscardInfo super_result = super.isObviousDynamically(vis); 508 if (super_result != null) { 509 return super_result; 510 } 511 512 VarInfo v = vis[0]; 513 514 // We can check if all values in the element sequence match 515 // with the ones we know about (useful for booleans and numeric 516 // enumerations). 517 if (v.aux.hasValue(VarInfoAux.VALID_VALUES) 518 && v.aux.hasValue(VarInfoAux.MAXIMUM_LENGTH) 519 && v.aux.hasValue(VarInfoAux.MINIMUM_LENGTH) 520 && v.aux.getInt(VarInfoAux.MAXIMUM_LENGTH) == 1 521 && v.aux.getInt(VarInfoAux.MINIMUM_LENGTH) == 1) { 522 523 String[] vsValidValues = v.aux.getList(VarInfoAux.VALID_VALUES); 524 Set<Double> setValidValues = new TreeSet<>(); 525 for (String s : vsValidValues) { 526 setValidValues.add(Double.valueOf(s)); 527 } 528 Set<Double> setValuesInvariant = new TreeSet<>(); 529 for (double @Interned [] e : elts) { 530 if (e == null) { 531 continue; 532} 533 for (Double b : e) { 534 setValuesInvariant.add(b); 535 } 536 } 537 if (setValidValues.equals(setValuesInvariant)) { 538 return new DiscardInfo(this, DiscardCode.obvious, 539 "The value list matches the allowed value list"); 540 } 541 } 542 543 return null; 544 } 545 546 /** 547 * Oneof can merge different formulas from lower points to create a single formula at an upper 548 * point. 549 */ 550 @Override 551 public boolean mergeFormulasOk() { 552 return true; 553 } 554 555 @Pure 556 @Override 557 public boolean isSameFormula(Invariant o) { 558 OneOfFloatSequence other = (OneOfFloatSequence) o; 559 if (num_elts != other.num_elts) { 560 return false; 561 } 562 if (num_elts == 0 && other.num_elts == 0) { 563 return true; 564 } 565 566 sort_rep(); 567 other.sort_rep(); 568 569 for (int i = 0; i < num_elts; i++) { 570 if (!((elts[i]) == (other.elts[i]))) { 571 return false; 572 } 573 } 574 575 return true; 576 } 577 578 @Pure 579 @Override 580 public boolean isExclusiveFormula(Invariant o) { 581 if (o instanceof OneOfFloatSequence) { 582 OneOfFloatSequence other = (OneOfFloatSequence) o; 583 584 if (num_elts == 0 || other.num_elts == 0) { 585 return false; 586 } 587 for (int i = 0; i < num_elts; i++) { 588 for (int j = 0; j < other.num_elts; j++) { 589 if (((elts[i]) == (other.elts[j]))) // elements are interned 590 return false; 591 } 592 } 593 594 return true; 595 } 596 597 return false; 598 } 599 600 @Override 601 public boolean hasUninterestingConstant() { 602 603 return false; 604 } 605 606 @Pure 607 @Override 608 public boolean isExact() { 609 return num_elts == 1; 610 } 611 612 // Look up a previously instantiated invariant. 613 public static @Nullable OneOfFloatSequence find(PptSlice ppt) { 614 assert ppt.arity() == 1; 615 for (Invariant inv : ppt.invs) { 616 if (inv instanceof OneOfFloatSequence) { 617 return (OneOfFloatSequence) inv; 618 } 619 } 620 return null; 621 } 622 623 // Interning is lost when an object is serialized and deserialized. 624 // Manually re-intern any interned fields upon deserialization. 625 private void readObject(ObjectInputStream in) throws IOException, 626 ClassNotFoundException { 627 in.defaultReadObject(); 628 629 for (int i = 0; i < num_elts; i++) { 630 elts[i] = Intern.intern(elts[i]); 631 } 632 } 633 634 /** 635 * Merge the invariants in invs to form a new invariant. Each must be a OneOfFloatSequence invariant. 636 * This code finds all of the oneof values from each of the invariants and returns the merged 637 * invariant (if any). 638 * 639 * @param invs list of invariants to merge. The invariants must all be of the same type and should 640 * come from the children of parent_ppt. They should also all be permuted to match the 641 * variable order in parent_ppt. 642 * @param parent_ppt slice that will contain the new invariant 643 */ 644 @Override 645 public @Nullable OneOfFloatSequence merge(List<Invariant> invs, PptSlice parent_ppt) { 646 647 // Create the initial parent invariant from the first child 648 OneOfFloatSequence first = (OneOfFloatSequence) invs.get(0); 649 OneOfFloatSequence result = first.clone(); 650 result.ppt = parent_ppt; 651 652 for (int i = 0; i < result.num_elts; i++) { 653 result.elts[i] = Intern.intern(result.elts[i]); 654 } 655 656 // Loop through the rest of the child invariants 657 for (int i = 1; i < invs.size(); i++ ) { 658 659 // Get this invariant 660 OneOfFloatSequence inv = (OneOfFloatSequence) invs.get(i); 661 662 // Loop through each distinct value found in this child and add 663 // it to the parent. If the invariant is falsified, there is no parent 664 // invariant 665 for (int j = 0; j < inv.num_elts; j++) { 666 double @Interned [] val = inv.elts[j]; 667 668 val = Intern.intern(val); 669 670 InvariantStatus status = result.add_mod_elem(val, 1); 671 if (status == InvariantStatus.FALSIFIED) { 672 673 result.log("%s", "child value '" + Arrays.toString(val) + "' destroyed oneof"); 674 675 return null; 676 } 677 } 678 } 679 680 result.log("Merged '%s' from %s child invariants", result.format(), invs.size()); 681 return result; 682 } 683 684 /** 685 * Setup the invariant with the specified elements. Normally used when searching for a specified 686 * OneOf. The elements of vals are not necessarily interned; this method interns each element. 687 */ 688 public void set_one_of_val(double[][] vals) { 689 690 num_elts = vals.length; 691 for (int i = 0; i < num_elts; i++) { 692 elts[i] = Intern.intern(vals[i]); 693 } 694 } 695 696 /** 697 * Returns true if every element in this invariant is contained in the specified state. For 698 * example if x = 1 and the state contains 1 and 2, true will be returned. 699 */ 700 @Override 701 public boolean state_match(Object state) { 702 703 if (num_elts == 0) { 704 return false; 705 } 706 707 if (!(state instanceof double[] @Interned [])) { 708 // Daikon is about to crash. Produce some debugging output. 709 System.out.printf("state = %s [%s]%n", state, state.getClass()); 710 System.out.printf("problem with %s%n", this); 711 } 712 double[] @Interned [] e = (double[] @Interned []) state; 713 for (int i = 0; i < num_elts; i++) { 714 boolean match = false; 715 for (int j = 0; j < e.length; j++) { 716 if (elts[i] == e[j]) { 717 match = true; 718 break; 719 } 720 } 721 if (!match) { 722 return false; 723 } 724 } 725 return true; 726 } 727 728}