public final class JavaInfo
extends java.lang.Object
KeYProgModelInfo
. This class can be extended to provide further
services.Modifier and Type | Class and Description |
---|---|
(package private) static class |
JavaInfo.Filter
inner class used to filter certain types of program elements
|
Modifier and Type | Field and Description |
---|---|
private LRUCache<Pair<KeYJavaType,KeYJavaType>,ImmutableList<KeYJavaType>> |
commonSubtypeCache |
protected KeYJavaType[] |
commonTypes
as accessed very often caches:
KeYJavaType of
java.lang.Object, java.lang.Clonable, java.io.Serializable
in in this order
|
protected boolean |
commonTypesCacheValid |
protected static java.lang.String |
DEFAULT_EXECUTION_CONTEXT_CLASS
the name of the class used as default execution context
|
protected static java.lang.String |
DEFAULT_EXECUTION_CONTEXT_METHOD |
protected ExecutionContext |
defaultExecutionContext
The default execution context is for the case of program statements on
the top level.
|
private ObserverFunction |
inv
caches the observer for
<inv> |
private ProgramVariable |
invProgVar
caches the program variable for
<inv> |
private KeYProgModelInfo |
kpmi |
private ProgramVariable |
length
caches the arrays' length attribute
|
private java.util.HashMap<java.lang.String,KeYJavaType> |
name2KJTCache |
private int |
nameCachedSize |
private KeYJavaType |
nullType
the type of null
|
protected Services |
services |
private java.util.HashMap<Sort,java.util.List<KeYJavaType>> |
sort2KJTCache |
private int |
sortCachedSize |
private java.util.HashMap<KeYJavaType,ObserverFunction> |
staticInvs |
private java.util.HashMap<Type,KeYJavaType> |
type2KJTCache |
Modifier | Constructor and Description |
---|---|
protected |
JavaInfo(JavaInfo proto,
Services s) |
protected |
JavaInfo(KeYProgModelInfo kpmi,
Services s)
creates a new JavaInfo object by giving a KeYProgModelInfo to access
the Recoder SourceInfo and using the given
Services object. |
Modifier and Type | Method and Description |
---|---|
private void |
buildNameCache()
caches all known types using their qualified name as retrieval key
|
Sort |
cloneableSort()
returns the KeYJavaType for class java.lang.Cloneable
|
JavaInfo |
copy(Services serv)
copies this JavaInfo and uses the given Services object as the
Services object of the copied JavaInfo
|
ImmutableList<KeYJavaType> |
createSignature(ImmutableArray<? extends Expression> arguments)
retrieves the signature according to the given expressions
|
TypeReference |
createTypeReference(KeYJavaType kjt)
creates a new TypeReference for the given KeYJavaType
|
protected void |
fillCommonTypesCache() |
private ImmutableList<Field> |
filterLocalDeclaredFields(TypeDeclaration classDecl,
JavaInfo.Filter filter)
retrieves all attributes locally declared in class cl
(inclusive the implicit attributes) satisfying the given filter
The returned list is in source code order.
|
private ProgramVariable |
find(java.lang.String programName,
ImmutableList<Field> fields)
retrieves a field with the given name out of the list
|
private IProgramMethod |
findToplevelPM(KeYJavaType kjt,
java.lang.String methodName,
ImmutableList<KeYJavaType> sig,
KeYJavaType context) |
ImmutableList<ProgramVariable> |
getAllAttributes(java.lang.String programName,
KeYJavaType type) |
ImmutableList<ProgramVariable> |
getAllAttributes(java.lang.String programName,
KeYJavaType type,
boolean traverseSubtypes)
returns a list of all attributes with the given program name
declared in one of type's sub- or supertype including
its own attributes
Attention:
The type must not denote the null type
|
ImmutableList<Field> |
getAllFields(TypeDeclaration classDecl)
retrieves all attributes locally declared in class cl
(inclusive the implicit attributes)
The returned list is in source code order.
|
java.util.Set<KeYJavaType> |
getAllKeYJavaTypes()
returns all known KeYJavaTypes of the current
program type model
|
ImmutableList<Method> |
getAllMethods(KeYJavaType kjt)
returns all methods from the given Type
|
ImmutableList<IProgramMethod> |
getAllProgramMethods(KeYJavaType kjt)
returns all methods from the given Type as IProgramMethods
|
ImmutableList<ProgramMethod> |
getAllProgramMethodsLocallyDeclared(KeYJavaType kjt)
returns all methods declared in the given Type as IProgramMethods
|
ImmutableList<KeYJavaType> |
getAllSubtypes(KeYJavaType type)
returns all proper subtypes of a given type
|
ImmutableList<KeYJavaType> |
getAllSupertypes(KeYJavaType type)
returns all supertypes of a given type
|
ProgramVariable |
getArrayLength()
returns the length attribute for arrays
|
ProgramVariable |
getAttribute(java.lang.String fullyQualifiedName)
returns the programvariable for the specified attribute.
|
ProgramVariable |
getAttribute(java.lang.String name,
KeYJavaType classType)
returns the program variable representing the attribute of the given
name declared locally in class classType
|
ProgramVariable |
getAttribute(java.lang.String attributeName,
Sort s)
returns an attribute named attributeName declared locally
in object type s
|
ProgramVariable |
getAttribute(java.lang.String programName,
java.lang.String qualifiedClassName)
returns the programvariable for the specified attribute declared in
the specified class
|
ProgramVariable |
getCanonicalFieldProgramVariable(java.lang.String fieldName,
KeYJavaType kjt) |
ImmutableList<KeYJavaType> |
getCommonSubtypes(KeYJavaType k1,
KeYJavaType k2)
returns the list of all common subtypes of types k1 and k2
(inclusive one of them if they are equal or subtypes themselves)
attention: Null is not a jav atype only a logic sort, i.e.
|
IProgramMethod |
getConstructor(KeYJavaType kjt,
ImmutableList<KeYJavaType> signature) |
ImmutableList<IProgramMethod> |
getConstructors(KeYJavaType kjt) |
ExecutionContext |
getDefaultExecutionContext()
returns the default execution context.
|
ImmutableList<KeYJavaType> |
getDirectSuperTypes(KeYJavaType type)
returns all direct supertypes (local declared types in extends and
implements) if extends is not given explict java.lang.Object is added
(it is not added for interfaces)
|
private ImmutableList<Field> |
getFields(FieldDeclaration field)
extracts all fields out of fielddeclaration
|
private ImmutableList<Field> |
getFields(ImmutableArray<MemberDeclaration> list)
extracts all field specifications out of the given
list.
|
java.lang.String |
getFullName(KeYJavaType t)
returns the full name of a given
KeYJavaType . |
ImmutableList<Field> |
getImplicitFields(ClassDeclaration cl)
retrieves all implicit attributes locally declared in the given class
The returned list is in source code order.
|
IObserverFunction |
getInv()
Returns the special symbol
<inv> which stands for the class invariant of an object. |
ProgramVariable |
getInvProgramVar()
Returns the special program variable symbol
<inv>
which stands for the class invariant of an object. |
KeYJavaType |
getJavaIoSerializable()
returns the KeYJavaType for class java.io.Serializable
|
KeYJavaType |
getJavaLangCloneable()
returns the KeYJavaType for class java.lang.Clonable
|
KeYJavaType |
getJavaLangObject()
returns the KeYJavaType for class java.lang.Object
|
KeYJavaType |
getKeYJavaType(Sort sort)
returns a KeYJavaType having the given sort
|
KeYJavaType |
getKeYJavaType(java.lang.String fullName)
returns a KeYJavaType (either primitive of object type) having the
full name of the given String fullName
|
KeYJavaType |
getKeYJavaType(Type t)
returns the KeYJavaType belonging to the given Type t
|
private ImmutableList<KeYJavaType> |
getKeYJavaTypes(ImmutableArray<? extends Expression> args)
gets an array of expression and returns a list of types
|
KeYProgModelInfo |
getKeYProgModelInfo()
returns the underlying KeYProgModelInfo providing access to the
Recoder structures.
|
ImmutableList<Method> |
getMethods(KeYJavaType kjt)
returns all locally declared methods from the given Type
|
KeYJavaType |
getNullType()
returns the KeYJavaType representing the type of 'null'
|
KeYJavaType |
getPrimitiveKeYJavaType(PrimitiveType type) |
KeYJavaType |
getPrimitiveKeYJavaType(java.lang.String typename)
returns a primitive KeYJavaType matching the given typename.
|
IProgramMethod |
getProgramMethod(KeYJavaType classType,
java.lang.String methodName,
ImmutableArray<? extends Type> signature,
KeYJavaType context) |
IProgramMethod |
getProgramMethod(KeYJavaType classType,
java.lang.String methodName,
ImmutableList<? extends Type> signature,
KeYJavaType context)
returns the program methods defined in the given KeYJavaType with name
m and the list of types as signature of the method
|
IProgramMethod |
getProgramMethod(KeYJavaType classType,
java.lang.String methodName,
java.util.List<java.util.List<KeYJavaType>> signature,
KeYJavaType context) |
IProgramMethod |
getProgramMethod(KeYJavaType classType,
java.lang.String methodName,
ProgramVariable[] args,
KeYJavaType context)
returns the program method defined in the KeYJavaType of the program
variable clv, with the name m, and the KeYJavaTypes of the given array
of program variables as signatures.
|
private IProgramMethod |
getProgramMethodFromPartialSignature(KeYJavaType classType,
java.lang.String methodName,
java.util.List<java.util.List<KeYJavaType>> signature,
ImmutableList<KeYJavaType> partialSignature,
KeYJavaType context) |
Term |
getProgramMethodTerm(Term prefix,
java.lang.String methodName,
Term[] args,
java.lang.String className,
boolean traverseHierarchy) |
Services |
getServices()
returns the services associated with this JavaInfo
|
IObserverFunction |
getStaticInv(KeYJavaType target)
Returns the special symbol
<staticInv> which stands for the static invariant of a type. |
Term |
getStaticProgramMethodTerm(java.lang.String methodName,
Term[] args,
java.lang.String className) |
KeYJavaType |
getSuperclass(KeYJavaType type)
retrieves the direct extended superclass for the given class
|
private ImmutableList<Sort> |
getSuperSorts(Sort sort) |
private Term |
getTermFromProgramMethod(IProgramMethod pm,
java.lang.String methodName,
java.lang.String className,
Term[] args,
Term prefix) |
IProgramMethod |
getToplevelPM(KeYJavaType kjt,
IProgramMethod pm) |
IProgramMethod |
getToplevelPM(KeYJavaType kjt,
java.lang.String methodName,
ImmutableList<KeYJavaType> sig) |
KeYJavaType |
getTypeByClassName(java.lang.String className)
looks up a KeYJavaType with given name.
|
KeYJavaType |
getTypeByClassName(java.lang.String name,
KeYJavaType containerType)
retrieves the KeYJavaType of the given type name.
|
KeYJavaType |
getTypeByName(java.lang.String fullName)
looks up the fully qualifying name given by a String
in the list of all available
KeYJavaTypes in the Java model
|
private TypeConverter |
getTypeConverter()
Don't make this method public, use
Services
instead
returns the TypeConverter to translate program parts to their
logic equivalent |
TypeDeclaration |
getTypeDeclaration(java.lang.String fullName)
returns a type declaration with the full name of the given String fullName
|
boolean |
isAJavaCommonSort(Sort sort)
tests if sort represents java.lang.Object, java.lang.Cloneable or
java.io.Serializable
|
boolean |
isCanonicalProgramMethod(IProgramMethod method,
KeYJavaType context)
This is used for pretty printing observer terms.
|
boolean |
isFinal(KeYJavaType kjt)
Checks whether the type is declared as final.
|
boolean |
isInterface(KeYJavaType t) |
boolean |
isPackage(java.lang.String name)
checks if name refers to a package
|
static boolean |
isPrivate(KeYJavaType kjt) |
boolean |
isSubtype(KeYJavaType subType,
KeYJavaType superType)
returns true iff the given subType KeYJavaType is a sub type of the
given KeYJavaType superType.
|
static boolean |
isVisibleTo(SpecificationElement ax,
KeYJavaType visibleTo) |
java.util.List<KeYJavaType> |
lookupSort2KJTCache(Sort sort) |
ProgramVariable |
lookupVisibleAttribute(java.lang.String programName,
KeYJavaType classType)
looks up for a field of the given program name
visible in the specified class type belonging to the type
or one of its supertypes
|
Sort |
nullSort() |
Sort |
objectSort()
returns the KeYJavaType for class java.lang.Object
|
ProgramElement |
readJava(java.lang.String java)
reads a Java statement not necessarily a block
|
JavaBlock |
readJavaBlock(java.lang.String java)
reads a Java block given as a String
|
JavaBlock |
readJavaBlock(java.lang.String java,
TypeDeclaration asIn)
reads a Java block given as a string java as it was in the given
TypeDeclaration asIn.
|
KeYRecoderMapping |
rec2key()
convenience method that returns the Recoder-to-KeY mapping underlying
the KeYProgModelInfo of this JavaInfo
|
void |
resetCaches() |
Sort |
serializableSort()
returns the KeYJavaType for class java.io.Serializable
|
(package private) void |
setKeYProgModelInfo(KeYProgModelInfo kpmi) |
private java.util.List<java.util.List<KeYJavaType>> |
termArrayToSignature(Term[] args) |
private java.lang.String |
translateArrayType(java.lang.String s)
Translates things like int[] into [I, etc.
|
private void |
updateSort2KJTCache() |
protected Services services
private KeYProgModelInfo kpmi
private KeYJavaType nullType
protected KeYJavaType[] commonTypes
private java.util.HashMap<Sort,java.util.List<KeYJavaType>> sort2KJTCache
private java.util.HashMap<Type,KeYJavaType> type2KJTCache
private java.util.HashMap<java.lang.String,KeYJavaType> name2KJTCache
private LRUCache<Pair<KeYJavaType,KeYJavaType>,ImmutableList<KeYJavaType>> commonSubtypeCache
private int nameCachedSize
private int sortCachedSize
protected ExecutionContext defaultExecutionContext
MethodBodyStatement
or a
MethodFrame
, which contains a
valid execution context.protected boolean commonTypesCacheValid
private ProgramVariable length
private ProgramVariable invProgVar
<inv>
private ObserverFunction inv
<inv>
protected static final java.lang.String DEFAULT_EXECUTION_CONTEXT_CLASS
protected static final java.lang.String DEFAULT_EXECUTION_CONTEXT_METHOD
private java.util.HashMap<KeYJavaType,ObserverFunction> staticInvs
protected JavaInfo(KeYProgModelInfo kpmi, Services s)
Services
object.public KeYProgModelInfo getKeYProgModelInfo()
void setKeYProgModelInfo(KeYProgModelInfo kpmi)
public KeYRecoderMapping rec2key()
public JavaInfo copy(Services serv)
serv
- the Services the copy will use and vice versaprivate TypeConverter getTypeConverter()
Services
instead
returns the TypeConverter to translate program parts to their
logic equivalentpublic Services getServices()
public java.lang.String getFullName(KeYJavaType t)
KeYJavaType
.t
- the KeYJavaType including the package prefixpublic TypeReference createTypeReference(KeYJavaType kjt)
public void resetCaches()
public KeYJavaType getTypeByName(java.lang.String fullName)
fullName
- the Stringprivate void buildNameCache()
public boolean isPackage(java.lang.String name)
name
- a String with the name to be checkedprivate java.lang.String translateArrayType(java.lang.String s)
public KeYJavaType getTypeByClassName(java.lang.String className)
cjava.lang
className
- the fully qualified class name (or an unqualified name from package java.lang)public TypeDeclaration getTypeDeclaration(java.lang.String fullName)
public java.util.Set<KeYJavaType> getAllKeYJavaTypes()
public KeYJavaType getPrimitiveKeYJavaType(PrimitiveType type)
public KeYJavaType getPrimitiveKeYJavaType(java.lang.String typename)
public KeYJavaType getKeYJavaType(java.lang.String fullName)
fullName
- a String with the type name to lookuppublic boolean isSubtype(KeYJavaType subType, KeYJavaType superType)
public boolean isInterface(KeYJavaType t)
public boolean isFinal(KeYJavaType kjt)
kjt
- public static boolean isPrivate(KeYJavaType kjt)
public static boolean isVisibleTo(SpecificationElement ax, KeYJavaType visibleTo)
public KeYJavaType getKeYJavaType(Sort sort)
private void updateSort2KJTCache()
public java.util.List<KeYJavaType> lookupSort2KJTCache(Sort sort)
public KeYJavaType getKeYJavaType(Type t)
public ImmutableList<Method> getAllMethods(KeYJavaType kjt)
public ImmutableList<Method> getMethods(KeYJavaType kjt)
public ImmutableList<IProgramMethod> getAllProgramMethods(KeYJavaType kjt)
public ImmutableList<ProgramMethod> getAllProgramMethodsLocallyDeclared(KeYJavaType kjt)
public ImmutableList<IProgramMethod> getConstructors(KeYJavaType kjt)
public IProgramMethod getConstructor(KeYJavaType kjt, ImmutableList<KeYJavaType> signature)
public IProgramMethod getProgramMethod(KeYJavaType classType, java.lang.String methodName, ImmutableList<? extends Type> signature, KeYJavaType context)
classType
- the KeYJavaType of the class where to look for the
methodmethodName
- the name of the methodsignature
- a IListcontext
- the KeYJavaType of the class context from where
the method is calledpublic IProgramMethod getProgramMethod(KeYJavaType classType, java.lang.String methodName, ImmutableArray<? extends Type> signature, KeYJavaType context)
private IProgramMethod getProgramMethodFromPartialSignature(KeYJavaType classType, java.lang.String methodName, java.util.List<java.util.List<KeYJavaType>> signature, ImmutableList<KeYJavaType> partialSignature, KeYJavaType context)
public IProgramMethod getProgramMethod(KeYJavaType classType, java.lang.String methodName, java.util.List<java.util.List<KeYJavaType>> signature, KeYJavaType context)
public IProgramMethod getProgramMethod(KeYJavaType classType, java.lang.String methodName, ProgramVariable[] args, KeYJavaType context)
classType
- the KeYJavaType of the class where to look for the
methodmethodName
- the name of the methodargs
- an array of ProgramVariables as the arguments of the
methodcontext
- the KeYJavaType of the class context from where
the method is calledpublic IProgramMethod getToplevelPM(KeYJavaType kjt, java.lang.String methodName, ImmutableList<KeYJavaType> sig)
private IProgramMethod findToplevelPM(KeYJavaType kjt, java.lang.String methodName, ImmutableList<KeYJavaType> sig, KeYJavaType context)
public IProgramMethod getToplevelPM(KeYJavaType kjt, IProgramMethod pm)
private java.util.List<java.util.List<KeYJavaType>> termArrayToSignature(Term[] args)
public Term getStaticProgramMethodTerm(java.lang.String methodName, Term[] args, java.lang.String className)
public Term getProgramMethodTerm(Term prefix, java.lang.String methodName, Term[] args, java.lang.String className, boolean traverseHierarchy)
private Term getTermFromProgramMethod(IProgramMethod pm, java.lang.String methodName, java.lang.String className, Term[] args, Term prefix) throws java.lang.IllegalArgumentException
java.lang.IllegalArgumentException
public ImmutableList<KeYJavaType> getDirectSuperTypes(KeYJavaType type)
public KeYJavaType getSuperclass(KeYJavaType type)
type
- the KeYJavaType of the type whose superclass
has to be determinedprivate ImmutableList<KeYJavaType> getKeYJavaTypes(ImmutableArray<? extends Expression> args)
public ImmutableList<KeYJavaType> createSignature(ImmutableArray<? extends Expression> arguments)
arguments
- ArrayOfpublic ImmutableList<Field> getAllFields(TypeDeclaration classDecl)
classDecl
- the ClassDeclaration whose attributes shall be collectedpublic ImmutableList<Field> getImplicitFields(ClassDeclaration cl)
cl
- the ClassDeclaration where to look for the implicit
attributesprivate ImmutableList<Field> filterLocalDeclaredFields(TypeDeclaration classDecl, JavaInfo.Filter filter)
classDecl
- the ClassDeclaration whose attributes shall be collectedfilter
- the Filter to be satisifed by the attributes to
be returnedpublic JavaBlock readJavaBlock(java.lang.String java, TypeDeclaration asIn)
public JavaBlock readJavaBlock(java.lang.String java)
public ProgramElement readJava(java.lang.String java)
private final ProgramVariable find(java.lang.String programName, ImmutableList<Field> fields)
programName
- a String with the name of the field to be looked forfields
- the IListprivate final ImmutableList<Field> getFields(FieldDeclaration field)
field
- the FieldDeclaration of which the field
specifications have to be extractedprivate ImmutableList<Field> getFields(ImmutableArray<MemberDeclaration> list)
list
- the ArrayOfpublic ProgramVariable getAttribute(java.lang.String fullyQualifiedName)
fullyQualifiedName
- the String with the fully qualified attribute
namejava.lang.IllegalArgumentException
- if the given name is not fully
qualifiedpublic ProgramVariable getAttribute(java.lang.String programName, java.lang.String qualifiedClassName)
programName
- the String with the name of the attributequalifiedClassName
- the String with the full (inclusive package) qualified
class namejava.lang.IllegalArgumentException
- if the qualified class name is empty or
nullUnknownJavaTypeException
- if the qualified name refers to an unknown typepublic ProgramVariable getAttribute(java.lang.String name, KeYJavaType classType)
public ProgramVariable getAttribute(java.lang.String attributeName, Sort s)
public ProgramVariable getCanonicalFieldProgramVariable(java.lang.String fieldName, KeYJavaType kjt)
public ImmutableList<ProgramVariable> getAllAttributes(java.lang.String programName, KeYJavaType type)
public ImmutableList<ProgramVariable> getAllAttributes(java.lang.String programName, KeYJavaType type, boolean traverseSubtypes)
programName
- the String with name of the attribute as declared
in a programtype
- the KeYJavaType specifying the part of the hierarchy
where to look fortraverseSubtypes
- The method will visit subtypes of type
while traversing its type hierarchy iff this is set to true. Otherwise
only supertypes will be visited.protected void fillCommonTypesCache()
public KeYJavaType getJavaLangObject()
public KeYJavaType getJavaLangCloneable()
public KeYJavaType getJavaIoSerializable()
public Sort objectSort()
public Sort cloneableSort()
public Sort serializableSort()
public Sort nullSort()
public boolean isAJavaCommonSort(Sort sort)
public KeYJavaType getNullType()
public ExecutionContext getDefaultExecutionContext()
public ImmutableList<KeYJavaType> getAllSubtypes(KeYJavaType type)
type
- the KeYJavaType whose subtypes are returnedpublic ImmutableList<KeYJavaType> getAllSupertypes(KeYJavaType type)
type
- the KeYJavaType whose supertypes are returnedprivate ImmutableList<Sort> getSuperSorts(Sort sort)
public ProgramVariable lookupVisibleAttribute(java.lang.String programName, KeYJavaType classType)
programName
- the String containing the name of the
field to be looked up. The name is in short notation,
i.e. not fully qualifiedclassType
- the KeYJavaType of the class used as contextpublic ImmutableList<KeYJavaType> getCommonSubtypes(KeYJavaType k1, KeYJavaType k2)
k1
- the first KeYJavaType denoting a class typek2
- the second KeYJavaType denoting a classtypepublic ProgramVariable getArrayLength()
public IObserverFunction getInv()
<inv>
which stands for the class invariant of an object.getInvProgramVar()
public ProgramVariable getInvProgramVar()
<inv>
which stands for the class invariant of an object.getInv()
public IObserverFunction getStaticInv(KeYJavaType target)
<staticInv>
which stands for the static invariant of a type.public boolean isCanonicalProgramMethod(IProgramMethod method, KeYJavaType context) throws java.lang.NullPointerException
method
- the program method.context
- the KeYJavaType.java.lang.NullPointerException
- e.g., if the receiver of the observer happens to be
replaced by "null".public KeYJavaType getTypeByClassName(java.lang.String name, KeYJavaType containerType)
containerType
first and
then in the java.lang
package.name
- the name of the type (if possible fully qualified)containerType
- the KeYJavaType of the context in which the type should be resolvednull
if type name is unknown