Fix WPI Non-Termination Issue with @UnknownInitialization Annotations

[erfan-arvan]

In some NJR benchmarks (Zenodo Record), when multiple constructors are present, WPI does not account for the absence of initializations. This oversight can lead to non-termination issues, particularly with @UnknownInitialization annotations when visiting object creation.

This repository (wpi-njr-debug) recreates the problem. The dataset/SimplifiedTestCode directory contains sample code that reproduces the issue.

Changes Made

I have modified the updateAnnotationSet method as follows:

For parameters, if rhsmATM is Nullable or MonotonicNonNull and has the @UnknownInitialization annotation, and if the annotation is not @UnknownInitialization(java.lang.Object.class), replace it with @UnknownInitialization(java.lang.Object.class). This is because there is likely a constructor where it hasn't been initialized, and we haven't considered its effect. Otherwise, WPI might get stuck in a loop.

Potential Trade-offs

This approach might result in losing some information regarding cases where the lhs is a parameter and the rhs is Nullable and has the @UnknownInitialization annotation for any class other than java.lang.Object.

We could narrow the domain of this change by analyzing the constructors and fields along with their initialization status or by delving deeper into the initialization checker and attempting to use it. However, based on my tests and pre-implementations, those approaches require significantly more effort and time to implement correctly.

Testing and Results

Based on my experiments, this change resolves the non-termination issue when combined with disabling contract annotations in most benchmarks.

@kelloggm, I would appreciate it if you could review the changes and provide your feedback.

[mernst]

@erfan-arvan Could you please make CI pass? Thanks.

[erfan-arvan]

@erfan-arvan Could you please make CI pass? Thanks.

@mernst
Done. Thank you very much.

[kelloggm]

Please don't add your username here (just your name is sufficient).

[kelloggm]

This code is nullness/initialization-specific, so WholeProgramInferenceImplementation isn't the logical place for it: it should be in the Nullness Checker somewhere.

[kelloggm]

WholeProgramInferenceImplementation has checker-specific callbacks, but we can add more if you need another one.

[kelloggm]

Why is this only an issue for parameters? I'm especially surprised that you need to do this for parameters but not for fields - the underlying issue seems to be about fields.

[erfan-arvan]

It used to be for all assignments and pseudo-assignments, but to narrow down the possible loss of information, I thought it might be better to merely block the propagation of potentially incorrect annotations to other places by filtering the parameters. This approach also stopped the loop problem in my test cases, just like the previous approach. However, to ensure accuracy, I am refining the entire approach, changing its application to field assignments, and transferring it to the Nullness Checker. After my tests pass, I will commit the changes. Thank you very much for your valuable feedback.

[kelloggm]

Use AnnotationUtils.areSameByName instead.

[kelloggm]

The name "wpiAdjustForInitializationAnnotations" doesn't convey the generic purpose of this method. Rather, it conveys the specific purpose that you've used the method for in the Nullness Checker.

The name here should be chosen to explain when this method is called and what it might be used for in the general case, not the specific case that you're trying to fix in this PR. I suggest choosing a name that will help someone reading WholeProgramInferenceImplementation#updateAnnotationSet to understand what this hook does.

[kelloggm]

This comment is inappropriate, because it may not remain true. In particular, it is mixing implementation details of a specific checker (nullness) with the generic WPI algorithm (which is what this code implements). The comment should explain the general purpose of this callback hook, not the specific use in one checker.

[kelloggm]

@erfan-arvan if this PR is ready for me to review again, please request another review using the GitHub UI or post a comment that says so.

[erfan-arvan]

@erfan-arvan if this PR is ready for me to review again, please request another review using the GitHub UI or post a comment that says so.

@kelloggm yes, it's ready for another round. Thank you.

[erfan-arvan]

@kelloggm Sorry, apparently one of the CI tests was canceled in the process. I will rerun the tests and let you know.

[erfan-arvan]

@kelloggm I would appreciate it if you could review the changes. More importantly, if the new naming is not satisfactory, I would appreciate it if you could propose a proper name for the method. Thanks.

[kelloggm]

This PR needs a test case in checker/tests/ainfer-nullness that fails without these changes (and passes with them, of course) before it is merged. If I recall correctly, you have a small test case that you used to demonstrate the problem to me. Please modify that test case so that it appropriately passes/fails and add it to this PR before you request another review.

[kelloggm]

This call to areSameByName cannot possibly return true, because the string input to areSameByName must be a qualified name of an annotation - that is, it cannot have arguments. You could replace this with a call to areSame that takes UNDER_INITIALIZATION as the other argument, I think, to get the semantics that you're looking for.

I'm not sure that this check is really necessary, though. When it resolves to true, it doesn't really matter whether the call to replaceAnnotation below occurs or not, since "replacing" an annotation with another copy of the same annotation has no effect. So, I'd just remove this condition rather than try to get the semantics correct.

[kelloggm]

I suggest the name wpiAdjustForUpdate, to match the existing methods in AnnotatedTypeFactory.

Moreover, I'm not sure that you actually need this new method at all. Conceptually, I don't see any difference between this and calling the code you've written in the implementation in the Nullness Checker from both wpiAdjustForUpdateField and wpiAdjustForUpdateNonField (in the Nullness Checker, of course). In fact, it may be sufficient to only override the latter, which also takes the RHS of a pseudo-assignment as its only argument.

[kelloggm]

"when being assigned to anything" isn't quite correct, I think. This method is called anytime an annotation set is updated, so it is not called just at assignments - instead, it is called any time that WPI does an update, which conceptually is at all pseudo-assignments. The other text that you have here makes that clear, as well; please make this consistent.

[erfan-arvan]

This PR needs a test case in checker/tests/ainfer-nullness that fails without these changes (and passes with them, of course) before it is merged. If I recall correctly, you have a small test case that you used to demonstrate the problem to me. Please modify that test case so that it appropriately passes/fails and add it to this PR before you request another review.

I have added the required test file, and it works as requested on my local system. However, it causes some CI tests to fail. Specifically, in the CI tests, it causes the Checker Framework to crash. According to the logs, the issue is:

> Task :checker:ainferNullnessGenerateJaifs

AinferNullnessJaifsGenerationTest > run[/__w/1/s/checker/tests/ainfer-nullness/non-annotated] STANDARD_OUT
    To see the javac command line and output, run with: -Pemit.test.debug

AinferNullnessJaifsGenerationTest > run[/__w/1/s/checker/tests/ainfer-nullness/non-annotated] FAILED
    java.lang.AssertionError: 8 out of 9 expected diagnostics were found.
    3 unexpected diagnostics were found:
      :-1: other: error: value = GameImpl [class com.sun.tools.javac.code.Type$ClassType]
      ; The Checker Framework crashed.  Please report the crash.  Version: Checker Framework 3.45.1-SNAPSHOT, branch HEAD, 2024-07-07, commit 53ca970, dirty=true. 
      Compilation unit: /__w/1/s/checker/tests/ainfer-nullness/non-annotated/WPIUnknownInitializationLoopTest.java
      Last visited tree at line 5 column 1:
      class GameImpl implements Game {
      Exception: java.lang.ClassNotFoundException: GameImpl; java.lang.ClassNotFoundException: GameImpl
...

I have made some changes, but the problem persists. Could you please guide me on how to solve this problem?
@kelloggm
Thank you very much.

[kelloggm]

@erfan-arvan the failures are in the mostly-deprecated JAIF-based WPI mode. I suspect that there is some problem in JAIF-based WPI that prevents it from handling the test file - probably something related to local classes.

Regardless, this test should be excluded for non-ajava-based WPI, because it relies on input ajava files. You should add an exclusion similar to this one for both JAIF- and stub-based ainferNullness tests, with the justification that the test shouldn't be expected to work without the input .ajava file.