Recoder2KeY (KeY API Documentation)

java.lang.Object
- de.uka.ilkd.key.java.Recoder2KeY

All Implemented Interfaces:

JavaReader

Direct Known Subclasses:

SchemaRecoder2KeY
```
public class Recoder2KeY
extends java.lang.Object
implements JavaReader
```
This class is the bridge between recoder ast data structures and KeY data structures. Syntactical entities and types can be transferred from recoder to KeY. It manages the entire contact with the recoder framework and ensures that their cross-referencing data is always uptodate. Prior to reading any source code, special classes (i.e. stubs for some needed library classes) are parsed in to have them available at any time. To use a Recoder2KeY bridge to convert data structures you can use the functions: 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.

See Also:

Recoder2KeYConverter, Recoder2KeYTypeConverter

Field Summary

Fields
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

Constructor Summary

Constructors
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.

Method Summary

All Methods Static Methods Instance Methods Concrete Methods
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.

Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

- Field Detail
  - classPath
```
private java.util.List<java.io.File> classPath
```
    the set of File objects that describes the classpath to be searched for classes. it may contain a null file which indicates that the default classes are not to be read.
  - bootClassPath
```
private java.io.File bootClassPath
```
    the File object that describes the directory from which the internal classes are to be read. They are read in differently - therefore the second category. A null value indicates that the boot classes are to be read from an internal repository.
  - mapping
```
private KeYRecoderMapping mapping
```
    this mapping stores the relation between recoder and KeY entities in a bidirectional way. It is used for syntactical structures and types.
  - servConf
```
private KeYCrossReferenceServiceConfiguration servConf
```
    Recoder's serviceConfiguration that is used throughout this process.
  - interactCounter
```
private static int interactCounter
```
    counter used to enumerate the anonymous implicit classes
  - parsingLibs
```
private boolean parsingLibs
```
    this flag indicates whether we are currently parsing library classes (special classes)
  - converter
```
private Recoder2KeYConverter converter
```
    the object that handles the transformation from recoder AST to KeY AST
  - typeConverter
```
private Recoder2KeYTypeConverter typeConverter
```
    the object that handles the transformation from recoder types to KeY types
  - dynamicallyCreatedCompilationUnits
```
private java.util.Collection<? extends CompilationUnit> dynamicallyCreatedCompilationUnits
```
    the list of classnames that contain the classes that are referenced but not defined. For those classe types a dummy stub is created at parse time.
  - services
```
private final Services services
```
- Constructor Detail
  - Recoder2KeY
```
public Recoder2KeY(Services services,
                   KeYCrossReferenceServiceConfiguration servConf,
                   KeYRecoderMapping rec2key,
                   NamespaceSet nss,
                   TypeConverter tc)
```
    create a new Recoder2KeY transformation object. The converter and type converter associated with this object will be created. Several properties of the recoder framework will be set up. The classpath is set to null, the mapping is retrieved from the services, as well as the underlying type converter
    
    Parameters:
    
    servConf - the service configuration to be used, not null
    
    rec2key - the mapping to store mapped types and mapped ASTs to, not null
    
    nss - the namespaces to work upon, not null
    
    tc - the type converter, not null
  - Recoder2KeY
```
public Recoder2KeY(Services services,
                   NamespaceSet nss)
```
    create a new Recoder2KeY transformation object. The converter and type converter associated with this object will be created. Several properties of the recoder framework will be set up. The classpath is set to null, the mapping is retrieved from the services, as well as the underlying type converter
    
    Parameters:
    
    services - services to retrieve objects from, not null
    
    nss - the namespaces to work upon, not null
  - Recoder2KeY
```
private Recoder2KeY(Services services,
                    KeYCrossReferenceServiceConfiguration servConf,
                    java.lang.String classPath,
                    KeYRecoderMapping rec2key,
                    NamespaceSet nss,
                    TypeConverter tc)
```
    create a new Recoder2KeY transformation object. The converter and type converter associated with this object will be created. Several properties of the recoder framework will be set up.
    
    Parameters:
    
    servConf - the service configuration to be used, not null
    
    classPath - the classpath to look up source files, ignored if null
    
    rec2key - the mapping to store mapped types and mapped ASTs to, not null
    
    nss - the namespaces to work upon, not null
    
    tc - the type converter, not null
    
    Throws:
    
    java.lang.IllegalArgumentException - if arguments are not valid (null e.g.)
- Method Detail
  - makeConverter
```
protected Recoder2KeYConverter makeConverter(Services services,
                                             NamespaceSet nss)
```
    create the ast converter. This is overwritten in SchemaRecoder2KeY to use schema-aware converters.
    
    Parameters:
    
    services -
    
    nss - the namespaces provided to the constructor
    
    Returns:
    
    a newley created converter
  - getConverter
```
public Recoder2KeYConverter getConverter()
```
    return the associated converter object
    
    Returns:
    
    not null
  - getTypeConverter
```
public Recoder2KeYTypeConverter getTypeConverter()
```
    return the associated type converter object
    
    Returns:
    
    not null
  - setParsingLibs
```
private void setParsingLibs(boolean v)
```
    set this to true before parsing special classes and to false afterwards.
    
    Parameters:
    
    v - the state of the special parsing flage
  - isParsingLibs
```
public boolean isParsingLibs()
```
    are we currently parsing library code (special classes)?
    
    Returns:
    
    true iff currently parsing special classes.
  - getServiceConfiguration
```
public KeYCrossReferenceServiceConfiguration getServiceConfiguration()
```
  - rec2key
```
public KeYRecoderMapping rec2key()
```
  - insertToMap
```
private void insertToMap(ModelElement r,
                         ModelElement k)
```
  - readCompilationUnitsAsFiles
```
public CompilationUnit[] readCompilationUnitsAsFiles(java.lang.String[] cUnitStrings)
                                              throws ParseExceptionInFile
```
    parse a list of java files and transform it to the corresponding KeY entities. Each element of the array is treated as a filename to read in.
    
    Parameters:
    
    cUnitStrings - a list of strings, each element is interpreted as a file to be read. not null.
    
    Returns:
    
    a new list containing the recoder compilation units corresponding to the given files.
    
    Throws:
    
    ParseExceptionInFile - any exception occurring while treating the file is wrapped into a parse exception that contains the filename.
  - recoderCompilationUnitsAsFiles
```
private java.util.List<CompilationUnit> recoderCompilationUnitsAsFiles(java.lang.String[] cUnitStrings)
```
    parse a list of java files. Each element of the array is treated as a filename to read in.
    
    Parameters:
    
    cUnitStrings - a list of strings, each element is interpreted as a file to be read. not null.
    
    Returns:
    
    a new list containing the recoder compilation units corresponding to the given files.
  - readCompilationUnit
```
public CompilationUnit readCompilationUnit(java.lang.String cUnitString)
```
    read a compilation unit, given as a string.
    
    Parameters:
    
    cUnitString - a string represents a compilation unit
    
    Returns:
    
    a KeY structured compilation unit.
  - recoderCompilationUnits
```
private java.util.List<CompilationUnit> recoderCompilationUnits(java.lang.String[] cUnitStrings)
```
    read a number of compilation units, each given as a string.
    
    Parameters:
    
    cUnitStrings - an array of strings, each element represents a compilation unit
    
    Returns:
    
    a list of KeY structured compilation units.
  - setClassPath
```
public void setClassPath(java.io.File bootClassPath,
                         java.util.List<java.io.File> classPath)
```
  - getDynamicallyCreatedClasses
```
public java.util.List<java.lang.String> getDynamicallyCreatedClasses()
```
    get the list of names of classes that have been created dynamically due to lacking definitions. For all classes that are referenced but not defined, an empty dummy stub is created. This method returns the list of their fully qualified class names.
    
    Returns:
    
    an unmodifiable list of fully qualified class names
  - parseInternalClasses
```
private void parseInternalClasses(ProgramFactory pf,
                                  java.util.List<CompilationUnit> rcuList)
                           throws java.io.IOException,
                                  ParseException,
                                  ParserException
```
    This method loads the internal classes - also called the "boot" classes. If 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.
    
    Throws:
    
    java.io.IOException
    
    ParseException
    
    ParserException
  - parseLibs
```
private java.util.List<CompilationUnit> parseLibs()
                                           throws ParseException,
                                                  java.io.IOException,
                                                  ParserException
```
    reads compilation units that will be treated as library classes. Proceed as follows:
    1. If "classPath" is set and contains at least one entry
      
      read every .java file within the entries (directories or zip files)
      read every .class file within the entries (directories or zip files)
    2. else read a special collection of classes that is stored internally
    Throws:
    
    ParserException
    
    java.io.IOException
    
    ParseException
  - removeCodeFromClasses
```
private void removeCodeFromClasses(CompilationUnit rcu,
                                   boolean allowed)
```
  - parseSpecialClasses
```
public void parseSpecialClasses()
```
    makes sure that the special classes (library classes) have been parsed in. If not parsed yet, the special classes are read in and converted. This method throws only runtime exceptions for historical reasons.
  - parseLibraryClasses0
```
private void parseLibraryClasses0()
                           throws ParseException,
                                  java.io.IOException,
                                  ParserException
```
    Throws:
    
    ParseException
    
    java.io.IOException
    
    ParserException
  - transformModel
```
protected void transformModel(java.util.List<CompilationUnit> cUnits)
```
    Transform a list of compilation units. Once a compilation unit has been parsed in and prior to converting it to the KeY structures, several transformations have to be performed upon it. You can add your own Transformation here. Make sure it is in the correct order.
    
    Parameters:
    
    cUnits - a list of compilation units, not null.
  - embedBlock
```
protected MethodDeclaration embedBlock(StatementBlock block)
```
    wraps a RECODER StatementBlock in a method it is wrapped in a method called <virtual_method_for_parsing>.
    
    Parameters:
    
    block - the recoder.java.StatementBlock to wrap
    
    Returns:
    
    the enclosing recoder.java.MethodDeclaration
  - embedMethod
```
protected ClassDeclaration embedMethod(MethodDeclaration mdecl,
                                       Context context)
```
    wraps a RECODER MethodDeclaration in a class
    
    Parameters:
    
    mdecl - the recoder.java.declaration.MethodDeclaration to wrap
    
    context - the recoder.java.declaration.ClassDeclaration where the method has to be embedded
    
    Returns:
    
    the enclosing recoder.java.declaration.ClassDeclaration
  - createEmptyContext
```
public Context createEmptyContext()
```
    creates an empty RECODER compilation unit with a temporary name.
    
    Returns:
    
    the new recoder.java.CompilationUnit
  - createContext
```
protected Context createContext(ImmutableList<ProgramVariable> pvs)
```
    create a new context with a temporary name and make a list of variables visible from within. Use the default source info.
    
    Parameters:
    
    pvs - a list of variables
    
    Returns:
    
    a newly created context.
  - createContext
```
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.
    
    Parameters:
    
    vars - a list of variables
    
    csi - a special source info
    
    Returns:
    
    a newly created context.
  - addProgramVariablesToClassContext
```
private void addProgramVariablesToClassContext(ClassDeclaration classContext,
                                               ImmutableList<ProgramVariable> vars,
                                               CrossReferenceSourceInfo csi)
```
    add a list of variables to a context
    
    Parameters:
    
    classContext - context to add to
    
    vars - vars to add
  - lookupVarSpec
```
private VariableSpecification lookupVarSpec(ProgramVariable pv)
```
    look up in the mapping the variable specification for a program variable. used by addProgramVariablesToClassContext
  - name2typeReference
```
private TypeReference name2typeReference(java.lang.String typeName)
```
    given a name as string, construct a recoder type reference from it.
    
    Parameters:
    
    typeName - non-null type name as string
    
    Returns:
    
    a freshly created type reference to the given type.
  - recoderBlock
```
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.
    
    Parameters:
    
    block - a String describing a java block
    
    context - recoder.java.CompilationUnit in which the block has to be interpreted
    
    Returns:
    
    the parsed and resolved recoder statement block
  - readBlock
```
public JavaBlock readBlock(java.lang.String block,
                           Context context)
```
    parses a given JavaBlock using the context to determine the right references
    
    Parameters:
    
    block - a String describing a java block
    
    context - recoder.java.CompilationUnit in which the block has to be interprested
    
    Returns:
    
    the parsed and resolved JavaBlock
  - readBlockWithEmptyContext
```
public JavaBlock readBlockWithEmptyContext(java.lang.String block)
```
    parses a given JavaBlock using the context to determine the right references using an empty context
    
    Specified by:
    
    readBlockWithEmptyContext in interface JavaReader
    
    Parameters:
    
    block - a String describing a java block
    
    Returns:
    
    the parsed and resolved JavaBlock
  - readBlockWithProgramVariables
```
public 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. The variables of the namespace are used to create a new class context
    
    Specified by:
    
    readBlockWithProgramVariables in interface JavaReader
    
    Parameters:
    
    s - a String describing a java block
    
    Returns:
    
    the parsed and resolved JavaBlock
  - interactClassDecl
```
private ClassDeclaration interactClassDecl()
```
    make a new classdeclaration with a temporary name. The name is a unique implicit identifier.
    
    Returns:
    
    a newly created recoder ClassDeclaration with a unique name
  - trim
```
private static java.lang.String trim(java.lang.String s)
```
    reduce the size of a string to a maximum of 150 characters. Introduces ellipses [...]
  - trim
```
private static java.lang.String trim(java.lang.String s,
                                     int length)
```
    reduce the size of a string to a maximum of length.
  - extractPositionInfo
```
private static int[] extractPositionInfo(java.lang.String errorMessage)
```
    tries to parse recoders exception position information
  - reportError
```
public static void reportError(java.lang.String message,
                               java.lang.Throwable t)
```
    report an error in form of a ConvertException. The cause is always attached to the resulting exception.
    
    Parameters:
    
    message - message to be used.
    
    t - the cause of the exceptional case
    
    Throws:
    
    ConvertException - always

Class Recoder2KeY

Field Summary

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

Field Detail

classPath

bootClassPath

mapping

servConf

interactCounter

parsingLibs

converter

typeConverter

dynamicallyCreatedCompilationUnits

services

Constructor Detail

Recoder2KeY

Recoder2KeY

Recoder2KeY

Method Detail

makeConverter

getConverter

getTypeConverter

setParsingLibs

isParsingLibs

getServiceConfiguration

rec2key

insertToMap

readCompilationUnitsAsFiles

recoderCompilationUnitsAsFiles

readCompilationUnit

recoderCompilationUnits

setClassPath

getDynamicallyCreatedClasses

parseInternalClasses

parseLibs

removeCodeFromClasses

parseSpecialClasses

parseLibraryClasses0

transformModel

embedBlock

embedMethod

createEmptyContext

createContext

createContext

addProgramVariablesToClassContext

lookupVarSpec

name2typeReference

recoderBlock

readBlock

readBlockWithEmptyContext

readBlockWithProgramVariables

interactClassDecl

trim

trim

extractPositionInfo

reportError