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 double scalars that are always members of a sequence of double values. Prints as 027 * {@code x in y[]} where {@code x} is a double scalar and {@code y[]} is a sequence 028 * of double. 029 */ 030public final class MemberFloat extends SequenceFloat { 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 MemberFloat(PptSlice ppt) { 041 super(ppt); 042 } 043 044 @Prototype MemberFloat() { 045 super(); 046 } 047 048 private static @Prototype MemberFloat proto = new @Prototype MemberFloat(); 049 050 /** Returns the prototype invariant for MemberFloat. */ 051 public static @Prototype MemberFloat get_proto() { 052 return proto; 053 } 054 055 @Override 056 public boolean enabled() { 057 return dkconfig_enabled; 058 } 059 060 @Override 061 protected MemberFloat instantiate_dyn(@Prototype PptSlice slice) { 062 return new MemberFloat(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 SequenceFloatSubsequence 123 || seqvar.derived instanceof SequenceFloatArbitrarySubsequence) { 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 SequenceFloatSubsequence) { 133 // the sequence is B[0..J-1] or similar. Get information about it. 134 SequenceFloatSubsequence seqsss = (SequenceFloatSubsequence) 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 SequenceFloatArbitrarySubsequence) { 143 // the sequence is B[I+1..J] or similar 144 SequenceFloatArbitrarySubsequence ssass = (SequenceFloatArbitrarySubsequence) 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 SequenceFloatSubscript) { 155 156 SequenceFloatSubscript sclsss = (SequenceFloatSubscript) 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 SequenceInitialFloat) { 185 186 // isObviousImplied: B[0] in B[0..J]; also B[-1] in B[J..] 187 SequenceInitialFloat sclse = (SequenceInitialFloat) 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 = SubSequenceFloat.isObviousSubSequence(sclvar_seq, seqvar); 201 return di != null; 202 } 203 } 204 205 return false; 206 } 207 208 @Override 209 public String repr(@GuardSatisfied MemberFloat this) { 210 return "Member" + varNames() + ": falsified=" + falsified; 211 } 212 213 @SideEffectFree 214 @Override 215 public String format_using(@GuardSatisfied MemberFloat 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.ESCJAVA) { 224 return format_esc(); 225 } else if (format == OutputFormat.CSHARPCONTRACT) { 226 return format_csharp_contract(); 227 } else { 228 return format_unimplemented(format); 229 } 230 } 231 232 public String format_daikon(@GuardSatisfied MemberFloat this) { 233 String sclname = sclvar().name(); 234 String seqname = seqvar().name(); 235 return sclname + " in " + seqname; 236 } 237 238 public String format_java() { 239 return "( (daikon.inv.FormatJavaHelper.memberOf(" 240 + sclvar().name() 241 + " , " 242 + seqvar().name() 243 + " ) == true ) "; 244 } 245 246 public String format_java_family(@GuardSatisfied MemberFloat this, OutputFormat format) { 247 String sclname = sclvar().name_using(format); 248 String seqname = seqvar().name_using(format); 249 return "daikon.Quant.memberOf(" + sclname + " , " + seqname + " )"; 250 } 251 252 public String format_esc(@GuardSatisfied MemberFloat this) { 253 // "exists x in a..b : P(x)" gets written as "!(forall x in a..b : !P(x))" 254 String[] form = VarInfo.esc_quantify(seqvar(), sclvar()); 255 return "!" + form[0] + "(" + form[1] + " != " + form[2] + ")" + form[3]; 256 } 257 258 public String format_csharp_contract(@GuardSatisfied MemberFloat this) { 259 String sclname = sclvar().csharp_name(); 260 String[] split = seqvar().csharp_array_split(); 261 return "Contract.Exists(" + split[0] + ", x => x" + split[1] + ".Equals(" + sclname + "))"; 262 } 263 264 @Override 265 public InvariantStatus check_modified(double @Interned [] a, double i, int count) { 266 if (a == null) { 267 return InvariantStatus.FALSIFIED; 268 } else if (Global.fuzzy.indexOf(a, i) == -1) { 269 return InvariantStatus.FALSIFIED; 270 } 271 return InvariantStatus.NO_CHANGE; 272 } 273 274 @Override 275 public InvariantStatus add_modified(double @Interned [] a, double i, int count) { 276 277 InvariantStatus is = check_modified(a, i, count); 278 if (debug.isLoggable(Level.FINE) && (is == InvariantStatus.FALSIFIED)) { 279 debug.fine( 280 "Member destroyed: " + format() + " because " + i + " not in " + Arrays.toString(a)); 281 } 282 return is; 283 } 284 285 @Override 286 protected double computeConfidence() { 287 return Invariant.CONFIDENCE_JUSTIFIED; 288 } 289 290 @Pure 291 @Override 292 public boolean isSameFormula(Invariant other) { 293 assert other instanceof MemberFloat; 294 return true; 295 } 296 297 /** 298 * Checks to see if this is obvious over the specified variables. Implements the following checks: 299 * 300 * <pre> 301 * (0 ≤ i ≤ j) ^ (A[] == B[]) ⇒ A[i] in B[0..j] 302 * (0 ≤ i ≤ j) ^ (A[] == B[]) ⇒ A[j] in B[i..] 303 * (A subset B) ⇒ A[i] in B 304 * </pre> 305 */ 306 @Pure 307 @Override 308 public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) { 309 310 if (Debug.logOn()) { 311 Debug.log(getClass(), ppt.parent, vis, "is obvious check" + format()); 312 } 313 314 DiscardInfo super_result = super.isObviousDynamically(vis); 315 if (super_result != null) { 316 return super_result; 317 } 318 319 // Check for subscript in subsequence 320 DiscardInfo di = subscript_in_subsequence(vis); 321 if (di != null) { 322 return di; 323 } 324 325 // Check for (A subset B) ==> (A[i] member B) 326 di = subset_in_subsequence(vis); 327 if (di != null) { 328 return di; 329 } 330 331 return null; 332 } 333 334 /** 335 * Checks to see if this is obvious over the specified variables. Implements the following check: 336 * 337 * <pre> 338 * (A subset B) ⇒ (A[i] member B) 339 * </pre> 340 */ 341 private @Nullable DiscardInfo subset_in_subsequence(VarInfo[] vis) { 342 343 VarInfo scl_var = sclvar(vis); 344 VarInfo seq_var = seqvar(vis); 345 346 if (Debug.logOn()) { 347 Debug.log(getClass(), ppt.parent, vis, "looking for subset in subseq"); 348 } 349 350 // If the scalar is not a subscript of a seq there is nothing to check. 351 if (scl_var.derived == null) { 352 return null; 353 } 354 if (!(scl_var.derived instanceof SequenceFloatSubscript)) { 355 return null; 356 } 357 SequenceFloatSubscript sssc = (SequenceFloatSubscript) scl_var.derived; 358 if (Debug.logOn()) { 359 Debug.log( 360 getClass(), 361 ppt.parent, 362 vis, 363 "Looking for " + sssc.seqvar().name() + " subset of " + seq_var.name()); 364 } 365 366 // check to see if subscripts sequence is a subset of the sequence var 367 if (ppt.parent.is_subset(sssc.seqvar(), seq_var)) { 368 return new DiscardInfo( 369 this, 370 DiscardCode.obvious, 371 "(" 372 + sssc.seqvar().name() 373 + " subset " 374 + seq_var.name() 375 + ") ==> " 376 + sssc.seqvar().name() 377 + "[" 378 + sssc.sclvar().name() 379 + "] member " 380 + seq_var.name()); 381 } 382 383 return null; 384 } 385 386 /** 387 * Checks to see if this is obvious over the specified variables. Implements the following checks: 388 * 389 * <pre> 390 * (0 ≤ i ≤ j) ^ (a[] == b[]) ⇒ a[i] in b[0..j] 391 * (0 ≤ i ≤ j) ^ (a[] == b[]) ⇒ a[j] in b[i..] 392 * </pre> 393 */ 394 private @Nullable DiscardInfo subscript_in_subsequence(VarInfo[] vis) { 395 396 VarInfo scl_var = sclvar(vis); 397 VarInfo seq_var = seqvar(vis); 398 399 // Both variables must be derived 400 if ((scl_var.derived == null) || (seq_var.derived == null)) { 401 return null; 402 } 403 404 // If the scalar is not SequenceScalarSubscript, there is nothing to check. 405 if (!(scl_var.derived instanceof SequenceFloatSubscript)) { 406 return null; 407 } 408 SequenceFloatSubscript sssc = (SequenceFloatSubscript) scl_var.derived; 409 410 // If the sequence is not SequenceScalarSubsequence, nothing to check 411 if (!(seq_var.derived instanceof SequenceFloatSubsequence)) { 412 return null; 413 } 414 SequenceFloatSubsequence ssss = (SequenceFloatSubsequence) seq_var.derived; 415 416 // Both variables must be derived from equal sequences 417 if (!ppt.parent.is_equal(sssc.seqvar(), ssss.seqvar())) { 418 return null; 419 } 420 421 // if a[i] in a[0..n], look for i <= n 422 if (ssss.from_start) { 423 if (Debug.logOn()) { 424 Debug.log( 425 getClass(), 426 ppt.parent, 427 vis, 428 "Looking for " 429 + sssc.sclvar().name() 430 + sssc.index_shift 431 + " <= " 432 + ssss.sclvar().name() 433 + ssss.index_shift); 434 } 435 if (ppt.parent.is_less_equal( 436 sssc.sclvar(), sssc.index_shift, ssss.sclvar(), ssss.index_shift)) { 437 return new DiscardInfo( 438 this, 439 DiscardCode.obvious, 440 "i <= n ==> a[i] in a[..n] for " + scl_var.name() + " and " + seq_var.name()); 441 } 442 } else { // a[i] in a[n..], look for i >= n 443 if (Debug.logOn()) { 444 Debug.log( 445 getClass(), 446 ppt.parent, 447 vis, 448 "Looking for " 449 + ssss.sclvar().name() 450 + ssss.index_shift 451 + " <= " 452 + sssc.sclvar().name() 453 + sssc.index_shift); 454 } 455 if (ppt.parent.is_less_equal( 456 ssss.sclvar(), ssss.index_shift, sssc.sclvar(), sssc.index_shift)) 457 return new DiscardInfo( 458 this, 459 DiscardCode.obvious, 460 "i >= n ==> a[i] in a[n..] for " + scl_var.name() + " and " + seq_var.name()); 461 } 462 return null; 463 } 464}