001package daikon.inv.unary.string;
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 String}. */
013public abstract class SingleString extends UnaryInvariant {
014  static final long serialVersionUID = 20020122L;
015
016  protected SingleString(PptSlice ppt) {
017    super(ppt);
018  }
019
020  protected @Prototype SingleString() {
021    super();
022  }
023
024  @Override
025  public final boolean valid_types(VarInfo[] vis) {
026    return (vis.length == 1) && vis[0].file_rep_type.isString();
027  }
028
029  public VarInfo var(@GuardSatisfied @UnknownInitialization(SingleString.class) SingleString 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(String,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    String value = (String) val;
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    String value = (String) val;
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(@Interned String 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(@Interned String value, int count) {
070    return InvariantStatus.NO_CHANGE;
071  }
072
073  /**
074   * Presents a sample to the invariant. Returns whether the sample is consistent with the
075   * invariant. Does not change the state of the invariant.
076   *
077   * @param count how many identical samples were observed in a row. For example, three calls to
078   *     check_modified with a count parameter of 1 is equivalent to one call to check_modified with
079   *     a count parameter of 3.
080   * @return whether or not the sample is consistent with the invariant
081   */
082  public abstract InvariantStatus check_modified(@Interned String value, int count);
083
084  public InvariantStatus check_unmodified(@Interned String value, int count) {
085    return InvariantStatus.NO_CHANGE;
086  }
087}