Source code

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