diff --git a/.claude/settings.json b/.claude/settings.json new file mode 100644 index 00000000000..1ca8b047bc6 --- /dev/null +++ b/.claude/settings.json @@ -0,0 +1,22 @@ +{ + "enabledPlugins": { + "rust-analyzer-lsp@claude-plugins-official": true + } + "permissions": { + "allow": [ + "WebFetch(domain:checkerframework.org)", + "Bash(mkdir:*)", + "Bash(./gradlew:*)", + "Bash(git -C /home/mernst/research/types/checker-framework-fork-mernst-branch-override-order diff master..override-order --stat)" + "Bash(git -C /home/mernst/research/types/checker-framework-fork-mernst-branch-override-order log master..override-order --oneline)", + "Bash(java:*)", + "Bash(javac:*)", + "Bash(ls)", + "Bash(timeout 300 ./gradlew:*)", + "Bash(./x.py check:*)", + "Read(//scratch/mernst/**)" + ], + "deny": [], + "ask": [] + } +} diff --git a/.coderabbit.yaml b/.coderabbit.yaml new file mode 100644 index 00000000000..bcd9365ae43 --- /dev/null +++ b/.coderabbit.yaml @@ -0,0 +1,46 @@ +# yaml-language-server: $schema=https://coderabbit.ai/integrations/schema.v2.json + +language: "en-US" + +reviews: + profile: "assertive" + high_level_summary: false + review_status: false + collapse_walkthrough: true + changed_files_summary: false + sequence_diagrams: false + estimate_code_review_effort: false + in_progress_fortune: false + poem: false + path_filters: + - "!**/build/**" + - "!**/out/**" + - "!**/.gradle/**" + - "!**/.idea/**" + - "!**/node_modules/**" + auto_review: + auto_pause_after_reviewed_commits: 0 + ignore_title_keywords: + - "wip" + - "draft" + ignore_usernames: + - "dependabot" + - "dependabot[bot]" + - "mend" + - "renovate" + - "renovate[bot]" + pre_merge_checks: + title: + mode: "off" + description: + mode: "off" + +chat: + art: false + +knowledge_base: + code_guidelines: + enabled: true + filePatterns: + - "**/.cursorrules" + - "**/CODING_STANDARDS.md" diff --git a/src/java.base/share/classes/java/lang/System.java b/src/java.base/share/classes/java/lang/System.java index 19439ccff41..6aea0892ef4 100644 --- a/src/java.base/share/classes/java/lang/System.java +++ b/src/java.base/share/classes/java/lang/System.java @@ -31,6 +31,7 @@ import org.checkerframework.checker.mustcall.qual.MustCall; import org.checkerframework.checker.nullness.qual.Nullable; import org.checkerframework.checker.nullness.qual.PolyNull; +import org.checkerframework.checker.regex.qual.Regex; import org.checkerframework.checker.signedness.qual.PolySigned; import org.checkerframework.dataflow.qual.Pure; import org.checkerframework.dataflow.qual.SideEffectFree; @@ -112,7 +113,7 @@ * * @since 1.0 */ -@AnnotatedFor({"index", "interning", "lock", "mustcall", "nullness", "signedness"}) +@AnnotatedFor({"index", "interning", "lock", "mustcall", "nullness", "regex", "signedness"}) public final @UsesObjectEquals class System { /* Register the natives via the static initializer. * @@ -854,7 +855,7 @@ public static Properties getProperties() { * @since 1.7 */ @Pure - public static String lineSeparator() { + public static @Regex String lineSeparator() { return lineSeparator; } diff --git a/src/java.base/share/classes/java/net/HttpURLConnection.java b/src/java.base/share/classes/java/net/HttpURLConnection.java index 9f7779dd011..ada97c4f54b 100644 --- a/src/java.base/share/classes/java/net/HttpURLConnection.java +++ b/src/java.base/share/classes/java/net/HttpURLConnection.java @@ -25,6 +25,9 @@ package java.net; +import org.checkerframework.checker.mustcall.qual.InheritableMustCall; +import org.checkerframework.framework.qual.AnnotatedFor; + import java.io.InputStream; import java.io.IOException; import java.security.Permission; @@ -66,6 +69,8 @@ * @see java.net.HttpURLConnection#disconnect() * @since 1.1 */ +@AnnotatedFor("mustcall") +@InheritableMustCall("disconnect") public abstract class HttpURLConnection extends URLConnection { /* instance variables */ diff --git a/src/java.base/share/classes/org/checkerframework/checker/fenum/qual/FenumUnqualified.java b/src/java.base/share/classes/org/checkerframework/checker/fenum/qual/FenumUnqualified.java index d516e69de09..247342a0707 100644 --- a/src/java.base/share/classes/org/checkerframework/checker/fenum/qual/FenumUnqualified.java +++ b/src/java.base/share/classes/org/checkerframework/checker/fenum/qual/FenumUnqualified.java @@ -6,6 +6,7 @@ import org.checkerframework.framework.qual.TypeUseLocation; import java.lang.annotation.Documented; +import java.lang.annotation.ElementType; import java.lang.annotation.Retention; import java.lang.annotation.RetentionPolicy; import java.lang.annotation.Target; @@ -21,7 +22,7 @@ */ @Documented @Retention(RetentionPolicy.RUNTIME) -@Target({}) // empty target prevents programmers from writing this in a program +@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) @SubtypeOf({FenumTop.class}) @DefaultQualifierInHierarchy @DefaultFor(TypeUseLocation.EXCEPTION_PARAMETER) diff --git a/src/java.base/share/classes/org/checkerframework/checker/index/qual/IndexFor.java b/src/java.base/share/classes/org/checkerframework/checker/index/qual/IndexFor.java index 3a0a4a7d1ed..13320e03a64 100644 --- a/src/java.base/share/classes/org/checkerframework/checker/index/qual/IndexFor.java +++ b/src/java.base/share/classes/org/checkerframework/checker/index/qual/IndexFor.java @@ -14,7 +14,7 @@ * different lengths. * *

The + * href="https://docs.oracle.com/en/java/javase/25/docs/api/java.base/java/lang/String.html#charAt(int)"> * {@code String.charAt(int)} method is declared as * *

{@code
diff --git a/src/java.base/share/classes/org/checkerframework/checker/index/qual/IndexOrHigh.java b/src/java.base/share/classes/org/checkerframework/checker/index/qual/IndexOrHigh.java
index c91497e94aa..31c222dc3aa 100644
--- a/src/java.base/share/classes/org/checkerframework/checker/index/qual/IndexOrHigh.java
+++ b/src/java.base/share/classes/org/checkerframework/checker/index/qual/IndexOrHigh.java
@@ -11,7 +11,7 @@
  * sequence's length.
  *
  * 

The + * href="https://docs.oracle.com/en/java/javase/25/docs/api/java.base/java/util/Arrays.html#binarySearch(java.lang.Object%5B%5D,int,int,java.lang.Object)"> * {@code Arrays.binarySearch} method is declared as * *

{@code
@@ -34,7 +34,10 @@
 @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
 public @interface IndexOrHigh {
     /**
-     * Sequences that the annotated expression is a valid index for or is equal to the lengeth of.
+     * Sequences that the annotated expression is a valid index for or is equal to the length of.
+     *
+     * @return sequences that the annotated expression is a valid index for or is equal to the
+     *     length of
      */
     String[] value();
 }
diff --git a/src/java.base/share/classes/org/checkerframework/checker/index/qual/IndexOrLow.java b/src/java.base/share/classes/org/checkerframework/checker/index/qual/IndexOrLow.java
index e4cd74d2b6d..594a6b3bb14 100644
--- a/src/java.base/share/classes/org/checkerframework/checker/index/qual/IndexOrLow.java
+++ b/src/java.base/share/classes/org/checkerframework/checker/index/qual/IndexOrLow.java
@@ -10,7 +10,7 @@
  * An integer that is either -1 or is a valid index for each of the given sequences.
  *
  * 

The + * href="https://docs.oracle.com/en/java/javase/25/docs/api/java.base/java/lang/String.html#indexOf(java.lang.String)"> * {@code String.indexOf(String)} method is declared as * *


diff --git a/src/java.base/share/classes/org/checkerframework/checker/lock/qual/LockHeld.java b/src/java.base/share/classes/org/checkerframework/checker/lock/qual/LockHeld.java
index 4d8af9898f8..eb402825340 100644
--- a/src/java.base/share/classes/org/checkerframework/checker/lock/qual/LockHeld.java
+++ b/src/java.base/share/classes/org/checkerframework/checker/lock/qual/LockHeld.java
@@ -4,6 +4,7 @@
 import org.checkerframework.framework.qual.SubtypeOf;
 
 import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
 import java.lang.annotation.Retention;
 import java.lang.annotation.RetentionPolicy;
 import java.lang.annotation.Target;
@@ -20,7 +21,7 @@
  */
 @Documented
 @Retention(RetentionPolicy.RUNTIME)
-@Target({})
+@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
 @SubtypeOf(LockPossiblyHeld.class) // This is the bottom type in this hierarchy
 @InvisibleQualifier
 public @interface LockHeld {}
diff --git a/src/java.base/share/classes/org/checkerframework/checker/lock/qual/LockPossiblyHeld.java b/src/java.base/share/classes/org/checkerframework/checker/lock/qual/LockPossiblyHeld.java
index 0cc89dae203..bf7b1095c40 100644
--- a/src/java.base/share/classes/org/checkerframework/checker/lock/qual/LockPossiblyHeld.java
+++ b/src/java.base/share/classes/org/checkerframework/checker/lock/qual/LockPossiblyHeld.java
@@ -10,6 +10,7 @@
 import org.checkerframework.framework.qual.TypeUseLocation;
 
 import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
 import java.lang.annotation.Retention;
 import java.lang.annotation.RetentionPolicy;
 import java.lang.annotation.Target;
@@ -25,7 +26,7 @@
  */
 @Documented
 @Retention(RetentionPolicy.RUNTIME)
-@Target({})
+@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
 @InvisibleQualifier
 @SubtypeOf({})
 @DefaultQualifierInHierarchy
diff --git a/src/java.base/share/classes/org/checkerframework/checker/signature/qual/SignatureUnknown.java b/src/java.base/share/classes/org/checkerframework/checker/signature/qual/SignatureUnknown.java
index a74c04d84fe..ef46ecb04bb 100644
--- a/src/java.base/share/classes/org/checkerframework/checker/signature/qual/SignatureUnknown.java
+++ b/src/java.base/share/classes/org/checkerframework/checker/signature/qual/SignatureUnknown.java
@@ -4,6 +4,7 @@
 import org.checkerframework.framework.qual.SubtypeOf;
 
 import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
 import java.lang.annotation.Retention;
 import java.lang.annotation.RetentionPolicy;
 import java.lang.annotation.Target;
@@ -18,7 +19,7 @@
  */
 @Documented
 @Retention(RetentionPolicy.RUNTIME)
-@Target({}) // empty target prevents programmers from writing this in a program
+@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
 @SubtypeOf({})
 @DefaultQualifierInHierarchy
 public @interface SignatureUnknown {}
diff --git a/src/java.base/share/classes/org/checkerframework/common/aliasing/qual/MaybeLeaked.java b/src/java.base/share/classes/org/checkerframework/common/aliasing/qual/MaybeLeaked.java
index 0d421fc3242..09a951be1f7 100644
--- a/src/java.base/share/classes/org/checkerframework/common/aliasing/qual/MaybeLeaked.java
+++ b/src/java.base/share/classes/org/checkerframework/common/aliasing/qual/MaybeLeaked.java
@@ -5,6 +5,7 @@
 import org.checkerframework.framework.qual.SubtypeOf;
 
 import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
 import java.lang.annotation.Retention;
 import java.lang.annotation.RetentionPolicy;
 import java.lang.annotation.Target;
@@ -22,7 +23,7 @@
  */
 @Documented
 @Retention(RetentionPolicy.RUNTIME)
-@Target({})
+@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
 @DefaultQualifierInHierarchy
 @SubtypeOf({LeakedToResult.class})
 @InvisibleQualifier
diff --git a/src/java.base/share/classes/org/checkerframework/common/subtyping/qual/Unqualified.java b/src/java.base/share/classes/org/checkerframework/common/subtyping/qual/Unqualified.java
index ab339ca71ea..0a71f75c51a 100644
--- a/src/java.base/share/classes/org/checkerframework/common/subtyping/qual/Unqualified.java
+++ b/src/java.base/share/classes/org/checkerframework/common/subtyping/qual/Unqualified.java
@@ -4,6 +4,7 @@
 import org.checkerframework.framework.qual.SubtypeOf;
 
 import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
 import java.lang.annotation.Retention;
 import java.lang.annotation.RetentionPolicy;
 import java.lang.annotation.Target;
@@ -22,7 +23,7 @@
  */
 @Documented
 @Retention(RetentionPolicy.SOURCE) // don't store in class file
-@Target({}) // empty target prevents programmers from writing this in a program.
+@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
 @InvisibleQualifier
 @SubtypeOf({})
 public @interface Unqualified {}
diff --git a/src/java.base/share/classes/org/checkerframework/common/value/qual/DoesNotMatchRegex.java b/src/java.base/share/classes/org/checkerframework/common/value/qual/DoesNotMatchRegex.java
index 8fb1c2667e1..1c7c7756d4e 100644
--- a/src/java.base/share/classes/org/checkerframework/common/value/qual/DoesNotMatchRegex.java
+++ b/src/java.base/share/classes/org/checkerframework/common/value/qual/DoesNotMatchRegex.java
@@ -13,7 +13,7 @@
  * Java regular expressions. If an expression's type has this annotation, then at run time, the
  * expression evaluates to a string that matches none of the regular expressions. Matching is via
  * the java.lang.String#matches
+ * href="https://docs.oracle.com/en/java/javase/25/docs/api/java.base/java/lang/String.html#matches(java.lang.String)">java.lang.String#matches
  * method, which matches against the entire string (it does not look for a match against a
  * substring).
  *
diff --git a/src/java.base/share/classes/org/checkerframework/common/value/qual/IntRangeFromGTENegativeOne.java b/src/java.base/share/classes/org/checkerframework/common/value/qual/IntRangeFromGTENegativeOne.java
index c1cbd3a1673..405a048e3cf 100644
--- a/src/java.base/share/classes/org/checkerframework/common/value/qual/IntRangeFromGTENegativeOne.java
+++ b/src/java.base/share/classes/org/checkerframework/common/value/qual/IntRangeFromGTENegativeOne.java
@@ -15,7 +15,7 @@
  *
  * 

IntRangeFromGTENegativeOne annotations derived from GTENegativeOne annotations are used to * create IntRange annotations, but IntRangeFromGTENegativeOne annotations are not checked when they - * appear on the left hand side of expressions. Therefore, the Index Checker MUST be run on any code + * appear on the left-hand side of expressions. Therefore, the Index Checker MUST be run on any code * with @GTENegativeOne annotations on the left-hand side of expressions, since the Value Checker * will derive information from them but not check them. * diff --git a/src/java.base/share/classes/org/checkerframework/common/value/qual/IntRangeFromNonNegative.java b/src/java.base/share/classes/org/checkerframework/common/value/qual/IntRangeFromNonNegative.java index ecce8296e88..cf393bc52bb 100644 --- a/src/java.base/share/classes/org/checkerframework/common/value/qual/IntRangeFromNonNegative.java +++ b/src/java.base/share/classes/org/checkerframework/common/value/qual/IntRangeFromNonNegative.java @@ -15,7 +15,7 @@ * *

IntRangeFromNonNegative annotations derived from NonNegative annotations are used to create * IntRange annotations, but IntRangeFromNonNegative annotations are not checked when they appear on - * the left hand side of expressions. Therefore, the Index Checker MUST be run on any code + * the left-hand side of expressions. Therefore, the Index Checker MUST be run on any code * with @NonNegative annotations on the left-hand side of expressions, since the Value Checker will * derive information from them but not check them. * diff --git a/src/java.base/share/classes/org/checkerframework/common/value/qual/IntRangeFromPositive.java b/src/java.base/share/classes/org/checkerframework/common/value/qual/IntRangeFromPositive.java index f1cfc6084f3..09a176785a7 100644 --- a/src/java.base/share/classes/org/checkerframework/common/value/qual/IntRangeFromPositive.java +++ b/src/java.base/share/classes/org/checkerframework/common/value/qual/IntRangeFromPositive.java @@ -14,10 +14,10 @@ * annotation. * *

IntRangeFromPositive annotations derived from Positive annotations are used to create IntRange - * annotations, but IntRangeFromPositive annotations are not checked when they appear on the left - * hand side of expressions. Therefore, the Index Checker MUST be run on any code with @Positive - * annotations on the left-hand side of expressions, since the Value Checker will derive information - * from them but not check them. + * annotations, but IntRangeFromPositive annotations are not checked when they appear on the + * left-hand side of expressions. Therefore, the Index Checker MUST be run on any code + * with @Positive annotations on the left-hand side of expressions, since the Value Checker will + * derive information from them but not check them. * *

It is an error to write this annotation directly. {@code @Positive} or {@code IntRange(from = * 1, to = Integer.MAX_VALUE)} should always be written instead. This annotation is not retained in diff --git a/src/java.base/share/classes/org/checkerframework/common/value/qual/MatchesRegex.java b/src/java.base/share/classes/org/checkerframework/common/value/qual/MatchesRegex.java index 49fa1377a88..5282daa65e4 100644 --- a/src/java.base/share/classes/org/checkerframework/common/value/qual/MatchesRegex.java +++ b/src/java.base/share/classes/org/checkerframework/common/value/qual/MatchesRegex.java @@ -13,7 +13,7 @@ * Java regular expressions. If an expression's type has this annotation, then at run time, the * expression evaluates to a string that matches at least one of the regular expressions. Matching * is via the java.lang.String#matches + * href="https://docs.oracle.com/en/java/javase/25/docs/api/java.base/java/lang/String.html#matches(java.lang.String)">java.lang.String#matches * method, which matches against the entire string (it does not look for a match against a * substring). * diff --git a/src/java.base/share/classes/sun/net/www/protocol/http/HttpURLConnection.java b/src/java.base/share/classes/sun/net/www/protocol/http/HttpURLConnection.java index 6280cc1c826..cf75165b839 100644 --- a/src/java.base/share/classes/sun/net/www/protocol/http/HttpURLConnection.java +++ b/src/java.base/share/classes/sun/net/www/protocol/http/HttpURLConnection.java @@ -25,6 +25,9 @@ package sun.net.www.protocol.http; +import org.checkerframework.checker.mustcall.qual.InheritableMustCall; +import org.checkerframework.framework.qual.AnnotatedFor; + import java.security.PrivilegedAction; import java.util.Arrays; import java.net.URL; @@ -97,6 +100,8 @@ */ +@AnnotatedFor("mustcall") +@InheritableMustCall("disconnect") public class HttpURLConnection extends java.net.HttpURLConnection { static final String HTTP_CONNECT = "CONNECT";