Commit f167cf52 authored by Sarah Grebing's avatar Sarah Grebing

Interim reafctoring for stepping

parent a8e7207d
...@@ -9,11 +9,9 @@ import edu.kit.formal.interpreter.InterpreterBuilder; ...@@ -9,11 +9,9 @@ import edu.kit.formal.interpreter.InterpreterBuilder;
import edu.kit.formal.interpreter.KeYProofFacade; import edu.kit.formal.interpreter.KeYProofFacade;
import edu.kit.formal.interpreter.ProofTreeController; import edu.kit.formal.interpreter.ProofTreeController;
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.Facade; import edu.kit.formal.proofscriptparser.Facade;
import edu.kit.formal.proofscriptparser.ast.ProofScript; import edu.kit.formal.proofscriptparser.ast.ProofScript;
import javafx.beans.property.SimpleBooleanProperty; import javafx.beans.property.SimpleBooleanProperty;
import javafx.beans.property.SimpleObjectProperty;
import javafx.beans.value.ObservableBooleanValue; import javafx.beans.value.ObservableBooleanValue;
import javafx.concurrent.Service; import javafx.concurrent.Service;
import javafx.concurrent.Task; import javafx.concurrent.Task;
...@@ -50,7 +48,6 @@ import java.util.concurrent.Executors; ...@@ -50,7 +48,6 @@ import java.util.concurrent.Executors;
public class DebuggerMainWindowController implements Initializable { public class DebuggerMainWindowController implements Initializable {
private static final Logger LOGGER = LogManager.getLogger(DebuggerMainWindowController.class); private static final Logger LOGGER = LogManager.getLogger(DebuggerMainWindowController.class);
private final PuppetMaster blocker = new PuppetMaster();
private SimpleBooleanProperty debugMode = new SimpleBooleanProperty(false); private SimpleBooleanProperty debugMode = new SimpleBooleanProperty(false);
...@@ -106,14 +103,15 @@ public class DebuggerMainWindowController implements Initializable { ...@@ -106,14 +103,15 @@ public class DebuggerMainWindowController implements Initializable {
private InterpretingService interpreterService = new InterpretingService();
private ObservableBooleanValue executeNotPossible = interpreterService.runningProperty().or(facade.readyToExecuteProperty().not());
/** /**
* Controller for debugging functions * Controller for debugging functions
*/ */
private ProofTreeController pc; private ProofTreeController pc = new ProofTreeController();
//TODO
private ObservableBooleanValue executeNotPossible = pc.executeNotPossibleProperty().or(facade.readyToExecuteProperty().not());
public static void showExceptionDialog(String title, String headerText, String contentText, Throwable ex) { public static void showExceptionDialog(String title, String headerText, String contentText, Throwable ex) {
Alert alert = new Alert(Alert.AlertType.ERROR); Alert alert = new Alert(Alert.AlertType.ERROR);
...@@ -174,10 +172,10 @@ public class DebuggerMainWindowController implements Initializable { ...@@ -174,10 +172,10 @@ public class DebuggerMainWindowController implements Initializable {
blocker.getBreakpoints().addAll(change.getSet()); blocker.getBreakpoints().addAll(change.getSet());
});*/ });*/
blocker.currentGoalsProperty().addListener((o, old, fresh) -> { pc.currentGoalsProperty().addListener((o, old, fresh) -> {
model.currentGoalNodesProperty().setAll(fresh); model.currentGoalNodesProperty().setAll(fresh);
}); });
model.currentSelectedGoalNodeProperty().bind(blocker.currentSelectedGoalProperty()); model.currentSelectedGoalNodeProperty().bind(pc.currentSelectedGoalProperty());
CustomTabPaneSkin skin = new CustomTabPaneSkin(tabPane); CustomTabPaneSkin skin = new CustomTabPaneSkin(tabPane);
...@@ -191,15 +189,15 @@ public class DebuggerMainWindowController implements Initializable { ...@@ -191,15 +189,15 @@ public class DebuggerMainWindowController implements Initializable {
@FXML @FXML
public void executeScriptFromCursor() { public void executeScriptFromCursor() {
InterpreterBuilder ib = facade.buildInterpreter(); // InterpreterBuilder ib = facade.buildInterpreter();
ib.inheritState(interpreterService.interpreter.get()); // ib.inheritState(interpreterService.interpreterProperty().get());
/* ///*
LineMapping lm = new LineMapping(scriptArea.getText()); // LineMapping lm = new LineMapping(scriptArea.getText());
int line = lm.getLine(scriptArea.getCaretPosition()); // int line = lm.getLine(scriptArea.getCaretPosition());
int inLine = lm.getCharInLine(scriptArea.getCaretPosition()); // int inLine = lm.getCharInLine(scriptArea.getCaretPosition());
*/ //*/
ib.ignoreLinesUntil(tabPane.getSelectedScriptArea().getCaretPosition()); // ib.ignoreLinesUntil(tabPane.getSelectedScriptArea().getCaretPosition());
executeScript(ib, true); // executeScript(ib, true);
} }
@FXML @FXML
...@@ -216,33 +214,20 @@ public class DebuggerMainWindowController implements Initializable { ...@@ -216,33 +214,20 @@ public class DebuggerMainWindowController implements Initializable {
*/ */
private void executeScript(InterpreterBuilder ib, boolean debugMode) { private void executeScript(InterpreterBuilder ib, boolean debugMode) {
this.debugMode.set(debugMode); this.debugMode.set(debugMode);
blocker.deinstall();
statusBar.publishMessage("Parse ..."); statusBar.publishMessage("Parse ...");
try { try {
List<ProofScript> scripts = Facade.getAST(tabPane.getSelectedScriptArea().getText()); List<ProofScript> scripts = Facade.getAST(tabPane.getSelectedScriptArea().getText());
statusBar.publishMessage("Creating new Interpreter instance ..."); statusBar.publishMessage("Creating new Interpreter instance ...");
ib.setScripts(scripts); ib.setScripts(scripts);
ib.captureHistory();
Interpreter<KeyData> currentInterpreter = ib.build(); Interpreter<KeyData> currentInterpreter = ib.build();
if (debugMode) { pc.setCurrentInterpreter(currentInterpreter);
//blocker.getStepUntilBlock().set(1); pc.setMainScript(scripts.get(0));
pc.executeScript(this.debugMode.get());
//for stepping functionality
pc = new ProofTreeController(currentInterpreter, scripts.get(0));
currentInterpreter.getEntryListeners().add(pc.getStateVisitor());
}
// blocker.install(currentInterpreter);
//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());
interpreterService.interpreter.set(currentInterpreter);
interpreterService.mainScript.set(scripts.get(0));
interpreterService.start();
} catch (RecognitionException e) { } catch (RecognitionException e) {
showExceptionDialog("Antlr Exception", "", "Could not parse scripts.", e); showExceptionDialog("Antlr Exception", "", "Could not parse scripts.", e);
} }
...@@ -421,6 +406,7 @@ public class DebuggerMainWindowController implements Initializable { ...@@ -421,6 +406,7 @@ public class DebuggerMainWindowController implements Initializable {
public Boolean getExecuteNotPossible() { public Boolean getExecuteNotPossible() {
return executeNotPossible.get(); return executeNotPossible.get();
} }
public ObservableBooleanValue executeNotPossibleProperty() { public ObservableBooleanValue executeNotPossibleProperty() {
...@@ -464,49 +450,5 @@ public class DebuggerMainWindowController implements Initializable { ...@@ -464,49 +450,5 @@ public class DebuggerMainWindowController implements Initializable {
} }
//endregion
private class InterpretingService extends Service<State<KeyData>> {
private final SimpleObjectProperty<Interpreter<KeyData>> interpreter = new SimpleObjectProperty<>();
private final SimpleObjectProperty<ProofScript> mainScript = new SimpleObjectProperty<>();
@Override
protected void succeeded() {
updateView();
}
@Override
protected void cancelled() {
updateView();
}
@Override
protected void failed() {
getException().printStackTrace();
showExceptionDialog("Execution failed", "", "", getException());
updateView();
}
private void updateView() {
//check proof
//check state for empty/error goal nodes
//currentGoals.set(state.getGoals());
//currentSelectedGoal.set(state.getSelectedGoalNode());
blocker.publishState();
}
@Override
protected Task<edu.kit.formal.interpreter.data.State<KeyData>> createTask() {
return new Task<edu.kit.formal.interpreter.data.State<KeyData>>() {
final Interpreter<KeyData> i = interpreter.get();
final ProofScript ast = mainScript.get();
@Override
protected edu.kit.formal.interpreter.data.State<KeyData> call() throws Exception {
i.interpret(ast);
return i.peekState();
}
};
}
}
//endregion
} }
package edu.kit.formal.interpreter;
import edu.kit.formal.gui.controller.DebuggerMainWindowController;
import edu.kit.formal.gui.controller.PuppetMaster;
import edu.kit.formal.interpreter.data.KeyData;
import edu.kit.formal.interpreter.data.State;
import edu.kit.formal.proofscriptparser.ast.ProofScript;
import javafx.beans.property.SimpleObjectProperty;
import javafx.concurrent.Service;
import javafx.concurrent.Task;
/**
* Service handling interpreting the script in an own thread
*
* @author A. Weigl
*/
class InterpretingService extends Service<State<KeyData>> {
/**
* The interpreter (with teh appropriate KeY state) that is used to traverse and execute the script
*/
private final SimpleObjectProperty<Interpreter<KeyData>> interpreter = new SimpleObjectProperty<>();
/**
* The main script that is traversed
*/
private final SimpleObjectProperty<ProofScript> mainScript = new SimpleObjectProperty<>();
/**
* The blocker, necessary for controlling how far the script should be interpreted
*/
private PuppetMaster blocker;
InterpretingService(PuppetMaster blocker) {
this.blocker = blocker;
}
@Override
protected void succeeded() {
updateView();
}
@Override
protected void cancelled() {
updateView();
}
@Override
protected void failed() {
getException().printStackTrace();
DebuggerMainWindowController.showExceptionDialog("Execution failed", "", "", getException());
updateView();
}
private void updateView() {
//check proof
//check state for empty/error goal nodes
//currentGoals.set(state.getGoals());
//currentSelectedGoal.set(state.getSelectedGoalNode());
blocker.publishState();
}
@Override
protected Task<edu.kit.formal.interpreter.data.State<KeyData>> createTask() {
return new Task<edu.kit.formal.interpreter.data.State<KeyData>>() {
final Interpreter<KeyData> i = interpreter.get();
final ProofScript ast = mainScript.get();
/**
* Start the interpreter with the AST of the parsed mainscript and return the last state from the interpreter
* after interpreting
* @return top of the state stack of the interpreter
* @throws Exception
*/
@Override
protected edu.kit.formal.interpreter.data.State<KeyData> call() throws Exception {
i.interpret(ast);
return i.peekState();
}
};
}
/**************************************************************************************************************
*
* Getter and Setter
*
**************************************************************************************************************/
public Interpreter<KeyData> getInterpreter() {
return interpreter.get();
}
public void setInterpreter(Interpreter<KeyData> interpreter) {
this.interpreter.set(interpreter);
}
public SimpleObjectProperty<Interpreter<KeyData>> interpreterProperty() {
return interpreter;
}
public ProofScript getMainScript() {
return mainScript.get();
}
public void setMainScript(ProofScript mainScript) {
this.mainScript.set(mainScript);
}
public SimpleObjectProperty<ProofScript> mainScriptProperty() {
return mainScript;
}
}
...@@ -4,14 +4,32 @@ import edu.kit.formal.interpreter.data.KeyData; ...@@ -4,14 +4,32 @@ import edu.kit.formal.interpreter.data.KeyData;
import edu.kit.formal.interpreter.data.State; import edu.kit.formal.interpreter.data.State;
import edu.kit.formal.proofscriptparser.ast.ASTNode; import edu.kit.formal.proofscriptparser.ast.ASTNode;
import java.util.LinkedList;
/** /**
* Inner class representing nodes in the graph * Inner class representing nodes in the graph
* A node contains a reference to the ASTNode and a reference to the corresponding interpreter state if this state is already interpreted, null otherwise. * A node contains a reference to the ASTNode and a reference to the corresponding interpreter state if this state is already interpreted, null otherwise.
*/ */
public class PTreeNode { public class PTreeNode {
State<KeyData> state; /**
* State after statement
*/
private State<KeyData> state;
/**
* Statement
*/
private ASTNode scriptstmt;
/**
* Call context
*/
private LinkedList<ASTNode> context = new LinkedList<>();
private boolean root;
ASTNode scriptstmt;
public PTreeNode(ASTNode node) { public PTreeNode(ASTNode node) {
this.setScriptstmt(node); this.setScriptstmt(node);
...@@ -37,13 +55,21 @@ public class PTreeNode { ...@@ -37,13 +55,21 @@ public class PTreeNode {
return state != null; return state != null;
} }
public LinkedList<ASTNode> getContext() {
return context;
}
public void setContext(LinkedList<ASTNode> context) {
this.context = context;
}
public String toString() { public String toString() {
StringBuilder sb = new StringBuilder(); StringBuilder sb = new StringBuilder();
sb.append("Node {"); sb.append("Node {");
if (scriptstmt != null) { if (scriptstmt != null) {
sb.append(scriptstmt.getNodeName() + "\n"); sb.append(scriptstmt.getNodeName() + "\n");
} else { } else {
sb.append("No Stmt"); sb.append("Root Node");
} }
if (hasState()) { if (hasState()) {
sb.append("\nState " + state.getGoals() + "\n"); sb.append("\nState " + state.getGoals() + "\n");
......
package edu.kit.formal.interpreter; 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.KeyData; import edu.kit.formal.interpreter.data.KeyData;
import edu.kit.formal.proofscriptparser.Visitor; import edu.kit.formal.proofscriptparser.Visitor;
import edu.kit.formal.proofscriptparser.ast.ProofScript; import edu.kit.formal.proofscriptparser.ast.ProofScript;
import javafx.beans.property.ReadOnlyBooleanProperty;
import javafx.beans.property.SimpleObjectProperty;
import java.util.List;
/** /**
* Class controlling and maintaining proof tree structure for debugger and handling step functions for the debugger * Class controlling and maintaining proof tree structure for debugger and handling step functions for the debugger
...@@ -16,6 +21,11 @@ public class ProofTreeController { ...@@ -16,6 +21,11 @@ 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 = blocker.currentGoalsProperty();
private final SimpleObjectProperty<GoalNode<KeyData>> currentSelectedGoal = blocker.currentSelectedGoalProperty();
//new SimpleBooleanProperty(false);
private InterpretingService interpreterService = new InterpretingService(blocker);
private ReadOnlyBooleanProperty executeNotPossible = interpreterService.runningProperty();
/** /**
* Visitor to retrieve state graph * Visitor to retrieve state graph
*/ */
...@@ -25,22 +35,33 @@ public class ProofTreeController { ...@@ -25,22 +35,33 @@ public class ProofTreeController {
*/ */
private ProgramFlowVisitor controlFlowGraphVisitor; private ProgramFlowVisitor controlFlowGraphVisitor;
/** /**
* Current interpreter * Current interpreter
*/ */
private Interpreter<KeyData> currentInterpreter; private Interpreter<KeyData> currentInterpreter;
/** /**
* Current State in graph * Current State in graph
*/ */
private PTreeNode statePointer; private PTreeNode statePointer = null;
private ProofScript mainScript;
public ProofTreeController(Interpreter<KeyData> inter, ProofScript mainScript) { public ProofTreeController() {
}
private ProofTreeController(Interpreter<KeyData> inter, ProofScript mainScript) {
blocker.deinstall(); blocker.deinstall();
this.currentInterpreter = inter; this.currentInterpreter = inter;
buildControlFlowGraph(mainScript); buildControlFlowGraph(mainScript);
this.stateGraphVisitor = new StateGraphVisitor(inter, mainScript, controlFlowGraphVisitor); this.stateGraphVisitor = new StateGraphVisitor(inter, mainScript, controlFlowGraphVisitor);
statePointer = stateGraphVisitor.getRootNode(); //statePointer = stateGraphVisitor.getRoot();
blocker.getStepUntilBlock().set(1); blocker.getStepUntilBlock().set(1);
blocker.install(currentInterpreter); blocker.install(currentInterpreter);
...@@ -54,28 +75,43 @@ public class ProofTreeController { ...@@ -54,28 +75,43 @@ public class ProofTreeController {
private void buildControlFlowGraph(ProofScript mainScript) { private void buildControlFlowGraph(ProofScript mainScript) {
this.controlFlowGraphVisitor = new ProgramFlowVisitor(currentInterpreter.getFunctionLookup()); this.controlFlowGraphVisitor = new ProgramFlowVisitor(currentInterpreter.getFunctionLookup());
mainScript.accept(controlFlowGraphVisitor); mainScript.accept(controlFlowGraphVisitor);
System.out.println("CFG\n" + controlFlowGraphVisitor.asdot()); System.out.println("CFG\n" + controlFlowGraphVisitor.asdot());
} }
public PTreeNode stepOver() { public PTreeNode stepOver() {
blocker.getStepUntilBlock().addAndGet(1); PTreeNode currentPointer = statePointer;
blocker.unlock();
if (statePointer == null) { if (statePointer == null) {
this.statePointer = stateGraphVisitor.getLastNode(); System.out.println("StatePointer is null");
} else {
PTreeNode nextNode = stateGraphVisitor.getStepOver(currentPointer);
if (nextNode != null) {
this.statePointer = nextNode;
} else {
//let interpreter run for one step
blocker.getStepUntilBlock().addAndGet(1);
blocker.unlock();
//sync problem???
//TODO make this right!
//TODO handle endpoint of graph
nextNode = stateGraphVisitor.getStepOver(currentPointer);
while (nextNode == null) {
nextNode = stateGraphVisitor.getStepOver(currentPointer);
}
this.statePointer = nextNode;
}
System.out.println("NEXT NODE \n\n" + this.statePointer + "\n-------------------\n");
} }
//PTreeNode current = statePointer;
//ASTNode stmt = current.getScriptstmt();
//System.out.println("CurrentPointer: " + stmt.getNodeName() + "@" + stmt.getStartPosition());
return null; return null;
} }
//TODO handle endpoint of graph
public PTreeNode stepBack() { public PTreeNode stepBack() {
PTreeNode current = statePointer;
this.statePointer = stateGraphVisitor.getStepBack(current);
System.out.println("PRED NODE \n\n" + this.statePointer + "\n-------------------\n");
return null; return null;
} }
...@@ -88,7 +124,83 @@ public class ProofTreeController { ...@@ -88,7 +124,83 @@ public class ProofTreeController {
} }
public void executeScript(boolean debugMode) {
blocker.deinstall();
blocker.install(currentInterpreter);
if (!debugMode) {
blocker.getStepUntilBlock().set(-1);
} else {
//build CFG
buildControlFlowGraph(mainScript);
//build StateGraph
this.stateGraphVisitor = new StateGraphVisitor(this.currentInterpreter, this.mainScript, this.controlFlowGraphVisitor);
// this.stateGraphVisitor = new StateGraphVisitor(blocker, this.mainScript, this.controlFlowGraphVisitor);
currentInterpreter.getEntryListeners().add(this.stateGraphVisitor);
//
// stateGraphVisitor.rootProperty().addListener((observable, oldValue, newValue) -> {
// this.statePointer = newValue;
// });
this.statePointer = stateGraphVisitor.getRoot();
blocker.getStepUntilBlock().set(1);
}
interpreterService.interpreterProperty().set(currentInterpreter);
interpreterService.mainScriptProperty().set(mainScript);
interpreterService.start();
}
/**************************************************************************************************************
*
* Getter and Setter
*
**************************************************************************************************************/
public void setCurrentInterpreter(Interpreter<KeyData> currentInterpreter) {
this.currentInterpreter = currentInterpreter;
}
public void setMainScript(ProofScript mainScript) {
this.mainScript = mainScript;
}
public Visitor getStateVisitor() { public Visitor getStateVisitor() {
return this.stateGraphVisitor; return this.stateGraphVisitor;
} }
public List<GoalNode<KeyData>> getCurrentGoals() {
return currentGoals.get();
}
public void setCurrentGoals(List<GoalNode<KeyData>> currentGoals) {
this.currentGoals.set(currentGoals);
}
public SimpleObjectProperty<List<GoalNode<KeyData>>> currentGoalsProperty() {
return currentGoals;
}
public GoalNode<KeyData> getCurrentSelectedGoal() {
return currentSelectedGoal.get();
}
public void setCurrentSelectedGoal(GoalNode<KeyData> currentSelectedGoal) {
this.currentSelectedGoal.set(currentSelectedGoal);
}
public SimpleObjectProperty<GoalNode<KeyData>> currentSelectedGoalProperty() {
return currentSelectedGoal;
}
public boolean isExecuteNotPossible() {
return executeNotPossible.get();
}
public ReadOnlyBooleanProperty executeNotPossibleProperty() {
return executeNotPossible;
}
} }
package edu.kit.formal.interpreter; package edu.kit.formal.interpreter;
import com.google.common.graph.EndpointPair;
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.proofscriptparser.DefaultASTVisitor; import edu.kit.formal.proofscriptparser.DefaultASTVisitor;
import edu.kit.formal.proofscriptparser.ast.*; import edu.kit.formal.proofscriptparser.ast.*;
import javafx.beans.property.SimpleObjectProperty;
import java.util.HashSet;
import java.util.Set; import java.util.Set;
...@@ -18,15 +20,18 @@ public class StateGraphVisitor extends DefaultASTVisitor<Void> { ...@@ -18,15 +20,18 @@ public class StateGraphVisitor extends DefaultASTVisitor<Void> {
* Interpreter * Interpreter
*/ */
private Interpreter currentInterpreter; private Interpreter currentInterpreter;