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    }