Skip to content

Commit 7ceda5b

Browse files
wadoonwadoon
authored
Linearized symbolic execution in proof tree (#3237)
2 parents a53e7f9 + 28025d8 commit 7ceda5b

File tree

13 files changed

+269
-122
lines changed

13 files changed

+269
-122
lines changed

‎key.core/src/main/antlr4/KeYParser.g4‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -754,7 +754,7 @@ option_expr
754754

755755
goalspec
756756
:
757-
(name=string_value COLON)?
757+
(name=string_value (LBRACKET tag=simple_ident RBRACKET)? COLON)?
758758
( rwObj=replacewith
759759
addSeq=add?
760760
addRList=addrules?

‎key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java‎

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -166,7 +166,7 @@ public Taclet visitTaclet(KeYParser.TacletContext ctx) {
166166
Sequent addSeq = JavaDLSequentKit.createAnteSequent(ImmutableSLList.singleton(sform));
167167
ImmutableList<Taclet> noTaclets = ImmutableSLList.nil();
168168
DefaultImmutableSet<SchemaVariable> noSV = DefaultImmutableSet.nil();
169-
addGoalTemplate(null, null, addSeq, noTaclets, noSV, null, ctx);
169+
addGoalTemplate(null, null, addSeq, noTaclets, noSV, null, null, ctx);
170170
b.setName(new Name(name));
171171
b.setChoices(choices);
172172
b.setAnnotations(tacletAnnotations);
@@ -746,7 +746,11 @@ public Object visitGoalspec(KeYParser.GoalspecContext ctx) {
746746
if (ctx.addprogvar() != null) {
747747
addpv = accept(ctx.addprogvar());
748748
}
749-
addGoalTemplate(name, rwObj, addSeq, addRList, addpv, soc, ctx);
749+
String tag = null;
750+
if (ctx.tag != null) {
751+
tag = ctx.tag.getText();
752+
}
753+
addGoalTemplate(name, rwObj, addSeq, addRList, addpv, soc, tag, ctx);
750754
return null;
751755
}
752756

@@ -811,7 +815,7 @@ public ImmutableList<Taclet> visitTacletlist(KeYParser.TacletlistContext ctx) {
811815

812816
private void addGoalTemplate(String id, Object rwObj, Sequent addSeq,
813817
ImmutableList<Taclet> addRList, ImmutableSet<SchemaVariable> pvs,
814-
@Nullable ChoiceExpr soc, ParserRuleContext ctx) {
818+
@Nullable ChoiceExpr soc, String tag, ParserRuleContext ctx) {
815819
TacletBuilder<?> b = peekTBuilder();
816820
TacletGoalTemplate gt = null;
817821
if (rwObj == null) {
@@ -843,6 +847,7 @@ private void addGoalTemplate(String id, Object rwObj, Sequent addSeq,
843847
"Could not find a suitable goal template builder for: " + b.getClass());
844848
}
845849
gt.setName(id);
850+
gt.setTag(tag);
846851
b.addTacletGoalTemplate(gt);
847852
if (soc != null) {
848853
b.addGoal2ChoicesMapping(gt, soc);

‎key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGoalTemplate.java‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -90,5 +90,4 @@ public ImmutableSet<QuantifiableVariable> getBoundVariables() {
9090

9191
return result.union(bvv.getBoundVariables());
9292
}
93-
9493
}

‎key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key‎

Lines changed: 43 additions & 43 deletions
Large diffs are not rendered by default.

‎key.core/src/main/resources/de/uka/ilkd/key/proof/rules/propRule.key‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -300,7 +300,7 @@
300300
};
301301

302302
cut {
303-
"CUT: #cutFormula TRUE":
303+
"CUT: #cutFormula TRUE" [main]:
304304
\add(cutFormula ==>);
305305
"CUT: #cutFormula FALSE":
306306
\add( ==> cutFormula)
@@ -310,7 +310,7 @@
310310
cut_direct {
311311
\find(cutFormula)
312312
\sameUpdateLevel
313-
"CUT: #cutFormula TRUE":
313+
"CUT: #cutFormula TRUE" [main]:
314314
\replacewith(true) \add(cutFormula ==>);
315315
"CUT: #cutFormula FALSE":
316316
\replacewith(false) \add( ==> cutFormula)

‎key.ncore.calculus/src/main/java/org/key_project/prover/rules/tacletbuilder/TacletGoalTemplate.java‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -28,6 +28,7 @@ public abstract class TacletGoalTemplate {
2828
protected final ImmutableSet<SchemaVariable> addedProgVars;
2929

3030
private @Nullable String name;
31+
private @Nullable String tag = null;
3132

3233
/// Creates a new goal template for a taclet
3334
///
@@ -88,10 +89,17 @@ public void setName(@Nullable String name) {
8889
this.name = name;
8990
}
9091

92+
public void setTag(String tag) {
93+
this.tag = tag;
94+
}
95+
9196
public @Nullable String name() {
9297
return name;
9398
}
9499

100+
public @Nullable String tag() {
101+
return tag;
102+
}
95103

96104
@Override
97105
public boolean equals(@Nullable Object o) {

‎key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIAbstractTreeNode.java‎

Lines changed: 36 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,10 @@
55

66

77
import java.lang.ref.WeakReference;
8+
import java.util.ArrayList;
89
import java.util.Enumeration;
910
import java.util.LinkedList;
11+
import java.util.List;
1012
import javax.swing.tree.TreeNode;
1113

1214
import de.uka.ilkd.key.proof.Node;
@@ -21,6 +23,8 @@ public abstract class GUIAbstractTreeNode implements TreeNode {
2123
// and ProofTreeView.delegateView.lastPathComponent
2224
private final WeakReference<Node> noderef;
2325

26+
protected TreeNode parent;
27+
2428
protected GUIProofTreeModel getProofTreeModel() {
2529
return tree;
2630
}
@@ -34,7 +38,18 @@ protected GUIAbstractTreeNode(GUIProofTreeModel tree, Node node) {
3438

3539
public abstract int getChildCount();
3640

37-
public abstract TreeNode getParent();
41+
@Override
42+
public TreeNode getParent() {
43+
if (parent == null && this != tree.getRoot()
44+
&& !(getNode() != null && ProofTreeViewFilter.hiddenByGlobalFilters(getNode()))) {
45+
Node n = getNode();
46+
if (n != null && n.proof().root() == n) {
47+
return null; // TODO: why can there be another instance of the root node?
48+
}
49+
throw new IllegalStateException("abstract tree node without parent: " + this);
50+
}
51+
return parent;
52+
}
3853

3954
public abstract boolean isLeaf();
4055

@@ -70,8 +85,8 @@ public TreeNode[] getPath() {
7085
return path.toArray(new TreeNode[0]);
7186
}
7287

73-
protected TreeNode findBranch(Node p_node) {
74-
TreeNode res = getProofTreeModel().findBranch(p_node);
88+
protected GUIAbstractTreeNode findBranch(Node p_node) {
89+
GUIAbstractTreeNode res = getProofTreeModel().findBranch(p_node);
7590
if (res != null) {
7691
return res;
7792
}
@@ -119,25 +134,34 @@ public Node getNode() {
119134
return noderef.get();
120135
}
121136

122-
protected Node findChild(Node n) {
137+
/**
138+
* Get the children of the specified node whilst respecting the configured
139+
* global view filters.
140+
*
141+
* @param n the nodes
142+
* @return children nodes
143+
*/
144+
protected List<Node> findChild(Node n) {
123145
if (n.childrenCount() == 1) {
124-
return n.child(0);
146+
return List.of(n.child(0));
125147
}
126148

127-
if (!getProofTreeModel().globalFilterActive()) {
128-
return null;
149+
if (!getProofTreeModel().globalFilterActive()
150+
&& !getProofTreeModel().linearizedModeActive()) {
151+
return List.of();
129152
}
130153

131-
Node nextN = null;
154+
List<Node> nextN = new ArrayList<>();
132155
for (int i = 0; i != n.childrenCount(); ++i) {
133156
if (!ProofTreeViewFilter.hiddenByGlobalFilters(n.child(i))) {
134-
if (nextN != null) {
135-
return null;
136-
}
137-
nextN = n.child(i);
157+
nextN.add(n.child(i));
138158
}
139159
}
140160

141161
return nextN;
142162
}
163+
164+
protected void setParent(TreeNode parent) {
165+
this.parent = parent;
166+
}
143167
}

‎key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIBranchNode.java‎

Lines changed: 73 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -4,14 +4,20 @@
44
package de.uka.ilkd.key.gui.prooftree;
55

66
import java.util.ArrayList;
7+
import java.util.List;
8+
import java.util.Objects;
79
import javax.swing.tree.TreeNode;
810

911
import de.uka.ilkd.key.proof.Node;
12+
import de.uka.ilkd.key.rule.Taclet;
1013

1114
import org.jspecify.annotations.NonNull;
1215

1316
/**
14-
* this class implements a TreeModel that can be displayed using the JTree class framework
17+
* Branch node indicating the start of a new proof branch.
18+
*
19+
* @author early KeY team
20+
* @see ProofTreeView
1521
*/
1622
class GUIBranchNode extends GUIAbstractTreeNode {
1723

@@ -25,46 +31,82 @@ public GUIBranchNode(GUIProofTreeModel tree, Node subTree, Object label) {
2531
this.label = label;
2632
}
2733

34+
private void createChildrenCache() {
35+
childrenCache = new ArrayList<>();
36+
}
37+
2838
public TreeNode getChildAt(int childIndex) {
29-
ensureChildrenCacheExists();
39+
fillChildrenCache(false);
3040
return childrenCache.get(childIndex);
31-
/*
32-
* int count = 0; Node n = subTree; while ( childIndex != count && n.childrenCount() == 1 )
33-
* { count++; n = n.child(0); } if ( childIndex == count ) { return getProofTreeModel
34-
* ().getProofTreeNode(n); } else { return findBranch ( n.child(childIndex-count-1) ); }
35-
*/
3641
}
3742

38-
private void ensureChildrenCacheExists() {
43+
/**
44+
* Fill the {@link #childrenCache}.
45+
*
46+
* @param dryRun if true, only count the number of children that would be added
47+
* @return number of children
48+
*/
49+
private int fillChildrenCache(boolean dryRun) {
3950
if (childrenCache == null) {
40-
childrenCache = new ArrayList<>();
41-
} else {
42-
return;
51+
createChildrenCache();
52+
}
53+
54+
if (!childrenCache.isEmpty()) {
55+
return childrenCache.size();
4356
}
4457

4558
int count = 0;
4659
Node n = getNode();
4760

4861
if (n == null) {
49-
return;
62+
return 0;
5063
}
5164

5265
while (true) {
53-
childrenCache.add(count, getProofTreeModel().getProofTreeNode(n));
5466
count++;
55-
final Node nextN = findChild(n);
56-
if (nextN == null) {
67+
if (!dryRun) {
68+
var newNode = getProofTreeModel().getProofTreeNode(n);
69+
newNode.setParent(this);
70+
childrenCache.add(newNode);
71+
}
72+
List<Node> nextN = findChild(n);
73+
if (nextN.isEmpty()) {
5774
break;
5875
}
59-
n = nextN;
76+
if (nextN.size() > 1) {
77+
// linearized mode: the main branch will be continued without a new BranchNode
78+
if (getProofTreeModel().linearizedModeActive()
79+
&& (n.getAppliedRuleApp().rule() instanceof Taclet taclet && Objects
80+
.equals(taclet.goalTemplates().last().tag(), "main"))) {
81+
n = nextN.get(0);
82+
nextN.remove(0);
83+
for (var node : nextN) {
84+
count++;
85+
if (!dryRun) {
86+
var branchNode = findBranch(node);
87+
branchNode.setParent(this);
88+
childrenCache.add(branchNode);
89+
}
90+
}
91+
continue;
92+
} else {
93+
break;
94+
}
95+
}
96+
n = nextN.get(0);
6097
}
6198

6299
for (int i = 0; i != n.childrenCount(); ++i) {
63100
if (!ProofTreeViewFilter.hiddenByGlobalFilters(n.child(i))) {
64-
childrenCache.add(count, findBranch(n.child(i)));
65101
count++;
102+
if (!dryRun) {
103+
var branchNode = findBranch(n.child(i));
104+
branchNode.setParent(this);
105+
childrenCache.add(branchNode);
106+
}
66107
}
67108
}
109+
return count;
68110
}
69111

70112
@Override
@@ -77,41 +119,30 @@ public void flushCache() {
77119
return toString();
78120
}
79121

122+
@Override
80123
public int getChildCount() {
81-
if (childrenCache == null) {
82-
ensureChildrenCacheExists();
83-
}
84-
return childrenCache.size();
124+
return fillChildrenCache(true);
85125
}
86126

87-
public TreeNode getParent() {
88-
Node self = getNode();
89-
if (self == null) {
90-
return null;
91-
}
92-
Node n = self.parent();
93-
if (n == null) {
94-
return null;
95-
} else {
96-
while (n.parent() != null && findChild(n.parent()) != null) {
97-
n = n.parent();
98-
}
99-
return findBranch(n);
100-
}
101-
}
102-
103-
// signalled by GUIProofTreeModel when the user has altered the value
127+
/**
128+
* Set the label of this branch node.
129+
* Signalled by GUIProofTreeModel when the user has altered the value.
130+
*
131+
* @param s new label
132+
*/
104133
public void setLabel(String s) {
105134
Node n = getNode();
106135
if (n != null) {
107136
n.getNodeInfo().setBranchLabel(s);
108137
}
109138
}
110139

140+
@Override
111141
public boolean isLeaf() {
112142
return false;
113143
}
114144

145+
@Override
115146
public String toString() {
116147
Node n = getNode();
117148
String res;
@@ -126,6 +157,10 @@ public String toString() {
126157
return res;
127158
}
128159

160+
/**
161+
* @return whether this branch is closed
162+
* @see Node#isClosed()
163+
*/
129164
public boolean isClosed() {
130165
Node node = getNode();
131166
return node != null && node.isClosed();

0 commit comments

Comments
 (0)