001package daikon.inv.filter;
002
003import daikon.PrintInvariants;
004import daikon.VarInfo;
005import daikon.inv.Invariant;
006
007/**
008 * Filter for not printing an Invariant if its VarInfos return isDerivedParameterAndUninteresting ==
009 * true.
010 */
011public class DerivedParameterFilter extends InvariantFilter {
012  @Override
013  public String getDescription() {
014    return "Suppress parameter-derived postcondition invariants";
015  }
016
017  /** Boolean. If true, DerivedParameterFilter is initially turned on. */
018  public static boolean dkconfig_enabled = true;
019
020  public DerivedParameterFilter() {
021    isOn = dkconfig_enabled;
022  }
023
024  /**
025   * Returns true if the invariant describes changes made to pass-by-value parameters that shouldn't
026   * be part of a routine's visible interface. E.g, suppose that "param" is a parameter to a Java
027   * method. If "param" itself is modified, that change won't be visible to a caller, so we
028   * shouldn't print it. If "param" points to an object, and that object is changed, that is
029   * visible, but only if "param" hasn't changed; otherwise, we're reporting a change in some object
030   * other than the one that was passed in.
031   *
032   * <p>More specifically, return true if the invariant is a post-state invariant, and a variable in
033   * it is either a parameter, or a variable derived from a parameter, when we think that the
034   * parameter itself may have changed by virtue of not having a "param == orig(param)" invariant.
035   */
036  @Override
037  boolean shouldDiscardInvariant(Invariant inv) {
038    if (inv.ppt.parent.ppt_name.isExitPoint()) {
039      PrintInvariants.debugFiltering.fine("\tconsidering DPF for vars " + inv.ppt.varNames());
040      for (int i = 0; i < inv.ppt.var_infos.length; i++) {
041        VarInfo vi = inv.ppt.var_infos[i];
042        // ppt has to be a PptSlice, not a PptTopLevel
043        PrintInvariants.debugFiltering.fine("\tconsidering DPF for " + vi.name());
044        if (vi.isDerivedParamAndUninteresting()) {
045          // System.out.printf("derived and uninteresting: %s%n", vi.name());
046          return true;
047        }
048      }
049    }
050    return false;
051  }
052}