001package daikon; 002 003import static daikon.tools.nullness.NullnessUtil.castNonNullDeep; 004 005import daikon.inv.Equality; 006import daikon.inv.Invariant; 007import java.util.ArrayList; 008import java.util.Arrays; 009import java.util.Collections; 010import java.util.Comparator; 011import java.util.HashMap; 012import java.util.Iterator; 013import java.util.LinkedHashMap; 014import java.util.List; 015import java.util.Map; 016import java.util.Set; 017import java.util.logging.Level; 018import java.util.logging.Logger; 019import org.checkerframework.checker.initialization.qual.UnknownInitialization; 020import org.checkerframework.checker.lock.qual.GuardSatisfied; 021import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf; 022import org.checkerframework.checker.nullness.qual.KeyFor; 023import org.checkerframework.checker.nullness.qual.Nullable; 024import org.checkerframework.dataflow.qual.Pure; 025import org.checkerframework.dataflow.qual.SideEffectFree; 026 027/** Holds Equality invariants. */ 028public class PptSliceEquality extends PptSlice { 029 static final long serialVersionUID = 20021231L; 030 031 // Variables starting with dkconfig_ should only be set via the 032 // daikon.config.Configuration interface. 033 034 /** 035 * If true, create one equality set for each variable. This has the effect of turning the equality 036 * optimization off, without actually removing the sets themselves (which are presumed to exist in 037 * many parts of the code). 038 */ 039 public static boolean dkconfig_set_per_var = false; 040 041 public static final Logger debug = Logger.getLogger("daikon.PptSliceEquality"); 042 043 public static final Logger debugGlobal = Logger.getLogger("daikon.PptSliceEquality.Global"); 044 045 PptSliceEquality(PptTopLevel parent) { 046 super(parent, parent.var_infos); 047 } 048 049 @Override 050 public final int arity(@UnknownInitialization(PptSlice.class) PptSliceEquality this) { 051 throw new Error("Don't call arity on PptSliceEquality"); 052 } 053 054 void init_po() { 055 throw new Error("Shouldn't get called"); 056 } 057 058 @Override 059 public void addInvariant(Invariant inv) { 060 assert inv instanceof Equality; 061 invs.add(inv); 062 } 063 064 // Not valid for this type of slice. Always pretend there are enough. 065 @Override 066 public int num_samples(@UnknownInitialization @GuardSatisfied PptSliceEquality this) { 067 if (true) { 068 throw new Error(); 069 } 070 return Integer.MAX_VALUE; 071 } 072 073 public int num_mod_samples() { 074 if (true) { 075 throw new Error(); 076 } 077 return Integer.MAX_VALUE; 078 } 079 080 @Override 081 public int num_values() { 082 if (true) { 083 throw new Error(); 084 } 085 return Integer.MAX_VALUE; 086 } 087 088 /** 089 * Encapsulates a VarInfo and its Comparability so that the two can be used to create sets of 090 * VarInfos that are initially equal. Two VarInfoAndComparability's are true iff they are 091 * VarComparability.comparable() to each other. 092 */ 093 private static class VarInfoAndComparability { 094 public VarInfo vi; 095 096 @Pure 097 @Override 098 public int hashCode(@GuardSatisfied VarInfoAndComparability this) { 099 // This is very coarse but is about as good as we can do it. Can't do hashcode of 100 // the comparability because two comparabilities may be 101 // comparable and yet be not the same. 102 // (e.g. VarComparabilityExplicit). 103 return vi.file_rep_type.hashCode(); 104 } 105 106 @EnsuresNonNullIf(result = true, expression = "#1") 107 @Pure 108 @Override 109 public boolean equals( 110 @GuardSatisfied VarInfoAndComparability this, @GuardSatisfied @Nullable Object o) { 111 if (!(o instanceof VarInfoAndComparability)) { 112 return false; 113 } 114 return equalsVarInfoAndComparability((VarInfoAndComparability) o); 115 } 116 117 /** 118 * Whether two VarInfos can be set to be equal to each other is whether they are comparableNWay. 119 * Since we do not yet handle inheritance, we require that the comparability go both ways. 120 */ 121 @EnsuresNonNullIf(result = true, expression = "#1") 122 @Pure 123 public boolean equalsVarInfoAndComparability( 124 @GuardSatisfied VarInfoAndComparability this, @GuardSatisfied VarInfoAndComparability o) { 125 126 return (vi.comparableNWay(o.vi) 127 && vi.comparability.equality_set_ok(o.vi.comparability) 128 && vi.aux.equals_for_instantiation(o.vi.aux)); 129 } 130 131 public VarInfoAndComparability(VarInfo vi) { 132 this.vi = vi; 133 } 134 } 135 136 /** Actually instantiate the equality sets. */ 137 @Override 138 void instantiate_invariants() { 139 140 // If each variable gets its own set, create those sets and return 141 if (dkconfig_set_per_var) { 142 // Debug.debugTrack.fine ("Vars for " + parent.name()); 143 for (VarInfo vi : var_infos) { 144 List<VarInfo> vi_list = Collections.singletonList(vi); 145 Equality eq = new Equality(vi_list, this); 146 invs.add(eq); 147 // System.out.println (" eq set = " + eq.shortString()); 148 } 149 return; 150 } 151 152 // Start with everything comparable being equal. 153 if (debug.isLoggable(Level.FINE)) { 154 debug.fine("PptSliceEquality.instantiate_invariants: " + parent.name() + " vars:"); 155 } 156 LinkedHashMap<VarInfoAndComparability, List<VarInfo>> multiMap = new LinkedHashMap<>(); 157 for (VarInfo vi : var_infos) { 158 VarInfoAndComparability viac = new VarInfoAndComparability(vi); 159 addToBindingList(multiMap, viac, vi); 160 if (debug.isLoggable(Level.FINE)) { 161 debug.fine(" " + vi.name() + ": " + vi.comparability); 162 } 163 } 164 if (debug.isLoggable(Level.FINE)) { 165 debug.fine( 166 "PptSliceEquality.instantiate_invariants " 167 + parent.name() 168 + ": " 169 + Integer.toString(multiMap.keySet().size()) 170 + " VarInfoAndComparability keys"); 171 } 172 Equality[] newInvs = new Equality[multiMap.keySet().size()]; 173 int varCount = 0; 174 int invCount = 0; 175 for (List<VarInfo> list : multiMap.values()) { 176 varCount += list.size(); 177 178 Equality eq = new Equality(list, this); 179 newInvs[invCount] = eq; 180 if (debug.isLoggable(Level.FINE)) { 181 debug.fine(" Created: " + eq); 182 for (VarInfo vi : list) { 183 debug.fine(" vi: " + vi + " aux : " + vi.aux); 184 } 185 } 186 if (Debug.logOn()) { 187 Debug.log(getClass(), parent, Debug.vis(eq.leader()), "Created"); 188 } 189 invCount++; 190 } 191 // Ensure determinism 192 Arrays.sort(newInvs, EqualityComparator.theInstance); 193 invs.addAll(Arrays.<Invariant>asList(newInvs)); 194 assert varCount == var_infos.length; // Check that we get all vis 195 } 196 197 /** 198 * Instantiate the full equality sets from a set of variable pairs where each member of a pair is 199 * equal to the other. 200 */ 201 public void instantiate_from_pairs(Set<VarInfo.Pair> eset) { 202 203 // Build a map from each variable to all those that are equal to it 204 Map<VarInfo, List<VarInfo>> varmap = new LinkedHashMap<>(); 205 Map<VarInfo, Integer> sample_cnt_map = new LinkedHashMap<>(); 206 for (VarInfo.Pair cp : eset) { 207 List<VarInfo> vlist = varmap.get(cp.v1); 208 if (vlist == null) { 209 vlist = new ArrayList<VarInfo>(); 210 vlist.add(cp.v1); 211 varmap.put(cp.v1, vlist); 212 sample_cnt_map.put(cp.v1, cp.samples); 213 } 214 vlist.add(cp.v2); 215 vlist = varmap.get(cp.v2); 216 if (vlist == null) { 217 vlist = new ArrayList<VarInfo>(); 218 vlist.add(cp.v2); 219 varmap.put(cp.v2, vlist); 220 sample_cnt_map.put(cp.v2, cp.samples); 221 } 222 vlist.add(cp.v1); 223 } 224 225 // Loop through each variable, building the appropriate equality set 226 // for each. Note that variables that are distinct still have an 227 // equality set (albeit with only the one variable) 228 ArrayList<Invariant> newInvs = new ArrayList<>(); 229 for (VarInfo v : var_infos) { 230 if (v.equalitySet != null) { 231 continue; 232 } 233 List<VarInfo> vlist = varmap.computeIfAbsent(v, Collections::singletonList); 234 Equality eq = new Equality(vlist, this); 235 Integer sample_cnt = sample_cnt_map.get(v); 236 if (sample_cnt != null) { 237 eq.setSamples(sample_cnt.intValue()); 238 } 239 v.equalitySet = eq; 240 newInvs.add(eq); 241 } 242 invs.addAll(newInvs); 243 } 244 245 /** 246 * Returns a List of Invariants that have been weakened/destroyed. However, this handles the 247 * creation of new Equality invariants and the instantiation of other invariants. 248 * 249 * @return a List of invariants that have been weakened 250 */ 251 // The basic approach is as follows: 252 // - Loop through each equality set 253 // - look for any variables that are no longer equal 254 // - Create new equality sets (call createEqualityInvs) 255 // - Get the new leaders 256 // - Create new slices and invariants (call CopyInvsFromLeader) 257 // 258 @Override 259 public List<Invariant> add(ValueTuple vt, int count) { 260 261 ArrayList<Equality> allNewInvs = new ArrayList<>(); 262 ArrayList<Invariant> weakenedInvs = new ArrayList<>(); 263 264 // Loop through each existing equality invariant 265 for (Invariant invar : invs) { 266 Equality inv = (Equality) invar; 267 268 // Add this sample to the invariant and track any vars that fall 269 // out of the set. 270 List<VarInfo> nonEqualVis = inv.add(vt, count); 271 272 // If some vars fell out 273 if (nonEqualVis.size() > 0) { 274 275 // Create new equality sets for all of the non-equal vars 276 List<Equality> newInvs = createEqualityInvs(nonEqualVis, vt, inv, count); 277 278 // Get a list of all of the new non-missing leaders 279 List<VarInfo> newInvsLeaders = new ArrayList<>(newInvs.size()); 280 for (Equality eq : newInvs) { 281 if ((parent.constants == null) || !parent.constants.is_missing(eq.leader())) { 282 newInvsLeaders.add(eq.leader()); 283 } 284 } 285 286 // Debug print the new leaders 287 if (Debug.logOn()) { 288 for (VarInfo nileader : newInvsLeaders) { 289 Debug.log( 290 getClass(), 291 parent, 292 Debug.vis(nileader), 293 "Split off from previous leader " 294 + inv.leader().name() 295 + ": new set = " 296 + nileader.equalitySet 297 + ": old set = " 298 + inv); 299 } 300 } 301 302 // Create new slices and invariants for each new leader 303 weakenedInvs.addAll(copyInvsFromLeader(inv.leader(), newInvsLeaders)); 304 305 // Keep track of all of the new invariants created. 306 allNewInvs.addAll(newInvs); 307 } 308 } 309 310 // Add all of the new equality sets to our list 311 invs.addAll(allNewInvs); 312 313 return weakenedInvs; 314 } 315 316 /** 317 * Dummy value that's incomparable to everything else to indicate missings in createEqualityInvs. 318 */ 319 private static final Object dummyMissing = new Object(); 320 321 /** 322 * Create a List of Equality invariants based on the values given by vt for the VarInfos in vis. 323 * Any variables that are out of bounds are forced into a separate equality set (since they no 324 * longer make sense and certainly shouldn't be equal to anything else) 325 * 326 * <p>Requires: vis.size() > 0 327 * 328 * <p>Ensures: result.size() > 0 329 * 330 * @param vis the VarInfos that were different from leader 331 * @param vt the ValueTuple associated with the VarInfos now 332 * @param leader the original leader of VarInfos 333 * @param count the number of samples seen (needed to set the number of samples for the new 334 * Equality invariants) 335 * @return a List of Equality invariants bundling together same values from vis, and if needed, 336 * another representing all the missing values 337 */ 338 private List<Equality> createEqualityInvs( 339 List<VarInfo> vis, ValueTuple vt, Equality leader, int count) { 340 assert vis.size() > 0; 341 HashMap<Object, List<VarInfo>> multiMap = new HashMap<>(); /* key is a value */ 342 List<VarInfo> out_of_bounds = new ArrayList<>(); 343 for (VarInfo vi : vis) { 344 if (vi.missingOutOfBounds()) { 345 out_of_bounds.add(vi); 346 } else if (vt.isMissing(vi)) { 347 addToBindingList(multiMap, dummyMissing, vi); 348 } else { 349 if (vi.getValue(vt) == null) { 350 System.out.printf( 351 "null value for variable %s, mod=%d at ppt %s%n", 352 vi.name(), vt.getModified(vi), parent.name()); 353 VarInfo rv = parent.find_var_by_name("return"); 354 assert rv != null : "@AssumeAssertion(nullness)"; 355 System.out.println("return value = " + Debug.toString(rv.getValue(vt))); 356 System.out.println("At line number " + FileIO.get_linenum()); 357 } 358 addToBindingList(multiMap, vi.getValue(vt), vi); 359 } 360 } 361 // Why use an array? Because we'll be sorting shortly 362 /*NNC:@MonotonicNonNull*/ Equality[] resultArray = 363 new Equality[multiMap.values().size() + out_of_bounds.size()]; 364 int resultCount = 0; 365 for (Map.Entry<@KeyFor("multiMap") Object, List<VarInfo>> entry : multiMap.entrySet()) { 366 Object key = entry.getKey(); 367 List<VarInfo> list = entry.getValue(); 368 assert list.size() > 0; 369 Equality eq = new Equality(list, this); 370 @SuppressWarnings("interning") // special value 371 boolean isMissing = (key == dummyMissing); 372 if (isMissing) { 373 eq.setSamples(leader.numSamples() - count); 374 } else { 375 eq.setSamples(leader.numSamples()); 376 } 377 if (debug.isLoggable(Level.FINE)) { 378 debug.fine(" created new inv: " + eq + " samples: " + eq.numSamples()); 379 } 380 resultArray[resultCount] = eq; 381 resultCount++; 382 } 383 for (VarInfo oob : out_of_bounds) { 384 List<VarInfo> list = Collections.singletonList(oob); 385 resultArray[resultCount] = new Equality(list, this); 386 resultCount++; 387 } 388 resultArray = castNonNullDeep(resultArray); // https://tinyurl.com/cfissue/986 389 390 // Sort for determinism 391 Arrays.sort(resultArray, EqualityComparator.theInstance); 392 List<Equality> result = Arrays.<Equality>asList(resultArray); 393 assert result.size() > 0; 394 return result; 395 } 396 397 /** 398 * Create a List of Equality invariants based on the VarInfos in vis. Assumes that the VarInfos in 399 * vis are not missing. The method is used exclusively for reversing optimizations in Daikon. 400 * 401 * <p>Requires: vis.size() > 0 402 * 403 * <p>Ensures: result.size() > 0 404 * 405 * @param vis the VarInfos that were different from leader 406 * @param leader the original leader of VarInfos 407 * @return a List of Equality invariants bundling together same values from vis 408 */ 409 public List<Equality> createEqualityInvs(List<VarInfo> vis, Equality leader) { 410 assert vis.size() > 0; 411 412 // Why use an array? Because we'll be sorting shortly 413 /*NNC:@MonotonicNonNull*/ Equality[] resultArray = new Equality[vis.size()]; 414 for (int i = 0; i < vis.size(); i++) { 415 VarInfo vi = vis.get(i); 416 List<VarInfo> list = new ArrayList<>(); 417 list.add(vi); 418 Equality eq = new Equality(list, this); 419 eq.setSamples(leader.numSamples()); 420 resultArray[i] = eq; 421 } 422 resultArray = castNonNullDeep(resultArray); // https://tinyurl.com/cfissue/986 423 424 // Sort for determinism 425 Arrays.sort(resultArray, PptSliceEquality.EqualityComparator.theInstance); 426 List<Equality> result = Arrays.<Equality>asList(resultArray); 427 assert result.size() > 0; 428 return result; 429 } 430 431 /** 432 * Map maps keys to non-empty lists of elements. This method adds var to the list mapped by key, 433 * creating a new list for key if one doesn't already exist. 434 * 435 * <p>Requires: Each value in map is a list of size 1 or greater 436 * 437 * <p>Ensures: Each value in map is a list of size 1 or greater 438 * 439 * @param map the map to add the bindings to 440 * @param key if there is already a List associated with key, then add value to key. Otherwise 441 * create a new List associated with key and insert value. 442 * @param value the value to insert into the List mapped to key 443 */ 444 private <T> void addToBindingList(Map<T, List<VarInfo>> map, T key, VarInfo value) { 445 if (key == null) { 446 throw new IllegalArgumentException(); 447 } 448 List<VarInfo> elements = map.computeIfAbsent(key, __ -> new ArrayList<VarInfo>()); 449 elements.add(value); 450 } 451 452 /** 453 * Instantiate invariants from each inv's leader. This is like instantiate_invariants at the start 454 * of reading the trace file, where we create new PptSliceNs. This is called when newVis have just 455 * split off from leader, and we want the leaders of newVis to have the same invariants as leader. 456 * 457 * <p>post: Adds the newly instantiated invariants and slices to this.parent. 458 * 459 * @param leader the old leader 460 * @param newVis a List of new VarInfos that used to be equal to leader. Actually, it's the list 461 * of canonical that were equal to leader, representing their own newly-created equality sets. 462 */ 463 public List<Invariant> copyInvsFromLeader(VarInfo leader, List<VarInfo> newVis) { 464 465 List<Invariant> falsified_invs = new ArrayList<>(); 466 List<PptSlice> newSlices = new ArrayList<>(); 467 if (debug.isLoggable(Level.FINE)) { 468 debug.fine( 469 "copyInvsFromLeader: " 470 + parent.name() 471 + ": leader " 472 + leader.name() 473 + ": new leaders = " 474 + newVis); 475 debug.fine(" orig slices count:" + parent.numViews()); 476 } 477 478 // Copy all possible combinations from the current ppt (with repetition) 479 // of replacing leader with different members of newVis. 480 481 // Loop through each slice. 482 // Uses old-style for loop and Iterator because it will be side-effected. 483 for (Iterator<PptSlice> i = parent.views_iterator(); i.hasNext(); ) { 484 PptSlice slice = i.next(); 485 486 if (debug.isLoggable(Level.FINE)) { 487 debug.fine(" Slice is: " + slice.toString()); 488 debug.fine(" With invs: " + slice.invs); 489 } 490 491 // If this slice contains the old leader 492 if (slice.containsVar(leader)) { 493 494 // Substitute new leader for old leader and create new slices/invs 495 VarInfo[] toFill = new VarInfo[slice.var_infos.length]; 496 copyInvsFromLeaderHelper(leader, newVis, slice, newSlices, 0, -1, toFill); 497 498 // Remove any statically obvious invariants in the old slice. 499 // This is called here because breaking up the equality set may 500 // cause some invariants to become statically obvious (because 501 // they will now be the only item in their set) 502 for (Invariant inv : slice.invs) { 503 if (!Daikon.dkconfig_undo_opts) { 504 if (inv.isObviousStatically_AllInEquality()) { 505 inv.falsify(); 506 falsified_invs.add(inv); 507 } 508 } 509 } 510 if (slice.invs.size() == 0) { 511 i.remove(); 512 } 513 } 514 } 515 516 // Add each new slice with invariants 517 for (PptSlice slice : newSlices) { 518 if (slice.invs.size() == 0) { 519 continue; 520 } 521 assert (parent.findSlice(slice.var_infos) == null) : parent.findSlice(slice.var_infos); 522 slice.repCheck(); 523 parent.addSlice(slice); 524 } 525 526 parent.repCheck(); 527 528 if (debug.isLoggable(Level.FINE)) { 529 debug.fine(" new slices count:" + parent.numViews()); 530 } 531 return falsified_invs; 532 } 533 534 /** 535 * Clones slice (zero or more times) such that instances of leader are replaced by members of 536 * newVis; places new slices in newSlices. The replacement is such that we get all combinations, 537 * with repetition of newVis and leader in every slot in slice where there used to be leader. For 538 * example, if slice contained (A1, A1, B) and A1 is leader and newVis contains A2 and A3, then 539 * the slices we produce would be: (A1, A2, B), (A1, A3, B), (A2, A2, B) (A2, A3, B), (A3, A3, B). 540 * We do not produce (A1, A1, B) because it is already there. We do not produce (A2, A1, B) 541 * because it is the same as (A1, A2, B) wrt combinations. This method does the main work of 542 * copyInvsFromLeader so that each new equality set that spawned off leader has the correct 543 * slices. It works as a nested series of for loops, whose depth is equal to the length of 544 * slice.var_infos. The position and loop arguments along with the call stack keep track of the 545 * loop nesting. When position reaches the end of slice.var_infos, this method attempts to 546 * instantiate the slice that has been produced. The standard start for position is 0, and for 547 * loop is -1. 548 * 549 * @param leader the variable to replace in slice 550 * @param newVis of VarInfos that will replace leader in combination in slice 551 * @param slice the slice to clone 552 * @param newSlices where to put the cloned slices 553 * @param position the position currently being replaced in source. Starts at 0. 554 * @param loop the iteration of the loop for this position. If -1, means the previous replacement 555 * is leader. 556 * @param soFar buffer to which assignments temporarily go before becoming instantiated. Has to 557 * equal slice.var_infos in length. 558 */ 559 private void copyInvsFromLeaderHelper( 560 VarInfo leader, 561 List<VarInfo> newVis, 562 PptSlice slice, 563 List<PptSlice> newSlices, 564 int position, 565 int loop, 566 VarInfo[] soFar) { 567 568 // Track debug if any variables are in newVis 569 Debug dlog = null; 570 if (Debug.logOn()) { 571 dlog = new Debug(getClass(), parent, newVis); 572 } 573 574 if (position >= slice.var_infos.length) { 575 // Done with assigning positions and recursion 576 if (parent.findSlice_unordered(soFar) == null) { 577 // If slice is already there, no need to clone. 578 579 if (parent.is_slice_ok(soFar, slice.arity())) { 580 PptSlice newSlice = slice.cloneAndPivot(soFar); 581 // Debug.debugTrack.fine ("LeaderHelper: Created Slice " + newSlice); 582 if (Debug.logOn()) { 583 assert dlog != null : "@AssumeAssertion(nullness): dependent: set if Debug.logOn()"; 584 dlog.log( 585 "Created slice " + newSlice + " Leader equality set = " + soFar[0].equalitySet); 586 Debug.log(getClass(), newSlice, "Created this slice"); 587 } 588 List<Invariant> invs = newSlice.invs; 589 for (Iterator<Invariant> iInvs = invs.iterator(); iInvs.hasNext(); ) { 590 Invariant inv = iInvs.next(); 591 if (!Daikon.dkconfig_undo_opts) { 592 if (inv.isObviousStatically_AllInEquality()) { 593 iInvs.remove(); 594 } 595 } 596 } 597 if (newSlice.invs.size() == 0) { 598 Debug.log(debug, getClass(), newSlice, soFar, "slice not added because 0 invs"); 599 } else { 600 newSlices.add(newSlice); 601 } 602 } 603 } else { 604 if (Debug.logOn()) { 605 assert dlog != null : "@AssumeAssertion(nullness): dependent: set if Debug.logOn()"; 606 dlog.log("Slice already existed " + parent.findSlice_unordered(soFar)); 607 } 608 } 609 return; 610 } else { 611 // Not yet done with recursion, keep assigning to soFar 612 if (slice.var_infos[position] == leader) { 613 // If leader does need replacing 614 // newLoop starts at loop so that we don't have repeats 615 for (int newLoop = loop; newLoop < newVis.size(); newLoop++) { 616 VarInfo vi = newLoop == -1 ? leader : newVis.get(newLoop); 617 soFar[position] = vi; 618 // Advance position to next step, let next loop variable be 619 // this loop's counter. 620 copyInvsFromLeaderHelper(leader, newVis, slice, newSlices, position + 1, newLoop, soFar); 621 } 622 } else { 623 // Non leader position, just keep going after assigning soFar 624 soFar[position] = slice.var_infos[position]; 625 copyInvsFromLeaderHelper(leader, newVis, slice, newSlices, position + 1, loop, soFar); 626 } 627 } 628 } 629 630 @Override 631 public void repCheck() { 632 for (Invariant inv : invs) { 633 inv.repCheck(); 634 assert inv.ppt == this; 635 } 636 } 637 638 @SideEffectFree 639 @Override 640 public String toString(@GuardSatisfied PptSliceEquality this) { 641 StringBuilder result = new StringBuilder("PptSliceEquality: ["); 642 for (Invariant inv : invs) { 643 result.append(inv.repr()); 644 result.append(lineSep); 645 } 646 result.append(" ]"); 647 return result.toString(); 648 } 649 650 /** Order Equality invariants by the indices of leaders. */ 651 public static final class EqualityComparator implements Comparator<Equality> { 652 public static final EqualityComparator theInstance = new EqualityComparator(); 653 654 private EqualityComparator() {} 655 656 @Pure 657 @Override 658 public int compare(Equality eq1, Equality eq2) { 659 return VarInfo.IndexComparator.theInstance.compare(eq1.leader(), eq2.leader()); 660 } 661 } 662 663 /** Returns an array of all of the leaders sorted by varinfo_index for this equality view. */ 664 public VarInfo[] get_leaders_sorted() { 665 List<VarInfo> leaders = new ArrayList<>(invs.size()); 666 for (Invariant inv : invs) { 667 VarInfo leader = ((Equality) inv).leader(); 668 assert leader != null; 669 leaders.add(leader); 670 } 671 Collections.sort(leaders, VarInfo.IndexComparator.getInstance()); 672 return leaders.toArray(new VarInfo[0]); 673 } 674}