Source code

001// ***** This file is automatically generated from EltwiseIntComparisons.java.jpp
002
003package daikon.inv.unary.sequence;
004
005import daikon.*;
006import daikon.Quantify.QuantFlags;
007import daikon.derive.*;
008import daikon.derive.binary.*;
009import daikon.inv.*;
010import java.util.*;
011import org.checkerframework.checker.interning.qual.Interned;
012import org.checkerframework.checker.lock.qual.GuardSatisfied;
013import org.checkerframework.checker.nullness.qual.Nullable;
014import org.checkerframework.dataflow.qual.Pure;
015import org.checkerframework.dataflow.qual.SideEffectFree;
016import org.plumelib.util.Intern;
017import typequals.prototype.qual.NonPrototype;
018import typequals.prototype.qual.Prototype;
019
020  /**
021   * Represents equality between adjacent elements (x[i], x[i+1]) of a double sequence. Prints as
022   * {@code x[] elements are equal}.
023   */
024
025public class EltwiseFloatEqual extends EltwiseFloatComparison {
026  // We are Serializable, so we specify a version to allow changes to
027  // method signatures without breaking serialization.  If you add or
028  // remove fields, you should change this number to the current date.
029  static final long serialVersionUID = 20030822L;
030
031  // Variables starting with dkconfig_ should only be set via the
032  // daikon.config.Configuration interface.
033  /** Boolean. True iff EltwiseIntComparison invariants should be considered. */
034  public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault;
035
036  static final boolean debugEltwiseIntComparison = false;
037
038  protected EltwiseFloatEqual(PptSlice ppt) {
039    super(ppt);
040  }
041
042  protected @Prototype EltwiseFloatEqual() {
043    super();
044  }
045
046  private static @Prototype EltwiseFloatEqual proto = new @Prototype EltwiseFloatEqual();
047
048  /** Returns the prototype invariant for EltwiseFloatEqual */
049  public static @Prototype EltwiseFloatEqual get_proto() {
050    return proto;
051  }
052
053  /** returns whether or not this invariant is enabled */
054  @Override
055  public boolean enabled() {
056    return dkconfig_enabled;
057  }
058
059  /** Non-equality EltwiseFloatEqual invariants are only valid on integral types. */
060  @Override
061  public boolean instantiate_ok(VarInfo[] vis) {
062
063    if (!valid_types(vis)) {
064      return false;
065    }
066
067    return true;
068  }
069
070  /** Instantiate the invariant on the specified slice. */
071  @Override
072  protected EltwiseFloatEqual instantiate_dyn(@Prototype EltwiseFloatEqual this, PptSlice slice) {
073    return new EltwiseFloatEqual(slice);
074  }
075
076  @SideEffectFree
077  @Override
078  public EltwiseFloatEqual clone(@GuardSatisfied EltwiseFloatEqual this) {
079    EltwiseFloatEqual result = (EltwiseFloatEqual) super.clone();
080    return result;
081  }
082
083  @Override
084  public String repr(@GuardSatisfied EltwiseFloatEqual this) {
085    return "EltwiseFloatEqual" + varNames() + ": falsified=" + falsified;
086  }
087
088  @SideEffectFree
089  @Override
090  public String format_using(@GuardSatisfied EltwiseFloatEqual this, OutputFormat format) {
091    if (format.isJavaFamily()) {
092      return format_java_family(format);
093    }
094
095    if (format == OutputFormat.DAIKON) {
096      return format_daikon();
097    }
098    if (format == OutputFormat.ESCJAVA) {
099      return format_esc();
100    }
101    if (format == OutputFormat.CSHARPCONTRACT) {
102      return format_csharp_contract();
103    }
104    if (format == OutputFormat.SIMPLIFY) {
105      return format_simplify();
106    }
107
108    return format_unimplemented(format);
109  }
110
111  public String format_daikon(@GuardSatisfied EltwiseFloatEqual this) {
112    if (debugEltwiseIntComparison) {
113      System.out.println(repr());
114    }
115
116    return var().name() + " sorted by ==";
117  }
118
119  public String format_esc(@GuardSatisfied EltwiseFloatEqual this) {
120    String[] form = VarInfo.esc_quantify(false, var(), var());
121
122      return form[0] + "(" + form[1] + " == " + form[2] + ")" + form[3];
123  }
124
125  public String format_java_family(@GuardSatisfied EltwiseFloatEqual this, OutputFormat format) {
126    return "daikon.Quant.eltwiseEqual(" + var().name_using(format) + ")";
127  }
128
129  public String format_csharp_contract(@GuardSatisfied EltwiseFloatEqual this) {
130    String[] split = var().csharp_array_split();
131    return "Contract.ForAll(0, " + split[0] + ".Count()-1, i => " + split[0] + "[i]" + split[1] + " == " + split[0] + "[i+1]" + split[1] + ")";
132  }
133
134  public String format_simplify(@GuardSatisfied EltwiseFloatEqual this) {
135    String[] form = VarInfo.simplify_quantify(QuantFlags.adjacent(),
136                                               var(), var());
137
138    String comparator = "EQ";
139
140    return form[0] + "(" + comparator + " " + form[1] + " " + form[2] + ")"
141      + form[3];
142  }
143
144  @Override
145  @SuppressWarnings("UnnecessaryParentheses")  // generated code, parentheses are sometimes needed
146  public InvariantStatus check_modified(double @Interned [] a, int count) {
147    for (int i = 1; i < a.length; i++) {
148      if (!Global.fuzzy.eq(a[i - 1], a[i])) {
149        return InvariantStatus.FALSIFIED;
150      }
151    }
152    return InvariantStatus.NO_CHANGE;
153  }
154
155  @Override
156  public InvariantStatus add_modified(double @Interned [] a, int count) {
157    return check_modified(a, count);
158  }
159
160  // Perhaps check whether all the arrays of interest have length 0 or 1.
161
162  @Override
163  protected double computeConfidence() {
164
165    if (ppt.num_samples() != 0) {
166      return Invariant.CONFIDENCE_JUSTIFIED;
167    } else {
168      return Invariant.CONFIDENCE_UNJUSTIFIED;
169    }
170
171  }
172
173  @Pure
174  @Override
175  public boolean isExact() {
176
177    return true;
178  }
179
180  @Pure
181  @Override
182  public boolean isSameFormula(Invariant other) {
183    return (other instanceof EltwiseFloatEqual);
184  }
185
186  // Not pretty... is there another way?
187  // Also, reasonably complicated, need to ensure exact correctness, not sure if the
188  // regression tests test this functionality
189
190  @Pure
191  @Override
192  public boolean isExclusiveFormula(Invariant other) {
193    // This whole approach is wrong in the case when the sequence can
194    // ever consist of only one element.  For now, just forget
195    // it. -SMcC
196    if (true) {
197      return false;
198    }
199
200    if (other instanceof EltwiseFloatComparison) {
201
202      return !((other instanceof EltwiseIntEqual) || (other instanceof EltwiseFloatEqual)
203               || (other instanceof EltwiseIntLessEqual) || (other instanceof EltwiseFloatLessEqual)
204               || (other instanceof EltwiseIntGreaterEqual) || (other instanceof EltwiseFloatGreaterEqual));
205
206    }
207    return false;
208  }
209
210  // Look up a previously instantiated invariant.
211  public static @Nullable EltwiseFloatEqual find(PptSlice ppt) {
212    assert ppt.arity() == 1;
213    for (Invariant inv : ppt.invs) {
214      if (inv instanceof EltwiseFloatEqual) {
215        return (EltwiseFloatEqual) inv;
216      }
217    }
218    return null;
219  }
220
221  // Copied from IntComparison.
222  // public boolean isExclusiveFormula(Invariant other)
223  // {
224  //   if (other instanceof IntComparison) {
225  //     return core.isExclusiveFormula(((IntComparison) other).core);
226  //   }
227  //   if (other instanceof IntNonEqual) {
228  //     return isExact();
229  //   }
230  //   return false;
231  // }
232
233  /**
234   * This function returns whether a sample has been seen by this Invariant that includes two or
235   * more entries in an array. For a 0 or 1 element array a, a[] sorted by any binary operation is
236   * "vacuously true" because no check is ever made since the binary operation requires two
237   * operands. Thus although invariants of this type are true regarding 0 or 1 length arrays, they
238   * are meaningless. This function is meant to be used in isObviousImplied() to prevent such
239   * meaningless invariants from being printed.
240   */
241  @Override
242  public boolean hasSeenNonSingletonSample() {
243    ValueSet.ValueSetFloatArray vs = (ValueSet.ValueSetFloatArray) ppt.var_infos[0].get_value_set();
244    return vs.nonsingleton_arr_cnt() > 0;
245  }
246
247  @Pure
248  @Override
249  public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) {
250    DiscardInfo super_result = super.isObviousDynamically(vis);
251    if (super_result != null) {
252      return super_result;
253    }
254
255    if (!hasSeenNonSingletonSample()) {
256      return new DiscardInfo(this, DiscardCode.obvious,
257                             "No samples sequences of size >=2 were seen. Vacuously true.");
258    }
259
260    EltOneOfFloat eoo = EltOneOfFloat.find(ppt);
261    if ((eoo != null) && eoo.enoughSamples() && (eoo.num_elts() == 1)) {
262      return new DiscardInfo(this, DiscardCode.obvious, "The sequence contains all equal values.");
263    }
264
265    // sorted by (any operation) for an entire sequence -> sorted by that same
266    // operation for a subsequence
267
268    // also, sorted by < for entire -> sorted by <= for subsequence
269    //       sorted by > for entire -> sorted by >= for subsequence
270
271    Derivation deriv = vis[0].derived;
272
273    if ((deriv instanceof SequenceScalarSubsequence) || (deriv instanceof SequenceFloatSubsequence)) {
274      // Find the slice with the full sequence, check for an invariant of this type
275      PptSlice sliceToCheck;
276
277      if (deriv instanceof SequenceScalarSubsequence) {
278        sliceToCheck = ppt.parent.findSlice(((SequenceScalarSubsequence)deriv).seqvar());
279      } else {
280        sliceToCheck = ppt.parent.findSlice(((SequenceFloatSubsequence)deriv).seqvar());
281      }
282
283      if (sliceToCheck != null) {
284        for (Invariant inv : sliceToCheck.invs) {
285
286          if (inv.getClass().equals(getClass())) {
287            String discardString = "This is a subsequence of a sequence for which the same invariant holds.";
288            return new DiscardInfo(this, DiscardCode.obvious, discardString);
289          }
290        }
291      }
292    }
293
294    return null;
295  }
296}