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