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
b36a3c1f
Commit
b36a3c1f
authored
Jan 17, 2018
by
LULUDBR\Lulu
Browse files
Merge remote-tracking branch 'origin/master'
parents
f323aa01
9f657295
Changes
18
Hide whitespace changes
Inline
Side-by-side
matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/MatcherFacade.java
View file @
b36a3c1f
package
edu.kit.iti.formal.psdbg.termmatcher
;
import
de.uka.ilkd.key.java.Services
;
import
de.uka.ilkd.key.logic.Semisequent
;
import
de.uka.ilkd.key.logic.Sequent
;
import
de.uka.ilkd.key.logic.Term
;
...
...
@@ -21,8 +22,8 @@ import org.apache.logging.log4j.Logger;
public
class
MatcherFacade
{
private
static
Logger
logger
=
LogManager
.
getLogger
(
MatcherFacade
.
class
);
public
static
Matchings
matches
(
String
pattern
,
Term
keyTerm
)
{
MatcherImpl
matcher
=
new
MatcherImpl
();
public
static
Matchings
matches
(
String
pattern
,
Term
keyTerm
,
Services
services
)
{
MatcherImpl
matcher
=
new
MatcherImpl
(
services
);
matcher
.
setCatchAll
(
false
);
MatchPatternParser
mpp
=
getParser
(
pattern
);
MatchPatternParser
.
TermPatternContext
ctx
=
mpp
.
termPattern
();
...
...
@@ -50,12 +51,13 @@ public class MatcherFacade {
* @param pattern Semisequent pattern e.g. f(x), f(x)
* @param semiSeq Concrete KeY Semisequent
* @param catchAll
* @param services
* @return Matchings
*/
public
static
Matchings
matches
(
String
pattern
,
Semisequent
semiSeq
,
boolean
catchAll
)
{
public
static
Matchings
matches
(
String
pattern
,
Semisequent
semiSeq
,
boolean
catchAll
,
Services
services
)
{
MatchPatternParser
mpp
=
getParser
(
pattern
);
MatchPatternParser
.
SemiSeqPatternContext
ctx
=
mpp
.
semiSeqPattern
();
MatcherImpl
matcher
=
new
MatcherImpl
();
MatcherImpl
matcher
=
new
MatcherImpl
(
services
);
matcher
.
setCatchAll
(
catchAll
);
Matchings
m
=
matcher
.
accept
(
ctx
,
MatchPathFacade
.
createRoot
(
semiSeq
));
return
m
;
...
...
@@ -67,9 +69,10 @@ public class MatcherFacade {
*
* @param pattern e.g., f(x) ==> f(y)
* @param sequent
* @param services
* @return
*/
public
static
Matchings
matches
(
String
pattern
,
Sequent
sequent
,
boolean
catchAll
)
{
public
static
Matchings
matches
(
String
pattern
,
Sequent
sequent
,
boolean
catchAll
,
Services
services
)
{
MatchPatternParser
mpp
=
getParser
(
pattern
);
MatchPatternParser
.
SequentPatternContext
ctx
=
mpp
.
sequentPattern
();
logger
.
info
(
"Matching \n"
+
pattern
+
"\n"
+
sequent
.
toString
());
...
...
@@ -78,21 +81,22 @@ public class MatcherFacade {
return
new
Matchings
();
}
MatcherImpl
matcher
=
new
MatcherImpl
();
MatcherImpl
matcher
=
new
MatcherImpl
(
services
);
matcher
.
setCatchAll
(
catchAll
);
Matchings
m
=
matcher
.
accept
(
ctx
,
MatchPathFacade
.
create
(
sequent
));
return
m
;
}
/**
* Like {@link #matches(String, Sequent)} but allows to use
* Like {@link #matches(String, Sequent
, Services
)} but allows to use
* MatcherImpl#isCatchAll.
*
* @param pattern
* @param sequent
* @param services
* @return
*/
public
static
Matchings
matches
(
String
pattern
,
Sequent
sequent
)
{
return
matches
(
pattern
,
sequent
,
true
);
public
static
Matchings
matches
(
String
pattern
,
Sequent
sequent
,
Services
services
)
{
return
matches
(
pattern
,
sequent
,
true
,
services
);
}
}
matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/MatcherImpl.java
View file @
b36a3c1f
package
edu.kit.iti.formal.psdbg.termmatcher
;
import
com.google.common.collect.Sets
;
import
de.uka.ilkd.key.logic.Semisequent
;
import
de.uka.ilkd.key.logic.SequentFormula
;
import
de.uka.ilkd.key.logic.Term
;
import
de.uka.ilkd.key.java.Services
;
import
de.uka.ilkd.key.logic.*
;
import
de.uka.ilkd.key.logic.op.QuantifiableVariable
;
import
edu.kit.formal.psdb.termmatcher.MatchPatternLexer
;
import
edu.kit.formal.psdb.termmatcher.MatchPatternParser
;
import
edu.kit.iti.formal.psdbg.termmatcher.mp.MatchPath
;
import
static
edu
.
kit
.
iti
.
formal
.
psdbg
.
termmatcher
.
mp
.
MatchPathFacade
.*;
import
lombok.Getter
;
import
lombok.RequiredArgsConstructor
;
import
lombok.Setter
;
import
org.antlr.v4.runtime.CommonToken
;
import
org.antlr.v4.runtime.Token
;
...
...
@@ -20,21 +19,24 @@ import java.util.stream.Collectors;
import
java.util.stream.IntStream
;
import
java.util.stream.Stream
;
import
static
edu
.
kit
.
iti
.
formal
.
psdbg
.
termmatcher
.
mp
.
MatchPathFacade
.*;
/**
* Matchpattern visitor visits the matchpatterns of case-statements
*
* @author Alexander Weigl
* @author S. Grebing
*/
@RequiredArgsConstructor
class
MatcherImpl
extends
MatchPatternDualVisitor
<
Matchings
,
MatchPath
>
{
static
final
Matchings
NO_MATCH
=
new
Matchings
();
static
final
Matchings
EMPTY_MATCH
=
Matchings
.
singleton
(
"EMPTY_MATCH"
,
null
);
static
final
Map
<
String
,
MatchPath
>
EMPTY_VARIABLE_ASSIGNMENT
=
EMPTY_MATCH
.
first
();
@Getter
private
final
Services
services
;
Random
random
=
new
Random
(
42L
);
/*
* Reduce two matchinfos
*
...
...
@@ -67,7 +69,6 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
}
*/
private
List
<
Integer
>
currentPosition
=
new
ArrayList
<>();
/**
* If true, we assume every term in the pattern has a binder.
* The binding names are generated.
...
...
@@ -79,17 +80,28 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
private
boolean
catchAll
=
false
;
private
static
HashMap
<
String
,
MatchPath
>
reduceConform
(
Map
<
String
,
MatchPath
>
h1
,
Map
<
String
,
MatchPath
>
h2
)
{
HashMap
<
String
,
MatchPath
>
listOfElementsofH1
=
new
HashMap
<>(
h1
);
HashMap
<
String
,
MatchPath
>
h3
=
new
HashMap
<>(
h1
);
for
(
String
s1
:
listOfElementsofH1
.
keySet
())
{
for
(
String
s1
:
h3
.
keySet
())
{
if
(!
s1
.
equals
(
"EMPTY_MATCH"
)
&&
(
h2
.
containsKey
(
s1
)
&&
!
h2
.
get
(
s1
).
equals
(
h1
.
get
(
s1
))))
{
return
null
;
}
if
(!
s1
.
equals
(
"EMPTY_MATCH"
)
&&
h2
.
containsKey
(
s1
))
{
if
(
h2
.
get
(
s1
)
instanceof
MatchPath
.
MPQuantifiableVariable
&&
!((
QuantifiableVariable
)
h2
.
get
(
s1
).
getUnit
()).
name
().
toString
().
equals
(
h1
.
get
(
s1
).
toString
()))
{
return
null
;
}
if
(
h1
.
get
(
s1
)
instanceof
MatchPath
.
MPQuantifiableVariable
&&
!((
QuantifiableVariable
)
h1
.
get
(
s1
).
getUnit
()).
name
().
toString
().
equals
(
h2
.
get
(
s1
).
toString
()))
{
return
null
;
}
if
(!
h2
.
get
(
s1
).
equals
(
h1
.
get
(
s1
)))
{
return
null
;
}
}
}
h3
.
putAll
(
h2
);
return
h3
;
listOfElementsofH1
.
putAll
(
h2
);
return
listOfElementsofH1
;
}
/**
...
...
@@ -122,6 +134,7 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
return
oneMatch
?
m3
:
NO_MATCH
;
}
/**
* Transform a number term into an int value.
* <p>
...
...
@@ -449,11 +462,17 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
QuantifiableVariable
qv
=
toMatch
.
boundVars
().
get
(
i
);
if
(
qfPattern
.
getType
()
==
MatchPatternLexer
.
DONTCARE
)
{
match
=
reduceConform
(
match
,
Matchings
.
singleton
(
qfPattern
.
getText
(),
new
MatchPath
.
MPQuantifiableVarible
(
peek
,
qv
,
i
)));
//match = reduceConform(match, Matchings.singleton(qfPattern.getText(), new MatchPath.MPQuantifiableVarible(peek, qv, i)));
match
=
reduceConform
(
match
,
EMPTY_MATCH
);
continue
;
}
if
(
qfPattern
.
getType
()
==
MatchPatternLexer
.
SID
)
{
match
=
reduceConform
(
match
,
Matchings
.
singleton
(
qfPattern
.
getText
(),
new
MatchPath
.
MPQuantifiableVarible
(
peek
,
qv
,
i
)));
TermFactory
tf
=
new
TermFactory
(
new
HashMap
<>());
TermBuilder
tb
=
new
TermBuilder
(
tf
,
services
);
Term
termQVariable
=
tb
.
var
(
qv
);
match
=
reduceConform
(
match
,
Matchings
.
singleton
(
qfPattern
.
getText
(),
new
MatchPath
.
MPTerm
(
peek
,
termQVariable
,
-
i
)));
}
else
{
if
(!
qv
.
name
().
toString
().
equals
(
qfPattern
.
getText
()))
{
return
NO_MATCH
;
...
...
@@ -464,8 +483,17 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
Matchings
fromTerm
=
accept
(
ctx
.
skope
,
create
(
peek
,
0
));
//return handleBindClause(ctx.bindClause(), path, m);
Matchings
retM
=
reduceConformQuant
(
fromTerm
,
match
);
Matchings
retM
=
reduceConform
(
fromTerm
,
match
);
retM
.
forEach
(
stringMatchPathMap
->
{
stringMatchPathMap
.
forEach
((
s
,
matchPath
)
->
{
if
(
matchPath
instanceof
MatchPath
.
MPQuantifiableVariable
)
{
//create term from variablename and put instead into map
}
}
);
});
return
handleBindClause
(
ctx
.
bindClause
(),
peek
,
retM
);
}
...
...
@@ -532,33 +560,6 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
}
private
Matchings
reduceConformQuant
(
Matchings
fromTerm
,
Matchings
match
)
{
Matchings
ret
=
new
Matchings
();
Map
<
String
,
MatchPath
>
quantifiedVarMap
=
match
.
first
();
List
<
Map
<
String
,
MatchPath
>>
list
=
fromTerm
.
stream
().
filter
(
map
->
map
.
entrySet
().
stream
().
allMatch
(
entry
->
{
if
(
entry
.
getValue
()
!=
null
)
{
MatchPath
mp
=
(
MatchPath
)
entry
.
getValue
();
Term
mterm
=
(
Term
)
mp
.
getUnit
();
if
(
quantifiedVarMap
.
containsKey
(
entry
.
getKey
()))
{
return
((
QuantifiableVariable
)
quantifiedVarMap
.
get
(
entry
.
getKey
()).
getUnit
()).
name
().
toString
().
equals
(
mterm
.
op
().
name
().
toString
());
}
else
{
return
true
;
}
}
else
{
return
true
;
}
}
)
).
collect
(
Collectors
.
toList
());
ret
.
addAll
(
list
);
return
ret
;
}
@Override
public
Matchings
visitExprParen
(
MatchPatternParser
.
ExprParenContext
ctx
,
MatchPath
peek
)
{
...
...
@@ -618,6 +619,39 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
}
public
int
getRandomNumber
()
{
return
random
.
nextInt
();
return
Math
.
abs
(
random
.
nextInt
()
)
;
}
}
/* private Matchings reduceConformQuant(Matchings fromTerm, Matchings match) {
Matchings ret = new Matchings();
Map<String, MatchPath> quantifiedVarMap = match.first();
System.out.println("quantifiedVarMap = " + quantifiedVarMap);
List<Map<String, MatchPath>> list = fromTerm.stream().filter(
map -> map.entrySet().stream().allMatch(
entry -> {
System.out.println("entry = " + entry);
if (entry.getValue() != null) {
MatchPath mp = (MatchPath) entry.getValue();
Term mterm = (Term) mp.getUnit();
if (quantifiedVarMap.containsKey(entry.getKey())) {
QuantifiableVariable unit = (QuantifiableVariable) quantifiedVarMap.get(entry.getKey()).getUnit();
return unit.name().toString().
equals(mterm.op().name().toString());
} else {
return true;
}
} else {
//in this case we have an empty match, however, we may have bound quantVars, we need to add them
System.out.println("entry.getKey() = " + entry.getKey());
return true;
}
}
)
).collect(Collectors.toList());
ret.addAll(list);
return ret;
}*/
\ No newline at end of file
matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/mp/MatchPath.java
View file @
b36a3c1f
...
...
@@ -47,9 +47,9 @@ public abstract class MatchPath<T, P> {
return
unit
.
toString
();
}
public
static
final
class
MPQuantifiableVarible
extends
MatchPath
<
QuantifiableVariable
,
Object
>
{
public
static
final
class
MPQuantifiableVari
a
ble
extends
MatchPath
<
QuantifiableVariable
,
Object
>
{
public
MPQuantifiableVarible
(
MatchPath
<?
extends
Object
,
?>
parent
,
QuantifiableVariable
unit
,
int
pos
)
{
public
MPQuantifiableVari
a
ble
(
MatchPath
<?
extends
Object
,
?>
parent
,
QuantifiableVariable
unit
,
int
pos
)
{
super
(
parent
,
unit
,
pos
);
}
...
...
@@ -75,7 +75,7 @@ public abstract class MatchPath<T, P> {
}
public
static
class
MPTerm
extends
MatchPath
<
Term
,
Object
>
{
MPTerm
(
MatchPath
<?
extends
Object
,
?>
parent
,
Term
unit
,
int
pos
)
{
public
MPTerm
(
MatchPath
<?
extends
Object
,
?>
parent
,
Term
unit
,
int
pos
)
{
super
(
parent
,
unit
,
pos
);
}
...
...
matcher/src/test/java/edu/kit/iti/formal/psdbg/termmatcher/MatcherFacadeTest.java
View file @
b36a3c1f
...
...
@@ -59,7 +59,11 @@ public class MatcherFacadeTest {
shouldMatchForm
(
"fint2(1,i)"
,
"fint2(1,i)"
);
shouldMatchForm
(
"\\exists int i; fint2(1,i)"
,
"(\\exists _ _)"
);
shouldMatchForm
(
"\\exists int i; fint2(1,i)"
,
"(\\exists _ ?Term)"
);
shouldMatchForm
(
"\\exists int i; fint2(1,i)"
,
"(\\exists ?X _)"
);
shouldMatchForm
(
"\\exists int i; fint2(1,i)"
,
"(\\exists ?X (fint2(1,?X)))"
);
shouldMatchForm
(
"\\exists int i; \\exists int j; fint2(j,i)"
,
"(\\exists i (\\exists j _))"
);
...
...
@@ -119,26 +123,26 @@ public class MatcherFacadeTest {
private
void
shouldMatch
(
String
key
,
String
pattern
)
throws
ParserException
{
Term
term
=
parseKeyTerm
(
key
);
Matchings
m
=
MatcherFacade
.
matches
(
pattern
,
term
);
Matchings
m
=
MatcherFacade
.
matches
(
pattern
,
term
,
services
);
System
.
out
.
println
(
m
);
}
private
void
shouldMatch
(
String
key
,
String
pattern
,
String
exp
)
throws
ParserException
{
Term
term
=
parseKeyTerm
(
key
);
Matchings
m
=
MatcherFacade
.
matches
(
pattern
,
term
);
Matchings
m
=
MatcherFacade
.
matches
(
pattern
,
term
,
services
);
System
.
out
.
println
(
m
);
Assert
.
assertEquals
(
exp
,
m
.
toString
());
}
private
void
shouldMatchForm
(
String
form
,
String
pattern
)
throws
ParserException
{
Term
formula
=
parserFormula
(
form
);
Matchings
m
=
MatcherFacade
.
matches
(
pattern
,
formula
);
Matchings
m
=
MatcherFacade
.
matches
(
pattern
,
formula
,
services
);
System
.
out
.
println
(
m
);
}
private
void
shouldMatchForm
(
String
form
,
String
pattern
,
String
exp
)
throws
ParserException
{
Term
formula
=
parserFormula
(
form
);
Matchings
m
=
MatcherFacade
.
matches
(
pattern
,
formula
);
Matchings
m
=
MatcherFacade
.
matches
(
pattern
,
formula
,
services
);
System
.
out
.
println
(
m
);
Assert
.
assertEquals
(
exp
,
m
.
toString
());
}
...
...
@@ -193,14 +197,14 @@ public class MatcherFacadeTest {
private
void
shouldMatchSemiSeq
(
String
s
,
String
s1
,
String
exp
)
throws
ParserException
{
Sequent
term
=
parseSeq
(
s
);
Matchings
m
=
MatcherFacade
.
matches
(
s1
,
term
);
Matchings
m
=
MatcherFacade
.
matches
(
s1
,
term
,
services
);
System
.
out
.
println
(
m
);
Assert
.
assertEquals
(
exp
,
m
.
toString
());
}
private
void
shouldMatchSemiSeq
(
String
s
,
String
s1
)
throws
ParserException
{
Sequent
term
=
parseSeq
(
s
);
Matchings
m
=
MatcherFacade
.
matches
(
s1
,
term
);
Matchings
m
=
MatcherFacade
.
matches
(
s1
,
term
,
services
);
System
.
out
.
println
(
m
);
}
...
...
@@ -290,7 +294,7 @@ public class MatcherFacadeTest {
private
void
shouldMatchSeq
(
String
seq
,
String
seqPattern
,
String
exp
)
throws
ParserException
{
Sequent
sequent
=
parseSeq
(
seq
);
Matchings
m
=
MatcherFacade
.
matches
(
seqPattern
,
sequent
);
Matchings
m
=
MatcherFacade
.
matches
(
seqPattern
,
sequent
,
services
);
System
.
out
.
println
(
m
);
Assert
.
assertEquals
(
removeNumbersInBinders
(
m
),
exp
);
}
...
...
@@ -304,7 +308,7 @@ public class MatcherFacadeTest {
private
void
shouldMatchSeq
(
String
seq
,
String
seqPattern
)
throws
ParserException
{
Sequent
sequent
=
parseSeq
(
seq
);
Matchings
m
=
MatcherFacade
.
matches
(
seqPattern
,
sequent
);
Matchings
m
=
MatcherFacade
.
matches
(
seqPattern
,
sequent
,
services
);
System
.
out
.
println
(
m
);
}
}
\ No newline at end of file
matcher/src/test/java/edu/kit/iti/formal/psdbg/termmatcher/TestUpdateMatch.java
View file @
b36a3c1f
...
...
@@ -3,6 +3,7 @@ package edu.kit.iti.formal.psdbg.termmatcher;
import
de.uka.ilkd.key.api.KeYApi
;
import
de.uka.ilkd.key.api.ProofApi
;
import
de.uka.ilkd.key.api.ProofManagementApi
;
import
de.uka.ilkd.key.java.Services
;
import
de.uka.ilkd.key.logic.Sequent
;
import
de.uka.ilkd.key.proof.init.ProofInputException
;
import
de.uka.ilkd.key.proof.io.ProblemLoaderException
;
...
...
@@ -19,7 +20,8 @@ public class TestUpdateMatch {
ProofApi
pa
=
a
.
startProof
(
a
.
getProofContracts
().
get
(
0
));
Sequent
sequent
=
pa
.
getProof
().
root
().
sequent
();
System
.
out
.
println
(
sequent
);
Matchings
result
=
MatcherFacade
.
matches
(
"... update-application(_, ?X) ..."
,
sequent
,
false
);
Matchings
result
=
MatcherFacade
.
matches
(
"... update-application(_, ?X) ..."
,
sequent
,
false
,
null
);
System
.
out
.
println
(
result
);
String
exp
=
normalize
(
"\\<{exc=null;try { result=self.foo(_x)@Test;} catch (java.lang.Throwable e) { exc=e; } }\\> (and(and(and(gt(result,Z(0(#))),java.lang.Object::<inv>(heap,self)),equals(exc,null)),all{f:Field}(all{o:java.lang.Object}(or(or(elementOf(o,f,allLocs),and(not(equals(o,null)),not(equals(boolean::select(heapAtPre,o,java.lang.Object::<created>),TRUE)))),equals(any::select(heap,o,f),any::select(heapAtPre,o,f)))))))"
);
String
x
=
normalize
(
result
.
iterator
().
next
().
get
(
"?X"
).
getUnit
().
toString
().
replace
(
"\n"
,
" "
));
...
...
rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/InterpreterBuilder.java
View file @
b36a3c1f
...
...
@@ -114,8 +114,7 @@ public class InterpreterBuilder {
}
public
InterpreterBuilder
addKeyMatcher
(
ProofApi
api
)
{
ScriptApi
scriptApi
=
api
.
getScriptApi
();
interpreter
.
setMatcherApi
(
new
KeYMatcher
(
scriptApi
,
interpreter
));
interpreter
.
setMatcherApi
(
new
KeYMatcher
(
api
.
getEnv
().
getServices
()));
return
this
;
}
...
...
rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeYMatcher.java
View file @
b36a3c1f
package
edu.kit.iti.formal.psdbg.interpreter
;
import
de.uka.ilkd.key.api.
Script
Api
;
import
de.uka.ilkd.key.
api.VariableAssignment
s
;
import
de.uka.ilkd.key.api.
Proof
Api
;
import
de.uka.ilkd.key.
java.Service
s
;
import
de.uka.ilkd.key.logic.Name
;
import
de.uka.ilkd.key.logic.Term
;
import
de.uka.ilkd.key.logic.op.SchemaVariable
;
...
...
@@ -18,14 +18,13 @@ import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
import
edu.kit.iti.formal.psdbg.interpreter.data.SortType
;
import
edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment
;
import
edu.kit.iti.formal.psdbg.parser.ast.Signature
;
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.termmatcher.MatcherFacade
;
import
edu.kit.iti.formal.psdbg.termmatcher.Matchings
;
import
edu.kit.iti.formal.psdbg.termmatcher.mp.MatchPath
;
import
lombok.Getter
;
import
org.apache.logging.log4j.LogManager
;
import
org.apache.logging.log4j.Logger
;
import
org.key_project.util.collection.ImmutableList
;
...
...
@@ -44,13 +43,13 @@ public class KeYMatcher implements MatcherApi<KeyData> {
private
static
final
Logger
LOGGER
=
LogManager
.
getLogger
(
KeYMatcher
.
class
);
private
static
final
Name
CUT_TACLET_NAME
=
new
Name
(
"cut"
);
private
ScriptApi
scrapi
;
private
KeyInterpreter
interpreter
;
private
List
<
MatchResult
>
resultsFromLabelMatch
;
public
KeYMatcher
(
ScriptApi
scrapi
,
KeyInterpreter
interpreter
)
{
this
.
scrapi
=
scrapi
;
this
.
interpreter
=
interpreter
;
@Getter
private
Services
services
;
public
KeYMatcher
(
Services
services
)
{
this
.
services
=
services
;
}
/**
...
...
@@ -162,75 +161,6 @@ public class KeYMatcher implements MatcherApi<KeyData> {
return
assignments
.
isEmpty
()?
null
:
assignments
;
}
/**
* Match against a sequent of a goal node
* @param currentState
* @param term
* @param signature
* @return
*/
//@Override
public
List
<
VariableAssignment
>
matchSeqKeY
(
GoalNode
<
KeyData
>
currentState
,
String
term
,
Signature
signature
)
{
VariableAssignment
interpreterAssignments
=
currentState
.
getAssignments
();
VariableAssignments
keyAssignments
=
new
VariableAssignments
(
null
);
interpreterAssignments
.
getTypes
().
forEach
((
k
,
v
)
->
keyAssignments
.
getTypeMap
().
put
(
k
.
getIdentifier
(),
interpreter
.
getTypeConversionBiMap
().
get
(
v
)));
interpreterAssignments
.
getValues
().
forEach
((
k
,
v
)
->
{
try
{
keyAssignments
.
addAssignment
(
k
.
getIdentifier
(),
v
);
}
catch
(
Exception
e
)
{
e
.
printStackTrace
();
}
});
Set
<
Map
.
Entry
<
Variable
,
Type
>>
sigEntrySet
=
signature
.
entrySet
();
sigEntrySet
.
forEach
(
e
->
{
try
{
keyAssignments
.
addType
(
e
.
getKey
().
getIdentifier
(),
interpreter
.
getTypeConversionBiMap
().
get
(
e
.
getValue
()));
}
catch
(
Exception
e1
)
{
e1
.
printStackTrace
();
}
});
// System.out.println("Matching: "+term.toString()+"\n================\n"+currentState.getData().getNode().sequent()+"\n================\n");
List
<
VariableAssignments
>
keyMatchResult
=
scrapi
.
matchPattern
(
term
,
currentState
.
getData
().
getNode
().
sequent
(),
keyAssignments
);
//empty keyassignments
// System.out.println("Matched " + keyMatchResult.size() + " goals from " + currentState.toString() + " with pattern " + term);
List
<
VariableAssignment
>
transformedMatchResults
=
new
ArrayList
<>();
for
(
VariableAssignments
mResult
:
keyMatchResult
)
{
transformedMatchResults
.
add
(
from
(
mResult
,
currentState
.
getData
()));
}
//keyMatchResult.forEach(r -> transformedMatchResults.add(from(r)));
return
transformedMatchResults
;
}
/**
* Transforms a KeY Variable Assignment into an assignment for the interpreter
*
* @param keyAssignments
* @param currentState
* @return
*/
public
VariableAssignment
from
(
VariableAssignments
keyAssignments
,
KeyData
currentState
)
{
VariableAssignment
interpreterAssignments
=
new
VariableAssignment
(
null
);
Map
<
String
,
VariableAssignments
.
VarType
>
keyTypeMap
=
keyAssignments
.
getTypeMap
();
keyTypeMap
.
entrySet
().
forEach
(
e
->
interpreterAssignments
.
declare
(
e
.
getKey
(),
interpreter
.
getTypeConversionBiMap
().
inverse
().
get
(
e
.
getValue
())));
keyTypeMap
.
keySet
().
forEach
(
k
->
{
try
{
interpreterAssignments
.
assign
(
k
,
toValueTerm
(
currentState
,
(
Term
)
keyAssignments
.
getVarValue
(
k
)));
//System.out.println(keyAssignments.getVarValue(k));
}
catch
(
Exception
e
)
{
e
.
printStackTrace
();
}
});
return
interpreterAssignments
;
}
private
Value
<
String
>
toValueTerm
(
KeyData
currentState
,
Term
matched
)
{
String
reprTerm
=
LogicPrinter
.
quickPrintTerm
(
matched
,
currentState
.
getEnv
().
getServices
());
...
...
@@ -241,11 +171,14 @@ public class KeYMatcher implements MatcherApi<KeyData> {
}
@Override
public
List
<
VariableAssignment
>
matchSeq
(
GoalNode
<
KeyData
>
currentState
,
String
data
,
Signature
sig
)
{
public
List
<
VariableAssignment
>
matchSeq
(
GoalNode
<
KeyData
>
currentState
,
String
data
,
Signature
sig
)
{
//System.out.println("State that will be matched " + currentState.getData().getNode().sequent() + " with pattern " + data);
//System.out.println("Signature " + sig.toString());
Matchings
m
=
MatcherFacade
.
matches
(
data
,
currentState
.
getData
().
getNode
().
sequent
(),
false
);
Matchings
m
=
MatcherFacade
.
matches
(
data
,
currentState
.
getData
().
getNode
().
sequent
(),
false
,
services
);
if
(
m
.
isEmpty
())
{
LOGGER
.
debug
(
"currentState has no match= "
+
currentState
.
getData
().
getNode
().
sequent
());
...
...
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/StepIntoReverseCommand.java
View file @
b36a3c1f
...
...
@@ -15,5 +15,6 @@ public class StepIntoReverseCommand<T> extends DebuggerCommand<T> {
info
(
"There is no previous state to the current one."
);
}
dbg
.
setStatePointer
(
stepBack
);
}
}
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/StepOverReverseCommand.java
View file @
b36a3c1f
package
edu.kit.iti.formal.psdbg.interpreter.dbg
;
import
lombok.val
;
public
class
StepOverReverseCommand
<
T
>
extends
DebuggerCommand
<
T
>
{
@Override
public
void
execute
(
DebuggerFramework
<
T
>
dbg
)
throws
DebuggerException
{
val
statePointer
=
dbg
.
getCurrentStatePointer
();
PTreeNode
<
T
>
stepOverReverse
=
statePointer
.
getStepInvInto
()
!=
null
?
statePointer
.
getStepInvInto
()
:
statePointer
.
getStepInvOver
();
if
(
stepOverReverse
==
null
)
{
info
(
"There is no previous state to the current one."
);