Commit 68463826 authored by Sarah Grebing's avatar Sarah Grebing
Browse files

StepBack and StepOver first version (TODO: implement platform runtlater adaptor for visitors)

parent f9302e14
Pipeline #11840 failed with stage
in 2 minutes and 37 seconds
...@@ -4,10 +4,7 @@ import de.uka.ilkd.key.proof.init.ProofInputException; ...@@ -4,10 +4,7 @@ import de.uka.ilkd.key.proof.init.ProofInputException;
import de.uka.ilkd.key.speclang.Contract; import de.uka.ilkd.key.speclang.Contract;
import edu.kit.formal.gui.controls.*; import edu.kit.formal.gui.controls.*;
import edu.kit.formal.gui.model.RootModel; import edu.kit.formal.gui.model.RootModel;
import edu.kit.formal.interpreter.Interpreter; import edu.kit.formal.interpreter.*;
import edu.kit.formal.interpreter.InterpreterBuilder;
import edu.kit.formal.interpreter.KeYProofFacade;
import edu.kit.formal.interpreter.ProofTreeController;
import edu.kit.formal.interpreter.data.KeyData; import edu.kit.formal.interpreter.data.KeyData;
import edu.kit.formal.proofscriptparser.Facade; import edu.kit.formal.proofscriptparser.Facade;
import edu.kit.formal.proofscriptparser.ast.ProofScript; import edu.kit.formal.proofscriptparser.ast.ProofScript;
...@@ -102,8 +99,6 @@ public class DebuggerMainWindowController implements Initializable { ...@@ -102,8 +99,6 @@ public class DebuggerMainWindowController implements Initializable {
private File initialDirectory; private File initialDirectory;
/** /**
* Controller for debugging functions * Controller for debugging functions
*/ */
...@@ -172,10 +167,12 @@ public class DebuggerMainWindowController implements Initializable { ...@@ -172,10 +167,12 @@ public class DebuggerMainWindowController implements Initializable {
blocker.getBreakpoints().addAll(change.getSet()); blocker.getBreakpoints().addAll(change.getSet());
});*/ });*/
pc.currentGoalsProperty().addListener((o, old, fresh) -> { /*pc.currentGoalsProperty().addListener((o, old, fresh) -> {
model.currentGoalNodesProperty().setAll(fresh); model.currentGoalNodesProperty().setAll(fresh);
}); });
model.currentSelectedGoalNodeProperty().bind(pc.currentSelectedGoalProperty()); model.currentSelectedGoalNodeProperty().bind(pc.currentSelectedGoalProperty());*/
//model.currentGoalNodesProperty().bind(pc.currentGoalsProperty());
CustomTabPaneSkin skin = new CustomTabPaneSkin(tabPane); CustomTabPaneSkin skin = new CustomTabPaneSkin(tabPane);
...@@ -226,6 +223,20 @@ public class DebuggerMainWindowController implements Initializable { ...@@ -226,6 +223,20 @@ public class DebuggerMainWindowController implements Initializable {
pc.setMainScript(scripts.get(0)); pc.setMainScript(scripts.get(0));
pc.executeScript(this.debugMode.get()); pc.executeScript(this.debugMode.get());
pc.currentGoalsProperty().addListener((o, old, fresh) -> {
if (fresh != null) {
model.currentGoalNodesProperty().setAll(fresh);
}
});
model.currentSelectedGoalNodeProperty().bind(pc.currentSelectedGoalProperty());
/* pc.currentGoalsProperty().addListener((observable, oldValue, newValue) -> {
if(newValue != null) {
model.currentGoalNodesProperty().get().
setAll(pc.currentGoalsProperty());
}
});*/
//highlight signature of main script //highlight signature of main script
tabPane.getSelectedScriptArea().setDebugMark(scripts.get(0).getStartPosition().getLineNumber()); tabPane.getSelectedScriptArea().setDebugMark(scripts.get(0).getStartPosition().getLineNumber());
} catch (RecognitionException e) { } catch (RecognitionException e) {
...@@ -376,16 +387,19 @@ public class DebuggerMainWindowController implements Initializable { ...@@ -376,16 +387,19 @@ public class DebuggerMainWindowController implements Initializable {
public void stepOver(ActionEvent actionEvent) { public void stepOver(ActionEvent actionEvent) {
// blocker.getStepUntilBlock().addAndGet(1); // blocker.getStepUntilBlock().addAndGet(1);
// blocker.unlock(); // blocker.unlock();
pc.stepOver(); PTreeNode newState = pc.stepOver();
// model.currentGoalNodesProperty().setAll(newState.getState().getGoals());
// model.setCurrentSelectedGoalNode(newState.getState().getSelectedGoalNode());
} }
public void stepBack(ActionEvent actionEvent) { public void stepBack(ActionEvent actionEvent) {
pc.stepBack(); PTreeNode newState = pc.stepBack();
// model.currentGoalNodesProperty().setAll(newState.getState().getGoals());
// model.setCurrentSelectedGoalNode(newState.getState().getSelectedGoalNode());
} }
public KeYProofFacade getFacade() { public KeYProofFacade getFacade() {
return facade; return facade;
} }
......
...@@ -4,8 +4,6 @@ import edu.kit.formal.gui.model.RootModel; ...@@ -4,8 +4,6 @@ import edu.kit.formal.gui.model.RootModel;
import edu.kit.formal.interpreter.data.GoalNode; import edu.kit.formal.interpreter.data.GoalNode;
import edu.kit.formal.interpreter.data.KeyData; import edu.kit.formal.interpreter.data.KeyData;
import javafx.beans.property.SimpleListProperty; import javafx.beans.property.SimpleListProperty;
import javafx.beans.value.ChangeListener;
import javafx.beans.value.ObservableValue;
import javafx.fxml.FXML; import javafx.fxml.FXML;
import javafx.fxml.FXMLLoader; import javafx.fxml.FXMLLoader;
import javafx.scene.control.ListCell; import javafx.scene.control.ListCell;
...@@ -52,7 +50,7 @@ public class ListGoalView extends VBox { ...@@ -52,7 +50,7 @@ public class ListGoalView extends VBox {
/** /**
* Set Bindings and listener * Set Bindings and listener
*/ */
public void init() { /* public void init() {
listOfGoalsView.itemsProperty().bind(this.rootModel.currentGoalNodesProperty()); listOfGoalsView.itemsProperty().bind(this.rootModel.currentGoalNodesProperty());
listOfGoalsView.getSelectionModel().selectedItemProperty().addListener(new ChangeListener<GoalNode<KeyData>>() { listOfGoalsView.getSelectionModel().selectedItemProperty().addListener(new ChangeListener<GoalNode<KeyData>>() {
...@@ -63,7 +61,7 @@ public class ListGoalView extends VBox { ...@@ -63,7 +61,7 @@ public class ListGoalView extends VBox {
}); });
} }
*/
private static class GoalNodeCell extends ListCell<GoalNode<KeyData>> { private static class GoalNodeCell extends ListCell<GoalNode<KeyData>> {
......
...@@ -26,6 +26,9 @@ import java.util.concurrent.locks.ReentrantLock; ...@@ -26,6 +26,9 @@ import java.util.concurrent.locks.ReentrantLock;
public class PuppetMaster { public class PuppetMaster {
private final Lock lock = new ReentrantLock(); private final Lock lock = new ReentrantLock();
private final Condition block = lock.newCondition(); private final Condition block = lock.newCondition();
/**
* Properties that are changed, when new states are added using the blocker
*/
private final SimpleObjectProperty<List<GoalNode<KeyData>>> currentGoals = new SimpleObjectProperty<>(); private final SimpleObjectProperty<List<GoalNode<KeyData>>> currentGoals = new SimpleObjectProperty<>();
private final SimpleObjectProperty<GoalNode<KeyData>> currentSelectedGoal = new SimpleObjectProperty<>(); private final SimpleObjectProperty<GoalNode<KeyData>> currentSelectedGoal = new SimpleObjectProperty<>();
private Interpreter<KeyData> puppet; private Interpreter<KeyData> puppet;
...@@ -155,9 +158,9 @@ public class PuppetMaster { ...@@ -155,9 +158,9 @@ public class PuppetMaster {
this.currentGoals.set(currentGoals); this.currentGoals.set(currentGoals);
} }
public SimpleObjectProperty<List<GoalNode<KeyData>>> currentGoalsProperty() { /* public SimpleObjectProperty<List<GoalNode<KeyData>>> currentGoalsProperty() {
return currentGoals; return currentGoals;
} }*/
public Set<Integer> getBreakpoints() { public Set<Integer> getBreakpoints() {
return brkpnts; return brkpnts;
......
...@@ -52,11 +52,14 @@ public class InspectionViewTabPane extends TabPane { ...@@ -52,11 +52,14 @@ public class InspectionViewTabPane extends TabPane {
this.getTabs().add(tab); this.getTabs().add(tab);
} }
//TODO schauen wie Goallist ins model kommt //TODO schauen wie Goallist ins model kommt
public void bindGoalNodesWithCurrentTab(RootModel model) { public void bindGoalNodesWithCurrentTab(RootModel model) {
getActiveInspectionViewTab().getGoalView().itemsProperty().bind(model.currentGoalNodesProperty()); getActiveInspectionViewTab().getGoalView().itemsProperty().bind(model.currentGoalNodesProperty());
model.currentSelectedGoalNodeProperty().addListener((p, old, fresh) -> { model.currentSelectedGoalNodeProperty().addListener((p, old, fresh) -> {
getActiveInspectionViewTab().getGoalView().getSelectionModel().select(fresh); getActiveInspectionViewTab().getGoalView().getSelectionModel().select(fresh);
/* TODO get lines of active statements marked lines /* TODO get lines of active statements marked lines
javaSourceCode.getMarkedLines().clear(); javaSourceCode.getMarkedLines().clear();
javaSourceCode.getMarkedLines().addAll( javaSourceCode.getMarkedLines().addAll(
......
...@@ -3,7 +3,9 @@ package edu.kit.formal.interpreter; ...@@ -3,7 +3,9 @@ package edu.kit.formal.interpreter;
import edu.kit.formal.gui.controller.PuppetMaster; import edu.kit.formal.gui.controller.PuppetMaster;
import edu.kit.formal.interpreter.data.GoalNode; import edu.kit.formal.interpreter.data.GoalNode;
import edu.kit.formal.interpreter.data.KeyData; import edu.kit.formal.interpreter.data.KeyData;
import edu.kit.formal.interpreter.data.State;
import edu.kit.formal.proofscriptparser.Visitor; import edu.kit.formal.proofscriptparser.Visitor;
import edu.kit.formal.proofscriptparser.ast.Position;
import edu.kit.formal.proofscriptparser.ast.ProofScript; import edu.kit.formal.proofscriptparser.ast.ProofScript;
import javafx.beans.property.ListProperty; import javafx.beans.property.ListProperty;
import javafx.beans.property.ReadOnlyBooleanProperty; import javafx.beans.property.ReadOnlyBooleanProperty;
...@@ -24,17 +26,36 @@ public class ProofTreeController { ...@@ -24,17 +26,36 @@ public class ProofTreeController {
* To control stepping * To control stepping
*/ */
private final PuppetMaster blocker = new PuppetMaster(); private final PuppetMaster blocker = new PuppetMaster();
private final SimpleObjectProperty<List<GoalNode<KeyData>>> currentGoals = new SimpleObjectProperty<>(); /**
//= blocker.currentGoalsProperty(); * Goals of the state which is referenced by the statePointer
private final ListProperty<GoalNode<KeyData>> currentGoalList = new SimpleListProperty<>(FXCollections.observableArrayList()); */
private final ListProperty<GoalNode<KeyData>> currentGoals = new SimpleListProperty<>(FXCollections.observableArrayList());
/**
* Selected Goal of the state which is referenced by the statePointer
*/
private final SimpleObjectProperty<GoalNode<KeyData>> currentSelectedGoal = new SimpleObjectProperty<>(); private final SimpleObjectProperty<GoalNode<KeyData>> currentSelectedGoal = new SimpleObjectProperty<>();
//= blocker.currentSelectedGoalProperty();
//new SimpleBooleanProperty(false);
/**
* Service to run interpreter in own thread
*/
private InterpretingService interpreterService = new InterpretingService(blocker); private InterpretingService interpreterService = new InterpretingService(blocker);
/**
* To identify when interpreterservice is running
*/
private ReadOnlyBooleanProperty executeNotPossible = interpreterService.runningProperty(); private ReadOnlyBooleanProperty executeNotPossible = interpreterService.runningProperty();
/**
* Node that is updated whenever a new node is added to the stategraph (this can only happen in debug mode when stepover is invoked)
*/
private SimpleObjectProperty<PTreeNode> nextComputedNode = new SimpleObjectProperty<>(); private SimpleObjectProperty<PTreeNode> nextComputedNode = new SimpleObjectProperty<>();
private SimpleObjectProperty<Position> startHighlightPositionProperty = new SimpleObjectProperty<>();
private SimpleObjectProperty<Position> endHighlightPositionProperty = new SimpleObjectProperty<>();
/** /**
* Visitor to retrieve state graph * Visitor to retrieve state graph
*/ */
...@@ -52,29 +73,42 @@ public class ProofTreeController { ...@@ -52,29 +73,42 @@ public class ProofTreeController {
private Interpreter<KeyData> currentInterpreter; private Interpreter<KeyData> currentInterpreter;
/** /**
* Current State in graph * Pointer to current selected state in graph
*/ */
private PTreeNode statePointer = null; private PTreeNode statePointer = null;
/**
* Teh mainscipt that is executed
*/
private ProofScript mainScript; private ProofScript mainScript;
/** /**
* Add a change listener for the stategraph * Add a change listener for the stategraph, whenever a new node is added it receives an event
*/ */
private GraphChangedListener graphChangedListener = nodeAddedEvent -> { private GraphChangedListener graphChangedListener = nodeAddedEvent -> {
if (statePointer.equals(nodeAddedEvent.getLastPointer())) { if (statePointer.equals(nodeAddedEvent.getLastPointer())) {
//set value of newly computed node
nextComputedNode.setValue(nodeAddedEvent.getAddedNode()); nextComputedNode.setValue(nodeAddedEvent.getAddedNode());
//setNewState(this.statePointer.getState());
} }
}; };
public ProofTreeController() { public ProofTreeController() {
this.currentGoals.bindBidirectional(blocker.currentGoalsProperty());
//get state from blocker, who communicates with interpreter
this.currentSelectedGoal.bindBidirectional(blocker.currentSelectedGoalProperty()); this.currentSelectedGoal.bindBidirectional(blocker.currentSelectedGoalProperty());
//add listener to nextcomputed node, that is updated whenever a new node is added to the stategraph
nextComputedNode.addListener((observable, oldValue, newValue) -> {
//update statepointer
this.statePointer = newValue;
setNewState(this.statePointer.getState());
});
} }
...@@ -91,55 +125,48 @@ public class ProofTreeController { ...@@ -91,55 +125,48 @@ public class ProofTreeController {
} }
//TODO handle endpoint //TODO handle endpoint
//handle inconsistency
/**
* StepOver and return the node to shich the state pointer is pointing to
*
* @return
*/
public PTreeNode stepOver() { public PTreeNode stepOver() {
//get current pointer into stategraph
PTreeNode currentPointer = statePointer; PTreeNode currentPointer = statePointer;
//if pointer is null, we do not have a root yet
if (currentPointer == null) { if (currentPointer == null) {
System.out.println("StatePointer is null"); //ask for root
} else { currentPointer = stateGraphVisitor.rootProperty().get();
if (this.statePointer.getState() != null && this.statePointer.getScriptstmt() != null) { statePointer = currentPointer;
System.out.println("StatePointer is " + currentPointer.getScriptstmt().getNodeName() + currentPointer.getScriptstmt().getStartPosition());
} else {
System.out.println("Possibly root node");
}
PTreeNode nextNode = stateGraphVisitor.getStepOver(currentPointer);
if (nextNode != null) {
this.statePointer = nextNode;
} else {
nextComputedNode.addListener((observable, oldValue, newValue) -> {
this.statePointer = newValue;
System.out.println("Added new Value to Statepointer: " + this.statePointer.getScriptstmt().getNodeName() + this.statePointer.getScriptstmt().getStartPosition());
});
//let interpreter run for one step
blocker.getStepUntilBlock().addAndGet(1);
blocker.unlock();
//stateGraphListener
//this.statePointer = nextNode;
}
} }
PTreeNode nextNode = stateGraphVisitor.getStepOver(currentPointer);
if (nextNode != null) {
return null; this.statePointer = nextNode;
setNewState(statePointer.getState());
} else {
//no next node is present yet
//let interpreter run for one step and let listener handle updating the statepointer
blocker.getStepUntilBlock().addAndGet(1);
blocker.unlock();
}
return statePointer;
} }
//TODO handle endpoint of graph //TODO handle endpoint of graph
/**
* Step Back one Node in the stategraph
* @return
*/
public PTreeNode stepBack() { public PTreeNode stepBack() {
PTreeNode current = statePointer; PTreeNode current = statePointer;
this.statePointer = stateGraphVisitor.getStepBack(current); PTreeNode backState = stateGraphVisitor.getStepBack(current);
if (this.statePointer == null) { this.statePointer = backState;
setNewState(statePointer.getState());
return statePointer;
} else {
this.currentGoals.set(this.statePointer.getState().getGoals());
this.currentSelectedGoal.set(this.statePointer.getState().getSelectedGoalNode());
}
System.out.println("PRED NODE \n\n" + this.statePointer.getState().getSelectedGoalNode().getData().getNode().serialNr() + ":" +
this.statePointer.getScriptstmt().getNodeName() + "@" + this.statePointer.getScriptstmt().getStartPosition() + "\n-------------------\n");
return null;
} }
public PTreeNode stepInto() { public PTreeNode stepInto() {
...@@ -157,20 +184,17 @@ public class ProofTreeController { ...@@ -157,20 +184,17 @@ public class ProofTreeController {
if (!debugMode) { if (!debugMode) {
blocker.getStepUntilBlock().set(-1); blocker.getStepUntilBlock().set(-1);
} else { } else {
this.startHighlightPositionProperty.set(mainScript.getSignature().getStartPosition());
this.endHighlightPositionProperty.set(mainScript.getSignature().getEndPosition());
//build CFG //build CFG
buildControlFlowGraph(mainScript); buildControlFlowGraph(mainScript);
//build StateGraph //build StateGraph
this.stateGraphVisitor = new StateGraphVisitor(this.currentInterpreter, this.mainScript, this.controlFlowGraphVisitor); this.stateGraphVisitor = new StateGraphVisitor(this.currentInterpreter, this.mainScript, this.controlFlowGraphVisitor);
// this.stateGraphVisitor = new StateGraphVisitor(blocker, this.mainScript, this.controlFlowGraphVisitor);
currentInterpreter.getEntryListeners().add(this.stateGraphVisitor); currentInterpreter.getEntryListeners().add(this.stateGraphVisitor);
//currentInterpreter.getExitListeners().add(this.stateGraphVisitor);
this.stateGraphVisitor.addChangeListener(graphChangedListener); this.stateGraphVisitor.addChangeListener(graphChangedListener);
//
// stateGraphVisitor.rootProperty().addListener((observable, oldValue, newValue) -> {
// this.statePointer = newValue;
// });
this.statePointer = stateGraphVisitor.getRoot();
blocker.getStepUntilBlock().set(1); blocker.getStepUntilBlock().set(1);
} }
interpreterService.interpreterProperty().set(currentInterpreter); interpreterService.interpreterProperty().set(currentInterpreter);
...@@ -181,6 +205,17 @@ public class ProofTreeController { ...@@ -181,6 +205,17 @@ public class ProofTreeController {
} }
/**
* Sets the properties that may notify GUI about statechanges with new state values
*
* @param state
*/
private void setNewState(State<KeyData> state) {
this.setCurrentGoals(state.getGoals());
this.setCurrentSelectedGoal(state.getSelectedGoalNode());
System.out.println("New State from this command: " + this.statePointer.getScriptstmt().getNodeName() + "@" + this.statePointer.getScriptstmt().getStartPosition());
}
/************************************************************************************************************** /**************************************************************************************************************
* *
* Getter and Setter * Getter and Setter
...@@ -205,10 +240,10 @@ public class ProofTreeController { ...@@ -205,10 +240,10 @@ public class ProofTreeController {
} }
public void setCurrentGoals(List<GoalNode<KeyData>> currentGoals) { public void setCurrentGoals(List<GoalNode<KeyData>> currentGoals) {
this.currentGoals.set(currentGoals); this.currentGoals.get().setAll(currentGoals);
} }
public SimpleObjectProperty<List<GoalNode<KeyData>>> currentGoalsProperty() { public ListProperty<GoalNode<KeyData>> currentGoalsProperty() {
return currentGoals; return currentGoals;
} }
...@@ -233,4 +268,5 @@ public class ProofTreeController { ...@@ -233,4 +268,5 @@ public class ProofTreeController {
} }
} }
...@@ -3,10 +3,11 @@ package edu.kit.formal.interpreter; ...@@ -3,10 +3,11 @@ package edu.kit.formal.interpreter;
import com.google.common.graph.MutableValueGraph; import com.google.common.graph.MutableValueGraph;
import com.google.common.graph.ValueGraphBuilder; import com.google.common.graph.ValueGraphBuilder;
import edu.kit.formal.gui.controller.PuppetMaster;
import edu.kit.formal.interpreter.data.KeyData; import edu.kit.formal.interpreter.data.KeyData;
import edu.kit.formal.interpreter.data.State;
import edu.kit.formal.proofscriptparser.DefaultASTVisitor; import edu.kit.formal.proofscriptparser.DefaultASTVisitor;
import edu.kit.formal.proofscriptparser.ast.*; import edu.kit.formal.proofscriptparser.ast.*;
import javafx.application.Platform;
import javafx.beans.property.SimpleObjectProperty; import javafx.beans.property.SimpleObjectProperty;
import lombok.Getter; import lombok.Getter;
...@@ -34,7 +35,7 @@ public class StateGraphVisitor extends DefaultASTVisitor<Void> { ...@@ -34,7 +35,7 @@ public class StateGraphVisitor extends DefaultASTVisitor<Void> {
*/ */
private Interpreter<KeyData> currentInterpreter; private Interpreter<KeyData> currentInterpreter;
private PuppetMaster blocker;
/** /**
* Graph that is computed on the fly in order to allow stepping * Graph that is computed on the fly in order to allow stepping
*/ */
...@@ -56,10 +57,7 @@ public class StateGraphVisitor extends DefaultASTVisitor<Void> { ...@@ -56,10 +57,7 @@ public class StateGraphVisitor extends DefaultASTVisitor<Void> {
*/ */
private ProgramFlowVisitor cfgVisitor; private ProgramFlowVisitor cfgVisitor;
/**
* Pointer for stepping
*/
private PTreeNode currentStatePointer;
private ProofScript mainScript; private ProofScript mainScript;
...@@ -68,7 +66,8 @@ public class StateGraphVisitor extends DefaultASTVisitor<Void> { ...@@ -68,7 +66,8 @@ public class StateGraphVisitor extends DefaultASTVisitor<Void> {
this.currentInterpreter = inter; this.currentInterpreter = inter;
this.cfgVisitor = cfgVisitor; this.cfgVisitor = cfgVisitor;
this.mainScript = mainScript; this.mainScript = mainScript;
createRootNode();
//createRootNode();
} }
...@@ -83,18 +82,29 @@ public class StateGraphVisitor extends DefaultASTVisitor<Void> { ...@@ -83,18 +82,29 @@ public class StateGraphVisitor extends DefaultASTVisitor<Void> {
} }