001// ***** This file is automatically generated from Member.java.jpp 002 003package daikon.inv.binary.sequenceScalar; 004 005import daikon.*; 006import daikon.derive.binary.*; 007import daikon.derive.ternary.*; 008import daikon.derive.unary.*; 009import daikon.inv.*; 010import daikon.inv.binary.twoSequence.*; 011import java.util.Arrays; 012import java.util.logging.Level; 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 org.plumelib.util.IPair; 022import typequals.prototype.qual.NonPrototype; 023import typequals.prototype.qual.Prototype; 024 025/** 026 * Represents long scalars that are always members of a sequence of long values. Prints as 027 * {@code x in y[]} where {@code x} is a long scalar and {@code y[]} is a sequence 028 * of long. 029 */ 030public final class Member extends SequenceScalar { 031 static final long serialVersionUID = 20031024L; 032 033 public static final Logger debug = Logger.getLogger("daikon.inv.binary.Member"); 034 035 // Variables starting with dkconfig_ should only be set via the 036 // daikon.config.Configuration interface. 037 /** Boolean. True iff Member invariants should be considered. */ 038 public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault; 039 040 Member(PptSlice ppt) { 041 super(ppt); 042 } 043 044 @Prototype Member() { 045 super(); 046 } 047 048 private static @Prototype Member proto = new @Prototype Member(); 049 050 /** Returns the prototype invariant for Member. */ 051 public static @Prototype Member get_proto() { 052 return proto; 053 } 054 055 @Override 056 public boolean enabled() { 057 return dkconfig_enabled; 058 } 059 060 @Override 061 protected Member instantiate_dyn(@Prototype PptSlice slice) { 062 return new Member(slice); 063 } 064 065 @Pure 066 @Override 067 public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) { 068 if (isObviousMember(sclvar(vis), seqvar(vis))) { 069 log("scalar is obvious member of"); 070 return new DiscardInfo( 071 this, 072 DiscardCode.obvious, 073 sclvar().name() + " is an obvious member of " + seqvar().name()); 074 } 075 return super.isObviousStatically(vis); 076 } 077 078 /** Check whether sclvar is a member of seqvar can be determined statically. */ 079 @Pure 080 public static boolean isObviousMember(VarInfo sclvar, VarInfo seqvar) { 081 082 VarInfo sclvar_seq = sclvar.isDerivedSequenceMember(); 083 084 if (sclvar_seq == null) { 085 // The scalar is not obviously (lexically) a member of any array. 086 return false; 087 } 088 // isObviousImplied: a[i] in a; max(a) in a 089 if (sclvar_seq == seqvar) { 090 // The scalar is a member of the same array. 091 return true; 092 } 093 // The scalar is a member of a different array than the sequence. 094 // But maybe the relationship is still obvious, so keep checking. 095 096 // isObviousImplied: when b==a[0..i]: b[j] in a; max(b) in a 097 // If the scalar is a member of a subsequence of the sequence, then 098 // the scalar is a member of the full sequence. 099 // This is satisfied, for instance, when determining that 100 // max(B[0..I]) is an obvious member of B. 101 VarInfo sclseqsuper = sclvar_seq.isDerivedSubSequenceOf(); 102 if (sclseqsuper == seqvar) { 103 return true; 104 } 105 106 // We know the scalar was derived from some array, but not from the 107 // sequence variable. If also not from what the sequence variable was 108 // derived from, we don't know anything about membership. 109 // Check: 110 // * whether comparing B[I] to B[0..J] 111 // * whether comparing min(B[0..I]) to B[0..J] 112 VarInfo seqvar_super = seqvar.isDerivedSubSequenceOf(); 113 if ((seqvar_super != sclvar_seq) && (seqvar_super != sclseqsuper)) { 114 return false; 115 } 116 117 // If the scalar is a positional element of the sequence from which 118 // the sequence at hand was derived, then any relationship will be 119 // (mostly) obvious by comparing the length of the sequence to the 120 // index. By contrast, if the scalar is max(...) or min(...), all bets 121 // are off. 122 if (seqvar.derived instanceof SequenceScalarSubsequence 123 || seqvar.derived instanceof SequenceScalarArbitrarySubsequence) { 124 125 // Determine the left index/shift and right index/shift of the 126 // subsequence. If the left VarInfo is null, the sequence starts 127 // at the beginning. If the right VarInfo is null, the sequence stops 128 // at the end. 129 VarInfo seq_left_index = null; 130 VarInfo seq_right_index = null; 131 int seq_left_shift = 0, seq_right_shift = 0; 132 if (seqvar.derived instanceof SequenceScalarSubsequence) { 133 // the sequence is B[0..J-1] or similar. Get information about it. 134 SequenceScalarSubsequence seqsss = (SequenceScalarSubsequence) seqvar.derived; 135 if (seqsss.from_start) { 136 seq_right_index = seqsss.sclvar(); 137 seq_right_shift = seqsss.index_shift; 138 } else { 139 seq_left_index = seqsss.sclvar(); 140 seq_left_shift = seqsss.index_shift; 141 } 142 } else if (seqvar.derived instanceof SequenceScalarArbitrarySubsequence) { 143 // the sequence is B[I+1..J] or similar 144 SequenceScalarArbitrarySubsequence ssass = (SequenceScalarArbitrarySubsequence) seqvar.derived; 145 seq_left_index = ssass.startvar(); 146 seq_left_shift = (ssass.left_closed ? 0 : 1); 147 seq_right_index = ssass.endvar(); 148 seq_right_shift = (ssass.right_closed ? 0 : -1); 149 } else { 150 throw new Error(); 151 } 152 153 // if the scalar is a a subscript (b[i]) 154 if (sclvar.derived instanceof SequenceScalarSubscript) { 155 156 SequenceScalarSubscript sclsss = (SequenceScalarSubscript) sclvar.derived; 157 VarInfo scl_index = sclsss.sclvar(); // "I" in "B[I]" 158 int scl_shift = sclsss.index_shift; 159 160 // determine if the scalar index is statically included in the 161 // left/right sequence 162 boolean left_included = false, right_included = false; 163 if (seq_left_index == null) { 164 left_included = true; 165 } 166 if (seq_left_index == scl_index) { 167 if (seq_left_shift <= scl_shift) { 168 left_included = true; 169 } 170 } 171 if (seq_right_index == null) { 172 right_included = true; 173 } 174 if (seq_right_index == scl_index) { 175 if (seq_right_shift >= scl_shift) { 176 right_included = true; 177 } 178 } 179 if (left_included && right_included) { 180 return true; 181 } 182 183 // else if the scalar is a specific positional element (eg, b[0]) 184 } else if (sclvar.derived instanceof SequenceInitial) { 185 186 // isObviousImplied: B[0] in B[0..J]; also B[-1] in B[J..] 187 SequenceInitial sclse = (SequenceInitial) sclvar.derived; 188 int scl_index = sclse.index; 189 if (((scl_index == 0) && seq_left_index == null) 190 || ((scl_index == -1) && seq_right_index == null)) 191 // It might not be true, because the array could be empty; 192 // but if the array isn't empty, then it's obvious. The empty 193 // array case is ok, because the variable itself would be 194 // destroyed in that case. 195 return true; 196 197 // else if the scalar is min or max of a sequence 198 } else if ((sclvar.derived instanceof SequenceMin) 199 || (sclvar.derived instanceof SequenceMax)) { 200 IPair<DiscardCode, String> di = SubSequence.isObviousSubSequence(sclvar_seq, seqvar); 201 return di != null; 202 } 203 } 204 205 return false; 206 } 207 208 @Override 209 public String repr(@GuardSatisfied Member this) { 210 return "Member" + varNames() + ": falsified=" + falsified; 211 } 212 213 @SideEffectFree 214 @Override 215 public String format_using(@GuardSatisfied Member this, OutputFormat format) { 216 217 if (format.isJavaFamily()) { 218 return format_java_family(format); 219 } 220 221 if (format == OutputFormat.DAIKON) { 222 return format_daikon(); 223 } else if (format == OutputFormat.SIMPLIFY) { 224 return format_simplify(); 225 } else if (format == OutputFormat.ESCJAVA) { 226 return format_esc(); 227 } else if (format == OutputFormat.CSHARPCONTRACT) { 228 return format_csharp_contract(); 229 } else { 230 return format_unimplemented(format); 231 } 232 } 233 234 public String format_daikon(@GuardSatisfied Member this) { 235 String sclname = sclvar().name(); 236 String seqname = seqvar().name(); 237 return sclname + " in " + seqname; 238 } 239 240 public String format_java() { 241 return "( (daikon.inv.FormatJavaHelper.memberOf(" 242 + sclvar().name() 243 + " , " 244 + seqvar().name() 245 + " ) == true ) "; 246 } 247 248 public String format_java_family(@GuardSatisfied Member this, OutputFormat format) { 249 String sclname = sclvar().name_using(format); 250 String seqname = seqvar().name_using(format); 251 return "daikon.Quant.memberOf(" + sclname + " , " + seqname + " )"; 252 } 253 254 public String format_esc(@GuardSatisfied Member this) { 255 // "exists x in a..b : P(x)" gets written as "!(forall x in a..b : !P(x))" 256 String[] form = VarInfo.esc_quantify(seqvar(), sclvar()); 257 return "!" + form[0] + "(" + form[1] + " != " + form[2] + ")" + form[3]; 258 } 259 260 public String format_csharp_contract(@GuardSatisfied Member this) { 261 String sclname = sclvar().csharp_name(); 262 String[] split = seqvar().csharp_array_split(); 263 return "Contract.Exists(" + split[0] + ", x => x" + split[1] + ".Equals(" + sclname + "))"; 264 } 265 266 public String format_simplify(@GuardSatisfied Member this) { 267 if (Invariant.dkconfig_simplify_define_predicates) { 268 String[] seq_name = seqvar().simplifyNameAndBounds(); 269 String scalar_name = sclvar().simplify_name(); 270 if (seq_name == null) { 271 return String.format( 272 "%s.format_simplify(%s): null seq_name for %s", 273 getClass().getSimpleName(), this, format()); 274 } 275 return "(member " 276 + scalar_name 277 + " " 278 + seq_name[0] 279 + " " 280 + seq_name[1] 281 + " " 282 + seq_name[2] 283 + ")"; 284 } else { 285 // "exists x in a..b : P(x)" gets written as 286 // "!(forall x in a..b : !P(x))" 287 String[] form = VarInfo.simplify_quantify(seqvar(), sclvar()); 288 return "(NOT " + form[0] + "(NEQ " + form[1] + " " + form[2] + ")" + form[3] + ")"; 289 } 290 } 291 292 @Override 293 public InvariantStatus check_modified(long @Interned [] a, long i, int count) { 294 if (a == null) { 295 return InvariantStatus.FALSIFIED; 296 } else if (ArraysPlume.indexOf(a, i) == -1) { 297 return InvariantStatus.FALSIFIED; 298 } 299 return InvariantStatus.NO_CHANGE; 300 } 301 302 @Override 303 public InvariantStatus add_modified(long @Interned [] a, long i, int count) { 304 305 InvariantStatus is = check_modified(a, i, count); 306 if (debug.isLoggable(Level.FINE) && (is == InvariantStatus.FALSIFIED)) { 307 debug.fine( 308 "Member destroyed: " + format() + " because " + i + " not in " + Arrays.toString(a)); 309 } 310 return is; 311 } 312 313 @Override 314 protected double computeConfidence() { 315 return Invariant.CONFIDENCE_JUSTIFIED; 316 } 317 318 @Pure 319 @Override 320 public boolean isSameFormula(Invariant other) { 321 assert other instanceof Member; 322 return true; 323 } 324 325 /** 326 * Checks to see if this is obvious over the specified variables. Implements the following checks: 327 * 328 * <pre> 329 * (0 ≤ i ≤ j) ^ (A[] == B[]) ⇒ A[i] in B[0..j] 330 * (0 ≤ i ≤ j) ^ (A[] == B[]) ⇒ A[j] in B[i..] 331 * (A subset B) ⇒ A[i] in B 332 * </pre> 333 */ 334 @Pure 335 @Override 336 public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) { 337 338 if (Debug.logOn()) { 339 Debug.log(getClass(), ppt.parent, vis, "is obvious check" + format()); 340 } 341 342 DiscardInfo super_result = super.isObviousDynamically(vis); 343 if (super_result != null) { 344 return super_result; 345 } 346 347 // Check for subscript in subsequence 348 DiscardInfo di = subscript_in_subsequence(vis); 349 if (di != null) { 350 return di; 351 } 352 353 // Check for (A subset B) ==> (A[i] member B) 354 di = subset_in_subsequence(vis); 355 if (di != null) { 356 return di; 357 } 358 359 return null; 360 } 361 362 /** 363 * Checks to see if this is obvious over the specified variables. Implements the following check: 364 * 365 * <pre> 366 * (A subset B) ⇒ (A[i] member B) 367 * </pre> 368 */ 369 private @Nullable DiscardInfo subset_in_subsequence(VarInfo[] vis) { 370 371 VarInfo scl_var = sclvar(vis); 372 VarInfo seq_var = seqvar(vis); 373 374 if (Debug.logOn()) { 375 Debug.log(getClass(), ppt.parent, vis, "looking for subset in subseq"); 376 } 377 378 // If the scalar is not a subscript of a seq there is nothing to check. 379 if (scl_var.derived == null) { 380 return null; 381 } 382 if (!(scl_var.derived instanceof SequenceScalarSubscript)) { 383 return null; 384 } 385 SequenceScalarSubscript sssc = (SequenceScalarSubscript) scl_var.derived; 386 if (Debug.logOn()) { 387 Debug.log( 388 getClass(), 389 ppt.parent, 390 vis, 391 "Looking for " + sssc.seqvar().name() + " subset of " + seq_var.name()); 392 } 393 394 // check to see if subscripts sequence is a subset of the sequence var 395 if (ppt.parent.is_subset(sssc.seqvar(), seq_var)) { 396 return new DiscardInfo( 397 this, 398 DiscardCode.obvious, 399 "(" 400 + sssc.seqvar().name() 401 + " subset " 402 + seq_var.name() 403 + ") ==> " 404 + sssc.seqvar().name() 405 + "[" 406 + sssc.sclvar().name() 407 + "] member " 408 + seq_var.name()); 409 } 410 411 return null; 412 } 413 414 /** 415 * Checks to see if this is obvious over the specified variables. Implements the following checks: 416 * 417 * <pre> 418 * (0 ≤ i ≤ j) ^ (a[] == b[]) ⇒ a[i] in b[0..j] 419 * (0 ≤ i ≤ j) ^ (a[] == b[]) ⇒ a[j] in b[i..] 420 * </pre> 421 */ 422 private @Nullable DiscardInfo subscript_in_subsequence(VarInfo[] vis) { 423 424 VarInfo scl_var = sclvar(vis); 425 VarInfo seq_var = seqvar(vis); 426 427 // Both variables must be derived 428 if ((scl_var.derived == null) || (seq_var.derived == null)) { 429 return null; 430 } 431 432 // If the scalar is not SequenceScalarSubscript, there is nothing to check. 433 if (!(scl_var.derived instanceof SequenceScalarSubscript)) { 434 return null; 435 } 436 SequenceScalarSubscript sssc = (SequenceScalarSubscript) scl_var.derived; 437 438 // If the sequence is not SequenceScalarSubsequence, nothing to check 439 if (!(seq_var.derived instanceof SequenceScalarSubsequence)) { 440 return null; 441 } 442 SequenceScalarSubsequence ssss = (SequenceScalarSubsequence) seq_var.derived; 443 444 // Both variables must be derived from equal sequences 445 if (!ppt.parent.is_equal(sssc.seqvar(), ssss.seqvar())) { 446 return null; 447 } 448 449 // if a[i] in a[0..n], look for i <= n 450 if (ssss.from_start) { 451 if (Debug.logOn()) { 452 Debug.log( 453 getClass(), 454 ppt.parent, 455 vis, 456 "Looking for " 457 + sssc.sclvar().name() 458 + sssc.index_shift 459 + " <= " 460 + ssss.sclvar().name() 461 + ssss.index_shift); 462 } 463 if (ppt.parent.is_less_equal( 464 sssc.sclvar(), sssc.index_shift, ssss.sclvar(), ssss.index_shift)) { 465 return new DiscardInfo( 466 this, 467 DiscardCode.obvious, 468 "i <= n ==> a[i] in a[..n] for " + scl_var.name() + " and " + seq_var.name()); 469 } 470 } else { // a[i] in a[n..], look for i >= n 471 if (Debug.logOn()) { 472 Debug.log( 473 getClass(), 474 ppt.parent, 475 vis, 476 "Looking for " 477 + ssss.sclvar().name() 478 + ssss.index_shift 479 + " <= " 480 + sssc.sclvar().name() 481 + sssc.index_shift); 482 } 483 if (ppt.parent.is_less_equal( 484 ssss.sclvar(), ssss.index_shift, sssc.sclvar(), sssc.index_shift)) 485 return new DiscardInfo( 486 this, 487 DiscardCode.obvious, 488 "i >= n ==> a[i] in a[n..] for " + scl_var.name() + " and " + seq_var.name()); 489 } 490 return null; 491 } 492}