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