From f15159eea5c73d1b65680180229422b974fb0991 Mon Sep 17 00:00:00 2001 From: Sarah Grebing Date: Mon, 26 Jun 2017 09:18:36 +0200 Subject: [PATCH] Interim (incomplete commit) --- .../DebuggerMainWindowController.java | 15 ++-- .../formal/interpreter/ControlFlowNode.java | 8 +- .../edu/kit/formal/interpreter/EdgeTypes.java | 2 +- .../edu/kit/formal/interpreter/PTreeNode.java | 14 +-- .../interpreter/ProgramFlowVisitor.java | 87 ++++++++++++++----- .../interpreter/ProofTreeController.java | 49 +++++++++-- .../formal/interpreter/StateGraphVisitor.java | 87 +++++++++++++++++++ 7 files changed, 217 insertions(+), 45 deletions(-) create mode 100644 src/main/java/edu/kit/formal/interpreter/StateGraphVisitor.java 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 2f606d6a..527449cd 100644 --- a/src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java +++ b/src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java @@ -4,10 +4,7 @@ import de.uka.ilkd.key.proof.init.ProofInputException; import de.uka.ilkd.key.speclang.Contract; import edu.kit.formal.gui.controls.*; import edu.kit.formal.gui.model.RootModel; -import edu.kit.formal.interpreter.Interpreter; -import edu.kit.formal.interpreter.InterpreterBuilder; -import edu.kit.formal.interpreter.KeYProofFacade; -import edu.kit.formal.interpreter.ProofTreeController; +import edu.kit.formal.interpreter.*; import edu.kit.formal.interpreter.data.KeyData; import edu.kit.formal.interpreter.data.State; import edu.kit.formal.proofscriptparser.Facade; @@ -113,6 +110,7 @@ public class DebuggerMainWindowController implements Initializable { private ObservableBooleanValue executeNotPossible = interpreterService.runningProperty().or(facade.readyToExecuteProperty().not()); + private ProofTreeController pc; public static void showExceptionDialog(String title, String headerText, String contentText, Throwable ex) { Alert alert = new Alert(Alert.AlertType.ERROR); alert.setTitle(title); @@ -225,8 +223,11 @@ public class DebuggerMainWindowController implements Initializable { Interpreter currentInterpreter = ib.build(); if (debugMode) { - ProofTreeController pc = new ProofTreeController(currentInterpreter, scripts.get(0)); - //blocker.getStepUntilBlock().set(1); + blocker.getStepUntilBlock().set(1); + //for stepping functionality + StateGraphVisitor visitor = new StateGraphVisitor(currentInterpreter, scripts.get(0)); + pc = new ProofTreeController(currentInterpreter, scripts.get(0), visitor); + currentInterpreter.getEntryListeners().add(visitor); } blocker.install(currentInterpreter); @@ -386,11 +387,13 @@ public class DebuggerMainWindowController implements Initializable { public void stepOver(ActionEvent actionEvent) { blocker.getStepUntilBlock().addAndGet(1); blocker.unlock(); + pc.stepOver(); } public void stepBack(ActionEvent actionEvent) { System.out.println(blocker.getHistoryLogger()); blocker.unlock(); + pc.stepBack(); } diff --git a/src/main/java/edu/kit/formal/interpreter/ControlFlowNode.java b/src/main/java/edu/kit/formal/interpreter/ControlFlowNode.java index f979aee6..d13e2bbb 100644 --- a/src/main/java/edu/kit/formal/interpreter/ControlFlowNode.java +++ b/src/main/java/edu/kit/formal/interpreter/ControlFlowNode.java @@ -5,20 +5,21 @@ import edu.kit.formal.proofscriptparser.ast.ASTNode; /** * ControlFlowNode for ControlFlowGraph to look up step-edges for teh debugger. */ +@Deprecated public class ControlFlowNode { - ASTNode scriptstmt; + edu.kit.formal.proofscriptparser.ast.ASTNode scriptstmt; public ControlFlowNode(ASTNode node) { this.setScriptstmt(node); } - public ASTNode getScriptstmt() { + public edu.kit.formal.proofscriptparser.ast.ASTNode getScriptstmt() { return scriptstmt; } - public void setScriptstmt(ASTNode scriptstmt) { + public void setScriptstmt(edu.kit.formal.proofscriptparser.ast.ASTNode scriptstmt) { this.scriptstmt = scriptstmt; } @@ -34,4 +35,5 @@ public class ControlFlowNode { return sb.toString(); } + } diff --git a/src/main/java/edu/kit/formal/interpreter/EdgeTypes.java b/src/main/java/edu/kit/formal/interpreter/EdgeTypes.java index 658aa3b7..af433117 100644 --- a/src/main/java/edu/kit/formal/interpreter/EdgeTypes.java +++ b/src/main/java/edu/kit/formal/interpreter/EdgeTypes.java @@ -4,5 +4,5 @@ package edu.kit.formal.interpreter; * Created by sarah on 6/20/17. */ public enum EdgeTypes { - STEP_INTO, STEP_OVER, STEP_BACK, STEP_RETURN; + STEP_INTO, STEP_OVER, STEP_BACK, STEP_RETURN, STEP_OVER_COND, STATE_FLOW; } diff --git a/src/main/java/edu/kit/formal/interpreter/PTreeNode.java b/src/main/java/edu/kit/formal/interpreter/PTreeNode.java index 5090b4b6..ea7c6213 100644 --- a/src/main/java/edu/kit/formal/interpreter/PTreeNode.java +++ b/src/main/java/edu/kit/formal/interpreter/PTreeNode.java @@ -1,6 +1,5 @@ package edu.kit.formal.interpreter; -import edu.kit.formal.interpreter.data.GoalNode; import edu.kit.formal.interpreter.data.KeyData; import edu.kit.formal.interpreter.data.State; import edu.kit.formal.proofscriptparser.ast.ASTNode; @@ -10,7 +9,7 @@ import edu.kit.formal.proofscriptparser.ast.ASTNode; * 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 state; ASTNode scriptstmt; @@ -18,11 +17,11 @@ public class PTreeNode { this.setScriptstmt(node); } - public State> getState() { + public State getState() { return state; } - public void setState(State> state) { + public void setState(State state) { this.state = state; } @@ -42,10 +41,15 @@ public class PTreeNode { StringBuilder sb = new StringBuilder(); sb.append("Node {"); if (scriptstmt != null) { - sb.append(scriptstmt.toString()); + sb.append(scriptstmt.getNodeName() + "\n"); } else { sb.append("No Stmt"); } + if (hasState()) { + sb.append("\nState " + state.getGoals() + "\n"); + } else { + sb.append("No State yet"); + } sb.append("}"); return sb.toString(); } diff --git a/src/main/java/edu/kit/formal/interpreter/ProgramFlowVisitor.java b/src/main/java/edu/kit/formal/interpreter/ProgramFlowVisitor.java index 558514df..86208a45 100644 --- a/src/main/java/edu/kit/formal/interpreter/ProgramFlowVisitor.java +++ b/src/main/java/edu/kit/formal/interpreter/ProgramFlowVisitor.java @@ -2,50 +2,60 @@ package edu.kit.formal.interpreter; import com.google.common.graph.MutableValueGraph; import com.google.common.graph.ValueGraphBuilder; -import edu.kit.formal.interpreter.data.KeyData; import edu.kit.formal.interpreter.funchdl.CommandLookup; import edu.kit.formal.interpreter.funchdl.ProofScriptHandler; import edu.kit.formal.proofscriptparser.DefaultASTVisitor; import edu.kit.formal.proofscriptparser.ast.*; +import java.util.List; + /** * Visitor to create ProgramFlowGraph */ public class ProgramFlowVisitor extends DefaultASTVisitor { + /** + * Lookup for names of scripts + */ private final CommandLookup functionLookup; - private ControlFlowNode lastNode; - private MutableValueGraph graph = ValueGraphBuilder.directed().allowsSelfLoops(true).build(); + /** + * Last visited Node + */ + private ASTNode lastNode; + + /** + * Control Flow Graph + */ + private MutableValueGraph graph = ValueGraphBuilder.directed().allowsSelfLoops(true).build(); - private Interpreter inter; public ProgramFlowVisitor(CommandLookup functionLookup) { this.functionLookup = functionLookup; } - public MutableValueGraph getGraph() { + public MutableValueGraph getGraph() { return graph; } @Override public Void visit(ProofScript proofScript) { - ControlFlowNode scriptNode = new ControlFlowNode(proofScript); - lastNode = scriptNode; + + lastNode = proofScript; return this.visit(proofScript.getBody()); } @Override public Void visit(AssignmentStatement assignment) { - ControlFlowNode node = new ControlFlowNode(assignment); - graph.addNode(node); - lastNode = node; + + graph.addNode(assignment); + lastNode = assignment; return null; } @Override public Void visit(Statements statements) { - ControlFlowNode curLastNode = lastNode; + ASTNode curLastNode = lastNode; for (Statement stmnt : statements) { stmnt.accept(this); graph.putEdgeValue(curLastNode, lastNode, EdgeTypes.STEP_OVER); @@ -58,7 +68,7 @@ public class ProgramFlowVisitor extends DefaultASTVisitor { @Override public Void visit(CallStatement call) { - ControlFlowNode currentNode = new ControlFlowNode(call); + ASTNode currentNode = call; graph.addNode(currentNode); graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_OVER); @@ -73,14 +83,15 @@ public class ProgramFlowVisitor extends DefaultASTVisitor { //Annahme: wenn ich zwischendrin keine return kante habe, dann wird solange durchgegangen, bis eine return kante da ist if (atomic) { - graph.putEdgeValue(currentNode, lastNode, EdgeTypes.STEP_INTO); + // graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_RETURN); ProofScriptHandler psh = (ProofScriptHandler) functionLookup.getBuilder(call); psh.getScript(call.getCommand()).getBody().accept(this); - //verbinde letzten knoten aus auruf mi step return zu aktuellem knoten + //verbinde letzten knoten aus auruf mit step return zu aktuellem knoten graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_RETURN); + graph.putEdgeValue(currentNode, lastNode, EdgeTypes.STEP_INTO); } lastNode = currentNode; @@ -90,30 +101,62 @@ public class ProgramFlowVisitor extends DefaultASTVisitor { @Override public Void visit(ForeachStatement foreach) { - ControlFlowNode currentNode = new ControlFlowNode(foreach); + ASTNode currentNode = foreach; graph.addNode(currentNode); graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_OVER); graph.putEdgeValue(currentNode, lastNode, EdgeTypes.STEP_BACK); lastNode = currentNode; foreach.getBody().accept(this); - graph.putEdgeValue(currentNode, lastNode, EdgeTypes.STEP_RETURN); - lastNode = currentNode; + graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_RETURN); + //lastNode = currentNode; ?? return null; } @Override public Void visit(TheOnlyStatement theOnly) { - return super.visit(theOnly); + ASTNode currentNode = theOnly; + graph.addNode(currentNode); + graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_OVER); + graph.putEdgeValue(currentNode, lastNode, EdgeTypes.STEP_BACK); + lastNode = currentNode; + theOnly.getBody().accept(this); + graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_RETURN); + //lastNode = currentNode; ?? + return null; + } @Override public Void visit(RepeatStatement repeatStatement) { - return super.visit(repeatStatement); + ASTNode currentNode = repeatStatement; + graph.addNode(currentNode); + graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_OVER); + graph.putEdgeValue(currentNode, lastNode, EdgeTypes.STEP_BACK); + lastNode = currentNode; + repeatStatement.getBody().accept(this); + graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_OVER); + lastNode = currentNode; + return null; } @Override public Void visit(CasesStatement casesStatement) { - return super.visit(casesStatement); + ASTNode currentNode = casesStatement; + graph.addNode(currentNode); + graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_OVER); + graph.putEdgeValue(currentNode, lastNode, EdgeTypes.STEP_BACK); + List cases = casesStatement.getCases(); + for (CaseStatement aCase : cases) { + ASTNode caseNode = aCase; + graph.addNode(caseNode); + graph.putEdgeValue(currentNode, caseNode, EdgeTypes.STEP_OVER); //??is this right? + graph.putEdgeValue(caseNode, currentNode, EdgeTypes.STEP_BACK); + lastNode = caseNode; + aCase.getBody().accept(this); + graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_RETURN); + } + lastNode = currentNode; + return null; } @@ -124,9 +167,9 @@ public class ProgramFlowVisitor extends DefaultASTVisitor { graph.nodes().forEach(n -> { sb.append(n.hashCode()) .append(" [label=\"") - .append(n.getScriptstmt().getNodeName()) + .append(n.getNodeName()) .append("@") - .append(n.getScriptstmt().getStartPosition().getLineNumber()) + .append(n.getStartPosition().getLineNumber()) .append("\"]\n"); }); diff --git a/src/main/java/edu/kit/formal/interpreter/ProofTreeController.java b/src/main/java/edu/kit/formal/interpreter/ProofTreeController.java index f5c85b30..1010ed8c 100644 --- a/src/main/java/edu/kit/formal/interpreter/ProofTreeController.java +++ b/src/main/java/edu/kit/formal/interpreter/ProofTreeController.java @@ -2,6 +2,7 @@ package edu.kit.formal.interpreter; import com.google.common.graph.MutableValueGraph; import edu.kit.formal.interpreter.data.KeyData; +import edu.kit.formal.proofscriptparser.ast.ASTNode; import edu.kit.formal.proofscriptparser.ast.ProofScript; /** @@ -10,30 +11,34 @@ import edu.kit.formal.proofscriptparser.ast.ProofScript; * @author S. Grebing */ public class ProofTreeController { - + //TODO Listener auf den Interperter + StateGraphVisitor stateGraphVisitor; /** * ControlFlowGraph to lookup edges */ - private MutableValueGraph controlFlowGraph; - + private MutableValueGraph controlFlowGraph; /** * Graph that is computed on the fly in order to allow stepping */ private MutableValueGraph stateGraph; - /** * Current interpreter */ private Interpreter currentInterpreter; - /** * Current State in graph */ private PTreeNode statePointer; - public ProofTreeController(Interpreter inter, ProofScript mainScript) { + public ProofTreeController(Interpreter inter, ProofScript mainScript, StateGraphVisitor stateGraphVisitor) { this.currentInterpreter = inter; + buildControlFlowGraph(mainScript); + stateGraph = stateGraphVisitor.getStateGraph(); + statePointer = stateGraphVisitor.getRootNode(); + this.stateGraphVisitor = stateGraphVisitor; + // System.out.println(stateGraph.nodes()); + //initializeStateGraph(mainScript); } @@ -48,13 +53,41 @@ public class ProofTreeController { mainScript.accept(visitor); this.controlFlowGraph = visitor.getGraph(); - System.out.println(visitor.asdot()); - // System.out.println(controlFlowGraph); + // System.out.println(visitor.asdot()); } + /* private void initializeStateGraph(ProofScript mainScript){ + stateGraph = ValueGraphBuilder.directed().build(); + + State initState = currentInterpreter.getCurrentState(); + System.out.println(initState); + PTreeNode initNode = new PTreeNode(mainScript); + initNode.setState(initState); + stateGraph.addNode(initNode); + + // statePointer = initNode; + + }*/ + public PTreeNode stepOver() { + PTreeNode current = statePointer; + ASTNode stmt = current.getScriptstmt(); + if (controlFlowGraph.asGraph().nodes().contains(stmt)) { + // System.out.println("\n\nAdjacent:{\n"+controlFlowGraph.asGraph().adjacentNodes(stmt)+"}\n\n\n"); + Object[] nodeArray = controlFlowGraph.asGraph().adjacentNodes(stmt).toArray(); + ASTNode firtSucc = (ASTNode) nodeArray[0]; + for (PTreeNode succ : stateGraph.successors(current)) { + if (succ.getScriptstmt().equals(firtSucc)) { + statePointer = succ; + } + } + } + //System.out.println(stateGraphVisitor.asdot()); + + + return null; } diff --git a/src/main/java/edu/kit/formal/interpreter/StateGraphVisitor.java b/src/main/java/edu/kit/formal/interpreter/StateGraphVisitor.java new file mode 100644 index 00000000..e5289bb1 --- /dev/null +++ b/src/main/java/edu/kit/formal/interpreter/StateGraphVisitor.java @@ -0,0 +1,87 @@ +package edu.kit.formal.interpreter; + + +import com.google.common.graph.MutableValueGraph; +import com.google.common.graph.ValueGraphBuilder; +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.ast.ASTNode; +import edu.kit.formal.proofscriptparser.ast.ProofScript; + +/** + * Created by sarah on 6/26/17. + */ +public class StateGraphVisitor extends DefaultASTVisitor { + Interpreter currentInterpreter; + /** + * Graph that is computed on the fly in order to allow stepping + */ + private MutableValueGraph stateGraph; + private PTreeNode root; + + + private PTreeNode lastNode; + + public StateGraphVisitor(Interpreter inter, ProofScript mainScript) { + stateGraph = ValueGraphBuilder.directed().build(); + this.currentInterpreter = inter; + State initState = currentInterpreter.getCurrentState(); + System.out.println(initState); + PTreeNode initNode = new PTreeNode(mainScript); + initNode.setState(initState); + stateGraph.addNode(initNode); + root = initNode; + lastNode = initNode; + + } + + public MutableValueGraph getStateGraph() { + return stateGraph; + } + + public PTreeNode getRootNode() { + return root; + } + + public PTreeNode getLastNode() { + return lastNode; + } + + @Override + public Void defaultVisit(ASTNode node) { + PTreeNode newStateNode = new PTreeNode(node); + newStateNode.setState(currentInterpreter.getCurrentState()); + stateGraph.addNode(newStateNode); + stateGraph.putEdgeValue(lastNode, newStateNode, EdgeTypes.STATE_FLOW); + lastNode = newStateNode; + System.out.println(asdot()); + return null; + } + + public String asdot() { + StringBuilder sb = new StringBuilder(); + sb.append("digraph G {\nnode [shape=rect]\n "); + + stateGraph.nodes().forEach(n -> { + sb.append(n.hashCode()) + .append(" [label=\"") + .append(n.getScriptstmt().getNodeName()) + .append("@") + .append(n.getScriptstmt().getStartPosition().getLineNumber()) + .append("\"]\n"); + }); + + stateGraph.edges().forEach(edge -> { + sb.append(edge.source().hashCode()) + .append(" -> ") + .append(edge.target().hashCode()) + .append(" [label=\"") + .append(stateGraph.edgeValue(edge.source(), edge.target()).name()) + .append("\"]\n"); + }); + + sb.append("}"); + return sb.toString(); + } +} -- 2.26.2