Commit 38d2c3e6 authored by Lulu Luong's avatar Lulu Luong
Browse files

foreach-end working for not closed goals

branchlabels working in the Maxtriplets Example
defaultcases added to visitor
parent 65615828
Pipeline #26698 passed with stages
in 4 minutes and 25 seconds
package edu.kit.iti.formal.psdbg.examples.java.maxtriplet;
import edu.kit.iti.formal.psdbg.examples.JavaExample;
public class MaxTripletExample extends JavaExample {
public MaxTripletExample() {
setName("MaxTriplet");
setJavaFile(this.getClass().getResource("MaxTriplet.java"));
defaultInit(getClass());
}
}
\ No newline at end of file
...@@ -1322,6 +1322,7 @@ public class DebuggerMain implements Initializable { ...@@ -1322,6 +1322,7 @@ public class DebuggerMain implements Initializable {
ScriptTreeGraph stg = new ScriptTreeGraph(); ScriptTreeGraph stg = new ScriptTreeGraph();
PTreeNode startnode = (model.getDebuggerFramework() != null)?model.getDebuggerFramework().getPtreeManager().getStartNode():null; PTreeNode startnode = (model.getDebuggerFramework() != null)?model.getDebuggerFramework().getPtreeManager().getStartNode():null;
if(startnode == null) return;
stg.createGraph(startnode, FACADE.getProof().root()); stg.createGraph(startnode, FACADE.getProof().root());
TreeItem<TreeNode> item = (stg.toView()); TreeItem<TreeNode> item = (stg.toView());
......
...@@ -41,7 +41,7 @@ public class ForeachTreeNode extends AbstractTreeNode { ...@@ -41,7 +41,7 @@ public class ForeachTreeNode extends AbstractTreeNode {
@Override @Override
public TreeNode toTreeNode() { public TreeNode toTreeNode() {
String label= (foreachstart)? "foreach in line " + linenr + " START": "foreach in line " + linenr + "END"; String label= (foreachstart)? "foreach in line " + linenr + " START": "foreach in line " + linenr + " END";
return new TreeNode(label, getNode()); return new TreeNode(label, getNode());
} }
......
...@@ -41,7 +41,9 @@ public class ScriptTreeNode extends AbstractTreeNode { ...@@ -41,7 +41,9 @@ public class ScriptTreeNode extends AbstractTreeNode {
public TreeNode toTreeNode() { public TreeNode toTreeNode() {
String label; String label;
if (isMatchEx()) { if (isMatchEx()) {
String matchexpression = ((TermLiteral) ((MatchExpression) ((GuardedCaseStatement) scriptState.getStatement()).getGuard()).getPattern()).getContent();
String matchexpression = (scriptState.getStatement() instanceof GuardedCaseStatement)?((TermLiteral) ((MatchExpression) ((GuardedCaseStatement) scriptState.getStatement()).getGuard()).getPattern()).getContent()
: "default";
label = "match ("+ matchexpression +") in line " + linenr; label = "match ("+ matchexpression +") in line " + linenr;
} else { } else {
label = ((CallStatement)scriptState.getStatement()).getCommand() + " (line " + linenr + ")"; label = ((CallStatement)scriptState.getStatement()).getCommand() + " (line " + linenr + ")";
......
package edu.kit.iti.formal.psdbg.gui.controls; package edu.kit.iti.formal.psdbg.gui.controls;
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;
...@@ -10,10 +11,7 @@ import edu.kit.iti.formal.psdbg.interpreter.data.KeyData; ...@@ -10,10 +11,7 @@ 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;
import edu.kit.iti.formal.psdbg.interpreter.dbg.PTreeNode; import edu.kit.iti.formal.psdbg.interpreter.dbg.PTreeNode;
import edu.kit.iti.formal.psdbg.parser.DefaultASTVisitor; import edu.kit.iti.formal.psdbg.parser.DefaultASTVisitor;
import edu.kit.iti.formal.psdbg.parser.ast.ASTNode; import edu.kit.iti.formal.psdbg.parser.ast.*;
import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
import edu.kit.iti.formal.psdbg.parser.ast.ForeachStatement;
import edu.kit.iti.formal.psdbg.parser.ast.GuardedCaseStatement;
import javafx.scene.control.TreeItem; import javafx.scene.control.TreeItem;
import lombok.Getter; import lombok.Getter;
import sun.reflect.generics.tree.Tree; import sun.reflect.generics.tree.Tree;
...@@ -62,8 +60,9 @@ public class ScriptTreeGraph { ...@@ -62,8 +60,9 @@ public class ScriptTreeGraph {
this.rootNode = rootNode; this.rootNode = rootNode;
computeList(); computeList();
compute(); compute();
addParentsAndChildren();
addGoals(); addGoals();
addParentsAndChildren();
mapping.size(); mapping.size();
//TODO: remove following //TODO: remove following
...@@ -121,7 +120,7 @@ public class ScriptTreeGraph { ...@@ -121,7 +120,7 @@ public class ScriptTreeGraph {
*/ */
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) == 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<>();
childlist.add(atn); childlist.add(atn);
...@@ -262,11 +261,13 @@ public class ScriptTreeGraph { ...@@ -262,11 +261,13 @@ public class ScriptTreeGraph {
if (nextPtreeNode.getStateBeforeStmt() == nextPtreeNode.getStateAfterStmt()) { if (nextPtreeNode.getStateBeforeStmt() == nextPtreeNode.getStateAfterStmt()) {
sn.setSucc(false); sn.setSucc(false);
} }
putIntoMapping(n, sn); putIntoMapping(n, sn);
//mapping.replace(n,sn); //mapping.replace(n,sn);
front.remove(n); front.remove(n);
// current = n; // current = n;
List<GoalNode<KeyData>> children = nextPtreeNode.getStateAfterStmt().getGoals(); List<GoalNode<KeyData>> children = nextPtreeNode.getStateAfterStmt().getGoals();
switch (children.size()) { switch (children.size()) {
...@@ -287,15 +288,20 @@ public class ScriptTreeGraph { ...@@ -287,15 +288,20 @@ public class ScriptTreeGraph {
BranchLabelNode branchNode; BranchLabelNode branchNode;
if(branchlabel.size() != 0) { if(branchlabel.size() != 0) {
insertBranchLabels(node, branchlabel);
//TODO: remove
System.out.println("_______Branchlabels");
Lists.reverse(branchlabel).forEach(k -> System.out.println(k.getNode().serialNr() + " " + k.getLabelName()));
insertBranchLabels(nextPtreeNode.getStateBeforeStmt().getSelectedGoalNode().getData().getNode(), 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); putIntoMapping(node, branchNode);
branchcounter++; branchcounter++;
} }
...@@ -327,6 +333,18 @@ public class ScriptTreeGraph { ...@@ -327,6 +333,18 @@ public class ScriptTreeGraph {
return null; return null;
} }
@Override
public Void visit(DefaultCaseStatement caseStatement) {
PTreeNode<KeyData> nextintoptn = nextPtreeNode.getStepInto();
ScriptTreeNode match = new ScriptTreeNode(nextPtreeNode.getStepInto().getStateBeforeStmt().getSelectedGoalNode().getData().getNode(),nextPtreeNode, nextPtreeNode.getStatement().getStartPosition().getLineNumber());
match.setMatchEx(true);
match.setSucc(true);
Node n = nextintoptn.getStateBeforeStmt().getSelectedGoalNode().getData().getNode();
putIntoMapping(n, match);
//front.remove(n);
return null;
}
@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();
...@@ -335,11 +353,11 @@ public class ScriptTreeGraph { ...@@ -335,11 +353,11 @@ public class ScriptTreeGraph {
goals.forEach(k -> putIntoMapping(k.getData().getNode(), new ForeachTreeNode(k.getData().getNode(), nextPtreeNode, nextPtreeNode.getStatement().getStartPosition().getLineNumber(),true))); goals.forEach(k -> putIntoMapping(k.getData().getNode(), new ForeachTreeNode(k.getData().getNode(), nextPtreeNode, nextPtreeNode.getStatement().getStartPosition().getLineNumber(),true)));
// add to foreachNodes lsit // add to foreachNodes lsit
if (nextPtreeNode.getStateAfterStmt() != null) { List<GoalNode<KeyData>> aftergoals = (nextPtreeNode.getStateAfterStmt() != null)? nextPtreeNode.getStateAfterStmt().getGoals()
List<GoalNode<KeyData>> aftergoals = nextPtreeNode.getStateAfterStmt().getGoals(); : (nextPtreeNode.getStepOver() != null && nextPtreeNode.getStepOver().getStateBeforeStmt() != null) ? nextPtreeNode.getStepOver().getStateBeforeStmt().getGoals()
aftergoals.forEach(k -> foreachNodes.put(k.getData().getNode(), nextPtreeNode)); : new ArrayList<>();
} aftergoals.forEach(k -> foreachNodes.put(k.getData().getNode(), nextPtreeNode));
//
return null; return null;
} }
...@@ -369,7 +387,15 @@ public class ScriptTreeGraph { ...@@ -369,7 +387,15 @@ public class ScriptTreeGraph {
private void checkIfForeachEnd(Node n) { private void checkIfForeachEnd(Node n) {
if(foreachNodes.containsKey(n)) { if(foreachNodes.containsKey(n)) {
PTreeNode ptn = foreachNodes.get(n); PTreeNode ptn = foreachNodes.get(n);
putIntoMapping(n, new ForeachTreeNode(n, ptn, ptn.getStatement().getStartPosition().getLineNumber(), false)); ForeachTreeNode ftn = new ForeachTreeNode(n, ptn, ptn.getStatement().getStartPosition().getLineNumber(), false);
addToSubChildren(nextPtreeNode.getStateBeforeStmt().getSelectedGoalNode().getData().getNode(), ftn);
if(mapping.get(n) == null) {
putIntoMapping(n,ftn);
}
foreachNodes.remove(n);
} }
} }
...@@ -378,16 +404,20 @@ public class ScriptTreeGraph { ...@@ -378,16 +404,20 @@ public class ScriptTreeGraph {
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; try {
while(childnode.parent() != parentnode) { while (childnode.parent() != parentnode) {
if(childnode.getNodeInfo().getBranchLabel() != null if (childnode.getNodeInfo().getBranchLabel() != null
&& isBranchLabel(childnode.getNodeInfo().getBranchLabel()) && isBranchLabel(childnode.getNodeInfo().getBranchLabel())&& !sameBranchlabelBefore(branchlabels, childnode))
&& !sameBranchlabelBefore(branchlabels, childnode)) branchlabels.add( new BranchLabelNode(childnode, childnode.getNodeInfo().getBranchLabel())); branchlabels.add(new BranchLabelNode(childnode, childnode.getNodeInfo().getBranchLabel()));
childnode = childnode.parent(); childnode = childnode.parent();
}
} catch (NullPointerException e) {
e.printStackTrace();
} }
return branchlabels; return branchlabels;
} }
private boolean sameBranchlabelBefore(List<BranchLabelNode> branchlabels, Node node) { private boolean sameBranchlabelBefore(List<BranchLabelNode> branchlabels, Node node) {
if(branchlabels.size() == 0) return false; if(branchlabels.size() == 0) return false;
return branchlabels.get(branchlabels.size()-1).getLabelName().equals(node.getNodeInfo().getBranchLabel()); return branchlabels.get(branchlabels.size()-1).getLabelName().equals(node.getNodeInfo().getBranchLabel());
...@@ -401,6 +431,51 @@ public class ScriptTreeGraph { ...@@ -401,6 +431,51 @@ public class ScriptTreeGraph {
private void insertBranchLabels(Node node, List<BranchLabelNode> branchlabels) { private void insertBranchLabels(Node node, List<BranchLabelNode> branchlabels) {
if(branchlabels == null) return; if(branchlabels == null) return;
Node topBranchNode = branchlabels.get(branchlabels.size()-1).getNode(); //start from last to first
int i = branchlabels.size()- 1;
List<AbstractTreeNode> currentChildren;
//check which Branchlabels are already in mapping -> afterwards forall x of [0,i]; branchlabels[x] not in mapping yet
if(mapping.containsKey(topBranchNode) && ((BranchLabelNode)mapping.get(topBranchNode)).getLabelName() == branchlabels.get(i).getLabelName()) {
currentChildren = mapping.get(topBranchNode).getChildren();
i--;
while (0 <= i && currentChildren != null && currentChildren.contains(branchlabels.get(i))) {
currentChildren = currentChildren.get(currentChildren.indexOf(branchlabels.get(i))).getChildren();
i--;
}
}
//insert all missing branchlabels //TODO missing parent and child
for (; 0 <= i; i--) {
if(i == branchlabels.size() -1) {
BranchLabelNode bn = branchlabels.get(i);
bn.setParent(mapping.get(node));
addToChildren(node, branchlabels.get(i));
putIntoMapping(branchlabels.get(i).getNode(), bn);
} else { //some branchlabels in mapping
addToChildren(branchlabels.get(i+1).getNode(), 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);
addToChildren(parent.getNode(), child);
/*
if (i == branchlabels.size() - 2) {
addToChildren(node, child);
} else {
addToChildren(parent.getNode(), child);
}
*/
}
/* old implementation
mapping.put(node, branchlabels.get(branchlabels.size()-1)); mapping.put(node, branchlabels.get(branchlabels.size()-1));
...@@ -424,12 +499,22 @@ public class ScriptTreeGraph { ...@@ -424,12 +499,22 @@ public class ScriptTreeGraph {
} }
} }
} }
*/
}
} }
private void addGoals() { private void addGoals() {
front.forEach(k -> putIntoMapping(k, new DummyGoalNode(k, k.isClosed()))); front.forEach(k -> {
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){
String s = ""; String s = "";
...@@ -448,4 +533,6 @@ public class ScriptTreeGraph { ...@@ -448,4 +533,6 @@ public class ScriptTreeGraph {
} }
return s; return s;
} }
} }
edu.kit.iti.formal.psdbg.examples.contraposition.ContrapositionExample edu.kit.iti.formal.psdbg.examples.contraposition.ContrapositionExample
edu.kit.iti.formal.psdbg.examples.fol.FirstOrderLogicExample edu.kit.iti.formal.psdbg.examples.fol.FirstOrderLogicExample
edu.kit.iti.formal.psdbg.examples.java.simple.JavaSimpleExample edu.kit.iti.formal.psdbg.examples.java.simple.JavaSimpleExample
edu.kit.iti.formal.psdbg.examples.java.maxtriplet.MaxTripletExample
#edu.kit.iti.formal.psdbg.examples.java.transitive.PaperExample #edu.kit.iti.formal.psdbg.examples.java.transitive.PaperExample
#edu.kit.iti.formal.psdbg.examples.java.dpqs.DualPivotExample #edu.kit.iti.formal.psdbg.examples.java.dpqs.DualPivotExample
edu.kit.iti.formal.psdbg.examples.java.quicksort.QuickSort edu.kit.iti.formal.psdbg.examples.java.quicksort.QuickSort
......
public class MaxTriplet {
/*@ public normal_behavior
@ requires true;
@ ensures \result >= a && \result >= b && \result >= c;
@*/
public int getMax(int a, int b, int c) {
int max;
if(a >= b) {
max = a;
} else {
max = b;
}
if(max <= c) {
max = c;
}
return max;
}
}
\ No newline at end of file
\profile "Java Profile";
\settings {
"#Proof-Settings-Config-File
#Tue Aug 28 16:59:30 CEST 2018
[StrategyProperty]OSS_OPTIONS_KEY=OSS_ON
[StrategyProperty]VBT_PHASE=VBT_SYM_EX
[SMTSettings]useUninterpretedMultiplication=true
[SMTSettings]SelectedTaclets=
[StrategyProperty]METHOD_OPTIONS_KEY=METHOD_CONTRACT
[StrategyProperty]USER_TACLETS_OPTIONS_KEY3=USER_TACLETS_OFF
[StrategyProperty]SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY=SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER
[StrategyProperty]LOOP_OPTIONS_KEY=LOOP_INVARIANT
[StrategyProperty]USER_TACLETS_OPTIONS_KEY2=USER_TACLETS_OFF
[StrategyProperty]USER_TACLETS_OPTIONS_KEY1=USER_TACLETS_OFF
[StrategyProperty]QUANTIFIERS_OPTIONS_KEY=QUANTIFIERS_NON_SPLITTING_WITH_PROGS
[StrategyProperty]NON_LIN_ARITH_OPTIONS_KEY=NON_LIN_ARITH_NONE
[SMTSettings]instantiateHierarchyAssumptions=true
[StrategyProperty]AUTO_INDUCTION_OPTIONS_KEY=AUTO_INDUCTION_OFF
[StrategyProperty]DEP_OPTIONS_KEY=DEP_ON
[StrategyProperty]BLOCK_OPTIONS_KEY=BLOCK_CONTRACT_INTERNAL
[StrategyProperty]CLASS_AXIOM_OPTIONS_KEY=CLASS_AXIOM_FREE
[StrategyProperty]SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY=SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF
[StrategyProperty]QUERY_NEW_OPTIONS_KEY=QUERY_OFF
[Strategy]Timeout=-1
[Strategy]MaximumNumberOfAutomaticApplications=10000
[SMTSettings]integersMaximum=2147483645
[Choice]DefaultChoices=assertions-assertions\\:safe , initialisation-initialisation\\:disableStaticInitialisation , intRules-intRules\\:arithmeticSemanticsIgnoringOF , programRules-programRules\\:Java , runtimeExceptions-runtimeExceptions\\:allow , JavaCard-JavaCard\\:off , Strings-Strings\\:on , modelFields-modelFields\\:treatAsAxiom , bigint-bigint\\:on , sequences-sequences\\:on , moreSeqRules-moreSeqRules\\:on , reach-reach\\:on , integerSimplificationRules-integerSimplificationRules\\:full , permissions-permissions\\:off , wdOperator-wdOperator\\:L , wdChecks-wdChecks\\:off , mergeGenerateIsWeakeningGoal-mergeGenerateIsWeakeningGoal\\:off
[SMTSettings]useConstantsForBigOrSmallIntegers=true
[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT
[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_ON
[StrategyProperty]INF_FLOW_CHECK_PROPERTY=INF_FLOW_CHECK_FALSE
[SMTSettings]maxGenericSorts=2
[SMTSettings]integersMinimum=-2147483645
[SMTSettings]invariantForall=false
[SMTSettings]UseBuiltUniqueness=false
[SMTSettings]explicitTypeHierarchy=false
[Strategy]ActiveStrategy=JavaCardDLStrategy
[StrategyProperty]SPLITTING_OPTIONS_KEY=SPLITTING_DELAYED
[StrategyProperty]MPS_OPTIONS_KEY=MPS_MERGE
"
}
\javaSource "";
\proofObligation "#Proof Obligation Settings
#Tue Aug 28 16:59:30 CEST 2018
name=MaxTriplet[MaxTriplet\\:\\:getMax(int,int,int)].JML normal_behavior operation contract.0
contract=MaxTriplet[MaxTriplet\\:\\:getMax(int,int,int)].JML normal_behavior operation contract.0
class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO
";
\proof {
(keyLog "0" (keyUser "Lulu" ) (keyVersion "f70bcf96664be17b2edcd824cec1bc6bfb2f9528"))
(autoModeTime "0")
(branch "dummy ID"
(opengoal " ")
)
}
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