From 985b0a8b67b6b1c9884d1bb8820147ea9bad67bd Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sun, 21 May 2017 20:24:49 +0200 Subject: [PATCH] simplifcations and fixes --- .../java/edu/kit/formal/dbg/Debugger.java | 199 +++++++----------- .../formal/interpreter/Evaluator.java.orig | 123 ----------- .../formal/interpreter/HistoryListener.java | 1 + .../interpreter/InterpreterBuilder.java | 85 ++++++-- .../funchdl/MacroCommandHandler.java | 3 +- .../funchdl/ProofScriptCommandBuilder.java | 9 +- 6 files changed, 156 insertions(+), 264 deletions(-) delete mode 100644 src/main/java/edu/kit/formal/interpreter/Evaluator.java.orig diff --git a/src/main/java/edu/kit/formal/dbg/Debugger.java b/src/main/java/edu/kit/formal/dbg/Debugger.java index 9e2a6021..c14e7496 100644 --- a/src/main/java/edu/kit/formal/dbg/Debugger.java +++ b/src/main/java/edu/kit/formal/dbg/Debugger.java @@ -2,6 +2,7 @@ package edu.kit.formal.dbg; import edu.kit.formal.interpreter.*; import edu.kit.formal.interpreter.funchdl.BuiltinCommands; +import edu.kit.formal.interpreter.funchdl.CommandHandler; import edu.kit.formal.interpreter.funchdl.DefaultLookup; import edu.kit.formal.proofscriptparser.*; import edu.kit.formal.proofscriptparser.ast.*; @@ -10,6 +11,7 @@ import org.antlr.v4.runtime.CharStreams; import java.io.*; import java.math.BigInteger; import java.util.List; +import java.util.function.BiConsumer; /** * @author Alexander Weigl @@ -36,14 +38,28 @@ public class Debugger { interpreter.getEntryListeners().add(new CommandLogger()); //TODO install debugger functions - debuggerFunctions.getBuilders().add(new Step()); - debuggerFunctions.getBuilders().add(new Printer()); - debuggerFunctions.getBuilders().add(new ChgSel()); - debuggerFunctions.getBuilders().add(new Start()); - debuggerFunctions.getBuilders().add(new Pause()); - debuggerFunctions.getBuilders().add(new BrkPnt()); - debuggerFunctions.getBuilders().add(new Status()); + registerDebuggerFunction("step", this::step); + registerDebuggerFunction("b", this::setBreakpoint); + registerDebuggerFunction("start", this::start); + registerDebuggerFunction("pause", this::pause); + registerDebuggerFunction("chgsel", this::changeSelected); + registerDebuggerFunction("psel", this::psel); + registerDebuggerFunction("status", this::status); + } + + private void registerDebuggerFunction(final String step, + BiConsumer func) { + debuggerFunctions.getBuilders().add(new CommandHandler() { + @Override + public boolean handles(CallStatement call) throws IllegalArgumentException { + return step.equals(call.getCommand()); + } + @Override + public void evaluate(Interpreter i, CallStatement call, VariableAssignment params) { + func.accept(call, params); + } + }); } public static void main(String[] args) throws IOException { @@ -64,11 +80,11 @@ public class Debugger { while (true) { System.out.printf("dbg (%03d)> ", ++counter); String input = br.readLine(); - execuate(input); + execute(input); } } - private void execuate(String input) { + private void execute(String input) { input = input.trim(); if (input.isEmpty()) { return; @@ -90,140 +106,83 @@ public class Debugger { } - private class Step implements edu.kit.formal.interpreter.funchdl.CommandHandler { - @Override - public boolean handles(CallStatement call) throws IllegalArgumentException { - return call.getCommand().equals("step"); - } - - @Override - public void evaluate(Interpreter interpreter, CallStatement call, VariableAssignment params) { - IntegerLiteral il = (IntegerLiteral) call.getParameters().get(new Variable("#1")); - int steps = 1; - if (il != null) - steps = il.getValue().intValue(); - blocker.stepUntilBlock.set(steps * 2); //FIXME times two is strange, something wrong on sync - //LockSupport.unpark(interpreterThread); - blocker.unlock(); - } + public void step(CallStatement call, VariableAssignment params) { + IntegerLiteral il = (IntegerLiteral) call.getParameters().get(new Variable("#1")); + int steps = 1; + if (il != null) + steps = il.getValue().intValue(); + blocker.stepUntilBlock.set(steps * 2); //FIXME times two is strange, something wrong on sync + //LockSupport.unpark(interpreterThread); + blocker.unlock(); } - private class Printer implements edu.kit.formal.interpreter.funchdl.CommandHandler { - @Override - public boolean handles(CallStatement call) throws IllegalArgumentException { - return call.getCommand().equals("psel"); + public void psel(CallStatement call, VariableAssignment params) { + AbstractState state = interpreter.getCurrentState(); + int i = 0; + GoalNode sel; + try { + sel = state.getSelectedGoalNode(); + } catch (IllegalStateException e) { + sel = null; } - @Override - public void evaluate(Interpreter interpreter, CallStatement call, VariableAssignment params) { - AbstractState state = interpreter.getCurrentState(); - int i = 0; - GoalNode sel; - try { - sel = state.getSelectedGoalNode(); - } catch (IllegalStateException e) { - sel = null; - } - - for (GoalNode g : state.getGoals()) { - System.out.printf("%2d %s %s\n %s\n", - i++, - g == sel ? "*" : " ", - g.getSequent(), - g.getAssignments().asMap()); - } + for (GoalNode g : state.getGoals()) { + System.out.printf("%2d %s %s\n %s\n", + i++, + g == sel ? "*" : " ", + g.getSequent(), + g.getAssignments().asMap()); } } - - private class Start implements edu.kit.formal.interpreter.funchdl.CommandHandler { - @Override - public boolean handles(CallStatement call) throws IllegalArgumentException { - return call.getCommand().equals("start"); - } - - @Override - public void evaluate(Interpreter interpreter, CallStatement call, VariableAssignment params) { - interpreterThread.start(); - } + public void start(CallStatement call, VariableAssignment params) { + interpreterThread.start(); } - private class Pause implements edu.kit.formal.interpreter.funchdl.CommandHandler { - @Override - public boolean handles(CallStatement call) throws IllegalArgumentException { - return call.getCommand().equals("pause"); - } - - @Override - public void evaluate(Interpreter interpreter, CallStatement call, VariableAssignment params) { - blocker.stepUntilBlock.set(1); // block at next statement - } + public void pause(CallStatement call, VariableAssignment params) { + blocker.stepUntilBlock.set(1); // block at next statement } - private class BrkPnt implements edu.kit.formal.interpreter.funchdl.CommandHandler { - @Override - public boolean handles(CallStatement call) throws IllegalArgumentException { - return call.getCommand().equals("b"); - } - - @Override - public void evaluate(Interpreter interpreter, CallStatement call, VariableAssignment params) { - IntegerLiteral il = (IntegerLiteral) call.getParameters().get(new Variable("#1")); - blocker.addBreakpoint(il.getValue().intValue()); + public void setBreakpoint(CallStatement call, VariableAssignment params) { + IntegerLiteral il = (IntegerLiteral) call.getParameters().get(new Variable("#1")); + blocker.addBreakpoint(il.getValue().intValue()); - System.out.println("brkpnts: " + blocker.brkpnts); + System.out.println("brkpnts: " + blocker.brkpnts); - } } - - private class Status implements edu.kit.formal.interpreter.funchdl.CommandHandler { - @Override - public boolean handles(CallStatement call) throws IllegalArgumentException { - return call.getCommand().equals("status"); - } - - @Override - public void evaluate(Interpreter interpreter, CallStatement call, VariableAssignment params) { - System.out.format("name: %s, p: %s, state: %s, alive:%s, daemon:%s, interrupted:%s %n", - interpreterThread.getName(), - interpreterThread.getPriority(), - interpreterThread.getState(), - interpreterThread.isAlive(), - interpreterThread.isDaemon(), - interpreterThread.isInterrupted()); - - List nodes = history.getQueueNode(); - List states = history.getQueueState(); - CommandLogger cmd = new CommandLogger(); - for (int i = 0; i < nodes.size(); i++) { - ASTNode node = nodes.get(i); - node.accept(cmd); - // System.out.format("\t\t\t>>> %d states: [%s]%n", states.get(i).getGoals().size(), - // states.get(i).getSelectedGoalNode().getAssignments().asMap()); - } + public void status(CallStatement call, VariableAssignment params) { + System.out.format("name: %s, p: %s, state: %s, alive:%s, daemon:%s, interrupted:%s %n", + interpreterThread.getName(), + interpreterThread.getPriority(), + interpreterThread.getState(), + interpreterThread.isAlive(), + interpreterThread.isDaemon(), + interpreterThread.isInterrupted()); + + List nodes = history.getQueueNode(); + List states = history.getQueueState(); + CommandLogger cmd = new CommandLogger(); + for (int i = 0; i < nodes.size(); i++) { + ASTNode node = nodes.get(i); + node.accept(cmd); + // System.out.format("\t\t\t>>> %d states: [%s]%n", states.get(i).getGoals().size(), + // states.get(i).getSelectedGoalNode().getAssignments().asMap()); } } - private class ChgSel implements edu.kit.formal.interpreter.funchdl.CommandHandler { - @Override - public boolean handles(CallStatement call) throws IllegalArgumentException { - return call.getCommand().equals("chgsel"); - } - - @Override - public void evaluate(Interpreter interpreter, CallStatement call, VariableAssignment params) { - AbstractState state = interpreter.getCurrentState(); - params = interpreter.evaluateParameters(call.getParameters()); - Value v = params.getValues().get("#1"); + public void changeSelected(CallStatement call, VariableAssignment params) { + AbstractState state = interpreter.getCurrentState(); + params = interpreter.evaluateParameters(call.getParameters()); + Value v = params.getValues().get("#1"); - interpreter.newState(state.getGoals(), - state.getGoals().get(v.getData().intValue())); + interpreter.newState(state.getGoals(), + state.getGoals().get(v.getData().intValue())); - } } + private class CommandLogger extends DefaultASTVisitor { public void suffix(ASTNode node) { System.out.format("%02d: ", node.getStartPosition().getLineNumber()); diff --git a/src/main/java/edu/kit/formal/interpreter/Evaluator.java.orig b/src/main/java/edu/kit/formal/interpreter/Evaluator.java.orig deleted file mode 100644 index 8733fdd2..00000000 --- a/src/main/java/edu/kit/formal/interpreter/Evaluator.java.orig +++ /dev/null @@ -1,123 +0,0 @@ -package edu.kit.formal.interpreter; - -import edu.kit.formal.proofscriptparser.DefaultASTVisitor; -import edu.kit.formal.proofscriptparser.ast.*; -import lombok.Getter; -import lombok.Setter; - -import java.util.List; - -/** - * Class handling evaluation of expressions (visitor for expressions) - * - * @author S.Grebing - */ -public class Evaluator extends DefaultASTVisitor { -<<<<<<< Updated upstream - private State currentState; - private Stack> matchedGoals = new Stack<>(); - private EvaluatorABI abi; -======= - private GoalNode currentState; - private List matchedVariables = new ArrayList<>(); - @Getter - @Setter - private MatcherApi matcher; ->>>>>>> Stashed changes - - public Evaluator(State s) { - this.currentState = s; - } - - /** - * Evaluation of an expression. - * - * @param truth - * @return - */ - public Value eval(Expression truth) { - return (Value) truth.accept(this); - } - - @Override - public Value visit(BinaryExpression e) { - Value v1 = (Value) e.getLeft().accept(this); - Value v2 = (Value) e.getRight().accept(this); - Operator op = e.getOperator(); - return op.evaluate(v1, v2); - } - - /** - * TODO Connect with KeY - * - * @param match - * @return - */ - @Override - public Value visit(MatchExpression match) { -<<<<<<< Updated upstream - -======= - Value pattern = (Value) match.getPattern().accept(this); ->>>>>>> Stashed changes - - List va = null; - if (pattern.getType() == Type.STRING) { - va = matcher.matchLabel(currentState, (String) pattern.getData()); - } else if (pattern.getType() == Type.TERM) { - va = matcher.matchSeq(currentState, (String) pattern.getData()); - } - - return va != null && va.size() > 0 ? Value.TRUE : Value.FALSE; - } - - /** - * TODO Connect with KeY - * - * @param term - * @return - */ - @Override - public Value visit(TermLiteral term) { - return null; - } - - @Override - public Value visit(StringLiteral string) { - return Value.from(string); - } - - @Override - public Value visit(Variable variable) { - //get variable value - String id = variable.getIdentifier(); - Value v = currentState.lookupVarValue(id); - if (v != null) { - return v; - } else { - throw new RuntimeException("Variable " + variable + " was not initialized"); - } - - } - - @Override - public Value visit(BooleanLiteral bool) { - return bool.isValue() ? Value.TRUE : Value.FALSE; - } - - - @Override - public Value visit(IntegerLiteral integer) { - return Value.from(integer); - } - - @Override - public Value visit(UnaryExpression e) { - Operator op = e.getOperator(); - Expression expr = e.getExpression(); - Value exValue = (Value) expr.accept(this); - return op.evaluate(exValue); - } - - -} diff --git a/src/main/java/edu/kit/formal/interpreter/HistoryListener.java b/src/main/java/edu/kit/formal/interpreter/HistoryListener.java index ed9d77d7..f4379762 100644 --- a/src/main/java/edu/kit/formal/interpreter/HistoryListener.java +++ b/src/main/java/edu/kit/formal/interpreter/HistoryListener.java @@ -4,6 +4,7 @@ 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; diff --git a/src/main/java/edu/kit/formal/interpreter/InterpreterBuilder.java b/src/main/java/edu/kit/formal/interpreter/InterpreterBuilder.java index d56fe7e1..3c3d85a5 100644 --- a/src/main/java/edu/kit/formal/interpreter/InterpreterBuilder.java +++ b/src/main/java/edu/kit/formal/interpreter/InterpreterBuilder.java @@ -1,53 +1,100 @@ package edu.kit.formal.interpreter; +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.control.KeYEnvironment; import de.uka.ilkd.key.macros.ProofMacro; import de.uka.ilkd.key.macros.scripts.ProofScriptCommand; import de.uka.ilkd.key.proof.Proof; +import edu.kit.formal.ScopeLogger; import edu.kit.formal.interpreter.funchdl.*; import edu.kit.formal.proofscriptparser.Facade; import edu.kit.formal.proofscriptparser.Visitor; import edu.kit.formal.proofscriptparser.ast.ProofScript; +import lombok.Getter; import java.io.File; import java.io.IOException; import java.util.Arrays; +import java.util.Collection; import java.util.List; /** * @author Alexander Weigl * @version 1 (21.05.17) */ + public class InterpreterBuilder { - private ProofScriptHandler psh = new ProofScriptHandler(); - private MacroCommandHandler pmh = new MacroCommandHandler(); - private RuleCommandHandler pmr = new RuleCommandHandler(); + @Getter + private final ProofScriptHandler psh = new ProofScriptHandler(); + @Getter + private final MacroCommandHandler pmh = new MacroCommandHandler(); + @Getter + private final RuleCommandHandler pmr = new RuleCommandHandler(); + @Getter private ProofScriptCommandBuilder pmc = new ProofScriptCommandBuilder(); - - - public Interpreter build(File file) throws IOException { - return build(Facade.getAST(file)); + @Getter + private ProofScript entryPoint; + @Getter + private Proof proof; + @Getter + private KeYEnvironment keyEnvironment; + @Getter + private HistoryListener historyLogger; + @Getter + private ScopeLogger logger; + @Getter + private DefaultLookup lookup = new DefaultLookup(psh, pmh, pmr, pmc); + + private Interpreter interpreter = new Interpreter(lookup); + + public InterpreterBuilder addProofScripts(File file) throws IOException { + return addProofScripts(Facade.getAST(file)); } - private Interpreter build(List ast) { + public InterpreterBuilder addProofScripts(List ast) { psh.addScripts(ast); - DefaultLookup lookup = new DefaultLookup(psh, pmh, pmr, pmc); - return new Interpreter(lookup); + return this; } - public InterpreterBuilder scriptSearchPath(File... paths) { + public InterpreterBuilder startWith(ProofScript entryPoint) { + this.entryPoint = entryPoint; + return this; + } + public Interpreter build() { + return interpreter; } - public InterpreterBuilder keyRules(Proof proof) { + public InterpreterBuilder scriptSearchPath(File... paths) { + psh.getSearchPath().addAll(Arrays.asList(paths)); + return this; + } + //TODO + public InterpreterBuilder proof(KeYEnvironment env, Proof proof) { + this.proof = proof; + this.keyEnvironment = env; + return this; } - public InterpreterBuilder defaultScriptCommands(List commands) { + public InterpreterBuilder scriptCommands() { + return scriptCommands(KeYApi.getScriptCommandApi().getScriptCommands()); + } + public InterpreterBuilder scriptCommands(Collection commands) { + commands.forEach(m -> pmc.getCommands().put(m.getName(), m)); + return this; } - public InterpreterBuilder defaultKeyMacros(List macros) { + public InterpreterBuilder macros() { + return macros(KeYApi.getMacroApi().getMacros()); + } + public InterpreterBuilder macros(Collection macros) { + macros.forEach(m -> pmh.getMacros().put(m.getName(), m)); + return this; } public InterpreterBuilder register(ProofScript... script) { @@ -56,21 +103,27 @@ public class InterpreterBuilder { } public InterpreterBuilder onEntry(Visitor v) { + interpreter.getEntryListeners().add(v); return this; } public InterpreterBuilder onExit(Visitor v) { + interpreter.getExitListeners().add(v); return this; } public InterpreterBuilder captureHistory() { - return this; + if (historyLogger != null) + historyLogger = new HistoryListener(interpreter); + return onEntry(historyLogger); } public InterpreterBuilder log(String prefix) { - return this; + if (logger == null) + logger = new ScopeLogger("interpreter"); + return onEntry(logger); } } diff --git a/src/main/java/edu/kit/formal/interpreter/funchdl/MacroCommandHandler.java b/src/main/java/edu/kit/formal/interpreter/funchdl/MacroCommandHandler.java index c2bfbf24..a7fd6f12 100644 --- a/src/main/java/edu/kit/formal/interpreter/funchdl/MacroCommandHandler.java +++ b/src/main/java/edu/kit/formal/interpreter/funchdl/MacroCommandHandler.java @@ -9,6 +9,7 @@ import edu.kit.formal.proofscriptparser.ast.CallStatement; import edu.kit.formal.proofscriptparser.ast.Parameters; import edu.kit.formal.proofscriptparser.ast.StringLiteral; import edu.kit.formal.proofscriptparser.ast.Variable; +import lombok.Getter; import lombok.RequiredArgsConstructor; import java.lang.reflect.Parameter; @@ -21,7 +22,7 @@ import java.util.Map; */ @RequiredArgsConstructor public class MacroCommandHandler implements CommandHandler { - private final Map macros; + @Getter private final Map macros; public MacroCommandHandler() { macros = new HashMap<>(); diff --git a/src/main/java/edu/kit/formal/interpreter/funchdl/ProofScriptCommandBuilder.java b/src/main/java/edu/kit/formal/interpreter/funchdl/ProofScriptCommandBuilder.java index 62697675..ba4d0576 100644 --- a/src/main/java/edu/kit/formal/interpreter/funchdl/ProofScriptCommandBuilder.java +++ b/src/main/java/edu/kit/formal/interpreter/funchdl/ProofScriptCommandBuilder.java @@ -1,11 +1,11 @@ package edu.kit.formal.interpreter.funchdl; -import de.uka.ilkd.key.api.ProofScriptCommandCall; import de.uka.ilkd.key.macros.scripts.EngineState; import de.uka.ilkd.key.macros.scripts.ProofScriptCommand; import edu.kit.formal.interpreter.Interpreter; import edu.kit.formal.interpreter.VariableAssignment; import edu.kit.formal.proofscriptparser.ast.CallStatement; +import lombok.Getter; import lombok.RequiredArgsConstructor; import java.util.HashMap; @@ -17,7 +17,8 @@ import java.util.Map; */ @RequiredArgsConstructor public class ProofScriptCommandBuilder implements CommandHandler { - private final Map scripts; + @Getter + private final Map commands; public ProofScriptCommandBuilder() { this(new HashMap<>()); @@ -25,14 +26,14 @@ public class ProofScriptCommandBuilder implements CommandHandler { @Override public boolean handles(CallStatement call) { - return scripts.containsKey(call.getCommand()); + return commands.containsKey(call.getCommand()); } @Override public void evaluate(Interpreter interpreter, CallStatement call, VariableAssignment params) { - ProofScriptCommand c = scripts.get(call.getCommand()); + ProofScriptCommand c = commands.get(call.getCommand()); EngineState state = null; Map map; //ProofScriptCommandCall cc = c.evaluateArguments(state, map); -- 2.26.2