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