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 }