001 package daikon.inv;
002
003 import daikon.*;
004 import daikon.Quantify.QuantFlags;
005
006 import utilMDE.*;
007 import java.util.logging.Logger;
008 import java.util.logging.Level;
009 import java.util.*;
010
011
012 // Note that this Invariant is used in a *very* different way from
013 // the same-named one in V2. In V2, this is just for printing. In V3,
014 // this does all the canonicalizing, etc.
015
016 // This is a Java (not Javadoc) comment because the Daikon user manual
017 // reproduces the Javadoc but doesn't need all these implementation
018 // details.
019 //
020 // During checking, Equality keeps track of variables that are
021 // comparable and equal, so we only need to instantiate (other)
022 // invariants for one member of each Equal set, the leader.
023 //
024 // During postProcessing, each instance of Equality instantiates into
025 // displaying several equality Comparison invariants ("x == y", "x ==
026 // z"). Equality invariants have leaders, which are the canonical
027 // forms of their variables. In the previous example, x is the
028 // leader. Equality invariants sort their variables by index ordering
029 // during checking. During printing, however, equality invariants may
030 // "pivot" -- that is, switch leaders if the current leader wouldn't
031 // be printed because it was not an interesting variable. Notice that
032 // when pivoting, all the other invariants based on this.leader also
033 // need to be pivoted.
034
035
036 /**
037 * Keeps track of sets of variables that are equal. Other invariants are
038 * instantiated for only one member of the Equality set, the leader. If
039 * variables <samp>x</samp>, <samp>y</samp>, and <samp>z</samp> are members
040 * of the Equality set and <samp>x</samp> is chosen as the leader, then
041 * the Equality will internally convert into binary comparison invariants
042 * that print as <samp>x == y</samp> and <samp>x == z</samp>.
043 *
044 **/
045 public final /*(at)Interned*/ class Equality
046 extends Invariant
047 {
048 // We are Serializable, so we specify a version to allow changes to
049 // method signatures without breaking serialization. If you add or
050 // remove fields, you should change this number to the current date.
051 static final long serialVersionUID = 20021231L;
052
053 public static final Logger debug =
054 Logger.getLogger ("daikon.inv.Equality");
055
056 public static final Logger debugPostProcess =
057 Logger.getLogger ("daikon.inv.Equality.postProcess");
058
059 /**
060 * How many samples this has seen.
061 **/
062 private int numSamples;
063
064 public void setSamples (int sample_cnt) {
065 numSamples = sample_cnt;
066 }
067
068 public int numSamples() {
069 return numSamples;
070 }
071
072 /**
073 * The Set of VarInfos that this represents equality for. Can
074 * change over time as this invariant weakens. Sorted by index
075 * until pivoting.
076 **/
077 private TreeSet<VarInfo> vars;
078
079 /** Returns the number of variables in the set. **/
080 public int size() {
081 return vars.size();
082 }
083
084 /**
085 * Returns the variables in their index order. Unmodifiable.
086 **/
087 public Set<VarInfo> getVars() {
088 return Collections.unmodifiableSet (vars);
089 }
090
091 /**
092 * @param variables Variables which are equivalent, with the canonical
093 * one first. Elements must be of type VarInfo.
094 **/
095 public Equality(Collection<VarInfo> variables, PptSlice ppt) {
096 super(ppt);
097 if (debug.isLoggable(Level.FINE)) {
098 debug.fine ("Creating at " + ppt.parent.name() + " vars: ");
099 }
100
101 numSamples = 0;
102 vars = new TreeSet<VarInfo>(VarInfo.IndexComparator.theInstance);
103 vars.addAll (variables);
104 VarInfo leader = leader();
105
106 // ensure well-formedness and set equality slots
107 assert variables.size() > 0;
108 assert vars.size() == variables.size();
109
110 for (VarInfo vi : variables) {
111 if (debug.isLoggable(Level.FINE)) {
112 debug.fine (" " + vi.name() + " [" + vi.comparability + "]");
113 }
114 assert vi.ppt == leader.ppt;
115 assert vi.comparableNWay (leader);
116 assert VarComparability.comparable (leader, vi)
117 : "not comparable " + leader.name() + " " + vi.name()
118 +" at ppt " + ppt.parent.name();
119 assert vi.rep_type.isArray() == leader.rep_type.isArray();
120 vi.equalitySet = this;
121 }
122 }
123
124 ////////////////////////
125 // Accessors
126
127
128 private /*@Nullable*/ VarInfo leaderCache = null;
129 /**
130 * Return the canonical VarInfo of this. Note that the leader never
131 * changes.
132 * @return the canonical VarInfo of this
133 **/
134 public VarInfo leader() {
135 if (leaderCache == null) {
136 leaderCache = vars.iterator().next();
137 }
138 return leaderCache;
139 }
140
141 public boolean hasNonCanonicalVariable() {
142 throw new Error("Illegal operation on Equality invariant");
143 }
144
145 /**
146 * Always return JUSTIFIED because we aggregate Comparison
147 * invariants that are all justified to the confidence_limit
148 * threshold.
149 **/
150 public double computeConfidence() {
151 return Invariant.CONFIDENCE_JUSTIFIED;
152 }
153
154
155 ////////////////////////
156 // Functions called during actual checking
157
158 private void flow(Invariant flowed) {
159 throw new UnsupportedOperationException("Equality invariants don't flow");
160 }
161
162 ////////////////////////
163 // Printing
164
165 public String repr() {
166 return "Equality: size=" + size()
167 + " leader: " + leader().name() + " with "
168 + format_daikon() + " samples: " + numSamples();
169 }
170
171 public String format_using(OutputFormat format) {
172
173
174 if (format.isJavaFamily()) return format_java_family(format);
175
176 if (format == OutputFormat.DAIKON) return format_daikon();
177 if (format == OutputFormat.ESCJAVA) return format_esc();
178 // Commented out by MDE 7/27/2003. I can't figure out whether
179 // to just change JAVA_IDENTIFIER to IDENTIFIER, or whether other
180 // changes are also necessary.
181 // if (format == OutputFormat.JAVA_IDENTIFIER) return format_java();
182 if (format == OutputFormat.SIMPLIFY) return format_simplify();
183 return format_unimplemented(format);
184 }
185
186 public String format_daikon() {
187 StringBuffer result = new StringBuffer();
188 boolean start = true;
189 for (VarInfo var : vars) {
190 if (!start) {
191 result.append(" == ");
192 } else {
193 start = false;
194 }
195 result.append(var.name());
196 result.append ("[" + var.varinfo_index + "]");
197 // result.append("[" + var.comparability + "]");
198 if (var == leader())
199 result.append ("L");
200 }
201 return result.toString();
202 }
203
204
205 // These format methods aren't called, because for output, we
206 // convert to normal two-way IntEqual type invariants. However,
207 // they can be called if desired.
208 public String format_java() {
209 VarInfo leader = leader();
210 String leaderName = leader.name();
211 List<String> clauses = new ArrayList<String>();
212 for (VarInfo var : vars) {
213 if (leader == var) continue;
214 clauses.add(String.format("(%s == %s)", leaderName, var.name()));
215 }
216 return UtilMDE.join(clauses, " && ");
217 }
218
219
220 public String format_esc() {
221 String result = "";
222
223 List<VarInfo> valid_equiv = new ArrayList<VarInfo>();
224 List<VarInfo> invalid_equiv = new ArrayList<VarInfo>();
225
226 List<VarInfo> equal_vars = new Vector<VarInfo>();
227
228 for (VarInfo other : vars) {
229 if (other.isDerivedSequenceMinMaxSum()) {
230 break;
231 }
232 if (other.isValidEscExpression()) {
233 valid_equiv.add(other);
234 } else {
235 invalid_equiv.add(other);
236 }
237 }
238 // Choose a leader, preferring the valid variables.
239 VarInfo leader;
240 if (valid_equiv.size() > 0) {
241 leader = valid_equiv.get(0);
242 } else {
243 assert invalid_equiv.size() > 0;
244 leader = invalid_equiv.get(0);
245 }
246 // Print the equality statements, stating expressible ones first.
247 equal_vars.clear();
248 equal_vars.addAll(valid_equiv);
249 equal_vars.addAll(invalid_equiv);
250 int numprinted = 0;
251 for (int j=0; j<equal_vars.size(); j++) {
252 VarInfo other = equal_vars.get(j);
253 if (other == leader) continue;
254 if (leader.prestate_name().equals(other.name())) continue;
255 if (other.prestate_name().equals(leader.name())) continue;
256 if (numprinted > 0) {
257 result += Global.lineSep;
258 }
259 numprinted++;
260 if (j >= valid_equiv.size()) {
261 result = result + "warning: method Equality.format_esc() needs to be implemented: " + format();
262 }
263 if (leader.rep_type.isArray()) {
264 String[] form = VarInfo.esc_quantify (leader, other);
265 result = result + form[0] + "( " + form[1] + " == " + form[2] + " )" + form[3];
266 } else {
267 result = result + leader.esc_name() + " == " + other.esc_name();
268 }
269
270 }
271 return result;
272
273 }
274
275 // When A and B are pointers, don't say (EQ A B); instead say (EQ
276 // (hash A) (hash B)). If we said the former, Simplify would
277 // presume that A and B were always interchangeable, which is not
278 // the case when your programming language involves mutation.
279 private String format_elt(String simname) {
280 String result = simname;
281 if (leader().is_reference()) {
282 result = "(hash " + result + ")";
283 }
284 return result;
285 }
286
287 public String format_simplify() {
288 StringBuffer result = new StringBuffer("(AND");
289 VarInfo leader = leader();
290 String leaderName = leader.simplify_name();
291 if (leader.rep_type.isArray()) {
292 for (VarInfo var : vars) {
293 if (var == leader) continue;
294 String[] form = VarInfo.simplify_quantify (QuantFlags.element_wise(),
295 leader, var);
296 String a = format_elt(form[1]);
297 String b = format_elt(form[2]);
298 result.append(" " + form[0] + "(EQ " + a + " " + b + ")" + form[3]);
299 }
300 } else {
301 for (VarInfo var : vars) {
302 if (var == leader) continue;
303 String a = format_elt(leaderName);
304 String b = format_elt(var.simplify_name());
305 result.append(" (EQ ");
306 result.append(a);
307 result.append(" ");
308 result.append(b);
309 result.append(")");
310 }
311 }
312 result.append(")");
313 return result.toString();
314 }
315
316 public String shortString() {
317 return format_daikon();
318 }
319
320 public String format_java_family(OutputFormat format) {
321 VarInfo leader = leader();
322 String leaderName = leader.name_using(format);
323 List<String> clauses = new ArrayList<String>();
324 for (VarInfo var : vars) {
325 if (leader == var) continue;
326 if (leader.rep_type.isArray()) {
327 clauses.add(String.format("(daikon.Quant.pairwiseEqual(%s, %s)",
328 leaderName,
329 var.name_using(format)));
330 } else {
331 if (leader.type.isFloat()) {
332 clauses.add("(" + Invariant.formatFuzzy("eq", leader, var, format) + ")");
333 } else {
334 if ((leaderName.indexOf("daikon.Quant.collectObject") != -1)
335 ||
336 (var.name_using(format).indexOf("daikon.Quant.collectObject") != -1)) {
337 clauses.add("(warning: it is meaningless to compare hashcodes for values "
338 + "obtained through daikon.Quant.collect... methods.");
339 } else {
340 clauses.add(String.format("(%s == %s)",
341 leaderName,
342 var.name_using(format)));
343 }
344 }
345 }
346 }
347 return UtilMDE.join(clauses, " && ");
348 }
349
350 public String toString() {
351 return repr();
352 }
353
354 //////////////////////////////////////////////////////////////////////
355 /// Processing of data
356
357 /**
358 * @return a List of VarInfos that do not fit into this set anymore
359 *
360 * Originally (8/14/2003), this did not check for the modified bits.
361 * It seems however, quite wrong to leave variables in the same equality
362 * set when one is missing and the other is not. Its possible we should
363 * go farther and break out of the equality set any variable that is
364 * missingOutOfBounds (JHP)
365 **/
366 public List<VarInfo> add(ValueTuple vt, int count) {
367 // Need to handle specially if leader is missing.
368 VarInfo leader = leader();
369 Object leaderValue = leader.getValueOrNull(vt);
370 int leaderMod = leader.getModified(vt);
371 boolean leaderOutOfBounds = leader.missingOutOfBounds();
372 if (leader.isMissing(vt)) {
373 } else {
374 numSamples += count;
375 }
376
377 List<VarInfo> result = new LinkedList<VarInfo>();
378 if (debug.isLoggable(Level.FINE)) {
379 debug.fine ("Doing add at " + this.ppt.parent.name() + " for " + this);
380 }
381 for (Iterator<VarInfo> i = vars.iterator(); i.hasNext(); ) {
382 VarInfo vi = i.next();
383 if (vi == leader)
384 continue;
385 assert vi.comparableNWay (leader);
386 Object viValue = vi.getValueOrNull(vt);
387 int viMod = vi.getModified(vt);
388 // The following is possible because values are interned. The
389 // test also takes into account missing values, since they are
390 // null.
391 if ((leaderValue == viValue) && (leaderMod == viMod)
392 && !leaderOutOfBounds && !vi.missingOutOfBounds()
393 // If the values are NaN, treat them as different.
394 && (!((leaderValue instanceof Double) && ((Double)leaderValue).isNaN()))) {
395 // The values are the same.
396 continue;
397 }
398 // The values differ. Remove this from the equality set.
399
400 // if (debug.isLoggable(Level.FINE)) {
401 // debug.fine (" vi name: " + vi.name.name());
402 // debug.fine (" vi value: " + viValue);
403 // debug.fine (" le value: " + leaderValue);
404 // }
405 if (Debug.logOn())
406 Debug.log (getClass(), ppt.parent, Debug.vis (vi),
407 "Var " + vi.name()
408 + " [" + viValue + "," + viMod + "] split from leader "
409 + leader.name() + " [" + leaderValue + ","
410 + leaderMod + "]");
411
412 result.add (vi);
413 i.remove();
414 }
415
416 return result;
417 }
418
419 // This method isn't going to be called, but it's declared abstract in Invariant.
420 protected Invariant resurrect_done(int[] permutation) {
421 throw new UnsupportedOperationException();
422 }
423
424 // This method isn't going to be called, but it's declared abstract in Invariant.
425 public boolean isSameFormula( Invariant other ) {
426 throw new UnsupportedOperationException( "Equality.isSameFormula(): this method should not be called" );
427 }
428
429 /**
430 * Convert Equality invariants into normal IntEqual type for
431 * filtering, printing, etc. Add these to parent.
432 *
433 * If the leader was changed to not be the first member of the group
434 * adds leader == leader invariant as well since that invariant is
435 * used in suppressions and obvious tests.
436 **/
437 public void postProcess () {
438 if (this.numSamples() == 0) return; // All were missing or not present
439 PptTopLevel parent = this.ppt.parent;
440 VarInfo[] varArray = this.vars.toArray(new VarInfo[0]);
441 if (debugPostProcess.isLoggable(Level.FINE)) {
442 debugPostProcess.fine ("Doing postProcess: " + this.format_daikon());
443 debugPostProcess.fine (" at: " + this.ppt.parent.name());
444 }
445 VarInfo leader = leader();
446
447 if (debugPostProcess.isLoggable(Level.FINE)) {
448 debugPostProcess.fine (" var1: " + leader.name());
449 }
450 for (int i = 0; i < varArray.length; i++) {
451 if (varArray[i] == leader) continue;
452 if (debugPostProcess.isLoggable(Level.FINE)) {
453 debugPostProcess.fine (" var2: " + varArray[i].name());
454 }
455
456 parent.create_equality_inv (leader, varArray[i], numSamples());
457 }
458 }
459
460 /**
461 * Switch the leader of this invariant, if possible, to a more canonical
462 * VarInfo: a VarInfo that is not isDerived() is better than one that is;
463 * one that is not isDerivedParamAndUninteresting() is better than one that
464 * is; and other things being equal, choose the least complex name.
465 * Call this only after postProcess has been called.
466 * We do a pivot so that anything that's interesting to be printed
467 * gets printed and not filtered out. For example, if a == b and a
468 * is the leader, but not interesting, we still want to print f(b)
469 * as an invariant. Thus we pivot b to be the leader. Later on,
470 * each relevant PptSlice gets pivoted. But not here.
471 **/
472 public void pivot() {
473 VarInfo newLeader = null;
474 for (VarInfo var : vars) {
475 // System.out.printf (" processing %s\n", var);
476 if (newLeader == null) {
477 newLeader = var;
478 }
479 else if (newLeader.isDerivedParamAndUninteresting() &&
480 !var.isDerivedParamAndUninteresting()) {
481 // System.out.printf ("%s derived and uninteresting, %s is leader%n",
482 // newLeader, var);
483 newLeader = var;
484 }
485 else if (var.isDerivedParamAndUninteresting() &&
486 !newLeader.isDerivedParamAndUninteresting()) {
487 // do nothing
488 }
489 else if (var.derivedDepth() < newLeader.derivedDepth()) {
490 // System.out.printf ("%s greater depth, %s is leader%n",
491 // newLeader, var);
492 newLeader = var;
493 }
494 else if (var.derivedDepth() > newLeader.derivedDepth()) {
495 // do nothing
496 }
497 // if we got here, this is the "all other things being equal" case
498 else if (var.complexity() < newLeader.complexity()) {
499 // System.out.printf ("%s greater comlexity, %s is leader%n",
500 // newLeader, var);
501 newLeader = var;
502 }
503 }
504 // System.out.printf ("%s complexity = %d, %s complexity = %d\n", leaderCache,
505 // leaderCache.complexity(), newLeader,
506 // newLeader.complexity());
507 leaderCache = newLeader;
508 }
509
510 public void repCheck() {
511 super.repCheck();
512 VarInfo leader = leader();
513 for (VarInfo var : vars) {
514 assert VarComparability.comparable (leader, var)
515 : "not comparable: " + leader.name() + " "
516 + var.name() + " at ppt " + ppt.parent.name();
517 }
518 }
519
520 }