Source code

001// ***** This file is automatically generated from Numeric.java.jpp
002
003package daikon.inv.binary.twoString;
004
005import org.checkerframework.checker.lock.qual.GuardSatisfied;
006import org.checkerframework.checker.nullness.qual.NonNull;
007import org.checkerframework.checker.nullness.qual.Nullable;
008import org.checkerframework.checker.signature.qual.ClassGetName;
009import org.checkerframework.dataflow.qual.Pure;
010import org.checkerframework.dataflow.qual.SideEffectFree;
011import static daikon.inv.Invariant.asInvClass;
012
013import daikon.*;
014import daikon.Quantify.QuantFlags;
015import daikon.derive.binary.*;
016import daikon.inv.*;
017import daikon.inv.binary.twoScalar.*;
018import daikon.inv.binary.twoString.*;
019import daikon.inv.unary.scalar.*;
020import daikon.inv.unary.sequence.*;
021import daikon.suppress.*;
022import java.util.*;
023import org.plumelib.util.UtilPlume;
024import typequals.prototype.qual.NonPrototype;
025import typequals.prototype.qual.Prototype;
026
027/**
028 * Baseclass for binary numeric invariants.
029 *
030 * Each specific invariant is implemented in a subclass (typically, in this file). The subclass must
031 * provide the methods instantiate(), check(), and format(). Symmetric functions should define
032 * is_symmetric() to return true.
033 */
034public abstract class StdString extends TwoString {
035
036  // We are Serializable, so we specify a version to allow changes to
037  // method signatures without breaking serialization.  If you add or
038  // remove fields, you should change this number to the current date.
039  static final long serialVersionUID = 20060609L;
040
041  protected StdString(PptSlice ppt, boolean swap) {
042    super(ppt);
043    this.swap = swap;
044  }
045
046  protected StdString(boolean swap) {
047    super();
048    this.swap = swap;
049  }
050
051  /** Returns true if it is ok to instantiate a numeric invariant over the specified slice. */
052  @Override
053  public boolean instantiate_ok(VarInfo[] vis) {
054
055    ProglangType type1 = vis[0].file_rep_type;
056    ProglangType type2 = vis[1].file_rep_type;
057    if (!type1.isString() || !type2.isString()) {
058      return false;
059    }
060
061    return true;
062  }
063
064  @Pure
065  @Override
066  public boolean isExact() {
067    return true;
068  }
069
070  @Override
071  public String repr(@GuardSatisfied StdString this) {
072    return getClass().getSimpleName() + ": " + format()
073      + (swap ? " [swapped]" : " [unswapped]");
074  }
075
076  /**
077   * Returns a string in the specified format that describes the invariant.
078   *
079   * The generic format string is obtained from the subclass specific get_format_str(). Instances of
080   * %varN% are replaced by the variable name in the specified format.
081   */
082  @SideEffectFree
083  @Override
084  public String format_using(@GuardSatisfied StdString this, OutputFormat format) {
085
086    if (ppt == null) {
087      return String.format("proto ppt [class %s] format %s", getClass(),
088                           get_format_str(format));
089    }
090    String fmt_str = get_format_str(format);
091
092    String v1 = var1().name_using(format);
093    String v2 = var2().name_using(format);
094
095    // Note that we do not use String.replaceAll here, because that's
096    // inseparable from the regex library, and we don't want to have to
097    // escape v1 with something like
098    // v1.replaceAll("([\\$\\\\])", "\\\\$1")
099    fmt_str = fmt_str.replace("%var1%", v1);
100    fmt_str = fmt_str.replace("%var2%", v2);
101
102    // if (false && (format == OutputFormat.DAIKON)) {
103    //   fmt_str = "[" + getClass() + "]" + fmt_str + " ("
104    //          + var1().get_value_info() + ", " + var2().get_value_info() +  ")";
105    // }
106    return fmt_str;
107  }
108
109  /** Calls the function specific equal check and returns the correct status. */
110
111  @Override
112  public InvariantStatus check_modified(String x, String y, int count) {
113
114    try {
115      if (eq_check(x, y)) {
116        return InvariantStatus.NO_CHANGE;
117      } else {
118        return InvariantStatus.FALSIFIED;
119      }
120    } catch (Exception e) {
121      return InvariantStatus.FALSIFIED;
122    }
123  }
124
125  /**
126   * Checks to see if 'x[a] op y[b]' where 'x[] op y[]' and 'a == b'. Doesn't catch the case where
127   * a = b+1.
128   */
129  public @Nullable DiscardInfo is_subscript(VarInfo[] vis) {
130
131    VarInfo v1 = var1(vis);
132    VarInfo v2 = var2(vis);
133
134    // Make sure each var is a sequence subscript
135    if (!v1.isDerived() || !(v1.derived instanceof SequenceStringSubscript)) {
136      return null;
137    }
138    if (!v2.isDerived() || !(v2.derived instanceof SequenceStringSubscript)) {
139      return null;
140    }
141
142    @NonNull SequenceStringSubscript der1 = (SequenceStringSubscript) v1.derived;
143    @NonNull SequenceStringSubscript der2 = (SequenceStringSubscript) v2.derived;
144
145    // Make sure the shifts match
146    if (der1.index_shift != der2.index_shift) {
147      return null;
148    }
149
150    // Look for this invariant over a sequence
151    String cstr = getClass().getName();
152    cstr = cstr.replaceFirst("Numeric", "PairwiseNumeric");
153    cstr = cstr.replaceFirst("twoScalar", "twoSequence");
154    cstr = cstr.replaceFirst("twoFloat", "twoSequence");
155    Class<? extends Invariant> pairwise_class;
156    try {
157      @SuppressWarnings("signature") // string manipulation; application invariants
158      @ClassGetName String cstr_cgn = cstr;
159      pairwise_class = asInvClass(Class.forName(cstr_cgn));
160    } catch (Exception e) {
161      throw new Error("can't create class for " + cstr, e);
162    }
163    Invariant inv = find(pairwise_class, der1.seqvar(), der2.seqvar());
164    if (inv == null) {
165      return null;
166    }
167
168    // Look to see if the subscripts are equal
169    Invariant subinv = find(StringEqual.class, der1.sclvar(), der2.sclvar());
170    if (subinv == null) {
171      return null;
172    }
173
174    return new DiscardInfo(this, DiscardCode.obvious, "Implied by "
175                           + inv.format() + " and " + subinv.format());
176  }
177
178  @Pure
179  @Override
180  public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) {
181
182    DiscardInfo super_result = super.isObviousDynamically(vis);
183    if (super_result != null) {
184      return super_result;
185    }
186
187      // any relation across subscripts is made obvious by the same
188      // relation across the original sequence if the subscripts are equal
189      DiscardInfo result = is_subscript(vis);
190      if (result != null) {
191        return result;
192      }
193
194    // Check for invariant specific obvious checks.  The obvious_checks
195    // method returns an array of arrays of antecedents.  If all of the
196    // antecedents in an array are true, then the invariant is obvoius.
197    InvDef[][] obvious_arr = obvious_checks(vis);
198    obvious_loop:
199    for (int i = 0; i < obvious_arr.length; i++) {
200      InvDef[] antecedents = obvious_arr[i];
201      StringBuilder why = null;
202      for (int j = 0; j < antecedents.length; j++) {
203        Invariant inv = antecedents[j].find();
204        if (inv == null) {
205          continue obvious_loop;
206        }
207        if (why == null) {
208          why = new StringBuilder(inv.format());
209        } else {
210          why.append(" and ");
211          why.append(inv.format());
212        }
213      }
214      return new DiscardInfo(this, DiscardCode.obvious, "Implied by " + why);
215    }
216
217    return null;
218  }
219
220  /**
221   * Return a format string for the specified output format. Each instance of %varN% will be
222   * replaced by the correct name for varN.
223   */
224  public abstract String get_format_str(@GuardSatisfied StdString this, OutputFormat format);
225
226  /** Returns true if x and y don't invalidate the invariant. */
227  public abstract boolean eq_check(String x, String y);
228
229  /**
230   * Returns an array of arrays of antecedents. If all of the antecedents in any array are true,
231   * then the invariant is obvious.
232   */
233  public InvDef[][] obvious_checks(VarInfo[] vis) {
234    return new InvDef[][] {};
235  }
236
237  public static List<@Prototype Invariant> get_proto_all() {
238
239    List<@Prototype Invariant> result = new ArrayList<>();
240
241        result.add(SubString.get_proto(false));
242        result.add(SubString.get_proto(true));
243
244    // System.out.printf("%s get proto: %s%n", StdString.class, result);
245    return result;
246  }
247
248  // suppressor definitions, used by many of the classes below
249  protected static NISuppressor
250
251    var1_eq_var2    = new NISuppressor(0, 1, StringEqual.class),
252    var2_eq_var1    = new NISuppressor(0, 1, StringEqual.class);
253
254  //
255  // Int and Float Numeric Invariants
256  //
257
258//
259// Standard String invariants
260//
261
262  /**
263   * Represents the substring invariant between two String scalars.
264   * Prints as {@code x is a substring of y}.
265   */
266  public static class SubString extends StdString {
267    // We are Serializable, so we specify a version to allow changes to
268    // method signatures without breaking serialization.  If you add or
269    // remove fields, you should change this number to the current date.
270    static final long serialVersionUID = 20081113L;
271
272    protected SubString(PptSlice ppt, boolean swap) {
273      super(ppt, swap);
274    }
275
276    protected SubString(boolean swap) {
277      super(swap);
278    }
279
280    private static @Prototype SubString proto = new @Prototype SubString(false);
281    private static @Prototype SubString proto_swap = new @Prototype SubString(true);
282
283    /** Returns the prototype invariant. */
284    public static @Prototype SubString get_proto(boolean swap) {
285      if (swap) {
286        return proto_swap;
287      } else {
288        return proto;
289      }
290    }
291
292    // Variables starting with dkconfig_ should only be set via the
293    // daikon.config.Configuration interface.
294    /** Boolean. True iff SubString invariants should be considered. */
295    public static boolean dkconfig_enabled = false;
296
297    /** Returns whether or not this invariant is enabled. */
298    @Override
299    public boolean enabled() {
300      return dkconfig_enabled;
301    }
302
303    @Override
304    protected SubString instantiate_dyn(@Prototype SubString this, PptSlice slice) {
305      return new SubString(slice, swap);
306    }
307
308    @Override
309    public String get_format_str(@GuardSatisfied SubString this, OutputFormat format) {
310      if (format == OutputFormat.DAIKON) {
311        return "%var1% is a substring of %var2%";
312      } else if (format.isJavaFamily()) {
313        return "%var2%.contains(%var1%)";
314      } else if (format == OutputFormat.CSHARPCONTRACT) {
315
316          return "%var2%.Contains(%var1%)";
317      } else {
318        return format_unimplemented(format);
319      }
320    }
321
322    @Override
323    public boolean eq_check(String x, String y) {
324      return y.contains(x);
325    }
326
327    /** Justified as long as there are samples. */
328    @Override
329    protected double computeConfidence() {
330      if (ppt.num_samples() == 0) {
331        return Invariant.CONFIDENCE_UNJUSTIFIED;
332      }
333
334      return Invariant.CONFIDENCE_JUSTIFIED;
335    }
336
337    /** Returns a list of non-instantiating suppressions for this invariant. */
338    @Pure
339    @Override
340    public NISuppressionSet get_ni_suppressions() {
341      if (swap) {
342        return suppressions_swap;
343      } else {
344        return suppressions;
345      }
346    }
347
348    /** definition of this invariant (the suppressee) (unswapped) */
349    private static NISuppressee suppressee = new NISuppressee(SubString.class, false);
350
351    private static NISuppressionSet suppressions =
352      new NISuppressionSet(
353          new NISuppression[] {
354              // v1 == v2 ==> v1 subsequence v2
355              new NISuppression(var1_eq_var2, suppressee),
356          });
357    private static NISuppressionSet suppressions_swap = suppressions.swap();
358  }
359
360}