Commit 985b0a8b authored by Alexander Weigl's avatar Alexander Weigl

simplifcations and fixes

parent 729fe9ca
Pipeline #10650 passed with stage
in 2 minutes and 7 seconds
...@@ -2,6 +2,7 @@ package edu.kit.formal.dbg; ...@@ -2,6 +2,7 @@ package edu.kit.formal.dbg;
import edu.kit.formal.interpreter.*; import edu.kit.formal.interpreter.*;
import edu.kit.formal.interpreter.funchdl.BuiltinCommands; 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.interpreter.funchdl.DefaultLookup;
import edu.kit.formal.proofscriptparser.*; import edu.kit.formal.proofscriptparser.*;
import edu.kit.formal.proofscriptparser.ast.*; import edu.kit.formal.proofscriptparser.ast.*;
...@@ -10,6 +11,7 @@ import org.antlr.v4.runtime.CharStreams; ...@@ -10,6 +11,7 @@ import org.antlr.v4.runtime.CharStreams;
import java.io.*; import java.io.*;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.List; import java.util.List;
import java.util.function.BiConsumer;
/** /**
* @author Alexander Weigl * @author Alexander Weigl
...@@ -36,14 +38,28 @@ public class Debugger { ...@@ -36,14 +38,28 @@ public class Debugger {
interpreter.getEntryListeners().add(new CommandLogger()); interpreter.getEntryListeners().add(new CommandLogger());
//TODO install debugger functions //TODO install debugger functions
debuggerFunctions.getBuilders().add(new Step()); registerDebuggerFunction("step", this::step);
debuggerFunctions.getBuilders().add(new Printer()); registerDebuggerFunction("b", this::setBreakpoint);
debuggerFunctions.getBuilders().add(new ChgSel()); registerDebuggerFunction("start", this::start);
debuggerFunctions.getBuilders().add(new Start()); registerDebuggerFunction("pause", this::pause);
debuggerFunctions.getBuilders().add(new Pause()); registerDebuggerFunction("chgsel", this::changeSelected);
debuggerFunctions.getBuilders().add(new BrkPnt()); registerDebuggerFunction("psel", this::psel);
debuggerFunctions.getBuilders().add(new Status()); registerDebuggerFunction("status", this::status);
}
private void registerDebuggerFunction(final String step,
BiConsumer<CallStatement, VariableAssignment> 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 { public static void main(String[] args) throws IOException {
...@@ -64,11 +80,11 @@ public class Debugger { ...@@ -64,11 +80,11 @@ public class Debugger {
while (true) { while (true) {
System.out.printf("dbg (%03d)> ", ++counter); System.out.printf("dbg (%03d)> ", ++counter);
String input = br.readLine(); String input = br.readLine();
execuate(input); execute(input);
} }
} }
private void execuate(String input) { private void execute(String input) {
input = input.trim(); input = input.trim();
if (input.isEmpty()) { if (input.isEmpty()) {
return; return;
...@@ -90,140 +106,83 @@ public class Debugger { ...@@ -90,140 +106,83 @@ public class Debugger {
} }
private class Step implements edu.kit.formal.interpreter.funchdl.CommandHandler { public void step(CallStatement call, VariableAssignment params) {
@Override IntegerLiteral il = (IntegerLiteral) call.getParameters().get(new Variable("#1"));
public boolean handles(CallStatement call) throws IllegalArgumentException { int steps = 1;
return call.getCommand().equals("step"); if (il != null)
} steps = il.getValue().intValue();
blocker.stepUntilBlock.set(steps * 2); //FIXME times two is strange, something wrong on sync
@Override //LockSupport.unpark(interpreterThread);
public void evaluate(Interpreter interpreter, CallStatement call, VariableAssignment params) { blocker.unlock();
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 { public void psel(CallStatement call, VariableAssignment params) {
@Override AbstractState state = interpreter.getCurrentState();
public boolean handles(CallStatement call) throws IllegalArgumentException { int i = 0;
return call.getCommand().equals("psel"); GoalNode sel;
try {
sel = state.getSelectedGoalNode();
} catch (IllegalStateException e) {
sel = null;
} }
@Override for (GoalNode g : state.getGoals()) {
public void evaluate(Interpreter interpreter, CallStatement call, VariableAssignment params) { System.out.printf("%2d %s %s\n %s\n",
AbstractState state = interpreter.getCurrentState(); i++,
int i = 0; g == sel ? "*" : " ",
GoalNode sel; g.getSequent(),
try { g.getAssignments().asMap());
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());
}
} }
} }
public void start(CallStatement call, VariableAssignment params) {
private class Start implements edu.kit.formal.interpreter.funchdl.CommandHandler { interpreterThread.start();
@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();
}
} }
private class Pause implements edu.kit.formal.interpreter.funchdl.CommandHandler { public void pause(CallStatement call, VariableAssignment params) {
@Override blocker.stepUntilBlock.set(1); // block at next statement
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
}
} }
private class BrkPnt implements edu.kit.formal.interpreter.funchdl.CommandHandler { public void setBreakpoint(CallStatement call, VariableAssignment params) {
@Override IntegerLiteral il = (IntegerLiteral) call.getParameters().get(new Variable("#1"));
public boolean handles(CallStatement call) throws IllegalArgumentException { blocker.addBreakpoint(il.getValue().intValue());
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());
System.out.println("brkpnts: " + blocker.brkpnts); System.out.println("brkpnts: " + blocker.brkpnts);
}
} }
public void status(CallStatement call, VariableAssignment params) {
private class Status implements edu.kit.formal.interpreter.funchdl.CommandHandler { System.out.format("name: %s, p: %s, state: %s, alive:%s, daemon:%s, interrupted:%s %n",
@Override interpreterThread.getName(),
public boolean handles(CallStatement call) throws IllegalArgumentException { interpreterThread.getPriority(),
return call.getCommand().equals("status"); interpreterThread.getState(),
} interpreterThread.isAlive(),
interpreterThread.isDaemon(),
@Override interpreterThread.isInterrupted());
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", List<ASTNode> nodes = history.getQueueNode();
interpreterThread.getName(), List<AbstractState> states = history.getQueueState();
interpreterThread.getPriority(), CommandLogger cmd = new CommandLogger();
interpreterThread.getState(), for (int i = 0; i < nodes.size(); i++) {
interpreterThread.isAlive(), ASTNode node = nodes.get(i);
interpreterThread.isDaemon(), node.accept(cmd);
interpreterThread.isInterrupted()); // System.out.format("\t\t\t>>> %d states: [%s]%n", states.get(i).getGoals().size(),
// states.get(i).getSelectedGoalNode().getAssignments().asMap());
List<ASTNode> nodes = history.getQueueNode();
List<AbstractState> 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 { public void changeSelected(CallStatement call, VariableAssignment params) {
@Override AbstractState state = interpreter.getCurrentState();
public boolean handles(CallStatement call) throws IllegalArgumentException { params = interpreter.evaluateParameters(call.getParameters());
return call.getCommand().equals("chgsel"); Value<BigInteger> v = params.getValues().get("#1");
}
@Override
public void evaluate(Interpreter interpreter, CallStatement call, VariableAssignment params) {
AbstractState state = interpreter.getCurrentState();
params = interpreter.evaluateParameters(call.getParameters());
Value<BigInteger> v = params.getValues().get("#1");
interpreter.newState(state.getGoals(), interpreter.newState(state.getGoals(),
state.getGoals().get(v.getData().intValue())); state.getGoals().get(v.getData().intValue()));
}
} }
private class CommandLogger extends DefaultASTVisitor<Void> { private class CommandLogger extends DefaultASTVisitor<Void> {
public void suffix(ASTNode node) { public void suffix(ASTNode node) {
System.out.format("%02d: ", node.getStartPosition().getLineNumber()); System.out.format("%02d: ", node.getStartPosition().getLineNumber());
......
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<Value> {
<<<<<<< Updated upstream
private State currentState;
private Stack<List<GoalNode>> matchedGoals = new Stack<>();
private EvaluatorABI abi;
=======
private GoalNode currentState;
private List<VariableAssignment> 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<VariableAssignment> 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);
}
}
...@@ -4,6 +4,7 @@ import edu.kit.formal.proofscriptparser.DefaultASTVisitor; ...@@ -4,6 +4,7 @@ import edu.kit.formal.proofscriptparser.DefaultASTVisitor;
import edu.kit.formal.proofscriptparser.ast.ASTNode; import edu.kit.formal.proofscriptparser.ast.ASTNode;
import lombok.Getter; import lombok.Getter;
import lombok.RequiredArgsConstructor; import lombok.RequiredArgsConstructor;
import lombok.Setter;
import java.util.LinkedList; import java.util.LinkedList;
import java.util.List; import java.util.List;
......
package edu.kit.formal.interpreter; 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.ProofMacro;
import de.uka.ilkd.key.macros.scripts.ProofScriptCommand; import de.uka.ilkd.key.macros.scripts.ProofScriptCommand;
import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.Proof;
import edu.kit.formal.ScopeLogger;
import edu.kit.formal.interpreter.funchdl.*; import edu.kit.formal.interpreter.funchdl.*;
import edu.kit.formal.proofscriptparser.Facade; import edu.kit.formal.proofscriptparser.Facade;
import edu.kit.formal.proofscriptparser.Visitor; import edu.kit.formal.proofscriptparser.Visitor;
import edu.kit.formal.proofscriptparser.ast.ProofScript; import edu.kit.formal.proofscriptparser.ast.ProofScript;
import lombok.Getter;
import java.io.File; import java.io.File;
import java.io.IOException; import java.io.IOException;
import java.util.Arrays; import java.util.Arrays;
import java.util.Collection;
import java.util.List; import java.util.List;
/** /**
* @author Alexander Weigl * @author Alexander Weigl
* @version 1 (21.05.17) * @version 1 (21.05.17)
*/ */
public class InterpreterBuilder { public class InterpreterBuilder {
private ProofScriptHandler psh = new ProofScriptHandler(); @Getter
private MacroCommandHandler pmh = new MacroCommandHandler(); private final ProofScriptHandler psh = new ProofScriptHandler();
private RuleCommandHandler pmr = new RuleCommandHandler(); @Getter
private final MacroCommandHandler pmh = new MacroCommandHandler();
@Getter
private final RuleCommandHandler pmr = new RuleCommandHandler();
@Getter
private ProofScriptCommandBuilder pmc = new ProofScriptCommandBuilder(); private ProofScriptCommandBuilder pmc = new ProofScriptCommandBuilder();
@Getter
private ProofScript entryPoint;
public Interpreter build(File file) throws IOException { @Getter
return build(Facade.getAST(file)); 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<ProofScript> ast) { public InterpreterBuilder addProofScripts(List<ProofScript> ast) {
psh.addScripts(ast); psh.addScripts(ast);
DefaultLookup lookup = new DefaultLookup(psh, pmh, pmr, pmc); return this;
return new Interpreter(lookup);
} }
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<ProofScriptCommand> commands) { public InterpreterBuilder scriptCommands() {
return scriptCommands(KeYApi.getScriptCommandApi().getScriptCommands());
}
public InterpreterBuilder scriptCommands(Collection<ProofScriptCommand> commands) {
commands.forEach(m -> pmc.getCommands().put(m.getName(), m));
return this;
} }
public InterpreterBuilder defaultKeyMacros(List<ProofMacro> macros) { public InterpreterBuilder macros() {
return macros(KeYApi.getMacroApi().getMacros());
}
public InterpreterBuilder macros(Collection<ProofMacro> macros) {
macros.forEach(m -> pmh.getMacros().put(m.getName(), m));
return this;
} }
public InterpreterBuilder register(ProofScript... script) { public InterpreterBuilder register(ProofScript... script) {
...@@ -56,21 +103,27 @@ public class InterpreterBuilder { ...@@ -56,21 +103,27 @@ public class InterpreterBuilder {
} }
public InterpreterBuilder onEntry(Visitor v) { public InterpreterBuilder onEntry(Visitor v) {
interpreter.getEntryListeners().add(v);
return this; return this;
} }
public InterpreterBuilder onExit(Visitor v) { public InterpreterBuilder onExit(Visitor v) {
interpreter.getExitListeners().add(v);
return this; return this;
} }
public InterpreterBuilder captureHistory() { public InterpreterBuilder captureHistory() {
return this; if (historyLogger != null)
historyLogger = new HistoryListener(interpreter);
return onEntry(historyLogger);
} }
public InterpreterBuilder log(String prefix) { public InterpreterBuilder log(String prefix) {
return this; if (logger == null)
logger = new ScopeLogger("interpreter");