Commit aa69aa43 authored by Sarah Grebing's avatar Sarah Grebing
Browse files

Merge remote-tracking branch 'origin/grebing_luong_workbranch' into grebing_luong_workbranch

# Conflicts:
#	ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script.kps
#	ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/maxtriplet/script.kps
parents 0054d220 b5c97400
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;
public class PlaceholderNode extends AbstractTreeNode {
public PlaceholderNode(Node node) {
super(node);
}
@Override
public TreeNode toTreeNode() {
return new TreeNode("-PlaceholderNode-", super.getNode());
}
}
...@@ -4,7 +4,6 @@ import com.google.common.collect.Lists; ...@@ -4,7 +4,6 @@ import com.google.common.collect.Lists;
import com.google.common.graph.GraphBuilder; 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 edu.kit.iti.formal.psdbg.gui.controls.ScriptTree.*; import edu.kit.iti.formal.psdbg.gui.controls.ScriptTree.*;
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;
...@@ -14,7 +13,6 @@ import edu.kit.iti.formal.psdbg.parser.DefaultASTVisitor; ...@@ -14,7 +13,6 @@ import edu.kit.iti.formal.psdbg.parser.DefaultASTVisitor;
import edu.kit.iti.formal.psdbg.parser.ast.*; import edu.kit.iti.formal.psdbg.parser.ast.*;
import javafx.scene.control.TreeItem; import javafx.scene.control.TreeItem;
import lombok.Getter; import lombok.Getter;
import sun.reflect.generics.tree.Tree;
import java.util.*; import java.util.*;
...@@ -35,6 +33,8 @@ public class ScriptTreeGraph { ...@@ -35,6 +33,8 @@ public class ScriptTreeGraph {
private List<PTreeNode<KeyData>> sortedList; private List<PTreeNode<KeyData>> sortedList;
private List<PlaceholderNode> placeholderNodes;
private HashMap<Node, PTreeNode> foreachNodes; 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();
...@@ -46,6 +46,7 @@ public class ScriptTreeGraph { ...@@ -46,6 +46,7 @@ public class ScriptTreeGraph {
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<>(); foreachNodes = new HashMap<>();
placeholderNodes = new ArrayList<>();
front = new ArrayList<>(); front = new ArrayList<>();
sortedList = new ArrayList<>(); sortedList = new ArrayList<>();
State<KeyData> stateAfterStmt = rootPTreeNode.getStateAfterStmt(); State<KeyData> stateAfterStmt = rootPTreeNode.getStateAfterStmt();
...@@ -61,7 +62,7 @@ public class ScriptTreeGraph { ...@@ -61,7 +62,7 @@ public class ScriptTreeGraph {
computeList(); computeList();
compute(); compute();
addGoals(); addGoals();
addParentsAndChildren(); // TODO: replace addParentsAndChildren() with placeholders;
mapping.size(); mapping.size();
...@@ -80,10 +81,13 @@ public class ScriptTreeGraph { ...@@ -80,10 +81,13 @@ public class ScriptTreeGraph {
AbstractTreeNode currentTreenode; AbstractTreeNode currentTreenode;
Iterator<PTreeNode<KeyData>> iter = sortedList.listIterator(0); Iterator<PTreeNode<KeyData>> iter = sortedList.listIterator(0);
//iterate through all ptreenodes in execution order
while (iter.hasNext()) { while (iter.hasNext()) {
PTreeNode<KeyData> next = iter.next(); PTreeNode<KeyData> next = iter.next();
if (next.getStateAfterStmt() != null) { if (next.getStateAfterStmt() != null) {
Map.Entry<Node, AbstractTreeNode> entry = getMap(next); //get entry in mapping Map.Entry<Node, AbstractTreeNode> entry = getMappingEntry(next); //get entry in mapping
if (entry == null) { if (entry == null) {
continue; continue;
} }
...@@ -93,7 +97,7 @@ public class ScriptTreeGraph { ...@@ -93,7 +97,7 @@ public class ScriptTreeGraph {
//set parent //set parent
Node parent = currentNode.parent(); Node parent = currentNode.parent();
if(parent != null && currentTreenode != null) { if(parent != null && currentTreenode != null) {
addToSubChildren(parent, mapping.get(currentNode)); addToSubChildren(searchParentInMapping(parent), mapping.get(currentNode));
} }
...@@ -119,7 +123,7 @@ public class ScriptTreeGraph { ...@@ -119,7 +123,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 (atn == null) return;
if(mapping.get(node) == null || mapping.get(node) == atn) return; if(mapping.get(node) == null || 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<>();
...@@ -140,6 +144,8 @@ public class ScriptTreeGraph { ...@@ -140,6 +144,8 @@ public class ScriptTreeGraph {
private void addToSubChildren(Node node, AbstractTreeNode atn) { private void addToSubChildren(Node node, AbstractTreeNode atn) {
if(atn == null) return; if(atn == null) return;
if(mapping.get(node) == atn) return; if(mapping.get(node) == atn) return;
//no children
if (mapping.get(node).getChildren() == null) { if (mapping.get(node).getChildren() == null) {
List<AbstractTreeNode> childlist = new ArrayList<>(); List<AbstractTreeNode> childlist = new ArrayList<>();
childlist.add(atn); childlist.add(atn);
...@@ -160,12 +166,17 @@ public class ScriptTreeGraph { ...@@ -160,12 +166,17 @@ public class ScriptTreeGraph {
} }
} }
private Map.Entry<Node, AbstractTreeNode> getMap (PTreeNode < KeyData > treeNode) { /**
* Returns an entry in mapping that was created on given PTreeNode ptn
* @param ptn
* @return
*/
private Map.Entry<Node, AbstractTreeNode> getMappingEntry(PTreeNode < KeyData > ptn) {
Iterator it = mapping.entrySet().iterator(); Iterator it = mapping.entrySet().iterator();
while (it.hasNext()) { while (it.hasNext()) {
Map.Entry<Node, AbstractTreeNode> pair = (Map.Entry) it.next(); Map.Entry<Node, AbstractTreeNode> pair = (Map.Entry) it.next();
if (pair.getValue() instanceof ScriptTreeNode) { if (pair.getValue() instanceof ScriptTreeNode) {
if (((ScriptTreeNode) pair.getValue()).getScriptState() == treeNode) { if (((ScriptTreeNode) pair.getValue()).getScriptState() == ptn) {
return pair; return pair;
} }
} }
...@@ -173,25 +184,30 @@ public class ScriptTreeGraph { ...@@ -173,25 +184,30 @@ public class ScriptTreeGraph {
return null; return null;
} }
private void computeList () { /**
* Fills sortedList with PtreeNodes in execution order
*/
private void computeList () {
while (currentNode != null) { while (currentNode != null) {
sortedList.add(currentNode); sortedList.add(currentNode);
currentNode = currentNode.getNextPtreeNode(currentNode); currentNode = currentNode.getNextPtreeNode(currentNode);
} }
} }
public void compute () { /**
* Fills mapping/Creates model for graph
*/
public void compute () {
Iterator<PTreeNode<KeyData>> iter = sortedList.listIterator(0); Iterator<PTreeNode<KeyData>> iter = sortedList.listIterator(0);
ScriptVisitor visitor = new ScriptVisitor(); ScriptVisitor visitor = new ScriptVisitor();
ASTNode statement; ASTNode statement;
//Node current = rootNode.getKeyNode();
while (iter.hasNext()) { while (iter.hasNext()) {
nextPtreeNode = iter.next(); nextPtreeNode = iter.next();
statement = nextPtreeNode.getStatement(); statement = nextPtreeNode.getStatement();
//if (nextPtreeNode.getStateBeforeStmt().getSelectedGoalNode() != null) {
statement.accept(visitor); statement.accept(visitor);
//}
} }
mapping.size(); mapping.size();
...@@ -257,57 +273,61 @@ public class ScriptTreeGraph { ...@@ -257,57 +273,61 @@ public class ScriptTreeGraph {
if(call.getCommand().equals("")) return null; if(call.getCommand().equals("")) return null;
if (nextPtreeNode.toString().equals("End of Script")) return null; if (nextPtreeNode.toString().equals("End of Script")) return null;
Node n = nextPtreeNode.getStateBeforeStmt().getSelectedGoalNode().getData().getNode(); Node callnode = nextPtreeNode.getStateBeforeStmt().getSelectedGoalNode().getData().getNode();
ScriptTreeNode sn = new ScriptTreeNode(n, nextPtreeNode, nextPtreeNode.getStatement().getStartPosition().getLineNumber()); ScriptTreeNode sn = new ScriptTreeNode(callnode, nextPtreeNode, nextPtreeNode.getStatement().getStartPosition().getLineNumber());
// sn.setParent(mapping.get(current)); //check if statement was applicable
if (nextPtreeNode.getStateBeforeStmt() == nextPtreeNode.getStateAfterStmt()) { if (nextPtreeNode.getStateBeforeStmt() == nextPtreeNode.getStateAfterStmt()) {
sn.setSucc(false); sn.setSucc(false);
} }
putIntoMapping(n, sn); replacePlaceholder(callnode, sn);
//mapping.replace(n,sn); putIntoMapping(callnode, sn);
front.remove(n); front.remove(callnode);
// current = n;
List<GoalNode<KeyData>> children = nextPtreeNode.getStateAfterStmt().getGoals(); List<GoalNode<KeyData>> children = nextPtreeNode.getStateAfterStmt().getGoals();
switch (children.size()) { switch (children.size()) {
case 0: case 0:
putIntoFront(n); putIntoFront(callnode);
checkIfForeachEnd(n); checkIfForeachEnd(callnode);
break; break;
case 1: case 1:
putIntoMapping(children.get(0).getData().getNode(), null); // putIntoMapping(children.get(0).getData().getNode(), null);
putIntoFront(children.get(0).getData().getNode()); putIntoFront(children.get(0).getData().getNode());
addPlaceholder(sn, children.get(0).getData().getNode(), false);
break; break;
default: //multiple open goals/children -> branch labels default: //multiple open goals/children -> branch labels
int branchcounter = 1; int branchcounter = 1;
for (GoalNode<KeyData> gn : children) { for (GoalNode<KeyData> gn : children) {
Node node = gn.getData().getNode(); Node childnode = gn.getData().getNode();
List<BranchLabelNode> branchlabel = getBranchLabels(nextPtreeNode.getStateBeforeStmt().getSelectedGoalNode(), gn); List<BranchLabelNode> branchlabel = getBranchLabels(nextPtreeNode.getStateBeforeStmt().getSelectedGoalNode(), gn);
BranchLabelNode branchNode;
if(branchlabel.size() != 0) { if(branchlabel.size() != 0) {
//TODO: remove //TODO: remove
System.out.println("_______Branchlabels"); System.out.println("_______Branchlabels");
Lists.reverse(branchlabel).forEach(k -> System.out.println(k.getNode().serialNr() + " " + k.getLabelName())); Lists.reverse(branchlabel).forEach(k -> System.out.println(k.getNode().serialNr() + " " + k.getLabelName()));
insertBranchLabels(nextPtreeNode.getStateBeforeStmt().getSelectedGoalNode().getData().getNode(), branchlabel); insertBranchLabels(callnode, branchlabel);
addPlaceholder(branchlabel.get(0), gn.getData().getNode(), true);
/*
branchNode = new BranchLabelNode(node, branchlabel.toString());
mapping.put(node, branchNode);
*/
} else { } else {
branchNode = new BranchLabelNode(node, "Case " + branchcounter); BranchLabelNode branchNode = new BranchLabelNode(childnode, "Case " + branchcounter);
putIntoMapping(node, branchNode);
// Link Case -Branchnodes to parent
branchNode.setParent(sn);
addToChildren(callnode, branchNode);
if (mapping.get(childnode) != null) putIntoMapping(childnode, branchNode);
addPlaceholder(branchNode, childnode, true);
branchcounter++; branchcounter++;
} }
putIntoFront(node); putIntoFront(childnode);
} }
} }
...@@ -323,14 +343,18 @@ public class ScriptTreeGraph { ...@@ -323,14 +343,18 @@ public class ScriptTreeGraph {
public Void visit(GuardedCaseStatement caseStatement) { public Void visit(GuardedCaseStatement caseStatement) {
PTreeNode<KeyData> nextintoptn = nextPtreeNode.getStepInto(); PTreeNode<KeyData> nextintoptn = nextPtreeNode.getStepInto();
ScriptTreeNode match = new ScriptTreeNode(nextPtreeNode.getStateBeforeStmt().getSelectedGoalNode().getData().getNode(),nextPtreeNode, nextPtreeNode.getStatement().getStartPosition().getLineNumber()); ScriptTreeNode match = new ScriptTreeNode(nextPtreeNode.getStateBeforeStmt().getSelectedGoalNode().getData().getNode(),nextPtreeNode, nextPtreeNode.getStatement().getStartPosition().getLineNumber());
match.setMatchEx(true); match.setMatchEx(true);
// check if match was sucessful
if (nextintoptn == null) { if (nextintoptn == null) {
match.setSucc(false); match.setSucc(false);
return null;
} }
Node n = nextintoptn.getStateBeforeStmt().getSelectedGoalNode().getData().getNode(); Node n = nextPtreeNode.getStateBeforeStmt().getSelectedGoalNode().getData().getNode();
replacePlaceholder(n, match);
putIntoMapping(n, match); putIntoMapping(n, match);
addPlaceholder(match, n, false);
//front.remove(n); //front.remove(n);
return null; return null;
} }
...@@ -342,7 +366,9 @@ public class ScriptTreeGraph { ...@@ -342,7 +366,9 @@ public class ScriptTreeGraph {
match.setMatchEx(true); match.setMatchEx(true);
match.setSucc(true); match.setSucc(true);
Node n = nextintoptn.getStateBeforeStmt().getSelectedGoalNode().getData().getNode(); Node n = nextintoptn.getStateBeforeStmt().getSelectedGoalNode().getData().getNode();
replacePlaceholder(n, match);
putIntoMapping(n, match); putIntoMapping(n, match);
addPlaceholder(match, n, false);
//front.remove(n); //front.remove(n);
return null; return null;
} }
...@@ -353,7 +379,8 @@ public class ScriptTreeGraph { ...@@ -353,7 +379,8 @@ public class ScriptTreeGraph {
if (goals.size() == 0) return null; if (goals.size() == 0) return null;
goals.forEach(k -> putIntoMapping(k.getData().getNode(), new ForeachTreeNode(k.getData().getNode(), nextPtreeNode, nextPtreeNode.getStatement().getStartPosition().getLineNumber(),true))); //TODO: sometime goals on different branches
goals.forEach(k -> putIntoMapping(searchParentInMapping(k.getData().getNode()), new ForeachTreeNode(k.getData().getNode(), nextPtreeNode, nextPtreeNode.getStatement().getStartPosition().getLineNumber(),true)));
// add to foreachNodes list // add to foreachNodes list
List<GoalNode<KeyData>> goalsAfterForeach = new ArrayList<>(); List<GoalNode<KeyData>> goalsAfterForeach = new ArrayList<>();
...@@ -379,6 +406,60 @@ public class ScriptTreeGraph { ...@@ -379,6 +406,60 @@ public class ScriptTreeGraph {
} }
} }
private void addPlaceholder(AbstractTreeNode parent, Node current, boolean isSplit) {
PlaceholderNode phn = new PlaceholderNode(current);
phn.setParent(parent);
if(mapping.get(current) == null) {
putIntoMapping(current, phn);
} else {
addToSubChildren(parent.getNode(), phn);
}
placeholderNodes.add(phn);
}
private void replacePlaceholder(Node n, AbstractTreeNode atn) {
Iterator<PlaceholderNode> iterator = placeholderNodes.iterator();
while (iterator.hasNext()) {
PlaceholderNode next = iterator.next();
if (next.getNode() == n) {
//search for placeholder in mapping
AbstractTreeNode current = mapping.get(n);
if (current instanceof PlaceholderNode ) {
//TODO : atn.setParent(current.getParent()); -> leads to concurretn exception
current.getParent().setChildren(new ArrayList<>(Arrays.asList(atn)));
mapping.put(n, atn);
iterator.remove();
return;
}
while (!(current instanceof PlaceholderNode)) {
//TODO: if(current.getChildren().size() > 0) return;
if (current.getChildren() == null) return;
if (current.getChildren().get(0) instanceof PlaceholderNode) {
//TODO: insert a variable instead of using atn?
atn.setParent(current.getChildren().get(0).getParent());
current.setChildren(new ArrayList<>(Arrays.asList(atn)));
iterator.remove();
return;
}
current = current.getChildren().get(0);
}
}
};
return;
}
/** /**
* put abstracttreenode to right location in the mapping hashmap * put abstracttreenode to right location in the mapping hashmap
* @param node * @param node
...@@ -394,6 +475,14 @@ public class ScriptTreeGraph { ...@@ -394,6 +475,14 @@ public class ScriptTreeGraph {
} }
} }
private Node searchParentInMapping (Node node) {
Node parent = node;
while (mapping.get(parent) == null) {
parent = parent.parent();
}
return parent;
}
private void putIntoFront (Node node) { private void putIntoFront (Node node) {
if(!front.contains(node)) { if(!front.contains(node)) {
front.add(node); front.add(node);
...@@ -462,10 +551,11 @@ public class ScriptTreeGraph { ...@@ -462,10 +551,11 @@ public class ScriptTreeGraph {
} }
} }
//insert all missing branchlabels //TODO missing parent and child //insert all missing branchlabels
for (; 0 <= i; i--) { for (; 0 <= i; i--) {
//if topBranchNode not in mapping yet
if(i == branchlabels.size() -1) { if(i == branchlabels.size() -1) {
BranchLabelNode bn = branchlabels.get(i); BranchLabelNode bn = branchlabels.get(i);
bn.setParent(mapping.get(node)); bn.setParent(mapping.get(node));
...@@ -521,15 +611,7 @@ public class ScriptTreeGraph { ...@@ -521,15 +611,7 @@ public class ScriptTreeGraph {
} }
private void addGoals() { private void addGoals() {
front.forEach(k -> { front.forEach(k -> replacePlaceholder(k, new DummyGoalNode(k, k.isClosed())));
Node currentparent = k;
while(mapping.get(currentparent) == null) {
currentparent = currentparent.parent();
}
addToSubChildren(currentparent, new DummyGoalNode(k, k.isClosed()));
});
} }
private String getMappingString (AbstractTreeNode node){ private String getMappingString (AbstractTreeNode node){
......
...@@ -9,6 +9,22 @@ script testfull(){ ...@@ -9,6 +9,22 @@ script testfull(){
auto; auto;
} }
script full0(){
impRight;
impRight;
impLeft;
cases {
case match `!q ==> p`:
notLeft;
case match `q==>!p`:
notLeft;
}
}
script full(){ script full(){
impRight; impRight;
impRight; impRight;
......
script s() { script s0() {
symbex;
}
script s1() {
symbex; symbex;
foreach{ foreach{
auto; auto;
} }
}
script s() {
symbex;
} }
\ No newline at end of file
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