Commit 15b00201 authored by Sarah Grebing's avatar Sarah Grebing

Merge remote-tracking branch 'origin/master'

parents fefcf60b 15bc40a0
...@@ -6,7 +6,7 @@ plugins { ...@@ -6,7 +6,7 @@ plugins {
allprojects { allprojects {
apply plugin: 'maven' apply plugin: 'maven'
group = 'edu.kit.iti.formal.psdbg' group = 'edu.kit.iti.formal.psdbg'
version = 'Experimental-1.1' version = '1.1-experimental'
} }
subprojects { subprojects {
......
package edu.kit.iti.formal.psdbg.parser;
import edu.kit.iti.formal.psdbg.parser.ast.*;
import javafx.util.Pair;
public class SavepointVisitor extends DefaultASTVisitor {
@Override
public Parameters visit(CallStatement call) {
if (call.getCommand().toString().equals("save")) {
Parameters param = call.getParameters().copy();
return param;
} else {
return null;
}
}
}
...@@ -23,10 +23,7 @@ import org.key_project.util.collection.ImmutableList; ...@@ -23,10 +23,7 @@ import org.key_project.util.collection.ImmutableList;
import java.io.File; import java.io.File;
import java.io.IOException; import java.io.IOException;
import java.util.Arrays; import java.util.*;
import java.util.Collection;
import java.util.List;
import java.util.Set;
import java.util.stream.Collectors; import java.util.stream.Collectors;
/** /**
...@@ -44,6 +41,8 @@ public class InterpreterBuilder { ...@@ -44,6 +41,8 @@ public class InterpreterBuilder {
@Getter @Getter
private ProofScriptCommandBuilder pmc = new ProofScriptCommandBuilder(); private ProofScriptCommandBuilder pmc = new ProofScriptCommandBuilder();
@Getter @Getter
private BuiltInCommandHandler bich = new BuiltInCommandHandler();
@Getter
private ProofScript entryPoint; private ProofScript entryPoint;
@Getter @Getter
private Proof proof; private Proof proof;
...@@ -54,13 +53,15 @@ public class InterpreterBuilder { ...@@ -54,13 +53,15 @@ public class InterpreterBuilder {
@Getter @Getter
private ScopeLogger logger; private ScopeLogger logger;
@Getter @Getter
private DefaultLookup lookup = new DefaultLookup(psh, pmh, pmc, pmr); private DefaultLookup lookup = new DefaultLookup(psh, pmh, pmc, bich, pmr);
@Getter @Getter
private KeyAssignmentHook keyHooks = new KeyAssignmentHook(); private KeyAssignmentHook keyHooks = new KeyAssignmentHook();
private KeyInterpreter interpreter = new KeyInterpreter(lookup); private KeyInterpreter interpreter = new KeyInterpreter(lookup);
@Getter @Getter
private InterpreterOptionsHook<KeyData> optionsHook = new InterpreterOptionsHook<>(interpreter); private InterpreterOptionsHook<KeyData> optionsHook = new InterpreterOptionsHook<>(interpreter);
...@@ -202,18 +203,33 @@ public class InterpreterBuilder { ...@@ -202,18 +203,33 @@ public class InterpreterBuilder {
if (proof == null || keyEnvironment == null) if (proof == null || keyEnvironment == null)
throw new IllegalStateException("Call proof(..) before startState"); throw new IllegalStateException("Call proof(..) before startState");
ImmutableList<Goal> openGoals = proof.getSubtreeGoals(proof.root()); ImmutableList<Goal> openGoals = proof.getSubtreeGoals(proof.root());
List<GoalNode<KeyData>> goals = openGoals.stream().map(g -> List<GoalNode<KeyData>> goals = openGoals.stream().map(g ->
new GoalNode<>(null, new KeyData(g, keyEnvironment, proof), false)) new GoalNode<>(null, new KeyData(g, keyEnvironment, proof), false))
.collect(Collectors.toList()); .collect(Collectors.toList());
interpreter.newState(goals); interpreter.newState(goals);
return this; return this;
} }
private InterpreterBuilder startState(GoalNode<KeyData> startGoal) { private InterpreterBuilder startState(GoalNode<KeyData> startGoal) {
interpreter.newState(startGoal); interpreter.newState(startGoal);
return this;
}
public InterpreterBuilder setProblemPath(File path){
Map<String, CommandHandler<KeyData>> builtinsnew = this.bich.getBuiltins();
SaveCommand sc = new SaveCommand(path);
builtinsnew.put(SaveCommand.SAVE_COMMAND_NAME, sc);
this.bich.setBuiltins(builtinsnew);
return this; return this;
} }
} }
...@@ -16,6 +16,7 @@ import javafx.beans.binding.BooleanBinding; ...@@ -16,6 +16,7 @@ import javafx.beans.binding.BooleanBinding;
import javafx.beans.property.SimpleBooleanProperty; import javafx.beans.property.SimpleBooleanProperty;
import javafx.beans.property.SimpleObjectProperty; import javafx.beans.property.SimpleObjectProperty;
import javafx.concurrent.Task; import javafx.concurrent.Task;
import jdk.nashorn.internal.objects.annotations.Getter;
import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger; import org.apache.logging.log4j.Logger;
import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableList;
...@@ -70,6 +71,8 @@ public class KeYProofFacade { ...@@ -70,6 +71,8 @@ public class KeYProofFacade {
//Workaround until api is relaxed //Workaround until api is relaxed
private ProofManagementApi pma; private ProofManagementApi pma;
private File filepath;
/** /**
* *
*/ */
...@@ -131,6 +134,7 @@ public class KeYProofFacade { ...@@ -131,6 +134,7 @@ public class KeYProofFacade {
ProofManagementApi pma = KeYApi.loadFromKeyFile(keYFile); ProofManagementApi pma = KeYApi.loadFromKeyFile(keYFile);
ProofApi pa = pma.getLoadedProof(); ProofApi pa = pma.getLoadedProof();
setLoading(false); setLoading(false);
filepath = keYFile;
return pa; return pa;
} }
...@@ -141,6 +145,7 @@ public class KeYProofFacade { ...@@ -141,6 +145,7 @@ public class KeYProofFacade {
proof.set(pa.getProof()); proof.set(pa.getProof());
contract.set(null); contract.set(null);
setLoading(false); setLoading(false);
filepath = keyFile;
return pa; return pa;
} }
...@@ -249,6 +254,13 @@ public class KeYProofFacade { ...@@ -249,6 +254,13 @@ public class KeYProofFacade {
return readyToExecute; return readyToExecute;
} }
/**
returns filepath of loaded KeY problem
**/
public File getFilepath() {
return filepath;
}
public Collection<GoalNode<KeyData>> getPseudoGoals() { public Collection<GoalNode<KeyData>> getPseudoGoals() {
Proof p = getProof(); Proof p = getProof();
KeYEnvironment env = getEnvironment(); KeYEnvironment env = getEnvironment();
......
package edu.kit.iti.formal.psdbg.interpreter.funchdl;
import edu.kit.iti.formal.psdbg.interpreter.Interpreter;
import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
import edu.kit.iti.formal.psdbg.interpreter.data.SavePoint;
import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
import lombok.Getter;
import lombok.Setter;
import javax.annotation.Nullable;
import java.util.HashMap;
import java.util.Map;
public class BuiltInCommandHandler implements CommandHandler<KeyData> {
@Getter @Setter
private Map<String, CommandHandler<KeyData>> builtins;
public BuiltInCommandHandler() {
builtins = new HashMap<>();
}
@Override
public boolean handles(CallStatement call, @Nullable KeyData data) throws IllegalArgumentException {
// handler only knows SaveCommand for now
return builtins.containsKey(call.getCommand());
}
@Override
public void evaluate(Interpreter<KeyData> interpreter, CallStatement call, VariableAssignment params, KeyData data) {
builtins.get(call.getCommand()).evaluate(interpreter,call,params, data);
}
@Override
public boolean isUninterpretedParams(CallStatement call) {
if(builtins.containsKey(call.getCommand())){
return builtins.get(call.getCommand()).isUninterpretedParams(call);
} else {
return false;
}
}
}
...@@ -85,11 +85,16 @@ public class RuleCommandHandler implements CommandHandler<KeyData> { ...@@ -85,11 +85,16 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
@Override @Override
public boolean handles(CallStatement call, KeyData data) throws IllegalArgumentException { public boolean handles(CallStatement call, KeyData data) throws IllegalArgumentException {
if (rules.containsKey(call.getCommand())) return true;//static/rigid rules if (rules.containsKey(call.getCommand())) return true;//static/rigid rules
try{
if (data != null) { if (data != null) {
Goal goal = data.getGoal(); Goal goal = data.getGoal();
Set<String> rules = findTaclets(data.getProof(), goal); Set<String> rules = findTaclets(data.getProof(), goal);
return rules.contains(call.getCommand()); return rules.contains(call.getCommand());
} }
} catch (NullPointerException npe) {
System.out.println("npe = " + npe);
return false;
}
return false; return false;
} }
......
package edu.kit.iti.formal.psdbg.interpreter.funchdl;
import edu.kit.iti.formal.psdbg.interpreter.Interpreter;
import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
import edu.kit.iti.formal.psdbg.interpreter.data.SavePoint;
import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
import lombok.Getter;
import lombok.Setter;
import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger;
import javax.annotation.Nullable;
import java.io.File;
import java.io.IOException;
public class SaveCommand implements CommandHandler<KeyData> {
public static final String SAVE_COMMAND_NAME = "#save";
private static Logger logger = LogManager.getLogger(SaveCommand.class);
private static Logger consoleLogger = LogManager.getLogger("console");
@Getter
@Setter
private File path;
public SaveCommand(File path) {
this.path = path;
}
@Override
public boolean handles(CallStatement call, @Nullable KeyData data) throws IllegalArgumentException {
return call.getCommand().equals(SAVE_COMMAND_NAME);
}
@Override
public void evaluate(Interpreter<KeyData> interpreter, CallStatement call, VariableAssignment params, KeyData data) {
//be careful parameters are uninterpreted
SavePoint sp = new SavePoint(call);
//Not via Parentpath -> dependency on OS
/* String parentPath = path.getAbsolutePath();
parentPath = parentPath.substring(0, parentPath.length() - path.getName().length());*/
File parent = path.getParentFile();
File newFile = sp.getProofFile(parent);
consoleLogger.info("(Safepoint) Location to be saved to = " + newFile.getAbsolutePath());
try {
interpreter.getSelectedNode().getData().getProof().saveToFile(newFile);
//TODO Call to key persistend facade
} catch (IOException e) {
e.printStackTrace();
}
}
@Override
public boolean isUninterpretedParams(CallStatement call) {
return true;
}
}
<?xml version="1.0" encoding="UTF-8"?> <?xml version="1.0" encoding="UTF-8"?>
<!--
https://logging.apache.org/log4j/2.x/manual/configuration.html
-->
<Configuration status="error"> <Configuration status="error">
<Appenders> <Appenders>
<Console name="ConsoleErr" target="SYSTEM_ERR">
<PatternLayout pattern="%d{HH:mm:ss.SSS} [%t] %-5level %logger{36} - %msg%n"/>
</Console>
<Console name="Console" target="SYSTEM_OUT"> <Console name="Console" target="SYSTEM_OUT">
<PatternLayout pattern="[%-5level] %msg%n"/> <PatternLayout>
<!--<PatternLayout pattern="%d{HH:mm:ss.SSS} [%t] %-5level %logger{36} - %msg%n"/>--> <!-- <pattern>%d %highlight{%p} %style{%C{1.} [%t] %m}{bold,green}%n</pattern>-->
<pattern>%r %highlight{%p} %style{[%t] %m}{bold,green} \n\t\tfrom %l%n</pattern>
</PatternLayout>
</Console> </Console>
<File name="F" fileName="debug.log" bufferSize="0" bufferedIO="false" append="false"> <File name="F" fileName="debug.log" bufferSize="0" bufferedIO="false" append="false">
<PatternLayout pattern="%d{HH:mm:ss.SSS} [%t] %-5level %logger{36} - %msg%n"/> <PatternLayout pattern="%d{HH:mm:ss.SSS} [%t] %-5level %logger{36} - %msg%n"/>
</File> </File>
</Appenders> </Appenders>
<Loggers> <Loggers>
<Root level="trace"> <Root level="trace">
<AppenderRef ref="Console" level="warn"/> <AppenderRef ref="ConsoleErr" level="error"/>
<AppenderRef ref="F"/> <AppenderRef ref="F"/>
</Root> </Root>
<Logger name="console">
<AppenderRef ref="Console" level="info"/>
</Logger>
</Loggers> </Loggers>
</Configuration> </Configuration>
...@@ -148,7 +148,7 @@ public class Evaluator<T> extends DefaultASTVisitor<Value> implements ScopeObser ...@@ -148,7 +148,7 @@ public class Evaluator<T> extends DefaultASTVisitor<Value> implements ScopeObser
String name = m.group().substring(1); // remove trailing '?' String name = m.group().substring(1); // remove trailing '?'
Expression t = expr.getSubstitution().get(m.group()); Expression t = expr.getSubstitution().get(m.group());
//either evalute the substitent or find ?X in the //either evalute the substituent or find ?X in the
String newVal = ""; String newVal = "";
if (t != null) if (t != null)
newVal = ((Value) t.accept(this)).getData().toString(); newVal = ((Value) t.accept(this)).getData().toString();
......
...@@ -85,7 +85,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object> ...@@ -85,7 +85,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
throw new InterpreterRuntimeException("no state on stack. call newState before interpret"); throw new InterpreterRuntimeException("no state on stack. call newState before interpret");
} }
if(getSelectedNode() != null) { if (getSelectedNode() != null) {
//initialize environment variables //initialize environment variables
for (VariableAssignmentHook<T> hook : variableHooks) { for (VariableAssignmentHook<T> hook : variableHooks) {
VariableAssignment va = hook.getStartAssignment(getSelectedNode().getData()); VariableAssignment va = hook.getStartAssignment(getSelectedNode().getData());
...@@ -186,7 +186,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object> ...@@ -186,7 +186,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
return evaluator.eval(expr); return evaluator.eval(expr);
} }
protected Evaluator<T> createEvaluator(VariableAssignment assignments, GoalNode<T> g) { protected Evaluator<T> createEvaluator(VariableAssignment assignments, GoalNode<T> g) {
Evaluator<T> evaluator = new Evaluator<>(assignments, g); Evaluator<T> evaluator = new Evaluator<>(assignments, g);
evaluator.setMatcher(matcherApi); evaluator.setMatcher(matcherApi);
return evaluator; return evaluator;
...@@ -562,30 +562,61 @@ public class Interpreter<T> extends DefaultASTVisitor<Object> ...@@ -562,30 +562,61 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
enterScope(call); enterScope(call);
if (!call.getCommand().isEmpty()) //real call, can handle pseudo calls! if (!call.getCommand().isEmpty()) //real call, can handle pseudo calls!
{ {
// System.out.println(stateStack.peek().hashCode());
//neuer VarScope //neuer VarScope
//enter new variable scope //enter new variable scope
VariableAssignment params = evaluateParameters(call.getParameters()); VariableAssignment params;
GoalNode<T> g = getSelectedNode(); GoalNode<T> g = null;
g.enterScope(); boolean unInterpretedParams = functionLookup.isUninterpretedParams(call);
if (!unInterpretedParams) {
params = evaluateParameters(call.getParameters());
g = getSelectedNode();
g.enterScope();
} else {
params = evaluateParametersStateLess(call.getParameters());
}
try { try {
functionLookup.callCommand(this, call, params); functionLookup.callCommand(this, call, params);
} catch (RuntimeException e) { } catch (RuntimeException e) {
System.err.println("Call command not applicable"); System.err.println("Call command " + call.getCommand() + "not applicable");
throw e; throw e;
//TODO handling of error state for each visit //TODO handling of error state for each visit
//State<T> newErrorState = newState(null, null); //State<T> newErrorState = newState(null, null);
//newErrorState.setErrorState(true); //newErrorState.setErrorState(true);
//pushState(newErrorState); //pushState(newErrorState);
} finally { } finally {
g.exitScope(); if (!unInterpretedParams) {
// System.out.println(stateStack.peek().hashCode()); //TODO this may not be needed
g.exitScope();
}
} }
} }
exitScope(call); exitScope(call);
return null; return null;
} }
private VariableAssignment evaluateParametersStateLess(Parameters parameters) {
VariableAssignment va = new VariableAssignment();
Evaluator<T> evaluator = createEvaluator(null, null);
parameters.entrySet().forEach(entry -> {
try {
Value val = evaluate(entry.getValue());
va.declare(entry.getKey(), val.getType());
va.assign(entry.getKey(), val);
} catch (NullPointerException npe) {
System.out.println("Caught Nullpointer in evaluation of Stateless parameters: " + entry.toString()
);
Value val = evaluator.eval(entry.getValue());
va.declare(entry.getKey(), val.getType());
va.assign(entry.getKey(), val);
}
});
return va;
}
public VariableAssignment evaluateParameters(Parameters parameters) { public VariableAssignment evaluateParameters(Parameters parameters) {
VariableAssignment va = new VariableAssignment(); VariableAssignment va = new VariableAssignment();
parameters.entrySet().forEach(entry -> { parameters.entrySet().forEach(entry -> {
...@@ -669,9 +700,9 @@ public class Interpreter<T> extends DefaultASTVisitor<Object> ...@@ -669,9 +700,9 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
// TODO: quickfix // TODO: quickfix
List<GoalNode<T>> currentGoals = getCurrentGoals(); List<GoalNode<T>> currentGoals = getCurrentGoals();
if(getCurrentGoals().size() > 1) { if (getCurrentGoals().size() > 1) {
if(getSelectedNode() == null) { if (getSelectedNode() == null) {
for(GoalNode<T> goal: currentGoals) { for (GoalNode<T> goal : currentGoals) {
goal.enterScope(); goal.enterScope();
signature.forEach(goal::declareVariable); signature.forEach(goal::declareVariable);
...@@ -694,8 +725,10 @@ public class Interpreter<T> extends DefaultASTVisitor<Object> ...@@ -694,8 +725,10 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
GoalNode<T> selectedGoalNode = stateStack.peek().getSelectedGoalNode(); GoalNode<T> selectedGoalNode = stateStack.peek().getSelectedGoalNode();
if (selectedGoalNode != null) { if (selectedGoalNode != null) {
assert stateStack.peek().getGoals().contains(selectedGoalNode); assert stateStack.peek().getGoals().contains(selectedGoalNode);
return selectedGoalNode;
} else {
throw new IllegalStateException();
} }
return selectedGoalNode;
} catch (IllegalStateException e) { } catch (IllegalStateException e) {
if (strictMode) if (strictMode)
throw e; throw e;
......
package edu.kit.iti.formal.psdbg.interpreter.data; package edu.kit.iti.formal.psdbg.interpreter.data;
import edu.kit.iti.formal.psdbg.parser.DefaultASTVisitor;
import edu.kit.iti.formal.psdbg.parser.ast.*; import edu.kit.iti.formal.psdbg.parser.ast.*;
import lombok.AllArgsConstructor;
import lombok.Data; import lombok.Data;
import lombok.Getter; import lombok.Getter;
import lombok.RequiredArgsConstructor; import lombok.RequiredArgsConstructor;
...@@ -9,47 +11,102 @@ import java.io.File; ...@@ -9,47 +11,102 @@ import java.io.File;
@Data @Data
@RequiredArgsConstructor @RequiredArgsConstructor
public class SavePoint { @AllArgsConstructor
public class SavePoint {
@Getter
private final String name;
private int startOffset = -1;
private int endOffset = -1;
@Getter
private int lineNumber = -1;
private ForceOption force = ForceOption.YES;
private final String savepointName; public SavePoint(CallStatement call) {
if (isSaveCommand(call)) {
private int start = -1;
private int end = -1;
public SavePoint(CallStatement call){
if(isSaveCommand(call)){
Parameters p = call.getParameters(); Parameters p = call.getParameters();
savepointName = ((StringLiteral) p.get(new Variable("#2"))).getText(); name = evalAsText(p, "#2", "not-available");
start = call.getRuleContext().getStart().getStartIndex(); force = ForceOption.valueOf(evalAsText(p, "force", "yes").toUpperCase());
end = call.getRuleContext().getStart().getStopIndex();
}
throw new IllegalArgumentException(call.getCommand()+" is not a save statement");
}
public static boolean isSaveCommand(CallStatement call){ try {
return (call.getCommand().equals("save")); startOffset = call.getRuleContext().getStart().getStartIndex();
endOffset = call.getRuleContext().getStart().getStopIndex();
lineNumber = call.getRuleContext().getStart().getLine();
} catch (NullPointerException npe) {
}
} else {
throw new IllegalArgumentException(call.getCommand() + " is not a save statement");
}
} }
public File getProofFile(File dir){ public static boolean isSaveCommand