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 }