diff --git a/pom.xml b/pom.xml index 6aea3a2d2ff1e249c05a9edb5af066bf5f54f59a..9537130c3c1ffd43f71ee703366b90803beb22d4 100644 --- a/pom.xml +++ b/pom.xml @@ -97,41 +97,6 @@ true - diff --git a/src/main/java/edu/kit/formal/dbg/Debugger.java b/src/main/java/edu/kit/formal/dbg/Debugger.java index b4714f5284d91e3be108a195f5694ef9d068cefc..120ff7a6070d68dcea3f28a5ff6fac4b466bd162 100644 --- a/src/main/java/edu/kit/formal/dbg/Debugger.java +++ b/src/main/java/edu/kit/formal/dbg/Debugger.java @@ -45,7 +45,6 @@ public class Debugger { interpreter.getEntryListeners().add(history); interpreter.getEntryListeners().add(blocker); interpreter.getEntryListeners().add(new CommandLogger()); - //TODO install debugger functions registerDebuggerFunction("step", this::step); registerDebuggerFunction("b", this::setBreakpoint); @@ -56,6 +55,11 @@ public class Debugger { registerDebuggerFunction("status", this::status); } + public static void main(String[] args) throws IOException { + Debugger d = new Debugger("src/test/resources/edu/kit/formal/interpreter/dbg.kps"); + d.run(); + } + private void registerDebuggerFunction(final String step, BiConsumer func) { debuggerFunctions.getBuilders().add(new CommandHandler() { @@ -71,11 +75,6 @@ public class Debugger { }); } - public static void main(String[] args) throws IOException { - Debugger d = new Debugger("src/test/resources/edu/kit/formal/interpreter/dbg.kps"); - d.run(); - } - private void run() throws IOException { blocker.stepUntilBlock.set(2); interpreterThread = new Thread(() -> { diff --git a/src/main/java/edu/kit/formal/interpreter/Evaluator.java b/src/main/java/edu/kit/formal/interpreter/Evaluator.java index 9e0ed3e254248ca5b802b1dfd04277631452729d..f77cf2a63703e185a3ff3246ab5fb2be317c61e2 100644 --- a/src/main/java/edu/kit/formal/interpreter/Evaluator.java +++ b/src/main/java/edu/kit/formal/interpreter/Evaluator.java @@ -7,6 +7,7 @@ import lombok.Getter; import lombok.Setter; import java.util.ArrayList; +import java.util.Collections; import java.util.List; /** diff --git a/src/main/java/edu/kit/formal/interpreter/GoalNode.java b/src/main/java/edu/kit/formal/interpreter/GoalNode.java index 123c544f5fae635a6f9aaf2b318298b6ec006f46..8eb44b44199e26c7628dd4c8593da54e77855b19 100644 --- a/src/main/java/edu/kit/formal/interpreter/GoalNode.java +++ b/src/main/java/edu/kit/formal/interpreter/GoalNode.java @@ -10,21 +10,36 @@ import lombok.Getter; * @author S.Grebing */ public class GoalNode { - //TODO this is only for testing, later Sequent object or similar + @Getter - private String sequent; + private String sequent; //TODO this is only for testing, when connected with key using projectednode private VariableAssignment assignments; private GoalNode parent; + @Getter + private ProjectedNode actualKeYGoalNode; + /** + * This conctructur will be replaced with concrete one that uses projectedNode + * + * @param parent + * @param seq + */ public GoalNode(GoalNode parent, String seq) { //BUG: Hier muesste deepcopy der assignments passieren this.assignments = new VariableAssignment(parent == null ? null : parent.deepCopyAssignments()); this.parent = parent; this.sequent = seq; + actualKeYGoalNode = null; } + public GoalNode(GoalNode parent, String seq, ProjectedNode pNode) { + this.actualKeYGoalNode = pNode; + this.assignments = new VariableAssignment(parent == null ? null : parent.deepCopyAssignments()); + this.parent = parent; + this.sequent = seq; + } private VariableAssignment deepCopyAssignments() { return assignments.deepCopy(); } diff --git a/src/main/java/edu/kit/formal/interpreter/HistoryListener.java b/src/main/java/edu/kit/formal/interpreter/HistoryListener.java index f4379762cd507b87324df8767f8be6f23d7d1c84..08814f29a32193aa9966df3bb7d392b2b8e64aff 100644 --- a/src/main/java/edu/kit/formal/interpreter/HistoryListener.java +++ b/src/main/java/edu/kit/formal/interpreter/HistoryListener.java @@ -4,7 +4,6 @@ import edu.kit.formal.proofscriptparser.DefaultASTVisitor; import edu.kit.formal.proofscriptparser.ast.ASTNode; import lombok.Getter; import lombok.RequiredArgsConstructor; -import lombok.Setter; import java.util.LinkedList; import java.util.List; @@ -28,4 +27,6 @@ public class HistoryListener extends DefaultASTVisitor { queueNode.add(node); return null; } + + } diff --git a/src/main/java/edu/kit/formal/interpreter/Interpreter.java b/src/main/java/edu/kit/formal/interpreter/Interpreter.java index 9a9acbde4c6193bccdf674b02638b13b3b50dc0c..b6c5e515b3ff9c2d0da8b85c6f49830030ff4c5f 100644 --- a/src/main/java/edu/kit/formal/interpreter/Interpreter.java +++ b/src/main/java/edu/kit/formal/interpreter/Interpreter.java @@ -2,12 +2,14 @@ package edu.kit.formal.interpreter; import de.uka.ilkd.key.api.ScriptApi; import de.uka.ilkd.key.macros.scripts.EngineState; +import edu.kit.formal.interpreter.funchdl.CommandCall; import edu.kit.formal.interpreter.funchdl.CommandLookup; import edu.kit.formal.proofscriptparser.DefaultASTVisitor; import edu.kit.formal.proofscriptparser.Visitor; import edu.kit.formal.proofscriptparser.ast.*; import lombok.Getter; import lombok.Setter; +import org.antlr.v4.runtime.ParserRuleContext; import java.util.*; import java.util.logging.Logger; @@ -19,6 +21,7 @@ import java.util.logging.Logger; */ public class Interpreter extends DefaultASTVisitor implements ScopeObservable { + private static final int MAX_ITERATIONS = 5; //TODO later also include information about source line for each state (for debugging purposes and rewind purposes) private Stack stateStack = new Stack<>(); private static Logger logger = Logger.getLogger("interpreter"); @@ -160,77 +163,80 @@ public class Interpreter extends DefaultASTVisitor @Override public Void visit(CasesStatement casesStatement) { enterScope(casesStatement); + AbstractState beforeCases = stateStack.pop(); + + + List allGoalsBeforeCases = beforeCases.getGoals(); + + //global List after all Case Statements List goalsAfterCases = new ArrayList<>(); //copy the list of goal nodes for keeping track of goals - Set currentGoals = new HashSet<>(getCurrentGoals()); - //List> matchedGoals = new ArrayList<>(); + Set copiedList = new HashSet<>(allGoalsBeforeCases); + //handle cases + + List cases = casesStatement.getCases(); + for (CaseStatement aCase : cases) { + Map matchedGoals = matchGoal(copiedList, aCase); + if (matchedGoals != null) { + copiedList.removeAll(matchedGoals.entrySet()); + goalsAfterCases.addAll(executeCase(aCase.getBody(), matchedGoals.keySet())); + } - for (CaseStatement currentCase : casesStatement.getCases()) { - //calculate the goal nodes activations - Map mg = getMatchedGoal(currentGoals, currentCase); - //matchedGoals.add(mg); - currentGoals.removeAll(mg.keySet()); - // execute - for (Map.Entry s : mg.entrySet()) { - enterScope(currentCase); - executeStatements(currentCase.getBody(), s.getKey(), s.getValue()); - exitScope(currentCase); + } + +/* Iterator casesIter = cases.iterator(); + while (casesIter.hasNext()) { + + //get information for case + CaseStatement currentCase = casesIter.next(); + Expression guard = currentCase.getGuard(); + Statements body = currentCase.getBody(); + + + Iterator goalIter = copiedList.iterator(); + Set forCase = new HashSet<>(); + //iterate over all available goals and select those that evaluate to true with the guard + //assumption, matchpattern handles varAssignments + while (goalIter.hasNext()) { + GoalNode g = goalIter.next(); + Value eval = evaluate(g, guard); + if (eval.getData().equals(true)) { + forCase.add(g); + } } + copiedList.removeAll(forCase); + + goalsAfterCases.addAll(executeCase(body, forCase)); + } + */ + //for all remaining goals execute default + if (!copiedList.isEmpty()) { + Statements defaultCase = casesStatement.getDefaultCase(); + goalsAfterCases.addAll(executeCase(defaultCase, copiedList)); - // execute - for (GoalNode s : currentGoals) { - executeStatements(casesStatement.getDefaultCase(), s, new VariableAssignment()); } - /*/exit scope and create a new state using the union of all newly created goals + //exit scope and create a new state using the union of all newly created goals + State newStateAfterCases; if (!goalsAfterCases.isEmpty()) { - for (GoalNode goalAfterCases : goalsAfterCases) { - goalAfterCases.exitNewVarScope(); - } + goalsAfterCases.forEach(node -> node.exitNewVarScope()); + if (goalsAfterCases.size() == 1) { newStateAfterCases = new State(goalsAfterCases, goalsAfterCases.get(0)); } else { newStateAfterCases = new State(goalsAfterCases, null); } stateStack.push(newStateAfterCases); - }*/ + } exitScope(casesStatement); return null; } - public void executeStatements(Statements currentCase, GoalNode gn, VariableAssignment va) { - enterScope(currentCase); - AbstractState ns = newState(gn); - ns.getSelectedGoalNode().enterNewVarScope(va); - currentCase.accept(this); - mergeGoalsAndPop(ns, gn); - exitScope(currentCase); - } - - private void mergeGoalsAndPop(AbstractState ns, GoalNode toRemoved) { - AbstractState popped = popState(); - assert popped == ns; - getCurrentState().getGoals().remove(toRemoved); - getCurrentState().getGoals().addAll(popped.getGoals()); - } - - - private Map getMatchedGoal(Collection currentGoals, - CaseStatement currentCase) { - Map map = new HashMap<>(); - for (GoalNode gn : currentGoals) { - VariableAssignment va = evaluateWithAssignments(gn, currentCase.getGuard()); - if (va != null) - map.put(gn, va); - } - return map; - } - /** * @param caseStatement @@ -325,8 +331,10 @@ public class Interpreter extends DefaultASTVisitor @Override public Void visit(RepeatStatement repeatStatement) { enterScope(repeatStatement); + int counter = 0; boolean b = false; do { + counter++; AbstractState prev = getCurrentState(); repeatStatement.getBody().accept(this); AbstractState end = getCurrentState(); @@ -334,6 +342,7 @@ public class Interpreter extends DefaultASTVisitor Set prevNodes = new HashSet<>(prev.getGoals()); Set endNodes = new HashSet<>(end.getGoals()); b = prevNodes.equals(endNodes); + b = b && counter <= MAX_ITERATIONS; } while (b); exitScope(repeatStatement); return null; @@ -363,6 +372,12 @@ public class Interpreter extends DefaultASTVisitor return getCurrentGoals().get(0); } } + /* @Override + public T visit(Parameters parameters) { + parameters.entrySet(); + System.out.println("Params " + parameters.toString()); + return null; + }*/ public AbstractState getCurrentState() { return stateStack.peek(); diff --git a/src/main/java/edu/kit/formal/interpreter/VariableAssignment.java b/src/main/java/edu/kit/formal/interpreter/VariableAssignment.java index bacb537d29357ec455d7a96d5cd7b47c8e38cc58..7fbbe52d409dc8045a8d910e21462bf0e6c87b5a 100644 --- a/src/main/java/edu/kit/formal/interpreter/VariableAssignment.java +++ b/src/main/java/edu/kit/formal/interpreter/VariableAssignment.java @@ -3,7 +3,10 @@ package edu.kit.formal.interpreter; import edu.kit.formal.proofscriptparser.ast.Type; import java.util.HashMap; +import java.util.HashSet; import java.util.Map; +import java.util.Set; +import java.util.stream.Collectors; /** * Variable Assignments for each goal node @@ -143,10 +146,43 @@ public class VariableAssignment { return asMap(new HashMap<>()); } - public VariableAssignment push(VariableAssignment va) { - VariableAssignment p = push(); - p.values.putAll(va.values); - p.types.putAll(va.types); - return p; + /** + * Method joins two variable assignments without checking their compatibility + * + * @param assignment + * @return + */ + public VariableAssignment joinWithoutCheck(VariableAssignment assignment) { + this.getValues().putAll(assignment.getValues()); + this.getTypes().putAll(assignment.getTypes()); + return this; + } + + /** + * @param assignment + * @return empty variable assignment if not possible to join conflictfree (i.e., if a variable name is present in both assignments with different types or dfferent values) + * @throws RuntimeException + */ + public VariableAssignment joinWithCheck(VariableAssignment assignment) throws RuntimeException { + + Set namesV2 = assignment.getValues().keySet(); + Set nonConflicting = new HashSet<>(); + Set conflictingCand = new HashSet<>(); + + //subtract V2 from V1 and add the nonconflicting varNames into the nonconflicting set + nonConflicting = this.getValues().keySet().stream().filter(item -> !namesV2.contains(item)).collect(Collectors.toSet()); + //subtract V1 from V2 and add the nonconflicting varNames into the nonconflicting set + nonConflicting.addAll(namesV2.stream().filter(item -> !this.getValues().keySet().contains(item)).collect(Collectors.toSet())); + //create intersection + conflictingCand = this.getValues().keySet().stream().filter(item -> namesV2.contains(item)).collect(Collectors.toSet()); + if (!conflictingCand.isEmpty()) { + for (String s : conflictingCand) { + if (!this.lookupVarValue(s).equals(assignment.lookupVarValue(s))) { + return new VariableAssignment(null); + } + } + } + + return this.joinWithoutCheck(assignment); } } diff --git a/src/main/java/edu/kit/formal/proofscriptparser/ast/BinaryExpression.java b/src/main/java/edu/kit/formal/proofscriptparser/ast/BinaryExpression.java index 6a26a5785e76455faaf25c4d99d4603297645fb6..a4968cfb55f2dfbf6d48d4e9f63f3bd5d9ce8fcb 100644 --- a/src/main/java/edu/kit/formal/proofscriptparser/ast/BinaryExpression.java +++ b/src/main/java/edu/kit/formal/proofscriptparser/ast/BinaryExpression.java @@ -75,6 +75,11 @@ public class BinaryExpression extends Expression { return operator.returnType(); } + @Override + public boolean hasMatchExpression() { + return left.hasMatchExpression() || right.hasMatchExpression(); + } + /** * {@inheritDoc} */ diff --git a/src/main/java/edu/kit/formal/proofscriptparser/ast/BooleanLiteral.java b/src/main/java/edu/kit/formal/proofscriptparser/ast/BooleanLiteral.java index 06a6908fd70beb8f4f458178cb68955341719264..b1bd3fea0783b4fb48f5f46c4ce10069ea6b8af8 100644 --- a/src/main/java/edu/kit/formal/proofscriptparser/ast/BooleanLiteral.java +++ b/src/main/java/edu/kit/formal/proofscriptparser/ast/BooleanLiteral.java @@ -65,6 +65,11 @@ public class BooleanLiteral extends Literal { return visitor.visit(this); } + @Override + public boolean hasMatchExpression() { + return false; + } + /** * {@inheritDoc} */ diff --git a/src/main/java/edu/kit/formal/proofscriptparser/ast/Expression.java b/src/main/java/edu/kit/formal/proofscriptparser/ast/Expression.java index cf4100ae82d512fcdfa1c4b873eec5b0f5ac3d2c..f559e4720c474faea2d4bb19b8a3bfd2eb9135e2 100644 --- a/src/main/java/edu/kit/formal/proofscriptparser/ast/Expression.java +++ b/src/main/java/edu/kit/formal/proofscriptparser/ast/Expression.java @@ -34,6 +34,24 @@ import org.antlr.v4.runtime.ParserRuleContext; * @version 1 (28.04.17) */ public abstract class Expression extends ASTNode { + /** + * @param type + * @param e + * @param signature + * @throws NotWelldefinedException + */ + public static final void checkType(Type type, Expression e, Signature signature) throws NotWelldefinedException { + Type got = e.getType(signature); + if (!type.equals(got)) { + throw new NotWelldefinedException("Typemismatch in expected " + type + ", got" + got, e); + } + } + + /** + * @return returns true if a child expression contains a match expression + */ + public abstract boolean hasMatchExpression(); + /** * Returns the precedence of the operator expression. *

@@ -54,17 +72,4 @@ public abstract class Expression extends ASTNode */ public abstract Type getType(Signature signature) throws NotWelldefinedException; - - /** - * @param type - * @param e - * @param signature - * @throws NotWelldefinedException - */ - public static final void checkType(Type type, Expression e, Signature signature) throws NotWelldefinedException { - Type got = e.getType(signature); - if (!type.equals(got)) { - throw new NotWelldefinedException("Typemismatch in expected " + type + ", got" + got, e); - } - } } diff --git a/src/main/java/edu/kit/formal/proofscriptparser/ast/IntegerLiteral.java b/src/main/java/edu/kit/formal/proofscriptparser/ast/IntegerLiteral.java index 313ce630815117b2afa1059bc683e9cc5d3d48d5..1edb994f4fcc68402c6021096f74e4eba0abc920 100644 --- a/src/main/java/edu/kit/formal/proofscriptparser/ast/IntegerLiteral.java +++ b/src/main/java/edu/kit/formal/proofscriptparser/ast/IntegerLiteral.java @@ -59,6 +59,11 @@ public class IntegerLiteral extends Literal { return visitor.visit(this); } + @Override + public boolean hasMatchExpression() { + return false; + } + /** * {@inheritDoc} */ diff --git a/src/main/java/edu/kit/formal/proofscriptparser/ast/MatchExpression.java b/src/main/java/edu/kit/formal/proofscriptparser/ast/MatchExpression.java index a0bd68847bcf62adb139cd644a61680680357b42..1a0e6b31fb99563f2158749e79559d91eae235f1 100644 --- a/src/main/java/edu/kit/formal/proofscriptparser/ast/MatchExpression.java +++ b/src/main/java/edu/kit/formal/proofscriptparser/ast/MatchExpression.java @@ -76,6 +76,11 @@ public class MatchExpression extends Expression { return operator.returnType(); } + @Override + public boolean hasMatchExpression() { + return expression.hasMatchExpression(); + } + /** * {@inheritDoc */ diff --git a/src/main/java/edu/kit/formal/proofscriptparser/ast/Variable.java b/src/main/java/edu/kit/formal/proofscriptparser/ast/Variable.java index 3acdf31085ddbc0dfb46406ac3ffb043d3871543..981af8d8650e9b4c2814e6f1625661f5abf57b07 100644 --- a/src/main/java/edu/kit/formal/proofscriptparser/ast/Variable.java +++ b/src/main/java/edu/kit/formal/proofscriptparser/ast/Variable.java @@ -52,6 +52,11 @@ public class Variable extends Literal { return visitor.visit(this); } + @Override + public boolean hasMatchExpression() { + return false; + } + @Override public Variable copy() { Variable v = new Variable(identifier);