[nullsafe] Split TypeOrigin.Formal into MethodParam and This

Summary:
This diff is a part of work teaching Nullsafe to explain decisions it's
making.

1. `Formal` was bit cryptic name.
2. Splitting method param and this makes a lot of sense. It is almost an
implementation detail that hey happen to come from "param" in the
method's signature.
3. Apart from others, this diff fixes a minor bug - we used to treat
this as DeclaredNonnull, which (in future) means suppressing legit warnings
like condition redundant. This would be an issue if we were to start
showing "high confidence" condition redundant warnings.

Reviewed By: ngorogiannis

Differential Revision: D18451294

fbshipit-source-id: acc295e3f

infer/src/nullsafe/eradicate.ml

@@ -35,7 +35,14 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct
     let add_formal typestate (param_signature : AnnotatedSignature.param_signature) =
       let pvar = Pvar.mk param_signature.mangled curr_pname in
       let inferred_nullability =
-        let origin = TypeOrigin.Formal param_signature.mangled in
+        let formal_name = param_signature.mangled in
+        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
+        else
+          let origin = TypeOrigin.MethodParameter param_signature in
           InferredNullability.of_annotated_nullability
             param_signature.param_annotated_type.nullability origin
       in

infer/src/nullsafe/eradicateChecks.ml

@@ -255,10 +255,9 @@ let check_constructor_initialization tenv find_canonical_duplicate curr_construc
                 | TypeOrigin.Undef ->
                     (* Special case: not really an initialization *)
                     false
-                | TypeOrigin.Field {object_origin= TypeOrigin.Formal name} ->
-                    (* Exclude circular initialization *)
-                    let circular = Mangled.is_this name in
-                    not circular
+                | TypeOrigin.Field {object_origin= TypeOrigin.This} ->
+                    (* Circular initialization - does not count *)
+                    false
                 | _ ->
                     (* Found in typestate, hence the field was initialized *)
                     true

infer/src/nullsafe/typeCheck.ml

@@ -194,8 +194,8 @@ let handle_field_access_via_temporary idenv curr_pname typestate exp =
     match Idenv.expand_expr idenv e with
     | Exp.Lvar pvar when name_is_temporary (Pvar.to_string pvar) -> (
       match pvar_get_origin pvar with
-      | Some (TypeOrigin.Formal s) ->
-          let pvar' = Pvar.mk s curr_pname in
+      | Some TypeOrigin.This ->
+          let pvar' = Pvar.mk Mangled.this curr_pname in
           Some (Exp.Lvar pvar')
       | _ ->
           None )

infer/src/nullsafe/typeOrigin.ml

@@ -13,7 +13,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`) *)
-  | Formal of Mangled.t  (** A formal parameter *)
+  | MethodParameter of AnnotatedSignature.param_signature  (** A method's parameter *)
+  | This (* `this` object. Can not be null, according to Java rules. *)
   | MethodCall of method_call_origin  (** A result of a method call *)
   | New  (** A new object creation *)
   | ArrayLengthResult  (** integer value - result of accessing array.length *)
@@ -43,8 +44,11 @@ let rec to_string = function
       "Field "
       ^ Typ.Fieldname.to_simplified_string field_name
       ^ " (object: " ^ to_string object_origin ^ ")"
-  | Formal s ->
-      "Formal " ^ Mangled.to_string s
+  | MethodParameter {mangled; param_annotated_type= {nullability}} ->
+      Format.asprintf "Param %s <%a>" (Mangled.to_string mangled) AnnotatedNullability.pp
+        nullability
+  | This ->
+      "this"
   | MethodCall {pname} ->
       Printf.sprintf "Fun %s" (Typ.Procname.to_simplified_string pname)
   | New ->
@@ -67,8 +71,8 @@ let get_description origin =
         ( "field " ^ Typ.Fieldname.to_simplified_string field_name ^ atline access_loc
         , Some access_loc
         , None )
-  | Formal s ->
-      Some ("method parameter " ^ Mangled.to_string s, None, None)
+  | MethodParameter {mangled} ->
+      Some ("method parameter " ^ Mangled.to_string mangled, None, None)
   | MethodCall {pname; call_loc; annotated_signature} ->
       let modelled_in =
         (* TODO(T54088319) don't calculate this info and propagate it from AnnotatedNullability instead *)
@@ -88,7 +92,7 @@ let get_description origin =
      But for these issues we currently don't print origins in the error string.
      It is a good idea to change this and start printing origins for these origins as well.
   *)
-  | New | NonnullConst _ | ArrayLengthResult ->
+  | This | New | NonnullConst _ | ArrayLengthResult ->
       None
   (* Two special cases - should not really occur in normal code *)
   | ONone | Undef ->
@@ -100,7 +104,7 @@ let join o1 o2 =
   (* left priority *)
   | Undef, _ | _, Undef ->
       Undef
-  | Field _, (NullConst _ | NonnullConst _ | Formal _ | MethodCall _ | New) ->
+  | Field _, (NullConst _ | NonnullConst _ | MethodParameter _ | 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`) *)
-  | Formal of Mangled.t  (** A formal parameter *)
+  | MethodParameter of AnnotatedSignature.param_signature  (** A method's parameter *)
+  | This (* `this` object. Can not be null, according to Java rules. *)
   | MethodCall of method_call_origin  (** A result of a method call *)
   | New  (** A new object creation *)
   | ArrayLengthResult  (** integer value - result of accessing array.length *)