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 &le; between two String scalars. Prints as {@code x <= y}.
030 */
031public final class StringLessEqual 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 StringLessEqual 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.StringLessEqual");
041
042  StringLessEqual(PptSlice ppt) {
043    super(ppt);
044  }
045
046  @Prototype StringLessEqual() {
047    super();
048  }
049
050  private static @Prototype StringLessEqual proto = new @Prototype StringLessEqual();
051
052  /** Returns the prototype invariant for StringLessEqual. */
053  public static @Prototype StringLessEqual 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 StringLessEqual. */
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("StringLessEqual.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 StringLessEqual instantiate_dyn(@Prototype StringLessEqual this, PptSlice slice) {
081
082    return new StringLessEqual(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      StringGreaterEqual result = new StringGreaterEqual(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 StringGreaterEqual.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 StringLessEqual relationship.
103  // Should this implementation be made more efficient?
104  public static @Nullable StringLessEqual find(PptSlice ppt) {
105    assert ppt.arity() == 2;
106    for (Invariant inv : ppt.invs) {
107      if (inv instanceof StringLessEqual) {
108        return (StringLessEqual) inv;
109      }
110    }
111
112    // If the invariant is suppressed, create it
113    if ((suppressions != null) && suppressions.suppressed(ppt)) {
114      StringLessEqual 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 StringLessEqual this) {
124    return "StringLessEqual" + varNames();
125  }
126
127  @SideEffectFree
128  @Override
129  public String format_using(@GuardSatisfied StringLessEqual 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("StringLessEqual.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          "StringLessEqual"
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 StringGreaterThan) {
256        return true;
257      }
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.MAXIMUM_VALUE)
268        && var2.aux.hasValue(VarInfoAux.MINIMUM_VALUE)) {
269      int maxA = var1.aux.getInt(VarInfoAux.MAXIMUM_VALUE),
270          minB = var2.aux.getInt(VarInfoAux.MINIMUM_VALUE);
271
272      if (maxA <= minB) {
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 NISuppressionSet get_ni_suppressions() {
310    if (suppressions == null) {
311
312        NISuppressee suppressee = new NISuppressee(StringLessEqual.class, 2);
313
314      // suppressor definitions (used in suppressions below)
315
316      NISuppressor v1_eq_v2 = new NISuppressor(0, 1, StringEqual.class);
317
318      NISuppressor v1_lt_v2 = new NISuppressor(0, 1, StringLessThan.class);
319
320      suppressions =
321          new NISuppressionSet(
322              new NISuppression[] {
323
324                  // v1 == v2 => v1 <= v2
325                  new NISuppression(v1_eq_v2, suppressee),
326                  // v1 < v2 => v1 <= v2
327                  new NISuppression(v1_lt_v2, suppressee),
328
329              });
330    }
331    return suppressions;
332  }
333
334}