First Phase of RLC inference #5870

Nargeshdb · 2023-05-15T17:08:55Z

This PR infers:

@Owning annotation for owning fields and parameters.
@EnsuresCalledMethods for methods that dispose owning fields' obligation
@InheritableMustCall on the class declaration

checker/src/main/java/org/checkerframework/checker/mustcall/MustCallTransfer.java

checker/src/main/java/org/checkerframework/checker/mustcall/MustCallVisitor.java

checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java

mernst

CI is failing. Could you at least make the misc job succeed?

kelloggm

This review only provides high-level feedback on the interactions with the rest of the Checker Framework (i.e., I didn't review MustCallInferenceLogic).

checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsTransfer.java

checker/src/main/java/org/checkerframework/checker/mustcall/MustCallAnnotatedTypeFactory.java

checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakVisitor.java

framework/src/main/java/org/checkerframework/common/accumulation/AccumulationTransfer.java

...rg/checkerframework/common/wholeprograminference/WholeProgramInferenceJavaParserStorage.java

checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java

...rg/checkerframework/common/wholeprograminference/WholeProgramInferenceJavaParserStorage.java

checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakVisitor.java

...rg/checkerframework/common/wholeprograminference/WholeProgramInferenceJavaParserStorage.java

kelloggm

I did a full review of all code not in MustCallInferenceLogic, but I only reviewed the documentation of methods/fields in that class.

checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsTransfer.java

checker/tests/ainfer-resourceleak/non-annotated/EnsuresCalledMethodsTest.java

kelloggm · 2023-06-05T20:42:51Z

framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java

+        analysis
+            .checker
+            .getUpstreamCheckerNames()
+            .contains("org.checkerframework.checker.resourceleak.ResourceLeakChecker");


Putting this in CFAbstractTransfer seems like too much coupling, to me. If you're going to use this implementation strategy (which I'd prefer we replace; see my comment on the first use of the isResourceLeakCheckerEnabled above), this logic should be in some Resource Leak Checker class (maybe as a static method that takes a BaseTypeChecker?)

This flag is used in MustCallTransfer and CalledMethodsTransfer, so I think it should be defined within these two checkers rather than in some Resource Leak Checker class, am I right?

checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java

checker/src/main/java/org/checkerframework/checker/mustcall/MustCallAnnotatedTypeFactory.java

checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java

...rc/main/java/org/checkerframework/checker/resourceleak/ResourceLeakAnnotatedTypeFactory.java

kelloggm · 2023-06-27T14:43:55Z

framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java

@@ -113,6 +113,9 @@ public abstract class CFAbstractTransfer<
  /** Indicates that the whole-program inference is on. */
  private final boolean infer;

+  /** Indicates that the resource leak checker is enabled. */
+  private final boolean enableWPIForRLC;


I still don't think CFAbstractTransfer is the appropriate place for this flag. I agree that it's the LUB of MustCallTransfer and CalledMethodsTransfer, but this class should only contain code that's germane to all CF checkers.

Maybe create an interface with this functionality instead that those two classes can implement?

msridhar

This is looking great! I have one (hopefully last!) comment.

checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInference.java

msridhar

LGTM!

docs/manual/resource-leak-checker.tex

checker/tests/ainfer-resourceleak/non-annotated/ECMInference.java

checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakChecker.java

kelloggm · 2023-10-16T14:25:15Z

checker/src/main/java/org/checkerframework/checker/mustcall/MustCallAnnotatedTypeFactory.java

+      if (getWholeProgramInference() != null
+          && elt.getKind() == ElementKind.PARAMETER
+          && getDeclAnnotation(elt, MustCallAlias.class) != null) {
+        type.replaceAnnotation(BOTTOM);
+      }


It doesn't appear that the comment that you promised here was actually added to the code.

...ker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java

checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInference.java

kelloggm · 2023-10-16T14:48:30Z

checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInference.java

+
+  /**
+   * Adds the node to the disposedFields set if it is a field and its must-call obligation is
+   * satisfied by the given method call. If so, it will be given an @Owning annotation later.


If so, it will be given an @Owning annotation later.

I don't think this is guaranteed to be true, based on the conversation related to disposedFields and its Javadoc, above. Please make sure this is consistent, and that the Javadoc does not make false claims.

I think if we want to be consistent with the algorithm, when we see somewhere in the code, must-call obligation of a field is satisfied, then the field has to be owning. Since disposedFields does not monotonically increase, I think we need to add it to the owningField set too.

I think we need to add it to the owningField set too

If you're saying that there is a bug in the implementation (which I think you are), then we should write a test case for this situation.

I was unable to reproduce a test case because the test infrastructure for WPI can only run for one iteration. I suspect that this issue arises when the @ECM annotation on the finalizer method is inferred during the second iteration.

{ Foo f; void overwriteFoo() { f.a(); f = new Foo(); } finalizer() { closeFoo(f); } }

I was unable to reproduce a test case because the test infrastructure for WPI can only run for one iteration

This should not prevent you from writing a test case: if you want to test what happens on the second iteration, the input should have the annotations produced by the first iteration. This process works inductively, so it is possible to test WPI behavior on any iteration using the one-iteration test infrastructure.

I wasn't able to reproduce this issue because in the test infrastructure, the final result (after inference) should be type checked. If a class has an owning field, it also needs to have a finalizer method m that disposes of the field and an @InheritableMustCall('m') annotation on the class declaration. This contradicts the scenario I described

I wasn't able to reproduce this issue because in the test infrastructure, the final result (after inference) should be type checked

It's possible to avoid this limitation in one of the following ways:

use an @SuppressWarnings annotation to ignore the other warning that you don't care about testing

use the same mechanism in the build.gradle file that is used by the ExpectedErrors.java test case for the AinferTestChecker: effectively, disable the removal of the expected warnings.

Of these two, I think in this situation, you should strongly prefer the former.

If you're not able to get this working, rather than a text-only response, can you include the full test case in your next comment on this thread so that I can try to get it working myself?

kelloggm · 2023-10-16T14:56:00Z

checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInference.java

+  }
+
+  /**
+   * Computes @Owning annotations for the arguments or receiver of a call.


Does it ever make sense for a receiver to be @Owning? I don't think so (and I don't think we considered this case in our formalism at all): receivers are an object of the class that's currently being considered, so I'm not sure what an "owning receiver" means - maybe that the method with that receiver should be a must-call method of the class?

Regardless, I'm concerned that we have code for it at all, since it doesn't make sense to me.

@kelloggm this is referring to the actual parameter passed in the receiver position at a call site, not this inside a method. Does that help?

thanks for the clarification. Yes, this helps. I think we need to distinguish "receiver" (i.e., the self object this of when discussing an instance method of a class) from the "receiver of a method invocation" (i.e., the actual argument passed in the receiver position at a call site). Maybe "receiver argument" would work? I think my confusion here could have been avoided if there was a comment noting this distinction at the first point that the receiver of the method invocation is mentioned here (although to be fair I probably should have figured this out myself from the code...)

checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInference.java

kelloggm · 2023-10-16T15:00:13Z

checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInference.java

+   * @param invocation the method or constructor invocation
+   */
+  private void computeOwningFromInvocation(Set<Obligation> obligations, Node invocation) {
+    if (methodElt == null) {


A brief comment to explain this (seemingly-unrelated) check here would be helpful. methodElt is a field of the class and might be unrelated to invocation, right? So why does it need to be checked here?

It's not actually dereferenced in the body of this method...

It is used in addOwningToParam. I can't recall if the null value here has caused any NPE in real benchmarks. Even if it does, I agree that here is not the best place to check this. I will remove it from here.

kelloggm

I am happy with the current state of this PR and I believe it is ready to merge.

@mernst, please review my changes in 29cfb1f to a method that you wrote. I think it contained a bug, which I fixed: the intention seemed to be to print the actual elements of the collection, not to print a field of the current instance repeatedly. I also made the method static to avoid that problem in the future.

mernst · 2023-10-25T16:05:58Z

Oops! Martin, thanks for fixing my bug.

Co-authored-by: Michael Ernst <mernst@cs.washington.edu> Co-authored-by: Manu Sridharan <msridhar@gmail.com> Co-authored-by: Martin Kellogg <martin.kellogg@njit.edu>

Nargeshdb added 2 commits May 14, 2023 21:31

first phase

695416d

update comments

ab26997

Nargeshdb requested a review from kelloggm May 15, 2023 17:08

mernst requested changes May 15, 2023

View reviewed changes

Undo wildcard imports

ad74e0b

mernst requested changes May 15, 2023

View reviewed changes

kelloggm requested changes May 15, 2023

View reviewed changes

mernst added 2 commits May 16, 2023 09:05

Merge ../checker-framework-branch-master into inference-phase-one

1f16be4

Put shorter clauses first

833231f

mernst requested changes May 16, 2023

View reviewed changes

...rg/checkerframework/common/wholeprograminference/WholeProgramInferenceJavaParserStorage.java Outdated Show resolved Hide resolved

Nargeshdb added 2 commits May 22, 2023 13:20

address comments

22af6f6

address feedbacks

2d23295

This comment was marked as duplicate.

Sign in to view

Nargeshdb added 5 commits May 23, 2023 19:27

address feedbacks

155ded6

update shouldPerformWholeProgramInference in MustCallTransfer

ef2ac88

Merge branch 'master' into inference-phase-one

6a28bfc

add comments

617a7c7

Merge remote-tracking branch 'origin' into inference-phase-one

8f27be1

kelloggm self-requested a review May 30, 2023 16:35

Nargeshdb requested review from msridhar and removed request for kelloggm May 30, 2023 16:35

kelloggm requested changes Jun 5, 2023

View reviewed changes

Nargeshdb added 4 commits June 13, 2023 13:49

Merge branch 'master' into inference-phase-one

e455aa1

update

3a483f5

update comments

2e87329

address Martin's feedback

aae7e30

Nargeshdb requested a review from kelloggm June 26, 2023 16:46

kelloggm requested changes Jun 27, 2023

View reviewed changes

address comments

c48227b

msridhar added 2 commits October 13, 2023 13:16

Merge branch 'master' into inference-phase-one

f3d465c

minor tweaks

75f2e84

msridhar reviewed Oct 13, 2023

View reviewed changes

checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInference.java Outdated Show resolved Hide resolved

add annotations after the while loop

f089e3c

msridhar previously approved these changes Oct 14, 2023

View reviewed changes

mernst assigned kelloggm and unassigned Nargeshdb Oct 14, 2023

Merge branch 'master' into inference-phase-one

3a7cfda

kelloggm requested changes Oct 16, 2023

View reviewed changes

improve documentation

2b2cca2

Nargeshdb dismissed msridhar’s stale review via 2b2cca2 October 17, 2023 03:48

Nargeshdb and others added 8 commits October 17, 2023 00:41

update

eb9f86f

improve comments

c03056b

merge

8bfa69c

add a test

b33b705

update comments

3b39cbb

Merge branch 'master' into inference-phase-one

f80dcde

remove the test

bf851fc

add arg

3011552

Nargeshdb requested a review from kelloggm October 24, 2023 20:51

make debug method static

29cfb1f

kelloggm approved these changes Oct 25, 2023

View reviewed changes

Nargeshdb and others added 3 commits October 25, 2023 10:38

Merge branch 'master' into inference-phase-one

4b64bf4

Merge branch 'master' into inference-phase-one

73fd978

Merge branch 'master' into inference-phase-one

f7f02bf

mernst approved these changes Oct 26, 2023

View reviewed changes

kelloggm enabled auto-merge (squash) October 26, 2023 14:47

kelloggm merged commit d282234 into typetools:master Oct 26, 2023
29 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

First Phase of RLC inference #5870

First Phase of RLC inference #5870

Nargeshdb commented May 15, 2023 •

edited by mernst

Loading

mernst left a comment

kelloggm left a comment

This comment was marked as duplicate.

kelloggm left a comment

kelloggm Jun 5, 2023

Nargeshdb Jun 26, 2023

kelloggm Jun 27, 2023

msridhar left a comment

msridhar left a comment

kelloggm Oct 16, 2023

kelloggm Oct 16, 2023

Nargeshdb Oct 17, 2023

kelloggm Oct 17, 2023

Nargeshdb Oct 17, 2023

kelloggm Oct 18, 2023

Nargeshdb Oct 20, 2023

kelloggm Oct 23, 2023

kelloggm Oct 16, 2023

msridhar Oct 16, 2023

kelloggm Oct 17, 2023

kelloggm Oct 16, 2023

kelloggm Oct 16, 2023

Nargeshdb Oct 17, 2023

kelloggm left a comment

mernst commented Oct 25, 2023

First Phase of RLC inference #5870

First Phase of RLC inference #5870

Conversation

Nargeshdb commented May 15, 2023 • edited by mernst Loading

mernst left a comment

Choose a reason for hiding this comment

kelloggm left a comment

Choose a reason for hiding this comment

This comment was marked as duplicate.

kelloggm left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

msridhar left a comment

Choose a reason for hiding this comment

msridhar left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

kelloggm left a comment

Choose a reason for hiding this comment

mernst commented Oct 25, 2023

Nargeshdb commented May 15, 2023 •

edited by mernst

Loading