001package daikon.inv.unary.scalar;
002
003import daikon.PptSlice;
004import daikon.VarInfo;
005import daikon.inv.InvariantStatus;
006import daikon.inv.unary.UnaryInvariant;
007import org.checkerframework.checker.initialization.qual.UnknownInitialization;
008import org.checkerframework.checker.interning.qual.Interned;
009import org.checkerframework.checker.lock.qual.GuardSatisfied;
010import typequals.prototype.qual.Prototype;
011
012/** Abstract base class for invariants over one variable of type {@code double}. */
013public abstract class SingleFloat extends UnaryInvariant {
014  static final long serialVersionUID = 20020122L;
015
016  protected SingleFloat(PptSlice ppt) {
017    super(ppt);
018  }
019
020  protected @Prototype SingleFloat() {
021    super();
022  }
023
024  @Override
025  public final boolean valid_types(VarInfo[] vis) {
026    return (vis.length == 1) && vis[0].file_rep_type.isFloat();
027  }
028
029  public VarInfo var(@GuardSatisfied @UnknownInitialization(SingleFloat.class) SingleFloat this) {
030    return ppt.var_infos[0];
031  }
032
033  // Should never be called with modified == ValueTuple.MISSING_NONSENSICAL.
034  // Subclasses need not override this except in special cases;
035  // just implement {@link add_modified(Object,int)}.
036  @Override
037  public InvariantStatus add(@Interned Object val, int mod_index, int count) {
038    assert !falsified;
039    assert (mod_index >= 0) && (mod_index < 2);
040    double value = ((Double) val).doubleValue();
041    if (mod_index == 0) {
042      return add_unmodified(value, count);
043    } else {
044      return add_modified(value, count);
045    }
046  }
047
048  @Override
049  public InvariantStatus check(@Interned Object val, int mod_index, int count) {
050    assert !falsified;
051    assert (mod_index >= 0) && (mod_index < 2);
052    double value = ((Double) val).doubleValue();
053    if (mod_index == 0) {
054      return check_unmodified(value, count);
055    } else {
056      return check_modified(value, count);
057    }
058  }
059
060  /**
061   * Similar to {@link #check_modified} except that it can change the state of the invariant if
062   * necessary. If the invariant doesn't have any state, then the implementation should simply call
063   * {@link #check_modified}. This method need not check for falsification; that is done by the
064   * caller.
065   */
066  public abstract InvariantStatus add_modified(double value, int count);
067
068  /** By default, do nothing if the value hasn't been seen yet. Subclasses can override this. */
069  public InvariantStatus add_unmodified(double value, int count) {
070    // System.out.println("SingleFloat.add_unmodified " + ppt.name() + ": parent=" + ppt.parent);
071    return InvariantStatus.NO_CHANGE;
072  }
073
074  /**
075   * Presents a sample to the invariant. Returns whether the sample is consistent with the
076   * invariant. Does not change the state of the invariant.
077   *
078   * @param count how many identical samples were observed in a row. For example, three calls to
079   *     check_modified with a count parameter of 1 is equivalent to one call to check_modified with
080   *     a count parameter of 3.
081   * @return whether or not the sample is consistent with the invariant
082   */
083  public abstract InvariantStatus check_modified(double value, int count);
084
085  public InvariantStatus check_unmodified(double value, int count) {
086    return InvariantStatus.NO_CHANGE;
087  }
088
089  // This has no additional suppression factories beyond those of Invariant.
090}