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}