Source code

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 StringEqual extends TwoString implements EqualityComparison {
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 StringEqual 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.StringEqual");
044
045  StringEqual(PptSlice ppt) {
046    super(ppt);
047  }
048
049  @Prototype StringEqual() {
050    super();
051  }
052
053  private static @Prototype StringEqual proto = new @Prototype StringEqual();
054
055  /** Returns the prototype invariant for StringEqual */
056  public static @Prototype StringEqual get_proto() {
057    return proto;
058  }
059
060  /** Returns whether or not this invariant is enabled. */
061  @Override
062  public boolean enabled() {
063    return dkconfig_enabled;
064  }
065
066  /** Returns whether or not the specified var types are valid for StringEqual */
067  @Override
068  public boolean instantiate_ok(VarInfo[] vis) {
069
070    if (!valid_types(vis)) {
071      return false;
072    }
073
074        boolean result = !(vis[0].has_typeof() ^ vis[1].has_typeof());
075        return result;
076  }
077
078  /** Instantiate an invariant on the specified slice. */
079  @Override
080  protected StringEqual instantiate_dyn(@Prototype StringEqual this, PptSlice slice) {
081
082    return new StringEqual(slice);
083  }
084
085  @Pure
086  public boolean is_equality_inv() {
087    return true;
088  }
089
090  @Override
091  protected Invariant resurrect_done_swapped() {
092
093      // we don't care if things swap; we have symmetry
094      return this;
095  }
096
097  @Pure
098  @Override
099  public boolean is_symmetric() {
100    return true;
101  }
102
103  // JHP: this should be removed in favor of checks in PptTopLevel
104  // such as is_equal, is_lessequal, etc.
105  // Look up a previously instantiated StringEqual relationship.
106  // Should this implementation be made more efficient?
107  public static @Nullable StringEqual find(PptSlice ppt) {
108    assert ppt.arity() == 2;
109    for (Invariant inv : ppt.invs) {
110      if (inv instanceof StringEqual) {
111        return (StringEqual) inv;
112      }
113    }
114
115    // If the invariant is suppressed, create it
116    if ((suppressions != null) && suppressions.suppressed(ppt)) {
117      StringEqual inv = proto.instantiate_dyn(ppt);
118      // System.out.printf("%s is suppressed in ppt %s%n", inv.format(), ppt.name());
119      return inv;
120    }
121
122    return null;
123  }
124
125  @Override
126  public String repr(@GuardSatisfied StringEqual this) {
127    return "StringEqual" + varNames();
128  }
129
130  @SideEffectFree
131  @Override
132  public String format_using(@GuardSatisfied StringEqual this, OutputFormat format) {
133
134    String var1name = var1().name_using(format);
135    String var2name = var2().name_using(format);
136
137    if ((format == OutputFormat.DAIKON) || (format == OutputFormat.ESCJAVA)) {
138      String comparator = "==";
139      return var1name + " " + comparator + " " + var2name;
140    }
141
142    if (format == OutputFormat.CSHARPCONTRACT) {
143
144        assert var1().has_typeof() == var2().has_typeof();
145        if (var1().has_typeof()) {
146          return var1name + " == " + var2name;
147        } else {
148          return var1name + ".Equals(" + var2name + ")";
149        }
150
151    }
152
153    if (format.isJavaFamily()) {
154
155        assert var1().has_typeof() == var2().has_typeof();
156        if (var1().has_typeof()) {
157          return var1name + " == " + var2name;
158        } else {
159          return var1name + ".equals(" + var2name + ")";
160        }
161
162    }
163
164    if (format == OutputFormat.SIMPLIFY) {
165
166        String comparator = "EQ";
167
168      return "("
169          + comparator
170          + " "
171          + var1().simplifyFixup(var1name)
172          + " "
173          + var2().simplifyFixup(var2name)
174          + ")";
175    }
176
177    return format_unimplemented(format);
178  }
179
180  @Override
181  public InvariantStatus check_modified(@Interned String v1, @Interned String v2, int count) {
182    if (!((v1 != null) && ( v2 != null) && (v1 == v2))) {
183      return InvariantStatus.FALSIFIED;
184    }
185    return InvariantStatus.NO_CHANGE;
186  }
187
188  @Override
189  public InvariantStatus add_modified(@Interned String v1, @Interned String v2, int count) {
190    if (logDetail() || debug.isLoggable(Level.FINE)) {
191      log(
192          debug,
193          "add_modified (" + v1 + ", " + v2 + ",  ppt.num_values = " + ppt.num_values() + ")");
194    }
195    if ((logOn() || debug.isLoggable(Level.FINE))
196        && check_modified(v1, v2, count) == InvariantStatus.FALSIFIED)
197      log(debug, "destroy in add_modified (" + v1 + ", " + v2 + ",  " + count + ")");
198
199    return check_modified(v1, v2, count);
200  }
201
202  // This is very tricky, because whether two variables are equal should
203  // presumably be transitive, but it's not guaranteed to be so when using
204  // this method and not dropping out all variables whose values are ever
205  // missing.
206  @Override
207  protected double computeConfidence() {
208    // Should perhaps check number of samples and be unjustified if too few
209    // samples.
210
211      // We MUST check if we have seen samples; otherwise we get
212      // undesired transitivity with missing values.
213      if (ppt.num_samples() == 0) {
214        return Invariant.CONFIDENCE_UNJUSTIFIED;
215      }
216
217      // It's an equality invariant.  I ought to use the actual ranges somehow.
218      // Actually, I can't even use this .5 test because it can make
219      // equality non-transitive.
220      // return Math.pow(.5, num_values());
221      return Invariant.CONFIDENCE_JUSTIFIED;
222
223  }
224
225  @Override
226  public boolean enoughSamples(@GuardSatisfied StringEqual this) {
227    return ppt.num_samples() > 0;
228  }
229
230  // For Comparison interface, which is satisfied only by exact equalities.
231  @Override
232  public double eq_confidence() {
233    if (isExact()) {
234      return getConfidence();
235    } else {
236      return Invariant.CONFIDENCE_NEVER;
237    }
238  }
239
240  @Pure
241  @Override
242  public boolean isExact() {
243
244      return true;
245  }
246
247  // // Temporary, for debugging
248  // public void destroy() {
249  //   if (debug.isLoggable(Level.FINE)) {
250  //     System.out.println("StringEqual.destroy(" + ppt.name() + ")");
251  //     System.out.println(repr());
252  //     (new Error()).printStackTrace();
253  //   }
254  //   super.destroy();
255  // }
256
257  @Override
258  public InvariantStatus add(
259      @Interned Object v1, @Interned Object v2, int mod_index, int count) {
260    if (debug.isLoggable(Level.FINE)) {
261      debug.fine(
262          "StringEqual"
263          + ppt.varNames()
264          + ".add("
265          + v1
266          + ","
267          + v2
268          + ", mod_index="
269          + mod_index
270          + "), count="
271          + count
272          + ")");
273    }
274    return super.add(v1, v2, mod_index, count);
275  }
276
277  @Pure
278  @Override
279  public boolean isSameFormula(Invariant other) {
280    return true;
281  }
282
283  @Pure
284  @Override
285  public boolean isExclusiveFormula(Invariant other) {
286
287    // Also ought to check against LinearBinary, etc.
288
289      if ((other instanceof StringLessThan)
290          || (other instanceof StringGreaterThan)
291          || (other instanceof StringNonEqual)) {
292        return true;
293      }
294
295    return false;
296  }
297
298  @Override
299  public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) {
300    final VarInfo var1 = vis[0];
301    final VarInfo var2 = vis[1];
302
303    // If A.minvalue==A.maxvalue==B.minvalue==B.maxvalue, then
304    // there's nothing to see here.
305    if (var1.aux.hasValue(VarInfoAux.MINIMUM_VALUE)
306        && var1.aux.hasValue(VarInfoAux.MAXIMUM_VALUE)
307        && var2.aux.hasValue(VarInfoAux.MINIMUM_VALUE)
308        && var2.aux.hasValue(VarInfoAux.MAXIMUM_VALUE)) {
309      @SuppressWarnings("all:argument") // EnsuresKeyFor for multiple maps; also https://tinyurl.com/cfissue/2586
310      int minA = var1.aux.getInt(VarInfoAux.MINIMUM_VALUE),
311          maxA = var1.aux.getInt(VarInfoAux.MAXIMUM_VALUE),
312          minB = var2.aux.getInt(VarInfoAux.MINIMUM_VALUE),
313          maxB = var2.aux.getInt(VarInfoAux.MAXIMUM_VALUE);
314
315      if (minA == maxA && maxA == minB && minB == maxB) {
316        return new DiscardInfo(
317            this, DiscardCode.obvious, var1.name() + " == " + var2.name() + " is already known");
318      }
319    }
320
321    return super.isObviousStatically(vis);
322  }
323
324  /**
325   * Since this invariant can be a postProcessed equality, we have to handle isObvious especially to
326   * avoid circular isObvious relations. We only check if this.ppt.var_infos imply obviousness
327   * rather than the cartesian product on the equality set.
328   */
329  @Pure
330  @Override
331  public @Nullable DiscardInfo isObviousStatically_SomeInEquality() {
332    if (var1().equalitySet == var2().equalitySet) {
333      return isObviousStatically(this.ppt.var_infos);
334    } else {
335      return super.isObviousStatically_SomeInEquality();
336    }
337  }
338
339  /**
340   * Since this invariant can be a postProcessed equality, we have to handle isObvious especially to
341   * avoid circular isObvious relations. We only check if this.ppt.var_infos imply obviousness
342   * rather than the cartesian product on the equality set.
343   */
344  @Pure
345  @Override
346  public @Nullable DiscardInfo isObviousDynamically_SomeInEquality() {
347    if (var1().equalitySet == var2().equalitySet) {
348      return isObviousDynamically(this.ppt.var_infos);
349    } else {
350      return super.isObviousDynamically_SomeInEquality();
351    }
352  }
353
354  @Pure
355  @Override
356  public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) {
357
358    // JHP: We might consider adding a check over bounds.   If
359    // x < c and y > c then we know that x < y.  Similarly for
360    // x > c and y < c.  We could also substitute oneof for
361    // one or both of the bound checks.
362
363    DiscardInfo super_result = super.isObviousDynamically(vis);
364    if (super_result != null) {
365      return super_result;
366    }
367
368    @SuppressWarnings("UnusedVariable") // generated code, variable is sometimes used
369    DiscardInfo di;
370
371      // Check for size(A[]) == Size(B[]) where A[] == B[]
372      di = array_eq_implies(vis);
373      if (di != null) {
374        return di;
375      }
376
377    return null;
378  } // isObviousDynamically
379
380  /**
381   * If the equality is between two array size variables, check to see if the underlying arrays are
382   * equal:
383   *
384   * <pre>(x[] = y[]) &rArr; size(x[]) = size(y[])</pre>
385   */
386  private @Nullable DiscardInfo array_eq_implies(VarInfo[] vis) {
387
388    // Make sure v1 and v2 are size(array) with the same shift
389    VarInfo v1 = vis[0];
390    if (!v1.isDerived() || !(v1.derived instanceof SequenceLength)) {
391      return null;
392    }
393    VarInfo v2 = vis[1];
394    if (!v2.isDerived() || !(v2.derived instanceof SequenceLength)) {
395      return null;
396    }
397    if (!v1.derived.isSameFormula(v2.derived)) {
398      return null;
399    }
400
401    VarInfo seqvar1 = v1.derived.getBase(0);
402    VarInfo seqvar2 = v2.derived.getBase(0);
403    if (ppt.parent.is_equal(seqvar1, seqvar2)) {
404      return new DiscardInfo(
405          this,
406          DiscardCode.obvious,
407          "Implied by "
408              + seqvar1
409              + " == "
410              + seqvar2
411              + " and "
412              + var1()
413              + " == "
414              + v1
415              + " and "
416              + var2()
417              + " == "
418              + v2);
419    }
420
421    return null;
422  }
423
424  /** NI suppressions, initialized in get_ni_suppressions() */
425  private static @Nullable NISuppressionSet suppressions = null;
426
427  /** Returns the non-instantiating suppressions for this invariant. */
428  @Pure
429  @Override
430  public @Nullable NISuppressionSet get_ni_suppressions() {
431    return null;
432  }
433
434}