[nullsafe] InferredNullability's nullability is determined by TypeOrigin

Summary:
This is one of key diff in this refactoring stack.

Previously, we used to set nullability independently of type origin,
which opened doors for inconsistent states, bugs, and overcomplicated
code.

Now we have just two method left:
1. `create` -> the main one, yay
2. `set_nonnull` -> will get rid of this in the next diff.

Reviewed By: artempyanykh

Differential Revision: D18451950

fbshipit-source-id: edc485709

infer/src/nullsafe/InferredNullability.ml

@@ -9,6 +9,8 @@ open! IStd
 
 type t = {nullability: Nullability.t; origin: TypeOrigin.t} [@@deriving compare]
 
+let create origin = {nullability= TypeOrigin.get_nullability origin; origin}
+
 let get_nullability {nullability} = nullability
 
 let is_nonnull_or_declared_nonnull {nullability} =
@@ -67,17 +69,3 @@ let origin_is_fun_library t =
       proc_origin.TypeOrigin.is_library
   | _ ->
       false
-
-
-let create_nullable origin = {origin; nullability= Nullability.Nullable}
-
-let create_nonnull origin = {origin; nullability= Nullability.Nonnull}
-
-let of_annotated_nullability annotated_nullability origin =
-  match annotated_nullability with
-  | AnnotatedNullability.Nullable _ ->
-      {origin; nullability= Nullability.Nullable}
-  | AnnotatedNullability.DeclaredNonnull _ ->
-      {origin; nullability= Nullability.DeclaredNonnull}
-  | AnnotatedNullability.Nonnull _ ->
-      {origin; nullability= Nullability.Nonnull}

infer/src/nullsafe/InferredNullability.mli

@@ -21,9 +21,7 @@ type t [@@deriving compare]
 
 val get_nullability : t -> Nullability.t
 
-val create_nullable : TypeOrigin.t -> t
+val create : TypeOrigin.t -> t
-
-val create_nonnull : TypeOrigin.t -> t
 
 val is_nonnull_or_declared_nonnull : t -> bool
 
@@ -36,12 +34,6 @@ val descr_origin : t -> TypeErr.origin_descr
   (How did nullsafe infer the nullability )
  *)
 
-val of_annotated_nullability : AnnotatedNullability.t -> TypeOrigin.t -> t
-(** Convert formal type to inferred nullability.
-  (e.g. to infer nullability of {[o]} in {[Object o = someFunction();]}
-   based on {[someFunction()]} formal return type.
- *)
-
 val get_origin : t -> TypeOrigin.t
 (** The simple explanation of how was nullability inferred.  *)
 

infer/src/nullsafe/eradicate.ml

@@ -34,18 +34,16 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct
       annotated_signature linereader proc_loc : bool * TypeState.t option =
     let add_formal typestate (param_signature : AnnotatedSignature.param_signature) =
       let pvar = Pvar.mk param_signature.mangled curr_pname in
-      let inferred_nullability =
       let formal_name = param_signature.mangled in
+      let origin =
         if Mangled.is_this formal_name then
           (* `this` is technically an implicit method param, but from syntactic and semantic points of view it
              has very special meaning and nullability limitations (it can never be null).
           *)
-          InferredNullability.create_nonnull TypeOrigin.This
+          TypeOrigin.This
-        else
+        else TypeOrigin.MethodParameter param_signature
-          let origin = TypeOrigin.MethodParameter param_signature in
-          InferredNullability.of_annotated_nullability
-            param_signature.param_annotated_type.nullability origin
       in
+      let inferred_nullability = InferredNullability.create origin in
       TypeState.add pvar (param_signature.param_annotated_type.typ, inferred_nullability) typestate
     in
     let get_initial_typestate () =

infer/src/nullsafe/eradicateChecks.ml

@@ -123,13 +123,13 @@ let check_field_assignment ~is_strict_mode tenv find_canonical_duplicate curr_pd
   let t_lhs, inferred_nullability_lhs =
     typecheck_expr node instr_ref curr_pdesc typestate exp_lhs
       (* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *)
-      (typ, InferredNullability.create_nonnull TypeOrigin.OptimisticFallback)
+      (typ, InferredNullability.create TypeOrigin.OptimisticFallback)
       loc
   in
   let _, inferred_nullability_rhs =
     typecheck_expr node instr_ref curr_pdesc typestate exp_rhs
       (* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *)
-      (typ, InferredNullability.create_nonnull TypeOrigin.OptimisticFallback)
+      (typ, InferredNullability.create TypeOrigin.OptimisticFallback)
       loc
   in
   let field_is_injector_readwrite () =
@@ -387,7 +387,7 @@ let check_call_receiver ~is_strict_mode tenv find_canonical_duplicate curr_pdesc
       let _, this_inferred_nullability =
         typecheck_expr tenv node instr_ref curr_pdesc typestate this_e
           (* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *)
-          (typ, InferredNullability.create_nonnull TypeOrigin.OptimisticFallback)
+          (typ, InferredNullability.create TypeOrigin.OptimisticFallback)
           loc
       in
       check_object_dereference ~is_strict_mode tenv find_canonical_duplicate curr_pdesc node

infer/src/nullsafe/typeCheck.ml

@@ -118,14 +118,14 @@ let rec typecheck_expr ~is_strict_mode find_canonical_duplicate visited checks t
          We distinct them by type.
       *)
       if PatternMatch.type_is_class typ then
-        (typ, InferredNullability.create_nullable (TypeOrigin.NullConst loc))
+        (typ, InferredNullability.create (TypeOrigin.NullConst loc))
       else
         (* 0 const (this is not the same as null) *)
-        (typ, InferredNullability.create_nonnull (TypeOrigin.NonnullConst loc))
+        (typ, InferredNullability.create (TypeOrigin.NonnullConst loc))
   | Exp.Const _ ->
       let typ, _ = tr_default in
       (* We already considered case of null literal above, so this is a non-null const. *)
-      (typ, InferredNullability.create_nonnull (TypeOrigin.NonnullConst loc))
+      (typ, InferredNullability.create (TypeOrigin.NonnullConst loc))
   | Exp.Lvar pvar ->
       Option.value (TypeState.lookup_pvar pvar typestate) ~default:tr_default
   | Exp.Var id ->
@@ -139,16 +139,16 @@ let rec typecheck_expr ~is_strict_mode find_canonical_duplicate visited checks t
         typecheck_expr ~is_strict_mode find_canonical_duplicate visited checks tenv node instr_ref
           curr_pdesc typestate exp
           (* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *)
-          (typ, InferredNullability.create_nonnull TypeOrigin.OptimisticFallback)
+          (typ, InferredNullability.create TypeOrigin.OptimisticFallback)
           loc
       in
       let object_origin = InferredNullability.get_origin inferred_nullability in
       let tr_new =
         match AnnotatedField.get tenv field_name typ with
-        | Some AnnotatedField.{annotated_type} ->
+        | Some AnnotatedField.{annotated_type= field_type} ->
-            ( annotated_type.typ
+            ( field_type.typ
-            , InferredNullability.of_annotated_nullability annotated_type.nullability
+            , InferredNullability.create
-                (TypeOrigin.Field {object_origin; field_name; access_loc= loc}) )
+                (TypeOrigin.Field {object_origin; field_name; field_type; access_loc= loc}) )
         | None ->
             tr_default
       in
@@ -246,11 +246,11 @@ let update_typestate_fld ~is_assignment tenv access_loc typestate pvar object_or
       typestate
   | _ -> (
     match AnnotatedField.get tenv field_name typ with
-    | Some AnnotatedField.{annotated_type} ->
+    | Some AnnotatedField.{annotated_type= field_type} ->
         let range =
-          ( annotated_type.typ
+          ( field_type.typ
-          , InferredNullability.of_annotated_nullability annotated_type.nullability
+          , InferredNullability.create
-              (TypeOrigin.Field {object_origin; field_name; access_loc}) )
+              (TypeOrigin.Field {object_origin; field_name; field_type; access_loc}) )
         in
         TypeState.add pvar range typestate
     | None ->
@@ -424,7 +424,7 @@ let typecheck_expr_simple ~is_strict_mode find_canonical_duplicate curr_pdesc ca
     node instr_ref typestate1 exp1 typ1 origin1 loc1 =
   typecheck_expr ~is_strict_mode find_canonical_duplicate calls_this checks tenv node instr_ref
     curr_pdesc typestate1 exp1
-    (typ1, InferredNullability.create_nonnull origin1)
+    (typ1, InferredNullability.create origin1)
     loc1
 
 
@@ -458,7 +458,7 @@ let do_preconditions_check_not_null instr_ref tenv find_canonical_duplicate node
             (Some instr_ref) loc curr_pdesc ) ;
         TypeState.add pvar
           (* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *)
-          (t, InferredNullability.create_nonnull TypeOrigin.OptimisticFallback)
+          (t, InferredNullability.create TypeOrigin.OptimisticFallback)
           typestate''
     | None ->
         typestate'
@@ -501,7 +501,7 @@ let do_preconditions_check_state instr_ref idenv tenv curr_pname curr_annotated_
     | Some (t, _) ->
         TypeState.add pvar
           (* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *)
-          (t, InferredNullability.create_nonnull TypeOrigin.OptimisticFallback)
+          (t, InferredNullability.create TypeOrigin.OptimisticFallback)
           typestate1
     | None ->
         typestate1
@@ -850,7 +850,7 @@ let calc_typestate_after_call find_canonical_duplicate calls_this checks tenv id
       typecheck_expr ~is_strict_mode find_canonical_duplicate calls_this checks tenv node instr_ref
         curr_pdesc typestate e2
         (* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *)
-        (t2, InferredNullability.create_nonnull TypeOrigin.OptimisticFallback)
+        (t2, InferredNullability.create TypeOrigin.OptimisticFallback)
         loc
     in
     let actual = (orig_e2, inferred_nullability_actual) in
@@ -872,10 +872,7 @@ let calc_typestate_after_call find_canonical_duplicate calls_this checks tenv id
         ; annotated_signature= callee_annotated_signature
         ; is_library }
     in
-    let ret_inferred_nullability =
+    (InferredNullability.create origin, ret.ret_annotated_type.typ)
-      InferredNullability.of_annotated_nullability ret.ret_annotated_type.nullability origin
-    in
-    (ret_inferred_nullability, ret.ret_annotated_type.typ)
   in
   let sig_len = List.length signature_params in
   let call_len = List.length call_params in
@@ -1069,7 +1066,7 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
   | Sil.Call ((id, _), Exp.Const (Const.Cfun pn), [(_, typ)], _, _)
     when Typ.Procname.equal pn BuiltinDecl.__new || Typ.Procname.equal pn BuiltinDecl.__new_array ->
       (* new never returns null *)
-      TypeState.add_id id (typ, InferredNullability.create_nonnull TypeOrigin.New) typestate
+      TypeState.add_id id (typ, InferredNullability.create TypeOrigin.New) typestate
   (* Type cast *)
   | Sil.Call ((id, _), Exp.Const (Const.Cfun pn), (e, typ) :: _, loc, _)
     when Typ.Procname.equal pn BuiltinDecl.__cast ->
@@ -1091,14 +1088,14 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
         typecheck_expr ~is_strict_mode find_canonical_duplicate calls_this checks tenv node
           instr_ref curr_pdesc typestate array_exp
           (* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *)
-          (t, InferredNullability.create_nonnull TypeOrigin.OptimisticFallback)
+          (t, InferredNullability.create TypeOrigin.OptimisticFallback)
           loc
       in
       if checks.eradicate then
         EradicateChecks.check_object_dereference ~is_strict_mode tenv find_canonical_duplicate
           curr_pdesc node instr_ref array_exp DereferenceRule.ArrayLengthAccess ta loc ;
       TypeState.add_id id
-        (Typ.mk (Tint Typ.IInt), InferredNullability.create_nonnull TypeOrigin.ArrayLengthResult)
+        (Typ.mk (Tint Typ.IInt), InferredNullability.create TypeOrigin.ArrayLengthResult)
         typestate
   (* All other builtins that are not considered above *)
   | Sil.Call (_, Exp.Const (Const.Cfun pn), _, _, _) when BuiltinDecl.is_declared pn ->

infer/src/nullsafe/typeOrigin.ml

@@ -32,6 +32,7 @@ type t =
 and field_origin =
   { object_origin: t  (** field's object origin (object is before field access operator `.`)  *)
   ; field_name: Typ.Fieldname.t
+  ; field_type: AnnotatedType.t
   ; access_loc: Location.t }
 
 and method_call_origin =
@@ -42,6 +43,24 @@ and method_call_origin =
 
 let equal = [%compare.equal: t]
 
+let get_nullability = function
+  | NullConst _ ->
+      Nullability.Nullable
+  | NonnullConst _
+  | This (* `this` can not be null according to Java rules *)
+  | New (* In Java `new` always create a non-null object  *)
+  | ArrayLengthResult (* integer hence non-nullable *)
+  | OptimisticFallback (* non-null is the most optimistic type *)
+  | Undef (* This is a very special case, assigning non-null is a technical trick *) ->
+      Nullability.Nonnull
+  | Field {field_type= {nullability}} ->
+      AnnotatedNullability.get_nullability nullability
+  | MethodParameter {param_annotated_type= {nullability}} ->
+      AnnotatedNullability.get_nullability nullability
+  | MethodCall {annotated_signature= {ret= {ret_annotated_type= {nullability}}}} ->
+      AnnotatedNullability.get_nullability nullability
+
+
 let rec to_string = function
   | NullConst _ ->
       "null"

infer/src/nullsafe/typeOrigin.mli

@@ -29,6 +29,7 @@ type t =
 and field_origin =
   { object_origin: t  (** field's object origin (object is before field access operator `.`)  *)
   ; field_name: Typ.Fieldname.t
+  ; field_type: AnnotatedType.t
   ; access_loc: Location.t }
 
 and method_call_origin =
@@ -39,6 +40,8 @@ and method_call_origin =
 
 val equal : t -> t -> bool
 
+val get_nullability : t -> Nullability.t
+
 val get_description : t -> TypeErr.origin_descr option
 (** Get a description to be used for error messages. *)