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 == OutputFormat.CSHARPCONTRACT) {
321        return "%var1% % %var2% == 0";
322      } else if (format.isJavaFamily()) {
323        return "daikon.Quant.fuzzy.eq(%var1% % %var2%, 0)";
324      } else {
325        return "%var1% % %var2% == 0";
326      }
327    }
328
329    @Override
330    public boolean eq_check(double x, double y) {
331      return Global.fuzzy.eq(0, (x % y));
332    }
333
334    /** Returns a list of non-instantiating suppressions for this invariant. */
335    @Pure
336    @Override
337    public NISuppressionSet get_ni_suppressions() {
338      if (swap) {
339        return suppressions_swap;
340      } else {
341        return suppressions;
342      }
343    }
344
345    /** definition of this invariant (the suppressee) (unswapped) */
346    private static NISuppressee suppressee = new NISuppressee(Divides.class, false);
347
348    private static NISuppressionSet suppressions =
349      new NISuppressionSet(
350          new NISuppression[] {
351
352            // These suppressions are only valid on scalars because the length
353            // of var1 and var2 must also be the same and there is no suppressor
354            // for that.
355
356            // var2 == 1 ==> var1 % var2 == 0
357            new NISuppression(var2_eq_1, suppressee),
358
359            // var2 == -1 ==> var1 % var2 == 0
360            new NISuppression(var2_eq_minus_1, suppressee),
361
362            // (var1 == 0) ^ (var2 != 0) ==> var1 % var2 == 0
363            new NISuppression(var1_eq_0, var2_ne_0, suppressee),
364
365            // (var1 == var2) ^ (var2 != 0) ==> var1 % var2 == 0
366            new NISuppression(var1_eq_var2, var2_ne_0, suppressee),
367
368            // (var2 == var1) ^ (var1 != 0) ==> var2 % var1 == 0
369            new NISuppression(var2_eq_var1, var1_ne_0, suppressee),
370
371          });
372    private static NISuppressionSet suppressions_swap = suppressions.swap();
373
374    /**
375     * Returns non-null if this invariant is obvious from an existing, non-falsified linear binary
376     * invariant in the same slice as this invariant. This invariant of the form "x % y == 0" is
377     * falsified if a linear binary invariant is found of the form "a*y - 1*x + 0 == 0"
378     *
379     * @return non-null value iff this invariant is obvious from other invariants in the same slice
380     */
381    @Pure
382    @Override
383    public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) {
384      // First call super type's method, and if it returns non-null, then
385      // this invariant is already known to be obvious, so just return
386      // whatever reason the super type returned.
387      DiscardInfo di = super.isObviousDynamically(vis);
388      if (di != null) {
389        return di;
390      }
391
392      VarInfo var1 = vis[0];
393      VarInfo var2 = vis[1];
394
395      // ensure that var1.varinfo_index <= var2.varinfo_index
396      if (var1.varinfo_index > var2.varinfo_index) {
397        var1 = vis[1];
398        var2 = vis[0];
399      }
400
401      // Find slice corresponding to these two variables.
402      // Ideally, this should always just be ppt if all
403      // falsified invariants have been removed.
404      PptSlice2 ppt2 = ppt.parent.findSlice(var1,var2);
405
406      // If no slice is found , no invariants exist to make this one obvious.
407      if (ppt2 == null) {
408        return null;
409      }
410
411      // For each invariant, check to see if it's a linear binary
412      // invariant of the form "a*y - 1*x + 0 == 0" and if so,
413      // you know this invariant of the form "x % y == 0" is obvious.
414      for(Invariant inv : ppt2.invs) {
415
416        if (inv instanceof LinearBinaryFloat) {
417          LinearBinaryFloat linv = (LinearBinaryFloat) inv;
418
419          // General form for linear binary: a*x + b*y + c == 0,
420          // but a and b can be switched with respect to vis, and either
421          // one may be negative, so instead check:
422          //  - c == 0
423          //  - a*b < 0   (a and b have different signs)
424          //  - |a| == 1 or |b| == 1, so one will divide the other
425          //     While this means that both x % y == 0 and y % x == 0,
426          //     only one of these invariants will still be true at this
427          //     time, and only that one will be falsified by this test.
428          if (!linv.is_false()
429              && Global.fuzzy.eq(linv.core.c, 0)
430              && linv.core.b * linv.core.a < 0
431              && (Global.fuzzy.eq(linv.core.a * linv.core.a, 1)
432                  || Global.fuzzy.eq(linv.core.b * linv.core.b, 1))) {
433            return new DiscardInfo(this, DiscardCode.obvious,
434                                   "Linear binary invariant implies divides");
435          }
436        }
437      }
438
439      return null;
440    }
441
442  }
443
444  /**
445   * Represents the square invariant between two double scalars.
446   * Prints as {@code x = y**2}.
447   */
448  public static class Square extends NumericFloat {
449    // We are Serializable, so we specify a version to allow changes to
450    // method signatures without breaking serialization.  If you add or
451    // remove fields, you should change this number to the current date.
452    static final long serialVersionUID = 20040113L;
453
454    protected Square(PptSlice ppt, boolean swap) {
455      super(ppt, swap);
456    }
457
458    protected Square(boolean swap) {
459      super(swap);
460    }
461
462    private static @Prototype Square proto = new @Prototype Square(false);
463    private static @Prototype Square proto_swap = new @Prototype Square(true);
464
465    /** Returns the prototype invariant. */
466    public static @Prototype Square get_proto(boolean swap) {
467      if (swap) {
468        return proto_swap;
469      } else {
470        return proto;
471      }
472    }
473
474    // Variables starting with dkconfig_ should only be set via the
475    // daikon.config.Configuration interface.
476    /** Boolean. True iff square invariants should be considered. */
477    public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault;
478
479    @Override
480    public boolean enabled() {
481      return dkconfig_enabled;
482    }
483    @Override
484    protected Square instantiate_dyn(@Prototype Square this, PptSlice slice) {
485      return new Square(slice, swap);
486    }
487
488    @Override
489    public String get_format_str(@GuardSatisfied Square this, OutputFormat format) {
490      if (format == OutputFormat.SIMPLIFY) {
491        return "(EQ %var1% (* %var2% %var2))";
492      } else if (format == OutputFormat.CSHARPCONTRACT) {
493        return "%var1% == %var2%*%var2%";
494      } else if (format.isJavaFamily()) {
495
496        return "daikon.Quant.fuzzy.eq(%var1%, %var2%*%var2%)";
497      } else {
498        return "%var1% == %var2%**2";
499      }
500    }
501
502    /** Check to see if x == y squared. */
503    @Override
504    public boolean eq_check(double x, double y) {
505      return Global.fuzzy.eq(x, y*y);
506    }
507
508    // Note there are no NI Suppressions for Square.  Two obvious
509    // suppressions are:
510    //
511    //      (var2 == 1) ^ (var1 == 1)  ==> var1 = var2*var2
512    //      (var2 == 0) ^ (var1 == 0)  ==> var1 = var2*var2
513    //
514    // But all of the antecedents would be constants, so we would
515    // never need to create this slice, so there is no reason to create
516    // these.
517
518  }
519
520  /**
521   * Represents the zero tracks invariant between
522   * two double scalars; that is, when {@code x} is zero,
523   * {@code y} is also zero.
524   * Prints as {@code x = 0 => y = 0}.
525   */
526  public static class ZeroTrack extends NumericFloat {
527    // We are Serializable, so we specify a version to allow changes to
528    // method signatures without breaking serialization.  If you add or
529    // remove fields, you should change this number to the current date.
530    static final long serialVersionUID = 20040313L;
531
532    protected ZeroTrack(PptSlice ppt, boolean swap) {
533      super(ppt, swap);
534    }
535
536    protected @Prototype ZeroTrack(boolean swap) {
537      super(swap);
538    }
539
540    private static @Prototype ZeroTrack proto = new @Prototype ZeroTrack(false);
541    private static @Prototype ZeroTrack proto_swap = new @Prototype ZeroTrack(true);
542
543    /** Returns the prototype invariant. */
544    public static @Prototype ZeroTrack get_proto(boolean swap) {
545      if (swap) {
546        return proto_swap;
547      } else {
548        return proto;
549      }
550    }
551
552    // Variables starting with dkconfig_ should only be set via the
553    // daikon.config.Configuration interface.
554    /** Boolean. True iff zero-track invariants should be considered. */
555    public static boolean dkconfig_enabled = false;
556
557    @Override
558    public boolean enabled() {
559      return dkconfig_enabled;
560    }
561
562    @Override
563    protected ZeroTrack instantiate_dyn(@Prototype ZeroTrack this, PptSlice slice) {
564      return new ZeroTrack(slice, swap);
565    }
566
567    @Override
568    public String get_format_str(@GuardSatisfied ZeroTrack this, OutputFormat format) {
569      if (format == OutputFormat.SIMPLIFY) {
570        return "(IMPLIES (EQ %var1% 0) (EQ %var2% 0))";
571      } else if (format.isJavaFamily() || format == OutputFormat.CSHARPCONTRACT) {
572        return "(!(%var1% == 0)) || (%var2% == 0)";
573      } else {
574        return "(%var1% == 0) ==> (%var2% == 0)";
575      }
576    }
577
578    @Override
579    public boolean eq_check(double x, double y) {
580      if (x == 0) {
581        return y == 0;
582      } else {
583        return true;
584      }
585    }
586
587    /** Returns a list of non-instantiating suppressions for this invariant. */
588    @Pure
589    @Override
590    public NISuppressionSet get_ni_suppressions() {
591      if (swap) {
592        return suppressions_swap;
593      } else {
594        return suppressions;
595      }
596    }
597
598    /** definition of this invariant (the suppressee) (unswapped) */
599    private static NISuppressee suppressee = new NISuppressee(ZeroTrack.class, false);
600
601    private static NISuppressionSet suppressions =
602      new NISuppressionSet(
603          new NISuppression[] {
604            // (var1 == var2) ==> (var1=0 ==> var2=0)
605            new NISuppression(var1_eq_var2, suppressee),
606            // (var1 != 0)    ==> (var1=0 ==> var2=0)
607            new NISuppression(var1_ne_0, suppressee),
608            // (var2 == 0) ==> (var1=0 ==> var2=0)
609            new NISuppression(var2_eq_0, suppressee),
610          });
611    private static NISuppressionSet suppressions_swap = suppressions.swap();
612
613  }
614
615//
616// Standard String invariants
617//
618
619}