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}