Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Class literals in CFGs and their type with conservative nullness #548

Open
wmdietl opened this issue Aug 1, 2023 · 6 comments · May be fixed by #550
Open

Class literals in CFGs and their type with conservative nullness #548

wmdietl opened this issue Aug 1, 2023 · 6 comments · May be fixed by #550
Assignees
@Ao-senXiong

Comments

@wmdietl
Copy link
Member

wmdietl commented Aug 1, 2023

In MyEnum.java put the following and compile with javac:

enum MyEnum {
	VALUE;
}

Then put the following into ConservativeClassLiteral.java:

import java.util.EnumSet;

class ConservativeClassLiteral {
  EnumSet<MyEnum> none() {
    return EnumSet.noneOf(MyEnum.class);
  }
}

Class literals should always be initialized and non-null, independent of whether conservative defaults are used.
However, when compiling with ./checker/bin/javac -cp . -processor nullness -AuseConservativeDefaultsForUncheckedCode=bytecode,-source ConservativeClassLiteral.java one gets:

ConservativeClassLiteral.java:5: error: [argument.type.incompatible] incompatible argument for parameter elementType of noneOf.
    return EnumSet.noneOf(MyEnum.class);
                                ^
  found   : @UnknownInitialization @Nullable Class<@Initialized @NonNull MyEnum>
  required: @Initialized @NonNull Class<@Initialized @NonNull MyEnum>
1 error

When looking at the CFG for the above example, one first sees a ClassName node for MyEnum followed by a FieldAccess node for MyEnum.class.
This is wrong, as the javadoc for FieldAccess explicitly states: It does not represent a class literal such as {@code SomeClass.class} or {@code int[].class}; see https://github.com/eisop/checker-framework/blob/388fdb094942de42e871a96171fadb80c4d1a0e1/dataflow/src/main/java/org/checkerframework/dataflow/expression/FieldAccess.java#L19C45-L20C43 .
@Ao-senXiong
Copy link
Member

Ao-senXiong commented Aug 2, 2023 •
edited
Loading

Thanks, I have reproduced the result and CFG. I am working on it right now.

@Ao-senXiong
Copy link
Member

@wmdietl Dear Prof. Dietl, for adding this test case to the repo, include the MyEnum.class or MyEnum.java with a compile script, which one do you think is better?

@wmdietl
Copy link
Member Author

wmdietl commented Aug 3, 2023

@wmdietl Dear Prof. Dietl, for adding this test case to the repo, include the MyEnum.class or MyEnum.java with a compile script, which one do you think is better?

In general let's try to avoid .class files. With jtreg you can very flexibly compile test files.
See e.g. this where we first compile a class without checker and then run different checks.
Something similar should work here, with different flags for how conservative to be.

@Ao-senXiong
Copy link
Member

@wmdietl Dear Prof. Dietl, for adding this test case to the repo, include the MyEnum.class or MyEnum.java with a compile script, which one do you think is better?

In general let's try to avoid .class files. With jtreg you can very flexibly compile test files. See e.g. this where we first compile a class without checker and then run different checks. Something similar should work here, with different flags for how conservative to be.

Thanks for providing me with the resource.

@Ao-senXiong Ao-senXiong linked a pull request Aug 4, 2023 that will close this issue
Open
@Ao-senXiong
Copy link
Member

As described in the isFieldAccess method javadoc: This method currently also returns true for class literals and qualified this. https://github.com/eisop/checker-framework/blob/dff55470ded29b0a99cb26ba9b4e5158db0ec849/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java#L1555C43-L1555C43.

I think this is wrong and cause the fieldaccess on class literal in

checker-framework/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java

Line 3561 in f50cbe3

if (!TreeUtils.isFieldAccess(tree)) {
.

I think we should use classnamenode for class literal. But I am not sure if is there any easy way to make sure the isFieldAccess method only returns true for field access.

@Ao-senXiong
Copy link
Member

I am a little confused, should we consider MyEnum.class a member select process? If not, there should be only one classname nodes for class literals.
image

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@Ao-senXiong Ao-senXiong

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Fix Class literals in field access and related type checks Ao-senXiong/checker-framework
2 participants
@wmdietl @Ao-senXiong