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