Skip to content

Commit 93f708c

Browse files
wadoonwadoon
committed
better and faster ImmutableList
1 parent 40d194c commit 93f708c

292 files changed

Lines changed: 1519 additions & 1248 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/ProofObligationVars.java‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,6 @@
1818
import org.key_project.logic.op.Function;
1919
import org.key_project.util.collection.ImmutableArray;
2020
import org.key_project.util.collection.ImmutableList;
21-
import org.key_project.util.collection.ImmutableSLList;
2221

2322
import org.jspecify.annotations.Nullable;
2423

@@ -135,7 +134,7 @@ private JTerm buildExceptionParameter(Services services) {
135134
*/
136135
private ImmutableList<JTerm> buildFormalParamVars(Services services)
137136
throws IllegalArgumentException {
138-
ImmutableList<JTerm> formalParamVars = ImmutableSLList.nil();
137+
ImmutableList<JTerm> formalParamVars = ImmutableList.nil();
139138
for (JTerm param : pre.localVars) {
140139
ProgramVariable paramVar = param.op(ProgramVariable.class);
141140
ProgramElementName pen = new ProgramElementName("_" + paramVar.name());

‎key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/macros/ExhaustiveProofMacro.java‎

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,6 @@
2323
import org.key_project.prover.sequent.PosInOccurrence;
2424
import org.key_project.prover.sequent.Sequent;
2525
import org.key_project.util.collection.ImmutableList;
26-
import org.key_project.util.collection.ImmutableSLList;
2726

2827
/**
2928
* The abstract class ExhaustiveProofMacro can be used to create compound macros which either apply
@@ -40,7 +39,7 @@ private PosInOccurrence getApplicablePosInOcc(Proof proof,
4039
ProofMacro macro) {
4140
if (posInOcc == null || posInOcc.subTerm() == null) {
4241
return null;
43-
} else if (macro.canApplyTo(proof, ImmutableSLList.<Goal>nil().prepend(goal), posInOcc)) {
42+
} else if (macro.canApplyTo(proof, ImmutableList.<Goal>nil().prepend(goal), posInOcc)) {
4443
return posInOcc;
4544
} else {
4645
final var subTerm = posInOcc.subTerm();
@@ -124,7 +123,7 @@ public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof,
124123
if (!isCached) {
125124
// node has not been checked before, so do it
126125
boolean canBeApplied =
127-
canApplyTo(proof, ImmutableSLList.<Goal>nil().prepend(goal), posInOcc);
126+
canApplyTo(proof, ImmutableList.<Goal>nil().prepend(goal), posInOcc);
128127
if (!canBeApplied) {
129128
// canApplyTo checks all open goals. thus, if it returns
130129
// false, then this macro is not applicable at all and
@@ -143,7 +142,7 @@ public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof,
143142
pml.taskStarted(new DefaultTaskStartedInfo(TaskKind.Macro, getName(), 0));
144143
synchronized (macro) {
145144
// wait for macro to terminate
146-
info = macro.applyTo(uic, proof, ImmutableSLList.<Goal>nil().prepend(goal),
145+
info = macro.applyTo(uic, proof, ImmutableList.<Goal>nil().prepend(goal),
147146
applicableAt, pml);
148147
}
149148
pml.taskFinished(info);

‎key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicBlockExecutionSnippet.java‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,6 @@
2121

2222
import org.key_project.util.collection.ImmutableArray;
2323
import org.key_project.util.collection.ImmutableList;
24-
import org.key_project.util.collection.ImmutableSLList;
2524

2625

2726
/**
@@ -33,7 +32,7 @@ class BasicBlockExecutionSnippet extends ReplaceAndRegisterMethod implements Fac
3332
@Override
3433
public JTerm produce(BasicSnippetData d, ProofObligationVars poVars)
3534
throws UnsupportedOperationException {
36-
ImmutableList<JTerm> posts = ImmutableSLList.nil();
35+
ImmutableList<JTerm> posts = ImmutableList.nil();
3736
if (poVars.post.self != null) {
3837
posts = posts.append(d.tb.equals(poVars.post.self, poVars.pre.self));
3938
}

‎key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicLoopExecutionSnippet.java‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -20,15 +20,14 @@
2020
import de.uka.ilkd.key.speclang.LoopSpecification;
2121

2222
import org.key_project.util.collection.ImmutableList;
23-
import org.key_project.util.collection.ImmutableSLList;
2423
import org.key_project.util.collection.Pair;
2524

2625
public class BasicLoopExecutionSnippet extends ReplaceAndRegisterMethod implements FactoryMethod {
2726

2827
@Override
2928
public JTerm produce(BasicSnippetData d, ProofObligationVars poVars)
3029
throws UnsupportedOperationException {
31-
ImmutableList<JTerm> posts = ImmutableSLList.nil();
30+
ImmutableList<JTerm> posts = ImmutableList.nil();
3231
if (poVars.post.self != null) {
3332
posts = posts.append(d.tb.equals(poVars.post.self, poVars.pre.self));
3433
}

‎key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicSnippetData.java‎

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,6 @@
2424
import de.uka.ilkd.key.util.MiscTools;
2525

2626
import org.key_project.util.collection.ImmutableList;
27-
import org.key_project.util.collection.ImmutableSLList;
2827
import org.key_project.util.collection.ImmutableSet;
2928

3029

@@ -150,7 +149,7 @@ public Class<?> getType() {
150149
// add guard term to information flow specs (necessary for soundness)
151150
// and add the modified specs to the table
152151
ImmutableList<InfFlowSpec> infFlowSpecs = invariant.getInfFlowSpecs(services);
153-
ImmutableList<InfFlowSpec> modifiedSpecs = ImmutableSLList.nil();
152+
ImmutableList<InfFlowSpec> modifiedSpecs = ImmutableList.nil();
154153
for (InfFlowSpec infFlowSpec : infFlowSpecs) {
155154
ImmutableList<JTerm> modifiedPreExps = infFlowSpec.preExpressions.append(guardTerm);
156155
ImmutableList<JTerm> modifiedPostExps = infFlowSpec.postExpressions.append(guardTerm);
@@ -234,7 +233,7 @@ public Class<?> getType() {
234233

235234

236235
private ImmutableList<JTerm> toTermList(ImmutableSet<LocationVariable> vars) {
237-
ImmutableList<JTerm> result = ImmutableSLList.nil();
236+
ImmutableList<JTerm> result = ImmutableList.nil();
238237
for (ProgramVariable v : vars) {
239238
result = result.append(tb.var(v));
240239
}

‎key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicSymbolicExecutionSnippet.java‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,6 @@
3333

3434
import org.key_project.util.collection.ImmutableArray;
3535
import org.key_project.util.collection.ImmutableList;
36-
import org.key_project.util.collection.ImmutableSLList;
3736

3837
/**
3938
*
@@ -47,7 +46,7 @@ public JTerm produce(BasicSnippetData d, ProofObligationVars poVars)
4746
assert poVars.exceptionParameter.op() instanceof LocationVariable
4847
: "Something is wrong with the catch variable";
4948

50-
ImmutableList<JTerm> posts = ImmutableSLList.nil();
49+
ImmutableList<JTerm> posts = ImmutableList.nil();
5150
if (poVars.post.self != null) {
5251
posts = posts.append(d.tb.equals(poVars.post.self, poVars.pre.self));
5352
}

‎key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/InfFlowContractAppInOutRelationSnippet.java‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,6 @@
1111
import de.uka.ilkd.key.util.InfFlowSpec;
1212

1313
import org.key_project.util.collection.ImmutableList;
14-
import org.key_project.util.collection.ImmutableSLList;
1514

1615
/**
1716
*
@@ -27,7 +26,7 @@ protected JTerm buildObjectSensitivePostRelation(InfFlowSpec infFlowSpec1,
2726
InfFlowSpec infFlowSpec2, BasicSnippetData d, ProofObligationVars vs1,
2827
ProofObligationVars vs2, JTerm eqAtLocsTerm) {
2928
// build equalities for newObjects terms
30-
ImmutableList<JTerm> newObjEqs = ImmutableSLList.nil();
29+
ImmutableList<JTerm> newObjEqs = ImmutableList.nil();
3130
Iterator<JTerm> newObjects1It = infFlowSpec1.newObjects.iterator();
3231
Iterator<JTerm> newObjects2It = infFlowSpec2.newObjects.iterator();
3332
for (int i = 0; i < infFlowSpec1.newObjects.size(); i++) {

‎key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/InfFlowInputOutputRelationSnippet.java‎

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,6 @@
1515
import org.key_project.logic.Term;
1616
import org.key_project.logic.op.Function;
1717
import org.key_project.util.collection.ImmutableList;
18-
import org.key_project.util.collection.ImmutableSLList;
1918

2019
/**
2120
* Generate term "self != null".
@@ -97,7 +96,7 @@ private JTerm buildInputRelation(BasicSnippetData d, ProofObligationVars vs1,
9796
private JTerm buildOutputRelation(BasicSnippetData d, ProofObligationVars vs1,
9897
ProofObligationVars vs2, InfFlowSpec infFlowSpec1, InfFlowSpec infFlowSpec2) {
9998
// build equalities for post expressions
100-
ImmutableList<JTerm> eqAtLocs = ImmutableSLList.nil();
99+
ImmutableList<JTerm> eqAtLocs = ImmutableList.nil();
101100

102101
Iterator<JTerm> postExp1It = infFlowSpec1.postExpressions.iterator();
103102
Iterator<JTerm> postExp2It = infFlowSpec2.postExpressions.iterator();
@@ -123,7 +122,7 @@ protected JTerm buildObjectSensitivePostRelation(InfFlowSpec infFlowSpec1,
123122
InfFlowSpec infFlowSpec2, BasicSnippetData d, ProofObligationVars vs1,
124123
ProofObligationVars vs2, JTerm eqAtLocsTerm) {
125124
// build equalities for newObjects terms
126-
ImmutableList<JTerm> newObjEqs = ImmutableSLList.nil();
125+
ImmutableList<JTerm> newObjEqs = ImmutableList.nil();
127126
Iterator<JTerm> newObjects1It = infFlowSpec1.newObjects.iterator();
128127
Iterator<JTerm> newObjects2It = infFlowSpec2.newObjects.iterator();
129128
for (int i = 0; i < infFlowSpec1.newObjects.size(); i++) {

‎key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/ReplaceAndRegisterMethod.java‎

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,6 @@
2222
import org.key_project.logic.op.Function;
2323
import org.key_project.logic.op.QuantifiableVariable;
2424
import org.key_project.util.collection.ImmutableList;
25-
import org.key_project.util.collection.ImmutableSLList;
2625

2726

2827
/**
@@ -78,15 +77,15 @@ final JTerm[] replace(JTerm[] terms, StateVars origVars, StateVars poVars, TermB
7877

7978
final InfFlowSpec replace(InfFlowSpec terms, StateVars origVars, StateVars poVars,
8079
TermBuilder tb) {
81-
ImmutableList<JTerm> resultPreExps = ImmutableSLList.nil();
80+
ImmutableList<JTerm> resultPreExps = ImmutableList.nil();
8281
for (JTerm t : terms.preExpressions) {
8382
resultPreExps = resultPreExps.append(replace(t, origVars, poVars, tb));
8483
}
85-
ImmutableList<JTerm> resultPostExps = ImmutableSLList.nil();
84+
ImmutableList<JTerm> resultPostExps = ImmutableList.nil();
8685
for (JTerm t : terms.postExpressions) {
8786
resultPostExps = resultPostExps.append(replace(t, origVars, poVars, tb));
8887
}
89-
ImmutableList<JTerm> resultNewObjecs = ImmutableSLList.nil();
88+
ImmutableList<JTerm> resultNewObjecs = ImmutableList.nil();
9089
for (JTerm t : terms.newObjects) {
9190
resultNewObjecs = resultNewObjecs.append(replace(t, origVars, poVars, tb));
9291
}

‎key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/TwoStateMethodPredicateSnippet.java‎

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,6 @@
2121
import org.key_project.logic.op.Function;
2222
import org.key_project.logic.sort.Sort;
2323
import org.key_project.util.collection.ImmutableList;
24-
import org.key_project.util.collection.ImmutableSLList;
2524

2625

2726
/**
@@ -118,8 +117,8 @@ abstract String generatePredicateName(IProgramMethod pm, StatementBlock block,
118117
*/
119118
private ImmutableList<JTerm> extractTermListForPredicate(IProgramMethod pm,
120119
ProofObligationVars poVars, boolean hasMby) {
121-
ImmutableList<JTerm> relevantPreVars = ImmutableSLList.nil();
122-
ImmutableList<JTerm> relevantPostVars = ImmutableSLList.nil();
120+
ImmutableList<JTerm> relevantPreVars = ImmutableList.nil();
121+
ImmutableList<JTerm> relevantPostVars = ImmutableList.nil();
123122

124123
if (!pm.isStatic()) {
125124
// self is relevant in the pre and post state for constructors

0 commit comments

Comments
 (0)