JML

org.multijava.mjc
Class CTopLevel

java.lang.Object
  extended byorg.multijava.util.Utils
      extended byorg.multijava.mjc.CTopLevel
All Implemented Interfaces:
Cloneable, Constants, Constants

public final class CTopLevel
extends Utils
implements Constants

This class is a facade for an instance of TypeLoader (or a subclass). It acts like a "class loader"; it keeps track of which classes and external generic functions referenced in a compilation session are being generated from source and which are being read from disk as class files. It also handles the loading of such classes and external generic functions from disk. in general all cached operations on types and type signatures are directed through this facade.


Field Summary
private static Main compiler
           
private static Main FROMCLASSES
           
private static Map gfCollSingletonMap
          Maps from qualified names to CGenericFunctionCollection singletons.
static int IS_GEN_FUNC
          A constant return value for whichIsThis(String,java.io.File).
static int IS_NEITHER
          A constant return value for whichIsThis(String,java.io.File).
static int IS_TYPE
          A constant return value for whichIsThis(String,java.io.File).
private static HashSet pendingGFs
           
private static TypeLoader typeLoader
           
 
Fields inherited from class org.multijava.util.Utils
DBG_LEVEL_HIGH, DBG_LEVEL_LOW, DBG_LEVEL_NO
 
Fields inherited from interface org.multijava.mjc.Constants
ACC_MODIFIER_FLAGS_MASK, ACC_NON_NULL, ACC_NON_NULL_BY_DEFAULT, ACC_NULLABLE, ACC_NULLABLE_BY_DEFAULT, ACC_PURE, ACCESS_FLAG_ARRAY, ACCESS_FLAG_NAMES, AMID_JAVA_MATH, AMID_MAX, AMID_SAFE_MATH, CMP_VERSION, IMPLICITLY_NON_NULL, JAV_ASSERTION_ERROR, JAV_CLASS, JAV_CLASSLOADER, JAV_CLASSNOTFOUND_EXCEPTION, JAV_CLONE, JAV_CLONEABLE, JAV_CONSTRUCTOR, JAV_ERROR, JAV_EXCEPTION, JAV_INIT, JAV_LENGTH, JAV_NAME_SEPARATOR, JAV_NOCLASSDEFFOUND_ERROR, JAV_OBJECT, JAV_OUTER_THIS, JAV_RMJ_RUNTIME_EXCEPTION, JAV_RUNTIME, JAV_RUNTIME_EXCEPTION, JAV_SERIALIZABLE, JAV_STATIC_INIT, JAV_STRING, JAV_STRINGBUFFER, JAV_SUPER, JAV_THIS, JAV_THROWABLE, MJ_ANCHOR, NULLITY_MODS, OPE_BAND, OPE_BNOT, OPE_BOR, OPE_BSR, OPE_BXOR, OPE_EQ, OPE_GE, OPE_GT, OPE_LAND, OPE_LE, OPE_LNOT, OPE_LOR, OPE_LT, OPE_MINUS, OPE_NE, OPE_PERCENT, OPE_PLUS, OPE_POSTDEC, OPE_POSTINC, OPE_PREDEC, OPE_PREINC, OPE_SIMPLE, OPE_SL, OPE_SLASH, OPE_SR, OPE_STAR, TID_ARRAY, TID_BOOLEAN, TID_BYTE, TID_CHAR, TID_CLASS, TID_DOUBLE, TID_FLOAT, TID_INT, TID_LONG, TID_MAX, TID_SHORT, TID_VOID, UNIV_ARRAY_TMP, UNIV_TMP
 
Fields inherited from interface org.multijava.util.classfile.Constants
ACC_ABSTRACT, ACC_FINAL, ACC_INTERFACE, ACC_NATIVE, ACC_PRIVATE, ACC_PROTECTED, ACC_PUBLIC, ACC_STATIC, ACC_STRICT, ACC_SUPER, ACC_SYNCHRONIZED, ACC_SYNTHETIC, ACC_TRANSIENT, ACC_VOLATILE, ATT_ANCHOR, ATT_BRIDGE, ATT_CODE, ATT_CONSTANTVALUE, ATT_DEPRECATED, ATT_DISPATCHER, ATT_EXCEPTIONS, ATT_GENERIC, ATT_GENERIC_FUNCTIONS, ATT_INNERCLASSES, ATT_LINENUMBERTABLE, ATT_LOCALVARIABLETABLE, ATT_MM_BODY, ATT_REDIRECTOR, ATT_RMJ_GLUE, ATT_RMJ_SIGNATURE, ATT_RUNTIME_VISIBLE_ANNOTATIONS, ATT_RUNTIME_VISIBLE_PARAMETER_ANNOTATIONS, ATT_SIGNATURE, ATT_SOURCEFILE, ATT_SYNTHETIC, ATT_UNIVERSE_FIELD, ATT_UNIVERSE_METHOD, ATT_UNIVERSE_VERSION, CST_CLASS, CST_DOUBLE, CST_FIELD, CST_FLOAT, CST_INTEGER, CST_INTERFACEMETHOD, CST_LONG, CST_METHOD, CST_NAMEANDTYPE, CST_STRING, CST_UTF8, ENV_DEBUG_MODE, ENV_USE_CACHE, JAVA_MAGIC, JAVA_MAJOR, JAVA_MINOR, MAX_CODE_PER_METHOD, opc_aaload, opc_aastore, opc_aconst_null, opc_aload, opc_aload_0, opc_aload_1, opc_aload_2, opc_aload_3, opc_anewarray, opc_areturn, opc_arraylength, opc_astore, opc_astore_0, opc_astore_1, opc_astore_2, opc_astore_3, opc_athrow, opc_baload, opc_bastore, opc_bipush, opc_caload, opc_castore, opc_checkcast, opc_d2f, opc_d2i, opc_d2l, opc_dadd, opc_daload, opc_dastore, opc_dcmpg, opc_dcmpl, opc_dconst_0, opc_dconst_1, opc_ddiv, opc_dload, opc_dload_0, opc_dload_1, opc_dload_2, opc_dload_3, opc_dmul, opc_dneg, opc_drem, opc_dreturn, opc_dstore, opc_dstore_0, opc_dstore_1, opc_dstore_2, opc_dstore_3, opc_dsub, opc_dup, opc_dup2, opc_dup2_x1, opc_dup2_x2, opc_dup_x1, opc_dup_x2, opc_f2d, opc_f2i, opc_f2l, opc_fadd, opc_faload, opc_fastore, opc_fcmpg, opc_fcmpl, opc_fconst_0, opc_fconst_1, opc_fconst_2, opc_fdiv, opc_fload, opc_fload_0, opc_fload_1, opc_fload_2, opc_fload_3, opc_fmul, opc_fneg, opc_frem, opc_freturn, opc_fstore, opc_fstore_0, opc_fstore_1, opc_fstore_2, opc_fstore_3, opc_fsub, opc_getfield, opc_getstatic, opc_goto, opc_goto_w, opc_i2b, opc_i2c, opc_i2d, opc_i2f, opc_i2l, opc_i2s, opc_iadd, opc_iaload, opc_iand, opc_iastore, opc_iconst_0, opc_iconst_1, opc_iconst_2, opc_iconst_3, opc_iconst_4, opc_iconst_5, opc_iconst_m1, opc_idiv, opc_if_acmpeq, opc_if_acmpne, opc_if_icmpeq, opc_if_icmpge, opc_if_icmpgt, opc_if_icmple, opc_if_icmplt, opc_if_icmpne, opc_ifeq, opc_ifge, opc_ifgt, opc_ifle, opc_iflt, opc_ifne, opc_ifnonnull, opc_ifnull, opc_iinc, opc_iload, opc_iload_0, opc_iload_1, opc_iload_2, opc_iload_3, opc_imul, opc_ineg, opc_instanceof, opc_invokeinterface, opc_invokespecial, opc_invokestatic, opc_invokevirtual, opc_ior, opc_irem, opc_ireturn, opc_ishl, opc_ishr, opc_istore, opc_istore_0, opc_istore_1, opc_istore_2, opc_istore_3, opc_isub, opc_iushr, opc_ixor, opc_jsr, opc_jsr_w, opc_l2d, opc_l2f, opc_l2i, opc_ladd, opc_laload, opc_land, opc_lastore, opc_lcmp, opc_lconst_0, opc_lconst_1, opc_ldc, opc_ldc2_w, opc_ldc_w, opc_ldiv, opc_lload, opc_lload_0, opc_lload_1, opc_lload_2, opc_lload_3, opc_lmul, opc_lneg, opc_lookupswitch, opc_lor, opc_lrem, opc_lreturn, opc_lshl, opc_lshr, opc_lstore, opc_lstore_0, opc_lstore_1, opc_lstore_2, opc_lstore_3, opc_lsub, opc_lushr, opc_lxor, opc_monitorenter, opc_monitorexit, opc_multianewarray, opc_new, opc_newarray, opc_nop, opc_pop, opc_pop2, opc_putfield, opc_putstatic, opc_ret, opc_return, opc_saload, opc_sastore, opc_sipush, opc_swap, opc_tableswitch, opc_wide, opc_xxxunusedxxx, POO_ASCII_CONSTANT, POO_CLASS_CONSTANT, POO_DOUBLE_CONSTANT, POO_FLOAT_CONSTANT, POO_INTEGER_CONSTANT, POO_LONG_CONSTANT, POO_NAT_CONSTANT, POO_REF_CONSTANT, POO_STRING_CONSTANT, TYP_ADDRESS, TYP_DOUBLE, TYP_FLOAT, TYP_INT, TYP_LONG, TYP_REFERENCE, TYP_VOID
 
Constructor Summary
CTopLevel()
           
 
Method Summary
static boolean addClass(CClass clazz)
          Adds the given class to the table of available classes.
static boolean addGFCollection(CGenericFunctionCollection coll)
          Adds the given generic function collection singleton to the map.
static void addTypeRep(String qName, CClassType typeRep)
          Adds the given type representation, which must represent a fully qualified type name, to the cache.
static boolean classExists(String qName)
          Checks whether a class with the given name is available in the class path.
static FileFinder fileFinder()
          Returns the FileFinder instance that is used by the current session when searching for classes and generic functions.
static File findSourceFile(String name)
           
static 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 Main getCompiler()
          Returns the top level compiler.
static Main getFromClassesCompiler()
           
static CClassType getTypeRep(String name, boolean isFullyQualified)
          return the lightweight type representation of the class with the given name, generating a new one if necessary.
static CClassType getTypeRep(String name, CClassType[][] arguments, boolean isFullyQualified)
          Returns the lightweight type representation of the class with the given name, generating a new one if necessary.
static CClassType getTypeRep(String name, CUniverse univ, boolean isFullyQualified)
          getTypeRep with a universe parameter and no arguments.
static CClassType getTypeRep(String name, CUniverse univ, CClassType[][] arguments, boolean isFullyQualified)
          getTypeRep with a universe parameter and arguments.
(package private) static void initSession(Main compiler, TypeLoader loader)
          Removes all non-trusted, cached information from this compilation sessions so that new declarations can be processed.
static boolean isClassLoaded(String qName)
          Returns true if the class with the given fully-qualified name has already been read and loaded.
static boolean isDeclaredInDifferentSourceFiles(boolean isUnique, CClass clazz)
          Determines whether the given Class, using its fully qualified name, has been declared in more one file.
static boolean isGFLoaded(String qName)
          Returns true if the generic function with the given fully-qualified name has already been read and loaded.
static CClass loadClass(String qName)
          Loads type definition; uses the FileFinder supplied in initSession to determine which file is loaded for the given name.
static CGenericFunctionCollection lookupGFCollection(String qualifiedIdent)
          Finds the generic function collection singleton for the given fully qualified name.
static CClassType lookupTypeRep(String qName)
           
static void registerPendingGFCollection(String qName)
          Registers that the external generic function with the given fully qualified name has been parsed and, barring an error during the preprocessDependencies pass, will be available to other compilation units.
static CClass reloadClass(CClass clazz)
          Reloads the specified class if this class has been defined during a previous compilation session.
static int whichIsThis(String qName, File f)
          Checks whether the source code contain in the given file declares a type or an external generic function of the given name.
 
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

IS_TYPE

public static final int IS_TYPE
A constant return value for whichIsThis(String,java.io.File).


IS_GEN_FUNC

public static final int IS_GEN_FUNC
A constant return value for whichIsThis(String,java.io.File).


IS_NEITHER

public static final int IS_NEITHER
A constant return value for whichIsThis(String,java.io.File).


compiler

private static Main compiler

FROMCLASSES

private static final Main FROMCLASSES

gfCollSingletonMap

private static Map gfCollSingletonMap
Maps from qualified names to CGenericFunctionCollection singletons.


pendingGFs

private static HashSet pendingGFs

typeLoader

private static TypeLoader typeLoader
Constructor Detail

CTopLevel

public CTopLevel()
Method Detail

getTypeRep

public static CClassType getTypeRep(String name,
                                    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)

getTypeRep

public static CClassType getTypeRep(String name,
                                    boolean isFullyQualified)
return the lightweight type representation of the class with the given name, generating a new one if necessary.


getTypeRep

public static CClassType getTypeRep(String name,
                                    CUniverse univ,
                                    boolean isFullyQualified)
getTypeRep with a universe parameter and no arguments. By WMD.


getTypeRep

public static CClassType getTypeRep(String name,
                                    CUniverse univ,
                                    CClassType[][] arguments,
                                    boolean isFullyQualified)
getTypeRep with a universe parameter and arguments. We get a cached version of the class and then clone it and set the correct universe modifier. The clone is "shallow" and most of the data can be shared between different universes. By WMD.


addTypeRep

public static 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 '.' *);
 


loadClass

public static CClass loadClass(String qName)
Loads type definition; uses the FileFinder supplied in initSession to determine which file is loaded for the given name. Returns CClass.CLS_UNDEFINED or null if the type could not be loaded.

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

Parameters:
qName - the fully qualified name of the type to load.

isDeclaredInDifferentSourceFiles

public static boolean isDeclaredInDifferentSourceFiles(boolean isUnique,
                                                       CClass clazz)
Determines whether the given Class, using its fully qualified name, has been declared in more 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.

  requires clazz != null; 
 


reloadClass

public static CClass reloadClass(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.


isClassLoaded

public static boolean isClassLoaded(String qName)
Returns true if the class with the given fully-qualified name has already been read and loaded.

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

Parameters:
qName - the fully qualified name of the type to load.

addClass

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

requires clazz != null;
modifies typeLoader;
 


classExists

public static 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

registerPendingGFCollection

public static void registerPendingGFCollection(String qName)
Registers that the external generic function with the given fully qualified name has been parsed and, barring an error during the preprocessDependencies pass, will be available to other compilation units.

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

See Also:
MJTopLevelMethodDeclaration.registerPendingGFCollection(String)

addGFCollection

public static boolean addGFCollection(CGenericFunctionCollection coll)
Adds the given generic function collection singleton to the map.

Returns:
true if this collection is OK, i.e., is not a redeclaration.

lookupGFCollection

public static CGenericFunctionCollection lookupGFCollection(String qualifiedIdent)
Finds the generic function collection singleton for the given fully qualified name. If no singleton exists then tries to read the collection from disk (either from binary or source). If no disk file is found then returns CGenericFunctionCollection.GF_UNDEFINED.

Parameters:
qualifiedIdent - the fully qualified name of the collection
Returns:
the singleton representing the collection, or CGenericFunctionCollection.GF_UNDEFINED if one cannot be found

lookupTypeRep

public static CClassType lookupTypeRep(String qName)

isGFLoaded

public static boolean isGFLoaded(String qName)
Returns true if the generic function with the given fully-qualified name has already been read and loaded.

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


whichIsThis

public static int whichIsThis(String qName,
                              File f)
Checks whether the source code contain in the given file declares a type or an external generic function of the given name.

Parameters:
qName - the fully qualified name of the class or generic function expected in f
f - the source code file to check
Returns:
IS_TYPE if the code in f declares a type named qName, IS_GEN_FUNC if the code in f declares an external generic function named qName, and IS_NEITHER otherwise.

initSession

static void initSession(Main compiler,
                        TypeLoader loader)
Removes all non-trusted, cached information from this compilation sessions so that new declarations can be processed. This is package protected so that tools inheriting from mjc.Main must use the Main.initSession(TypeLoader) method for session initialization.

requires loader != null;
modifies CTopLevel.compiler;
modifies typeLoader;
modifies gfCollSingletonMap, pendingGFs;
ensures CTopLevel.compiler == compiler &&
CTopLevel.typeLoader == loader;
 


getCompiler

public static Main getCompiler()
Returns the top level compiler. Result may be null if called after initSession() is invoked with a null first argument.


getFromClassesCompiler

public static Main getFromClassesCompiler()

fileFinder

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


findSourceFile

public static File findSourceFile(String name)

forgetEverythingAbout

public static 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.


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.