001 // ***** This file is automatically generated from Member.java.jpp
002
003 package daikon.inv.binary.sequenceScalar;
004
005 import daikon.*;
006 import daikon.inv.*;
007 import daikon.inv.binary.twoSequence.*;
008 import daikon.derive.unary.*;
009 import daikon.derive.binary.*;
010 import daikon.derive.ternary.*;
011 import plume.*;
012 import java.util.logging.Logger;
013 import java.util.logging.Level;
014
015 /**
016 * Represents long scalars that are always members of a sequence of long
017 * values.
018 * Prints as <samp>x in y[]</samp> where <samp>x</samp> is a long scalar
019 * and <samp>y[]</samp> is a sequence of long.
020 **/
021 public final class Member
022 extends SequenceScalar
023 {
024 // We are Serializable, so we specify a version to allow changes to
025 // method signatures without breaking serialization. If you add or
026 // remove fields, you should change this number to the current date.
027 static final long serialVersionUID = 20031024L;
028
029 public static final Logger debug =
030 Logger.getLogger ("daikon.inv.binary.Member");
031
032 // Variables starting with dkconfig_ should only be set via the
033 // daikon.config.Configuration interface.
034 /**
035 * Boolean. True iff Member invariants should be considered.
036 **/
037 public static boolean dkconfig_enabled = true;
038
039 protected Member(PptSlice ppt) {
040 super(ppt);
041 }
042
043 protected /*@Prototype*/ Member() {
044 super();
045 }
046
047 private static /*@Prototype*/ Member proto;
048
049 /** Returns the prototype invariant for Member **/
050 public static /*@Prototype*/ Member get_proto() {
051 if (proto == null)
052 proto = new /*@Prototype*/ Member ();
053 return (proto);
054 }
055
056 /** Returns whether or not this invariant is enabled **/
057 public boolean enabled() {
058 return dkconfig_enabled;
059 }
060
061 /** instantiates the invariant on the specified slice **/
062 protected Member instantiate_dyn (/*@Prototype*/ PptSlice slice) {
063 return new Member (slice);
064 }
065
066 public /*@Nullable*/ DiscardInfo isObviousStatically(VarInfo[] vis) {
067 if (isObviousMember(sclvar(vis), seqvar(vis))) {
068 log ("scalar is obvious member of");
069 return new DiscardInfo(this, DiscardCode.obvious, sclvar().name()
070 + " is an obvious member of " + seqvar().name());
071 }
072 return super.isObviousStatically (vis);
073 }
074
075 /**
076 * Check whether sclvar is a member of seqvar can be determined
077 * statically.
078 **/
079 public static boolean isObviousMember(VarInfo sclvar, VarInfo seqvar) {
080
081 VarInfo sclvar_seq = sclvar.isDerivedSequenceMember();
082
083 if (sclvar_seq == null) {
084 // The scalar is not obviously (lexically) a member of any array.
085 return false;
086 }
087 // isObviousImplied: a[i] in a; max(a) in a
088 if (sclvar_seq == seqvar) {
089 // The scalar is a member of the same array.
090 return true;
091 }
092 // The scalar is a member of a different array than the sequence.
093 // But maybe the relationship is still obvious, so keep checking.
094
095 // isObviousImplied: when b==a[0..i]: b[j] in a; max(b) in a
096 // If the scalar is a member of a subsequence of the sequence, then
097 // the scalar is a member of the full sequence.
098 // This is satisfied, for instance, when determining that
099 // max(B[0..I]) is an obvious member of B.
100 VarInfo sclseqsuper = sclvar_seq.isDerivedSubSequenceOf();
101 if (sclseqsuper == seqvar)
102 return true;
103
104 // We know the scalar was derived from some array, but not from the
105 // sequence variable. If also not from what the sequence variable was
106 // derived from, we don't know anything about membership.
107 // Check:
108 // * whether comparing B[I] to B[0..J]
109 // * whether comparing min(B[0..I]) to B[0..J]
110 VarInfo seqvar_super = seqvar.isDerivedSubSequenceOf();
111 if ((seqvar_super != sclvar_seq)
112 && (seqvar_super != sclseqsuper)) {
113 return false;
114 }
115
116 // If the scalar is a positional element of the sequence from which
117 // the sequence at hand was derived, then any relationship will be
118 // (mostly) obvious by comparing the length of the sequence to the
119 // index. By contrast, if the scalar is max(...) or min(...), all bets
120 // are off.
121 if (seqvar.derived instanceof SequenceScalarSubsequence ||
122 seqvar.derived instanceof SequenceScalarArbitrarySubsequence) {
123
124 // Determine the left index/shift and right index/shift of the
125 // subsequence. If the left VarInfo is null, the sequence starts
126 // at the beginning. If the right VarInfo is null, the sequence stops
127 // at the end.
128 VarInfo seq_left_index = null, seq_right_index = null;
129 int seq_left_shift = 0, seq_right_shift = 0;
130 if (seqvar.derived instanceof SequenceScalarSubsequence) {
131 // the sequence is B[0..J-1] or similar. Get information about it.
132 SequenceScalarSubsequence seqsss
133 = (SequenceScalarSubsequence)seqvar.derived;
134 if (seqsss.from_start) {
135 seq_right_index = seqsss.sclvar();
136 seq_right_shift = seqsss.index_shift;
137 } else {
138 seq_left_index = seqsss.sclvar();
139 seq_left_shift = seqsss.index_shift;
140 }
141 } else if (seqvar.derived instanceof SequenceScalarArbitrarySubsequence) {
142 // the sequence is B[I+1..J] or similar
143 SequenceScalarArbitrarySubsequence ssass = (SequenceScalarArbitrarySubsequence)seqvar.derived;
144 seq_left_index = ssass.startvar();
145 seq_left_shift = (ssass.left_closed ? 0 : 1);
146 seq_right_index = ssass.endvar();
147 seq_right_shift = (ssass.right_closed ? 0 : -1);
148 } else {
149 throw new Error();
150 }
151
152 // if the scalar is a a subscript (b[i])
153 if (sclvar.derived instanceof SequenceScalarSubscript) {
154
155 SequenceScalarSubscript sclsss = (SequenceScalarSubscript) sclvar.derived;
156 VarInfo scl_index = sclsss.sclvar(); // "I" in "B[I]"
157 int scl_shift = sclsss.index_shift;
158
159 // determine if the scalar index is statically included in the
160 // left/right sequence
161 boolean left_included = false, right_included = false;
162 if (seq_left_index == null)
163 left_included = true;
164 if (seq_left_index == scl_index) {
165 if (seq_left_shift <= scl_shift) left_included = true;
166 }
167 if (seq_right_index == null)
168 right_included = true;
169 if (seq_right_index == scl_index) {
170 if (seq_right_shift >= scl_shift) right_included = true;
171 }
172 if (left_included && right_included)
173 return true;
174
175 // else if the scalar is a specific positional element (eg, b[0])
176 } else if (sclvar.derived instanceof SequenceInitial) {
177
178 // isObviousImplied: B[0] in B[0..J]; also B[-1] in B[J..]
179 SequenceInitial sclse = (SequenceInitial) sclvar.derived;
180 int scl_index = sclse.index;
181 if (((scl_index == 0) && seq_left_index == null)
182 || ((scl_index == -1) && seq_right_index == null))
183 // It might not be true, because the array could be empty;
184 // but if the array isn't empty, then it's obvious. The empty
185 // array case is ok, because the variable itself would be
186 // destroyed in that case.
187 return true;
188
189 // else if the scalar is min or max of a sequence
190 } else if ((sclvar.derived instanceof SequenceMin)
191 || (sclvar.derived instanceof SequenceMax)) {
192 Pair<DiscardCode,String> di = SubSequence.isObviousSubSequence(sclvar_seq, seqvar);
193 return (di != null);
194 }
195 }
196
197 return false;
198 }
199
200 public String repr() {
201 return "Member" + varNames() + ": "
202 + "falsified=" + falsified;
203 }
204
205 public String format_using(OutputFormat format) {
206
207 if (format.isJavaFamily()) return format_java_family(format);
208
209 if (format == OutputFormat.DAIKON) {
210 return format_daikon();
211 } else if (format == OutputFormat.SIMPLIFY) {
212 return format_simplify();
213 } else if (format == OutputFormat.ESCJAVA) {
214 return format_esc();
215 } else {
216 return format_unimplemented(format);
217 }
218 }
219
220 public String format_daikon() {
221 String sclname = sclvar().name();
222 String seqname = seqvar().name();
223 return sclname + " in " + seqname;
224 }
225
226 public String format_java() {
227 return "( (daikon.inv.FormatJavaHelper.memberOf("
228 + sclvar().name()
229 + " , " + seqvar().name() + " ) == true ) ";
230 }
231
232 public String format_java_family(OutputFormat format) {
233 String sclname = sclvar().name_using(format);
234 String seqname = seqvar().name_using(format);
235 return "daikon.Quant.memberOf(" + sclname
236 + " , " + seqname + " )";
237 }
238
239 public String format_esc() {
240 // "exists x in a..b : P(x)" gets written as "!(forall x in a..b : !P(x))"
241 String[] form = VarInfo.esc_quantify (seqvar(), sclvar());
242 return "!" + form[0] + "(" + form[1] + " != " + form[2] + ")" + form[3];
243 }
244
245 public String format_simplify() {
246 if (Invariant.dkconfig_simplify_define_predicates) {
247 String[] seq_name = seqvar().simplifyNameAndBounds();
248 String scalar_name = sclvar().simplify_name();
249 if (seq_name == null) {
250 return "format_simplify can't handle this sequence: "
251 + format();
252 }
253 return "(member " + scalar_name + " " +
254 seq_name[0] + " " + seq_name[1] + " " + seq_name[2] + ")";
255 } else {
256 // "exists x in a..b : P(x)" gets written as
257 // "!(forall x in a..b : !P(x))"
258 String[] form = VarInfo.simplify_quantify (seqvar(), sclvar());
259 return "(NOT " + form[0] + "(NEQ " + form[1] + " " + form[2] + ")"
260 + form[3] + ")";
261 }
262 }
263
264 public InvariantStatus check_modified(long[] a, long i, int count) {
265 if (a == null) {
266 return InvariantStatus.FALSIFIED;
267 } else if (ArraysMDE.indexOf(a, i) == -1) {
268 return InvariantStatus.FALSIFIED;
269 }
270 return InvariantStatus.NO_CHANGE;
271 }
272
273 public InvariantStatus add_modified(long[] a, long i, int count) {
274
275 InvariantStatus is = check_modified(a, i, count);
276 if (debug.isLoggable(Level.FINE) && (is == InvariantStatus.FALSIFIED))
277 debug.fine ("Member destroyed: " + format() + " because " + i +
278 " not in " + ArraysMDE.toString(a));
279 return (is);
280 }
281
282 protected double computeConfidence() {
283 return Invariant.CONFIDENCE_JUSTIFIED;
284 }
285
286 public boolean isSameFormula(Invariant other) {
287 assert other instanceof Member;
288 return true;
289 }
290
291 /**
292 * Checks to see if this is obvious over the specified variables.
293 * Implements the following checks: <pre>
294 *
295 * (0 <= i <= j) ^ (A[] == B[]) ==> A[i] in B[0..j]
296 * (0 <= i <= j) ^ (A[] == B[]) ==> A[j] in B[i..]
297 * (A subset B) ==> A[i] in B
298 * </pre>
299 */
300 public /*@Nullable*/ DiscardInfo isObviousDynamically (VarInfo[] vis) {
301
302 if (Debug.logOn())
303 Debug.log (getClass(), ppt.parent, vis, "is obvious check" + format());
304
305 DiscardInfo super_result = super.isObviousDynamically(vis);
306 if (super_result != null) {
307 return super_result;
308 }
309
310 // Check for subscript in subsequence
311 DiscardInfo di = subscript_in_subsequence (vis);
312 if (di != null)
313 return (di);
314
315 // Check for (A subset B) ==> (A[i] member B)
316 di = subset_in_subsequence (vis);
317 if (di != null)
318 return (di);
319
320 return (null);
321 }
322
323 /*
324 * Checks to see if this is obvious over the specified variables.
325 * Implements the following check: <pre>
326 *
327 * (A subset B) ==> (A[i] member B)
328 * </pre>
329 */
330 private /*@Nullable*/ DiscardInfo subset_in_subsequence (VarInfo[] vis) {
331
332 VarInfo scl_var = sclvar (vis);
333 VarInfo seq_var = seqvar (vis);
334
335 if (Debug.logOn())
336 Debug.log (getClass(), ppt.parent, vis, "looking for subset in subseq");
337
338 // If the scalar is not a subscript of a seq there is nothing to check.
339 if (scl_var.derived == null)
340 return null;
341 if (!(scl_var.derived instanceof SequenceScalarSubscript))
342 return null;
343 SequenceScalarSubscript sssc = (SequenceScalarSubscript) scl_var.derived;
344 if (Debug.logOn())
345 Debug.log (getClass(), ppt.parent, vis, "Looking for "
346 + sssc.seqvar().name() + " subset of "
347 + seq_var.name());
348
349 // check to see if subscripts sequence is a subset of the sequence var
350 if (ppt.parent.is_subset (sssc.seqvar(), seq_var)) {
351 return new DiscardInfo(this, DiscardCode.obvious,
352 "(" + sssc.seqvar().name() + " subset "
353 + seq_var.name() + ") ==> "
354 + sssc.seqvar().name() + "["
355 + sssc.sclvar().name()
356 + "] member " + seq_var.name());
357 }
358
359 return (null);
360 }
361
362 /*
363 * Checks to see if this is obvious over the specified variables.
364 * Implements the following checks: <pre>
365 *
366 * (0 <= i <= j) ^ (a[] == b[]) ==> a[i] in b[0..j]
367 * (0 <= i <= j) ^ (a[] == b[]) ==> a[j] in b[i..]
368 * </pre>
369 */
370 private /*@Nullable*/ DiscardInfo subscript_in_subsequence (VarInfo[] vis) {
371
372 VarInfo scl_var = sclvar (vis);
373 VarInfo seq_var = seqvar (vis);
374
375 // Both variables must be derived
376 if ((scl_var.derived == null) || (seq_var.derived == null))
377 return (null);
378
379 // If the scalar is not SequenceScalarSubscript, there is nothing to check.
380 if (!(scl_var.derived instanceof SequenceScalarSubscript))
381 return null;
382 SequenceScalarSubscript sssc = (SequenceScalarSubscript) scl_var.derived;
383
384 // If the sequence is not SequenceScalarSubsequence, nothing to check
385 if (!(seq_var.derived instanceof SequenceScalarSubsequence))
386 return (null);
387 SequenceScalarSubsequence ssss = (SequenceScalarSubsequence) seq_var.derived;
388
389 // Both variables must be derived from equal sequences
390 if (!ppt.parent.is_equal (sssc.seqvar(), ssss.seqvar()))
391 return (null);
392
393 // if a[i] in a[0..n], look for i <= n
394 if (ssss.from_start) {
395 if (Debug.logOn())
396 Debug.log (getClass(), ppt.parent, vis,
397 "Looking for " + sssc.sclvar().name() + sssc.index_shift
398 + " <= " + ssss.sclvar().name() + ssss.index_shift);
399 if (ppt.parent.is_less_equal (sssc.sclvar(), sssc.index_shift,
400 ssss.sclvar(), ssss.index_shift))
401 return new DiscardInfo(this, DiscardCode.obvious,
402 "i <= n ==> a[i] in a[..n] for "
403 + scl_var.name() + " and " + seq_var.name());
404 } else { // a[i] in a[n..], look for i >= n
405 if (Debug.logOn())
406 Debug.log (getClass(), ppt.parent, vis,
407 "Looking for " + ssss.sclvar().name() + ssss.index_shift
408 + " <= " + sssc.sclvar().name() + sssc.index_shift);
409 if (ppt.parent.is_less_equal (ssss.sclvar(), ssss.index_shift,
410 sssc.sclvar(), sssc.index_shift))
411 return new DiscardInfo(this, DiscardCode.obvious,
412 "i >= n ==> a[i] in a[n..] for "
413 + scl_var.name() + " and " + seq_var.name());
414 }
415 return (null);
416 }
417
418 }