001// ***** This file is automatically generated from PairwiseIntComparison.java.jpp 002 003package daikon.inv.binary.twoSequence; 004 005import daikon.*; 006import daikon.Quantify.QuantFlags; 007import daikon.derive.binary.*; 008import daikon.inv.*; 009import daikon.inv.binary.twoScalar.*; 010import daikon.suppress.*; 011import java.util.Arrays; 012import java.util.Iterator; 013import java.util.logging.Level; 014import java.util.logging.Logger; 015import org.checkerframework.checker.interning.qual.Interned; 016import org.checkerframework.checker.lock.qual.GuardSatisfied; 017import org.checkerframework.checker.nullness.qual.NonNull; 018import org.checkerframework.checker.nullness.qual.Nullable; 019import org.checkerframework.dataflow.qual.Pure; 020import org.checkerframework.dataflow.qual.SideEffectFree; 021import org.plumelib.util.ArraysPlume; 022import org.plumelib.util.Intern; 023import typequals.prototype.qual.NonPrototype; 024import typequals.prototype.qual.Prototype; 025 026/** 027 * Represents an invariant between corresponding elements of two sequences of String values. The 028 * length of the sequences must match for the invariant to hold. A comparison is made over each 029 * {@code (x[i], y[i])} pair. Thus, {@code x[0]} is compared to {@code y[0]}, 030 * {@code x[1]} to {@code y[1]}, and so forth. Prints as {@code x[] == y[]}. 031 */ 032public class PairwiseStringEqual extends TwoSequenceString { 033 static final long serialVersionUID = 20030822L; 034 035 /** Debug tracer. */ 036 public static final Logger debug = 037 Logger.getLogger("daikon.inv.binary.twoSequence.PairwiseStringEqual"); 038 039 // Variables starting with dkconfig_ should only be set via the 040 // daikon.config.Configuration interface. 041 /** Boolean. True iff PairwiseIntComparison invariants should be considered. */ 042 public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault; 043 044 static final boolean debugPairwiseIntComparison = false; 045 046 protected PairwiseStringEqual(PptSlice ppt) { 047 super(ppt); 048 } 049 050 protected @Prototype PairwiseStringEqual() { 051 super(); 052 } 053 054 private static @Prototype PairwiseStringEqual proto = new @Prototype PairwiseStringEqual(); 055 056 /** Returns the prototype invariant for PairwiseStringEqual. */ 057 public static @Prototype PairwiseStringEqual get_proto() { 058 return proto; 059 } 060 061 @Override 062 public boolean enabled() { 063 return dkconfig_enabled; 064 } 065 066 @Override 067 public boolean instantiate_ok(VarInfo[] vis) { 068 069 if (!valid_types(vis)) { 070 return false; 071 } 072 073 return true; 074 } 075 076 @Override 077 protected PairwiseStringEqual instantiate_dyn(@Prototype PairwiseStringEqual this, PptSlice slice) { 078 PairwiseStringEqual inv = new PairwiseStringEqual(slice); 079 if (logOn()) { 080 inv.log("instantiate"); 081 } 082 return inv; 083 } 084 085 @Pure 086 @Override 087 public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) { 088 VarInfo var1 = vis[0]; 089 VarInfo var2 = vis[1]; 090 091 DiscardInfo di = SubSequence.isObviousSubSequence(this, var1, var2); 092 if (di == null) { 093 di = SubSequence.isObviousSubSequence(this, var2, var1); 094 } 095 if (di != null) { 096 Global.implied_noninstantiated_invariants++; 097 return di; 098 } 099 100 // Don't instantiate if the variables can't have order 101 if (!var1.aux.hasOrder() || !var2.aux.hasOrder()) { 102 if (debug.isLoggable(Level.FINE)) { 103 debug.fine("Not instantitating for because order has no meaning: " 104 + var1.name() + " and " + var2.name()); 105 } 106 return new DiscardInfo(this, DiscardCode.obvious, "Obvious statically since order has no meaning"); 107 } 108 109 return super.isObviousStatically(vis); 110 } 111 112 @Pure 113 @Override 114 public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) { 115 DiscardInfo super_result = super.isObviousDynamically(vis); 116 if (super_result != null) { 117 return super_result; 118 } 119 120 // Subsequence invariants are implied by the same invariant over 121 // the supersequence 122 DiscardInfo di = superseq_implies(vis); 123 if (di != null) { 124 return di; 125 } 126 127 return null; 128 } 129 130 /** 131 * Checks to see if the same invariant exists over supersequences of these variables: 132 * 133 * <pre> 134 * (A[] op B[]) ^ (i == j) ⇒ A[i..] op B[j..] 135 * (A[] op B[]) ^ (i == j) ⇒ A[..i] op B[..j] 136 * </pre> 137 */ 138 private @Nullable DiscardInfo superseq_implies(VarInfo[] vis) { 139 140 // Make sure the variables are SequenceStringSubsequence with the same start/end 141 VarInfo v1 = vis[0]; 142 VarInfo v2 = vis[1]; 143 if (!v1.isDerived() || !(v1.derived instanceof SequenceStringSubsequence)) { 144 return null; 145 } 146 if (!v2.isDerived() || !(v2.derived instanceof SequenceStringSubsequence)) { 147 return null; 148 } 149 @NonNull SequenceStringSubsequence der1 = (SequenceStringSubsequence) v1.derived; 150 @NonNull SequenceStringSubsequence der2 = (SequenceStringSubsequence) v2.derived; 151 if ((der1.from_start != der2.from_start) 152 || (der1.index_shift != der2.index_shift)) 153 return null; 154 155 // Make sure the subscripts are equal 156 DiscardInfo di = new DiscardInfo(this, DiscardCode.obvious, ""); 157 if (!ppt.parent.check_implied_canonical(di, der1.sclvar(), der2.sclvar(), 158 IntEqual.get_proto())) 159 return null; 160 161 // See if the super-sequences have the same invariant 162 if (!ppt.parent.check_implied_canonical(di, der1.seqvar(), der2.seqvar(), 163 PairwiseStringEqual.get_proto())) 164 return null; 165 166 // Add in the vis variables to di reason (if they are different) 167 di.add_implied_vis(vis); 168 return di; 169 } 170 171 @Override 172 protected Invariant resurrect_done_swapped() { 173 174 return this; 175 } 176 177 @Pure 178 @Override 179 public boolean is_symmetric() { 180 return true; 181 } 182 183 @Override 184 public String repr(@GuardSatisfied PairwiseStringEqual this) { 185 return "PairwiseStringEqual" + varNames() + ": "; 186 } 187 188 public String getComparator() { 189 return "=="; 190 } 191 192 @SideEffectFree 193 @Override 194 public String format_using(@GuardSatisfied PairwiseStringEqual this, OutputFormat format) { 195 196 if (format.isJavaFamily()) { 197 return format_java_family(format); 198 } 199 200 if (format == OutputFormat.DAIKON) { 201 return format_daikon(); 202 } 203 if (format == OutputFormat.ESCJAVA) { 204 return format_esc(); 205 } 206 if (format == OutputFormat.SIMPLIFY) { 207 return format_simplify(); 208 } 209 if (format == OutputFormat.CSHARPCONTRACT) { 210 return format_csharp(); 211 } 212 213 return format_unimplemented(format); 214 } 215 216 public String format_daikon(@GuardSatisfied PairwiseStringEqual this) { 217 return var1().name() + " == " + var2().name() + " (elementwise)"; 218 } 219 220 public String format_esc(@GuardSatisfied PairwiseStringEqual this) { 221 String[] form = VarInfo.esc_quantify(var1(), var2()); 222 return form[0] + "(" + form[1] + " == " + form[2] + ")" + form[3]; 223 } 224 225 public String format_simplify(@GuardSatisfied PairwiseStringEqual this) { 226 String[] form = VarInfo.simplify_quantify(QuantFlags.element_wise(), var1(), var2()); 227 return form[0] + "(EQ " + form[1] + " " + form[2] + ")" + form[3]; 228 } 229 230 public String format_java_family(@GuardSatisfied PairwiseStringEqual this, OutputFormat format) { 231 return "daikon.Quant.pairwiseEqual(" + var1().name_using(format) 232 + ", " + var2().name_using(format) + ")"; 233 } 234 235 public String format_csharp(@GuardSatisfied PairwiseStringEqual this) { 236 237 String[] split1 = var1().csharp_array_split(); 238 String[] split2 = var2().csharp_array_split(); 239 240 String equals_str; 241 String end_str; 242 243 equals_str = ".Equals("; 244 end_str = ")"; 245 246 return "Contract.ForAll(0, " + split1[0] + ".Count(), i => " + split1[0] + "[i]" + split1[1] + equals_str + split2[0] + "[i]" + split2[1] + end_str + ")"; 247 } 248 249 @Override 250 public InvariantStatus check_modified(String @Interned [] a1, String @Interned [] a2, int count) { 251 assert a1 != null && a2 != null 252 : var1() + " " + var2() + " " + FileIO.get_linenum(); 253 if (a1.length != a2.length || a1.length == 0 || a2.length == 0) { 254 // destroyAndFlow(); 255 return InvariantStatus.FALSIFIED; 256 } 257 258 int len = a1.length; 259 // int len = Math.min(a1.length, a2.length); 260 261 for (int i = 0; i < len; i++) { 262 String v1 = a1[i]; 263 String v2 = a2[i]; 264 if (!(v1 != null && v2 != null && v1.equals( v2)) ) { 265 // destroyAndFlow(); 266 return InvariantStatus.FALSIFIED; 267 } 268 } 269 return InvariantStatus.NO_CHANGE; 270 } 271 272 @Override 273 public InvariantStatus add_modified(String @Interned [] a1, String @Interned [] a2, 274 int count) { 275 if (logDetail()) { 276 log(debug, "saw add_modified (" + Arrays.toString(a1) 277 + ", " + Arrays.toString(a2) + ")"); 278 } 279 return check_modified(a1, a2, count); 280 } 281 282 @Override 283 protected double computeConfidence() { 284 // num_elt_values() would be more appropriate 285 // int num_values = ((PptSlice2) ppt).num_elt_values(); 286 int num_values = ppt.num_samples(); 287 if (num_values == 0) { 288 return Invariant.CONFIDENCE_UNJUSTIFIED; 289 } else { 290 291 // It's an equality invariant 292 return Invariant.CONFIDENCE_JUSTIFIED; 293 } 294 } 295 296 @Pure 297 @Override 298 public boolean isSameFormula(Invariant other) { 299 return true; 300 } 301 302 @Pure 303 @Override 304 public boolean isExclusiveFormula(Invariant other) { 305 return false; 306 } 307 308 // Look up a previously instantiated invariant. 309 public static @Nullable PairwiseStringEqual find(PptSlice ppt) { 310 assert ppt.arity() == 2; 311 for (Invariant inv : ppt.invs) { 312 if (inv instanceof PairwiseStringEqual) { 313 return (PairwiseStringEqual) inv; 314 } 315 } 316 return null; 317 } 318 319 /** Returns a list of non-instantiating suppressions for this invariant. */ 320 @Pure 321 @Override 322 public @Nullable NISuppressionSet get_ni_suppressions() { 323 return suppressions; 324 } 325 326 private static @Nullable NISuppressionSet suppressions = null; 327 328}