    001    /* Copyright 2000, 2001, Compaq Computer Corporation */
    002
    003    package escjava.translate;
    004
    005    import javafe.util.Assert;
    006    import javafe.util.Location;
    007    import java.util.Hashtable;
    008
    009    import javafe.ast.*;
    010    import escjava.tc.Types;
    011    import escjava.ast.TagConstants;
    012
    013
    014    /**
    015     ** This class provides methods for unique-ifying names, as described
    016     ** in ESCJ 23b, "Unique names in ESC/Java".
    017     **
    018     ** Methods <code>suffixToString</code> and <code>suffixToLoc</code> call
    019     ** private method <code>parseSuffix</code> whose out-parameters are stored
    020     ** in some static fields of this class, these methods are not thread safe.
    021     ** (To make them thread safe, these numbers could be returned in a
    022     ** newly allocated array.)
    023     **/
    024
    025    public final class UniqName {
    026
    027      /**********************************************************************
    028       * Sets the "<em>default suffix file</em> to be that of location
    029       * <code>loc</code>, or to none if <code>loc</code> is the null location.
    030       * The default suffix file is used in the converting of a location to
    031       * a suffix and back.
    032       **********************************************************************/
    033
    034      private static int idDefaultSuffixFile = -1;
    035
    036      public static void setDefaultSuffixFile(int loc) {
    037          resetUnique();        // Make sure changed names don't cause problems
    038
    039          if (loc == Location.NULL)
    040              idDefaultSuffixFile = -1;
    041          else
    042              idDefaultSuffixFile = Location.toStreamId(loc);
    043      }
    044
    045      /**********************************************************************
    046       * Convert a location into a printable string suitable for use as a
    047       * suffix in unique-ifying a name declared at <code>loc</code>.
    048
    049       * <p>Precondition: <code>loc</code> should be a valid non-null location.
    050       * <p>Postcondition:  <code>\result != null</code>
    051       **********************************************************************/
    052
    053      //@ requires loc != Location.NULL;
    054      //@ ensures \result != null;
    055      public static String locToSuffix(int loc) {
    056            return locToSuffix(loc,true);
    057      }
    058
    059      //@ ensures \result != null;
    060      public static String locToSuffix(int loc, boolean useDefault) {
    061        Assert.notFalse(loc != Location.NULL);
    062
    063        int streamID = Location.toStreamId(loc);
    064        if (Location.isWholeFileLoc(loc))
    065          return streamID + "..";
    066
    067        String suffix = Location.toLineNumber(loc) + "." + Location.toColumn(loc);
    068            // We can't always use the default suffix file because we put label expressions
    069            // into preconditions during desugaring.  That way we can report the
    070            // location of a portion of a composite precondition.  But when the
    071            // precondition gets used by a routine in another file, the default
    072            // stream id has now changed and the suffix specified is invalid.
    073            // I think the only problem is extra characters in the communication
    074            // to and from Simplify. -- DRCok
    075        if (useDefault && streamID == idDefaultSuffixFile && !escjava.Main.options().guardedVC)
    076          return suffix;
    077        else
    078          return streamID + "." + suffix;
    079      }
    080
    081      /** Returns the location corresponding to <code>suffix</code>.
    082        * Requires <code>suffix</code> to be a valid suffix.
    083        **/
    084      public static int suffixToLoc(/*@ non_null @*/ String suffix) {
    085        return suffixToLoc(suffix, false);
    086      }
    087
    088      /** Returns the location corresponding to <code>suffix</code>, if any,
    089        * and the null location if <code>suffix</code> is not a valid suffix.
    090        * Requires <code>recoverable</code> or that <code>suffix</code> is
    091        * a valid suffix.
    092        **/
    093      public static int suffixToLoc(/*@ non_null @*/ String suffix,
    094                                    boolean recoverable)
    095      {
    096        if (parseSuffix(suffix, recoverable)) {
    097          return Location.make( psout0, psout1, psout2 );
    098        } else {
    099          return Location.NULL;
    100        }
    101      }
    102
    103      /**********************************************************************
    104       * Convert a location suffix string into a printable string that
    105       * describes the location.
    106       *
    107       * <p>Precondition: <code>suffix</code> should be a string previously
    108       * returned by <code>locToSuffix</code>, and the default suffix
    109       * file should be the same as it was when the corresponding
    110       * <code>locToSuffix</code> was called.
    111       *
    112       * Not thread safe.
    113       **********************************************************************/
    114
    115      //@ ensures \result != null;
    116      public static String suffixToString(/*@ non_null @*/ String suffix) {
    117        parseSuffix(suffix, false);
    118        String s = Location.streamIdToFile(psout0).getHumanName();
    119        if (psout1 == 0)
    120          return s + "(offset ?)";
    121        else
    122          return s + "(" + psout1 + "," + psout2 + ")";
    123      }
    124
    125      private static int psout0;
    126      private static int psout1;
    127      private static int psout2;
    128
    129      /** Parses <code>suffix</code>, which is expected to have one of the forms
    130        * <ul>
    131        * <li>  Number "." Number "." Number
    132        * <li>  Number "." Number
    133        * <li>  Number ".."
    134        * </ul>
    135        * The first form indicates a stream ID, a line number (1-based), and
    136        * and column number (0-based).
    137        * The second form indicates a line number and a column number, where
    138        * the implicit stream ID number is <code>idDefaultSuffixFile</code>.
    139        * The third form indicates a stream number, where the location that
    140        * was converted into this suffix string was a whole-file location
    141        * (this occurs if the location refers to a place in a .class file). <p>
    142        *
    143        * This method uses <code>psout0</code>, <code>psout1</code>, and
    144        * <code>psout2</code> as out parameters.  The will contain the values
    145        * of the stream ID, line number, and column number of the location parsed
    146        * from the suffix, or the stream ID and two 0's if the suffix has
    147        * the third form. <p>
    148        *
    149        * If <code>recoverable</code> is <code>true</code>, then this method
    150        * can be called even if <code>suffix</code> is not known to be a valid
    151        * suffix.  If it isn't, <code>false</code> is returned.  If
    152        * <code>suffix</code> is a valid suffix, then <code>true</code> is
    153        * returned. <p>
    154        *
    155        * Not thread safe (since global variables are used to contain out
    156        * parameters).
    157        **/
    158
    159      private static boolean parseSuffix(/*@ non_null @*/ String suffix,
    160                                         boolean recoverable)
    161      {
    162        // These numbers will be shifted as dots are discovered
    163        int a0 = 0;
    164        int a1 = idDefaultSuffixFile;
    165        int a2 = 0;
    166
    167        int cDots = 0;
    168        for (int k = 0; k < suffix.length(); k++) {
    169          char ch = suffix.charAt(k);
    170          switch (ch) {
    171            case '0':
    172            case '1':
    173            case '2':
    174            case '3':
    175            case '4':
    176            case '5':
    177            case '6':
    178            case '7':
    179            case '8':
    180            case '9':
    181              a2 = a2 * 10 + (ch - '0');
    182              break;
    183            case '.':
    184              cDots++;
    185              a0 = a1;  a1 = a2;  a2 = 0;
    186              break;
    187            default:
    188              if (recoverable) {
    189                return false;
    190              }
    191              //@ unreachable;
    192              Assert.fail("unexpected character '" + ch +
    193                          "' in purported location suffix '" + suffix + "'");
    194              break;
    195          }
    196        }
    197
    198        if (! (cDots == 2 || (cDots == 1 && idDefaultSuffixFile != -1))) {
    199          if (recoverable) {
    200            return false;
    201          }
    202          //@ unreachable;
    203          Assert.fail("wrong number of dots in purported location suffix '" +
    204                      suffix + "'");
    205        }
    206
    207        // set out parameters
    208        psout0 = a0;
    209        psout1 = a1;
    210        psout2 = a2;
    211
    212        return true;
    213      }
    214
    215
    216        /**
    217         ** Returns the unique-ification of the type <code>t</code>. <p>
    218         **
    219         ** Handles case 7 of ESCJ 23b. <p>
    220         **/
    221        //@ ensures \result != null;
    222        public static String type(/*@ non_null */ Type t) {
    223            /*
    224             * Special case primitive type TYPE to avoid confusion with any
    225             * reference type named "TYPE":
    226             */
    227            if (t instanceof PrimitiveType
    228                    && ((PrimitiveType)t).tag==TagConstants.TYPECODE)
    229                return "T_.TYPE";
    230                    // FIXME - TYPE-EQUIV
    231               // return "T_" + Types.printName(Types.javaLangClass());
    232
    233            return "T_" + Types.printName(t);
    234        }
    235
    236
    237        /***************************************************
    238         *                                                 *
    239         * Producing names for variables:                  *
    240         *                                                 *
    241         ***************************************************/
    242
    243        /**
    244         ** Use this location *only* in declarations of special variables
    245         ** (see case 4 of ESCJ 23b for the complete list of these).
    246         **/
    247        public static final int specialVariable =
    248                    Location.createFakeLoc("<special variable>");
    249
    250        /**
    251         ** Use this location *only* in declarations of temporary variables
    252         ** (see case 6 of ESCJ 23b for rules on the names allowed for these).
    253         **/
    254        public static final int temporaryVariable =
    255                    Location.createFakeLoc("<temporary variable>");
    256
    257        /**
    258         ** Use this location *only* in declarations of automatically
    259         ** generated bound variables.  (See case 3 of ESCJ 23b for rules on
    260         ** the names allowed for these).
    261         **/
    262        private static final int autoBoundVariable =
    263                    Location.createFakeLoc("<bound variable>");
    264
    265
    266        /**
    267         ** Returns a new bound variable for use in a quantificiation, where
    268         ** we do not wish to or cannot associate the variable with an
    269         ** existing VariableAccess. <p>
    270         **
    271         ** See newBoundThis() for an important exceptional case, though.<p>
    272         **
    273         ** The resulting name will be of the form "<prefix>".<p>
    274         **
    275         ** (This partially handles case 3 of ESCJ 23b.)
    276         **/
    277        //@ ensures \result != null;
    278        public static LocalVarDecl newBoundVariable(char prefix) {
    279            return newBoundVariable(String.valueOf(prefix));
    280        }
    281
    282        /**
    283         ** Returns a new bound variable for use in quantifying over "this" in
    284         ** an invariant. <p>
    285         **
    286         ** The resulting name will be of the form "brokenObj".
    287         **
    288         ** (This partially handles case 3 of ESCJ 23b.)
    289         **/
    290        //@ ensures \result != null;
    291        public static LocalVarDecl newBoundThis() {
    292            return newBoundVariable("brokenObj");
    293        }
    294
    295        /**
    296         ** Private routine to create a new bound variable for use in a
    297         ** quantificiation, where we do not wish to or cannot associate the
    298         ** variable with an existing VariableAccess. <p>
    299         **
    300         ** This handles case 3 of ESCJ 23b.
    301         **/
    302        //@ ensures \result != null;
    303        public static LocalVarDecl newBoundVariable(/*@ non_null @*/ String name) {
    304            Identifier id = Identifier.intern(name);
    305            return LocalVarDecl.make(Modifiers.NONE,  // Java modifiers
    306                                     null,            // pragma modifiers
    307                                     id,
    308                                     Types.anyType,
    309                                     autoBoundVariable,
    310                                     null, Location.NULL); // initializer
    311        }
    312
    313
    314        /**
    315         ** Returns a new intermediate-state variable
    316         ** associated with an existing VariableAccess. <p>
    317         **
    318         ** The resulting name will be of the form
    319         ** <last segment of name>:<location>, where <location> is the
    320         ** location of the variable reference in the given VariableAccess
    321         ** if available, and the location of the variable declaration
    322         ** otherwise. <p>
    323         **
    324         ** This handles case 15 of ESCJ 23b.
    325         **/
    326        //@ ensures \result != null;
    327        //@ ensures \result.id == v.id;
    328        public static LocalVarDecl newIntermediateStateVar(/*@ non_null */ VariableAccess v,
    329                                                           /*@ non_null */ String suffix) {
    330            int loc = v.loc;
    331            if (loc==Location.NULL)
    332                loc = v.decl.locId;
    333
    334            Identifier id;
    335            if (suffix.length() == 0) {
    336                id = v.id;
    337            } else {
    338                id = Identifier.intern(v.id.toString() + suffix);
    339            }
    340            return LocalVarDecl.make( Modifiers.NONE,
    341                                      null,
    342                                      id,
    343                                      v.decl.type,
    344                                      loc,
    345                                      null, Location.NULL );
    346        }
    347
    348        //@ ensures \result != null;
    349        //@ ensures \result.id == vd.id;
    350        public static LocalVarDecl newIntermediateStateVar(/*@ non_null */ GenericVarDecl vd,
    351                                                           /*@ non_null */ String suffix) {
    352            int loc = vd.locId;
    353
    354            Identifier id;
    355            if (suffix.length() == 0) {
    356                id = vd.id;
    357            } else {
    358                id = Identifier.intern(vd.id.toString() + suffix);
    359            }
    360            return LocalVarDecl.make( Modifiers.NONE,
    361                                      null,
    362                                      id,
    363                                      vd.type,
    364                                      loc,
    365                                      null, Location.NULL );
    366        }
    367
    368
    369        /**
    370         ** Returns the unique-ification of the variable <code>v</code>. <p>
    371         **
    372         ** Handles cases 3, 4, 6, 10, 11, 12, 13 and 15 of ESCJ 23b. <p>
    373         **/
    374        //@ ensures \result != null;
    375        public static String variable(/*@ non_null @*/ GenericVarDecl v) {
    376            String s = v.id.toString();
    377            int loc = v.locId;
    378
    379            if (loc==autoBoundVariable) {
    380                // Case 3:
    381                return verifyUnique(v,s);
    382            } else if (loc==specialVariable) {
    383                // Case 4, (part of) 13:
    384                return verifyUnique(v,s);
    385            } else if (loc==temporaryVariable) {
    386                // Case 6:
    387                return verifyUnique(v,s);
    388            } else if (loc != Location.NULL) {
    389                // Cases 10, 11, 12, (part of) 13, 15:
    390                // All of these produce '<last segment of name>:<location>':
    391                return verifyUnique(v, s+":"+locToSuffix(loc));
    392            } else {
    393                // This shouldn't happen...
    394                // Assert.fail("GenericVarDecl with NULL location: "+ v.id);
    395
    396                return verifyUnique(v,s+":unknown");
    397            }
    398        }
    399
    400
    401        /***************************************************
    402         *                                                 *
    403         * Ensuring unique names for variables:            *
    404         *                                                 *
    405         ***************************************************/
    406
    407        private static /*@ non_null @*/ Hashtable mapObjStr = new Hashtable();
    408        private static /*@ non_null @*/ Hashtable mapStrObj = new Hashtable();
    409
    410        /**
    411         ** Reset the <n>-uniqueness-ensuring mechanism.
    412         **/
    413        public static void resetUnique() {
    414            mapObjStr = new Hashtable();
    415            mapStrObj = new Hashtable();
    416        }
    417
    418
    419        //@ ensures \result != null;
    420        private static String verifyUnique(/*@ non_null @*/ GenericVarDecl o,
    421                                           /*@ non_null @*/ String s) {
    422            String s2 = (String)mapObjStr.get(o);
    423            if( s2 != null ) {
    424                // Mapping already initialized, use it
    425                return s2;
    426            } else {
    427                // Mapping not initialized, so initialize it
    428                // Prefer s, if not already used
    429
    430                String s3 = s.intern();
    431                int i=0;
    432
    433                for(;;) {
    434                    if( mapStrObj.get(s3) == null ) {
    435                        // s does not clash with existing name
    436                        mapObjStr.put( o, s3 );
    437                        mapStrObj.put( s3, o );
    438                        return s3;
    439                    }
    440                    // Increment i, and try new postfix
    441                    i++;
    442                    s3 = (s+"<"+i+">").intern();
    443                }
    444            }
    445        }
    446
    447    }