From c07223293d80af20df96a8e39a81e7c314a0f473 Mon Sep 17 00:00:00 2001 From: Mitya Lyubarskiy Date: Tue, 3 Nov 2020 03:06:27 -0800 Subject: [PATCH] [nullsafe][annotation graph] Issue a provisional violation in assignments between two provisionally nullables Summary: This change is what makes the annotation graph a _graph_. Now we can detect places when adding one annotation causes an issue that can be fixed by adding another annotation. Reviewed By: artempyanykh Differential Revision: D24650979 fbshipit-source-id: b8452b822 --- infer/src/nullsafe/AssignmentRule.ml | 22 ++++++++++++++++------ 1 file changed, 16 insertions(+), 6 deletions(-) diff --git a/infer/src/nullsafe/AssignmentRule.ml b/infer/src/nullsafe/AssignmentRule.ml index 2abdaa139..19abe8449 100644 --- a/infer/src/nullsafe/AssignmentRule.ml +++ b/infer/src/nullsafe/AssignmentRule.ml @@ -266,9 +266,19 @@ module ReportableViolation = struct end let check ~lhs ~rhs = - let is_subtype = - Nullability.is_subtype - ~supertype:(AnnotatedNullability.get_nullability lhs) - ~subtype:(InferredNullability.get_nullability rhs) - in - Result.ok_if_true is_subtype ~error:{lhs; rhs} + match (lhs, InferredNullability.get_nullability rhs) with + | AnnotatedNullability.ProvisionallyNullable _, Nullability.ProvisionallyNullable -> + (* This is a special case. Assignment of something that comes from provisionally nullable annotation to something that + is annotated as provisionally nullable is a (provisional) violation. + (With an exception when it is an assignment to the same annotation e.g. in recursion calls; + but such exceptions are non-essential for the purposes of calculation of the annotation graph. + ) + *) + Error {lhs; rhs} + | _ -> + let is_subtype = + Nullability.is_subtype + ~supertype:(AnnotatedNullability.get_nullability lhs) + ~subtype:(InferredNullability.get_nullability rhs) + in + Result.ok_if_true is_subtype ~error:{lhs; rhs}