001 // ***** This file is automatically generated from PairwiseIntComparison.java.jpp
002
003 package daikon.inv.binary.twoSequence;
004
005 import daikon.*;
006 import daikon.inv.*;
007 import daikon.inv.binary.twoScalar.*;
008 import daikon.derive.binary.*;
009 import daikon.suppress.*;
010 import daikon.Quantify.QuantFlags;
011
012 import plume.ArraysMDE;
013 import java.util.Iterator;
014 import java.util.logging.Logger;
015 import java.util.logging.Level;
016
017 /**
018 * Represents an invariant between corresponding elements of two
019 * sequences of long values. The length of the sequences must match for
020 * the invariant to hold. A comparison is made over each
021 * <samp>(x[i], y[i])</samp> pair.
022 * Thus, <samp>x[0]</samp> is compared to <samp>y[0]</samp>,
023 * <samp>x[1]</samp> to <samp>y[1]</samp>, and so forth.
024 * Prints as <samp>x[] <= y[]</samp>.
025 **/
026
027 public class PairwiseIntLessEqual
028 extends TwoSequence
029 {
030 // We are Serializable, so we specify a version to allow changes to
031 // method signatures without breaking serialization. If you add or
032 // remove fields, you should change this number to the current date.
033 static final long serialVersionUID = 20030822L;
034
035 /** Debug tracer. **/
036 public static final Logger debug =
037 Logger.getLogger("daikon.inv.binary.twoSequence.PairwiseIntLessEqual");
038
039 // Variables starting with dkconfig_ should only be set via the
040 // daikon.config.Configuration interface.
041 /**
042 * Boolean. True iff PairwiseIntComparison invariants should be considered.
043 **/
044 public static boolean dkconfig_enabled = true;
045
046 static final boolean debugPairwiseIntComparison = false;
047
048 protected PairwiseIntLessEqual(PptSlice ppt) {
049 super(ppt);
050 }
051
052 protected /*@Prototype*/ PairwiseIntLessEqual() {
053 super();
054 }
055
056 private static /*@Prototype*/ PairwiseIntLessEqual proto;
057
058 /** Returns the prototype invariant for PairwiseIntLessEqual **/
059 public static /*@Prototype*/ PairwiseIntLessEqual get_proto() {
060 if (proto == null)
061 proto = new /*@Prototype*/ PairwiseIntLessEqual ();
062 return (proto);
063 }
064
065 /** Returns whether or not this invariant is enabled **/
066 public boolean enabled() {
067 return dkconfig_enabled;
068 }
069
070 /** PairwiseIntLessEqual is only valid on integral types **/
071 public boolean instantiate_ok (VarInfo[] vis) {
072
073 if (!valid_types (vis))
074 return (false);
075
076 if (!(vis[0].type.elementIsIntegral() && vis[1].type.elementIsIntegral()))
077 return false;
078
079 return (true);
080 }
081
082 /** instantiates the invariant on the specified slice **/
083 protected PairwiseIntLessEqual instantiate_dyn (PptSlice slice) /*@Prototype*/ {
084 PairwiseIntLessEqual inv = new PairwiseIntLessEqual(slice);
085 if (logOn())
086 inv.log ("instantiate");
087 return inv;
088 }
089
090 protected PairwiseIntLessEqual(PairwiseIntGreaterEqual swapped_pic) {
091 super(swapped_pic.ppt);
092 if (logOn())
093 log ("Instantiated from resurrect_done_swapped");
094 }
095
096 public /*@Nullable*/ DiscardInfo isObviousStatically (VarInfo[] vis) {
097 VarInfo var1 = vis[0];
098 VarInfo var2 = vis[1];
099
100 DiscardInfo di = null;
101 di = SubSequence.isObviousSubSequence(this, var1, var2);
102 if (di == null) {
103 di = SubSequence.isObviousSubSequence(this, var2, var1);
104 }
105 if (di != null) {
106 Global.implied_noninstantiated_invariants++;
107 return di;
108 }
109
110 // Don't instantiate if the variables can't have order
111 if (!var1.aux.getFlag(VarInfoAux.HAS_ORDER) ||
112 !var2.aux.getFlag(VarInfoAux.HAS_ORDER)) {
113 if (debug.isLoggable(Level.FINE)) {
114 debug.fine ("Not instantitating for because order has no meaning: " +
115 var1.name() + " and " + var2.name());
116 }
117 return new DiscardInfo(this, DiscardCode.obvious, "Obvious statically since order has no meaning");
118 }
119
120 return super.isObviousStatically (vis);
121 }
122
123 public /*@Nullable*/ DiscardInfo isObviousDynamically (VarInfo[] vis) {
124 DiscardInfo super_result = super.isObviousDynamically(vis);
125 if (super_result != null) {
126 return super_result;
127 }
128
129 // Subsequence invariants are implied by the same invariant over
130 // the supersequence
131 DiscardInfo di = superseq_implies (vis);
132 if (di != null)
133 return (di);
134
135 return null;
136 }
137
138 /**
139 * Checks to see if the same invariant exists over supersequences of
140 * these variables:
141 *
142 * (A[] op B[]) ^ (i == j) ==> A[i..] op B[j..]
143 * (A[] op B[]) ^ (i == j) ==> A[..i] op B[..j]
144 */
145 private /*@Nullable*/ DiscardInfo superseq_implies (VarInfo[] vis) {
146
147 // Make sure the variables are SequenceScalarSubsequence with the same start/end
148 VarInfo v1 = vis[0];
149 VarInfo v2 = vis[1];
150 if (!v1.isDerived() || !(v1.derived instanceof SequenceScalarSubsequence))
151 return (null);
152 if (!v2.isDerived() || !(v2.derived instanceof SequenceScalarSubsequence))
153 return (null);
154 SequenceScalarSubsequence der1 = (SequenceScalarSubsequence) v1.derived;
155 SequenceScalarSubsequence der2 = (SequenceScalarSubsequence) v2.derived;
156 if ((der1.from_start != der2.from_start)
157 || (der1.index_shift != der2.index_shift))
158 return (null);
159
160 // Make sure the subscripts are equal
161 DiscardInfo di = new DiscardInfo (this, DiscardCode.obvious, "");
162 if (!ppt.parent.check_implied_canonical (di, der1.sclvar(), der2.sclvar(),
163 IntEqual.get_proto()))
164 return (null);
165
166 // See if the super-sequences have the same invariant
167 if (!ppt.parent.check_implied_canonical (di, der1.seqvar(), der2.seqvar(),
168 PairwiseIntLessEqual.get_proto()))
169 return (null);
170
171 // Add in the vis variables to di reason (if they are different)
172 di.add_implied_vis (vis);
173 return (di);
174 }
175
176 protected Invariant resurrect_done_swapped() {
177
178 return new PairwiseIntGreaterEqual(this);
179 }
180
181 /**
182 * Returns the class that corresponds to this class with its variable
183 * order swapped.
184 */
185 public static Class<PairwiseIntGreaterEqual> swap_class () {
186 return PairwiseIntGreaterEqual.class;
187 }
188
189 public String repr() {
190 return "PairwiseIntLessEqual" + varNames() + ": ";
191 }
192
193 public String getComparator() {
194 return "<=";
195 }
196
197 public String format_using(OutputFormat format) {
198
199 if (format.isJavaFamily()) return format_java_family(format);
200
201 if (format == OutputFormat.DAIKON) return format_daikon();
202 if (format == OutputFormat.ESCJAVA) return format_esc();
203 if (format == OutputFormat.SIMPLIFY) return format_simplify();
204
205 return format_unimplemented(format);
206 }
207
208 public String format_daikon() {
209 return var1().name() + " <= " + var2().name()
210 + " (elementwise)";
211 }
212
213 public String format_esc() {
214 String[] form = VarInfo.esc_quantify (var1(), var2());
215 return form[0] + "(" + form[1] + " <= " + form[2] + ")" + form[3];
216 }
217
218 public String format_simplify() {
219 String[] form = VarInfo.simplify_quantify (QuantFlags.element_wise(),
220 var1(), var2());
221 return form[0] + "(<= " + form[1] + " " + form[2] + ")" + form[3];
222 }
223
224 public String format_java_family(OutputFormat format) {
225 return "daikon.Quant.pairwiseLTE(" + var1().name_using(format)
226 + ", " + var2().name_using(format) + ")";
227 }
228
229 public InvariantStatus check_modified(long[] a1, long[] a2, int count) {
230 assert a1 != null && a2 != null
231 : var1() + " " + var2() + " " + FileIO.get_linenum();
232 if (a1.length != a2.length || a1.length == 0 || a2.length == 0) {
233 // destroyAndFlow();
234 return InvariantStatus.FALSIFIED;
235 }
236
237 int len = a1.length;
238 // int len = Math.min(a1.length, a2.length);
239
240 for (int i=0; i<len; i++) {
241 long v1 = a1[i];
242 long v2 = a2[i];
243 if (! (v1 <= v2) ) {
244 // destroyAndFlow();
245 return InvariantStatus.FALSIFIED;
246 }
247 }
248 return InvariantStatus.NO_CHANGE;
249 }
250
251 public InvariantStatus add_modified(long[] a1, long[] a2,
252 int count) {
253 if (logDetail())
254 log (debug, "saw add_modified (" + ArraysMDE.toString(a1) +
255 ", " + ArraysMDE.toString(a2) + ")");
256 return check_modified(a1, a2, count);
257 }
258
259 protected double computeConfidence() {
260 // num_elt_values() would be more appropriate
261 // int num_values = ((PptSlice2) ppt).num_elt_values();
262 int num_values = ppt.num_samples();
263 if (num_values == 0) {
264 return Invariant.CONFIDENCE_UNJUSTIFIED;
265 } else {
266
267 return 1 - Math.pow(.5, num_values);
268 }
269 }
270
271 public boolean isSameFormula(Invariant other) {
272 return true;
273 }
274
275 public boolean isExclusiveFormula(Invariant other) {
276 return false;
277 }
278
279 // Look up a previously instantiated invariant.
280 public static /*@Nullable*/ PairwiseIntLessEqual find(PptSlice ppt) {
281 assert ppt.arity() == 2;
282 for (Invariant inv : ppt.invs) {
283 if (inv instanceof PairwiseIntLessEqual)
284 return (PairwiseIntLessEqual) inv;
285 }
286 return null;
287 }
288
289 /**
290 * Returns a list of non-instantiating suppressions for this invariant.
291 */
292 public /*@Nullable*/ NISuppressionSet get_ni_suppressions() {
293 return (suppressions);
294 }
295
296 /** Definition of this invariant (the suppressee) **/
297 private static NISuppressee suppressee
298 = new NISuppressee (PairwiseIntLessEqual.class, 2);
299
300 // Suppressor definitions (used in suppressions below)
301 private static NISuppressor
302 v1_eq_v2 = new NISuppressor (0, 1, PairwiseIntEqual.class),
303 v1_gt_v2 = new NISuppressor (0, 1, PairwiseIntGreaterThan.class),
304 v1_lt_v2 = new NISuppressor (0, 1, PairwiseIntLessThan.class);
305
306 private static NISuppressionSet suppressions =
307 new NISuppressionSet (new NISuppression[] {
308
309 // v1 == v2 => v1 <= v2
310 new NISuppression (v1_eq_v2, suppressee),
311
312 // v1 < v2 => v1 <= v2
313 new NISuppression (v1_lt_v2, suppressee),
314
315 });
316
317 }