001package daikon.inv; 002 003import daikon.inv.filter.DerivedParameterFilter; 004import daikon.inv.filter.InvariantFilter; 005import daikon.inv.filter.ObviousFilter; 006import daikon.inv.filter.OnlyConstantVariablesFilter; 007import daikon.inv.filter.SimplifyFilter; 008import daikon.inv.filter.UnjustifiedFilter; 009import daikon.inv.filter.UnmodifiedVariableEqualityFilter; 010import daikon.inv.filter.VariableFilter; 011import java.io.ObjectStreamException; 012import java.io.Serializable; 013import org.checkerframework.checker.lock.qual.GuardSatisfied; 014import org.checkerframework.dataflow.qual.Pure; 015import org.checkerframework.dataflow.qual.SideEffectFree; 016 017/** 018 * DiscardCode is an enumeration type. It represents reasons why an invariant is falsified or 019 * disregarded. Methods that decide whether an Invariant should be printed later (such as 020 * isObviousImplied()), side effect Invariants to contain DiscardCode instances in their discardCode 021 * field slot. 022 * 023 * <p>The different elements of the enumeration are: 024 * 025 * <p>obvious // is implied by other already known invariants 026 * 027 * <p>bad_sample // is falsified by a seen example 028 * 029 * <p>bad_confidence // has an unjustified confidence 030 * 031 * <p>(unused) // was few_modified_samples 032 * 033 * <p>not_enough_samples // not enough samples seen for the Invariant 034 * 035 * <p>non_canonical_var // expression involves a non-canonical variable 036 * 037 * <p>implied_post_condition // implied by some prestate conditions 038 * 039 * <p>only_constant_vars // expression for invariant only contains constant variables 040 * 041 * <p>derived_param // has a VarInfo that has derived and uninteresting param 042 * 043 * <p>unmodified_var // invariant discarded because it says some var hasn't been modified 044 * 045 * <p>control_check // if discarded due to the ControlledInvariantFilter 046 * 047 * <p>exact // isExact() fails 048 * 049 * <p>var_filtered // Doesn't contain a desirable variable 050 * 051 * <p>filtered // filtered by some other means not in the above list 052 * 053 * <p>There is no representation for an invariant that is *not* discarded; don't use a DiscardCode 054 * in that situation. 055 */ 056public class DiscardCode implements Comparable<DiscardCode>, Serializable { 057 058 // We are Serializable, so we specify a version to allow changes to 059 // method signatures without breaking serialization. If you add or 060 // remove fields, you should change this number to the current date. 061 static final long serialVersionUID = 20031016L; 062 063 /** used when an invariant is implied by other known invariants */ 064 public static final DiscardCode obvious = new DiscardCode(0); 065 066 /** used when an invariant is falsified by a seen example */ 067 public static final DiscardCode bad_sample = new DiscardCode(1); 068 069 /** used when an invariant has an unjustified confidence */ 070 public static final DiscardCode bad_confidence = new DiscardCode(2); 071 072 /** used when an invariant has not had enough samples */ 073 public static final DiscardCode not_enough_samples = new DiscardCode(4); 074 075 /** used when an invariant contains a non-canonical variable */ 076 public static final DiscardCode non_canonical_var = new DiscardCode(5); 077 078 /** used when an invariant is implied by some prestate conditions */ 079 public static final DiscardCode implied_post_condition = new DiscardCode(6); 080 081 /** used when an invariant's expression contains only constant variables */ 082 public static final DiscardCode only_constant_vars = new DiscardCode(7); 083 084 /** used when an invariant's VarInfo returns true for isDerivedParamAndUninteresting() */ 085 public static final DiscardCode derived_param = new DiscardCode(8); 086 087 /** used for invariants that describe unmodified variables */ 088 public static final DiscardCode unmodified_var = new DiscardCode(9); 089 090 /** used for invariants discarded because of the ControlledInvariantsFilter */ 091 public static final DiscardCode control_check = new DiscardCode(10); 092 093 /** used for invariants discarded when isExact() fails */ 094 public static final DiscardCode exact = new DiscardCode(11); 095 096 /** used for invariants that don't contain desired variables */ 097 public static final DiscardCode var_filtered = new DiscardCode(12); 098 099 /** used for invariants that are filtered by some means not in the above list */ 100 public static final DiscardCode filtered = new DiscardCode(13); 101 102 /** Each member of the enumeration is associated with a distinct int for comparability. */ 103 public final int enumValue; 104 105 // Prevents the user from using DiscardCode types not in the enumeration 106 // by making the default constructor private. This constructor should never be 107 // used to make new elements of the enumeration. 108 private DiscardCode() { 109 this.enumValue = -1; 110 } 111 112 // Makes it easier to add a new DiscardCode type by simply constructing it as a field with the 113 // next non-used integer value. 114 private DiscardCode(int enumValue) { 115 this.enumValue = enumValue; 116 } 117 118 /** 119 * The enumeration members in sorted order: <br> 120 * obvious, bad_sample, bad_confidence, [unused], not_enough_samples, non_canonical_var,<br> 121 * implied_post_condition, only_constant_vars, derived_param, unmodified_var, control_check, 122 * exact, var filter 123 * 124 * @return this.enumValue.compareTo(o.enumValue) where the enumValue are treated as Integers 125 * @throws ClassCastException iff !(o instanceof DiscardCode) 126 */ 127 @Pure 128 @Override 129 public int compareTo(@GuardSatisfied DiscardCode this, DiscardCode o) { 130 if (this.enumValue < o.enumValue) { 131 return -1; 132 } else if (this.enumValue == o.enumValue) { 133 return 0; 134 } else { 135 return 1; 136 } 137 } 138 139 /** Returns the DiscardCode most associated with the given filter. */ 140 public static DiscardCode findCode(InvariantFilter filter) { 141 if ((filter instanceof ObviousFilter) || (filter instanceof SimplifyFilter)) { 142 return obvious; 143 } else if (filter instanceof DerivedParameterFilter) { 144 return derived_param; 145 } else if (filter instanceof OnlyConstantVariablesFilter) { 146 return only_constant_vars; 147 } else if (filter instanceof UnjustifiedFilter) { 148 return bad_confidence; 149 } else if (filter instanceof UnmodifiedVariableEqualityFilter) { 150 return unmodified_var; 151 } else if (filter instanceof VariableFilter) { 152 return var_filtered; 153 } else { 154 return filtered; 155 } 156 } 157 158 /** 159 * Prints out a string describing the reason for discard. 160 * 161 * @return one of {"Not discarded", "Obvious, "Bad sample seen", "Unjustified confidence", "Few 162 * modified samples", "Not enough samples", "Non-canonical variable", "Implied post state", 163 * "Only constant variables in this expression", "Derived Param", "Control Check", "Exact", 164 * "Variable Filter", "Filtered"} 165 */ 166 @SideEffectFree 167 @Override 168 public String toString(@GuardSatisfied DiscardCode this) { 169 if (this.enumValue == -1) { 170 return "Not discarded"; 171 } else if (this.enumValue == 0) { 172 return "Obvious"; 173 } else if (this.enumValue == 1) { 174 return "Bad sample seen"; 175 } else if (this.enumValue == 2) { 176 return "Unjustified confidence"; 177 } else if (this.enumValue == 3) { 178 return "Few modified samples"; 179 } else if (this.enumValue == 4) { 180 return "Not enough samples"; 181 } else if (this.enumValue == 5) { 182 return "Non-canonical variable"; 183 } else if (this.enumValue == 6) { 184 return "Implied post state"; 185 } else if (this.enumValue == 7) { 186 return "Only constant variables in this expression"; 187 } else if (this.enumValue == 8) { 188 return "Derived Param"; 189 } else if (this.enumValue == 9) { 190 return "Unmodified var"; 191 } else if (this.enumValue == 10) { 192 return "Control Check"; 193 } else if (this.enumValue == 11) { 194 return "Exact"; 195 } else if (this.enumValue == 12) { 196 return "Variable Filter"; 197 } else if (this.enumValue == 13) { 198 return "Filtered"; 199 } else { // this should never happen since the constructor is private 200 return "Unknown instance of DiscardCode used"; 201 } 202 } 203 204 /** 205 * To prevent deserialization causing more DiscardCodes to be instantiated. 206 * 207 * @return one of the static DiscardCode instances 208 */ 209 public Object readResolve() throws ObjectStreamException { 210 if (enumValue == 0) { 211 return obvious; 212 } else if (enumValue == 1) { 213 return bad_sample; 214 } else if (enumValue == 2) { 215 return bad_confidence; 216 } else if (enumValue == 3) throw new Error("few_modified_samples no longer exists"); 217 else if (enumValue == 4) { 218 return not_enough_samples; 219 } else if (enumValue == 5) { 220 return non_canonical_var; 221 } else if (enumValue == 6) { 222 return implied_post_condition; 223 } else if (enumValue == 7) { 224 return only_constant_vars; 225 } else if (enumValue == 8) { 226 return derived_param; 227 } else if (enumValue == 9) { 228 return unmodified_var; 229 } else if (enumValue == 10) { 230 return control_check; 231 } else if (enumValue == 11) { 232 return exact; 233 } else if (enumValue == 12) { 234 return var_filtered; 235 } else if (enumValue == 13) { 236 return filtered; 237 } else { // this should never happen 238 // return null; 239 throw new Error("impossible"); 240 } 241 } 242}