001 // #define PAIRWISEINTEQUAL PairwiseStringEqual 002 003// ***** This file is automatically generated from SeqComparison.java.jpp 004 005package daikon.inv.binary.twoSequence; 006 007import daikon.*; 008import daikon.Quantify.QuantFlags; 009import daikon.derive.binary.*; 010import daikon.inv.*; 011import daikon.suppress.*; 012import java.util.*; 013import java.util.logging.Logger; 014import org.checkerframework.checker.interning.qual.Interned; 015import org.checkerframework.checker.lock.qual.GuardSatisfied; 016import org.checkerframework.checker.nullness.qual.Nullable; 017import org.checkerframework.dataflow.qual.Pure; 018import org.checkerframework.dataflow.qual.SideEffectFree; 019import org.plumelib.util.ArraysPlume; 020import org.plumelib.util.Intern; 021import typequals.prototype.qual.NonPrototype; 022import typequals.prototype.qual.Prototype; 023 024/** 025 * Represents invariants between two sequences of String values. If order matters for each 026 * variable (which it does by default), then the sequences are compared lexically. Prints as 027 * {@code x[] == y[] lexically}. 028 * 029 030 * <p>If order doesn't matter for each variable, then the sequences are compared to see if they are 031 * set equivalent. Prints as {@code x[] == y[]}. 032 * 033 034 * <p>If the auxiliary information (e.g., order matters) doesn't match between two variables, then 035 * this invariant cannot apply to those variables. 036 */ 037public class SeqSeqStringEqual extends TwoSequenceString 038 039 implements EqualityComparison 040 041{ 042 static final long serialVersionUID = 20030822L; 043 044 // Variables starting with dkconfig_ should only be set via the 045 // daikon.config.Configuration interface. 046 /** Boolean. True iff SeqSeqStringEqual invariants should be considered. */ 047 public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault; 048 049 /** Debugging logger. */ 050 static final Logger debug = Logger.getLogger("daikon.inv.binary.twoSequence.SeqSeqStringEqual"); 051 052 static Comparator<String[]> comparator = ArraysPlume.StringArrayComparatorLexical.it; 053 054 boolean orderMatters; 055 056 protected SeqSeqStringEqual(PptSlice ppt, boolean orderMatters) { 057 super(ppt); 058 this.orderMatters = orderMatters; 059 } 060 061 protected @Prototype SeqSeqStringEqual(boolean orderMatters) { 062 super(); 063 this.orderMatters = orderMatters; 064 } 065 066 private static @Prototype SeqSeqStringEqual proto = new @Prototype SeqSeqStringEqual(true); 067 068 /** Returns the prototype invariant for SeqSeqStringEqual */ 069 public static @Prototype SeqSeqStringEqual get_proto() { 070 return proto; 071 } 072 073 @Override 074 public boolean enabled() { 075 return dkconfig_enabled; 076 } 077 078 @Override 079 public boolean instantiate_ok(VarInfo[] vis) { 080 081 if (!valid_types(vis)) { 082 return false; 083 } 084 085 return true; 086 } 087 088 @Override 089 protected SeqSeqStringEqual instantiate_dyn(@Prototype SeqSeqStringEqual this, PptSlice slice) { 090 boolean has_order = slice.var_infos[0].aux.hasOrder() && slice.var_infos[1].aux.hasOrder(); 091 return new SeqSeqStringEqual(slice, has_order); 092 } 093 094 @Override 095 protected Invariant resurrect_done_swapped() { 096 097 return this; 098 } 099 100 @Override 101 public String repr(@GuardSatisfied SeqSeqStringEqual this) { 102 return "SeqSeqStringEqual" + varNames() + ": ,orderMatters=" + orderMatters 103 + ",enoughSamples=" + enoughSamples() 104 ; 105 } 106 107 @SideEffectFree 108 @Override 109 public String format_using(@GuardSatisfied SeqSeqStringEqual this, OutputFormat format) { 110 // System.out.println("Calling SeqSeqStringEqual.format for: " + repr()); 111 112 if (format == OutputFormat.SIMPLIFY) { 113 return format_simplify(); 114 } 115 116 if (format == OutputFormat.DAIKON) { 117 String name1 = var1().name_using(format); 118 String name2 = var2().name_using(format); 119 120 return name1 + " == " + name2; 121 } 122 123 if (format == OutputFormat.CSHARPCONTRACT) { 124 125 String[] split1 = var1().csharp_array_split(); 126 String[] split2 = var2().csharp_array_split(); 127 // Pairwise equal. 128 return "Contract.ForAll(0, " + split1[0] + ".Count(), i => " + split1[0] + "[i]" + split1[1] + ".Equals(" + split2[0] + "[i]" + split2[1] + "))"; 129 } 130 131 if (format.isJavaFamily()) { 132 String name1 = var1().name_using(format); 133 String name2 = var2().name_using(format); 134 135 return "daikon.Quant.pairwiseEqual(" + name1 + ", " + name2 + ")"; 136 } 137 138 return format_unimplemented(format); 139 } 140 141 public String format_simplify(@GuardSatisfied SeqSeqStringEqual this) { 142 if (Invariant.dkconfig_simplify_define_predicates) { 143 return format_simplify_defined(); 144 } else { 145 return format_simplify_explicit(); 146 } 147 } 148 149 private String format_simplify_defined(@GuardSatisfied SeqSeqStringEqual this) { 150 String[] var1_name = var1().simplifyNameAndBounds(); 151 String[] var2_name = var2().simplifyNameAndBounds(); 152 if (var1_name == null || var2_name == null) { 153 return String.format("%s.format_simplify_defined(%s): var1_name=%s, var2_name=%s, for %s", 154 getClass().getSimpleName(), this, 155 Arrays.toString(var1_name), Arrays.toString(var2_name), format()); 156 } 157 return "(|lexical-==| " 158 + var1_name[0] + " " + var1_name[1] + " " + var1_name[2] + " " 159 + var2_name[0] + " " + var2_name[1] + " " + var2_name[2] + ")"; 160 } 161 162 private String format_simplify_explicit(@GuardSatisfied SeqSeqStringEqual this) { 163 164 // A simple case: if two sequences are lexically equal iff they 165 // are elementwise equal. 166 String[] form = VarInfo.simplify_quantify(QuantFlags.element_wise(), 167 var1(), var2()); 168 return form[0] 169 + "(EQ " + form[1] + " " + form[2] + ")" + form[3]; 170 171 } 172 173 @Override 174 public InvariantStatus check_modified( 175 String @Interned [] v1, String @Interned [] v2, int count) { 176 /// This does not do the right thing; I really want to avoid comparisons 177 /// if one is missing, but not if one is zero-length. 178 // // Don't make comparisons with empty arrays. 179 // if ((v1.length == 0) || (v2.length == 0)) { 180 // return; 181 // } 182 183 int comparison = 0; 184 if (orderMatters) { 185 // Standard element wise comparison 186 comparison = comparator.compare(v1, v2); 187 } else { 188 // Do a double subset comparison 189 comparison = (ArraysPlume.isSubset(v1, v2) && ArraysPlume.isSubset( v2, v1)) ? 0 : -1; 190 } 191 192 if (!(comparison == 0) ) { 193 return InvariantStatus.FALSIFIED; 194 } 195 return InvariantStatus.NO_CHANGE; 196 } 197 198 @Override 199 public InvariantStatus add_modified(String @Interned [] v1, String @Interned [] v2, int count) { 200 if (logDetail()) { 201 log("add_modified (%s, %s)", Arrays.toString(v1), Arrays.toString(v2)); 202 } 203 return check_modified(v1, v2, count); 204 } 205 206 @Override 207 protected double computeConfidence() { 208 209 // It's an equality invariant 210 if (ppt.num_samples() == 0) { 211 return Invariant.CONFIDENCE_UNJUSTIFIED; 212 } else { 213 return Invariant.CONFIDENCE_JUSTIFIED; 214 } 215 216 } 217 218 // For Comparison interface 219 @Override 220 public double eq_confidence() { 221 return getConfidence(); 222 } 223 224 @Pure 225 @Override 226 public boolean isSameFormula(Invariant o) { 227 return true; 228 } 229 230 @Pure 231 @Override 232 public boolean isExclusiveFormula(Invariant o) { 233 return false; 234 } 235 236 /** 237 * Since this invariant can be a postProcessed equality, we have to handle isObvious especially to 238 * avoid circular isObvious relations. 239 */ 240 @Pure 241 @Override 242 public @Nullable DiscardInfo isObviousStatically_SomeInEquality() { 243 if (var1().equalitySet == var2().equalitySet) { 244 return isObviousStatically(this.ppt.var_infos); 245 } else { 246 return super.isObviousStatically_SomeInEquality(); 247 } 248 } 249 250 /** 251 * Since this invariant can be a postProcessed equality, we have to handle isObvious especially to 252 * avoid circular isObvious relations. 253 */ 254 @Pure 255 @Override 256 public @Nullable DiscardInfo isObviousDynamically_SomeInEquality() { 257 if (logOn()) { 258 log("Considering dynamically_someInEquality"); 259 } 260 if (var1().equalitySet == var2().equalitySet) { 261 return isObviousDynamically(this.ppt.var_infos); 262 } else { 263 return super.isObviousDynamically_SomeInEquality(); 264 } 265 } 266 267 @Pure 268 @Override 269 public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) { 270 271 return super.isObviousStatically(vis); 272 } 273 274 @Pure 275 @Override 276 public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) { 277 DiscardInfo super_result = super.isObviousDynamically(vis); 278 if (super_result != null) { 279 return super_result; 280 } 281 assert ppt != null; 282 283 return null; 284 } 285 286 @Override 287 public void repCheck() { 288 super.repCheck(); 289 /* 290 This code is no longer needed now that the can_be_x's are gone 291 if (!(this.can_be_eq || this.can_be_lt || this.can_be_gt) 292 && ppt.num_samples() != 0) { 293 System.err.println(this.repr()); 294 System.err.println(this.ppt.num_samples()); 295 throw new Error(); 296 } 297 */ 298 } 299 300 @Pure 301 public boolean isEqual() { 302 303 return true; 304 } 305 306 // Look up a previously instantiated invariant. 307 public static @Nullable SeqSeqStringEqual find(PptSlice ppt) { 308 assert ppt.arity() == 2; 309 for (Invariant inv : ppt.invs) { 310 if (inv instanceof SeqSeqStringEqual) { 311 return (SeqSeqStringEqual) inv; 312 } 313 } 314 return null; 315 } 316 317 /** Returns a list of non-instantiating suppressions for this invariant. */ 318 @Pure 319 @Override 320 public @Nullable NISuppressionSet get_ni_suppressions() { 321 return suppressions; 322 } 323 324 private static @Nullable NISuppressionSet suppressions = null; 325 326 @Override 327 public @Nullable @NonPrototype SeqSeqStringEqual merge( 328 @Prototype SeqSeqStringEqual this, List<@NonPrototype Invariant> invs, PptSlice parent_ppt) { 329 // Ignore the orderMatters field, because it is always the same (and is always true). 330 return (SeqSeqStringEqual) super.merge(invs, parent_ppt); 331 } 332}