001// ***** This file is automatically generated from Numeric.java.jpp
002
003package daikon.inv.binary.twoSequence;
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 PairwiseNumericInt extends TwoSequence {
035
036  static final long serialVersionUID = 20060609L;
037
038  protected PairwiseNumericInt(PptSlice ppt, boolean swap) {
039    super(ppt);
040    this.swap = swap;
041  }
042
043  protected PairwiseNumericInt(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.baseIsIntegral() || !type2.baseIsIntegral()) {
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 PairwiseNumericInt 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 PairwiseNumericInt 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;
089    String v2;
090        if (format.isJavaFamily()) {
091
092            v1 = var1().name_using(format);
093            v2 = var2().name_using(format);
094            if (this instanceof Divides) {
095              return "daikon.Quant.pairwiseDivides(" + v1 + ", " + v2 + ")";
096            } else if (this instanceof Square) {
097              return "daikon.Quant.pairwiseSquare(" + v1 + ", " + v2 + ")";
098            } else if (this instanceof BitwiseComplement) {
099              return "daikon.Quant.pairwiseBitwiseComplement(" +v1+", "+v2+ ")";
100            } else if (this instanceof BitwiseSubset) {
101              return "daikon.Quant.pairwiseBitwiseSubset(" +v1+ ", " + v2 + ")";
102            } else {
103              return format_unimplemented(format);
104            }
105
106        } else if (format == OutputFormat.CSHARPCONTRACT) {
107
108            v1 = var1().csharp_name();
109            v2 = var2().csharp_name();
110            String[] split1 = var1().csharp_array_split();
111            String[] split2 = var2().csharp_array_split();
112            if (this instanceof Divides) {
113              return "Contract.ForAll(0, " + split1[0] + ".Count(), i => " + split1[0] + " [i]" + split1[1] + " % " + split2[0] + "[i]" + split2[1] + " == 0)";
114            } else if (this instanceof Square) {
115              return "Contract.ForAll(0, " + split1[0] + ".Count(), i => " + split1[0] + " [i]" + split1[1] + " == " + split2[0] + "[i]" + split2[1] + "*" + split2[0] + "[i]" + split2[1] + ")";
116            } else if (this instanceof BitwiseComplement) {
117              return "Contract.ForAll(0, " + split1[0] + ".Count(), i => " + split1[0] + " [i]" + split1[1] + " == ~" + split2[0] + "[i]" + split2[1] + ")";
118            } else if (this instanceof BitwiseSubset) {
119              return "Contract.ForAll(0, " + split1[0] + ".Count(), i => " + split1[0] + " [i]" + split1[1] + " == " + split1[0] + "[i]" + split1[1] + " | " + split2[0] + "[i]" + split2[1] + ")";
120            } else {
121              return format_unimplemented(format);
122            }
123
124        }
125
126      if (format == OutputFormat.ESCJAVA) {
127        String[] form = VarInfo.esc_quantify(var1(), var2());
128        fmt_str = form[0] + "(" + fmt_str + ")" + form[3];
129        v1 = form[1];
130        v2 = form[2];
131      } else if (format == OutputFormat.SIMPLIFY) {
132        String[] form = VarInfo.simplify_quantify(QuantFlags.element_wise(),
133                                                   var1(), var2());
134        fmt_str = form[0] + " " + fmt_str + " " + form[3];
135        v1 = form[1];
136        v2 = form[2];
137      } else {
138        v1 = var1().name_using(format);
139        v2 = var2().name_using(format);
140        if (format == OutputFormat.DAIKON) {
141          fmt_str += " (elementwise)";
142        }
143      }
144
145    // Note that we do not use String.replaceAll here, because that's
146    // inseparable from the regex library, and we don't want to have to
147    // escape v1 with something like
148    // v1.replaceAll("([\\$\\\\])", "\\\\$1")
149    fmt_str = fmt_str.replace("%var1%", v1);
150    fmt_str = fmt_str.replace("%var2%", v2);
151
152    // if (false && (format == OutputFormat.DAIKON)) {
153    //   fmt_str = "[" + getClass() + "]" + fmt_str + " ("
154    //          + var1().get_value_info() + ", " + var2().get_value_info() +  ")";
155    // }
156    return fmt_str;
157  }
158
159  /** Calls the function specific equal check and returns the correct status. */
160
161  @Override
162  public InvariantStatus check_modified(long[] x, long[] y,
163                                        int count) {
164    if (x.length != y.length) {
165      if (Debug.logOn()) {
166        log("Falsified - x length = %s y length = %s", x.length, y.length);
167      }
168      return InvariantStatus.FALSIFIED;
169    }
170
171    if (Debug.logDetail()) {
172      log("testing values %s, %s", Arrays.toString (x),
173           Arrays.toString(y));
174    }
175
176    try {
177      for (int i = 0; i < x.length; i++) {
178        if (!eq_check(x[i], y[i])) {
179          if (Debug.logOn()) {
180            log("Falsified - x[%s]=%s y[%s]=%s", i, x[i], i, y[i]);
181          }
182          return InvariantStatus.FALSIFIED;
183        }
184      }
185      return InvariantStatus.NO_CHANGE;
186    } catch (Exception e) {
187      if (Debug.logOn()) {
188        log("Falsified - exception %s", e);
189      }
190      return InvariantStatus.FALSIFIED;
191    }
192  }
193
194  /**
195   * Checks to see if this invariant is over subsequences and if the same relationship holds over
196   * the full sequence. This is obvious if it does. For example 'x[foo..] op y[bar..]' would be
197   * obvious if 'x[] op y[]' This can't fully be handled as a suppression since a suppression needs
198   * to insure that foo == bar as well. But that is not a requirement here (the fact that 'x[] op
199   * y[]' implies that foo == bar when x[] and y[] are not missing).
200   */
201  public @Nullable DiscardInfo is_subsequence(VarInfo[] vis) {
202
203    VarInfo v1 = var1(vis);
204    VarInfo v2 = var2(vis);
205
206    // Make sure each var is a sequence subsequence
207    if (!v1.isDerived() || !(v1.derived instanceof SequenceScalarSubsequence)) {
208      return null;
209    }
210    if (!v2.isDerived() || !(v2.derived instanceof SequenceScalarSubsequence)) {
211      return null;
212    }
213
214    @NonNull SequenceScalarSubsequence der1 = (SequenceScalarSubsequence) v1.derived;
215    @NonNull SequenceScalarSubsequence der2 = (SequenceScalarSubsequence) v2.derived;
216
217    // Both of the indices must be either from the start or up to the end.
218    // It is not necessary to check that they match in any other way since
219    // if the supersequence holds, that implies that the sequences are
220    // of the same length.  Thus any subsequence that starts from the
221    // beginning or finishes at the end must end or start at the same
222    // spot (or it would have been falsified when it didn't)
223    if (der1.from_start != der2.from_start) {
224      return null;
225    }
226
227    // Look up this class over the sequence variables
228    Invariant inv = find(getClass(), der1.seqvar(), der2.seqvar());
229    if (inv == null) {
230      return null;
231    }
232    return new DiscardInfo(this, DiscardCode.obvious, "Implied by "
233                           + inv.format());
234  }
235
236  @Pure
237  @Override
238  public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) {
239
240    DiscardInfo super_result = super.isObviousDynamically(vis);
241    if (super_result != null) {
242      return super_result;
243    }
244
245      // any elementwise relation across subsequences is made obvious by
246      // the same relation across the original sequence
247      DiscardInfo result = is_subsequence(vis);
248      if (result != null) {
249        return result;
250      }
251
252    // Check for invariant specific obvious checks.  The obvious_checks
253    // method returns an array of arrays of antecedents.  If all of the
254    // antecedents in an array are true, then the invariant is obvoius.
255    InvDef[][] obvious_arr = obvious_checks(vis);
256    obvious_loop:
257    for (int i = 0; i < obvious_arr.length; i++) {
258      InvDef[] antecedents = obvious_arr[i];
259      StringBuilder why = null;
260      for (int j = 0; j < antecedents.length; j++) {
261        Invariant inv = antecedents[j].find();
262        if (inv == null) {
263          continue obvious_loop;
264        }
265        if (why == null) {
266          why = new StringBuilder(inv.format());
267        } else {
268          why.append(" and ");
269          why.append(inv.format());
270        }
271      }
272      return new DiscardInfo(this, DiscardCode.obvious, "Implied by " + why);
273    }
274
275    return null;
276  }
277
278  /**
279   * Returns an invariant that is true when the size(v1) == size(v2). There are a number of
280   * possible cases for an array:
281   *
282   * <pre>
283   *    x[]         - entire array, size usually available as size(x[])
284   *    x[..(n-1)]  - size is n
285   *    x[..n]      - size is n+1
286   *    x[n..]      - size is size(x[]) - n
287   *    x[(n+1)..]  - size is size(x[]) - (n+1)
288   * </pre>
289   *
290   * Each combination of the above must be considered in creating the equality invariant. Not all
291   * possibilities can be handled. Null is returned in that case. In the following table, s stands
292   * for the size
293   *
294   * <pre>
295   *                    x[]     x[..(n-1)]  x[..n]  x[n..]    x[(n+1)..]
296   *                  --------- ----------  ------  ------    ----------
297   *    y[]           s(y)=s(x)   s(y)=n
298   *    y[..(m-1)]        x         m=n
299   *    y[..m]            x         x         m=n
300   *    y[m..]            x         x          x     m=n &and;
301   *                                                s(y)=s(x)
302   *    y[(m+1)..]        x         x          x        x       m=n &and;
303   *                                                           s(y)=s(x)
304   * </pre>
305   * NOTE: this is not currently used. Many (if not all) of the missing table cells above could be
306   * filled in with linear binary invariants (eg, m = n + 1).
307   */
308  public @Nullable InvDef array_sizes_eq(VarInfo v1, VarInfo v2) {
309
310    VarInfo v1_size = get_array_size(v1);
311    VarInfo v2_size = get_array_size(v2);
312
313    // If we can find a size variable for each side build the invariant
314    if ((v1_size != null) && (v2_size != null)) {
315      return new InvDef(v1_size, v2_size, IntEqual.class);
316    }
317
318    // If either variable is not derived, there is no possible invariant
319    // (since we covered all of the direct size comparisons above)
320    if ((v1.derived == null) || (v2.derived == null)) {
321      return null;
322    }
323
324    // Get the sequence subsequence derivations
325    SequenceScalarSubsequence v1_ss = (SequenceScalarSubsequence) v1.derived;
326    SequenceScalarSubsequence v2_ss = (SequenceScalarSubsequence) v2.derived;
327
328    // If both are from_start and have the same index_shift, just compare
329    // the variables
330    if (v1_ss.from_start && v2_ss.from_start
331        && (v1_ss.index_shift == v2_ss.index_shift)) {
332      return new InvDef(v1_ss.sclvar(), v2_ss.sclvar(), IntEqual.class);
333    }
334
335    return null;
336  }
337
338  /**
339   * Returns a variable that corresponds to the size of v. Returns null if no such variable exists.
340   *
341   * There are two cases that are not handled: x[..n] with an index shift and x[n..].
342   */
343  public @Nullable VarInfo get_array_size(VarInfo v) {
344
345    assert v.rep_type.isArray();
346
347    if (v.derived == null) {
348      return v.sequenceSize();
349    } else if (v.derived instanceof SequenceScalarSubsequence) {
350      SequenceScalarSubsequence ss = (SequenceScalarSubsequence) v.derived;
351      if (ss.from_start && (ss.index_shift == -1)) {
352        return ss.sclvar();
353      }
354    }
355
356    return null;
357  }
358
359  /**
360   * Return a format string for the specified output format. Each instance of %varN% will be
361   * replaced by the correct name for varN.
362   */
363  public abstract String get_format_str(@GuardSatisfied PairwiseNumericInt this, OutputFormat format);
364
365  /** Returns true if x and y don't invalidate the invariant. */
366  public abstract boolean eq_check(long x, long y);
367
368  /**
369   * Returns an array of arrays of antecedents. If all of the antecedents in any array are true,
370   * then the invariant is obvious.
371   */
372  public InvDef[][] obvious_checks(VarInfo[] vis) {
373    return new InvDef[][] {};
374  }
375
376  public static List<@Prototype Invariant> get_proto_all() {
377
378    List<@Prototype Invariant> result = new ArrayList<>();
379
380      result.add(Divides.get_proto(false));
381      result.add(Divides.get_proto(true));
382      result.add(Square.get_proto(false));
383      result.add(Square.get_proto(true));
384
385      result.add(BitwiseComplement.get_proto());
386      result.add(BitwiseSubset.get_proto(false));
387      result.add(BitwiseSubset.get_proto(true));
388
389    // System.out.printf("%s get proto: %s%n", PairwiseNumericInt.class, result);
390    return result;
391  }
392
393  // suppressor definitions, used by many of the classes below
394  protected static NISuppressor
395
396      var1_eq_0       = new NISuppressor(0, EltRangeInt.EqualZero.class),
397      var2_eq_0       = new NISuppressor(1, EltRangeInt.EqualZero.class),
398      var1_ge_0       = new NISuppressor(0, EltRangeInt.GreaterEqualZero.class),
399      var2_ge_0       = new NISuppressor(1, EltRangeInt.GreaterEqualZero.class),
400      var1_eq_1       = new NISuppressor(0, EltRangeInt.EqualOne.class),
401      var2_eq_1       = new NISuppressor(1, EltRangeInt.EqualOne.class),
402      var1_eq_minus_1 = new NISuppressor(0, EltRangeInt.EqualMinusOne.class),
403      var2_eq_minus_1 = new NISuppressor(1, EltRangeInt.EqualMinusOne.class),
404      var1_ne_0       = new NISuppressor(0, EltNonZero.class),
405      var2_ne_0       = new NISuppressor(1, EltNonZero.class),
406      var1_le_var2    = new NISuppressor(0, 1, PairwiseIntLessEqual.class),
407
408    var1_eq_var2    = new NISuppressor(0, 1, PairwiseIntEqual.class),
409    var2_eq_var1    = new NISuppressor(0, 1, PairwiseIntEqual.class);
410
411    protected static NISuppressor var2_valid_shift =
412      new NISuppressor(1, EltRangeInt.Bound0_63.class);
413
414  //
415  // Int and Float Numeric Invariants
416  //
417
418  /**
419   * Represents the divides without remainder invariant between corresponding elements of two sequences of long.
420   * Prints as {@code x[] % y[] == 0}.
421   */
422  public static class Divides extends PairwiseNumericInt {
423    // We are Serializable, so we specify a version to allow changes to
424    // method signatures without breaking serialization.  If you add or
425    // remove fields, you should change this number to the current date.
426    static final long serialVersionUID = 20040113L;
427
428    protected Divides(PptSlice ppt, boolean swap) {
429      super(ppt, swap);
430    }
431
432    protected Divides(boolean swap) {
433      super(swap);
434    }
435
436    private static @Prototype Divides proto = new @Prototype Divides(false);
437    private static @Prototype Divides proto_swap = new @Prototype Divides(true);
438
439    /** Returns the prototype invariant. */
440    public static @Prototype PairwiseNumericInt get_proto(boolean swap) {
441      if (swap) {
442        return proto_swap;
443      } else {
444        return proto;
445      }
446    }
447
448    // Variables starting with dkconfig_ should only be set via the
449    // daikon.config.Configuration interface.
450    /** Boolean. True iff divides invariants should be considered. */
451    public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault;
452
453    @Override
454    public boolean enabled() {
455      return dkconfig_enabled;
456    }
457
458    @Override
459    protected Divides instantiate_dyn(@Prototype Divides this, PptSlice slice) {
460      return new Divides(slice, swap);
461    }
462
463    @Override
464    public String get_format_str(@GuardSatisfied Divides this, OutputFormat format) {
465      if (format == OutputFormat.SIMPLIFY) {
466        return "(EQ 0 (MOD %var1% %var2%))";
467      } else {
468        return "%var1% % %var2% == 0";
469      }
470    }
471
472    @Override
473    public boolean eq_check(long x, long y) {
474      return (0 == (x % y));
475    }
476
477      /**
478       * This needs to be an obvious check and not a suppression for sequences because there is no
479       * consistent way to check that var1 and var2 have the same length (for derivations).
480       */
481      @Override
482      public InvDef[][] obvious_checks(VarInfo[] vis) {
483
484        return new InvDef[][] {
485          new InvDef[] {
486            new InvDef(var2(vis), EltOneOf.class, InvDef.elts_minus_one_and_plus_one)
487          },
488          new InvDef[] {
489            new InvDef(var1(), EltOneOf.class, InvDef.elts_zero)
490          }
491        };
492      }
493
494    /** Returns a list of non-instantiating suppressions for this invariant. */
495    @Pure
496    @Override
497    public NISuppressionSet get_ni_suppressions() {
498      if (swap) {
499        return suppressions_swap;
500      } else {
501        return suppressions;
502      }
503    }
504
505    /** definition of this invariant (the suppressee) (unswapped) */
506    private static NISuppressee suppressee = new NISuppressee(Divides.class, false);
507
508    private static NISuppressionSet suppressions =
509      new NISuppressionSet(
510          new NISuppression[] {
511
512            // (var1 == var2) ^ (var2 != 0) ==> var1 % var2 == 0
513            new NISuppression(var1_eq_var2, var2_ne_0, suppressee),
514
515            // (var2 == var1) ^ (var1 != 0) ==> var2 % var1 == 0
516            new NISuppression(var2_eq_var1, var1_ne_0, suppressee),
517
518          });
519    private static NISuppressionSet suppressions_swap = suppressions.swap();
520
521    /**
522     * Returns non-null if this invariant is obvious from an existing, non-falsified linear binary
523     * invariant in the same slice as this invariant. This invariant of the form "x % y == 0" is
524     * falsified if a linear binary invariant is found of the form "a*y - 1*x + 0 == 0"
525     *
526     * @return non-null value iff this invariant is obvious from other invariants in the same slice
527     */
528    @Pure
529    @Override
530    public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) {
531      // First call super type's method, and if it returns non-null, then
532      // this invariant is already known to be obvious, so just return
533      // whatever reason the super type returned.
534      DiscardInfo di = super.isObviousDynamically(vis);
535      if (di != null) {
536        return di;
537      }
538
539      VarInfo var1 = vis[0];
540      VarInfo var2 = vis[1];
541
542      // ensure that var1.varinfo_index <= var2.varinfo_index
543      if (var1.varinfo_index > var2.varinfo_index) {
544        var1 = vis[1];
545        var2 = vis[0];
546      }
547
548      // Find slice corresponding to these two variables.
549      // Ideally, this should always just be ppt if all
550      // falsified invariants have been removed.
551      PptSlice2 ppt2 = ppt.parent.findSlice(var1,var2);
552
553      // If no slice is found , no invariants exist to make this one obvious.
554      if (ppt2 == null) {
555        return null;
556      }
557
558      // For each invariant, check to see if it's a linear binary
559      // invariant of the form "a*y - 1*x + 0 == 0" and if so,
560      // you know this invariant of the form "x % y == 0" is obvious.
561      for(Invariant inv : ppt2.invs) {
562
563        if (inv instanceof LinearBinary) {
564          LinearBinary linv = (LinearBinary) inv;
565
566          // General form for linear binary: a*x + b*y + c == 0,
567          // but a and b can be switched with respect to vis, and either
568          // one may be negative, so instead check:
569          //  - c == 0
570          //  - a*b < 0   (a and b have different signs)
571          //  - |a| == 1 or |b| == 1, so one will divide the other
572          //     While this means that both x % y == 0 and y % x == 0,
573          //     only one of these invariants will still be true at this
574          //     time, and only that one will be falsified by this test.
575          if (!linv.is_false()
576              && Global.fuzzy.eq(linv.core.c, 0)
577              && linv.core.b * linv.core.a < 0
578              && (Global.fuzzy.eq(linv.core.a * linv.core.a, 1)
579                  || Global.fuzzy.eq(linv.core.b * linv.core.b, 1))) {
580            return new DiscardInfo(this, DiscardCode.obvious,
581                                   "Linear binary invariant implies divides");
582          }
583        }
584      }
585
586      return null;
587    }
588
589  }
590
591  /**
592   * Represents the square invariant between corresponding elements of two sequences of long.
593   * Prints as {@code x[] = y[]**2}.
594   */
595  public static class Square extends PairwiseNumericInt {
596    // We are Serializable, so we specify a version to allow changes to
597    // method signatures without breaking serialization.  If you add or
598    // remove fields, you should change this number to the current date.
599    static final long serialVersionUID = 20040113L;
600
601    protected Square(PptSlice ppt, boolean swap) {
602      super(ppt, swap);
603    }
604
605    protected Square(boolean swap) {
606      super(swap);
607    }
608
609    private static @Prototype Square proto = new @Prototype Square(false);
610    private static @Prototype Square proto_swap = new @Prototype Square(true);
611
612    /** Returns the prototype invariant. */
613    public static @Prototype Square get_proto(boolean swap) {
614      if (swap) {
615        return proto_swap;
616      } else {
617        return proto;
618      }
619    }
620
621    // Variables starting with dkconfig_ should only be set via the
622    // daikon.config.Configuration interface.
623    /** Boolean. True iff square invariants should be considered. */
624    public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault;
625
626    @Override
627    public boolean enabled() {
628      return dkconfig_enabled;
629    }
630    @Override
631    protected Square instantiate_dyn(@Prototype Square this, PptSlice slice) {
632      return new Square(slice, swap);
633    }
634
635    @Override
636    public String get_format_str(@GuardSatisfied Square this, OutputFormat format) {
637      if (format == OutputFormat.SIMPLIFY) {
638        return "(EQ %var1% (* %var2% %var2))";
639      } else if (format == OutputFormat.CSHARPCONTRACT) {
640        return "%var1% == %var2%*%var2%";
641      } else if (format.isJavaFamily()) {
642
643        return "%var1% == %var2%*%var2%";
644      } else {
645        return "%var1% == %var2%**2";
646      }
647    }
648
649    /** Check to see if x == y squared. */
650    @Override
651    public boolean eq_check(long x, long y) {
652      return (x == y*y);
653    }
654
655    // Note there are no NI Suppressions for Square.  Two obvious
656    // suppressions are:
657    //
658    //      (var2 == 1) ^ (var1 == 1)  ==> var1 = var2*var2
659    //      (var2 == 0) ^ (var1 == 0)  ==> var1 = var2*var2
660    //
661    // But all of the antecedents would be constants, so we would
662    // never need to create this slice, so there is no reason to create
663    // these.
664
665  }
666
667  /**
668   * Represents the zero tracks invariant between
669   * corresponding elements of two sequences of long; that is, when {@code x[]} is zero,
670   * {@code y[]} is also zero.
671   * Prints as {@code x[] = 0 => y[] = 0}.
672   */
673  public static class ZeroTrack extends PairwiseNumericInt {
674    // We are Serializable, so we specify a version to allow changes to
675    // method signatures without breaking serialization.  If you add or
676    // remove fields, you should change this number to the current date.
677    static final long serialVersionUID = 20040313L;
678
679    protected ZeroTrack(PptSlice ppt, boolean swap) {
680      super(ppt, swap);
681    }
682
683    protected @Prototype ZeroTrack(boolean swap) {
684      super(swap);
685    }
686
687    private static @Prototype ZeroTrack proto = new @Prototype ZeroTrack(false);
688    private static @Prototype ZeroTrack proto_swap = new @Prototype ZeroTrack(true);
689
690    /** Returns the prototype invariant. */
691    public static @Prototype ZeroTrack get_proto(boolean swap) {
692      if (swap) {
693        return proto_swap;
694      } else {
695        return proto;
696      }
697    }
698
699    // Variables starting with dkconfig_ should only be set via the
700    // daikon.config.Configuration interface.
701    /** Boolean. True iff zero-track invariants should be considered. */
702    public static boolean dkconfig_enabled = false;
703
704    @Override
705    public boolean enabled() {
706      return dkconfig_enabled;
707    }
708
709    @Override
710    protected ZeroTrack instantiate_dyn(@Prototype ZeroTrack this, PptSlice slice) {
711      return new ZeroTrack(slice, swap);
712    }
713
714    @Override
715    public String get_format_str(@GuardSatisfied ZeroTrack this, OutputFormat format) {
716      if (format == OutputFormat.SIMPLIFY) {
717        return "(IMPLIES (EQ %var1% 0) (EQ %var2% 0))";
718      } else if (format.isJavaFamily() || format == OutputFormat.CSHARPCONTRACT) {
719        return "(!(%var1% == 0)) || (%var2% == 0)";
720      } else {
721        return "(%var1% == 0) ==> (%var2% == 0)";
722      }
723    }
724
725    @Override
726    public boolean eq_check(long x, long y) {
727      if (x == 0) {
728        return y == 0;
729      } else {
730        return true;
731      }
732    }
733
734    /** Returns a list of non-instantiating suppressions for this invariant. */
735    @Pure
736    @Override
737    public NISuppressionSet get_ni_suppressions() {
738      if (swap) {
739        return suppressions_swap;
740      } else {
741        return suppressions;
742      }
743    }
744
745    /** definition of this invariant (the suppressee) (unswapped) */
746    private static NISuppressee suppressee = new NISuppressee(ZeroTrack.class, false);
747
748    private static NISuppressionSet suppressions =
749      new NISuppressionSet(
750          new NISuppression[] {
751            // (var1 == var2) ==> (var1=0 ==> var2=0)
752            new NISuppression(var1_eq_var2, suppressee),
753            // (var1 != 0)    ==> (var1=0 ==> var2=0)
754            new NISuppression(var1_ne_0, suppressee),
755            // (var2 == 0) ==> (var1=0 ==> var2=0)
756            new NISuppression(var2_eq_0, suppressee),
757          });
758    private static NISuppressionSet suppressions_swap = suppressions.swap();
759
760  }
761
762  /**
763   * Represents the bitwise complement invariant between corresponding elements of two sequences of long.
764   * Prints as {@code x[] = ~y[]}.
765   */
766  public static class BitwiseComplement extends PairwiseNumericInt {
767    // We are Serializable, so we specify a version to allow changes to
768    // method signatures without breaking serialization.  If you add or
769    // remove fields, you should change this number to the current date.
770    static final long serialVersionUID = 20040113L;
771
772    protected BitwiseComplement(PptSlice ppt) {
773      super(ppt, false);
774    }
775
776    protected @Prototype BitwiseComplement() {
777      super(false);
778    }
779
780    private static @Prototype BitwiseComplement proto = new @Prototype BitwiseComplement();
781
782    /** Returns the prototype invariant. */
783    public static @Prototype BitwiseComplement get_proto() {
784      return proto;
785    }
786
787    // Variables starting with dkconfig_ should only be set via the
788    // daikon.config.Configuration interface.
789    /** Boolean. True iff bitwise complement invariants should be considered. */
790    public static boolean dkconfig_enabled = false;
791
792    @Override
793    public boolean enabled() {
794      return dkconfig_enabled;
795    }
796
797    @Override
798    protected BitwiseComplement instantiate_dyn(@Prototype BitwiseComplement this, PptSlice slice) {
799      return new BitwiseComplement(slice);
800    }
801
802    @Pure
803    @Override
804    public boolean is_symmetric() {
805      return true;
806    }
807
808    @Override
809    public String get_format_str(@GuardSatisfied BitwiseComplement this, OutputFormat format) {
810      if (format == OutputFormat.SIMPLIFY) {
811        return "(EQ %var1% (~ %var2%))";
812      } else {
813        return "%var1% == ~%var2%";
814      }
815    }
816
817    /** Check to see if x == ~y . */
818    @Override
819    public boolean eq_check(long x, long y) {
820      return (x == ~y);
821    }
822  }
823
824  /**
825   * Represents the bitwise subset invariant between corresponding elements of two sequences of long; that is, the bits of
826   * {@code y[]} are a subset of the bits of {@code x[]}.
827   * Prints as {@code x[] = y[] | x[]}.
828   */
829  public static class BitwiseSubset extends PairwiseNumericInt {
830    // We are Serializable, so we specify a version to allow changes to
831    // method signatures without breaking serialization.  If you add or
832    // remove fields, you should change this number to the current date.
833    static final long serialVersionUID = 20040113L;
834
835    protected BitwiseSubset(PptSlice ppt, boolean swap) {
836      super(ppt, swap);
837    }
838
839    protected BitwiseSubset(boolean swap) {
840      super(swap);
841    }
842
843    private static @Prototype BitwiseSubset proto = new @Prototype BitwiseSubset(false);
844    private static @Prototype BitwiseSubset proto_swap = new @Prototype BitwiseSubset(true);
845
846    /** Returns the prototype invariant. */
847    public static @Prototype BitwiseSubset get_proto(boolean swap) {
848      if (swap) {
849        return proto_swap;
850      } else {
851        return proto;
852      }
853    }
854
855    // Variables starting with dkconfig_ should only be set via the
856    // daikon.config.Configuration interface.
857    /** Boolean. True iff bitwise subset invariants should be considered. */
858    public static boolean dkconfig_enabled = false;
859
860    @Override
861    public boolean enabled() {
862      return dkconfig_enabled;
863    }
864
865    @Override
866    public BitwiseSubset instantiate_dyn(@Prototype BitwiseSubset this, PptSlice slice) {
867      return new BitwiseSubset(slice, swap);
868    }
869
870    @Override
871    public String get_format_str(@GuardSatisfied BitwiseSubset this, OutputFormat format) {
872      if (format == OutputFormat.SIMPLIFY) {
873        return "(EQ %var1% (|java-bitwise-or| %var2% %var1%))";
874      } else if (format == OutputFormat.DAIKON) {
875        return "%var2% is a bitwise subset of %var1%";
876      } else {
877        return "%var1% == (%var2% | %var1%)";
878      }
879    }
880
881    @Override
882    public boolean eq_check(long x, long y) {
883      return (x == (y | x));
884    }
885
886      /**
887       * This needs to be an obvious check and not a suppression for sequences because there is no
888       * consistent way to check that var1 and var2 have the same length (for derivations).
889       */
890      @Override
891      public InvDef[][] obvious_checks(VarInfo[] vis) {
892
893        return new InvDef[][] {
894          // suppress if var2 == 0
895          new InvDef[] {new InvDef(var2(), EltOneOf.class, InvDef.elts_zero)},
896          // suppress if var1 == -1 (all of its bits are on)
897          new InvDef[] {new InvDef(var1(), EltOneOf.class, InvDef.elts_minus_one)}
898        };
899      }
900
901    /** Returns a list of non-instantiating suppressions for this invariant. */
902    @Pure
903    @Override
904    public NISuppressionSet get_ni_suppressions() {
905      if (swap) {
906        return suppressions_swap;
907      } else {
908        return suppressions;
909      }
910    }
911
912    /** definition of this invariant (the suppressee) (unswapped) */
913    private static NISuppressee suppressee = new NISuppressee(BitwiseSubset.class, false);
914
915    private static NISuppressionSet suppressions =
916      new NISuppressionSet(
917          new NISuppression[] {
918
919              // (var1 == var2) ==> var1 = (var2 | var1)
920              new NISuppression(var1_eq_var2, suppressee),
921
922      });
923    private static NISuppressionSet suppressions_swap = suppressions.swap();
924  }
925
926  /**
927   * Represents the BitwiseAnd == 0 invariant between corresponding elements of two sequences of long; that is, {@code x[]} and
928   * {@code y[]} have no bits in common.
929   * Prints as {@code x[] & y[] == 0}.
930   */
931  public static class BitwiseAndZero extends PairwiseNumericInt {
932    // We are Serializable, so we specify a version to allow changes to
933    // method signatures without breaking serialization.  If you add or
934    // remove fields, you should change this number to the current date.
935    static final long serialVersionUID = 20040313L;
936
937    protected BitwiseAndZero(PptSlice ppt) {
938      super(ppt, false);
939    }
940
941    protected @Prototype BitwiseAndZero() {
942      super(false);
943    }
944
945    private static @Prototype BitwiseAndZero proto = new @Prototype BitwiseAndZero();
946
947    /** Returns the prototype invariant. */
948    public static @Prototype BitwiseAndZero get_proto() {
949      return proto;
950    }
951
952    // Variables starting with dkconfig_ should only be set via the
953    // daikon.config.Configuration interface.
954    /** Boolean. True iff BitwiseAndZero invariants should be considered. */
955    public static boolean dkconfig_enabled = false;
956
957    @Override
958    public boolean enabled() {
959      return dkconfig_enabled;
960    }
961
962    @Override
963    public BitwiseAndZero instantiate_dyn(@Prototype BitwiseAndZero this, PptSlice slice) {
964      return new BitwiseAndZero(slice);
965    }
966
967    @Override
968    public String get_format_str(@GuardSatisfied BitwiseAndZero this, OutputFormat format) {
969      if (format == OutputFormat.SIMPLIFY) {
970        return "(EQ (|java-&| %var1% %var2%) 0)";
971      } else {
972        return "(%var1% & %var2%) == 0";
973      }
974    }
975
976    @Pure
977    @Override
978    public boolean is_symmetric() {
979      return true;
980    }
981
982    @Override
983    public boolean eq_check(long x, long y) {
984      return (x & y) == 0;
985    }
986
987    /** Returns a list of non-instantiating suppressions for this invariant. */
988    @Pure
989    @Override
990    public @Nullable NISuppressionSet get_ni_suppressions() {
991      return suppressions;
992    }
993
994    private static @Nullable NISuppressionSet suppressions = null;
995
996  }
997
998  /**
999   * Represents the ShiftZero invariant between corresponding elements of two sequences of long; that is, {@code x[]}
1000   * right-shifted by {@code y[]} is always zero.
1001   * Prints as {@code x[] >> y[] = 0}.
1002   */
1003  public static class ShiftZero  extends PairwiseNumericInt {
1004    // We are Serializable, so we specify a version to allow changes to
1005    // method signatures without breaking serialization.  If you add or
1006    // remove fields, you should change this number to the current date.
1007    static final long serialVersionUID = 20040313L;
1008
1009    protected ShiftZero(PptSlice ppt, boolean swap) {
1010      super(ppt, swap);
1011    }
1012
1013    protected ShiftZero(boolean swap) {
1014      super(swap);
1015    }
1016
1017    private static @Prototype ShiftZero proto = new @Prototype ShiftZero(false);
1018    private static @Prototype ShiftZero proto_swap = new @Prototype ShiftZero(true);
1019
1020    /** Returns the prototype invariant. */
1021    public static @Prototype ShiftZero get_proto(boolean swap) {
1022      if (swap) {
1023        return proto_swap;
1024      } else {
1025        return proto;
1026      }
1027    }
1028
1029    // Variables starting with dkconfig_ should only be set via the
1030    // daikon.config.Configuration interface.
1031    /** Boolean. True iff ShiftZero invariants should be considered. */
1032    public static boolean dkconfig_enabled = false;
1033
1034    @Override
1035    public boolean enabled() {
1036      return dkconfig_enabled;
1037    }
1038
1039    @Override
1040    protected ShiftZero instantiate_dyn(@Prototype ShiftZero this, PptSlice slice) {
1041      return new ShiftZero(slice, swap);
1042    }
1043
1044    @Override
1045    public String get_format_str(@GuardSatisfied ShiftZero this, OutputFormat format) {
1046      if (format == OutputFormat.SIMPLIFY) {
1047        return "(EQ (|java->>| %var1% %var2%) 0)";
1048      } else {
1049        return "(%var1% >> %var2% == 0)";
1050      }
1051    }
1052
1053    @Override
1054    public boolean eq_check(long x, long y) {
1055      if ((y < 0) || (y > 63)) {
1056        throw new ArithmeticException("shift op (" + y + ") is out of range");
1057      }
1058      return (x >> y) == 0;
1059    }
1060
1061    /** Returns a list of non-instantiating suppressions for this invariant. */
1062    @Pure
1063    @Override
1064    public NISuppressionSet get_ni_suppressions() {
1065      if (swap) {
1066        return suppressions_swap;
1067      } else {
1068        return suppressions;
1069      }
1070    }
1071
1072    /** definition of this invariant (the suppressee) (unswapped) */
1073    private static NISuppressee suppressee = new NISuppressee(ShiftZero.class, false);
1074
1075    private static NISuppressionSet suppressions =
1076      new NISuppressionSet(
1077          new NISuppression[] {
1078              // (var1>=0) ^ (var1<=var2) ^ (0<=var2<=63) ==> (var1 >> var2) == 0
1079              new NISuppression(var1_ge_0, var1_le_var2, var2_valid_shift,
1080                                suppressee),
1081          });
1082    private static NISuppressionSet suppressions_swap = suppressions.swap();
1083  }
1084
1085//
1086// Standard String invariants
1087//
1088
1089}