Second Phase of RLC inference #6278

Nargeshdb · 2023-10-31T19:14:17Z

This PR infers:

@NotOwning for return types
@MustCallAlias for both return types and parameter types
@Owning for constructor parameters when there are multiple owning fields.

…amework into inference-phase-two

mernst

Thanks for these enhancements. I have a few comments.

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

mernst · 2023-11-14T16:57:00Z

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

+   * inference. For example, if a field's must-call method is called, it is added to this set. If,
+   * in a later statement in the same method, the same field is re-assigned, it will be removed from
+   * this set (since the field assignment invalidated the previously-inferred closing of the
+   * obligation).
   */
  private final Set<VariableElement> disposedFields = new HashSet<>();


Does the use of a HashSet make the algorithm nondeterministic? (I'm not sure; don't make it a LinkedHashSet unless it needs to be.)

This might cause nondeterministic ordering of fields in @EnsuresCalledMethods annotations, and to prevent this, I've switched to using LinkedHashSet.

mernst · 2023-11-14T16:57:08Z

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

+   *   <li>the inferred owning fields in this analysis.
+   * </ul>
+   *
+   * This set is a superset of the {@code disposedFields} set.
   */
  private final Set<VariableElement> owningFields = new HashSet<>();


Does the use of a HashSet make the algorithm nondeterministic? (I'm not sure; don't make it a LinkedHashSet unless it needs to be.)

Since we don't iterate over this field in our computation, I think using a HashSet should be fine.

mernst · 2023-11-14T16:58:23Z

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

+   * The owned fields. This includes:
+   *
+   * <ul>
+   *   <li>fields with written {@code @Owning} annotations at the entry point of the CFG currently


What does it mean to have an @Owning annotation at the entry point? Does that mean @Owning is written on a field or formal parameter?

It's pointing to the fields, I removed "at the entry ..." to prevent future confusion.

mernst · 2023-11-14T17:00:03Z

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

+   * The keys are the obligation of return nodes, and the values are the index of current method
+   * formal parameter (1-based) that is aliased with the return node.
+   */
+  private final Map<Obligation, Integer> returnNodeToParameter = new HashMap<>();


Should this be named "returnObligationToParameter"?

More generally, please discuss the choice to use obligations rather than nodes as the keys. The documentation says that the map is from return nodes to method parameters, but the implementation is different. Why are obligations needed? Is it because they indicate resource aliasing relationships? Or is it for some other reason?

They are needed to check aliasing relationships of return nodes with parameters.

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

mernst · 2023-11-14T17:18:14Z

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

-    // methods should be called. This map is used to create a single @EnsuresCalledMethods
-    // annotation for fields that share the same must-call obligation.
+    // methods should be called. This map is used to create a @EnsuresCalledMethods annotation for
+    // each set of fields that share the same must-call obligation.
    Map<String, Set<String>> methodToFields = new LinkedHashMap<>();
    for (VariableElement disposedField : disposedFields) {
      List<String> mustCallValues = resourceLeakAtf.getMustCallValues(disposedField);


The value of mustCallValues was known when constructing disposedFields. Would it make sense to record it it dispasedFields so it does not need to be recomputed here?

I changed the deposedFields set to a map to keep the must-call value and save some computation here. Thanks for the suggestion.

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

mernst · 2023-11-14T17:22:38Z

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

@@ -493,7 +610,7 @@ private void addOrUpdateClassMustCall() {
  }

  /**
-   * Computes ownership transfer at the method call to infer @Owning annotation for the arguments
+   * Computes ownership transfer at the method call to infer @Owning annotations for the arguments


I am confused by this comment. Should it be, "Computes ownership transfer at the method call to infer @owning annotations for formal parameters of the current method, if the parameter is passed into the call and the corresponding formal parameter of the callee is @owning."?

It is correct, I updated the comment to what you suggested.

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

msridhar · 2023-12-04T18:25:25Z

@mernst can I get one more approval from you? I had to remove some logic related to resource variables that should be unnecessary now that #6273 has landed

mernst

Thanks for the simplifictation!

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 and others added 30 commits May 14, 2023 21:31

first phase

695416d

update comments

ab26997

Undo wildcard imports

ad74e0b

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

1f16be4

Put shorter clauses first

833231f

address comments

22af6f6

address feedbacks

2d23295

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

Merge branch 'master' into inference-phase-one

e455aa1

update

3a483f5

update comments

2e87329

address Martin's feedback

aae7e30

address comments

c48227b

address Martin's comments

d83eb35

update java doc for checkMethodInvocation

98279da

update

37cd3e2

update java doc for checkMethodInvocation

9e2cc1a

add a test case

a958009

update

f795b0e

update

7e678fb

fix deprecation warning

d32645e

remove a MustAliasWithDifferentMCSet.java

ee90781

update

3bd8772

cleanup

74cfa33

handle arguments passed in varArgs position

6b9f194

address Martin's feedback

6b787ca

mernst added 2 commits November 14, 2023 08:30

Merge branch 'inference-phase-two' of github.com:nargeshdb/checker-fr…

5c86c43

…amework into inference-phase-two

Code review changes

8b41fec

mernst dismissed msridhar’s stale review via 8b41fec November 14, 2023 16:54

mernst added 2 commits November 14, 2023 09:07

Comments

db0ed91

Add TODO comments

7a735cd

mernst requested changes Nov 14, 2023

View reviewed changes

mernst assigned Nargeshdb and unassigned mernst Nov 14, 2023

Nargeshdb and others added 4 commits November 14, 2023 17:35

improve comments

d107269

address Mike's comments

ea65dc4

chage disposedFields set to map

6f4819d

Merge branch 'master' into inference-phase-two

d8681c0

Nargeshdb requested a review from mernst November 17, 2023 00:58

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

b4e1b2a

mernst previously approved these changes Dec 4, 2023

View reviewed changes

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

2ba55f1

mernst dismissed their stale review via 2ba55f1 December 4, 2023 18:02

mernst previously approved these changes Dec 4, 2023

View reviewed changes

Merge branch 'master' into inference-phase-two

324e9f6

msridhar enabled auto-merge (squash) December 4, 2023 18:16

msridhar disabled auto-merge December 4, 2023 18:19

remove unneeded resource variable logic

acc5d3e

msridhar dismissed mernst’s stale review via acc5d3e December 4, 2023 18:24

msridhar enabled auto-merge (squash) December 4, 2023 18:25

mernst approved these changes Dec 4, 2023

View reviewed changes

msridhar mentioned this pull request Dec 4, 2023

Add manual section on RLC inference #6340

Merged

msridhar merged commit ff3cca9 into typetools:master Dec 5, 2023
29 checks passed

msridhar deleted the inference-phase-two branch December 11, 2023 17:02

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Second Phase of RLC inference #6278

Second Phase of RLC inference #6278

Nargeshdb commented Oct 31, 2023

mernst left a comment

mernst Nov 14, 2023

Nargeshdb Nov 16, 2023

mernst Nov 14, 2023

Nargeshdb Nov 16, 2023 •

edited

Loading

mernst Nov 14, 2023

Nargeshdb Nov 16, 2023

mernst Nov 14, 2023

Nargeshdb Nov 16, 2023

mernst Nov 14, 2023

Nargeshdb Nov 17, 2023

mernst Nov 14, 2023

Nargeshdb Nov 16, 2023

msridhar commented Dec 4, 2023

mernst left a comment

Second Phase of RLC inference #6278

Second Phase of RLC inference #6278

Conversation

Nargeshdb commented Oct 31, 2023

mernst 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

Nargeshdb Nov 16, 2023 • edited Loading

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

msridhar commented Dec 4, 2023

mernst left a comment

Choose a reason for hiding this comment

Nargeshdb Nov 16, 2023 •

edited

Loading