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.

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

CheckerFramework vs Intellij Idea built-in checkers? #3126

Closed
fzyzcjy opened this issue Mar 3, 2020 · 16 comments
Closed

CheckerFramework vs Intellij Idea built-in checkers? #3126

fzyzcjy opened this issue Mar 3, 2020 · 16 comments

Comments

@fzyzcjy
Copy link

fzyzcjy commented Mar 3, 2020

Thanks for the wonderful library! I wonder what are the differences (pros) between this framework and Intellij's default one?

@mernst
Copy link
Member

mernst commented Mar 3, 2020

This is discussed in the Checker Framework manual: https://checkerframework.org/manual/#faq-type-checking-vs-bug-detectors

IntelliJ's only handles one type system: nullness. The Checker Framework handles many type systems and thus can find more different types of bugs in your program.
Even considering only nullness, IntelliJ is unsound and finds fewer nullness errors than the Nullness Checker does.

@fzyzcjy
Copy link
Author

fzyzcjy commented Mar 4, 2020

@mernst Thanks very much!

@fzyzcjy fzyzcjy closed this as completed Mar 4, 2020
@mernst
Copy link
Member

mernst commented Mar 4, 2020

In favor of IntelliJ, it's only fair to note that it runs faster and has nicer IDE integration.

@fzyzcjy
Copy link
Author

fzyzcjy commented Mar 4, 2020

Get it. So I may try to do the following: (1) Do not disable Intellij (2) Install Checker's Intellij plugin (https://blog.rcook.org/blog/2019/01-intellij-checker-framework/) (3) Use Checker inside a continuous integration pipeline (e.g. Jenkins). :)

@mernst
Copy link
Member

mernst commented Mar 4, 2020

That is a reasonable approach. If IntelliJ issues false positive warnings, you may need to suppress them (same for the Checker Framework).
I suggest that you use the official instructions at https://checkerframework.org/manual/#intellij rather than an external blog from over a year ago. However, if there are any problems with the Checker Framework manual, please report them so that we can fix them.

@fzyzcjy
Copy link
Author

fzyzcjy commented Mar 5, 2020

@mernst Sorry I find a cornerstone in the way of using the library: I am using Spring together with lots of libraries. Thus, I have to annotate a LOT of libraries :/

P.S. I am confused about the description of @top and @bottom. Which mean NotNull and which means Nullable, in the context of null checker, or neither? Thanks!

@mernst
Copy link
Member

mernst commented Mar 5, 2020

  1. By default, the Checker Framework will treat libraries optimistically (unsoundly), so you don't have to annotate all the libraries that your program uses. Eventually, if you want sound checking, that will be necessary, however. There are also many ways to suppress warnings to let you focus on just your code.

  2. In the type hierarchy, the type at the top of the figure is the top type, and the type at the bottom of the figure is the botttom type.

@fzyzcjy
Copy link
Author

fzyzcjy commented Mar 6, 2020

Thanks! I find 26.5.6 says

@Top String concatenate(@Bottom String p1, @Bottom String p2)

So does it mean

@Nullable **Object** concatenate(@NonNull String p1, @NonNull String p2)

Or

@Nullable **String** concatenate(@NonNull String p1, @NonNull String p2)

Thanks!

@mernst
Copy link
Member

mernst commented Mar 6, 2020

Regular Java types are never read or changed by the Checker Framework. It only works with type qualifiers/annotations.

@fzyzcjy
Copy link
Author

fzyzcjy commented Mar 6, 2020

Thanks!

@fzyzcjy
Copy link
Author

fzyzcjy commented Mar 6, 2020

I tried to install it using the Maven section since I am running it using pom.xml in Intellij. I am also using lombok so have to use delombok as well. The problem is that, delombok requires any lombok-ed classes to be in a separate directory, which is not that satisfactory (one workaround also has some problems)... In addition, it seems that the Checker framework slows down the compilation to some extent.

Thus, I am thinking about an alternative:

(1) When developing (with Intellij), run without Checker Framework or Delombok.
(2) Use Jenkins to execute the Checker Framework, Delombok, etc, and fix the code when seeing errors. (maybe using a different "maven profile")

What do you think about this strategy?

By the way, what is your workflow or pipeline in your daily life when using Checker Framework?

Anyway, thanks so much for this wonderful library that I believe can save a lot of time and energy!

@mernst
Copy link
Member

mernst commented Mar 6, 2020

I agree that Lombok integration is a problem. The Gradle plugin removes some of the pain, but it sounds like you are using Maven.

Slow compilation is the worst thing about the Checker Framework.

Personally, I run the Checker Framework on every compile for small projects (ones that have less than about 10KLOC). For larger projects, I do what you suggest: I run the Checker Framework periodically, such as in a git pre-commit hook or in continuous integration (such as Jenkins).

I added some text about this to the manual, in commit 64a90ca.

@fzyzcjy
Copy link
Author

fzyzcjy commented Mar 6, 2020

Thanks very much! I will try to do that in a continuous integration environment. By the way, there are some libraries which generate code when running (instead of compiling). For instance, MyBatis. The full code looks like:

public interface BlogMapper {
  @Select("SELECT * FROM blog WHERE id = #{id}")
  Blog selectBlog(int id);
}

and nothing more - no implementation classes or anything more! MyBatis will generate code when starting the application. And note that the result Blog can be null (by their definition).

My idea is that, I have to manually be aware of the problem, and manually change to Optional<Blog> selectBlog(int id). And if I forget it in even one function, the NPE may come and the Checker Framework cannot help me... Is my understanding correct?

In addition, such dynamically generated classes are very common in the Spring framework... So I do not know whether there will be much more such things hidden in the dark, generating NPEs...

Thanks!

@mernst
Copy link
Member

mernst commented Mar 8, 2020

This issue #3126 about the Checker Framework versus IntelliJ is really not the right place for many unrelated questions about the Checker Framework. Could you please open new issues or use the mailing list?

I can't answer your question because I don't know MyBatis details.
If the BlogMapper interface is generated at run time, how is it compiled? How are implementations of the interface compiled? (Or did you show the code that is not generated?)
If only that interface is generated (that's the "full code" and there are no implementing classes), then what is the problem?
Why are you Optional, given that the value is actually nullable and does not have Optional type?

@fzyzcjy
Copy link
Author

fzyzcjy commented Mar 8, 2020

@mernst Sorry for wrongly using this issue! I will open new issues or using mailing list (https://groups.google.com/forum/#!forum/checker-framework-discuss ).

The Mybatis has similar implementations as lombok. It uses cglib to dynamically generate implementations of the interface. So I think checker framework can never have a look at it... P.S. Ignore the part about "Optional" if it is confusing.

@fzyzcjy
Copy link
Author

fzyzcjy commented Mar 8, 2020

@mernst New issue posted: #3139

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants