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