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}