Commit 7c42f49c authored by LULUDBR\Lulu's avatar LULUDBR\Lulu

Merge remote-tracking branch 'origin/master'

parents 7933e262 c467d761
......@@ -2,3 +2,6 @@ target/
*.iml
.idea
website/site/
*/build/
*/out/
.gradle
......@@ -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
......
......@@ -26,7 +26,9 @@ package edu.kit.iti.formal.psdbg.parser;
import edu.kit.iti.formal.psdbg.parser.ast.*;
import edu.kit.iti.formal.psdbg.parser.types.Type;
import java.util.Map;
import java.util.*;
import java.util.stream.Collectors;
import java.util.stream.Stream;
/**
* {@link ASTTraversal} provides a visitor with a a default traversal of the given AST.
......@@ -35,6 +37,41 @@ import java.util.Map;
* @version 1 (29.04.17)
*/
public interface ASTTraversal<T> extends Visitor<T> {
default Stream<T> allOf(Stream<ASTNode> nodes) {
return nodes.map(n -> (T) n.accept(this));
}
default List<T> allOf(Collection<ASTNode> nodes) {
if (nodes.size() == 0) return Collections.emptyList();
return allOf(nodes.stream()).collect(Collectors.toList());
}
default Stream<T> allOf(ASTNode... nodes) {
if (nodes.length == 0) return (Stream<T>) Collections.emptyList().stream();
return allOf(Arrays.stream(nodes));
}
default T oneOf(Stream<? extends ASTNode> nodes) {
return (T) nodes
.filter(Objects::nonNull)
.map(n -> (T) n.accept(this))
.filter(Objects::nonNull)
.findFirst()
.orElse((T) null);
}
default T oneOf(ASTNode... nodes) {
if (nodes.length == 0) return null;
return oneOf(Arrays.stream(nodes));
}
default T oneOf(Collection<ASTNode> nodes) {
if (nodes.size() == 0) return null;
return oneOf(nodes.stream());
}
@Override
default T visit(ProofScript proofScript) {
proofScript.getSignature().accept(this);
......@@ -226,4 +263,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;
}
}
......@@ -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);
}
}
......@@ -197,7 +197,7 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
@Override
public Void visit(TermLiteral termLiteral) {
String termLit = termLiteral.getText();
String termLit = termLiteral.getContent();
if (termLit.contains("\n")) {
termLit = termLit.trim();
}
......
......@@ -121,12 +121,12 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
@Override
public Signature visitArgList(ScriptLanguageParser.ArgListContext ctx) {
Signature signature = new Signature();
signature.setRuleContext(ctx);
for (ScriptLanguageParser.VarDeclContext decl : ctx.varDecl()) {
Variable key = new Variable(decl.name);
key.setParent(signature);
signature.put(key, TypeFacade.findType(decl.type.getText()));
}
signature.setRuleContext(ctx);
return signature;
}
......@@ -148,6 +148,7 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
@Override
public Statements visitStmtList(ScriptLanguageParser.StmtListContext ctx) {
Statements statements = new Statements();
statements.setRuleContext(ctx);
for (ScriptLanguageParser.StatementContext stmt : ctx.statement()) {
Statement<ParserRuleContext> statement = (Statement<ParserRuleContext>) stmt.accept(this);
statement.setParent(statements);
......@@ -244,6 +245,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);
......@@ -325,7 +334,7 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
@Override
public Object visitLiteralTerm(ScriptLanguageParser.LiteralTermContext ctx) {
return new TermLiteral(ctx.getText());
return new TermLiteral(ctx.TERM_LITERAL().getSymbol());
}
@Override
......
......@@ -90,4 +90,5 @@ public interface Visitor<T> {
T visit(RelaxBlock relaxBlock);
T visit(NamespaceSetExpression nss);
}
......@@ -81,8 +81,8 @@ public abstract class ASTNode<T extends ParserRuleContext>
}
public void setRuleContext(T c) {
startPosition = Position.from(c.getStart());
endPosition = Position.from(c.getStop());
startPosition = Position.start(c);
endPosition = Position.end(c);
ruleContext = c;
}
......
......@@ -51,7 +51,7 @@ public class BooleanLiteral extends Literal {
public BooleanLiteral(boolean value, Token token) {
this.value = value;
this.token = token;
setToken(token);
}
BooleanLiteral(boolean b) {
......@@ -76,7 +76,7 @@ public class BooleanLiteral extends Literal {
*/
@Override
public BooleanLiteral copy() {
return new BooleanLiteral(value, token);
return new BooleanLiteral(value, getToken());
}
/**
......
......@@ -71,7 +71,7 @@ public class IntegerLiteral extends Literal {
*/
@Override public IntegerLiteral copy() {
IntegerLiteral il = new IntegerLiteral(value);
il.token = token;
il.setToken(getToken());
return il;
}
......
......@@ -23,7 +23,6 @@ package edu.kit.iti.formal.psdbg.parser.ast;
*/
import lombok.Getter;
import lombok.Setter;
import org.antlr.v4.runtime.ParserRuleContext;
......@@ -38,7 +37,15 @@ import java.util.Optional;
public abstract class Literal extends Expression<ParserRuleContext> {
@Getter
@Setter
protected Token token;
private Token token;
public void setToken(Token token) {
this.token = token;
if (token != null) {
startPosition = Position.start(token);
endPosition = Position.end(token);
}
}
/**
* {@inheritDoc}
......
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);
}
}
......@@ -23,26 +23,51 @@ package edu.kit.iti.formal.psdbg.parser.ast;
*/
import lombok.*;
import lombok.Data;
import lombok.RequiredArgsConstructor;
import lombok.Value;
import org.antlr.v4.runtime.ParserRuleContext;
import org.antlr.v4.runtime.Token;
/**
* @author Alexander Weigl
*/
@Data @Value @RequiredArgsConstructor public class Position implements Copyable<Position> {
@Data
@Value
@RequiredArgsConstructor
public class Position implements Copyable<Position> {
private final int offset;
private final int lineNumber;
private final int charInLine;
public Position() {
this(-1, -1);
this(-1, -1, -1);
}
public static Position start(Token token) {
return new Position(
token.getStartIndex(),
token.getLine(),
token.getCharPositionInLine());
}
public static Position end(Token token) {
return new Position(
token.getStopIndex(),
token.getLine(),
token.getCharPositionInLine());
}
public static Position start(ParserRuleContext token) {
return start(token.start);
}
@Override public Position copy() {
return new Position(lineNumber, charInLine);
public static Position end(ParserRuleContext token) {
return end(token.stop);
}
public static Position from(Token token) {
return new Position(token.getLine(), token.getCharPositionInLine());
@Override
public Position copy() {
return new Position(offset, lineNumber, charInLine);
}
}
......@@ -23,12 +23,12 @@ package edu.kit.iti.formal.psdbg.parser.ast;
*/
import edu.kit.iti.formal.psdbg.parser.NotWelldefinedException;
import edu.kit.iti.formal.psdbg.parser.Visitor;
import edu.kit.iti.formal.psdbg.parser.types.Type;
import edu.kit.iti.formal.psdbg.parser.types.TypeFacade;
import lombok.Data;
import org.antlr.v4.runtime.Token;
/**
* @author Alexander Weigl
......@@ -36,16 +36,27 @@ import lombok.Data;
*/
@Data
public class TermLiteral extends Literal {
private final String text;
private final String content;
public TermLiteral(String text) {
public TermLiteral(Token token) {
setToken(token);
String text = token.getText();
if (text.charAt(0) == '`')
text = text.substring(1);
if (text.charAt(text.length() - 1) == '`') //remove last backtick
text = text.substring(0, text.length() - 1);
if (text.charAt(0) == '`')
text = text.substring(0, text.length() - 2);
this.text = text;
content = text;
}
private TermLiteral(String sfTerm) {
content = sfTerm;
}
public static TermLiteral from(String sfTerm) {
TermLiteral tl = new TermLiteral(sfTerm);
return tl;
}
/**
......@@ -67,7 +78,7 @@ public class TermLiteral extends Literal {
@Override
public TermLiteral copy() {
return new TermLiteral(text);
return new TermLiteral(getToken());
}
/**
......@@ -77,5 +88,4 @@ public class TermLiteral extends Literal {
public Type getType(Signature signature) throws NotWelldefinedException {
return TypeFacade.ANY_TERM;
}
}
......@@ -61,7 +61,7 @@ public class Variable extends Literal implements Comparable<Variable> {
@Override
public Variable copy() {
Variable v = new Variable(identifier);
v.token = token;
v.setToken(getToken());
return v;
}
......
......@@ -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;
......@@ -56,7 +57,7 @@ public class Value<T> {
}
public static Value<String> from(TermLiteral term) {
return new Value<>(TypeFacade.ANY_TERM, term.getText());
return new Value<>(TypeFacade.ANY_TERM, term.getContent());
}
@Override
......
......@@ -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;
}
}
......@@ -29,4 +29,8 @@ public class TermType implements Type {
+ ">";
}
@Override
public String interpreterSort() {
return argTypes.get(0).interpreterSort();
}
}
......@@ -6,4 +6,5 @@ package edu.kit.iti.formal.psdbg.parser.types;
*/
public interface Type {
String symbol();
String interpreterSort();
}
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());
QuantifiableVariable gf;
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;
return g.getLocalNamespaces().sorts().lookup(symbol.interpreterSort());
}
@Override
public Value visit(SubstituteExpression expr) {
Value term = (Value) expr.getSub().accept(this);
if (term.getType() instanceof TermType) {
TermType tt = (TermType) term.getData();
//TODO better and new
Pattern pattern = Pattern.compile("\\?[a-zA-Z_]+");
String termstr = term.getData().toString();
Matcher m = pattern.matcher(termstr);
StringBuffer newTerm = new StringBuffer();
while (m.find()) {
String name = m.group().substring(1); // remove trailing '?'
Expression t = expr.getSubstitution().get(m.group());
//either evalute the substitent or find ?X in the
String newVal = "";
if (t != null)
newVal = ((Value) t.accept(this)).getData().toString();
else
// newVal = state.getValue(new Variable(name)).getData().toString();
m.appendReplacement(newTerm, newVal);
}
m.appendTail(newTerm);
return new Value<>(TypeFacade.ANY_TERM, newTerm.toString());
} else {
throw new IllegalStateException("Try to apply substitute on a non-term value.");
}
}
}
package edu.kit.iti.formal.psdbg.interpreter;
import com.google.common.collect.BiMap;
import com.google.common.collect.HashBiMap;
import com.google.common.collect.ImmutableBiMap;
import de.uka.ilkd.key.api.VariableAssignments;
import de.uka.ilkd.key.logic.sort.Sort;
import de.uka.ilkd.key.proof.Node;
import de.uka.ilkd.key.proof.Proof;
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.State;
import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
import edu.kit.iti.formal.psdbg.interpreter.data.*;
import edu.kit.iti.formal.psdbg.interpreter.funchdl.CommandLookup;
import edu.kit.iti.formal.psdbg.parser.Visitor;
import edu.kit.iti.formal.psdbg.parser.ast.ClosesCase;
import edu.kit.iti.formal.psdbg.parser.ast.Statements;
import edu.kit.iti.formal.psdbg.parser.ast.TermLiteral;
import edu.kit.iti.formal.psdbg.parser.ast.TryCase;
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 lombok.Getter;
import lombok.val;
import java.util.List;
import java.util.function.Function;
/**
* @author Alexander Weigl
......@@ -27,15 +33,17 @@ public class KeyInterpreter extends Interpreter<KeyData> {
@Getter
private static final BiMap<SimpleType, VariableAssignments.VarType> typeConversionBiMap =
new ImmutableBiMap.Builder<SimpleType, VariableAssignments.VarType>()
.put(SimpleType.ANY, VariableAssignments.VarType.ANY)
// .put(SimpleType.ANY, VariableAssignments.VarType.ANY)
.put(SimpleType.BOOL, VariableAssignments.VarType.BOOL)
//.put(SimpleType.TERM, VariableAssignments.VarType.FORMULA) //TODO: parametrisierte Terms
.put(SimpleType.INT, VariableAssignments.VarType.INT)
.put(SimpleType.STRING, VariableAssignments.VarType.OBJECT)
.put(SimpleType.INT_ARRAY, VariableAssignments.VarType.INT_ARRAY)
.put(SimpleType.SEQ, VariableAssignments.VarType.SEQ)
// .put(SimpleType.INT_ARRAY, VariableAssignments.VarType.INT_ARRAY)
// .put(SimpleType.SEQ, VariableAssignments.VarType.SEQ)
.build();
public KeyInterpreter(CommandLookup lookup) {
super(lookup);
}
......@@ -126,4 +134,17 @@ public class KeyInterpreter extends Interpreter<KeyData> {
entryListeners = backupEntryListener;
}
}
@Override
protected Evaluator<KeyData> createEvaluator(VariableAssignment assignments, GoalNode<KeyData> g) {
KeyEvaluator eval = new KeyEvaluator(assignments, g);
eval.setMatcher(getMatcherApi());
eval.setTermValueFactory(new Function<TermLiteral, Value>() {
@Override
public Value apply(TermLiteral termLiteral) {
return new Value(TypeFacade.ANY_TERM, new TermValue(termLiteral.getContent()));
}
});
return eval;
}
}