001// ***** This file is automatically generated from BinaryInvariant.java.jpp 002 003package daikon.inv.binary.twoScalar; 004 005import daikon.*; 006import daikon.inv.*; 007import daikon.inv.InvariantStatus; 008import daikon.inv.binary.*; 009import org.checkerframework.checker.interning.qual.Interned; 010import org.checkerframework.checker.lock.qual.GuardSatisfied; 011import org.checkerframework.dataflow.qual.Pure; 012import org.plumelib.util.ArraysPlume; 013import org.plumelib.util.Intern; 014import typequals.prototype.qual.NonPrototype; 015import typequals.prototype.qual.Prototype; 016 017/** 018 * Base class for invariants over two variables of type double. 019 * An example is {@code y = abs(x)}. 020 * 021 * <p>Provides a simpler mechanism for non-symmetric invariants to function over both permutations 022 * of their variables. 023 * 024 * <p>Non-symmetric invariants must instantiate two objects (one for each argument order). This is 025 * tracked by the variable swap. They must always access their variables via the methods var1() and 026 * var2() which return the correct variable (based on the swap setting). No other work is necessary, 027 * all permuations and resurrection is handled here. 028 * 029 * <p>Symmetric invariants should define symmetric() to return true or override 030 * resurrect_done_swapped to do nothing. Non-symmetric invariants that use converse operations (eg, 031 * less than and greater than) rather than argument swapping should override resurrect_done_swapped 032 * to return the correct class. 033 */ 034public abstract class TwoFloat extends BinaryInvariant { 035 static final long serialVersionUID = 20040113L; 036 037 // if true, swap the order of the invariant variables 038 protected boolean swap = false; 039 040 protected TwoFloat(PptSlice ppt) { 041 super(ppt); 042 } 043 044 protected @Prototype TwoFloat() { 045 super(); 046 } 047 048 @Override 049 final public boolean valid_types(VarInfo[] vis) { 050 051 if (vis.length != 2) { 052 return false; 053 } 054 055 boolean dim_ok = !vis[0].file_rep_type.isArray() && !vis[1].file_rep_type.isArray(); 056 057 return dim_ok && vis[0].file_rep_type.baseIsFloat() && vis[1].file_rep_type.baseIsFloat(); 058 } 059 060 /** Returns whether or not the variable order is currently swapped for this invariant. */ 061 @Override 062 public boolean get_swap() { 063 return swap; 064 } 065 066 /** Checks to see if the variable order was swapped and calls the correct routine to handle it. */ 067 @Override 068 protected Invariant resurrect_done(int[] permutation) { 069 assert permutation.length == 2; 070 // assert ArraysPlume.fnIsPermutation(permutation); 071 if (permutation[0] == 1) { 072 return resurrect_done_swapped(); 073 } else { 074 return resurrect_done_unswapped(); 075 } 076 } 077 078 /** Swaps the variables by inverting the state of swap. */ 079 protected Invariant resurrect_done_swapped() { 080 if (!is_symmetric()) { 081 swap = !swap; 082 } 083 return this; 084 } 085 086 /** Subclasses can override in the rare cases they need to fix things even when not swapped. */ 087 protected Invariant resurrect_done_unswapped() { 088 // do nothing 089 return this; 090 } 091 092 /** 093 * Returns the first variable. This is the only mechanism by which subclasses should access 094 * variables. 095 */ 096 public VarInfo var1(@GuardSatisfied TwoFloat this) { 097 if (swap) { 098 return ppt.var_infos[1]; 099 } else { 100 return ppt.var_infos[0]; 101 } 102 } 103 104 /** 105 * Returns the first variable. This is the only mechanism by which subclasses should access 106 * variables. 107 */ 108 public VarInfo var2(@GuardSatisfied TwoFloat this) { 109 if (swap) { 110 return ppt.var_infos[0]; 111 } else { 112 return ppt.var_infos[1]; 113 } 114 } 115 116 /** 117 * Returns the first variable from the specified vis. This is the only mechanism by which 118 * subclasses should access variables. 119 */ 120 public VarInfo var1(VarInfo[] vis) { 121 if (swap) { 122 return vis[1]; 123 } else { 124 return vis[0]; 125 } 126 } 127 128 /** 129 * Returns the first variable in the specified vis. This is the only mechanism by which subclasses 130 * should access variables. 131 */ 132 public VarInfo var2(VarInfo[] vis) { 133 if (swap) { 134 return vis[0]; 135 } else { 136 return vis[1]; 137 } 138 } 139 140 @Override 141 public InvariantStatus check( 142 @Interned Object val1, @Interned Object val2, int mod_index, int count) { 143 // Tests for whether a value is missing should be performed before 144 // making this call, so as to reduce overall work. 145 assert ! falsified; 146 assert (mod_index >= 0) && (mod_index < 4); 147 double v1 = ((Double) val1).doubleValue(); 148 double v2 = ((Double) val2).doubleValue(); 149 if (mod_index == 0) { 150 if (swap) { 151 return check_unmodified(v2, v1, count); 152 } else { 153 return check_unmodified(v1, v2, count); 154 } 155 } else { 156 if (swap) { 157 return check_modified(v2, v1, count); 158 } else { 159 return check_modified(v1, v2, count); 160 } 161 } 162 } 163 164 @Override 165 public InvariantStatus add( 166 @Interned Object val1, @Interned Object val2, int mod_index, int count) { 167 // Tests for whether a value is missing should be performed before 168 // making this call, so as to reduce overall work. 169 assert ! falsified; 170 assert (mod_index >= 0) && (mod_index < 4); 171 double v1 = ((Double) val1).doubleValue(); 172 double v2 = ((Double) val2).doubleValue(); 173 if (mod_index == 0) { 174 if (swap) { 175 return add_unmodified(v2, v1, count); 176 } else { 177 return add_unmodified(v1, v2, count); 178 } 179 } else { 180 if (swap) { 181 return add_modified(v2, v1, count); 182 } else { 183 return add_modified(v1, v2, count); 184 } 185 } 186 } 187 188 /** 189 * Presents a sample to the invariant. Returns whether the sample is consistent with the 190 * invariant. Does not change the state of the invariant. 191 * 192 * @param count how many identical samples were observed in a row. For example, three calls to 193 * check_modified with a count parameter of 1 is equivalent to one call to check_modified with 194 * a count parameter of 3. 195 * @return whether or not the sample is consistent with the invariant 196 */ 197 public abstract InvariantStatus check_modified(double v1, double v2, int count); 198 199 public InvariantStatus check_unmodified(double v1, double v2, int count) { 200 return InvariantStatus.NO_CHANGE; 201 } 202 203 /** Default implementation simply calls check. Subclasses can override. */ 204 public InvariantStatus add_modified(double v1, double v2, int count) { 205 return check_modified(v1, v2, count); 206 } 207 208 /** By default, do nothing if the value hasn't been seen yet. Subclasses can override this. */ 209 public InvariantStatus add_unmodified(double v1, double v2, int count) { 210 return InvariantStatus.NO_CHANGE; 211 } 212 213 /** Returns a representation of the class. This includes the classname, variables, and swap state. */ 214 @Override 215 public String repr(@GuardSatisfied TwoFloat this) { 216 return getClass().getName() + " (" + var1().name() + ", " 217 + var2().name() + ") [swap=" + swap + "]"; 218 } 219 220 /** 221 * Return true if both invariants are the same class and the order of the variables (swap) is the 222 * same. 223 */ 224 @Pure 225 @Override 226 public boolean isSameFormula(Invariant other) { 227 TwoFloat inv = (TwoFloat) other; 228 return (this.getClass() == inv.getClass()) && (this.swap == inv.swap); 229 } 230 231 @Override 232 protected double computeConfidence() { 233 return Invariant.conf_is_ge(ppt.num_values(), 5); 234 } 235}