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