001 // ***** This file is automatically generated from OneOf.java.jpp
002
003 package daikon.inv.unary.string;
004
005 import daikon.*;
006 import daikon.inv.*;
007
008 import utilMDE.*;
009
010 import java.io.*;
011 import java.util.logging.Logger;
012 import java.util.logging.Level;
013
014 import java.util.regex.*;
015
016 import java.util.*;
017
018 // This subsumes an "exact" invariant that says the value is always exactly
019 // a specific value. Do I want to make that a separate invariant
020 // nonetheless? Probably not, as this will simplify implication and such.
021
022 /**
023 * Represents String variables that take on only a few distinct
024 * values. Prints as either
025 * <samp>x == c</samp> (when there is only one value)
026 * or as <samp>x one of {c1, c2, c3}</samp> (when there are multiple values).
027 */
028
029 public final class OneOfString
030 extends SingleString
031 implements OneOf
032 {
033 // We are Serializable, so we specify a version to allow changes to
034 // method signatures without breaking serialization. If you add or
035 // remove fields, you should change this number to the current date.
036 static final long serialVersionUID = 20030822L;
037
038 /**
039 * Debugging logger.
040 **/
041 public static final Logger debug
042 = Logger.getLogger (OneOfString.class.getName());
043
044 // Variables starting with dkconfig_ should only be set via the
045 // daikon.config.Configuration interface.
046 /**
047 * Boolean. True iff OneOf invariants should be considered.
048 **/
049 public static boolean dkconfig_enabled = true;
050
051 /**
052 * Positive integer. Specifies the maximum set size for this type
053 * of invariant (x is one of <code>size</code> items).
054 **/
055
056 public static int dkconfig_size = 3;
057
058 // Probably needs to keep its own list of the values, and number of each seen.
059 // (That depends on the slice; maybe not until the slice is cleared out.
060 // But so few values is cheap, so this is quite fine for now and long-term.)
061
062 private /*(at)Interned*/ String[] elts;
063 private int num_elts;
064
065 public OneOfString (/*@Dependent(result=Nullable.class, when=Prototype.class)*/ PptSlice slice) {
066 super (slice);
067 if (slice == null)
068 return;
069
070 elts = new /*(at)Interned*/ String[dkconfig_size];
071
072 num_elts = 0;
073 }
074
075 private static /*@Prototype*/ OneOfString proto;
076
077 /** Returns the prototype invariant for OneOfString **/
078 public static /*@Prototype*/ OneOfString get_proto() {
079 if (proto == null)
080 proto = new /*@Prototype*/ OneOfString (null);
081 return (proto);
082 }
083
084 /** returns whether or not this invariant is enabled **/
085 public boolean enabled() {
086 return dkconfig_enabled;
087 }
088
089 /** instantiate an invariant on the specified slice **/
090 public OneOfString instantiate_dyn (PptSlice slice) /*@Prototype*/ {
091 return new OneOfString(slice);
092 }
093
094 public boolean is_boolean() {
095 return (var().file_rep_type.elementType() == ProglangType.BOOLEAN);
096 }
097 public boolean is_hashcode() {
098 return (var().file_rep_type.elementType() == ProglangType.HASHCODE);
099 }
100
101 public OneOfString clone() {
102 OneOfString result = (OneOfString) super.clone();
103 result.elts = elts.clone();
104
105 result.num_elts = this.num_elts;
106 return result;
107 }
108
109 public int num_elts() {
110 return num_elts;
111 }
112
113 public Object elt() {
114 return elt(0);
115 }
116
117 public Object elt(int index) {
118 if (num_elts <= index)
119 throw new Error("Represents " + num_elts + " elements, index " + index + " not valid");
120
121 return elts[index];
122 }
123
124 static Comparator<String> comparator = new UtilMDE.NullableStringComparator();
125
126 private void sort_rep() {
127 Arrays.sort(elts, 0, num_elts , comparator);
128 }
129
130 public /*(at)Interned*/ String min_elt() {
131 if (num_elts == 0)
132 throw new Error("Represents no elements");
133 sort_rep();
134 return elts[0];
135 }
136
137 public /*(at)Interned*/ String max_elt() {
138 if (num_elts == 0)
139 throw new Error("Represents no elements");
140 sort_rep();
141 return elts[num_elts-1];
142 }
143
144 // Assumes the other array is already sorted
145 public boolean compare_rep(int num_other_elts, /*(at)Interned*/ String[] other_elts) {
146 if (num_elts != num_other_elts)
147 return false;
148 sort_rep();
149 for (int i=0; i < num_elts; i++)
150 if (! ((elts[i]) == (other_elts[i]))) // elements are interned
151 return false;
152 return true;
153 }
154
155 private String subarray_rep() {
156 // Not so efficient an implementation, but simple;
157 // and how often will we need to print this anyway?
158 sort_rep();
159 StringBuffer sb = new StringBuffer();
160 sb.append("{ ");
161 for (int i=0; i<num_elts; i++) {
162 if (i != 0)
163 sb.append(", ");
164
165 if (PrintInvariants.dkconfig_static_const_infer) {
166 boolean curVarMatch = false;
167 PptTopLevel pptt = ppt.parent;
168 for (VarInfo vi : pptt.var_infos) {
169 if (vi.is_static_constant && VarComparability.comparable(vi, var())) {
170 Object constantVal = vi.constantValue();
171 if (constantVal.equals(elts[i])) {
172 sb.append(vi.name());
173 curVarMatch = true;
174 }
175 }
176 }
177
178 if (curVarMatch == false) {
179 sb.append(((elts[i]==null) ? "null" : "\"" + UtilMDE.escapeNonASCII(elts[i]) + "\""));
180 }
181 }
182 else {
183 sb.append(((elts[i]==null) ? "null" : "\"" + UtilMDE.escapeNonASCII(elts[i]) + "\""));
184 }
185
186 }
187 sb.append(" }");
188 return sb.toString();
189 }
190
191 public String repr() {
192 return "OneOfString" + varNames() + ": "
193 + "falsified=" + falsified
194 + ", num_elts=" + num_elts
195 + ", elts=" + subarray_rep();
196 }
197
198 public /*(at)Interned*/ String[] getElts() {
199 /*(at)Interned*/ String[] temp = new /*(at)Interned*/ String[elts.length];
200 for (int i=0; i < elts.length; i++) {
201 temp[i] = elts[i];
202 }
203 return temp;
204 }
205
206 public String format_using(OutputFormat format) {
207 sort_rep();
208
209 if (format.isJavaFamily()) return format_java_family(format);
210
211 if (format == OutputFormat.DAIKON) {
212 return format_daikon();
213 } else if (format == OutputFormat.SIMPLIFY) {
214 return format_simplify();
215 } else if (format == OutputFormat.ESCJAVA) {
216 return format_esc();
217 } else {
218 return format_unimplemented(format);
219 }
220 }
221
222 public String format_daikon() {
223 String varname = var().name();
224 if (num_elts == 1) {
225
226 boolean is_type = is_type();
227 if (! is_type) {
228 return varname + " == " + ((elts[0]==null) ? "null" : "\"" + UtilMDE.escapeNonASCII(elts[0]) + "\"");
229 } else {
230 // It's a type
231 String str = elts[0];
232 if ((str == null) || "null".equals(str)) {
233 return varname + " == null";
234 } else {
235 if (str.startsWith("[")) {
236 str = UtilMDE.classnameFromJvm(str);
237 }
238 if (PrintInvariants.dkconfig_static_const_infer) {
239 PptTopLevel pptt = ppt.parent;
240 for (VarInfo vi : pptt.var_infos) {
241 if (vi.is_static_constant && VarComparability.comparable(vi, var())) {
242 Object constantVal = vi.constantValue();
243 if (constantVal.equals(str)) {
244 return varname + " == " + vi.name();
245 }
246 }
247 }
248 }
249 // ".class" (which is a suffix for a type name) and not
250 // getClassSuffix (which is a suffix for an expression).
251 return varname + " == " + str + ".class";
252 }
253 }
254
255 } else {
256 return varname + " one of " + subarray_rep();
257 }
258 }
259
260 private boolean is_type() {
261 return var().has_typeof();
262 }
263
264 private static Pattern dollar_char_pat = Pattern.compile("\\$([A-Za-z])");
265
266 private static String format_esc_string2type(String str) {
267 if ((str == null) || "null".equals(str)) {
268 return "\\typeof(null)";
269 }
270 String type_str;
271 if (str.startsWith("[")) {
272 type_str = UtilMDE.classnameFromJvm(str);
273 } else {
274 type_str = str;
275 if (type_str.startsWith("\"") && type_str.endsWith("\"")) {
276 type_str = type_str.substring(1, type_str.length()-1);
277 }
278 }
279
280 // Inner classes
281 // type_str = type_str.replace('$', '.');
282 // For named inner classes, convert "$" to ".".
283 // For anonymous inner classes, leave as "$".
284 Matcher m = dollar_char_pat.matcher(type_str);
285 type_str = m.replaceAll(".$1");
286
287 return "\\type(" + type_str + ")";
288 }
289
290 public String format_esc() {
291 sort_rep();
292
293 String varname = var().esc_name();
294
295 String result;
296
297 // We cannot say anything about Strings in ESC, just types (which
298 // Daikon stores as Strings).
299 if (! is_type()) {
300 result = format_unimplemented(OutputFormat.ESCJAVA); // "needs to be implemented"
301 } else {
302 // Format \typeof(theArray) = "[Ljava.lang.Object;"
303 // as \typeof(theArray) == \type(java.lang.Object[])
304 // ... but still ...
305 // format \typeof(other) = "package.SomeClass;"
306 // as \typeof(other) == \type(package.SomeClass)
307
308 result = "";
309 for (int i=0; i<num_elts; i++) {
310 if (i != 0) { result += " || "; }
311 result += varname + " == " + format_esc_string2type(elts[i]);
312 }
313 }
314
315 return result;
316 }
317
318 public String format_java_family(OutputFormat format) {
319
320 String result;
321
322 // Setting up the name of the unary variable
323 String varname = var().name_using(format);
324
325 result = "";
326 boolean is_type = is_type();
327 for (int i=0; i<num_elts; i++) {
328 if (i != 0) { result += " || "; }
329 String str = elts[i];
330 if (!is_type) {
331 result += varname + ".equals(" + ((str==null) ? "null" : "\"" + UtilMDE.escapeNonASCII(str) + "\"") + ")";
332 } else {
333 // It's a type
334 if ((str == null) || "null".equals(str)) {
335 result += varname + " == null";
336 } else {
337 if (str.startsWith("[")) {
338 str = UtilMDE.classnameFromJvm(str);
339 }
340 // ".class" (which is a suffix for a type name) and not
341 // getClassSuffix (which is a suffix for an expression).
342 result += varname + " == " + str + ".class";
343 }
344 }
345 }
346
347 return result;
348 }
349
350 public String format_simplify() {
351
352 sort_rep();
353
354 String varname =
355 var().simplifyFixup(var().name_using(OutputFormat.SIMPLIFY));
356
357 String result;
358
359 result = "";
360 boolean is_type = is_type();
361 for (int i=0; i<num_elts; i++) {
362 String value = elts[i];
363 if (is_type) {
364 if (value == null) {
365 // do nothing
366 } else if (value.startsWith("[")) {
367 value = UtilMDE.classnameFromJvm(value);
368 } else if (value.startsWith("\"") && value.endsWith("\"")) {
369 value = value.substring(1, value.length()-1);
370 }
371 value = "|T_" + value + "|";
372 } else {
373 value = simplify_format_string(value);
374 }
375 result += " (EQ " + varname + " " + value + ")";
376 }
377 if (num_elts > 1) {
378 result = "(OR" + result + ")";
379 } else if (num_elts == 1) {
380 // chop leading space
381 result = result.substring(1);
382 } else if (num_elts == 0) {
383 return format_too_few_samples(OutputFormat.SIMPLIFY, null);
384 }
385
386 if (result.indexOf("format_simplify") == -1)
387 daikon.simplify.SimpUtil.assert_well_formed(result);
388 return result;
389 }
390
391 public InvariantStatus add_modified(/*(at)Interned*/ String a, int count) {
392 return runValue(a, count, true);
393 }
394
395 public InvariantStatus check_modified(/*(at)Interned*/ String a, int count) {
396 return runValue(a, count, false);
397 }
398
399 private InvariantStatus runValue(/*(at)Interned*/ String v, int count, boolean mutate) {
400 InvariantStatus status;
401 if (mutate) {
402 status = add_mod_elem(v, count);
403 } else {
404 status = check_mod_elem(v, count);
405 }
406 if (status == InvariantStatus.FALSIFIED) {
407 if (logOn() && mutate) {
408 StringBuffer eltString = new StringBuffer();
409 for (int i = 0; i < num_elts; i++) {
410 eltString.append(((elts[i]==null) ? "null" : "\"" + UtilMDE.escapeNonASCII(elts[i]) + "\"") + " ");
411 }
412 log ("destroyed on sample " + ((v==null) ? "null" : "\"" + UtilMDE.escapeNonASCII(v) + "\"") + " previous vals = { "
413 + eltString + "} num_elts = " + num_elts);
414 }
415 return InvariantStatus.FALSIFIED;
416 }
417 return status;
418 }
419
420 /**
421 * Adds a single sample to the invariant. Returns
422 * the appropriate InvariantStatus from the result
423 * of adding the sample to this.
424 */
425 public InvariantStatus add_mod_elem (/*(at)Interned*/ String v, int count) {
426 InvariantStatus status = check_mod_elem(v, count);
427 if (status == InvariantStatus.WEAKENED) {
428 elts[num_elts] = v;
429 num_elts++;
430 }
431 return status;
432 }
433
434 /**
435 * Checks a single sample to the invariant. Returns
436 * the appropriate InvariantStatus from the result
437 * of adding the sample to this.
438 */
439 public InvariantStatus check_mod_elem (/*(at)Interned*/ String v, int count) {
440
441 // Look for v in our list of previously seen values. If it's
442 // found, we're all set.
443 for (int i=0; i<num_elts; i++) {
444 //if (logDetail())
445 // log ("add_modified (" + v + ")");
446 if (((elts[i]) == ( v))) {
447 return (InvariantStatus.NO_CHANGE);
448 }
449 }
450
451 if (num_elts == dkconfig_size) {
452 return (InvariantStatus.FALSIFIED);
453 }
454
455 if (is_type() && (num_elts == 1)) {
456 return (InvariantStatus.FALSIFIED);
457 }
458
459 return (InvariantStatus.WEAKENED);
460 }
461
462 protected double computeConfidence() {
463 // This is not ideal.
464 if (num_elts == 0) {
465 return Invariant.CONFIDENCE_UNJUSTIFIED;
466 } else {
467 return Invariant.CONFIDENCE_JUSTIFIED;
468 }
469 }
470
471 public /*@Nullable*/ DiscardInfo isObviousStatically(VarInfo[] vis) {
472 // Static constants are necessarily OneOf precisely one value.
473 // This removes static constants from the output, which might not be
474 // desirable if the user doesn't know their actual value.
475 if (vis[0].isStaticConstant()) {
476 assert num_elts <= 1;
477 return new DiscardInfo(this, DiscardCode.obvious, vis[0].name() + " is a static constant.");
478 }
479 return super.isObviousStatically(vis);
480 }
481
482 /**
483 * Oneof can merge different formulas from lower points to create a single
484 * formula at an upper point.
485 */
486 public boolean mergeFormulasOk() {
487 return (true);
488 }
489
490 public boolean isSameFormula(Invariant o) {
491 OneOfString other = (OneOfString) o;
492 if (num_elts != other.num_elts)
493 return false;
494 if (num_elts == 0 && other.num_elts == 0)
495 return true;
496
497 sort_rep();
498 other.sort_rep();
499
500 for (int i=0; i < num_elts; i++) {
501 if (! ((elts[i]) == (other.elts[i])))
502 return false;
503 }
504
505 return true;
506 }
507
508 public boolean isExclusiveFormula(Invariant o) {
509 if (o instanceof OneOfString) {
510 OneOfString other = (OneOfString) o;
511
512 if (num_elts == 0 || other.num_elts == 0)
513 return false;
514 for (int i=0; i < num_elts; i++) {
515 for (int j=0; j < other.num_elts; j++) {
516 if (((elts[i]) == (other.elts[j]))) // elements are interned
517 return false;
518 }
519 }
520
521 return true;
522 }
523
524 return false;
525 }
526
527 // OneOf invariants that indicate a small set of possible values are
528 // uninteresting. OneOf invariants that indicate exactly one value
529 // are interesting.
530 public boolean isInteresting() {
531 if (num_elts() > 1) {
532 return false;
533 } else {
534 return true;
535 }
536 }
537
538 public boolean hasUninterestingConstant() {
539
540 return false;
541 }
542
543 public boolean isExact() {
544 return (num_elts == 1);
545 }
546
547 // Look up a previously instantiated invariant.
548 public static /*@Nullable*/ OneOfString find(PptSlice ppt) {
549 assert ppt.arity() == 1;
550 for (Invariant inv : ppt.invs) {
551 if (inv instanceof OneOfString)
552 return (OneOfString) inv;
553 }
554 return null;
555 }
556
557 // Interning is lost when an object is serialized and deserialized.
558 // Manually re-intern any interned fields upon deserialization.
559 private void readObject(ObjectInputStream in) throws IOException,
560 ClassNotFoundException {
561 in.defaultReadObject();
562
563 for (int i=0; i < num_elts; i++)
564 elts[i] = Intern.intern(elts[i]);
565 }
566
567 /**
568 * Merge the invariants in invs to form a new invariant. Each must be
569 * a OneOfString invariant. This code finds all of the oneof values
570 * from each of the invariants and returns the merged invariant (if any).
571 *
572 * @param invs List of invariants to merge. The invariants must all be
573 * of the same type and should come from the children of
574 * parent_ppt. They should also all be permuted to match
575 * the variable order in parent_ppt.
576 * @param parent_ppt Slice that will contain the new invariant
577 */
578 public /*@Nullable*/ Invariant merge (List<Invariant> invs, PptSlice parent_ppt) {
579
580 // Create the initial parent invariant from the first child
581 OneOfString first = (OneOfString) invs.get(0);
582 OneOfString result = first.clone();
583 result.ppt = parent_ppt;
584
585 // Loop through the rest of the child invariants
586 for (int i = 1; i < invs.size(); i++ ) {
587
588 // Get this invariant
589 OneOfString inv = (OneOfString) invs.get (i);
590
591 // Loop through each distinct value found in this child and add
592 // it to the parent. If the invariant is falsified, there is no parent
593 // invariant
594 for (int j = 0; j < inv.num_elts; j++) {
595 /*(at)Interned*/ String val = inv.elts[j];
596
597 InvariantStatus status = result.add_mod_elem(val, 1);
598 if (status == InvariantStatus.FALSIFIED) {
599 result.log ("child value '" + val + "' destroyed oneof");
600 return (null);
601 }
602 }
603 }
604
605 result.log ("Merged '" + result.format() + "' from " + invs.size()
606 + " child invariants");
607 return (result);
608 }
609
610 /**
611 * Setup the invariant with the specified elements. Normally
612 * used when searching for a specified OneOf
613 */
614 public void set_one_of_val (/*(at)Interned*/ String[] vals) {
615
616 num_elts = vals.length;
617 for (int i = 0; i < num_elts; i++)
618 elts[i] = Intern.intern (vals[i]);
619 }
620
621 /**
622 * Returns true if every element in this invariant is contained in
623 * the specified state. For example if x = 1 and the state contains
624 * 1 and 2, true will be returned.
625 */
626 public boolean state_match (Object state) {
627
628 if (num_elts == 0)
629 return (false);
630
631 if (!(state instanceof /*(at)Interned*/ String[]))
632 System.out.println ("state is of class '" + state.getClass().getName()
633 + "'");
634 /*(at)Interned*/ String[] e = (/*(at)Interned*/ String[]) state;
635 for (int i = 0; i < num_elts; i++) {
636 boolean match = false;
637 for (int j = 0; j < e.length; j++) {
638 if (elts[i] == e[j]) {
639 match = true;
640 break;
641 }
642 }
643 if (!match)
644 return (false);
645 }
646 return (true);
647 }
648
649 }