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