public class Recoder2KeYConverter
extends java.lang.Object
callConvert(recoder.java.ProgramElement)
that does the job in general. Several special cases must be treated
separately.
This code used to be part of Recoder2KeY
and has been 'out-sourced'.Modifier and Type | Field and Description |
---|---|
private java.util.HashMap<java.lang.Class<? extends JavaProgramElement>,java.lang.reflect.Constructor<?>> |
constructorCache
caches constructor access for reflection.
|
private java.lang.String |
currentClass
stores the class that is currently processed
|
private java.util.HashMap<FieldSpecification,ProgramVariable> |
fieldSpecificationMapping
Hashmap from
recoder.java.declaration.FieldSpecification
to ProgramVariable ; this is necessary to avoid cycles
when converting initializers. |
private boolean |
inLoopInit
flag which is true if currently in a for initialiser or update
|
protected java.util.HashMap<?,?> |
locClass2finalVar
locClass2finalVar stores the final variables that need to be passed
to the constructor of an anonymous class.
|
private java.util.HashMap<java.lang.Class<?>,java.lang.reflect.Method> |
methodCache
caches access to methods for reflection.
|
private java.util.HashMap<MethodDeclaration,IProgramMethod> |
methodsDeclaring
methodsDeclaring contains the recoder method declarations as keys that
have been started to convert but are not yet finished.
|
private NamespaceSet |
namespaceSet
The namespaces are here to provide some conversion functions access to
previously defined logical symbols.
|
private Recoder2KeY |
rec2key
the associated Recoder2KeY object
|
private static int |
RECODER_PREFIX_LENGTH |
private Services |
services |
Constructor and Description |
---|
Recoder2KeYConverter(Recoder2KeY rec2key,
Services services,
NamespaceSet nss) |
Modifier and Type | Method and Description |
---|---|
protected java.lang.Object |
callConvert(ProgramElement pe)
convert a recoder ProgramElement to a corresponding KeY data structure
entity.
|
protected ExtList |
collectChildren(NonTerminalProgramElement pe)
iterate over all children and call convert upon them.
|
private ExtList |
collectChildrenAndComments(ProgramElement pe)
collects both comments and children of a program element
|
private ExtList |
collectComments(ProgramElement pe)
collects comments and adds their converted KeY-counterpart to the list of
children
|
Abstract |
convert(Abstract m) |
AllFields |
convert(AllFields e) |
AllObjects |
convert(AllObjects e) |
AnnotationUseSpecification |
convert(AnnotationUseSpecification aus) |
ArrayInitializer |
convert(ArrayInitializer arg) |
FieldReference |
convert(ArrayLengthReference alr)
converts a recoder array length reference to a usual KeY field reference
|
ArrayReference |
convert(ArrayReference ar)
converts an ArrayReference.
|
Assert |
convert(Assert a)
convert Assert
|
BinaryAnd |
convert(BinaryAnd arg) |
BinaryAndAssignment |
convert(BinaryAndAssignment arg) |
BinaryNot |
convert(BinaryNot arg) |
BinaryOr |
convert(BinaryOr arg) |
BinaryOrAssignment |
convert(BinaryOrAssignment arg) |
BinaryXOr |
convert(BinaryXOr arg) |
BinaryXOrAssignment |
convert(BinaryXOrAssignment arg) |
BooleanLiteral |
convert(BooleanLiteral booleanLit)
convert a recoder BooleanLiteral to a KeY BooleanLiteral
|
Break |
convert(Break arg) |
Case |
convert(Case c)
converts a Case.
|
Catch |
convert(Catch arg) |
CatchAllStatement |
convert(CatchAllStatement cas) |
CharLiteral |
convert(CharLiteral charLit)
convert a recoder CharLiteral to a KeY CharLiteral
|
ClassDeclaration |
convert(ClassDeclaration td)
convert a recoder ClassDeclaration to a KeY ClassDeclaration
|
ClassInitializer |
convert(ClassInitializer arg) |
Comment |
convert(Comment rc)
converts the recoder.java.Comment to the KeYDependance
|
CompilationUnit |
convert(CompilationUnit arg) |
Conditional |
convert(Conditional arg) |
IProgramMethod |
convert(ConstructorDeclaration cd)
convert a recoder ConstructorDeclaration to a KeY IProgramMethod
(especially the declaration type of its parent is determined and handed
over)
|
CopyAssignment |
convert(CopyAssignment arg) |
IProgramMethod |
convert(DefaultConstructor dc)
convert a recoder DefaultConstructor to a KeY IProgramMethod (especially
the declaration type of its parent is determined and handed over)
|
Divide |
convert(Divide arg) |
DivideAssignment |
convert(DivideAssignment arg) |
Do |
convert(Do d)
converts a Do.
|
DoubleLiteral |
convert(DoubleLiteral doubleLit)
convert a recoder DoubleLiteral to a KeY DoubleLiteral
|
Else |
convert(Else arg) |
EmptyMapLiteral |
convert(EmptyMapLiteral e) |
EmptySeqLiteral |
convert(EmptySeqLiteral e) |
EmptySetLiteral |
convert(EmptySetLiteral e) |
EmptyStatement |
convert(EmptyStatement m) |
EnhancedFor |
convert(EnhancedFor f)
converts a java5-enhanced-for.
|
EnumClassDeclaration |
convert(EnumClassDeclaration td)
convert a recoder EnumDeclaration to a KeY EnumClassDeclaration.
|
Equals |
convert(Equals arg) |
DLEmbeddedExpression |
convert(EscapeExpression e)
Resolve the function symbol which is embedded here to its logical
counterpart.
|
ExecutionContext |
convert(ExecutionContext arg) |
Extends |
convert(Extends arg) |
FieldDeclaration |
convert(FieldDeclaration fd)
convert a recoder FieldDeclaration to a KeY FieldDeclaration (especially
the declaration type of its parent is determined and handed over)
|
Expression |
convert(FieldReference fr)
converts a recoder field reference.
|
FieldSpecification |
convert(FieldSpecification recoderVarSpec)
convert a recoder FieldSpecification to a KeY FieldSpecification (checks
dimension and hands it over and insert in hash map)
|
Final |
convert(Final m) |
Finally |
convert(Finally arg) |
FloatLiteral |
convert(FloatLiteral floatLit)
convert a recoder FloatLiteral to a KeY FloatLiteral
|
For |
convert(For f)
converts a For.
|
Ghost |
convert(Ghost m) |
GreaterOrEquals |
convert(GreaterOrEquals arg) |
GreaterThan |
convert(GreaterThan arg) |
ProgramElementName |
convert(Identifier id)
convert a recoder Identifier to a KeY Identifier
|
If |
convert(If arg) |
Implements |
convert(Implements arg) |
ProgramElementName |
convert(ImplicitIdentifier id) |
Import |
convert(Import im) |
Instanceof |
convert(Instanceof rio) |
InterfaceDeclaration |
convert(InterfaceDeclaration td) |
Intersect |
convert(Intersect e) |
IntLiteral |
convert(IntLiteral intLit)
convert a recoder IntLiteral to a KeY IntLiteral
|
ProgramElement |
convert(JavaProgramElement pe)
The default procedure.
|
LabeledStatement |
convert(LabeledStatement l)
convert a labeled statement.
|
LessOrEquals |
convert(LessOrEquals arg) |
LessThan |
convert(LessThan arg) |
LocalVariableDeclaration |
convert(LocalVariableDeclaration arg) |
LogicalAnd |
convert(LogicalAnd arg) |
LogicalNot |
convert(LogicalNot arg) |
LogicalOr |
convert(LogicalOr arg) |
LongLiteral |
convert(LongLiteral longLit)
convert a recoder LongLiteral to a KeY LongLiteral
|
MergePointStatement |
convert(MergePointStatement mps) |
MethodBodyStatement |
convert(MethodBodyStatement rmbs)
convert a recoderext MethodBodyStatement to a KeY MethodBodyStatement
|
MethodFrame |
convert(MethodCallStatement rmcs)
convert a recoderext MethodFrameStatement to a KeY MethodFrameStatement
|
IProgramMethod |
convert(MethodDeclaration md)
convert a recoder MethodDeclaration to a KeY IProgramMethod (especially
the declaration type of its parent is determined and handed over)
|
MethodReference |
convert(MethodReference mr)
converts a recoder method reference.
|
Minus |
convert(Minus arg) |
MinusAssignment |
convert(MinusAssignment arg) |
Model |
convert(Model m) |
Modulo |
convert(Modulo arg) |
ModuloAssignment |
convert(ModuloAssignment arg) |
JavaProgramElement |
convert(Negative arg)
Converts the Negative from recoder to the corresponding KeY JavaProgramElement.
|
New |
convert(New n)
converts a New.
|
NewArray |
convert(NewArray newArr)
converts the recoder.java.expression.operator.NewArray node to the
KeYDependance
|
NoState |
convert(NoState m) |
NotEquals |
convert(NotEquals arg) |
NullLiteral |
convert(NullLiteral nullLit)
convert a recoder NullLiteral to a KeY NullLiteral
|
PackageReference |
convert(PackageReference m) |
PackageSpecification |
convert(PackageSpecification arg) |
ParameterDeclaration |
convert(ParameterDeclaration pd)
converts a recoder ParameterDeclaration to a KeY ParameterDeclaration
(especially the declaration type of its parent is determined and handed
over)
|
ParenthesizedExpression |
convert(ParenthesizedExpression arg) |
PassiveExpression |
convert(PassiveExpression arg) |
Plus |
convert(Plus arg) |
PlusAssignment |
convert(PlusAssignment arg) |
Positive |
convert(Positive arg) |
PostDecrement |
convert(PostDecrement arg) |
PostIncrement |
convert(PostIncrement arg) |
PreDecrement |
convert(PreDecrement arg) |
PreIncrement |
convert(PreIncrement arg) |
Private |
convert(Private m) |
Protected |
convert(Protected m) |
Public |
convert(Public m) |
Return |
convert(Return arg) |
SeqConcat |
convert(SeqConcat e) |
SeqGet |
convert(SeqGet e) |
SeqIndexOf |
convert(SeqIndexOf e) |
SeqLength |
convert(SeqLength e) |
SeqReverse |
convert(SeqReverse e) |
SeqSingleton |
convert(SeqSingleton e) |
SeqSub |
convert(SeqSub e) |
SetMinus |
convert(SetMinus e) |
SetUnion |
convert(SetUnion e) |
ShiftLeft |
convert(ShiftLeft arg) |
ShiftLeftAssignment |
convert(ShiftLeftAssignment arg) |
ShiftRight |
convert(ShiftRight arg) |
ShiftRightAssignment |
convert(ShiftRightAssignment arg) |
Singleton |
convert(Singleton e) |
StatementBlock |
convert(StatementBlock block)
convert a statement block and remove all included anonymous classes.
|
Static |
convert(Static m) |
StrictFp |
convert(StrictFp m) |
StringLiteral |
convert(StringLiteral stringLit)
convert a recoder StringLiteral to a KeY StringLiteral
|
SuperConstructorReference |
convert(SuperConstructorReference scr)
converts a SpecialConstructorReference.
|
SuperReference |
convert(SuperReference sr)
Convert a super referene.
|
SynchronizedBlock |
convert(SynchronizedBlock arg) |
Then |
convert(Then arg) |
ThisConstructorReference |
convert(ThisConstructorReference arg) |
ThisReference |
convert(ThisReference tr)
Convert a this referene.
|
Throw |
convert(Throw arg) |
Throws |
convert(Throws arg) |
Times |
convert(Times arg) |
TimesAssignment |
convert(TimesAssignment arg) |
TransactionStatement |
convert(TransactionStatement tr) |
Try |
convert(Try arg) |
TwoState |
convert(TwoState m) |
TypeCast |
convert(TypeCast c)
convert a recoder type cast to a KeY TypeCast
|
TypeReference |
convert(TypeReference tr)
convert a recoder TypeReference to a KeY TypeReference (checks dimension
and hands it over)
|
ProgramElement |
convert(UncollatedReferenceQualifier urq)
if an UncollatedReferenceQualifier appears throw a ConvertExceception
because these qualifiers have to be resolved by running the
CrossReferencer
|
UnsignedShiftRight |
convert(UnsignedShiftRight arg) |
UnsignedShiftRightAssignment |
convert(UnsignedShiftRightAssignment arg) |
ProgramVariable |
convert(VariableReference vr)
converts a recoder variable reference.
|
VariableSpecification |
convert(VariableSpecification recoderVarSpec)
convert a recoder VariableSpecification to a KeY VariableSpecification
(checks dimension and hands it over and insert in hashmap)
|
While |
convert(While w)
converts a While.
|
Statement |
convertBody(LoopStatement ls)
helper for convert(x) with x a LoopStatement.
|
Guard |
convertGuard(LoopStatement ls)
helper for convert(x) with x a LoopStatement.
|
LoopInit |
convertLoopInitializers(LoopStatement ls)
helper for convert(x) with x a LoopStatement.
|
ForUpdates |
convertUpdates(LoopStatement ls)
helper for convert(x) with x a LoopStatement.
|
private ImmutableList<Field> |
filterField(FieldDeclaration field)
extracts all fields out of fielddeclaration
|
private ProgramVariable |
find(java.lang.String name,
ImmutableList<Field> fields)
retrieves a field with the given name out of the list
|
private Literal |
getCompileTimeConstantInitializer(FieldSpecification recoderVarSpec)
|
private java.lang.Class<?> |
getKeYClass(java.lang.Class<? extends JavaProgramElement> recoderClass)
gets the KeY-Class related to the recoder one
|
private java.lang.reflect.Constructor<?> |
getKeYClassConstructor(java.lang.Class<? extends JavaProgramElement> recoderClass)
determines the right standard constructor of the KeYClass.
|
private KeYJavaType |
getKeYJavaType(Type javaType)
retrieve a key type using the converter available from Recoder2KeY
|
private java.lang.String |
getKeYName(java.lang.Class<? extends JavaProgramElement> recoderClass)
constructs the name of the corresponding KeYClass.
|
private Literal |
getLiteralFor(ConstantEvaluator.EvaluationResult p_er) |
protected KeYRecoderMapping |
getMapping()
retrieve the recoder<->key mapping from the associated Recoder2KeY.
|
private ProgramVariable |
getProgramVariableForFieldSpecification(FieldSpecification recoderVarSpec)
this is needed by #convert(FieldSpecification).
|
private VariableSpecification |
getRecoderVarSpec(VariableReference vr)
this is needed to convert variable references
|
private CrossReferenceServiceConfiguration |
getServiceConfiguration()
retrieve the service configuration from the associated Recoder2KeY.
|
private Recoder2KeYTypeConverter |
getTypeConverter()
retrieve the type converter from the associated Recoder2KeY
|
protected void |
insertToMap(ModelElement r,
ModelElement k)
store an element to the recoder<->key mapping.
|
private boolean |
isParsingLibs()
are we currently parsing library code?
|
(package private) static java.lang.String |
makeAdmissibleName(java.lang.String s)
replace some numbers from anonymous class names.
|
private PositionInfo |
positionInfo(SourceElement se)
convert recoder position info to key position info
|
ProgramElement |
process(ProgramElement pe) |
CompilationUnit |
processCompilationUnit(CompilationUnit cu,
java.lang.String context) |
IProgramMethod |
processDefaultConstructor(DefaultConstructor df) |
private final Services services
private final java.util.HashMap<java.lang.Class<?>,java.lang.reflect.Method> methodCache
private final java.util.HashMap<java.lang.Class<? extends JavaProgramElement>,java.lang.reflect.Constructor<?>> constructorCache
private java.util.HashMap<FieldSpecification,ProgramVariable> fieldSpecificationMapping
recoder.java.declaration.FieldSpecification
to ProgramVariable
; this is necessary to avoid cycles
when converting initializers. Access to this map is performed via the
method getProgramVariableForFieldSpecification
private java.util.HashMap<MethodDeclaration,IProgramMethod> methodsDeclaring
protected java.util.HashMap<?,?> locClass2finalVar
private java.lang.String currentClass
private boolean inLoopInit
private Recoder2KeY rec2key
private final NamespaceSet namespaceSet
private static int RECODER_PREFIX_LENGTH
public Recoder2KeYConverter(Recoder2KeY rec2key, Services services, NamespaceSet nss)
public ProgramElement process(ProgramElement pe)
public IProgramMethod processDefaultConstructor(DefaultConstructor df)
public CompilationUnit processCompilationUnit(CompilationUnit cu, java.lang.String context)
private KeYJavaType getKeYJavaType(Type javaType)
javaType
- type to look upprivate Recoder2KeYTypeConverter getTypeConverter()
private CrossReferenceServiceConfiguration getServiceConfiguration()
protected KeYRecoderMapping getMapping()
private boolean isParsingLibs()
Recoder2KeY.isParsingLibs()
protected java.lang.Object callConvert(ProgramElement pe) throws ConvertException
pe
- the recoder.java.JavaProgramElement to be converted, not null.ConvertException
- if the conversion failsprotected ExtList collectChildren(NonTerminalProgramElement pe)
pe
- the NonTerminalProgramElement that needs its children before
being convertedstatic java.lang.String makeAdmissibleName(java.lang.String s)
private ExtList collectComments(ProgramElement pe)
pe
- the ProgramElement that needs its comments before being
convertedprivate ExtList collectChildrenAndComments(ProgramElement pe)
pe
- program elementprivate PositionInfo positionInfo(SourceElement se)
se
- the sourcelement to extract from, not nullprivate Literal getLiteralFor(ConstantEvaluator.EvaluationResult p_er)
p_er
private ImmutableList<Field> filterField(FieldDeclaration field)
field
- the FieldDeclaration of which the field specifications have to
be extractedprivate ProgramVariable find(java.lang.String name, ImmutableList<Field> fields)
name
- a String with the name of the field to be looked forfields
- the IListpublic ProgramElement convert(JavaProgramElement pe)
pe
- the recoder.java.ProgramElement to be convertedprivate java.lang.Class<?> getKeYClass(java.lang.Class<? extends JavaProgramElement> recoderClass)
recoderClass
- the original Class within recoderConvertException
- for various reasonsprivate java.lang.String getKeYName(java.lang.Class<? extends JavaProgramElement> recoderClass)
recoderClass
- Class that is the original recoderprivate java.lang.reflect.Constructor<?> getKeYClassConstructor(java.lang.Class<? extends JavaProgramElement> recoderClass)
recoderClass
- the Class of the recoder AST objectprotected void insertToMap(ModelElement r, ModelElement k)
r
- the recoder element (not null)k
- the key element (not null)public Instanceof convert(Instanceof rio)
public NewArray convert(NewArray newArr)
public IntLiteral convert(IntLiteral intLit)
public BooleanLiteral convert(BooleanLiteral booleanLit)
public EmptySetLiteral convert(EmptySetLiteral e)
public AllObjects convert(AllObjects e)
public EmptySeqLiteral convert(EmptySeqLiteral e)
public SeqSingleton convert(SeqSingleton e)
public SeqIndexOf convert(SeqIndexOf e)
public SeqReverse convert(SeqReverse e)
public EmptyMapLiteral convert(EmptyMapLiteral e)
public DLEmbeddedExpression convert(EscapeExpression e)
public StringLiteral convert(StringLiteral stringLit)
public DoubleLiteral convert(DoubleLiteral doubleLit)
public FloatLiteral convert(FloatLiteral floatLit)
public LongLiteral convert(LongLiteral longLit)
longLit
- the LongLiteral from recoderpublic CharLiteral convert(CharLiteral charLit)
charLit
- the CharLiteral from recoderpublic NullLiteral convert(NullLiteral nullLit)
public ProgramElementName convert(Identifier id)
public ProgramElementName convert(ImplicitIdentifier id)
public MethodFrame convert(MethodCallStatement rmcs)
public MethodBodyStatement convert(MethodBodyStatement rmbs)
public MergePointStatement convert(MergePointStatement mps)
public CatchAllStatement convert(CatchAllStatement cas)
public ClassDeclaration convert(ClassDeclaration td)
public EnumClassDeclaration convert(EnumClassDeclaration td)
public InterfaceDeclaration convert(InterfaceDeclaration td)
public ParameterDeclaration convert(ParameterDeclaration pd)
public FieldDeclaration convert(FieldDeclaration fd)
public IProgramMethod convert(ConstructorDeclaration cd)
public IProgramMethod convert(DefaultConstructor dc)
public SuperConstructorReference convert(SuperConstructorReference scr)
public ThisReference convert(ThisReference tr)
public SuperReference convert(SuperReference sr)
public VariableSpecification convert(VariableSpecification recoderVarSpec)
public IProgramMethod convert(MethodDeclaration md)
public FieldSpecification convert(FieldSpecification recoderVarSpec)
private ProgramVariable getProgramVariableForFieldSpecification(FieldSpecification recoderVarSpec)
private Literal getCompileTimeConstantInitializer(FieldSpecification recoderVarSpec)
recoderVarSpec
, if the variable is a compile-time
constant, and null
otherwisepublic TypeReference convert(TypeReference tr)
public ProgramElement convert(UncollatedReferenceQualifier urq)
private VariableSpecification getRecoderVarSpec(VariableReference vr)
public ProgramVariable convert(VariableReference vr)
vr
- the recoder variable reference.public FieldReference convert(ArrayLengthReference alr)
public Expression convert(FieldReference fr)
fr
- the recoder field reference.public MethodReference convert(MethodReference mr)
mr
- the recoder method reference.public LabeledStatement convert(LabeledStatement l)
public For convert(For f)
f
- the For of recoderpublic AnnotationUseSpecification convert(AnnotationUseSpecification aus)
public EnhancedFor convert(EnhancedFor f)
f
- the EnhancedFor of recoderpublic While convert(While w)
w
- the While of recoderpublic Do convert(Do d)
d
- the Do of recoderpublic Statement convertBody(LoopStatement ls)
public Guard convertGuard(LoopStatement ls)
public ForUpdates convertUpdates(LoopStatement ls)
public LoopInit convertLoopInitializers(LoopStatement ls)
public ArrayReference convert(ArrayReference ar)
public Case convert(Case c)
public New convert(New n)
public StatementBlock convert(StatementBlock block)
block
- the recoder.java.StatementBlock to be convertedpublic PassiveExpression convert(PassiveExpression arg)
public ParenthesizedExpression convert(ParenthesizedExpression arg)
public CopyAssignment convert(CopyAssignment arg)
public TransactionStatement convert(TransactionStatement tr)
public PostIncrement convert(PostIncrement arg)
public PreIncrement convert(PreIncrement arg)
public PostDecrement convert(PostDecrement arg)
public PreDecrement convert(PreDecrement arg)
public PlusAssignment convert(PlusAssignment arg)
public MinusAssignment convert(MinusAssignment arg)
public TimesAssignment convert(TimesAssignment arg)
public DivideAssignment convert(DivideAssignment arg)
public LessOrEquals convert(LessOrEquals arg)
public GreaterThan convert(GreaterThan arg)
public GreaterOrEquals convert(GreaterOrEquals arg)
public LogicalNot convert(LogicalNot arg)
public LogicalAnd convert(LogicalAnd arg)
public ArrayInitializer convert(ArrayInitializer arg)
public SynchronizedBlock convert(SynchronizedBlock arg)
public CompilationUnit convert(CompilationUnit arg)
public ClassInitializer convert(ClassInitializer arg)
public PackageSpecification convert(PackageSpecification arg)
public Implements convert(Implements arg)
public LocalVariableDeclaration convert(LocalVariableDeclaration arg)
public ExecutionContext convert(ExecutionContext arg)
public ThisConstructorReference convert(ThisConstructorReference arg)
public BinaryAndAssignment convert(BinaryAndAssignment arg)
public BinaryOrAssignment convert(BinaryOrAssignment arg)
public BinaryXOrAssignment convert(BinaryXOrAssignment arg)
public ShiftRight convert(ShiftRight arg)
public UnsignedShiftRight convert(UnsignedShiftRight arg)
public ShiftLeftAssignment convert(ShiftLeftAssignment arg)
public ShiftRightAssignment convert(ShiftRightAssignment arg)
public UnsignedShiftRightAssignment convert(UnsignedShiftRightAssignment arg)
public JavaProgramElement convert(Negative arg)
arg
- the recoder Negativepublic ModuloAssignment convert(ModuloAssignment arg)
public Conditional convert(Conditional arg)
public EmptyStatement convert(EmptyStatement m)
public PackageReference convert(PackageReference m)