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  // We are Serializable, so we specify a version to allow changes to
015  // method signatures without breaking serialization.  If you add or
016  // remove fields, you should change this number to the current date.
017  static final long serialVersionUID = 20020122L;
018
019  protected SingleFloat(PptSlice ppt) {
020    super(ppt);
021  }
022
023  protected @Prototype SingleFloat() {
024    super();
025  }
026
027  /** Returns whether or not the specified types are valid for unary float. */
028  @Override
029  public final boolean valid_types(VarInfo[] vis) {
030    return (vis.length == 1) && vis[0].file_rep_type.isFloat();
031  }
032
033  public VarInfo var(@GuardSatisfied @UnknownInitialization(SingleFloat.class) SingleFloat this) {
034    return ppt.var_infos[0];
035  }
036
037  // Should never be called with modified == ValueTuple.MISSING_NONSENSICAL.
038  // Subclasses need not override this except in special cases;
039  // just implement {@link add_modified(Object,int)}.
040  @Override
041  public InvariantStatus add(@Interned Object val, int mod_index, int count) {
042    assert !falsified;
043    assert (mod_index >= 0) && (mod_index < 2);
044    double value = ((Double) val).doubleValue();
045    if (mod_index == 0) {
046      return add_unmodified(value, count);
047    } else {
048      return add_modified(value, count);
049    }
050  }
051
052  @Override
053  public InvariantStatus check(@Interned Object val, int mod_index, int count) {
054    assert !falsified;
055    assert (mod_index >= 0) && (mod_index < 2);
056    double value = ((Double) val).doubleValue();
057    if (mod_index == 0) {
058      return check_unmodified(value, count);
059    } else {
060      return check_modified(value, count);
061    }
062  }
063
064  /**
065   * Similar to {@link #check_modified} except that it can change the state of the invariant if
066   * necessary. If the invariant doesn't have any state, then the implementation should simply call
067   * {@link #check_modified}. This method need not check for falsification; that is done by the
068   * caller.
069   */
070  public abstract InvariantStatus add_modified(double value, int count);
071
072  /** By default, do nothing if the value hasn't been seen yet. Subclasses can override this. */
073  public InvariantStatus add_unmodified(double value, int count) {
074    // System.out.println("SingleFloat.add_unmodified " + ppt.name() + ": parent=" + ppt.parent);
075    return InvariantStatus.NO_CHANGE;
076  }
077
078  /**
079   * Presents a sample to the invariant. Returns whether the sample is consistent with the
080   * invariant. Does not change the state of the invariant.
081   *
082   * @param count how many identical samples were observed in a row. For example, three calls to
083   *     check_modified with a count parameter of 1 is equivalent to one call to check_modified with
084   *     a count parameter of 3.
085   * @return whether or not the sample is consistent with the invariant
086   */
087  public abstract InvariantStatus check_modified(double value, int count);
088
089  public InvariantStatus check_unmodified(double value, int count) {
090    return InvariantStatus.NO_CHANGE;
091  }
092
093  // This has no additional suppression factories beyond those of Invariant.
094}