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