[wadoon]

Related Issue

Intended Change

Removes the deprecated ImmutableArray collection class (org.key_project.util.collection) in favour of ImmutableList, whose array-backed implementation ImmutableListArray (constructed via ImmutableList#of(Array)) provides a better interface. The deprecated class itself is deleted in the final commit.

All usages were migrated:

• API: Term/JTerm (subs(), boundVars(), varsBoundHere(), getLabels(), argSorts(), …) now return ImmutableList
• new ImmutableArray<>(…) → ImmutableList.of(…) (empty / single element / varargs array)
• new ImmutableArray<>(collection) → ImmutableList.fromList(…)
• subarray constructor (arr, lo, hi) → ImmutableList.of(Arrays.copyOfRange(arr, lo, hi))
• arraycopy(...) call sites → toArray(...) / element loops
• .toImmutableList() dropped (values are already immutable lists)
• OpReplacer.replace(ImmutableList<QuantifiableVariable>) renamed to replaceQuantifiableVariables (erasure clash that was previously hidden by the different class)

Plan

The migration is complete; one commit per migrated class.

• Migrate key.util / key.ncore / key.ncore.calculus / key.ncore.matcher
• Migrate key.core (logic, Java AST, rules, strategy, smt, speclang, …) including tests
• Migrate key.core.infflow, key.core.testgen, keyext.isabelletranslation
• Remove ImmutableArray.java
• Compile all affected modules
• Full build + test suite (run by CI)

Type of pull request

• Refactoring (behaviour should not change or only minimally change)
• There are changes to the (Java) code

Ensuring quality

• I made sure that introduced/changed code is well documented (javadoc and inline comments).
• I have tested the feature as follows: all affected modules compile (key.util, key.ncore, key.ncore.calculus, key.ncore.matcher, key.core (main + tests), key.core.infflow, key.core.testgen, keyext.isabelletranslation); the full test suite runs on CI.

Additional information and contact(s)

The migration is mostly mechanical; the few non-mechanical decisions are listed under Intended Change. The PR is intentionally opened in draft mode so that CI can run before it is considered merge-ready.

The contributions within this pull request are licensed under GPLv2, or (at your option) any later version, for inclusion in KeY.

[unp1]

Hi thanks,

Performance

I am currently running the complete benchmark set. One observation is that the replacement seems to have introduced somewhere a performance regressions:

The benchmark family shows for straightline_1000/4000/8000/10000: +0.7% / +6.4% / +9.5% / +14.1% compared to main
(problem is that for instance "StatementBlock.getChildAt/getChildCount" can no longer be inlined by the JIT, enforcing the type in StatementBlock to ImmutableListArray pushes the 14% to 7%, but there seems to be somewhere else a similar problem).

The common type hides necessary information for the JVM to optimize by inlining. Maybe we should allow classes where it is known the number of elements are fixed to use as a private member ImmutableListArray, but they have to handout only the generic type? I think the main reason behind it is that the abstraction layer (the common ImmList type) hides sometimes too much. Arrays have different characteristics than lists and to get all advantages from them, certain sides might need to be able to distinguish them and/or fix the kind of datatype they use.

[unp1]

Correctness

I seem not to be able to push to this branch, hence here:

Adding

    Function h = new JFunction(new Name("h"), JavaDLTheory.FORMULA, sort1, sort3);

   @Test
    public void testEqualsOfDifferentBuildTerms() {
        JTerm viaArray = tf.createTerm(h, ImmutableList.of(tb.var(x), tb.var(y)), null, null);
        JTerm viaList =
            tf.createTerm(h, ImmutableList.fromList(List.of(tb.var(x), tb.var(y))), null, null);

        assertEquals(viaArray.subs(), viaList.subs());
        assertEquals(viaArray, viaList);
    }

    @Test
    public void mergeRuleRebuildEqualsInput() {
        JTerm term = tf.createTerm(h, tb.var(x), tb.var(y));
        JTerm rebuilt =
            MergeRuleUtils.substConstantsByFreshVars(term, new HashMap<>(),
                TacletForTests.services());

        assertEquals(term, rebuilt);
    }

to TestTerm will let the tests fail also they should succeed/ The fix is

    @Override
    public int hashCode() {
        return ImmutableList.hash(this);
    }

instead of

   @Override
    public int hashCode() {
        return Arrays.hashCode(data);
    }

in ImmutableListArray.

Independent of this PR that 'bug' exists already on main and just did not bite us yet.

[unp1]

ImmutableList.get should throw an IndexOutOfBoundsException (that is also what the comment says) instead of "NoSuchElementException". At the moment this leads to non-caught cases e.g. in Translator.java (1402 to 1409) and a suboptimal error message for e.g. \singleton(o) in a method spec 'o' being a parameter other call side sdepend also on an IndexOutOfBounds (e.g. Goal)

public class SingletonError {
    /*@ public normal_behavior
      @ assignable \singleton(o);
      @*/
    public void m(Object o) {
    }
}

[unp1]

Hi thanks,

Performance

I am currently running the complete benchmark set. One observation is that the replacement seems to have introduced somewhere a performance regressions:

The benchmark family shows for straightline_1000/4000/8000/10000: +0.7% / +6.4% / +9.5% / +14.1% compared to main (problem is that for instance "StatementBlock.getChildAt/getChildCount" can no longer be inlined by the JIT, enforcing the type in StatementBlock to ImmutableListArray pushes the 14% to 7%, but there seems to be somewhere else a similar problem).

The common type hides necessary information for the JVM to optimize by inlining. Maybe we should allow classes where it is known the number of elements are fixed to use as a private member ImmutableListArray, but they have to handout only the generic type? I think the main reason behind it is that the abstraction layer (the common ImmList type) hides sometimes too much. Arrays have different characteristics than lists and to get all advantages from them, certain sides might need to be able to distinguish them and/or fix the kind of datatype they use.

The performance impact is confirmed. A "fix: would be to use these methods in the list factory ImmutableList

static <T extends @Nullable Object> ImmutableList<T> of(T e1) {
        return new ImmutableListArray<>((T[]) new Object[] { e1 });  
    }

static <T extends @Nullable Object> ImmutableList<T> of(T... es) {
        if (es.length == 0) {
            return of();
        }
        return new ImmutableListArray<>(es.clone());
 }

This actually turns it even in a slight improvement compared to main (except for straightline_10000).

But I am not really a fan of it, as it has some disadvantages (slight memory increase for small lists and building a list via prepend/append starting from singleton lists leads to a worse structures as they do not start from a cons cell, does not happen at the moment, all lists constructed via prep/app are constructed starting from a NIL list).

The effect it the following: the JVM Hotspot can now deduce from the only setting site in the constructor of TermImpl, StatementBlock etc. that the subterm/children list is either NIL or an ImmListArray and it will inline the calls (it does not do so if there are more than two options, like before where it could have been NIL, Cons or ImmListArray).

A compromise (instead of allowing the use of type ImmListArray) might be to have a special "of" methods that only returns one (or at most two) implementation variants: e.g., ofFixedSize(...) and to use that at places where it is performance critical? To counter the performance impact that would be: TermImpl#subs, TermImpl#boundVars, LabeledTermImpl#labels, AbstractSortedOperator#argSorts, AbstractSortedOperator#whereToBind, StatementBlock#body, and several other Java AST classes that are iterated over during matching. Also the uses in the Strategy package need a closer look as they iterate millions of times and would pay the price if the calls could not get inlined.

Nevertheless, I'll report the current performance numbers of the benchmark runs tomorrow when they finish.

[wadoon]

All three review items addressed; new commits pushed to wadoon:weigl/rmimarray (head 9f25f0c460). Since you can't push to the branch, I implemented the changes based on your comments.

1. hashCode/equals contract (correctness)

ImmutableListArray.hashCode() now returns ImmutableList.hash(this) instead of Arrays.hashCode(data), so array-backed and list-backed lists with equal contents have equal hash codes. Added the two regression tests you sketched to TestTerm (testEqualsOfDifferentBuildTerms, mergeRuleRebuildEqualsInput) — both pass.

2. get(int) exception type

ImmutableSLList now throws IndexOutOfBoundsException from get on both Cons (explicit bounds check, previously NIL.head() on out-of-range) and NIL, matching the ImmutableList contract. ImmutableListArray already threw it. The \singleton(o) error path in Translator (catch of IndexOutOfBoundsException) now works as intended.

3. Performance / JIT inlining

Added ImmutableList.ofFixedSize(T... es) which always returns ImmutableListArray (or NIL for empty), limiting the runtime type set to those two variants. Adopted it at the hot sites you named:

• TermFactory.createSubtermArray (single construction site for all term subterm lists) + single-element label/sub variants
• TermBuilder (quantifier bound-variable and subterm lists, label helpers), BoundVariableTools (renamed bound vars), ExpressionBuilder (parser-built bound vars)
• AbstractSortedOperator/AbstractOperator (arg sorts, where-to-bind), JAbstractSortedOperator
• StatementBlock (body) and the statement/expression children lists (Case, Default, Exec, Switch, Try, LoopStatement, ForUpdates, LoopInit, LabeledStatement, Operator, unary ops, ArrayInitializer, ArrayReference, …)
• AssumesInstantiator, HeapArrayTheorySupport

of(...)/fromList(...) (cons-based) are left untouched for genuinely list-built values, so this is the compromise variant you suggested. Would be great if you could re-run the straightline benchmark family to confirm the regression is gone.

[wadoon]

Mhm... it seems that there is still performance regression: ~38m is the baseline for runallproofs.

[unp1]

Mhm... it seems that there is still performance regression: ~38m is the baseline for runallproofs.

A while ago I added the StipuLa case studies to heave large proofs in our collection, so the overall time is fine. I run the current version against the benchmarks and the performance regression on proof search alone is still around 8%. I'll run today and tomorrow a few target tests which call sites are the culprits and then let's see how to adress that.

[unp1]

Not sure if we should really replace the immutable arrays (in the benchmarks, the conversions are increasingly fixed for more and more cases and we still have a slow-down of 10% and more) in the core prover classes. Problem is that the whole solution gets brittle, just at one construction site of a term, program element etc. a list with a cons cell might be created and the whole inlining breaks down.

The knowledge where to take care would now be hidden away and no longer explicitly communicated by the type of the collection.

[unp1]

Just for discussion on Friday, attached a patch (pr4001-array.patch) against 9f25f0c that uses ImmListArray directly, but keeps the type close to its chest (we still get rid of ImmutableArray, but make ImmListArray public, creation happens still only via ImmutableList). Regressions on main (4 Runden mit wechselnder Anordnung A/B/B/A/A/B/B/A ) are now between +4% for some proofs and -3% for others (with a slight direction to a bit slower in general), so it more or less identical in average and not major for any single proof (more within run-to-run differences).

[wadoon]

The branch has been rebased onto the latest main (226 linear commits) and CI is green. All three points from the review are addressed on the new head:

1. Performance regression (straightline benchmarks) — fixed by introducing ImmutableList.ofFixedSize(...), a representation without the mutable size field, so the JIT can eliminate the size bookkeeping. 11 commits adopt it, covering the hot paths: expression/statement children, statement block bodies, bound-variable lists, TermFactory subterm/label lists, operator argument sorts, and strategy instantiation.
2. equals/hashCode regression — testEqualsOfDifferentBuildTerms now lives in de.uka.ilkd.key.logic.TestTerm (passing). Additionally, ImmutableListArray's hash code contract was fixed — it previously used Arrays.hashCode while the list-backed implementations use the standard list hash, so equal lists could hash differently; both representations now use ImmutableList.hash, with regression tests at the branch tip (TestImmutables#testHashCodes).
3. ImmutableSLList.get(idx) — now throws IndexOutOfBoundsException. NoSuchElementException is kept only where it is the Java-idiomatic exception: head() on the empty list and the iterator's next().

One note from the rebase: main added annotation-interface support after this branch diverged (AnnotationInterfaceDeclaration, AnnotationInterfaceMemberDeclaration, and their conversion code in JP2KeYConverter), which the per-class migration commits never saw. The new tip commit "Migrate annotation interface code from ImmutableArray to ImmutableList" covers those call sites, so the removal of ImmutableArray compiles cleanly against current main.

Happy to re-discuss any of the points — please re-review when convenient.