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 long sequence. Prints as
023   * {@code x[] sorted by >=}.
024   */
025
026public class EltwiseIntGreaterEqual extends EltwiseIntComparison {
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 EltwiseIntGreaterEqual(PptSlice ppt) {
037    super(ppt);
038  }
039
040  protected @Prototype EltwiseIntGreaterEqual() {
041    super();
042  }
043
044  private static @Prototype EltwiseIntGreaterEqual proto = new @Prototype EltwiseIntGreaterEqual();
045
046  /** Returns the prototype invariant for EltwiseIntGreaterEqual */
047  public static @Prototype EltwiseIntGreaterEqual get_proto() {
048    return proto;
049  }
050
051  @Override
052  public boolean enabled() {
053    return dkconfig_enabled;
054  }
055
056  /** Non-equality EltwiseIntGreaterEqual 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      if (!vis[0].type.baseIsIntegral()) {
065        return false;
066      }
067
068    return true;
069  }
070
071  @Override
072  protected EltwiseIntGreaterEqual instantiate_dyn(@Prototype EltwiseIntGreaterEqual this, PptSlice slice) {
073    return new EltwiseIntGreaterEqual(slice);
074  }
075
076  @SideEffectFree
077  @Override
078  public EltwiseIntGreaterEqual clone(@GuardSatisfied EltwiseIntGreaterEqual this) {
079    EltwiseIntGreaterEqual result = (EltwiseIntGreaterEqual) super.clone();
080    return result;
081  }
082
083  @Override
084  public String repr(@GuardSatisfied EltwiseIntGreaterEqual this) {
085    return "EltwiseIntGreaterEqual" + varNames() + ": falsified=" + falsified;
086  }
087
088  @SideEffectFree
089  @Override
090  public String format_using(@GuardSatisfied EltwiseIntGreaterEqual 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 EltwiseIntGreaterEqual 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 EltwiseIntGreaterEqual this) {
120    String[] form = VarInfo.esc_quantify(false, var(), var());
121
122      return form[0] + "((i+1 == j) ==> (" + form[1] + " >= " + form[2] + "))" + form[3];
123  }
124
125  public String format_java_family(@GuardSatisfied EltwiseIntGreaterEqual this, OutputFormat format) {
126    return "daikon.Quant.eltwiseGTE(" + var().name_using(format) + ")";
127  }
128
129  public String format_csharp_contract(@GuardSatisfied EltwiseIntGreaterEqual 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 EltwiseIntGreaterEqual this) {
135    String[] form = VarInfo.simplify_quantify(QuantFlags.adjacent(),
136                                               var(), var());
137
138    String comparator = ">=";
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(long @Interned [] a, int count) {
147    for (int i = 1; i < a.length; i++) {
148      if (!((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(long @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    return 1 - Math.pow(.5, ppt.num_samples());
166  }
167
168  @Pure
169  @Override
170  public boolean isExact() {
171
172    return false;
173  }
174
175  @Pure
176  @Override
177  public boolean isSameFormula(Invariant other) {
178    return (other instanceof EltwiseIntGreaterEqual);
179  }
180
181  // Not pretty... is there another way?
182  // Also, reasonably complicated, need to ensure exact correctness, not sure if the
183  // regression tests test this functionality
184
185  @Pure
186  @Override
187  public boolean isExclusiveFormula(Invariant other) {
188    // This whole approach is wrong in the case when the sequence can
189    // ever consist of only one element.  For now, just forget
190    // it. -SMcC
191    if (true) {
192      return false;
193    }
194
195    if (other instanceof EltwiseIntComparison) {
196
197      return (other instanceof EltwiseIntLessThan) || (other instanceof EltwiseFloatLessThan);
198    }
199    return false;
200  }
201
202  // Look up a previously instantiated invariant.
203  public static @Nullable EltwiseIntGreaterEqual find(PptSlice ppt) {
204    assert ppt.arity() == 1;
205    for (Invariant inv : ppt.invs) {
206      if (inv instanceof EltwiseIntGreaterEqual) {
207        return (EltwiseIntGreaterEqual) inv;
208      }
209    }
210    return null;
211  }
212
213  // Copied from IntComparison.
214  // public boolean isExclusiveFormula(Invariant other)
215  // {
216  //   if (other instanceof IntComparison) {
217  //     return core.isExclusiveFormula(((IntComparison) other).core);
218  //   }
219  //   if (other instanceof IntNonEqual) {
220  //     return isExact();
221  //   }
222  //   return false;
223  // }
224
225  /**
226   * This function returns whether a sample has been seen by this Invariant that includes two or
227   * more entries in an array. For a 0 or 1 element array a, a[] sorted by any binary operation is
228   * "vacuously true" because no check is ever made since the binary operation requires two
229   * operands. Thus although invariants of this type are true regarding 0 or 1 length arrays, they
230   * are meaningless. This function is meant to be used in isObviousImplied() to prevent such
231   * meaningless invariants from being printed.
232   */
233  @Override
234  public boolean hasSeenNonSingletonSample() {
235    ValueSet.ValueSetScalarArray vs = (ValueSet.ValueSetScalarArray) ppt.var_infos[0].get_value_set();
236    return vs.nonsingleton_arr_cnt() > 0;
237  }
238
239  @Pure
240  @Override
241  public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) {
242    DiscardInfo super_result = super.isObviousDynamically(vis);
243    if (super_result != null) {
244      return super_result;
245    }
246
247    if (!hasSeenNonSingletonSample()) {
248      return new DiscardInfo(this, DiscardCode.obvious,
249                             "No samples sequences of size >=2 were seen. Vacuously true.");
250    }
251
252    EltOneOf eoo = EltOneOf.find(ppt);
253    if ((eoo != null) && eoo.enoughSamples() && (eoo.num_elts() == 1)) {
254      return new DiscardInfo(this, DiscardCode.obvious, "The sequence contains all equal values.");
255    }
256
257    {
258      // some relations imply others as follows: < -> <=, > -> >=
259      // == -> <=, >=
260
261      // This code lets through some implied invariants, here is how:
262      // In the ESC, JML, Java modes of output, the invariants are guarded
263      // before printing.  This guarding makes some of the invariants that
264      // are searched for (example, NoDuplicates) unable to be found since it
265      // won't find something of the form (a -> NoDuplicates).  This can
266      // cause cases to exist, for example, the invariants (a -> b[] sorted
267      // by !=), (a -> b[] has no duplicates) existing in the same ppt where
268      // one is obviously implied by the other. I am not sure currently of
269      // the best way with dealing with this, but I am going to allow these
270      // other invariants to exist for now because they are not wrong, just
271      // obvious.
272
273      for (Invariant inv : ppt.invs) {
274
275        if ((inv instanceof EltwiseIntGreaterThan) || (inv instanceof EltwiseFloatGreaterThan)) {
276          String discardString = "The invariant holds for > which implies >=.";
277          return new DiscardInfo(this, DiscardCode.obvious, discardString);
278        } else if ((inv instanceof EltwiseIntEqual) || (inv instanceof EltwiseFloatEqual)) {
279          String discardString = "The invariant holds for == which implies >=.";
280          return new DiscardInfo(this, DiscardCode.obvious, discardString);
281        }
282
283      }
284
285    }
286
287    // sorted by (any operation) for an entire sequence -> sorted by that same
288    // operation for a subsequence
289
290    // also, sorted by < for entire -> sorted by <= for subsequence
291    //       sorted by > for entire -> sorted by >= for subsequence
292
293    Derivation deriv = vis[0].derived;
294
295    if ((deriv instanceof SequenceScalarSubsequence) || (deriv instanceof SequenceFloatSubsequence)) {
296      // Find the slice with the full sequence, check for an invariant of this type
297      PptSlice sliceToCheck;
298
299      if (deriv instanceof SequenceScalarSubsequence) {
300        sliceToCheck = ppt.parent.findSlice(((SequenceScalarSubsequence)deriv).seqvar());
301      } else {
302        sliceToCheck = ppt.parent.findSlice(((SequenceFloatSubsequence)deriv).seqvar());
303      }
304
305      if (sliceToCheck != null) {
306        for (Invariant inv : sliceToCheck.invs) {
307
308          if ((inv instanceof EltwiseIntGreaterThan) || (inv instanceof EltwiseFloatGreaterThan)) {
309             String discardString = "This is a subsequence of a sequence for which the > invariant holds.";
310            return new DiscardInfo(this, DiscardCode.obvious, discardString);
311          }
312
313          if (inv.getClass().equals(getClass())) {
314            String discardString = "This is a subsequence of a sequence for which the same invariant holds.";
315            return new DiscardInfo(this, DiscardCode.obvious, discardString);
316          }
317        }
318      }
319    }
320
321    return null;
322  }
323}