public class Recoder2KeY extends java.lang.Object implements JavaReader
readCompilationUnit(String)
,
readCompilationUnitsAsFiles(String[])
or the
readBlock(String, Context)
-methods.
Results are often stored in caches.
It used to be monolithic but now uses separate classes for doing the actual
conversion and type conversion.Recoder2KeYConverter
,
Recoder2KeYTypeConverter
Modifier and Type | Field and Description |
---|---|
private java.io.File |
bootClassPath
the File object that describes the directory from which the internal
classes are to be read.
|
private java.util.List<java.io.File> |
classPath
the set of File objects that describes the classpath to be searched
for classes.
|
private Recoder2KeYConverter |
converter
the object that handles the transformation from recoder AST to KeY AST
|
private java.util.Collection<? extends CompilationUnit> |
dynamicallyCreatedCompilationUnits
the list of classnames that contain the classes that are referenced but not
defined.
|
private static int |
interactCounter
counter used to enumerate the anonymous implicit classes
|
private KeYRecoderMapping |
mapping
this mapping stores the relation between recoder and KeY entities in a
bidirectional way.
|
private boolean |
parsingLibs
this flag indicates whether we are currently parsing library classes
(special classes)
|
private KeYCrossReferenceServiceConfiguration |
servConf
Recoder's serviceConfiguration that is used throughout this process.
|
private Services |
services |
private Recoder2KeYTypeConverter |
typeConverter
the object that handles the transformation from recoder types to KeY
types
|
Modifier | Constructor and Description |
---|---|
|
Recoder2KeY(Services services,
KeYCrossReferenceServiceConfiguration servConf,
KeYRecoderMapping rec2key,
NamespaceSet nss,
TypeConverter tc)
create a new Recoder2KeY transformation object.
|
private |
Recoder2KeY(Services services,
KeYCrossReferenceServiceConfiguration servConf,
java.lang.String classPath,
KeYRecoderMapping rec2key,
NamespaceSet nss,
TypeConverter tc)
create a new Recoder2KeY transformation object.
|
|
Recoder2KeY(Services services,
NamespaceSet nss)
create a new Recoder2KeY transformation object.
|
Modifier and Type | Method and Description |
---|---|
private void |
addProgramVariablesToClassContext(ClassDeclaration classContext,
ImmutableList<ProgramVariable> vars,
CrossReferenceSourceInfo csi)
add a list of variables to a context
|
protected Context |
createContext(ImmutableList<ProgramVariable> pvs)
create a new context with a temporary name and make a list of variables
visible from within.
|
protected Context |
createContext(ImmutableList<ProgramVariable> vars,
CrossReferenceSourceInfo csi)
create a new Context with a temporary name and make a list of variables
visible from within.
|
Context |
createEmptyContext()
creates an empty RECODER compilation unit with a temporary name.
|
protected MethodDeclaration |
embedBlock(StatementBlock block)
wraps a RECODER StatementBlock in a method
it is wrapped in a method called
<virtual_method_for_parsing> . |
protected ClassDeclaration |
embedMethod(MethodDeclaration mdecl,
Context context)
wraps a RECODER MethodDeclaration in a class
|
private static int[] |
extractPositionInfo(java.lang.String errorMessage)
tries to parse recoders exception position information
|
Recoder2KeYConverter |
getConverter()
return the associated converter object
|
java.util.List<java.lang.String> |
getDynamicallyCreatedClasses()
get the list of names of classes that have been created dynamically due
to lacking definitions.
|
KeYCrossReferenceServiceConfiguration |
getServiceConfiguration() |
Recoder2KeYTypeConverter |
getTypeConverter()
return the associated type converter object
|
private void |
insertToMap(ModelElement r,
ModelElement k) |
private ClassDeclaration |
interactClassDecl()
make a new classdeclaration with a temporary name.
|
boolean |
isParsingLibs()
are we currently parsing library code (special classes)?
|
private VariableSpecification |
lookupVarSpec(ProgramVariable pv)
look up in the mapping the variable specification for a program variable.
|
protected Recoder2KeYConverter |
makeConverter(Services services,
NamespaceSet nss)
create the ast converter.
|
private TypeReference |
name2typeReference(java.lang.String typeName)
given a name as string, construct a recoder type reference from it.
|
private void |
parseInternalClasses(ProgramFactory pf,
java.util.List<CompilationUnit> rcuList)
This method loads the internal classes - also called the "boot" classes.
|
private void |
parseLibraryClasses0() |
private java.util.List<CompilationUnit> |
parseLibs()
reads compilation units that will be treated as library classes.
|
void |
parseSpecialClasses()
makes sure that the special classes (library classes) have been parsed
in.
|
JavaBlock |
readBlock(java.lang.String block,
Context context)
parses a given JavaBlock using the context to determine the right
references
|
JavaBlock |
readBlockWithEmptyContext(java.lang.String block)
parses a given JavaBlock using the context to determine the right
references using an empty context
|
JavaBlock |
readBlockWithProgramVariables(Namespace<IProgramVariable> varns,
java.lang.String s)
parses a given JavaBlock using a namespace to determine the right
references using an empty context.
|
CompilationUnit |
readCompilationUnit(java.lang.String cUnitString)
read a compilation unit, given as a string.
|
CompilationUnit[] |
readCompilationUnitsAsFiles(java.lang.String[] cUnitStrings)
parse a list of java files and transform it to the corresponding KeY
entities.
|
KeYRecoderMapping |
rec2key() |
(package private) StatementBlock |
recoderBlock(java.lang.String block,
Context context)
parses a given JavaBlock using the context to determine the right
references and returns a statement block of recoder.
|
private java.util.List<CompilationUnit> |
recoderCompilationUnits(java.lang.String[] cUnitStrings)
read a number of compilation units, each given as a string.
|
private java.util.List<CompilationUnit> |
recoderCompilationUnitsAsFiles(java.lang.String[] cUnitStrings)
parse a list of java files.
|
private void |
removeCodeFromClasses(CompilationUnit rcu,
boolean allowed) |
static void |
reportError(java.lang.String message,
java.lang.Throwable t)
report an error in form of a ConvertException.
|
void |
setClassPath(java.io.File bootClassPath,
java.util.List<java.io.File> classPath) |
private void |
setParsingLibs(boolean v)
set this to true before parsing special classes and to false afterwards.
|
protected void |
transformModel(java.util.List<CompilationUnit> cUnits)
Transform a list of compilation units.
|
private static java.lang.String |
trim(java.lang.String s)
reduce the size of a string to a maximum of 150 characters.
|
private static java.lang.String |
trim(java.lang.String s,
int length)
reduce the size of a string to a maximum of length.
|
private java.util.List<java.io.File> classPath
private java.io.File bootClassPath
private KeYRecoderMapping mapping
private KeYCrossReferenceServiceConfiguration servConf
private static int interactCounter
private boolean parsingLibs
private Recoder2KeYConverter converter
private Recoder2KeYTypeConverter typeConverter
private java.util.Collection<? extends CompilationUnit> dynamicallyCreatedCompilationUnits
private final Services services
public Recoder2KeY(Services services, KeYCrossReferenceServiceConfiguration servConf, KeYRecoderMapping rec2key, NamespaceSet nss, TypeConverter tc)
servConf
- the service configuration to be used, not nullrec2key
- the mapping to store mapped types and mapped ASTs to, not nullnss
- the namespaces to work upon, not nulltc
- the type converter, not nullpublic Recoder2KeY(Services services, NamespaceSet nss)
services
- services to retrieve objects from, not nullnss
- the namespaces to work upon, not nullprivate Recoder2KeY(Services services, KeYCrossReferenceServiceConfiguration servConf, java.lang.String classPath, KeYRecoderMapping rec2key, NamespaceSet nss, TypeConverter tc)
servConf
- the service configuration to be used, not nullclassPath
- the classpath to look up source files, ignored if nullrec2key
- the mapping to store mapped types and mapped ASTs to, not nullnss
- the namespaces to work upon, not nulltc
- the type converter, not nulljava.lang.IllegalArgumentException
- if arguments are not valid (null e.g.)protected Recoder2KeYConverter makeConverter(Services services, NamespaceSet nss)
services
- nss
- the namespaces provided to the constructorpublic Recoder2KeYConverter getConverter()
public Recoder2KeYTypeConverter getTypeConverter()
private void setParsingLibs(boolean v)
v
- the state of the special parsing flagepublic boolean isParsingLibs()
public KeYCrossReferenceServiceConfiguration getServiceConfiguration()
public KeYRecoderMapping rec2key()
private void insertToMap(ModelElement r, ModelElement k)
public CompilationUnit[] readCompilationUnitsAsFiles(java.lang.String[] cUnitStrings) throws ParseExceptionInFile
cUnitStrings
- a list of strings, each element is interpreted as a file to be
read. not null.ParseExceptionInFile
- any exception occurring while treating the file is wrapped
into a parse exception that contains the filename.private java.util.List<CompilationUnit> recoderCompilationUnitsAsFiles(java.lang.String[] cUnitStrings)
cUnitStrings
- a list of strings, each element is interpreted as a file to be
read. not null.public CompilationUnit readCompilationUnit(java.lang.String cUnitString)
cUnitString
- a string represents a compilation unitprivate java.util.List<CompilationUnit> recoderCompilationUnits(java.lang.String[] cUnitStrings)
cUnitStrings
- an array of strings, each element represents a compilation
unitpublic void setClassPath(java.io.File bootClassPath, java.util.List<java.io.File> classPath)
public java.util.List<java.lang.String> getDynamicallyCreatedClasses()
private void parseInternalClasses(ProgramFactory pf, java.util.List<CompilationUnit> rcuList) throws java.io.IOException, ParseException, ParserException
bootClassPath
is set to null, it locates java classes that
are stored internally within the jar-file or the binary directory. The
JAVALANG.TXT file lists all files to be loaded. The files are found using
a special JavaReduxFileCollection
.
If, however, bootClassPath
is assigned a value, this is treated
as a directory (not a JAR file at the moment) and all files in this
directory are read in. This is done using a
DirectoryFileCollection
.java.io.IOException
ParseException
ParserException
private java.util.List<CompilationUnit> parseLibs() throws ParseException, java.io.IOException, ParserException
.java
file within the entries (directories
or zip files)
.class
file within the entries
(directories or zip files)
ParserException
java.io.IOException
ParseException
private void removeCodeFromClasses(CompilationUnit rcu, boolean allowed)
public void parseSpecialClasses()
private void parseLibraryClasses0() throws ParseException, java.io.IOException, ParserException
ParseException
java.io.IOException
ParserException
protected void transformModel(java.util.List<CompilationUnit> cUnits)
cUnits
- a list of compilation units, not null.protected MethodDeclaration embedBlock(StatementBlock block)
<virtual_method_for_parsing>
.block
- the recoder.java.StatementBlock to wrapprotected ClassDeclaration embedMethod(MethodDeclaration mdecl, Context context)
mdecl
- the recoder.java.declaration.MethodDeclaration to wrapcontext
- the recoder.java.declaration.ClassDeclaration where the method
has to be embeddedpublic Context createEmptyContext()
protected Context createContext(ImmutableList<ProgramVariable> pvs)
pvs
- a list of variablesprotected Context createContext(ImmutableList<ProgramVariable> vars, CrossReferenceSourceInfo csi)
vars
- a list of variablescsi
- a special source infoprivate void addProgramVariablesToClassContext(ClassDeclaration classContext, ImmutableList<ProgramVariable> vars, CrossReferenceSourceInfo csi)
classContext
- context to add tovars
- vars to addprivate VariableSpecification lookupVarSpec(ProgramVariable pv)
private TypeReference name2typeReference(java.lang.String typeName)
typeName
- non-null type name as stringStatementBlock recoderBlock(java.lang.String block, Context context)
block
- a String describing a java blockcontext
- recoder.java.CompilationUnit in which the block has to be
interpretedpublic JavaBlock readBlock(java.lang.String block, Context context)
block
- a String describing a java blockcontext
- recoder.java.CompilationUnit in which the block has to be
interprestedpublic JavaBlock readBlockWithEmptyContext(java.lang.String block)
readBlockWithEmptyContext
in interface JavaReader
block
- a String describing a java blockpublic JavaBlock readBlockWithProgramVariables(Namespace<IProgramVariable> varns, java.lang.String s)
readBlockWithProgramVariables
in interface JavaReader
s
- a String describing a java blockprivate ClassDeclaration interactClassDecl()
private static java.lang.String trim(java.lang.String s)
private static java.lang.String trim(java.lang.String s, int length)
private static int[] extractPositionInfo(java.lang.String errorMessage)
public static void reportError(java.lang.String message, java.lang.Throwable t)
message
- message to be used.t
- the cause of the exceptional caseConvertException
- always