JML

org.multijava.mjc
Class TypeLoader

java.lang.Object
  extended byorg.multijava.util.Utils
      extended byorg.multijava.mjc.TypeLoader
All Implemented Interfaces:
CClass.Observer, Cloneable
Direct Known Subclasses:
JmlTypeLoader

public class TypeLoader
extends Utils
implements CClass.Observer

This class acts as a symbol table and a cache for types, type signatures, and external generic functions. It includes methods to load unknown type signatures. It maintains a mapping from fully qualified names to the CClass instances representing their signatures. Specifically the mapping is from a fully qualified type name to a set of instances that can be sorted. In MultiJava that set is a singleton set; however, for tools like JML where a single fully qualified name can refer to a specification and one or more refinements to that specification, the set may contain multiple items.


Field Summary
private  HashMap compilationSessionRepCache
          Maintains a mapping of qualified names to type representations; that is, it maps a fully qualified name to the CClassType instance that represents the type.
protected  MjcHashRelation compilationSessionTypeCache
          This relation stores a mapping from fully qualified type names to their CClass instances.
protected  FileFinder fileFinder
           
private  String oldClassPath
           
private static TypeLoader singletonInstance
           
private  HashMap vmSessionRepCache
          Maintains a mapping of qualified names to type representations; that is, it maps a fully qualified name to the CClassType instance that represents the type.
protected  MjcHashRelation vmSessionTypeCache
          This relation stores a mapping from fully qualified type names to their CClass instances.
 
Fields inherited from class org.multijava.util.Utils
DBG_LEVEL_HIGH, DBG_LEVEL_LOW, DBG_LEVEL_NO
 
Constructor Summary
private TypeLoader()
           
protected TypeLoader(FileFinder fileFinder)
          This constructor is only for use by subclasses.
 
Method Summary
 boolean addToTypeCache(CClass typ)
          Adds the given source class to the table of loaded classes.
 void addTypeRep(String qName, CClassType typeRep)
          Adds the given type representation, which must represent a fully qualified type name, to the cache.
protected  boolean checkUniqueness(CClass typ, CClass last)
          Returns true if typ is a legal unique type declaration.
 boolean classExists(String qName)
          Checks whether a class with the given name is available in the class path.
protected  ClassInfo createClassInfo(String qName)
          Creates and returns a class info object by reading the symbol file for the class with the given fully qualified name qName.
 FileFinder fileFinder()
          Returns the FileFinder instance that is used by the current loader when searching for classes and generic functions.
 ClassPath.ClassDescription find(String name)
          This method finds a file for the given class name; it looks for both a java file on the source path and a class file on the class path, returning the newer one if both are found (and null if neither is found).
 ClassPath.ClassDescription findSourceFile(String name)
           
protected  void forgetEverythingAbout(File f, JCompilationUnitType cunit)
          Called by Main when the given file, from which the given compilation unit AST was derived, did not contain an expected result; this method removes all cached info. for the file.
static TypeLoader getSingleton()
           
 CClassType getTypeRep(String name, CUniverse univ, CClassType[][] arguments, boolean isFullyQualified)
          Returns the lightweight type representation of the class with the given name, generating a new one if necessary.
 void initSession()
          Empties the compilation session caches to prepare for a new compilation session.
 boolean isDeclaredInDifferentSourceFiles(boolean isUnique, CClass clazz)
          This method is needed so it can be overridden by JML in order to handle classes that have been refined, e.g., when its specifications have intentionally been declared in a separate file.
protected  boolean isTrusted(String qName)
          Returns true if the information for the type or package of the given qualified name should be retained for subsequent compilation sessions.
 boolean isTypeLoaded(String qName)
          Checks whether a class with the given name has already been successfully loaded.
 CClass loadType(String qName)
           
 CClass lookupType(String qName)
          Returns the first CClass instance in the set mapped to by the given fully qualified name, or null if no such instance exists.
 CClassType lookupTypeRep(String qName)
           
private static boolean mayShare(CClassType type, CUniverse univ, CClassType[][] arguments)
          Returns whether the given type can be shared by another type having the given univ and type arguments.
 CClass reloadType(CClass clazz)
          Reloads the specified class if this class has been defined during a previous compilation session.
protected  void removeFromTypeCache(CClass typ)
          Removes the qualified name of the given source class from the table of loaded classes (so it can be reloaded without causing conflicts).
 void signatureCompleted(CClass typ)
          Implements CClass.Observer by moving typ from compilationSessionTypeCache to vmSessionTypeCache if typ is trusted.
 
Methods inherited from class org.multijava.util.Utils
assertTrue, assertTrue, combineArrays, escapeString, escapeString, fail, fail, getFilePath, hasFlag, hasOtherFlags, parsePathParts, relativePathTo, splitQualifiedName, splitQualifiedName, stripJavaModifiers, stripNonJavaModifiers, stripPrivateModifier, unescapeString, vectorToArray, vectorToIntArray
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

compilationSessionTypeCache

protected MjcHashRelation compilationSessionTypeCache
This relation stores a mapping from fully qualified type names to their CClass instances. The mappings are for the types processed during this compilation session that are likely to change for the next compilation session.

See Also:
vmSessionTypeCache, isTrusted(String)

vmSessionTypeCache

protected MjcHashRelation vmSessionTypeCache
This relation stores a mapping from fully qualified type names to their CClass instances. The mappings are for the types processed during this compilation session that are not likely to change for subsequent compilation sessions and that have been processed to the point that they can be used for field and method lookup.

See Also:
compilationSessionTypeCache, isTrusted(String)

compilationSessionRepCache

private HashMap compilationSessionRepCache
Maintains a mapping of qualified names to type representations; that is, it maps a fully qualified name to the CClassType instance that represents the type. The mappings are for the types processed during this compilation session that are likely to change for the next compilation session.

See Also:
vmSessionRepCache, isTrusted(String)

vmSessionRepCache

private HashMap vmSessionRepCache
Maintains a mapping of qualified names to type representations; that is, it maps a fully qualified name to the CClassType instance that represents the type. The mappings are for the types processed during this compilation session that are not likely to change for the next compilation session.

See Also:
compilationSessionRepCache, isTrusted(String)

fileFinder

protected FileFinder fileFinder

oldClassPath

private String oldClassPath

singletonInstance

private static TypeLoader singletonInstance
Constructor Detail

TypeLoader

private TypeLoader()

TypeLoader

protected TypeLoader(FileFinder fileFinder)
This constructor is only for use by subclasses. Clients should use the factory method getSingleton().

See Also:
getSingleton()
Method Detail

getSingleton

public static TypeLoader getSingleton()

getTypeRep

public CClassType getTypeRep(String name,
                             CUniverse univ,
                             CClassType[][] arguments,
                             boolean isFullyQualified)
Returns the lightweight type representation of the class with the given name, generating a new one if necessary.

Parameters:
name - the name of the class
isFullyQualified - the name is known to be fully qualified
Returns:
an object representing the type of the named class (singleton within this compilation session if isFullyQualified)

 requires name != null;
 modifies compilationSessionRepCache;
 ensures isFullyQualified ==> 
   compilationSessionRepCache.containsKey(name) ||
   vmSessionRepCache.containsKey(name);
 

mayShare

private static boolean mayShare(CClassType type,
                                CUniverse univ,
                                CClassType[][] arguments)
Returns whether the given type can be shared by another type having the given univ and type arguments. This is the case iff the Universe modifier and the type arguments of the type are equivalent to the ones provided here.

Parameters:
type - The target type.
univ - The Universe modifier.
arguments - The generic type arguments.
Returns:
Whether the given type may be shared.

lookupTypeRep

public CClassType lookupTypeRep(String qName)

addTypeRep

public void addTypeRep(String qName,
                       CClassType typeRep)
Adds the given type representation, which must represent a fully qualified type name, to the cache.

 requires qName != null && typeRep != null &&
          (* all separators in qName are '/' not '.' *);
 modifies compilationSessionRepCache, vmSessionRepCache;
 ensures compilationSessionRepCache.containsKey(qName) ||
         vmSessionRepCache.containsKey(qName);
 


findSourceFile

public ClassPath.ClassDescription findSourceFile(String name)

find

public ClassPath.ClassDescription find(String name)
This method finds a file for the given class name; it looks for both a java file on the source path and a class file on the class path, returning the newer one if both are found (and null if neither is found).


addToTypeCache

public boolean addToTypeCache(CClass typ)
Adds the given source class to the table of loaded classes. Returns true if the class was not declared in more than one source file and false otherwise.

requires typ != null;
modifies compilationSessionTypeCache, vmSessionTypeCache;
 


checkUniqueness

protected boolean checkUniqueness(CClass typ,
                                  CClass last)
Returns true if typ is a legal unique type declaration.

Parameters:
typ - a type to be added to the cache
last - the previous cache entry mapped to by typ.qualifiedName()

forgetEverythingAbout

protected void forgetEverythingAbout(File f,
                                     JCompilationUnitType cunit)
Called by Main when the given file, from which the given compilation unit AST was derived, did not contain an expected result; this method removes all cached info. for the file.


removeFromTypeCache

protected void removeFromTypeCache(CClass typ)
Removes the qualified name of the given source class from the table of loaded classes (so it can be reloaded without causing conflicts). This is only done if the conflict occurs because the names were added during two different compilation sessions.

    requires typ != null;
    modifies compilationSessionTypeCache, vmSessionTypeCache;
 


lookupType

public CClass lookupType(String qName)
Returns the first CClass instance in the set mapped to by the given fully qualified name, or null if no such instance exists.

  requires qName != null && 
	    (* any separators in qName are slashes ('/'), not dots ('.') *);
 


loadType

public CClass loadType(String qName)

createClassInfo

protected ClassInfo createClassInfo(String qName)
Creates and returns a class info object by reading the symbol file for the class with the given fully qualified name qName. If no symbol file is found, null is returned. This method also create a binary class object and adds it to the system cache. This is a factory method that may be overridden by subclasses.


reloadType

public CClass reloadType(CClass clazz)
Reloads the specified class if this class has been defined during a previous compilation session. Note that this method can return either null or CLS_UNDEFINED or a valid CClass value.


isTypeLoaded

public boolean isTypeLoaded(String qName)
Checks whether a class with the given name has already been successfully loaded.

Parameters:
qName - the fully qualified name of the type with slash separators not dots
Returns:
true iff the class has already been loaded.

classExists

public boolean classExists(String qName)
Checks whether a class with the given name is available in the class path. Note that this is true if the class has already been successfully loaded or if there is a file that can be expected to hold its definition. The file may actually not hold a valid definition, so classExists is not a guarantee that the class with the given name actually does exist.

Parameters:
qName - the fully qualified name of the type with slash separators not dots
Returns:
true iff the class is in the class path

isDeclaredInDifferentSourceFiles

public boolean isDeclaredInDifferentSourceFiles(boolean isUnique,
                                                CClass clazz)
This method is needed so it can be overridden by JML in order to handle classes that have been refined, e.g., when its specifications have intentionally been declared in a separate file. In MultiJava, this method always returns isUnique since addToTypeCache has already determined whether the Type has already been declared in another file.


signatureCompleted

public void signatureCompleted(CClass typ)
Implements CClass.Observer by moving typ from compilationSessionTypeCache to vmSessionTypeCache if typ is trusted.

 also
 old String qName = typ.qualifiedName();
 requires typ != null && isTrusted(qName);
 ensures \old(compilationSessionTypeCache.getImage(qName).contains(typ))
         ==> !compilationSessionTypeCache.getImage(qName).contains(typ) &&
             vmSessionTypeCache.getImage(qName).contains(typ);
 

Specified by:
signatureCompleted in interface CClass.Observer

isTrusted

protected boolean isTrusted(String qName)
Returns true if the information for the type or package of the given qualified name should be retained for subsequent compilation sessions.

  requires qName != null && (* package separators in qName are '/' not '.' *);
 


initSession

public void initSession()
Empties the compilation session caches to prepare for a new compilation session.

 requires (* ClassPath.init() has been called with to set the 
             class path for this upcoming session *);
 


fileFinder

public FileFinder fileFinder()
Returns the FileFinder instance that is used by the current loader when searching for classes and generic functions.


JML

JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.