Source code

001// ***** This file is automatically generated from IntComparisons.java.jpp
002
003package daikon.inv.binary.twoString;
004
005import daikon.*;
006import daikon.derive.binary.*;
007import daikon.derive.unary.*;
008import daikon.inv.*;
009import daikon.inv.binary.twoScalar.*;
010import daikon.inv.binary.twoSequence.*;
011import daikon.inv.unary.scalar.*;
012import daikon.inv.unary.sequence.*;
013import daikon.inv.unary.string.*;
014import daikon.suppress.*;
015import java.util.*;
016import java.util.logging.Level;
017import java.util.logging.Logger;
018import org.checkerframework.checker.interning.qual.Interned;
019import org.checkerframework.checker.lock.qual.GuardSatisfied;
020import org.checkerframework.checker.nullness.qual.NonNull;
021import org.checkerframework.checker.nullness.qual.Nullable;
022import org.checkerframework.dataflow.qual.Pure;
023import org.checkerframework.dataflow.qual.SideEffectFree;
024import org.plumelib.util.Intern;
025import typequals.prototype.qual.NonPrototype;
026import typequals.prototype.qual.Prototype;
027
028/**
029 * Represents an invariant of &lt; between two String scalars. Prints as {@code x < y}.
030 */
031public final class StringLessThan extends TwoString {
032
033  static final long serialVersionUID = 20030822L;
034
035  // Variables starting with dkconfig_ should only be set via the
036  // daikon.config.Configuration interface.
037  /** Boolean. True iff StringLessThan invariants should be considered. */
038  public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault;
039
040  public static final Logger debug = Logger.getLogger("daikon.inv.binary.twoScalar.StringLessThan");
041
042  StringLessThan(PptSlice ppt) {
043    super(ppt);
044  }
045
046  @Prototype StringLessThan() {
047    super();
048  }
049
050  private static @Prototype StringLessThan proto = new @Prototype StringLessThan();
051
052  /** Returns the prototype invariant for StringLessThan. */
053  public static @Prototype StringLessThan get_proto() {
054    return proto;
055  }
056
057  @Override
058  public boolean enabled() {
059    return dkconfig_enabled;
060  }
061
062  /** Returns whether or not the specified var types are valid for StringLessThan. */
063  @Override
064  public boolean instantiate_ok(VarInfo[] vis) {
065
066    if (!valid_types(vis)) {
067      return false;
068    }
069
070        boolean result = !(vis[0].has_typeof() || vis[1].has_typeof());
071        // System.out.printf("StringLessThan.instantiate_ok(");
072        // for (VarInfo vi : vis) {
073        //   System.out.printf("%s ", vi.name());
074        // }
075        // System.out.printf(") => %s%n", result);
076        return result;
077  }
078
079  @Override
080  protected StringLessThan instantiate_dyn(@Prototype StringLessThan this, PptSlice slice) {
081
082    return new StringLessThan(slice);
083  }
084
085  @Override
086  protected Invariant resurrect_done_swapped() {
087
088      // we have no non-static member data, so we only need care about our type
089      // As of now, the constructor chain is side-effect free;
090      // let's hope it stays that way.
091      StringGreaterThan result = new StringGreaterThan(ppt);
092      return result;
093  }
094
095  /** Returns the class that corresponds to this class with its variable order swapped. */
096  public static Class<? extends Invariant> swap_class() {
097    return StringGreaterThan.class;
098  }
099
100  // JHP: this should be removed in favor of checks in PptTopLevel
101  // such as is_equal, is_lessequal, etc.
102  // Look up a previously instantiated StringLessThan relationship.
103  // Should this implementation be made more efficient?
104  public static @Nullable StringLessThan find(PptSlice ppt) {
105    assert ppt.arity() == 2;
106    for (Invariant inv : ppt.invs) {
107      if (inv instanceof StringLessThan) {
108        return (StringLessThan) inv;
109      }
110    }
111
112    // If the invariant is suppressed, create it
113    if ((suppressions != null) && suppressions.suppressed(ppt)) {
114      StringLessThan inv = proto.instantiate_dyn(ppt);
115      // System.out.printf("%s is suppressed in ppt %s%n", inv.format(), ppt.name());
116      return inv;
117    }
118
119    return null;
120  }
121
122  @Override
123  public String repr(@GuardSatisfied StringLessThan this) {
124    return "StringLessThan" + varNames();
125  }
126
127  @SideEffectFree
128  @Override
129  public String format_using(@GuardSatisfied StringLessThan this, OutputFormat format) {
130
131    String var1name = var1().name_using(format);
132    String var2name = var2().name_using(format);
133
134    if ((format == OutputFormat.DAIKON) || (format == OutputFormat.ESCJAVA)) {
135      String comparator = "<";
136      return var1name + " " + comparator + " " + var2name;
137    }
138
139    if (format == OutputFormat.CSHARPCONTRACT) {
140
141        return var1name + ".CompareTo(" + var2name +") < 0";
142
143    }
144
145    if (format.isJavaFamily()) {
146
147        return var1name + ".compareTo(" + var2name +") < 0";
148
149    }
150
151    if (format == OutputFormat.SIMPLIFY) {
152
153        String comparator = "<";
154
155      return "("
156          + comparator
157          + " "
158          + var1().simplifyFixup(var1name)
159          + " "
160          + var2().simplifyFixup(var2name)
161          + ")";
162    }
163
164    return format_unimplemented(format);
165  }
166
167  @Override
168  public InvariantStatus check_modified(@Interned String v1, @Interned String v2, int count) {
169    if (!((v1 != null) && ( v2 != null) && (v1.compareTo( v2) < 0))) {
170      return InvariantStatus.FALSIFIED;
171    }
172    return InvariantStatus.NO_CHANGE;
173  }
174
175  @Override
176  public InvariantStatus add_modified(@Interned String v1, @Interned String v2, int count) {
177    if (logDetail() || debug.isLoggable(Level.FINE)) {
178      log(
179          debug,
180          "add_modified (" + v1 + ", " + v2 + ",  ppt.num_values = " + ppt.num_values() + ")");
181    }
182    if ((logOn() || debug.isLoggable(Level.FINE))
183        && check_modified(v1, v2, count) == InvariantStatus.FALSIFIED)
184      log(debug, "destroy in add_modified (" + v1 + ", " + v2 + ",  " + count + ")");
185
186    return check_modified(v1, v2, count);
187  }
188
189  // This is very tricky, because whether two variables are equal should
190  // presumably be transitive, but it's not guaranteed to be so when using
191  // this method and not dropping out all variables whose values are ever
192  // missing.
193  @Override
194  protected double computeConfidence() {
195    // Should perhaps check number of samples and be unjustified if too few
196    // samples.
197
198      // // The reason for this multiplication is that there might be only a
199      // // very few possible values.  Example:  towers of hanoi has only 6
200      // // possible (pegA, pegB) pairs.
201      // return 1 - (Math.pow(.5, ppt.num_values())
202      //             * Math.pow(.99, ppt.num_mod_samples()));
203      return 1 - Math.pow(.5, ppt.num_samples());
204  }
205
206  @Pure
207  @Override
208  public boolean isExact() {
209
210      return false;
211  }
212
213  // // Temporary, for debugging
214  // public void destroy() {
215  //   if (debug.isLoggable(Level.FINE)) {
216  //     System.out.println("StringLessThan.destroy(" + ppt.name() + ")");
217  //     System.out.println(repr());
218  //     (new Error()).printStackTrace();
219  //   }
220  //   super.destroy();
221  // }
222
223  @Override
224  public InvariantStatus add(
225      @Interned Object v1, @Interned Object v2, int mod_index, int count) {
226    if (debug.isLoggable(Level.FINE)) {
227      debug.fine(
228          "StringLessThan"
229          + ppt.varNames()
230          + ".add("
231          + v1
232          + ","
233          + v2
234          + ", mod_index="
235          + mod_index
236          + "), count="
237          + count
238          + ")");
239    }
240    return super.add(v1, v2, mod_index, count);
241  }
242
243  @Pure
244  @Override
245  public boolean isSameFormula(Invariant other) {
246    return true;
247  }
248
249  @Pure
250  @Override
251  public boolean isExclusiveFormula(Invariant other) {
252
253    // Also ought to check against LinearBinary, etc.
254
255        if ((other instanceof StringEqual)
256            || (other instanceof StringGreaterEqual)
257            || (other instanceof StringGreaterThan))
258          return true;
259
260    return false;
261  }
262
263  @Override
264  public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) {
265    final VarInfo var1 = vis[0];
266    final VarInfo var2 = vis[1];
267
268    if (var1.aux.hasValue(VarInfoAux.MAXIMUM_VALUE)
269        && var2.aux.hasValue(VarInfoAux.MINIMUM_VALUE)) {
270      int maxA = var1.aux.getInt(VarInfoAux.MAXIMUM_VALUE),
271          minB = var2.aux.getInt(VarInfoAux.MINIMUM_VALUE);
272
273      if (maxA < minB) {
274        return new DiscardInfo(
275            this,
276            DiscardCode.obvious,
277            var1.name() + " DISCARD_OP " + var2.name() + " is already known");
278      }
279    }
280
281    return super.isObviousStatically(vis);
282  }
283
284  @Pure
285  @Override
286  public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) {
287
288    // JHP: We might consider adding a check over bounds.   If
289    // x < c and y > c then we know that x < y.  Similarly for
290    // x > c and y < c.  We could also substitute oneof for
291    // one or both of the bound checks.
292
293    DiscardInfo super_result = super.isObviousDynamically(vis);
294    if (super_result != null) {
295      return super_result;
296    }
297
298    @SuppressWarnings("UnusedVariable") // generated code, variable is sometimes used
299    DiscardInfo di;
300
301    return null;
302  } // isObviousDynamically
303
304  /** NI suppressions, initialized in get_ni_suppressions() */
305  private static @Nullable NISuppressionSet suppressions = null;
306
307  /** Returns the non-instantiating suppressions for this invariant. */
308  @Pure
309  @Override
310  public @Nullable NISuppressionSet get_ni_suppressions() {
311    return null;
312  }
313
314}