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