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