001 package daikon.suppress;
002
003 import daikon.*;
004 import daikon.inv.*;
005 import daikon.inv.unary.*;
006 import daikon.inv.binary.*;
007 import static daikon.inv.Invariant.asInvClass;
008
009 import plume.*;
010
011 import java.lang.reflect.*;
012 import java.util.logging.*;
013 import java.util.*;
014
015 /**
016 * Class that defines a suppressor invariant for use in non-instantiating
017 * suppressions. In non-instantiating suppressions, suppressor invariants
018 * are defined independent of specific variables. Instead, arguments
019 * are identified by their variable index in the suppressee.
020 */
021 public class NISuppressor {
022
023 /** Debug tracer. **/
024 public static final Logger debug
025 = Logger.getLogger ("daikon.inv.NISuppressor");
026
027
028 /**
029 * Argument indices used by the invariant.
030 */
031 int v1_index = -1;
032 int v2_index = -1;
033 int v3_index = -1;
034
035 /** Invariant class. **/
036 Class<? extends Invariant> inv_class;
037
038 /** True if the order of the variables was swapped. **/
039 boolean swap = false;
040
041 /** True if invariant permutes by changing its class. **/
042 boolean swap_class = false;
043
044 /**
045 * State of the suppressor for the current check. The state must be
046 * one of the defined above. They can always be compared with ==.
047 **/
048 String state = NIS.NONE;
049
050 /**
051 * information about the suppressor for the current check. This is just
052 * used for debugging purposes
053 */
054 /*@Nullable*/ String current_state_str = null;
055
056 /**
057 * Sample invariant - used to check the suppressor over constants.
058 * this is a prototype invariant; that is, sample_inv.ppt == null.
059 **/
060 /*@Prototype*/ Invariant sample_inv;
061
062 /**
063 * Defines a unary suppressor.
064 */
065 public NISuppressor (int v1_index, Class<? extends Invariant> cls) {
066
067 debug.fine (String.format ("creating %s over arg %d", cls.getName(),
068 v1_index));
069
070 this.v1_index = v1_index;
071 this.inv_class = cls;
072
073 // Create a sample invariant
074 try {
075 Method get_proto = inv_class.getMethod ("get_proto",
076 new Class<?>[] {});
077 @SuppressWarnings("prototype")
078 /*@Prototype*/ Invariant sample_inv_local = (/*@Prototype*/ Invariant) get_proto.invoke (null, new Object[] {});
079 sample_inv = sample_inv_local;
080 assert sample_inv != null;
081 } catch (Exception e) {
082 throw new RuntimeException ("error instantiating invariant "
083 + inv_class.getName() + ": " + e);
084 }
085
086 debug.fine ("Created " + this);
087 }
088
089 /**
090 * Defines a binary suppressor.
091 */
092 public NISuppressor (int v1_index, int v2_index, Class<? extends Invariant> cls) {
093
094 debug.fine (String.format ("creating %s over args %d and %d", cls.getName(),
095 v1_index, v2_index));
096
097 // put the variables in their standard order
098 if (v1_index > v2_index) {
099 this.v1_index = v2_index;
100 this.v2_index = v1_index;
101 swap = true;
102 } else {
103 this.v1_index = v1_index;
104 this.v2_index = v2_index;
105 swap = false;
106 }
107
108 // If the specified class handles swapping with a different class,
109 // get the class
110 swap_class = true;
111 try {
112 Method swap_method = cls.getMethod ("swap_class", (Class<?>[])null);
113 if (swap)
114 cls = asInvClass(swap_method.invoke (null, (Object /*@Nullable*/ []) null));
115 } catch (Exception e) {
116 swap_class = false;
117 }
118
119 this.inv_class = cls;
120
121 // Create a sample invariant, by reflectively calling either
122 // get_proto(boolean) or get_proto().
123 try {
124 try {
125 Method get_proto = inv_class.getMethod ("get_proto",
126 new Class<?>[] {boolean.class});
127 @SuppressWarnings("prototype")
128 /*@Prototype*/ Invariant sample_inv_local = (/*@Prototype*/ Invariant)get_proto.invoke (null,
129 new Object[] {Boolean.valueOf(swap)});
130 sample_inv = sample_inv_local;
131 } catch (NoSuchMethodException e) {
132 Method get_proto = inv_class.getMethod ("get_proto",
133 new Class<?>[] {});
134 @SuppressWarnings("prototype")
135 /*@Prototype*/ Invariant sample_inv_local = (/*@Prototype*/ Invariant)get_proto.invoke (null, new Object[] {});
136 sample_inv = sample_inv_local;
137 }
138 } catch (Exception e) {
139 throw new RuntimeException ("error getting proto invariant "
140 + inv_class.getName() + ": " + e);
141 }
142
143 assert sample_inv != null;
144 debug.fine ("Created " + this);
145 }
146
147 /**
148 * Returns a new suppressor that is the same as this one except
149 * with its variables swapped. Unary suppressors have their variable
150 * index swapped from 0 to 1 or 1 to 0.
151 */
152 public NISuppressor swap() {
153
154 if (v2_index == -1) {
155 int new_index = 0;
156 if (v1_index == 0)
157 new_index = 1;
158 return (new NISuppressor (new_index, inv_class));
159 }
160 assert v3_index == -1;
161
162 if (swap)
163 return new NISuppressor (v1_index, v2_index, inv_class);
164 else
165 return new NISuppressor (v2_index, v1_index, inv_class);
166 }
167
168 /**
169 * Returns whether or not this suppressor is enabled. A suppressor
170 * is enabled if the invariant on which it depends is enabled.
171 */
172 public boolean is_enabled() {
173 return (sample_inv.enabled());
174 }
175
176 /**
177 * Returns whether or not this suppressor invariant could be instantiated
178 * over the specified variables. A suppressor that canot be instantiated
179 * over the variables cannot possibly suppress. Consider the NonZero
180 * invariant. It is suppressed by EqualsOne. But while NonZero is
181 * valid over all variables, EqualsOne is only valid over non-pointer
182 * variables. Thus the suppression is only valid over non-pointer variables.
183 */
184 public boolean instantiate_ok(VarInfo[] vis) {
185 return sample_inv.instantiate_ok (vis);
186 }
187
188 /**
189 * Sets the status of this suppressor with regards to the specified
190 * vis and falsified invariant. The status consists of whether or
191 * not the suppressor is valid (true) and whether or not it matches
192 * the falsified invariant.
193 *
194 * Matching a suppressor is more complex than is apparent at first
195 * glance. The invariant AND its variables must match. Since
196 * suppressors are specified without variables, the variables are
197 * taken from the specified vis. The variable indices specify which
198 * variables to consider.
199 *
200 * For example consider the suppressor {1, 2, IntLessEqual} and a
201 * vis of {x, y, z}. The suppressor is true if the IntLessEqual
202 * invariant exists in the slice {y, z}. This allows ternary
203 * invariants to specify exactly the suppressor required for their
204 * particular permutation ofarguments. Invariants that have an
205 * internal permute variable must match that as well.
206 *
207 * @param ppt The top level program point
208 * @param vis The slice of the suppressee. Thus, if the suppressee is
209 * ternary, vis, should specify three variables.
210 * @param inv The falsified invariant. inv_match indicates whether
211 * or not inv matches this suppressor
212 *
213 * @return the state of this suppressor which is one of (NIS.MATCH,
214 * NIS.VALID, NIS.INVALID, NIS.NONSENSICAL)
215 */
216
217 public String check (PptTopLevel ppt, VarInfo[] vis, /*@Nullable*/ Invariant inv) {
218
219 // Currently we only support unary and binary suppressors
220 assert v3_index == -1;
221 assert v1_index != -1;
222
223 // If the underlying invariant is not enabled, we can't possibly be true
224 if (!is_enabled())
225 return (state = NIS.INVALID);
226
227 if (Debug.logDetail() && NIS.debug.isLoggable (Level.FINE))
228 NIS.debug.fine ("checking suppressor " + this + " against inv "
229 + ((inv != null) ? inv.format() : "null") + " over vars "
230 + VarInfo.arrayToString(vis) + " in ppt " + ppt.name);
231
232 // If unary
233 if (v2_index == -1) {
234
235 VarInfo v1 = vis[v1_index];
236
237 // If the underlying inariant can't be instantiated over these variables,
238 // this can't possibly be true
239 if (!instantiate_ok(new VarInfo[] {v1})) {
240 // System.out.printf ("suppressor %s invalid over variable %s\n",
241 // this, v1);
242 return (state = NIS.INVALID);
243 }
244
245 // Check to see if inv matches this suppressor. The invariant class
246 // and variables must match for this to be true. This check is only
247 // needed for the falsified method.
248 if (!NIS.antecedent_method) {
249 if ((inv != null) &&
250 (inv.getClass() == inv_class) && (v1 == inv.ppt.var_infos[0])) {
251 return (state = NIS.MATCH);
252 }
253 }
254
255 // Check to see if the suppressor is true over all constants.
256 if (ppt.is_prev_constant (v1)) {
257 assert ppt.constants != null : "@SuppressWarnings(nullness)";
258 boolean valid = false;
259 VarInfo[] sup_vis = new VarInfo[] {v1};
260 assert sample_inv.valid_types (sup_vis);
261 if (sample_inv.instantiate_ok(sup_vis)) {
262 UnaryInvariant uinv = (UnaryInvariant) sample_inv;
263 @SuppressWarnings("nullness") // elements of ppt.constants have a constant_value
264 InvariantStatus status = uinv.check
265 (ppt.constants.constant_value(v1), ValueTuple.MODIFIED, 1);
266 valid = (status == InvariantStatus.NO_CHANGE);
267 }
268 if (NIS.debug.isLoggable(Level.FINE))
269 NIS.debug.fine("constant args - " + valid);
270 if (valid)
271 current_state_str = "true over constant " + ppt.constants.constant_value(v1);
272 else
273 current_state_str = "invalid over constant " + ppt.constants.constant_value(v1);
274 return (state = (valid ? NIS.VALID : NIS.INVALID));
275 }
276
277 // Check to see the variable is missing
278 if (ppt.is_prev_missing(v1)) {
279 current_state_str = "nonsensical";
280 return (state = NIS.NONSENSICAL);
281 }
282
283 // Check to see if this suppressor is true. Note that we don't check
284 // to see if the invariant has been falsified. That is because we
285 // do this processing as falsified invariants are removed from the lists.
286 // An invariant that is still in the list, but marked falsified, is true
287 // for our purposes (we will process it later, when it is removed)
288 PptSlice slice = ppt.findSlice (v1);
289 if (slice != null) {
290 for (Invariant slice_inv : slice.invs) {
291 if (match_true (slice_inv)) {
292 current_state_str = "invariant " + slice_inv.format();
293 return (state = NIS.VALID);
294 }
295 }
296 }
297 current_state_str = "invariant not found";
298 return (state = NIS.INVALID);
299
300 } else /* must be binary */ {
301 if (v1_index >= vis.length || v2_index >= vis.length) {
302 // Stringifying "this" is expensive, so only do it if one of the
303 // assertions will fail
304 assert (v1_index < vis.length)
305 : "v1/len= "
306 + v1_index + "/" + vis.length +
307 " suppressor " + this;
308 assert (v2_index < vis.length)
309 : "v2/len= "
310 + v2_index + "/" + vis.length +
311 " suppressor " + this;
312 }
313 VarInfo v1 = vis[v1_index];
314 VarInfo v2 = vis[v2_index];
315
316 // If the underlying inariant can't be instantiated over these variables,
317 // this can't possibly be true
318 if (!instantiate_ok(new VarInfo[] {v1, v2})) {
319 // System.out.printf ("suppressor %s invalid over variables %s & %s\n",
320 // this, v1, v2);
321 return (state = NIS.INVALID);
322 }
323
324 // Check to see if inv matches this suppressor. The invariant class,
325 // variables, and swap must match for this to be true. This check is
326 // only needed in the falsified method.
327 if (!NIS.antecedent_method) {
328 if ((inv != null) && match(inv) && (v1 == inv.ppt.var_infos[0])
329 && (v2 == inv.ppt.var_infos[1])) {
330 if (NIS.debug.isLoggable(Level.FINE))
331 NIS.debug.fine("Matches falsified inv " + inv.format());
332 return (state = NIS.MATCH);
333 }
334 }
335
336 // Check to see if the suppressor is true over all constants. This
337 // code only works for stateless invariants!
338 if (ppt.is_prev_constant (v1) && ppt.is_prev_constant (v2)) {
339 assert ppt.constants != null : "@SuppressWarnings(nullness)";
340 boolean valid = false;
341 VarInfo[] sup_vis = new VarInfo[] {v1, v2};
342 assert sample_inv.valid_types (sup_vis);
343 if (sample_inv.instantiate_ok(sup_vis)) {
344 BinaryInvariant binv = (BinaryInvariant) sample_inv;
345 InvariantStatus status
346 = binv.check_unordered (ppt.constants.constant_value(v1),
347 ppt.constants.constant_value(v2),
348 ValueTuple.MODIFIED, 1);
349 valid = (status == InvariantStatus.NO_CHANGE);
350 }
351 if (NIS.debug.isLoggable (Level.FINE))
352 NIS.debug.fine (String.format ("constant args (%s, %s) = %b ",
353 Debug.toString (ppt.constants.constant_value(v1)),
354 Debug.toString (ppt.constants.constant_value(v2)),
355 valid));
356 current_state_str = "true over constants " + ppt.constants.constant_value(v1)
357 + " and " + ppt.constants.constant_value(v2);
358 if (!valid)
359 current_state_str = "not " + current_state_str;
360 return (state = (valid ? NIS.VALID : NIS.INVALID));
361 }
362
363 // Check to see if either variable is missing
364 if (ppt.is_prev_missing(v1) || ppt.is_prev_missing(v2)) {
365 current_state_str = "nonsensical";
366 return (state = NIS.NONSENSICAL);
367 }
368
369 // Check to see if this suppressor is true. Note that we don't check
370 // to see if the invariant has been falsified. That is because we
371 // do this processing as falsified invariants are removed from the lists.
372 // An invariant that is still in the list, but marked falsified, is true
373 // for our purposes (we will process it later, when it is removed)
374 PptSlice slice = ppt.findSlice (v1, v2);
375 if (slice != null) {
376 for (Invariant slice_inv : slice.invs) {
377 // NIS.debug.fine (": processing inv " + slice_inv.format());
378 if (match_true (slice_inv)) {
379 if (NIS.debug.isLoggable (Level.FINE))
380 NIS.debug.fine ("suppressor matches inv " + slice_inv.format()
381 + " " + !slice_inv.is_false());
382 current_state_str = "invariant " + slice_inv.format();
383 return (state = NIS.VALID);
384 }
385 }
386 }
387 NIS.debug.fine ("suppressor not found");
388 return (state = NIS.INVALID);
389 }
390 }
391
392 /**
393 * Returns true if inv matches this suppressor and the invariant
394 * is not falsified.
395 * @see #match(Invariant)
396 */
397 public boolean match_true (Invariant inv) {
398 if (NIS.antecedent_method)
399 return (match (inv) && !inv.is_false());
400 else
401 return (match (inv));
402 }
403
404 /**
405 * Returns true if inv matches this suppressor. It is assumed that
406 * inv's variables already match (i.e., that it was looked up in
407 * compatible slice
408 */
409 public boolean match (Invariant inv) {
410
411 if (v2_index == -1)
412 return (inv.getClass() == inv_class);
413 else {
414 if (inv.getClass() != inv_class)
415 return (false);
416 if (!swap_class) {
417 BinaryInvariant binv = (BinaryInvariant) inv;
418 return (binv.is_symmetric() || (swap == binv.get_swap()));
419 }
420 return (true);
421 }
422 }
423
424 /**
425 * Returns true if the suppressee matches this suppressor. Currently
426 * only checks that the class matches but this will need to be expanded
427 * to check for a permutation match as well
428 */
429 public boolean match (NISuppressee sse) {
430
431 if (v2_index == -1)
432 return (sse.sup_class == inv_class);
433 else {
434 if (sse.sup_class != inv_class) {
435 return (false);
436 }
437 if (!swap_class) {
438 BinaryInvariant binv = (BinaryInvariant) sse.sample_inv;
439 boolean match = (binv.is_symmetric() || (swap == binv.get_swap()));
440 return (match);
441 }
442 return (true);
443 }
444
445 }
446
447 /**
448 * Returns a copy of this suppressor translated to match the variable
449 * order in sor.
450 */
451 public NISuppressor translate (NISuppressor sor) {
452
453 int new_v1 = sor.translate_index (v1_index);
454 int new_v2 = sor.translate_index (v2_index);
455 int new_v3 = sor.translate_index (v3_index);
456
457 if (new_v2 == -1)
458 return new NISuppressor (new_v1, inv_class);
459 else if (new_v3 == -1)
460 return new NISuppressor (new_v1, new_v2, inv_class);
461 else {
462 throw new Error("Unexpected ternary suppressor");
463 }
464 }
465
466 /** Returns the variable index that corresponds to index **/
467 private int translate_index (int index) {
468
469 if (index == 0)
470 return (v1_index);
471 else if (index == 1)
472 return (v2_index);
473 else if (index == 2)
474 return (v3_index);
475 else
476 return (index);
477 }
478
479
480 /** Returns the invariant class of this suppressor **/
481 public Class<? extends Invariant> get_inv_class() {
482 return (inv_class);
483 }
484
485 /** clears the state of this suppressor to NIS.none **/
486 public void clear_state() {
487 state = NIS.NONE;
488 current_state_str = null;
489 }
490
491 static String[] varname = new String[] { "x", "y", "z" };
492
493 /**
494 * Returns a string representation of the suppressor. Rather than show
495 * var indices as numbers, the variables x, y, and z are shown instead
496 * with indices 0, 1, and 2 respectively
497 */
498 public String toString() {
499
500 String cname = inv_class.getCanonicalName();
501
502 String status = state;
503 if (status == NIS.NONE)
504 status = "";
505
506 if (current_state_str != null)
507 status = status + " [" + current_state_str + "]";
508
509 if (v2_index == -1)
510 return (String.format ("%s(%s) [%s]", cname, varname[v1_index], status));
511 else if (v3_index == -1) {
512 if (swap && !swap_class)
513 return (String.format ("%s(%s,%s) [%s]", cname, varname[v2_index],
514 varname[v1_index], status));
515 else
516 return (String.format ("%s(%s,%s) [%s]", cname, varname[v1_index],
517 varname[v2_index], status));
518 } else
519 return (String.format ("%s(%s,%s,%s) [%s]", cname, varname[v1_index],
520 varname[v2_index], varname[v3_index], status));
521 }
522
523 }