[kotlin] Add argument index to NULL_ARGUMENT issue type error message

Summary: Improve NULL_ARGUMENT issue type error messages by adding additional information about argument index.

Reviewed By: dulmarod

Differential Revision:
D50969238

Privacy Context Container: L1122176

fbshipit-source-id: c3ed9561ecc5557fa3396ba8b3c0bd697c537066

infer/src/pulse/PulseAbductiveDomain.ml

@@ -1451,9 +1451,18 @@ let get_post {post} = (post :> BaseDomain.t)
 let update_pre_for_kotlin_proc astate (proc_attrs : ProcAttributes.t) formals =
   let proc_name = proc_attrs.proc_name in
   let location = proc_attrs.loc in
+  (* Drop this reference to make sure that formals' indices are always zero based
+     for consistent error reporting *)
+  let formals =
+    match formals with
+    | _ :: tail ->
+        if Procname.is_java_instance_method proc_name then tail else formals
+    | [] ->
+        []
+  in
   (* Kotlin procs are Java procs under the hood *)
   if Procname.is_java proc_name then
-    List.fold formals ~init:astate ~f:(fun (acc : t) (var, _, annot_opt, (_, history)) ->
+    List.foldi formals ~init:astate ~f:(fun index (acc : t) (var, _, annot_opt, (_, history)) ->
         (* We're interested specifically in org.jetbrains.annotations.NotNull since this annotation
            is emitted by kotlinc to denote non-nullable function parameters *)
         let is_not_nullable = Option.exists annot_opt ~f:Annotations.ia_is_jetbrains_notnull in
@@ -1464,7 +1473,7 @@ let update_pre_for_kotlin_proc astate (proc_attrs : ProcAttributes.t) formals =
             Attribute.MustBeValid
               ( Timestamp.t0
               , Trace.Immediate {location; history}
-              , Some (NullArgumentWhereNonNullExpected (CallEvent.Call proc_name)) )
+              , Some (NullArgumentWhereNonNullExpected (CallEvent.Call proc_name, Some index)) )
           in
           let new_pre =
             PreDomain.update acc.pre

infer/src/pulse/PulseDiagnostic.ml

@@ -473,7 +473,7 @@ let get_message_and_suggestion diagnostic =
              | Some BlockCall ->
                  F.fprintf fmt "%a is called%a, causing a crash" pp_prefix "nil block"
                    pp_access_trace access_trace
-             | Some (NullArgumentWhereNonNullExpected call_event) ->
+             | Some (NullArgumentWhereNonNullExpected (call_event, index)) ->
                  let {Location.file} = Trace.get_outer_location invalidation_trace in
                  let null =
                    match call_event with
@@ -488,7 +488,8 @@ let get_message_and_suggestion diagnostic =
                  in
                  F.fprintf fmt
                    "%a is passed as argument to %a; this function requires a non-%s argument"
-                   pp_prefix null CallEvent.pp call_event null
+                   pp_prefix null CallEvent.pp call_event null ;
+                 Option.iter index ~f:(fun index -> F.fprintf fmt " at position #%i" index)
              | None ->
                  F.fprintf fmt "%a is dereferenced%a" pp_prefix "null" pp_access_trace access_trace
            in

infer/src/pulse/PulseInvalidation.ml

@@ -104,7 +104,7 @@ type must_be_valid_reason =
   | InsertionIntoCollectionKey
   | InsertionIntoCollectionValue
   | SelfOfNonPODReturnMethod of Typ.t
-  | NullArgumentWhereNonNullExpected of PulseCallEvent.t
+  | NullArgumentWhereNonNullExpected of PulseCallEvent.t * int option
 [@@deriving compare, equal]
 
 let pp_must_be_valid_reason f = function

infer/src/pulse/PulseInvalidation.mli

@@ -60,7 +60,7 @@ type must_be_valid_reason =
   | InsertionIntoCollectionKey
   | InsertionIntoCollectionValue
   | SelfOfNonPODReturnMethod of Typ.t
-  | NullArgumentWhereNonNullExpected of PulseCallEvent.t
+  | NullArgumentWhereNonNullExpected of PulseCallEvent.t * int option
 [@@deriving compare, equal]
 
 val pp_must_be_valid_reason : F.formatter -> must_be_valid_reason option -> unit

infer/src/pulse/PulseModelsObjC.ml

@@ -246,7 +246,8 @@ let check_arg_not_nil (value, value_hist) ~desc : model =
   let event = Hist.call_event path location desc in
   let<*> astate, _ =
     PulseOperations.eval_access path
-      ~must_be_valid_reason:(NullArgumentWhereNonNullExpected (CallEvent.Model desc)) Read location
+      ~must_be_valid_reason:(NullArgumentWhereNonNullExpected (CallEvent.Model desc, None))
+      Read location
       (value, Hist.add_event path event value_hist)
       Dereference astate
   in

infer/tests/build_systems/pulse_messages_kotlin/issues.exp

@@ -1,4 +1,4 @@
-build_systems/pulse_messages_kotlin/BasicJavaKotlinBoundary.java, codetoanalyze.kotlin.pulse.BasicJavaKotlinBoundary.passNullWhenDisallowedBad1(codetoanalyze.kotlin.pulse.Kotlin):void, 21, -1, ERROR, NULL_ARGUMENT, `input` could be null (null value originating from line 20) and is passed as argument to `void Kotlin.doesNotAcceptNullFirstParam(Object)`; this function requires a non-null argument., 
-build_systems/pulse_messages_kotlin/BasicJavaKotlinBoundary.java, codetoanalyze.kotlin.pulse.BasicJavaKotlinBoundary.passNullWhenDisallowedBad2(codetoanalyze.kotlin.pulse.Kotlin):void, 33, -1, ERROR, NULL_ARGUMENT, `input2` could be null (null value originating from line 32) and is passed as argument to `void Kotlin.doesNotAcceptNullSecondParam(Object,Object)`; this function requires a non-null argument., 
-build_systems/pulse_messages_kotlin/BasicJavaKotlinBoundary.java, codetoanalyze.kotlin.pulse.BasicJavaKotlinBoundary.passNullWhenDisallowedInterprocBad1(codetoanalyze.kotlin.pulse.Kotlin):void, 38, -1, ERROR, NULL_ARGUMENT, `input` could be null (from the call to `BasicJavaKotlinBoundary.returnsNull()` on line 37) and is passed as argument to `void Kotlin.doesNotAcceptNullFirstParam(Object)`; this function requires a non-null argument., 
-build_systems/pulse_messages_kotlin/BasicJavaKotlinBoundary.java, codetoanalyze.kotlin.pulse.BasicJavaKotlinBoundary.passNullWhenDisallowedInterprocBad2(codetoanalyze.kotlin.pulse.Kotlin):void, 50, -1, ERROR, NULL_ARGUMENT, `input2` could be null (from the call to `BasicJavaKotlinBoundary.returnsNull()` on line 49) and is passed as argument to `void Kotlin.doesNotAcceptNullSecondParam(Object,Object)`; this function requires a non-null argument., 
+build_systems/pulse_messages_kotlin/BasicJavaKotlinBoundary.java, codetoanalyze.kotlin.pulse.BasicJavaKotlinBoundary.passNullWhenDisallowedBad1(codetoanalyze.kotlin.pulse.Kotlin):void, 21, -1, ERROR, NULL_ARGUMENT, `input` could be null (null value originating from line 20) and is passed as argument to `void Kotlin.doesNotAcceptNullFirstParam(Object)`; this function requires a non-null argument at position #0., 
+build_systems/pulse_messages_kotlin/BasicJavaKotlinBoundary.java, codetoanalyze.kotlin.pulse.BasicJavaKotlinBoundary.passNullWhenDisallowedBad2(codetoanalyze.kotlin.pulse.Kotlin):void, 33, -1, ERROR, NULL_ARGUMENT, `input2` could be null (null value originating from line 32) and is passed as argument to `void Kotlin.doesNotAcceptNullSecondParam(Object,Object)`; this function requires a non-null argument at position #1., 
+build_systems/pulse_messages_kotlin/BasicJavaKotlinBoundary.java, codetoanalyze.kotlin.pulse.BasicJavaKotlinBoundary.passNullWhenDisallowedInterprocBad1(codetoanalyze.kotlin.pulse.Kotlin):void, 38, -1, ERROR, NULL_ARGUMENT, `input` could be null (from the call to `BasicJavaKotlinBoundary.returnsNull()` on line 37) and is passed as argument to `void Kotlin.doesNotAcceptNullFirstParam(Object)`; this function requires a non-null argument at position #0., 
+build_systems/pulse_messages_kotlin/BasicJavaKotlinBoundary.java, codetoanalyze.kotlin.pulse.BasicJavaKotlinBoundary.passNullWhenDisallowedInterprocBad2(codetoanalyze.kotlin.pulse.Kotlin):void, 50, -1, ERROR, NULL_ARGUMENT, `input2` could be null (from the call to `BasicJavaKotlinBoundary.returnsNull()` on line 49) and is passed as argument to `void Kotlin.doesNotAcceptNullSecondParam(Object,Object)`; this function requires a non-null argument at position #1.,