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