From e0b90eccbee1494440157712998d783125e2cc06 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sun, 16 Aug 2026 15:25:21 +0200 Subject: [PATCH 1/3] fix leaking --- .../util/collection/ImmutableList.java | 17 +++++++++++++++-- .../util/collection/ImmutableListArray.java | 2 +- .../util/collection/ImmutableListArrayTest.java | 16 ++++++++++++++++ 3 files changed, 32 insertions(+), 3 deletions(-) diff --git a/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java b/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java index 7cdc34a9231..a011b34e2d3 100644 --- a/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java +++ b/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java @@ -111,7 +111,7 @@ public interface ImmutableList /// @param list the list to wrap /// @return an ImmutableList containing the elements of the input list static ImmutableList fromList(List list) { - return new ImmutableListList<>(list); + return new ImmutableListList<>(new ArrayList<>(list)); } /// Creates an [ImmutableList] from an array. @@ -123,6 +123,18 @@ public interface ImmutableList /// @param array the array to wrap /// @return an ImmutableList containing the elements of the input array static ImmutableList fromArray(T[] array) { + return new ImmutableListArray<>(Arrays.copyOf(array, array.length)); + } + + /// Creates an [ImmutableList] from an array. + /// + /// This method wraps the given array in an immutable wrapper. + /// + /// @param the element type + /// @param array the array to wrap + /// @return an ImmutableList containing the elements of the input array + static ImmutableList fromItems(T... array) { + // weigl: copy needed, array dynamical created and not leaked. return new ImmutableListArray<>(array); } @@ -246,7 +258,8 @@ default ImmutableList prependReverse(Iterable collection) { /// @param array the array to prepend /// @return a new list with the array's elements at the beginning default ImmutableList prepend(T... array) { - return new ImmutableListConcat<>(ImmutableList.fromArray(array), this); + // weigl: here we can use the leaky version + return new ImmutableListConcat<>(new ImmutableListArray<>(array), this); } /// Appends a single element to this list. diff --git a/key.util/src/main/java/org/key_project/util/collection/ImmutableListArray.java b/key.util/src/main/java/org/key_project/util/collection/ImmutableListArray.java index 5c6e224138d..7561588ce50 100644 --- a/key.util/src/main/java/org/key_project/util/collection/ImmutableListArray.java +++ b/key.util/src/main/java/org/key_project/util/collection/ImmutableListArray.java @@ -22,7 +22,7 @@ final class ImmutableListArray implements ImmutableList { private final T[] data; - public ImmutableListArray(T[] data) { + ImmutableListArray(T[] data) { this.data = data; } diff --git a/key.util/src/test/java/org/key_project/util/collection/ImmutableListArrayTest.java b/key.util/src/test/java/org/key_project/util/collection/ImmutableListArrayTest.java index 15c6605efdd..3ca78013864 100644 --- a/key.util/src/test/java/org/key_project/util/collection/ImmutableListArrayTest.java +++ b/key.util/src/test/java/org/key_project/util/collection/ImmutableListArrayTest.java @@ -29,6 +29,22 @@ public static Integer[] create(int i) { return IntStream.range(1, i + 1).boxed().toArray(Integer[]::new); } + @Test + void immutability1() { + Integer[] array = { 0, 1, 4 }; + // constructor itself is dangerous + ImmutableListArray list = new ImmutableListArray<>(array); + array[2] = 2; + assertThat(list.get(2)).isEqualTo(2); + } + + @Test + void immutability2() { + Integer[] array = { 0, 1, 4 }; + ImmutableList list = ImmutableList.fromArray(array); + array[2] = 2; + assertThat(list.get(2)).isEqualTo(4); + } @Test void size() { From 71e9e6d9d5669d85966f4033c40d493faea22195 Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Sun, 16 Aug 2026 20:28:38 +0200 Subject: [PATCH 2/3] add test cases in ImmutableListArrayTest --- .../util/collection/ImmutableListArray.java | 7 +++++++ .../collection/ImmutableListArrayTest.java | 21 ++++++++++++++++++- 2 files changed, 27 insertions(+), 1 deletion(-) diff --git a/key.util/src/main/java/org/key_project/util/collection/ImmutableListArray.java b/key.util/src/main/java/org/key_project/util/collection/ImmutableListArray.java index 7561588ce50..0dd4f6c7116 100644 --- a/key.util/src/main/java/org/key_project/util/collection/ImmutableListArray.java +++ b/key.util/src/main/java/org/key_project/util/collection/ImmutableListArray.java @@ -22,6 +22,13 @@ final class ImmutableListArray implements ImmutableList { private final T[] data; + /** + * Caution: This constructor does *not* the argument array but refers to it directly. + * Do not call it but from contexts where you know that data remains unmodified. + * + * @see ImmutableList#fromArray(Object[]) + * @param data the array data + */ ImmutableListArray(T[] data) { this.data = data; } diff --git a/key.util/src/test/java/org/key_project/util/collection/ImmutableListArrayTest.java b/key.util/src/test/java/org/key_project/util/collection/ImmutableListArrayTest.java index 3ca78013864..dae423b10c5 100644 --- a/key.util/src/test/java/org/key_project/util/collection/ImmutableListArrayTest.java +++ b/key.util/src/test/java/org/key_project/util/collection/ImmutableListArrayTest.java @@ -32,8 +32,10 @@ public static Integer[] create(int i) { @Test void immutability1() { Integer[] array = { 0, 1, 4 }; - // constructor itself is dangerous + // constructor does not copy the array, so changes to the array are reflected in the list + // While this seems dangerous, the constructur is package-private and thus considered safe. ImmutableListArray list = new ImmutableListArray<>(array); + assertThat(list.get(2)).isEqualTo(4); array[2] = 2; assertThat(list.get(2)).isEqualTo(2); } @@ -46,6 +48,23 @@ void immutability2() { assertThat(list.get(2)).isEqualTo(4); } + @Test + void immutability3() { + Integer[] array = { 0, 1, 4 }; + ImmutableList list = ImmutableList.fromItems(array); + array[2] = 2; + assertThat(list.get(2)).isEqualTo(4); + } + + @Test + void immutability4() { + Integer[] array = { 0, 1, 4 }; + ImmutableList list = ImmutableList.fromItems(-1).prepend(array); + assertThat(list.get(2)).isEqualTo(4); + array[2] = 2; + assertThat(list.get(2)).isEqualTo(4); + } + @Test void size() { assertThat(list123.size()).isEqualTo(3); From e8492c7f9639019edb5218392e5189d258c5437b Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Sun, 16 Aug 2026 20:38:33 +0200 Subject: [PATCH 3/3] cloning an array ... checker-framework-friendly. --- .../java/org/key_project/util/collection/ImmutableList.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java b/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java index a011b34e2d3..4936563ae05 100644 --- a/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java +++ b/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java @@ -123,7 +123,7 @@ public interface ImmutableList /// @param array the array to wrap /// @return an ImmutableList containing the elements of the input array static ImmutableList fromArray(T[] array) { - return new ImmutableListArray<>(Arrays.copyOf(array, array.length)); + return new ImmutableListArray<>(array.clone()); } /// Creates an [ImmutableList] from an array.