[nullsafe] When inferring type based on the formal type, respect NullsafeType instead of reading annotations

Summary:
This continues work for eliminating Annot.Item.t from Nullsafe low-level
code.

The introduced function `from_nullsafe_type` is called when we infer
initial type of the equation based on the function or field formal signature.

Before that, we did it via reading the annotation directly, which
complicates the logic and making introducing Unknown nullability tricky.

## Clarifying the semantics of PropagatesNullable

This diff also clarifies (and changes) the behavior of PropagatesNullable params.

Previously, if the return value of a function that has PropagatesNullable params was
annotated as Nullable, nullsafe was effectively ignoring PropagatesNullable effect.

This is especially bad because one can add Nullable annotation based on the logic "if the function can return `null`, it should be annotated with Nullable`.

In the new design, there is no possibility for such a misuse: the code that
applies the rule "any param is PropagatesNullable hence the return
value is nullable even if not explicitly annotated" lives in NullsafeType.ml, so
this will be automatically taken into account.

Meaning that now we implicitly deduce Nullable annotation for the return value, and providing it explicitly as an alternative that does not change the effect.

In the future, we might consider annotating the return value with `Nullable` explicit.

Reviewed By: jvillard

Differential Revision: D17479157

fbshipit-source-id: 66c2c8777

infer/src/nullsafe/eradicate.ml

@@ -36,7 +36,7 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct
       let pvar = Pvar.mk param_signature.mangled curr_pname in
       let ta =
         let origin = TypeOrigin.Formal param_signature.mangled in
-        TypeAnnotation.from_item_annotation param_signature.param_annotation_deprecated origin
+        TypeAnnotation.from_nullsafe_type param_signature.param_nullsafe_type origin
       in
       TypeState.add pvar (param_signature.param_nullsafe_type.typ, ta, []) typestate
     in

infer/src/nullsafe/eradicateChecks.ml

@@ -326,7 +326,7 @@ type resolved_param =
   { num: int
   ; formal: Mangled.t * TypeAnnotation.t * Typ.t
   ; actual: Exp.t * TypeAnnotation.t
-  ; propagates_nullable: bool }
+  ; is_formal_propagates_nullable: bool }
 
 (** Check the parameters of a call. *)
 let check_call_parameters tenv find_canonical_duplicate curr_pdesc node callee_attributes

infer/src/nullsafe/typeAnnotation.ml

@@ -54,4 +54,9 @@ let const_nullable is_nullable origin = {origin; is_nullable}
 
 let with_origin ta o = {ta with origin= o}
 
-let from_item_annotation ia origin = const_nullable (Annotations.ia_is_nullable ia) origin
+let from_nullsafe_type NullsafeType.{nullability} origin =
+  match nullability with
+  | Nullable _ ->
+      {origin; is_nullable= true}
+  | Nonnull _ ->
+      {origin; is_nullable= false}

infer/src/nullsafe/typeAnnotation.mli

@@ -16,7 +16,7 @@ val const_nullable : bool -> TypeOrigin.t -> t
 val descr_origin : t -> TypeErr.origin_descr
 (** Human-readable description of the origin of a nullable value. *)
 
-val from_item_annotation : Annot.Item.t -> TypeOrigin.t -> t
+val from_nullsafe_type : NullsafeType.t -> TypeOrigin.t -> t
 
 val get_origin : t -> TypeOrigin.t
 

infer/src/nullsafe/typeCheck.ml

@@ -146,9 +146,9 @@ let rec typecheck_expr find_canonical_duplicate visited checks tenv node instr_r
       let exp_origin = TypeAnnotation.get_origin ta in
       let tr_new =
         match EradicateChecks.get_field_annotation tenv fn typ with
-        | Some EradicateChecks.{nullsafe_type; annotation_deprecated} ->
+        | Some EradicateChecks.{nullsafe_type} ->
             ( nullsafe_type.typ
-            , TypeAnnotation.from_item_annotation annotation_deprecated
+            , TypeAnnotation.from_nullsafe_type nullsafe_type
                 (TypeOrigin.Field (exp_origin, fn, loc))
             , locs' )
         | None ->
@@ -226,10 +226,10 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
           typestate
       | _ -> (
         match EradicateChecks.get_field_annotation tenv fn typ with
-        | Some EradicateChecks.{nullsafe_type; annotation_deprecated} ->
+        | Some EradicateChecks.{nullsafe_type} ->
             let range =
               ( nullsafe_type.typ
-              , TypeAnnotation.from_item_annotation annotation_deprecated
+              , TypeAnnotation.from_nullsafe_type nullsafe_type
                   (TypeOrigin.Field (origin, fn, loc))
               , [loc] )
             in
@@ -533,7 +533,7 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
       let is_anonymous_inner_class_constructor =
         Typ.Procname.Java.is_anonymous_inner_class_constructor callee_pname_java
       in
-      let do_return (ret_ta, NullsafeType.{typ= ret_typ}) loc' typestate' =
+      let do_return (ret_ta, ret_typ) loc' typestate' =
         let mk_return_range () = (ret_typ, ret_ta, [loc']) in
         let id = fst ret_id_typ in
         TypeState.add_id id (mk_return_range ()) typestate'
@@ -682,15 +682,14 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
         | _ ->
             typestate'
       in
-      let typestate_after_call, resolved_ret =
+      let typestate_after_call, finally_resolved_ret =
         let resolve_param i (sparam, cparam) =
           let AnnotatedSignature.{mangled; param_annotation_deprecated; param_nullsafe_type} =
             sparam
           in
           let (orig_e2, e2), t2 = cparam in
           let ta1 =
-            TypeAnnotation.from_item_annotation param_annotation_deprecated
-              (TypeOrigin.Formal mangled)
+            TypeAnnotation.from_nullsafe_type param_nullsafe_type (TypeOrigin.Formal mangled)
           in
           let _, ta2, _ =
             typecheck_expr find_canonical_duplicate calls_this checks tenv node instr_ref
@@ -701,39 +700,37 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
           let formal = (mangled, ta1, param_nullsafe_type.typ) in
           let actual = (orig_e2, ta2) in
           let num = i + 1 in
-          let formal_is_propagates_nullable =
+          let is_formal_propagates_nullable =
             Annotations.ia_is_propagates_nullable param_annotation_deprecated
           in
-          let actual_is_nullable = TypeAnnotation.is_nullable ta2 in
-          let propagates_nullable = formal_is_propagates_nullable && actual_is_nullable in
-          EradicateChecks.{num; formal; actual; propagates_nullable}
+          EradicateChecks.{num; formal; actual; is_formal_propagates_nullable}
         in
-        (* Apply a function that operates on annotations *)
-        let apply_annotation_transformer resolved_ret
+        (* If the function has @PropagatesNullable params, and inferred type for each of
+           corresponding actual param is non-nullable, inferred type for the whole result
+           can be strengthened to non-nullable as well.
+         *)
+        let clarify_ret_by_propagates_nullable ret
             (resolved_params : EradicateChecks.resolved_param list) =
-          let rec handle_params resolved_ret params =
-            match (params : EradicateChecks.resolved_param list) with
-            | param :: params' when param.propagates_nullable ->
-                let _, actual_ta = param.actual in
-                let resolved_ret' =
-                  let ret_ta, ret_typ = resolved_ret in
-                  let ret_ta' =
-                    let is_actual_nullable = TypeAnnotation.is_nullable actual_ta in
-                    let is_old_nullable = TypeAnnotation.is_nullable ret_ta in
-                    let is_new_nullable = is_old_nullable || is_actual_nullable in
-                    TypeAnnotation.set_nullable is_new_nullable ret_ta
-                  in
-                  (ret_ta', ret_typ)
-                in
-                handle_params resolved_ret' params'
-            | _ :: params' ->
-                handle_params resolved_ret params'
-            | [] ->
-                resolved_ret
+          let propagates_nullable_params =
+            List.filter resolved_params ~f:(fun (param : EradicateChecks.resolved_param) ->
+                param.is_formal_propagates_nullable )
           in
-          handle_params resolved_ret resolved_params
+          if List.is_empty propagates_nullable_params then ret
+          else if
+            List.for_all propagates_nullable_params
+              ~f:(fun EradicateChecks.{actual= _, inferred_nullability_actual} ->
+                not (TypeAnnotation.is_nullable inferred_nullability_actual) )
+          then
+            (* All params' inferred types are non-nullable.
+              Strengten the result to be non-nullable as well! *)
+            let ret_type_annotation, ret_typ = ret in
+            (TypeAnnotation.set_nullable false ret_type_annotation, ret_typ)
+          else
+            (* At least one param's inferred type is nullable, can not strengthen the result *)
+            ret
         in
-        let resolved_ret_ =
+        (* Infer nullability of function call result based on its signature *)
+        let preliminary_resolved_ret =
           let ret = callee_annotated_signature.AnnotatedSignature.ret in
           let is_library = Summary.OnDisk.proc_is_library callee_attributes in
           let origin =
@@ -743,8 +740,8 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
               ; annotated_signature= callee_annotated_signature
               ; is_library }
           in
-          let ret_ta = TypeAnnotation.from_item_annotation ret.ret_annotation_deprecated origin in
-          (ret_ta, ret.ret_nullsafe_type)
+          let ret_ta = TypeAnnotation.from_nullsafe_type ret.ret_nullsafe_type origin in
+          (ret_ta, ret.ret_nullsafe_type.typ)
         in
         let sig_len = List.length signature_params in
         let call_len = List.length call_params in
@@ -766,7 +763,11 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
             (List.zip_exn sig_slice call_slice)
         in
         let resolved_params = List.mapi ~f:resolve_param sig_call_params in
-        let resolved_ret = apply_annotation_transformer resolved_ret_ resolved_params in
+        (* Clarify function call result nullability based on params annotated with @PropagatesNullable
+           and inferred nullability of those params *)
+        let ret_respecting_propagates_nullable =
+          clarify_ret_by_propagates_nullable preliminary_resolved_ret resolved_params
+        in
         let typestate_after_call =
           if not is_anonymous_inner_class_constructor then (
             if cflags.CallFlags.cf_virtual && checks.eradicate then
@@ -792,9 +793,9 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
             else typestate1 )
           else typestate1
         in
-        (typestate_after_call, resolved_ret)
+        (typestate_after_call, ret_respecting_propagates_nullable)
       in
-      do_return resolved_ret loc typestate_after_call
+      do_return finally_resolved_ret loc typestate_after_call
   | Sil.Call _ ->
       typestate
   | Sil.Prune (cond, loc, true_branch, _) ->

infer/tests/codetoanalyze/java/nullsafe-default/CustomAnnotations.java

@@ -197,6 +197,53 @@ public class CustomAnnotations {
         propagatesNullable(sNonnull, sNonnull).length(); // OK: result can be null
       }
     }
+
+    // For convenience, we do not require to annotate return type with @Nullable,
+    // make sure it is respected.
+    class TestReturnValueAnnotationIsAutomaticallyInferred {
+
+      // Ensure that we do not warn with "return not nullable" even if we did not annotate the
+      // return with @Nullable
+
+      String notAnnotatingReturnWhenThereIsPropagatesNullableIsOK(@PropagatesNullable String s) {
+        return null; // OK: treat is as implicitly nullable
+      }
+
+      String notAnnotatingReturnWhenThereAreNoPropagatesNullableIsBAD(@Nullable String s) {
+        return null; // BAD: return not nullable
+      }
+
+      // Ensure that the behavior remains the same for explicitly and implicitly annotated functions
+
+      @Nullable
+      String annotatedReturn(@PropagatesNullable String s) {
+        return s;
+      }
+
+      String notAnnotatedReturn(@PropagatesNullable String s) {
+        return s;
+      }
+
+      // 1. Both versions equally catch non-legit usages
+
+      void annotated_dereferencingAfterPassingNullableIsBAD(@Nullable String s) {
+        annotatedReturn(s).toString(); // BAD: nullable dereference
+      }
+
+      void notAnnotated_dereferencingAfterPassingNullableIsBAD(@Nullable String s) {
+        notAnnotatedReturn(s).toString(); // BAD: nullable dereference
+      }
+
+      // 2. Both versions equally allow legit usages
+
+      void annotated_dereferencingAfterPassingNonnullIsOK(String s) {
+        annotatedReturn(s).toString(); // OK: inferred to be non-nullable
+      }
+
+      void notAnnotated_dereferencingAfterPassingNonnullIsOK(String s) {
+        notAnnotatedReturn(s).toString(); // OK: inferred to be non-nullable
+      }
+    }
   }
 
 }

infer/tests/codetoanalyze/java/nullsafe-default/issues.exp

@@ -43,6 +43,9 @@ codetoanalyze/java/nullsafe-default/CustomAnnotations.java, codetoanalyze.java.n
 codetoanalyze/java/nullsafe-default/CustomAnnotations.java, codetoanalyze.java.nullsafe_default.CustomAnnotations$TestPropagatesNullable$TestOneParameter.test(java.lang.String,java.lang.String):void, 15, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, WARNING, [The value of `nullable(...)` in the call to `length()` is nullable and is not locally checked for null. (Origin: call to nullable(...) at line 133)]
 codetoanalyze/java/nullsafe-default/CustomAnnotations.java, codetoanalyze.java.nullsafe_default.CustomAnnotations$TestPropagatesNullable$TestOneParameter.test(java.lang.String,java.lang.String):void, 21, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, WARNING, [The value of `propagatesNullable(...)` in the call to `length()` is nullable and is not locally checked for null. (Origin: call to propagatesNullable(...) at line 124)]
 codetoanalyze/java/nullsafe-default/CustomAnnotations.java, codetoanalyze.java.nullsafe_default.CustomAnnotations$TestPropagatesNullable$TestOneParameter.test(java.lang.String,java.lang.String):void, 22, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, WARNING, [The value of `nullable(...)` in the call to `length()` is nullable and is not locally checked for null. (Origin: call to nullable(...) at line 125)]
+codetoanalyze/java/nullsafe-default/CustomAnnotations.java, codetoanalyze.java.nullsafe_default.CustomAnnotations$TestPropagatesNullable$TestReturnValueAnnotationIsAutomaticallyInferred.annotated_dereferencingAfterPassingNullableIsBAD(java.lang.String):void, 1, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, WARNING, [The value of `annotatedReturn(...)` in the call to `toString()` is nullable and is not locally checked for null. (Origin: call to annotatedReturn(...) at line 230)]
+codetoanalyze/java/nullsafe-default/CustomAnnotations.java, codetoanalyze.java.nullsafe_default.CustomAnnotations$TestPropagatesNullable$TestReturnValueAnnotationIsAutomaticallyInferred.notAnnotated_dereferencingAfterPassingNullableIsBAD(java.lang.String):void, 1, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, WARNING, [The value of `notAnnotatedReturn(...)` in the call to `toString()` is nullable and is not locally checked for null. (Origin: call to notAnnotatedReturn(...) at line 234)]
+codetoanalyze/java/nullsafe-default/CustomAnnotations.java, codetoanalyze.java.nullsafe_default.CustomAnnotations$TestPropagatesNullable$TestReturnValueAnnotationIsAutomaticallyInferred.notAnnotatingReturnWhenThereAreNoPropagatesNullableIsBAD(java.lang.String):java.lang.String, 0, ERADICATE_RETURN_NOT_NULLABLE, no_bucket, WARNING, [Method `notAnnotatingReturnWhenThereAreNoPropagatesNullableIsBAD(...)` may return null but it is not annotated with `@Nullable`. (Origin: null constant at line 213)]
 codetoanalyze/java/nullsafe-default/CustomAnnotations.java, codetoanalyze.java.nullsafe_default.CustomAnnotations$TestPropagatesNullable$TestSecondParameter.test(java.lang.String,java.lang.String):void, 2, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, WARNING, [The value of `propagatesNullable(...)` in the call to `length()` is nullable and is not locally checked for null. (Origin: call to propagatesNullable(...) at line 169)]
 codetoanalyze/java/nullsafe-default/CustomAnnotations.java, codetoanalyze.java.nullsafe_default.CustomAnnotations$TestPropagatesNullable$TestSecondParameter.test(java.lang.String,java.lang.String):void, 3, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, WARNING, [The value of `nullable(...)` in the call to `length()` is nullable and is not locally checked for null. (Origin: call to nullable(...) at line 170)]
 codetoanalyze/java/nullsafe-default/CustomAnnotations.java, codetoanalyze.java.nullsafe_default.CustomAnnotations$TestPropagatesNullable$TestSecondParameter.test(java.lang.String,java.lang.String):void, 6, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, WARNING, [The value of `propagatesNullable(...)` in the call to `length()` is nullable and is not locally checked for null. (Origin: call to propagatesNullable(...) at line 173)]