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 the invariant &ge; between adjacent elements
022   * (x[i], x[i+1]) of a double sequence. Prints as
023   * {@code x[] sorted by >=}.
024   */
025
026public class EltwiseFloatGreaterEqual extends EltwiseFloatComparison {
027  static final long serialVersionUID = 20030822L;
028
029  // Variables starting with dkconfig_ should only be set via the
030  // daikon.config.Configuration interface.
031  /** Boolean. True iff EltwiseIntComparison invariants should be considered. */
032  public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault;
033
034  static final boolean debugEltwiseIntComparison = false;
035
036  protected EltwiseFloatGreaterEqual(PptSlice ppt) {
037    super(ppt);
038  }
039
040  protected @Prototype EltwiseFloatGreaterEqual() {
041    super();
042  }
043
044  private static @Prototype EltwiseFloatGreaterEqual proto = new @Prototype EltwiseFloatGreaterEqual();
045
046  /** Returns the prototype invariant for EltwiseFloatGreaterEqual */
047  public static @Prototype EltwiseFloatGreaterEqual get_proto() {
048    return proto;
049  }
050
051  @Override
052  public boolean enabled() {
053    return dkconfig_enabled;
054  }
055
056  /** Non-equality EltwiseFloatGreaterEqual invariants are only valid on integral types. */
057  @Override
058  public boolean instantiate_ok(VarInfo[] vis) {
059
060    if (!valid_types(vis)) {
061      return false;
062    }
063
064    return true;
065  }
066
067  @Override
068  protected EltwiseFloatGreaterEqual instantiate_dyn(@Prototype EltwiseFloatGreaterEqual this, PptSlice slice) {
069    return new EltwiseFloatGreaterEqual(slice);
070  }
071
072  @SideEffectFree
073  @Override
074  public EltwiseFloatGreaterEqual clone(@GuardSatisfied EltwiseFloatGreaterEqual this) {
075    EltwiseFloatGreaterEqual result = (EltwiseFloatGreaterEqual) super.clone();
076    return result;
077  }
078
079  @Override
080  public String repr(@GuardSatisfied EltwiseFloatGreaterEqual this) {
081    return "EltwiseFloatGreaterEqual" + varNames() + ": falsified=" + falsified;
082  }
083
084  @SideEffectFree
085  @Override
086  public String format_using(@GuardSatisfied EltwiseFloatGreaterEqual this, OutputFormat format) {
087    if (format.isJavaFamily()) {
088      return format_java_family(format);
089    }
090
091    if (format == OutputFormat.DAIKON) {
092      return format_daikon();
093    }
094    if (format == OutputFormat.ESCJAVA) {
095      return format_esc();
096    }
097    if (format == OutputFormat.CSHARPCONTRACT) {
098      return format_csharp_contract();
099    }
100    if (format == OutputFormat.SIMPLIFY) {
101      return format_simplify();
102    }
103
104    return format_unimplemented(format);
105  }
106
107  public String format_daikon(@GuardSatisfied EltwiseFloatGreaterEqual this) {
108    if (debugEltwiseIntComparison) {
109      System.out.println(repr());
110    }
111
112    return var().name() + " sorted by >=";
113  }
114
115  public String format_esc(@GuardSatisfied EltwiseFloatGreaterEqual this) {
116    String[] form = VarInfo.esc_quantify(false, var(), var());
117
118      return form[0] + "((i+1 == j) ==> (" + form[1] + " >= " + form[2] + "))" + form[3];
119  }
120
121  public String format_java_family(@GuardSatisfied EltwiseFloatGreaterEqual this, OutputFormat format) {
122    return "daikon.Quant.eltwiseGTE(" + var().name_using(format) + ")";
123  }
124
125  public String format_csharp_contract(@GuardSatisfied EltwiseFloatGreaterEqual this) {
126    String[] split = var().csharp_array_split();
127    return "Contract.ForAll(0, " + split[0] + ".Count()-1, i => " + split[0] + "[i]" + split[1] + " >= " + split[0] + "[i+1]" + split[1] + ")";
128  }
129
130  public String format_simplify(@GuardSatisfied EltwiseFloatGreaterEqual this) {
131    String[] form = VarInfo.simplify_quantify(QuantFlags.adjacent(),
132                                               var(), var());
133
134    String comparator = ">=";
135
136    return form[0] + "(" + comparator + " " + form[1] + " " + form[2] + ")"
137      + form[3];
138  }
139
140  @Override
141  @SuppressWarnings("UnnecessaryParentheses")  // generated code, parentheses are sometimes needed
142  public InvariantStatus check_modified(double @Interned [] a, int count) {
143    for (int i = 1; i < a.length; i++) {
144      if (!Global.fuzzy.gte(a[i - 1], a[i])) {
145        return InvariantStatus.FALSIFIED;
146      }
147    }
148    return InvariantStatus.NO_CHANGE;
149  }
150
151  @Override
152  public InvariantStatus add_modified(double @Interned [] a, int count) {
153    return check_modified(a, count);
154  }
155
156  // Perhaps check whether all the arrays of interest have length 0 or 1.
157
158  @Override
159  protected double computeConfidence() {
160
161    return 1 - Math.pow(.5, ppt.num_samples());
162  }
163
164  @Pure
165  @Override
166  public boolean isExact() {
167
168    return false;
169  }
170
171  @Pure
172  @Override
173  public boolean isSameFormula(Invariant other) {
174    return (other instanceof EltwiseFloatGreaterEqual);
175  }
176
177  // Not pretty... is there another way?
178  // Also, reasonably complicated, need to ensure exact correctness, not sure if the
179  // regression tests test this functionality
180
181  @Pure
182  @Override
183  public boolean isExclusiveFormula(Invariant other) {
184    // This whole approach is wrong in the case when the sequence can
185    // ever consist of only one element.  For now, just forget
186    // it. -SMcC
187    if (true) {
188      return false;
189    }
190
191    if (other instanceof EltwiseFloatComparison) {
192
193      return (other instanceof EltwiseIntLessThan) || (other instanceof EltwiseFloatLessThan);
194    }
195    return false;
196  }
197
198  // Look up a previously instantiated invariant.
199  public static @Nullable EltwiseFloatGreaterEqual find(PptSlice ppt) {
200    assert ppt.arity() == 1;
201    for (Invariant inv : ppt.invs) {
202      if (inv instanceof EltwiseFloatGreaterEqual) {
203        return (EltwiseFloatGreaterEqual) inv;
204      }
205    }
206    return null;
207  }
208
209  // Copied from IntComparison.
210  // public boolean isExclusiveFormula(Invariant other)
211  // {
212  //   if (other instanceof IntComparison) {
213  //     return core.isExclusiveFormula(((IntComparison) other).core);
214  //   }
215  //   if (other instanceof IntNonEqual) {
216  //     return isExact();
217  //   }
218  //   return false;
219  // }
220
221  /**
222   * This function returns whether a sample has been seen by this Invariant that includes two or
223   * more entries in an array. For a 0 or 1 element array a, a[] sorted by any binary operation is
224   * "vacuously true" because no check is ever made since the binary operation requires two
225   * operands. Thus although invariants of this type are true regarding 0 or 1 length arrays, they
226   * are meaningless. This function is meant to be used in isObviousImplied() to prevent such
227   * meaningless invariants from being printed.
228   */
229  @Override
230  public boolean hasSeenNonSingletonSample() {
231    ValueSet.ValueSetFloatArray vs = (ValueSet.ValueSetFloatArray) ppt.var_infos[0].get_value_set();
232    return vs.nonsingleton_arr_cnt() > 0;
233  }
234
235  @Pure
236  @Override
237  public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) {
238    DiscardInfo super_result = super.isObviousDynamically(vis);
239    if (super_result != null) {
240      return super_result;
241    }
242
243    if (!hasSeenNonSingletonSample()) {
244      return new DiscardInfo(this, DiscardCode.obvious,
245                             "No samples sequences of size >=2 were seen. Vacuously true.");
246    }
247
248    EltOneOfFloat eoo = EltOneOfFloat.find(ppt);
249    if ((eoo != null) && eoo.enoughSamples() && (eoo.num_elts() == 1)) {
250      return new DiscardInfo(this, DiscardCode.obvious, "The sequence contains all equal values.");
251    }
252
253    {
254      // some relations imply others as follows: < -> <=, > -> >=
255      // == -> <=, >=
256
257      // This code lets through some implied invariants, here is how:
258      // In the ESC, JML, Java modes of output, the invariants are guarded
259      // before printing.  This guarding makes some of the invariants that
260      // are searched for (example, NoDuplicates) unable to be found since it
261      // won't find something of the form (a -> NoDuplicates).  This can
262      // cause cases to exist, for example, the invariants (a -> b[] sorted
263      // by !=), (a -> b[] has no duplicates) existing in the same ppt where
264      // one is obviously implied by the other. I am not sure currently of
265      // the best way with dealing with this, but I am going to allow these
266      // other invariants to exist for now because they are not wrong, just
267      // obvious.
268
269      for (Invariant inv : ppt.invs) {
270
271        if ((inv instanceof EltwiseIntGreaterThan) || (inv instanceof EltwiseFloatGreaterThan)) {
272          String discardString = "The invariant holds for > which implies >=.";
273          return new DiscardInfo(this, DiscardCode.obvious, discardString);
274        } else if ((inv instanceof EltwiseIntEqual) || (inv instanceof EltwiseFloatEqual)) {
275          String discardString = "The invariant holds for == which implies >=.";
276          return new DiscardInfo(this, DiscardCode.obvious, discardString);
277        }
278
279      }
280
281    }
282
283    // sorted by (any operation) for an entire sequence -> sorted by that same
284    // operation for a subsequence
285
286    // also, sorted by < for entire -> sorted by <= for subsequence
287    //       sorted by > for entire -> sorted by >= for subsequence
288
289    Derivation deriv = vis[0].derived;
290
291    if ((deriv instanceof SequenceScalarSubsequence) || (deriv instanceof SequenceFloatSubsequence)) {
292      // Find the slice with the full sequence, check for an invariant of this type
293      PptSlice sliceToCheck;
294
295      if (deriv instanceof SequenceScalarSubsequence) {
296        sliceToCheck = ppt.parent.findSlice(((SequenceScalarSubsequence)deriv).seqvar());
297      } else {
298        sliceToCheck = ppt.parent.findSlice(((SequenceFloatSubsequence)deriv).seqvar());
299      }
300
301      if (sliceToCheck != null) {
302        for (Invariant inv : sliceToCheck.invs) {
303
304          if ((inv instanceof EltwiseIntGreaterThan) || (inv instanceof EltwiseFloatGreaterThan)) {
305             String discardString = "This is a subsequence of a sequence for which the > invariant holds.";
306            return new DiscardInfo(this, DiscardCode.obvious, discardString);
307          }
308
309          if (inv.getClass().equals(getClass())) {
310            String discardString = "This is a subsequence of a sequence for which the same invariant holds.";
311            return new DiscardInfo(this, DiscardCode.obvious, discardString);
312          }
313        }
314      }
315    }
316
317    return null;
318  }
319}