Fix Pulse NULL_DEREFERENCE false negative caused by irrelevant inequa…#2018
Fix Pulse NULL_DEREFERENCE false negative caused by irrelevant inequa…#2018bhuvii2005 wants to merge 1 commit intofacebook:mainfrom
Conversation
|
Hi @bhuvii2005! Thank you for your pull request and welcome to our community. Action RequiredIn order to merge any pull request (code, docs, etc.), we require contributors to sign our Contributor License Agreement, and we don't seem to have one on file for you. ProcessIn order for us to review and merge your suggested changes, please sign at https://code.facebook.com/cla. If you are contributing on behalf of someone else (eg your employer), the individual CLA may not be sufficient and your employer may need to sign the corporate CLA. Once the CLA is signed, our tooling will perform checks and validations. Afterwards, the pull request will be tagged with If you have received this in error or have any questions, please contact us at cla@meta.com. Thanks! |
|
Thank you for signing our Contributor License Agreement. We can now accept your code for this (and any) Meta Open Source project. Thanks! |
|
Hi @bhuvii2005 Thanks for your contribution. I don't have enough time to experiment myself your proposal, but you have to be aware that relaxing the heuristic for "relevant variable" raise a risk of False Positive. In our industrial setting, this a costly risk. With your approach, if a function relies on some global invariants about global variables, you will make error manifest. If you are sure your approach si useful at least for you (but did you run large experiments to prove that?), you can propose a pull-request where your approach is gated with a specific new option. But I would like to read a bit about your experiments first. |
Title: Fix Pulse NULL_DEREFERENCE false negative caused by irrelevant inequalities
(Note: This contribution was developed with the assistance of an AI coding agent to trace the OCaml bug through the Pulse arithmetic logic.)
Summary: Infer's Pulse analysis currently fails to report a NULL_DEREFERENCE when the null-dereference occurs in a branch that is preceded by an irrelevant if-else statement checking a constant non-null value (e.g., if (System.out != null)).
This happens because PulseFormula.is_manifest incorrectly suppresses the issue as a "latent" issue. When evaluating the condition System.out != null, Pulse adds an inequality constraint [System.out ≠ 0] to the path condition. is_manifest then evaluates this constraint—which involves an unallocated variable—and assumes the path is only possible in specific caller contexts, thereby suppressing the NULL_DEREFERENCE that occurs later on a completely unrelated variable.
Changes: This PR makes PulseFormula.is_manifest context-aware by piping down the diagnostic parameter from LatentIssue.should_report.
Extracted the invalid address variable from the AccessToInvalidAddress diagnostic.
Updated is_manifest to ignore neq_zero conditions if the variable involved in the constraint is unrelated to the variable that was null-dereferenced.
Piped ~diagnostic through PulseLatentIssue.should_report, PulseArithmetic, and down to PulseFormula.
Test Plan:
Added test1_useless_branch_npe_Bad and test2_useless_branch_npe_Ok to infer/tests/codetoanalyze/java/pulse/NullPointerExceptions.java.
This guarantees that the NULL_DEREFERENCE is correctly caught on the array variable even when preceded by an irrelevant System.out == null check.