Source code

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