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}