Move PICO to EISOP by aosen-xiong · Pull Request #1013 · eisop/checker-framework

aosen-xiong · 2024-12-09T22:41:15Z

Original code repo: https://github.com/opprop/immutability
Some of commits are presented in: https://github.com/Ao-senXiong/immutability/tree/pico-cf-only
Merge with: eisop/jdk#106
As discussed before, I will try to move PICO here gradually. Hopefully adding test cases and Javadoc with more discussion as well.

Co-authored-by: Werner Dietl <wdietl@gmail.com> Co-authored-by: Haifeng Shi <shihaifeng1998@gmail.com> Co-authored-by: Weitian Xing <xingweitian@gmail.com> Co-authored-by: Jeff Luo <j36luo@uwaterloo.ca> Co-authored-by: Mier Ta <m2ta@uwaterloo.ca>

wmdietl

A quick round of initial comments.

Co-authored-by: Werner Dietl <wdietl@gmail.com>

aosen-xiong · 2024-12-27T02:20:31Z

+        PICOViewpointAdapter vpa = atypeFactory.getViewpointAdapter();
+        AnnotationMirror adapted = vpa.combineAnnotationWithAnnotation(lhs, rhs);
+        return atypeFactory.getQualifierHierarchy().isSubtypeQualifiersOnly(adapted, lhs);
+    }


After #1032, this method and the override of isValidUse( AnnotatedDeclaredType declarationType, AnnotatedDeclaredType useType, Tree tree) can be removed.

…alization`

aosen-xiong · 2025-01-11T22:29:49Z

Looks like this hack override of checkoverride I removed in 38a547a also indicates a bug in the framework StructuralEqualityComparer. Upstream has similar 6867.

I am using a different branch for doing case study on guava based on the hack.

aosen-xiong · 2025-01-16T23:53:39Z

+    protected boolean isTypeCastSafe(AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) {
+        QualifierHierarchy qualifierHierarchy = atypeFactory.getQualifierHierarchy();
+
+        final TypeKind castTypeKind = castType.getKind();
+        if (castTypeKind == TypeKind.DECLARED) {
+            // Don't issue an error if the mutability annotations are equivalent to the qualifier
+            // upper bound of the type.
+            // BaseTypeVisitor#isTypeCastSafe is not used, to be consistent with inference which
+            // only have mutability qualifiers if inference is supporting FBC in the future, this
+            // overridden method can be removed.
+            AnnotatedDeclaredType castDeclared = (AnnotatedDeclaredType) castType;
+            AnnotationMirror bound =
+                    qualifierHierarchy.findAnnotationInHierarchy(
+                            atypeFactory.getTypeDeclarationBounds(castDeclared.getUnderlyingType()),
+                            atypeFactory.READONLY);
+            assert bound != null;
+
+            if (AnnotationUtils.areSame(
+                    castDeclared.getAnnotationInHierarchy(atypeFactory.READONLY), bound)) {
+                return true;
+            }
+        }
+
+        return super.isTypeCastSafe(castType, exprType);


This should be nicer after #1049

Copilot

Pull request overview

Note

Copilot was unable to run its full agentic suite in this review.

Introduces the PICO immutability checker (qualifiers, viewpoint adaptation, validation, and initialization integration) and adds a comprehensive pico-immutability test suite.

Changes:

Added new PICO type system implementation (checker, type factory, viewpoint adapter, validator, qualifier hierarchy, and utilities).
Added extensive negative/positive tests and a JUnit per-directory test runner for pico-immutability.
Updated formatting tooling to recognize the new type annotations.

Reviewed changes

Copilot reviewed 61 out of 62 changed files in this pull request and generated 5 comments.

Show a summary per file

File	Description
framework/src/main/java/org/jmlspecs/annotation/Readonly.java	Adds a JML `@Readonly` annotation for aliasing into PICO.
framework/src/main/java/org/checkerframework/framework/type/AbstractViewpointAdapter.java	Adjusts method viewpoint adaptation behavior (varargs).
checker/tests/pico-immutability/ViewpointAdaptationRules.java	Adds viewpoint adaptation rules test coverage.
checker/tests/pico-immutability/Transitive.java	Adds transitive mutability test coverage.
checker/tests/pico-immutability/SupportedBuilderPattern.java	Adds builder-pattern mutability tests.
checker/tests/pico-immutability/SuperClassTest.java	Adds inheritance/super-call mutability tests.
checker/tests/pico-immutability/StaticTest.java	Adds static-context restrictions tests.
checker/tests/pico-immutability/ReimStudy.java	Adds study/regression tests for viewpoint adaptation constraints.
checker/tests/pico-immutability/RawTypeTest.java	Adds raw-type interaction tests.
checker/tests/pico-immutability/RGB.java	Adds example test for mutable vs immutable receivers.
checker/tests/pico-immutability/RDMClassUse.java	Adds receiver-dependent mutable class usage tests.
checker/tests/pico-immutability/RDMClassConstructor.java	Adds constructor/return qualifier tests for RDM classes.
checker/tests/pico-immutability/RDMClass.java	Adds constructor/method invocation tests for RDM classes.
checker/tests/pico-immutability/PolyMutableTest.java	Adds polymorphic mutability tests.
checker/tests/pico-immutability/PICOTypeUseLocation.java	Adds tests for invalid qualifier locations/uses.
checker/tests/pico-immutability/PICOMethodInit.java	Adds tests for initialization via helper methods.
checker/tests/pico-immutability/PICOInitialization.java	Adds tests for PICO-specific initialization requirements.
checker/tests/pico-immutability/PICOCircularInit.java	Adds circular initialization pattern tests.
checker/tests/pico-immutability/OverrideEquals.java	Adds override checks for `equals`/`clone`/Throwable methods.
checker/tests/pico-immutability/Operators.java	Adds operator write/side-effect tests for readonly receivers.
checker/tests/pico-immutability/ObjectMethods.java	Adds tests for Object method signatures across mutability bounds.
checker/tests/pico-immutability/LocalVariableRefinement.java	Adds tests for local refinement/flow interactions.
checker/tests/pico-immutability/ImplicitMutable.java	Adds tests for implicit shallow-immutable violations.
checker/tests/pico-immutability/ImmutableList.java	Adds tests around immutable collection construction patterns.
checker/tests/pico-immutability/ImmutableClass.java	Adds tests around immutable classes, bounds, and assignability.
checker/tests/pico-immutability/HashCodeSafetyExample.java	Adds object-identity/abstract-state motivation test.
checker/tests/pico-immutability/Generics.java	Adds generic bound/abstract-state interaction tests.
checker/tests/pico-immutability/FactoryPattern.java	Adds a factory/polymutable return behavior test.
checker/tests/pico-immutability/EnumTest.java	Adds enum implicit-immutable tests.
checker/tests/pico-immutability/CloneTest.java	Adds clone-related proposal/regression test content.
checker/tests/pico-immutability/ClassAnnotation.java	Adds tests for class-level qualifier bounds and inheritance rules.
checker/tests/pico-immutability/CastTest.java	Adds cast-safety tests.
checker/tests/pico-immutability/Builder.java	Adds additional builder-pattern examples and edge cases.
checker/tests/pico-immutability/AssignabilityAnnotation.java	Adds tests for `@Assignable` declaration validity rules.
checker/tests/pico-immutability/Arrays.java	Adds array qualifier behavior tests.
checker/src/test/java/org/checkerframework/checker/test/junit/PICOImmutabilityTest.java	Adds JUnit harness for pico-immutability directory tests.
checker/src/main/java/org/checkerframework/checker/pico/messages.properties	Adds user-visible diagnostics for PICO checker.
checker/src/main/java/org/checkerframework/checker/pico/PICOViewpointAdapter.java	Implements PICO-specific viewpoint adaptation rules.
checker/src/main/java/org/checkerframework/checker/pico/PICOValidator.java	Adds PICO-specific type/usage validation rules.
checker/src/main/java/org/checkerframework/checker/pico/PICOTypeUtil.java	Adds helper logic for PICO semantics (assignability, identity, etc.).
checker/src/main/java/org/checkerframework/checker/pico/PICOQualifierHierarchy.java	Customizes qualifier hierarchy behavior (e.g., non-reflexive Lost).
checker/src/main/java/org/checkerframework/checker/pico/PICONoInitVisitor.java	Core type-checking visitor for PICO (without init qualifiers).
checker/src/main/java/org/checkerframework/checker/pico/PICONoInitValue.java	Defines abstract value type for PICO dataflow.
checker/src/main/java/org/checkerframework/checker/pico/PICONoInitTransfer.java	Implements transfer rules (notably null initializer refinement).
checker/src/main/java/org/checkerframework/checker/pico/PICONoInitSubchecker.java	Registers PICO subchecker and initialization interop subchecker.
checker/src/main/java/org/checkerframework/checker/pico/PICONoInitStore.java	Defines store for PICO dataflow analysis.
checker/src/main/java/org/checkerframework/checker/pico/PICONoInitAnnotatedTypeFactory.java	Annotated type factory with defaults, viewpoint adapter, and annotators.
checker/src/main/java/org/checkerframework/checker/pico/PICONoInitAnalysis.java	Analysis factory for stores/values/transfers.
checker/src/main/java/org/checkerframework/checker/pico/PICOInitializationVisitor.java	Hooks PICO into initialization checker visitor.
checker/src/main/java/org/checkerframework/checker/pico/PICOInitializationAnnotatedTypeFactory.java	Filters uninitialized fields per PICO assignability semantics.
checker/src/main/java/org/checkerframework/checker/pico/PICOChecker.java	Top-level checker wiring PICO + initialization.
checker/src/main/java/org/checkerframework/checker/pico/ObjectIdentityMethodEnforcer.java	Enforces object-identity method restrictions in abstract-state-only mode.
checker-qual/src/main/java/org/checkerframework/checker/pico/qual/ReceiverDependentMutable.java	Adds `@ReceiverDependentMutable` qualifier definition.
checker-qual/src/main/java/org/checkerframework/checker/pico/qual/Readonly.java	Adds `@Readonly` qualifier definition and defaults.
checker-qual/src/main/java/org/checkerframework/checker/pico/qual/PolyMutable.java	Adds `@PolyMutable` qualifier definition and target locations.
checker-qual/src/main/java/org/checkerframework/checker/pico/qual/PICOLost.java	Adds `@PICOLost` qualifier definition.
checker-qual/src/main/java/org/checkerframework/checker/pico/qual/PICOBottom.java	Adds `@PICOBottom` qualifier definition and defaulting.
checker-qual/src/main/java/org/checkerframework/checker/pico/qual/ObjectIdentityMethod.java	Adds marker annotation for object identity methods.
checker-qual/src/main/java/org/checkerframework/checker/pico/qual/Mutable.java	Adds `@Mutable` qualifier definition.
checker-qual/src/main/java/org/checkerframework/checker/pico/qual/Immutable.java	Adds `@Immutable` qualifier definition plus DefaultFor/UpperBoundFor.
checker-qual/src/main/java/org/checkerframework/checker/pico/qual/Assignable.java	Adds `@Assignable` annotation definition.
build.gradle	Updates Spotless annotation formatting to recognize PICO qualifiers.

Comments suppressed due to low confidence (5)

framework/src/main/java/org/checkerframework/framework/type/AbstractViewpointAdapter.java:1

computeVarargType() is called before the parameter types are set on methodType. If computeVarargType() relies on the current parameter list (common for determining varargs element type), this can compute the wrong varargs metadata. Move methodType.computeVarargType() to after setParameterTypes(...) (or compute it from unsubstitutedMethodType before copying) so varargs info is derived from the correct parameter types.
checker/tests/pico-immutability/ViewpointAdaptationRules.java:1
These identifiers contain typos (assingableMuatbleField, muatbleObject) that make the test harder to read and maintain. Rename them to correctly spelled names (e.g., assignableMutableField, mutableObject) to keep the tests as clear specifications of the intended typing rules.
checker/tests/pico-immutability/ViewpointAdaptationRules.java:1
These identifiers contain typos (assingableMuatbleField, muatbleObject) that make the test harder to read and maintain. Rename them to correctly spelled names (e.g., assignableMutableField, mutableObject) to keep the tests as clear specifications of the intended typing rules.
checker/tests/pico-immutability/ViewpointAdaptationRules.java:1
These identifiers contain typos (assingableMuatbleField, muatbleObject) that make the test harder to read and maintain. Rename them to correctly spelled names (e.g., assignableMutableField, mutableObject) to keep the tests as clear specifications of the intended typing rules.
framework/src/main/java/org/jmlspecs/annotation/Readonly.java:1
Consider adding an explicit @Target (e.g., ElementType.TYPE_USE and ElementType.TYPE_PARAMETER) to document intended usage and prevent accidental application in unrelated contexts. This is especially useful since the annotation is being aliased into a type system qualifier.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

+            List<? extends AnnotationMirror> recieverAnnotations =
+                    getAllRecieverAnnotation(enclosingMethod);
+            for (AnnotationMirror anno : recieverAnnotations) {
+                if (AnnotationUtils.areSame(anno, atypeFactory.UNDER_INITALIZATION)) {
+                    // If the enclosing method receiver is under initialization, allow assignment
+                    return;
+                }
+            }


+    private List<? extends AnnotationMirror> getAllRecieverAnnotation(MethodTree tree) {
+        com.sun.tools.javac.code.Symbol meth =
+                (com.sun.tools.javac.code.Symbol) TreeUtils.elementFromDeclaration(tree);
+        return meth.getRawTypeAttributes();
+    }


+    public List<VariableTree> getUninitializedFields(
+            InitializationStore initStore,
+            CFAbstractStore<?, ?> targetStore,
+            TreePath path,
+            boolean isStatic,
+            Collection<? extends AnnotationMirror> receiverAnnotations) {
+        List<VariableTree> uninitializedFields =
+                super.getUninitializedFields(initStore, path, isStatic, receiverAnnotations);


+    public PICONoInitStore(PICONoInitStore s) {
+        super(s);
+        if (s.initializedFields != null) {
+            initializedFields = s.initializedFields;
+        }
+    }


+object.identity.method.invocation.invalid=Cannot invoke non-object identity method %s from object identity context!
+object.identity.field.access.invalid=Object identity context cannot reference non abstract state field %s!
+object.identity.static.field.access.forbidden=Object identity context cannot reference static field %s!
+implicit.shallow.immutable=Write an explicit mutable qualifier if wants to exclude the field from the abstract state! Otherwise change the class mutability of this object !


Starting move PICO to EISOP

32a297b

Co-authored-by: Werner Dietl <wdietl@gmail.com> Co-authored-by: Haifeng Shi <shihaifeng1998@gmail.com> Co-authored-by: Weitian Xing <xingweitian@gmail.com> Co-authored-by: Jeff Luo <j36luo@uwaterloo.ca> Co-authored-by: Mier Ta <m2ta@uwaterloo.ca>

aosen-xiong force-pushed the pico-move branch from 33dfd50 to 32a297b Compare December 14, 2024 19:35

aosen-xiong self-assigned this Dec 17, 2024

aosen-xiong added 10 commits December 18, 2024 14:20

Remove static import and holder class

9cc1911

Clear star import and static import again

514a607

Lots of Javadoc and remove some unused method

2a48ae3

Remove dangling Javadoc

4260bd3

Add Javadoc

2e4fffd

A few more Javadoc

7341fad

Add PICO's annotation for format

7a4d4a3

Fix a few errors and add the very first test cases

cac7afa

Format poly and forbid RDM on static class

6d911e4

Yet another test case

61601da

aosen-xiong mentioned this pull request Dec 19, 2024

Add Javadoc to qualifers for viewpoint test checker #1021

Merged

Add object creation test

646b5cb

wmdietl requested changes Dec 20, 2024

View reviewed changes

aosen-xiong and others added 8 commits December 19, 2024 20:52

Use PolyMutable for iterator

911355b

Co-authored-by: Werner Dietl <wdietl@gmail.com>

Rename qualifier to PICO...

d7cdc75

Remove hack

cb648fe

Fixes misc-21 error

63bd81e

Also test validity of annotation on interface and abstract class

b09a116

Remove wrong todo and add JML readonly aliasing

fa1fdd7

Apply spotless

cf0cc18

Add assignability annotation test and improve the error message

2e82b65

aosen-xiong commented Dec 27, 2024

View reviewed changes

aosen-xiong added 5 commits December 26, 2024 18:43

Add RDM class test and initialization test

96c92a9

Merge branch 'master' into pico-move

ebae3a8

Add implicit mutable test

108a938

Add Definite Assignment test

8bb7327

Delete Definite Assignment test as it is already tested in `PICOIniti…

c02a0b2

…alization`

aosen-xiong added 3 commits January 12, 2025 02:05

Fixes PolyMutable factory pattern

e2827d9

Compute Varargs before calling setParameterTypes

3fccd21

Merge branch 'master' into pico-move

da92fa8

aosen-xiong commented Jan 16, 2025

View reviewed changes

aosen-xiong and others added 23 commits January 25, 2025 00:45

Doc cleanup

e3db549

Clean up duplicate code for constructor invocation

586433e

Fixed crash bugs and a few more cleanups

c3a6cea

Clean up code and default method receiver to its class bound

dcfde22

Merge branch 'master' into pico-move

1cc754f

Fix behavior in transitive mutable field

e31d2f7

Fixes array component type

ffb39ee

Merge branch 'master' into pico-move

2f9f082

Merge branch 'master' into pico-move

958f36a

Adapt framework change

e6c21c2

Fixing newest change

698dfc9

Allow underinit receiver to do assignment

58c78d9

Add test case

87a8ca1

Add Circular initialization test case

4c35416

Allow static class be annotated as RDM

c79959b

Merge branch 'master' into pico-move

5f76aaa

Add assumeInitialized option

2ba3033

Merge branch 'master' into pico-move

59367a2

Add suppress warning string

3f22ec2

Merge branch 'master' into pico-move

3fdc6b3

Merge branch 'master' into pico-move

7d3a209

Lost adapts RDM

0d80050

Merge branch 'master' into pico-move

8fcd2b7

Copilot AI review requested due to automatic review settings May 26, 2026 07:17

Copilot AI reviewed May 26, 2026

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Move PICO to EISOP#1013

Move PICO to EISOP#1013
aosen-xiong wants to merge 85 commits into
eisop:masterfrom
aosen-xiong:pico-move

aosen-xiong commented Dec 9, 2024 •

edited

Loading

Uh oh!

wmdietl left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

aosen-xiong Dec 27, 2024

Uh oh!

aosen-xiong commented Jan 11, 2025 •

edited

Loading

Uh oh!

aosen-xiong Jan 16, 2025

Uh oh!

Copilot AI left a comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

aosen-xiong commented Dec 9, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

wmdietl left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

aosen-xiong Dec 27, 2024

Choose a reason for hiding this comment

Uh oh!

aosen-xiong commented Jan 11, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

aosen-xiong Jan 16, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

aosen-xiong commented Dec 9, 2024 •

edited

Loading

aosen-xiong commented Jan 11, 2025 •

edited

Loading