[nullsafe] Don't ever issue violation when dereferencing params.

Summary:
# Problem

Consider
```
some_method(Object a) { a.deref(); }
```

What is nullability of `a` when we dereference it?
Logically, things like "LocallyCheckedNonnull" etc are not applicable
here.

This would be applicable if we called some_method() outside! But not
inside. Inside the function, it can freely treat params as non-null, as
long they are declared as non-nullable.

The best we can capture it is via StrictNonnull nullability.

Reviewed By: artempyanykh

Differential Revision: D20536586

fbshipit-source-id: 5c2ba7f0d

infer/src/nullsafe/ErrorRenderingUtils.ml

@@ -45,13 +45,14 @@ let is_object_nullability_self_explanatory ~object_expression (object_origin : T
   | NullConst _ ->
       (* Expect either a local variable or null literal (latter case is trivial) *)
       String.equal object_expression "null"
-  | MethodParameter (Normal {mangled}) ->
+  | CurrMethodParameter (Normal {mangled}) ->
       (* Either local variable or literally parameter. In latter case, its nullability is
          self-explanatory because the user can quickly see the current method signature.
       *)
       let param_name = Mangled.to_string mangled in
       String.equal object_expression param_name
-  | MethodParameter ObjectEqualsOverride ->
+  | CurrMethodParameter ObjectEqualsOverride ->
+      (* This needs a dedicated explanation for the user *)
       false
   | Field {field_name} ->
       (* Either local variable or expression like `<smth>.field_name`. Latter case is trivial:

infer/src/nullsafe/eradicate.ml

@@ -40,8 +40,8 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct
           *)
           TypeOrigin.This
         else if PatternMatch.is_override_of_java_lang_object_equals curr_pname then
-          TypeOrigin.MethodParameter ObjectEqualsOverride
-        else TypeOrigin.MethodParameter (Normal param_signature)
+          TypeOrigin.CurrMethodParameter ObjectEqualsOverride
+        else TypeOrigin.CurrMethodParameter (Normal param_signature)
       in
       let inferred_nullability = InferredNullability.create origin in
       TypeState.add pvar

infer/src/nullsafe/typeErr.ml

@@ -198,7 +198,7 @@ let get_nonnull_explanation_for_condition_redudant (nonnull_origin : TypeOrigin.
   | NonnullConst _
   | Field _
   | CallToGetKnownToContainsKey
-  | MethodParameter _
+  | CurrMethodParameter _
   | This
   | New
   | ArrayAccess

infer/src/nullsafe/typeOrigin.ml

@@ -13,7 +13,7 @@ type t =
   | NullConst of Location.t
   | NonnullConst of Location.t
   | Field of field_origin
-  | MethodParameter of method_parameter_origin
+  | CurrMethodParameter of method_parameter_origin
   | This
   | MethodCall of method_call_origin
   | CallToGetKnownToContainsKey
@@ -59,9 +59,24 @@ let get_nullability = function
       Nullability.StrictNonnull
   | Field {field_type= {nullability}} ->
       AnnotatedNullability.get_nullability nullability
-  | MethodParameter (Normal {param_annotated_type= {nullability}}) ->
-      AnnotatedNullability.get_nullability nullability
-  | MethodParameter ObjectEqualsOverride ->
+  | CurrMethodParameter (Normal {param_annotated_type= {nullability}}) -> (
+    match nullability with
+    | AnnotatedNullability.Nullable _ ->
+        (* Annotated as Nullable explicitly or implicitly *)
+        Nullability.Nullable
+    | AnnotatedNullability.UncheckedNonnull _
+    | AnnotatedNullability.ThirdPartyNonnull
+    | AnnotatedNullability.LocallyCheckedNonnull
+    | AnnotatedNullability.StrictNonnull _ ->
+        (* Nonnull param should be treated as trusted inside this function context:
+           Things like dereferences or conversions should be allowed without any extra check
+           independendly of mode.
+           NOTE. However, in practice a function should be allowed to check any param for null
+           and be defensive, because no function can gurantee it won't ever be called with `null`, so
+           in theory we might want to distinct that in the future.
+        *)
+        Nullability.StrictNonnull )
+  | CurrMethodParameter ObjectEqualsOverride ->
       (* `Object.equals(obj)` should expect to be called with null `obj` *)
       Nullability.Nullable
   | MethodCall {annotated_signature= {ret= {ret_annotated_type= {nullability}}}} ->
@@ -75,10 +90,10 @@ let rec to_string = function
       "Const (nonnull)"
   | Field {object_origin; field_name} ->
       "Field " ^ Fieldname.to_string field_name ^ " (object: " ^ to_string object_origin ^ ")"
-  | MethodParameter (Normal {mangled; param_annotated_type= {nullability}}) ->
+  | CurrMethodParameter (Normal {mangled; param_annotated_type= {nullability}}) ->
       Format.asprintf "Param %s <%a>" (Mangled.to_string mangled) AnnotatedNullability.pp
         nullability
-  | MethodParameter ObjectEqualsOverride ->
+  | CurrMethodParameter ObjectEqualsOverride ->
       "Param(ObjectEqualsOverride)"
   | This ->
       "this"
@@ -144,9 +159,9 @@ let get_description origin =
       Some ("null constant" ^ atline loc)
   | Field {field_name; access_loc} ->
       Some ("field " ^ Fieldname.get_field_name field_name ^ atline access_loc)
-  | MethodParameter (Normal {mangled}) ->
+  | CurrMethodParameter (Normal {mangled}) ->
       Some ("method parameter " ^ Mangled.to_string mangled)
-  | MethodParameter ObjectEqualsOverride ->
+  | CurrMethodParameter ObjectEqualsOverride ->
       Some "Object.equals() should be able to accept `null`, according to the Java specification"
   | MethodCall {pname; call_loc; annotated_signature} ->
       Some (get_method_ret_description pname call_loc annotated_signature)
@@ -171,7 +186,7 @@ let get_description origin =
 
 let join o1 o2 =
   match (o1, o2) with
-  | Field _, (NullConst _ | NonnullConst _ | MethodParameter _ | This | MethodCall _ | New) ->
+  | Field _, (NullConst _ | NonnullConst _ | CurrMethodParameter _ | This | MethodCall _ | New) ->
       (* low priority to Field, to support field initialization patterns *)
       o2
   | _ ->

infer/src/nullsafe/typeOrigin.mli

@@ -11,7 +11,8 @@ type t =
   | NullConst of Location.t  (** A null literal in the source *)
   | NonnullConst of Location.t  (** A constant (not equal to null) in the source. *)
   | Field of field_origin  (** A field access (result of expression `some_object.some_field`) *)
-  | MethodParameter of method_parameter_origin  (** A method's parameter *)
+  | CurrMethodParameter of method_parameter_origin
+      (** Parameter of a method we are currently in, *)
   | This (* `this` object. Can not be null, according to Java rules. *)
   | MethodCall of method_call_origin  (** A result of a method call *)
   | CallToGetKnownToContainsKey

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

@@ -198,7 +198,7 @@ codetoanalyze/java/nullsafe-default/NullMethodCall.java, Linters_dummy_method, 1
 codetoanalyze/java/nullsafe-default/NullMethodCall.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_IS_CLEAN, no_bucket, INFO, []
 codetoanalyze/java/nullsafe-default/NullMethodCall.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_IS_CLEAN, no_bucket, INFO, []
 codetoanalyze/java/nullsafe-default/NullMethodCall.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_IS_CLEAN, no_bucket, INFO, []
-codetoanalyze/java/nullsafe-default/NullMethodCall.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_NEEDS_FIXING, no_bucket, INFO, []
+codetoanalyze/java/nullsafe-default/NullMethodCall.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_IS_CLEAN, no_bucket, INFO, []
 codetoanalyze/java/nullsafe-default/NullMethodCall.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_NEEDS_FIXING, no_bucket, INFO, []
 codetoanalyze/java/nullsafe-default/NullMethodCall.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_NEEDS_FIXING, no_bucket, INFO, []
 codetoanalyze/java/nullsafe-default/NullMethodCall.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_NEEDS_FIXING, no_bucket, INFO, []
@@ -229,7 +229,7 @@ codetoanalyze/java/nullsafe-default/NullMethodCall.java, codetoanalyze.java.null
 codetoanalyze/java/nullsafe-default/NullsafeMode.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_IS_CLEAN, no_bucket, INFO, []
 codetoanalyze/java/nullsafe-default/NullsafeMode.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_IS_CLEAN, no_bucket, INFO, []
 codetoanalyze/java/nullsafe-default/NullsafeMode.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_IS_CLEAN, no_bucket, INFO, []
-codetoanalyze/java/nullsafe-default/NullsafeMode.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_NEEDS_FIXING, no_bucket, INFO, []
+codetoanalyze/java/nullsafe-default/NullsafeMode.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_IS_CLEAN, no_bucket, INFO, []
 codetoanalyze/java/nullsafe-default/NullsafeMode.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_NEEDS_FIXING, no_bucket, INFO, []
 codetoanalyze/java/nullsafe-default/NullsafeMode.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_NEEDS_FIXING, no_bucket, INFO, []
 codetoanalyze/java/nullsafe-default/NullsafeMode.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_NEEDS_FIXING, no_bucket, INFO, []
@@ -372,7 +372,7 @@ codetoanalyze/java/nullsafe-default/TrueFalseOnNull.java, Linters_dummy_method,
 codetoanalyze/java/nullsafe-default/TrueFalseOnNull.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_IS_CLEAN, no_bucket, INFO, []
 codetoanalyze/java/nullsafe-default/TrueFalseOnNull.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_IS_CLEAN, no_bucket, INFO, []
 codetoanalyze/java/nullsafe-default/TrueFalseOnNull.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_IS_CLEAN, no_bucket, INFO, []
-codetoanalyze/java/nullsafe-default/TrueFalseOnNull.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_NEEDS_FIXING, no_bucket, INFO, []
+codetoanalyze/java/nullsafe-default/TrueFalseOnNull.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_IS_CLEAN, no_bucket, INFO, []
 codetoanalyze/java/nullsafe-default/TrueFalseOnNull.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_NEEDS_FIXING, no_bucket, INFO, []
 codetoanalyze/java/nullsafe-default/TrueFalseOnNull.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_NEEDS_FIXING, no_bucket, INFO, []
 codetoanalyze/java/nullsafe-default/TrueFalseOnNull.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_NEEDS_FIXING, no_bucket, INFO, []