From 8f253d8030065b8a2540b179edff5e05f8eb7cbe Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Tue, 2 Sep 2025 22:53:50 -0700 Subject: [PATCH 1/6] Fix typo --- .../framework/test/junit/ValueUncheckedDefaultsTest.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/framework/src/test/java/org/checkerframework/framework/test/junit/ValueUncheckedDefaultsTest.java b/framework/src/test/java/org/checkerframework/framework/test/junit/ValueUncheckedDefaultsTest.java index d33bdf51dd8e..89e9e93e4a68 100644 --- a/framework/src/test/java/org/checkerframework/framework/test/junit/ValueUncheckedDefaultsTest.java +++ b/framework/src/test/java/org/checkerframework/framework/test/junit/ValueUncheckedDefaultsTest.java @@ -20,7 +20,7 @@ public ValueUncheckedDefaultsTest(List testFiles) { "value", // Ignore the test suite's usage of qualifiers in illegal locations. "-AignoreTargetLocations", - "-AuseConservativeDefaultsForUncheckedCode=btyecode", + "-AuseConservativeDefaultsForUncheckedCode=bytecode", "-A" + ValueChecker.REPORT_EVAL_WARNS); } From 9b04b24952d6837c80b4befa508d9bd65a1b63fe Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Mon, 25 May 2026 11:49:50 -0400 Subject: [PATCH 2/6] Fix value unchecked bytecode defaults test --- .../junit/ValueUncheckedDefaultsTest.java | 1 + .../tests/value/unchecked-bytecode.astub | 235 ++++++++++++++++++ 2 files changed, 236 insertions(+) create mode 100644 framework/tests/value/unchecked-bytecode.astub diff --git a/framework/src/test/java/org/checkerframework/framework/test/junit/ValueUncheckedDefaultsTest.java b/framework/src/test/java/org/checkerframework/framework/test/junit/ValueUncheckedDefaultsTest.java index 89e9e93e4a68..f9d836539d24 100644 --- a/framework/src/test/java/org/checkerframework/framework/test/junit/ValueUncheckedDefaultsTest.java +++ b/framework/src/test/java/org/checkerframework/framework/test/junit/ValueUncheckedDefaultsTest.java @@ -20,6 +20,7 @@ public ValueUncheckedDefaultsTest(List testFiles) { "value", // Ignore the test suite's usage of qualifiers in illegal locations. "-AignoreTargetLocations", + "-Astubs=tests/value/unchecked-bytecode.astub", "-AuseConservativeDefaultsForUncheckedCode=bytecode", "-A" + ValueChecker.REPORT_EVAL_WARNS); } diff --git a/framework/tests/value/unchecked-bytecode.astub b/framework/tests/value/unchecked-bytecode.astub new file mode 100644 index 000000000000..8397967d27eb --- /dev/null +++ b/framework/tests/value/unchecked-bytecode.astub @@ -0,0 +1,235 @@ +import org.checkerframework.common.value.qual.ArrayLen; +import org.checkerframework.common.value.qual.ArrayLenRange; +import org.checkerframework.common.value.qual.StringVal; +import org.checkerframework.common.value.qual.UnknownVal; + +package java.lang; + +class Math { + static int min(@UnknownVal int a, @UnknownVal int b); + + static long min(@UnknownVal long a, @UnknownVal long b); + + static float min(@UnknownVal float a, @UnknownVal float b); + + static double min(@UnknownVal double a, @UnknownVal double b); + + static int max(@UnknownVal int a, @UnknownVal int b); + + static long max(@UnknownVal long a, @UnknownVal long b); + + static float max(@UnknownVal float a, @UnknownVal float b); + + static double max(@UnknownVal double a, @UnknownVal double b); +} + +class String { + static String format(@UnknownVal String format, @UnknownVal Object... args); + + String(@UnknownVal byte[] bytes); + + String(@UnknownVal char[] value); + + String(@UnknownVal char[] value, @UnknownVal int offset, @UnknownVal int count); + + boolean equalsIgnoreCase(@UnknownVal String anotherString); + + int indexOf(@UnknownVal int ch); + + int indexOf(@UnknownVal int ch, @UnknownVal int fromIndex); + + int indexOf(@UnknownVal String str, @UnknownVal int fromIndex); + + String replace(@UnknownVal char oldChar, @UnknownVal char newChar); + + String substring(@UnknownVal int beginIndex); + + String substring(@UnknownVal int beginIndex, @UnknownVal int endIndex); + + String @ArrayLenRange(from = 1) [] split(@UnknownVal String regex); + + boolean startsWith(@UnknownVal String prefix); + + boolean endsWith(@UnknownVal String suffix); + + static @StringVal({"true", "false"}) String valueOf(@UnknownVal boolean b); + + static @ArrayLen(1) String valueOf(@UnknownVal char c); + + static @ArrayLenRange(from = 1, to = 11) String valueOf(@UnknownVal int i); + + static @ArrayLenRange(from = 1, to = 20) String valueOf(@UnknownVal long l); +} + +class StringBuilder { + StringBuilder append(@UnknownVal char c); + + StringBuilder append(@UnknownVal String str); +} + +package java.io; + +import org.checkerframework.common.value.qual.UnknownVal; + +class PrintStream { + void print(@UnknownVal String s); + + void print(@UnknownVal char c); + + void println(@UnknownVal Object x); + + void println(@UnknownVal String x); + + void println(@UnknownVal int x); +} + +class IOException { + IOException(@UnknownVal String message); +} + +package java.lang; + +import org.checkerframework.common.value.qual.UnknownVal; + +class ClassLoader { + Class loadClass(@UnknownVal String name); +} + +class Class { + Class asSubclass(@UnknownVal Class clazz); +} + +class Object { + boolean equals(@UnknownVal Object obj); +} + +class IllegalArgumentException { + IllegalArgumentException(@UnknownVal String s); +} + +class UnsupportedOperationException { + UnsupportedOperationException(@UnknownVal String message); +} + +class RuntimeException { + RuntimeException(@UnknownVal String message, @UnknownVal Throwable cause); +} + +class AssertionError { + AssertionError(@UnknownVal Object detailMessage); +} + +class Error { + Error(@UnknownVal String message); +} + +package org.checkerframework.framework.testchecker.lib; + +import org.checkerframework.common.value.qual.StaticallyExecutable; +import org.checkerframework.common.value.qual.UnknownVal; + +class VarargsMethods { + @StaticallyExecutable + static int test0(@UnknownVal Object... objects); + + @StaticallyExecutable + static int test1(@UnknownVal String s, @UnknownVal Object... objects); + + @StaticallyExecutable + static int test2(@UnknownVal String s, @UnknownVal String s2, @UnknownVal Object... objects); +} + +package java.util; + +import org.checkerframework.common.value.qual.UnknownVal; + +class Arrays { + static List asList(@UnknownVal T... a); +} + +class ArrayList { + ArrayList(@UnknownVal Collection c); +} + +class Collections { + static > T min(@UnknownVal Collection coll); + + static T min( + @UnknownVal Collection coll, @UnknownVal Comparator comp); + + static Collection checkedCollection( + @UnknownVal Collection c, @UnknownVal Class type); + + static > void sort(@UnknownVal List list); +} + +class HashSet { + HashSet(@UnknownVal Collection c); + + boolean contains(@UnknownVal Object o); +} + +interface Set { + boolean retainAll(@UnknownVal Collection c); +} + +package java.nio.file; + +import org.checkerframework.common.value.qual.UnknownVal; + +class Paths { + static Path get(@UnknownVal String first, @UnknownVal String... more); +} + +class Files { + static java.io.BufferedWriter newBufferedWriter( + @UnknownVal Path path, @UnknownVal java.nio.charset.Charset cs, @UnknownVal OpenOption... options); + + static boolean isRegularFile(@UnknownVal Path path, @UnknownVal LinkOption... options); +} + +package java.lang.invoke; + +import org.checkerframework.common.value.qual.UnknownVal; + +class MethodHandle { + Object invoke(@UnknownVal Object... args); +} + +package java.util.stream; + +import org.checkerframework.common.value.qual.UnknownVal; + +interface Stream { + static Stream of(@UnknownVal T... values); + + R collect(@UnknownVal Collector collector); + + Stream skip(@UnknownVal long n); + + Stream sorted(@UnknownVal java.util.Comparator comparator); + + java.util.Optional max(@UnknownVal java.util.Comparator comparator); +} + +interface IntStream { + static IntStream range(@UnknownVal int startInclusive, @UnknownVal int endExclusive); +} + +class Collectors { + static Collector joining(@UnknownVal CharSequence delimiter); + + static Collector> toMap( + @UnknownVal java.util.function.Function keyMapper, + @UnknownVal java.util.function.Function valueMapper); + + static > Collector toMap( + @UnknownVal java.util.function.Function keyMapper, + @UnknownVal java.util.function.Function valueMapper, + @UnknownVal java.util.function.BinaryOperator mergeFunction, + @UnknownVal java.util.function.Supplier mapSupplier); + + static Collector collectingAndThen( + @UnknownVal Collector downstream, + @UnknownVal java.util.function.Function finisher); +} From d7772679b38316965dc51dc2e206f98c97ffb935 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Mon, 25 May 2026 12:04:01 -0400 Subject: [PATCH 3/6] Address Copilot stub review comments --- framework/tests/value/unchecked-bytecode.astub | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/framework/tests/value/unchecked-bytecode.astub b/framework/tests/value/unchecked-bytecode.astub index 8397967d27eb..b3f51796243d 100644 --- a/framework/tests/value/unchecked-bytecode.astub +++ b/framework/tests/value/unchecked-bytecode.astub @@ -1,10 +1,10 @@ +package java.lang; + import org.checkerframework.common.value.qual.ArrayLen; import org.checkerframework.common.value.qual.ArrayLenRange; import org.checkerframework.common.value.qual.StringVal; import org.checkerframework.common.value.qual.UnknownVal; -package java.lang; - class Math { static int min(@UnknownVal int a, @UnknownVal int b); @@ -46,7 +46,7 @@ class String { String substring(@UnknownVal int beginIndex, @UnknownVal int endIndex); - String @ArrayLenRange(from = 1) [] split(@UnknownVal String regex); + String @ArrayLenRange(from = 0) [] split(@UnknownVal String regex); boolean startsWith(@UnknownVal String prefix); @@ -92,7 +92,7 @@ package java.lang; import org.checkerframework.common.value.qual.UnknownVal; class ClassLoader { - Class loadClass(@UnknownVal String name); + Class loadClass(@UnknownVal String name) throws ClassNotFoundException; } class Class { @@ -193,7 +193,7 @@ package java.lang.invoke; import org.checkerframework.common.value.qual.UnknownVal; class MethodHandle { - Object invoke(@UnknownVal Object... args); + Object invoke(@UnknownVal Object... args) throws Throwable; } package java.util.stream; From bf919f2fba5f1cc13aa514661f8418c7300c3c93 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Mon, 25 May 2026 13:11:11 -0400 Subject: [PATCH 4/6] Expect String.split unchecked bytecode error --- framework/tests/value/StringSplit.java | 1 + 1 file changed, 1 insertion(+) diff --git a/framework/tests/value/StringSplit.java b/framework/tests/value/StringSplit.java index aba7942c2786..1c063cc18103 100644 --- a/framework/tests/value/StringSplit.java +++ b/framework/tests/value/StringSplit.java @@ -6,6 +6,7 @@ public class StringSplit { void needsALR1(String @ArrayLenRange(from = 1) [] arg) {} void g(String compiler) { + // :: error: (argument.type.incompatible) needsALR1(compiler.trim().split(" +")); } From 8337fa7c5455fb9ebb9fe8580aedc721e3e30600 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Mon, 25 May 2026 13:28:55 -0400 Subject: [PATCH 5/6] Use sound split stub in ValueTest --- .../org/checkerframework/framework/test/junit/ValueTest.java | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/framework/src/test/java/org/checkerframework/framework/test/junit/ValueTest.java b/framework/src/test/java/org/checkerframework/framework/test/junit/ValueTest.java index 01579f71a5e0..bd06c7daa6c3 100644 --- a/framework/src/test/java/org/checkerframework/framework/test/junit/ValueTest.java +++ b/framework/src/test/java/org/checkerframework/framework/test/junit/ValueTest.java @@ -28,7 +28,9 @@ public ValueTest(List testFiles) { // Ignore the test suite's usage of qualifiers in illegal locations. "-AignoreTargetLocations", TestUtilities.adapt( - "-Astubs=tests/value/minints-stub.astub:tests/value/lowercase.astub"), + "-Astubs=tests/value/minints-stub.astub" + + ":tests/value/lowercase.astub" + + ":tests/value/unchecked-bytecode.astub"), "-A" + ValueChecker.REPORT_EVAL_WARNS); } From 168f0171a867fe26212330d5e842360272d37d35 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Mon, 25 May 2026 16:07:12 -0400 Subject: [PATCH 6/6] Use sound split stub in range overflow test --- .../framework/test/junit/ValueIgnoreRangeOverflowTest.java | 2 ++ 1 file changed, 2 insertions(+) diff --git a/framework/src/test/java/org/checkerframework/framework/test/junit/ValueIgnoreRangeOverflowTest.java b/framework/src/test/java/org/checkerframework/framework/test/junit/ValueIgnoreRangeOverflowTest.java index afd06a041383..a50a74f83569 100644 --- a/framework/src/test/java/org/checkerframework/framework/test/junit/ValueIgnoreRangeOverflowTest.java +++ b/framework/src/test/java/org/checkerframework/framework/test/junit/ValueIgnoreRangeOverflowTest.java @@ -2,6 +2,7 @@ import org.checkerframework.common.value.ValueChecker; import org.checkerframework.framework.test.CheckerFrameworkPerDirectoryTest; +import org.checkerframework.framework.test.TestUtilities; import org.junit.runners.Parameterized.Parameters; import java.io.File; @@ -20,6 +21,7 @@ public ValueIgnoreRangeOverflowTest(List testFiles) { "value", // Ignore the test suite's usage of qualifiers in illegal locations. "-AignoreTargetLocations", + TestUtilities.adapt("-Astubs=tests/value/unchecked-bytecode.astub"), "-A" + ValueChecker.REPORT_EVAL_WARNS, "-A" + ValueChecker.IGNORE_RANGE_OVERFLOW); }