Source code

001// ***** This file is automatically generated from PairwiseIntComparison.java.jpp
002
003package daikon.inv.binary.twoSequence;
004
005import daikon.*;
006import daikon.Quantify.QuantFlags;
007import daikon.derive.binary.*;
008import daikon.inv.*;
009import daikon.inv.binary.twoScalar.*;
010import daikon.suppress.*;
011import java.util.Arrays;
012import java.util.Iterator;
013import java.util.logging.Level;
014import java.util.logging.Logger;
015import org.checkerframework.checker.interning.qual.Interned;
016import org.checkerframework.checker.lock.qual.GuardSatisfied;
017import org.checkerframework.checker.nullness.qual.NonNull;
018import org.checkerframework.checker.nullness.qual.Nullable;
019import org.checkerframework.dataflow.qual.Pure;
020import org.checkerframework.dataflow.qual.SideEffectFree;
021import org.plumelib.util.ArraysPlume;
022import org.plumelib.util.Intern;
023import typequals.prototype.qual.NonPrototype;
024import typequals.prototype.qual.Prototype;
025
026/**
027 * Represents an invariant between corresponding elements of two sequences of double values. The
028 * length of the sequences must match for the invariant to hold. A comparison is made over each
029 * {@code (x[i], y[i])} pair. Thus, {@code x[0]} is compared to {@code y[0]},
030 * {@code x[1]} to {@code y[1]}, and so forth. Prints as {@code x[] == y[]}.
031 */
032public class PairwiseFloatEqual extends TwoSequenceFloat {
033  // We are Serializable, so we specify a version to allow changes to
034  // method signatures without breaking serialization.  If you add or
035  // remove fields, you should change this number to the current date.
036  static final long serialVersionUID = 20030822L;
037
038  /** Debug tracer. */
039  public static final Logger debug =
040    Logger.getLogger("daikon.inv.binary.twoSequence.PairwiseFloatEqual");
041
042  // Variables starting with dkconfig_ should only be set via the
043  // daikon.config.Configuration interface.
044  /** Boolean. True iff PairwiseIntComparison invariants should be considered. */
045  public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault;
046
047  static final boolean debugPairwiseIntComparison = false;
048
049  protected PairwiseFloatEqual(PptSlice ppt) {
050    super(ppt);
051  }
052
053  protected @Prototype PairwiseFloatEqual() {
054    super();
055  }
056
057  private static @Prototype PairwiseFloatEqual proto = new @Prototype PairwiseFloatEqual();
058
059  /** Returns the prototype invariant for PairwiseFloatEqual */
060  public static @Prototype PairwiseFloatEqual get_proto() {
061    return proto;
062  }
063
064  /** Returns whether or not this invariant is enabled. */
065  @Override
066  public boolean enabled() {
067    return dkconfig_enabled;
068  }
069
070  /** PairwiseFloatEqual is only valid on integral types. */
071  @Override
072  public boolean instantiate_ok(VarInfo[] vis) {
073
074    if (!valid_types(vis)) {
075      return false;
076    }
077
078    return true;
079  }
080
081  /** instantiates the invariant on the specified slice */
082  @Override
083  protected PairwiseFloatEqual instantiate_dyn(@Prototype PairwiseFloatEqual this, PptSlice slice) {
084    PairwiseFloatEqual inv = new PairwiseFloatEqual(slice);
085    if (logOn()) {
086      inv.log("instantiate");
087    }
088    return inv;
089  }
090
091  @Pure
092  @Override
093  public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) {
094    VarInfo var1 = vis[0];
095    VarInfo var2 = vis[1];
096
097    DiscardInfo di = SubSequence.isObviousSubSequence(this, var1, var2);
098    if (di == null) {
099      di = SubSequence.isObviousSubSequence(this, var2, var1);
100    }
101    if (di != null) {
102      Global.implied_noninstantiated_invariants++;
103      return di;
104    }
105
106    // Don't instantiate if the variables can't have order
107    if (!var1.aux.hasOrder() || !var2.aux.hasOrder()) {
108      if (debug.isLoggable(Level.FINE)) {
109        debug.fine("Not instantitating for because order has no meaning: "
110                     + var1.name() + " and " + var2.name());
111      }
112      return new DiscardInfo(this, DiscardCode.obvious, "Obvious statically since order has no meaning");
113    }
114
115    return super.isObviousStatically(vis);
116  }
117
118  @Pure
119  @Override
120  public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) {
121    DiscardInfo super_result = super.isObviousDynamically(vis);
122    if (super_result != null) {
123      return super_result;
124    }
125
126    // Subsequence invariants are implied by the same invariant over
127    // the supersequence
128    DiscardInfo di = superseq_implies(vis);
129    if (di != null) {
130      return di;
131    }
132
133    return null;
134    }
135
136  /**
137   * Checks to see if the same invariant exists over supersequences of these variables:
138   *
139   * <pre>
140   *    (A[] op B[]) ^ (i == j)  &rArr; A[i..] op B[j..]
141   *    (A[] op B[]) ^ (i == j)  &rArr; A[..i] op B[..j]
142   * </pre>
143   */
144  private @Nullable DiscardInfo superseq_implies(VarInfo[] vis) {
145
146    // Make sure the variables are SequenceFloatSubsequence with the same start/end
147    VarInfo v1 = vis[0];
148    VarInfo v2 = vis[1];
149    if (!v1.isDerived() || !(v1.derived instanceof SequenceFloatSubsequence)) {
150      return null;
151    }
152    if (!v2.isDerived() || !(v2.derived instanceof SequenceFloatSubsequence)) {
153      return null;
154    }
155    @NonNull SequenceFloatSubsequence der1 = (SequenceFloatSubsequence) v1.derived;
156    @NonNull SequenceFloatSubsequence der2 = (SequenceFloatSubsequence) v2.derived;
157    if ((der1.from_start != der2.from_start)
158        || (der1.index_shift != der2.index_shift))
159      return null;
160
161    // Make sure the subscripts are equal
162    DiscardInfo di = new DiscardInfo(this, DiscardCode.obvious, "");
163    if (!ppt.parent.check_implied_canonical(di, der1.sclvar(), der2.sclvar(),
164                                             IntEqual.get_proto()))
165      return null;
166
167    // See if the super-sequences have the same invariant
168    if (!ppt.parent.check_implied_canonical(di, der1.seqvar(), der2.seqvar(),
169                                             PairwiseFloatEqual.get_proto()))
170      return null;
171
172    // Add in the vis variables to di reason (if they are different)
173    di.add_implied_vis(vis);
174    return di;
175  }
176
177  @Override
178  protected Invariant resurrect_done_swapped() {
179
180      return this;
181  }
182
183    @Pure
184    @Override
185    public boolean is_symmetric() {
186    return true;
187  }
188
189  @Override
190  public String repr(@GuardSatisfied PairwiseFloatEqual this) {
191    return "PairwiseFloatEqual" + varNames() + ": ";
192  }
193
194  public String getComparator() {
195    return "==";
196  }
197
198  @SideEffectFree
199  @Override
200  public String format_using(@GuardSatisfied PairwiseFloatEqual this, OutputFormat format) {
201
202    if (format.isJavaFamily()) {
203      return format_java_family(format);
204    }
205
206    if (format == OutputFormat.DAIKON) {
207      return format_daikon();
208    }
209    if (format == OutputFormat.ESCJAVA) {
210      return format_esc();
211    }
212    if (format == OutputFormat.SIMPLIFY) {
213      return format_simplify();
214    }
215    if (format == OutputFormat.CSHARPCONTRACT) {
216      return format_csharp();
217    }
218
219    return format_unimplemented(format);
220  }
221
222  public String format_daikon(@GuardSatisfied PairwiseFloatEqual this) {
223    return var1().name() + " == " + var2().name() + " (elementwise)";
224  }
225
226  public String format_esc(@GuardSatisfied PairwiseFloatEqual this) {
227    String[] form = VarInfo.esc_quantify(var1(), var2());
228    return form[0] + "(" + form[1] + " == " + form[2] + ")" + form[3];
229  }
230
231  public String format_simplify(@GuardSatisfied PairwiseFloatEqual this) {
232    String[] form = VarInfo.simplify_quantify(QuantFlags.element_wise(), var1(), var2());
233    return form[0] + "(EQ " + form[1] + " " + form[2] + ")" + form[3];
234  }
235
236  public String format_java_family(@GuardSatisfied PairwiseFloatEqual this, OutputFormat format) {
237    return "daikon.Quant.pairwiseEqual(" + var1().name_using(format)
238      + ", " + var2().name_using(format) + ")";
239  }
240
241  public String format_csharp(@GuardSatisfied PairwiseFloatEqual this) {
242
243    String[] split1 = var1().csharp_array_split();
244    String[] split2 = var2().csharp_array_split();
245
246    String equals_str;
247    String end_str;
248
249    equals_str = " == ";
250    end_str = "";
251
252    return "Contract.ForAll(0, " + split1[0] + ".Count(), i => " +  split1[0] + "[i]"  + split1[1] + equals_str + split2[0] + "[i]" + split2[1] + end_str + ")";
253  }
254
255  @Override
256  public InvariantStatus check_modified(double @Interned [] a1, double @Interned [] a2, int count) {
257    assert a1 != null && a2 != null
258      : var1() + " " + var2() + " " + FileIO.get_linenum();
259    if (a1.length != a2.length || a1.length == 0 || a2.length == 0) {
260      // destroyAndFlow();
261      return InvariantStatus.FALSIFIED;
262    }
263
264    int len = a1.length;
265    // int len = Math.min(a1.length, a2.length);
266
267    for (int i = 0; i < len; i++) {
268      double v1 = a1[i];
269      double v2 = a2[i];
270      if (!Global.fuzzy.eq(v1, v2) ) {
271        //  destroyAndFlow();
272        return InvariantStatus.FALSIFIED;
273      }
274    }
275    return InvariantStatus.NO_CHANGE;
276  }
277
278    @Override
279    public InvariantStatus add_modified(double @Interned [] a1, double @Interned [] a2,
280                                        int count) {
281      if (logDetail()) {
282        log(debug, "saw add_modified (" + Arrays.toString(a1)
283             + ", " + Arrays.toString(a2) + ")");
284      }
285      return check_modified(a1, a2, count);
286    }
287
288  @Override
289  protected double computeConfidence() {
290    // num_elt_values() would be more appropriate
291    // int num_values = ((PptSlice2) ppt).num_elt_values();
292    int num_values = ppt.num_samples();
293    if (num_values == 0) {
294      return Invariant.CONFIDENCE_UNJUSTIFIED;
295    } else {
296
297      // It's an equality invariant
298      return Invariant.CONFIDENCE_JUSTIFIED;
299    }
300  }
301
302  @Pure
303  @Override
304  public boolean isSameFormula(Invariant other) {
305    return true;
306  }
307
308  @Pure
309  @Override
310  public boolean isExclusiveFormula(Invariant other) {
311    return false;
312  }
313
314  // Look up a previously instantiated invariant.
315  public static @Nullable PairwiseFloatEqual find(PptSlice ppt) {
316    assert ppt.arity() == 2;
317    for (Invariant inv : ppt.invs) {
318      if (inv instanceof PairwiseFloatEqual) {
319        return (PairwiseFloatEqual) inv;
320      }
321    }
322    return null;
323  }
324
325  /** Returns a list of non-instantiating suppressions for this invariant. */
326  @Pure
327  @Override
328  public @Nullable NISuppressionSet get_ni_suppressions() {
329    return suppressions;
330  }
331
332    private static @Nullable NISuppressionSet suppressions = null;
333
334}