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 long sequence. Prints as
022   * {@code x[] elements are equal}.
023   */
024
025public class EltwiseIntEqual extends EltwiseIntComparison {
026  static final long serialVersionUID = 20030822L;
027
028  // Variables starting with dkconfig_ should only be set via the
029  // daikon.config.Configuration interface.
030  /** Boolean. True iff EltwiseIntComparison invariants should be considered. */
031  public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault;
032
033  static final boolean debugEltwiseIntComparison = false;
034
035  protected EltwiseIntEqual(PptSlice ppt) {
036    super(ppt);
037  }
038
039  protected @Prototype EltwiseIntEqual() {
040    super();
041  }
042
043  private static @Prototype EltwiseIntEqual proto = new @Prototype EltwiseIntEqual();
044
045  /** Returns the prototype invariant for EltwiseIntEqual */
046  public static @Prototype EltwiseIntEqual get_proto() {
047    return proto;
048  }
049
050  @Override
051  public boolean enabled() {
052    return dkconfig_enabled;
053  }
054
055  /** Non-equality EltwiseIntEqual invariants are only valid on integral types. */
056  @Override
057  public boolean instantiate_ok(VarInfo[] vis) {
058
059    if (!valid_types(vis)) {
060      return false;
061    }
062
063    return true;
064  }
065
066  @Override
067  protected EltwiseIntEqual instantiate_dyn(@Prototype EltwiseIntEqual this, PptSlice slice) {
068    return new EltwiseIntEqual(slice);
069  }
070
071  @SideEffectFree
072  @Override
073  public EltwiseIntEqual clone(@GuardSatisfied EltwiseIntEqual this) {
074    EltwiseIntEqual result = (EltwiseIntEqual) super.clone();
075    return result;
076  }
077
078  @Override
079  public String repr(@GuardSatisfied EltwiseIntEqual this) {
080    return "EltwiseIntEqual" + varNames() + ": falsified=" + falsified;
081  }
082
083  @SideEffectFree
084  @Override
085  public String format_using(@GuardSatisfied EltwiseIntEqual this, OutputFormat format) {
086    if (format.isJavaFamily()) {
087      return format_java_family(format);
088    }
089
090    if (format == OutputFormat.DAIKON) {
091      return format_daikon();
092    }
093    if (format == OutputFormat.ESCJAVA) {
094      return format_esc();
095    }
096    if (format == OutputFormat.CSHARPCONTRACT) {
097      return format_csharp_contract();
098    }
099    if (format == OutputFormat.SIMPLIFY) {
100      return format_simplify();
101    }
102
103    return format_unimplemented(format);
104  }
105
106  public String format_daikon(@GuardSatisfied EltwiseIntEqual this) {
107    if (debugEltwiseIntComparison) {
108      System.out.println(repr());
109    }
110
111    return var().name() + " elements are equal";
112  }
113
114  public String format_esc(@GuardSatisfied EltwiseIntEqual this) {
115    String[] form = VarInfo.esc_quantify(false, var(), var());
116
117      return form[0] + "(" + form[1] + " == " + form[2] + ")" + form[3];
118  }
119
120  public String format_java_family(@GuardSatisfied EltwiseIntEqual this, OutputFormat format) {
121    return "daikon.Quant.eltwiseEqual(" + var().name_using(format) + ")";
122  }
123
124  public String format_csharp_contract(@GuardSatisfied EltwiseIntEqual this) {
125    String[] split = var().csharp_array_split();
126    return "Contract.ForAll(0, " + split[0] + ".Count()-1, i => " + split[0] + "[i]" + split[1] + " == " + split[0] + "[i+1]" + split[1] + ")";
127  }
128
129  public String format_simplify(@GuardSatisfied EltwiseIntEqual this) {
130    String[] form = VarInfo.simplify_quantify(QuantFlags.adjacent(),
131                                               var(), var());
132
133    String comparator = "EQ";
134
135    return form[0] + "(" + comparator + " " + form[1] + " " + form[2] + ")"
136      + form[3];
137  }
138
139  @Override
140  @SuppressWarnings("UnnecessaryParentheses")  // generated code, parentheses are sometimes needed
141  public InvariantStatus check_modified(long @Interned [] a, int count) {
142    for (int i = 1; i < a.length; i++) {
143      if (!((a[i - 1]) == ( a[i]))) {
144        return InvariantStatus.FALSIFIED;
145      }
146    }
147    return InvariantStatus.NO_CHANGE;
148  }
149
150  @Override
151  public InvariantStatus add_modified(long @Interned [] a, int count) {
152    return check_modified(a, count);
153  }
154
155  // Perhaps check whether all the arrays of interest have length 0 or 1.
156
157  @Override
158  protected double computeConfidence() {
159
160    if (ppt.num_samples() != 0) {
161      return Invariant.CONFIDENCE_JUSTIFIED;
162    } else {
163      return Invariant.CONFIDENCE_UNJUSTIFIED;
164    }
165
166  }
167
168  @Pure
169  @Override
170  public boolean isExact() {
171
172    return true;
173  }
174
175  @Pure
176  @Override
177  public boolean isSameFormula(Invariant other) {
178    return (other instanceof EltwiseIntEqual);
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 EltwiseIntEqual) || (other instanceof EltwiseFloatEqual)
198               || (other instanceof EltwiseIntLessEqual) || (other instanceof EltwiseFloatLessEqual)
199               || (other instanceof EltwiseIntGreaterEqual) || (other instanceof EltwiseFloatGreaterEqual));
200
201    }
202    return false;
203  }
204
205  // Look up a previously instantiated invariant.
206  public static @Nullable EltwiseIntEqual find(PptSlice ppt) {
207    assert ppt.arity() == 1;
208    for (Invariant inv : ppt.invs) {
209      if (inv instanceof EltwiseIntEqual) {
210        return (EltwiseIntEqual) inv;
211      }
212    }
213    return null;
214  }
215
216  // Copied from IntComparison.
217  // public boolean isExclusiveFormula(Invariant other)
218  // {
219  //   if (other instanceof IntComparison) {
220  //     return core.isExclusiveFormula(((IntComparison) other).core);
221  //   }
222  //   if (other instanceof IntNonEqual) {
223  //     return isExact();
224  //   }
225  //   return false;
226  // }
227
228  /**
229   * This function returns whether a sample has been seen by this Invariant that includes two or
230   * more entries in an array. For a 0 or 1 element array a, a[] sorted by any binary operation is
231   * "vacuously true" because no check is ever made since the binary operation requires two
232   * operands. Thus although invariants of this type are true regarding 0 or 1 length arrays, they
233   * are meaningless. This function is meant to be used in isObviousImplied() to prevent such
234   * meaningless invariants from being printed.
235   */
236  @Override
237  public boolean hasSeenNonSingletonSample() {
238    ValueSet.ValueSetScalarArray vs = (ValueSet.ValueSetScalarArray) ppt.var_infos[0].get_value_set();
239    return vs.nonsingleton_arr_cnt() > 0;
240  }
241
242  @Pure
243  @Override
244  public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) {
245    DiscardInfo super_result = super.isObviousDynamically(vis);
246    if (super_result != null) {
247      return super_result;
248    }
249
250    if (!hasSeenNonSingletonSample()) {
251      return new DiscardInfo(this, DiscardCode.obvious,
252                             "No samples sequences of size >=2 were seen. Vacuously true.");
253    }
254
255    EltOneOf eoo = EltOneOf.find(ppt);
256    if ((eoo != null) && eoo.enoughSamples() && (eoo.num_elts() == 1)) {
257      return new DiscardInfo(this, DiscardCode.obvious, "The sequence contains all equal values.");
258    }
259
260    // sorted by (any operation) for an entire sequence -> sorted by that same
261    // operation for a subsequence
262
263    // also, sorted by < for entire -> sorted by <= for subsequence
264    //       sorted by > for entire -> sorted by >= for subsequence
265
266    Derivation deriv = vis[0].derived;
267
268    if ((deriv instanceof SequenceScalarSubsequence) || (deriv instanceof SequenceFloatSubsequence)) {
269      // Find the slice with the full sequence, check for an invariant of this type
270      PptSlice sliceToCheck;
271
272      if (deriv instanceof SequenceScalarSubsequence) {
273        sliceToCheck = ppt.parent.findSlice(((SequenceScalarSubsequence)deriv).seqvar());
274      } else {
275        sliceToCheck = ppt.parent.findSlice(((SequenceFloatSubsequence)deriv).seqvar());
276      }
277
278      if (sliceToCheck != null) {
279        for (Invariant inv : sliceToCheck.invs) {
280
281          if (inv.getClass().equals(getClass())) {
282            String discardString = "This is a subsequence of a sequence for which the same invariant holds.";
283            return new DiscardInfo(this, DiscardCode.obvious, discardString);
284          }
285        }
286      }
287    }
288
289    return null;
290  }
291}