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