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