Source code

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