Skip to content

Commit 5d76195

Browse files
FliegendeWurstFliegendeWurst
committed
Optimize offline dependency tracker and add tests
1 parent 53cdf38 commit 5d76195

2 files changed

Lines changed: 66 additions & 34 deletions

File tree

‎keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java‎

Lines changed: 15 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -44,6 +44,7 @@
4444
import org.key_project.slicing.graph.PseudoInput;
4545
import org.key_project.slicing.graph.PseudoOutput;
4646
import org.key_project.slicing.graph.TrackedFormula;
47+
import org.key_project.util.collection.IdentityHashSet;
4748
import org.key_project.util.collection.ImmutableList;
4849

4950
/**
@@ -195,12 +196,14 @@ private Set<PosInOccurrence> formulasRemovedBy(Node node) {
195196
return removed;
196197
}
197198
Sequent seqParent = parent.sequent();
198-
Sequent seqNew = node.sequent();
199-
for (int i = 1; i <= seqParent.size(); i++) {
200-
var f = seqParent.getFormulabyNr(i);
201-
if (!seqNew.contains(f)) {
202-
removed.add(PosInOccurrence.findInSequent(seqParent, i, PosInTerm.getTopLevel()));
199+
var seqNew = new IdentityHashSet<>(node.sequent().asList());
200+
int i = 1;
201+
for (final var parentFormula : seqParent) {
202+
if (!seqNew.contains(parentFormula)) {
203+
removed.add(new PosInOccurrence(parentFormula, PosInTerm.getTopLevel(),
204+
seqParent.numberInAntec(i)));
203205
}
206+
i++;
204207
}
205208
return removed;
206209
}
@@ -232,13 +235,16 @@ private List<Pair<PosInOccurrence, Integer>> outputsOfNode(Node node) {
232235
int sibling = 0;
233236
for (Node b : node.children()) {
234237
// compare sequents
235-
Sequent oldSeq = node.sequent();
238+
var oldSeq = new IdentityHashSet<>(node.sequent().asList());
236239
Sequent newSeq = b.sequent();
237-
for (int i = 1; i <= newSeq.size(); i++) {
238-
var pio = PosInOccurrence.findInSequent(newSeq, i, PosInTerm.getTopLevel());
239-
if (!oldSeq.contains(pio.sequentFormula())) {
240+
int index = 1;
241+
for (var f : newSeq) {
242+
if (!oldSeq.contains(f)) {
243+
var pio = new PosInOccurrence(f, PosInTerm.getTopLevel(),
244+
newSeq.numberInAntec(index));
240245
outputs.add(new Pair<>(pio, node.childrenCount() > 1 ? sibling : -1));
241246
}
247+
index++;
242248
}
243249
sibling++;
244250
}

‎keyext.slicing/src/test/java/org/key_project/slicing/EndToEndTests.java‎

Lines changed: 51 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -63,6 +63,7 @@ void sliceAgatha() throws Exception {
6363
assertEquals(producingNodes[i],
6464
tracker.getNodeThatProduced(node26, pio).serialNr());
6565
}
66+
proof.dispose();
6667
}
6768

6869
/**
@@ -78,15 +79,20 @@ void sliceMultipleIterations() throws Exception {
7879
Pair<Proof, File> iteration1 = sliceProofFullFilename(
7980
new File(testCaseDirectory,
8081
"../../../../../key.ui/examples/firstTouch/05-ReverseArray/reverseArray.proof"),
81-
6535, 4234, true, true);
82+
6535, 4234, true, true, true);
8283
Pair<Proof, File> iteration2 =
83-
sliceProofFullFilename(iteration1.second, 4234, 4227, true, true);
84+
sliceProofFullFilename(iteration1.second, 4234, 4227, true, true, true);
8485
Pair<Proof, File> iteration3 =
85-
sliceProofFullFilename(iteration2.second, 4227, 4218, true, true);
86+
sliceProofFullFilename(iteration2.second, 4227, 4218, true, true, true);
8687
Pair<Proof, File> iteration4 =
87-
sliceProofFullFilename(iteration3.second, 4218, 4207, true, true);
88+
sliceProofFullFilename(iteration3.second, 4218, 4207, true, true, true);
8889
Pair<Proof, File> iteration5 =
89-
sliceProofFullFilename(iteration4.second, 4207, 4195, true, true);
90+
sliceProofFullFilename(iteration4.second, 4207, 4195, true, true, true);
91+
iteration5.first.dispose();
92+
iteration4.first.dispose();
93+
iteration3.first.dispose();
94+
iteration2.first.dispose();
95+
iteration1.first.dispose();
9096
Files.delete(iteration5.second.toPath());
9197
Files.delete(iteration4.second.toPath());
9298
Files.delete(iteration3.second.toPath());
@@ -103,7 +109,10 @@ void sliceMultipleIterations() throws Exception {
103109
void sliceJavaProof() throws Exception {
104110
sliceProof(
105111
"../../../../../key.ui/examples/heap/verifyThis15_2_ParallelGcd/parallelGcd.proof",
106-
3238, 1336, true, false);
112+
3238, 1336, true, false).dispose();
113+
sliceProofOffline(
114+
"../../../../../key.ui/examples/heap/verifyThis15_2_ParallelGcd/parallelGcd.proof",
115+
3238, 1336, true, false).dispose();
107116
}
108117

109118
/**
@@ -113,7 +122,7 @@ void sliceJavaProof() throws Exception {
113122
*/
114123
@Test
115124
void sliceCutExample() throws Exception {
116-
sliceProof("/cutExample.proof", 10, 7, true, false);
125+
sliceProof("/cutExample.proof", 10, 7, true, false).dispose();
117126
}
118127

119128
/**
@@ -123,7 +132,8 @@ void sliceCutExample() throws Exception {
123132
*/
124133
@Test
125134
void sliceAgathaWithOpenGoal() throws Exception {
126-
sliceProof("/agathaOpenGoal.proof", 145, 124, true, false);
135+
sliceProof("/agathaOpenGoal.proof", 145, 124, true, false).dispose();
136+
sliceProofOffline("/agathaOpenGoal.proof", 145, 124, true, false).dispose();
127137
}
128138

129139
/**
@@ -133,8 +143,8 @@ void sliceAgathaWithOpenGoal() throws Exception {
133143
*/
134144
@Test
135145
void sliceWithOpenGoal() throws Exception {
136-
sliceProof("/openGoal1.proof", 10, 7, true, false);
137-
sliceProof("/openGoal2.proof", 10, 7, true, false);
146+
sliceProof("/openGoal1.proof", 10, 7, true, false).dispose();
147+
sliceProof("/openGoal2.proof", 10, 7, true, false).dispose();
138148
}
139149

140150
/**
@@ -150,13 +160,13 @@ void sliceIfThenElseSplit() throws Exception {
150160

151161
// duplicate analysis: merge duplicated steps (one at a time)
152162
Pair<Proof, File> iteration1 = sliceProofFullFilename(
153-
new File(testCaseDirectory, "/ifThenElseSplit.proof"), 12, 11, false, true);
163+
new File(testCaseDirectory, "/ifThenElseSplit.proof"), 12, 11, false, true, true);
154164
Pair<Proof, File> iteration2 =
155-
sliceProofFullFilename(iteration1.second, 11, 10, false, true);
165+
sliceProofFullFilename(iteration1.second, 11, 10, false, true, true);
156166
Pair<Proof, File> iteration3 =
157-
sliceProofFullFilename(iteration2.second, 10, 9, false, true);
167+
sliceProofFullFilename(iteration2.second, 10, 9, false, true, true);
158168
Pair<Proof, File> iteration4 =
159-
sliceProofFullFilename(iteration3.second, 9, 8, false, true);
169+
sliceProofFullFilename(iteration3.second, 9, 8, false, true, true);
160170
assertEquals("w TRUE",
161171
iteration4.first.findAny(x -> x.serialNr() == 6).getNodeInfo().getBranchLabel());
162172
assertEquals("w FALSE",
@@ -200,13 +210,13 @@ void deduplicateChecksMergabilityCorrectly() throws Exception {
200210
@Test
201211
void sliceDuplicatesAway() throws Exception {
202212
Pair<Proof, File> iteration1 = sliceProofFullFilename(
203-
new File(testCaseDirectory, "/exampleDuplicate.proof"), 10, 9, false, true);
213+
new File(testCaseDirectory, "/exampleDuplicate.proof"), 10, 9, false, true, true);
204214
Pair<Proof, File> iteration2 =
205-
sliceProofFullFilename(iteration1.second, 9, 8, false, true);
215+
sliceProofFullFilename(iteration1.second, 9, 8, false, true, true);
206216
Pair<Proof, File> iteration3 =
207-
sliceProofFullFilename(iteration2.second, 8, 7, false, true);
217+
sliceProofFullFilename(iteration2.second, 8, 7, false, true, true);
208218
Pair<Proof, File> iteration4 =
209-
sliceProofFullFilename(iteration3.second, 7, 7, false, true);
219+
sliceProofFullFilename(iteration3.second, 7, 7, false, true, true);
210220
Files.delete(iteration4.second.toPath());
211221
Files.delete(iteration3.second.toPath());
212222
Files.delete(iteration2.second.toPath());
@@ -221,13 +231,13 @@ void sliceDuplicatesAway() throws Exception {
221231
@Test
222232
void sliceDuplicatesAwayOpenGoals() throws Exception {
223233
Pair<Proof, File> iteration1 = sliceProofFullFilename(
224-
new File(testCaseDirectory, "/exampleDuplicateOpen.proof"), 10, 9, false, true);
234+
new File(testCaseDirectory, "/exampleDuplicateOpen.proof"), 10, 9, false, true, true);
225235
Pair<Proof, File> iteration2 =
226-
sliceProofFullFilename(iteration1.second, 9, 8, false, true);
236+
sliceProofFullFilename(iteration1.second, 9, 8, false, true, true);
227237
Pair<Proof, File> iteration3 =
228-
sliceProofFullFilename(iteration2.second, 8, 7, false, true);
238+
sliceProofFullFilename(iteration2.second, 8, 7, false, true, true);
229239
Pair<Proof, File> iteration4 =
230-
sliceProofFullFilename(iteration3.second, 7, 7, false, true);
240+
sliceProofFullFilename(iteration3.second, 7, 7, false, true, true);
231241
Files.delete(iteration4.second.toPath());
232242
Files.delete(iteration3.second.toPath());
233243
Files.delete(iteration2.second.toPath());
@@ -239,14 +249,24 @@ private Proof sliceProof(String filename, int expectedTotal,
239249
throws Exception {
240250
Pair<Proof, File> it =
241251
sliceProofFullFilename(new File(testCaseDirectory, filename), expectedTotal,
242-
expectedInSlice, doDependencyAnalysis, doDeduplicateRuleApps);
252+
expectedInSlice, doDependencyAnalysis, doDeduplicateRuleApps, true);
253+
Files.delete(it.second.toPath());
254+
return it.first;
255+
}
256+
257+
private Proof sliceProofOffline(String filename, int expectedTotal,
258+
int expectedInSlice, boolean doDependencyAnalysis, boolean doDeduplicateRuleApps)
259+
throws Exception {
260+
Pair<Proof, File> it =
261+
sliceProofFullFilename(new File(testCaseDirectory, filename), expectedTotal,
262+
expectedInSlice, doDependencyAnalysis, doDeduplicateRuleApps, false);
243263
Files.delete(it.second.toPath());
244264
return it.first;
245265
}
246266

247267
private Pair<Proof, File> sliceProofFullFilename(File proofFile, int expectedTotal,
248268
int expectedInSlice, boolean doDependencyAnalysis,
249-
boolean doDeduplicateRuleApps) throws Exception {
269+
boolean doDeduplicateRuleApps, boolean trackOnline) throws Exception {
250270
boolean oldValue = GeneralSettings.noPruningClosed;
251271
GeneralSettings.noPruningClosed = false;
252272
// load proof
@@ -256,13 +276,19 @@ private Pair<Proof, File> sliceProofFullFilename(File proofFile, int expectedTot
256276
KeYEnvironment<?> environment =
257277
KeYEnvironment.load(JavaProfile.getDefaultInstance(), proofFile, null, null, null, null,
258278
null, proof -> {
259-
tracker.set(new DependencyTracker(proof));
279+
if (trackOnline) {
280+
tracker.set(new DependencyTracker(proof));
281+
}
260282
}, true);
261283
try {
262284
// get loaded proof
263285
Proof proof = environment.getLoadedProof();
264286
Assertions.assertNotNull(proof);
265287
boolean originalProofClosed = proof.closed();
288+
// track proof (if not done already)
289+
if (!trackOnline) {
290+
tracker.set(new DependencyTracker(proof));
291+
}
266292
// analyze proof
267293
AnalysisResults results =
268294
tracker.get().analyze(doDependencyAnalysis, doDeduplicateRuleApps);

0 commit comments

Comments
 (0)