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
009  import daikon.inv.binary.twoSequence.SubSequence;
010  import daikon.inv.unary.scalar.*;
011
012import java.io.*;
013import java.util.logging.Logger;
014import java.util.logging.Level;
015import java.util.*;
016
017import org.checkerframework.checker.initialization.qual.Initialized;
018import org.checkerframework.checker.interning.qual.Interned;
019import org.checkerframework.checker.lock.qual.GuardSatisfied;
020import org.checkerframework.checker.nullness.qual.NonNull;
021import org.checkerframework.checker.nullness.qual.Nullable;
022import org.checkerframework.dataflow.qual.Pure;
023import org.checkerframework.dataflow.qual.SideEffectFree;
024import org.checkerframework.framework.qual.Unused;
025import daikon.SignaturesUtil;
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 long 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   * May print as {@code x[] elements has only one value} when {@code x} is an array of hashcodes
044   * (pointers) -- this is because the numerical value of the hashcode (pointer) is uninteresting.
045
046   */
047
048@SuppressWarnings("UnnecessaryParentheses")  // generated code, parentheses are sometimes needed
049public final class EltOneOf extends SingleScalarSequence implements OneOf {
050  static final long serialVersionUID = 20030822L;
051
052  /** Debugging logger. */
053  public static final Logger debug =
054    Logger.getLogger(EltOneOf.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  /**
069   * Boolean. If true, invariants describing hashcode-typed variables as having any particular value
070   * will have an artificial value substituted for the exact hashhode values. The artificial values
071   * will stay the same from run to run even if the actual hashcode values change (as long as the
072   * OneOf invariants remain the same). If false, hashcodes will be formatted as the application of
073   * a hashcode uninterpreted function to an integer representing the bit pattern of the hashcode.
074   * One might wish to omit the exact values of the hashcodes because they are usually
075   * uninteresting; this is the same reason they print in the native Daikon format, for instance, as
076   * {@code var has only one value} rather than {@code var == 150924732}.
077   */
078  public static boolean dkconfig_omit_hashcode_values_Simplify = false;
079
080  // Probably needs to keep its own list of the values, and number of each seen.
081  // (That depends on the slice; maybe not until the slice is cleared out.
082  // But so few values is cheap, so this is quite fine for now and long-term.)
083
084  @Unused(when=Prototype.class)
085  private long[] elts;
086  @Unused(when=Prototype.class)
087  private int num_elts;
088
089  @Prototype EltOneOf() {
090    super();
091  }
092
093  EltOneOf(PptSlice slice) {
094    super(slice);
095
096    elts = new long[dkconfig_size];
097
098    num_elts = 0;
099
100    // var() is initialized by the super constructor
101    assert var().is_array() :
102      String.format("In %s constructor, var %s (type=%s, rep_type=%s) should be an array",
103                     "EltOneOf", var().name(), var().type, var().rep_type);
104
105  }
106
107  private static @Prototype EltOneOf proto = new @Prototype EltOneOf();
108
109  /** Returns the prototype invariant for EltOneOf */
110  public static @Prototype EltOneOf get_proto() {
111    return proto;
112  }
113
114  @Override
115  public boolean enabled() {
116    return dkconfig_enabled;
117  }
118
119  @Override
120  public EltOneOf instantiate_dyn(@Prototype EltOneOf this, PptSlice slice) {
121    return new EltOneOf(slice);
122  }
123
124  @Pure
125  public boolean is_boolean(@GuardSatisfied EltOneOf this) {
126    return var().file_rep_type.elementType() == ProglangType.BOOLEAN;
127  }
128  @Pure
129  public boolean is_hashcode(@GuardSatisfied EltOneOf this) {
130    return var().file_rep_type.elementType() == ProglangType.HASHCODE;
131  }
132
133  @SideEffectFree
134  @Override
135  public EltOneOf clone(@GuardSatisfied EltOneOf this) {
136    EltOneOf result = (EltOneOf) super.clone();
137    result.elts = elts.clone();
138
139    result.num_elts = this.num_elts;
140    return result;
141  }
142
143  @Override
144  public int num_elts() {
145    return num_elts;
146  }
147
148  @Override
149  public Object elt() {
150    return elt(0);
151  }
152
153  public Object elt(int index) {
154    if (num_elts <= index) {
155      throw new Error("Represents " + num_elts + " elements, index " + index + " not valid");
156    }
157
158    // Not sure whether interning is necessary (or just returning an Integer
159    // would be sufficient), but just in case...
160    return Intern.internedLong(elts[index]);
161  }
162
163  private void sort_rep(@GuardSatisfied EltOneOf this) {
164    Arrays.sort(elts, 0, num_elts );
165  }
166
167  public long min_elt() {
168    if (num_elts == 0) {
169      throw new Error("Represents no elements");
170    }
171    sort_rep();
172    return elts[0];
173  }
174
175  public long max_elt() {
176    if (num_elts == 0) {
177      throw new Error("Represents no elements");
178    }
179    sort_rep();
180    return elts[num_elts - 1];
181  }
182
183  // Assumes the other array is already sorted
184  public boolean compare_rep(int num_other_elts, long[] other_elts) {
185    if (num_elts != num_other_elts) {
186      return false;
187    }
188    sort_rep();
189    for (int i = 0; i < num_elts; i++) {
190      if (!((elts[i]) == (other_elts[i]))) { // elements are interned
191        return false;
192      }
193    }
194    return true;
195  }
196
197  private String subarray_rep(@GuardSatisfied EltOneOf this) {
198    // Not so efficient an implementation, but simple;
199    // and how often will we need to print this anyway?
200    sort_rep();
201    StringJoiner sj = new StringJoiner(", ", "{ ", " }");
202    for (int i = 0; i < num_elts; i++) {
203
204      if (PrintInvariants.dkconfig_static_const_infer) {
205        boolean curVarMatch = false;
206        PptTopLevel pptt = ppt.parent;
207        for (VarInfo vi : pptt.var_infos) {
208          if (vi.isStaticConstant() && VarComparability.comparable(vi, var())) {
209            Object constantVal = vi.constantValue();
210            if (constantVal.equals(elts[i])) {
211              sj.add(vi.name());
212              curVarMatch = true;
213            }
214          }
215        }
216
217        if (curVarMatch == false) {
218          sj.add((((elts[i] == 0) && (var().file_rep_type == ProglangType.HASHCODE_ARRAY)) ? "null" : ((Integer.MIN_VALUE <= elts[i] && elts[i] <= Integer.MAX_VALUE) ? String.valueOf(elts[i]) : (String.valueOf(elts[i]) + "L"))));
219        }
220      } else {
221        sj.add((((elts[i] == 0) && (var().file_rep_type == ProglangType.HASHCODE_ARRAY)) ? "null" : ((Integer.MIN_VALUE <= elts[i] && elts[i] <= Integer.MAX_VALUE) ? String.valueOf(elts[i]) : (String.valueOf(elts[i]) + "L"))));
222      }
223
224    }
225    return sj.toString();
226  }
227
228  @Override
229  public String repr(@GuardSatisfied EltOneOf this) {
230    return "EltOneOf" + varNames() + ": falsified=" + falsified
231      + ", num_elts=" + num_elts
232      + ", elts=" + subarray_rep();
233  }
234
235  @SideEffectFree
236  @Override
237  public String format_using(@GuardSatisfied EltOneOf this, OutputFormat format) {
238    sort_rep();
239
240    if (format.isJavaFamily()) {
241      return format_java_family(format);
242    }
243
244    if (format == OutputFormat.DAIKON) {
245      return format_daikon();
246    } else if (format == OutputFormat.SIMPLIFY) {
247      return format_simplify();
248    } else if (format == OutputFormat.ESCJAVA) {
249      String result = format_esc();
250      return result;
251    } else if (format == OutputFormat.CSHARPCONTRACT) {
252      return format_csharp_contract();
253    } else {
254      return format_unimplemented(format);
255    }
256  }
257
258  public String format_daikon(@GuardSatisfied EltOneOf this) {
259    String varname = var().name() + " elements";
260    if (num_elts == 1) {
261
262        if (is_boolean()) {
263          if ((elts[0] != 0) && (elts[0] != 1)) {
264              System.out.println("WARNING:: Variable "
265              + varname + " is of type boolean, but has non boolean value: "
266              + elts[0]);
267          }
268          return varname + " == " + ((elts[0] == 0) ? "false" : "true");
269        } else if (is_hashcode()) {
270          if (elts[0] == 0) {
271            return varname + " == null";
272          } else {
273            return varname + " has only one value"
274              // + " (hashcode=" + elts[0] + ")"
275              ;
276          }
277        } else {
278          if (PrintInvariants.dkconfig_static_const_infer) {
279            PptTopLevel pptt = ppt.parent;
280            for (VarInfo vi : pptt.var_infos) {
281              if (vi.isStaticConstant() && VarComparability.comparable(vi, var())) {
282                Object constantVal = vi.constantValue();
283                if (constantVal.equals(elts[0])) {
284                  return varname + " == " + vi.name();
285                }
286              }
287            }
288          }
289          return varname + " == " + (((elts[0] == 0) && (var().file_rep_type == ProglangType.HASHCODE_ARRAY)) ? "null" : ((Integer.MIN_VALUE <= elts[0] && elts[0] <= Integer.MAX_VALUE) ? String.valueOf(elts[0]) : (String.valueOf(elts[0]) + "L")));
290        }
291
292    } else {
293      return varname + " one of " + subarray_rep();
294    }
295  }
296
297  public String format_esc(@GuardSatisfied EltOneOf this) {
298    sort_rep();
299
300    String[] form = VarInfo.esc_quantify(var());
301    String varname = form[1];
302
303    String result;
304
305    if (is_boolean()) {
306      assert num_elts == 1;
307      assert (elts[0] == 0) || (elts[0] == 1);
308      result = varname + " == " + ((elts[0] == 0) ? "false" : "true");
309    } else if (is_hashcode()) {
310      if (num_elts == 1) {
311        if (elts[0] == 0) {
312          result = varname + " == null";
313        } else {
314          // This seems wrong, because there is already a "!= null" invariant.
315          // This invariant (EltOneOf) just shouldn't print for ESC format.
316          result = varname + " != null";
317          // varname + " has only one value"
318          // + " (hashcode=" + elts[0] + ")"
319        }
320      } else if (num_elts == 2) {
321        // add_modified allows two elements iff one is null
322        assert elts[0] == 0;
323        assert elts[1] != 0;
324        return format_unimplemented(OutputFormat.ESCJAVA); // "needs to be implemented"
325      } else if (num_elts == 0) {
326        // Do nothing
327        return format_unimplemented(OutputFormat.ESCJAVA); // "needs to be implemented"
328      } else {
329        throw new Error("Contains more than 2 elements");
330      }
331    } else {
332      result = "";
333      for (int i = 0; i < num_elts; i++) {
334        if (i != 0) { result += " || "; }
335        result += varname + " == " + (((elts[i] == 0) && (var().file_rep_type == ProglangType.HASHCODE_ARRAY)) ? "null" : ((Integer.MIN_VALUE <= elts[i] && elts[i] <= Integer.MAX_VALUE) ? String.valueOf(elts[i]) : (String.valueOf(elts[i]) + "L")));
336      }
337    }
338
339    result = form[0] + "(" + result + ")" + form[2];
340
341    return result;
342  }
343
344public String format_csharp_contract(@GuardSatisfied EltOneOf this) {
345
346    @NonNull @Initialized String result;
347
348    String equalsString = " == ";
349    String endString = "";
350
351    String[] split = var().csharp_array_split();
352    List<String> args_list = new ArrayList<>();
353    // Construct the array that unary value will be compared against.
354    for (int i = 0; i < num_elts; i++) {
355
356      args_list.add((((elts[i] == 0) && (var().file_rep_type == ProglangType.HASHCODE_ARRAY)) ? "null" : ((Integer.MIN_VALUE <= elts[i] && elts[i] <= Integer.MAX_VALUE) ? String.valueOf(elts[i]) : (String.valueOf(elts[i]) + "L"))));
357
358    }
359    String args = String.join(", ", args_list);
360
361    if (num_elts == 0) { // If there are no elements, length must be 0.
362      String varname = var().csharp_name();
363      return varname + ".Count() == 0";
364    } else if (num_elts == 1) {
365
366      if (is_boolean()) {
367        String bool_str = (elts[0] == 0) ? "false" : "true";
368        result = "Contract.ForAll(" + split[0] + ", x => x" + split[1] + " == " + bool_str + ")";
369      } else if (is_hashcode()) {
370        String null_str = elts[0] == 0 ? " == null" : " != null"; // interned
371        result = "Contract.ForAll(" + split[0] + ", x => x" + split[1] + null_str + ")";
372      } else {
373        result = "Contract.ForAll(" + split[0] + ", x => x" + split[1] + equalsString + args + endString + ")";
374      }
375    } else {
376      assert num_elts > 1;
377      result = "Contract.ForAll(" + split[0] + ", x => x" + split[1] + ".OneOf(" + args + "))";
378    }
379
380    return result;
381  }
382
383  public String format_java_family(@GuardSatisfied EltOneOf this, OutputFormat format) {
384
385    String result;
386
387    // Setting up the name of the unary variable
388    String varname = var().name_using(format);
389
390    // Constructing the array that unary val will be compared against
391
392    String oneOfArray = "new long[] { ";
393
394    for (int i = 0 ; i < num_elts ; i++) {
395      if (i != 0) {
396        oneOfArray += ", ";
397      }
398      oneOfArray = oneOfArray + (((elts[i] == 0) && (var().file_rep_type == ProglangType.HASHCODE_ARRAY)) ? "null" : ((Integer.MIN_VALUE <= elts[i] && elts[i] <= Integer.MAX_VALUE) ? String.valueOf(elts[i]) : (String.valueOf(elts[i]) + "L")));
399    }
400    oneOfArray += " }";
401
402    // Calling quantification method
403    if (num_elts == 1) {
404
405      if (is_boolean()) {
406        result = "daikon.Quant.eltsEqual(" + varname + ", "
407          + ((elts[0] == 0) ? "false" : "true") + ")";
408      } else if (is_hashcode()) {
409        result =
410          ((elts[0] == 0)
411           ? ("daikon.Quant.eltsEqual(" + varname + ", null)")
412           : ("daikon.Quant.eltsNotEqual(" + varname + ", null)"));
413      } else {
414          result = "daikon.Quant.eltsEqual(" + varname + ", "
415            + (((elts[0] == 0) && (var().file_rep_type == ProglangType.HASHCODE_ARRAY)) ? "null" : ((Integer.MIN_VALUE <= elts[0] && elts[0] <= Integer.MAX_VALUE) ? String.valueOf(elts[0]) : (String.valueOf(elts[0]) + "L"))) + ")";
416        }
417    } else {
418      assert num_elts > 1;
419      // eltsOneOf == subsetOf
420      result = "daikon.Quant.subsetOf(" + varname + ", " + oneOfArray + ")";
421    }
422
423    return result;
424  }
425
426  public String format_simplify(@GuardSatisfied EltOneOf this) {
427
428    // if (is_hashcode() && dkconfig_omit_hashcode_values_Simplify)
429    //   return "(AND)";
430
431    sort_rep();
432
433    String[] form = VarInfo.simplify_quantify(var());
434    String varname = form[1];
435
436    String result;
437
438    if (is_boolean()) {
439      assert num_elts == 1;
440      assert (elts[0] == 0) || (elts[0] == 1);
441      result = "(EQ " + varname + " " + ((elts[0] == 0) ? "|@false|" : "|@true|") + ")";
442    } else if (is_hashcode()) {
443      if (num_elts == 1) {
444        long hashcode_val = get_hashcode_val(elts[0]);
445        result = "(EQ " + varname + " "
446          + ((elts[0] == 0) ? "null" :
447           ("(hashcode " + simplify_format_long(hashcode_val) + ")")) + ")";
448      } else if (num_elts == 2) {
449        // add_modified allows two elements iff one is null
450        assert elts[0] == 0;
451        assert elts[1] != 0;
452        long hashcode_val = get_hashcode_val(elts[1]);
453        result = "(OR (EQ " + varname + " null) (EQ " + varname
454          + "(hashcode " + simplify_format_long(hashcode_val) + ")))";
455      } else if (num_elts == 0) {
456        return format_too_few_samples(OutputFormat.SIMPLIFY, null);
457      } else {
458        throw new Error("Contains more than 2 elements");
459      }
460    } else {
461      result = "";
462      for (int i = 0; i < num_elts; i++) {
463        result += " (EQ " + varname + " " + (((elts[i] == 0) && (var().file_rep_type == ProglangType.HASHCODE_ARRAY)) ? "null" : simplify_format_long(elts[i])) + ")";
464      }
465      if (num_elts > 1) {
466        result = "(OR" + result + ")";
467      } else if (num_elts == 1) {
468        // chop leading space
469        result = result.substring(1);
470      } else {
471        // Haven't actually seen any data, so we're vacuously true
472        return format_too_few_samples(OutputFormat.SIMPLIFY, null);
473      }
474    }
475
476    result = form[0] + result + form[2];
477
478    if (result.indexOf("format_simplify") == -1) {
479      daikon.simplify.SimpUtil.assert_well_formed(result);
480    }
481    return result;
482  }
483
484  @Override
485  public InvariantStatus add_modified(long[] a, int count) {
486    return runValue(a, count, true);
487  }
488
489  @Override
490  public InvariantStatus check_modified(long[] a, int count) {
491    return runValue(a, count, false);
492  }
493
494  private InvariantStatus runValue(long[] a, int count, boolean mutate) {
495    InvariantStatus finalStatus = InvariantStatus.NO_CHANGE;
496    for (int ai = 0; ai <a.length; ai++) {
497      InvariantStatus status;
498      if (mutate) {
499        status = add_mod_elem(a[ai], count);
500      } else {
501        status = check_mod_elem(a[ai], count);
502      }
503      if (status == InvariantStatus.FALSIFIED) {
504        return InvariantStatus.FALSIFIED;
505      } else if (status == InvariantStatus.WEAKENED) {
506        finalStatus = InvariantStatus.WEAKENED;
507      }
508    }
509    return finalStatus;
510  }
511
512  /**
513   * Adds a single sample to the invariant. Returns
514   * the appropriate InvariantStatus from the result
515   * of adding the sample to this.
516   */
517  public InvariantStatus add_mod_elem(long v, int count) {
518    InvariantStatus status = check_mod_elem(v, count);
519    if (status == InvariantStatus.WEAKENED) {
520      elts[num_elts] = v;
521      num_elts++;
522    }
523    return status;
524  }
525
526  /**
527   * Checks a single sample to the invariant. Returns
528   * the appropriate InvariantStatus from the result
529   * of adding the sample to this.
530   */
531  public InvariantStatus check_mod_elem(long v, int count) {
532
533    // Look for v in our list of previously seen values.  If it's
534    // found, we're all set.
535    for (int i = 0; i < num_elts; i++) {
536      // if (logDetail())
537      //  log ("add_modified (" + v + ")");
538      if (((elts[i]) == ( v))) {
539        return InvariantStatus.NO_CHANGE;
540      }
541    }
542
543    if (num_elts == dkconfig_size) {
544      return InvariantStatus.FALSIFIED;
545    }
546
547    if ((is_boolean() && (num_elts == 1)) || (is_hashcode() && (num_elts == 2))) {
548      return InvariantStatus.FALSIFIED;
549    }
550
551    if (is_hashcode() && (num_elts == 1)) {
552      // Permit two object values only if one of them is null
553      if ((elts[0] != 0) && (v != 0)) {
554        return InvariantStatus.FALSIFIED;
555      }
556    }
557
558    return InvariantStatus.WEAKENED;
559  }
560
561  // It is possible to have seen many (array) samples, but no (long)
562  // array element values.
563  @Override
564  public boolean enoughSamples(@GuardSatisfied EltOneOf this) {
565    return num_elts > 0;
566  }
567
568  @Override
569  protected double computeConfidence() {
570    // This is not ideal.
571    if (num_elts == 0) {
572      return Invariant.CONFIDENCE_UNJUSTIFIED;
573    } else if (is_hashcode() && (num_elts > 1)) {
574      // This should never happen
575      return Invariant.CONFIDENCE_UNJUSTIFIED;
576    } else {
577      return Invariant.CONFIDENCE_JUSTIFIED;
578    }
579  }
580
581  @Pure
582  @Override
583  public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) {
584    // Static constants are necessarily OneOf precisely one value.
585    // This removes static constants from the output, which might not be
586    // desirable if the user doesn't know their actual value.
587    if (vis[0].isStaticConstant()) {
588      assert num_elts <= 1;
589      return new DiscardInfo(this, DiscardCode.obvious, vis[0].name() + " is a static constant.");
590    }
591    return super.isObviousStatically(vis);
592  }
593
594  @Pure
595  @Override
596  public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) {
597    DiscardInfo super_result = super.isObviousDynamically(vis);
598    if (super_result != null) {
599      return super_result;
600    }
601
602    VarInfo v = vis[0];
603
604    // We can check if all values in the list match with the ones we know about
605    // (useful for booleans and numeric enumerations).
606    if (v.aux.hasValue(VarInfoAux.VALID_VALUES)) {
607      String[] vsValidValues         = v.aux.getList(VarInfoAux.VALID_VALUES);
608      Set<Long> setValidValues = new TreeSet<>();
609      for (String s : vsValidValues) {
610        setValidValues.add(Long.valueOf(s));
611      }
612      Set<Long> setValuesInvariant = new TreeSet<>();
613      for (long e : elts) {
614        setValuesInvariant.add(e);
615      }
616      if (setValidValues.equals(setValuesInvariant)) {
617        return new DiscardInfo(this, DiscardCode.obvious,
618          "The value list matches the allowed value list");
619      }
620    }
621
622    // Look for the same property over a supersequence of this one.
623    PptTopLevel pptt = ppt.parent;
624    for (Iterator<Invariant> inv_itor = pptt.invariants_iterator(); inv_itor.hasNext(); ) {
625      Invariant inv = inv_itor.next();
626      if (inv == this) {
627        continue;
628      }
629      if (inv instanceof EltOneOf) {
630        EltOneOf other = (EltOneOf) inv;
631        if (isSameFormula(other)
632          && SubSequence.isObviousSubSequenceDynamically(this, v, other.var())) {
633          debug.fine("isObviousDyn: Returning true because isObviousSubSequenceDynamically");
634          return new DiscardInfo(this, DiscardCode.obvious, "The same property holds over a supersequence " + other.var().name());
635        }
636      }
637    }
638
639    return null;
640  }
641
642  /**
643   * Oneof can merge different formulas from lower points to create a single formula at an upper
644   * point.
645   */
646  @Override
647  public boolean mergeFormulasOk() {
648    return true;
649  }
650
651  @Pure
652  @Override
653  public boolean isSameFormula(Invariant o) {
654    EltOneOf other = (EltOneOf) o;
655    if (num_elts != other.num_elts) {
656      return false;
657    }
658    if (num_elts == 0 && other.num_elts == 0) {
659      return true;
660    }
661
662    sort_rep();
663    other.sort_rep();
664
665    // All nonzero hashcode values should be considered equal to each other
666    //
667    // Examples:
668    // inv1  inv2  result
669    // ----  ----  ------
670    // 19    0     false
671    // 19    22    true
672    // 0     0     true
673
674    if (is_hashcode() && other.is_hashcode()) {
675      if (num_elts == 1 && other.num_elts == 1) {
676        return ((elts[0] == 0 && other.elts[0] == 0)
677                || (elts[0] != 0 && other.elts[0] != 0));
678      } else if (num_elts == 2 && other.num_elts == 2) {
679        // add_modified allows two elements iff one is null
680        assert elts[0] == 0;
681        assert other.elts[0] == 0;
682        assert elts[1] != 0;
683        assert other.elts[1] != 0;
684
685        // Since we know the first elements of each invariant are
686        // zero, and the second elements are nonzero, we can immediately
687        // return true
688        return true;
689      } else {
690        return false;
691      }
692    }
693
694    for (int i = 0; i < num_elts; i++) {
695      if (!((elts[i]) == (other.elts[i]))) {
696        return false;
697      }
698    }
699
700    return true;
701  }
702
703  @Pure
704  @Override
705  public boolean isExclusiveFormula(Invariant o) {
706    if (o instanceof EltOneOf) {
707      EltOneOf other = (EltOneOf) o;
708
709      if (num_elts == 0 || other.num_elts == 0) {
710        return false;
711      }
712      for (int i = 0; i < num_elts; i++) {
713        for (int j = 0; j < other.num_elts; j++) {
714          if (((elts[i]) == (other.elts[j]))) // elements are interned
715            return false;
716        }
717      }
718
719      // Don't consider two instances of "non-null" as exclusive.
720      if (is_hashcode() && num_elts == 1
721          && other.is_hashcode() && other.num_elts == 1
722          && elts[0] != 0 && other.elts[0] != 0) {
723        return false;
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    // Many more checks can be added here:  against nonzero, modulus, etc.
740    if ((o instanceof EltNonZero) && (num_elts == 1) && (elts[0] == 0)) {
741      return true;
742    }
743    long elts_min = Long.MAX_VALUE;
744    long elts_max = Long.MIN_VALUE;
745    for (int i = 0; i < num_elts; i++) {
746      elts_min = Math.min(elts_min, elts[i]);
747      elts_max = Math.max(elts_max, elts[i]);
748    }
749    if ((o instanceof LowerBound) && (elts_max < ((LowerBound)o).min())) {
750      return true;
751    }
752    if ((o instanceof UpperBound) && (elts_min > ((UpperBound)o).max())) {
753      return true;
754    }
755
756    return false;
757  }
758
759  @Override
760  public boolean hasUninterestingConstant() {
761
762    for (int i = 0; i < num_elts; i++) {
763      if (elts[i] < -1 || elts[i] > 2) {
764        return true;
765      }
766    }
767
768    return false;
769  }
770
771  @Pure
772  @Override
773  public boolean isExact() {
774    return num_elts == 1;
775  }
776
777  // Look up a previously instantiated invariant.
778  public static @Nullable EltOneOf find(PptSlice ppt) {
779    assert ppt.arity() == 1;
780    for (Invariant inv : ppt.invs) {
781      if (inv instanceof EltOneOf) {
782        return (EltOneOf) inv;
783      }
784    }
785    return null;
786  }
787
788  // Interning is lost when an object is serialized and deserialized.
789  // Manually re-intern any interned fields upon deserialization.
790  private void readObject(ObjectInputStream in) throws IOException,
791    ClassNotFoundException {
792    in.defaultReadObject();
793
794    for (int i = 0; i < num_elts; i++) {
795      elts[i] = Intern.intern(elts[i]);
796    }
797  }
798
799  /**
800   * Merge the invariants in invs to form a new invariant. Each must be a EltOneOf invariant.
801   * This code finds all of the oneof values from each of the invariants and returns the merged
802   * invariant (if any).
803   *
804   * @param invs list of invariants to merge. The invariants must all be of the same type and should
805   *     come from the children of parent_ppt. They should also all be permuted to match the
806   *     variable order in parent_ppt.
807   * @param parent_ppt slice that will contain the new invariant
808   */
809  @Override
810  public @Nullable EltOneOf merge(List<Invariant> invs, PptSlice parent_ppt) {
811
812    // Create the initial parent invariant from the first child
813    EltOneOf  first = (EltOneOf) invs.get(0);
814    EltOneOf result = first.clone();
815    result.ppt = parent_ppt;
816
817    // Loop through the rest of the child invariants
818    for (int i = 1; i < invs.size(); i++ ) {
819
820      // Get this invariant
821      EltOneOf inv = (EltOneOf) invs.get(i);
822
823      // Loop through each distinct value found in this child and add
824      // it to the parent.  If the invariant is falsified, there is no parent
825      // invariant
826      for (int j = 0; j < inv.num_elts; j++) {
827        long val = inv.elts[j];
828
829        InvariantStatus status = result.add_mod_elem(val, 1);
830        if (status == InvariantStatus.FALSIFIED) {
831
832          result.log("%s", "child value '" + val + "' destroyed oneof");
833
834          return null;
835        }
836      }
837    }
838
839    result.log("Merged '%s' from %s child invariants", result.format(), invs.size());
840    return result;
841  }
842
843  /**
844   * Setup the invariant with the specified elements. Normally used when searching for a specified
845   * OneOf. The elements of vals are not necessarily interned; this method interns each element.
846   */
847  public void set_one_of_val(long[] vals) {
848
849    num_elts = vals.length;
850    for (int i = 0; i < num_elts; i++) {
851      elts[i] = Intern.intern(vals[i]);
852    }
853  }
854
855  /**
856   * Returns true if every element in this invariant is contained in the specified state. For
857   * example if x = 1 and the state contains 1 and 2, true will be returned.
858   */
859  @Override
860  public boolean state_match(Object state) {
861
862    if (num_elts == 0) {
863      return false;
864    }
865
866    if (!(state instanceof long[])) {
867      // Daikon is about to crash.  Produce some debugging output.
868      System.out.printf("state = %s [%s]%n", state, state.getClass());
869      System.out.printf("problem with %s%n", this);
870    }
871    long[] e = (long[]) state;
872    for (int i = 0; i < num_elts; i++) {
873      boolean match = false;
874      for (int j = 0; j < e.length; j++) {
875        if (elts[i] == e[j]) {
876          match = true;
877          break;
878        }
879      }
880      if (!match) {
881        return false;
882      }
883    }
884    return true;
885  }
886
887  /**
888   * Map that holds dummy hashcode values for hashcodes. Each hashcode seen is assigned a small
889   * integer in the order they are seen. These values will be consistent as long as new hashcodes do
890   * not appear in the output. Not a perfect fix for regressions consistency, but workable.
891   */
892  private static Map<Long,Long> dummy_hashcode_vals = new LinkedHashMap<>();
893  private static long next_dummy_hashcode = 1001;
894
895  private long get_hashcode_val(@GuardSatisfied EltOneOf this, long hashcode) {
896    if (!dkconfig_omit_hashcode_values_Simplify) {
897      return hashcode;
898    }
899
900    Long val = dummy_hashcode_vals.get(hashcode);
901    if (val != null) {
902      return val;
903    }
904    dummy_hashcode_vals.put(hashcode, next_dummy_hashcode);
905    return next_dummy_hashcode++;
906  }
907
908}