From a8e7207d35f1c6f7a15b1513d0ffb804aef2acd9 Mon Sep 17 00:00:00 2001 From: Sarah Grebing Date: Tue, 27 Jun 2017 15:06:29 +0200 Subject: [PATCH] Interim (incomplete commit) --- .../DebuggerMainWindowController.java | 21 +++---- .../formal/interpreter/ControlFlowNode.java | 17 ++++-- .../interpreter/ProgramFlowVisitor.java | 60 ++++++++++++++++--- .../interpreter/ProofTreeController.java | 56 ++++++++--------- .../formal/interpreter/StateGraphVisitor.java | 48 ++++++++++++--- .../interpreter/contraposition/recursion.kps | 12 ++++ 6 files changed, 154 insertions(+), 60 deletions(-) create mode 100644 src/test/resources/edu/kit/formal/interpreter/contraposition/recursion.kps 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 8d78eebf..67097f94 100644 --- a/src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java +++ b/src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java @@ -52,7 +52,7 @@ public class DebuggerMainWindowController implements Initializable { private final PuppetMaster blocker = new PuppetMaster(); private SimpleBooleanProperty debugMode = new SimpleBooleanProperty(false); - // private GoalOptionsMenu goalOptionsMenu = new GoalOptionsMenu(); + @FXML private Pane rootPane; @@ -62,12 +62,9 @@ public class DebuggerMainWindowController implements Initializable { * Code Area * **********************************************************************************************************/ - //@FXML - //private ScriptArea scriptArea; @FXML private ScriptTabPane tabPane; - //@FXML - //private Tab startTab; + /*********************************************************************************************************** * MenuBar * **********************************************************************************************************/ @@ -113,7 +110,11 @@ public class DebuggerMainWindowController implements Initializable { private ObservableBooleanValue executeNotPossible = interpreterService.runningProperty().or(facade.readyToExecuteProperty().not()); + /** + * Controller for debugging functions + */ 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); @@ -226,14 +227,14 @@ public class DebuggerMainWindowController implements Initializable { Interpreter currentInterpreter = ib.build(); if (debugMode) { - blocker.getStepUntilBlock().set(1); + //blocker.getStepUntilBlock().set(1); //for stepping functionality pc = new ProofTreeController(currentInterpreter, scripts.get(0)); currentInterpreter.getEntryListeners().add(pc.getStateVisitor()); } - blocker.install(currentInterpreter); + // blocker.install(currentInterpreter); //highlight signature of main script tabPane.getSelectedScriptArea().setDebugMark(scripts.get(0).getStartPosition().getLineNumber()); @@ -388,8 +389,8 @@ public class DebuggerMainWindowController implements Initializable { } public void stepOver(ActionEvent actionEvent) { - blocker.getStepUntilBlock().addAndGet(1); - blocker.unlock(); + // blocker.getStepUntilBlock().addAndGet(1); + // blocker.unlock(); pc.stepOver(); } @@ -487,7 +488,7 @@ public class DebuggerMainWindowController implements Initializable { private void updateView() { //check proof - // check state for empty/error goal nodes leer + //check state for empty/error goal nodes //currentGoals.set(state.getGoals()); //currentSelectedGoal.set(state.getSelectedGoalNode()); blocker.publishState(); diff --git a/src/main/java/edu/kit/formal/interpreter/ControlFlowNode.java b/src/main/java/edu/kit/formal/interpreter/ControlFlowNode.java index 30ca34c0..529e4f6f 100644 --- a/src/main/java/edu/kit/formal/interpreter/ControlFlowNode.java +++ b/src/main/java/edu/kit/formal/interpreter/ControlFlowNode.java @@ -2,7 +2,7 @@ package edu.kit.formal.interpreter; import edu.kit.formal.proofscriptparser.ast.ASTNode; -import java.util.ArrayList; +import java.util.LinkedList; import java.util.List; /** @@ -11,18 +11,27 @@ import java.util.List; public class ControlFlowNode { + /** + * Statement node + */ private ASTNode scriptstmt; - private List callCtx = new ArrayList<>(); + + /** + * Call context + */ + private LinkedList callCtx = new LinkedList<>(); + public ControlFlowNode(ASTNode node) { this.setScriptstmt(node); } + public List getCallCtx() { return callCtx; } - public void setCallCtx(List callCtx) { + public void setCallCtx(LinkedList callCtx) { this.callCtx = callCtx; } @@ -38,7 +47,7 @@ public class ControlFlowNode { StringBuilder sb = new StringBuilder(); sb.append("Node {"); if (scriptstmt != null) { - sb.append(scriptstmt.getNodeName().toString()); + sb.append(scriptstmt.getNodeName().toString() + "@" + scriptstmt.getStartPosition()); } else { sb.append("No Stmt"); } diff --git a/src/main/java/edu/kit/formal/interpreter/ProgramFlowVisitor.java b/src/main/java/edu/kit/formal/interpreter/ProgramFlowVisitor.java index b9b2cbda..0c1f93ce 100644 --- a/src/main/java/edu/kit/formal/interpreter/ProgramFlowVisitor.java +++ b/src/main/java/edu/kit/formal/interpreter/ProgramFlowVisitor.java @@ -1,5 +1,6 @@ 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.interpreter.funchdl.CommandLookup; @@ -7,8 +8,7 @@ import edu.kit.formal.interpreter.funchdl.ProofScriptHandler; import edu.kit.formal.proofscriptparser.DefaultASTVisitor; import edu.kit.formal.proofscriptparser.ast.*; -import java.util.ArrayList; -import java.util.List; +import java.util.*; /** * Visitor to create ProgramFlowGraph @@ -19,7 +19,7 @@ public class ProgramFlowVisitor extends DefaultASTVisitor { * Lookup for names of scripts */ private final CommandLookup functionLookup; - + private Map mappingOfNodes; /** * Last visited Node */ @@ -30,20 +30,45 @@ public class ProgramFlowVisitor extends DefaultASTVisitor { */ private MutableValueGraph graph = ValueGraphBuilder.directed().allowsSelfLoops(true).build(); - private List context = new ArrayList<>(); + private LinkedList context = new LinkedList<>(); public ProgramFlowVisitor(CommandLookup functionLookup) { this.functionLookup = functionLookup; + mappingOfNodes = new HashMap<>(); } public MutableValueGraph getGraph() { return graph; } + + public Set> getAllEdgesForNodeAsTarget(ASTNode node) { + + ControlFlowNode assocNode = mappingOfNodes.get(node); + if (assocNode != null) { + Set> edges = new HashSet<>(); + + graph.edges().forEach(e -> { + if (e.target().equals(assocNode)) { + + edges.add(e); + System.out.println(e.target()); + System.out.println(e.source()); + System.out.println(graph.edgeValue(e.target(), e.source())); + } + }); + return edges; + } else { + return Collections.EMPTY_SET; + } + } + + @Override public Void visit(ProofScript proofScript) { ControlFlowNode scriptNode = new ControlFlowNode(proofScript); + mappingOfNodes.put(proofScript, scriptNode); graph.addNode(scriptNode); System.out.println("\n" + scriptNode + "\n"); lastNode = scriptNode; @@ -55,6 +80,7 @@ public class ProgramFlowVisitor extends DefaultASTVisitor { public Void visit(AssignmentStatement assignment) { ControlFlowNode assignmentNode = new ControlFlowNode(assignment); + mappingOfNodes.put(assignment, assignmentNode); graph.addNode(assignmentNode); System.out.println("\n" + assignmentNode + "\n"); lastNode = assignmentNode; @@ -74,32 +100,45 @@ public class ProgramFlowVisitor extends DefaultASTVisitor { return null; } - //stack wenn atomic false + @Override public Void visit(CallStatement call) { ControlFlowNode currentNode = new ControlFlowNode(call); if (!context.isEmpty()) { currentNode.setCallCtx(context); } + mappingOfNodes.put(call, currentNode); graph.addNode(currentNode); - System.out.println("\n" + currentNode + "\n"); graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_OVER); graph.putEdgeValue(currentNode, lastNode, EdgeTypes.STEP_BACK); + lastNode = currentNode; boolean atomic = functionLookup.isAtomic(call); //Annahme: wenn ich zwischendrin keine return kante habe, dann wird solange durchgegangen, bis eine return kante da ist if (atomic) { + + LinkedList copiedContext = new LinkedList<>(); + + //to check whether context is restored properly, copy context before call + context.stream().forEach(e -> { + copiedContext.add(e); + }); context.add(call); -// 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 mit step return zu aktuellem knoten graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_RETURN); graph.putEdgeValue(currentNode, lastNode, EdgeTypes.STEP_INTO); + + context.removeLast(); + //check if context is restored properly + //copiedcontext == context + } - context.remove(call); + lastNode = currentNode; return null; @@ -108,6 +147,7 @@ public class ProgramFlowVisitor extends DefaultASTVisitor { @Override public Void visit(ForeachStatement foreach) { ControlFlowNode currentNode = new ControlFlowNode(foreach); + mappingOfNodes.put(foreach, currentNode); graph.addNode(currentNode); System.out.println("\n" + currentNode + "\n"); graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_OVER); @@ -122,6 +162,7 @@ public class ProgramFlowVisitor extends DefaultASTVisitor { @Override public Void visit(TheOnlyStatement theOnly) { ControlFlowNode currentNode = new ControlFlowNode(theOnly); + mappingOfNodes.put(theOnly, currentNode); graph.addNode(currentNode); System.out.println("\n" + currentNode + "\n"); graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_OVER); @@ -137,6 +178,7 @@ public class ProgramFlowVisitor extends DefaultASTVisitor { @Override public Void visit(RepeatStatement repeatStatement) { ControlFlowNode currentNode = new ControlFlowNode(repeatStatement); + mappingOfNodes.put(repeatStatement, currentNode); graph.addNode(currentNode); System.out.println("\n" + currentNode + "\n"); graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_OVER); @@ -151,6 +193,7 @@ public class ProgramFlowVisitor extends DefaultASTVisitor { @Override public Void visit(CasesStatement casesStatement) { ControlFlowNode currentNode = new ControlFlowNode(casesStatement); + mappingOfNodes.put(casesStatement, currentNode); graph.addNode(currentNode); System.out.println("\n" + currentNode + "\n"); graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_OVER); @@ -158,6 +201,7 @@ public class ProgramFlowVisitor extends DefaultASTVisitor { List cases = casesStatement.getCases(); for (CaseStatement aCase : cases) { ControlFlowNode caseNode = new ControlFlowNode(aCase); + mappingOfNodes.put(aCase, caseNode); graph.addNode(caseNode); System.out.println("\n" + caseNode + "\n"); graph.putEdgeValue(currentNode, caseNode, EdgeTypes.STEP_OVER); //??is this right? diff --git a/src/main/java/edu/kit/formal/interpreter/ProofTreeController.java b/src/main/java/edu/kit/formal/interpreter/ProofTreeController.java index 5d4d8ffe..c04a3b9d 100644 --- a/src/main/java/edu/kit/formal/interpreter/ProofTreeController.java +++ b/src/main/java/edu/kit/formal/interpreter/ProofTreeController.java @@ -1,9 +1,8 @@ package edu.kit.formal.interpreter; -import com.google.common.graph.MutableValueGraph; +import edu.kit.formal.gui.controller.PuppetMaster; import edu.kit.formal.interpreter.data.KeyData; import edu.kit.formal.proofscriptparser.Visitor; -import edu.kit.formal.proofscriptparser.ast.ASTNode; import edu.kit.formal.proofscriptparser.ast.ProofScript; /** @@ -14,17 +13,18 @@ import edu.kit.formal.proofscriptparser.ast.ProofScript; public class ProofTreeController { /** - * Visitor to retrieve state graph + * To control stepping */ - private StateGraphVisitor stateGraphVisitor; + private final PuppetMaster blocker = new PuppetMaster(); /** - * ControlFlowGraph to lookup edges + * Visitor to retrieve state graph */ - private MutableValueGraph controlFlowGraph; + private StateGraphVisitor stateGraphVisitor; /** * Graph that is computed on the fly in order to allow stepping */ - private MutableValueGraph stateGraph; + + private ProgramFlowVisitor controlFlowGraphVisitor; /** * Current interpreter */ @@ -35,17 +35,15 @@ public class ProofTreeController { private PTreeNode statePointer; public ProofTreeController(Interpreter inter, ProofScript mainScript) { - this.currentInterpreter = inter; + blocker.deinstall(); + this.currentInterpreter = inter; buildControlFlowGraph(mainScript); - this.stateGraphVisitor = new StateGraphVisitor(inter, mainScript, this.controlFlowGraph); - stateGraph = stateGraphVisitor.getStateGraph(); + this.stateGraphVisitor = new StateGraphVisitor(inter, mainScript, controlFlowGraphVisitor); statePointer = stateGraphVisitor.getRootNode(); - // System.out.println(stateGraph.nodes()); - //initializeStateGraph(mainScript); - - + blocker.getStepUntilBlock().set(1); + blocker.install(currentInterpreter); } /** @@ -54,30 +52,26 @@ public class ProofTreeController { * @param mainScript */ private void buildControlFlowGraph(ProofScript mainScript) { - ProgramFlowVisitor visitor = new ProgramFlowVisitor(currentInterpreter.getFunctionLookup()); - mainScript.accept(visitor); - this.controlFlowGraph = visitor.getGraph(); - System.out.println(visitor.asdot()); + 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(); + + + if (statePointer == null) { this.statePointer = stateGraphVisitor.getLastNode(); } - PTreeNode current = statePointer; - ASTNode stmt = current.getScriptstmt(); - System.out.println("CurrentPointer: " + stmt.getNodeName() + "@" + stmt.getStartPosition()); - if (controlFlowGraph.asGraph().nodes().contains(stmt)) { - // Object[] nodeArray = controlFlowGraph.asGraph().adjacentNodes(stmt).toArray(); - // ControlFlowNode firtSucc = (ControlFlowNode) nodeArray[0]; - // for (PTreeNode succ : stateGraph.successors(current)) { - // if (succ.getScriptstmt().equals(firtSucc)) { - // statePointer = succ; - // } - // } - } - //System.out.println(stateGraphVisitor.asdot()); + //PTreeNode current = statePointer; + //ASTNode stmt = current.getScriptstmt(); + //System.out.println("CurrentPointer: " + stmt.getNodeName() + "@" + stmt.getStartPosition()); + return null; } diff --git a/src/main/java/edu/kit/formal/interpreter/StateGraphVisitor.java b/src/main/java/edu/kit/formal/interpreter/StateGraphVisitor.java index 5b5dfffe..24183a9b 100644 --- a/src/main/java/edu/kit/formal/interpreter/StateGraphVisitor.java +++ b/src/main/java/edu/kit/formal/interpreter/StateGraphVisitor.java @@ -1,40 +1,53 @@ 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.proofscriptparser.DefaultASTVisitor; import edu.kit.formal.proofscriptparser.ast.*; +import java.util.Set; + /** * Created by sarah on 6/26/17. */ public class StateGraphVisitor extends DefaultASTVisitor { - Interpreter currentInterpreter; + /** + * Interpreter + */ + private Interpreter currentInterpreter; /** * Graph that is computed on the fly in order to allow stepping */ private MutableValueGraph stateGraph; + /** + * Root of state graph + */ private PTreeNode root; - + /** + * last added node + */ private PTreeNode lastNode; /** - * Control Flow Graph + * Visitor for control flow graph */ - private MutableValueGraph graph; + private ProgramFlowVisitor cfgVisitor; + - public StateGraphVisitor(Interpreter inter, ProofScript mainScript, MutableValueGraph cfg) { + public StateGraphVisitor(Interpreter inter, ProofScript mainScript, ProgramFlowVisitor cfgVisitor) { stateGraph = ValueGraphBuilder.directed().build(); this.currentInterpreter = inter; - graph = cfg; - System.out.println(cfg.nodes().stream().toString()); + this.cfgVisitor = cfgVisitor; + } + public MutableValueGraph getStateGraph() { return stateGraph; } @@ -47,16 +60,35 @@ public class StateGraphVisitor extends DefaultASTVisitor { return lastNode; } + //public (ControlFlowNode, ControlflowNode, Edge) getReturnEdge(ASTNode node) + + + //public Node findNode(ASTNode, state){} + + /** + * Creat a new node for the state graph and add edges to already existing nodes + * + * @param node + * @return + */ public Void createNewNode(ASTNode node) { + PTreeNode newStateNode = new PTreeNode(node); newStateNode.setState(currentInterpreter.getCurrentState()); stateGraph.addNode(newStateNode); + 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); } + lastNode = newStateNode; return null; @@ -134,4 +166,6 @@ public class StateGraphVisitor extends DefaultASTVisitor { sb.append("}"); return sb.toString(); } + + } diff --git a/src/test/resources/edu/kit/formal/interpreter/contraposition/recursion.kps b/src/test/resources/edu/kit/formal/interpreter/contraposition/recursion.kps new file mode 100644 index 00000000..dfba573d --- /dev/null +++ b/src/test/resources/edu/kit/formal/interpreter/contraposition/recursion.kps @@ -0,0 +1,12 @@ +script t(){ + f; + impRight; +} + +script f(){ + g; +} + +script g(){ + f; +} \ No newline at end of file -- 2.26.2