Source code

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