Commit 4dbfb023 authored by Alexander Weigl's avatar Alexander Weigl

fix bugs from lulu

parent e8a49bad
Pipeline #15832 passed with stages
in 9 minutes and 55 seconds
......@@ -22,6 +22,7 @@ import lombok.Getter;
import java.io.File;
import java.io.IOException;
import java.security.Key;
import java.util.Arrays;
import java.util.Collection;
import java.util.List;
......@@ -168,12 +169,12 @@ public class InterpreterBuilder {
public InterpreterBuilder ignoreLines(Set<Integer> lines) {
CommandHandler<KeyData> ignoreHandler = new CommandHandler<KeyData>() {
@Override
public boolean handles(CallStatement call) throws IllegalArgumentException {
public boolean handles(CallStatement call, KeyData data) throws IllegalArgumentException {
return lines.contains(call.getStartPosition().getLineNumber());
}
@Override
public void evaluate(Interpreter<KeyData> interpreter, CallStatement call, VariableAssignment params) {
public void evaluate(Interpreter<KeyData> interpreter, CallStatement call, VariableAssignment params, KeyData data) {
//System.out.println("InterpreterBuilder.evaluate");
}
};
......@@ -184,12 +185,12 @@ public class InterpreterBuilder {
public InterpreterBuilder ignoreLinesUntil(final int caretPosition) {
CommandHandler<KeyData> ignoreHandler = new CommandHandler<KeyData>() {
@Override
public boolean handles(CallStatement call) throws IllegalArgumentException {
public boolean handles(CallStatement call, KeyData data) throws IllegalArgumentException {
return call.getRuleContext().getStart().getStartIndex() < caretPosition;
}
@Override
public void evaluate(Interpreter<KeyData> interpreter, CallStatement call, VariableAssignment params) {
public void evaluate(Interpreter<KeyData> interpreter, CallStatement call, VariableAssignment params, KeyData data) {
System.out.println("InterpreterBuilder.evaluate");
}
};
......
......@@ -245,10 +245,10 @@ public class KeYMatcher implements MatcherApi<KeyData> {
//System.out.println("State that will be matched " + currentState.getData().getNode().sequent() + " with pattern " + data);
//System.out.println("Signature " + sig.toString());
Matchings m = MatcherFacade.matches(data, currentState.getData().getNode().sequent());
Matchings m = MatcherFacade.matches(data, currentState.getData().getNode().sequent(), false);
if (m.isEmpty()) {
LOGGER.error("currentState has no match= " + currentState.getData().getNode().sequent());
LOGGER.debug("currentState has no match= " + currentState.getData().getNode().sequent());
return Collections.emptyList();
} else {
Map<String, MatchPath> firstMatch = m.first();
......
......@@ -48,6 +48,7 @@ public class KeyData {
public KeyData(Goal g, KeYEnvironment environment, Proof proof) {
goal = g;
node = goal.node();
env = environment;
this.proof = proof;
closedNode = proof.closed();
......
......@@ -3,8 +3,11 @@ package edu.kit.iti.formal.psdbg.interpreter.exceptions;
import de.uka.ilkd.key.macros.scripts.RuleCommand;
import java.util.Map;
/**
* Exception for not applicable Rules
* Exception for not applicable rules
*
* @author grebing
*/
public class ScriptCommandNotApplicableException extends InterpreterRuntimeException {
......@@ -17,13 +20,16 @@ public class ScriptCommandNotApplicableException extends InterpreterRuntimeExcep
}
public ScriptCommandNotApplicableException(Exception e, RuleCommand c, Map<String, String> params) {
StringBuffer sb = new StringBuffer();
super(createMessage(c, params), e);
}
private static String createMessage(RuleCommand c, Map<String, String> params) {
StringBuilder sb = new StringBuilder();
sb.append("Call " + c.getName() + " with parameters ");
for (String s : params.keySet()) {
sb.append(s + " " + params.get(s));
sb.append(s).append(" ").append(params.get(s));
}
sb.append(" was not applicable");
System.out.println(e.getMessage() + sb.toString());
return sb.toString();
}
}
......@@ -4,9 +4,7 @@ import de.uka.ilkd.key.api.KeYApi;
import de.uka.ilkd.key.control.AbstractUserInterfaceControl;
import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
import de.uka.ilkd.key.macros.ProofMacro;
import de.uka.ilkd.key.macros.ProofMacroFinishedInfo;
import de.uka.ilkd.key.proof.Goal;
import de.uka.ilkd.key.proof.Node;
import edu.kit.iti.formal.psdbg.interpreter.Interpreter;
import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
......@@ -21,7 +19,6 @@ import org.key_project.util.collection.ImmutableList;
import java.util.Collection;
import java.util.HashMap;
import java.util.Iterator;
import java.util.Map;
/**
......@@ -46,18 +43,21 @@ public class MacroCommandHandler implements CommandHandler<KeyData> {
@Override
public boolean handles(CallStatement call) throws IllegalArgumentException {
public boolean handles(CallStatement call, KeyData data) throws IllegalArgumentException {
return macros.containsKey(call.getCommand());
}
@Override
public void evaluate(Interpreter<KeyData> interpreter,
CallStatement call,
VariableAssignment params) {
VariableAssignment params, KeyData data) {
long startTime = System.currentTimeMillis();
//ProofMacro m = macros.get(call.getCommand());
ProofMacro macro = KeYApi.getMacroApi().getMacro(call.getCommand());
ProofMacroFinishedInfo info = ProofMacroFinishedInfo.getDefaultInfo(macro,
/*ProofMacroFinishedInfo info = ProofMacroFinishedInfo.getDefaultInfo(macro,
interpreter.getCurrentState().getSelectedGoalNode().getData().getProof());
*/
State<KeyData> state = interpreter.getCurrentState();
GoalNode<KeyData> expandedNode = state.getSelectedGoalNode();
......@@ -68,37 +68,22 @@ public class MacroCommandHandler implements CommandHandler<KeyData> {
//uiControl.taskStarted(new DefaultTaskStartedInfo(TaskStartedInfo.TaskKind.Macro, macro.getName(), 0));
synchronized (macro) {
AbstractUserInterfaceControl uiControl = new DefaultUserInterfaceControl();
info = macro.applyTo(uiControl, expandedNode.getData().getNode(), null, uiControl);
macro.applyTo(uiControl, expandedNode.getData().getNode(), null, uiControl);
ImmutableList<Goal> ngoals = expandedNode.getData().getProof().getSubtreeGoals(expandedNode.getData().getNode());
state.getGoals().remove(expandedNode);
state.setSelectedGoalNode(null);
if (ngoals.isEmpty()) {
Node start = expandedNode.getData().getNode();
//start.leavesIterator()
// Goal s = kd.getProof().getGoal(start);
Iterator<Node> nodeIterator = start.leavesIterator();
while (nodeIterator.hasNext()) {
Node n = nodeIterator.next();
LOGGER.error(n.isClosed());
}
} else {
for (Goal g : ngoals) {
KeyData kdn = new KeyData(expandedNode.getData(), g.node());
state.getGoals().add(new GoalNode<>(expandedNode, kdn, kdn.isClosedNode()));
}
if (!ngoals.isEmpty()) {
ngoals.stream()
.map(g -> new KeyData(expandedNode.getData(), g))
.map(kd -> new GoalNode<>(expandedNode, kd, false))
.forEachOrdered(gn -> state.getGoals().add(gn));
assert !state.getGoals().contains(expandedNode);
}
}
} catch (InterruptedException e) {
e.printStackTrace();
} catch (Exception e) {
e.printStackTrace();
} finally {
LOGGER.debug("Execution of {} took {} ms", call.getCommand(), (System.currentTimeMillis() - startTime));
}
}
}
......@@ -47,7 +47,7 @@ public class ProofScriptCommandBuilder implements CommandHandler<KeyData> {
}
@Override
public boolean handles(CallStatement call) {
public boolean handles(CallStatement call, KeyData data) {
return commands.containsKey(call.getCommand());
}
......@@ -55,7 +55,7 @@ public class ProofScriptCommandBuilder implements CommandHandler<KeyData> {
@Override
public void evaluate(Interpreter<KeyData> interpreter,
CallStatement call,
VariableAssignment params) {
VariableAssignment params, KeyData data) {
ProofScriptCommand c = commands.get(call.getCommand());
State<KeyData> state = interpreter.getCurrentState();
GoalNode<KeyData> expandedNode = state.getSelectedGoalNode();
......
......@@ -7,12 +7,12 @@ import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
public class RigidRuleCommandHandler implements CommandHandler<KeyData> {
@Override
public boolean handles(CallStatement call) throws IllegalArgumentException {
public boolean handles(CallStatement call, KeyData data) throws IllegalArgumentException {
return true;
}
@Override
public void evaluate(Interpreter<KeyData> interpreter, CallStatement call, VariableAssignment params) {
public void evaluate(Interpreter<KeyData> interpreter, CallStatement call, VariableAssignment params, KeyData data) {
// Evaluator evaluator = new Evaluator(g.getAssignments(), g);
// evaluator.setMatcher(interpreter.getMatcherApi());
......
......@@ -2,11 +2,20 @@ package edu.kit.iti.formal.psdbg.interpreter.funchdl;
import de.uka.ilkd.key.control.AbstractUserInterfaceControl;
import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.PosInOccurrence;
import de.uka.ilkd.key.logic.PosInTerm;
import de.uka.ilkd.key.logic.SequentFormula;
import de.uka.ilkd.key.macros.scripts.EngineState;
import de.uka.ilkd.key.macros.scripts.RuleCommand;
import de.uka.ilkd.key.macros.scripts.ScriptException;
import de.uka.ilkd.key.proof.Goal;
import de.uka.ilkd.key.proof.Proof;
import de.uka.ilkd.key.proof.RuleAppIndex;
import de.uka.ilkd.key.proof.rulefilter.TacletFilter;
import de.uka.ilkd.key.rule.Rule;
import de.uka.ilkd.key.rule.Taclet;
import de.uka.ilkd.key.rule.TacletApp;
import edu.kit.iti.formal.psdbg.interpreter.Interpreter;
import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
......@@ -19,9 +28,12 @@ import lombok.RequiredArgsConstructor;
import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger;
import org.key_project.util.collection.ImmutableList;
import org.key_project.util.collection.ImmutableSLList;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Map;
import java.util.Set;
/**
* @author Alexander Weigl
......@@ -39,14 +51,49 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
}
@Override
public boolean handles(CallStatement call) throws IllegalArgumentException {
return rules.containsKey(call.getCommand());
public boolean handles(CallStatement call, KeyData data) throws IllegalArgumentException {
if (rules.containsKey(call.getCommand())) return true;//static/rigid rules
if (data != null) {
Goal goal = data.getGoal();
Set<String> rules = findTaclets(data.getProof(), goal);
return rules.contains(call.getCommand());
}
return false;
}
private Set<String> findTaclets(Proof p, Goal g) {
Services services = p.getServices();
TacletFilter filter = new TacletFilter() {
@Override
protected boolean filter(Taclet taclet) {
return true;
}
};
RuleAppIndex index = g.ruleAppIndex();
index.autoModeStopped();
HashSet<String> set = new HashSet<>();
ImmutableList<TacletApp> allApps = ImmutableSLList.nil();
for (SequentFormula sf : g.node().sequent().antecedent()) {
ImmutableList<TacletApp> apps = index.getTacletAppAtAndBelow(filter,
new PosInOccurrence(sf, PosInTerm.getTopLevel(), true),
services);
apps.forEach(t -> set.add(t.taclet().name().toString()));
}
for (SequentFormula sf : g.node().sequent().succedent()) {
ImmutableList<TacletApp> apps = index.getTacletAppAtAndBelow(filter,
new PosInOccurrence(sf, PosInTerm.getTopLevel(), true),
services);
apps.forEach(t -> set.add(t.taclet().name().toString()));
}
return set;
}
@Override
public void evaluate(Interpreter<KeyData> interpreter,
CallStatement call,
VariableAssignment params) throws IllegalStateException, RuntimeException, ScriptCommandNotApplicableException {
VariableAssignment params,
KeyData data) throws RuntimeException, ScriptCommandNotApplicableException {
if (!rules.containsKey(call.getCommand())) {
throw new IllegalStateException();
}
......
......@@ -4,7 +4,7 @@
<Console name="Console" target="SYSTEM_OUT">
<PatternLayout pattern="[%-5level] %msg%n"/>
</Console>
<File name="F" fileName="debug.log" bufferSize="0" bufferedIO="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"/>
</File>
</Appenders>
......
......@@ -448,9 +448,8 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
MatchEvaluator mEval = new MatchEvaluator(goal.getAssignments(), goal, matcherApi);
mEval.getEntryListeners().addAll(getEntryListeners());
mEval.getExitListeners().addAll(getExitListeners());
exitScope(matchExpression);
matchResult = mEval.eval(matchExpression);
exitScope(matchExpression);
} else {
matchResult = new ArrayList<>();
......
......@@ -168,7 +168,7 @@ public class MatchEvaluator extends DefaultASTVisitor<List<VariableAssignment>>
//TODO extract the results form the matcher in order to retrieve the selection results
} else if (TypeFacade.isTerm(pattern.getType())) {
va = getMatcher().matchSeq(goal, (String) pattern.getData(), sig);
System.out.println("va = " + va);
// System.out.println("va = " + va);
}
return va != null ? va : Collections.emptyList();
}
......
......@@ -150,14 +150,14 @@ public class StateWrapper<T> implements InterpreterObserver<T> {
private class ExitListener extends DefaultASTVisitor<Void> {
@Override
public Void defaultVisit(ASTNode node) {
LOGGER.error("exit {}", node.accept(new ShortCommandPrinter()));
LOGGER.debug("exit {}", node.accept(new ShortCommandPrinter()));
completeLastNode(node);
return null;
}
@Override
public Void visit(ProofScript proofScript) {
LOGGER.error("exit {}", proofScript.accept(new ShortCommandPrinter()));
LOGGER.debug("exit {}", proofScript.accept(new ShortCommandPrinter()));
if (proofScript.equals(root)) {
createSentinel();
......
......@@ -23,7 +23,7 @@ public abstract class BuiltinCommands {
private final String name;
@Override
public boolean handles(CallStatement call) throws IllegalArgumentException {
public boolean handles(CallStatement call, T data) throws IllegalArgumentException {
return name.equals(call.getCommand());
}
}
......@@ -34,7 +34,7 @@ public abstract class BuiltinCommands {
}
@Override
public void evaluate(Interpreter<T> interpreter, CallStatement call, VariableAssignment params) {
public void evaluate(Interpreter<T> interpreter, CallStatement call, VariableAssignment params, T data) {
for (GoalNode<T> gn : interpreter.getCurrentGoals()) {
System.out.format("%s %s%n %s%n", gn == interpreter.getSelectedNode() ? "*" : " ", gn.getData(), gn.getAssignments().asMap());
}
......@@ -51,7 +51,7 @@ public abstract class BuiltinCommands {
* Created by sarah on 5/17/17.
*/
@Override
public void evaluate(Interpreter<String> interpreter, CallStatement call, VariableAssignment params) {
public void evaluate(Interpreter<String> interpreter, CallStatement call, VariableAssignment params, String data) {
Value<BigInteger> val = (Value<BigInteger>) params.getValues().getOrDefault(
new Variable("#2"),
Value.from(2));
......
......@@ -4,6 +4,8 @@ import edu.kit.iti.formal.psdbg.interpreter.Interpreter;
import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
import javax.annotation.Nullable;
/**
* @author Alexander Weigl
* @version 1 (20.05.17)
......@@ -16,16 +18,17 @@ public interface CommandHandler<T> {
* @return
* @throws IllegalArgumentException
*/
boolean handles(CallStatement call) throws IllegalArgumentException;
boolean handles(CallStatement call, @Nullable T data) throws IllegalArgumentException;
/**
* @param interpreter
* @param call
* @param params
* @param data
*/
void evaluate(Interpreter<T> interpreter,
CallStatement call,
VariableAssignment params);
VariableAssignment params, T data);
default boolean isAtomic() {
return true;
......
......@@ -13,7 +13,7 @@ public interface CommandLookup<T> {
boolean isAtomic(CallStatement call);
public CommandHandler getBuilder(CallStatement callStatement);
public CommandHandler<T> getBuilder(CallStatement callStatement, T data);
String getHelp(CallStatement call);
}
......@@ -6,6 +6,7 @@ import edu.kit.iti.formal.psdbg.interpreter.exceptions.NoCallHandlerException;
import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
import lombok.Getter;
import javax.annotation.Nullable;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.List;
......@@ -14,29 +15,30 @@ import java.util.List;
* @author Alexander Weigl
* @version 1 (20.05.17)
*/
public class DefaultLookup implements CommandLookup {
public class DefaultLookup<T> implements CommandLookup<T> {
@Getter
private final List<CommandHandler> builders = new ArrayList<>(1024);
private final List<CommandHandler<T>> builders = new ArrayList<>(1024);
public DefaultLookup() {
}
public DefaultLookup(CommandHandler... cmdh) {
public DefaultLookup(CommandHandler<T>... cmdh) {
builders.addAll(Arrays.asList(cmdh));
}
public void callCommand(Interpreter interpreter,
public void callCommand(Interpreter<T> interpreter,
CallStatement call,
VariableAssignment params) {
CommandHandler b = getBuilder(call);
b.evaluate(interpreter, call, params);
T data = interpreter.getSelectedNode().getData();
CommandHandler b = getBuilder(call, data);
b.evaluate(interpreter, call, params, data);
}
@Override
public boolean isAtomic(CallStatement call) {
try {
CommandHandler cmdh = getBuilder(call);
CommandHandler cmdh = getBuilder(call, null);
if (cmdh != null)
return cmdh.isAtomic();
return true;
......@@ -45,40 +47,34 @@ public class DefaultLookup implements CommandLookup {
}
}
public CommandHandler getBuilder(CallStatement callStatement) {
boolean mayBeEscapedMacro = callStatement.getCommand().contains("_");
List<CommandHandler> foundHandlers = new ArrayList<>();
CommandHandler found = null;
for (CommandHandler b : builders) {
if (b.handles(callStatement)) {
foundHandlers.add(b);
found = b;
private CommandHandler<T> getBuilderImpl(CallStatement callStatement, @Nullable T data) {
for (CommandHandler<T> b : builders) {
if (b.handles(callStatement, data)) {
return b;
}
}
return null;
}
if (found == null && mayBeEscapedMacro) {
@Override
public CommandHandler<T> getBuilder(CallStatement callStatement, @Nullable T data) {
CommandHandler<T> found = getBuilderImpl(callStatement, data);
if (found == null && callStatement.getCommand().contains("_")) {
//if a proof macro contains a "-" character, the proof script language does not support this.
// Therefore we have to check for both versions
// if (mayBeEscapedMacro) {
String command = callStatement.getCommand();
callStatement.setCommand(command.replace("_", "-"));
for (CommandHandler b : builders) {
if (b.handles(callStatement)) {
foundHandlers.add(b);
found = b;
}
}
// weigl, remark: it is bad style to change the call statement!
//callStatement = callStatement.copy();
callStatement.setCommand(callStatement.getCommand().replace("_", "-"));
found = getBuilderImpl(callStatement, data);
}
if (foundHandlers.size() >= 1) return foundHandlers.get(0);
if (found == null)
throw new NoCallHandlerException(callStatement);
return found;
}
@Override
public String getHelp(CallStatement call) {
return getBuilder(call).getHelp(call);
return getBuilder(call, null).getHelp(call);
}
}
......@@ -20,7 +20,7 @@ import java.util.Map;
* @version 1 (21.05.17)
*/
@RequiredArgsConstructor
public class ProofScriptHandler implements CommandHandler {
public class ProofScriptHandler implements CommandHandler<Object> {
private static final String SUFFIX = ".kps";
@Getter
private final Map<String, ProofScript> scripts;
......@@ -76,7 +76,7 @@ public class ProofScriptHandler implements CommandHandler {
}
@Override
public boolean handles(CallStatement call) throws IllegalArgumentException {
public boolean handles(CallStatement call, Object data) throws IllegalArgumentException {
if (scripts.containsKey(call.getCommand()))
return true;
try {
......@@ -88,7 +88,7 @@ public class ProofScriptHandler implements CommandHandler {
}
@Override
public void evaluate(Interpreter interpreter, CallStatement call, VariableAssignment params) {
public void evaluate(Interpreter interpreter, CallStatement call, VariableAssignment params, Object data) {
ProofScript ps = scripts.get(call.getCommand());
//new State
//
......
......@@ -83,7 +83,7 @@ public class InterpreterTest {
}
@Override
public void evaluate(Interpreter interpreter, CallStatement call, VariableAssignment params) {
public void evaluate(Interpreter interpreter, CallStatement call, VariableAssignment params, Object data) {
Map<Variable, Value> m = params.asMap();
Value exp = get(m, "exp", "expected", "#2");
Value act = get(m, "act", "actual", "#3");
......@@ -102,7 +102,7 @@ public class InterpreterTest {
}
@Override
public void evaluate(Interpreter interpreter, CallStatement call, VariableAssignment params) {
public void evaluate(Interpreter interpreter, CallStatement call, VariableAssignment params, Object data) {
Map<Variable, Value> m = params.asMap();
Value<Boolean> exp = get(m, "val", "#2");
Value<String> msg = get(m, "msg", "#3");
......
......@@ -6,6 +6,5 @@ public class AgathaExample extends Example {
public AgathaExample() {
setName("Agatha");
defaultInit(getClass());
System.out.println(this);
}
}
......@@ -10,8 +10,6 @@ public class ContrapositionExample extends Example {
public ContrapositionExample() {
setName("Contraposition");
defaultInit(getClass());
System.out.println(this);
}
}
......@@ -7,7 +7,5 @@ public class BubbleSortExample extends JavaExample {
setName("Bubble Sort");
setJavaFile(this.getClass().getResource("Bubblesort.java"));
defaultInit(getClass());
System.out.println(this);
}
}
......@@ -5,13 +5,8 @@ import edu.kit.iti.formal.psdbg.examples.JavaExample;
public class DualPivotExample extends JavaExample {
public DualPivotExample() {
setName("Dual Pivot Quicksort");
setJavaFile(this.getClass().getResource("DualPivotQuicksort.java"));
defaultInit(getClass());
System.out.println(this);
}
}
......@@ -7,10 +7,6 @@ public class JavaSimpleExample extends JavaExample {
public JavaSimpleExample() {
setName("Simple Java Example");
setJavaFile(this.getClass().getResource("Test.java"));
defaultInit(getClass());
System.out.println(this);
}
}
......@@ -7,11 +7,6 @@ public class SumAndMaxExample extends JavaExample {
public SumAndMaxExample() {
setName("SumAndMax Example");
setJavaFile(this.getClass().getResource("SumAndMax.java"));
defaultInit(getClass());
System.out.println(this);
}
}
......@@ -6,11 +6,7 @@ public class PaperExample extends JavaExample {
public PaperExample() {
setName("Transitive Permutation");
setJavaFile(this.getClass().getResource("Simple.java"));
defaultInit(getClass());
System.out.println(this);
}
}
package edu.kit.iti.formal.psdbg.examples.lulu;
import edu.kit.iti.formal.psdbg.examples.JavaExample;