-
Notifications
You must be signed in to change notification settings - Fork 6
Home
Welcome!
This is a hands-on, play-along tutorial for null-safe programming with the Checker Framework.
Suppose you have created a neat little utility that turns the String A wonderful autumn afternoon
into a-wonderful-autumn-afternoon
:
public static String makeSlug(String s) {
return s.replaceAll("\\s+", "-").toLowerCase();
}
Somewhere else in the app this utility is used to create a page title:
String title = hasTitle()
? getTitle()
: System.getProperty("defaults.title");
String titleSlug = makeSlug(title);
What could go wrong?
If you have been programming Java for any amount of time, the call to
makeSlug()
probably has you shifting around uneasily in your chair: this code
may blow up with a NullPointerException
.
Though it doesn't make it explicit, makeSlug
does not accept a null
argument. We cannot be sure that title
is not null. We don't know if
getTitle()
always returns a non-null value, but at least
System.getProperty()
will return null if the property does not exist.
Therefore the code is not correct.
This is the kind of reasoning we do every day: read the code, follow the flow of references, and track which references may be null at a given point to make sure the code is correct.
Wouldn't it be nice if this sort of reasoning about what may and may not be null at a given place in the code could somehow be expressed in code? And wouldn't it be nice to then have a machine check the flow of nullable and non-null references for us, and establish if the code is correct with respect to null?
This is where the Checker Framework comes in.
-
Intro
-
Tutorial
- Our mission
- Set up
- requirements: Java 1.8, Maven, Checker Framework (could do it just in IDE, but we want to learn this from the ground up, so pure Maven it is)
- install checker framework
- small tweaks to POM, Java version
- First analysis
- where we start,
@Nullable
on entities
- where we start,
- First easy bug fixes
- also more obvious
@Nullable
- also more obvious
- Tweaking the checker, skipUses
- again various improvements
- Using assertions
- assumeAssertions, using assertions to guide the checker
- Suppressing warnings
- on injected fields
- Fixing all bugs in the source
-
mvn compile
successful
-
- Fixing the tests
- What we've achieved
- number of annotations, asserts, suppressions; number of null bugs
- also list LOC; churn -> clearly this refactoring used a very soft brush
-
Summary
-
Further info
- Tooling
- References
etc.