[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

@@ -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 ())

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