Skip to content

Commit 9947adb

Browse files
committed
performance optimisation - keep track of where the selected tree came from to avoid the array search, this is importaint as code abstraction can introduce a large number of new child TraceTress in one go
1 parent 271b562 commit 9947adb

File tree

1 file changed

+30
-26
lines changed
  • svm-partition-trace-symb/src/main/java/com/lexicalscope/svm/search2

1 file changed

+30
-26
lines changed

svm-partition-trace-symb/src/main/java/com/lexicalscope/svm/search2/TreeSearch.java

Lines changed: 30 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -28,13 +28,15 @@ public class TreeSearch implements StateSearch<JState>, TraceTreeObserver {
2828
private final TraceTree tt;
2929
private final TraceTreeSearchState searchState;
3030

31-
private JState pending;
31+
private JState pendingJState;
3232

3333
private boolean pstateGiven;
3434
private boolean qstateGiven;
3535

3636
private TraceTree selectedTree;
3737

38+
private int selectedTreeIndex;
39+
3840

3941
public TreeSearch(
4042
final GuidedSearchObserver observer,
@@ -50,7 +52,7 @@ public TreeSearch(
5052
}
5153

5254
@Override public JState pendingState() {
53-
if(pending == null) {
55+
if(pendingJState == null) {
5456
if(searchState.currentSide().equals(PSIDE) && anyQStatesAvailable()) {
5557
pickAQstate();
5658
} else if (searchState.currentSide().equals(QSIDE) && anyPStatesAvailable()) {
@@ -61,76 +63,76 @@ public TreeSearch(
6163
pickAQstate();
6264
}
6365

64-
if(pending != null) {
65-
observer.picked(pending, searchState.currentSide());
66+
if(pendingJState != null) {
67+
observer.picked(pendingJState, searchState.currentSide());
6668
}
6769
}
68-
return pending;
70+
return pendingJState;
6971
}
7072

7173
private void pickAQstate() {
72-
selectedTree = node(qstatesAvailable());
73-
pending = selectedTree.qStates().pickState();
74+
selectAnotherTree(qstatesAvailable());
75+
pendingJState = selectedTree.qStates().pickState();
7476

7577
searchState.search(QSIDE, selectedTree);
7678
}
7779

7880
private void pickAPstate() {
79-
selectedTree = node(pstatesAvailable());
80-
pending = selectedTree.pStates().pickState();
81+
selectAnotherTree(pstatesAvailable());
82+
pendingJState = selectedTree.pStates().pickState();
8183

8284
searchState.search(PSIDE, selectedTree);
8385
}
8486

85-
public TraceTree node(final List<TraceTree> statesAvailable) {
86-
final int node1 = randomiser.random(statesAvailable.size());
87-
return statesAvailable.get(node1);
87+
public void selectAnotherTree(final List<TraceTree> withStatesAvailable) {
88+
selectedTreeIndex = randomiser.random(withStatesAvailable.size());
89+
selectedTree = withStatesAvailable.get(selectedTreeIndex);
8890
}
8991

9092
@Override public void reachedLeaf() {
91-
pending.complete();
92-
observer.leaf(pending);
93-
results.add(pending);
93+
pendingJState.complete();
94+
observer.leaf(pendingJState);
95+
results.add(pendingJState);
9496

95-
final Trace goal = metaExtractor.goal(pending);
97+
final Trace goal = metaExtractor.goal(pendingJState);
9698
pushGoalToCurrentNode(terminateTrace(goal));
9799

98-
pending = null;
100+
pendingJState = null;
99101
}
100102

101103
@Override public void fork(final JState parent, final JState[] states) {
102104
assert states.length == 2;
103105
observer.forkAt(parent);
104106
pushStateToSearchLater(searchState.currentNode(), states[0]);
105107
pushStateToSearchLater(searchState.currentNode(), states[1]);
106-
pending = null;
108+
pendingJState = null;
107109
}
108110

109111
@Override public void forkDisjoined(final JState parent, final JState[] states) {
110112
fork(parent, states);
111113
}
112114

113115
@Override public void goal() {
114-
observer.goal(pending);
116+
observer.goal(pendingJState);
115117

116-
final Trace goal = metaExtractor.goal(pending);
118+
final Trace goal = metaExtractor.goal(pendingJState);
117119
final TraceTree child = pushGoalToCurrentNode(goal);
118120

119-
pushStateToSearchLater(child, pending);
121+
pushStateToSearchLater(child, pendingJState);
120122

121-
pending = null;
123+
pendingJState = null;
122124
}
123125

124126
private TraceTree pushGoalToCurrentNode(final Trace goal) {
125127
final TraceTree child = searchState.currentNode().child(goal);
126128

127129
switch (searchState.currentSide()) {
128130
case PSIDE:
129-
child.disjoinP(metaExtractor.pc(pending));
131+
child.disjoinP(metaExtractor.pc(pendingJState));
130132
break;
131133

132134
case QSIDE:
133-
child.disjoinQ(metaExtractor.pc(pending));
135+
child.disjoinQ(metaExtractor.pc(pendingJState));
134136
break;
135137
}
136138
new TraceTreeChildMismatchDetector(feasibilityChecker).mismatch(searchState.currentNode(), new MismatchReport(){
@@ -186,7 +188,8 @@ private void pushStateToSearchLater(final TraceTree node, final JState state) {
186188

187189
@Override public void pstateUnavailable(final TraceTree traceTree) {
188190
assert selectedTree == traceTree;
189-
removeWithSwap(pstatesAvailable.indexOf(traceTree), pstatesAvailable);
191+
final TraceTree removed = removeWithSwap(selectedTreeIndex, pstatesAvailable);
192+
assert removed == traceTree;
190193
}
191194

192195
@Override public void qstateAvailable(final TraceTree traceTree) {
@@ -195,7 +198,8 @@ private void pushStateToSearchLater(final TraceTree node, final JState state) {
195198

196199
@Override public void qstateUnavailable(final TraceTree traceTree) {
197200
assert selectedTree == traceTree;
198-
removeWithSwap(qstatesAvailable.indexOf(traceTree), qstatesAvailable);
201+
final TraceTree removed = removeWithSwap(selectedTreeIndex, qstatesAvailable);
202+
assert removed == traceTree;
199203
}
200204

201205
public List<TraceTree> pstatesAvailable() {

0 commit comments

Comments
 (0)