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