Source code

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