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