JML

org.jmlspecs.checker
Class JmlTypeLoader

java.lang.Object
  extended byorg.multijava.util.Utils
      extended byorg.multijava.mjc.TypeLoader
          extended byorg.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
Constructor Detail

JmlTypeLoader

private JmlTypeLoader()

JmlTypeLoader

protected JmlTypeLoader(JmlFileFinder finder)
Creates an instance with the given file finder. This constructor is for use by subclass.

Method Detail

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

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.