Source code

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