From 28db342629b07dfd5781498661c8b514bf37441f Mon Sep 17 00:00:00 2001 From: Mitya Lyubarskiy Date: Tue, 10 Mar 2020 04:51:15 -0700 Subject: [PATCH] [nullsafe] Evaluate lhs nullability in assignment check based on field declaration Summary: When assigning to field `field = expr()` we need to compare actual nullability of `expr()` (rhs) with formal nullability of field (lhs). Formal nullability is based on field declaration. Before this diff lhs nullability was calculated based on actual nullability of lhs. This is an absolutely wrong thing to do! E.g. `field = null` would update nullability of field in typestate, and from this field will be considered as nullable, so next time field = null is allowed... Due to series of hacks pile on top of each other, this wrong behavior actually works correctly; but this depends on completely wrong things happening in other places of the program (e.g. typestate modifies in wrong places to make this work!). This diff unblocks refactoring that will clean up hacks mentioned above, and simplify typechecking logic. Reviewed By: artempyanykh Differential Revision: D20334925 fbshipit-source-id: 8bbcbd33a --- infer/src/nullsafe/eradicateChecks.ml | 28 ++++++++++----------------- infer/src/nullsafe/typeCheck.ml | 16 +++++++++------ 2 files changed, 20 insertions(+), 24 deletions(-) diff --git a/infer/src/nullsafe/eradicateChecks.ml b/infer/src/nullsafe/eradicateChecks.ml index 0fe248650..ae0a3cf0c 100644 --- a/infer/src/nullsafe/eradicateChecks.ml +++ b/infer/src/nullsafe/eradicateChecks.ml @@ -118,30 +118,20 @@ let check_condition_for_redundancy tenv ~is_always_true find_canonical_duplicate (** Check an assignment to a field. *) let check_field_assignment ~nullsafe_mode tenv find_canonical_duplicate curr_pdesc node instr_ref - typestate exp_lhs exp_rhs typ loc fname annotated_field_opt typecheck_expr : unit = + typestate ~expr_rhs ~field_type loc fname (annotated_field : AnnotatedField.t) typecheck_expr : + unit = L.d_with_indent ~name:"check_field_assignment" (fun () -> let curr_pname = Procdesc.get_proc_name curr_pdesc in let curr_pattrs = Procdesc.get_attributes curr_pdesc in - let t_lhs, inferred_nullability_lhs = - L.d_strln "Typechecking lhs" ; - typecheck_expr node instr_ref curr_pdesc typestate exp_lhs - (* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *) - (typ, InferredNullability.create TypeOrigin.OptimisticFallback) - loc - in let _, inferred_nullability_rhs = L.d_strln "Typechecking rhs" ; - typecheck_expr node instr_ref curr_pdesc typestate exp_rhs + typecheck_expr node instr_ref curr_pdesc typestate expr_rhs (* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *) - (typ, InferredNullability.create TypeOrigin.OptimisticFallback) + (field_type, InferredNullability.create TypeOrigin.OptimisticFallback) loc in let field_is_injector_readwrite () = - match annotated_field_opt with - | Some AnnotatedField.{annotation_deprecated} -> - Annotations.ia_is_field_injector_readwrite annotation_deprecated - | _ -> - false + Annotations.ia_is_field_injector_readwrite annotated_field.annotation_deprecated in let field_is_in_cleanup_context () = let AnnotatedSignature.{ret_annotation_deprecated} = @@ -150,15 +140,17 @@ let check_field_assignment ~nullsafe_mode tenv find_canonical_duplicate curr_pde in Annotations.ia_is_cleanup ret_annotation_deprecated in + let declared_nullability = + AnnotatedNullability.get_nullability annotated_field.annotated_type.nullability + in let assignment_check_result = - AssignmentRule.check ~nullsafe_mode - ~lhs:(InferredNullability.get_nullability inferred_nullability_lhs) + AssignmentRule.check ~nullsafe_mode ~lhs:declared_nullability ~rhs:(InferredNullability.get_nullability inferred_nullability_rhs) in Result.iter_error assignment_check_result ~f:(fun assignment_violation -> let should_report = (not (AndroidFramework.is_destroy_method curr_pname)) - && PatternMatch.type_is_class t_lhs + && PatternMatch.type_is_class field_type && (not (Fieldname.is_java_outer_instance fname)) && (not (field_is_injector_readwrite ())) && not (field_is_in_cleanup_context ()) diff --git a/infer/src/nullsafe/typeCheck.ml b/infer/src/nullsafe/typeCheck.ml index beb4da3fe..7cde8f425 100644 --- a/infer/src/nullsafe/typeCheck.ml +++ b/infer/src/nullsafe/typeCheck.ml @@ -1121,12 +1121,16 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p in let check_field_assign () = match e1 with - | Exp.Lfield (_, fn, f_typ) -> - let field_type_opt = AnnotatedField.get tenv fn f_typ in - if checks.eradicate then - EradicateChecks.check_field_assignment ~nullsafe_mode tenv find_canonical_duplicate - curr_pdesc node instr_ref typestate1 e1' e2 typ loc fn field_type_opt - (typecheck_expr ~nullsafe_mode find_canonical_duplicate calls_this checks tenv) + | Exp.Lfield (_, field_name, field_class_type) -> ( + match AnnotatedField.get tenv field_name field_class_type with + | Some annotated_field -> + if checks.eradicate then + EradicateChecks.check_field_assignment ~nullsafe_mode tenv find_canonical_duplicate + curr_pdesc node instr_ref typestate1 ~expr_rhs:e2 ~field_type:typ loc field_name + annotated_field + (typecheck_expr ~nullsafe_mode find_canonical_duplicate calls_this checks tenv) + | None -> + L.d_strln "WARNING: could not fetch field declaration; skipping assignment check" ) | _ -> () in