001package daikon.suppress; 002 003import static daikon.tools.nullness.NullnessUtil.castNonNullDeep; 004 005import daikon.Debug; 006import daikon.PptSlice; 007import daikon.PptTopLevel; 008import daikon.VarInfo; 009import daikon.inv.Invariant; 010import java.util.ArrayList; 011import java.util.Arrays; 012import java.util.Iterator; 013import java.util.LinkedHashSet; 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.lock.qual.GuardSatisfied; 020import org.checkerframework.dataflow.qual.Pure; 021import org.checkerframework.dataflow.qual.SideEffectFree; 022import org.plumelib.util.StringsPlume; 023 024/** 025 * Class that defines a set of non-instantiating suppressions for a single invariant (suppressee). 026 * 027 * <p>Not immutable: see recurse_definitions(). 028 */ 029public class NISuppressionSet implements Iterable<NISuppression> { 030 031 public static final Logger debug = Logger.getLogger("daikon.suppress.NISuppressionSet"); 032 033 NISuppression[] suppression_set; 034 035 public NISuppressionSet(NISuppression[] suppressions) { 036 assert suppressions != null; 037 assert suppressions.length != 0; 038 suppression_set = suppressions; 039 } 040 041 @Override 042 public Iterator<NISuppression> iterator() { 043 List<NISuppression> asList = Arrays.<NISuppression>asList(suppression_set); 044 return asList.iterator(); 045 } 046 047 /** 048 * Adds this set to the suppressor map. The map is from the class of the suppressor to this. If 049 * the same suppressor class appears more than once, the suppression is only added once. 050 */ 051 public void add_to_suppressor_map( 052 Map<Class<? extends Invariant>, List<NISuppressionSet>> suppressor_map) { 053 054 Set<Class<? extends Invariant>> all_suppressors = 055 new LinkedHashSet<Class<? extends Invariant>>(); 056 057 // Loop through each suppression in the suppression set 058 for (int i = 0; i < suppression_set.length; i++) { 059 NISuppression suppression = suppression_set[i]; 060 061 // Loop through each suppressor in the suppression 062 for (Iterator<NISuppressor> j = suppression.suppressor_iterator(); j.hasNext(); ) { 063 NISuppressor suppressor = j.next(); 064 065 // If we have seen this suppressor already, skip it 066 if (all_suppressors.contains(suppressor.get_inv_class())) { 067 continue; 068 } 069 070 // Note that we have now seen this suppressor invariant class 071 all_suppressors.add(suppressor.get_inv_class()); 072 073 // Get the list of suppression sets for this suppressor. Create it 074 // if this is the first one. Add this set to the list 075 List<NISuppressionSet> suppression_set_list = 076 suppressor_map.computeIfAbsent( 077 suppressor.get_inv_class(), __ -> new ArrayList<NISuppressionSet>()); 078 suppression_set_list.add(this); 079 } 080 } 081 } 082 083 /** 084 * NIS process a falsified invariant. This method should be called for each falsified invariant in 085 * turn. Any invariants for which inv is the last valid suppressor are added to new_invs. 086 * 087 * <p>Note, this is no longer the preferred approach, but is kept for informational purposes. Use 088 * NIS.process_falsified_invs() instead. 089 */ 090 public void falsified(Invariant inv, List<Invariant> new_invs) { 091 092 // Get the ppt we are working in 093 PptTopLevel ppt = inv.ppt.parent; 094 assert ppt.equality_view != null 095 : "@AssumeAssertion(nullness): haven't reasoned through the reason"; 096 097 // For now all suppressors are unary/binary and 098 // all suppressees are unary, binary or ternary 099 assert inv.ppt.var_infos.length < 3; 100 101 // check unary, binary and ternary suppressees separately 102 103 // unary suppressee 104 if (suppression_set[0].suppressee.var_count == 1) { 105 // Create all of the valid unary slices that use the vars from inv 106 // and check to see if the invariant should be created for each slice 107 if (inv.ppt.var_infos.length == 1) { 108 VarInfo v1 = inv.ppt.var_infos[0]; 109 VarInfo[] vis = new VarInfo[] {v1}; 110 111 // Make sure the slice is interesting and has valid types over the 112 // suppressee invariant 113 if (!v1.missingOutOfBounds() && ppt.is_slice_ok(v1)) { 114 if (suppression_set[0].suppressee.sample_inv.valid_types(vis)) { 115 check_falsified(ppt, vis, inv, new_invs); 116 } 117 } 118 } 119 return; 120 } 121 122 // binary suppressee 123 if (suppression_set[0].suppressee.var_count == 2) { 124 // Create all of the valid binary slices that use the vars from inv 125 // and check to see if the invariant should be created for each slice 126 if (inv.ppt.var_infos.length == 2) { 127 VarInfo v1 = inv.ppt.var_infos[0]; 128 VarInfo v2 = inv.ppt.var_infos[1]; 129 VarInfo[] vis = new VarInfo[] {v1, v2}; 130 131 // Make sure the slice is interesting and has valid types over the 132 // suppressee invariant 133 if (!v1.missingOutOfBounds() && !v2.missingOutOfBounds() && ppt.is_slice_ok(v1, v2)) { 134 if (suppression_set[0].suppressee.sample_inv.valid_types(vis)) { 135 check_falsified(ppt, vis, inv, new_invs); 136 } 137 } 138 139 } else /* must be unary */ { 140 VarInfo v1 = inv.ppt.var_infos[0]; 141 VarInfo[] leaders = ppt.equality_view.get_leaders_sorted(); 142 for (int i = 0; i < leaders.length; i++) { 143 VarInfo l1 = leaders[i]; 144 145 // hashcode types are not involved in suppressions 146 if (NIS.dkconfig_skip_hashcode_type) { 147 if (l1.file_rep_type.isHashcode()) { 148 continue; 149 } 150 } 151 152 // Make sure the slice is interesting 153 if (v1.missingOutOfBounds() || l1.missingOutOfBounds()) { 154 continue; 155 } 156 if (!ppt.is_slice_ok(v1, l1)) { 157 continue; 158 } 159 160 VarInfo[] vis; 161 162 // Sort the variables 163 if (v1.varinfo_index <= l1.varinfo_index) { 164 vis = new VarInfo[] {v1, l1}; 165 } else { 166 vis = new VarInfo[] {l1, v1}; 167 } 168 169 if (!suppression_set[0].suppressee.sample_inv.valid_types(vis)) { 170 continue; 171 } 172 173 if (NIS.debug.isLoggable(Level.FINE)) { 174 NIS.debug.fine( 175 "processing slice " 176 + Arrays.toString(vis) 177 + " in ppt " 178 + ppt.name() 179 + " with " 180 + ppt.numViews()); 181 } 182 183 check_falsified(ppt, vis, inv, new_invs); 184 } 185 } 186 return; 187 } 188 189 // ternary suppressee 190 if (suppression_set[0].suppressee.var_count == 3) { 191 // Create all of the valid ternary slices that use the vars from inv 192 // and check to see if the invariant should be created for each slice 193 if (inv.ppt.var_infos.length == 2) { 194 VarInfo v1 = inv.ppt.var_infos[0]; 195 VarInfo v2 = inv.ppt.var_infos[1]; 196 VarInfo[] leaders = ppt.equality_view.get_leaders_sorted(); 197 for (int i = 0; i < leaders.length; i++) { 198 VarInfo l = leaders[i]; 199 200 if (NIS.dkconfig_skip_hashcode_type) { 201 if (l.file_rep_type.isHashcode()) { 202 continue; 203 } 204 } 205 206 if (!ppt.is_slice_ok(l, v1, v2)) { 207 continue; 208 } 209 if (l.missingOutOfBounds() || v1.missingOutOfBounds() || v2.missingOutOfBounds()) { 210 continue; 211 } 212 213 VarInfo[] vis; 214 215 // Order the variables, 216 if (l.varinfo_index <= v1.varinfo_index) { 217 vis = new VarInfo[] {l, v1, v2}; 218 } else if (l.varinfo_index <= v2.varinfo_index) { 219 vis = new VarInfo[] {v1, l, v2}; 220 } else { 221 vis = new VarInfo[] {v1, v2, l}; 222 } 223 224 if (!suppression_set[0].suppressee.sample_inv.valid_types(vis)) { 225 continue; 226 } 227 228 if (NIS.debug.isLoggable(Level.FINE)) { 229 NIS.debug.fine( 230 "processing slice " 231 + Arrays.toString(vis) 232 + " in ppt " 233 + ppt.name() 234 + " with " 235 + ppt.numViews()); 236 } 237 238 check_falsified(ppt, vis, inv, new_invs); 239 } 240 } else /* must be unary */ { 241 VarInfo v1 = inv.ppt.var_infos[0]; 242 VarInfo[] leaders = ppt.equality_view.get_leaders_sorted(); 243 for (int i = 0; i < leaders.length; i++) { 244 VarInfo l1 = leaders[i]; 245 246 if (NIS.dkconfig_skip_hashcode_type) { 247 if (l1.file_rep_type.isHashcode()) { 248 continue; 249 } 250 } 251 252 for (int j = i; j < leaders.length; j++) { 253 VarInfo l2 = leaders[j]; 254 255 if (NIS.dkconfig_skip_hashcode_type) { 256 if (l2.file_rep_type.isHashcode()) { 257 continue; 258 } 259 } 260 261 // Make sure the slice is interesting 262 if (v1.missingOutOfBounds() || l1.missingOutOfBounds() || l2.missingOutOfBounds()) { 263 continue; 264 } 265 if (!ppt.is_slice_ok(v1, l1, l2)) { 266 continue; 267 } 268 269 VarInfo[] vis; 270 271 // Sort the variables 272 if (v1.varinfo_index <= l1.varinfo_index) { 273 vis = new VarInfo[] {v1, l1, l2}; 274 } else if (v1.varinfo_index <= l2.varinfo_index) { 275 vis = new VarInfo[] {l1, v1, l2}; 276 } else { 277 vis = new VarInfo[] {l1, l2, v1}; 278 } 279 280 if (!suppression_set[0].suppressee.sample_inv.valid_types(vis)) { 281 continue; 282 } 283 284 if (NIS.debug.isLoggable(Level.FINE)) { 285 NIS.debug.fine( 286 "processing slice " 287 + Arrays.toString(vis) 288 + " in ppt " 289 + ppt.name() 290 + " with " 291 + ppt.numViews()); 292 } 293 294 check_falsified(ppt, vis, inv, new_invs); 295 } 296 } 297 } 298 return; 299 } 300 } 301 302 /** 303 * Checks the falsified invariant against the slice specified by vis. If the falsification of inv 304 * removed the last valid suppression, then instantiates the suppressee. 305 */ 306 private void check_falsified( 307 PptTopLevel ppt, VarInfo[] vis, Invariant inv, List<Invariant> new_invs) { 308 309 // process each suppression in the set, marking each suppressor as 310 // to whether it is true, false, or matches the falsified inv 311 // If any particular suppression is still valid, just return as there 312 // is nothing to be done (the suppressee is still suppressed) 313 314 for (int i = 0; i < suppression_set.length; i++) { 315 316 NIS.SuppressState status = suppression_set[i].check(ppt, vis, inv); 317 if (status == NIS.SuppressState.VALID) { 318 if (NIS.debug.isLoggable(Level.FINE)) { 319 NIS.debug.fine("suppression " + suppression_set[i] + " is valid"); 320 } 321 return; 322 } 323 assert status != NIS.SuppressState.NONSENSICAL; 324 } 325 326 if (NIS.debug.isLoggable(Level.FINE)) { 327 NIS.debug.fine("After check, suppression set: " + this); 328 } 329 330 // There are no remaining valid (true) suppressions. If inv is the 331 // first suppressor to be removed from any suppressions, then this 332 // falsification removed the last valid suppression. In that case we 333 // need to instantiate the suppressee. 334 for (int i = 0; i < suppression_set.length; i++) { 335 if (suppression_set[i].invalidated()) { 336 337 Invariant v = suppression_set[i].suppressee.instantiate(vis, ppt); 338 if (v != null) { 339 new_invs.add(v); 340 } 341 return; 342 } 343 } 344 } 345 346 /** 347 * Determines whether or not the suppression set is valid in the specified slice. The suppression 348 * set is valid if any of its suppressions are valid. A suppression is valid if all of its 349 * suppressors are true. 350 * 351 * <p>Also updates the debug information in each suppressor. 352 * 353 * @see #is_instantiate_ok(PptSlice) for a check that considers missing 354 */ 355 public boolean suppressed(PptSlice slice) { 356 357 return suppressed(slice.parent, slice.var_infos); 358 } 359 360 /** 361 * Determines whether or not the suppression set is valid in the specified ppt and var_infos. The 362 * suppression set is valid if any of its suppressions are valid. A suppression is valid if all of 363 * its suppressors are true. 364 * 365 * <p>Also updates the debug information in each suppressor. 366 * 367 * @see #is_instantiate_ok(PptTopLevel,VarInfo[]) for a check that considers missing 368 */ 369 public boolean suppressed(PptTopLevel ppt, VarInfo[] var_infos) { 370 371 // Check each suppression to see if it is valid 372 for (int i = 0; i < suppression_set.length; i++) { 373 NIS.SuppressState status = suppression_set[i].check(ppt, var_infos, null); 374 if (status == NIS.SuppressState.VALID) { 375 if (Debug.logOn() || NIS.debug.isLoggable(Level.FINE)) { 376 Debug.log( 377 NIS.debug, 378 getClass(), 379 ppt, 380 var_infos, 381 "suppression " 382 + suppression_set[i] 383 + " is " 384 + status 385 + " in ppt " 386 + ppt 387 + " with var infos " 388 + Arrays.toString(var_infos)); 389 } 390 return true; 391 } 392 } 393 394 if (Debug.logOn() || NIS.debug.isLoggable(Level.FINE)) { 395 Debug.log( 396 NIS.debug, 397 getClass(), 398 ppt, 399 var_infos, 400 "suppression " 401 + this 402 + " is not valid in ppt " 403 + ppt 404 + " with var infos " 405 + Arrays.toString(var_infos)); 406 } 407 return false; 408 } 409 410 /** 411 * Determines whether or not the suppression set is valid in the specified slice. The suppression 412 * set is valid if any of its suppressions are valid. A suppression is valid if all of its 413 * non-missing suppressors are true. 414 */ 415 @Pure 416 public boolean is_instantiate_ok(PptSlice slice) { 417 418 return is_instantiate_ok(slice.parent, slice.var_infos); 419 } 420 421 /** 422 * Determines whether or not the suppressee of the suppression set should be instantiated. 423 * Instantiation is ok only if each suppression is invalid. A suppression is valid if all of its 424 * non-missing suppressors are true. 425 */ 426 @Pure 427 public boolean is_instantiate_ok(PptTopLevel ppt, VarInfo[] var_infos) { 428 429 // Check each suppression to see if it is valid 430 for (int i = 0; i < suppression_set.length; i++) { 431 NIS.SuppressState status = suppression_set[i].check(ppt, var_infos, null); 432 if ((status == NIS.SuppressState.VALID) || (status == NIS.SuppressState.NONSENSICAL)) { 433 if (Debug.logOn() || NIS.debug.isLoggable(Level.FINE)) { 434 Debug.log( 435 NIS.debug, 436 getClass(), 437 ppt, 438 var_infos, 439 "suppression " 440 + suppression_set[i] 441 + " is " 442 + status 443 + " in ppt " 444 + ppt 445 + " with var infos " 446 + Arrays.toString(var_infos)); 447 } 448 return false; 449 } 450 } 451 452 if (Debug.logOn() || NIS.debug.isLoggable(Level.FINE)) { 453 Debug.log( 454 NIS.debug, 455 getClass(), 456 ppt, 457 var_infos, 458 "suppression " 459 + this 460 + " is not valid in ppt " 461 + ppt 462 + " with var infos " 463 + Arrays.toString(var_infos)); 464 } 465 return true; 466 } 467 468 /** 469 * Side-effects this NISuppressionSet. Each suppression where a suppressor matches the suppressee 470 * in ss is augmented by additional suppression(s) where the suppressor is replaced by each of its 471 * suppressions. This allows recursive suppressions. 472 * 473 * <p>For example, consider the suppressions: 474 * 475 * <pre> 476 * (r == arg1) ∧ (arg2 ≤ arg1) ⇒ r = max(arg1,arg2) 477 * (arg2 == arg1) ⇒ arg2 ≤ arg1 478 * </pre> 479 * 480 * The suppressor (arg2 ≤ arg1) in the first suppression matches the suppressee in the second 481 * suppression. In order for the first suppression to work even when (arg2 ≤ arg1) is 482 * suppressed, the second suppression is added to the first: 483 * 484 * <pre> 485 * (r == arg1) ∧ (arg2 ≤ arg1) ⇒ r = max(arg1,arg2) 486 * (r == arg1) ∧ (arg2 == arg1) ⇒ r = max(arg1,arg2) 487 * </pre> 488 * 489 * When (arg2 ≤ arg1) is suppressed, the second suppression for max will still suppress max. If 490 * (arg2 == arg1) is falsified, the (arg2 ≤ arg1) invariant will be created and can continue to 491 * suppress max (as long as it is not falsified itself). 492 */ 493 public void recurse_definitions(NISuppressionSet ss) { 494 495 // Get all of the new suppressions 496 List<NISuppression> new_suppressions = new ArrayList<>(); 497 for (int i = 0; i < suppression_set.length; i++) { 498 new_suppressions.addAll(suppression_set[i].recurse_definition(ss)); 499 } 500 // This isn't necessarily true if the suppressee is of the same 501 // class but doesn't match due to variable swapping. 502 // assert new_suppressions.size() > 0; 503 504 // Create a new suppression set with all of the suppressions. 505 /*NNC:@MonotonicNonNull*/ NISuppression[] new_array = 506 new NISuppression[suppression_set.length + new_suppressions.size()]; 507 for (int i = 0; i < suppression_set.length; i++) { 508 new_array[i] = suppression_set[i]; 509 } 510 for (int i = 0; i < new_suppressions.size(); i++) { 511 new_array[suppression_set.length + i] = new_suppressions.get(i); 512 } 513 new_array = castNonNullDeep(new_array); // https://tinyurl.com/cfissue/986 514 suppression_set = new_array; 515 } 516 517 /** 518 * Swaps each suppressor and suppressee to the opposite variable order. Valid only on unary and 519 * binary suppressors and suppressees. 520 */ 521 public NISuppressionSet swap() { 522 523 NISuppression[] swap_sups = new NISuppression[suppression_set.length]; 524 for (int i = 0; i < swap_sups.length; i++) { 525 NISuppression std_sup = suppression_set[i]; 526 /*NNC:@MonotonicNonNull*/ NISuppressor[] sors = new NISuppressor[std_sup.suppressors.length]; 527 for (int j = 0; j < sors.length; j++) { 528 sors[j] = std_sup.suppressors[j].swap(); 529 } 530 sors = castNonNullDeep(sors); // https://tinyurl.com/cfissue/986 531 swap_sups[i] = new NISuppression(sors, std_sup.suppressee.swap()); 532 } 533 NISuppressionSet new_ss = new NISuppressionSet(swap_sups); 534 return new_ss; 535 } 536 537 /** Returns the suppressee. */ 538 public NISuppressee get_suppressee() { 539 return suppression_set[0].suppressee; 540 } 541 542 /** Clears the suppressor state in each suppression. */ 543 public void clear_state() { 544 for (int i = 0; i < suppression_set.length; i++) { 545 suppression_set[i].clear_state(); 546 } 547 } 548 549 /** Returns a string containing each suppression separated by commas. */ 550 @SideEffectFree 551 @Override 552 public String toString(@GuardSatisfied NISuppressionSet this) { 553 return "{ " + StringsPlume.join(", ", suppression_set) + " }"; 554 } 555}