diff --git a/src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java b/src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java index 67097f94f8a80e84add011e9d698a5f36b622d60..732e4562b6819815a36b1ae898172a4cdbc06e79 100644 --- a/src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java +++ b/src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java @@ -9,11 +9,9 @@ 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.State; import edu.kit.formal.proofscriptparser.Facade; import edu.kit.formal.proofscriptparser.ast.ProofScript; import javafx.beans.property.SimpleBooleanProperty; -import javafx.beans.property.SimpleObjectProperty; import javafx.beans.value.ObservableBooleanValue; import javafx.concurrent.Service; import javafx.concurrent.Task; @@ -50,7 +48,6 @@ import java.util.concurrent.Executors; public class DebuggerMainWindowController implements Initializable { private static final Logger LOGGER = LogManager.getLogger(DebuggerMainWindowController.class); - private final PuppetMaster blocker = new PuppetMaster(); private SimpleBooleanProperty debugMode = new SimpleBooleanProperty(false); @@ -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 */ - 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) { Alert alert = new Alert(Alert.AlertType.ERROR); @@ -174,10 +172,10 @@ public class DebuggerMainWindowController implements Initializable { blocker.getBreakpoints().addAll(change.getSet()); });*/ - blocker.currentGoalsProperty().addListener((o, old, fresh) -> { + pc.currentGoalsProperty().addListener((o, old, fresh) -> { model.currentGoalNodesProperty().setAll(fresh); }); - model.currentSelectedGoalNodeProperty().bind(blocker.currentSelectedGoalProperty()); + model.currentSelectedGoalNodeProperty().bind(pc.currentSelectedGoalProperty()); CustomTabPaneSkin skin = new CustomTabPaneSkin(tabPane); @@ -191,15 +189,15 @@ public class DebuggerMainWindowController implements Initializable { @FXML public void executeScriptFromCursor() { - InterpreterBuilder ib = facade.buildInterpreter(); - ib.inheritState(interpreterService.interpreter.get()); -/* - LineMapping lm = new LineMapping(scriptArea.getText()); - int line = lm.getLine(scriptArea.getCaretPosition()); - int inLine = lm.getCharInLine(scriptArea.getCaretPosition()); -*/ - ib.ignoreLinesUntil(tabPane.getSelectedScriptArea().getCaretPosition()); - executeScript(ib, true); +// InterpreterBuilder ib = facade.buildInterpreter(); +// ib.inheritState(interpreterService.interpreterProperty().get()); +///* +// LineMapping lm = new LineMapping(scriptArea.getText()); +// int line = lm.getLine(scriptArea.getCaretPosition()); +// int inLine = lm.getCharInLine(scriptArea.getCaretPosition()); +//*/ +// ib.ignoreLinesUntil(tabPane.getSelectedScriptArea().getCaretPosition()); +// executeScript(ib, true); } @FXML @@ -216,33 +214,20 @@ public class DebuggerMainWindowController implements Initializable { */ private void executeScript(InterpreterBuilder ib, boolean debugMode) { this.debugMode.set(debugMode); - blocker.deinstall(); statusBar.publishMessage("Parse ..."); try { List scripts = Facade.getAST(tabPane.getSelectedScriptArea().getText()); statusBar.publishMessage("Creating new Interpreter instance ..."); ib.setScripts(scripts); - ib.captureHistory(); Interpreter currentInterpreter = ib.build(); - if (debugMode) { - //blocker.getStepUntilBlock().set(1); - - //for stepping functionality - pc = new ProofTreeController(currentInterpreter, scripts.get(0)); - currentInterpreter.getEntryListeners().add(pc.getStateVisitor()); - - } - // blocker.install(currentInterpreter); + pc.setCurrentInterpreter(currentInterpreter); + pc.setMainScript(scripts.get(0)); + pc.executeScript(this.debugMode.get()); //highlight signature of main script tabPane.getSelectedScriptArea().setDebugMark(scripts.get(0).getStartPosition().getLineNumber()); - - interpreterService.interpreter.set(currentInterpreter); - interpreterService.mainScript.set(scripts.get(0)); - - interpreterService.start(); } catch (RecognitionException e) { showExceptionDialog("Antlr Exception", "", "Could not parse scripts.", e); } @@ -421,6 +406,7 @@ public class DebuggerMainWindowController implements Initializable { public Boolean getExecuteNotPossible() { return executeNotPossible.get(); + } public ObservableBooleanValue executeNotPossibleProperty() { @@ -464,49 +450,5 @@ public class DebuggerMainWindowController implements Initializable { } - - private class InterpretingService extends Service> { - private final SimpleObjectProperty> interpreter = new SimpleObjectProperty<>(); - private final SimpleObjectProperty 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> createTask() { - return new Task>() { - final Interpreter i = interpreter.get(); - final ProofScript ast = mainScript.get(); - - @Override - protected edu.kit.formal.interpreter.data.State call() throws Exception { - i.interpret(ast); - return i.peekState(); - } - }; - } - } -//endregion + //endregion } diff --git a/src/main/java/edu/kit/formal/interpreter/InterpretingService.java b/src/main/java/edu/kit/formal/interpreter/InterpretingService.java new file mode 100644 index 0000000000000000000000000000000000000000..2cd4f245a95bc5dceba299f7f1c148525bbc1447 --- /dev/null +++ b/src/main/java/edu/kit/formal/interpreter/InterpretingService.java @@ -0,0 +1,115 @@ +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> { + + /** + * The interpreter (with teh appropriate KeY state) that is used to traverse and execute the script + */ + private final SimpleObjectProperty> interpreter = new SimpleObjectProperty<>(); + + /** + * The main script that is traversed + */ + private final SimpleObjectProperty 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> createTask() { + return new Task>() { + final Interpreter 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 call() throws Exception { + i.interpret(ast); + return i.peekState(); + } + }; + } + + /************************************************************************************************************** + * + * Getter and Setter + * + **************************************************************************************************************/ + public Interpreter getInterpreter() { + return interpreter.get(); + } + + public void setInterpreter(Interpreter interpreter) { + this.interpreter.set(interpreter); + } + + public SimpleObjectProperty> interpreterProperty() { + return interpreter; + } + + public ProofScript getMainScript() { + return mainScript.get(); + } + + public void setMainScript(ProofScript mainScript) { + this.mainScript.set(mainScript); + } + + public SimpleObjectProperty mainScriptProperty() { + return mainScript; + } + + +} diff --git a/src/main/java/edu/kit/formal/interpreter/PTreeNode.java b/src/main/java/edu/kit/formal/interpreter/PTreeNode.java index ea7c62139076626f930a0d77ead2a05c965a44ed..b3c4919a89e7150520c6d981eb0d5031cadcd8bc 100644 --- a/src/main/java/edu/kit/formal/interpreter/PTreeNode.java +++ b/src/main/java/edu/kit/formal/interpreter/PTreeNode.java @@ -4,14 +4,32 @@ import edu.kit.formal.interpreter.data.KeyData; import edu.kit.formal.interpreter.data.State; import edu.kit.formal.proofscriptparser.ast.ASTNode; +import java.util.LinkedList; + /** * 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. */ public class PTreeNode { - State state; + /** + * State after statement + */ + private State state; + + /** + * Statement + */ + private ASTNode scriptstmt; + + + /** + * Call context + */ + private LinkedList context = new LinkedList<>(); + + private boolean root; + - ASTNode scriptstmt; public PTreeNode(ASTNode node) { this.setScriptstmt(node); @@ -37,13 +55,21 @@ public class PTreeNode { return state != null; } + public LinkedList getContext() { + return context; + } + + public void setContext(LinkedList context) { + this.context = context; + } + public String toString() { StringBuilder sb = new StringBuilder(); sb.append("Node {"); if (scriptstmt != null) { sb.append(scriptstmt.getNodeName() + "\n"); } else { - sb.append("No Stmt"); + sb.append("Root Node"); } if (hasState()) { sb.append("\nState " + state.getGoals() + "\n"); diff --git a/src/main/java/edu/kit/formal/interpreter/ProofTreeController.java b/src/main/java/edu/kit/formal/interpreter/ProofTreeController.java index c04a3b9d2d85a25742e6c0d276d37a8eef9f100b..1814ed88791aa7ac680764ff67836c933644d585 100644 --- a/src/main/java/edu/kit/formal/interpreter/ProofTreeController.java +++ b/src/main/java/edu/kit/formal/interpreter/ProofTreeController.java @@ -1,9 +1,14 @@ package edu.kit.formal.interpreter; 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.proofscriptparser.Visitor; 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 @@ -16,6 +21,11 @@ public class ProofTreeController { * To control stepping */ private final PuppetMaster blocker = new PuppetMaster(); + private final SimpleObjectProperty>> currentGoals = blocker.currentGoalsProperty(); + private final SimpleObjectProperty> currentSelectedGoal = blocker.currentSelectedGoalProperty(); + //new SimpleBooleanProperty(false); + private InterpretingService interpreterService = new InterpretingService(blocker); + private ReadOnlyBooleanProperty executeNotPossible = interpreterService.runningProperty(); /** * Visitor to retrieve state graph */ @@ -25,22 +35,33 @@ public class ProofTreeController { */ private ProgramFlowVisitor controlFlowGraphVisitor; + + /** * Current interpreter */ private Interpreter currentInterpreter; + /** * Current State in graph */ - private PTreeNode statePointer; + private PTreeNode statePointer = null; + + + private ProofScript mainScript; - public ProofTreeController(Interpreter inter, ProofScript mainScript) { + public ProofTreeController() { + + + } + + private ProofTreeController(Interpreter inter, ProofScript mainScript) { blocker.deinstall(); this.currentInterpreter = inter; buildControlFlowGraph(mainScript); this.stateGraphVisitor = new StateGraphVisitor(inter, mainScript, controlFlowGraphVisitor); - statePointer = stateGraphVisitor.getRootNode(); + //statePointer = stateGraphVisitor.getRoot(); blocker.getStepUntilBlock().set(1); blocker.install(currentInterpreter); @@ -54,28 +75,43 @@ public class ProofTreeController { private void buildControlFlowGraph(ProofScript mainScript) { this.controlFlowGraphVisitor = new ProgramFlowVisitor(currentInterpreter.getFunctionLookup()); mainScript.accept(controlFlowGraphVisitor); - System.out.println("CFG\n" + controlFlowGraphVisitor.asdot()); } public PTreeNode stepOver() { - blocker.getStepUntilBlock().addAndGet(1); - blocker.unlock(); - - - + PTreeNode currentPointer = statePointer; 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; } + //TODO handle endpoint of graph public PTreeNode stepBack() { + PTreeNode current = statePointer; + this.statePointer = stateGraphVisitor.getStepBack(current); + System.out.println("PRED NODE \n\n" + this.statePointer + "\n-------------------\n"); return null; } @@ -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 currentInterpreter) { + this.currentInterpreter = currentInterpreter; + } + + public void setMainScript(ProofScript mainScript) { + this.mainScript = mainScript; + + } public Visitor getStateVisitor() { return this.stateGraphVisitor; } + + public List> getCurrentGoals() { + return currentGoals.get(); + } + + public void setCurrentGoals(List> currentGoals) { + this.currentGoals.set(currentGoals); + } + + public SimpleObjectProperty>> currentGoalsProperty() { + return currentGoals; + } + + public GoalNode getCurrentSelectedGoal() { + return currentSelectedGoal.get(); + } + + public void setCurrentSelectedGoal(GoalNode currentSelectedGoal) { + this.currentSelectedGoal.set(currentSelectedGoal); + } + + public SimpleObjectProperty> currentSelectedGoalProperty() { + return currentSelectedGoal; + } + + public boolean isExecuteNotPossible() { + return executeNotPossible.get(); + } + + public ReadOnlyBooleanProperty executeNotPossibleProperty() { + return executeNotPossible; + } + } diff --git a/src/main/java/edu/kit/formal/interpreter/StateGraphVisitor.java b/src/main/java/edu/kit/formal/interpreter/StateGraphVisitor.java index 24183a9b15929aaee6a3e876fe04febe953c4b10..56e2173da1cbe6e92f9757f0e5b2c8112d551ab8 100644 --- a/src/main/java/edu/kit/formal/interpreter/StateGraphVisitor.java +++ b/src/main/java/edu/kit/formal/interpreter/StateGraphVisitor.java @@ -1,12 +1,14 @@ package edu.kit.formal.interpreter; -import com.google.common.graph.EndpointPair; import com.google.common.graph.MutableValueGraph; import com.google.common.graph.ValueGraphBuilder; +import edu.kit.formal.gui.controller.PuppetMaster; import edu.kit.formal.proofscriptparser.DefaultASTVisitor; import edu.kit.formal.proofscriptparser.ast.*; +import javafx.beans.property.SimpleObjectProperty; +import java.util.HashSet; import java.util.Set; @@ -18,15 +20,18 @@ public class StateGraphVisitor extends DefaultASTVisitor { * Interpreter */ private Interpreter currentInterpreter; + + private PuppetMaster blocker; /** * Graph that is computed on the fly in order to allow stepping */ private MutableValueGraph stateGraph; + /** * Root of state graph */ - private PTreeNode root; + private SimpleObjectProperty root = new SimpleObjectProperty<>(); /** * last added node @@ -38,35 +43,99 @@ public class StateGraphVisitor extends DefaultASTVisitor { */ private ProgramFlowVisitor cfgVisitor; + /** + * Pointer for stepping + */ + private PTreeNode currentStatePointer; public StateGraphVisitor(Interpreter inter, ProofScript mainScript, ProgramFlowVisitor cfgVisitor) { stateGraph = ValueGraphBuilder.directed().build(); this.currentInterpreter = inter; this.cfgVisitor = cfgVisitor; - + createRootNode(); } + /* public StateGraphVisitor(PuppetMaster blocker, ProofScript mainScript, ProgramFlowVisitor cfgVisitor) { + stateGraph = ValueGraphBuilder.directed().build(); + this.cfgVisitor = cfgVisitor; + this.blocker = blocker; + createRootNode(); + }*/ public MutableValueGraph getStateGraph() { return stateGraph; } - public PTreeNode getRootNode() { - return root; - } + public PTreeNode getLastNode() { return lastNode; } - //public (ControlFlowNode, ControlflowNode, Edge) getReturnEdge(ASTNode node) + + public void createRootNode() { + PTreeNode newStateNode = new PTreeNode(null); + newStateNode.setState(currentInterpreter.getCurrentState()); + stateGraph.addNode(newStateNode); + this.root.set(newStateNode); + lastNode = newStateNode; + } - //public Node findNode(ASTNode, state){} + //careful TODO look for right edges + //TODO handle endpoint of graph + public PTreeNode getStepOver(PTreeNode statePointer) { + + Set successors = this.stateGraph.successors(statePointer); + if (successors.isEmpty()) { + return null; + } else { + Object[] sucs = successors.toArray(); + getNodeWithEdgeType(statePointer, EdgeTypes.STATE_FLOW); + return (PTreeNode) sucs[0]; + } + + } + + //TODO handle endpoint of graph + public PTreeNode getStepBack(PTreeNode statePointer) { + + Set pred = this.stateGraph.predecessors(statePointer); + if (pred.isEmpty()) { + return null; + } else { + Object[] sucs = pred.toArray(); + return (PTreeNode) sucs[0]; + } + + } + + private PTreeNode getNodeWithEdgeType(PTreeNode source, EdgeTypes type) { + Set predecessors = stateGraph.predecessors(source); + Set chosenNodes = new HashSet<>(); + + predecessors.forEach(pred -> { + EdgeTypes typeToCheck = stateGraph.edgeValue(pred, source); + if (type.equals(typeToCheck)) { + chosenNodes.add(pred); + } + }); + + Set successors = stateGraph.successors(source); + successors.forEach(succ -> { + EdgeTypes typeToCheck = stateGraph.edgeValue(source, succ); + if (type.equals(typeToCheck)) { + chosenNodes.add(succ); + } + }); + chosenNodes.forEach(n -> System.out.println(n.toString())); + //stateGraph.edgeValue() + return null; + } /** - * Creat a new node for the state graph and add edges to already existing nodes + * Create a new node for the state graph and add edges to already existing nodes * * @param node * @return @@ -76,19 +145,15 @@ public class StateGraphVisitor extends DefaultASTVisitor { PTreeNode newStateNode = new PTreeNode(node); newStateNode.setState(currentInterpreter.getCurrentState()); stateGraph.addNode(newStateNode); - Set> targetEdges = cfgVisitor.getAllEdgesForNodeAsTarget(node); + + /*Set> targetEdges = cfgVisitor.getAllEdgesForNodeAsTarget(node); for (EndpointPair targetEdge : targetEdges) { ControlFlowNode cfn = targetEdge.source(); ASTNode assocNode = cfn.getScriptstmt(); //mapping - } - if (lastNode == null) { - root = newStateNode; - } else { - stateGraph.putEdgeValue(lastNode, newStateNode, EdgeTypes.STATE_FLOW); - - } + }*/ + stateGraph.putEdgeValue(lastNode, newStateNode, EdgeTypes.STATE_FLOW); lastNode = newStateNode; return null; @@ -168,4 +233,16 @@ public class StateGraphVisitor extends DefaultASTVisitor { } + public PTreeNode getRoot() { + return root.get(); + } + + public void setRoot(PTreeNode root) { + this.root.set(root); + } + + public SimpleObjectProperty rootProperty() { + return root; + } + }