Commit 1c4e67af authored by Alexander Weigl's avatar Alexander Weigl

fix some test cases, clean up a little bit

parent 68ec6cce
......@@ -10,12 +10,12 @@ package edu.kit.iti.formal.psdbg.parser.ast;
* it under the terms of the GNU General Public License as
* published by the Free Software Foundation, either version 3 of the
* License, or (at your option) any later version.
*
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
*
* You should have received a copy of the GNU General Public
* License along with this program. If not, see
* <http://www.gnu.org/licenses/gpl-3.0.html>.
......@@ -25,12 +25,13 @@ package edu.kit.iti.formal.psdbg.parser.ast;
import edu.kit.iti.formal.psdbg.parser.Visitable;
import edu.kit.iti.formal.psdbg.parser.Visitor;
import lombok.EqualsAndHashCode;
import lombok.Getter;
import lombok.Setter;
import lombok.val;
import org.antlr.v4.runtime.ParserRuleContext;
import javax.annotation.Nullable;
import java.util.Arrays;
import java.util.Objects;
/**
......@@ -47,7 +48,9 @@ public abstract class ASTNode<T extends ParserRuleContext>
/**
*
*/
@Getter @Setter @Nullable
@Getter
@Setter
@Nullable
protected ASTNode parent;
/**
......@@ -116,7 +119,7 @@ public abstract class ASTNode<T extends ParserRuleContext>
@Override
public abstract ASTNode<T> copy();
public boolean isAncestor(ASTNode node){
public boolean isAncestor(ASTNode node) {
ASTNode n = this;
do {
if (n.equals(node))
......@@ -140,6 +143,17 @@ public abstract class ASTNode<T extends ParserRuleContext>
return depth;
}
public ASTNode[] getChildren() {
return new ASTNode[0];
}
public final ASTNode[] asList() {
val ary = getChildren();
val nry = Arrays.copyOf(ary, ary.length + 1);
nry[nry.length - 1] = this;
return nry;
}
@Override
public boolean equals(Object o) {
if (this == o) return true;
......
......@@ -10,12 +10,12 @@ package edu.kit.iti.formal.psdbg.parser.ast;
* it under the terms of the GNU General Public License as
* published by the Free Software Foundation, either version 3 of the
* License, or (at your option) any later version.
*
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
*
* You should have received a copy of the GNU General Public
* License along with this program. If not, see
* <http://www.gnu.org/licenses/gpl-3.0.html>.
......@@ -23,7 +23,6 @@ package edu.kit.iti.formal.psdbg.parser.ast;
*/
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;
......@@ -74,6 +73,10 @@ public class AssignmentStatement
return type != null;
}
@Override
public ASTNode[] getChildren() {
return new ASTNode[]{getLhs(), getRhs()};
}
@Override
public boolean eq(ASTNode o) {
......
......@@ -10,12 +10,12 @@ package edu.kit.iti.formal.psdbg.parser.ast;
* it under the terms of the GNU General Public License as
* published by the Free Software Foundation, either version 3 of the
* License, or (at your option) any later version.
*
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
*
* You should have received a copy of the GNU General Public
* License along with this program. If not, see
* <http://www.gnu.org/licenses/gpl-3.0.html>.
......@@ -47,6 +47,11 @@ public class BinaryExpression extends Expression<ParserRuleContext> {
this.right = right;
}
@Override
public ASTNode[] getChildren() {
return new ASTNode[]{getLeft(), getRight()};
}
@Override
public <T> T accept(Visitor<T> visitor) {
return visitor.visit(this);
......
......@@ -10,12 +10,12 @@ package edu.kit.iti.formal.psdbg.parser.ast;
* it under the terms of the GNU General Public License as
* published by the Free Software Foundation, either version 3 of the
* License, or (at your option) any later version.
*
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
*
* You should have received a copy of the GNU General Public
* License along with this program. If not, see
* <http://www.gnu.org/licenses/gpl-3.0.html>.
......@@ -23,7 +23,6 @@ package edu.kit.iti.formal.psdbg.parser.ast;
*/
import edu.kit.iti.formal.psdbg.parser.ScriptLanguageParser;
import edu.kit.iti.formal.psdbg.parser.Visitor;
import lombok.*;
......@@ -58,6 +57,11 @@ public class CallStatement extends Statement<ScriptLanguageParser.ScriptCommandC
return visitor.visit(this);
}
@Override
public ASTNode[] getChildren() {
return new ASTNode[]{getParameters()};
}
/**
* {@inheritDoc}
*/
......
......@@ -10,12 +10,12 @@ package edu.kit.iti.formal.psdbg.parser.ast;
* it under the terms of the GNU General Public License as
* published by the Free Software Foundation, either version 3 of the
* License, or (at your option) any later version.
*
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
*
* You should have received a copy of the GNU General Public
* License along with this program. If not, see
* <http://www.gnu.org/licenses/gpl-3.0.html>.
......@@ -44,14 +44,21 @@ public abstract class CaseStatement extends Statement<ScriptLanguageParser.Cases
/**
* {@inheritDoc}
*/
@Override public <T> T accept(Visitor<T> visitor) {
@Override
public <T> T accept(Visitor<T> visitor) {
return visitor.visit(this);
}
/**
* {@inheritDoc}
*/
@Override public abstract CaseStatement copy();
@Override
public abstract CaseStatement copy();
@Override
public ASTNode[] getChildren() {
return new ASTNode[]{getBody()};
}
@Override
public boolean equals(Object o) {
......@@ -63,5 +70,4 @@ public abstract class CaseStatement extends Statement<ScriptLanguageParser.Cases
return getBody().eq(that.getBody());
}
}
......@@ -10,12 +10,12 @@ package edu.kit.iti.formal.psdbg.parser.ast;
* it under the terms of the GNU General Public License as
* published by the Free Software Foundation, either version 3 of the
* License, or (at your option) any later version.
*
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
*
* You should have received a copy of the GNU General Public
* License along with this program. If not, see
* <http://www.gnu.org/licenses/gpl-3.0.html>.
......@@ -25,10 +25,7 @@ package edu.kit.iti.formal.psdbg.parser.ast;
import edu.kit.iti.formal.psdbg.parser.ScriptLanguageParser;
import edu.kit.iti.formal.psdbg.parser.Visitor;
import lombok.Getter;
import lombok.NonNull;
import lombok.RequiredArgsConstructor;
import lombok.Setter;
import lombok.*;
import java.util.ArrayList;
import java.util.List;
......@@ -41,22 +38,37 @@ import java.util.List;
@Getter
@RequiredArgsConstructor
public class CasesStatement extends Statement<ScriptLanguageParser.CasesStmtContext> {
@NonNull private final List<CaseStatement> cases = new ArrayList<>();
@NonNull
private final List<CaseStatement> cases = new ArrayList<>();
// @NonNull private Statements defaultCase = new Statements();
@NonNull
private DefaultCaseStatement defCaseStmt = new DefaultCaseStatement();
@Override
public ASTNode[] getChildren() {
if (defCaseStmt == null)
return (ASTNode[]) cases.toArray();
else {
val ret = new ASTNode[cases.size() + (defCaseStmt != null ? 1 : 0)];
System.arraycopy(cases.toArray(), 0, ret, 0, cases.size());
ret[ret.length - 1] = defCaseStmt;
return ret;
}
}
/**
* {@inheritDoc}
*/
@Override public <T> T accept(Visitor<T> visitor) {
@Override
public <T> T accept(Visitor<T> visitor) {
return visitor.visit(this);
}
/**
* {@inheritDoc}
*/
@Override public CasesStatement copy() {
@Override
public CasesStatement copy() {
CasesStatement c = new CasesStatement();
cases.forEach(caseStatement -> c.cases.add(caseStatement.copy()));
// if (defaultCase != null)
......@@ -76,7 +88,7 @@ public class CasesStatement extends Statement<ScriptLanguageParser.CasesStmtCont
CasesStatement that = (CasesStatement) o;
for (int i = 0; i < cases.size(); i++) {
if(!cases.get(i).eq(that.cases.get(i)))
if (!cases.get(i).eq(that.cases.get(i)))
return false;
}
......
......@@ -19,7 +19,7 @@ public class ClosesCase extends CaseStatement {
* A close subscript() {bodyscript} expression
*
* @param closesGuard the script that is exectued in order to determine whether goal would clos. This proof is pruned afterwards
* @param body the actual script that is then executed when closesscript was successful and pruned
* @param body the actual script that is then executed when closesscript was successful and pruned
*/
public ClosesCase(Statements closesGuard, Statements body) {
this.body = body;
......@@ -55,4 +55,9 @@ public class ClosesCase extends CaseStatement {
return getClosesGuard() != null ? getClosesGuard().eq(that.getClosesGuard()) : that.getClosesGuard() == null;
}
@Override
public ASTNode[] getChildren() {
return new ASTNode[]{getClosesGuard(), getBody()};
}
}
package edu.kit.iti.formal.psdbg.parser.ast;
/*-
* #%L
* ProofScriptParser
* %%
* Copyright (C) 2017 Application-oriented Formal Verification
* %%
* This program is free software: you can redistribute it and/or modify
* it under the terms of the GNU General Public License as
* published by the Free Software Foundation, either version 3 of the
* License, or (at your option) any later version.
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
* You should have received a copy of the GNU General Public
* License along with this program. If not, see
* <http://www.gnu.org/licenses/gpl-3.0.html>.
* #L%
*/
/*-
* #%L
* ProofScriptParser
* %%
* Copyright (C) 2017 Application-oriented Formal Verification
* %%
* This program is free software: you can redistribute it and/or modify
* it under the terms of the GNU General Public License as
* published by the Free Software Foundation, either version 3 of the
* License, or (at your option) any later version.
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
* You should have received a copy of the GNU General Public
* License along with this program. If not, see
* <http://www.gnu.org/licenses/gpl-3.0.html>.
* #L%
*/
import edu.kit.iti.formal.psdbg.parser.ScriptLanguageParser;
import lombok.*;
import org.antlr.v4.runtime.ParserRuleContext;
/**
* @author Alexander Weigl
......@@ -39,11 +38,13 @@ public abstract class ConditionalBlock
extends Statement<ScriptLanguageParser.ConditionalBlockContext> {
@Getter
@Setter
@NonNull protected Statements body = new Statements();
@NonNull
protected Statements body = new Statements();
@Getter
@Setter
@NonNull protected Expression condition = BooleanLiteral.TRUE;
@NonNull
protected Expression condition = BooleanLiteral.TRUE;
@Override
public boolean eq(ASTNode o) {
......@@ -56,4 +57,8 @@ public abstract class ConditionalBlock
return getBody() != null ? getBody().eq(that.getBody()) : that.getBody() == null;
}
@Override
public ASTNode[] getChildren() {
return new ASTNode[]{getCondition(), getBody()};
}
}
......@@ -8,7 +8,6 @@ import lombok.Setter;
@Getter
@Setter
public class DefaultCaseStatement extends Statement<ScriptLanguageParser.StmtListContext> {
protected Statements body;
public DefaultCaseStatement() {
......@@ -55,6 +54,12 @@ public class DefaultCaseStatement extends Statement<ScriptLanguageParser.StmtLis
result = 31 * result + getBody().hashCode();
return result;
}
@Override
public ASTNode[] getChildren() {
return new ASTNode[]{getBody()};
}
}
......
......@@ -10,12 +10,12 @@ package edu.kit.iti.formal.psdbg.parser.ast;
* it under the terms of the GNU General Public License as
* published by the Free Software Foundation, either version 3 of the
* License, or (at your option) any later version.
*
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
*
* You should have received a copy of the GNU General Public
* License along with this program. If not, see
* <http://www.gnu.org/licenses/gpl-3.0.html>.
......@@ -57,4 +57,8 @@ public class ForeachStatement extends UnconditionalBlock {
fs.setRuleContext(this.ruleContext);
return fs;
}
}
@Override
public ASTNode[] getChildren() {
return new ASTNode[]{getBody()};
}}
......@@ -48,4 +48,8 @@ public class GuardedCaseStatement extends CaseStatement {
return getGuard().eq(that.getGuard());
}
@Override
public ASTNode[] getChildren() {
return new ASTNode[]{getGuard(), getBody()};
}
}
......@@ -10,12 +10,12 @@ package edu.kit.iti.formal.psdbg.parser.ast;
* it under the terms of the GNU General Public License as
* published by the Free Software Foundation, either version 3 of the
* License, or (at your option) any later version.
*
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
*
* You should have received a copy of the GNU General Public
* License along with this program. If not, see
* <http://www.gnu.org/licenses/gpl-3.0.html>.
......@@ -30,8 +30,6 @@ 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 lombok.Data;
import lombok.Getter;
import lombok.Setter;
/**
* A match expression contains an argument and a uses clause.
......@@ -43,13 +41,15 @@ import lombok.Setter;
public class MatchExpression extends Expression<ScriptLanguageParser.MatchPatternContext> {
//private Signature signature = new Signature();
private Expression pattern;
@Getter
@Setter
private boolean isDerivable;
@Getter
@Setter
@Deprecated
private Expression derivableTerm;
@Override
public ASTNode[] getChildren() {
return new ASTNode[]{pattern};
}
/**
* {@inheritDoc}
*/
......@@ -95,8 +95,4 @@ public class MatchExpression extends Expression<ScriptLanguageParser.MatchPatter
public int getPrecedence() {
return Operator.MATCH.precedence();
}
public void setPattern(Expression pattern) {
this.pattern = pattern;
}
}
......@@ -10,12 +10,12 @@ package edu.kit.iti.formal.psdbg.parser.ast;
* it under the terms of the GNU General Public License as
* published by the Free Software Foundation, either version 3 of the
* License, or (at your option) any later version.
*
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
*
* You should have received a copy of the GNU General Public
* License along with this program. If not, see
* <http://www.gnu.org/licenses/gpl-3.0.html>.
......@@ -58,6 +58,10 @@ public class ProofScript extends ASTNode<ScriptLanguageParser.ScriptContext> {
return ps;
}
@Override
public ASTNode[] getChildren() {
return new ASTNode[]{getSignature(), getBody()};
}
@Override
public boolean eq(ASTNode o) {
......
......@@ -45,6 +45,10 @@ public class Statements extends ASTNode<ScriptLanguageParser.StmtListContext>
implements Visitable, Iterable<Statement> {
private final List<Statement> statements = new ArrayList<>();
@Override
public ASTNode[] getChildren() {
return (ASTNode[]) toArray();
}
public Statements(Statements body) {
statements.addAll(body.statements);
......
......@@ -46,9 +46,14 @@ public class SubstituteExpression extends Expression<ScriptLanguageParser.ExprSu
@Override
public Type getType(Signature signature) throws NotWelldefinedException {
Type t = sub.getType(signature);
if(!TypeFacade.isTerm(t)){
if (!TypeFacade.isTerm(t)) {
throw new NotWelldefinedException("Term<?> expected, got " + t.symbol(), this);
}
return TypeFacade.ANY_TERM;
}
@Override
public ASTNode[] getChildren() {
return new ASTNode[]{getSub()};
}
}
......@@ -59,4 +59,6 @@ public class TheOnlyStatement extends UnconditionalBlock {
tos.setRuleContext(this.ruleContext);
return tos;
}
}
......@@ -10,12 +10,12 @@ package edu.kit.iti.formal.psdbg.parser.ast;
* it under the terms of the GNU General Public License as
* published by the Free Software Foundation, either version 3 of the
* License, or (at your option) any later version.
*
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
*
* You should have received a copy of the GNU General Public
* License along with this program. If not, see
* <http://www.gnu.org/licenses/gpl-3.0.html>.
......@@ -23,7 +23,6 @@ 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;
......@@ -88,4 +87,10 @@ public class UnaryExpression extends Expression<ParserRuleContext> {
public int getPrecedence() {
return Operator.NOT.precedence();//a placeholder, because MINUS is used as binary operator,too
}
@Override
public ASTNode[] getChildren() {
return new ASTNode[]{getExpression()};
}
}
package edu.kit.iti.formal.psdbg.parser.ast;
/*-
* #%L
* ProofScriptParser
* %%
* Copyright (C) 2017 Application-oriented Formal Verification
* %%
* This program is free software: you can redistribute it and/or modify
* it under the terms of the GNU General Public License as
* published by the Free Software Foundation, either version 3 of the
* License, or (at your option) any later version.
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
* You should have received a copy of the GNU General Public
* License along with this program. If not, see
* <http://www.gnu.org/licenses/gpl-3.0.html>.
* #L%
*/
/*-
* #%L
* ProofScriptParser
* %%
* Copyright (C) 2017 Application-oriented Formal Verification
* %%
* This program is free software: you can redistribute it and/or modify
* it under the terms of the GNU General Public License as
* published by the Free Software Foundation, either version 3 of the
* License, or (at your option) any later version.
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
* You should have received a copy of the GNU General Public
* License along with this program. If not, see
* <http://www.gnu.org/licenses/gpl-3.0.html>.
* #L%
*/
import edu.kit.iti.formal.psdbg.parser.ScriptLanguageParser;
......@@ -38,7 +38,8 @@ public abstract class UnconditionalBlock
extends Statement<ScriptLanguageParser.UnconditionalBlockContext> {
@Getter
@Setter
@NonNull protected Statements body = new Statements();
@NonNull
protected Statements body = new Statements();
@Override
public boolean eq(ASTNode o) {
......@@ -51,4 +52,9 @@ public abstract class UnconditionalBlock
return getBody() != null ? getBody().eq(that.getBody()) : that.getBody() == null;
}
@Override
public ASTNode[] getChildren() {
return new ASTNode[]{getBody()};
}
}
......@@ -95,9 +95,9 @@ public class ValueInjector {
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));
valueInjector.addConverter(Term.class, termConverter);
return valueInjector;
}
......
......@@ -5,6 +5,7 @@ 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.SubstituteExpression;
......@@ -25,7 +26,7 @@ public class KeyEvaluator extends Evaluator<KeyData> {
private Sort asKeySort(Type symbol, Goal g) {
NamespaceSet global = g.proof().getServices().getNamespaces();
Sort s = global.sorts().lookup(symbol.interpreterSort());
if(s!=null)
if (s != null)
return s;
return g.getLocalNamespaces().sorts().lookup(symbol.interpreterSort());
}
......@@ -34,10 +35,10 @@ public class KeyEvaluator extends Evaluator<KeyData> {
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
TermValue data = (TermValue) term.getData();
Pattern pattern = Pattern.compile("\\?[a-zA-Z_]+");
String termstr = term.getData().toString();
String termstr = data.getTermRepr();
Matcher m = pattern.matcher(termstr);
StringBuffer newTerm = new StringBuffer();
while (m.find()) {
......@@ -49,11 +50,11 @@ public class KeyEvaluator extends Evaluator<KeyData> {
if (t != null)
newVal = ((Value) t.accept(this)).getData().toString();
else
// newVal = state.getValue(new Variable(name)).getData().toString();
m.appendReplacement(newTerm, newVal);
// newVal = state.getValue(new Variable(name)).getData().toString();