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