Separate Initialization Checker #444

flo2702 · 2023-03-23T19:47:14Z

This branch rewrites the Initialization Checker such that checking of the initialization hierarchy and the target hierarchy is done in two separate checkers instead of at once. The Javadoc to the InitializationChecker class explains how this can be implemented for any given target type system.

For every type system that uses the Initialization Checker (only nullness so far), initialization checking can now be deactivated via the -AassumeInitialized command-line option or via @SuppressWarnings("initialization") annotations.

Also fixes #297.

Merge together with eisop/checker-framework.demos#4.

…trized with an invariant, but considers every field to be an invariant annotation

…ere monotonically initialized

wmdietl

Thanks for all your further refinement!
I've pushed a few changes directly, please review them - in particular the changelog.
A few more comments about the documentation, but I haven't gone through everything yet.

...ain/java/org/checkerframework/checker/initialization/InitializationAnnotatedTypeFactory.java

checker/src/main/java/org/checkerframework/checker/initialization/InitializationChecker.java

...g/checkerframework/checker/initialization/InitializationFieldAccessAnnotatedTypeFactory.java

checker/tests/initialization/NotOnlyInitializedTest.java

checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitTransfer.java

...al/src/main/java/org/checkerframework/checker/initialization/qual/HoldsForDefaultValues.java

wmdietl

Great work! I really like all these improvements!
I pushed a few more changes myself and asked a few more questions.

...g/checkerframework/checker/initialization/InitializationFieldAccessAnnotatedTypeFactory.java

...va/org/checkerframework/checker/initialization/InitializationParentAnnotatedTypeFactory.java

checker/src/test/java/org/checkerframework/checker/test/junit/NullnessTest.java

checker/tests/initialization/Suppression.java

docs/manual/nullness-checker.tex

wmdietl · 2023-09-20T23:17:55Z

framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java

@@ -2625,7 +2642,7 @@ public boolean shouldSkipUses(@FullyQualifiedName String typeName) {
     * @param tree class to potentially skip
     * @return true if checker should not test {@code tree}
     */
-    public final boolean shouldSkipDefs(ClassTree tree) {
+    public boolean shouldSkipDefs(ClassTree tree) {


Instead of making these two methods non-final, how about adding handling of parentChecker to these methods?
The logic in NullnessNoInitSubchecker.java makes sense for all checkers with a parent, right?

Will be addressed by #572

framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java

…, move to top-level class, and improve comments

wmdietl

Thanks for the final touches. I'll merge this now. Let's try it in practice and see what the feedback is.

wmdietl · 2023-09-25T16:53:30Z

framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java

@@ -2655,7 +2672,7 @@ public final boolean shouldSkipDefs(ClassTree tree) {
     * @param meth method to potentially skip
     * @return true if checker should not test {@code meth}
     */
-    public final boolean shouldSkipDefs(ClassTree cls, MethodTree meth) {
+    public boolean shouldSkipDefs(ClassTree cls, MethodTree meth) {


Undo with #572

flo2702 added 30 commits November 14, 2022 18:30

Turn InitChecker into subchecker; the InitChecker is no longer parame…

633c24f

…trized with an invariant, but considers every field to be an invariant annotation

Fix some false positives

67cc9e8

Add CommitmentFieldAccessTreeAnnotator

31b3988

Don't emit init errors for assigned fields

c92b254

Keep declared type of assignable fields in method call transfer function

6cc92ea

Defer initialization errors to parent checker

1357b6e

Transfer function takes receiver initialization into account

8449449

Fix bug in init checker viewpoint adaption

79d2bda

Fix bug where NotOnlyInitialized fields would be treated as if they w…

030f894

…ere monotonically initialized

The result of a binary or unary operator is always @initialized

b393ebc

Add some additional expected errors to test cases

f1f25ce

Fix checks for static initialization

e7e5961

Fix bug which treated access to other instance's field as self access

5dd834a

Fix treatment of generics

9057bdb

Fix bug where this and super were sometimes not considered initialized

1af1ebd

Fix contracts

b35b6f3

Allow multiple invariants

64262e6

Code cleanup

26a2c5b

Make error handling more general

5132b3c

Fix -AassumeInit option

29846b6

Add documentation

0b8b23a

Close typetools#297

e418c65

Merge branch 'eisopmaster' into separateInitChecker

31732b1

Re-fix typetools issue 5402, which was broken by merge

8f2a097

Fix type errors

093c8a1

Fix wrong reference in Javadoc

09faec2

Don't warn about redundant stubs for initialization

9e4af8c

Adapt jtreg tests to new init checker

97d4b4e

Make all classes immutable w.r.t. initialization

c7c435a

Adapt SuppressWarnings annotations to new init checker

6f55574

flo2702 and others added 5 commits September 12, 2023 14:53

Merge branch 'master' into separateInitChecker

8c1a567

Merge branch 'master' into separateInitChecker

2a2ff62

First attempt at a changelog entry

54fda8f

Some rewordings and expansions

b1d3730

Adapt error messages

96c7f35

wmdietl requested changes Sep 19, 2023

View reviewed changes

wmdietl reviewed Sep 19, 2023

View reviewed changes

...al/src/main/java/org/checkerframework/checker/initialization/qual/HoldsForDefaultValues.java Outdated Show resolved Hide resolved

wmdietl added 9 commits September 20, 2023 19:35

Use canonical expected error format

0fec7d1

Don't store type factory with all stores

51a85ce

Consistent capitalization of Lhs

d429f93

Use @see references

c39272c

Add fixed issues

de1822d

Add back WPI comment

5569192

Don't add trivial subclass

48253bc

Improve javadoc

6d82704

Directly use type factory

7e2dae7

wmdietl reviewed Sep 20, 2023

View reviewed changes

wmdietl and others added 2 commits September 20, 2023 19:51

Apply suggestions from code review

caacabc

Improve some documentation

c62334a

flo2702 mentioned this pull request Sep 22, 2023

Unify handling of supported options of subcheckers #571

Open

flo2702 added 4 commits September 22, 2023 12:33

Update outdated comments

7f9fb36

Rename CommitmentFieldAccessTreeAnnot to InitializationFieldAccess...…

d6e93fd

…, move to top-level class, and improve comments

Extend changelog

7d727b5

Improve documentation of InitATF

2803f89

wmdietl approved these changes Sep 25, 2023

View reviewed changes

wmdietl merged commit 280d513 into eisop:master Sep 25, 2023

wmdietl reviewed Sep 25, 2023

View reviewed changes

wmdietl mentioned this pull request Nov 18, 2023

Scan through members in InitializationFieldAccessVisitor #619

Merged

wmdietl mentioned this pull request Feb 19, 2024

Conservatively remove InitializationStore#newFieldValueAfterMethodCall to optimize performance #712

Merged

wmdietl mentioned this pull request Mar 1, 2024

NotOnlyInitialized test coverage #720

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Separate Initialization Checker #444

Separate Initialization Checker #444

flo2702 commented Mar 23, 2023 •

edited by wmdietl

Loading

wmdietl left a comment

wmdietl left a comment

wmdietl Sep 20, 2023

wmdietl Sep 25, 2023

wmdietl left a comment

wmdietl Sep 25, 2023

Separate Initialization Checker #444

Separate Initialization Checker #444

Conversation

flo2702 commented Mar 23, 2023 • edited by wmdietl Loading

wmdietl left a comment

Choose a reason for hiding this comment

wmdietl left a comment

Choose a reason for hiding this comment

wmdietl Sep 20, 2023

Choose a reason for hiding this comment

wmdietl Sep 25, 2023

Choose a reason for hiding this comment

wmdietl left a comment

Choose a reason for hiding this comment

wmdietl Sep 25, 2023

Choose a reason for hiding this comment

flo2702 commented Mar 23, 2023 •

edited by wmdietl

Loading