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