org.jmlspecs.checker
Class JmlTypeLoader

java.lang.Object
  org.multijava.util.Utils
      org.multijava.mjc.TypeLoader
          org.jmlspecs.checker.JmlTypeLoader

All Implemented Interfaces:

CClass.Observer, Cloneable

public class JmlTypeLoader

extends TypeLoader

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 static CClass	currentHostClass
private  HashMap	fileASTs           A mapping from files to the ASTs parsed from those files.
private static HashSet	filesProcessed
private  HashMap	incompleteTasksByQName
private static JmlTypeLoader	singletonInstance
private static HashMap	typeDeclASTs           A mapping from CClass to JmlTypeDeclaration for traversal of "extends" and "implements" hierarchies.

 

Fields inherited from class org.multijava.mjc.TypeLoader

compilationSessionTypeCache, fileFinder, vmSessionTypeCache

 

Fields inherited from class org.multijava.util.Utils

DBG_LEVEL_HIGH, DBG_LEVEL_LOW, DBG_LEVEL_NO

 

Constructor Summary
private	JmlTypeLoader()
protected	JmlTypeLoader(JmlFileFinder finder)           Creates an instance with the given file finder.

 

Method Summary
void	activatePartiallyProcessedTask(JmlCompilationUnit cUnit)           Reactivate the task for the compilation unit cUnit.
void	activateSymbolTableBuild(String qName)           Reactivate the task for the qualified type name qName.
void	activateSymbolTableBuild(JmlCompilationUnit cUnit)           Reactivate the task for the compilation unit cUnit if the symbol table has not been built.
void	activateTypeCheck(String qName)           Reactivate the task for the qualified type name qName.
void	activateTypeCheck(JmlCompilationUnit cUnit)           Reactivate the task for the compilation unit cUnit if the symbol table has not been built.
boolean	addToTypeCache(CClass typ)           Adds the given source class to the table of available classes.
void	addTypeDeclAST(JmlTypeDeclaration decl)           Adds a JML type declaration into the database.
protected  boolean	checkUniqueness(CClass typ, CClass last)           Returns true if typ is a legal unique type declaration.
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.
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.
JCompilationUnitType	getCUnitAST(File f)           Returns the AST parsed from the given file, or null if no AST is cached for the given file (either because the file has not been parsed or because no AST was created when parsing the file.
static CClass	getCurrentHostClass()           Returns the nearest host class to the current context.
protected  String	getFileIdent(File f)           Returns the Java identifier associated with the name of the file contained in this file.
static JmlTypeLoader	getJmlSingleton()
JmlCompilationUnit	getSuspendedCUnit(String qName)           Look for partially processed compilation unit (if suspended) for the qualified type name qName.
void	initSession()           Empties the compilation session caches to prepare for a new compilation session.
JmlInterfaceDeclaration[]	interfacesOf(JmlTypeDeclaration typeDecl)           Returns the interfaces of a given JML type declaration.
boolean	isDeclaredInDifferentSourceFiles(boolean isUnique, CClass clazz)           Determines whether the given Class, using its fully qualified name, has been declared in more than one 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.
protected  void	loadMostRefinedType(JmlSourceClass sourceClass)           Loads the "most refined" source class of this type.
JCompilationUnitType	putCUnitAST(File f, JCompilationUnitType cunit)           Records a mapping from the given file to the given AST.
JmlTypeDeclaration	refinedDeclOf(JmlTypeDeclaration cdecl)           Returns the refined declaration of a given JML class declaration.
CClass	reloadType(CClass sourceClass)            also requires sourceClass !
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	removePartiallyProcessedTask(JmlCompilationUnit cUnit)
void	savePartiallyProcessedTask(JmlCompilationUnit cUnit)           Save the task in case it needs to be reactivated.
static void	setCurrentHostClass(CClass sourceClass)           Records the host class nearest to the current context which is used by the method reloadType.
JmlClassDeclaration	superClassOf(JmlClassDeclaration cdecl)           Returns the superclass of a given JML class declaration.
JmlClassDeclaration	superClassOf(CClass cls)           Returns the superclass of a given JML class declaration.
JmlTypeDeclaration	typeDeclarationOf(CClass typ)           Returns the JML type declaration corresponding to the given source class; null is returned if no corresponding JML type declaration is found in the database.

 

Methods inherited from class org.multijava.mjc.TypeLoader

addTypeRep, classExists, fileFinder, find, findSourceFile, getSingleton, getTypeRep, isTypeLoaded, loadType, lookupType, lookupTypeRep, signatureCompleted

 

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

filesProcessed

private static HashSet filesProcessed

fileASTs

private HashMap fileASTs

A mapping from files to the ASTs parsed from those files. Note that the domain of this map is not necessarily equal to the filesProcessed set.

incompleteTasksByQName

private HashMap incompleteTasksByQName

typeDeclASTs

private static HashMap typeDeclASTs

A mapping from CClass to JmlTypeDeclaration for traversal of "extends" and "implements" hierarchies.

 invariant typeDeclASTs != null;
 

currentHostClass

private static CClass currentHostClass

singletonInstance

private static JmlTypeLoader singletonInstance

JmlTypeLoader

private JmlTypeLoader()

JmlTypeLoader

protected JmlTypeLoader(JmlFileFinder finder)

Creates an instance with the given file finder. This constructor is for use by subclass.

getJmlSingleton

public static JmlTypeLoader getJmlSingleton()

initSession

public void initSession()

Empties the compilation session caches to prepare for a new compilation session.

Overrides:

initSession in class TypeLoader

addToTypeCache

public boolean addToTypeCache(CClass typ)

Adds the given source class to the table of available classes. Returns true if the class was not declared in more than one source file and false otherwise.

 also
   requires typ != null;
   modifies compilationSessionTypeCache, filesProcessed;
 

Overrides:

addToTypeCache in class TypeLoader

getSuspendedCUnit

public JmlCompilationUnit getSuspendedCUnit(String qName)

Look for partially processed compilation unit (if suspended) for the qualified type name qName.

activateSymbolTableBuild

public void activateSymbolTableBuild(String qName)

Reactivate the task for the qualified type name qName.

activateSymbolTableBuild

public void activateSymbolTableBuild(JmlCompilationUnit cUnit)

Reactivate the task for the compilation unit cUnit if the symbol table has not been built.

activateTypeCheck

public void activateTypeCheck(String qName)

Reactivate the task for the qualified type name qName.

activateTypeCheck

public void activateTypeCheck(JmlCompilationUnit cUnit)

Reactivate the task for the compilation unit cUnit if the symbol table has not been built.

activatePartiallyProcessedTask

public void activatePartiallyProcessedTask(JmlCompilationUnit cUnit)

Reactivate the task for the compilation unit cUnit.

savePartiallyProcessedTask

public void savePartiallyProcessedTask(JmlCompilationUnit cUnit)

Save the task in case it needs to be reactivated.

removePartiallyProcessedTask

public void removePartiallyProcessedTask(JmlCompilationUnit cUnit)

checkUniqueness

protected boolean checkUniqueness(CClass typ,
                                  CClass last)

Returns true if typ is a legal unique type declaration.

Overrides:

checkUniqueness in class TypeLoader

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.

Overrides:

forgetEverythingAbout in class TypeLoader

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.

  also
    requires typ != null;
    modifies compilationSessionTypeCache, vmSessionTypeCache,
             filesProcessed;
 

Overrides:

removeFromTypeCache in class TypeLoader

setCurrentHostClass

public static void setCurrentHostClass(CClass sourceClass)

Records the host class nearest to the current context which is used by the method reloadType. This is needed so typechecking of refinement chains are handled properly.

getCurrentHostClass

public static CClass getCurrentHostClass()

Returns the nearest host class to the current context.

reloadType

public CClass reloadType(CClass sourceClass)

  also
    requires sourceClass != null;
 

Overrides:

reloadType in class TypeLoader

loadMostRefinedType

protected final void loadMostRefinedType(JmlSourceClass sourceClass)

Loads the "most refined" source class of this type.

    requires sourceClass != null;
    modifies compilationSessionTypeCache, vmSessionTypeCache,
             filesProcessed;
 

getFileIdent

protected String getFileIdent(File f)

Returns the Java identifier associated with the name of the file contained in this file. For example, if the file is named "MyClass.java" then this method returns "MyClass".

isDeclaredInDifferentSourceFiles

public boolean isDeclaredInDifferentSourceFiles(boolean isUnique,
                                                CClass clazz)

Determines whether the given Class, using its fully qualified name, has been declared in more than one file. This method is needed by JML in order to handle classes that have been refined, e.g., when its specifications have intentionally been declared in a separate file. Returns true if the class has been declared in more than one source file (unless refined), and false otherwise.

  also
    requires clazz != null; 
 

Overrides:

isDeclaredInDifferentSourceFiles in class TypeLoader

putCUnitAST

public final JCompilationUnitType putCUnitAST(File f,
                                              JCompilationUnitType cunit)

Records a mapping from the given file to the given AST.

getCUnitAST

public final JCompilationUnitType getCUnitAST(File f)

Returns the AST parsed from the given file, or null if no AST is cached for the given file (either because the file has not been parsed or because no AST was created when parsing the file.

addTypeDeclAST

public final void addTypeDeclAST(JmlTypeDeclaration decl)

Adds a JML type declaration into the database. The type declaration is assumed to have been interface-checked with its signature added to the signature forest, i.e., typeDecl.getCClass() != null.

 requires decl != null && decl.getCClass() != null &&
   !typeDeclASTs.containsKey(decl);
 

typeDeclarationOf

public final JmlTypeDeclaration typeDeclarationOf(CClass typ)

Returns the JML type declaration corresponding to the given source class; null is returned if no corresponding JML type declaration is found in the database.

 requires typ != null;
 

refinedDeclOf

public final JmlTypeDeclaration refinedDeclOf(JmlTypeDeclaration cdecl)

Returns the refined declaration of a given JML class declaration. If the given class is not a refining declaration, null is returned.

 requires cdecl != null && cdecl.getCClass() != null;
 

superClassOf

public final JmlClassDeclaration superClassOf(JmlClassDeclaration cdecl)

Returns the superclass of a given JML class declaration. If the given class has no superclass or its superclass is a binary class (i.e., not registered in the database), null is returned.

 requires cdecl != null && cdecl.getCClass() != null;
 

superClassOf

public final JmlClassDeclaration superClassOf(CClass cls)

Returns the superclass of a given JML class declaration. If the class has no superclass or its superclass is a binary class (i.e., not registered in the database), null is returned.

 requires cls != null;
 

interfacesOf

public final JmlInterfaceDeclaration[] interfacesOf(JmlTypeDeclaration typeDecl)

Returns the interfaces of a given JML type declaration. If the given type has no interface or all of its interfaces are binaries (i.e., not registered in the database), an empty array is returned. Binary interfaces, i.e., interfaces parsed from bytecode are omitted from the return array.

 requires typeDecl != null && typeDecl.getCClass() != null;
 

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.

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

Overrides:

isTrusted in class TypeLoader

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 creates a binary class object and adds it to the system cache. This method is overriden here to create JML-specific class info object and binary class object.

Overrides:

createClassInfo in class TypeLoader