001package daikon.inv.filter;
002
003import daikon.PrintInvariants;
004import daikon.ProglangType;
005import daikon.VarInfo;
006import daikon.inv.Invariant;
007import daikon.inv.binary.BinaryInvariant;
008import daikon.inv.binary.twoString.StringEqual;
009import daikon.inv.unary.scalar.NonZero;
010import daikon.inv.unary.scalar.OneOfScalar;
011import daikon.inv.unary.string.OneOfString;
012import java.util.logging.Level;
013
014/**
015 * Suppress string invariants that are redundant for .NET. The following invariants will be
016 * discarded:
017 *
018 * <ul>
019 *   <li>{@code x != null}, if {@code !string.IsNullOrEmpty(...)} or {@code
020 *       !string.IsNullOrWhitespace(...)} is inferred.
021 *   <li>Frame conditions for string properties, if the frame condition exists for the string
022 *       (reference or value)
023 *   <li>String properties, if {@link OneOfString} is inferred.
024 *   <li>{@code !string.IsNullOrEmpty(...)} if {@code !string.IsNullOrWhitespace(...)} is inferred.
025 *   <li>{@code string.IsNullOrWhitespace(...)} if {@code string.IsNullOrEmpty(...)} is inferred.
026 * </ul>
027 */
028public class DotNetStringFilter extends InvariantFilter {
029
030  /** Boolean. If true, DotNetStringFilter is initially turned on. See its Javadoc. */
031  public static boolean dkconfig_enabled = false;
032
033  public DotNetStringFilter() {
034    isOn = dkconfig_enabled;
035  }
036
037  @Override
038  public String getDescription() {
039    return "Suppress string invariants that are redundant for .NET.";
040  }
041
042  boolean isNullOrEmptyVar(VarInfo var) {
043    return var.name().startsWith("string.IsNullOrEmpty")
044        || var.name().startsWith("String.IsNullOrEmpty");
045  }
046
047  boolean isNullOrWhitespaceVar(VarInfo var) {
048    return var.name().startsWith("string.IsNullOrWhiteSpace")
049        || var.name().startsWith("String.IsNullOrWhiteSpace");
050  }
051
052  boolean isFrame(VarInfo lhs, VarInfo rhs) {
053    return lhs.is_prestate_version(rhs) || rhs.is_prestate_version(lhs);
054  }
055
056  boolean isFrame(Invariant invariant) {
057    return invariant instanceof BinaryInvariant
058        && isFrame(invariant.ppt.var_infos[0], invariant.ppt.var_infos[1]);
059  }
060
061  /**
062   * Since strings are immutable, discard all frame conditions for the properties of the string if a
063   * frame condition for the string (reference of value) is inferred.
064   */
065  boolean shouldDiscardDerivedStringFrameCondition(Invariant invariant) {
066    if (isFrame(invariant)
067        && invariant.ppt.var_infos[0].enclosing_var != null
068        && invariant.ppt.var_infos[0].enclosing_var.type == ProglangType.STRING) {
069      VarInfo str = invariant.ppt.var_infos[0].enclosing_var;
070
071      for (Invariant other : str.ppt.getInvariants()) {
072        if (!other.is_false() && isFrame(other)) {
073
074          boolean refEq = other.ppt.var_infos[0] == str;
075          boolean valEq =
076              other instanceof StringEqual && other.ppt.var_infos[0].enclosing_var == str;
077
078          if (refEq || (valEq && !(invariant instanceof StringEqual))) {
079            return true;
080          }
081        }
082      }
083    }
084
085    return false;
086  }
087
088  /**
089   * Since properties are pure, discard all properties of the string if the possible values are
090   * known (a {@link OneOfString} invariant is present).
091   */
092  boolean shouldDiscardDerivedStringInvariant(Invariant invariant) {
093    if (invariant.ppt.var_infos.length == 1 && !(invariant instanceof OneOfString)) {
094      VarInfo var = invariant.ppt.var_infos[0];
095
096      if (var.enclosing_var != null && var.enclosing_var.type == ProglangType.STRING) {
097        // variable is derived from a string
098
099        for (Invariant other : var.ppt.getInvariants()) {
100          if (!other.is_false()
101              && other instanceof OneOfString
102              && ((OneOfString) other).var().enclosing_var == var.enclosing_var) {
103            // search for a variable.ToString() invariant
104
105            return true;
106          }
107        }
108      }
109    }
110
111    return false;
112  }
113
114  /**
115   * Returns {@code true} iff {@code invariant} encodes {@code x != null} and {@code
116   * !string.IsNullOrEmpty(x)} is an inferred invariant
117   *
118   * @param invariant an invariant
119   * @return true iff {@code invariant} encodes {@code x != null} and is implied
120   */
121  boolean shouldDiscardNonNullInvariant(Invariant invariant) {
122    if (invariant instanceof NonZero) {
123
124      NonZero i = (NonZero) invariant;
125      if (i.var().type == ProglangType.STRING) {
126
127        for (Invariant other : i.var().ppt.getInvariants()) {
128          if (!other.is_false() && other instanceof OneOfScalar) {
129            OneOfScalar o = (OneOfScalar) other;
130
131            if (o.var().enclosing_var == i.var()
132                && (isNullOrEmptyVar(o.var()) || isNullOrWhitespaceVar(o.var()))
133                && o.getElts()[0] == 0) {
134
135              return true;
136            }
137          }
138        }
139      }
140    }
141    return false;
142  }
143
144  /**
145   * Returns {@code true} iff {@code invariant} encodes {@code !string.IsNullOrEmpty()} and {@code
146   * !string.IsNullOrWhitespace()} is an inferred invariant.
147   *
148   * @param invariant an invariant
149   * @return true iff {@code invariant} encodes {@code x != null} and is implied
150   */
151  boolean shouldDiscardNullOrEmptyInvariant(Invariant invariant) {
152    if (invariant instanceof OneOfScalar) {
153      OneOfScalar i = (OneOfScalar) invariant;
154
155      if (isNullOrEmptyVar(i.var()) && i.getElts()[0] == 0) {
156        // invariant encodes !string.IsNullOrEmpty()
157
158        for (Invariant other : i.var().ppt.getInvariants()) {
159          if (!other.is_false() && other instanceof OneOfScalar) {
160            OneOfScalar o = (OneOfScalar) other;
161
162            if (o.var().enclosing_var == i.var().enclosing_var
163                && isNullOrWhitespaceVar(o.var())
164                && o.getElts()[0] == 0) {
165
166              return true;
167            }
168          }
169        }
170      }
171    }
172
173    return false;
174  }
175
176  /**
177   * {@code true} iff {@code invariant} encodes {@code string.IsNullOrWhitespace()} and {@code
178   * string.IsNullOrEmpty()} is an inferred invariant.
179   *
180   * @param invariant an invariant
181   * @return true iff {@code invariant} encodes {@code x != null} and is implied
182   */
183  boolean shouldDiscardNullOrWhitespaceInvariant(Invariant invariant) {
184    if (invariant instanceof OneOfScalar) {
185      OneOfScalar i = (OneOfScalar) invariant;
186
187      if (isNullOrWhitespaceVar(i.var()) && i.getElts()[0] == 1) {
188        // invariant encodes !string.IsNullOrEmpty()
189
190        for (Invariant other : i.var().ppt.getInvariants()) {
191          if (!other.is_false() && other instanceof OneOfScalar) {
192            OneOfScalar o = (OneOfScalar) other;
193
194            if (o.var().enclosing_var == i.var().enclosing_var
195                && isNullOrEmptyVar(o.var())
196                && o.getElts()[0] == 1) {
197
198              return true;
199            }
200          }
201        }
202      }
203    }
204
205    return false;
206  }
207
208  @Override
209  boolean shouldDiscardInvariant(Invariant invariant) {
210
211    if (PrintInvariants.debugFiltering.isLoggable(Level.FINE)) {
212      PrintInvariants.debugFiltering.fine("\tEntering DotNetStringFilter.shouldDiscard");
213    }
214
215    return shouldDiscardDerivedStringFrameCondition(invariant)
216        || shouldDiscardNonNullInvariant(invariant)
217        || shouldDiscardDerivedStringInvariant(invariant)
218        || shouldDiscardNullOrEmptyInvariant(invariant)
219        || shouldDiscardNullOrWhitespaceInvariant(invariant);
220  }
221}