Source code

001// ***** This file is automatically generated from OneOf.java.jpp
002
003package daikon.inv.unary.sequence;
004
005import daikon.*;
006import daikon.inv.*;
007import daikon.inv.unary.OneOf;
008
009  import daikon.inv.binary.twoSequence.SubSequence;
010  import daikon.inv.unary.scalar.*;
011
012import java.io.*;
013import java.util.logging.Logger;
014import java.util.logging.Level;
015import java.util.*;
016
017import org.checkerframework.checker.initialization.qual.Initialized;
018import org.checkerframework.checker.interning.qual.Interned;
019import org.checkerframework.checker.lock.qual.GuardSatisfied;
020import org.checkerframework.checker.nullness.qual.NonNull;
021import org.checkerframework.checker.nullness.qual.Nullable;
022import org.checkerframework.dataflow.qual.Pure;
023import org.checkerframework.dataflow.qual.SideEffectFree;
024import org.checkerframework.framework.qual.Unused;
025import daikon.SignaturesUtil;
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 sequences of double values where the elements of the sequence take on only a
040   * few distinct values. Prints as either {@code x[] elements == c} (when there is only one value),
041   * or as {@code x[] elements one of {c1, c2, c3}} (when there are multiple values).
042
043   */
044
045@SuppressWarnings("UnnecessaryParentheses")  // generated code, parentheses are sometimes needed
046public final class EltOneOfFloat extends SingleFloatSequence implements OneOf {
047  static final long serialVersionUID = 20030822L;
048
049  /** Debugging logger. */
050  public static final Logger debug =
051    Logger.getLogger(EltOneOfFloat.class.getName());
052
053  // Variables starting with dkconfig_ should only be set via the
054  // daikon.config.Configuration interface.
055  /** Boolean. True iff OneOf invariants should be considered. */
056  public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault;
057
058  /**
059   * Positive integer. Specifies the maximum set size for this type of invariant (x is one of
060   * {@code size} items).
061   */
062
063  public static int dkconfig_size = 3;
064
065  // Probably needs to keep its own list of the values, and number of each seen.
066  // (That depends on the slice; maybe not until the slice is cleared out.
067  // But so few values is cheap, so this is quite fine for now and long-term.)
068
069  @Unused(when=Prototype.class)
070  private double[] elts;
071  @Unused(when=Prototype.class)
072  private int num_elts;
073
074  @Prototype EltOneOfFloat() {
075    super();
076  }
077
078  EltOneOfFloat(PptSlice slice) {
079    super(slice);
080
081    elts = new double[dkconfig_size];
082
083    num_elts = 0;
084
085    // var() is initialized by the super constructor
086    assert var().is_array() :
087      String.format("In %s constructor, var %s (type=%s, rep_type=%s) should be an array",
088                     "EltOneOfFloat", var().name(), var().type, var().rep_type);
089
090  }
091
092  private static @Prototype EltOneOfFloat proto = new @Prototype EltOneOfFloat();
093
094  /** Returns the prototype invariant for EltOneOfFloat */
095  public static @Prototype EltOneOfFloat get_proto() {
096    return proto;
097  }
098
099  @Override
100  public boolean enabled() {
101    return dkconfig_enabled;
102  }
103
104  @Override
105  public EltOneOfFloat instantiate_dyn(@Prototype EltOneOfFloat this, PptSlice slice) {
106    return new EltOneOfFloat(slice);
107  }
108
109  @Pure
110  public boolean is_boolean(@GuardSatisfied EltOneOfFloat this) {
111    return var().file_rep_type.elementType() == ProglangType.BOOLEAN;
112  }
113  @Pure
114  public boolean is_hashcode(@GuardSatisfied EltOneOfFloat this) {
115    return var().file_rep_type.elementType() == ProglangType.HASHCODE;
116  }
117
118  @SideEffectFree
119  @Override
120  public EltOneOfFloat clone(@GuardSatisfied EltOneOfFloat this) {
121    EltOneOfFloat result = (EltOneOfFloat) super.clone();
122    result.elts = elts.clone();
123
124    result.num_elts = this.num_elts;
125    return result;
126  }
127
128  @Override
129  public int num_elts() {
130    return num_elts;
131  }
132
133  @Override
134  public Object elt() {
135    return elt(0);
136  }
137
138  public Object elt(int index) {
139    if (num_elts <= index) {
140      throw new Error("Represents " + num_elts + " elements, index " + index + " not valid");
141    }
142
143    return Intern.internedDouble(elts[index]);
144  }
145
146  private void sort_rep(@GuardSatisfied EltOneOfFloat this) {
147    Arrays.sort(elts, 0, num_elts );
148  }
149
150  public double min_elt() {
151    if (num_elts == 0) {
152      throw new Error("Represents no elements");
153    }
154    sort_rep();
155    return elts[0];
156  }
157
158  public double max_elt() {
159    if (num_elts == 0) {
160      throw new Error("Represents no elements");
161    }
162    sort_rep();
163    return elts[num_elts - 1];
164  }
165
166  // Assumes the other array is already sorted
167  public boolean compare_rep(int num_other_elts, double[] other_elts) {
168    if (num_elts != num_other_elts) {
169      return false;
170    }
171    sort_rep();
172    for (int i = 0; i < num_elts; i++) {
173      if (!(Global.fuzzy.eq(elts[i], other_elts[i]) || (Double.isNaN(elts[i]) && Double.isNaN(other_elts[i])))) { // elements are interned
174        return false;
175      }
176    }
177    return true;
178  }
179
180  private String subarray_rep(@GuardSatisfied EltOneOfFloat this) {
181    // Not so efficient an implementation, but simple;
182    // and how often will we need to print this anyway?
183    sort_rep();
184    StringJoiner sj = new StringJoiner(", ", "{ ", " }");
185    for (int i = 0; i < num_elts; i++) {
186
187      if (PrintInvariants.dkconfig_static_const_infer) {
188        boolean curVarMatch = false;
189        PptTopLevel pptt = ppt.parent;
190        for (VarInfo vi : pptt.var_infos) {
191          if (vi.isStaticConstant() && VarComparability.comparable(vi, var())) {
192            // If variable is a double, then use fuzzy comparison
193            if (vi.rep_type == ProglangType.DOUBLE) {
194              Double constantVal = (Double)vi.constantValue();
195              if (Global.fuzzy.eq(constantVal, elts[i]) || (Double.isNaN(constantVal) && Double.isNaN(elts[i]))) {
196                sj.add(vi.name());
197                curVarMatch = true;
198              }
199            }
200            // Otherwise just use the equals method
201            else {
202              Object constantVal = vi.constantValue();
203              if (constantVal.equals(elts[i])) {
204                sj.add(vi.name());
205                curVarMatch = true;
206              }
207            }
208          }
209        }
210
211        if (curVarMatch == false) {
212          sj.add((Double.isNaN(elts[i]) ? "Double.NaN" : String.valueOf(elts[i])));
213        }
214      } else {
215        sj.add((Double.isNaN(elts[i]) ? "Double.NaN" : String.valueOf(elts[i])));
216      }
217
218    }
219    return sj.toString();
220  }
221
222  @Override
223  public String repr(@GuardSatisfied EltOneOfFloat this) {
224    return "EltOneOfFloat" + varNames() + ": falsified=" + falsified
225      + ", num_elts=" + num_elts
226      + ", elts=" + subarray_rep();
227  }
228
229  @SideEffectFree
230  @Override
231  public String format_using(@GuardSatisfied EltOneOfFloat this, OutputFormat format) {
232    sort_rep();
233
234    if (format.isJavaFamily()) {
235      return format_java_family(format);
236    }
237
238    if (format == OutputFormat.DAIKON) {
239      return format_daikon();
240    } else if (format == OutputFormat.SIMPLIFY) {
241      return format_simplify();
242    } else if (format == OutputFormat.ESCJAVA) {
243      String result = format_esc();
244      return result;
245    } else if (format == OutputFormat.CSHARPCONTRACT) {
246      return format_csharp_contract();
247    } else {
248      return format_unimplemented(format);
249    }
250  }
251
252  public String format_daikon(@GuardSatisfied EltOneOfFloat this) {
253    String varname = var().name() + " elements";
254    if (num_elts == 1) {
255
256        if (PrintInvariants.dkconfig_static_const_infer) {
257          PptTopLevel pptt = ppt.parent;
258          for (VarInfo vi : pptt.var_infos) {
259            if (vi.isStaticConstant() && VarComparability.comparable(vi, var())) {
260              if (vi.rep_type == ProglangType.DOUBLE) {
261                Double constantVal = (Double)vi.constantValue();
262                if (Global.fuzzy.eq(constantVal, elts[0]) || (Double.isNaN(constantVal) && Double.isNaN(elts[0]))) {
263                  return varname + " == " + vi.name();
264                }
265              } else {
266                Object constantVal = vi.constantValue();
267                if (constantVal.equals(elts[0])) {
268                  return varname + " == " + vi.name();
269                }
270              }
271            }
272          }
273        }
274        return varname + " == " + (Double.isNaN(elts[0]) ? "Double.NaN" : String.valueOf(elts[0]));
275    } else {
276      return varname + " one of " + subarray_rep();
277    }
278  }
279
280  public String format_esc(@GuardSatisfied EltOneOfFloat this) {
281    sort_rep();
282
283    String[] form = VarInfo.esc_quantify(var());
284    String varname = form[1];
285
286    String result;
287
288    {
289      result = "";
290      for (int i = 0; i < num_elts; i++) {
291        if (i != 0) { result += " || "; }
292        result += varname + " == " + (Double.isNaN(elts[i]) ? "Double.NaN" : String.valueOf(elts[i]));
293      }
294    }
295
296    result = form[0] + "(" + result + ")" + form[2];
297
298    return result;
299  }
300
301public String format_csharp_contract(@GuardSatisfied EltOneOfFloat this) {
302
303    @NonNull @Initialized String result;
304
305    String equalsString = " == ";
306    String endString = "";
307
308    String[] split = var().csharp_array_split();
309    List<String> args_list = new ArrayList<>();
310    // Construct the array that unary value will be compared against.
311    for (int i = 0; i < num_elts; i++) {
312
313      args_list.add((Double.isNaN(elts[i]) ? "Double.NaN" : String.valueOf(elts[i])));
314
315    }
316    String args = String.join(", ", args_list);
317
318    if (num_elts == 0) { // If there are no elements, length must be 0.
319      String varname = var().csharp_name();
320      return varname + ".Count() == 0";
321    } else if (num_elts == 1) {
322
323      {
324        result = "Contract.ForAll(" + split[0] + ", x => x" + split[1] + equalsString + args + endString + ")";
325      }
326    } else {
327      assert num_elts > 1;
328      result = "Contract.ForAll(" + split[0] + ", x => x" + split[1] + ".OneOf(" + args + "))";
329    }
330
331    return result;
332  }
333
334  public String format_java_family(@GuardSatisfied EltOneOfFloat this, OutputFormat format) {
335
336    String result;
337
338    // Setting up the name of the unary variable
339    String varname = var().name_using(format);
340
341    // Constructing the array that unary val will be compared against
342
343    String oneOfArray = "new double[] { ";
344
345    for (int i = 0 ; i < num_elts ; i++) {
346      if (i != 0) {
347        oneOfArray += ", ";
348      }
349      oneOfArray = oneOfArray + (Double.isNaN(elts[i]) ? "Double.NaN" : String.valueOf(elts[i]));
350    }
351    oneOfArray += " }";
352
353    // Calling quantification method
354    if (num_elts == 1) {
355
356        {
357          result = "daikon.Quant.eltsEqual(" + varname + ", "
358            + (Double.isNaN(elts[0]) ? "Double.NaN" : String.valueOf(elts[0])) + ")";
359        }
360    } else {
361      assert num_elts > 1;
362      // eltsOneOf == subsetOf
363      result = "daikon.Quant.subsetOf(" + varname + ", " + oneOfArray + ")";
364    }
365
366    return result;
367  }
368
369  public String format_simplify(@GuardSatisfied EltOneOfFloat this) {
370
371    sort_rep();
372
373    String[] form = VarInfo.simplify_quantify(var());
374    String varname = form[1];
375
376    String result;
377
378    {
379      result = "";
380      for (int i = 0; i < num_elts; i++) {
381        result += " (EQ " + varname + " " + simplify_format_double(elts[i]) + ")";
382      }
383      if (num_elts > 1) {
384        result = "(OR" + result + ")";
385      } else if (num_elts == 1) {
386        // chop leading space
387        result = result.substring(1);
388      } else {
389        // Haven't actually seen any data, so we're vacuously true
390        return format_too_few_samples(OutputFormat.SIMPLIFY, null);
391      }
392    }
393
394    result = form[0] + result + form[2];
395
396    if (result.indexOf("format_simplify") == -1) {
397      daikon.simplify.SimpUtil.assert_well_formed(result);
398    }
399    return result;
400  }
401
402  @Override
403  public InvariantStatus add_modified(double[] a, int count) {
404    return runValue(a, count, true);
405  }
406
407  @Override
408  public InvariantStatus check_modified(double[] a, int count) {
409    return runValue(a, count, false);
410  }
411
412  private InvariantStatus runValue(double[] a, int count, boolean mutate) {
413    InvariantStatus finalStatus = InvariantStatus.NO_CHANGE;
414    for (int ai = 0; ai <a.length; ai++) {
415      InvariantStatus status;
416      if (mutate) {
417        status = add_mod_elem(a[ai], count);
418      } else {
419        status = check_mod_elem(a[ai], count);
420      }
421      if (status == InvariantStatus.FALSIFIED) {
422        return InvariantStatus.FALSIFIED;
423      } else if (status == InvariantStatus.WEAKENED) {
424        finalStatus = InvariantStatus.WEAKENED;
425      }
426    }
427    return finalStatus;
428  }
429
430  /**
431   * Adds a single sample to the invariant. Returns
432   * the appropriate InvariantStatus from the result
433   * of adding the sample to this.
434   */
435  public InvariantStatus add_mod_elem(double v, int count) {
436    InvariantStatus status = check_mod_elem(v, count);
437    if (status == InvariantStatus.WEAKENED) {
438      elts[num_elts] = v;
439      num_elts++;
440    }
441    return status;
442  }
443
444  /**
445   * Checks 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 check_mod_elem(double v, int count) {
450
451    // Look for v in our list of previously seen values.  If it's
452    // found, we're all set.
453    for (int i = 0; i < num_elts; i++) {
454      // if (logDetail())
455      //  log ("add_modified (" + v + ")");
456      if ((Global.fuzzy.eq(elts[i], v) || (Double.isNaN(elts[i]) && Double.isNaN( v)))) {
457        return InvariantStatus.NO_CHANGE;
458      }
459    }
460
461    if (num_elts == dkconfig_size) {
462      return InvariantStatus.FALSIFIED;
463    }
464
465    return InvariantStatus.WEAKENED;
466  }
467
468  // It is possible to have seen many (array) samples, but no (double)
469  // array element values.
470  @Override
471  public boolean enoughSamples(@GuardSatisfied EltOneOfFloat this) {
472    return num_elts > 0;
473  }
474
475  @Override
476  protected double computeConfidence() {
477    // This is not ideal.
478    if (num_elts == 0) {
479      return Invariant.CONFIDENCE_UNJUSTIFIED;
480    } else {
481      return Invariant.CONFIDENCE_JUSTIFIED;
482    }
483  }
484
485  @Pure
486  @Override
487  public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) {
488    // Static constants are necessarily OneOf precisely one value.
489    // This removes static constants from the output, which might not be
490    // desirable if the user doesn't know their actual value.
491    if (vis[0].isStaticConstant()) {
492      assert num_elts <= 1;
493      return new DiscardInfo(this, DiscardCode.obvious, vis[0].name() + " is a static constant.");
494    }
495    return super.isObviousStatically(vis);
496  }
497
498  @Pure
499  @Override
500  public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) {
501    DiscardInfo super_result = super.isObviousDynamically(vis);
502    if (super_result != null) {
503      return super_result;
504    }
505
506    VarInfo v = vis[0];
507
508    // We can check if all values in the list match with the ones we know about
509    // (useful for booleans and numeric enumerations).
510    if (v.aux.hasValue(VarInfoAux.VALID_VALUES)) {
511      String[] vsValidValues         = v.aux.getList(VarInfoAux.VALID_VALUES);
512      Set<Double> setValidValues = new TreeSet<>();
513      for (String s : vsValidValues) {
514        setValidValues.add(Double.valueOf(s));
515      }
516      Set<Double> setValuesInvariant = new TreeSet<>();
517      for (double e : elts) {
518        setValuesInvariant.add(e);
519      }
520      if (setValidValues.equals(setValuesInvariant)) {
521        return new DiscardInfo(this, DiscardCode.obvious,
522          "The value list matches the allowed value list");
523      }
524    }
525
526    // Look for the same property over a supersequence of this one.
527    PptTopLevel pptt = ppt.parent;
528    for (Iterator<Invariant> inv_itor = pptt.invariants_iterator(); inv_itor.hasNext(); ) {
529      Invariant inv = inv_itor.next();
530      if (inv == this) {
531        continue;
532      }
533      if (inv instanceof EltOneOfFloat) {
534        EltOneOfFloat other = (EltOneOfFloat) inv;
535        if (isSameFormula(other)
536          && SubSequence.isObviousSubSequenceDynamically(this, v, other.var())) {
537          debug.fine("isObviousDyn: Returning true because isObviousSubSequenceDynamically");
538          return new DiscardInfo(this, DiscardCode.obvious, "The same property holds over a supersequence " + other.var().name());
539        }
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    EltOneOfFloat other = (EltOneOfFloat) 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 (!(Global.fuzzy.eq(elts[i], other.elts[i]) || (Double.isNaN(elts[i]) && Double.isNaN(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 EltOneOfFloat) {
582      EltOneOfFloat other = (EltOneOfFloat) 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 ((Global.fuzzy.eq(elts[i], other.elts[j]) || (Double.isNaN(elts[i]) && Double.isNaN(other.elts[j])))) // elements are interned
590            return false;
591        }
592      }
593
594      return true;
595    }
596
597    // Many more checks can be added here:  against nonzero, modulus, etc.
598    if ((o instanceof EltNonZeroFloat) && (num_elts == 1) && (elts[0] == 0)) {
599      return true;
600    }
601    double elts_min = Double.MAX_VALUE;
602    double elts_max = Double.MIN_VALUE;
603    for (int i = 0; i < num_elts; i++) {
604      elts_min = Math.min(elts_min, elts[i]);
605      elts_max = Math.max(elts_max, elts[i]);
606    }
607    if ((o instanceof LowerBoundFloat) && (elts_max < ((LowerBoundFloat)o).min())) {
608      return true;
609    }
610    if ((o instanceof UpperBoundFloat) && (elts_min > ((UpperBoundFloat)o).max())) {
611      return true;
612    }
613
614    return false;
615  }
616
617  @Override
618  public boolean hasUninterestingConstant() {
619
620    for (int i = 0; i < num_elts; i++) {
621      if (elts[i] < -1.0 || elts[i] > 2.0 || elts[i] != (long)elts[i]) {
622        return true;
623      }
624    }
625
626    return false;
627  }
628
629  @Pure
630  @Override
631  public boolean isExact() {
632    return num_elts == 1;
633  }
634
635  // Look up a previously instantiated invariant.
636  public static @Nullable EltOneOfFloat find(PptSlice ppt) {
637    assert ppt.arity() == 1;
638    for (Invariant inv : ppt.invs) {
639      if (inv instanceof EltOneOfFloat) {
640        return (EltOneOfFloat) inv;
641      }
642    }
643    return null;
644  }
645
646  // Interning is lost when an object is serialized and deserialized.
647  // Manually re-intern any interned fields upon deserialization.
648  private void readObject(ObjectInputStream in) throws IOException,
649    ClassNotFoundException {
650    in.defaultReadObject();
651
652    for (int i = 0; i < num_elts; i++) {
653      elts[i] = Intern.intern(elts[i]);
654    }
655  }
656
657  /**
658   * Merge the invariants in invs to form a new invariant. Each must be a EltOneOfFloat invariant.
659   * This code finds all of the oneof values from each of the invariants and returns the merged
660   * invariant (if any).
661   *
662   * @param invs list of invariants to merge. The invariants must all be of the same type and should
663   *     come from the children of parent_ppt. They should also all be permuted to match the
664   *     variable order in parent_ppt.
665   * @param parent_ppt slice that will contain the new invariant
666   */
667  @Override
668  public @Nullable EltOneOfFloat merge(List<Invariant> invs, PptSlice parent_ppt) {
669
670    // Create the initial parent invariant from the first child
671    EltOneOfFloat  first = (EltOneOfFloat) invs.get(0);
672    EltOneOfFloat result = first.clone();
673    result.ppt = parent_ppt;
674
675    // Loop through the rest of the child invariants
676    for (int i = 1; i < invs.size(); i++ ) {
677
678      // Get this invariant
679      EltOneOfFloat inv = (EltOneOfFloat) invs.get(i);
680
681      // Loop through each distinct value found in this child and add
682      // it to the parent.  If the invariant is falsified, there is no parent
683      // invariant
684      for (int j = 0; j < inv.num_elts; j++) {
685        double val = inv.elts[j];
686
687        InvariantStatus status = result.add_mod_elem(val, 1);
688        if (status == InvariantStatus.FALSIFIED) {
689
690          result.log("%s", "child value '" + val + "' destroyed oneof");
691
692          return null;
693        }
694      }
695    }
696
697    result.log("Merged '%s' from %s child invariants", result.format(), invs.size());
698    return result;
699  }
700
701  /**
702   * Setup the invariant with the specified elements. Normally used when searching for a specified
703   * OneOf. The elements of vals are not necessarily interned; this method interns each element.
704   */
705  public void set_one_of_val(double[] vals) {
706
707    num_elts = vals.length;
708    for (int i = 0; i < num_elts; i++) {
709      elts[i] = Intern.intern(vals[i]);
710    }
711  }
712
713  /**
714   * Returns true if every element in this invariant is contained in the specified state. For
715   * example if x = 1 and the state contains 1 and 2, true will be returned.
716   */
717  @Override
718  public boolean state_match(Object state) {
719
720    if (num_elts == 0) {
721      return false;
722    }
723
724    if (!(state instanceof double[])) {
725      // Daikon is about to crash.  Produce some debugging output.
726      System.out.printf("state = %s [%s]%n", state, state.getClass());
727      System.out.printf("problem with %s%n", this);
728    }
729    double[] e = (double[]) state;
730    for (int i = 0; i < num_elts; i++) {
731      boolean match = false;
732      for (int j = 0; j < e.length; j++) {
733        if (elts[i] == e[j]) {
734          match = true;
735          break;
736        }
737      }
738      if (!match) {
739        return false;
740      }
741    }
742    return true;
743  }
744
745}