Commit 7483d913 authored by Lulu Luong's avatar Lulu Luong

Branchlabels verzweigung buggy

foreach afterstatements not defined
icons added
parent 5f28b2fc
Pipeline #26633 passed with stages
in 2 minutes and 52 seconds
package edu.kit.iti.formal.psdbg.gui.controls.ScriptTree;
import de.uka.ilkd.key.proof.Node;
import edu.kit.iti.formal.psdbg.gui.controls.TreeNode;
import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
import edu.kit.iti.formal.psdbg.interpreter.dbg.PTreeNode;
import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
import edu.kit.iti.formal.psdbg.parser.ast.GuardedCaseStatement;
import edu.kit.iti.formal.psdbg.parser.ast.MatchExpression;
import edu.kit.iti.formal.psdbg.parser.ast.TermLiteral;
import lombok.Getter;
import lombok.RequiredArgsConstructor;
import lombok.Setter;
/**
* This calss represents a node in the script tree, whcih can be of different kinds.
* The scriptTreeNodes is the model calls for TreeNodes
*/
public class ForeachTreeNode extends AbstractTreeNode {
@Getter
private final PTreeNode<KeyData> scriptState;
@Getter @Setter
private final int linenr;
private final boolean foreachstart;
public ForeachTreeNode(Node node, PTreeNode<KeyData> scriptState, int linenr, boolean foreachstart) {
super(node);
this.scriptState = scriptState;
this.linenr = linenr;
this.foreachstart = foreachstart;
}
@Override
public String toString(){
return scriptState.getStatement().toString()+" with ID "+scriptState.getId();
}
@Override
public TreeNode toTreeNode() {
String label= (foreachstart)? "foreach in line " + linenr + " START": "foreach in line " + linenr + "END";
return new TreeNode(label, getNode());
}
}
\ No newline at end of file
...@@ -24,10 +24,12 @@ public class ScriptTreeNode extends AbstractTreeNode { ...@@ -24,10 +24,12 @@ public class ScriptTreeNode extends AbstractTreeNode {
@Getter @Setter @Getter @Setter
private final int linenr; private final int linenr;
public ScriptTreeNode(Node node, PTreeNode<KeyData> scriptState, int linenr) { public ScriptTreeNode(Node node, PTreeNode<KeyData> scriptState, int linenr) {
super(node); super(node);
this.scriptState = scriptState; this.scriptState = scriptState;
this.linenr = linenr; this.linenr = linenr;
} }
@Override @Override
...@@ -42,9 +44,7 @@ public class ScriptTreeNode extends AbstractTreeNode { ...@@ -42,9 +44,7 @@ public class ScriptTreeNode extends AbstractTreeNode {
String matchexpression = ((TermLiteral) ((MatchExpression) ((GuardedCaseStatement) scriptState.getStatement()).getGuard()).getPattern()).getContent(); String matchexpression = ((TermLiteral) ((MatchExpression) ((GuardedCaseStatement) scriptState.getStatement()).getGuard()).getPattern()).getContent();
label = "match ("+ matchexpression +") in line " + linenr; label = "match ("+ matchexpression +") in line " + linenr;
} else { } else {
label = (scriptState.getStatement() instanceof CallStatement)? label = ((CallStatement)scriptState.getStatement()).getCommand() + " (line " + linenr + ")";
((CallStatement)scriptState.getStatement()).getCommand() + " (line " + linenr + ")"
: "foreach in line " + linenr + " START";
} }
......
...@@ -4,10 +4,7 @@ import com.google.common.graph.GraphBuilder; ...@@ -4,10 +4,7 @@ import com.google.common.graph.GraphBuilder;
import com.google.common.graph.MutableGraph; import com.google.common.graph.MutableGraph;
import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Node;
import de.uka.ilkd.key.rule.BlockContractBuilders; import de.uka.ilkd.key.rule.BlockContractBuilders;
import edu.kit.iti.formal.psdbg.gui.controls.ScriptTree.AbstractTreeNode; import edu.kit.iti.formal.psdbg.gui.controls.ScriptTree.*;
import edu.kit.iti.formal.psdbg.gui.controls.ScriptTree.BranchLabelNode;
import edu.kit.iti.formal.psdbg.gui.controls.ScriptTree.DummyGoalNode;
import edu.kit.iti.formal.psdbg.gui.controls.ScriptTree.ScriptTreeNode;
import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode; import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
import edu.kit.iti.formal.psdbg.interpreter.data.KeyData; import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
import edu.kit.iti.formal.psdbg.interpreter.data.State; import edu.kit.iti.formal.psdbg.interpreter.data.State;
...@@ -39,6 +36,8 @@ public class ScriptTreeGraph { ...@@ -39,6 +36,8 @@ public class ScriptTreeGraph {
private PTreeNode<KeyData> nextPtreeNode; private PTreeNode<KeyData> nextPtreeNode;
private List<PTreeNode<KeyData>> sortedList; private List<PTreeNode<KeyData>> sortedList;
private HashMap<Node, PTreeNode> foreachNodes;
private final MutableGraph<AbstractTreeNode> graph = private final MutableGraph<AbstractTreeNode> graph =
GraphBuilder.directed().allowsSelfLoops(false).build(); GraphBuilder.directed().allowsSelfLoops(false).build();
...@@ -48,6 +47,7 @@ public class ScriptTreeGraph { ...@@ -48,6 +47,7 @@ public class ScriptTreeGraph {
if(currentNode == null) return; if(currentNode == null) return;
ScriptTreeNode rootNode = new ScriptTreeNode(root, rootPTreeNode, rootPTreeNode.getStatement().getStartPosition().getLineNumber()); ScriptTreeNode rootNode = new ScriptTreeNode(root, rootPTreeNode, rootPTreeNode.getStatement().getStartPosition().getLineNumber());
mapping = new HashMap<>(); mapping = new HashMap<>();
foreachNodes = new HashMap<>();
front = new ArrayList<>(); front = new ArrayList<>();
sortedList = new ArrayList<>(); sortedList = new ArrayList<>();
State<KeyData> stateAfterStmt = rootPTreeNode.getStateAfterStmt(); State<KeyData> stateAfterStmt = rootPTreeNode.getStateAfterStmt();
...@@ -100,7 +100,7 @@ public class ScriptTreeGraph { ...@@ -100,7 +100,7 @@ public class ScriptTreeGraph {
//set children //set children
for (GoalNode<KeyData> gn: next.getStateAfterStmt().getGoals()) { for (GoalNode<KeyData> gn: next.getStateAfterStmt().getGoals()) {
if(mapping.get(gn.getData().getNode()).getParent() != null) if(mapping.get(gn.getData().getNode()) != null && mapping.get(gn.getData().getNode()).getParent() != null)
mapping.get(gn.getData().getNode()).setParent(currentTreenode); mapping.get(gn.getData().getNode()).setParent(currentTreenode);
addToChildren(currentNode, mapping.get(gn.getData().getNode())); addToChildren(currentNode, mapping.get(gn.getData().getNode()));
...@@ -120,6 +120,7 @@ public class ScriptTreeGraph { ...@@ -120,6 +120,7 @@ public class ScriptTreeGraph {
* @param atn * @param atn
*/ */
private void addToChildren(Node node, AbstractTreeNode atn) { private void addToChildren(Node node, AbstractTreeNode atn) {
if(atn == null) return;
if(mapping.get(node) == atn) return; if(mapping.get(node) == atn) return;
if (mapping.get(node).getChildren() == null) { if (mapping.get(node).getChildren() == null) {
List<AbstractTreeNode> childlist = new ArrayList<>(); List<AbstractTreeNode> childlist = new ArrayList<>();
...@@ -270,18 +271,8 @@ public class ScriptTreeGraph { ...@@ -270,18 +271,8 @@ public class ScriptTreeGraph {
switch (children.size()) { switch (children.size()) {
case 0: case 0:
/*
DummyGoalNode goalnode = new DummyGoalNode(nextPtreeNode.getStateBeforeStmt().getSelectedGoalNode().getData().getNode(), nextPtreeNode.getStateAfterStmt().getGoals().size() == 0);
goalnode.setParent(sn);
List<AbstractTreeNode> childlist = new ArrayList<>();
childlist.add(goalnode);
sn.setChildren(childlist);
putIntoMapping(sn.getNode(), goalnode);*/
putIntoFront(n); putIntoFront(n);
checkIfForeachEnd(n);
break; break;
case 1: case 1:
putIntoMapping(children.get(0).getData().getNode(), null); putIntoMapping(children.get(0).getData().getNode(), null);
...@@ -295,12 +286,13 @@ public class ScriptTreeGraph { ...@@ -295,12 +286,13 @@ public class ScriptTreeGraph {
List<BranchLabelNode> branchlabel = getBranchLabels(nextPtreeNode.getStateBeforeStmt().getSelectedGoalNode(), gn); List<BranchLabelNode> branchlabel = getBranchLabels(nextPtreeNode.getStateBeforeStmt().getSelectedGoalNode(), gn);
BranchLabelNode branchNode; BranchLabelNode branchNode;
if(branchlabel != null) { if(branchlabel.size() != 0) {
//TODO: insertBranchLabels(branchlabel); insertBranchLabels(node, branchlabel);
/*
branchNode = new BranchLabelNode(node, branchlabel.toString()); branchNode = new BranchLabelNode(node, branchlabel.toString());
mapping.put(node, branchNode); mapping.put(node, branchNode);
*/
}else{ }else{
branchNode = new BranchLabelNode(node, "Case " + branchcounter); branchNode = new BranchLabelNode(node, "Case " + branchcounter);
mapping.put(node, branchNode); mapping.put(node, branchNode);
...@@ -310,6 +302,11 @@ public class ScriptTreeGraph { ...@@ -310,6 +302,11 @@ public class ScriptTreeGraph {
putIntoFront(node); putIntoFront(node);
} }
} }
if(children.size() > 0) {
children.forEach(k -> checkIfForeachEnd(k.getData().getNode()));
}
return null; return null;
} }
...@@ -331,12 +328,21 @@ public class ScriptTreeGraph { ...@@ -331,12 +328,21 @@ public class ScriptTreeGraph {
} }
@Override @Override
public Void visit(ForeachStatement foreachStatement){ public Void visit(ForeachStatement foreachStatement) {
List<GoalNode<KeyData>> goals = nextPtreeNode.getStateBeforeStmt().getGoals(); List<GoalNode<KeyData>> goals = nextPtreeNode.getStateBeforeStmt().getGoals();
if(goals.size() == 0) return null; if (goals.size() == 0) return null;
goals.forEach(k -> putIntoMapping(k.getData().getNode(), new ScriptTreeNode(k.getData().getNode(), nextPtreeNode, nextPtreeNode.getStatement().getStartPosition().getLineNumber())));return null;} goals.forEach(k -> putIntoMapping(k.getData().getNode(), new ForeachTreeNode(k.getData().getNode(), nextPtreeNode, nextPtreeNode.getStatement().getStartPosition().getLineNumber(),true)));
//TODO: add end foreach
// add to foreachNodes lsit
if (nextPtreeNode.getStateAfterStmt() != null) {
List<GoalNode<KeyData>> aftergoals = nextPtreeNode.getStateAfterStmt().getGoals();
aftergoals.forEach(k -> foreachNodes.put(k.getData().getNode(), nextPtreeNode));
}
return null;
}
} }
/** /**
...@@ -345,7 +351,8 @@ public class ScriptTreeGraph { ...@@ -345,7 +351,8 @@ public class ScriptTreeGraph {
* @param treeNode * @param treeNode
*/ */
private void putIntoMapping (Node node, AbstractTreeNode treeNode){ private void putIntoMapping (Node node, AbstractTreeNode treeNode){
if(treeNode == null)
return;
if (mapping.get(node) == null) { if (mapping.get(node) == null) {
mapping.put(node, treeNode); mapping.put(node, treeNode);
} else { } else {
...@@ -359,26 +366,64 @@ public class ScriptTreeGraph { ...@@ -359,26 +366,64 @@ public class ScriptTreeGraph {
} }
} }
private void checkIfForeachEnd(Node n) {
if(foreachNodes.containsKey(n)) {
PTreeNode ptn = foreachNodes.get(n);
putIntoMapping(n, new ForeachTreeNode(n, ptn, ptn.getStatement().getStartPosition().getLineNumber(), false));
}
}
private List<BranchLabelNode> getBranchLabels(GoalNode<KeyData> parent, GoalNode<KeyData> child) { private List<BranchLabelNode> getBranchLabels(GoalNode<KeyData> parent, GoalNode<KeyData> child) {
List<BranchLabelNode> branchlabels = new ArrayList<>(); List<BranchLabelNode> branchlabels = new ArrayList<>();
Node parentnode = parent.getData().getNode(); Node parentnode = parent.getData().getNode();
Node childnode = child.getData().getNode(); Node childnode = child.getData().getNode();
if(childnode.getNodeInfo().getBranchLabel() != null && isBranchLabel(childnode.getNodeInfo().getBranchLabel())) branchlabels.add( new BranchLabelNode(childnode, childnode.getNodeInfo().getBranchLabel())); if(childnode.getNodeInfo().getBranchLabel() != null && isBranchLabel(childnode.getNodeInfo().getBranchLabel())) branchlabels.add( new BranchLabelNode(childnode, childnode.getNodeInfo().getBranchLabel()));
if(childnode == null) return branchlabels;
while(childnode.parent() != parentnode) { while(childnode.parent() != parentnode) {
if(childnode.getNodeInfo().getBranchLabel() != null && isBranchLabel(childnode.getNodeInfo().getBranchLabel())) branchlabels.add( new BranchLabelNode(childnode, childnode.getNodeInfo().getBranchLabel())); if(childnode.getNodeInfo().getBranchLabel() != null
&& isBranchLabel(childnode.getNodeInfo().getBranchLabel())
&& !sameBranchlabelBefore(branchlabels, childnode)) branchlabels.add( new BranchLabelNode(childnode, childnode.getNodeInfo().getBranchLabel()));
childnode = childnode.parent(); childnode = childnode.parent();
} }
return branchlabels; return branchlabels;
} }
private boolean sameBranchlabelBefore(List<BranchLabelNode> branchlabels, Node node) {
if(branchlabels.size() == 0) return false;
return branchlabels.get(branchlabels.size()-1).getLabelName().equals(node.getNodeInfo().getBranchLabel());
}
private boolean isBranchLabel(String label) { private boolean isBranchLabel(String label) {
if (label.contains("rule") || label.contains("rules")) return false; if (label.contains("rule") || label.contains("rules")) return false;
return true; return true;
} }
private void insertBranchLabels(List<BranchLabelNode> branchlabels) { private void insertBranchLabels(Node node, List<BranchLabelNode> branchlabels) {
if(branchlabels == null) return; if(branchlabels == null) return;
mapping.put(node, branchlabels.get(branchlabels.size()-1));
for (int i = branchlabels.size() -2; 0 <= i; i--) {
//to check if Branchlabel already exists
Node n = branchlabels.get(i).getNode();
if(!mapping.containsKey(n) || mapping.get(n) != branchlabels.get(i)) {
putIntoMapping(branchlabels.get(i).getNode(), branchlabels.get(i));
if(0 <= i-1) {
BranchLabelNode child = branchlabels.get(i-1);
BranchLabelNode parent = branchlabels.get(i);
child.setParent(parent);
if(i == branchlabels.size() -2) {
addToChildren(node, child);
} else {
addToChildren(parent.getNode(), child);
}
}
}
}
} }
......
...@@ -10,6 +10,7 @@ ...@@ -10,6 +10,7 @@
<?import javafx.scene.layout.VBox?> <?import javafx.scene.layout.VBox?>
<?import org.dockfx.DockPane?> <?import org.dockfx.DockPane?>
<?import javafx.scene.image.ImageView?> <?import javafx.scene.image.ImageView?>
<?import javafx.scene.image.Image?>
<BorderPane xmlns:fx="http://javafx.com/fxml/1" fx:id="rootPane" xmlns="http://javafx.com/javafx/8.0.112" <BorderPane xmlns:fx="http://javafx.com/fxml/1" fx:id="rootPane" xmlns="http://javafx.com/javafx/8.0.112"
fx:controller="edu.kit.iti.formal.psdbg.gui.controller.DebuggerMain" fx:controller="edu.kit.iti.formal.psdbg.gui.controller.DebuggerMain"
prefWidth="1024" prefHeight="640"> prefWidth="1024" prefHeight="640">
...@@ -184,13 +185,18 @@ ...@@ -184,13 +185,18 @@
</graphic> </graphic>
</CheckMenuItem> </CheckMenuItem>
<CheckMenuItem fx:id="miScriptTree" onAction="#showScriptTree" text="Show Script Tree"> <CheckMenuItem fx:id="miScriptTree" onAction="#showScriptTree" text="Show Script Tree">
<!--
<graphic> <graphic>
<ImageView <ImageView>
image="resources\edu\kit\iti\formal\psdbg\gui\icon\treescript.jpg"> <image>
<Image requestedHeight="22.0" requestedWidth="24.0"
url="/edu/kit/iti/formal/psdbg/gui/icon/treescript.png"
/>
</image>
</ImageView> </ImageView>
</graphic> </graphic>
-->
</CheckMenuItem> </CheckMenuItem>
<CheckMenuItem fx:id="miCommandHelp" onAction="#showCommandHelp" <CheckMenuItem fx:id="miCommandHelp" onAction="#showCommandHelp"
accelerator="F1" accelerator="F1"
...@@ -399,8 +405,14 @@ ...@@ -399,8 +405,14 @@
<ToggleButton fx:id="togBtnScriptTree" onAction="#showScriptTree"> <ToggleButton fx:id="togBtnScriptTree" onAction="#showScriptTree">
<graphic> <graphic>
<!-- FILE-TREE--> <ImageView>
<MaterialDesignIconView glyphName="TREE" size="24.0"/> <image>
<Image requestedHeight="22.0" requestedWidth="24.0"
url="/edu/kit/iti/formal/psdbg/gui/icon/treescript.png"
/>
</image>
</ImageView>
</graphic> </graphic>
<tooltip> <tooltip>
<Tooltip text="Show Script Tree"/> <Tooltip text="Show Script Tree"/>
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment