001// ***** This file is automatically generated from IntComparisons.java.jpp 002 003package daikon.inv.binary.twoString; 004 005import daikon.*; 006import daikon.derive.binary.*; 007import daikon.derive.unary.*; 008import daikon.inv.*; 009import daikon.inv.binary.twoScalar.*; 010import daikon.inv.binary.twoSequence.*; 011import daikon.inv.unary.scalar.*; 012import daikon.inv.unary.sequence.*; 013import daikon.inv.unary.string.*; 014import daikon.suppress.*; 015import java.util.*; 016import java.util.logging.Level; 017import java.util.logging.Logger; 018import org.checkerframework.checker.interning.qual.Interned; 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 org.plumelib.util.Intern; 025import typequals.prototype.qual.NonPrototype; 026import typequals.prototype.qual.Prototype; 027 028/** 029 * Represents an invariant of != between two String scalars. Prints as {@code x != y}. 030 */ 031public final class StringNonEqual extends TwoString { 032 033 static final long serialVersionUID = 20030822L; 034 035 // Variables starting with dkconfig_ should only be set via the 036 // daikon.config.Configuration interface. 037 /** Boolean. True iff StringNonEqual invariants should be considered. */ 038 public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault; 039 040 public static final Logger debug = Logger.getLogger("daikon.inv.binary.twoScalar.StringNonEqual"); 041 042 StringNonEqual(PptSlice ppt) { 043 super(ppt); 044 } 045 046 @Prototype StringNonEqual() { 047 super(); 048 } 049 050 private static @Prototype StringNonEqual proto = new @Prototype StringNonEqual(); 051 052 /** Returns the prototype invariant for StringNonEqual. */ 053 public static @Prototype StringNonEqual get_proto() { 054 return proto; 055 } 056 057 @Override 058 public boolean enabled() { 059 return dkconfig_enabled; 060 } 061 062 /** Returns whether or not the specified var types are valid for StringNonEqual. */ 063 @Override 064 public boolean instantiate_ok(VarInfo[] vis) { 065 066 if (!valid_types(vis)) { 067 return false; 068 } 069 070 boolean result = !(vis[0].has_typeof() ^ vis[1].has_typeof()); 071 return result; 072 } 073 074 @Override 075 protected StringNonEqual instantiate_dyn(@Prototype StringNonEqual this, PptSlice slice) { 076 077 return new StringNonEqual(slice); 078 } 079 080 @Override 081 protected Invariant resurrect_done_swapped() { 082 083 // we don't care if things swap; we have symmetry 084 return this; 085 } 086 087 @Pure 088 @Override 089 public boolean is_symmetric() { 090 return true; 091 } 092 093 // JHP: this should be removed in favor of checks in PptTopLevel 094 // such as is_equal, is_lessequal, etc. 095 // Look up a previously instantiated StringNonEqual relationship. 096 // Should this implementation be made more efficient? 097 public static @Nullable StringNonEqual find(PptSlice ppt) { 098 assert ppt.arity() == 2; 099 for (Invariant inv : ppt.invs) { 100 if (inv instanceof StringNonEqual) { 101 return (StringNonEqual) inv; 102 } 103 } 104 105 // If the invariant is suppressed, create it 106 if ((suppressions != null) && suppressions.suppressed(ppt)) { 107 StringNonEqual inv = proto.instantiate_dyn(ppt); 108 // System.out.printf("%s is suppressed in ppt %s%n", inv.format(), ppt.name()); 109 return inv; 110 } 111 112 return null; 113 } 114 115 @Override 116 public String repr(@GuardSatisfied StringNonEqual this) { 117 return "StringNonEqual" + varNames(); 118 } 119 120 @SideEffectFree 121 @Override 122 public String format_using(@GuardSatisfied StringNonEqual this, OutputFormat format) { 123 124 String var1name = var1().name_using(format); 125 String var2name = var2().name_using(format); 126 127 if ((format == OutputFormat.DAIKON) || (format == OutputFormat.ESCJAVA)) { 128 String comparator = "!="; 129 return var1name + " " + comparator + " " + var2name; 130 } 131 132 if (format == OutputFormat.CSHARPCONTRACT) { 133 134 assert var1().has_typeof() == var2().has_typeof(); 135 if (var1().has_typeof()) { 136 return var1name + " != " + var2name; 137 } else { 138 return "!" + var1name + ".Equals(" + var2name + ")"; 139 } 140 141 } 142 143 if (format.isJavaFamily()) { 144 145 assert var1().has_typeof() == var2().has_typeof(); 146 if (var1().has_typeof()) { 147 return var1name + " != " + var2name; 148 } else { 149 return "!" + var1name + ".equals(" + var2name + ")"; 150 } 151 152 } 153 154 if (format == OutputFormat.SIMPLIFY) { 155 156 String comparator = "NEQ"; 157 158 return "(" 159 + comparator 160 + " " 161 + var1().simplifyFixup(var1name) 162 + " " 163 + var2().simplifyFixup(var2name) 164 + ")"; 165 } 166 167 return format_unimplemented(format); 168 } 169 170 @Override 171 public InvariantStatus check_modified(@Interned String v1, @Interned String v2, int count) { 172 if (!(v1 != v2)) { 173 return InvariantStatus.FALSIFIED; 174 } 175 return InvariantStatus.NO_CHANGE; 176 } 177 178 @Override 179 public InvariantStatus add_modified(@Interned String v1, @Interned String v2, int count) { 180 if (logDetail() || debug.isLoggable(Level.FINE)) { 181 log( 182 debug, 183 "add_modified (" + v1 + ", " + v2 + ", ppt.num_values = " + ppt.num_values() + ")"); 184 } 185 if ((logOn() || debug.isLoggable(Level.FINE)) 186 && check_modified(v1, v2, count) == InvariantStatus.FALSIFIED) 187 log(debug, "destroy in add_modified (" + v1 + ", " + v2 + ", " + count + ")"); 188 189 return check_modified(v1, v2, count); 190 } 191 192 // This is very tricky, because whether two variables are equal should 193 // presumably be transitive, but it's not guaranteed to be so when using 194 // this method and not dropping out all variables whose values are ever 195 // missing. 196 @Override 197 protected double computeConfidence() { 198 // Should perhaps check number of samples and be unjustified if too few 199 // samples. 200 201 // // The reason for this multiplication is that there might be only a 202 // // very few possible values. Example: towers of hanoi has only 6 203 // // possible (pegA, pegB) pairs. 204 // return 1 - (Math.pow(.5, ppt.num_values()) 205 // * Math.pow(.99, ppt.num_mod_samples())); 206 return 1 - Math.pow(.5, ppt.num_samples()); 207 } 208 209 @Pure 210 @Override 211 public boolean isExact() { 212 213 return false; 214 } 215 216 // // Temporary, for debugging 217 // public void destroy() { 218 // if (debug.isLoggable(Level.FINE)) { 219 // System.out.println("StringNonEqual.destroy(" + ppt.name() + ")"); 220 // System.out.println(repr()); 221 // (new Error()).printStackTrace(); 222 // } 223 // super.destroy(); 224 // } 225 226 @Override 227 public InvariantStatus add( 228 @Interned Object v1, @Interned Object v2, int mod_index, int count) { 229 if (debug.isLoggable(Level.FINE)) { 230 debug.fine( 231 "StringNonEqual" 232 + ppt.varNames() 233 + ".add(" 234 + v1 235 + "," 236 + v2 237 + ", mod_index=" 238 + mod_index 239 + "), count=" 240 + count 241 + ")"); 242 } 243 return super.add(v1, v2, mod_index, count); 244 } 245 246 @Pure 247 @Override 248 public boolean isSameFormula(Invariant other) { 249 return true; 250 } 251 252 @Pure 253 @Override 254 public boolean isExclusiveFormula(Invariant other) { 255 256 // Also ought to check against LinearBinary, etc. 257 258 if (other instanceof StringEqual) { 259 return true; 260 } 261 262 return false; 263 } 264 265 @Override 266 public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) { 267 final VarInfo var1 = vis[0]; 268 final VarInfo var2 = vis[1]; 269 270 if (var1.aux.hasValue(VarInfoAux.MAXIMUM_VALUE) 271 && var2.aux.hasValue(VarInfoAux.MINIMUM_VALUE)) { 272 int maxA = var1.aux.getInt(VarInfoAux.MAXIMUM_VALUE), 273 minB = var2.aux.getInt(VarInfoAux.MINIMUM_VALUE); 274 275 if (maxA < minB) { 276 return new DiscardInfo( 277 this, 278 DiscardCode.obvious, 279 var1.name() + " DISCARD_OP " + var2.name() + " is already known"); 280 } 281 } 282 283 if (var1.aux.hasValue(VarInfoAux.MINIMUM_VALUE) 284 && var2.aux.hasValue(VarInfoAux.MAXIMUM_VALUE)) { 285 int maxB = var2.aux.getInt(VarInfoAux.MAXIMUM_VALUE), 286 minA = var1.aux.getInt(VarInfoAux.MINIMUM_VALUE); 287 288 if (minA > maxB) { 289 return new DiscardInfo( 290 this, 291 DiscardCode.obvious, 292 var1.name() + " DISCARD_OP " + var2.name() + " is already known"); 293 } 294 } 295 296 return super.isObviousStatically(vis); 297 } 298 299 @Pure 300 @Override 301 public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) { 302 303 // JHP: We might consider adding a check over bounds. If 304 // x < c and y > c then we know that x < y. Similarly for 305 // x > c and y < c. We could also substitute oneof for 306 // one or both of the bound checks. 307 308 DiscardInfo super_result = super.isObviousDynamically(vis); 309 if (super_result != null) { 310 return super_result; 311 } 312 313 @SuppressWarnings("UnusedVariable") // generated code, variable is sometimes used 314 DiscardInfo di; 315 316 return null; 317 } // isObviousDynamically 318 319 /** NI suppressions, initialized in get_ni_suppressions() */ 320 private static @Nullable NISuppressionSet suppressions = null; 321 322 /** Returns the non-instantiating suppressions for this invariant. */ 323 @Pure 324 @Override 325 public NISuppressionSet get_ni_suppressions() { 326 if (suppressions == null) { 327 328 NISuppressee suppressee = new NISuppressee(StringNonEqual.class, 2); 329 330 // suppressor definitions (used in suppressions below) 331 332 NISuppressor v1_gt_v2 = new NISuppressor(0, 1, StringGreaterThan.class); 333 334 NISuppressor v1_lt_v2 = new NISuppressor(0, 1, StringLessThan.class); 335 336 suppressions = 337 new NISuppressionSet( 338 new NISuppression[] { 339 340 // v1 < v2 => v1 != v2 341 new NISuppression(v1_lt_v2, suppressee), 342 // v1 > v2 => v1 != v2 343 new NISuppression(v1_gt_v2, suppressee), 344 345 }); 346 } 347 return suppressions; 348 } 349 350}