Source code

001// ***** This file is automatically generated from Numeric.java.jpp
002
003package daikon.inv.binary.twoScalar;
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 NumericFloat extends TwoFloat {
035
036  static final long serialVersionUID = 20060609L;
037
038  protected NumericFloat(PptSlice ppt, boolean swap) {
039    super(ppt);
040    this.swap = swap;
041  }
042
043  protected NumericFloat(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.isFloat() || !type2.isFloat()) {
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 NumericFloat 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 NumericFloat 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(double x, double 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 SequenceFloatSubscript)) {
132      return null;
133    }
134    if (!v2.isDerived() || !(v2.derived instanceof SequenceFloatSubscript)) {
135      return null;
136    }
137
138    @NonNull SequenceFloatSubscript der1 = (SequenceFloatSubscript) v1.derived;
139    @NonNull SequenceFloatSubscript der2 = (SequenceFloatSubscript) 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(FloatEqual.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 NumericFloat this, OutputFormat format);
221
222  /** Returns true if x and y don't invalidate the invariant. */
223  public abstract boolean eq_check(double x, double 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(Divides.get_proto(false));
238      result.add(Divides.get_proto(true));
239      result.add(Square.get_proto(false));
240      result.add(Square.get_proto(true));
241
242      result.add(ZeroTrack.get_proto(false));
243      result.add(ZeroTrack.get_proto(true));
244
245    // System.out.printf("%s get proto: %s%n", NumericFloat.class, result);
246    return result;
247  }
248
249  // suppressor definitions, used by many of the classes below
250  protected static NISuppressor
251
252      var1_eq_0       = new NISuppressor(0, RangeFloat.EqualZero.class),
253      var2_eq_0       = new NISuppressor(1, RangeFloat.EqualZero.class),
254      var1_ge_0       = new NISuppressor(0, RangeFloat.GreaterEqualZero.class),
255      var2_ge_0       = new NISuppressor(1, RangeFloat.GreaterEqualZero.class),
256      var1_eq_1       = new NISuppressor(0, RangeFloat.EqualOne.class),
257      var2_eq_1       = new NISuppressor(1, RangeFloat.EqualOne.class),
258      var1_eq_minus_1 = new NISuppressor(0, RangeFloat.EqualMinusOne.class),
259      var2_eq_minus_1 = new NISuppressor(1, RangeFloat.EqualMinusOne.class),
260      var1_ne_0       = new NISuppressor(0, NonZeroFloat.class),
261      var2_ne_0       = new NISuppressor(1, NonZeroFloat.class),
262      var1_le_var2    = new NISuppressor(0, 1, FloatLessEqual.class),
263
264    var1_eq_var2    = new NISuppressor(0, 1, FloatEqual.class),
265    var2_eq_var1    = new NISuppressor(0, 1, FloatEqual.class);
266
267  //
268  // Int and Float Numeric Invariants
269  //
270
271  /**
272   * Represents the divides without remainder invariant between two double scalars.
273   * Prints as {@code x % y == 0}.
274   */
275  public static class Divides extends NumericFloat {
276    // We are Serializable, so we specify a version to allow changes to
277    // method signatures without breaking serialization.  If you add or
278    // remove fields, you should change this number to the current date.
279    static final long serialVersionUID = 20040113L;
280
281    protected Divides(PptSlice ppt, boolean swap) {
282      super(ppt, swap);
283    }
284
285    protected Divides(boolean swap) {
286      super(swap);
287    }
288
289    private static @Prototype Divides proto = new @Prototype Divides(false);
290    private static @Prototype Divides proto_swap = new @Prototype Divides(true);
291
292    /** Returns the prototype invariant. */
293    public static @Prototype NumericFloat get_proto(boolean swap) {
294      if (swap) {
295        return proto_swap;
296      } else {
297        return proto;
298      }
299    }
300
301    // Variables starting with dkconfig_ should only be set via the
302    // daikon.config.Configuration interface.
303    /** Boolean. True iff divides invariants should be considered. */
304    public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault;
305
306    @Override
307    public boolean enabled() {
308      return dkconfig_enabled;
309    }
310
311    @Override
312    protected Divides instantiate_dyn(@Prototype Divides this, PptSlice slice) {
313      return new Divides(slice, swap);
314    }
315
316    @Override
317    public String get_format_str(@GuardSatisfied Divides this, OutputFormat format) {
318      if (format == OutputFormat.SIMPLIFY) {
319        return "(EQ 0 (MOD %var1% %var2%))";
320      } else if (format.isJavaFamily()) {
321        return "daikon.Quant.fuzzy.eq(%var1% % %var2%, 0)";
322      } else {
323        return "%var1% % %var2% == 0";
324      }
325    }
326
327    @Override
328    public boolean eq_check(double x, double y) {
329      return Global.fuzzy.eq(0, (x % y));
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(Divides.class, false);
345
346    private static NISuppressionSet suppressions =
347      new NISuppressionSet(
348          new NISuppression[] {
349
350            // These suppressions are only valid on scalars because the length
351            // of var1 and var2 must also be the same and there is no suppressor
352            // for that.
353
354            // var2 == 1 ==> var1 % var2 == 0
355            new NISuppression(var2_eq_1, suppressee),
356
357            // var2 == -1 ==> var1 % var2 == 0
358            new NISuppression(var2_eq_minus_1, suppressee),
359
360            // (var1 == 0) ^ (var2 != 0) ==> var1 % var2 == 0
361            new NISuppression(var1_eq_0, var2_ne_0, suppressee),
362
363            // (var1 == var2) ^ (var2 != 0) ==> var1 % var2 == 0
364            new NISuppression(var1_eq_var2, var2_ne_0, suppressee),
365
366            // (var2 == var1) ^ (var1 != 0) ==> var2 % var1 == 0
367            new NISuppression(var2_eq_var1, var1_ne_0, suppressee),
368
369          });
370    private static NISuppressionSet suppressions_swap = suppressions.swap();
371
372    /**
373     * Returns non-null if this invariant is obvious from an existing, non-falsified linear binary
374     * invariant in the same slice as this invariant. This invariant of the form "x % y == 0" is
375     * falsified if a linear binary invariant is found of the form "a*y - 1*x + 0 == 0"
376     *
377     * @return non-null value iff this invariant is obvious from other invariants in the same slice
378     */
379    @Pure
380    @Override
381    public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) {
382      // First call super type's method, and if it returns non-null, then
383      // this invariant is already known to be obvious, so just return
384      // whatever reason the super type returned.
385      DiscardInfo di = super.isObviousDynamically(vis);
386      if (di != null) {
387        return di;
388      }
389
390      VarInfo var1 = vis[0];
391      VarInfo var2 = vis[1];
392
393      // ensure that var1.varinfo_index <= var2.varinfo_index
394      if (var1.varinfo_index > var2.varinfo_index) {
395        var1 = vis[1];
396        var2 = vis[0];
397      }
398
399      // Find slice corresponding to these two variables.
400      // Ideally, this should always just be ppt if all
401      // falsified invariants have been removed.
402      PptSlice2 ppt2 = ppt.parent.findSlice(var1,var2);
403
404      // If no slice is found , no invariants exist to make this one obvious.
405      if (ppt2 == null) {
406        return null;
407      }
408
409      // For each invariant, check to see if it's a linear binary
410      // invariant of the form "a*y - 1*x + 0 == 0" and if so,
411      // you know this invariant of the form "x % y == 0" is obvious.
412      for(Invariant inv : ppt2.invs) {
413
414        if (inv instanceof LinearBinaryFloat) {
415          LinearBinaryFloat linv = (LinearBinaryFloat) inv;
416
417          // General form for linear binary: a*x + b*y + c == 0,
418          // but a and b can be switched with respect to vis, and either
419          // one may be negative, so instead check:
420          //  - c == 0
421          //  - a*b < 0   (a and b have different signs)
422          //  - |a| == 1 or |b| == 1, so one will divide the other
423          //     While this means that both x % y == 0 and y % x == 0,
424          //     only one of these invariants will still be true at this
425          //     time, and only that one will be falsified by this test.
426          if (!linv.is_false()
427              && Global.fuzzy.eq(linv.core.c, 0)
428              && linv.core.b * linv.core.a < 0
429              && (Global.fuzzy.eq(linv.core.a * linv.core.a, 1)
430                  || Global.fuzzy.eq(linv.core.b * linv.core.b, 1))) {
431            return new DiscardInfo(this, DiscardCode.obvious,
432                                   "Linear binary invariant implies divides");
433          }
434        }
435      }
436
437      return null;
438    }
439
440  }
441
442  /**
443   * Represents the square invariant between two double scalars.
444   * Prints as {@code x = y**2}.
445   */
446  public static class Square extends NumericFloat {
447    // We are Serializable, so we specify a version to allow changes to
448    // method signatures without breaking serialization.  If you add or
449    // remove fields, you should change this number to the current date.
450    static final long serialVersionUID = 20040113L;
451
452    protected Square(PptSlice ppt, boolean swap) {
453      super(ppt, swap);
454    }
455
456    protected Square(boolean swap) {
457      super(swap);
458    }
459
460    private static @Prototype Square proto = new @Prototype Square(false);
461    private static @Prototype Square proto_swap = new @Prototype Square(true);
462
463    /** Returns the prototype invariant. */
464    public static @Prototype Square get_proto(boolean swap) {
465      if (swap) {
466        return proto_swap;
467      } else {
468        return proto;
469      }
470    }
471
472    // Variables starting with dkconfig_ should only be set via the
473    // daikon.config.Configuration interface.
474    /** Boolean. True iff square invariants should be considered. */
475    public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault;
476
477    @Override
478    public boolean enabled() {
479      return dkconfig_enabled;
480    }
481    @Override
482    protected Square instantiate_dyn(@Prototype Square this, PptSlice slice) {
483      return new Square(slice, swap);
484    }
485
486    @Override
487    public String get_format_str(@GuardSatisfied Square this, OutputFormat format) {
488      if (format == OutputFormat.SIMPLIFY) {
489        return "(EQ %var1% (* %var2% %var2))";
490      } else if (format == OutputFormat.CSHARPCONTRACT) {
491        return "%var1% == %var2%*%var2%";
492      } else if (format.isJavaFamily()) {
493
494        return "daikon.Quant.fuzzy.eq(%var1%, %var2%*%var2%)";
495      } else {
496        return "%var1% == %var2%**2";
497      }
498    }
499
500    /** Check to see if x == y squared. */
501    @Override
502    public boolean eq_check(double x, double y) {
503      return Global.fuzzy.eq(x, y*y);
504    }
505
506    // Note there are no NI Suppressions for Square.  Two obvious
507    // suppressions are:
508    //
509    //      (var2 == 1) ^ (var1 == 1)  ==> var1 = var2*var2
510    //      (var2 == 0) ^ (var1 == 0)  ==> var1 = var2*var2
511    //
512    // But all of the antecedents would be constants, so we would
513    // never need to create this slice, so there is no reason to create
514    // these.
515
516  }
517
518  /**
519   * Represents the zero tracks invariant between
520   * two double scalars; that is, when {@code x} is zero,
521   * {@code y} is also zero.
522   * Prints as {@code x = 0 => y = 0}.
523   */
524  public static class ZeroTrack extends NumericFloat {
525    // We are Serializable, so we specify a version to allow changes to
526    // method signatures without breaking serialization.  If you add or
527    // remove fields, you should change this number to the current date.
528    static final long serialVersionUID = 20040313L;
529
530    protected ZeroTrack(PptSlice ppt, boolean swap) {
531      super(ppt, swap);
532    }
533
534    protected @Prototype ZeroTrack(boolean swap) {
535      super(swap);
536    }
537
538    private static @Prototype ZeroTrack proto = new @Prototype ZeroTrack(false);
539    private static @Prototype ZeroTrack proto_swap = new @Prototype ZeroTrack(true);
540
541    /** Returns the prototype invariant. */
542    public static @Prototype ZeroTrack get_proto(boolean swap) {
543      if (swap) {
544        return proto_swap;
545      } else {
546        return proto;
547      }
548    }
549
550    // Variables starting with dkconfig_ should only be set via the
551    // daikon.config.Configuration interface.
552    /** Boolean. True iff zero-track invariants should be considered. */
553    public static boolean dkconfig_enabled = false;
554
555    @Override
556    public boolean enabled() {
557      return dkconfig_enabled;
558    }
559
560    @Override
561    protected ZeroTrack instantiate_dyn(@Prototype ZeroTrack this, PptSlice slice) {
562      return new ZeroTrack(slice, swap);
563    }
564
565    @Override
566    public String get_format_str(@GuardSatisfied ZeroTrack this, OutputFormat format) {
567      if (format == OutputFormat.SIMPLIFY) {
568        return "(IMPLIES (EQ %var1% 0) (EQ %var2% 0))";
569      } else if (format.isJavaFamily() || format == OutputFormat.CSHARPCONTRACT) {
570        return "(!(%var1% == 0)) || (%var2% == 0)";
571      } else {
572        return "(%var1% == 0) ==> (%var2% == 0)";
573      }
574    }
575
576    @Override
577    public boolean eq_check(double x, double y) {
578      if (x == 0) {
579        return y == 0;
580      } else {
581        return true;
582      }
583    }
584
585    /** Returns a list of non-instantiating suppressions for this invariant. */
586    @Pure
587    @Override
588    public NISuppressionSet get_ni_suppressions() {
589      if (swap) {
590        return suppressions_swap;
591      } else {
592        return suppressions;
593      }
594    }
595
596    /** definition of this invariant (the suppressee) (unswapped) */
597    private static NISuppressee suppressee = new NISuppressee(ZeroTrack.class, false);
598
599    private static NISuppressionSet suppressions =
600      new NISuppressionSet(
601          new NISuppression[] {
602            // (var1 == var2) ==> (var1=0 ==> var2=0)
603            new NISuppression(var1_eq_var2, suppressee),
604            // (var1 != 0)    ==> (var1=0 ==> var2=0)
605            new NISuppression(var1_ne_0, suppressee),
606            // (var2 == 0) ==> (var1=0 ==> var2=0)
607            new NISuppression(var2_eq_0, suppressee),
608          });
609    private static NISuppressionSet suppressions_swap = suppressions.swap();
610
611  }
612
613//
614// Standard String invariants
615//
616
617}