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