Source code

001// ***** This file is automatically generated from IntComparisons.java.jpp
002
003package daikon.inv.binary.twoScalar;
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 double scalars. Prints as {@code x >= y}.
030 */
031public final class FloatGreaterEqual extends TwoFloat {
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 FloatGreaterEqual 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.FloatGreaterEqual");
041
042  FloatGreaterEqual(PptSlice ppt) {
043    super(ppt);
044  }
045
046  @Prototype FloatGreaterEqual() {
047    super();
048  }
049
050  private static @Prototype FloatGreaterEqual proto = new @Prototype FloatGreaterEqual();
051
052  /** Returns the prototype invariant for FloatGreaterEqual. */
053  public static @Prototype FloatGreaterEqual 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 FloatGreaterEqual. */
063  @Override
064  public boolean instantiate_ok(VarInfo[] vis) {
065
066    if (!valid_types(vis)) {
067      return false;
068    }
069
070      return true;
071  }
072
073  @Override
074  protected FloatGreaterEqual instantiate_dyn(@Prototype FloatGreaterEqual this, PptSlice slice) {
075
076    return new FloatGreaterEqual(slice);
077  }
078
079  @Override
080  protected Invariant resurrect_done_swapped() {
081
082      // we have no non-static member data, so we only need care about our type
083      // As of now, the constructor chain is side-effect free;
084      // let's hope it stays that way.
085      FloatLessEqual result = new FloatLessEqual(ppt);
086      return result;
087  }
088
089  /** Returns the class that corresponds to this class with its variable order swapped. */
090  public static Class<? extends Invariant> swap_class() {
091    return FloatLessEqual.class;
092  }
093
094  // JHP: this should be removed in favor of checks in PptTopLevel
095  // such as is_equal, is_lessequal, etc.
096  // Look up a previously instantiated FloatGreaterEqual relationship.
097  // Should this implementation be made more efficient?
098  public static @Nullable FloatGreaterEqual find(PptSlice ppt) {
099    assert ppt.arity() == 2;
100    for (Invariant inv : ppt.invs) {
101      if (inv instanceof FloatGreaterEqual) {
102        return (FloatGreaterEqual) inv;
103      }
104    }
105
106    // If the invariant is suppressed, create it
107    if ((suppressions != null) && suppressions.suppressed(ppt)) {
108      FloatGreaterEqual inv = proto.instantiate_dyn(ppt);
109      // System.out.printf("%s is suppressed in ppt %s%n", inv.format(), ppt.name());
110      return inv;
111    }
112
113    return null;
114  }
115
116  @Override
117  public String repr(@GuardSatisfied FloatGreaterEqual this) {
118    return "FloatGreaterEqual" + varNames();
119  }
120
121  @SideEffectFree
122  @Override
123  public String format_using(@GuardSatisfied FloatGreaterEqual this, OutputFormat format) {
124
125    String var1name = var1().name_using(format);
126    String var2name = var2().name_using(format);
127
128    if ((format == OutputFormat.DAIKON) || (format == OutputFormat.ESCJAVA)) {
129      String comparator = ">=";
130      return var1name + " " + comparator + " " + var2name;
131    }
132
133    if (format == OutputFormat.CSHARPCONTRACT) {
134
135        String comparator = ">=";
136        return var1name + " " + comparator + " " + var2name;
137    }
138
139    if (format.isJavaFamily()) {
140
141        return Invariant.formatFuzzy("gte", var1(), var2(), format);
142
143    }
144
145    if (format == OutputFormat.SIMPLIFY) {
146
147        String comparator = ">=";
148
149      return "("
150          + comparator
151          + " "
152          + var1().simplifyFixup(var1name)
153          + " "
154          + var2().simplifyFixup(var2name)
155          + ")";
156    }
157
158    return format_unimplemented(format);
159  }
160
161  @Override
162  public InvariantStatus check_modified(double v1, double v2, int count) {
163    if (!Global.fuzzy.gte(v1, v2)) {
164      return InvariantStatus.FALSIFIED;
165    }
166    return InvariantStatus.NO_CHANGE;
167  }
168
169  @Override
170  public InvariantStatus add_modified(double v1, double v2, int count) {
171    if (logDetail() || debug.isLoggable(Level.FINE)) {
172      log(
173          debug,
174          "add_modified (" + v1 + ", " + v2 + ",  ppt.num_values = " + ppt.num_values() + ")");
175    }
176    if ((logOn() || debug.isLoggable(Level.FINE))
177        && check_modified(v1, v2, count) == InvariantStatus.FALSIFIED)
178      log(debug, "destroy in add_modified (" + v1 + ", " + v2 + ",  " + count + ")");
179
180    return check_modified(v1, v2, count);
181  }
182
183  // This is very tricky, because whether two variables are equal should
184  // presumably be transitive, but it's not guaranteed to be so when using
185  // this method and not dropping out all variables whose values are ever
186  // missing.
187  @Override
188  protected double computeConfidence() {
189    // Should perhaps check number of samples and be unjustified if too few
190    // samples.
191
192      // // The reason for this multiplication is that there might be only a
193      // // very few possible values.  Example:  towers of hanoi has only 6
194      // // possible (pegA, pegB) pairs.
195      // return 1 - (Math.pow(.5, ppt.num_values())
196      //             * Math.pow(.99, ppt.num_mod_samples()));
197      return 1 - Math.pow(.5, ppt.num_samples());
198  }
199
200  @Pure
201  @Override
202  public boolean isExact() {
203
204      return false;
205  }
206
207  // // Temporary, for debugging
208  // public void destroy() {
209  //   if (debug.isLoggable(Level.FINE)) {
210  //     System.out.println("FloatGreaterEqual.destroy(" + ppt.name() + ")");
211  //     System.out.println(repr());
212  //     (new Error()).printStackTrace();
213  //   }
214  //   super.destroy();
215  // }
216
217  @Override
218  public InvariantStatus add(
219      @Interned Object v1, @Interned Object v2, int mod_index, int count) {
220    if (debug.isLoggable(Level.FINE)) {
221      debug.fine(
222          "FloatGreaterEqual"
223          + ppt.varNames()
224          + ".add("
225          + v1
226          + ","
227          + v2
228          + ", mod_index="
229          + mod_index
230          + "), count="
231          + count
232          + ")");
233    }
234    return super.add(v1, v2, mod_index, count);
235  }
236
237  @Pure
238  @Override
239  public boolean isSameFormula(Invariant other) {
240    return true;
241  }
242
243  @Pure
244  @Override
245  public boolean isExclusiveFormula(Invariant other) {
246
247    // Also ought to check against LinearBinary, etc.
248
249      if (other instanceof FloatLessThan) {
250        return true;
251      }
252
253    return false;
254  }
255
256  @Override
257  public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) {
258    final VarInfo var1 = vis[0];
259    final VarInfo var2 = vis[1];
260
261    if (var1.aux.hasValue(VarInfoAux.MINIMUM_VALUE)
262        && var2.aux.hasValue(VarInfoAux.MAXIMUM_VALUE)) {
263      int maxB = var2.aux.getInt(VarInfoAux.MAXIMUM_VALUE),
264          minA = var1.aux.getInt(VarInfoAux.MINIMUM_VALUE);
265
266      if (minA >= maxB) {
267        return new DiscardInfo(
268            this,
269            DiscardCode.obvious,
270            var1.name() + " DISCARD_OP " + var2.name() + " is already known");
271      }
272    }
273
274    return super.isObviousStatically(vis);
275  }
276
277  @Pure
278  @Override
279  public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) {
280
281    // JHP: We might consider adding a check over bounds.   If
282    // x < c and y > c then we know that x < y.  Similarly for
283    // x > c and y < c.  We could also substitute oneof for
284    // one or both of the bound checks.
285
286    DiscardInfo super_result = super.isObviousDynamically(vis);
287    if (super_result != null) {
288      return super_result;
289    }
290
291    VarInfo var1 = vis[0];
292    VarInfo var2 = vis[1];
293
294    @SuppressWarnings("UnusedVariable") // generated code, variable is sometimes used
295    DiscardInfo di;
296
297      // Check for the same invariant over enclosing arrays
298      di = pairwise_implies(vis);
299      if (di != null) {
300        return di;
301      }
302
303    { // Sequence length tests
304      SequenceLength sl1 = null;
305      if (var1.isDerived() && (var1.derived instanceof SequenceLength)) {
306        sl1 = (SequenceLength) var1.derived;
307      }
308      SequenceLength sl2 = null;
309      if (var2.isDerived() && (var2.derived instanceof SequenceLength)) {
310        sl2 = (SequenceLength) var2.derived;
311      }
312
313      // "size(a)-1 cmp size(b)-1" is never even instantiated;
314      // use "size(a) cmp size(b)" instead.
315
316      // This might never get invoked, as equality is printed out specially.
317      VarInfo s1 = (sl1 == null) ? null : sl1.base;
318      VarInfo s2 = (sl2 == null) ? null : sl2.base;
319      if ((s1 != null) && (s2 != null) && (s1.equalitySet == s2.equalitySet)) {
320        // lengths of equal arrays being compared
321        String n1 = var1.name();
322        String n2 = var2.name();
323        return new DiscardInfo(
324            this,
325            DiscardCode.obvious,
326            n1 + " and " + n2 + " are equal arrays, so equal size is implied");
327      }
328
329    }
330
331    return null;
332  } // isObviousDynamically
333
334  /**
335   * If both variables are subscripts and the underlying arrays have the same invariant, then this
336   * invariant is implied:
337   *
338   * <pre>(x[] op y[]) ^ (i == j) &rArr; (x[i] op y[j])</pre>
339   */
340  private @Nullable DiscardInfo pairwise_implies(VarInfo[] vis) {
341
342    VarInfo v1 = vis[0];
343    VarInfo v2 = vis[1];
344
345    // Make sure v1 and v2 are SequenceFloatSubscript with the same shift
346    if (!v1.isDerived() || !(v1.derived instanceof SequenceFloatSubscript)) {
347      return null;
348    }
349    if (!v2.isDerived() || !(v2.derived instanceof SequenceFloatSubscript)) {
350      return null;
351    }
352    @NonNull SequenceFloatSubscript der1 = (SequenceFloatSubscript) v1.derived;
353    @NonNull SequenceFloatSubscript der2 = (SequenceFloatSubscript) v2.derived;
354    if (der1.index_shift != der2.index_shift) {
355      return null;
356    }
357
358    // Make sure that the indices are equal
359    if (!ppt.parent.is_equal(der1.sclvar().canonicalRep(), der2.sclvar().canonicalRep())) {
360      return null;
361    }
362
363    // See if the same relationship holds over the arrays
364    Invariant proto = PairwiseFloatGreaterEqual.get_proto();
365    DiscardInfo di = ppt.parent.check_implied_canonical(this, der1.seqvar(), der2.seqvar(), proto);
366    return di;
367  }
368
369  /** NI suppressions, initialized in get_ni_suppressions() */
370  private static @Nullable NISuppressionSet suppressions = null;
371
372  /** Returns the non-instantiating suppressions for this invariant. */
373  @Pure
374  @Override
375  public NISuppressionSet get_ni_suppressions() {
376    if (suppressions == null) {
377
378        NISuppressee suppressee = new NISuppressee(FloatGreaterEqual.class, 2);
379
380      // suppressor definitions (used in suppressions below)
381
382      NISuppressor v1_eq_v2 = new NISuppressor(0, 1, FloatEqual.class);
383
384      NISuppressor v1_gt_v2 = new NISuppressor(0, 1, FloatGreaterThan.class);
385
386      suppressions =
387          new NISuppressionSet(
388              new NISuppression[] {
389
390                  // v1 == v2 => v1 >= v2
391                  new NISuppression(v1_eq_v2, suppressee),
392                  // v1 > v2 => v1 >= v2
393                  new NISuppression(v1_gt_v2, suppressee),
394
395              });
396    }
397    return suppressions;
398  }
399
400}