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