001package daikon.inv.unary.scalar; 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 double}. */ 013public abstract class SingleFloat extends UnaryInvariant { 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 = 20020122L; 018 019 protected SingleFloat(PptSlice ppt) { 020 super(ppt); 021 } 022 023 protected @Prototype SingleFloat() { 024 super(); 025 } 026 027 /** Returns whether or not the specified types are valid for unary float. */ 028 @Override 029 public final boolean valid_types(VarInfo[] vis) { 030 return (vis.length == 1) && vis[0].file_rep_type.isFloat(); 031 } 032 033 public VarInfo var(@GuardSatisfied @UnknownInitialization(SingleFloat.class) SingleFloat this) { 034 return ppt.var_infos[0]; 035 } 036 037 // Should never be called with modified == ValueTuple.MISSING_NONSENSICAL. 038 // Subclasses need not override this except in special cases; 039 // just implement {@link add_modified(Object,int)}. 040 @Override 041 public InvariantStatus add(@Interned Object val, int mod_index, int count) { 042 assert !falsified; 043 assert (mod_index >= 0) && (mod_index < 2); 044 double value = ((Double) val).doubleValue(); 045 if (mod_index == 0) { 046 return add_unmodified(value, count); 047 } else { 048 return add_modified(value, count); 049 } 050 } 051 052 @Override 053 public InvariantStatus check(@Interned Object val, int mod_index, int count) { 054 assert !falsified; 055 assert (mod_index >= 0) && (mod_index < 2); 056 double value = ((Double) val).doubleValue(); 057 if (mod_index == 0) { 058 return check_unmodified(value, count); 059 } else { 060 return check_modified(value, count); 061 } 062 } 063 064 /** 065 * Similar to {@link #check_modified} except that it can change the state of the invariant if 066 * necessary. If the invariant doesn't have any state, then the implementation should simply call 067 * {@link #check_modified}. This method need not check for falsification; that is done by the 068 * caller. 069 */ 070 public abstract InvariantStatus add_modified(double value, int count); 071 072 /** By default, do nothing if the value hasn't been seen yet. Subclasses can override this. */ 073 public InvariantStatus add_unmodified(double value, int count) { 074 // System.out.println("SingleFloat.add_unmodified " + ppt.name() + ": parent=" + ppt.parent); 075 return InvariantStatus.NO_CHANGE; 076 } 077 078 /** 079 * Presents a sample to the invariant. Returns whether the sample is consistent with the 080 * invariant. Does not change the state of the invariant. 081 * 082 * @param count how many identical samples were observed in a row. For example, three calls to 083 * check_modified with a count parameter of 1 is equivalent to one call to check_modified with 084 * a count parameter of 3. 085 * @return whether or not the sample is consistent with the invariant 086 */ 087 public abstract InvariantStatus check_modified(double value, int count); 088 089 public InvariantStatus check_unmodified(double value, int count) { 090 return InvariantStatus.NO_CHANGE; 091 } 092 093 // This has no additional suppression factories beyond those of Invariant. 094}