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