Commit b3b1128d authored by Alexander Weigl's avatar Alexander Weigl

Merge branch 'master' of git.scc.kit.edu:xt9634/ProofScriptParser

* 'master' of git.scc.kit.edu:xt9634/ProofScriptParser:
  First footsteps towards interactive mode
  interim
  interim
  better branching labels
parents 47cf84ca 73c88fff
Pipeline #15250 passed with stages
in 10 minutes and 20 seconds
......@@ -4,9 +4,9 @@
# Execute this in this folder.
# Set to key/key/deployment/components/
#COMPONENTS=${COMPONENTS:-/home/sarah/Documents/KIT_Mitarbeiter/KeYDevelopment/KeYGitDir/key/key/deployment/components/}
COMPONENTS=${COMPONENTS:-/home/sarah/Documents/KIT_Mitarbeiter/KeYDevelopment/KeYGitDir/key/key/deployment/components/}
#COMPONENTS=$HOME/work/key/key/deployment/components/
COMPONENTS=lib/components/
#COMPONENTS=lib/components/
......
......@@ -3,6 +3,7 @@ package edu.kit.iti.formal.psdbg;
import de.uka.ilkd.key.proof.Goal;
import de.uka.ilkd.key.proof.Node;
import de.uka.ilkd.key.proof.Proof;
import lombok.val;
import org.apache.commons.lang.ArrayUtils;
import org.key_project.util.collection.ImmutableList;
......@@ -23,7 +24,6 @@ public class LabelFactory {
public static String RANGE_SEPARATOR = " -- ";
/**
* Create Label for goalview according to function that is passed.
* The following functions can be given:
......@@ -58,7 +58,20 @@ public class LabelFactory {
}
public static String getBranchingLabel(Node node) {
return constructLabel(node, n -> n.getNodeInfo().getBranchLabel());
StringBuilder sb = new StringBuilder();
while (node != null) {
val p = node.parent();
if (p != null && p.childrenCount() != 1) {
val branchLabel = node.getNodeInfo().getBranchLabel();
sb.append(branchLabel != null && !branchLabel.isEmpty()
? branchLabel
: "#" + p.getChildNr(node))
.append(SEPARATOR);
}
node = p;
}
sb.append("$$");
return sb.toString();
}
public static String getNameLabel(Node node) {
......
......@@ -26,6 +26,8 @@ import edu.kit.iti.formal.psdbg.parser.types.Type;
import edu.kit.iti.formal.psdbg.termmatcher.MatcherFacade;
import edu.kit.iti.formal.psdbg.termmatcher.Matchings;
import edu.kit.iti.formal.psdbg.termmatcher.mp.MatchPath;
import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger;
import org.key_project.util.collection.ImmutableList;
import java.util.*;
......@@ -39,6 +41,8 @@ import java.util.regex.Pattern;
* @author S. Grebing
*/
public class KeYMatcher implements MatcherApi<KeyData> {
private static final Logger LOGGER = LogManager.getLogger(KeYMatcher.class);
private static final Name CUT_TACLET_NAME = new Name("cut");
private ScriptApi scrapi;
private KeyInterpreter interpreter;
......@@ -244,6 +248,7 @@ public class KeYMatcher implements MatcherApi<KeyData> {
Matchings m = MatcherFacade.matches(data, currentState.getData().getNode().sequent());
if (m.isEmpty()) {
LOGGER.error("currentState has no match= " + currentState.getData().getNode().sequent());
return Collections.emptyList();
} else {
Map<String, MatchPath> firstMatch = m.first();
......@@ -260,11 +265,11 @@ public class KeYMatcher implements MatcherApi<KeyData> {
Value<String> value = toValueTerm(currentState.getData(), matched);
va.declare(s, value.getType());
va.assign(s, value);
System.out.println("Variable " + s + " : " + value);
LOGGER.error("Variables to match " + s + " : " + value);
}
}
List<VariableAssignment> retList = new LinkedList();
System.out.println("Matched Variables " + va.toString());
LOGGER.error("Matched Variables " + va.toString());
retList.add(va);
return retList;
}
......
package edu.kit.iti.formal.psdbg.interpreter.data;
import de.uka.ilkd.key.control.KeYEnvironment;
import de.uka.ilkd.key.java.Label;
import de.uka.ilkd.key.java.SourceElement;
import de.uka.ilkd.key.proof.Goal;
import de.uka.ilkd.key.proof.Node;
......@@ -11,7 +10,6 @@ import lombok.*;
import java.util.HashSet;
import java.util.Set;
import java.util.function.Function;
/**
* @author Alexander Weigl
......@@ -52,6 +50,7 @@ public class KeyData {
env = environment;
this.proof = proof;
closedNode = proof.closed();
}
public KeyData(Node root, KeYEnvironment environment, Proof proof) {
......
......@@ -74,6 +74,7 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
}
} catch (Exception e) {
if (e.getClass().equals(ScriptException.class)) {
System.out.println("e.getMessage() = " + e.getMessage());
throw new ScriptCommandNotApplicableException(e, c, map);
} else {
......
......@@ -84,6 +84,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
* starting point is a statement list
*/
public void interpret(ProofScript script) {
enterScope(script);
if (stateStack.empty()) {
throw new InterpreterRuntimeException("no state on stack. call newState before interpret");
}
......@@ -96,6 +97,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
}
script.accept(this);
exitScope(script);
}
/**
......
......@@ -32,7 +32,6 @@ public abstract class Blocker {
@Override
public boolean test(ASTNode node) {
Evaluator<T> evaluator = new Evaluator<>(interpreter.getSelectedNode().getAssignments(), interpreter.getSelectedNode());
for (Breakpoint brkpt : getBreakpoints()) {
// check file name
if (brkpt.getSourceName().equals(node.getOrigin())) {
......@@ -42,6 +41,7 @@ public abstract class Blocker {
if (brkpt.getConditionAst() == null) {
return true; // no condition ==> trigger
} else { // if there is a condition, we check:
Evaluator<T> evaluator = new Evaluator<>(interpreter.getSelectedNode().getAssignments(), interpreter.getSelectedNode());
val v = evaluator.eval(brkpt.getConditionAst());
if (v.getType() != SimpleType.BOOL)
throw new InterpreterRuntimeException(
......
......@@ -134,6 +134,7 @@ public class DebuggerFramework<T> {
private void run() {
try {
interpreter.interpret(mainScript);
//dummyproofnode
succeedListener.accept(this);
} catch (Exception e) {
error = e;
......
......@@ -36,6 +36,10 @@ public class PTreeNode<T> {
private boolean atomic;
private boolean isFirstNode = false;
private boolean isLastNode = false;
@Nullable
private PTreeNode<T> stepInto;
......
......@@ -43,6 +43,9 @@ public class StateWrapper<T> implements InterpreterObserver<T> {
private Consumer<PTreeNode<T>> emitNode = (n) -> {
};
@Getter
private ProofScript root;
@Nullable
private PTreeNode<T> lastNode;
......@@ -74,6 +77,7 @@ public class StateWrapper<T> implements InterpreterObserver<T> {
}
public void createRoot(ProofScript node) {
this.root = node;
emitNode.accept(createNode(node));
}
......@@ -81,6 +85,12 @@ public class StateWrapper<T> implements InterpreterObserver<T> {
emitNode.accept(createNode(node));
}
public void createSentinel() {
PTreeNode<T> node = createNode(getRoot());
node.setLastNode(true);
emitNode.accept(node);
}
public State<T> getInterpreterStateCopy() {
return interpreter.getCurrentState().copy();
......@@ -145,6 +155,16 @@ public class StateWrapper<T> implements InterpreterObserver<T> {
return null;
}
@Override
public Void visit(ProofScript proofScript) {
LOGGER.error("exit {}", proofScript.accept(new ShortCommandPrinter()));
if (proofScript.equals(root)) {
createSentinel();
}
return null;
}
@Override
public Void visit(Statements statements) {
return null;
......
package edu.kit.iti.formal.psdbg.examples.java.bubbleSort;
import edu.kit.iti.formal.psdbg.examples.JavaExample;
public class BubbleSortExample extends JavaExample {
public BubbleSortExample() {
setName("Bubble Sort");
setJavaFile(this.getClass().getResource("Bubblesort.java"));
defaultInit(getClass());
System.out.println(this);
}
}
......@@ -127,6 +127,9 @@ public class DebuggerMain implements Initializable {
@FXML
private CheckMenuItem miProofTree;
@FXML
private Button btnIM;
private JavaArea javaArea = new JavaArea();
private DockNode javaAreaDock = new DockNode(javaArea, "Java Source",
......@@ -148,6 +151,8 @@ public class DebuggerMain implements Initializable {
private DockNode commandHelpDock = new DockNode(commandHelp, "DebuggerCommand Help");
private InteractiveModeController interactiveModeController;
@FXML
private Menu examplesMenu;
......@@ -193,6 +198,7 @@ public class DebuggerMain implements Initializable {
Events.register(this);
model.setDebugMode(false);
scriptController = new ScriptController(dockStation);
interactiveModeController = new InteractiveModeController(scriptController);
inspectionViewsController = new InspectionViewsController(dockStation);
activeInspectorDock = inspectionViewsController.getActiveInterpreterTabDock();
//register the welcome dock in the center
......@@ -493,10 +499,12 @@ public class DebuggerMain implements Initializable {
Platform.runLater(() -> {
scriptController.getDebugPositionHighlighter().remove();
statusBar.publishSuccessMessage("Interpreter finished.");
btnIM.setDisable(false);
assert model.getDebuggerFramework() != null;
PTreeNode<KeyData> statePointer = model.getDebuggerFramework().getStatePointer();
State<KeyData> lastState = statePointer.getStateAfterStmt();
getInspectionViewsController().getActiveInspectionViewTab().activate(statePointer, lastState);
});
}
......@@ -834,10 +842,27 @@ public class DebuggerMain implements Initializable {
stop.setText("Reload");
}
/* public void handle(Events.TacletApplicationEvent tap){
TacletApp app = tap.getApp();
Goal currentGoal = tap.getCurrentGoal();
ImmutableList<Goal> apply = currentGoal.apply(app);
}*/
public void newScript(ActionEvent actionEvent) {
scriptController.newScript();
}
@FXML
public void interactiveMode(ActionEvent actionEvent) {
interactiveModeController.setActivated(true);
interactiveModeController.start(getFacade().getProof(), getInspectionViewsController().getActiveInspectionViewTab().getModel());
}
@FXML
public void showWelcomeDock(ActionEvent actionEvent) {
if (!welcomePaneDock.isDocked() && !welcomePaneDock.isFloating()) {
......@@ -971,15 +996,19 @@ public class DebuggerMain implements Initializable {
ptree.setRoot(pnode);
ptree.setDeactivateRefresh(true);
Set<Node> sentinels = proof.getSubtreeGoals(pnode)
.stream()
.map(Goal::node)
.collect(Collectors.toSet());
ptree.getSentinels().addAll(sentinels);
ptree.expandRootToLeaves();
//TODO set coloring of starting and end node
DockNode node = new DockNode(ptree, "Proof Tree for Step Into: " +
original.getStatement().accept(new ShortCommandPrinter())
);
node.dock(dockStation, DockPos.CENTER, getActiveInspectorDock());
node.dock(dockStation, DockPos.CENTER, scriptController.getOpenScripts().get(getScriptController().getMainScript().getScriptArea()));
}
}
//endregion
......
......@@ -2,6 +2,7 @@ package edu.kit.iti.formal.psdbg.gui.controller;
import com.google.common.eventbus.EventBus;
import de.uka.ilkd.key.logic.PosInOccurrence;
import de.uka.ilkd.key.proof.Goal;
import de.uka.ilkd.key.proof.Node;
import de.uka.ilkd.key.rule.TacletApp;
import edu.kit.iti.formal.psdbg.gui.controls.ScriptArea;
......@@ -47,8 +48,11 @@ public class Events {
@RequiredArgsConstructor
public static class TacletApplicationEvent {
private final TacletApp app;
private final PosInOccurrence pio;
private final Goal currentGoal;
}
@Data
......
package edu.kit.iti.formal.psdbg.gui.controller;
import com.google.common.eventbus.Subscribe;
import de.uka.ilkd.key.control.AbstractUserInterfaceControl;
import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
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.Node;
import de.uka.ilkd.key.proof.Proof;
import edu.kit.iti.formal.psdbg.LabelFactory;
import edu.kit.iti.formal.psdbg.gui.controls.ScriptArea;
import edu.kit.iti.formal.psdbg.gui.controls.ScriptController;
import edu.kit.iti.formal.psdbg.gui.model.InspectionModel;
import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
import edu.kit.iti.formal.psdbg.interpreter.exceptions.ScriptCommandNotApplicableException;
import edu.kit.iti.formal.psdbg.parser.PrettyPrinter;
import edu.kit.iti.formal.psdbg.parser.ast.*;
import javafx.beans.property.BooleanProperty;
import javafx.beans.property.SimpleBooleanProperty;
import javafx.collections.ObservableList;
import lombok.Getter;
import lombok.RequiredArgsConstructor;
import lombok.Setter;
import lombok.val;
import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger;
import org.key_project.util.collection.ImmutableList;
import java.util.HashMap;
import java.util.List;
import java.util.Map;
import java.util.stream.Collectors;
@Getter
@Setter
@RequiredArgsConstructor
public class InteractiveModeController {
private static final Logger LOGGER = LogManager.getLogger(InteractiveModeController.class);
private final Map<Node, Statements> cases = new HashMap<>();
private BooleanProperty activated = new SimpleBooleanProperty();
private final ScriptController scriptController;
private ScriptArea scriptArea;
private InspectionModel model;
public InteractiveModeController() {
}
public void start() {
public void start(Proof currentProof, InspectionModel model) {
Events.register(this);
cases.clear();
activated.set(true);
currentProof.getSubtreeGoals(currentProof.root()).forEach(goal -> {
cases.put(goal.node(), new Statements());
});
this.scriptArea = scriptController.newScript();
this.model = model;
}
public void stop() {
Events.unregister(this);
String c = getCasesAsString();
Events.fire(new Events.InsertAtTheEndOfMainScript(c));
activated.set(false);
}
@Subscribe
public void handle(Events.TacletApplicationEvent tap) {
LOGGER.debug("Handling {}", tap);
String tapName = tap.getApp().taclet().displayName();
Goal g = tap.getCurrentGoal();
SequentFormula seqForm = tap.getPio().sequentFormula();
//transform term to parsable string representation
String term = edu.kit.iti.formal.psdbg.termmatcher.Utils.toPrettyTerm(seqForm.formula());
Parameters params = new Parameters();
params.put(new Variable("formula"), new TermLiteral(term));
VariableAssignment va = new VariableAssignment(null);
CallStatement call = new CallStatement(tapName, params);
// Insert into the right cases
Node currentNode = null;
Node currentNode = g.node();
cases.get(findRoot(currentNode)).add(call);
// How to Play this on the Proof?
// How to Build a new StatePointer? Is it still possible?
// or only at #stop()?
String c = getCasesAsString();
scriptArea.setText("" +
"//Preview \n" + c);
applyRule(call, g);
}
private Node findRoot(Node cur) {
......@@ -82,6 +119,7 @@ public class InteractiveModeController {
));
gcs.setGuard(m);
gcs.setBody(v);
c.getCases().add(gcs);
});
PrettyPrinter pp = new PrettyPrinter();
......@@ -89,6 +127,50 @@ public class InteractiveModeController {
return pp.toString();
}
private void applyRule(CallStatement call, Goal g) {
ObservableList<GoalNode<KeyData>> goals = model.getGoals();
GoalNode<KeyData> expandedNode;
List<GoalNode<KeyData>> collect = goals.stream().filter(keyDataGoalNode -> keyDataGoalNode.getData().getGoal().equals(g)).collect(Collectors.toList());
if (collect.isEmpty() || collect.size() > 1) {
throw new RuntimeException("Interactive Rule can not be applied, can not find goal in goal list");
} else {
expandedNode = collect.get(0);
}
RuleCommand c = new RuleCommand();
// KeyData kd = g.getData();
Map<String, String> map = new HashMap<>();
// call.getParameters().forEach((k, v) -> map.put(k.getIdentifier(), v.getData().toString()));
LOGGER.info("Execute {} with {}", call, map);
try {
KeyData kd = expandedNode.getData();
map.put("#2", call.getCommand());
EngineState estate = new EngineState(g.proof());
estate.setGoal(g);
RuleCommand.Parameters cc = c.evaluateArguments(estate, map); //reflection exception
AbstractUserInterfaceControl uiControl = new DefaultUserInterfaceControl();
c.execute(uiControl, cc, estate);
ImmutableList<Goal> ngoals = g.proof().getSubtreeGoals(g.node());
goals.remove(expandedNode);
for (Goal newGoalNode : ngoals) {
KeyData kdn = new KeyData(kd, newGoalNode.node());
goals.add(new GoalNode<>(expandedNode, kdn, kdn.getNode().isClosed()));
}
} catch (Exception e) {
if (e.getClass().equals(ScriptException.class)) {
System.out.println("e.getMessage() = " + e.getMessage());
throw new ScriptCommandNotApplicableException(e, c, map);
} else {
throw new RuntimeException(e);
}
}
}
public boolean isActivated() {
return activated.get();
}
......
......@@ -170,8 +170,14 @@ public class InspectionView extends BorderPane {
public void activate(PTreeNode<KeyData> node, State<KeyData> lastState) {
InspectionModel im = model.get();
im.getGoals().setAll(lastState.getGoals());
im.setSelectedGoalNodeToShow(lastState.getSelectedGoalNode());
if (lastState != null && lastState.getGoals() != null) {
im.getGoals().setAll(lastState.getGoals());
im.setSelectedGoalNodeToShow(lastState.getSelectedGoalNode());
} else {
lastState = node.getStepInvOver().getStateBeforeStmt();
im.getGoals().setAll(lastState.getGoals());
im.setSelectedGoalNodeToShow(lastState.getSelectedGoalNode());
}
//Experimental
List<PTreeNode<KeyData>> ctxn = node.getContextNodes();
......
......@@ -47,6 +47,8 @@ public class ProofTree extends BorderPane {
@FXML
private TreeView<TreeNode> treeProof;
public void addNodeColor() {
}
private ContextMenu contextMenu;
@Getter @Setter
......@@ -123,6 +125,10 @@ public class ProofTree extends BorderPane {
init();
}
public void expandRootToLeaves() {
expandRootToLeaves(getTreeProof().getRoot());
}
/**
* From https://www.programcreek.com/java-api-examples/index.php?api=javafx.scene.control.TreeItem
*
......@@ -137,6 +143,9 @@ public class ProofTree extends BorderPane {
}
}
public TreeView<TreeNode> getTreeProof() {
return treeProof;
}
private static void expandRootToLeaves(TreeItem candidate) {
if (candidate != null) {
if (!candidate.isLeaf()) {
......@@ -266,8 +275,7 @@ public class ProofTree extends BorderPane {
});
MenuItem expandAllNodes = new MenuItem("Expand Tree");
expandAllNodes.setOnAction(event -> {
expandAllNodes.setOnAction((event) -> {
expandRootToLeaves(treeProof.getRoot());
});
......
......@@ -318,7 +318,7 @@ public class TacletContextMenu extends ContextMenu {
//System.out.println("event = [" + event + "]");
Events.fire(new Events.TacletApplicationEvent(event, pos.getPosInOccurrence()));
Events.fire(new Events.TacletApplicationEvent(event, pos.getPosInOccurrence(), goal));
}
/**
......
......@@ -40,6 +40,7 @@ public class DebuggerMainModel {
private ObjectProperty<InterpreterThreadState> interpreterState = new SimpleObjectProperty<>(this, "interpreterState",
InterpreterThreadState.NO_THREAD);
/**
* True, iff the execution is not possible
*/
......
......@@ -3,4 +3,5 @@ edu.kit.iti.formal.psdbg.examples.fol.FirstOrderLogicExample
edu.kit.iti.formal.psdbg.examples.java.simple.JavaSimpleExample
edu.kit.iti.formal.psdbg.examples.java.transitive.PaperExample
edu.kit.iti.formal.psdbg.examples.java.dpqs.DualPivotExample
edu.kit.iti.formal.psdbg.examples.agatha.AgathaExample
\ No newline at end of file
edu.kit.iti.formal.psdbg.examples.agatha.AgathaExample
edu.kit.iti.formal.psdbg.examples.java.bubbleSort.BubbleSortExample
\ No newline at end of file
script test(){
impRight;
andLeft;
notLeft;
repeat { andLeft; }
exLeft;
andLeft;
eqSymm formula = `agatha = butler`;
nnf_imp2or formula=`\foral S w6;(hates(agatha,w6) -> hates(butler,w6))`;
}
script SolveAgathaRiddle_1() {
impRight;
andLeft;
......
class Bubblesort {
/*@
@ public normal_behaviour
@ requires arr != null;
@ requires arr.length > 0;
@ ensures (\forall int i, j; 0 <= i && i < j && j < arr.length; arr[i] <= arr[j]);
@ assignable arr[*];
@*/
public int[] bubbleSort(int[] arr) {
int temp = 0;
/*@
@ loop_invariant 0 <= i && i <= arr.length;
@ loop_invariant (\forall int a,b; a >= arr.length - i && b <= arr.length && a < b && i > 0; arr[a] <= arr[b]);
@ assignable arr[*], temp;
@ decreases arr.length - i;
@*/
for(int i=0; i < arr.length; i++){
/*@
@ loop_invariant 1 <= j && j <= arr.length - i + 1;