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 &ge; between two String scalars. Prints as {@code x >= y}.
030 */
031public final class StringGreaterEqual 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 StringGreaterEqual 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.StringGreaterEqual");
041
042  StringGreaterEqual(PptSlice ppt) {
043    super(ppt);
044  }
045
046  @Prototype StringGreaterEqual() {
047    super();
048  }
049
050  private static @Prototype StringGreaterEqual proto = new @Prototype StringGreaterEqual();
051
052  /** Returns the prototype invariant for StringGreaterEqual. */
053  public static @Prototype StringGreaterEqual 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 StringGreaterEqual. */
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("StringGreaterEqual.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 StringGreaterEqual instantiate_dyn(@Prototype StringGreaterEqual this, PptSlice slice) {
081
082    return new StringGreaterEqual(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      StringLessEqual result = new StringLessEqual(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 StringLessEqual.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 StringGreaterEqual relationship.
103  // Should this implementation be made more efficient?
104  public static @Nullable StringGreaterEqual find(PptSlice ppt) {
105    assert ppt.arity() == 2;
106    for (Invariant inv : ppt.invs) {
107      if (inv instanceof StringGreaterEqual) {
108        return (StringGreaterEqual) inv;
109      }
110    }
111
112    // If the invariant is suppressed, create it
113    if ((suppressions != null) && suppressions.suppressed(ppt)) {
114      StringGreaterEqual 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 StringGreaterEqual this) {
124    return "StringGreaterEqual" + varNames();
125  }
126
127  @SideEffectFree
128  @Override
129  public String format_using(@GuardSatisfied StringGreaterEqual 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      // Integer and float cases:
143
144    }
145
146    if (format.isJavaFamily()) {
147
148        return var1name + ".compareTo(" + var2name +") >= 0";
149
150    }
151
152    if (format == OutputFormat.SIMPLIFY) {
153
154        String comparator = ">=";
155
156      return "("
157          + comparator
158          + " "
159          + var1().simplifyFixup(var1name)
160          + " "
161          + var2().simplifyFixup(var2name)
162          + ")";
163    }
164
165    return format_unimplemented(format);
166  }
167
168  @Override
169  public InvariantStatus check_modified(@Interned String v1, @Interned String v2, int count) {
170    if (!((v1 != null) && ( v2 != null) && (v1.compareTo( v2) >= 0))) {
171      return InvariantStatus.FALSIFIED;
172    }
173    return InvariantStatus.NO_CHANGE;
174  }
175
176  @Override
177  public InvariantStatus add_modified(@Interned String v1, @Interned String v2, int count) {
178    if (logDetail() || debug.isLoggable(Level.FINE)) {
179      log(
180          debug,
181          "add_modified (" + v1 + ", " + v2 + ",  ppt.num_values = " + ppt.num_values() + ")");
182    }
183    if ((logOn() || debug.isLoggable(Level.FINE))
184        && check_modified(v1, v2, count) == InvariantStatus.FALSIFIED)
185      log(debug, "destroy in add_modified (" + v1 + ", " + v2 + ",  " + count + ")");
186
187    return check_modified(v1, v2, count);
188  }
189
190  // This is very tricky, because whether two variables are equal should
191  // presumably be transitive, but it's not guaranteed to be so when using
192  // this method and not dropping out all variables whose values are ever
193  // missing.
194  @Override
195  protected double computeConfidence() {
196    // Should perhaps check number of samples and be unjustified if too few
197    // samples.
198
199      // // The reason for this multiplication is that there might be only a
200      // // very few possible values.  Example:  towers of hanoi has only 6
201      // // possible (pegA, pegB) pairs.
202      // return 1 - (Math.pow(.5, ppt.num_values())
203      //             * Math.pow(.99, ppt.num_mod_samples()));
204      return 1 - Math.pow(.5, ppt.num_samples());
205  }
206
207  @Pure
208  @Override
209  public boolean isExact() {
210
211      return false;
212  }
213
214  // // Temporary, for debugging
215  // public void destroy() {
216  //   if (debug.isLoggable(Level.FINE)) {
217  //     System.out.println("StringGreaterEqual.destroy(" + ppt.name() + ")");
218  //     System.out.println(repr());
219  //     (new Error()).printStackTrace();
220  //   }
221  //   super.destroy();
222  // }
223
224  @Override
225  public InvariantStatus add(
226      @Interned Object v1, @Interned Object v2, int mod_index, int count) {
227    if (debug.isLoggable(Level.FINE)) {
228      debug.fine(
229          "StringGreaterEqual"
230          + ppt.varNames()
231          + ".add("
232          + v1
233          + ","
234          + v2
235          + ", mod_index="
236          + mod_index
237          + "), count="
238          + count
239          + ")");
240    }
241    return super.add(v1, v2, mod_index, count);
242  }
243
244  @Pure
245  @Override
246  public boolean isSameFormula(Invariant other) {
247    return true;
248  }
249
250  @Pure
251  @Override
252  public boolean isExclusiveFormula(Invariant other) {
253
254    // Also ought to check against LinearBinary, etc.
255
256      if (other instanceof StringLessThan) {
257        return true;
258      }
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.MINIMUM_VALUE)
269        && var2.aux.hasValue(VarInfoAux.MAXIMUM_VALUE)) {
270      int maxB = var2.aux.getInt(VarInfoAux.MAXIMUM_VALUE),
271          minA = var1.aux.getInt(VarInfoAux.MINIMUM_VALUE);
272
273      if (minA >= maxB) {
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 NISuppressionSet get_ni_suppressions() {
311    if (suppressions == null) {
312
313        NISuppressee suppressee = new NISuppressee(StringGreaterEqual.class, 2);
314
315      // suppressor definitions (used in suppressions below)
316
317      NISuppressor v1_eq_v2 = new NISuppressor(0, 1, StringEqual.class);
318
319      NISuppressor v1_gt_v2 = new NISuppressor(0, 1, StringGreaterThan.class);
320
321      suppressions =
322          new NISuppressionSet(
323              new NISuppression[] {
324
325                  // v1 == v2 => v1 >= v2
326                  new NISuppression(v1_eq_v2, suppressee),
327                  // v1 > v2 => v1 >= v2
328                  new NISuppression(v1_gt_v2, suppressee),
329
330              });
331    }
332    return suppressions;
333  }
334
335}