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 != between two String scalars. Prints as {@code x != y}.
030 */
031public final class StringNonEqual 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 StringNonEqual 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.StringNonEqual");
041
042  StringNonEqual(PptSlice ppt) {
043    super(ppt);
044  }
045
046  @Prototype StringNonEqual() {
047    super();
048  }
049
050  private static @Prototype StringNonEqual proto = new @Prototype StringNonEqual();
051
052  /** Returns the prototype invariant for StringNonEqual. */
053  public static @Prototype StringNonEqual 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 StringNonEqual. */
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        return result;
072  }
073
074  @Override
075  protected StringNonEqual instantiate_dyn(@Prototype StringNonEqual this, PptSlice slice) {
076
077    return new StringNonEqual(slice);
078  }
079
080  @Override
081  protected Invariant resurrect_done_swapped() {
082
083      // we don't care if things swap; we have symmetry
084      return this;
085  }
086
087  @Pure
088  @Override
089  public boolean is_symmetric() {
090    return true;
091  }
092
093  // JHP: this should be removed in favor of checks in PptTopLevel
094  // such as is_equal, is_lessequal, etc.
095  // Look up a previously instantiated StringNonEqual relationship.
096  // Should this implementation be made more efficient?
097  public static @Nullable StringNonEqual find(PptSlice ppt) {
098    assert ppt.arity() == 2;
099    for (Invariant inv : ppt.invs) {
100      if (inv instanceof StringNonEqual) {
101        return (StringNonEqual) inv;
102      }
103    }
104
105    // If the invariant is suppressed, create it
106    if ((suppressions != null) && suppressions.suppressed(ppt)) {
107      StringNonEqual inv = proto.instantiate_dyn(ppt);
108      // System.out.printf("%s is suppressed in ppt %s%n", inv.format(), ppt.name());
109      return inv;
110    }
111
112    return null;
113  }
114
115  @Override
116  public String repr(@GuardSatisfied StringNonEqual this) {
117    return "StringNonEqual" + varNames();
118  }
119
120  @SideEffectFree
121  @Override
122  public String format_using(@GuardSatisfied StringNonEqual this, OutputFormat format) {
123
124    String var1name = var1().name_using(format);
125    String var2name = var2().name_using(format);
126
127    if ((format == OutputFormat.DAIKON) || (format == OutputFormat.ESCJAVA)) {
128      String comparator = "!=";
129      return var1name + " " + comparator + " " + var2name;
130    }
131
132    if (format == OutputFormat.CSHARPCONTRACT) {
133
134        assert var1().has_typeof() == var2().has_typeof();
135        if (var1().has_typeof()) {
136          return var1name + " != " + var2name;
137        } else {
138          return "!" + var1name + ".Equals(" + var2name + ")";
139        }
140
141    }
142
143    if (format.isJavaFamily()) {
144
145        assert var1().has_typeof() == var2().has_typeof();
146        if (var1().has_typeof()) {
147          return var1name + " != " + var2name;
148        } else {
149          return "!" + var1name + ".equals(" + var2name + ")";
150        }
151
152    }
153
154    if (format == OutputFormat.SIMPLIFY) {
155
156        String comparator = "NEQ";
157
158      return "("
159          + comparator
160          + " "
161          + var1().simplifyFixup(var1name)
162          + " "
163          + var2().simplifyFixup(var2name)
164          + ")";
165    }
166
167    return format_unimplemented(format);
168  }
169
170  @Override
171  public InvariantStatus check_modified(@Interned String v1, @Interned String v2, int count) {
172    if (!(v1 != v2)) {
173      return InvariantStatus.FALSIFIED;
174    }
175    return InvariantStatus.NO_CHANGE;
176  }
177
178  @Override
179  public InvariantStatus add_modified(@Interned String v1, @Interned String v2, int count) {
180    if (logDetail() || debug.isLoggable(Level.FINE)) {
181      log(
182          debug,
183          "add_modified (" + v1 + ", " + v2 + ",  ppt.num_values = " + ppt.num_values() + ")");
184    }
185    if ((logOn() || debug.isLoggable(Level.FINE))
186        && check_modified(v1, v2, count) == InvariantStatus.FALSIFIED)
187      log(debug, "destroy in add_modified (" + v1 + ", " + v2 + ",  " + count + ")");
188
189    return check_modified(v1, v2, count);
190  }
191
192  // This is very tricky, because whether two variables are equal should
193  // presumably be transitive, but it's not guaranteed to be so when using
194  // this method and not dropping out all variables whose values are ever
195  // missing.
196  @Override
197  protected double computeConfidence() {
198    // Should perhaps check number of samples and be unjustified if too few
199    // samples.
200
201      // // The reason for this multiplication is that there might be only a
202      // // very few possible values.  Example:  towers of hanoi has only 6
203      // // possible (pegA, pegB) pairs.
204      // return 1 - (Math.pow(.5, ppt.num_values())
205      //             * Math.pow(.99, ppt.num_mod_samples()));
206      return 1 - Math.pow(.5, ppt.num_samples());
207  }
208
209  @Pure
210  @Override
211  public boolean isExact() {
212
213      return false;
214  }
215
216  // // Temporary, for debugging
217  // public void destroy() {
218  //   if (debug.isLoggable(Level.FINE)) {
219  //     System.out.println("StringNonEqual.destroy(" + ppt.name() + ")");
220  //     System.out.println(repr());
221  //     (new Error()).printStackTrace();
222  //   }
223  //   super.destroy();
224  // }
225
226  @Override
227  public InvariantStatus add(
228      @Interned Object v1, @Interned Object v2, int mod_index, int count) {
229    if (debug.isLoggable(Level.FINE)) {
230      debug.fine(
231          "StringNonEqual"
232          + ppt.varNames()
233          + ".add("
234          + v1
235          + ","
236          + v2
237          + ", mod_index="
238          + mod_index
239          + "), count="
240          + count
241          + ")");
242    }
243    return super.add(v1, v2, mod_index, count);
244  }
245
246  @Pure
247  @Override
248  public boolean isSameFormula(Invariant other) {
249    return true;
250  }
251
252  @Pure
253  @Override
254  public boolean isExclusiveFormula(Invariant other) {
255
256    // Also ought to check against LinearBinary, etc.
257
258      if (other instanceof StringEqual) {
259        return true;
260      }
261
262    return false;
263  }
264
265  @Override
266  public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) {
267    final VarInfo var1 = vis[0];
268    final VarInfo var2 = vis[1];
269
270    if (var1.aux.hasValue(VarInfoAux.MAXIMUM_VALUE)
271        && var2.aux.hasValue(VarInfoAux.MINIMUM_VALUE)) {
272      int maxA = var1.aux.getInt(VarInfoAux.MAXIMUM_VALUE),
273          minB = var2.aux.getInt(VarInfoAux.MINIMUM_VALUE);
274
275      if (maxA < minB) {
276        return new DiscardInfo(
277            this,
278            DiscardCode.obvious,
279            var1.name() + " DISCARD_OP " + var2.name() + " is already known");
280      }
281    }
282
283    if (var1.aux.hasValue(VarInfoAux.MINIMUM_VALUE)
284        && var2.aux.hasValue(VarInfoAux.MAXIMUM_VALUE)) {
285      int maxB = var2.aux.getInt(VarInfoAux.MAXIMUM_VALUE),
286          minA = var1.aux.getInt(VarInfoAux.MINIMUM_VALUE);
287
288      if (minA > maxB) {
289        return new DiscardInfo(
290            this,
291            DiscardCode.obvious,
292            var1.name() + " DISCARD_OP " + var2.name() + " is already known");
293      }
294    }
295
296    return super.isObviousStatically(vis);
297  }
298
299  @Pure
300  @Override
301  public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) {
302
303    // JHP: We might consider adding a check over bounds.   If
304    // x < c and y > c then we know that x < y.  Similarly for
305    // x > c and y < c.  We could also substitute oneof for
306    // one or both of the bound checks.
307
308    DiscardInfo super_result = super.isObviousDynamically(vis);
309    if (super_result != null) {
310      return super_result;
311    }
312
313    @SuppressWarnings("UnusedVariable") // generated code, variable is sometimes used
314    DiscardInfo di;
315
316    return null;
317  } // isObviousDynamically
318
319  /** NI suppressions, initialized in get_ni_suppressions() */
320  private static @Nullable NISuppressionSet suppressions = null;
321
322  /** Returns the non-instantiating suppressions for this invariant. */
323  @Pure
324  @Override
325  public NISuppressionSet get_ni_suppressions() {
326    if (suppressions == null) {
327
328        NISuppressee suppressee = new NISuppressee(StringNonEqual.class, 2);
329
330      // suppressor definitions (used in suppressions below)
331
332      NISuppressor v1_gt_v2 = new NISuppressor(0, 1, StringGreaterThan.class);
333
334      NISuppressor v1_lt_v2 = new NISuppressor(0, 1, StringLessThan.class);
335
336      suppressions =
337          new NISuppressionSet(
338              new NISuppression[] {
339
340                  // v1 < v2 => v1 != v2
341                  new NISuppression(v1_lt_v2, suppressee),
342                  // v1 > v2 => v1 != v2
343                  new NISuppression(v1_gt_v2, suppressee),
344
345              });
346    }
347    return suppressions;
348  }
349
350}