001package daikon; 002 003import daikon.chicory.DaikonVariableInfo; 004import daikon.derive.Derivation; 005import daikon.derive.binary.BinaryDerivation; 006import daikon.derive.binary.SequenceFloatSubscript; 007import daikon.derive.binary.SequenceScalarSubscript; 008import daikon.derive.binary.SequenceStringSubscript; 009import daikon.derive.binary.SequenceSubsequence; 010import daikon.derive.ternary.SequenceFloatArbitrarySubsequence; 011import daikon.derive.ternary.SequenceScalarArbitrarySubsequence; 012import daikon.derive.ternary.SequenceStringArbitrarySubsequence; 013import daikon.derive.unary.SequenceLength; 014import daikon.derive.unary.UnaryDerivation; 015import daikon.inv.OutputFormat; 016import java.io.IOException; 017import java.io.ObjectInputStream; 018import java.io.Serializable; 019import java.lang.ref.WeakReference; 020import java.util.ArrayList; 021import java.util.Arrays; 022import java.util.Collection; 023import java.util.Collections; 024import java.util.Comparator; 025import java.util.HashSet; 026import java.util.List; 027import java.util.ListIterator; 028import java.util.Set; 029import java.util.StringJoiner; 030import java.util.WeakHashMap; 031import java.util.logging.Level; 032import java.util.logging.Logger; 033import org.checkerframework.checker.interning.qual.InternMethod; 034import org.checkerframework.checker.interning.qual.Interned; 035import org.checkerframework.checker.lock.qual.GuardSatisfied; 036import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf; 037import org.checkerframework.checker.nullness.qual.Nullable; 038import org.checkerframework.dataflow.qual.Pure; 039import org.checkerframework.dataflow.qual.SideEffectFree; 040import org.plumelib.util.StringsPlume; 041 042// This class is deprecated. It should be removed as soon as Daikon no 043// longer supports the old decl format. 044 045// If you change this file, also change class daikon.test.VarInfoNameTest. 046 047/** 048 * VarInfoName represents the "name" of a variable. Calling it a "name", however, is somewhat 049 * misleading. It can be some expression that includes more than one variable, term, etc. We 050 * separate this from the VarInfo itself because clients wish to manipulate names into new 051 * expressions independent of the VarInfo that they might be associated with. VarInfoName's child 052 * classes are specific types of names, like applying a function to something. For example, "a" is a 053 * name, and "sin(a)" is a name that is the name "a" with the function "sin" applied to it. 054 */ 055@SuppressWarnings({"nullness", "interning"}) // deprecated file 056public abstract @Interned class VarInfoName implements Serializable, Comparable<VarInfoName> { 057 058 /** Debugging Logger. */ 059 public static Logger debug = Logger.getLogger("daikon.VarInfoName"); 060 061 static final long serialVersionUID = 20020614L; 062 063 /** 064 * When true, apply orig directly to variables, do not apply orig to derived variables. For 065 * example, create 'size(orig(a[]))' rather than 'orig(size(a[]))'. 066 */ 067 public static boolean dkconfig_direct_orig = false; 068 069 /** 070 * Given the standard String representation of a variable name (like what appears in the normal 071 * output format), return the corresponding VarInfoName. This method can't parse all the strings 072 * that the VarInfoName name() method might produce, but it should be able to handle anything that 073 * appears in a decls file. Specifically, it can only handle a subset of the grammar of derived 074 * variables. For some values of "name", "name.equals(parse(e.name()))" might throw an exception, 075 * but if it completes normally, the result should be true. 076 */ 077 public static VarInfoName parse(String name) { 078 079 // Remove the array indication from the new decl format 080 name = name.replace("[..]", "[]"); 081 082 // orig(x) 083 if (name.startsWith("orig(")) { 084 // throw new Error("orig() variables shouldn't appear in .decls files"); 085 assert name.endsWith(")") : name; 086 return parse(name.substring(5, name.length() - 1)).applyPrestate(); 087 } 088 089 // x.class 090 if (name.endsWith(DaikonVariableInfo.class_suffix)) { 091 return parse(name.substring(0, name.length() - DaikonVariableInfo.class_suffix.length())) 092 .applyTypeOf(); 093 } 094 095 // a quoted string 096 if (name.startsWith("\"") && name.endsWith("\"")) { 097 String content = name.substring(1, name.length() - 1); 098 if (content.equals(StringsPlume.escapeJava(StringsPlume.unescapeJava(content)))) { 099 return new Simple(name).intern(); 100 } 101 } 102 103 // x or this.x 104 if ((name.indexOf('[') == -1) && (name.indexOf('(') == -1)) { 105 // checking for only legal characters would be more robust 106 int dot = name.lastIndexOf('.'); 107 int arrow = name.lastIndexOf("->"); 108 if (dot >= 0 && dot > arrow) { 109 String first = name.substring(0, dot); 110 String field = name.substring(dot + 1); 111 return parse(first).applyField(field); 112 } else if (arrow >= 0 && arrow > dot) { 113 String first = name.substring(0, arrow); 114 String field = name.substring(arrow + 2); 115 return parse(first).applyField(field); 116 } else { 117 return new Simple(name).intern(); 118 } 119 } 120 121 // a[] 122 if (name.endsWith("[]")) { 123 return parse(name.substring(0, name.length() - 2)).applyElements(); 124 } 125 126 // foo[bar] -- IOA input only (pre-derived) 127 if (name.endsWith("]")) { 128 // This isn't quite right: we really want the matching open bracket, 129 // not the last open bracket. 130 int lbracket = name.lastIndexOf("["); 131 if (lbracket >= 0) { 132 String seqname = name.substring(0, lbracket) + "[]"; 133 String idxname = name.substring(lbracket + 1, name.length() - 1); 134 VarInfoName seq = parse(seqname); 135 VarInfoName idx = parse(idxname); 136 return seq.applySubscript(idx); 137 } 138 } 139 140 // a[].foo or a[].foo.bar 141 if (name.indexOf("[]") >= 0) { 142 int brackets = name.lastIndexOf("[]"); 143 int dot = name.lastIndexOf('.'); 144 int arrow = name.lastIndexOf("->"); 145 if (dot >= brackets && dot > arrow) { 146 String first = name.substring(0, dot); 147 String field = name.substring(dot + 1); 148 return parse(first).applyField(field); 149 } else if (arrow >= brackets && arrow > dot) { 150 String first = name.substring(0, arrow); 151 String field = name.substring(arrow + 2); 152 return parse(first).applyField(field); 153 } 154 } 155 156 // A.B, where A is complex: foo(x).y, x[7].y, etc. 157 int dot = name.lastIndexOf('.'); 158 int arrow = name.lastIndexOf("->"); 159 if (dot >= 0 && dot > arrow) { 160 String first = name.substring(0, dot); 161 String field = name.substring(dot + 1); 162 return parse(first).applyField(field); 163 } 164 165 // A->B, where A is complex: foo(x)->y, x[7]->y, etc. 166 if (arrow >= 0 && arrow > dot) { 167 String first = name.substring(0, arrow); 168 String field = name.substring(arrow + 2); 169 return parse(first).applyField(field); 170 } 171 172 // New decl format permits arbitrary uninterpreted strings as names 173 if (FileIO.new_decl_format) { 174 return new Simple(name).intern(); 175 } else { 176 throw new UnsupportedOperationException("parse error: '" + name + "'"); 177 } 178 } 179 180 /** 181 * Return the String representation of this name in the default output format. 182 * 183 * @return the string representation (interned) of this name, in the default output format 184 */ 185 @Pure 186 public @Interned String name(@GuardSatisfied VarInfoName this) { 187 if (name_cached == null) { 188 try { 189 name_cached = name_impl().intern(); 190 } catch (RuntimeException e) { 191 System.err.println("repr = " + repr()); 192 throw e; 193 } 194 } 195 return name_cached; 196 } 197 198 private @Interned String name_cached = null; // interned 199 200 /** 201 * Returns the String representation of this name in the default output format. Result is not 202 * interned; the client (name()) does so, then caches the interned value. 203 */ 204 protected abstract String name_impl(@GuardSatisfied VarInfoName this); 205 206 /** 207 * Return the String representation of this name in the esc style output format. 208 * 209 * @return the string representation (interned) of this name, in the esc style output format 210 */ 211 public @Interned String esc_name() { 212 if (esc_name_cached == null) { 213 try { 214 esc_name_cached = esc_name_impl().intern(); 215 } catch (RuntimeException e) { 216 System.err.println("repr = " + repr()); 217 throw e; 218 } 219 } 220 // System.out.println("esc_name = " + esc_name_cached + " for " + name() + " of class " + 221 // this.getClass().getName()); 222 return esc_name_cached; 223 } 224 225 private @Interned String esc_name_cached = null; // interned 226 227 /** 228 * Returns the String representation of this name in the ESC style output format. Cached by {@link 229 * #esc_name()}. 230 */ 231 protected abstract String esc_name_impl(); 232 233 /** 234 * Returns the string representation (interned) of this name, in the Simplify tool output format 235 * in the pre-state context. 236 * 237 * @return the string representation (interned) of this name, in the Simplify tool output format 238 * in the pre-state context 239 */ 240 public @Interned String simplify_name() { 241 return simplify_name(false); 242 } 243 244 /** 245 * Returns the string representation (interned) of this name, in the Simplify tool output format, 246 * in the given pre/post-state context. 247 * 248 * @param prestate if true, return the variable in a prestate context; if false, return the 249 * variable in a poststate context 250 * @return the string representation (interned) of this name, in the Simplify tool output format, 251 * in the given pre/post-state context 252 */ 253 protected @Interned String simplify_name(boolean prestate) { 254 int which = prestate ? 0 : 1; 255 if (simplify_name_cached[which] == null) { 256 try { 257 simplify_name_cached[which] = simplify_name_impl(prestate).intern(); 258 } catch (RuntimeException e) { 259 System.err.println("repr = " + repr()); 260 throw e; 261 } 262 } 263 return simplify_name_cached[which]; 264 } 265 266 // each element is interned 267 private @Interned String[] simplify_name_cached = new @Interned String[2]; 268 269 /** 270 * Returns the String representation of this name in the simplify output format in either prestate 271 * or poststate context. 272 */ 273 protected abstract String simplify_name_impl(boolean prestate); 274 275 /** 276 * Return the String representation of this name in the java style output format. 277 * 278 * @return the string representation (interned) of this name, in the java style output format 279 */ 280 public @Interned String java_name(VarInfo v) { 281 if (java_name_cached == null) { 282 try { 283 java_name_cached = java_name_impl(v).intern(); 284 } catch (RuntimeException e) { 285 System.err.println("repr = " + repr()); 286 throw e; 287 } 288 } 289 return java_name_cached; 290 } 291 292 private @Interned String java_name_cached = null; // interned 293 294 /** 295 * Return the String representation of this name in java format. Cached and interned by {@link 296 * #java_name}. 297 */ 298 protected abstract String java_name_impl(VarInfo v); 299 300 /** Return the String representation of this name in the JML style output format. */ 301 public @Interned String jml_name(VarInfo v) { 302 if (jml_name_cached == null) { 303 try { 304 jml_name_cached = jml_name_impl(v).intern(); 305 } catch (RuntimeException e) { 306 System.err.println("repr = " + repr()); 307 throw e; 308 } 309 } 310 // System.out.println("jml_name = " + jml_name_cached + " for " + name() + " of class " + 311 // this.getClass().getName()); 312 return jml_name_cached; 313 } 314 315 private @Interned String jml_name_cached = null; // interned 316 317 /** Returns the name in JML style output format. Cached and interned by {@link #jml_name}. */ 318 protected abstract String jml_name_impl(VarInfo v); 319 320 // For DBC, Java and JML formats, the formatting methods take as 321 // argument the VarInfo related to the VarInfoName in question. This 322 // causes trouble with VarInfoNameDriver (a class for testing 323 // VarInfoName), because there are no VarInfo's to pass to the 324 // formatting methods. So in places where the VarInfo argument is 325 // required by the formatting code, we use this variable to check 326 // whether we're doing testing. If we are, then we know that the 327 // VarInfo being passed is probably null, and we do something other 328 // than the normal thing (which would probably be to signal an 329 // error). Unfortunately, this prevents testing of some of those 330 // formats that make use of VarInfo information. 331 public static boolean testCall = false; 332 333 /** 334 * Return the String representation of this name in the dbc style output format. 335 * 336 * @param var the VarInfo which goes along with this VarInfoName. Used to determine the type of 337 * the variable. 338 * <p>If var is null, the only repercussion is that if `this' is an "orig(x)" expression, it 339 * will be formatted in jml-style, something like "\old(x)". 340 * <p>If var is not null and `this' is an "orig(x)" expressions, it will be formatted in 341 * Jtest's DBC style, as "$pre(<em>type</em>, x)". 342 * @return the string representation (interned) of this name, in the dbc style output format 343 */ 344 public @Interned String dbc_name(VarInfo var) { 345 if (dbc_name_cached == null) { 346 try { 347 dbc_name_cached = dbc_name_impl(var).intern(); 348 } catch (RuntimeException e) { 349 System.err.println("repr = " + repr()); 350 throw e; 351 } 352 } 353 return dbc_name_cached; 354 } 355 356 private @Interned String dbc_name_cached = null; // interned 357 358 /** 359 * Return the name in the DBC style output format. If v is null, uses JML style instead. Cached 360 * and interned by {@link #dbc_name}. 361 */ 362 protected abstract String dbc_name_impl(VarInfo v); 363 364 /** Return the String representation of this name using only letters, numbers, and underscores. */ 365 public @Interned String identifier_name() { 366 if (identifier_name_cached == null) { 367 try { 368 identifier_name_cached = identifier_name_impl().intern(); 369 } catch (RuntimeException e) { 370 System.err.println("repr = " + repr()); 371 throw e; 372 } 373 } 374 // System.out.println("identifier_name = " + identifier_name_cached + " for " + name() + " of 375 // class " + this.getClass().getName()); 376 return identifier_name_cached; 377 } 378 379 private @Interned String identifier_name_cached = null; // interned 380 381 /** 382 * Returns the name using only letters, numbers, and underscores. Cached and interned by {@link 383 * #identifier_name()}. 384 * 385 * @return the name using only letters, numbers, and underscores 386 */ 387 protected abstract String identifier_name_impl(); 388 389 /** 390 * Returns name of this in the specified format. 391 * 392 * @param format the format in which to return this variable name 393 * @param vi the VarInfo for this variable name 394 * @return name of this in the specified format 395 */ 396 public String name_using(OutputFormat format, VarInfo vi) { 397 398 if (format == OutputFormat.DAIKON) { 399 return name(); 400 } 401 if (format == OutputFormat.SIMPLIFY) { 402 return simplify_name(); 403 } 404 if (format == OutputFormat.ESCJAVA) { 405 return esc_name(); 406 } 407 if (format == OutputFormat.JAVA) { 408 return java_name(vi); 409 } 410 if (format == OutputFormat.JML) { 411 return jml_name(vi); 412 } 413 if (format == OutputFormat.DBCJAVA) { 414 return dbc_name(vi); 415 } 416 throw new UnsupportedOperationException("Unknown format requested: " + format); 417 } 418 419 /** 420 * Returns the name, in a debugging format. 421 * 422 * @return the name, in a debugging format 423 */ 424 public String repr(@GuardSatisfied VarInfoName this) { 425 // AAD: Used to be interned for space reasons, but removed during 426 // profiling when it was determined that the interns are unique 427 // anyway. 428 if (repr_cached == null) { 429 repr_cached = repr_impl(); // .intern(); 430 } 431 return repr_cached; 432 } 433 434 /** The cached output of {@link #repr_impl}, or null. */ 435 private String repr_cached = null; 436 437 /** 438 * Returns the name in a verbose debugging format. Cached by {@link #repr}. 439 * 440 * @return the name in a verbose debugging format 441 */ 442 protected abstract String repr_impl(@GuardSatisfied VarInfoName this); 443 444 // It would be nice if a generalized form of the mechanics of 445 // interning were abstracted out somewhere. 446 private static final WeakHashMap<VarInfoName, WeakReference<VarInfoName>> internTable = 447 new WeakHashMap<>(); 448 449 // This does not make any guarantee that the components of the 450 // VarInfoName are themselves interned. Should it? (I suspect so...) 451 @InternMethod 452 public VarInfoName intern() { 453 WeakReference<VarInfoName> ref = internTable.get(this); 454 if (ref != null) { 455 VarInfoName result = ref.get(); 456 return result; 457 } else { 458 @SuppressWarnings("interning") // intern method 459 @Interned VarInfoName this_interned = this; 460 internTable.put(this_interned, new WeakReference<>(this_interned)); 461 return this_interned; 462 } 463 } 464 465 // ============================================================ 466 // Constants 467 468 public static final VarInfoName ZERO = parse("0"); 469 public static final VarInfoName THIS = parse("this"); 470 public static final VarInfoName ORIG_THIS = parse("this").applyPrestate(); 471 472 // ============================================================ 473 // Observers 474 475 /** 476 * Returns true when this is "0", "-1", "1", etc. 477 * 478 * @return true when this is "0", "-1", "1", etc 479 */ 480 @Pure 481 public boolean isLiteralConstant() { 482 return false; 483 } 484 485 /** 486 * Returns the nodes of this, as given by an inorder traversal. 487 * 488 * @return the nodes of this, as given by an inorder traversal 489 */ 490 public Collection<VarInfoName> inOrderTraversal(@Interned VarInfoName this) { 491 return Collections.unmodifiableCollection(new InorderFlattener(this).nodes()); 492 } 493 494 /** 495 * Returns true iff the given node can be found in this. If the node has children, the whole 496 * subtree must match. 497 * 498 * @param node a variable name 499 * @return true iff the given node can be found in this. If the node has children, the whole 500 * subtree must match 501 */ 502 public boolean hasNode(VarInfoName node) { 503 return inOrderTraversal().contains(node); 504 } 505 506 /** 507 * Returns true iff a node of the given type exists in this. 508 * 509 * @param type the type to search for 510 * @return true iff a node of the given type exists in this 511 */ 512 public boolean hasNodeOfType(Class<?> type) { 513 for (VarInfoName vin : inOrderTraversal()) { 514 if (type.equals(vin.getClass())) { 515 return true; 516 } 517 } 518 return false; 519 } 520 521 /** 522 * Returns true iff a TypeOf node exists in this. 523 * 524 * @return true iff a TypeOf node exists in this 525 */ 526 public boolean hasTypeOf() { 527 return hasNodeOfType(VarInfoName.TypeOf.class); 528 } 529 530 /** 531 * Returns whether or not this name refers to the 'this' variable of a class. True for both normal 532 * and prestate versions of the variable. 533 */ 534 @Pure 535 public boolean isThis() { 536 if (name() == "this") { // interned 537 return true; 538 } 539 if (this instanceof VarInfoName.Prestate 540 && ((VarInfoName.Prestate) this).term.name() == "this") { // interned 541 return true; 542 } 543 544 return false; 545 } 546 547 /** 548 * Returns true if the given node is in a prestate context within this tree. 549 * 550 * @param node a member of this tree 551 * @return true if the given node is in a prestate context within this tree 552 */ 553 public boolean inPrestateContext(@Interned VarInfoName this, VarInfoName node) { 554 return new NodeFinder(this, node).inPre(); 555 } 556 557 /** 558 * Returns true if every variable in the name is an orig(...) variable. 559 * 560 * @return true if every variable in the name is an orig(...) variable 561 */ 562 @Pure 563 public boolean isAllPrestate(@Interned VarInfoName this) { 564 return new IsAllPrestateVisitor(this).result(); 565 } 566 567 /** 568 * Returns true if this VarInfoName contains a simple variable whose name is NAME. 569 * 570 * @param name the name to search for in this VarInfoName 571 * @return true if this VarInfoName contains a simple variable whose name is NAME 572 */ 573 public boolean includesSimpleName(@Interned VarInfoName this, String name) { 574 return new SimpleNamesVisitor(this).simples().contains(name); 575 } 576 577 // ============================================================ 578 // Special producers, or other helpers 579 580 /** Replace the first instance of node by replacement, in the data structure rooted at this. */ 581 public VarInfoName replace( 582 @Interned VarInfoName this, VarInfoName node, VarInfoName replacement) { 583 if (node == replacement) { // "interned": equality optimization pattern 584 return this; 585 } 586 Replacer r = new Replacer(node, replacement); 587 return r.replace(this).intern(); 588 } 589 590 /** Replace all instances of node by replacement, in the data structure rooted at this. */ 591 public VarInfoName replaceAll( 592 @Interned VarInfoName this, VarInfoName node, VarInfoName replacement) { 593 if (node == replacement) { // "interned": equality optimization pattern 594 return this; 595 } 596 597 // assert ! replacement.hasNode(node); // no infinite loop 598 599 // It doesn't make sense to assert this as we have plenty of times when 600 // we want to replace x by y where y may contain x. 601 602 Replacer r = new Replacer(node, replacement); 603 604 // This code used to loop as long as node was in result, but this isn't 605 // necessary -- all occurances are replaced by replacer. 606 607 VarInfoName result = r.replace(this).intern(); 608 return result; 609 } 610 611 // ============================================================ 612 // The usual Object methods 613 614 @EnsuresNonNullIf(result = true, expression = "#1") 615 @Pure 616 @Override 617 public boolean equals(@GuardSatisfied VarInfoName this, @GuardSatisfied @Nullable Object o) { 618 return (o instanceof VarInfoName) && equalsVarInfoName((VarInfoName) o); 619 } 620 621 @EnsuresNonNullIf(result = true, expression = "#1") 622 @Pure 623 public boolean equalsVarInfoName( 624 @GuardSatisfied @Interned VarInfoName this, @GuardSatisfied VarInfoName other) { 625 return ((other == this) // "interned": equality optimization pattern 626 || ((other != null) && this.repr().equals(other.repr()))); 627 } 628 629 // This should be safe even in the absence of caching, because "repr()" 630 // returns a new string each time, but it is equal() to any other 631 // returned string, so their hashCode()s should be the same. 632 @Pure 633 @Override 634 public int hashCode(@GuardSatisfied VarInfoName this) { 635 return repr().hashCode(); 636 } 637 638 @Pure 639 @Override 640 public int compareTo(@GuardSatisfied VarInfoName this, VarInfoName other) { 641 int nameCmp = name().compareTo(other.name()); 642 if (nameCmp != 0) { 643 return nameCmp; 644 } 645 int reprCmp = repr().compareTo(other.repr()); 646 return reprCmp; 647 } 648 649 // This is a debugging method, not intended for ordinary output. 650 // Code producing output should usually call name() rather than 651 // calling toString (perhaps implicitly). 652 @SideEffectFree 653 @Override 654 public String toString(@GuardSatisfied VarInfoName this) { 655 return repr(); 656 } 657 658 // Interning is lost when an object is serialized and deserialized. 659 // Manually re-intern any interned fields upon deserialization. 660 private void readObject(ObjectInputStream in) throws IOException, ClassNotFoundException { 661 in.defaultReadObject(); 662 if (name_cached != null) { 663 name_cached = name_cached.intern(); 664 } 665 if (esc_name_cached != null) { 666 esc_name_cached = esc_name_cached.intern(); 667 } 668 if (simplify_name_cached[0] != null) { 669 simplify_name_cached[0] = simplify_name_cached[0].intern(); 670 } 671 if (simplify_name_cached[1] != null) { 672 simplify_name_cached[1] = simplify_name_cached[1].intern(); 673 } 674 if (java_name_cached != null) { 675 java_name_cached = java_name_cached.intern(); 676 } 677 if (jml_name_cached != null) { 678 jml_name_cached = jml_name_cached.intern(); 679 } 680 if (dbc_name_cached != null) { 681 dbc_name_cached = dbc_name_cached.intern(); 682 } 683 } 684 685 // ============================================================ 686 // Static inner classes that form the expression langugage 687 688 /** A simple identifier like "a", etc. */ 689 public static @Interned class Simple extends VarInfoName { 690 // We are Serializable, so we specify a version to allow changes to 691 // method signatures without breaking serialization. If you add or 692 // remove fields, you should change this number to the current date. 693 static final long serialVersionUID = 20020130L; 694 695 public final String name; 696 697 public Simple(String name) { 698 assert name != null; 699 this.name = name; 700 } 701 702 @Pure 703 @Override 704 public boolean isLiteralConstant() { 705 try { 706 Integer.parseInt(name); 707 return true; 708 } catch (NumberFormatException e) { 709 return false; 710 } 711 } 712 713 @Override 714 protected String repr_impl(@GuardSatisfied Simple this) { 715 return name; 716 } 717 718 @Override 719 protected String name_impl(@GuardSatisfied Simple this) { 720 return name; 721 } 722 723 @Override 724 protected String esc_name_impl() { 725 return "return".equals(name) ? "\\result" : name; 726 } 727 728 @Override 729 protected String simplify_name_impl(boolean prestate) { 730 if (isLiteralConstant()) { 731 return name; 732 } else { 733 return simplify_name_impl(name, prestate); 734 } 735 } 736 737 // Names must be either a legal C/Java style identifier, or 738 // surrounded by vertical bars (Simplify's quoting mechanism); 739 // other than that, they only have to be consistent within one 740 // execution of Daikon. 741 protected static String simplify_name_impl(String s, boolean prestate) { 742 if (s.startsWith("~") && s.endsWith("~")) { 743 s = s.substring(1, s.length() - 2) + ":closure"; 744 } 745 if (prestate) { 746 s = "__orig__" + s; 747 } 748 return "|" + s + "|"; 749 } 750 751 @Override 752 protected String java_name_impl(VarInfo v) { 753 return "return".equals(name) ? "\\result" : name; 754 } 755 756 @Override 757 protected String jml_name_impl(VarInfo v) { 758 return "return".equals(name) ? "\\result" : name; 759 } 760 761 @Override 762 protected String dbc_name_impl(VarInfo v) { 763 if (name.equals("return")) { 764 return "$result"; 765 } else { 766 return name; 767 } 768 } 769 770 @Override 771 protected String identifier_name_impl() { 772 if (name.equals("return")) { 773 return "Daikon_return"; 774 } else if (name.equals("this")) { 775 return "Daikon_this"; 776 } else { 777 StringBuilder buf = new StringBuilder(); 778 for (int i = 0; i < name.length(); i++) { 779 char c = name.charAt(i); 780 if (Character.isLetterOrDigit(c)) buf.append(c); 781 else if (c == '_') buf.append("__"); 782 else if (c == '$') buf.append("_dollar_"); 783 else if (c == ':') buf.append("_colon_"); 784 else if (c == '*') buf.append("star_"); 785 else { 786 throw new Error("Unexpected character in VarInfoName$Simple"); 787 } 788 } 789 return buf.toString(); 790 } 791 } 792 793 @Override 794 public <T> T accept(Visitor<T> v) { 795 return v.visitSimple(this); 796 } 797 } 798 799 /** 800 * Returns true iff applySize will not throw an exception. 801 * 802 * @return true iff applySize will not throw an exception 803 * @see #applySize 804 */ 805 @Pure 806 public boolean isApplySizeSafe() { 807 return new ElementsFinder(this).elems() != null; 808 } 809 810 /** 811 * Returns a name for the size of this (this object should be a sequence). Form is like 812 * "size(a[])" or "a.length". 813 * 814 * @return a name for the size of this 815 */ 816 public VarInfoName applySize(@Interned VarInfoName this) { 817 // The simple approach: 818 // return new SizeOf((Elements) this).intern(); 819 // is wrong because this might be "orig(a[])". 820 if (dkconfig_direct_orig) { 821 return new SizeOf(this).intern(); 822 } else { 823 Elements elems = new ElementsFinder(this).elems(); 824 if (elems == null) { 825 throw new Error( 826 "applySize should have elements to use in " 827 + name() 828 + ";" 829 + Global.lineSep 830 + "that is, " 831 + name() 832 + " does not appear to be a sequence/collection." 833 + Global.lineSep 834 + "Perhaps its name should be suffixed by \"[]\"?" 835 + Global.lineSep 836 + " this.class = " 837 + getClass().getName()); 838 } 839 840 // If this is orig, replace the elems with sizeof, leaving orig 841 // where it is. If it is not orig, simply return the sizeof the 842 // elems (ignoring anthing outside of the elems (like additional 843 // fields or typeof)). This allows this code to work correctly 844 // for variables such as a[].b.c (returns size(a[])) or 845 // a[].getClass().getName() (returns size(a[])) 846 if (this instanceof Prestate) { 847 VarInfoName size = new SizeOf(elems).intern(); 848 return new Prestate(size).intern(); 849 // Replacer r = new Replacer(elems, new SizeOf(elems).intern()); 850 // return r.replace(this).intern(); 851 } else { 852 return new SizeOf(elems).intern(); 853 } 854 } 855 } 856 857 /** 858 * If this is a slice, (potentially in pre-state), return its lower and upper bounds, which can be 859 * subtracted to get one less than its size. 860 */ 861 public @Interned VarInfoName[] getSliceBounds(@Interned VarInfoName this) { 862 VarInfoName vin = this; 863 boolean inPrestate = false; 864 if (vin instanceof Prestate) { 865 inPrestate = true; 866 vin = ((Prestate) vin).term; 867 } 868 while (vin instanceof Field) { 869 vin = ((Field) vin).term; 870 } 871 if (!(vin instanceof Slice)) { 872 return null; 873 } 874 Slice slice = (Slice) vin; 875 @Interned VarInfoName[] ret = new @Interned VarInfoName[2]; 876 if (slice.i != null) { 877 ret[0] = slice.i; 878 } else { 879 ret[0] = ZERO; 880 } 881 if (slice.j != null) { 882 ret[1] = slice.j; 883 } else { 884 ret[1] = slice.sequence.applySize().applyAdd(-1); 885 } 886 if (inPrestate) { 887 ret[0] = ret[0].applyPrestate(); 888 ret[1] = ret[1].applyPrestate(); 889 } 890 return ret; 891 } 892 893 /** The size of a contained sequence; form is like "size(sequence)" or "sequence.length". */ 894 public static @Interned class SizeOf extends VarInfoName { 895 // We are Serializable, so we specify a version to allow changes to 896 // method signatures without breaking serialization. If you add or 897 // remove fields, you should change this number to the current date. 898 static final long serialVersionUID = 20020130L; 899 900 public final VarInfoName sequence; 901 902 public SizeOf(VarInfoName sequence) { 903 assert sequence != null; 904 this.sequence = sequence; 905 } 906 907 @Override 908 protected String repr_impl(@GuardSatisfied SizeOf this) { 909 return "SizeOf[" + sequence.repr() + "]"; 910 } 911 912 @Override 913 protected String name_impl(@GuardSatisfied SizeOf this) { 914 return "size(" + sequence.name() + ")"; 915 916 // I'm not sure how to get this right; seems to require info about 917 // the variable type. 918 // // The result could be either "sequence.length" or "sequence.size()", 919 // // depending on the type of "sequence". 920 // String seqname = sequence.name(); 921 // if (seqname.endsWith("[]") 922 // // This clause is too confusing for C output, where some 923 // // variables get "size(seq)" and some get seq.length. 924 // // && ! seqname.startsWith("::") 925 // ) { 926 // return sequence.term.name() + ".length"; 927 // } else { 928 // return seqname + ".size()"; 929 // } 930 } 931 932 /** Returns the hashcode that is the base of the array. */ 933 @Pure 934 public VarInfoName get_term() { 935 if (sequence instanceof Elements) { 936 return ((Elements) sequence).term; 937 } else if (sequence instanceof Prestate) { 938 VarInfoName term = ((Prestate) sequence).term; 939 return ((Elements) term).term; 940 } 941 throw new RuntimeException("unexpected term in sizeof " + this); 942 } 943 944 @Override 945 protected String esc_name_impl() { 946 return get_term().esc_name() + ".length"; 947 } 948 949 @Override 950 protected String simplify_name_impl(boolean prestate) { 951 return "(arrayLength " + get_term().simplify_name(prestate) + ")"; 952 } 953 954 @Override 955 protected String java_name_impl(VarInfo v) { 956 return java_family_impl(OutputFormat.JAVA, v); 957 } 958 959 @Override 960 protected String jml_name_impl(VarInfo v) { 961 return java_family_impl(OutputFormat.JML, v); 962 } 963 964 @Override 965 protected String dbc_name_impl(VarInfo v) { 966 return java_family_impl(OutputFormat.DBCJAVA, v); 967 } 968 969 protected String java_family_impl(OutputFormat format, VarInfo v) { 970 971 // See declaration of testCall for explanation of this flag. 972 if (testCall) { 973 return "no format when testCall."; 974 } 975 976 assert v != null; 977 assert v.isDerived(); 978 Derivation derived = v.derived; 979 assert derived instanceof SequenceLength; 980 VarInfo seqVarInfo = ((SequenceLength) derived).base; 981 String prefix = get_term().name_using(format, seqVarInfo); 982 return "daikon.Quant.size(" + prefix + ")"; 983 // if (seqVarInfo.type.pseudoDimensions() > seqVarInfo.type.dimensions()) { 984 // if (prefix.startsWith("daikon.Quant.collect")) { 985 // // Quant collect methods returns an array 986 // return prefix + ".length"; 987 // } else { 988 // // It's a Collection 989 // return prefix + ".size()"; 990 // } 991 // } else { 992 // // It's an array 993 // return prefix + ".length"; 994 // } 995 } 996 997 @Override 998 protected String identifier_name_impl() { 999 return "size_of" + sequence.identifier_name() + "___"; 1000 } 1001 1002 @Override 1003 public <T> T accept(Visitor<T> v) { 1004 return v.visitSizeOf(this); 1005 } 1006 } 1007 1008 /** 1009 * Returns a name for a unary function applied to this object. The result is like "sum(this)". 1010 * 1011 * @param function the function to apply 1012 * @return a name for the function applied to this 1013 */ 1014 public VarInfoName applyFunction(@Interned VarInfoName this, String function) { 1015 return new FunctionOf(function, this).intern(); 1016 } 1017 1018 /** 1019 * Returns a name for a function applied to more than one argument. The result is like "sum(var1, 1020 * var2)". 1021 * 1022 * @param function the name of the function 1023 * @param vars the arguments to the function, of type VarInfoName 1024 * @return a name for a function applied to multiple arguments 1025 */ 1026 public static VarInfoName applyFunctionOfN(String function, List<VarInfoName> vars) { 1027 return new FunctionOfN(function, vars).intern(); 1028 } 1029 1030 /** 1031 * Returns a name for a function of more than one argument. The result is like "sum(var1, var2)". 1032 * 1033 * @param function the name of the function 1034 * @param vars the arguments to the function 1035 */ 1036 public static VarInfoName applyFunctionOfN(String function, @Interned VarInfoName[] vars) { 1037 // This causes an odd error with the Interned checker: 1038 // return applyFunctionOfN(function, Arrays.<@Interned VarInfoName>asList(vars)); 1039 return applyFunctionOfN(function, Arrays.asList(vars)); 1040 } 1041 1042 /** A function over a term, like "sum(argument)". */ 1043 public static @Interned class FunctionOf extends VarInfoName { 1044 // We are Serializable, so we specify a version to allow changes to 1045 // method signatures without breaking serialization. If you add or 1046 // remove fields, you should change this number to the current date. 1047 static final long serialVersionUID = 20020130L; 1048 1049 public final String function; 1050 public final VarInfoName argument; 1051 1052 public FunctionOf(String function, VarInfoName argument) { 1053 assert function != null; 1054 assert argument != null; 1055 this.function = function; 1056 this.argument = argument; 1057 } 1058 1059 @Override 1060 protected String repr_impl(@GuardSatisfied FunctionOf this) { 1061 return "FunctionOf{" + function + "}[" + argument.repr() + "]"; 1062 } 1063 1064 @Override 1065 protected String name_impl(@GuardSatisfied FunctionOf this) { 1066 return function + "(" + argument.name() + ")"; 1067 } 1068 1069 @Override 1070 protected String esc_name_impl() { 1071 return "(warning: format_esc() needs to be implemented: " 1072 + function 1073 + " on " 1074 + argument.repr() 1075 + ")"; 1076 } 1077 1078 @Override 1079 protected String simplify_name_impl(boolean prestate) { 1080 return "(warning: format_simplify() needs to be implemented: " 1081 + function 1082 + " on " 1083 + argument.repr() 1084 + ")"; 1085 } 1086 1087 @Override 1088 protected String java_name_impl(VarInfo v) { 1089 return java_family_name_impl(OutputFormat.JAVA, v); 1090 } 1091 1092 @Override 1093 protected String jml_name_impl(VarInfo v) { 1094 return java_family_name_impl(OutputFormat.JML, v); 1095 } 1096 1097 @Override 1098 protected String dbc_name_impl(VarInfo v) { 1099 return java_family_name_impl(OutputFormat.DBCJAVA, v); 1100 } 1101 1102 protected String java_family_name_impl(OutputFormat format, VarInfo v) { 1103 1104 // See declaration of testCall for explanation of this flag. 1105 if (testCall) { 1106 return "no format when testCall."; 1107 } 1108 1109 assert v != null; 1110 assert v.isDerived(); 1111 Derivation derived = v.derived; 1112 assert derived instanceof UnaryDerivation; 1113 VarInfo argVarInfo = ((UnaryDerivation) derived).base; 1114 return "daikon.Quant." + function + "(" + argument.name_using(format, argVarInfo) + ")"; 1115 } 1116 1117 @Override 1118 protected String identifier_name_impl() { 1119 return function + "_of_" + argument.identifier_name() + "___"; 1120 } 1121 1122 @Override 1123 public <T> T accept(Visitor<T> v) { 1124 return v.visitFunctionOf(this); 1125 } 1126 } 1127 1128 /** A function of multiple parameters. */ 1129 public static @Interned class FunctionOfN extends VarInfoName { 1130 /** If you add or remove fields, change this number to the current date. */ 1131 static final long serialVersionUID = 20020130L; 1132 1133 /** The function being invoked. */ 1134 public final String function; 1135 1136 /** The parameters. */ 1137 @SuppressWarnings("serial") 1138 public final List<VarInfoName> args; 1139 1140 /** 1141 * Construct a new function of multiple arguments. 1142 * 1143 * @param function the name of the function 1144 * @param args the arguments to the function, of type VarInfoName 1145 */ 1146 public FunctionOfN(String function, List<VarInfoName> args) { 1147 assert function != null; 1148 assert args != null; 1149 this.args = args; 1150 this.function = function; 1151 } 1152 1153 /** 1154 * Returns a string representation of the elements of this. 1155 * 1156 * @return a string representation of the elements of this 1157 */ 1158 private List<String> elts_repr(@GuardSatisfied FunctionOfN this) { 1159 List<String> elts = new ArrayList<>(args.size()); 1160 for (VarInfoName vin : args) { 1161 elts.add(vin.repr()); 1162 } 1163 return elts; 1164 } 1165 1166 /** 1167 * Return a comma-separated list of element names. 1168 * 1169 * @return comma-separated list of element names 1170 */ 1171 private String elts_repr_commas(@GuardSatisfied FunctionOfN this) { 1172 return String.join(", ", elts_repr()); 1173 } 1174 1175 @Override 1176 protected String repr_impl(@GuardSatisfied FunctionOfN this) { 1177 return "FunctionOfN{" + function + "}[" + elts_repr_commas() + "]"; 1178 } 1179 1180 @Override 1181 protected String name_impl(@GuardSatisfied FunctionOfN this) { 1182 return function + "(" + elts_repr_commas() + ")"; 1183 } 1184 1185 @Override 1186 protected String esc_name_impl() { 1187 return "(warning: format_esc() needs to be implemented: " 1188 + function 1189 + " on " 1190 + elts_repr_commas() 1191 + ")"; 1192 } 1193 1194 @Override 1195 protected String simplify_name_impl(boolean prestate) { 1196 return "(warning: format_simplify() needs to be implemented: " 1197 + function 1198 + " on " 1199 + elts_repr_commas() 1200 + ")"; 1201 } 1202 1203 @Override 1204 protected String java_name_impl(VarInfo v) { 1205 return java_family_name_impl(OutputFormat.JAVA, v); 1206 } 1207 1208 @Override 1209 protected String jml_name_impl(VarInfo v) { 1210 return java_family_name_impl(OutputFormat.JML, v); 1211 } 1212 1213 @Override 1214 protected String dbc_name_impl(VarInfo v) { 1215 return java_family_name_impl(OutputFormat.DBCJAVA, v); 1216 } 1217 1218 // Only works for two-argument functions. There are currently no 1219 // ternary (or greater) function applications in Daikon. 1220 protected String java_family_name_impl(OutputFormat format, VarInfo v) { 1221 1222 // See declaration of testCall for explanation of this flag. 1223 if (testCall) { 1224 return "no format when testCall."; 1225 } 1226 1227 assert v != null; 1228 assert v.isDerived(); 1229 Derivation derived = v.derived; 1230 assert derived instanceof BinaryDerivation; 1231 // || derived instanceof TernaryDerivation); 1232 assert args.size() == 2; 1233 VarInfo arg1VarInfo = ((BinaryDerivation) derived).base1; 1234 VarInfo arg2VarInfo = ((BinaryDerivation) derived).base2; 1235 return "daikon.Quant." 1236 + function 1237 + "(" 1238 + args.get(0).name_using(format, arg1VarInfo) 1239 + ", " 1240 + args.get(1).name_using(format, arg2VarInfo) 1241 + ")"; 1242 } 1243 1244 @Override 1245 protected String identifier_name_impl() { 1246 List<String> elts = new ArrayList<>(args.size()); 1247 for (VarInfoName vin : args) { 1248 elts.add(vin.identifier_name()); 1249 } 1250 return function + "_of_" + String.join("_comma_", elts) + "___"; 1251 } 1252 1253 /** Shortcut getter to avoid repeated type casting. */ 1254 public VarInfoName getArg(int n) { 1255 return args.get(n); 1256 } 1257 1258 @Override 1259 public <T> T accept(Visitor<T> v) { 1260 return v.visitFunctionOfN(this); 1261 } 1262 } 1263 1264 /** 1265 * Returns a name for the intersection of with another sequence, like "intersect(a[], b[])". 1266 * 1267 * @param seq2 the variable to intersect with 1268 * @return the name for the intersection of this and seq2 1269 */ 1270 public VarInfoName applyIntersection(@Interned VarInfoName this, VarInfoName seq2) { 1271 assert seq2 != null; 1272 return new Intersection(this, seq2).intern(); 1273 } 1274 1275 /** 1276 * Intersection of two sequences. Extends FunctionOfN, and the only change is that it does special 1277 * formatting for IOA. 1278 */ 1279 public static @Interned class Intersection extends FunctionOfN { 1280 // We are Serializable, so we specify a version to allow changes to 1281 // method signatures without breaking serialization. If you add or 1282 // remove fields, you should change this number to the current date. 1283 static final long serialVersionUID = 20020130L; 1284 1285 public Intersection(VarInfoName seq1, VarInfoName seq2) { 1286 super("intersection", Arrays.asList(seq1, seq2)); 1287 } 1288 } 1289 1290 /** 1291 * Returns a name for the union of this with another sequence, like "union(a[], b[])". 1292 * 1293 * @param seq2 the variable to union with 1294 * @return the name for the intersection of this and seq2 1295 */ 1296 public VarInfoName applyUnion(@Interned VarInfoName this, VarInfoName seq2) { 1297 assert seq2 != null; 1298 return new Union(this, seq2).intern(); 1299 } 1300 1301 /** 1302 * Union of two sequences. Extends FunctionOfN, and the only change is that it does special 1303 * formatting for IOA. 1304 */ 1305 public static @Interned class Union extends FunctionOfN { 1306 // We are Serializable, so we specify a version to allow changes to 1307 // method signatures without breaking serialization. If you add or 1308 // remove fields, you should change this number to the current date. 1309 static final long serialVersionUID = 20020130L; 1310 1311 public Union(VarInfoName seq1, VarInfoName seq2) { 1312 super("intersection", Arrays.asList(seq1, seq2)); 1313 } 1314 } 1315 1316 /** 1317 * Returns a 'getter' operation for some field of this name, like a.foo if this is a. 1318 * 1319 * @param field the field 1320 * @return the name for the given field of this 1321 */ 1322 public VarInfoName applyField(@Interned VarInfoName this, String field) { 1323 return new Field(this, field).intern(); 1324 } 1325 1326 /** A 'getter' operation for some field, like a.foo. */ 1327 public static @Interned class Field extends VarInfoName { 1328 // We are Serializable, so we specify a version to allow changes to 1329 // method signatures without breaking serialization. If you add or 1330 // remove fields, you should change this number to the current date. 1331 static final long serialVersionUID = 20020130L; 1332 1333 public final VarInfoName term; 1334 public final String field; 1335 1336 public Field(VarInfoName term, String field) { 1337 assert term != null; 1338 assert field != null; 1339 this.term = term; 1340 this.field = field; 1341 } 1342 1343 @Override 1344 protected String repr_impl(@GuardSatisfied Field this) { 1345 return "Field{" + field + "}[" + term.repr() + "]"; 1346 } 1347 1348 @Override 1349 protected String name_impl(@GuardSatisfied Field this) { 1350 return term.name() + "." + field; 1351 } 1352 1353 @Override 1354 protected String esc_name_impl() { 1355 return term.esc_name() + "." + field; 1356 } 1357 1358 @Override 1359 protected String simplify_name_impl(boolean prestate) { 1360 return "(select " 1361 + Simple.simplify_name_impl(field, false) 1362 + " " 1363 + term.simplify_name(prestate) 1364 + ")"; 1365 } 1366 1367 @Override 1368 protected String java_name_impl(VarInfo v) { 1369 return java_family_name(OutputFormat.JAVA, v); 1370 } 1371 1372 @Override 1373 protected String jml_name_impl(VarInfo v) { 1374 return java_family_name(OutputFormat.JML, v); 1375 } 1376 1377 @Override 1378 protected String dbc_name_impl(VarInfo v) { 1379 return java_family_name(OutputFormat.DBCJAVA, v); 1380 } 1381 1382 // Special case: the fake "toString" field in Daikon is output 1383 // with parens, so that it's legal Java. 1384 protected String java_field(String f) { 1385 if (f.equals("toString")) { 1386 return "toString()"; 1387 } else { 1388 return f; 1389 } 1390 } 1391 1392 // For JAVA, JML and DBC formats. 1393 protected String java_family_name(OutputFormat format, VarInfo v) { 1394 1395 // See declaration of testCall for explanation of this flag. 1396 if (testCall) { 1397 return "no format when testCall."; 1398 } 1399 1400 if (term.name().indexOf("..") != -1) { 1401 // We cannot translate arr[i..].x because this translates into 1402 // 1403 // "daikon.Quant.collect(daikon.Quant.slice(arr,i,arr.length),"x")" 1404 // 1405 // but slice() returns an array of Objects, so an error will 1406 // occur when method collect() tries to query for field "x". 1407 return "(warning: " 1408 + format 1409 + " format cannot express a field applied to a slice:" 1410 + " [repr=" 1411 + repr() 1412 + "])"; 1413 } 1414 1415 boolean hasBrackets = (term.name().indexOf("[]") != -1); 1416 1417 if (format == OutputFormat.JAVA) { 1418 assert !hasBrackets || v.type.dimensions() > 0 1419 : "hasBrackets:" + hasBrackets + ", dimensions:" + v.type.dimensions() + ", v:" + v; 1420 } 1421 1422 if (!hasBrackets && format != OutputFormat.JAVA) { 1423 // Case 1: Not an array collection 1424 String term_name = null; 1425 if (format == OutputFormat.JML) { 1426 term_name = term.jml_name(v); 1427 } else { 1428 term_name = term.dbc_name(v); 1429 } 1430 return term_name + "." + java_field(field); 1431 } 1432 1433 // Case 2: An array collection 1434 1435 // How to translate foo[].f, which is the array obtained from 1436 // collecting o.f for every element o in the array foo? Just as 1437 // we did for slices, we'll translate this into a call of an 1438 // external function to do the job: 1439 1440 // x.y.foo[].bar.f 1441 // ---translates-into---> 1442 // daikon.Quant.collect_TYPE_(x, "y.foo[].bar.f") 1443 1444 // The method Quant.collect takes care of the "y.foo[].bar.f" 1445 // mess for object x. 1446 1447 if (field.equals("toString")) { 1448 return "(warning: " 1449 + format 1450 + " format cannot express a slice with String objects:" 1451 + " obtained by toString(): [repr=" 1452 + repr() 1453 + "])"; 1454 } 1455 1456 String term_name_no_brackets = term.name().replaceAll("\\[\\]", "") + "." + field; 1457 1458 @SuppressWarnings("keyfor") // PACKAGE_NAME is always a key 1459 String packageName = v.aux.getValue(VarInfoAux.PACKAGE_NAME); 1460 if (packageName.equals(VarInfoAux.NO_PACKAGE_NAME)) { 1461 packageName = ""; 1462 } 1463 1464 String[] splits; 1465 boolean isStatic = false; 1466 String packageNamePrefix = null; 1467 // if (isStatic) { 1468 if (term_name_no_brackets.startsWith(packageName + ".")) { 1469 // throw new Error("packageName=" + packageName + ", term_name_no_brackets=" + 1470 // term_name_no_brackets); 1471 // } 1472 // Before splitting, remove the package name. 1473 packageNamePrefix = (packageName.equals("") ? "" : packageName + "."); 1474 isStatic = true; 1475 splits = term_name_no_brackets.substring(packageNamePrefix.length()).split("\\."); 1476 } else { 1477 packageNamePrefix = ""; 1478 isStatic = false; 1479 splits = term_name_no_brackets.split("\\."); 1480 } 1481 1482 String object = splits[0]; 1483 if (isStatic) { 1484 object += DaikonVariableInfo.class_suffix; 1485 } 1486 if (object.equals("return")) { 1487 if (format == OutputFormat.DBCJAVA) { 1488 object = "$return"; 1489 } else { 1490 object = "\\result"; 1491 } 1492 } 1493 1494 String fields = ""; 1495 for (int j = 1; j < splits.length; j++) { 1496 if (j != 1) { 1497 fields += "."; 1498 } 1499 fields += splits[j]; 1500 } 1501 1502 String collectType = (v.type.baseIsPrimitive() ? v.type.base() : "Object"); 1503 1504 if (format == OutputFormat.JAVA) { 1505 return 1506 // On one line to enable searches for "collect.*_field". 1507 "daikon.Quant.collect" 1508 + collectType 1509 + (!v.is_array() ? "_field" : "") 1510 + "(" 1511 + packageNamePrefix 1512 + object 1513 + ", " 1514 + "\"" 1515 + fields 1516 + "\"" 1517 + ")"; 1518 } else { 1519 return "daikon.Quant.collect" 1520 + collectType 1521 + "(" 1522 + packageNamePrefix 1523 + object 1524 + ", " 1525 + "\"" 1526 + fields 1527 + "\"" 1528 + ")"; 1529 } 1530 } 1531 1532 @Override 1533 protected String identifier_name_impl() { 1534 return term.identifier_name() + "_dot_" + field; 1535 } 1536 1537 @Override 1538 public <T> T accept(Visitor<T> v) { 1539 return v.visitField(this); 1540 } 1541 } 1542 1543 /** 1544 * Returns a name for the type of this object; form is like "this.getClass().getName()" or 1545 * "\typeof(this)". 1546 * 1547 * @return the name for the type of this object 1548 */ 1549 public VarInfoName applyTypeOf(@Interned VarInfoName this) { 1550 return new TypeOf(this).intern(); 1551 } 1552 1553 /** The type of the term, like "term.getClass().getName()" or "\typeof(term)". */ 1554 public static @Interned class TypeOf extends VarInfoName { 1555 // We are Serializable, so we specify a version to allow changes to 1556 // method signatures without breaking serialization. If you add or 1557 // remove fields, you should change this number to the current date. 1558 static final long serialVersionUID = 20020130L; 1559 1560 public final VarInfoName term; 1561 1562 public TypeOf(VarInfoName term) { 1563 assert term != null; 1564 this.term = term; 1565 } 1566 1567 @Override 1568 protected String repr_impl(@GuardSatisfied TypeOf this) { 1569 return "TypeOf[" + term.repr() + "]"; 1570 } 1571 1572 @Override 1573 protected String name_impl(@GuardSatisfied TypeOf this) { 1574 return term.name() + DaikonVariableInfo.class_suffix; 1575 } 1576 1577 @Override 1578 protected String esc_name_impl() { 1579 return "\\typeof(" + term.esc_name() + ")"; 1580 } 1581 1582 @Override 1583 protected String simplify_name_impl(boolean prestate) { 1584 return "(typeof " + term.simplify_name(prestate) + ")"; 1585 } 1586 1587 @SideEffectFree 1588 protected String javaFamilyFormat(String varname, boolean isArray) { 1589 if (isArray) { 1590 return "daikon.Quant.typeArray(" + varname + ")"; 1591 } else { 1592 return varname + DaikonVariableInfo.class_suffix; 1593 } 1594 } 1595 1596 @Override 1597 protected String java_name_impl(VarInfo v) { 1598 if (testCall) { 1599 return "no format when testCall."; 1600 } 1601 return javaFamilyFormat(term.java_name(v), v.type.isArray()); 1602 } 1603 1604 @Override 1605 protected String jml_name_impl(VarInfo v) { 1606 if (testCall) { 1607 return "no format when testCall."; 1608 } 1609 return javaFamilyFormat(term.jml_name(v), v.type.isArray()); 1610 } 1611 1612 @Override 1613 protected String dbc_name_impl(VarInfo v) { 1614 if (testCall) { 1615 return "no format when testCall."; 1616 } 1617 return javaFamilyFormat(term.dbc_name(v), v.type.isArray()); 1618 } 1619 1620 @Override 1621 protected String identifier_name_impl() { 1622 return "type_of_" + term.identifier_name() + "___"; 1623 } 1624 1625 @Override 1626 public <T> T accept(Visitor<T> v) { 1627 return v.visitTypeOf(this); 1628 } 1629 } 1630 1631 /** 1632 * Returns a name for a the prestate value of this object; form is like "orig(this)" or 1633 * "\old(this)". 1634 */ 1635 public VarInfoName applyPrestate(@Interned VarInfoName this) { 1636 if (this instanceof Poststate) { 1637 return ((Poststate) this).term; 1638 } else if ((this instanceof Add) && ((Add) this).term instanceof Poststate) { 1639 Add a = (Add) this; 1640 Poststate p = (Poststate) a.term; 1641 return p.term.applyAdd(a.amount); 1642 } else { 1643 return new Prestate(this).intern(); 1644 } 1645 } 1646 1647 /** The prestate value of a term, like "orig(term)" or "\old(term)". */ 1648 public static @Interned class Prestate extends VarInfoName { 1649 // We are Serializable, so we specify a version to allow changes to 1650 // method signatures without breaking serialization. If you add or 1651 // remove fields, you should change this number to the current date. 1652 static final long serialVersionUID = 20020130L; 1653 1654 public final VarInfoName term; 1655 1656 public Prestate(VarInfoName term) { 1657 assert term != null; 1658 this.term = term; 1659 } 1660 1661 @Override 1662 protected String repr_impl(@GuardSatisfied Prestate this) { 1663 return "Prestate[" + term.repr() + "]"; 1664 } 1665 1666 @Override 1667 protected String name_impl(@GuardSatisfied Prestate this) { 1668 return "orig(" + term.name() + ")"; 1669 } 1670 1671 @Override 1672 protected String esc_name_impl() { 1673 return "\\old(" + term.esc_name() + ")"; 1674 } 1675 1676 @Override 1677 protected String simplify_name_impl(boolean prestate) { 1678 return term.simplify_name(true); 1679 } 1680 1681 @Override 1682 protected String java_name_impl(VarInfo v) { 1683 if (PrintInvariants.dkconfig_replace_prestate) { 1684 return PrintInvariants.addPrestateExpression(term.java_name(v)); 1685 } 1686 return "\\old(" + term.java_name(v) + ")"; 1687 } 1688 1689 @Override 1690 protected String jml_name_impl(VarInfo v) { 1691 return "\\old(" + term.jml_name(v) + ")"; 1692 } 1693 1694 @Override 1695 protected String dbc_name_impl(VarInfo v) { 1696 1697 // See declaration of testCall for explanation of this flag. 1698 if (testCall) { 1699 return "no format when testCall."; 1700 } 1701 1702 String brackets = ""; 1703 assert v != null; 1704 String preType = v.type.base(); 1705 if ((term instanceof Slice) 1706 // Slices are obtained by calling daikon.Quant.slice(...) 1707 // which returns things of type java.lang.Object 1708 && v.type.dimensions() > 0 1709 && v.type.base().equals("java.lang.Object")) { 1710 preType = "java.lang.Object"; 1711 } 1712 for (int i = 0; i < v.type.dimensions(); i++) { 1713 brackets += "[]"; 1714 } 1715 return "$pre(" + preType + brackets + ", " + term.dbc_name(v) + ")"; 1716 } 1717 1718 @Override 1719 protected String identifier_name_impl() { 1720 return "orig_of_" + term.identifier_name() + "___"; 1721 } 1722 1723 @Override 1724 public <T> T accept(Visitor<T> v) { 1725 return v.visitPrestate(this); 1726 } 1727 } 1728 1729 // sansOrig() 1730 // int origpos = s.indexOf("orig("); 1731 // assert origpos != -1; 1732 // int rparenpos = s.lastIndexOf(")"); 1733 // return s.substring(0, origpos) 1734 // + s.substring(origpos+5, rparenpos) 1735 // + s.substring(rparenpos+1); 1736 1737 // int origpos = s.indexOf("\\old("); 1738 // assert origpos != -1; 1739 // int rparenpos = s.lastIndexOf(")"); 1740 // return s.substring(0, origpos) 1741 // + s.substring(origpos+5, rparenpos) 1742 // + s.substring(rparenpos+1); 1743 1744 /** 1745 * Returns a name for a the poststate value of this object; form is like "new(this)" or 1746 * "\new(this)". 1747 * 1748 * @return the name for the poststate value of this object 1749 */ 1750 public VarInfoName applyPoststate(@Interned VarInfoName this) { 1751 return new Poststate(this).intern(); 1752 } 1753 1754 /** 1755 * The poststate value of a term, like "new(term)". Only used within prestate, so like 1756 * "orig(this.myArray[new(index)]". 1757 */ 1758 public static @Interned class Poststate extends VarInfoName { 1759 // We are Serializable, so we specify a version to allow changes to 1760 // method signatures without breaking serialization. If you add or 1761 // remove fields, you should change this number to the current date. 1762 static final long serialVersionUID = 20020130L; 1763 1764 public final VarInfoName term; 1765 1766 public Poststate(VarInfoName term) { 1767 assert term != null; 1768 this.term = term; 1769 } 1770 1771 @Override 1772 protected String repr_impl(@GuardSatisfied Poststate this) { 1773 return "Poststate[" + term.repr() + "]"; 1774 } 1775 1776 @Override 1777 protected String name_impl(@GuardSatisfied Poststate this) { 1778 return "post(" + term.name() + ")"; 1779 } 1780 1781 @Override 1782 protected String esc_name_impl() { 1783 return "\\new(" + term.esc_name() + ")"; 1784 } 1785 1786 @Override 1787 protected String simplify_name_impl(boolean prestate) { 1788 return term.simplify_name(false); 1789 } 1790 1791 @Override 1792 protected String java_name_impl(VarInfo v) { 1793 return "\\post(" + term.java_name(v) + ")"; 1794 } 1795 1796 @Override 1797 protected String jml_name_impl(VarInfo v) { 1798 return "\\new(" + term.jml_name(v) + ")"; 1799 // return "(warning: JML format cannot express a Poststate" 1800 // + " [repr=" + repr() + "])"; 1801 } 1802 1803 @Override 1804 protected String dbc_name_impl(VarInfo v) { 1805 return "(warning: DBC format cannot express a Poststate [repr=" + repr() + "])"; 1806 } 1807 1808 @Override 1809 protected String identifier_name_impl() { 1810 return "post_of_" + term.identifier_name() + "___"; 1811 } 1812 1813 @Override 1814 public <T> T accept(Visitor<T> v) { 1815 return v.visitPoststate(this); 1816 } 1817 } 1818 1819 /** Returns a name for the this term plus a constant, like "this-1" or "this+1". */ 1820 public VarInfoName applyAdd(@Interned VarInfoName this, int amount) { 1821 if (amount == 0) { 1822 return this; 1823 } else { 1824 return new Add(this, amount).intern(); 1825 } 1826 } 1827 1828 /** An integer amount more or less than some other value, like "x+2". */ 1829 public static @Interned class Add extends VarInfoName { 1830 // We are Serializable, so we specify a version to allow changes to 1831 // method signatures without breaking serialization. If you add or 1832 // remove fields, you should change this number to the current date. 1833 static final long serialVersionUID = 20020130L; 1834 1835 public final VarInfoName term; 1836 public final int amount; 1837 1838 public Add(VarInfoName term, int amount) { 1839 assert term != null; 1840 this.term = term; 1841 this.amount = amount; 1842 } 1843 1844 private String amount(@GuardSatisfied Add this) { 1845 return (amount < 0) ? String.valueOf(amount) : "+" + amount; 1846 } 1847 1848 @Override 1849 protected String repr_impl(@GuardSatisfied Add this) { 1850 return "Add{" + amount() + "}[" + term.repr() + "]"; 1851 } 1852 1853 @Override 1854 protected String name_impl(@GuardSatisfied Add this) { 1855 return term.name() + amount(); 1856 } 1857 1858 @Override 1859 protected String esc_name_impl() { 1860 return term.esc_name() + amount(); 1861 } 1862 1863 @Override 1864 protected String simplify_name_impl(boolean prestate) { 1865 return (amount < 0) 1866 ? "(- " + term.simplify_name(prestate) + " " + -amount + ")" 1867 : "(+ " + term.simplify_name(prestate) + " " + amount + ")"; 1868 } 1869 1870 @Override 1871 protected String java_name_impl(VarInfo v) { 1872 return term.java_name(v) + amount(); 1873 } 1874 1875 @Override 1876 protected String jml_name_impl(VarInfo v) { 1877 return term.jml_name(v) + amount(); 1878 } 1879 1880 @Override 1881 protected String dbc_name_impl(VarInfo v) { 1882 return term.dbc_name(v) + amount(); 1883 } 1884 1885 @Override 1886 protected String identifier_name_impl() { 1887 if (amount >= 0) { 1888 return term.identifier_name() + "_plus" + amount; 1889 } else { 1890 return term.identifier_name() + "_minus" + -amount; 1891 } 1892 } 1893 1894 @Override 1895 public <T> T accept(Visitor<T> v) { 1896 return v.visitAdd(this); 1897 } 1898 1899 // override for cleanliness 1900 @Override 1901 public VarInfoName applyAdd(int _amount) { 1902 int amt = _amount + this.amount; 1903 return (amt == 0) ? term : term.applyAdd(amt); 1904 } 1905 } 1906 1907 /** Returns a name for the decrement of this term, like "this-1". */ 1908 public VarInfoName applyDecrement(@Interned VarInfoName this) { 1909 return applyAdd(-1); 1910 } 1911 1912 /** Returns a name for the increment of this term, like "this+1". */ 1913 public VarInfoName applyIncrement(@Interned VarInfoName this) { 1914 return applyAdd(+1); 1915 } 1916 1917 /** 1918 * Returns a name for the elements of a container (as opposed to the identity of the container) 1919 * like "this[]" or "(elements this)". 1920 * 1921 * @return the name for the elements of this container 1922 */ 1923 public VarInfoName applyElements(@Interned VarInfoName this) { 1924 return new Elements(this).intern(); 1925 } 1926 1927 /** The elements of a container, like "term[]". */ 1928 public static @Interned class Elements extends VarInfoName { 1929 // We are Serializable, so we specify a version to allow changes to 1930 // method signatures without breaking serialization. If you add or 1931 // remove fields, you should change this number to the current date. 1932 static final long serialVersionUID = 20020130L; 1933 1934 public final VarInfoName term; 1935 1936 public Elements(VarInfoName term) { 1937 assert term != null; 1938 this.term = term; 1939 } 1940 1941 @Override 1942 protected String repr_impl(@GuardSatisfied Elements this) { 1943 return "Elements[" + term.repr() + "]"; 1944 } 1945 1946 @Override 1947 protected String name_impl(@GuardSatisfied Elements this) { 1948 return name_impl(""); 1949 } 1950 1951 protected String name_impl(@GuardSatisfied Elements this, String index) { 1952 return term.name() + "[" + index + "]"; 1953 } 1954 1955 @Override 1956 protected String esc_name_impl() { 1957 throw new UnsupportedOperationException( 1958 "ESC cannot format an unquantified sequence of elements [repr=" + repr() + "]"); 1959 } 1960 1961 protected String esc_name_impl(String index) { 1962 return term.esc_name() + "[" + index + "]"; 1963 } 1964 1965 @Override 1966 protected String simplify_name_impl(boolean prestate) { 1967 return "(select elems " + term.simplify_name(prestate) + ")"; 1968 } 1969 1970 @Override 1971 protected String java_name_impl(VarInfo v) { 1972 return term.java_name(v); 1973 } 1974 1975 protected String java_name_impl(String index, VarInfo v) { 1976 return java_family_impl(OutputFormat.JAVA, v, index); 1977 } 1978 1979 @Override 1980 protected String jml_name_impl(VarInfo v) { 1981 return term.jml_name(v); 1982 } 1983 1984 protected String jml_name_impl(String index, VarInfo v) { 1985 return java_family_impl(OutputFormat.JML, v, index); 1986 } 1987 1988 @Override 1989 protected String dbc_name_impl(VarInfo v) { 1990 return term.dbc_name(v); 1991 } 1992 1993 protected String dbc_name_impl(String index, VarInfo v) { 1994 return java_family_impl(OutputFormat.DBCJAVA, v, index); 1995 } 1996 1997 protected String java_family_impl(OutputFormat format, VarInfo v, String index) { 1998 1999 // If the collection goes through daikon.Quant.collect___, then 2000 // it will be returned as an array no matter what. 2001 String formatted = term.name_using(format, v); 2002 String collectType = (v.type.baseIsPrimitive() ? v.type.base() : "Object"); 2003 return "daikon.Quant.getElement_" + collectType + "(" + formatted + ", " + index + ")"; 2004 // // XXX temporary fix: sometimes long is passed as index. 2005 // // I can't find where the VarInfo for "index" is found. Wherever that is, 2006 // // we should check if its type is long, and do the casting only for that 2007 // // case. 2008 // if (formatted.startsWith("daikon.Quant.collect")) { 2009 // return formatted + "[(int)" + index + "]"; 2010 // } else { 2011 // if (v.type.pseudoDimensions() > v.type.dimensions()) { 2012 // // it's a collection 2013 // return formatted + ".get((int)" + index + ")"; 2014 // } else { 2015 // // it's an array 2016 // return formatted + "[(int)" + index + "]"; 2017 // } 2018 // } 2019 } 2020 2021 protected String identifier_name_impl(String index) { 2022 if (index.equals("")) { 2023 return term.identifier_name() + "_elems"; 2024 } else { 2025 return term.identifier_name() + "_in_" + index + "_dex_"; 2026 } 2027 } 2028 2029 @Override 2030 protected String identifier_name_impl() { 2031 return identifier_name_impl(""); 2032 } 2033 2034 @Override 2035 public <T> T accept(Visitor<T> v) { 2036 return v.visitElements(this); 2037 } 2038 2039 public VarInfoName getLowerBound() { 2040 return ZERO; 2041 } 2042 2043 public VarInfoName getUpperBound() { 2044 return applySize().applyDecrement(); 2045 } 2046 2047 public VarInfoName getSubscript(VarInfoName index) { 2048 return applySubscript(index); 2049 } 2050 } 2051 2052 /** 2053 * Caller is subscripting an orig(a[]) array. Take the requested index and make it useful in that 2054 * context. 2055 */ 2056 static VarInfoName indexToPrestate(VarInfoName index) { 2057 // 1 orig(a[]) . orig(index) -> orig(a[index]) 2058 // 2 orig(a[]) . index -> orig(a[post(index)]) 2059 if (index instanceof Prestate) { 2060 index = ((Prestate) index).term; // #1 2061 } else if (index instanceof Add) { 2062 Add add = (Add) index; 2063 if (add.term instanceof Prestate) { 2064 index = ((Prestate) add.term).term.applyAdd(add.amount); // #1 2065 } else { 2066 index = index.applyPoststate(); // #2 2067 } 2068 } else if (index.isLiteralConstant()) { 2069 // we don't want orig(a[post(0)]), so leave index alone 2070 } else { 2071 index = index.applyPoststate(); // #2 2072 } 2073 return index; 2074 } 2075 2076 /** Returns a name for an element selected from a sequence, like "this[i]". */ 2077 public VarInfoName applySubscript(@Interned VarInfoName this, VarInfoName index) { 2078 assert index != null; 2079 ElementsFinder finder = new ElementsFinder(this); 2080 Elements elems = finder.elems(); 2081 assert elems != null : "applySubscript should have elements to use in " + this; 2082 if (finder.inPre()) { 2083 index = indexToPrestate(index); 2084 } 2085 Replacer r = new Replacer(elems, new Subscript(elems, index).intern()); 2086 return r.replace(this).intern(); 2087 } 2088 2089 // Given a sequence and subscript index, convert the index to an 2090 // explicit form if necessary (e.g. a[-1] becomes a[a.length-1]). 2091 // Result is not interned, because it is only ever used for printing. 2092 static VarInfoName indexExplicit(Elements sequence, VarInfoName index) { 2093 if (!index.isLiteralConstant()) { 2094 return index; 2095 } 2096 2097 int i = Integer.parseInt(index.name()); 2098 if (i >= 0) { 2099 return index; 2100 } 2101 2102 return sequence.applySize().applyAdd(i); 2103 } 2104 2105 /** An element from a sequence, like "sequence[index]". */ 2106 public static @Interned class Subscript extends VarInfoName { 2107 // We are Serializable, so we specify a version to allow changes to 2108 // method signatures without breaking serialization. If you add or 2109 // remove fields, you should change this number to the current date. 2110 static final long serialVersionUID = 20020130L; 2111 2112 public final Elements sequence; 2113 public final VarInfoName index; 2114 2115 public Subscript(Elements sequence, VarInfoName index) { 2116 assert sequence != null; 2117 assert index != null; 2118 this.sequence = sequence; 2119 this.index = index; 2120 } 2121 2122 @Override 2123 protected String repr_impl(@GuardSatisfied Subscript this) { 2124 return "Subscript{" + index.repr() + "}[" + sequence.repr() + "]"; 2125 } 2126 2127 @Override 2128 protected String name_impl(@GuardSatisfied Subscript this) { 2129 return sequence.name_impl(index.name()); 2130 } 2131 2132 @Override 2133 protected String esc_name_impl() { 2134 return sequence.esc_name_impl(indexExplicit(sequence, index).esc_name()); 2135 } 2136 2137 @Override 2138 protected String simplify_name_impl(boolean prestate) { 2139 return "(select " 2140 + sequence.simplify_name(prestate) 2141 + " " 2142 + indexExplicit(sequence, index).simplify_name(prestate) 2143 + ")"; 2144 } 2145 2146 @Override 2147 protected String java_name_impl(VarInfo v) { 2148 return java_family_impl(OutputFormat.JAVA, v); 2149 } 2150 2151 @Override 2152 protected String jml_name_impl(VarInfo v) { 2153 return java_family_impl(OutputFormat.JML, v); 2154 } 2155 2156 @Override 2157 protected String dbc_name_impl(VarInfo v) { 2158 return java_family_impl(OutputFormat.DBCJAVA, v); 2159 } 2160 2161 protected String java_family_impl(OutputFormat format, VarInfo v) { 2162 2163 // See declaration of testCall for explanation of this flag. 2164 if (testCall) { 2165 return "no format when testCall."; 2166 } 2167 2168 assert v != null; 2169 assert v.isDerived(); 2170 Derivation derived = v.derived; 2171 assert derived instanceof SequenceScalarSubscript 2172 || derived instanceof SequenceStringSubscript 2173 || derived instanceof SequenceFloatSubscript; 2174 VarInfo indexVarInfo = ((BinaryDerivation) derived).base2; 2175 VarInfo seqVarInfo = ((BinaryDerivation) derived).base1; 2176 if (format == OutputFormat.JAVA) { 2177 return sequence.java_name_impl(index.java_name_impl(indexVarInfo), seqVarInfo); 2178 } else if (format == OutputFormat.JML) { 2179 return sequence.jml_name_impl(index.jml_name_impl(indexVarInfo), seqVarInfo); 2180 } else { // format == OutputFormat.DBCJAVA 2181 return sequence.dbc_name_impl(index.dbc_name_impl(indexVarInfo), seqVarInfo); 2182 } 2183 } 2184 2185 @Override 2186 protected String identifier_name_impl() { 2187 return sequence.identifier_name_impl(index.identifier_name()); 2188 } 2189 2190 @Override 2191 public <T> T accept(Visitor<T> v) { 2192 return v.visitSubscript(this); 2193 } 2194 } 2195 2196 /** 2197 * Returns a name for a slice of element selected from a sequence, like "this[i..j]". If an 2198 * endpoint is null, it means "from the start" or "to the end". 2199 */ 2200 public VarInfoName applySlice( 2201 @Interned VarInfoName this, @Nullable VarInfoName i, @Nullable VarInfoName j) { 2202 // a[] -> a[index..] 2203 // orig(a[]) -> orig(a[post(index)..]) 2204 ElementsFinder finder = new ElementsFinder(this); 2205 Elements elems = finder.elems(); 2206 assert elems != null; 2207 if (finder.inPre()) { 2208 if (i != null) { 2209 i = indexToPrestate(i); 2210 } 2211 if (j != null) { 2212 j = indexToPrestate(j); 2213 } 2214 } 2215 Replacer r = new Replacer(finder.elems(), new Slice(elems, i, j).intern()); 2216 return r.replace(this).intern(); 2217 } 2218 2219 /** A slice of elements from a sequence, like "sequence[i..j]". */ 2220 public static @Interned class Slice extends VarInfoName { 2221 // We are Serializable, so we specify a version to allow changes to 2222 // method signatures without breaking serialization. If you add or 2223 // remove fields, you should change this number to the current date. 2224 static final long serialVersionUID = 20020130L; 2225 2226 public final Elements sequence; 2227 public final VarInfoName i, j; 2228 2229 public Slice(Elements sequence, VarInfoName i, VarInfoName j) { 2230 assert sequence != null; 2231 assert (i != null) || (j != null); 2232 this.sequence = sequence; 2233 this.i = i; 2234 this.j = j; 2235 } 2236 2237 @Override 2238 protected String repr_impl(@GuardSatisfied Slice this) { 2239 return "Slice{" 2240 + ((i == null) ? "" : i.repr()) 2241 + "," 2242 + ((j == null) ? "" : j.repr()) 2243 + "}[" 2244 + sequence.repr() 2245 + "]"; 2246 } 2247 2248 @Override 2249 protected String name_impl(@GuardSatisfied Slice this) { 2250 return sequence.name_impl( 2251 "" + ((i == null) ? "0" : i.name()) + ".." + ((j == null) ? "" : j.name())); 2252 } 2253 2254 @Override 2255 protected String esc_name_impl() { 2256 // return the default implementation for now. 2257 // return name_impl(); 2258 throw new UnsupportedOperationException( 2259 "ESC cannot format an unquantified slice of elements"); 2260 } 2261 2262 @Override 2263 protected String simplify_name_impl(boolean prestate) { 2264 System.out.println(" seq: " + sequence + " " + i + " " + j); 2265 throw new UnsupportedOperationException( 2266 "Simplify cannot format an unquantified slice of elements"); 2267 } 2268 2269 @Override 2270 protected String java_name_impl(VarInfo v) { 2271 return slice_helper(OutputFormat.JAVA, v); 2272 } 2273 2274 @Override 2275 protected String jml_name_impl(VarInfo v) { 2276 return slice_helper(OutputFormat.JML, v); 2277 } 2278 2279 @Override 2280 protected String dbc_name_impl(VarInfo v) { 2281 return slice_helper(OutputFormat.DBCJAVA, v); 2282 } 2283 2284 // Helper for JML, Java and DBC formats 2285 protected String slice_helper(OutputFormat format, VarInfo v) { 2286 2287 // See declaration of testCall for explanation of this flag. 2288 if (testCall) { 2289 return "no format when testCall."; 2290 } 2291 2292 assert v != null; 2293 assert v.isDerived(); 2294 Derivation derived = v.derived; 2295 assert derived instanceof SequenceSubsequence 2296 || derived instanceof SequenceScalarArbitrarySubsequence 2297 || derived instanceof SequenceFloatArbitrarySubsequence 2298 || derived instanceof SequenceStringArbitrarySubsequence; 2299 if (derived instanceof SequenceSubsequence) { 2300 assert i == null || j == null; 2301 if (i == null) { // sequence[0..j] 2302 assert j != null; 2303 return "daikon.Quant.slice(" 2304 + sequence.name_using(format, ((SequenceSubsequence) derived).seqvar()) 2305 + ", 0, " 2306 + j.name_using(format, ((SequenceSubsequence) derived).sclvar()) 2307 + ")"; 2308 } else { 2309 VarInfo seqVarInfo = ((SequenceSubsequence) derived).seqvar(); 2310 String prefix = sequence.name_using(format, seqVarInfo); 2311 String lastIdxString = "daikon.Quant.size(" + prefix + ")"; 2312 // if (seqVarInfo.type.pseudoDimensions() > seqVarInfo.type.dimensions()) { 2313 // if (prefix.startsWith("daikon.Quant.collect")) { 2314 // // Quant collect methods returns an array 2315 // lastIdxString = prefix + ".length-1"; 2316 // } else { 2317 // // it's a collection 2318 // lastIdxString = prefix + ".size()-1"; 2319 // } 2320 // } else { 2321 // // it's an array 2322 // lastIdxString = prefix + ".length-1"; 2323 // } 2324 return "daikon.Quant.slice(" 2325 + sequence.name_using(format, ((SequenceSubsequence) derived).seqvar()) 2326 + ", " 2327 + i.name_using(format, ((SequenceSubsequence) derived).sclvar()) 2328 + ", " 2329 + lastIdxString 2330 + ")"; 2331 } 2332 } else { 2333 assert i != null && j != null; 2334 if (derived instanceof SequenceScalarArbitrarySubsequence) { 2335 SequenceScalarArbitrarySubsequence derived2 = 2336 (SequenceScalarArbitrarySubsequence) derived; 2337 return "daikon.Quant.slice(" 2338 + sequence.name_using(format, derived2.seqvar()) 2339 + ", " 2340 + i.name_using(format, derived2.startvar()) 2341 + ", " 2342 + j.name_using(format, derived2.endvar()) 2343 + ")"; 2344 } else if (derived instanceof SequenceFloatArbitrarySubsequence) { 2345 SequenceFloatArbitrarySubsequence derived2 = (SequenceFloatArbitrarySubsequence) derived; 2346 return "daikon.Quant.slice(" 2347 + sequence.name_using(format, derived2.seqvar()) 2348 + ", " 2349 + i.name_using(format, derived2.startvar()) 2350 + ", " 2351 + j.name_using(format, derived2.endvar()) 2352 + ")"; 2353 } else { 2354 SequenceStringArbitrarySubsequence derived2 = 2355 (SequenceStringArbitrarySubsequence) derived; 2356 return "daikon.Quant.slice(" 2357 + sequence.name_using(format, derived2.seqvar()) 2358 + ", " 2359 + i.name_using(format, derived2.startvar()) 2360 + ", " 2361 + j.name_using(format, derived2.endvar()) 2362 + ")"; 2363 } 2364 } 2365 } 2366 2367 @Override 2368 protected String identifier_name_impl() { 2369 String start = (i == null) ? "0" : i.identifier_name(); 2370 String end = (j == null) ? "" : j.identifier_name(); 2371 return sequence.identifier_name_impl(start + "_to_" + end); 2372 } 2373 2374 @Override 2375 public <T> T accept(Visitor<T> v) { 2376 return v.visitSlice(this); 2377 } 2378 2379 public VarInfoName getLowerBound() { 2380 return (i != null) ? i : ZERO; 2381 } 2382 2383 public VarInfoName getUpperBound() { 2384 return (j != null) ? j : sequence.getUpperBound(); 2385 } 2386 2387 public VarInfoName getSubscript(VarInfoName index) { 2388 return sequence.getSubscript(index); 2389 } 2390 } 2391 2392 /** Accept the actions of a visitor. */ 2393 public abstract <T> T accept(Visitor<T> v); 2394 2395 /** Visitor framework for processing of VarInfoNames. */ 2396 public static interface Visitor<T> { 2397 public T visitSimple(Simple o); 2398 2399 public T visitSizeOf(SizeOf o); 2400 2401 public T visitFunctionOf(FunctionOf o); 2402 2403 public T visitFunctionOfN(FunctionOfN o); 2404 2405 public T visitField(Field o); 2406 2407 public T visitTypeOf(TypeOf o); 2408 2409 public T visitPrestate(Prestate o); 2410 2411 public T visitPoststate(Poststate o); 2412 2413 public T visitAdd(Add o); 2414 2415 public T visitElements(Elements o); 2416 2417 public T visitSubscript(Subscript o); 2418 2419 public T visitSlice(Slice o); 2420 } 2421 2422 /** 2423 * Traverse the tree elements that have exactly one branch (so the traversal order doesn't 2424 * matter). Visitors need to implement methods for traversing elements (e.g. FunctionOfN) with 2425 * more than one branch. 2426 */ 2427 public abstract static class AbstractVisitor<T> implements Visitor<T> { 2428 @Override 2429 public T visitSimple(Simple o) { 2430 // nothing to do; leaf node 2431 return null; 2432 } 2433 2434 @Override 2435 public T visitSizeOf(SizeOf o) { 2436 return o.sequence.accept(this); 2437 } 2438 2439 @Override 2440 public T visitFunctionOf(FunctionOf o) { 2441 return o.argument.accept(this); 2442 } 2443 2444 /** By default, return effect on first argument, but traverse all, backwards. */ 2445 @Override 2446 public T visitFunctionOfN(FunctionOfN o) { 2447 T retval = null; 2448 for (ListIterator<VarInfoName> i = o.args.listIterator(o.args.size()); i.hasPrevious(); ) { 2449 VarInfoName vin = i.previous(); 2450 retval = vin.accept(this); 2451 } 2452 return retval; 2453 } 2454 2455 @Override 2456 public T visitField(Field o) { 2457 return o.term.accept(this); 2458 } 2459 2460 @Override 2461 public T visitTypeOf(TypeOf o) { 2462 return o.term.accept(this); 2463 } 2464 2465 @Override 2466 public T visitPrestate(Prestate o) { 2467 return o.term.accept(this); 2468 } 2469 2470 @Override 2471 public T visitPoststate(Poststate o) { 2472 return o.term.accept(this); 2473 } 2474 2475 @Override 2476 public T visitAdd(Add o) { 2477 return o.term.accept(this); 2478 } 2479 2480 @Override 2481 public T visitElements(Elements o) { 2482 return o.term.accept(this); 2483 } 2484 2485 // leave abstract; traversal order and return values matter 2486 @Override 2487 public abstract T visitSubscript(Subscript o); 2488 2489 // leave abstract; traversal order and return values matter 2490 @Override 2491 public abstract T visitSlice(Slice o); 2492 } 2493 2494 /** 2495 * Use to report whether a node is in a pre- or post-state context. Throws an assertion error if a 2496 * given goal isn't present. 2497 */ 2498 public static class NodeFinder extends AbstractVisitor<VarInfoName> { 2499 /** 2500 * Creates a new NodeFinder. 2501 * 2502 * @param root the root of the tree to search 2503 * @param goal the goal to find 2504 */ 2505 public NodeFinder(VarInfoName root, VarInfoName goal) { 2506 this.goal = goal; 2507 assert root.accept(this) != null; 2508 } 2509 2510 // state and accessors 2511 private final VarInfoName goal; 2512 private boolean pre; 2513 2514 public boolean inPre() { 2515 return pre; 2516 } 2517 2518 // visitor methods that get the job done 2519 @Override 2520 public VarInfoName visitSimple(Simple o) { 2521 return (o == goal) ? goal : null; 2522 } 2523 2524 @Override 2525 public VarInfoName visitSizeOf(SizeOf o) { 2526 return (o == goal) ? goal : super.visitSizeOf(o); 2527 } 2528 2529 @Override 2530 public VarInfoName visitFunctionOf(FunctionOf o) { 2531 return (o == goal) ? goal : super.visitFunctionOf(o); 2532 } 2533 2534 @Override 2535 public VarInfoName visitFunctionOfN(FunctionOfN o) { 2536 VarInfoName retval = null; 2537 for (VarInfoName vin : o.args) { 2538 retval = vin.accept(this); 2539 if (retval != null) { 2540 return retval; 2541 } 2542 } 2543 return retval; 2544 } 2545 2546 @Override 2547 public VarInfoName visitField(Field o) { 2548 return (o == goal) ? goal : super.visitField(o); 2549 } 2550 2551 @Override 2552 public VarInfoName visitTypeOf(TypeOf o) { 2553 return (o == goal) ? goal : super.visitTypeOf(o); 2554 } 2555 2556 @Override 2557 public VarInfoName visitPrestate(Prestate o) { 2558 pre = true; 2559 return super.visitPrestate(o); 2560 } 2561 2562 @Override 2563 public VarInfoName visitPoststate(Poststate o) { 2564 pre = false; 2565 return super.visitPoststate(o); 2566 } 2567 2568 @Override 2569 public VarInfoName visitAdd(Add o) { 2570 return (o == goal) ? goal : super.visitAdd(o); 2571 } 2572 2573 @Override 2574 public VarInfoName visitElements(Elements o) { 2575 return (o == goal) ? goal : super.visitElements(o); 2576 } 2577 2578 @Override 2579 public VarInfoName visitSubscript(Subscript o) { 2580 if (o == goal) { 2581 return goal; 2582 } 2583 if (o.sequence.accept(this) != null) { 2584 return goal; 2585 } 2586 if (o.index.accept(this) != null) { 2587 return goal; 2588 } 2589 return null; 2590 } 2591 2592 @Override 2593 public VarInfoName visitSlice(Slice o) { 2594 if (o == goal) { 2595 return goal; 2596 } 2597 if (o.sequence.accept(this) != null) { 2598 return goal; 2599 } 2600 if ((o.i != null) && (o.i.accept(this) != null)) { 2601 return goal; 2602 } 2603 if ((o.j != null) && (o.j.accept(this) != null)) { 2604 return goal; 2605 } 2606 return null; 2607 } 2608 } 2609 2610 /** 2611 * Finds if a given VarInfoName is contained in a set of nodes in the VarInfoName tree using == 2612 * comparison. Recurse through everything except fields, so in x.a, we don't look at a. 2613 */ 2614 public static class Finder extends AbstractVisitor<VarInfoName> { 2615 // state and accessors 2616 private final Set<VarInfoName> goals; 2617 2618 /** 2619 * Creates a new Finder. Uses equals() to find. 2620 * 2621 * @param argGoals the goals to find 2622 */ 2623 public Finder(Set<VarInfoName> argGoals) { 2624 goals = new HashSet<VarInfoName>(); 2625 for (VarInfoName name : argGoals) { 2626 this.goals.add(name.intern()); 2627 } 2628 } 2629 2630 /** Returns true iff some part of root is contained in this.goals. */ 2631 @EnsuresNonNullIf(result = true, expression = "getPart(#1") 2632 public boolean contains(VarInfoName root) { 2633 VarInfoName o = getPart(root); 2634 return (o != null); 2635 } 2636 2637 /** Returns the part of root that is contained in this.goals, or null if not found. */ 2638 public @Nullable VarInfoName getPart(VarInfoName root) { 2639 VarInfoName o = root.intern().accept(this); 2640 return o; 2641 } 2642 2643 // visitor methods that get the job done 2644 @Override 2645 public VarInfoName visitSimple(Simple o) { 2646 return goals.contains(o) ? o : null; 2647 } 2648 2649 @Override 2650 public VarInfoName visitSizeOf(SizeOf o) { 2651 return goals.contains(o) ? o : o.sequence.intern().accept(this); 2652 } 2653 2654 @Override 2655 public VarInfoName visitFunctionOf(FunctionOf o) { 2656 return goals.contains(o) ? o : super.visitFunctionOf(o); 2657 } 2658 2659 @Override 2660 public VarInfoName visitFunctionOfN(FunctionOfN o) { 2661 VarInfoName result = null; 2662 if (goals.contains(o)) { 2663 return o; 2664 } 2665 for (VarInfoName vin : o.args) { 2666 result = vin.accept(this); 2667 if (result != null) { 2668 return result; 2669 } 2670 } 2671 return result; 2672 } 2673 2674 @Override 2675 public VarInfoName visitField(Field o) { 2676 return goals.contains(o) ? o : super.visitField(o); 2677 } 2678 2679 @Override 2680 public VarInfoName visitTypeOf(TypeOf o) { 2681 return goals.contains(o) ? o : super.visitTypeOf(o); 2682 } 2683 2684 @Override 2685 public VarInfoName visitPrestate(Prestate o) { 2686 if (goals.contains(o)) { 2687 return o; 2688 } 2689 return super.visitPrestate(o); 2690 } 2691 2692 @Override 2693 public VarInfoName visitPoststate(Poststate o) { 2694 if (goals.contains(o)) { 2695 return o; 2696 } 2697 return super.visitPoststate(o); 2698 } 2699 2700 @Override 2701 public VarInfoName visitAdd(Add o) { 2702 return goals.contains(o) ? o : super.visitAdd(o); 2703 } 2704 2705 @Override 2706 public VarInfoName visitElements(Elements o) { 2707 return goals.contains(o) ? o : super.visitElements(o); 2708 } 2709 2710 @Override 2711 public VarInfoName visitSubscript(Subscript o) { 2712 if (goals.contains(o)) { 2713 return o; 2714 } 2715 VarInfoName temp = o.sequence.accept(this); 2716 if (temp != null) { 2717 return temp; 2718 } 2719 temp = o.index.accept(this); 2720 if (temp != null) { 2721 return temp; 2722 } 2723 return null; 2724 } 2725 2726 @Override 2727 public VarInfoName visitSlice(Slice o) { 2728 if (goals.contains(o)) { 2729 return o; 2730 } 2731 VarInfoName temp = o.sequence.accept(this); 2732 if (temp != null) { 2733 return temp; 2734 } 2735 if (o.i != null) { 2736 temp = o.i.accept(this); 2737 if (temp != null) { 2738 return temp; 2739 } 2740 } 2741 if (o.j != null) { 2742 temp = o.j.accept(this); 2743 if (temp != null) { 2744 return temp; 2745 } 2746 } 2747 return null; 2748 } 2749 } 2750 2751 // An abstract base class for visitors that compute some predicate 2752 // of a conjunctive nature (true only if true on all subparts), 2753 // returning Boolean.FALSE or Boolean.TRUE. 2754 public abstract static class BooleanAndVisitor extends AbstractVisitor<Boolean> { 2755 private boolean result; 2756 2757 protected BooleanAndVisitor(VarInfoName name) { 2758 result = (name.accept(this) != null); 2759 } 2760 2761 public boolean result() { 2762 return result; 2763 } 2764 2765 @Override 2766 public Boolean visitFunctionOfN(FunctionOfN o) { 2767 Boolean retval = null; 2768 for (ListIterator<VarInfoName> i = o.args.listIterator(o.args.size()); i.hasPrevious(); ) { 2769 VarInfoName vin = i.previous(); 2770 retval = vin.accept(this); 2771 if (retval != null) { 2772 return null; 2773 } 2774 } 2775 return retval; 2776 } 2777 2778 @Override 2779 public Boolean visitSubscript(Subscript o) { 2780 Boolean temp = o.sequence.accept(this); 2781 if (temp == null) { 2782 return temp; 2783 } 2784 temp = o.index.accept(this); 2785 return temp; 2786 } 2787 2788 @Override 2789 public Boolean visitSlice(Slice o) { 2790 Boolean temp = o.sequence.accept(this); 2791 if (temp == null) { 2792 return temp; 2793 } 2794 if (o.i != null) { 2795 temp = o.i.accept(this); 2796 if (temp == null) { 2797 return temp; 2798 } 2799 } 2800 if (o.j != null) { 2801 temp = o.j.accept(this); 2802 if (temp == null) { 2803 return temp; 2804 } 2805 } 2806 return temp; 2807 } 2808 } 2809 2810 public static class IsAllPrestateVisitor extends BooleanAndVisitor { 2811 2812 public IsAllPrestateVisitor(VarInfoName vin) { 2813 super(vin); 2814 } 2815 2816 @Override 2817 public Boolean visitSimple(Simple o) { 2818 // Any var not inside an orig() isn't prestate 2819 return null; 2820 } 2821 2822 @Override 2823 public Boolean visitPrestate(Prestate o) { 2824 // orig(...) is all prestate unless it contains post(...) 2825 return new IsAllNonPoststateVisitor(o).result() ? Boolean.TRUE : null; 2826 } 2827 } 2828 2829 public static class IsAllNonPoststateVisitor extends BooleanAndVisitor { 2830 public IsAllNonPoststateVisitor(VarInfoName vin) { 2831 super(vin); 2832 } 2833 2834 @Override 2835 public Boolean visitSimple(Simple o) { 2836 // Any var not inside a post() isn't poststate 2837 return Boolean.TRUE; 2838 } 2839 2840 @Override 2841 public Boolean visitPoststate(Poststate o) { 2842 // If we see a post(...), we aren't all poststate. 2843 return null; 2844 } 2845 } 2846 2847 /** 2848 * Use to traverse a tree, find the first (elements ...) node, and report whether it's in pre or 2849 * post-state. 2850 */ 2851 public static class ElementsFinder extends AbstractVisitor<Elements> { 2852 public ElementsFinder(VarInfoName name) { 2853 elems = name.accept(this); 2854 } 2855 2856 // state and accessors 2857 private boolean pre = false; 2858 private Elements elems = null; 2859 2860 public boolean inPre() { 2861 return pre; 2862 } 2863 2864 public Elements elems() { 2865 return elems; 2866 } 2867 2868 // visitor methods that get the job done 2869 @Override 2870 public Elements visitFunctionOfN(FunctionOfN o) { 2871 Elements retval = null; 2872 for (VarInfoName vin : o.args) { 2873 retval = vin.accept(this); 2874 if (retval != null) { 2875 return retval; 2876 } 2877 } 2878 return retval; 2879 } 2880 2881 @Override 2882 public Elements visitPrestate(Prestate o) { 2883 pre = true; 2884 return super.visitPrestate(o); 2885 } 2886 2887 @Override 2888 public Elements visitPoststate(Poststate o) { 2889 pre = false; 2890 return super.visitPoststate(o); 2891 } 2892 2893 @Override 2894 public Elements visitElements(Elements o) { 2895 return o; 2896 } 2897 2898 @Override 2899 public Elements visitSubscript(Subscript o) { 2900 // skip the subscripted sequence 2901 Elements tmp = o.sequence.term.accept(this); 2902 if (tmp == null) { 2903 tmp = o.index.accept(this); 2904 } 2905 return tmp; 2906 } 2907 2908 @Override 2909 public Elements visitSlice(Slice o) { 2910 // skip the sliced sequence 2911 Elements tmp = o.sequence.term.accept(this); 2912 if (tmp == null && o.i != null) { 2913 tmp = o.i.accept(this); 2914 } 2915 if (tmp == null && o.j != null) { 2916 tmp = o.j.accept(this); 2917 } 2918 return tmp; 2919 } 2920 } 2921 2922 /** 2923 * A Replacer is a Visitor that makes a copy of a tree, but replaces some node (and its children) 2924 * with another. The result is *not* interned; the client must do that if desired. 2925 */ 2926 public static class Replacer extends AbstractVisitor<VarInfoName> { 2927 private final VarInfoName old; 2928 private final VarInfoName _new; 2929 2930 public Replacer(VarInfoName old, VarInfoName _new) { 2931 this.old = old; 2932 this._new = _new; 2933 } 2934 2935 public VarInfoName replace(VarInfoName root) { 2936 return root.accept(this); 2937 } 2938 2939 @Override 2940 public VarInfoName visitSimple(Simple o) { 2941 return (o == old) ? _new : o; 2942 } 2943 2944 @Override 2945 public VarInfoName visitSizeOf(SizeOf o) { 2946 return (o == old) ? _new : super.visitSizeOf(o).applySize(); 2947 } 2948 2949 @Override 2950 public VarInfoName visitFunctionOf(FunctionOf o) { 2951 return (o == old) ? _new : super.visitFunctionOf(o).applyFunction(o.function); 2952 } 2953 2954 @Override 2955 public VarInfoName visitFunctionOfN(FunctionOfN o) { 2956 // If o is getting replaced, then just replace it 2957 // otherwise, create a new function and check if arguments get replaced 2958 if (o == old) { 2959 return _new; 2960 } 2961 ArrayList<VarInfoName> newArgs = new ArrayList<>(); 2962 for (VarInfoName vin : o.args) { 2963 VarInfoName retval = vin.accept(this); 2964 newArgs.add(retval); 2965 } 2966 return VarInfoName.applyFunctionOfN(o.function, newArgs); 2967 } 2968 2969 @Override 2970 public VarInfoName visitField(Field o) { 2971 return (o == old) ? _new : super.visitField(o).applyField(o.field); 2972 } 2973 2974 @Override 2975 public VarInfoName visitTypeOf(TypeOf o) { 2976 return (o == old) ? _new : super.visitTypeOf(o).applyTypeOf(); 2977 } 2978 2979 @Override 2980 public VarInfoName visitPrestate(Prestate o) { 2981 return (o == old) ? _new : super.visitPrestate(o).applyPrestate(); 2982 } 2983 2984 @Override 2985 public VarInfoName visitPoststate(Poststate o) { 2986 return (o == old) ? _new : super.visitPoststate(o).applyPoststate(); 2987 } 2988 2989 @Override 2990 public VarInfoName visitAdd(Add o) { 2991 return (o == old) ? _new : super.visitAdd(o).applyAdd(o.amount); 2992 } 2993 2994 @Override 2995 public VarInfoName visitElements(Elements o) { 2996 return (o == old) ? _new : super.visitElements(o).applyElements(); 2997 } 2998 2999 @Override 3000 public VarInfoName visitSubscript(Subscript o) { 3001 return (o == old) ? _new : o.sequence.accept(this).applySubscript(o.index.accept(this)); 3002 } 3003 3004 @Override 3005 public VarInfoName visitSlice(Slice o) { 3006 return (o == old) 3007 ? _new 3008 : o.sequence 3009 .accept(this) 3010 .applySlice( 3011 (o.i == null) ? null : o.i.accept(this), (o.j == null) ? null : o.j.accept(this)); 3012 } 3013 } 3014 3015 /** 3016 * Replace pre states by normal variables, and normal variables by post states. We should do this 3017 * for all variables except for variables derived from return. This piggybacks on replacer but the 3018 * actual replacement is done elsewhere. 3019 */ 3020 public static class PostPreConverter extends Replacer { 3021 3022 public PostPreConverter() { 3023 super(null, null); 3024 } 3025 3026 @Override 3027 public VarInfoName visitSimple(Simple o) { 3028 if (o.name.equals("return")) { 3029 return o; 3030 } 3031 return o.applyPoststate(); 3032 } 3033 3034 @Override 3035 public VarInfoName visitPrestate(Prestate o) { 3036 return o.term; 3037 } 3038 } 3039 3040 public static class NoReturnValue {} 3041 3042 /** 3043 * Use to collect all elements in a tree into an inorder-traversal list. Result includes the root 3044 * element. All methods return null; to obtain the result, call nodes(). 3045 */ 3046 public static class InorderFlattener extends AbstractVisitor<NoReturnValue> { 3047 public InorderFlattener(VarInfoName root) { 3048 root.accept(this); 3049 } 3050 3051 // state and accessors 3052 private final List<VarInfoName> result = new ArrayList<>(); 3053 3054 /** Method returning the actual results (the nodes in order). */ 3055 public List<VarInfoName> nodes() { 3056 return Collections.unmodifiableList(result); 3057 } 3058 3059 // visitor methods that get the job done 3060 @Override 3061 public NoReturnValue visitSimple(Simple o) { 3062 result.add(o); 3063 return super.visitSimple(o); 3064 } 3065 3066 @Override 3067 public NoReturnValue visitSizeOf(SizeOf o) { 3068 result.add(o); 3069 return super.visitSizeOf(o); 3070 } 3071 3072 @Override 3073 public NoReturnValue visitFunctionOf(FunctionOf o) { 3074 result.add(o); 3075 return super.visitFunctionOf(o); 3076 } 3077 3078 @Override 3079 public NoReturnValue visitFunctionOfN(FunctionOfN o) { 3080 result.add(o); 3081 for (VarInfoName vin : o.args) { 3082 vin.accept(this); 3083 } 3084 return null; 3085 } 3086 3087 @Override 3088 public NoReturnValue visitField(Field o) { 3089 result.add(o); 3090 return super.visitField(o); 3091 } 3092 3093 @Override 3094 public NoReturnValue visitTypeOf(TypeOf o) { 3095 result.add(o); 3096 return super.visitTypeOf(o); 3097 } 3098 3099 @Override 3100 public NoReturnValue visitPrestate(Prestate o) { 3101 result.add(o); 3102 return super.visitPrestate(o); 3103 } 3104 3105 @Override 3106 public NoReturnValue visitPoststate(Poststate o) { 3107 result.add(o); 3108 return super.visitPoststate(o); 3109 } 3110 3111 @Override 3112 public NoReturnValue visitAdd(Add o) { 3113 result.add(o); 3114 return super.visitAdd(o); 3115 } 3116 3117 @Override 3118 public NoReturnValue visitElements(Elements o) { 3119 result.add(o); 3120 return super.visitElements(o); 3121 } 3122 3123 @Override 3124 public NoReturnValue visitSubscript(Subscript o) { 3125 result.add(o); 3126 o.sequence.accept(this); 3127 o.index.accept(this); 3128 return null; 3129 } 3130 3131 @Override 3132 public NoReturnValue visitSlice(Slice o) { 3133 result.add(o); 3134 o.sequence.accept(this); 3135 if (o.i != null) { 3136 o.i.accept(this); 3137 } 3138 if (o.j != null) { 3139 o.j.accept(this); 3140 } 3141 return null; 3142 } 3143 } 3144 3145 // ============================================================ 3146 // Quantification for formatting in ESC or Simplify 3147 3148 public static class SimpleNamesVisitor extends AbstractVisitor<NoReturnValue> { 3149 public SimpleNamesVisitor(VarInfoName root) { 3150 assert root != null; 3151 simples = new HashSet<String>(); 3152 root.accept(this); 3153 } 3154 3155 /** 3156 * See {@link #simples()}. 3157 * 3158 * @see #simples() 3159 */ 3160 private Set<String> simples; 3161 3162 /** 3163 * Returns collection of simple identifiers used in this expression, as Strings. (Used, for 3164 * instance, to check for conflict with a quantifier variable name.) 3165 * 3166 * @return collection of simple identifiers used in this expression, as Strings 3167 */ 3168 public Set<String> simples() { 3169 return Collections.unmodifiableSet(simples); 3170 } 3171 3172 // visitor methods that get the job done 3173 @Override 3174 public NoReturnValue visitSimple(Simple o) { 3175 simples.add(o.name); 3176 return super.visitSimple(o); 3177 } 3178 3179 @Override 3180 public NoReturnValue visitElements(Elements o) { 3181 return super.visitElements(o); 3182 } 3183 3184 @Override 3185 public NoReturnValue visitFunctionOf(FunctionOf o) { 3186 simples.add(o.function); 3187 return super.visitFunctionOf(o); 3188 } 3189 3190 @Override 3191 public NoReturnValue visitFunctionOfN(FunctionOfN o) { 3192 simples.add(o.function); 3193 return super.visitFunctionOfN(o); 3194 } 3195 3196 @Override 3197 public NoReturnValue visitSubscript(Subscript o) { 3198 o.sequence.accept(this); 3199 return o.index.accept(this); 3200 } 3201 3202 @Override 3203 public NoReturnValue visitSlice(Slice o) { 3204 if (o.i != null) { 3205 o.i.accept(this); 3206 } 3207 if (o.j != null) { 3208 o.j.accept(this); 3209 } 3210 return o.sequence.accept(this); 3211 } 3212 } 3213 3214 /** 3215 * A quantifier visitor can be used to search a tree and return all unquantified sequences (e.g. 3216 * a[] or a[i..j]). 3217 */ 3218 public static class QuantifierVisitor extends AbstractVisitor<NoReturnValue> { 3219 public QuantifierVisitor(VarInfoName root) { 3220 assert root != null; 3221 unquant = new HashSet<VarInfoName>(); 3222 root.accept(this); 3223 } 3224 3225 // state and accessors 3226 /** 3227 * See {@link #unquants()}. 3228 * 3229 * @see #unquants() 3230 */ 3231 private Set<VarInfoName> /*actually <Elements || Slice>*/ unquant; 3232 3233 /** 3234 * Returns a collection of the nodes under the root that need quantification. Each node 3235 * represents an array; in particular, the values are either of type Elements or Slice. 3236 * 3237 * @return the nodes under the root that need quantification 3238 */ 3239 // Here are some inputs and the corresponding output sets: 3240 // terms[index].elts[num] ==> { } 3241 // terms[index].elts[] ==> { terms[index].elts[] } 3242 // terms[].elts[] ==> { terms[], terms[].elts[] } 3243 // ary[row][col] ==> { } 3244 // ary[row][] ==> { ary[row][] } 3245 // ary[][] ==> { ary[], ary[][] } 3246 public Set<VarInfoName> unquants() { 3247 if (QuantHelper.debug.isLoggable(Level.FINE)) { 3248 QuantHelper.debug.fine("unquants: " + unquant); 3249 } 3250 return Collections.unmodifiableSet(unquant); 3251 } 3252 3253 // visitor methods that get the job done 3254 @Override 3255 public NoReturnValue visitSimple(Simple o) { 3256 return super.visitSimple(o); 3257 } 3258 3259 @Override 3260 public NoReturnValue visitElements(Elements o) { 3261 unquant.add(o); 3262 return super.visitElements(o); 3263 } 3264 3265 @Override 3266 public NoReturnValue visitFunctionOf(FunctionOf o) { 3267 return null; 3268 // return o.args.get(0).accept(this); // Return value doesn't matter 3269 // We only use one of them because we don't want double quantifiers 3270 } 3271 3272 /** 3273 * We do *not* want to pull out array members of FunctionOfN because a FunctionOfN creates a 3274 * black-box array with respect to quantification. (Also, otherwise, there may be two or more 3275 * arrays that are returned, making the quantification engine think it's working with 2-d 3276 * arrays.) 3277 */ 3278 @Override 3279 public NoReturnValue visitFunctionOfN(FunctionOfN o) { 3280 return null; 3281 // return o.args.get(0).accept(this); // Return value doesn't matter 3282 // We only use one of them because we don't want double quantifiers 3283 } 3284 3285 @Override 3286 public NoReturnValue visitSizeOf(SizeOf o) { 3287 // don't visit the sequence; we aren't using the elements of it, 3288 // just the length, so we don't want to include it in the results 3289 return o.get_term().accept(this); 3290 } 3291 3292 @Override 3293 public NoReturnValue visitSubscript(Subscript o) { 3294 o.index.accept(this); 3295 // don't visit the sequence; it is fixed with an exact 3296 // subscript, so we don't want to include it in the results 3297 return o.sequence.term.accept(this); 3298 } 3299 3300 @Override 3301 public NoReturnValue visitSlice(Slice o) { 3302 unquant.add(o); 3303 if (o.i != null) { 3304 o.i.accept(this); 3305 } 3306 if (o.j != null) { 3307 o.j.accept(this); 3308 } 3309 // don't visit the sequence; we will replace the slice with the 3310 // subscript, so we want to leave the elements alone 3311 return o.sequence.term.accept(this); 3312 } 3313 } 3314 3315 // ============================================================ 3316 // Quantification for formatting in ESC or Simplify: QuantHelper 3317 3318 /** 3319 * Helper for writing parts of quantification expressions. Formatting methods in invariants call 3320 * the formatting methods in this class to get commonly-used parts, like how universal 3321 * quanitifiers look in the different formatting schemes. 3322 */ 3323 public static class QuantHelper { 3324 3325 /** Debug tracer. */ 3326 public static final Logger debug = Logger.getLogger("daikon.inv.Invariant.print.QuantHelper"); 3327 3328 /** 3329 * A FreeVar is very much like a Simple, except that it doesn't care if it's in prestate or 3330 * poststate for simplify formatting. 3331 */ 3332 public static class FreeVar extends Simple { 3333 // We are Serializable, so we specify a version to allow changes to 3334 // method signatures without breaking serialization. If you add or 3335 // remove fields, you should change this number to the current date. 3336 static final long serialVersionUID = 20020130L; 3337 3338 public FreeVar(String name) { 3339 super(name); 3340 } 3341 3342 @Override 3343 protected String repr_impl(@GuardSatisfied FreeVar this) { 3344 return "Free[" + super.repr_impl() + "]"; 3345 } 3346 3347 @Override 3348 protected String jml_name_impl(VarInfo v) { 3349 return super.jml_name_impl(v); 3350 } 3351 3352 // protected String esc_name_impl() { 3353 // return super.esc_name_impl(); 3354 // } 3355 @Override 3356 protected String simplify_name_impl(boolean prestate) { 3357 return super.simplify_name_impl(false); 3358 } 3359 } 3360 3361 // <root, needy, index> -> <root', lower, upper> 3362 /** 3363 * Replaces a needy (unquantified term) with its subscripted equivalent, using the given index 3364 * variable. 3365 * 3366 * @param root the root of the expression to be modified. Substitution occurs only in the 3367 * subtree reachable from root. 3368 * @param needy the term to be subscripted (must be of type Elements or Slice) 3369 * @param index the variable to place in the subscript 3370 * @return a 3-element array consisting of the new root, the lower bound for the index 3371 * (inclusive), and the upper bound for the index (inclusive), in that order 3372 */ 3373 public static VarInfoName[] replace(VarInfoName root, VarInfoName needy, VarInfoName index) { 3374 assert root != null; 3375 assert needy != null; 3376 assert index != null; 3377 assert (needy instanceof Elements) || (needy instanceof Slice); 3378 3379 // Figure out what to replace needy with, and the appropriate 3380 // bounds to use 3381 VarInfoName replace_with; 3382 VarInfoName lower, upper; 3383 if (needy instanceof Elements) { 3384 Elements sequence = (Elements) needy; 3385 replace_with = sequence.getSubscript(index); 3386 lower = sequence.getLowerBound(); 3387 upper = sequence.getUpperBound(); 3388 } else if (needy instanceof Slice) { 3389 Slice slice = (Slice) needy; 3390 replace_with = slice.getSubscript(index); 3391 lower = slice.getLowerBound(); 3392 upper = slice.getUpperBound(); 3393 } else { 3394 // unreachable; placate javac 3395 throw new IllegalStateException(); 3396 } 3397 assert replace_with != null; 3398 3399 // If needy was in prestate, adjust bounds appropriately 3400 if (root.inPrestateContext(needy)) { 3401 if (!lower.isLiteralConstant()) { 3402 if (lower instanceof Poststate) { 3403 lower = ((Poststate) lower).term; 3404 } else { 3405 lower = lower.applyPrestate(); 3406 } 3407 } 3408 if (!upper.isLiteralConstant()) { 3409 if (upper instanceof Poststate) { 3410 upper = ((Poststate) upper).term; 3411 } else { 3412 upper = upper.applyPrestate(); 3413 } 3414 } 3415 } 3416 3417 // replace needy 3418 VarInfoName root_prime = new Replacer(needy, replace_with).replace(root).intern(); 3419 3420 assert root_prime != null; 3421 assert lower != null; 3422 assert upper != null; 3423 3424 return new VarInfoName[] {root_prime, lower, upper}; 3425 } 3426 3427 /** 3428 * Assuming that root is a sequence, return a VarInfoName representing the 3429 * (index_base+index_off)-th element of that sequence. index_base may be null, to represent 0. 3430 */ 3431 public static VarInfoName selectNth( 3432 VarInfoName root, @Nullable VarInfoName index_base, int index_off) { 3433 QuantifierVisitor qv = new QuantifierVisitor(root); 3434 List<VarInfoName> unquants = new ArrayList<>(qv.unquants()); 3435 if (unquants.size() == 0) { 3436 // Nothing to do? 3437 return null; 3438 } else if (unquants.size() == 1) { 3439 VarInfoName index_vin; 3440 if (index_base != null) { 3441 index_vin = index_base; 3442 if (index_off != 0) { 3443 index_vin = index_vin.applyAdd(index_off); 3444 } 3445 } else { 3446 index_vin = new Simple(Integer.toString(index_off)).intern(); 3447 } 3448 VarInfoName to_replace = unquants.get(0); 3449 @Interned VarInfoName[] replace_result = replace(root, to_replace, index_vin); 3450 return replace_result[0]; 3451 } else { 3452 throw new Error("Can't handle multi-dim array in VarInfoName.QuantHelper.select_nth()"); 3453 } 3454 } 3455 3456 /** 3457 * Assuming that root is a sequence, return a VarInfoName representing the 3458 * (index_base+index_off)-th element of that sequence. index_base may be null, to represent 0. 3459 */ 3460 public static VarInfoName selectNth( 3461 VarInfoName root, String index_base, boolean free, int index_off) { 3462 QuantifierVisitor qv = new QuantifierVisitor(root); 3463 List<VarInfoName> unquants = new ArrayList<>(qv.unquants()); 3464 if (unquants.size() == 0) { 3465 // Nothing to do? 3466 return null; 3467 } else if (unquants.size() == 1) { 3468 VarInfoName index_vin; 3469 if (index_base != null) { 3470 if (index_off != 0) { 3471 index_base += "+" + index_off; 3472 } 3473 if (free) { 3474 index_vin = new FreeVar(index_base); 3475 } else { 3476 index_vin = VarInfoName.parse(index_base); 3477 } 3478 // if (index_base.contains ("a")) 3479 // System.out.printf("selectNth: '%s' '%s'%n", index_base, 3480 // index_vin); 3481 } else { 3482 index_vin = new Simple(Integer.toString(index_off)); 3483 } 3484 VarInfoName to_replace = unquants.get(0); 3485 VarInfoName[] replace_result = replace(root, to_replace, index_vin); 3486 // if ((index_base != null) && index_base.contains ("a")) 3487 // System.out.printf("root = %s, to_replace = %s, index_vin = %s%n", 3488 // root, to_replace, index_vin); 3489 return replace_result[0]; 3490 } else { 3491 throw new Error("Can't handle multi-dim array in VarInfoName.QuantHelper.select_nth()"); 3492 } 3493 } 3494 3495 // Return a string distinct from any of the strings in "taken". 3496 private static String freshDistinctFrom(Set<String> taken) { 3497 char c = 'i'; 3498 String name; 3499 do { 3500 name = String.valueOf(c++); 3501 } while (taken.contains(name)); 3502 return name; 3503 } 3504 3505 /** Return a fresh variable name that doesn't appear in the given variable names. */ 3506 public static VarInfoName getFreeIndex(VarInfoName... vins) { 3507 Set<String> simples = new HashSet<>(); 3508 for (VarInfoName vin : vins) { 3509 simples.addAll(new SimpleNamesVisitor(vin).simples()); 3510 } 3511 return new FreeVar(freshDistinctFrom(simples)); 3512 } 3513 3514 /** Record type for return value of the quantify method below. */ 3515 public static class QuantifyReturn { 3516 public @Interned VarInfoName[] root_primes; 3517 public List<@Interned VarInfoName[]> 3518 bound_vars; // each element is VarInfoName[3] = <variable, lower, upper> 3519 } 3520 3521 // <root*> -> <root'*, <index, lower, upper>*> 3522 // (The lengths of root* and root'* are the same; not sure about <i,l,u>*.) 3523 /** 3524 * Given a list of roots, changes all Elements and Slice terms to Subscripts by inserting a new 3525 * free variable; also return bounds for the new variables. 3526 */ 3527 public static QuantifyReturn quantify(VarInfoName[] roots) { 3528 assert roots != null; 3529 3530 if (QuantHelper.debug.isLoggable(Level.FINE)) { 3531 QuantHelper.debug.fine("roots: " + Arrays.asList(roots)); 3532 } 3533 3534 // create empty result 3535 QuantifyReturn result = new QuantifyReturn(); 3536 result.root_primes = new VarInfoName[roots.length]; 3537 result.bound_vars = new ArrayList<VarInfoName[]>(); 3538 3539 // all of the simple identifiers used by these roots 3540 Set<String> simples = new HashSet<>(); 3541 3542 // build helper for each roots; collect identifiers 3543 QuantifierVisitor[] helper = new QuantifierVisitor[roots.length]; 3544 for (int i = 0; i < roots.length; i++) { 3545 if (QuantHelper.debug.isLoggable(Level.FINE)) { 3546 QuantHelper.debug.fine("Calling quanthelper on: " + i + " " + roots[i]); 3547 } 3548 3549 helper[i] = new QuantifierVisitor(roots[i]); 3550 simples.addAll(new SimpleNamesVisitor(roots[i]).simples()); 3551 } 3552 3553 // choose names for the indices that don't conflict, and then 3554 // replace the right stuff in the term 3555 char tmp = 'i'; 3556 for (int i = 0; i < roots.length; i++) { 3557 List<VarInfoName> uq = new ArrayList<>(helper[i].unquants()); 3558 if (uq.size() == 0) { 3559 // nothing needs quantification 3560 result.root_primes[i] = roots[i]; 3561 } else { 3562 if (QuantHelper.debug.isLoggable(Level.FINE)) { 3563 QuantHelper.debug.fine("root: " + roots[i]); 3564 QuantHelper.debug.fine("uq_elts: " + uq.toString()); 3565 } 3566 3567 // We assume that the input was one unquantified sequence 3568 // variable. If uq has more than one element, then the 3569 // sequence had more than one dimension. 3570 assert uq.size() == 1 : "We can only handle 1D arrays for now"; 3571 3572 VarInfoName uq_elt = uq.get(0); 3573 3574 String idx_name; 3575 do { 3576 idx_name = String.valueOf(tmp++); 3577 } while (simples.contains(idx_name)); 3578 assert tmp <= 'z' : "Ran out of letters in quantification"; 3579 VarInfoName idx = new FreeVar(idx_name).intern(); 3580 3581 if (QuantHelper.debug.isLoggable(Level.FINE)) { 3582 QuantHelper.debug.fine("idx: " + idx); 3583 } 3584 3585 // call replace and unpack results 3586 VarInfoName[] replace_result = replace(roots[i], uq_elt, idx); 3587 VarInfoName root_prime = replace_result[0]; 3588 VarInfoName lower = replace_result[1]; 3589 VarInfoName upper = replace_result[2]; 3590 3591 result.root_primes[i] = root_prime; 3592 result.bound_vars.add(new VarInfoName[] {idx, lower, upper}); 3593 } 3594 } 3595 3596 return result; 3597 } 3598 3599 // <root*> -> <string string* string> 3600 /** 3601 * Given a list of roots, return a String array where the first element is a ESC-style 3602 * quantification over newly-introduced bound variables, the last element is a closer, and the 3603 * other elements are esc-named strings for the provided roots (with sequences subscripted by 3604 * one of the new bound variables). 3605 */ 3606 public static String[] format_esc(VarInfoName[] roots) { 3607 return format_esc(roots, false); 3608 } 3609 3610 public static String[] format_esc(VarInfoName[] roots, boolean elementwise) { 3611 // The call to format_esc is now handled by the combined formatter format_java_style 3612 return format_java_style(roots, elementwise, true, OutputFormat.ESCJAVA); 3613 } 3614 3615 // <root*> -> <string string*> 3616 /** 3617 * Given a list of roots, return a String array where the first element is a JML-style 3618 * quantification over newly-introduced bound variables, the last element is a closer, and the 3619 * other elements are jml-named strings for the provided roots (with sequenced subscripted by 3620 * one of the new bound variables). 3621 */ 3622 // public static String[] format_jml(VarInfoName[] roots) { 3623 // return format_jml(roots, false); 3624 // } 3625 // public static String[] format_jml(VarInfoName[] roots, boolean elementwise) { 3626 // return format_jml(roots, elementwise, true); 3627 // } 3628 // public static String[] format_jml(VarInfoName[] roots, boolean elementwise, boolean forall) { 3629 // return format_java_style(roots, elementwise, forall, OutputFormat.JML); 3630 // } 3631 3632 /* CP: Quantification for DBC: We would like quantified expression 3633 * to always return a boolean value, and in the previous 3634 * implementation (commented out below), quantification was 3635 * expressed as a for-loop, which does not return boolean 3636 * values. An alternative solution would be to use Jtest's $forall 3637 * and $exists constrcuts, but testing showed that Jtest does not 3638 * allow these constructs in @post annotations (!). The current 3639 * implementation uses helper methods defined in a separate class 3640 * daikon.Quant (not currently included with Daikon's 3641 * distribution). These methods always return a boolean value and 3642 * look something like this: 3643 * 3644 * Quant.eltsEqual(this.theArray, null) 3645 * Quant.subsetOf(this.arr, new int[] { 1, 2, 3 }) 3646 * 3647 */ 3648 // /** 3649 // * vi is the Varinfo corresponding to the VarInfoName var. Uses 3650 // * the variable i to iterate. This could mean a conflict with the 3651 // * name of the argument var. 3652 // */ 3653 // public static String dbcForalli(VarInfoName.Elements var, VarInfo vi, 3654 // String condition) { 3655 // if (vi.type.isArray()) { 3656 // return 3657 // "(java.util.Arrays.asList(" + var.term.dbc_name(vi) 3658 // + ")).$forall(" + vi.type.base() + " i, " 3659 // + condition + ")"; 3660 // } 3661 // return var.term.dbc_name(vi) 3662 // + ".$forall(" + vi.type.base() + " i, " 3663 // + condition + ")"; 3664 // } 3665 3666 // /** 3667 // * vi is the Varinfo corresponding to the VarInfoName var. Uses 3668 // * the variable i to iterate. This could mean a conflict with the 3669 // * name of the argument var. 3670 // */ 3671 // public static String dbcExistsi(VarInfoName.Elements var, VarInfo vi, 3672 // String condition) { 3673 // if (vi.type.isArray()) { 3674 // return 3675 // "(java.util.Arrays.asList(" + var.term.dbc_name(vi) 3676 // + ")).$exists(" + vi.type.base() + " i, " 3677 // + condition + ")"; 3678 // } 3679 // return var.term.dbc_name(vi) 3680 // + ".$exists(" + vi.type.base() + " i, " 3681 // + condition + ")"; 3682 // } 3683 3684 // //@tx 3685 // public static String[] format_dbc(VarInfoName[] roots, VarInfo[] varinfos) { 3686 // return format_dbc(roots, true, varinfos); 3687 // } 3688 // public static String[] format_dbc(VarInfoName[] roots, boolean elementwise, 3689 // VarInfo[] varinfos) { 3690 // return format_dbc(roots, elementwise, true, varinfos); 3691 // } 3692 // public static String[] format_dbc(VarInfoName[] roots, boolean elementwise, 3693 // boolean forall, VarInfo[] varinfos) { 3694 // assert roots != null; 3695 3696 // QuantifyReturn qret = quantify(roots); 3697 3698 // // build the "\forall ..." predicate 3699 // String[] result = new String[roots.length + 2]; 3700 // StringBuilder int_list, conditions, closing; 3701 // StringBuilder tempResult; 3702 // { 3703 // tempResult = new StringBuilder(); 3704 // // "i, j, ..." 3705 // int_list = new StringBuilder(); 3706 // // "ai <= i && i <= bi && aj <= j && j <= bj && ..." 3707 // // if elementwise, also do "(i-ai) == (b-bi) && ..." 3708 // conditions = new StringBuilder(); 3709 // closing = new StringBuilder(); 3710 // for (int i = 0; i < qret.bound_vars.size(); i++) { 3711 // int_list.setLength(0); 3712 // conditions.setLength(0); 3713 // closing.setLength(0); 3714 3715 // VarInfoName[] boundv = qret.bound_vars.get(i); 3716 // VarInfoName idx = boundv[0], low = boundv[1], high = boundv[2]; 3717 // if (i != 0) { 3718 // //int_list.append(", "); 3719 // //conditions.append(" && "); 3720 // //closing.append(", "); 3721 // closing.append(idx.dbc_name(null)); 3722 // closing.append("++"); 3723 // } else { 3724 // closing.append(idx.dbc_name(null)); 3725 // closing.append("++"); 3726 // } 3727 // int_list.append(idx.dbc_name(null)); 3728 // int_list.append(" = "); //@TX 3729 // int_list.append(low.dbc_name(null)); 3730 3731 // conditions.append(idx.dbc_name(null)); 3732 // conditions.append(" <= "); 3733 // conditions.append(high.dbc_name(null)); 3734 3735 // if (elementwise && (i >= 1)) { 3736 // VarInfoName[] _boundv = qret.bound_vars.get(i - 1); 3737 // VarInfoName _idx = _boundv[0], _low = _boundv[1]; 3738 // conditions.append(" && "); 3739 // if (ZERO.equals(_low)) { 3740 // conditions.append(_idx); 3741 // } else { 3742 // conditions.append("("); 3743 // conditions.append(_idx.dbc_name(null)); 3744 // conditions.append("-("); 3745 // conditions.append(_low.dbc_name(null)); 3746 // conditions.append("))"); 3747 // } 3748 // conditions.append(" == "); 3749 // if (ZERO.equals(low)) { 3750 // conditions.append(idx.dbc_name(null)); 3751 // } else { 3752 // conditions.append("("); 3753 // conditions.append(idx.dbc_name(null)); 3754 // conditions.append("-("); 3755 // conditions.append(low.dbc_name(null)); 3756 // conditions.append("))"); 3757 // } 3758 // } 3759 // tempResult.append(" for (int " + int_list + " ; " + conditions + "; " + closing + 3760 // ") "); 3761 // } 3762 // } 3763 // //result[0] = "{ for (int " + int_list + " ; " + conditions + "; " 3764 // + closing + ") $assert ("; //@TX 3765 // result[0] = "{ " + tempResult + " $assert ("; //@TX 3766 // result[result.length - 1] = "); }"; 3767 3768 // // stringify the terms 3769 // for (int i = 0; i < roots.length; i++) { 3770 // result[i + 1] = qret.root_primes[i].dbc_name(null); 3771 // } 3772 3773 // return result; 3774 // } 3775 3776 ////////////////////////// 3777 3778 public static String[] simplifyNameAndBounds(VarInfoName name) { 3779 String[] results = new String[3]; 3780 boolean preState = false; 3781 if (name instanceof Prestate) { 3782 Prestate wrapped = (Prestate) name; 3783 name = wrapped.term; 3784 preState = true; 3785 } 3786 if (name instanceof Elements) { 3787 Elements sequence = (Elements) name; 3788 VarInfoName array = sequence.term; 3789 results[0] = array.simplify_name(preState); 3790 results[1] = sequence.getLowerBound().simplify_name(preState); 3791 results[2] = sequence.getUpperBound().simplify_name(preState); 3792 return results; 3793 } else if (name instanceof Slice) { 3794 Slice slice = (Slice) name; 3795 VarInfoName array = slice.sequence.term; 3796 results[0] = array.simplify_name(preState); 3797 results[1] = slice.getLowerBound().simplify_name(preState); 3798 results[2] = slice.getUpperBound().simplify_name(preState); 3799 return results; 3800 } else { 3801 // There are some other cases this scheme can't handle. 3802 // For instance, if every Book has an ISBN, a front-end 3803 // might distribute the access to that field over an array 3804 // of books, so that "books[].isbn" is an array of ISBNs, 3805 // though its name has type Field. 3806 return null; 3807 } 3808 } 3809 3810 // <root*> -> <string string*> 3811 /** 3812 * Given a list of roots, return a String array where the first element is a simplify-style 3813 * quantification over newly-introduced bound variables, the last element is a closer, and the 3814 * other elements are simplify-named strings for the provided roots (with sequences subscripted 3815 * by one of the new bound variables). 3816 * 3817 * <p>If elementwise is true, include the additional contraint that the indices (there must be 3818 * exactly two in this case) refer to corresponding positions. If adjacent is true, include the 3819 * additional constraint that the second index be one more than the first. If distinct is true, 3820 * include the constraint that the two indices are different. If includeIndex is true, return 3821 * additional strings, after the roots but before the closer, with the names of the index 3822 * variables. 3823 */ 3824 // XXX This argument list is starting to get out of hand. -smcc 3825 public static String[] format_simplify(VarInfoName[] roots) { 3826 return format_simplify(roots, false, false, false, false); 3827 } 3828 3829 public static String[] format_simplify(VarInfoName[] roots, boolean eltwise) { 3830 return format_simplify(roots, eltwise, false, false, false); 3831 } 3832 3833 public static String[] format_simplify(VarInfoName[] roots, boolean eltwise, boolean adjacent) { 3834 return format_simplify(roots, eltwise, adjacent, false, false); 3835 } 3836 3837 public static String[] format_simplify( 3838 VarInfoName[] roots, boolean eltwise, boolean adjacent, boolean distinct) { 3839 return format_simplify(roots, eltwise, adjacent, distinct, false); 3840 } 3841 3842 public static String[] format_simplify( 3843 VarInfoName[] roots, 3844 boolean elementwise, 3845 boolean adjacent, 3846 boolean distinct, 3847 boolean includeIndex) { 3848 assert roots != null; 3849 3850 if (adjacent || distinct) { 3851 assert roots.length == 2; 3852 } 3853 3854 QuantifyReturn qret = quantify(roots); 3855 3856 // build the forall predicate 3857 String[] result = new String[(includeIndex ? 2 : 1) * roots.length + 2]; 3858 3859 StringJoiner int_list, conditions; 3860 { 3861 // "i j ..." 3862 int_list = new StringJoiner(" "); 3863 // "(AND (<= ai i) (<= i bi) (<= aj j) (<= j bj) ...)" 3864 // if elementwise, also insert "(EQ (- i ai) (- j aj)) ..." 3865 conditions = new StringJoiner(" "); 3866 for (int i = 0; i < qret.bound_vars.size(); i++) { 3867 VarInfoName[] boundv = qret.bound_vars.get(i); 3868 VarInfoName idx = boundv[0], low = boundv[1], high = boundv[2]; 3869 int_list.add(idx.simplify_name()); 3870 conditions.add("(<= " + low.simplify_name() + " " + idx.simplify_name() + ")"); 3871 conditions.add("(<= " + idx.simplify_name() + " " + high.simplify_name() + ")"); 3872 if (elementwise && (i >= 1)) { 3873 VarInfoName[] _boundv = qret.bound_vars.get(i - 1); 3874 VarInfoName _idx = _boundv[0], _low = _boundv[1]; 3875 if (_low.simplify_name().equals(low.simplify_name())) { 3876 conditions.add("(EQ " + _idx.simplify_name() + " " + idx.simplify_name() + ")"); 3877 } else { 3878 conditions.add(" (EQ (- " + _idx.simplify_name() + " " + _low.simplify_name() + ")"); 3879 conditions.add("(- " + idx.simplify_name() + " " + low.simplify_name() + "))"); 3880 } 3881 } 3882 if (i == 1 && (adjacent || distinct)) { 3883 VarInfoName[] _boundv = qret.bound_vars.get(i - 1); 3884 VarInfoName prev_idx = _boundv[0]; 3885 if (adjacent) { 3886 conditions.add( 3887 "(EQ (+ " + prev_idx.simplify_name() + " 1) " + idx.simplify_name() + ")"); 3888 } 3889 if (distinct) { 3890 conditions.add("(NEQ " + prev_idx.simplify_name() + " " + idx.simplify_name() + ")"); 3891 } 3892 } 3893 } 3894 } 3895 result[0] = "(FORALL (" + int_list + ") (IMPLIES (AND " + conditions + ") "; 3896 3897 // stringify the terms 3898 for (int i = 0; i < qret.root_primes.length; i++) { 3899 result[i + 1] = qret.root_primes[i].simplify_name(); 3900 } 3901 3902 // stringify the indices, if requested 3903 // note that the index should be relative to the slice, not relative 3904 // to the original array (we used to get this wrong) 3905 if (includeIndex) { 3906 for (int i = 0; i < qret.root_primes.length; i++) { 3907 VarInfoName[] boundv = qret.bound_vars.get(i); 3908 VarInfoName idx_var = boundv[0]; 3909 String idx_var_name = idx_var.simplify_name(); 3910 String lower_bound = qret.bound_vars.get(i)[1].simplify_name(); 3911 String idx_expr = "(- " + idx_var_name + " " + lower_bound + ")"; 3912 result[i + qret.root_primes.length + 1] = idx_expr; 3913 } 3914 } 3915 3916 result[result.length - 1] = "))"; // close IMPLIES, FORALL 3917 3918 return result; 3919 } 3920 3921 // Important Note: The Java quantification style actually makes no 3922 // sense as is. The resultant quantifications are statements as 3923 // opposed to expressions, and thus no value can be derived from 3924 // them. This must be fixed before the java statements are of any 3925 // value. However, the ESC and JML quantifications are fine because 3926 // they actually produce expressions with values. 3927 3928 // <root*> -> <string string* string> 3929 /** 3930 * Given a list of roots, return a String array where the first element is a Java-style 3931 * quantification over newly-introduced bound variables, the last element is a closer, and the 3932 * other elements are java-named strings for the provided roots (with sequences subscripted by 3933 * one of the new bound variables). 3934 */ 3935 // public static String[] format_java(VarInfoName[] roots) { 3936 // return format_java(roots, false); 3937 // } 3938 // public static String[] format_java(VarInfoName[] roots, boolean elementwise) { 3939 // return format_java_style(roots, false, true, OutputFormat.JAVA); 3940 // } 3941 3942 // This set of functions quantifies in the same manner to the ESC quantification, except that 3943 // JML names are used instead of ESC names, and minor formatting changes are incorporated 3944 // public static String[] format_jml(QuantifyReturn qret) { 3945 // return format_java_style(qret, false, true, OutputFormat.JML); 3946 // } 3947 // public static String[] format_jml(QuantifyReturn qret, boolean elementwise) { 3948 // return format_java_style(qret, elementwise, true, OutputFormat.JML); 3949 // } 3950 // public static String[] format_jml(QuantifyReturn qret, boolean elementwise, boolean 3951 // forall) { 3952 // return format_java_style(qret, elementwise, forall, OutputFormat.JML); 3953 // } 3954 3955 // This set of functions assists in quantification for all of the java style 3956 // output formats, that is, Java, ESC, and JML. It does the actual work behind 3957 // those formatting functions. This function was meant to be called only through 3958 // the other public formatting functions. 3959 // 3960 // The OutputFormat must be one of those three previously mentioned. 3961 // Also, if the Java format is selected, forall must be true. 3962 3963 protected static String[] format_java_style(VarInfoName[] roots, OutputFormat format) { 3964 return format_java_style(roots, false, true, format); 3965 } 3966 3967 protected static String[] format_java_style( 3968 VarInfoName[] roots, boolean elementwise, OutputFormat format) { 3969 return format_java_style(roots, elementwise, true, format); 3970 } 3971 3972 protected static String[] format_java_style( 3973 VarInfoName[] roots, boolean elementwise, boolean forall, OutputFormat format) { 3974 assert roots != null; 3975 3976 QuantifyReturn qret = quantify(roots); 3977 3978 return format_java_style(qret, elementwise, forall, format); 3979 } 3980 3981 // This form allows the indicies and bounds to be modified before quantification 3982 protected static String[] format_java_style(QuantifyReturn qret, OutputFormat format) { 3983 return format_java_style(qret, false, true, format); 3984 } 3985 3986 protected static String[] format_java_style( 3987 QuantifyReturn qret, boolean elementwise, OutputFormat format) { 3988 return format_java_style(qret, elementwise, true, format); 3989 } 3990 3991 protected static String[] format_java_style( 3992 QuantifyReturn qret, boolean elementwise, boolean forall, OutputFormat format) { 3993 // build the "\forall ..." predicate 3994 String[] result = new String[qret.root_primes.length + 2]; 3995 StringBuilder int_list, conditions, closing; 3996 { 3997 // "i, j, ..." 3998 int_list = new StringBuilder(); 3999 // "ai <= i && i <= bi && aj <= j && j <= bj && ..." 4000 // if elementwise, also do "(i-ai) == (b-bi) && ..." 4001 conditions = new StringBuilder(); 4002 closing = new StringBuilder(); 4003 for (int i = 0; i < qret.bound_vars.size(); i++) { 4004 VarInfoName[] boundv = qret.bound_vars.get(i); 4005 VarInfoName idx = boundv[0], low = boundv[1], high = boundv[2]; 4006 if (i != 0) { 4007 int_list.append(", "); 4008 conditions.append(" && "); 4009 } 4010 closing.append(quant_increment(idx, i, format)); 4011 4012 int_list.append(quant_var_initial_state(idx, low, format)); 4013 conditions.append(quant_execution_condition(low, idx, high, format)); 4014 4015 if (elementwise && (i >= 1)) { 4016 VarInfoName[] _boundv = qret.bound_vars.get(i - 1); 4017 VarInfoName _idx = _boundv[0], _low = _boundv[1]; 4018 if (format == OutputFormat.JAVA) { 4019 conditions.append(" || "); 4020 } else { 4021 conditions.append(" && "); 4022 } 4023 4024 conditions.append(quant_element_conditions(_idx, _low, idx, low, format)); 4025 } 4026 } 4027 } 4028 4029 if (forall) { 4030 result[0] = quant_format_forall(format); 4031 } else { 4032 result[0] = quant_format_exists(format); 4033 } 4034 4035 result[0] += 4036 (int_list 4037 + quant_separator1(format) 4038 + conditions 4039 + quant_separator2(format) 4040 + closing 4041 + quant_step_terminator(format)); 4042 result[result.length - 1] = ")"; 4043 4044 // stringify the terms 4045 for (int i = 0; i < qret.root_primes.length; i++) { 4046 result[i + 1] = qret.root_primes[i].name_using(format, null); 4047 } 4048 4049 return result; 4050 } 4051 4052 // This set of functions are helper functions to the quantification function. 4053 4054 /** 4055 * This function creates a string that represents how to increment the variables involved in 4056 * quantification. Since the increment is not stated explicitly in the JML and ESC formats this 4057 * function merely returns an empty string for those formats. 4058 */ 4059 protected static String quant_increment(VarInfoName idx, int i, OutputFormat format) { 4060 if (format != OutputFormat.JAVA) { 4061 return ""; 4062 } else { 4063 if (i != 0) { 4064 return (", " + idx.esc_name() + "++"); 4065 } else { 4066 return (idx.esc_name() + "++"); 4067 } 4068 } 4069 } 4070 4071 /** 4072 * This function returns a string that represents the initial condition for the index variable. 4073 */ 4074 protected static String quant_var_initial_state( 4075 VarInfoName idx, VarInfoName low, OutputFormat format) { 4076 if (format == OutputFormat.JAVA) { 4077 return idx.esc_name() + " == " + low.esc_name(); 4078 } else { 4079 return idx.name_using(format, null); 4080 } 4081 } 4082 4083 /** 4084 * This function returns a string that represents the execution condition for the 4085 * quantification. 4086 */ 4087 protected static String quant_execution_condition( 4088 VarInfoName low, VarInfoName idx, VarInfoName high, OutputFormat format) { 4089 if (format == OutputFormat.JAVA) { 4090 return idx.esc_name() + " <= " + high.esc_name(); 4091 } else { 4092 return low.name_using(format, null) 4093 + " <= " 4094 + idx.name_using(format, null) 4095 + " && " 4096 + idx.name_using(format, null) 4097 + " <= " 4098 + high.name_using(format, null); 4099 } 4100 } 4101 4102 /** 4103 * This function returns a string representing the extra conditions necessary if the 4104 * quantification is element-wise. 4105 */ 4106 protected static String quant_element_conditions( 4107 VarInfoName _idx, VarInfoName _low, VarInfoName idx, VarInfoName low, OutputFormat format) { 4108 StringBuilder conditions = new StringBuilder(); 4109 4110 if (ZERO.equals(_low)) { 4111 conditions.append(_idx.name_using(format, null)); 4112 } else { 4113 conditions.append("("); 4114 conditions.append(_idx.name_using(format, null)); 4115 conditions.append("-("); 4116 conditions.append(_low.name_using(format, null)); 4117 conditions.append("))"); 4118 } 4119 conditions.append(" == "); 4120 if (ZERO.equals(low)) { 4121 conditions.append(idx.name_using(format, null)); 4122 } else { 4123 conditions.append("("); 4124 conditions.append(idx.name_using(format, null)); 4125 conditions.append("-("); 4126 conditions.append(low.name_using(format, null)); 4127 conditions.append("))"); 4128 } 4129 4130 return conditions.toString(); 4131 } 4132 4133 /** 4134 * This function returns a string representing how to format a forall statement in a given 4135 * output mode. 4136 */ 4137 protected static String quant_format_forall(OutputFormat format) { 4138 if (format == OutputFormat.JAVA) { 4139 return "(for (int "; 4140 } else { 4141 return "(\\forall int "; 4142 } 4143 } 4144 4145 /** 4146 * This function returns a string representing how to format an exists statement in a given 4147 * output mode. 4148 */ 4149 protected static String quant_format_exists(OutputFormat format) { 4150 return "(\\exists int "; 4151 } 4152 4153 /** 4154 * This function returns a string representing how to format the first seperation in the 4155 * quantification, that is, the one between the intial condition and the execution condition. 4156 */ 4157 protected static String quant_separator1(OutputFormat format) { 4158 if (format == OutputFormat.JML) { 4159 return "; "; 4160 } else { 4161 return "; ("; 4162 } 4163 } 4164 4165 /** 4166 * This function returns a string representing how to format the second seperation in the 4167 * quantification, that is, the one between the execution condition and the assertion. 4168 */ 4169 protected static String quant_separator2(OutputFormat format) { 4170 if (format == OutputFormat.ESCJAVA) { 4171 return ") ==> "; 4172 } else { 4173 return "; "; 4174 } 4175 } 4176 4177 /** 4178 * This function returns a string representing how to format the final seperation in the 4179 * quantification, that is, the one between the assertion and any closing symbols. 4180 */ 4181 protected static String quant_step_terminator(OutputFormat format) { 4182 if (format == OutputFormat.JAVA) { 4183 return ")"; 4184 } 4185 return ""; 4186 } 4187 } // QuantHelper 4188 4189 // Special JML capability, since JML cannot format a sequence of elements, 4190 // often what is wanted is the name of the reference (we have a[], we want 4191 // a. This function provides the appropriate name for these circumstances. 4192 public VarInfoName JMLElementCorrector() { 4193 if (this instanceof Elements) { 4194 return ((Elements) this).term; 4195 } else if (this instanceof Slice) { 4196 return ((Slice) this).sequence.term; 4197 } else if (this instanceof Prestate) { 4198 return ((Prestate) this).term.JMLElementCorrector().applyPrestate(); 4199 } else if (this instanceof Poststate) { 4200 return ((Poststate) this).term.JMLElementCorrector().applyPoststate(); 4201 } 4202 return this; 4203 } 4204 4205 // ============================================================ 4206 // Transformation framework 4207 4208 /** Specifies a function that performs a transformation on VarInfoNames. */ 4209 public interface Transformer { 4210 /** Perform a transformation on the argument. */ 4211 public VarInfoName transform(VarInfoName v); 4212 } 4213 4214 /** A pass-through transformer. */ 4215 public static final Transformer IDENTITY_TRANSFORMER = 4216 new Transformer() { 4217 @Override 4218 public VarInfoName transform(VarInfoName v) { 4219 return v; 4220 } 4221 }; 4222 4223 /** Compare VarInfoNames alphabetically. */ 4224 public static class LexicalComparator implements Comparator<VarInfoName> { 4225 @Pure 4226 @Override 4227 public int compare(VarInfoName name1, VarInfoName name2) { 4228 return name1.compareTo(name2); 4229 } 4230 } 4231}