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 long[] 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 OneOfSequence extends SingleScalarSequence implements OneOf { 044 static final long serialVersionUID = 20030822L; 045 046 /** Debugging logger. */ 047 public static final Logger debug = 048 Logger.getLogger(OneOfSequence.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 /** 063 * Boolean. If true, invariants describing hashcode-typed variables as having any particular value 064 * will have an artificial value substituted for the exact hashhode values. The artificial values 065 * will stay the same from run to run even if the actual hashcode values change (as long as the 066 * OneOf invariants remain the same). If false, hashcodes will be formatted as the application of 067 * a hashcode uninterpreted function to an integer representing the bit pattern of the hashcode. 068 * One might wish to omit the exact values of the hashcodes because they are usually 069 * uninteresting; this is the same reason they print in the native Daikon format, for instance, as 070 * {@code var has only one value} rather than {@code var == 150924732}. 071 */ 072 public static boolean dkconfig_omit_hashcode_values_Simplify = false; 073 074 // Probably needs to keep its own list of the values, and number of each seen. 075 // (That depends on the slice; maybe not until the slice is cleared out. 076 // But so few values is cheap, so this is quite fine for now and long-term.) 077 078 @Unused(when=Prototype.class) 079 private long[] @Interned [] elts; 080 @Unused(when=Prototype.class) 081 private int num_elts; 082 083 @Prototype OneOfSequence() { 084 super(); 085 } 086 087 OneOfSequence(PptSlice slice) { 088 super(slice); 089 090 // Elements are interned, so can test with == 091 // (in the general online case, it's not worth interning). 092 elts = new long[dkconfig_size] @Interned []; 093 094 num_elts = 0; 095 096 // var() is initialized by the super constructor 097 assert var().is_array() : 098 String.format("In %s constructor, var %s (type=%s, rep_type=%s) should be an array", 099 "OneOfSequence", var().name(), var().type, var().rep_type); 100 101 } 102 103 private static @Prototype OneOfSequence proto = new @Prototype OneOfSequence(); 104 105 /** Returns the prototype invariant for OneOfSequence */ 106 public static @Prototype OneOfSequence get_proto() { 107 return proto; 108 } 109 110 @Override 111 public boolean enabled() { 112 return dkconfig_enabled; 113 } 114 115 @Override 116 public OneOfSequence instantiate_dyn(@Prototype OneOfSequence this, PptSlice slice) { 117 return new OneOfSequence(slice); 118 } 119 120 @Pure 121 public boolean is_boolean(@GuardSatisfied OneOfSequence this) { 122 return var().file_rep_type.elementType() == ProglangType.BOOLEAN; 123 } 124 @Pure 125 public boolean is_hashcode(@GuardSatisfied OneOfSequence this) { 126 return var().file_rep_type.elementType() == ProglangType.HASHCODE; 127 } 128 129 @SideEffectFree 130 @Override 131 public OneOfSequence clone(@GuardSatisfied OneOfSequence this) { 132 OneOfSequence result = (OneOfSequence) super.clone(); 133 result.elts = elts.clone(); 134 135 for (int i = 0; i < num_elts; i++) { 136 result.elts[i] = Intern.intern(elts[i].clone()); 137 } 138 139 result.num_elts = this.num_elts; 140 return result; 141 } 142 143 @Override 144 public int num_elts() { 145 return num_elts; 146 } 147 148 @Override 149 public Object elt() { 150 return elt(0); 151 } 152 153 public Object elt(int index) { 154 if (num_elts <= index) { 155 throw new Error("Represents " + num_elts + " elements, index " + index + " not valid"); 156 } 157 158 return elts[index]; 159 } 160 161 static Comparator<long[]> comparator = ArraysPlume.LongArrayComparatorLexical.it; 162 163 private void sort_rep(@GuardSatisfied OneOfSequence this) { 164 Arrays.sort(elts, 0, num_elts , comparator); 165 } 166 167 public long @Interned [] min_elt() { 168 if (num_elts == 0) { 169 throw new Error("Represents no elements"); 170 } 171 sort_rep(); 172 return elts[0]; 173 } 174 175 public long @Interned [] max_elt() { 176 if (num_elts == 0) { 177 throw new Error("Represents no elements"); 178 } 179 sort_rep(); 180 return elts[num_elts - 1]; 181 } 182 183 // Assumes the other array is already sorted 184 public boolean compare_rep(int num_other_elts, long[] @Interned [] other_elts) { 185 if (num_elts != num_other_elts) { 186 return false; 187 } 188 sort_rep(); 189 for (int i = 0; i < num_elts; i++) { 190 if (!((elts[i]) == (other_elts[i]))) { // elements are interned 191 return false; 192 } 193 } 194 return true; 195 } 196 197 private String subarray_rep(@GuardSatisfied OneOfSequence this) { 198 // Not so efficient an implementation, but simple; 199 // and how often will we need to print this anyway? 200 sort_rep(); 201 StringJoiner sj = new StringJoiner(", ", "{ ", " }"); 202 for (int i = 0; i < num_elts; i++) { 203 204 if (PrintInvariants.dkconfig_static_const_infer) { 205 boolean curVarMatch = false; 206 PptTopLevel pptt = ppt.parent; 207 for (VarInfo vi : pptt.var_infos) { 208 if (vi.isStaticConstant() && VarComparability.comparable(vi, var())) { 209 Object constantVal = vi.constantValue(); 210 if (constantVal.equals(elts[i])) { 211 sj.add(vi.name()); 212 curVarMatch = true; 213 } 214 } 215 } 216 217 if (curVarMatch == false) { 218 sj.add(Arrays.toString(elts[i])); 219 } 220 } else { 221 sj.add(Arrays.toString(elts[i])); 222 } 223 224 } 225 return sj.toString(); 226 } 227 228 @Override 229 public String repr(@GuardSatisfied OneOfSequence this) { 230 return "OneOfSequence" + varNames() + ": falsified=" + falsified 231 + ", num_elts=" + num_elts 232 + ", elts=" + subarray_rep(); 233 } 234 235 private boolean all_nulls(@GuardSatisfied OneOfSequence this, int value_no) { 236 long @Interned [] seq = elts[value_no]; 237 for (int i = 0; i < seq.length; i++) { 238 if (seq[i] != 0) { 239 return false; 240 } 241 } 242 return true; 243 } 244 private boolean no_nulls(@GuardSatisfied OneOfSequence this, int value_no) { 245 long @Interned [] seq = elts[value_no]; 246 for (int i = 0; i < seq.length; i++) { 247 if (seq[i] == 0) { 248 return false; 249 } 250 } 251 return true; 252 } 253 254 @SideEffectFree 255 @Override 256 public String format_using(@GuardSatisfied OneOfSequence this, OutputFormat format) { 257 sort_rep(); 258 259 if (format.isJavaFamily()) { 260 return format_java_family(format); 261 } 262 263 if (format == OutputFormat.DAIKON) { 264 return format_daikon(); 265 } else if (format == OutputFormat.SIMPLIFY) { 266 return format_simplify(); 267 } else if (format == OutputFormat.ESCJAVA) { 268 String result = format_esc(); 269 return result; 270 } else if (format == OutputFormat.CSHARPCONTRACT) { 271 return format_csharp_contract(); 272 } else { 273 return format_unimplemented(format); 274 } 275 } 276 277 public String format_daikon(@GuardSatisfied OneOfSequence this) { 278 String varname = var().name(); 279 if (num_elts == 1) { 280 281 if (is_hashcode()) { 282 // we only have one value, because add_modified dies if more 283 assert num_elts == 1; 284 long @Interned [] value = elts[0]; 285 if (value.length == 0) { 286 return varname + " == []"; 287 } else if ((value.length == 1) && (value[0] == 0)) { 288 return varname + " == [null]"; 289 } else if (no_nulls(0)) { 290 return varname + " contains no nulls and has only one value, of length " + value.length; 291 } else if (all_nulls(0)) { 292 return varname + " contains only nulls and has only one value, of length " + value.length; 293 } else { 294 return varname + " has only one value, of length " + value.length; 295 } 296 } else { 297 if (PrintInvariants.dkconfig_static_const_infer) { 298 PptTopLevel pptt = ppt.parent; 299 for (VarInfo vi : pptt.var_infos) { 300 if (vi.isStaticConstant() && VarComparability.comparable(vi, var())) { 301 Object constantVal = vi.constantValue(); 302 if (constantVal.equals(elts[0])) { 303 return varname + " == " + vi.name(); 304 } 305 } 306 } 307 } 308 return varname + " == " + Arrays.toString(elts[0]); 309 } 310 311 } else { 312 return varname + " one of " + subarray_rep(); 313 } 314 } 315 316 public String format_esc(@GuardSatisfied OneOfSequence this) { 317 sort_rep(); 318 319 String result; 320 321 String length = null; 322 String forall = null; 323 324 if (is_hashcode()) { 325 // we only have one value, because add_modified dies if more 326 assert num_elts == 1; 327 long @Interned [] value = elts[0]; 328 if (var().isArray()) { 329 length = null; 330 if (!var().isSlice()) { 331 length = var().get_length().esc_name() + " == " + value.length; 332 } 333 String[] form = VarInfo.esc_quantify(var()); 334 if (no_nulls(0)) { 335 forall = form[0] + "(" + form[1] + " != null)" + form[2]; 336 } else if (all_nulls(0)) { 337 forall = form[0] + "(" + form[1] + " == null)" + form[2]; 338 } 339 } 340 } 341 342 if (length == null) { 343 if (forall == null) { 344 return format_unimplemented(OutputFormat.ESCJAVA); // "needs to be implemented" 345 } else { 346 result = forall; 347 } 348 } else { 349 if (forall == null) { 350 result = length; 351 } else { 352 result = "(" + length + ") && (" + forall + ")"; 353 } 354 } 355 356 return result; 357 } 358 359public String format_csharp_contract(@GuardSatisfied OneOfSequence this) { 360 361 @NonNull @Initialized String result; 362 363 result = "(\"oneOf.java.jpp: SEQUENCE unimplemented\" != null)"; // "interned" 364 365 return result; 366 } 367 368 public String format_java_family(@GuardSatisfied OneOfSequence this, OutputFormat format) { 369 370 String result; 371 372 result = "(\"oneOf.java.jpp: SEQUENCE unimplemented\" != null)"; // "interned" 373 374 return result; 375 } 376 377 public String format_simplify(@GuardSatisfied OneOfSequence this) { 378 379 // if (is_hashcode() && dkconfig_omit_hashcode_values_Simplify) 380 // return "(AND)"; 381 382 sort_rep(); 383 384 String result; 385 386 StringBuilder resultBuf = new StringBuilder(); 387 for (int i = 0; i < num_elts; i++) { 388 long @Interned [] seq = elts[i]; 389 String offset = null; 390 String contents = null; 391 String[] bounds_name; 392 String length = var().get_simplify_size_name(); 393 // if ((length == null) && var().name.isApplySizeSafe()) 394 // System.out.printf("var %s, type %s, is_array %b%n", var().name(), 395 // var().type, var().type.isArray()); 396 if (length != null) { 397 length = "(EQ " + length + " "+ simplify_format_long(seq.length) + ")"; 398 } else if ((bounds_name = var().get_simplify_slice_bounds()) != null) { 399 String size = "(+ 1 (- " + bounds_name[1] +" " + bounds_name[0] + "))"; 400 length = "(EQ " + size + " " + simplify_format_long(seq.length) + ")"; 401 offset = bounds_name[0]; 402 } 403 404 if (is_hashcode()) { 405 String[] form = VarInfo.simplify_quantify(var()); 406 if (no_nulls(i)) { 407 contents = form[0] + "(NEQ " + form[1] + " null)" + form[2]; 408 } else if (all_nulls(i)) { 409 contents = form[0] + "(EQ " + form[1] + " null)" + form[2]; 410 } 411 } else { 412 StringBuilder contentsBuf = new StringBuilder(); 413 for (int j = 0; j < seq.length; j++) { 414 if (j + 3 < seq.length 415 && ((seq[j]) == ( seq[j + 1])) 416 && ((seq[j]) == ( seq[j + 2])) 417 && ((seq[j]) == ( seq[j + 3]))) { 418 // Compress a sequence of adjacent values 419 int k = j + 4; 420 for (; k < seq.length; k++) { 421 if (!((seq[j]) == ( seq[k]))) { 422 break; 423 } 424 } 425 k--; 426 String index_name = VarInfo.get_simplify_free_index(var()); 427 String cond_left, cond_right; 428 if (offset == null) { 429 cond_left = "(<= " + j + " " + index_name + ")"; 430 cond_right = "(<= " + index_name + " " + k + ")"; 431 } else { 432 cond_left = "(<= (+ " + offset + " " + j + ") " 433 + index_name + ")"; 434 cond_right = "(>= (+ " + offset + " " + k + ") " 435 + index_name + ")"; 436 } 437 String cond = "(AND " + cond_left + " " + cond_right + ")"; 438 String nth = var().get_simplify_selectNth(index_name, true, 0); 439 String eq = "(EQ " + nth + " " + simplify_format_long(seq[j]) + ")"; 440 String implies = "(IMPLIES " + cond + " " + eq + ")"; 441 String forall = "(FORALL (" + index_name + ") " + implies + ")"; 442 contentsBuf.append(" " + forall); 443 j = k; 444 } else { 445 // Output a single value 446 String nth = var().get_simplify_selectNth_lower(j); 447 if (nth == null) { 448 String classname = this.getClass().toString().substring(6); 449 result = "warning: method " + classname 450 + ".format_simplify() needs to fix selectNth(): " + format(); 451 return result; 452 } 453 String value = simplify_format_long(seq[j]); 454 contentsBuf.append(" (EQ " + nth + " " + value + ")"); 455 // if (nth.contains ("--orig__a")) 456 // System.out.printf("regular orig__a%n"); 457 458 } 459 } 460 if (seq.length > 1) { 461 contents = "(AND " + contentsBuf.toString() + ")"; 462 } else if (seq.length == 1) { 463 contents = contentsBuf.toString().substring(1); 464 } else if (seq.length == 0) { 465 contents = null; // back from "" 466 } 467 } 468 if (length == null && contents == null) { 469 resultBuf.append(" "); 470 } else if (length == null && contents != null) { 471 resultBuf.append(" " + contents); 472 } else if (length != null && contents == null) { 473 resultBuf.append(" " + length); 474 } else { 475 assert length != null && contents != null; 476 resultBuf.append(" (AND " + length + " " + contents + ")"); 477 } 478 479 } 480 if (num_elts > 1) { 481 result = "(OR" + resultBuf.toString() + ")"; 482 } else if (num_elts == 1) { 483 // chop leading space 484 result = resultBuf.toString().substring(1); 485 } else if (num_elts == 0) { 486 return format_too_few_samples(OutputFormat.SIMPLIFY, null); 487 } else { 488 throw new Error("this can't happen"); 489 // result = null; 490 } 491 if (result.trim().equals("")) { 492 result = "format_simplify() failed on a weird OneOf"; 493 } 494 495 if (result.indexOf("format_simplify") == -1) { 496 daikon.simplify.SimpUtil.assert_well_formed(result); 497 } 498 return result; 499 } 500 501 @Override 502 public InvariantStatus add_modified(long @Interned [] a, int count) { 503 return runValue(a, count, true); 504 } 505 506 @Override 507 public InvariantStatus check_modified(long @Interned [] a, int count) { 508 return runValue(a, count, false); 509 } 510 511 private InvariantStatus runValue(long @Interned [] v, int count, boolean mutate) { 512 InvariantStatus status; 513 if (mutate) { 514 status = add_mod_elem(v, count); 515 } else { 516 status = check_mod_elem(v, count); 517 } 518 if (status == InvariantStatus.FALSIFIED) { 519 if (logOn() && mutate) { 520 StringBuilder eltString = new StringBuilder(); 521 for (int i = 0; i < num_elts; i++) { 522 eltString.append(Arrays.toString(elts[i]) + " "); 523 } 524 log("destroyed on sample %s previous vals = {%s} num_elts = %s", 525 Arrays.toString(v), eltString, num_elts); 526 } 527 return InvariantStatus.FALSIFIED; 528 } 529 return status; 530 } 531 532 /** 533 * Adds a single sample to the invariant. Returns 534 * the appropriate InvariantStatus from the result 535 * of adding the sample to this. 536 */ 537 public InvariantStatus add_mod_elem(long @Interned [] v, int count) { 538 InvariantStatus status = check_mod_elem(v, count); 539 if (status == InvariantStatus.WEAKENED) { 540 elts[num_elts] = v; 541 num_elts++; 542 } 543 return status; 544 } 545 546 /** 547 * Checks a single sample to the invariant. Returns 548 * the appropriate InvariantStatus from the result 549 * of adding the sample to this. 550 */ 551 public InvariantStatus check_mod_elem(long @Interned [] v, int count) { 552 553 // Look for v in our list of previously seen values. If it's 554 // found, we're all set. 555 for (int i = 0; i < num_elts; i++) { 556 // if (logDetail()) 557 // log ("add_modified (" + v + ")"); 558 if (((elts[i]) == ( v))) { 559 return InvariantStatus.NO_CHANGE; 560 } 561 } 562 563 if (num_elts == dkconfig_size) { 564 return InvariantStatus.FALSIFIED; 565 } 566 567 if (is_hashcode() && (num_elts == 1)) { 568 return InvariantStatus.FALSIFIED; 569 } 570 571 return InvariantStatus.WEAKENED; 572 } 573 574 @Override 575 protected double computeConfidence() { 576 // This is not ideal. 577 if (num_elts == 0) { 578 return Invariant.CONFIDENCE_UNJUSTIFIED; 579 } else { 580 return Invariant.CONFIDENCE_JUSTIFIED; 581 } 582 } 583 584 @Pure 585 @Override 586 public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) { 587 // Static constants are necessarily OneOf precisely one value. 588 // This removes static constants from the output, which might not be 589 // desirable if the user doesn't know their actual value. 590 if (vis[0].isStaticConstant()) { 591 assert num_elts <= 1; 592 return new DiscardInfo(this, DiscardCode.obvious, vis[0].name() + " is a static constant."); 593 } 594 return super.isObviousStatically(vis); 595 } 596 597 @Override 598 public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) { 599 DiscardInfo super_result = super.isObviousDynamically(vis); 600 if (super_result != null) { 601 return super_result; 602 } 603 604 VarInfo v = vis[0]; 605 606 // We can check if all values in the element sequence match 607 // with the ones we know about (useful for booleans and numeric 608 // enumerations). 609 if (v.aux.hasValue(VarInfoAux.VALID_VALUES) 610 && v.aux.hasValue(VarInfoAux.MAXIMUM_LENGTH) 611 && v.aux.hasValue(VarInfoAux.MINIMUM_LENGTH) 612 && v.aux.getInt(VarInfoAux.MAXIMUM_LENGTH) == 1 613 && v.aux.getInt(VarInfoAux.MINIMUM_LENGTH) == 1) { 614 615 String[] vsValidValues = v.aux.getList(VarInfoAux.VALID_VALUES); 616 Set<Long> setValidValues = new TreeSet<>(); 617 for (String s : vsValidValues) { 618 setValidValues.add(Long.valueOf(s)); 619 } 620 Set<Long> setValuesInvariant = new TreeSet<>(); 621 for (long @Interned [] e : elts) { 622 if (e == null) { 623 continue; 624} 625 for (Long b : e) { 626 setValuesInvariant.add(b); 627 } 628 } 629 if (setValidValues.equals(setValuesInvariant)) { 630 return new DiscardInfo(this, DiscardCode.obvious, 631 "The value list matches the allowed value list"); 632 } 633 } 634 635 return null; 636 } 637 638 /** 639 * Oneof can merge different formulas from lower points to create a single formula at an upper 640 * point. 641 */ 642 @Override 643 public boolean mergeFormulasOk() { 644 return true; 645 } 646 647 @Pure 648 @Override 649 public boolean isSameFormula(Invariant o) { 650 OneOfSequence other = (OneOfSequence) o; 651 if (num_elts != other.num_elts) { 652 return false; 653 } 654 if (num_elts == 0 && other.num_elts == 0) { 655 return true; 656 } 657 658 sort_rep(); 659 other.sort_rep(); 660 661 // All nonzero hashcode values should be considered equal to each other 662 // 663 // Examples: 664 // inv1 inv2 result 665 // ------- ------- ------ 666 // {19,23} {91,0} false 667 // {19,23} {91,32} true 668 // {19,0} {91,0} true 669 // {0,0} {0,0} true 670 671 if (is_hashcode() && other.is_hashcode()) { 672 // we only have one value, because add_modified dies if more 673 assert num_elts == 1 && other.num_elts == 1; 674 675 long @Interned [] thisSeq = elts[0]; 676 long @Interned [] otherSeq = other.elts[0]; 677 if (thisSeq.length != otherSeq.length) { 678 return false; 679 } 680 681 for (int i = 0; i < thisSeq.length; i++) { 682 if ((thisSeq[i] == 0 && otherSeq[i] != 0) 683 || (thisSeq[i] != 0 && otherSeq[i] == 0)) { 684 return false; 685 } 686 } 687 688 return true; 689 } 690 691 for (int i = 0; i < num_elts; i++) { 692 if (!((elts[i]) == (other.elts[i]))) { 693 return false; 694 } 695 } 696 697 return true; 698 } 699 700 @Pure 701 @Override 702 public boolean isExclusiveFormula(Invariant o) { 703 if (o instanceof OneOfSequence) { 704 OneOfSequence other = (OneOfSequence) o; 705 706 if (num_elts == 0 || other.num_elts == 0) { 707 return false; 708 } 709 for (int i = 0; i < num_elts; i++) { 710 for (int j = 0; j < other.num_elts; j++) { 711 if (((elts[i]) == (other.elts[j]))) // elements are interned 712 return false; 713 } 714 } 715 716 // Be even more aggressive about rejecting these for use in 717 // implications in this case, since, we'd be printing them as 718 // "true" 719 /* 720 if (dkconfig_omit_hashcode_values_Simplify 721 && (is_hashcode() || other.is_hashcode())) { 722 return false; 723 } 724 */ 725 726 return true; 727 } 728 729 return false; 730 } 731 732 @Override 733 public boolean hasUninterestingConstant() { 734 735 for (int i = 0; i < num_elts; i++) { 736 for (int j = 0; j < elts[i].length; j++) { 737 if (elts[i][j] < -1 || elts[i][j] > 2) { 738 return true; 739 } 740 } 741 } 742 743 return false; 744 } 745 746 @Pure 747 @Override 748 public boolean isExact() { 749 return num_elts == 1; 750 } 751 752 // Look up a previously instantiated invariant. 753 public static @Nullable OneOfSequence find(PptSlice ppt) { 754 assert ppt.arity() == 1; 755 for (Invariant inv : ppt.invs) { 756 if (inv instanceof OneOfSequence) { 757 return (OneOfSequence) inv; 758 } 759 } 760 return null; 761 } 762 763 // Interning is lost when an object is serialized and deserialized. 764 // Manually re-intern any interned fields upon deserialization. 765 private void readObject(ObjectInputStream in) throws IOException, 766 ClassNotFoundException { 767 in.defaultReadObject(); 768 769 for (int i = 0; i < num_elts; i++) { 770 elts[i] = Intern.intern(elts[i]); 771 } 772 } 773 774 /** 775 * Merge the invariants in invs to form a new invariant. Each must be a OneOfSequence invariant. 776 * This code finds all of the oneof values from each of the invariants and returns the merged 777 * invariant (if any). 778 * 779 * @param invs list of invariants to merge. The invariants must all be of the same type and should 780 * come from the children of parent_ppt. They should also all be permuted to match the 781 * variable order in parent_ppt. 782 * @param parent_ppt slice that will contain the new invariant 783 */ 784 @Override 785 public @Nullable OneOfSequence merge(List<Invariant> invs, PptSlice parent_ppt) { 786 787 // Create the initial parent invariant from the first child 788 OneOfSequence first = (OneOfSequence) invs.get(0); 789 OneOfSequence result = first.clone(); 790 result.ppt = parent_ppt; 791 792 for (int i = 0; i < result.num_elts; i++) { 793 result.elts[i] = Intern.intern(result.elts[i]); 794 } 795 796 // Loop through the rest of the child invariants 797 for (int i = 1; i < invs.size(); i++ ) { 798 799 // Get this invariant 800 OneOfSequence inv = (OneOfSequence) invs.get(i); 801 802 // Loop through each distinct value found in this child and add 803 // it to the parent. If the invariant is falsified, there is no parent 804 // invariant 805 for (int j = 0; j < inv.num_elts; j++) { 806 long @Interned [] val = inv.elts[j]; 807 808 val = Intern.intern(val); 809 810 InvariantStatus status = result.add_mod_elem(val, 1); 811 if (status == InvariantStatus.FALSIFIED) { 812 813 result.log("%s", "child value '" + Arrays.toString(val) + "' destroyed oneof"); 814 815 return null; 816 } 817 } 818 } 819 820 result.log("Merged '%s' from %s child invariants", result.format(), invs.size()); 821 return result; 822 } 823 824 /** 825 * Setup the invariant with the specified elements. Normally used when searching for a specified 826 * OneOf. The elements of vals are not necessarily interned; this method interns each element. 827 */ 828 public void set_one_of_val(long[][] vals) { 829 830 num_elts = vals.length; 831 for (int i = 0; i < num_elts; i++) { 832 elts[i] = Intern.intern(vals[i]); 833 } 834 } 835 836 /** 837 * Returns true if every element in this invariant is contained in the specified state. For 838 * example if x = 1 and the state contains 1 and 2, true will be returned. 839 */ 840 @Override 841 public boolean state_match(Object state) { 842 843 if (num_elts == 0) { 844 return false; 845 } 846 847 if (!(state instanceof long[] @Interned [])) { 848 // Daikon is about to crash. Produce some debugging output. 849 System.out.printf("state = %s [%s]%n", state, state.getClass()); 850 System.out.printf("problem with %s%n", this); 851 } 852 long[] @Interned [] e = (long[] @Interned []) state; 853 for (int i = 0; i < num_elts; i++) { 854 boolean match = false; 855 for (int j = 0; j < e.length; j++) { 856 if (elts[i] == e[j]) { 857 match = true; 858 break; 859 } 860 } 861 if (!match) { 862 return false; 863 } 864 } 865 return true; 866 } 867 868}