001 package daikon.inv;
002
003 import daikon.*;
004 import daikon.Debug;
005 import daikon.inv.unary.*;
006 import daikon.inv.binary.*;
007 import daikon.inv.ternary.*;
008 import daikon.inv.ternary.threeScalar.*;
009 import daikon.inv.filter.*;
010 import daikon.suppress.*;
011 import daikon.simplify.SimpUtil;
012 import daikon.simplify.LemmaStack;
013 import static daikon.inv.Invariant.asInvClass;
014
015 import plume.*;
016
017 import java.util.logging.Logger;
018 import java.util.logging.Level;
019 import java.util.regex.*;
020 import java.util.*;
021 import java.io.Serializable;
022
023 /**
024 * Base implementation for Invariant objects.
025 * Intended to be subclassed but not to be directly instantiated.
026 * Rules/assumptions for invariants:
027 *
028 * <li> For each program point's set of VarInfos, there exists exactly
029 * no more than one invariant of its type. For example, between
030 * variables a and b at PptTopLevel T, there will not be two instances
031 * of invariant I(a, b).
032 **/
033 /*@Prototype*/
034 public abstract class Invariant
035 implements Serializable, Cloneable // but don't YOU clone it
036 {
037 // We are Serializable, so we specify a version to allow changes to
038 // method signatures without breaking serialization. If you add or
039 // remove fields, you should change this number to the current date.
040 static final long serialVersionUID = 20040921L;
041
042 /**
043 * General debug tracer.
044 **/
045 public static final Logger debug = Logger.getLogger("daikon.inv.Invariant");
046
047 /**
048 * Debug tracer for printing invariants.
049 **/
050 public static final Logger debugPrint = Logger.getLogger ("daikon.print");
051
052 /**
053 * Debug tracer for invariant flow.
054 **/
055 public static final Logger debugFlow = Logger.getLogger ("daikon.flow.flow");
056
057 /**
058 * Debug tracer for printing equality invariants.
059 **/
060 public static final Logger debugPrintEquality = Logger.getLogger ("daikon.print.equality");
061
062 /**
063 * Debug tracer for isWorthPrinting() checks.
064 **/
065 public static final Logger debugIsWorthPrinting = Logger.getLogger("daikon.print.isWorthPrinting");
066
067 /**
068 * Debug tracer for guarding.
069 **/
070 public static final Logger debugGuarding = Logger.getLogger("daikon.guard");
071
072 /**
073 * Debug tracer for isObvious checks.
074 **/
075 public static final Logger debugIsObvious = Logger.getLogger("daikon.inv.Invariant.isObvious");
076
077 /**
078 * Floating-point number between 0 and 1. Invariants are displayed only if
079 * the confidence that the invariant did not occur by chance is
080 * greater than this. (May also be set
081 * via <samp>--conf_limit</samp> switch to Daikon; refer to manual.)
082 **/
083 public static double dkconfig_confidence_limit = .99;
084
085 /**
086 * A boolean value. If true, Daikon's Simplify output (printed when
087 * the <samp>--format simplify</samp> flag is enabled, and used internally by
088 * <samp>--suppress_redundant</samp>)
089 * will include new predicates representing
090 * some complex relationships in invariants, such as lexical
091 * ordering among sequences. If false, some complex relationships
092 * will appear in the output as complex quantified formulas, while
093 * others will not appear at all. When enabled, Simplify may be able
094 * to make more inferences, allowing <samp>--suppress_redundant</samp> to
095 * suppress more redundant invariants, but Simplify may also run
096 * more slowly.
097 **/
098 public static boolean dkconfig_simplify_define_predicates = false;
099
100 /**
101 * Floating-point number between 0 and 0.1, representing the maximum
102 * relative difference
103 * between two floats for fuzzy comparisons. Larger values will
104 * result in floats that are relatively farther apart being treated
105 * as equal. A value of 0 essentially disables fuzzy comparisons.
106 * Specifically, if <code>abs (1 - f1/f2)</code> is less than or equal
107 * to this value, then the two doubles (<code>f1</code> and <code>f2</code>)
108 * will be treated as equal by
109 * Daikon.
110 */
111 public static double dkconfig_fuzzy_ratio = 0.0001;
112
113
114 /**
115 * The program point for this invariant; includes values, number of
116 * samples, VarInfos, etc. Can be null for a "prototype" invariant.
117 **/
118 /*@Unused(when=Prototype.class)*/
119 public PptSlice ppt;
120
121 // Has to be public so wrappers can read it.
122 /**
123 * True exactly if the invariant has been falsified: it is guaranteed
124 * never to hold (and should be either in the process of being destroyed
125 * or about to be destroyed. This should never be set directly; instead,
126 * call destroy().
127 **/
128 protected boolean falsified = false;
129
130 // Whether an invariant is a guarding predicate, that is, creately solely
131 // for the purpose of ensuring invariants with variables that can be
132 // missing do not cause exceptions when tested. If this is true, then
133 // the invariant itself does not hold over the observed data.
134 public boolean isGuardingPredicate = false;
135
136 /**
137 * The probability that this could have happened by chance alone. <br>
138 * 1 = could never have happened by chance; that is, we are fully confident
139 * that this invariant is a real invariant
140 **/
141 public static final double CONFIDENCE_JUSTIFIED = 1;
142
143 /**
144 * (0..1) = greater to lesser likelihood of coincidence <br>
145 * 0 = must have happened by chance
146 **/
147 public static final double CONFIDENCE_UNJUSTIFIED = 0;
148
149 /**
150 * -1 = delete this invariant; we know it's not true
151 **/
152 public static final double CONFIDENCE_NEVER = -1;
153
154
155 /**
156 * The probability that this could have happened by chance alone. <br>
157 * 0 = could never have happened by chance; that is, we are fully confident
158 * that this invariant is a real invariant
159 **/
160 public static final double PROBABILITY_JUSTIFIED = 0;
161
162 /**
163 * (0..1) = lesser to greater likelihood of coincidence <br>
164 * 1 = must have happened by chance
165 **/
166 public static final double PROBABILITY_UNJUSTIFIED = 1;
167
168 /**
169 * 3 = delete this invariant; we know it's not true
170 **/
171 public static final double PROBABILITY_NEVER = 3;
172
173 /**
174 * Return Invariant.CONFIDENCE_JUSTIFIED if x≥goal.
175 * Return Invariant.CONFIDENCE_UNJUSTIFIED if x≤1.
176 * For intermediate inputs, the result gives confidence that grades
177 * between the two extremes.
178 * See the discussion of gradual vs. sudden confidence transitions.
179 **/
180 public static final double conf_is_ge(double x, double goal) {
181 if (x>=goal)
182 return 1;
183 if (x<=1)
184 return 0;
185 double result = 1 - (goal - x)/(goal-1);
186 assert 0 <= result && result <= 1
187 : "conf_is_ge: bad result = " + result + " for (x=" + x + ", goal=" + goal + ")";
188 return result;
189 }
190
191 /**
192 * Return Invariant.PROBABILITY_JUSTIFIED if x≥goal.
193 * Return Invariant.PROBABILITY_UNJUSTIFIED if x≤1.
194 * For intermediate inputs, the result gives probability that grades
195 * between the two extremes.
196 * See the discussion of gradual vs. sudden probability transitions.
197 **/
198 public static final double prob_is_ge(double x, double goal) {
199 if (x>=goal)
200 return 0;
201 if (x<=1)
202 return 1;
203 double result = (goal - x)/(goal-1);
204 assert 0 <= result && result <= 1
205 : "prob_is_ge: bad result = " + result + " for (x=" + x + ", goal=" + goal + ")";
206 return result;
207 }
208
209
210 /** Return the confidence that both conditions are satisfied. */
211 public static final double confidence_and(double c1, double c2) {
212 assert 0 <= c1 && c1 <= 1 : "confidence_and: bad c1 = " + c1;
213 assert 0 <= c2 && c2 <= 1 : "confidence_and: bad c2 = " + c2;
214
215 double result = c1*c2;
216
217 assert 0 <= result && result <= 1 : "confidence_and: bad result = " + result;
218 return result;
219 }
220
221 /** Return the confidence that all three conditions are satisfied. */
222 public static final double confidence_and(double c1, double c2, double c3) {
223 assert 0 <= c1 && c1 <= 1 : "confidence_and: bad c1 = " + c1;
224 assert 0 <= c2 && c2 <= 1 : "confidence_and: bad c2 = " + c1;
225 assert 0 <= c3 && c3 <= 1 : "confidence_and: bad c3 = " + c1;
226
227 double result = c1*c2*c3;
228
229 assert 0 <= result && result <= 1 : "confidence_and: bad result = " + result;
230 return result;
231 }
232
233 /** Return the confidence that either condition is satisfied. */
234 public static final double confidence_or(double c1, double c2) {
235 // Not "1-(1-c1)*(1-c2)" because that can produce a value too large; we
236 // don't want the result to be larger than the larger argument.
237 return Math.max(c1, c2);
238 }
239
240
241 /** Return the probability that both conditions are satisfied. */
242 public static final double prob_and(double p1, double p2) {
243 assert 0 <= p1 && p1 <= 1 : "prob_and: bad p1 = " + p1;
244 assert 0 <= p2 && p2 <= 1 : "prob_and: bad p2 = " + p2;
245
246 // 1 - (1-p1)*(1-p2)
247 double result = p1 + p2 - p1*p2;
248
249 assert 0 <= result && result <= 1 : "prob_and: bad result = " + result;
250 return result;
251 }
252
253 /** Return the probability that all three conditions are satisfied. */
254 public static final double prob_and(double p1, double p2, double p3) {
255 assert 0 <= p1 && p1 <= 1 : "prob_and: bad p1 = " + p1;
256 assert 0 <= p2 && p2 <= 1 : "prob_and: bad p2 = " + p1;
257 assert 0 <= p3 && p3 <= 1 : "prob_and: bad p3 = " + p1;
258
259 double result = 1 - (1 - p1) * (1 - p2) * (1 - p3);
260
261 assert 0 <= result && result <= 1 : "prob_and: bad result = " + result;
262 return result;
263 }
264
265 /** Return the probability that either condition is satisfied. */
266 public static final double prob_or(double p1, double p2) {
267 // Not "p1*p2" because that can produce a value too small; we don't
268 // want the result to be smaller than the smaller argument.
269 return Math.min(p1, p2);
270 }
271
272
273 // Subclasses should set these; Invariant never does.
274
275 /**
276 * At least this many samples are required, or else we don't report any
277 * invariant at all. (Except that OneOf invariants are treated differently.)
278 **/
279 public static final int min_mod_non_missing_samples = 5;
280
281 /**
282 * @return true if the invariant has enough samples to have its
283 * computed constants well-formed. Is overridden in classes like
284 * LinearBinary/Ternary and Upper/LowerBound.
285 **/
286 public boolean enoughSamples() /*@NonPrototype*/ {
287 return true;
288 }
289
290
291 // The confidence routines (getConfidence and internal helper
292 // computeConfidence) use ModBitTracker information to compute
293 // justification.
294
295 // There are three confidence routines:
296 // justified() is what most clients should call
297 // getConfidence() gives the actual confidence. It used to cache
298 // results, but it does not do so any longer.
299 // computeConfidence() is an internal helper method that does the
300 // actual work, but it should not be called externally, only by
301 // getConfidence. It ignores whether the invariant is falsified.
302
303 // There are two general approaches to computing confidence
304 // when there is a threshold (such as needing to see 10 samples):
305 // * Make the confidence typically either 0 or 1, transitioning
306 // suddenly between the two as soon as the 10th sample is observed.
307 // * Make the confidence transition more gradually; for instance, each
308 // sample changes the confidence by 10%.
309 // The gradual approach has advantages and disadvantages:
310 // + Users can set the confidence limit to see invariants earlier; this
311 // is simpler than figuring out all the thresholds to set.
312 // + Tools such as the operational difference for test suite generation
313 // are assisted by knowing whether they are getting closer to
314 // justification.
315 // - The code is a bit more complicated.
316
317
318 /** A wrapper around getConfidence() or getConfidence(). **/
319 public final boolean justified() /*@NonPrototype*/ {
320 boolean just = (!falsified
321 && (getConfidence() >= dkconfig_confidence_limit));
322 if (logOn())
323 log ("justified = " + just + ", confidence = " + getConfidence()
324 + ", samples = " + ppt.num_samples());
325 return (just);
326 }
327
328 // If confidence == CONFIDENCE_NEVER, then this invariant can be eliminated.
329 /**
330 * Given that this invariant has been true for all values seen so far,
331 * this method returns the confidence that that situation has occurred
332 * by chance alone. The result is a value between 0 and 1 inclusive. 0
333 * means that this invariant could never have occurred by chance alone;
334 * we are fully confident that its truth is no coincidence. 1 means that
335 * the invariant is certainly a happenstance, so the truth of the
336 * invariant is not relevant and it should not be reported. Values
337 * between 0 and 1 give differing confidences in the invariant.
338 * <p>
339 *
340 * As an example, if the invariant is "x!=0", and only one value, 22, has
341 * been seen for x, then the conclusion "x!=0" is not justified. But if
342 * there have been 1,000,000 values, and none of them were 0, then we may
343 * be confident that the property "x!=0" is not a coincidence.
344 * <p>
345 *
346 * This method need not check the value of field "falsified", as the
347 * caller does that.
348 * <p>
349 *
350 * This method is a wrapper around computeConfidence(), which does the
351 * actual work.
352 * @see #computeConfidence()
353 **/
354 public final double getConfidence() /*@NonPrototype*/ {
355 assert ! falsified;
356 // if (falsified)
357 // return CONFIDENCE_NEVER;
358 double result = computeConfidence();
359 // System.out.println("getConfidence: " + getClass().getName() + " " + ppt.varNames());
360 if (!((result == CONFIDENCE_JUSTIFIED)
361 || (result == CONFIDENCE_UNJUSTIFIED)
362 || (result == CONFIDENCE_NEVER)
363 || ((0 <= result) && (result <= 1)))) {
364 // Can't print this.repr_prob(), as it may compute the confidence!
365 System.out.println("getConfidence: " + getClass().getName() + " " + ppt.varNames() + " => " + result);
366 System.out.println(" " + this.format() + "; " + repr());
367 }
368 assert ((0 <= result) && (result <= 1))
369 || (result == CONFIDENCE_JUSTIFIED)
370 || (result == CONFIDENCE_UNJUSTIFIED)
371 || (result == CONFIDENCE_NEVER)
372 : "unexpected conf value: " + getClass().getName() + ": " + repr() + ", result=" + result;
373 return result;
374 }
375
376 /**
377 * This method computes the confidence that this invariant occurred by chance.
378 * Users should use getConfidence() instead.
379 * @see #getConfidence()
380 **/
381 protected abstract double computeConfidence() /*@NonPrototype*/ ;
382
383 /**
384 * Subclasses should override. An exact invariant indicates that given
385 * all but one variable value, the last one can be computed. (I think
386 * that's correct, anyway.) Examples are IntComparison (when only
387 * equality is possible), LinearBinary, FunctionUnary.
388 * OneOf is treated differently, as an interface.
389 * The result of this method does not depend on whether the invariant is
390 * justified, destroyed, etc.
391 **/
392 public boolean isExact() /*@Prototype*/ {
393 return false;
394 }
395
396 // Implementations of this need to examine all the data values already
397 // in the ppt. Or, don't put too much work in the constructor and instead
398 // have the caller do that.
399 // The "ppt" argument can be null if this is a prototype invariant.
400 protected Invariant(PptSlice ppt) {
401 this.ppt = ppt;
402 }
403
404 protected /*@Prototype*/ Invariant() {
405 this.ppt = null;
406 }
407
408 @SuppressWarnings("unused")
409 private boolean isPrototype() {
410 return this.ppt == null;
411 }
412
413
414 /**
415 * Marks the invariant as falsified. Should always be called rather
416 * than just setting the flag so that we can track when this happens
417 */
418 public void falsify() /*@NonPrototype*/ {
419 falsified = true;
420 if (logOn())
421 log ("Destroyed " + format());
422 }
423
424 /** Clear the falsified flag. */
425 public void clear_falsified() /*@NonPrototype*/ {
426 falsified = false;
427 }
428
429 /** Returns whether or not this invariant has been destroyed. */
430 public boolean is_false() /*@NonPrototype*/ {
431 return (falsified);
432 }
433
434 /**
435 * Do nothing special, Overridden to remove
436 * exception from declaration
437 **/
438 public Invariant clone() /*@NonPrototype*/ {
439 try {
440 Invariant result = (Invariant) super.clone();
441 return result;
442 } catch (CloneNotSupportedException e) {
443 throw new Error(); // can never happen
444 }
445 }
446
447 /**
448 * Take an invariant and transfer it into a new PptSlice.
449 * @param new_ppt must have the same arity and types
450 * @param permutation gives the varinfo array index mapping in the
451 * new ppt
452 **/
453 public Invariant transfer(PptSlice new_ppt,
454 int[] permutation
455 ) /*@NonPrototype*/ {
456 // Check some sanity conditions
457 assert new_ppt.arity() == ppt.arity();
458 assert permutation.length == ppt.arity();
459 for (int i=0; i < ppt.arity(); i++) {
460 VarInfo oldvi = ppt.var_infos[i];
461 VarInfo newvi = new_ppt.var_infos[permutation[i]];
462 // We used to check that all 3 types were equal, but we can't do
463 // that anymore, because with equality, invariants may get
464 // transferred between old and new VarInfos of different types.
465 // They are, however, comparable
466 assert oldvi.comparableNWay(newvi);
467 }
468
469 Invariant result;
470 // Clone it
471 result = this.clone();
472
473 // Fix up the fields
474 result.ppt = new_ppt;
475 // Let subclasses fix what they need to
476 result = result.resurrect_done(permutation);
477
478 if (logOn()) {
479 result.log ("Created " + result.getClass().getName() + ":"
480 + result.format() + " via transfer from "
481 + getClass().getName() + ":" + format()
482 + " using permutation "
483 + ArraysMDE.toString (permutation)
484 + " old_ppt = " + ppt
485 + " new_ppt = " + new_ppt);
486 // result.log (UtilMDE.backTrace());
487 }
488 //if (debug.isLoggable(Level.FINE))
489 // debug.fine ("Invariant.transfer to " + new_ppt.name() + " "
490 // + result.repr());
491
492 return result;
493 }
494
495 /**
496 * Clones the invariant and then permutes it as specified. Normally
497 * used to make child invariant match the variable order of the parent
498 * when merging invariants bottom up.
499 */
500 public Invariant clone_and_permute (int[] permutation) /*@NonPrototype*/{
501
502 Invariant result = this.clone();
503 result = result.resurrect_done (permutation);
504
505 if (logOn())
506 result.log ("Created " + result.format() + " via clone_and_permute from "
507 + format() + " using permutation "
508 + ArraysMDE.toString (permutation)
509 + " old_ppt = " + VarInfo.arrayToString (ppt.var_infos)
510 // + " new_ppt = " + VarInfo.arrayToString (new_ppt.var_infos)
511 );
512
513 return (result);
514 }
515
516 /**
517 * Take a falsified invariant and resurrect it in a new PptSlice.
518 * @param new_ppt must have the same arity and types
519 * @param permutation gives the varinfo array index mapping
520 **/
521 public Invariant resurrect(PptSlice new_ppt,
522 int[] permutation
523 ) /*@NonPrototype*/ {
524 // Check some sanity conditions
525 assert falsified;
526 assert new_ppt.arity() == ppt.arity();
527 assert permutation.length == ppt.arity();
528 for (int i=0; i < ppt.arity(); i++) {
529 VarInfo oldvi = ppt.var_infos[i];
530 VarInfo newvi = new_ppt.var_infos[permutation[i]];
531 // We used to check that all 3 types were equal, but we can't do
532 // that anymore, because with equality, invariants may get
533 // resurrected between old and new VarInfos of different types.
534 // They are, however, comparable
535 assert oldvi.comparableNWay(newvi);
536 }
537
538 Invariant result;
539 // Clone it
540 result = this.clone();
541
542 // Fix up the fields
543 result.falsified = false;
544 result.ppt = new_ppt;
545 // Let subclasses fix what they need to
546 result = result.resurrect_done(permutation);
547
548 if (logOn())
549 result.log ("Created " + result.format() + " via resurrect from "
550 + format() + " using permutation "
551 + ArraysMDE.toString (permutation)
552 + " old_ppt = " + VarInfo.arrayToString (ppt.var_infos)
553 + " new_ppt = " + VarInfo.arrayToString (new_ppt.var_infos));
554
555 return result;
556 }
557
558 /**
559 * Returns a single VarComparability that describes the set of
560 * variables used by this invariant. Since all of the variables
561 * in an invariant must be comparable, this can usually be the
562 * comparability information for any variable. The exception is
563 * when one or more variables is always comparable (comparable to
564 * everythign else). An always comparable VarComparability is
565 * returned only if all of the variables involved are always
566 * comparable. Otherwise the comparability information from one
567 * of the non always-comparable variables is returned.
568 */
569 public VarComparability get_comparability() /*@NonPrototype*/{
570
571 // assert ppt != null : "class " + getClass();
572
573 // Return the first variable that is not always-comparable
574 for (int i = 0; i < ppt.var_infos.length; i++) {
575 VarComparability vc = ppt.var_infos[i].comparability;
576 if (!vc.alwaysComparable())
577 return (vc);
578 }
579
580 // All the variables are always-comparable, just return the first one
581 // return (ppt.var_infos[0].comparability);
582 return VarComparabilityImplicit.unknown;
583 }
584
585 /**
586 * Merge the invariants in invs to form a new invariant. This implementation
587 * merely returns a clone of the first invariant in the list. This is
588 * correct for simple invariants whose equation or statistics don't depend
589 * on the actual samples seen. It should be overriden for more complex
590 * invariants (eg, bound, oneof, linearbinary, etc).
591 *
592 * @param invs List of invariants to merge. The invariants must
593 * all be of the same type and should come from
594 * the children of parent_ppt. They should also all be
595 * permuted to match the variable order in parent_ppt.
596 * @param parent_ppt Slice that will contain the new invariant
597 *
598 * @return the merged invariant or null if the invariants didn't represent
599 * the same invariant.
600 */
601 public /*@Nullable*/ /*@NonPrototype*/ Invariant
602 merge (List</*@NonPrototype*/ Invariant> invs, PptSlice parent_ppt) /*@Prototype*/ {
603
604 Invariant first = invs.get(0);
605 Invariant result = first.clone();
606 result.ppt = parent_ppt;
607 result.log ("Merged '" + result.format() + "' from " + invs.size()
608 + " child invariants " /* + first.ppt.name() */);
609
610 // Make sure that each invariant was really of the same type
611 boolean assert_enabled = false;
612 assert (assert_enabled = true);
613 if (assert_enabled) {
614 Match m = new Match (result);
615 for (int i = 1; i < invs.size(); i++ )
616 assert m.equals (new Match (invs.get(i)));
617 }
618
619 return (result);
620
621 }
622
623 /**
624 * Permutes the invariant as specified. Often creates a new invariant
625 * (with a different class)
626 */
627 public /*@NonPrototype*/ Invariant permute (int[] permutation)
628 /*@NonPrototype*/ {
629 return (resurrect_done (permutation));
630 }
631
632 /**
633 * Called on the new invariant just before resurrect() returns it to
634 * allow subclasses to fix any information they might have cached
635 * from the old Ppt and VarInfos.
636 **/
637 protected abstract Invariant resurrect_done(int[] permutation)
638 /*@NonPrototype*/;
639
640 // Regrettably, I can't declare a static abstract method.
641 // // The return value is probably ignored. The new Invariant installs
642 // // itself on the PptSlice, and that's what really matters (right?).
643 // public static abstract Invariant instantiate(PptSlice ppt);
644
645 public boolean usesVar(VarInfo vi) /*@NonPrototype*/ {
646 return ppt.usesVar(vi);
647 }
648
649 public boolean usesVar(String name) /*@NonPrototype*/ {
650 return ppt.usesVar(name);
651 }
652
653 public boolean usesVarDerived(String name) /*@NonPrototype*/ {
654 return ppt.usesVarDerived(name);
655 }
656
657 // Not used as of 1/31/2000
658 // // For use by subclasses.
659 // /** Put a string representation of the variable names in the StringBuffer. */
660 // public void varNames(StringBuffer sb) {
661 // // sb.append(this.getClass().getName());
662 // ppt.varNames(sb);
663 // }
664
665 /** Return a string representation of the variable names. */
666 public final String varNames() /*@NonPrototype*/ {
667 return ppt.varNames();
668 }
669
670 // repr()'s output should not include result of getConfidence, because
671 // repr() may be called from computeConfidence or elsewhere for
672 // debugging purposes.
673 /**
674 * For printing invariants, there are two interfaces:
675 * repr gives a low-level representation
676 * (repr_prop also prints the confidence), and
677 * format gives a high-level representation for user output.
678 **/
679 public String repr() /*@NonPrototype*/ {
680 // A better default would be to use reflection and print out all
681 // the variable names.
682 return getClass() + varNames() + ": " + format();
683 }
684
685 /**
686 * For printing invariants, there are two interfaces:
687 * repr gives a low-level representation
688 * (repr_prop also prints the confidence), and
689 * format gives a high-level representation for user output.
690 **/
691 public String repr_prob() /*@NonPrototype*/ {
692 return repr()
693 + "; confidence = " + getConfidence()
694 ;
695 }
696
697 /**
698 * For printing invariants, there are two interfaces:
699 * repr gives a low-level representation
700 * (repr_prop also prints the confidence), and
701 * format gives a high-level representation for user output.
702 **/
703 public String format() /*@NonPrototype*/ {
704 String result = format_using(OutputFormat.DAIKON);
705 if (PrintInvariants.dkconfig_print_inv_class) {
706 String classname = getClass().getName();
707 int index = classname.lastIndexOf('.');
708 classname = classname.substring(index+1);
709 result = result + " [" + classname + "]";
710 }
711 return result;
712 }
713
714 public abstract String format_using(OutputFormat format) /*@NonPrototype*/ ;
715
716 /**
717 * @return conjuction of mapping the same function of our
718 * expresssions's VarInfos, in general. Subclasses may override if
719 * they are able to handle generally-inexpressible properties in
720 * special-case ways.
721 *
722 * @see VarInfo#isValidEscExpression
723 **/
724 public boolean isValidEscExpression() /*@NonPrototype*/ {
725 for (int i=0; i < ppt.var_infos.length; i++) {
726 if (! ppt.var_infos[i].isValidEscExpression()) {
727 return false;
728 }
729 }
730 return true;
731 }
732
733 /** A "\type(...)" construct where the "..." contains a "$". **/
734 private static Pattern anontype_pat = Pattern.compile("\\\\type\\([^\\)]*\\$");
735
736 /**
737 * @return true if this Invariant can be properly formatted for Java output.
738 **/
739 public boolean isValidExpression(OutputFormat format) /*@NonPrototype*/ {
740 if ((format == OutputFormat.ESCJAVA) && (! isValidEscExpression())) {
741 return false;
742 }
743
744 String s = format_using(format);
745
746 if ((format == OutputFormat.ESCJAVA) || format.isJavaFamily()) {
747 // This list should get shorter as we improve the formatting.
748 if ((s.indexOf(" needs to be implemented: ") != -1)
749 || (s.indexOf("<<") != -1)
750 || (s.indexOf(">>") != -1)
751 || (s.indexOf("warning: ") != -1)
752 || (s.indexOf('~') != -1)
753 || (s.indexOf("\\new") != -1)
754 || (s.indexOf(".toString ") != -1)
755 || (s.endsWith(".toString"))
756 || (s.indexOf(".getClass") != -1)
757 || (s.indexOf(".typeArray") != -1)
758 || (s.indexOf("warning: method") != -1)
759 || (s.indexOf("inexpressible") != -1)
760 || (s.indexOf("unimplemented") != -1)
761 || (s.indexOf("Infinity") != -1)
762 || anontype_pat.matcher(s).find()) {
763 return false;
764 }
765 }
766 return true;
767 }
768
769
770 /**
771 * @return standard "format needs to be implemented" for the given
772 * requested format. Made public so cores can call it.
773 **/
774 public String format_unimplemented(OutputFormat request) /*@NonPrototype*/ {
775 String classname = this.getClass().getName();
776 return "warning: method " + classname + ".format(" + request + ")"
777 + " needs to be implemented: " + format();
778 }
779
780 /**
781 * @return standard "too few samples for to have interesting
782 * invariant" for the requested format. For machine-readable
783 * formats, this is just "true". An optional string argument, if
784 * supplied, is a human-readable description of the invariant in its
785 * uninformative state, which will be added to the message.
786 **/
787 public String format_too_few_samples(OutputFormat request, /*@Nullable*/ String attempt) /*@NonPrototype*/ {
788 if (request == OutputFormat.SIMPLIFY) {
789 return "(AND)";
790 } else if (request == OutputFormat.JAVA ||
791 request == OutputFormat.ESCJAVA ||
792 request == OutputFormat.JML ||
793 request == OutputFormat.DBCJAVA ) {
794 return "true";
795 }
796 String classname = this.getClass().getName();
797 if (attempt == null) {
798 attempt = varNames();
799 }
800 return "warning: too few samples for " + classname
801 + " invariant: " + attempt;
802 }
803
804 /**
805 * Convert a floating point value into the weird Modula-3-like
806 * floating point format that the Simplify tool requires.
807 */
808 public static String simplify_format_double(double d) {
809 String s = d + "";
810 if (s.indexOf('E') != -1) {
811 // 1E6 -> 1d6
812 // 1.43E6 -> 1.43d6
813 s = s.replace('E', 'd');
814 } else if (s.indexOf('.') != -1) {
815 // 3.14 -> 3.14d0
816 s = s + "d0";
817 } else if (s.equals("-Infinity")) {
818 // -Infinity -> NegativeInfinity
819 s = "NegativeInfinity";
820 }
821 // 5 -> 5
822 // NaN -> NaN
823 // Infinity -> Infinity
824 return s;
825 }
826
827 /**
828 * Conver a long integer value into a format that Simplify can
829 * use. If the value is too big, we have to print it in a weird way,
830 * then tell Simplify about its properties specially. **/
831 public static String simplify_format_long(long l) {
832 LemmaStack.noticeInt(l);
833 if (l > -LemmaStack.SMALL_INTEGER && l < LemmaStack.SMALL_INTEGER) {
834 // Simplify's internal numeric representation is based on
835 // (ratios of) signed 32-bit integers, so it can't be both sound
836 // and precise with respect to integer overflow. In its default
837 // configuration it crashes with an internal error when any
838 // internal computation overflows. To work around this, we print
839 // large integers in an abstract format, and then explicitly
840 // give the ordering among those values. This loses other
841 // arithmetic facts, but is good enough for the way we use it.
842 // Examples of inputs containing large integers that crash:
843 // > (BG_PUSH (< 2147483647 n))
844 // (assertion in negative argument to GCD)
845 // > (BG_PUSH (>= x -1073741825))
846 // > (BG_PUSH (<= x 1073741825))
847 // > (OR)
848 // (assertion: unexpected negative value in the Simplex engine)
849 // > (BG_PUSH (EQ x 56312))
850 // > (BG_PUSH (EQ y (* y x)))
851 // (assertion: negative denomniator in rational normalize)
852 // The value 32000 for SMALL_INTEGER is semi-empirically derived
853 // as "2**15 - some slop" in hopes of working around as many
854 // potential overflows in Simplify as possible, while still
855 // letting it do concrete arithmetic on small integers. It may
856 // be that there's no bound that would work with arbitrary
857 // formulas, but this one seems to work OK for formulas
858 // generated by Daikon.
859 return "" + l;
860 } else {
861 return SimpUtil.formatInteger(l);
862 }
863 }
864
865 /**
866 * Convert a string value into the weird |-quoted format that the
867 * Simplify tool requires. (Note that Simplify doesn't distinguish
868 * between variables, symbolic constants, and strings, so we prepend
869 * "_string_" to avoid collisions with variables and other symbols).
870 */
871 public static String simplify_format_string(String s) {
872 if (s == null)
873 return "null";
874 StringBuffer buf = new StringBuffer("|_string_");
875 if (s.length() > 150) {
876 // Simplify can't handle long strings (its input routines have a
877 // 4000-character limit for |...| identifiers, but it gets an
878 // internal array overflow for ones more than about 195
879 // characters), so replace all but the beginning and end of a
880 // long string with a hashed summary.
881 int summ_length = s.length() - 100;
882 int p1 = 50 + summ_length / 4;
883 int p2 = 50 + summ_length / 2;
884 int p3 = 50 + 3 * summ_length / 4;
885 int p4 = 50 + summ_length;
886 StringBuffer summ_buf = new StringBuffer(s.substring(0, 50));
887 summ_buf.append("...");
888 summ_buf.append(Integer.toHexString(s.substring(50, p1).hashCode()));
889 summ_buf.append(Integer.toHexString(s.substring(p1, p2).hashCode()));
890 summ_buf.append(Integer.toHexString(s.substring(p2, p3).hashCode()));
891 summ_buf.append(Integer.toHexString(s.substring(p3, p4).hashCode()));
892 summ_buf.append("...");
893 summ_buf.append(s.substring(p4));
894 s = summ_buf.toString();
895 }
896 for (int i = 0; i < s.length(); i++) {
897 char c = s.charAt(i);
898 if (c == '\n') // not lineSep
899 buf.append("\\n"); // not lineSep
900 else if (c == '\r')
901 buf.append("\\r");
902 else if (c == '\t')
903 buf.append("\\t");
904 else if (c == '\f')
905 buf.append("\\f");
906 else if (c == '\\')
907 buf.append("\\\\");
908 else if (c == '|')
909 buf.append("\\|");
910 else if (c >= ' ' && c <= '~')
911 buf.append(c);
912 else {
913 buf.append("\\");
914 // AFAIK, Simplify doesn't glork Unicode, so lop off all but
915 // the low 8 bits
916 String octal = Integer.toOctalString(c & 0xff);
917 // Also, Simplify only accepts octal escapes with exactly 3 digits
918 while (octal.length() < 3)
919 octal = "0" + octal;
920 buf.append(octal);
921 }
922 }
923 buf.append("|");
924 return buf.toString();
925 }
926
927 // This should perhaps be merged with some kind of PptSlice comparator.
928 /**
929 * Compare based on arity, then printed representation.
930 **/
931 public static final class InvariantComparatorForPrinting implements Comparator<Invariant> {
932 /*@NonNullOnEntry("FileIO.new_decl_format")*/
933 public int compare(/*@NonPrototype*/ Invariant inv1, /*@NonPrototype*/ Invariant inv2) {
934 if (inv1 == inv2)
935 return 0;
936
937 // Guarding implications should compare as if they were without the
938 // guarding predicate
939
940 if (inv1 instanceof GuardingImplication)
941 inv1 = ((GuardingImplication)inv1).right;
942 if (inv2 instanceof GuardingImplication)
943 inv2 = ((GuardingImplication)inv2).right;
944
945 // Put equality invariants first
946 if ((inv1 instanceof Comparison) && (! (inv2 instanceof Comparison)))
947 return -1;
948 if ((! (inv1 instanceof Comparison)) && (inv2 instanceof Comparison))
949 return 1;
950
951 // assert inv1.ppt.parent == inv2.ppt.parent;
952 VarInfo[] vis1 = inv1.ppt.var_infos;
953 VarInfo[] vis2 = inv2.ppt.var_infos;
954 int arity_cmp = vis1.length - vis2.length;
955 if (arity_cmp != 0)
956 return arity_cmp;
957 // Comparing on variable index is wrong in general: variables of the
958 // same name may have different indices at different program points.
959 // However, it's safe if the invariants are from the same program
960 // point. Also, it is nice to avoid changing the order of variables
961 // from that of the data trace file.
962
963 if (inv1.ppt.parent == inv2.ppt.parent) {
964 for (int i=0; i<vis1.length; i++) {
965 int tmp = vis1[i].varinfo_index - vis2[i].varinfo_index;
966 if (tmp != 0) {
967 return tmp;
968 }
969 }
970 } else {
971 // // Debugging
972 // System.out.println("ICFP: different parents for " + inv1.format() + ", " + inv2.format());
973
974 for (int i=0; i<vis1.length; i++) {
975 String name1 = vis1[i].name();
976 String name2 = vis2[i].name();
977 if (name1.equals(name2)) {
978 continue;
979 }
980 int name1in2 = inv2.ppt.parent.indexOf(name1);
981 int name2in1 = inv1.ppt.parent.indexOf(name2);
982 int cmp1 = (name1in2 == -1) ? 0 : vis1[i].varinfo_index - name1in2;
983 int cmp2 = (name2in1 == -1) ? 0 : vis2[i].varinfo_index - name2in1;
984 int cmp = MathMDE.sign(cmp1) + MathMDE.sign(cmp2);
985 if (cmp != 0)
986 return cmp;
987 }
988 }
989
990 // Sort OneOf invariants earlier than others
991 if ((inv1 instanceof OneOf) && (! (inv2 instanceof OneOf)))
992 return -1;
993 if ((! (inv1 instanceof OneOf)) && (inv2 instanceof OneOf))
994 return 1;
995
996 // System.out.println("ICFP: default rule yields "
997 // + inv1.format().compareTo(inv2.format())
998 // + " for " + inv1.format() + ", " + inv2.format());
999 if (PrintInvariants.dkconfig_old_array_names && FileIO.new_decl_format)
1000 return inv1.format().replace ("[..]", "[]")
1001 .compareTo (inv2.format().replace ("[..]", "[]"));
1002 else
1003 return inv1.format().compareTo(inv2.format());
1004 }
1005 }
1006
1007 /**
1008 * @return true iff the two invariants represent the same
1009 * mathematical formula. Does not consider the context such as
1010 * variable names, confidences, sample counts, value counts, or
1011 * related quantities. As a rule of thumb, if two invariants format
1012 * the same, this method returns true. Furthermore, in many cases,
1013 * if an invariant does not involve computed constants (as "x>c" and
1014 * "y=ax+b" do for constants a, b, and c), then this method vacuously
1015 * returns true.
1016 *
1017 * @exception RuntimeException if other.getClass() != this.getClass()
1018 **/
1019 public boolean isSameFormula(Invariant other) /*@Prototype*/ {
1020 return false;
1021 }
1022
1023 /**
1024 * Returns whether or not it is possible to merge invariants of the same
1025 * class but with different formulas when combining invariants from lower
1026 * ppts to build invariants at upper program points. Invariants that
1027 * have this characteristic (eg, bound, oneof) should override this
1028 * function. Note that invariants that can do this, normally need special
1029 * merge code as well (to merge the different formulas into a single formula
1030 * at the upper point
1031 */
1032 public boolean mergeFormulasOk () /*@Prototype*/ {
1033 return (false);
1034 }
1035
1036 /**
1037 * @return true iff the argument is the "same" invariant as this.
1038 * Same, in this case, means a matching type, formula, and variable
1039 * names.
1040 **/
1041 public boolean isSameInvariant(Invariant inv2) /*@NonPrototype*/ {
1042 // return isSameInvariant(inv2, defaultIsSameInvariantNameExtractor);
1043
1044 Invariant inv1 = this;
1045
1046 // Can't be the same if they aren't the same type
1047 if (!inv1.getClass().equals(inv2.getClass())) {
1048 return false;
1049 }
1050
1051 // Can't be the same if they aren't the same formula
1052 if (!inv1.isSameFormula(inv2)) {
1053 return false;
1054 }
1055
1056 // The variable names much match up, in order
1057 VarInfo[] vars1 = inv1.ppt.var_infos;
1058 VarInfo[] vars2 = inv2.ppt.var_infos;
1059
1060 // due to inv type match already
1061 assert vars1.length == vars2.length;
1062
1063 for (int i=0; i < vars1.length; i++) {
1064 VarInfo var1 = vars1[i];
1065 VarInfo var2 = vars2[i];
1066 if (!var1.name().equals (var2.name()))
1067 return false;
1068 }
1069
1070 return true;
1071 }
1072
1073
1074 /**
1075 * @return true iff the two invariants represent mutually exclusive
1076 * mathematical formulas -- that is, if one of them is true, then the
1077 * other must be false. This method does not consider the context such
1078 * as variable names, confidences, sample counts, value counts, or
1079 * related quantities.
1080 **/
1081 public boolean isExclusiveFormula(Invariant other) /*@NonPrototype*/{
1082 return false;
1083 }
1084
1085
1086 /**
1087 * Look up a previously instantiated Invariant.
1088 **/
1089 // This implementation should be made more efficient, because it's used in
1090 // suppression. We should somehow index invariants by their type.
1091 public static /*@Nullable*/ Invariant find(Class<? extends Invariant> invclass, PptSlice ppt) {
1092 for (Invariant inv : ppt.invs) {
1093 if (inv.getClass() == invclass)
1094 return inv;
1095 }
1096 return null;
1097 }
1098
1099 /**
1100 * Returns the set of non-instantiating suppressions for this invariant.
1101 * May return null instead of an empty set.
1102 * Should be overridden by subclasses with non-instantiating suppressions.
1103 */
1104 public /*@Nullable*/ NISuppressionSet get_ni_suppressions() /*@Prototype*/ {
1105 return (null);
1106 }
1107
1108 /**
1109 * Returns whether or not this invariant is ni-suppressed.
1110 */
1111 /*@AssertNonNullIfTrue("get_ni_suppressions()")*/
1112 public boolean is_ni_suppressed() {
1113
1114 NISuppressionSet ss = get_ni_suppressions();
1115 if (ss == null)
1116 return (false);
1117 boolean suppressed = ss.suppressed (ppt);
1118 if (suppressed && Debug.logOn() && (Daikon.current_inv != null))
1119 Daikon.current_inv.log ("inv " + format() + " suppressed: " + ss);
1120 if (Debug.logDetail())
1121 log ("suppressed = " + suppressed + " suppression set = " + ss);
1122
1123 return (suppressed);
1124 }
1125
1126
1127 ///////////////////////////////////////////////////////////////////////////
1128 /// Tests about the invariant (for printing)
1129 ///
1130
1131 // DO NOT OVERRIDE. Should be declared "final", but the "final" is
1132 // omitted to allow for easier testing.
1133 public boolean isWorthPrinting() /*@NonPrototype*/ {
1134 return InvariantFilters.defaultFilters().shouldKeep(this) == null;
1135 }
1136
1137 ////////////////////////////////////////////////////////////////////////////
1138 // Static and dynamic checks for obviousness
1139
1140 /**
1141 * Return true if this invariant is necessarily true from a fact
1142 * that can be determined statically (i.e., the decls files) (e.g.,
1143 * by being from a certain derivation). Intended to be overridden
1144 * by subclasses.
1145 *
1146 * <p> This method is final because children of Invariant should be
1147 * extending isObviousStatically(VarInfo[]) because it is more
1148 * general.
1149 **/
1150 public final /*@Nullable*/ DiscardInfo isObviousStatically()
1151 /*@NonPrototype*/{
1152 return isObviousStatically(this.ppt.var_infos);
1153 }
1154
1155 /**
1156 * Return true if this invariant is necessarily true from a fact
1157 * that can be determined statically -- for the given varInfos
1158 * rather than the varInfos of this. Conceptually, this means "is
1159 * this invariant statically obvious if its VarInfos were switched
1160 * with vis?" Intended to be overridden by subclasses. Should only
1161 * do static checking.
1162 * Precondition: vis.length == this.ppt.var_infos.length
1163 * @param vis The VarInfos this invariant is obvious over. The
1164 * position and data type of the variables is the *same* as that of
1165 * this.ppt.var_infos.
1166 **/
1167 public /*@Nullable*/ DiscardInfo isObviousStatically(VarInfo[] vis) /*@Prototype*/ {
1168 return null;
1169 }
1170
1171 /**
1172 * Return true if this invariant and all equality combinations of
1173 * its member variables are necessarily true from a fact that can be
1174 * determined statically (i.e., the decls files). For example, a ==
1175 * b, and f(a) is obvious, but f(b) is not. In that case, this
1176 * method on f(a) would return false. If f(b) is also obvious, then
1177 * this method would return true.
1178 **/
1179 // This is used because we cannot decide to non-instantiate some
1180 // invariants just because isObviousStatically is true, since some
1181 // of the member variables may be equal to non-obvious varInfos. If
1182 // we were to non-instantiate, we could not copy an invariant to the
1183 // non-obvious VarInfos should they split off from the obvious one.
1184 // Of course, it's expensive to examine every possible permutation
1185 // of VarInfos and their equality set, so a possible conservative
1186 // approximation is to simply return false.
1187 public boolean isObviousStatically_AllInEquality() /*@NonPrototype*/ {
1188 // If the leaders aren't statically obvious, then clearly not all
1189 // combinations are.
1190 if (isObviousStatically() == null) return false;
1191
1192 for (int i = 0; i < ppt.var_infos.length; i++) {
1193 if (ppt.var_infos[i].equalitySet.getVars().size() > 1) return false;
1194 }
1195 return true;
1196 }
1197
1198 /**
1199 * Return true if this invariant and some equality combinations of
1200 * its member variables are statically obvious. For example, if a ==
1201 * b, and f(a) is obvious, then so is f(b). We use the someInEquality
1202 * (or least interesting) method during printing so we only print an
1203 * invariant if all its variables are interesting, since a single,
1204 * static, non interesting occurance means all the equality
1205 * combinations aren't interesting.
1206 * @return the VarInfo array that contains the VarInfos that showed
1207 * this invariant to be obvious. The contains variables that are
1208 * elementwise in the same equality set as this.ppt.var_infos. Can
1209 * be null if no such assignment exists.
1210 **/
1211 public /*@Nullable*/ DiscardInfo isObviousStatically_SomeInEquality()
1212 /*@NonPrototype*/ {
1213 DiscardInfo result = isObviousStatically();
1214 if (result != null) return result;
1215 return isObviousStatically_SomeInEqualityHelper (this.ppt.var_infos,
1216 new VarInfo[this.ppt.var_infos.length],
1217 0);
1218 }
1219
1220 // TODO: finish this comment.
1221 /**
1222 * Recurse through vis and generate the cartesian product of ...
1223 **/
1224 protected /*@Nullable*/ DiscardInfo
1225 isObviousStatically_SomeInEqualityHelper(VarInfo[] vis,
1226 VarInfo[] assigned,
1227 int position) /*@NonPrototype*/ {
1228 if (position == vis.length) {
1229 if (debugIsObvious.isLoggable(Level.FINE)) {
1230 StringBuffer sb = new StringBuffer();
1231 sb.append (" isObviousStatically_SomeInEquality: ");
1232 for (int i = 0; i < vis.length; i++) {
1233 sb.append (assigned[i].name() + " ");
1234 }
1235 debugIsObvious.fine (sb.toString());
1236 }
1237
1238 return isObviousStatically(assigned);
1239 } else {
1240 for (VarInfo vi : vis[position].get_equalitySet_vars ()) {
1241 assigned[position] = vi;
1242 DiscardInfo temp =
1243 isObviousStatically_SomeInEqualityHelper (vis, assigned, position + 1);
1244 if (temp != null) return temp;
1245 }
1246 return null;
1247 }
1248 }
1249
1250 /**
1251 * Return true if this invariant is necessarily true from a fact that can
1252 * be determined statically (i.e., the decls files) or dynamically (after
1253 * checking data). Intended not to be overriden, because sub-classes
1254 * should override isObviousStatically or isObviousDynamically. Wherever
1255 * possible, suppression, rather than this, should do the dynamic checking.
1256 **/
1257 public final /*@Nullable*/ DiscardInfo isObvious() /*@NonPrototype*/ {
1258 // Actually actually, we'll eliminate invariants as they become obvious
1259 // rather than on output; the point of this is to speed up computation.
1260 // // Actually, we do need to check isObviousDerived after all because we
1261 // // add invariants that might be obvious, but might also turn out to be
1262 // // even stronger (and so not obvious). We don't know how the invariant
1263 // // turns out until after testing it.
1264 // // // We don't need to check isObviousDerived because we won't add
1265 // // // obvious-derived invariants to lists in the first place.
1266 DiscardInfo staticResult = isObviousStatically_SomeInEquality();
1267 if (staticResult != null) {
1268 if (debugPrint.isLoggable(Level.FINE))
1269 debugPrint.fine (" [obvious: " + repr_prob() + " ]");
1270 return staticResult;
1271 } else {
1272 DiscardInfo dynamicResult = isObviousDynamically_SomeInEquality();
1273 if (dynamicResult != null) {
1274 if (debugPrint.isLoggable(Level.FINE))
1275 debugPrint.fine (" [obvious: " + repr_prob() + " ]");
1276 return dynamicResult;
1277 } else {
1278 return null;
1279 }
1280 }
1281 }
1282
1283 /**
1284 * Return non-null if this invariant is necessarily true from a fact that
1285 * can be determined dynamically (after checking data) -- for the given
1286 * varInfos rather than the varInfos of this. Conceptually, this means,
1287 * "Is this invariant dynamically obvious if its VarInfos were switched
1288 * with vis?" Intended to be overriden by subclasses so they can filter
1289 * invariants after checking; the overriding method should first call
1290 * "super.isObviousDynamically(vis)". Since this method is
1291 * dynamic, it should only be called after all processing.
1292 **/
1293 public /*@Nullable*/ DiscardInfo isObviousDynamically(VarInfo[] vis) /*@NonPrototype*/ {
1294 assert !Daikon.isInferencing;
1295 assert vis.length <= 3 : "Unexpected more-than-ternary invariant";
1296 if (! ArraysMDE.noDuplicates(vis)) {
1297 log ("Two or more variables are equal " + format());
1298 return new DiscardInfo(this, DiscardCode.obvious,
1299 "Two or more variables are equal");
1300 }
1301 // System.out.println("Passed Invariant.isObviousDynamically(): " + format());
1302 return null;
1303 }
1304
1305 /**
1306 * Return true if more than one of the variables in the invariant
1307 * are the same variable. We create such invariants for the purpose
1308 * of equality set processing, but they aren't intended for
1309 * printing; there should be invariants with the same meaning but
1310 * lower arity instead. For instance, we don't need "x = x + x"
1311 * because we have "x = 0" instead.
1312 *
1313 * Actually, this isn't strictly true: we don't have an invariant
1314 * "a[] is a palindrome" corresponding to "a[] is the reverse of
1315 * a[]", for instance.
1316 **/
1317 public boolean isReflexive() /*@NonPrototype*/ {
1318 return ! ArraysMDE.noDuplicates(ppt.var_infos);
1319 }
1320
1321 /**
1322 * Return true if this invariant is necessarily true from a fact
1323 * that can be determined dynamically (after checking data). Since
1324 * this method is dynamic, it should only be called after all
1325 * processing.
1326 *
1327 * <p> This method is final because subclasses should extend
1328 * isObviousDynamically(VarInfo[]) since that method is more general.
1329 **/
1330 public final /*@Nullable*/ DiscardInfo isObviousDynamically()
1331 /*@NonPrototype*/{
1332 assert !Daikon.isInferencing;
1333 return isObviousDynamically (ppt.var_infos);
1334 }
1335
1336 /**
1337 * Return true if this invariant and some equality combinations of
1338 * its member variables are dynamically obvious. For example, a ==
1339 * b, and f(a) is obvious, so is f(b). We use the someInEquality
1340 * (or least interesting) method during printing so we only print an
1341 * invariant if all its variables are interesting, since a single,
1342 * dynamic, non interesting occurance means all the equality
1343 * combinations aren't interesting.
1344 * @return the VarInfo array that contains the VarInfos that showed
1345 * this invariant to be obvious. The contains variables that are
1346 * elementwise in the same equality set as this.ppt.var_infos. Can
1347 * be null if no such assignment exists.
1348 **/
1349 public /*@Nullable*/ DiscardInfo isObviousDynamically_SomeInEquality()
1350 /*@NonPrototype*/ {
1351 DiscardInfo result = isObviousDynamically();
1352 if (result != null)
1353 return result;
1354 return isObviousDynamically_SomeInEqualityHelper (this.ppt.var_infos,
1355 new VarInfo[this.ppt.var_infos.length],
1356 0);
1357 }
1358
1359 /**
1360 * Recurse through vis (an array of leaders) and generate the cartesian
1361 * product of their equality sets; in other words, every combination of
1362 * one element from each equality set. For each such combination, test
1363 * isObviousDynamically; if any test is true, then return that
1364 * combination. The combinations are generated via recursive calls to
1365 * this routine.
1366 **/
1367 protected /*@Nullable*/ DiscardInfo
1368 isObviousDynamically_SomeInEqualityHelper(VarInfo[] vis,
1369 VarInfo[] assigned,
1370 int position) /*@NonPrototype*/ {
1371 if (position == vis.length) {
1372 // base case
1373 if (debugIsObvious.isLoggable(Level.FINE)) {
1374 StringBuffer sb = new StringBuffer();
1375 sb.append (" isObviousDynamically_SomeInEquality: ");
1376 for (int i = 0; i < vis.length; i++) {
1377 sb.append (assigned[i].name() + " ");
1378 }
1379 debugIsObvious.fine (sb.toString());
1380 }
1381 return isObviousDynamically (assigned);
1382 } else {
1383 // recursive case
1384 for (VarInfo vi : vis[position].get_equalitySet_vars ()) {
1385 assigned[position] = vi;
1386 DiscardInfo temp =
1387 isObviousDynamically_SomeInEqualityHelper (vis, assigned, position + 1);
1388 if (temp != null) return temp;
1389 }
1390 return null;
1391 }
1392 }
1393
1394
1395 /**
1396 * @return true if this invariant is only over prestate variables .
1397 */
1398 public boolean isAllPrestate() /*@NonPrototype*/ {
1399 return ppt.allPrestate();
1400 }
1401
1402 // The notion of "interesting" embodied by this method is
1403 // unclear. You'd probably be better off using
1404 // hasUninterestingConstant(), or some other filter.
1405 // Uninteresting invariants will override this method to return
1406 // false
1407 public boolean isInteresting() /*@NonPrototype*/ {
1408 return true;
1409 }
1410
1411
1412 /** This is the test that's planned to replace the poorly specified
1413 * "isInteresting" check. In the future, the set of interesting
1414 * constants might be determined by a static analysis of the source
1415 * code, but for the moment, we only consider -1, 0, 1, and 2 as
1416 * interesting.
1417 *
1418 * Intuitively, the justification for this test is that an invariant
1419 * that includes an uninteresting constant (say, "size(x[]) < 237")
1420 * is likely to be an artifact of the way the program was tested,
1421 * rather than a statement that would in fact hold over all possible
1422 * executions. */
1423 public boolean hasUninterestingConstant() /*@NonPrototype*/ {
1424 return false;
1425 }
1426
1427 // Orders invariants by class, then by variable names. If the
1428 // invariants are both of class Implication, they are ordered by
1429 // comparing the predicate, then the consequent.
1430 public static final class ClassVarnameComparator implements Comparator<Invariant> {
1431 public int compare(Invariant inv1, Invariant inv2) {
1432
1433 if (inv1 instanceof Implication && inv2 instanceof Implication)
1434 return compareImplications((Implication) inv1, (Implication) inv2);
1435
1436 int compareClass = compareClass(inv1, inv2);
1437 if (compareClass != 0)
1438 return compareClass;
1439
1440 return compareVariables(inv1, inv2);
1441 }
1442
1443 // Returns 0 if the invariants are of the same class. Else,
1444 // returns the comparison of the class names.
1445 private int compareClass(Invariant inv1, Invariant inv2) {
1446 if (inv1.getClass().equals(inv2.getClass())) {
1447 if (inv1 instanceof DummyInvariant) {
1448 // This special case is needed because the other code
1449 // assumes that all invariants of a given class have the
1450 // same arity.
1451 String df1 = inv1.format();
1452 String df2 = inv2.format();
1453 int cmp = df1.compareTo(df2);
1454 if (cmp != 0)
1455 return cmp;
1456 return inv1.ppt.var_infos.length - inv2.ppt.var_infos.length;
1457 }
1458 return 0;
1459 } else {
1460 String classname1 = inv1.getClass().getName();
1461 String classname2 = inv2.getClass().getName();
1462 return classname1.compareTo(classname2);
1463 }
1464 }
1465
1466 // Returns 0 if the invariants have the same variable names.
1467 // Else, returns the comparison of the first variable names that
1468 // differ. Requires that the invariants be of the same class.
1469 private int compareVariables(Invariant inv1, Invariant inv2) {
1470 VarInfo[] vars1 = inv1.ppt.var_infos;
1471 VarInfo[] vars2 = inv2.ppt.var_infos;
1472
1473 // due to inv type match already
1474 assert vars1.length == vars2.length :
1475 "Bad type match: " + inv1.format() + " vs. " + inv2.format();
1476
1477 for (int i=0; i < vars1.length; i++) {
1478 VarInfo var1 = vars1[i];
1479 VarInfo var2 = vars2[i];
1480 int compare = var1.name().compareTo(var2.name());
1481 if (compare != 0)
1482 return compare;
1483 }
1484
1485 // All the variable names matched
1486 return 0;
1487 }
1488
1489 private int compareImplications(Implication inv1, Implication inv2) {
1490 int comparePredicate = compare(inv1.predicate(), inv2.predicate());
1491 if (comparePredicate != 0)
1492 return comparePredicate;
1493
1494 return compare(inv1.consequent(), inv2.consequent());
1495 }
1496 }
1497
1498 /**
1499 * Orders invariants by class, then variable names, then formula.
1500 * If the formulas are the same, compares the printed representation
1501 * obtained from the format() method.
1502 **/
1503 public static final class ClassVarnameFormulaComparator
1504 implements Comparator<Invariant> {
1505
1506 Comparator<Invariant> classVarnameComparator = new ClassVarnameComparator();
1507
1508 public int compare(/*@NonPrototype*/ Invariant inv1,
1509 /*@NonPrototype*/ Invariant inv2) {
1510 int compareClassVarname = classVarnameComparator.compare(inv1, inv2);
1511
1512 if (compareClassVarname != 0) {
1513 return compareClassVarname;
1514 }
1515
1516 if (inv1.isSameInvariant(inv2)) {
1517 return 0;
1518 }
1519
1520 int result = inv1.format().compareTo(inv2.format());
1521
1522 // The purpose of the assertion below would seem to be to insist that
1523 // anything that doesn't return true to isSameInvariant() will not
1524 // produce the same written formula. This can happen, however, if the
1525 // variables have a different order (as in function binary), but the
1526 // swapped variables are actually the same (since we create invariants
1527 // of the form f(a, a, a) because of equality sets.
1528 // assert result != 0
1529 // : "isSameInvariant() returned false "
1530 // + "(isSameFormula returned " + inv1.isSameFormula(inv2) + ")," + lineSep
1531 // + "but format().compareTo() returned 0:" + lineSep
1532 // + " " + inv1.format() + lineSep + " " + inv1.repr() + lineSep
1533 // + " " + inv1.ppt.parent.name + lineSep
1534 // + " " + inv2.format() + lineSep + " " + inv2.repr() + lineSep
1535 // + " " + inv1.ppt.parent.name + lineSep
1536 // ;
1537
1538 return result;
1539 }
1540 }
1541
1542 /**
1543 * Class used as a key to store invariants in a MAP where their
1544 * equality depends on the invariant representing the same invariant
1545 * (i.e., their class is the same) and the same internal state (when
1546 * multiple invariants with the same class are possible)
1547 *
1548 * Note that this is based on the Invariant type (i.e., class) and the
1549 * internal state and not on what ppt the invariant is in or what
1550 * variables it is over. Thus, invariants from different ppts are
1551 * the same if they represent the same type of invariant.
1552 */
1553 public static class Match {
1554
1555 public Invariant inv;
1556
1557 public Match (Invariant inv) {
1558 this.inv = inv;
1559 }
1560
1561 /*@AssertNonNullIfTrue("#0")*/
1562 public boolean equals (/*@Nullable*/ Object obj) {
1563 if (!(obj instanceof Match))
1564 return (false);
1565
1566 Match ic = (Match) obj;
1567 return (ic.inv.match (inv));
1568 }
1569
1570 public int hashCode() {
1571 return (inv.getClass().hashCode());
1572 }
1573 }
1574
1575 /**
1576 * Returns whether or not two invariants are of the same type. To
1577 * be of the same type, invariants must be of the same class.
1578 * Some invariant classes represent multiple invariants (such as
1579 * FunctionBinary). They must also be the same formula.
1580 * Note that invariants with different formulas based on their
1581 * samples (LinearBinary, Bounds, etc) will still match as
1582 * long as the mergeFormulaOk() method returns true.
1583 */
1584
1585 public boolean match (/*@Prototype*/ Invariant inv) {
1586
1587 if (inv.getClass() == getClass())
1588 return (inv.mergeFormulasOk() || isSameFormula (inv));
1589 else
1590 return (false);
1591 }
1592
1593 /**
1594 * Returns whether or not the invariant matches the specified state.
1595 * Must be overriden by subclasses that support this. Otherwise, it
1596 * returns true only if the state is null.
1597 */
1598 public boolean state_match (Object state) /*@NonPrototype*/ {
1599 return (state == null);
1600 }
1601
1602 /**
1603 * Create a guarding predicate for a given invariant.
1604 * Returns null if no guarding is needed.
1605 **/
1606 public /*@Nullable*/ /*@NonPrototype*/ Invariant
1607 createGuardingPredicate(boolean install) {
1608 if (debugGuarding.isLoggable(Level.FINE)) {
1609 debugGuarding.fine ("Guarding predicate being created for: ");
1610 debugGuarding.fine (" " + this.format());
1611 }
1612
1613 // Find which VarInfos must be guarded
1614 List<VarInfo> mustBeGuarded = getGuardingList();
1615
1616 if (mustBeGuarded.isEmpty()) {
1617 if (debugGuarding.isLoggable(Level.FINE)) {
1618 debugGuarding.fine ("No guarding is needed, returning");
1619 }
1620 return null;
1621 }
1622
1623 // This conjunction would look better if it was built up right-to-left.
1624 Invariant guardingPredicate = null;
1625 for (VarInfo vi : mustBeGuarded) {
1626 Invariant currentGuard = vi.createGuardingPredicate(install);
1627 if (currentGuard == null)
1628 continue;
1629 debugGuarding.fine (String.format("VarInfo %s guard is %s", vi, currentGuard));
1630 if (guardingPredicate == null) {
1631 guardingPredicate = currentGuard;
1632 } else {
1633 guardingPredicate = new AndJoiner(ppt.parent, guardingPredicate, currentGuard);
1634 }
1635 debugGuarding.fine (String.format(" predicate so far: %s", guardingPredicate));
1636 }
1637
1638 // If the guarding predicate has been previously constructed, return it.
1639 // Otherwise, we will return the newly constructed one.
1640 // This algorithm is inefficient.
1641 if (mustBeGuarded.size() > 1) {
1642 Invariants joinerViewInvs = ppt.parent.joiner_view.invs;
1643 for (Invariant currentInv : joinerViewInvs) {
1644 if (currentInv.isSameInvariant(guardingPredicate)) {
1645 return currentInv;
1646 }
1647 }
1648 }
1649 return guardingPredicate;
1650 }
1651
1652 // Gets a list of all the variables that must be guarded for this
1653 // invariant.
1654 public List<VarInfo> getGuardingList() /*@NonPrototype*/ {
1655 return getGuardingList(ppt.var_infos);
1656 }
1657
1658 public static List<VarInfo> getGuardingList(VarInfo[] varInfos) {
1659 List<VarInfo> guardingList = new ArrayList<VarInfo>();
1660
1661 for (int i=0; i<varInfos.length; i++) {
1662 // debugGuarding.fine (varInfos[i]);
1663 guardingList.addAll(varInfos[i].getGuardingList());
1664 // debugGuarding.fine (guardingSet.toString());
1665 }
1666
1667 return UtilMDE.removeDuplicates(guardingList);
1668 }
1669
1670
1671 // This is called only from finally_print_the_invariants().
1672 // Nothing is ever done with the result except print it and discard it.
1673 /**
1674 * This procedure guards one invariant and returns the resulting guarded
1675 * invariant (implication), without placing it in any slice and without
1676 * modifying the original invariant.
1677 * Returns null if the invariant does not need to be guarded.
1678 **/
1679 public /*@Nullable*/ /*@NonPrototype*/ Invariant createGuardedInvariant(boolean install) {
1680 if (Daikon.dkconfig_guardNulls == "never") { // interned
1681 return null;
1682 }
1683
1684 if (debugGuarding.isLoggable(Level.FINE)) {
1685 debugGuarding.fine (" Trying to add guard for: " + this + "; repr = " + repr());
1686 }
1687 if (isGuardingPredicate) {
1688 debugGuarding.fine (" Do not guard: this is a guarding predicate");
1689 return null;
1690 }
1691 Invariant guardingPredicate = createGuardingPredicate(install);
1692 if (debugGuarding.isLoggable(Level.FINE)) {
1693 if (guardingPredicate != null) {
1694 debugGuarding.fine (" Predicate: " +
1695 guardingPredicate.format());
1696 debugGuarding.fine (" Consequent: " +
1697 format());
1698 } else {
1699 debugGuarding.fine (" No implication needed");
1700 }
1701 }
1702
1703 if (guardingPredicate == null) {
1704 return null;
1705 }
1706
1707 Implication guardingImplication =
1708 GuardingImplication.makeGuardingImplication(ppt.parent, guardingPredicate, this, false);
1709
1710 if (install) {
1711 if (! ppt.parent.joiner_view.hasImplication(guardingImplication)) {
1712 ppt.parent.joiner_view.addInvariant(guardingImplication);
1713 }
1714 }
1715 return guardingImplication;
1716 }
1717
1718
1719 /**
1720 * Instantiates an invariant of the same class on the specified
1721 * slice. Must be overridden in each class. Must be used rather
1722 * than clone so that checks in instantiate for reasonable invariants
1723 * are done.
1724 * @return the new invariant
1725 */
1726 protected /*@NonPrototype*/ Invariant instantiate_dyn (PptSlice slice) /*@Prototype*/ {
1727 throw new Error("no instantiate_dyn for class " + getClass());
1728 }
1729
1730 /**
1731 * Returns whether or not this class of invariants are currently
1732 * enabled
1733 */
1734 public boolean enabled() /*@Prototype*/ {
1735 throw new Error("no implementation of enabled() for class " + getClass());
1736 }
1737
1738
1739 /**
1740 * Returns whether or not the invariant is valid over the specified
1741 * types.
1742 */
1743 // public boolean valid_types (ProglangType[] rep_types) {
1744 // throw new Error("no valid_types for class " + getClass());
1745 // return (false);
1746 // }
1747
1748 /**
1749 * Returns whether or not the invariant is valid over the basic types
1750 * in vis. This only checks basic types (scalar, string, array, etc)
1751 * and should match the basic superclasses of invariant (SingleFloat,
1752 * SingleScalarSequence, ThreeScalar, etc). More complex checks
1753 * that depend on variable details can be implemented in instantiate_ok()
1754 *
1755 * @see #instantiate_ok(VarInfo[])
1756 */
1757 public boolean valid_types (VarInfo[] vis) /*@Prototype*/ {
1758 throw new Error("no implementation of valid_types() for class " + getClass());
1759 }
1760
1761 /**
1762 * Checks to see if the invariant can reasonably be instantiated over
1763 * the specified variables. Checks details beyond what is provided
1764 * by valid_types. This should never be called without calling
1765 * valid_types first (implementations should be able to presume that
1766 * valid_types is true).
1767 *
1768 * @see #valid_types(VarInfo[])
1769 */
1770 public boolean instantiate_ok (VarInfo[] vis) /*@Prototype*/{
1771 return (true);
1772 }
1773
1774 // Every Invariant is either a regular Invariant, or a "prototype"
1775 // Invariant. A prototype invariant is really a factory. The
1776 // "instantiate" method should only be called on a prototype invariant,
1777 // and many methods should only be called on non-prototype methods.
1778 // Another (arguably better, though less convenient in certain ways)
1779 // design would not represent the factory as an Invariant object. An
1780 // object never transitions at runtime between being a factory/prototype
1781 // and being a normal invariant.
1782 //
1783 // Could we just use the class, such as Positive.class, as (a proxy for)
1784 // the factory?
1785 // * That would require use of reflection to call the constructor, which
1786 // is ugly.
1787 // * The factory needs at least some state is needed, for example to
1788 // distinguish between creating a division operator "a/b" vs. "b/a".
1789 //
1790 // Could the factories be represented by a separate class, unrelated in
1791 // the type hierarchy to Invariant?
1792 // * That would probably be a better design.
1793 // * instantiate_dyn would have to have more than just the single line that
1794 // it is right now; longer code is more error-prone.
1795 // * Not all the code for an invariant would be in a single class any
1796 // more; but it could still all be in the same file, for example.
1797 // * There are probably other difficulties that escape me at the moment.
1798
1799 /**
1800 * Instantiates this invariant over the specified slice. The slice
1801 * must not be null and its variables must be valid for this type of
1802 * invariant. Returns null if the invariant is not enabled or if the
1803 * invariant is not reasonable over the specified variables. Otherwise
1804 * returns the new invariant.
1805 */
1806 public /*@Nullable*/ Invariant instantiate (PptSlice slice) /*@Prototype*/ {
1807
1808 assert isPrototype(); // receiver should be a "prototype" invariant
1809 assert slice != null;
1810 if (! valid_types(slice.var_infos)) {
1811 System.out.printf("this.getClass(): %s%n", this.getClass());
1812 System.out.printf("slice: %s%n", slice);
1813 System.out.printf("slice.var_infos (length %d): %s%n", slice.var_infos.length, (Object)slice.var_infos);
1814 for (VarInfo vi : slice.var_infos) {
1815 System.out.printf(" var_info: %s %s%n", vi, vi.type);
1816 }
1817 }
1818 assert valid_types(slice.var_infos)
1819 : String.format("valid_types(%s) = false for %s", slice.var_infos, this);
1820 if (!enabled() || !instantiate_ok (slice.var_infos))
1821 return (null);
1822 Invariant inv = instantiate_dyn (slice);
1823 assert inv != null;
1824 if (inv.ppt == null) {
1825 // Avoid creating the message if the check succeeds
1826 assert inv.ppt != null : "invariant class " + inv.getClass();
1827 }
1828 return (inv);
1829 }
1830
1831 /**
1832 * Adds the specified sample to the invariant and returns the result.
1833 */
1834 public InvariantStatus add_sample (ValueTuple vt, int count)
1835 /*@NonPrototype*/ {
1836
1837 if (ppt instanceof PptSlice1) {
1838
1839 VarInfo v = ppt.var_infos[0];
1840 UnaryInvariant unary_inv = (UnaryInvariant) this;
1841 return (unary_inv.add (vt.getValue(v), vt.getModified(v), count));
1842
1843 } else if (ppt instanceof PptSlice2) {
1844
1845 VarInfo v1 = ppt.var_infos[0];
1846 VarInfo v2 = ppt.var_infos[1];
1847 BinaryInvariant bin_inv = (BinaryInvariant) this;
1848 return (bin_inv.add_unordered (vt.getValue(v1), vt.getValue(v2),
1849 vt.getModified(v1), count));
1850
1851 } else /* must be ternary */ {
1852
1853 VarInfo v1 = ppt.var_infos[0];
1854 VarInfo v2 = ppt.var_infos[1];
1855 VarInfo v3 = ppt.var_infos[2];
1856 assert (this instanceof TernaryInvariant)
1857 : "invariant '" + format() + "' in slice "
1858 + ppt.name() + " is not ternary";
1859 TernaryInvariant ternary_inv = (TernaryInvariant) this;
1860 return (ternary_inv.add (vt.getValue(v1), vt.getValue(v2),
1861 vt.getValue(v3), vt.getModified(v1), count));
1862 }
1863 }
1864
1865 /**
1866 * Check the rep invariants of this.
1867 **/
1868 public void repCheck() /*@Prototype*/{
1869 }
1870
1871 /**
1872 * Returns whether or not the invariant is currently active. This is
1873 * used to identify those invariants that require a certain number
1874 * of points before they actually do computation (eg, LinearBinary)
1875 *
1876 * This is used during suppresion. Any invariant that is not active
1877 * cannot suppress another invariant
1878 */
1879 public boolean isActive() /*@NonPrototype*/ {
1880 return (true);
1881 }
1882
1883 // TODO: The logDetail and (especially) logOn methods are misleading,
1884 // because they are static but are very often called with an instance as
1885 // the receiver, suggesting that they have something to do with the
1886 // receiver. This should be corrected. -MDE
1887
1888 /**
1889 * Returns whether or not detailed logging is on. Note that this check
1890 * is not performed inside the logging calls themselves, it must be
1891 * performed by the caller.
1892 *
1893 * @see daikon.Debug#logDetail()
1894 * @see daikon.Debug#logOn()
1895 * @see daikon.Debug#log(Logger, Class, Ppt, String)
1896 */
1897
1898 public static boolean logDetail () {
1899 return (Debug.logDetail());
1900 }
1901
1902 /**
1903 * Returns whether or not logging is on.
1904 *
1905 * @see daikon.Debug#logOn()
1906 */
1907
1908 public static boolean logOn() {
1909 return (Debug.logOn());
1910 }
1911
1912 /**
1913 * Logs a description of the invariant and the specified msg via the
1914 * logger as described in {@link daikon.Debug#log(Logger, Class, Ppt,
1915 * VarInfo[], String)}.
1916 */
1917
1918 public void log (Logger log, String msg) /*@NonPrototype*/ {
1919
1920 if (Debug.logOn()) {
1921 Debug.log (log, getClass(), ppt, msg);
1922 }
1923 }
1924
1925
1926 /**
1927 * Logs a description of the invariant and the specified msg via the
1928 * logger as described in {@link daikon.Debug#log(Logger, Class, Ppt,
1929 * VarInfo[], String)}.
1930 *
1931 * @return whether or not it logged anything
1932 */
1933
1934 public boolean log (String format, /*@Nullable*/ Object...args) /*@Raw*/ {
1935 if (ppt != null) {
1936 String msg = format;
1937 if (args.length > 0)
1938 msg = String.format (format, args);
1939 return (Debug.log (getClass(), ppt, msg));
1940 } else
1941 return (false);
1942 }
1943
1944 public String toString() /*@NonPrototype*/ {
1945 return format();
1946 }
1947
1948 public static String toString (/*@NonPrototype*/ Invariant[] invs) {
1949
1950 ArrayList<String> strings = new ArrayList<String>(invs.length);
1951 for (int i = 0; i < invs.length; i++) {
1952 if (invs[i] == null)
1953 strings.add("null");
1954 else
1955 strings.add(invs[i].format());
1956 }
1957 return UtilMDE.join(strings, ", ");
1958 }
1959
1960
1961 /**
1962 * Used throught Java family formatting of invariants.
1963 *
1964 * Returns
1965 *
1966 * "plume.FuzzyFloat.method(v1_name, v2_name)"
1967 *
1968 * Where v1_name and v2_name are the properly formatted
1969 * varinfos v1 and v2, under the given format.
1970 *
1971 * Author: Carlos Pacheco
1972 */
1973 // [[ This method doesn't belong here. But where? ]]
1974 public static String formatFuzzy(String method,
1975 VarInfo v1,
1976 VarInfo v2,
1977 OutputFormat format) {
1978
1979 StringBuffer results = new StringBuffer();
1980 return
1981 results
1982 .append("daikon.Quant.fuzzy.")
1983 .append(method)
1984 .append("(")
1985 .append(v1.name_using(format))
1986 .append(", ")
1987 .append(v2.name_using(format))
1988 .append(")")
1989 .toString();
1990 }
1991
1992 @SuppressWarnings("unchecked") // casting method
1993 public static Class<? extends Invariant> asInvClass(Object x) {
1994 return (Class<? extends Invariant>)x;
1995 }
1996
1997 }
1998
1999
2000
2001 // def format(self, args=None):
2002 // if self.one_of:
2003 // # If it can be None, print it only if it is always None and
2004 // # is an invariant over non-derived variable.
2005 // if self.can_be_None:
2006 // if ((len(self.one_of) == 1)
2007 // and self.var_infos):
2008 // some_nonderived = false
2009 // for vi in self.var_infos:
2010 // some_nonderived = some_nonderived or not vi.is_derived
2011 // if some_nonderived:
2012 // return "%s = uninit" % (args,)
2013 // elif len(self.one_of) == 1:
2014 // return "%s = %s" % (args, self.one_of[0])
2015 // ## Perhaps I should unconditionally return this value;
2016 // ## otherwise I end up printing ranges more often than small
2017 // ## numbers of values (because when few values and many samples,
2018 // ## the range always looks justified).
2019 // # If few samples, don't try to infer a function over the values;
2020 // # just return the list.
2021 // elif (len(self.one_of) <= 3) or (self.samples < 100):
2022 // return "%s in %s" % (args, util.format_as_set(self.one_of))
2023 // return None