Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Sign in
Toggle navigation
Menu
Open sidebar
sarah.grebing
ProofScriptParser
Commits
e0c77460
Commit
e0c77460
authored
Feb 20, 2018
by
Sarah Grebing
Browse files
local converter for local namespaces
parent
9aba5490
Pipeline
#18884
failed with stages
in 2 minutes and 12 seconds
Changes
21
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
lang/src/main/antlr/edu/kit/iti/formal/psdbg/parser/ScriptLanguage.g4
View file @
e0c77460
...
...
@@ -46,6 +46,7 @@ assignment
| variable=ID (COLON type=ID)? ASSIGN expression SEMICOLON
;
expression
:
expression MUL expression #exprMultiplication
...
...
@@ -56,6 +57,7 @@ expression
| expression AND expression #exprAnd
| expression OR expression #exprOr
| expression IMP expression #exprIMP
| expression USING LBRACKET argList RBRACKET #namespaceset
//| expression EQUIV expression already covered by EQ/NEQ
| expression LBRACKET substExpressionList RBRACKET #exprSubst
| ID LPAREN (expression (',' expression)*)? RPAREN #function
...
...
lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ASTTraversal.java
View file @
e0c77460
...
...
@@ -226,4 +226,11 @@ public interface ASTTraversal<T> extends Visitor<T> {
relaxBlock
.
getBody
().
accept
(
this
);
return
null
;
}
@Override
default
T
visit
(
NamespaceSetExpression
nss
)
{
nss
.
getExpression
().
accept
(
this
);
nss
.
getSignature
().
accept
(
this
);
return
null
;
}
}
lang/src/main/java/edu/kit/iti/formal/psdbg/parser/DefaultASTVisitor.java
View file @
e0c77460
...
...
@@ -176,5 +176,10 @@ public class DefaultASTVisitor<T> implements Visitor<T> {
public
T
visit
(
RelaxBlock
relaxBlock
)
{
return
defaultVisit
(
relaxBlock
);
}
@Override
public
T
visit
(
NamespaceSetExpression
nss
)
{
return
defaultVisit
(
nss
);
}
}
lang/src/main/java/edu/kit/iti/formal/psdbg/parser/TransformAst.java
View file @
e0c77460
...
...
@@ -244,6 +244,14 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
return
ctx
.
matchPattern
().
accept
(
this
);
}
@Override
public
Object
visitNamespaceset
(
ScriptLanguageParser
.
NamespacesetContext
ctx
)
{
NamespaceSetExpression
nse
=
new
NamespaceSetExpression
();
nse
.
setExpression
((
Expression
)
ctx
.
expression
().
accept
(
this
));
nse
.
setSignature
((
Signature
)
ctx
.
argList
().
accept
(
this
));
return
nse
;
}
@Override
public
Object
visitExprIMP
(
ScriptLanguageParser
.
ExprIMPContext
ctx
)
{
return
createBinaryExpression
(
ctx
,
ctx
.
expression
(),
Operator
.
IMPLICATION
);
...
...
lang/src/main/java/edu/kit/iti/formal/psdbg/parser/Visitor.java
View file @
e0c77460
...
...
@@ -90,4 +90,5 @@ public interface Visitor<T> {
T
visit
(
RelaxBlock
relaxBlock
);
T
visit
(
NamespaceSetExpression
nss
);
}
lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/NamespaceSetExpression.java
0 → 100644
View file @
e0c77460
package
edu.kit.iti.formal.psdbg.parser.ast
;
import
edu.kit.iti.formal.psdbg.parser.NotWelldefinedException
;
import
edu.kit.iti.formal.psdbg.parser.ScriptLanguageParser
;
import
edu.kit.iti.formal.psdbg.parser.Visitor
;
import
edu.kit.iti.formal.psdbg.parser.types.Type
;
import
lombok.Getter
;
import
lombok.Setter
;
public
class
NamespaceSetExpression
extends
Expression
<
ScriptLanguageParser
.
NamespacesetContext
>{
@Getter
@Setter
private
Expression
expression
;
@Getter
@Setter
private
Signature
signature
=
new
Signature
();
@Override
public
<
T
>
T
accept
(
Visitor
<
T
>
visitor
)
{
return
visitor
.
visit
(
this
);
}
@Override
public
boolean
hasMatchExpression
()
{
return
expression
.
hasMatchExpression
();
}
@Override
public
int
getPrecedence
()
{
return
5
;
}
@Override
public
NamespaceSetExpression
copy
()
{
NamespaceSetExpression
nse
=
new
NamespaceSetExpression
();
nse
.
expression
=
expression
.
copy
();
nse
.
signature
=
signature
.
copy
();
return
nse
;
}
@Override
public
Type
getType
(
Signature
signature
)
throws
NotWelldefinedException
{
return
expression
.
getType
(
signature
);
}
}
lang/src/main/java/edu/kit/iti/formal/psdbg/parser/data/Value.java
View file @
e0c77460
...
...
@@ -2,6 +2,7 @@ package edu.kit.iti.formal.psdbg.parser.data;
import
edu.kit.iti.formal.psdbg.parser.ast.*
;
import
edu.kit.iti.formal.psdbg.parser.types.SimpleType
;
import
edu.kit.iti.formal.psdbg.parser.types.TermType
;
import
edu.kit.iti.formal.psdbg.parser.types.Type
;
import
edu.kit.iti.formal.psdbg.parser.types.TypeFacade
;
import
lombok.Getter
;
...
...
lang/src/main/java/edu/kit/iti/formal/psdbg/parser/types/SimpleType.java
View file @
e0c77460
...
...
@@ -23,27 +23,52 @@ package edu.kit.iti.formal.psdbg.parser.types;
*/
import
javax.annotation.Nullable
;
/**
* Represents the possible types (including scriptVarTypes).
* <p>
* Created at 30.04.2017
*
* INT("\\term int"),
BOOL("\\term bool"),
ANY("\\term any"),
INT_ARRAY("\\term int[]"),
OBJECT("\\term Object"),
HEAP("\\term Heap"),
FIELD("\\term Field"),
LOCSET("\\term LocSet"),
FORMULA("\\formula"),
SEQ("\\term Seq");
* @author Sarah Grebing
*/
public
enum
SimpleType
implements
Type
{
STRING
(
"string"
),
ANY
(
"any"
),
PATTERN
(
"pattern"
),
INT
(
"int"
),
BOOL
(
"bool"
),
INT_ARRAY
(
"int[]"
),
OBJECT
(
"object"
),
HEAP
(
"heap"
),
FIELD
(
"field"
),
LOCSET
(
"locset"
),
NULL
(
"null"
),
FORMULA
(
"formula"
),
SEQ
(
"Seq"
);
STRING
(
"string"
,
"string"
),
//ANY("any", "any"),
PATTERN
(
"pattern"
,
null
),
INT
(
"int"
,
"int"
),
BOOL
(
"bool"
,
"bool"
),
/*NULL("null", interpreterSort),
FORMULA("formula", interpreterSort),
SEQ("Seq", interpreterSort)*/
;
private
final
String
symbol
;
private
@Nullable
final
String
interpreterSort
;
SimpleType
(
String
symbol
)
{
SimpleType
(
String
symbol
,
@Nullable
String
interpreterSort
)
{
this
.
symbol
=
symbol
;
this
.
interpreterSort
=
interpreterSort
;
}
@Override
public
String
symbol
()
{
return
symbol
;
}
@Override
public
String
interpreterSort
()
{
return
interpreterSort
;
}
}
lang/src/main/java/edu/kit/iti/formal/psdbg/parser/types/TermType.java
View file @
e0c77460
...
...
@@ -29,4 +29,8 @@ public class TermType implements Type {
+
">"
;
}
@Override
public
String
interpreterSort
()
{
return
argTypes
.
get
(
0
).
interpreterSort
();
}
}
lang/src/main/java/edu/kit/iti/formal/psdbg/parser/types/Type.java
View file @
e0c77460
...
...
@@ -6,4 +6,5 @@ package edu.kit.iti.formal.psdbg.parser.types;
*/
public
interface
Type
{
String
symbol
();
String
interpreterSort
();
}
rt-key/src/main/java/edu/kit/iti/formal/psdbg/ValueInjector.java
0 → 100644
View file @
e0c77460
package
edu.kit.iti.formal.psdbg
;
import
de.uka.ilkd.key.java.Services
;
import
de.uka.ilkd.key.logic.*
;
import
de.uka.ilkd.key.logic.sort.Sort
;
import
de.uka.ilkd.key.macros.scripts.ProofScriptCommand
;
import
de.uka.ilkd.key.macros.scripts.ScriptException
;
import
de.uka.ilkd.key.macros.scripts.meta.*
;
import
de.uka.ilkd.key.parser.DefaultTermParser
;
import
de.uka.ilkd.key.parser.ParserException
;
import
de.uka.ilkd.key.pp.AbbrevMap
;
import
de.uka.ilkd.key.proof.Goal
;
import
de.uka.ilkd.key.proof.Node
;
import
de.uka.ilkd.key.proof.Proof
;
import
edu.kit.iti.formal.psdbg.interpreter.data.TermValue
;
import
jdk.nashorn.internal.objects.annotations.Getter
;
import
jdk.nashorn.internal.objects.annotations.Setter
;
import
lombok.RequiredArgsConstructor
;
import
lombok.Value
;
import
sun.security.jca.GetInstance
;
import
java.io.StringReader
;
import
java.lang.annotation.Retention
;
import
java.lang.reflect.Method
;
import
java.math.BigInteger
;
import
java.util.ArrayList
;
import
java.util.HashMap
;
import
java.util.List
;
import
java.util.Map
;
/**
* @author Alexander Weigl
* @version 1 (29.03.17)
*/
public
class
ValueInjector
{
/**
* A default instance
*
* @see #getInstance()
*/
private
static
ValueInjector
instance
;
/**
* A mapping between desired types and suitable @{@link StringConverter}.
* <p>
* Should be <pre>T --> StringConverter<T></pre>
*/
private
List
<
ConverterWrapper
>
converters
=
new
ArrayList
<>();
public
static
<
T
>
T
injection
(
ProofScriptCommand
command
,
T
obj
,
Map
<
String
,
Object
>
arguments
)
throws
ArgumentRequiredException
,
InjectionReflectionException
,
NoSpecifiedConverterException
,
ConversionException
{
return
getInstance
().
inject
(
command
,
obj
,
arguments
);
}
/**
* Returns the default instance of a {@link ValueInjector}
* Use with care. No multi-threading.
*
* @return a static reference to the default converter.
* @see #createDefault()
*/
public
static
ValueInjector
getInstance
()
{
if
(
instance
==
null
)
{
instance
=
createDefault
();
}
return
instance
;
}
/**
* Returns a fresh instance of a {@link ValueInjector} with the support
* for basic primitive data types.
*
* @return a fresh instance
*/
public
static
ValueInjector
createDefault
()
{
ValueInjector
vi
=
new
ValueInjector
();
vi
.
addConverter
(
Integer
.
class
,
Integer:
:
parseInt
);
vi
.
addConverter
(
Long
.
class
,
Long:
:
parseLong
);
vi
.
addConverter
(
Boolean
.
class
,
Boolean:
:
parseBoolean
);
vi
.
addConverter
(
Double
.
class
,
Double:
:
parseDouble
);
vi
.
addConverter
(
String
.
class
,
(
String
s
)
->
s
);
vi
.
addConverter
(
Boolean
.
TYPE
,
Boolean:
:
parseBoolean
);
vi
.
addConverter
(
Byte
.
TYPE
,
Byte:
:
parseByte
);
vi
.
addConverter
(
Character
.
TYPE
,
s
->
s
.
charAt
(
0
));
vi
.
addConverter
(
Short
.
TYPE
,
Short:
:
parseShort
);
vi
.
addConverter
(
Integer
.
TYPE
,
Integer:
:
parseInt
);
vi
.
addConverter
(
Long
.
TYPE
,
Long:
:
parseLong
);
vi
.
addConverter
(
Double
.
TYPE
,
Double:
:
parseDouble
);
vi
.
addConverter
(
Float
.
TYPE
,
Float:
:
parseFloat
);
vi
.
addConverter
(
BigInteger
.
class
,
Integer
.
class
,
(
BigInteger
b
)
->
b
.
intValue
());
vi
.
addConverter
(
BigInteger
.
class
,
Integer
.
TYPE
,
(
BigInteger
b
)
->
b
.
intValue
());
return
vi
;
}
public
static
ValueInjector
createDefault
(
Node
node
)
{
ValueInjector
valueInjector
=
createDefault
();
TermConverter
termConverter
=
new
TermConverter
(
node
);
valueInjector
.
addConverter
(
Term
.
class
,
termConverter
);
valueInjector
.
addConverter
(
Sort
.
class
,
new
SortConverter
(
node
.
proof
()));
valueInjector
.
addConverter
(
TermValue
.
class
,
Term
.
class
,
new
TermValueConverter
(
node
));
return
valueInjector
;
}
@Value
public
static
class
TermValueConverter
implements
Converter
<
TermValue
,
Term
>
{
private
Node
node
;
@Override
public
Term
convert
(
TermValue
s
)
throws
Exception
{
if
(
s
.
getTerm
()
!=
null
)
{
return
s
.
getTerm
();
}
else
{
TermConverter
converter
=
new
TermConverter
(
node
);
Term
t
=
converter
.
convert
(
s
.
getTermRepr
());
s
.
setTerm
(
t
);
return
t
;
}
}
}
@RequiredArgsConstructor
public
static
class
TermConverter
implements
Converter
<
String
,
Term
>
{
private
final
Node
node
;
private
final
static
DefaultTermParser
PARSER
=
new
DefaultTermParser
();
private
NamespaceSet
additionalNamespace
;
@Override
public
Term
convert
(
String
string
)
throws
ParserException
{
StringReader
reader
=
new
StringReader
(
string
);
Services
services
=
node
.
proof
().
getServices
();
//TODO check if local namespace is needed
NamespaceSet
ns
;
Goal
g
=
node
.
proof
().
getGoal
(
node
);
if
(
g
!=
null
)
{
ns
=
g
.
getLocalNamespaces
();
}
else
{
ns
=
node
.
proof
().
getNamespaces
();
}
if
(
additionalNamespace
!=
null
)
{
ns
=
ns
.
copy
();
ns
.
add
(
additionalNamespace
);
}
Term
formula
=
PARSER
.
parse
(
reader
,
null
,
services
,
ns
,
node
.
proof
().
abbreviations
());
return
formula
;
}
}
@Value
public
static
class
SortConverter
implements
Converter
<
String
,
Sort
>{
private
Proof
proof
;
@Override
public
Sort
convert
(
String
sortName
)
{
return
proof
.
getServices
().
getNamespaces
().
sorts
().
lookup
(
sortName
);
}
}
/**
* Injects the converted version of the given {@code arguments} in the given {@code obj}.
*
* @param command a proof script command
* @param obj a non-null instance of a parameter class (with annotation)
* @param arguments a non-null string map
* @param <T> type safety
* @return the same object as {@code obj}
* @throws ArgumentRequiredException a required argument was not given in {@code arguments}
* @throws InjectionReflectionException an access on some reflection methods occured
* @throws NoSpecifiedConverterException unknown type for the current converter map
* @throws ConversionException an converter could not translage the given value
* in {@arguments}
* @see Option
* @see Flag
*/
public
<
T
>
T
inject
(
ProofScriptCommand
command
,
T
obj
,
Map
<
String
,
Object
>
arguments
)
throws
ConversionException
,
InjectionReflectionException
,
NoSpecifiedConverterException
,
ArgumentRequiredException
{
List
<
ProofScriptArgument
>
meta
=
ArgumentsLifter
.
inferScriptArguments
(
obj
.
getClass
(),
command
);
List
<
ProofScriptArgument
>
varArgs
=
new
ArrayList
<>(
meta
.
size
());
List
<
String
>
usedKeys
=
new
ArrayList
<>();
for
(
ProofScriptArgument
arg
:
meta
)
{
if
(
arg
.
hasVariableArguments
())
{
varArgs
.
add
(
arg
);
}
else
{
injectIntoField
(
arg
,
arguments
,
obj
);
usedKeys
.
add
(
arg
.
getName
());
}
}
for
(
ProofScriptArgument
vararg
:
varArgs
)
{
final
Map
map
=
getStringMap
(
obj
,
vararg
);
final
int
prefixLength
=
vararg
.
getName
().
length
();
for
(
Map
.
Entry
<
String
,
Object
>
e
:
arguments
.
entrySet
())
{
String
k
=
e
.
getKey
();
Object
v
=
e
.
getValue
();
if
(!
usedKeys
.
contains
(
k
)
&&
k
.
startsWith
(
vararg
.
getName
()))
{
map
.
put
(
k
.
substring
(
prefixLength
),
convert
(
vararg
,
v
));
usedKeys
.
add
(
k
);
}
}
}
return
obj
;
}
private
Map
getStringMap
(
Object
obj
,
ProofScriptArgument
vararg
)
throws
InjectionReflectionException
{
try
{
Map
map
=
(
Map
)
vararg
.
getField
().
get
(
obj
);
if
(
map
==
null
)
{
map
=
new
HashMap
();
vararg
.
getField
().
set
(
obj
,
map
);
}
return
map
;
}
catch
(
IllegalAccessException
e
)
{
throw
new
InjectionReflectionException
(
"Error on using reflection on class "
+
obj
.
getClass
(),
e
,
vararg
);
}
}
private
void
injectIntoField
(
ProofScriptArgument
meta
,
Map
<
String
,
Object
>
args
,
Object
obj
)
throws
InjectionReflectionException
,
ArgumentRequiredException
,
ConversionException
,
NoSpecifiedConverterException
{
final
Object
val
=
args
.
get
(
meta
.
getName
());
if
(
val
==
null
)
{
if
(
meta
.
isRequired
())
{
throw
new
ArgumentRequiredException
(
String
.
format
(
"Argument %s:%s is required, but %s was given. "
+
"For comamnd class: '%s'"
,
meta
.
getName
(),
meta
.
getField
().
getType
(),
val
,
meta
.
getCommand
().
getClass
()),
meta
);
}
}
else
{
Object
value
=
convert
(
meta
,
val
);
try
{
//if (meta.getType() != value.getClass())
// throw new ConversionException("The typed returned '" + val.getClass()
// + "' from the converter mismtached with the
// type of the field " + meta.getType(), meta);
meta
.
getField
().
set
(
obj
,
value
);
}
catch
(
IllegalAccessException
e
)
{
throw
new
InjectionReflectionException
(
"Could not inject values via reflection"
,
e
,
meta
);
}
}
}
@SuppressWarnings
(
"unchecked"
)
private
Object
convert
(
ProofScriptArgument
meta
,
Object
val
)
throws
NoSpecifiedConverterException
,
ConversionException
{
Converter
converter
=
getConverter
(
val
.
getClass
(),
meta
.
getType
());
if
(
converter
==
null
)
{
throw
new
NoSpecifiedConverterException
(
"No converter registered for class: "
+
meta
.
getField
().
getType
(),
meta
);
}
try
{
return
converter
.
convert
(
val
);
}
catch
(
Exception
e
)
{
throw
new
ConversionException
(
String
.
format
(
"Could not convert value %s to type %s"
,
val
,
meta
.
getField
().
getType
()),
e
,
meta
);
}
}
/**
* Registers the given converter for the specified class.
*
* @param clazz a class
* @param conv a converter for the given class
* @param <T> an arbitrary type
*/
public
<
T
,
R
>
void
addConverter
(
Class
<
T
>
from
,
Class
<
R
>
to
,
Converter
<
T
,
R
>
conv
)
{
converters
.
add
(
new
ConverterWrapper
<
T
,
R
>(
from
,
to
,
conv
));
}
public
<
R
>
void
addConverter
(
Class
<
R
>
to
,
Converter
<
String
,
R
>
conv
)
{
addConverter
(
String
.
class
,
to
,
conv
);
}
public
<
T
,
R
>
void
addConverter
(
Converter
<
T
,
R
>
conv
)
{
Method
[]
ms
=
conv
.
getClass
().
getMethods
();
for
(
Method
m
:
ms
)
{
if
(
m
.
getParameterCount
()
==
1
)
{
Class
<
T
>
t
=
(
Class
<
T
>)
m
.
getParameterTypes
()[
0
];
Class
<
R
>
c
=
(
Class
<
R
>)
m
.
getReturnType
();
addConverter
(
t
,
c
,
conv
);
}
}
}
/**
* Finds a converter for the given class.
* @return null or a suitable converter (registered) converter for the requested class.
*/
@SuppressWarnings
(
"unchecked"
)
public
<
T
,
R
>
Converter
<
T
,
R
>
getConverter
(
Class
<
T
>
from
,
Class
<
R
>
to
)
{
for
(
ConverterWrapper
c:
converters
)
{
if
(
c
.
getFrom
().
equals
(
from
)
&&
c
.
getTo
().
equals
(
to
))
return
c
.
getConverter
();
}
throw
new
RuntimeException
(
"Could not find a suitable converter for types "
+
from
+
" to "
+
to
);
}
@Value
private
static
class
ConverterWrapper
<
T
,
R
>
{
Class
<
T
>
from
;
Class
<
R
>
to
;
Converter
<
T
,
R
>
converter
;
}
interface
Converter
<
T
,
R
>
{
R
convert
(
T
o
)
throws
Exception
;
}
}
rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeyEvaluator.java
0 → 100644
View file @
e0c77460
package
edu.kit.iti.formal.psdbg.interpreter
;
import
de.uka.ilkd.key.logic.Name
;
import
de.uka.ilkd.key.logic.NamespaceSet
;
import
de.uka.ilkd.key.logic.Term
;
import
de.uka.ilkd.key.logic.op.LogicVariable
;
import
de.uka.ilkd.key.logic.op.QuantifiableVariable
;
import
de.uka.ilkd.key.logic.sort.Sort
;
import
de.uka.ilkd.key.proof.Goal
;
import
edu.kit.iti.formal.psdbg.interpreter.data.GoalNode
;
import
edu.kit.iti.formal.psdbg.interpreter.data.KeyData
;
import
edu.kit.iti.formal.psdbg.interpreter.data.TermValue
;
import
edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment
;
import
edu.kit.iti.formal.psdbg.parser.ast.Expression
;
import
edu.kit.iti.formal.psdbg.parser.ast.NamespaceSetExpression
;
import
edu.kit.iti.formal.psdbg.parser.ast.SubstituteExpression
;
import
edu.kit.iti.formal.psdbg.parser.ast.Variable
;
import
edu.kit.iti.formal.psdbg.parser.data.Value
;
import
edu.kit.iti.formal.psdbg.parser.types.SimpleType
;
import
edu.kit.iti.formal.psdbg.parser.types.TermType
;
import
edu.kit.iti.formal.psdbg.parser.types.Type
;
import
edu.kit.iti.formal.psdbg.parser.types.TypeFacade
;
import
org.key_project.util.collection.ImmutableArray
;
import
java.util.regex.Matcher
;
import
java.util.regex.Pattern
;
public
class
KeyEvaluator
extends
Evaluator
<
KeyData
>
{
public
KeyEvaluator
(
VariableAssignment
assignments
,
GoalNode
<
KeyData
>
g
)
{
super
(
assignments
,
g
);
}
@Override
public
Value
visit
(
NamespaceSetExpression
nss
)
{
Value
term
=
(
Value
)
nss
.
getExpression
().
accept
(
this
);
if
(
term
.
getType
()
instanceof
TermType
)
{
TermValue
data
=
((
TermValue
)
term
.
getData
()).
copy
();
nss
.
getSignature
().
forEach
((
v
,
s
)
->
{
Sort
sort
=
asKeySort
(
s
,
getGoal
().
getData
().
getGoal
());
data
.
getNs
().
variables
().
add
(
new
LogicVariable
(
new
Name
(
v
.
getIdentifier
()),
sort
));
});
return
new
Value
(
term
.
getType
(),
data
);
}
else
{
throw
new
IllegalStateException
(
"Try to apply substitute on a non-term value."
);
}
}
private
Sort
asKeySort
(
Type
symbol
,
Goal
g
)
{
NamespaceSet
global
=
g
.
proof
().
getServices
().
getNamespaces
();
Sort
s
=
global
.
sorts
().
lookup
(
symbol
.
interpreterSort
());
if
(
s
!=
null
)
return
s
;