Nullness Checker Case Study of Email Client Java Project

[Damika Anupama]

Dear Checker Framework Organization,

I'm Damika Anupama, a final year undergraduate from Computer Science & Engineering department, University of Moratuwa, Sri Lanka. I'm willing to participate GSoC 2025. And there I selected your organization to go further. After reading your guidelines, I choosed one of old java projects that I did in an early semester: Email Client for the case study. It's a simple java application that covers sending emails and few functionalities. To the main branch, I did few modifications like applying maven build system. 

I went through first 3 sections in the checker framework documentation few times. Then I created a separate branch called nullness-checker-experiment to apply nullness checker. I have used @Nullable, @NonNull, @MonotonicNonNull nullness type qualifiers and @RequiresNonNull, @EnsuresNonNull nullness method annotations in my code. I had to go through couple of times of applying annotations, compiling, solving nullness compiletime errors, rerun, checking functionality in my linux machine. These are the requested details in the guidelines regarding case study:

• Original Code (Unannotated): https://github.com/Damika-Anupama/Email-Client/blob/main/src/main/java/com/damika/emailclient/EmailClient.java
• Annotated Code (Nullness Checker applied): https://github.com/Damika-Anupama/Email-Client/tree/nullness-checker-experiment
• compile command: `mvn clean package`
• run command: `mvn exec:java -Dexec.mainClass="com.damika.emailclient.EmailClient"`
• Build Tool: Maven
• Java Version: 1.8

I've updated the readme.md file in github repo for the further details. Need to mention that there are some areas need to be developed in the code like security, adding tests and so on. In this case study I majorly focused on applying Nullness checker. Please email me if there any issue or problem regarding the code, and I'm happy to guide. I've already ran the code successfully in my linux computer. About GSoC, I haven't choosed any project listed on the list and still working on it.

Thanks,

Kind Regards,

Damika Anupama.

[Damika Anupama]

[Michael Ernst]

Thanks for this annotated project!

It's difficult to understand the diffs between the `main` and `nullness-checker-experiment` branches of your code, because you reorganized the code (you moved the code into different directories).  It would be helpful to make the changes that are not related to nullness per se in the `main` branch as well, so that this diff shows only the nullness annotations (and import statements, etc.):  https://github.com/Damika-Anupama/Email-Client/compare/initialization-checker-experiment

Also, there is no need to write `@NonNull`, because it is the default.  As stated in the second paragraph of https://checkerframework.org/manual/#nullness-checker: "@NonNull is rarely written, because it is the default."

                    -Mike

--
You received this message because you are subscribed to the Google Groups "checker-framework-gsoc" group.
To unsubscribe from this group and stop receiving emails from it, send an email to checker-framework...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/checker-framework-gsoc/41a1ae76-83b7-4eaa-b7a4-72d1555d40b2n%40googlegroups.com.

[Damika Anupama]

Dear Mike,

Thank you very much for your feedback.

I sincerely apologize for the confusion caused due to the major changes in the directory structure between the main and nullness-checker-experiment branches. I've now resolved this by applying all structural and unrelated changes (such as Maven integration and folder restructuring) directly to the main branch. As a result, the nullness-checker-experiment branch now cleanly reflects only the changes related to the Nullness Checker—such as type annotations and corresponding imports.

Following your suggestion, I’ve also removed redundant uses of @NonNull, recognizing that it is the default qualifier.

In addition, I made an effort to explore the Initialization Checker and Map Key Checker as part of this case study. I carefully went through the documentation and examined multiple classes and methods in my codebase to identify potential spots where these checkers might be useful. For the Initialization Checker, I reviewed constructor flows and method pre/postconditions to detect uninitialized fields. Similarly, for the Map Key Checker, I analyzed the use of maps in my application, especially in command selection and validator logic, to find suitable variables that could be annotated with @KeyFor.

However, based on my current understanding and after experimenting with annotations and checker feedback, I was not able to confidently identify places where these checkers could be applied without compilation issues. I fully acknowledge that there might still be places in the codebase I may have overlooked, and I’m open to revisiting these areas with further guidance or deeper insights.

Furthermore codebase follows a modular structure:
com.damika.emailclient
├── model         // Data models (Email, Recipient types)
├── factory       // Factory & abstract creator dp for creating emails and recipients
├── command       // Command pattern for CLI interactions
├── service       // Email sending, file I/O, birthday greetings
├── util          // Input validation, I/O handlers, global exception handler
├── handler       // Global uncaught exception handling

└── EmailClient   // Main entry point and coordinator

• Original Code (Unannotated):https://github.com/Damika-Anupama/Email-Client/tree/main

• Annotated Code (Nullness Checker applied): https://github.com/Damika-Anupama/Email-Client/tree/nullness-checker-experiment

Thanks again for your time and valuable advice. Please let me know if there’s anything else I should refine or improve.

Kind Regards,
Damika Anupama

On Sat, Apr 5, 2025 at 5:22 PM Damika Anupama <damika...@gmail.com> wrote:

Dear Mike,

Thank you very much for your feedback.

I sincerely apologize for the confusion caused due to the major changes in the directory structure between the main and nullness-checker-experiment branches. I've now resolved this by applying all structural and unrelated changes (such as Maven integration and folder restructuring) directly to the main branch. As a result, the nullness-checker-experiment branch now cleanly reflects only the changes related to the Nullness Checker—such as type annotations and corresponding imports.

Following your suggestion, I’ve also removed redundant uses of @NonNull, recognizing that it is the default qualifier.

In addition, I made an effort to explore the Initialization Checker and Map Key Checker as part of this case study. I carefully went through the documentation and examined multiple classes and methods in my codebase to identify potential spots where these checkers might be useful. For the Initialization Checker, I reviewed constructor flows and method pre/postconditions to detect uninitialized fields. Similarly, for the Map Key Checker, I analyzed the use of maps in my application, especially in command selection and validator logic, to find suitable variables that could be annotated with @KeyFor.

However, based on my current understanding and after experimenting with annotations and checker feedback, I was not able to confidently identify places where these checkers could be applied without compilation issues. I fully acknowledge that there might still be places in the codebase I may have overlooked, and I’m open to revisiting these areas with further guidance or deeper insights.

Furthermore codebase follows a modular structure:
com.damika.emailclient
├── model         // Data models (Email, Recipient types)
├── factory       // Factory & abstract creator dp for creating emails and recipients
├── command       // Command pattern for CLI interactions
├── service       // Email sending, file I/O, birthday greetings
├── util          // Input validation, I/O handlers, global exception handler
├── handler       // Global uncaught exception handling

└── EmailClient   // Main entry point and coordinator

• Original Code (Unannotated):https://github.com/Damika-Anupama/Email-Client/tree/main

• Annotated Code (Nullness Checker applied): https://github.com/Damika-Anupama/Email-Client/tree/nullness-checker-experiment

Thanks again for your time and valuable advice. Please let me know if there’s anything else I should refine or improve.

Kind Regards,
Damika Anupama

[Damika Anupama]

Dear Checker Framework Organization,

Could you please review my draft proposal on GSoC: Introducing NullnessLight: A Simplified Nullness Type System for Detecting Null Bugs with the Checker Framework.pdf

I choosed the project creating new type system: Nullness bug detector/ NullnessLight Checker

I've added

• an Introduction
• draft user manual for the checker
• my case study
• resume & grade report

Thanks for your time and consideration.

Kind regards,

Damika