Source code

001// ***** This file is automatically generated from SeqComparison.java.jpp
002
003package daikon.inv.binary.twoSequence;
004
005import daikon.*;
006import daikon.Quantify.QuantFlags;
007import daikon.derive.binary.*;
008import daikon.inv.*;
009import daikon.suppress.*;
010import java.util.*;
011import java.util.logging.Logger;
012import org.checkerframework.checker.interning.qual.Interned;
013import org.checkerframework.checker.lock.qual.GuardSatisfied;
014import org.checkerframework.checker.nullness.qual.Nullable;
015import org.checkerframework.dataflow.qual.Pure;
016import org.checkerframework.dataflow.qual.SideEffectFree;
017import org.plumelib.util.ArraysPlume;
018import org.plumelib.util.Intern;
019import typequals.prototype.qual.NonPrototype;
020import typequals.prototype.qual.Prototype;
021
022/**
023 * Represents invariants between two sequences of long values. If order matters for each
024 * variable (which it does by default), then the sequences are compared lexically. Prints as
025 * {@code x[] > y[] lexically}.
026 *
027
028 * <p>If the auxiliary information (e.g., order matters) doesn't match between two variables, then
029 * this invariant cannot apply to those variables.
030 */
031public class SeqSeqIntGreaterThan extends TwoSequence
032
033{
034  static final long serialVersionUID = 20030822L;
035
036  // Variables starting with dkconfig_ should only be set via the
037  // daikon.config.Configuration interface.
038  /** Boolean. True iff SeqSeqIntGreaterThan invariants should be considered. */
039  public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault;
040
041  /** Debugging logger. */
042  static final Logger debug = Logger.getLogger("daikon.inv.binary.twoSequence.SeqSeqIntGreaterThan");
043
044  static Comparator<long[]> comparator = ArraysPlume.LongArrayComparatorLexical.it;
045
046  boolean orderMatters;
047
048  protected SeqSeqIntGreaterThan(PptSlice ppt, boolean orderMatters) {
049    super(ppt);
050    this.orderMatters = orderMatters;
051  }
052
053  protected @Prototype SeqSeqIntGreaterThan(boolean orderMatters) {
054    super();
055    this.orderMatters = orderMatters;
056  }
057
058  protected SeqSeqIntGreaterThan(SeqSeqIntLessThan seq_swap) {
059    super(seq_swap.ppt);
060    orderMatters = seq_swap.orderMatters;
061  }
062
063  private static @Prototype SeqSeqIntGreaterThan proto = new @Prototype SeqSeqIntGreaterThan(true);
064
065  /** Returns the prototype invariant for SeqSeqIntGreaterThan */
066  public static @Prototype SeqSeqIntGreaterThan get_proto() {
067    return proto;
068  }
069
070  @Override
071  public boolean enabled() {
072    return dkconfig_enabled;
073  }
074
075  @Override
076  public boolean instantiate_ok(VarInfo[] vis) {
077
078    if (!valid_types(vis)) {
079      return false;
080    }
081
082      VarInfo var1 = vis[0];
083      VarInfo var2 = vis[1];
084      ProglangType type1 = var1.type;
085      ProglangType type2 = var2.type;
086
087      // This intentonally checks dimensions(), not pseudoDimensions.
088      boolean only_eq =
089        !((type1.dimensions() == 1)
090          && type1.baseIsIntegral()
091          && (type2.dimensions() == 1)
092          && type2.baseIsIntegral());
093      if (only_eq) {
094        return false;
095      }
096
097      // non equality comparisons don't make sense if the arrays aren't ordered
098      if (!var1.aux.hasOrder() || !var2.aux.hasOrder()) {
099        return false;
100      }
101
102    return true;
103  }
104
105  @Override
106  protected SeqSeqIntGreaterThan instantiate_dyn(@Prototype SeqSeqIntGreaterThan this, PptSlice slice) {
107    boolean has_order = slice.var_infos[0].aux.hasOrder() && slice.var_infos[1].aux.hasOrder();
108    return new SeqSeqIntGreaterThan(slice, has_order);
109  }
110
111  @Override
112  protected Invariant resurrect_done_swapped() {
113
114    return new SeqSeqIntLessThan(this);
115  }
116
117  @Override
118  public String repr(@GuardSatisfied SeqSeqIntGreaterThan this) {
119    return "SeqSeqIntGreaterThan" + varNames() + ": ,orderMatters=" + orderMatters
120      + ",enoughSamples=" + enoughSamples()
121      ;
122  }
123
124  @SideEffectFree
125  @Override
126  public String format_using(@GuardSatisfied SeqSeqIntGreaterThan this, OutputFormat format) {
127    // System.out.println("Calling SeqSeqIntGreaterThan.format for: " + repr());
128
129    if (format == OutputFormat.SIMPLIFY) {
130      return format_simplify();
131    }
132
133    if (format == OutputFormat.DAIKON) {
134      String name1 = var1().name_using(format);
135      String name2 = var2().name_using(format);
136
137      String lexically = (var1().aux.hasOrder() ? " (lexically)" : "");
138      return name1 + " > " + name2 + lexically;
139    }
140
141    if (format == OutputFormat.CSHARPCONTRACT) {
142
143      if (var1().aux.hasOrder()) {
144        String name1 = var1().csharp_collection_string();
145        String name2 = var2().csharp_collection_string();
146        String dbc = "LlexGT".substring(1);
147        return name1 + "." + dbc + "(" + name2 + ")";
148      } else {
149        return "\"SeqComparison.java.jpp: sequence comparison does not apply to unordered collections unimplemented\" != null)"; // interned
150      }
151
152    }
153
154    if (format.isJavaFamily()) {
155      String name1 = var1().name_using(format);
156      String name2 = var2().name_using(format);
157
158      return "daikon.Quant."
159        + (var1().aux.hasOrder() ? "lexGT" : "setEqual" )
160        + "("
161        + name1
162        + ", "
163        + name2
164        + ")";
165
166    }
167
168    return format_unimplemented(format);
169  }
170
171  public String format_simplify(@GuardSatisfied SeqSeqIntGreaterThan this) {
172    if (Invariant.dkconfig_simplify_define_predicates) {
173      return format_simplify_defined();
174    } else {
175      return format_simplify_explicit();
176    }
177  }
178
179  private String format_simplify_defined(@GuardSatisfied SeqSeqIntGreaterThan this) {
180    String[] var1_name = var1().simplifyNameAndBounds();
181    String[] var2_name = var2().simplifyNameAndBounds();
182    if (var1_name == null || var2_name == null) {
183      return String.format("%s.format_simplify_defined(%s): var1_name=%s, var2_name=%s, for %s",
184                           getClass().getSimpleName(), this,
185                           Arrays.toString(var1_name), Arrays.toString(var2_name), format());
186    }
187    return "(|lexical->| "
188      + var1_name[0] + " " + var1_name[1] + " " + var1_name[2] + " "
189      + var2_name[0] + " " + var2_name[1] + " " + var2_name[2] + ")";
190  }
191
192  private String format_simplify_explicit(@GuardSatisfied SeqSeqIntGreaterThan this) {
193
194      String classname = this.getClass().toString().substring(6);
195      return "warning: method " + classname
196        + ".format_simplify_explicit() needs to be implemented: " + format();
197
198  }
199
200  @Override
201  public InvariantStatus check_modified(
202      long @Interned [] v1, long @Interned [] v2, int count) {
203    /// This does not do the right thing; I really want to avoid comparisons
204    /// if one is missing, but not if one is zero-length.
205    // // Don't make comparisons with empty arrays.
206    // if ((v1.length == 0) || (v2.length == 0)) {
207    //   return;
208    // }
209
210    int comparison = 0;
211    if (orderMatters) {
212      // Standard element wise comparison
213       comparison = comparator.compare(v1, v2);
214    } else {
215      // Do a double subset comparison
216      comparison = (ArraysPlume.isSubset(v1, v2) && ArraysPlume.isSubset( v2, v1)) ? 0 : -1;
217    }
218
219    if (!(comparison > 0) ) {
220      return InvariantStatus.FALSIFIED;
221    }
222    return InvariantStatus.NO_CHANGE;
223  }
224
225  @Override
226  public InvariantStatus add_modified(long @Interned [] v1, long @Interned [] v2, int count) {
227    if (logDetail()) {
228      log("add_modified (%s, %s)", Arrays.toString(v1), Arrays.toString(v2));
229    }
230        return check_modified(v1, v2, count);
231  }
232
233  @Override
234  protected double computeConfidence() {
235
236    return 1 - Math.pow(.5, ppt.num_values());
237  }
238
239  @Pure
240  @Override
241  public boolean isSameFormula(Invariant o) {
242    return true;
243  }
244
245  @Pure
246  @Override
247  public boolean isExclusiveFormula(Invariant o) {
248    return false;
249  }
250
251  /**
252   * Since this invariant can be a postProcessed equality, we have to handle isObvious especially to
253   * avoid circular isObvious relations.
254   */
255  @Pure
256  @Override
257  public @Nullable DiscardInfo isObviousStatically_SomeInEquality() {
258    if (var1().equalitySet == var2().equalitySet) {
259      return isObviousStatically(this.ppt.var_infos);
260    } else {
261      return super.isObviousStatically_SomeInEquality();
262    }
263  }
264
265  /**
266   * Since this invariant can be a postProcessed equality, we have to handle isObvious especially to
267   * avoid circular isObvious relations.
268   */
269  @Pure
270  @Override
271  public @Nullable DiscardInfo isObviousDynamically_SomeInEquality() {
272    if (logOn()) {
273      log("Considering dynamically_someInEquality");
274    }
275    if (var1().equalitySet == var2().equalitySet) {
276      return isObviousDynamically(this.ppt.var_infos);
277    } else {
278      return super.isObviousDynamically_SomeInEquality();
279    }
280  }
281
282  @Pure
283  @Override
284  public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) {
285
286      VarInfo var1 = vis[0];
287      VarInfo var2 = vis[1];
288      DiscardInfo di;
289      di = SubSequence.isObviousSubSequence(this, var1, var2);
290      if (di == null) {
291        di = SubSequence.isObviousSubSequence(this, var2, var1);
292      }
293      if (di != null) {
294        return di;
295      }
296
297    return super.isObviousStatically(vis);
298  }
299
300  @Pure
301  @Override
302  public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) {
303    DiscardInfo super_result = super.isObviousDynamically(vis);
304    if (super_result != null) {
305      return super_result;
306    }
307    assert ppt != null;
308
309      Debug debug = new Debug(getClass(), ppt, vis);
310
311      if (logOn()) {
312        debug.log("Checking IsObviousDynamically");
313      }
314
315      // Check to see if the same Pairwise invariant exists
316      DiscardInfo di = new DiscardInfo(this, DiscardCode.obvious, "");
317      if (ppt.parent.check_implied(di, vis[0], vis[1], PairwiseIntGreaterThan.get_proto())) {
318        di.add_implied_vis(vis);
319        return di;
320      }
321
322      // If either variable is a subsequence and the original arrays
323      // are related elementwise this isn't interesting
324      VarInfo v1 = vis[0];
325      VarInfo v2 = vis[1];
326      VarInfo arr1 = v1;
327      VarInfo arr2 = v2;
328      if (v1.derived instanceof SequenceScalarSubsequence) {
329        arr1 = ((SequenceScalarSubsequence) v1.derived).seqvar();
330      }
331      if (v2.derived instanceof SequenceScalarSubsequence) {
332        arr2 = ((SequenceScalarSubsequence) v2.derived).seqvar();
333      }
334      if (!isEqual() && ((arr1 != v1) || (arr2 != v2))) {
335        VarInfo[] avis = new VarInfo [] {arr1, arr2};
336        PptSlice slice = this.ppt.parent.findSlice_unordered(avis);
337        if (slice != null) {
338          PairwiseIntEqual picEQ = PairwiseIntEqual.find(slice);
339          if (picEQ != null) {
340            return new DiscardInfo(this, DiscardCode.obvious, "Implied by " + picEQ.format());
341          }
342          PairwiseIntLessThan picLT = PairwiseIntLessThan.find(slice);
343          if (picLT != null) {
344            return new DiscardInfo(this, DiscardCode.obvious, "Implied by " + picLT.format());
345          }
346          PairwiseIntGreaterThan picGT = PairwiseIntGreaterThan.find(slice);
347          if (picGT != null) {
348            return new DiscardInfo(this, DiscardCode.obvious, "Implied by " + picGT.format());
349          }
350          PairwiseIntLessEqual picLE = PairwiseIntLessEqual.find(slice);
351          if (picLE != null) {
352            return new DiscardInfo(this, DiscardCode.obvious, "Implied by " + picLE.format());
353          }
354          PairwiseIntGreaterEqual picGE = PairwiseIntGreaterEqual.find(slice);
355          if (picGE != null) {
356            return new DiscardInfo(this, DiscardCode.obvious, "Implied by " + picGE.format());
357          }
358        }
359      }
360
361      // Similarly, if either variable is a subsequence and the original
362      // arrays are related lexically this isn't interesting
363      if ((arr1 != v1) || (arr2 != v2)) {
364        if (arr1 == arr2) {
365          debug.log("Obvious Dynamic- subsequence from same array");
366          return new DiscardInfo(this, DiscardCode.obvious, "Supersequences are related lexically");
367        }
368        VarInfo[] avis = {arr1, arr2};
369        debug.log("looking for " + avis[0].name() + " " + avis[1].name());
370        PptSlice slice = this.ppt.parent.findSlice_unordered(avis);
371        debug.log("Found ppt " + slice);
372        if (slice != null) {
373          for (Invariant inv : slice.invs) {
374            debug.log("-- invariant " + inv.format());
375          }
376          Invariant inv;
377          inv = SeqSeqIntEqual.find(slice);
378          if (inv != null) {
379            if (logOn()) {
380              debug.log("Obvious Dynamic from " + inv.format() + "(" + inv.getClass() + ")");
381            }
382            return new DiscardInfo(this, DiscardCode.obvious, "Implied by " + inv.format());
383          }
384          inv = SeqSeqIntLessThan.find(slice);
385          if (inv != null) {
386            if (logOn()) {
387              debug.log("Obvious Dynamic from " + inv.format() + "(" + inv.getClass() + ")");
388            }
389            return new DiscardInfo(this, DiscardCode.obvious, "Implied by " + inv.format());
390          }
391          inv = SeqSeqIntGreaterThan.find(slice);
392          if (inv != null) {
393            if (logOn()) {
394              debug.log("Obvious Dynamic from " + inv.format() + "(" + inv.getClass() + ")");
395            }
396            return new DiscardInfo(this, DiscardCode.obvious, "Implied by " + inv.format());
397          }
398          inv = SeqSeqIntLessEqual.find(slice);
399          if (inv != null) {
400            if (logOn()) {
401              debug.log("Obvious Dynamic from " + inv.format() + "(" + inv.getClass() + ")");
402            }
403            return new DiscardInfo(this, DiscardCode.obvious, "Implied by " + inv.format());
404          }
405          inv = SeqSeqIntGreaterEqual.find(slice);
406          if (inv != null) {
407            if (logOn()) {
408              debug.log("Obvious Dynamic from " + inv.format() + "(" + inv.getClass() + ")");
409            }
410            return new DiscardInfo(this, DiscardCode.obvious, "Implied by " + inv.format());
411          }
412        }
413      }
414
415      // Check to see if these variables are obviously related
416      if (v1.isDerived() || v2.isDerived()) {
417        if (SubSequence.isObviousSubSequenceDynamically(this, v1, v2)
418          || SubSequence.isObviousSubSequenceDynamically(this, v2, v1)) {
419          if (logOn()) {
420            debug.log("Obvious SubSequence Dynamically");
421          }
422          assert ppt != null;
423          return new DiscardInfo(
424              this,
425              DiscardCode.obvious,
426              "Both vars are derived and one is a subsequence of the other");
427        }
428      }
429
430    return null;
431  }
432
433  @Override
434  public void repCheck() {
435    super.repCheck();
436    /*
437      This code is no longer needed now that the can_be_x's are gone
438    if (!(this.can_be_eq || this.can_be_lt || this.can_be_gt)
439        && ppt.num_samples() != 0) {
440      System.err.println(this.repr());
441      System.err.println(this.ppt.num_samples());
442      throw new Error();
443    }
444    */
445  }
446
447  @Pure
448  public boolean isEqual() {
449
450    return false;
451  }
452
453  // Look up a previously instantiated invariant.
454  public static @Nullable SeqSeqIntGreaterThan find(PptSlice ppt) {
455    assert ppt.arity() == 2;
456    for (Invariant inv : ppt.invs) {
457      if (inv instanceof SeqSeqIntGreaterThan) {
458        return (SeqSeqIntGreaterThan) inv;
459      }
460    }
461    return null;
462  }
463
464  /** Returns a list of non-instantiating suppressions for this invariant. */
465  @Pure
466  @Override
467  public @Nullable NISuppressionSet get_ni_suppressions() {
468    return suppressions;
469  }
470
471    /** Definition of this invariant (the suppressee) */
472    private static NISuppressee suppressee = new NISuppressee(SeqSeqIntGreaterThan.class, 2);
473
474    // Suppressor definitions (used in suppressions below)
475    private static NISuppressor v1_pw_v2 = new NISuppressor(0, 1, PairwiseIntGreaterThan.class);
476
477    private static NISuppressionSet suppressions =
478      new NISuppressionSet(
479          new NISuppression[] {
480            // pairwise => lexical
481            new NISuppression(v1_pw_v2, suppressee),
482          });
483
484  @Override
485  public @Nullable @NonPrototype SeqSeqIntGreaterThan merge(
486      @Prototype SeqSeqIntGreaterThan this, List<@NonPrototype Invariant> invs, PptSlice parent_ppt) {
487    // Ignore the orderMatters field, because it is always the same (and is always true).
488    return (SeqSeqIntGreaterThan) super.merge(invs, parent_ppt);
489  }
490}