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 &gt; between two String scalars. Prints as {@code x > y}.
030 */
031public final class StringGreaterThan 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 StringGreaterThan 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.StringGreaterThan");
041
042  StringGreaterThan(PptSlice ppt) {
043    super(ppt);
044  }
045
046  @Prototype StringGreaterThan() {
047    super();
048  }
049
050  private static @Prototype StringGreaterThan proto = new @Prototype StringGreaterThan();
051
052  /** Returns the prototype invariant for StringGreaterThan. */
053  public static @Prototype StringGreaterThan 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 StringGreaterThan. */
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("StringGreaterThan.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 StringGreaterThan instantiate_dyn(@Prototype StringGreaterThan this, PptSlice slice) {
081
082    return new StringGreaterThan(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      StringLessThan result = new StringLessThan(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 StringLessThan.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 StringGreaterThan relationship.
103  // Should this implementation be made more efficient?
104  public static @Nullable StringGreaterThan find(PptSlice ppt) {
105    assert ppt.arity() == 2;
106    for (Invariant inv : ppt.invs) {
107      if (inv instanceof StringGreaterThan) {
108        return (StringGreaterThan) inv;
109      }
110    }
111
112    // If the invariant is suppressed, create it
113    if ((suppressions != null) && suppressions.suppressed(ppt)) {
114      StringGreaterThan 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 StringGreaterThan this) {
124    return "StringGreaterThan" + varNames();
125  }
126
127  @SideEffectFree
128  @Override
129  public String format_using(@GuardSatisfied StringGreaterThan 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    if (format.isJavaFamily()) {
145
146        return var1name + ".compareTo(" + var2name +") > 0";
147
148    }
149
150    if (format == OutputFormat.SIMPLIFY) {
151
152        String comparator = ">";
153
154      return "("
155          + comparator
156          + " "
157          + var1().simplifyFixup(var1name)
158          + " "
159          + var2().simplifyFixup(var2name)
160          + ")";
161    }
162
163    return format_unimplemented(format);
164  }
165
166  @Override
167  public InvariantStatus check_modified(@Interned String v1, @Interned String v2, int count) {
168    if (!((v1 != null) && ( v2 != null) && (v1.compareTo( v2) > 0))) {
169      return InvariantStatus.FALSIFIED;
170    }
171    return InvariantStatus.NO_CHANGE;
172  }
173
174  @Override
175  public InvariantStatus add_modified(@Interned String v1, @Interned String v2, int count) {
176    if (logDetail() || debug.isLoggable(Level.FINE)) {
177      log(
178          debug,
179          "add_modified (" + v1 + ", " + v2 + ",  ppt.num_values = " + ppt.num_values() + ")");
180    }
181    if ((logOn() || debug.isLoggable(Level.FINE))
182        && check_modified(v1, v2, count) == InvariantStatus.FALSIFIED)
183      log(debug, "destroy in add_modified (" + v1 + ", " + v2 + ",  " + count + ")");
184
185    return check_modified(v1, v2, count);
186  }
187
188  // This is very tricky, because whether two variables are equal should
189  // presumably be transitive, but it's not guaranteed to be so when using
190  // this method and not dropping out all variables whose values are ever
191  // missing.
192  @Override
193  protected double computeConfidence() {
194    // Should perhaps check number of samples and be unjustified if too few
195    // samples.
196
197      // // The reason for this multiplication is that there might be only a
198      // // very few possible values.  Example:  towers of hanoi has only 6
199      // // possible (pegA, pegB) pairs.
200      // return 1 - (Math.pow(.5, ppt.num_values())
201      //             * Math.pow(.99, ppt.num_mod_samples()));
202      return 1 - Math.pow(.5, ppt.num_samples());
203  }
204
205  @Pure
206  @Override
207  public boolean isExact() {
208
209      return false;
210  }
211
212  // // Temporary, for debugging
213  // public void destroy() {
214  //   if (debug.isLoggable(Level.FINE)) {
215  //     System.out.println("StringGreaterThan.destroy(" + ppt.name() + ")");
216  //     System.out.println(repr());
217  //     (new Error()).printStackTrace();
218  //   }
219  //   super.destroy();
220  // }
221
222  @Override
223  public InvariantStatus add(
224      @Interned Object v1, @Interned Object v2, int mod_index, int count) {
225    if (debug.isLoggable(Level.FINE)) {
226      debug.fine(
227          "StringGreaterThan"
228          + ppt.varNames()
229          + ".add("
230          + v1
231          + ","
232          + v2
233          + ", mod_index="
234          + mod_index
235          + "), count="
236          + count
237          + ")");
238    }
239    return super.add(v1, v2, mod_index, count);
240  }
241
242  @Pure
243  @Override
244  public boolean isSameFormula(Invariant other) {
245    return true;
246  }
247
248  @Pure
249  @Override
250  public boolean isExclusiveFormula(Invariant other) {
251
252    // Also ought to check against LinearBinary, etc.
253
254      if ((other instanceof StringLessThan)
255          || (other instanceof StringLessEqual)
256          || (other instanceof StringEqual))
257        return true;
258
259    return false;
260  }
261
262  @Override
263  public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) {
264    final VarInfo var1 = vis[0];
265    final VarInfo var2 = vis[1];
266
267    if (var1.aux.hasValue(VarInfoAux.MINIMUM_VALUE)
268        && var2.aux.hasValue(VarInfoAux.MAXIMUM_VALUE)) {
269      int maxB = var2.aux.getInt(VarInfoAux.MAXIMUM_VALUE),
270          minA = var1.aux.getInt(VarInfoAux.MINIMUM_VALUE);
271
272      if (minA > maxB) {
273        return new DiscardInfo(
274            this,
275            DiscardCode.obvious,
276            var1.name() + " DISCARD_OP " + var2.name() + " is already known");
277      }
278    }
279
280    return super.isObviousStatically(vis);
281  }
282
283  @Pure
284  @Override
285  public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) {
286
287    // JHP: We might consider adding a check over bounds.   If
288    // x < c and y > c then we know that x < y.  Similarly for
289    // x > c and y < c.  We could also substitute oneof for
290    // one or both of the bound checks.
291
292    DiscardInfo super_result = super.isObviousDynamically(vis);
293    if (super_result != null) {
294      return super_result;
295    }
296
297    @SuppressWarnings("UnusedVariable") // generated code, variable is sometimes used
298    DiscardInfo di;
299
300    return null;
301  } // isObviousDynamically
302
303  /** NI suppressions, initialized in get_ni_suppressions() */
304  private static @Nullable NISuppressionSet suppressions = null;
305
306  /** Returns the non-instantiating suppressions for this invariant. */
307  @Pure
308  @Override
309  public @Nullable NISuppressionSet get_ni_suppressions() {
310    return null;
311  }
312
313}