001package daikon.inv.unary.sequence;
002
003import daikon.PptSlice;
004import daikon.VarInfo;
005import daikon.inv.InvariantStatus;
006import org.checkerframework.checker.initialization.qual.UnknownInitialization;
007import org.checkerframework.checker.interning.qual.Interned;
008import org.checkerframework.checker.lock.qual.GuardSatisfied;
009import org.plumelib.util.Intern;
010import typequals.prototype.qual.Prototype;
011
012/** Abstract base class for invariants over one variable of type {@code long[]}. */
013public abstract class SingleScalarSequence extends SingleSequence {
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 = 20020813;
018
019  protected SingleScalarSequence(PptSlice ppt) {
020    super(ppt);
021  }
022
023  protected @Prototype SingleScalarSequence() {
024    super();
025  }
026
027  /** Returns whether or not the specified types are valid. (Static version of method.) */
028  public static final boolean valid_types_static(VarInfo[] vis) {
029    return ((vis.length == 1)
030        && vis[0].file_rep_type.baseIsScalar()
031        && vis[0].file_rep_type.isArray());
032  }
033
034  /** Returns whether or not the specified types are valid. */
035  @Override
036  public final boolean valid_types(VarInfo[] vis) {
037    return valid_types_static(vis);
038  }
039
040  // Identical to superclass definition, and therefore gratuitious
041  @Override
042  public VarInfo var(
043      @GuardSatisfied @UnknownInitialization(SingleSequence.class) SingleScalarSequence this) {
044    return ppt.var_infos[0];
045  }
046
047  // Should never be called with modified == ValueTuple.MISSING.
048  // Subclasses need not override this except in special cases;
049  // just implement {@link #add_modified(Object,int)}.
050  @Override
051  public InvariantStatus add(@Interned Object val, int mod_index, int count) {
052    assert !falsified;
053    assert (mod_index >= 0) && (mod_index < 2);
054    assert Intern.isInterned(val) : "not interned: " + val + "/" + val.getClass();
055    assert Intern.isInterned(val);
056    // System.out.println("SingleScalarSequence.add(" + Arrays.toString(value) + ", " + modified +
057    // ", " + count + ")");
058    long[] value = (long[]) val;
059    if (value == null) {
060      return InvariantStatus.NO_CHANGE;
061    } else if (mod_index == 0) {
062      return add_unmodified(value, count);
063    } else {
064      return add_modified(value, count);
065    }
066  }
067
068  @Override
069  public InvariantStatus check(@Interned Object val, int mod_index, int count) {
070    assert !falsified;
071    assert (mod_index >= 0) && (mod_index < 2);
072    assert Intern.isInterned(val);
073    long[] value = (long[]) val;
074    if (value == null) {
075      return InvariantStatus.NO_CHANGE;
076    } else if (mod_index == 0) {
077      return check_unmodified(value, count);
078    } else {
079      return check_modified(value, count);
080    }
081  }
082
083  /**
084   * Similar to {@link #check_modified} except that it can change the state of the invariant if
085   * necessary. If the invariant doesn't have any state, then the implementation should simply call
086   * {@link #check_modified}. This method need not check for falsification; that is done by the
087   * caller.
088   */
089  public abstract InvariantStatus add_modified(long @Interned [] value, int count);
090
091  /** By default, do nothing if the value hasn't been seen yet. Subclasses can override this. */
092  public InvariantStatus add_unmodified(long @Interned [] value, int count) {
093    return InvariantStatus.NO_CHANGE;
094  }
095
096  /**
097   * Presents a sample to the invariant. Returns whether the sample is consistent with the
098   * invariant. Does not change the state of the invariant.
099   *
100   * @param count how many identical samples were observed in a row. For example, three calls to
101   *     check_modified with a count parameter of 1 is equivalent to one call to check_modified with
102   *     a count parameter of 3.
103   * @return whether or not the sample is consistent with the invariant
104   */
105  public abstract InvariantStatus check_modified(long @Interned [] value, int count);
106
107  public InvariantStatus check_unmodified(long @Interned [] value, int count) {
108    return InvariantStatus.NO_CHANGE;
109  }
110}