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