Source code

001  // #define PAIRWISEINTEQUAL PairwiseStringLessThan
002
003// ***** This file is automatically generated from SeqComparison.java.jpp
004
005package daikon.inv.binary.twoSequence;
006
007import daikon.*;
008import daikon.Quantify.QuantFlags;
009import daikon.derive.binary.*;
010import daikon.inv.*;
011import daikon.suppress.*;
012import java.util.*;
013import java.util.logging.Logger;
014import org.checkerframework.checker.interning.qual.Interned;
015import org.checkerframework.checker.lock.qual.GuardSatisfied;
016import org.checkerframework.checker.nullness.qual.Nullable;
017import org.checkerframework.dataflow.qual.Pure;
018import org.checkerframework.dataflow.qual.SideEffectFree;
019import org.plumelib.util.ArraysPlume;
020import org.plumelib.util.Intern;
021import typequals.prototype.qual.NonPrototype;
022import typequals.prototype.qual.Prototype;
023
024/**
025 * Represents invariants between two sequences of String values. If order matters for each
026 * variable (which it does by default), then the sequences are compared lexically. Prints as
027 * {@code x[] < y[] lexically}.
028 *
029
030 * <p>If the auxiliary information (e.g., order matters) doesn't match between two variables, then
031 * this invariant cannot apply to those variables.
032 */
033public class SeqSeqStringLessThan extends TwoSequenceString
034
035{
036  static final long serialVersionUID = 20030822L;
037
038  // Variables starting with dkconfig_ should only be set via the
039  // daikon.config.Configuration interface.
040  /** Boolean. True iff SeqSeqStringLessThan invariants should be considered. */
041  public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault;
042
043  /** Debugging logger. */
044  static final Logger debug = Logger.getLogger("daikon.inv.binary.twoSequence.SeqSeqStringLessThan");
045
046  static Comparator<String[]> comparator = ArraysPlume.StringArrayComparatorLexical.it;
047
048  boolean orderMatters;
049
050  protected SeqSeqStringLessThan(PptSlice ppt, boolean orderMatters) {
051    super(ppt);
052    this.orderMatters = orderMatters;
053  }
054
055  protected @Prototype SeqSeqStringLessThan(boolean orderMatters) {
056    super();
057    this.orderMatters = orderMatters;
058  }
059
060  protected SeqSeqStringLessThan(SeqSeqStringGreaterThan seq_swap) {
061    super(seq_swap.ppt);
062    orderMatters = seq_swap.orderMatters;
063  }
064
065  private static @Prototype SeqSeqStringLessThan proto = new @Prototype SeqSeqStringLessThan(true);
066
067  /** Returns the prototype invariant for SeqSeqStringLessThan */
068  public static @Prototype SeqSeqStringLessThan get_proto() {
069    return proto;
070  }
071
072  @Override
073  public boolean enabled() {
074    return dkconfig_enabled;
075  }
076
077  @Override
078  public boolean instantiate_ok(VarInfo[] vis) {
079
080    if (!valid_types(vis)) {
081      return false;
082    }
083
084      VarInfo var1 = vis[0];
085      VarInfo var2 = vis[1];
086      ProglangType type1 = var1.type;
087      ProglangType type2 = var2.type;
088
089      // This intentonally checks dimensions(), not pseudoDimensions.
090      boolean only_eq =
091        !((type1.dimensions() == 1)
092          && type1.baseIsString()
093          && (type2.dimensions() == 1)
094          && type2.baseIsString());
095      if (only_eq) {
096        return false;
097      }
098
099      // non equality comparisons don't make sense if the arrays aren't ordered
100      if (!var1.aux.hasOrder() || !var2.aux.hasOrder()) {
101        return false;
102      }
103
104    return true;
105  }
106
107  @Override
108  protected SeqSeqStringLessThan instantiate_dyn(@Prototype SeqSeqStringLessThan this, PptSlice slice) {
109    boolean has_order = slice.var_infos[0].aux.hasOrder() && slice.var_infos[1].aux.hasOrder();
110    return new SeqSeqStringLessThan(slice, has_order);
111  }
112
113  @Override
114  protected Invariant resurrect_done_swapped() {
115
116    return new SeqSeqStringGreaterThan(this);
117  }
118
119  @Override
120  public String repr(@GuardSatisfied SeqSeqStringLessThan this) {
121    return "SeqSeqStringLessThan" + varNames() + ": ,orderMatters=" + orderMatters
122      + ",enoughSamples=" + enoughSamples()
123      ;
124  }
125
126  @SideEffectFree
127  @Override
128  public String format_using(@GuardSatisfied SeqSeqStringLessThan this, OutputFormat format) {
129    // System.out.println("Calling SeqSeqStringLessThan.format for: " + repr());
130
131    if (format == OutputFormat.SIMPLIFY) {
132      return format_simplify();
133    }
134
135    if (format == OutputFormat.DAIKON) {
136      String name1 = var1().name_using(format);
137      String name2 = var2().name_using(format);
138
139      String lexically = (var1().aux.hasOrder() ? " (lexically)" : "");
140      return name1 + " < " + name2 + lexically;
141    }
142
143    if (format == OutputFormat.CSHARPCONTRACT) {
144
145      if (var1().aux.hasOrder()) {
146        String name1 = var1().csharp_collection_string();
147        String name2 = var2().csharp_collection_string();
148        String dbc = "LlexLT".substring(1);
149        return name1 + "." + dbc + "(" + name2 + ")";
150      } else {
151        return "\"SeqComparison.java.jpp: sequence comparison does not apply to unordered collections unimplemented\" != null)"; // interned
152      }
153
154    }
155
156    if (format.isJavaFamily()) {
157      String name1 = var1().name_using(format);
158      String name2 = var2().name_using(format);
159
160      return "daikon.Quant."
161        + (var1().aux.hasOrder() ? "lexLT" : "setEqual" )
162        + "("
163        + name1
164        + ", "
165        + name2
166        + ")";
167
168    }
169
170    return format_unimplemented(format);
171  }
172
173  public String format_simplify(@GuardSatisfied SeqSeqStringLessThan this) {
174    if (Invariant.dkconfig_simplify_define_predicates) {
175      return format_simplify_defined();
176    } else {
177      return format_simplify_explicit();
178    }
179  }
180
181  private String format_simplify_defined(@GuardSatisfied SeqSeqStringLessThan this) {
182    String[] var1_name = var1().simplifyNameAndBounds();
183    String[] var2_name = var2().simplifyNameAndBounds();
184    if (var1_name == null || var2_name == null) {
185      return String.format("%s.format_simplify_defined(%s): var1_name=%s, var2_name=%s, for %s",
186                           getClass().getSimpleName(), this,
187                           Arrays.toString(var1_name), Arrays.toString(var2_name), format());
188    }
189    return "(|lexical-<| "
190      + var1_name[0] + " " + var1_name[1] + " " + var1_name[2] + " "
191      + var2_name[0] + " " + var2_name[1] + " " + var2_name[2] + ")";
192  }
193
194  private String format_simplify_explicit(@GuardSatisfied SeqSeqStringLessThan this) {
195
196      String classname = this.getClass().toString().substring(6);
197      return "warning: method " + classname
198        + ".format_simplify_explicit() needs to be implemented: " + format();
199
200  }
201
202  @Override
203  public InvariantStatus check_modified(
204      String @Interned [] v1, String @Interned [] v2, int count) {
205    /// This does not do the right thing; I really want to avoid comparisons
206    /// if one is missing, but not if one is zero-length.
207    // // Don't make comparisons with empty arrays.
208    // if ((v1.length == 0) || (v2.length == 0)) {
209    //   return;
210    // }
211
212    int comparison = 0;
213    if (orderMatters) {
214      // Standard element wise comparison
215       comparison = comparator.compare(v1, v2);
216    } else {
217      // Do a double subset comparison
218      comparison = (ArraysPlume.isSubset(v1, v2) && ArraysPlume.isSubset( v2, v1)) ? 0 : -1;
219    }
220
221    if (!(comparison < 0) ) {
222      return InvariantStatus.FALSIFIED;
223    }
224    return InvariantStatus.NO_CHANGE;
225  }
226
227  @Override
228  public InvariantStatus add_modified(String @Interned [] v1, String @Interned [] v2, int count) {
229    if (logDetail()) {
230      log("add_modified (%s, %s)", Arrays.toString(v1), Arrays.toString(v2));
231    }
232        return check_modified(v1, v2, count);
233  }
234
235  @Override
236  protected double computeConfidence() {
237
238    return 1 - Math.pow(.5, ppt.num_values());
239  }
240
241  @Pure
242  @Override
243  public boolean isSameFormula(Invariant o) {
244    return true;
245  }
246
247  @Pure
248  @Override
249  public boolean isExclusiveFormula(Invariant o) {
250    return false;
251  }
252
253  /**
254   * Since this invariant can be a postProcessed equality, we have to handle isObvious especially to
255   * avoid circular isObvious relations.
256   */
257  @Pure
258  @Override
259  public @Nullable DiscardInfo isObviousStatically_SomeInEquality() {
260    if (var1().equalitySet == var2().equalitySet) {
261      return isObviousStatically(this.ppt.var_infos);
262    } else {
263      return super.isObviousStatically_SomeInEquality();
264    }
265  }
266
267  /**
268   * Since this invariant can be a postProcessed equality, we have to handle isObvious especially to
269   * avoid circular isObvious relations.
270   */
271  @Pure
272  @Override
273  public @Nullable DiscardInfo isObviousDynamically_SomeInEquality() {
274    if (logOn()) {
275      log("Considering dynamically_someInEquality");
276    }
277    if (var1().equalitySet == var2().equalitySet) {
278      return isObviousDynamically(this.ppt.var_infos);
279    } else {
280      return super.isObviousDynamically_SomeInEquality();
281    }
282  }
283
284  @Pure
285  @Override
286  public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) {
287
288    return super.isObviousStatically(vis);
289  }
290
291  @Pure
292  @Override
293  public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) {
294    DiscardInfo super_result = super.isObviousDynamically(vis);
295    if (super_result != null) {
296      return super_result;
297    }
298    assert ppt != null;
299
300    return null;
301  }
302
303  @Override
304  public void repCheck() {
305    super.repCheck();
306    /*
307      This code is no longer needed now that the can_be_x's are gone
308    if (!(this.can_be_eq || this.can_be_lt || this.can_be_gt)
309        && ppt.num_samples() != 0) {
310      System.err.println(this.repr());
311      System.err.println(this.ppt.num_samples());
312      throw new Error();
313    }
314    */
315  }
316
317  @Pure
318  public boolean isEqual() {
319
320    return false;
321  }
322
323  // Look up a previously instantiated invariant.
324  public static @Nullable SeqSeqStringLessThan find(PptSlice ppt) {
325    assert ppt.arity() == 2;
326    for (Invariant inv : ppt.invs) {
327      if (inv instanceof SeqSeqStringLessThan) {
328        return (SeqSeqStringLessThan) 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    private static @Nullable NISuppressionSet suppressions = null;
342
343  @Override
344  public @Nullable @NonPrototype SeqSeqStringLessThan merge(
345      @Prototype SeqSeqStringLessThan this, List<@NonPrototype Invariant> invs, PptSlice parent_ppt) {
346    // Ignore the orderMatters field, because it is always the same (and is always true).
347    return (SeqSeqStringLessThan) super.merge(invs, parent_ppt);
348  }
349}