Commit 74bfe221 authored by Alexander Weigl's avatar Alexander Weigl

Assignment hooks

* small bug fixes
parent c2e74e84
......@@ -65,6 +65,8 @@ OR: '|' ;
IMP: '->';
MOD:'%';
XOR:'^';
FORALL: '\forall' | '∀';
EXISTS: '\exists';
DIGITS : DIGIT+ ;
fragment DIGIT : [0-9] ;
......
......@@ -7,6 +7,7 @@ import de.uka.ilkd.key.api.ScriptApi;
import de.uka.ilkd.key.api.VariableAssignments;
import de.uka.ilkd.key.proof.Goal;
import de.uka.ilkd.key.proof.Proof;
import edu.kit.formal.psdb.interpreter.assignhook.VariableAssignmentHook;
import edu.kit.formal.psdb.interpreter.data.*;
import edu.kit.formal.psdb.interpreter.exceptions.InterpreterRuntimeException;
import edu.kit.formal.psdb.interpreter.exceptions.ScriptCommandNotApplicableException;
......@@ -62,6 +63,10 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
@Getter
private ScriptApi scriptApi;
@Getter
@Setter
private VariableAssignmentHook<T> variableAssignmentHook = null;
public Interpreter(CommandLookup lookup) {
functionLookup = lookup;
}
......@@ -73,6 +78,14 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
if (stateStack.empty()) {
throw new InterpreterRuntimeException("no state on stack. call newState before interpret");
}
//initialize environment variables
if (variableAssignmentHook != null) {
VariableAssignment va = variableAssignmentHook.getStartAssignment(getSelectedNode().getData());
getSelectedNode().setAssignments(
getSelectedNode().getAssignments().push(va));
}
script.accept(this);
}
......@@ -119,7 +132,9 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
throw new RuntimeException("SimpleType of Variable " + var + " is not declared yet");
} else {
Value v = evaluate(expr);
node.setVariableValue(var, v);
if (fireVariableAssignmentHook(node, var.getIdentifier(), v)) {
node.setVariableValue(var, v);
}
}
}
exitScope(assignmentStatement);
......@@ -127,6 +142,13 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
return null;
}
protected boolean fireVariableAssignmentHook(GoalNode<T> node, String identifier, Value v) {
if (variableAssignmentHook != null) {
return variableAssignmentHook.handleAssignment(node.getData(), identifier, v);
}
return true;
}
private Value evaluate(Expression expr) {
return evaluate(getSelectedNode(), expr);
......@@ -519,6 +541,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
/**
* Create new state containing goals and selected goal node an push to stack
*
* @param goals
* @param selected
* @return state that is pushed to stack
......@@ -532,6 +555,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
/**
* Cretae a ew state conatining the goals but without selected goal node and push to stack
*
* @param goals
* @return
*/
......@@ -541,6 +565,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
/**
* Cretae a new state containing only the selected goal node and push to stack
*
* @param selected
* @return reference to state on stack
*/
......@@ -550,6 +575,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
/**
* Push state to stack and return reference to this state
*
* @param state
* @return
*/
......@@ -563,6 +589,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
/**
* Remove top level state from stack and throw an Exception if state does not equal expected state
*
* @param expected
* @return
*/
......@@ -576,6 +603,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
/**
* Remove top level state from stack
*
* @return
*/
private State<T> popState() {
......@@ -584,6 +612,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
/**
* Lookup state on the stack but do not remove it
*
* @return
*/
public State<T> peekState() {
......@@ -592,6 +621,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
/**
* Get goalnodes from current state
*
* @return
*/
public List<GoalNode<T>> getCurrentGoals() {
......
......@@ -8,6 +8,7 @@ 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.psdb.interpreter.assignhook.KeyAssignmentHook;
import edu.kit.formal.psdb.interpreter.data.GoalNode;
import edu.kit.formal.psdb.interpreter.data.KeyData;
import edu.kit.formal.psdb.interpreter.data.VariableAssignment;
......@@ -53,6 +54,9 @@ public class InterpreterBuilder {
private DefaultLookup lookup = new DefaultLookup(psh, pmh, pmr, pmc);
private Interpreter<KeyData> interpreter = new Interpreter<>(lookup);
@Getter
private KeyAssignmentHook variableHook = new KeyAssignmentHook();
public InterpreterBuilder addProofScripts(File file) throws IOException {
return addProofScripts(Facade.getAST(file));
}
......@@ -68,6 +72,7 @@ public class InterpreterBuilder {
}
public Interpreter<KeyData> build() {
interpreter.setVariableAssignmentHook(variableHook);
return interpreter;
}
......
package edu.kit.formal.psdb.interpreter.assignhook;
import edu.kit.formal.psdb.interpreter.data.Value;
import edu.kit.formal.psdb.interpreter.data.VariableAssignment;
import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger;
import java.util.HashMap;
import java.util.Map;
import java.util.function.BiFunction;
import java.util.function.Function;
/**
* @author Alexander Weigl
* @version 1 (21.08.17)
*/
public abstract class DefaultAssignmentHook<T> implements VariableAssignmentHook<T> {
private static Logger logger = LogManager.getLogger(KeyAssignmentHook.class);
private Map<String, Function<T, Value>> initFunctions = new HashMap<>();
private Map<String, BiFunction<T, Value, Boolean>> hooks = new HashMap<>();
protected void register(String varName, BiFunction<T, Value, Boolean> setter, Function<T, Value> getter) {
initFunctions.put(varName, getter);
hooks.put(varName, setter);
}
@Override
public <S> boolean handleAssignment(T data, String variableName, Value<S> value) {
if (hooks.containsKey(variableName)) {
return hooks.get(variableName).apply(data, value);
}
return true;
}
@Override
public VariableAssignment getStartAssignment(T data) {
VariableAssignment va = new VariableAssignment();
for (Map.Entry<String, Function<T, Value>> s : initFunctions.entrySet()) {
Value apply = s.getValue().apply(data);
va.declare(s.getKey(), apply.getType());
va.assign(s.getKey(), apply);
}
return va;
}
}
package edu.kit.formal.psdb.interpreter.assignhook;
import edu.kit.formal.psdb.interpreter.data.KeyData;
import edu.kit.formal.psdb.interpreter.data.Value;
import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger;
import java.math.BigInteger;
/**
* @author Alexander Weigl
* @version 1 (21.08.17)
*/
public class KeyAssignmentHook extends DefaultAssignmentHook<KeyData> {
private static Logger logger = LogManager.getLogger(KeyAssignmentHook.class);
public KeyAssignmentHook() {
register("MAX_AUTO_STEPS", this::setMaxAutosteps, this::getMaxAutosteps);
}
public Value<BigInteger> getMaxAutosteps(KeyData data) {
return Value.from(100);
}
public boolean setMaxAutosteps(KeyData data, Value<BigInteger> val) {
return true;
}
}
package edu.kit.formal.psdb.interpreter.assignhook;
import edu.kit.formal.psdb.interpreter.data.Value;
import edu.kit.formal.psdb.interpreter.data.VariableAssignment;
/**
* @author Alexander Weigl
* @version 1 (21.08.17)
*/
public interface VariableAssignmentHook<T> {
/**
* @param data
* @param variableName
* @param value
* @param <S>
*/
<S> boolean handleAssignment(T data, String variableName, Value<S> value);
/**
* @param data
* @return
*/
VariableAssignment getStartAssignment(T data);
}
......@@ -3,6 +3,7 @@ package edu.kit.formal.psdb.interpreter.data;
import edu.kit.formal.psdb.parser.ast.Variable;
import edu.kit.formal.psdb.parser.types.Type;
import lombok.Getter;
import lombok.Setter;
import lombok.ToString;
/**
......@@ -13,6 +14,8 @@ import lombok.ToString;
*/
@ToString
public class GoalNode<T> {
@Getter
@Setter
private VariableAssignment assignments;
@Getter
......@@ -31,18 +34,11 @@ public class GoalNode<T> {
* @param data
*/
public GoalNode(GoalNode<T> parent, T data, boolean isClosed) {
//BUG: Hier muesste deepcopy der assignments passieren
this.assignments = new VariableAssignment(parent == null ? null : parent.deepCopyAssignments());
this.assignments = new VariableAssignment(parent == null ? null :
parent.getAssignments().deepCopy());
this.parent = parent;
this.data = data;
}
private VariableAssignment deepCopyAssignments() {
return assignments.deepCopy();
}
public VariableAssignment getAssignments() {
return assignments;
this.isClosed = isClosed;
}
/**
......
......@@ -273,7 +273,8 @@ public class ProofTreeController {
}
//create interpreter service and start
if (interpreterService.getState() == Worker.State.SUCCEEDED || interpreterService.getState() == Worker.State.CANCELLED) {
if (interpreterService.getState() == Worker.State.SUCCEEDED
|| interpreterService.getState() == Worker.State.CANCELLED) {
interpreterService.reset();
}
interpreterService.interpreterProperty().set(currentInterpreter);
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment