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