001// ***** This file is automatically generated from Numeric.java.jpp 002 003package daikon.inv.binary.twoSequence; 004 005import org.checkerframework.checker.lock.qual.GuardSatisfied; 006import org.checkerframework.checker.nullness.qual.NonNull; 007import org.checkerframework.checker.nullness.qual.Nullable; 008import org.checkerframework.checker.signature.qual.ClassGetName; 009import org.checkerframework.dataflow.qual.Pure; 010import org.checkerframework.dataflow.qual.SideEffectFree; 011import static daikon.inv.Invariant.asInvClass; 012 013import daikon.*; 014import daikon.Quantify.QuantFlags; 015import daikon.derive.binary.*; 016import daikon.inv.*; 017import daikon.inv.binary.twoScalar.*; 018import daikon.inv.binary.twoString.*; 019import daikon.inv.unary.scalar.*; 020import daikon.inv.unary.sequence.*; 021import daikon.suppress.*; 022import java.util.*; 023import org.plumelib.util.UtilPlume; 024import typequals.prototype.qual.NonPrototype; 025import typequals.prototype.qual.Prototype; 026 027/** 028 * Baseclass for binary numeric invariants. 029 * 030 * Each specific invariant is implemented in a subclass (typically, in this file). The subclass must 031 * provide the methods instantiate(), check(), and format(). Symmetric functions should define 032 * is_symmetric() to return true. 033 */ 034public abstract class PairwiseString extends TwoSequenceString { 035 036 static final long serialVersionUID = 20060609L; 037 038 protected PairwiseString(PptSlice ppt, boolean swap) { 039 super(ppt); 040 this.swap = swap; 041 } 042 043 protected PairwiseString(boolean swap) { 044 super(); 045 this.swap = swap; 046 } 047 048 @Override 049 public boolean instantiate_ok(VarInfo[] vis) { 050 051 ProglangType type1 = vis[0].file_rep_type; 052 ProglangType type2 = vis[1].file_rep_type; 053 if (!type1.baseIsString() || !type2.baseIsString()) { 054 return false; 055 } 056 057 return true; 058 } 059 060 @Pure 061 @Override 062 public boolean isExact() { 063 return true; 064 } 065 066 @Override 067 public String repr(@GuardSatisfied PairwiseString this) { 068 return getClass().getSimpleName() + ": " + format() 069 + (swap ? " [swapped]" : " [unswapped]"); 070 } 071 072 /** 073 * Returns a string in the specified format that describes the invariant. 074 * 075 * The generic format string is obtained from the subclass specific get_format_str(). Instances of 076 * %varN% are replaced by the variable name in the specified format. 077 */ 078 @SideEffectFree 079 @Override 080 public String format_using(@GuardSatisfied PairwiseString this, OutputFormat format) { 081 082 if (ppt == null) { 083 return String.format("proto ppt [class %s] format %s", getClass(), 084 get_format_str(format)); 085 } 086 String fmt_str = get_format_str(format); 087 088 String v1; 089 String v2; 090 if (format.isJavaFamily()) { 091 092 return format_unimplemented(format); 093 094 } else if (format == OutputFormat.CSHARPCONTRACT) { 095 096 fmt_str = fmt_str.replace("%var1%", var1().csharp_name()); 097 fmt_str = fmt_str.replace("%var2%", var2().csharp_name()); 098 return fmt_str; 099 100 } 101 102 if (format == OutputFormat.ESCJAVA) { 103 String[] form = VarInfo.esc_quantify(var1(), var2()); 104 fmt_str = form[0] + "(" + fmt_str + ")" + form[3]; 105 v1 = form[1]; 106 v2 = form[2]; 107 } else if (format == OutputFormat.SIMPLIFY) { 108 String[] form = VarInfo.simplify_quantify(QuantFlags.element_wise(), 109 var1(), var2()); 110 fmt_str = form[0] + " " + fmt_str + " " + form[3]; 111 v1 = form[1]; 112 v2 = form[2]; 113 } else { 114 v1 = var1().name_using(format); 115 v2 = var2().name_using(format); 116 if (format == OutputFormat.DAIKON) { 117 fmt_str += " (elementwise)"; 118 } 119 } 120 121 // Note that we do not use String.replaceAll here, because that's 122 // inseparable from the regex library, and we don't want to have to 123 // escape v1 with something like 124 // v1.replaceAll("([\\$\\\\])", "\\\\$1") 125 fmt_str = fmt_str.replace("%var1%", v1); 126 fmt_str = fmt_str.replace("%var2%", v2); 127 128 // if (false && (format == OutputFormat.DAIKON)) { 129 // fmt_str = "[" + getClass() + "]" + fmt_str + " (" 130 // + var1().get_value_info() + ", " + var2().get_value_info() + ")"; 131 // } 132 return fmt_str; 133 } 134 135 /** Calls the function specific equal check and returns the correct status. */ 136 137 @Override 138 public InvariantStatus check_modified(String[] x, String[] y, 139 int count) { 140 if (x.length != y.length) { 141 if (Debug.logOn()) { 142 log("Falsified - x length = %s y length = %s", x.length, y.length); 143 } 144 return InvariantStatus.FALSIFIED; 145 } 146 147 if (Debug.logDetail()) { 148 log("testing values %s, %s", Arrays.toString (x), 149 Arrays.toString(y)); 150 } 151 152 try { 153 for (int i = 0; i < x.length; i++) { 154 if (!eq_check(x[i], y[i])) { 155 if (Debug.logOn()) { 156 log("Falsified - x[%s]=%s y[%s]=%s", i, x[i], i, y[i]); 157 } 158 return InvariantStatus.FALSIFIED; 159 } 160 } 161 return InvariantStatus.NO_CHANGE; 162 } catch (Exception e) { 163 if (Debug.logOn()) { 164 log("Falsified - exception %s", e); 165 } 166 return InvariantStatus.FALSIFIED; 167 } 168 } 169 170 /** 171 * Checks to see if this invariant is over subsequences and if the same relationship holds over 172 * the full sequence. This is obvious if it does. For example 'x[foo..] op y[bar..]' would be 173 * obvious if 'x[] op y[]' This can't fully be handled as a suppression since a suppression needs 174 * to insure that foo == bar as well. But that is not a requirement here (the fact that 'x[] op 175 * y[]' implies that foo == bar when x[] and y[] are not missing). 176 */ 177 public @Nullable DiscardInfo is_subsequence(VarInfo[] vis) { 178 179 VarInfo v1 = var1(vis); 180 VarInfo v2 = var2(vis); 181 182 // Make sure each var is a sequence subsequence 183 if (!v1.isDerived() || !(v1.derived instanceof SequenceStringSubsequence)) { 184 return null; 185 } 186 if (!v2.isDerived() || !(v2.derived instanceof SequenceStringSubsequence)) { 187 return null; 188 } 189 190 @NonNull SequenceStringSubsequence der1 = (SequenceStringSubsequence) v1.derived; 191 @NonNull SequenceStringSubsequence der2 = (SequenceStringSubsequence) v2.derived; 192 193 // Both of the indices must be either from the start or up to the end. 194 // It is not necessary to check that they match in any other way since 195 // if the supersequence holds, that implies that the sequences are 196 // of the same length. Thus any subsequence that starts from the 197 // beginning or finishes at the end must end or start at the same 198 // spot (or it would have been falsified when it didn't) 199 if (der1.from_start != der2.from_start) { 200 return null; 201 } 202 203 // Look up this class over the sequence variables 204 Invariant inv = find(getClass(), der1.seqvar(), der2.seqvar()); 205 if (inv == null) { 206 return null; 207 } 208 return new DiscardInfo(this, DiscardCode.obvious, "Implied by " 209 + inv.format()); 210 } 211 212 @Pure 213 @Override 214 public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) { 215 216 DiscardInfo super_result = super.isObviousDynamically(vis); 217 if (super_result != null) { 218 return super_result; 219 } 220 221 // any elementwise relation across subsequences is made obvious by 222 // the same relation across the original sequence 223 DiscardInfo result = is_subsequence(vis); 224 if (result != null) { 225 return result; 226 } 227 228 // Check for invariant specific obvious checks. The obvious_checks 229 // method returns an array of arrays of antecedents. If all of the 230 // antecedents in an array are true, then the invariant is obvoius. 231 InvDef[][] obvious_arr = obvious_checks(vis); 232 obvious_loop: 233 for (int i = 0; i < obvious_arr.length; i++) { 234 InvDef[] antecedents = obvious_arr[i]; 235 StringBuilder why = null; 236 for (int j = 0; j < antecedents.length; j++) { 237 Invariant inv = antecedents[j].find(); 238 if (inv == null) { 239 continue obvious_loop; 240 } 241 if (why == null) { 242 why = new StringBuilder(inv.format()); 243 } else { 244 why.append(" and "); 245 why.append(inv.format()); 246 } 247 } 248 return new DiscardInfo(this, DiscardCode.obvious, "Implied by " + why); 249 } 250 251 return null; 252 } 253 254 /** 255 * Returns an invariant that is true when the size(v1) == size(v2). There are a number of 256 * possible cases for an array: 257 * 258 * <pre> 259 * x[] - entire array, size usually available as size(x[]) 260 * x[..(n-1)] - size is n 261 * x[..n] - size is n+1 262 * x[n..] - size is size(x[]) - n 263 * x[(n+1)..] - size is size(x[]) - (n+1) 264 * </pre> 265 * 266 * Each combination of the above must be considered in creating the equality invariant. Not all 267 * possibilities can be handled. Null is returned in that case. In the following table, s stands 268 * for the size 269 * 270 * <pre> 271 * x[] x[..(n-1)] x[..n] x[n..] x[(n+1)..] 272 * --------- ---------- ------ ------ ---------- 273 * y[] s(y)=s(x) s(y)=n 274 * y[..(m-1)] x m=n 275 * y[..m] x x m=n 276 * y[m..] x x x m=n ∧ 277 * s(y)=s(x) 278 * y[(m+1)..] x x x x m=n ∧ 279 * s(y)=s(x) 280 * </pre> 281 * NOTE: this is not currently used. Many (if not all) of the missing table cells above could be 282 * filled in with linear binary invariants (eg, m = n + 1). 283 */ 284 public @Nullable InvDef array_sizes_eq(VarInfo v1, VarInfo v2) { 285 286 VarInfo v1_size = get_array_size(v1); 287 VarInfo v2_size = get_array_size(v2); 288 289 // If we can find a size variable for each side build the invariant 290 if ((v1_size != null) && (v2_size != null)) { 291 return new InvDef(v1_size, v2_size, IntEqual.class); 292 } 293 294 // If either variable is not derived, there is no possible invariant 295 // (since we covered all of the direct size comparisons above) 296 if ((v1.derived == null) || (v2.derived == null)) { 297 return null; 298 } 299 300 // Get the sequence subsequence derivations 301 SequenceStringSubsequence v1_ss = (SequenceStringSubsequence) v1.derived; 302 SequenceStringSubsequence v2_ss = (SequenceStringSubsequence) v2.derived; 303 304 // If both are from_start and have the same index_shift, just compare 305 // the variables 306 if (v1_ss.from_start && v2_ss.from_start 307 && (v1_ss.index_shift == v2_ss.index_shift)) { 308 return new InvDef(v1_ss.sclvar(), v2_ss.sclvar(), IntEqual.class); 309 } 310 311 return null; 312 } 313 314 /** 315 * Returns a variable that corresponds to the size of v. Returns null if no such variable exists. 316 * 317 * There are two cases that are not handled: x[..n] with an index shift and x[n..]. 318 */ 319 public @Nullable VarInfo get_array_size(VarInfo v) { 320 321 assert v.rep_type.isArray(); 322 323 if (v.derived == null) { 324 return v.sequenceSize(); 325 } else if (v.derived instanceof SequenceStringSubsequence) { 326 SequenceStringSubsequence ss = (SequenceStringSubsequence) v.derived; 327 if (ss.from_start && (ss.index_shift == -1)) { 328 return ss.sclvar(); 329 } 330 } 331 332 return null; 333 } 334 335 /** 336 * Return a format string for the specified output format. Each instance of %varN% will be 337 * replaced by the correct name for varN. 338 */ 339 public abstract String get_format_str(@GuardSatisfied PairwiseString this, OutputFormat format); 340 341 /** Returns true if x and y don't invalidate the invariant. */ 342 public abstract boolean eq_check(String x, String y); 343 344 /** 345 * Returns an array of arrays of antecedents. If all of the antecedents in any array are true, 346 * then the invariant is obvious. 347 */ 348 public InvDef[][] obvious_checks(VarInfo[] vis) { 349 return new InvDef[][] {}; 350 } 351 352 public static List<@Prototype Invariant> get_proto_all() { 353 354 List<@Prototype Invariant> result = new ArrayList<>(); 355 356 result.add(SubString.get_proto(false)); 357 result.add(SubString.get_proto(true)); 358 359 // System.out.printf("%s get proto: %s%n", PairwiseString.class, result); 360 return result; 361 } 362 363 // suppressor definitions, used by many of the classes below 364 protected static NISuppressor 365 366 var1_eq_var2 = new NISuppressor(0, 1, PairwiseStringEqual.class), 367 var2_eq_var1 = new NISuppressor(0, 1, PairwiseStringEqual.class); 368 369 // 370 // Int and Float Numeric Invariants 371 // 372 373// 374// Standard String invariants 375// 376 377 /** 378 * Represents the substring invariant between corresponding elements of two sequences of String. 379 * Prints as {@code x[] is a substring of y[]}. 380 */ 381 public static class SubString extends PairwiseString { 382 // We are Serializable, so we specify a version to allow changes to 383 // method signatures without breaking serialization. If you add or 384 // remove fields, you should change this number to the current date. 385 static final long serialVersionUID = 20081113L; 386 387 protected SubString(PptSlice ppt, boolean swap) { 388 super(ppt, swap); 389 } 390 391 protected SubString(boolean swap) { 392 super(swap); 393 } 394 395 private static @Prototype SubString proto = new @Prototype SubString(false); 396 private static @Prototype SubString proto_swap = new @Prototype SubString(true); 397 398 /** Returns the prototype invariant. */ 399 public static @Prototype SubString get_proto(boolean swap) { 400 if (swap) { 401 return proto_swap; 402 } else { 403 return proto; 404 } 405 } 406 407 // Variables starting with dkconfig_ should only be set via the 408 // daikon.config.Configuration interface. 409 /** Boolean. True iff SubString invariants should be considered. */ 410 public static boolean dkconfig_enabled = false; 411 412 @Override 413 public boolean enabled() { 414 return dkconfig_enabled; 415 } 416 417 @Override 418 protected SubString instantiate_dyn(@Prototype SubString this, PptSlice slice) { 419 return new SubString(slice, swap); 420 } 421 422 @Override 423 public String get_format_str(@GuardSatisfied SubString this, OutputFormat format) { 424 if (format == OutputFormat.DAIKON) { 425 return "%var1% is a substring of %var2%"; 426 } else if (format.isJavaFamily()) { 427 return "%var2%.contains(%var1%)"; 428 } else if (format == OutputFormat.CSHARPCONTRACT) { 429 430 return "Contract.ForAll(0, %var2%.Count(), i => %var2%[i].Contains(%var1%[i]))"; 431 } else { 432 return format_unimplemented(format); 433 } 434 } 435 436 @Override 437 public boolean eq_check(String x, String y) { 438 return y.contains(x); 439 } 440 441 /** Justified as long as there are samples. */ 442 @Override 443 protected double computeConfidence() { 444 if (ppt.num_samples() == 0) { 445 return Invariant.CONFIDENCE_UNJUSTIFIED; 446 } 447 448 return Invariant.CONFIDENCE_JUSTIFIED; 449 } 450 451 /** Returns a list of non-instantiating suppressions for this invariant. */ 452 @Pure 453 @Override 454 public NISuppressionSet get_ni_suppressions() { 455 if (swap) { 456 return suppressions_swap; 457 } else { 458 return suppressions; 459 } 460 } 461 462 /** definition of this invariant (the suppressee) (unswapped) */ 463 private static NISuppressee suppressee = new NISuppressee(SubString.class, false); 464 465 private static NISuppressionSet suppressions = 466 new NISuppressionSet( 467 new NISuppression[] { 468 // v1 == v2 ==> v1 subsequence v2 469 new NISuppression(var1_eq_var2, suppressee), 470 }); 471 private static NISuppressionSet suppressions_swap = suppressions.swap(); 472 } 473 474}