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