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 long 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 PairwiseIntLessEqual extends TwoSequence {
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.PairwiseIntLessEqual");
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 PairwiseIntLessEqual(PptSlice ppt) {
050    super(ppt);
051  }
052
053  protected @Prototype PairwiseIntLessEqual() {
054    super();
055  }
056
057  private static @Prototype PairwiseIntLessEqual proto = new @Prototype PairwiseIntLessEqual();
058
059  /** Returns the prototype invariant for PairwiseIntLessEqual */
060  public static @Prototype PairwiseIntLessEqual 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  /** PairwiseIntLessEqual 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      if (!(vis[0].type.elementIsIntegral() && vis[1].type.elementIsIntegral())) {
079        return false;
080      }
081
082    return true;
083  }
084
085  /** instantiates the invariant on the specified slice */
086  @Override
087  protected PairwiseIntLessEqual instantiate_dyn(@Prototype PairwiseIntLessEqual this, PptSlice slice) {
088    PairwiseIntLessEqual inv = new PairwiseIntLessEqual(slice);
089    if (logOn()) {
090      inv.log("instantiate");
091    }
092    return inv;
093  }
094
095  protected PairwiseIntLessEqual(PairwiseIntGreaterEqual swapped_pic) {
096    super(swapped_pic.ppt);
097    if (logOn()) {
098      log("Instantiated from resurrect_done_swapped");
099    }
100  }
101
102  @Pure
103  @Override
104  public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) {
105    VarInfo var1 = vis[0];
106    VarInfo var2 = vis[1];
107
108    DiscardInfo di = SubSequence.isObviousSubSequence(this, var1, var2);
109    if (di == null) {
110      di = SubSequence.isObviousSubSequence(this, var2, var1);
111    }
112    if (di != null) {
113      Global.implied_noninstantiated_invariants++;
114      return di;
115    }
116
117    // Don't instantiate if the variables can't have order
118    if (!var1.aux.hasOrder() || !var2.aux.hasOrder()) {
119      if (debug.isLoggable(Level.FINE)) {
120        debug.fine("Not instantitating for because order has no meaning: "
121                     + var1.name() + " and " + var2.name());
122      }
123      return new DiscardInfo(this, DiscardCode.obvious, "Obvious statically since order has no meaning");
124    }
125
126    return super.isObviousStatically(vis);
127  }
128
129  @Pure
130  @Override
131  public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) {
132    DiscardInfo super_result = super.isObviousDynamically(vis);
133    if (super_result != null) {
134      return super_result;
135    }
136
137    // Subsequence invariants are implied by the same invariant over
138    // the supersequence
139    DiscardInfo di = superseq_implies(vis);
140    if (di != null) {
141      return di;
142    }
143
144    return null;
145    }
146
147  /**
148   * Checks to see if the same invariant exists over supersequences of these variables:
149   *
150   * <pre>
151   *    (A[] op B[]) ^ (i == j)  &rArr; A[i..] op B[j..]
152   *    (A[] op B[]) ^ (i == j)  &rArr; A[..i] op B[..j]
153   * </pre>
154   */
155  private @Nullable DiscardInfo superseq_implies(VarInfo[] vis) {
156
157    // Make sure the variables are SequenceScalarSubsequence with the same start/end
158    VarInfo v1 = vis[0];
159    VarInfo v2 = vis[1];
160    if (!v1.isDerived() || !(v1.derived instanceof SequenceScalarSubsequence)) {
161      return null;
162    }
163    if (!v2.isDerived() || !(v2.derived instanceof SequenceScalarSubsequence)) {
164      return null;
165    }
166    @NonNull SequenceScalarSubsequence der1 = (SequenceScalarSubsequence) v1.derived;
167    @NonNull SequenceScalarSubsequence der2 = (SequenceScalarSubsequence) v2.derived;
168    if ((der1.from_start != der2.from_start)
169        || (der1.index_shift != der2.index_shift))
170      return null;
171
172    // Make sure the subscripts are equal
173    DiscardInfo di = new DiscardInfo(this, DiscardCode.obvious, "");
174    if (!ppt.parent.check_implied_canonical(di, der1.sclvar(), der2.sclvar(),
175                                             IntEqual.get_proto()))
176      return null;
177
178    // See if the super-sequences have the same invariant
179    if (!ppt.parent.check_implied_canonical(di, der1.seqvar(), der2.seqvar(),
180                                             PairwiseIntLessEqual.get_proto()))
181      return null;
182
183    // Add in the vis variables to di reason (if they are different)
184    di.add_implied_vis(vis);
185    return di;
186  }
187
188  @Override
189  protected Invariant resurrect_done_swapped() {
190
191      return new PairwiseIntGreaterEqual(this);
192  }
193
194  /** Returns the class that corresponds to this class with its variable order swapped. */
195  public static Class<PairwiseIntGreaterEqual> swap_class() {
196    return PairwiseIntGreaterEqual.class;
197  }
198
199  @Override
200  public String repr(@GuardSatisfied PairwiseIntLessEqual this) {
201    return "PairwiseIntLessEqual" + varNames() + ": ";
202  }
203
204  public String getComparator() {
205    return "<=";
206  }
207
208  @SideEffectFree
209  @Override
210  public String format_using(@GuardSatisfied PairwiseIntLessEqual this, OutputFormat format) {
211
212    if (format.isJavaFamily()) {
213      return format_java_family(format);
214    }
215
216    if (format == OutputFormat.DAIKON) {
217      return format_daikon();
218    }
219    if (format == OutputFormat.ESCJAVA) {
220      return format_esc();
221    }
222    if (format == OutputFormat.SIMPLIFY) {
223      return format_simplify();
224    }
225    if (format == OutputFormat.CSHARPCONTRACT) {
226      return format_csharp();
227    }
228
229    return format_unimplemented(format);
230  }
231
232  public String format_daikon(@GuardSatisfied PairwiseIntLessEqual this) {
233    return var1().name() + " <= " + var2().name() + " (elementwise)";
234  }
235
236  public String format_esc(@GuardSatisfied PairwiseIntLessEqual this) {
237    String[] form = VarInfo.esc_quantify(var1(), var2());
238    return form[0] + "(" + form[1] + " <= " + form[2] + ")" + form[3];
239  }
240
241  public String format_simplify(@GuardSatisfied PairwiseIntLessEqual this) {
242    String[] form = VarInfo.simplify_quantify(QuantFlags.element_wise(), var1(), var2());
243    return form[0] + "(<= " + form[1] + " " + form[2] + ")" + form[3];
244  }
245
246  public String format_java_family(@GuardSatisfied PairwiseIntLessEqual this, OutputFormat format) {
247    return "daikon.Quant.pairwiseLTE(" + var1().name_using(format)
248      + ", " + var2().name_using(format) + ")";
249  }
250
251  public String format_csharp(@GuardSatisfied PairwiseIntLessEqual this) {
252
253    String[] split1 = var1().csharp_array_split();
254    String[] split2 = var2().csharp_array_split();
255
256    String equals_str;
257    String end_str;
258
259    equals_str = " <= ";
260    end_str = "";
261
262    return "Contract.ForAll(0, " + split1[0] + ".Count(), i => " +  split1[0] + "[i]"  + split1[1] + equals_str + split2[0] + "[i]" + split2[1] + end_str + ")";
263  }
264
265  @Override
266  public InvariantStatus check_modified(long @Interned [] a1, long @Interned [] a2, int count) {
267    assert a1 != null && a2 != null
268      : var1() + " " + var2() + " " + FileIO.get_linenum();
269    if (a1.length != a2.length || a1.length == 0 || a2.length == 0) {
270      // destroyAndFlow();
271      return InvariantStatus.FALSIFIED;
272    }
273
274    int len = a1.length;
275    // int len = Math.min(a1.length, a2.length);
276
277    for (int i = 0; i < len; i++) {
278      long v1 = a1[i];
279      long v2 = a2[i];
280      if (!(v1 <= v2) ) {
281        //  destroyAndFlow();
282        return InvariantStatus.FALSIFIED;
283      }
284    }
285    return InvariantStatus.NO_CHANGE;
286  }
287
288    @Override
289    public InvariantStatus add_modified(long @Interned [] a1, long @Interned [] a2,
290                                        int count) {
291      if (logDetail()) {
292        log(debug, "saw add_modified (" + Arrays.toString(a1)
293             + ", " + Arrays.toString(a2) + ")");
294      }
295      return check_modified(a1, a2, count);
296    }
297
298  @Override
299  protected double computeConfidence() {
300    // num_elt_values() would be more appropriate
301    // int num_values = ((PptSlice2) ppt).num_elt_values();
302    int num_values = ppt.num_samples();
303    if (num_values == 0) {
304      return Invariant.CONFIDENCE_UNJUSTIFIED;
305    } else {
306
307      return 1 - Math.pow(.5, num_values);
308    }
309  }
310
311  @Pure
312  @Override
313  public boolean isSameFormula(Invariant other) {
314    return true;
315  }
316
317  @Pure
318  @Override
319  public boolean isExclusiveFormula(Invariant other) {
320    return false;
321  }
322
323  // Look up a previously instantiated invariant.
324  public static @Nullable PairwiseIntLessEqual find(PptSlice ppt) {
325    assert ppt.arity() == 2;
326    for (Invariant inv : ppt.invs) {
327      if (inv instanceof PairwiseIntLessEqual) {
328        return (PairwiseIntLessEqual) inv;
329      }
330    }
331    return null;
332  }
333
334  /** Returns a list of non-instantiating suppressions for this invariant. */
335  @Pure
336  @Override
337  public @Nullable NISuppressionSet get_ni_suppressions() {
338    return suppressions;
339  }
340
341  /** Definition of this invariant (the suppressee) */
342  private static NISuppressee suppressee = new NISuppressee(PairwiseIntLessEqual.class, 2);
343
344  // Suppressor definitions (used in suppressions below)
345  private static NISuppressor v1_eq_v2 = new NISuppressor(0, 1, PairwiseIntEqual.class);
346  private static NISuppressor v1_lt_v2 = new NISuppressor(0, 1, PairwiseIntLessThan.class);
347
348  private static NISuppressionSet suppressions =
349    new NISuppressionSet(
350        new NISuppression[] {
351
352          // v1 == v2 => v1 <= v2
353          new NISuppression(v1_eq_v2, suppressee),
354
355          // v1 < v2 => v1 <= v2
356          new NISuppression(v1_lt_v2, suppressee),
357
358        });
359
360}