[pulse][nullptr][objc] Include non-pod return type to improve error messages for non-pod issues

Reviewed By: skcho

Differential Revision: D28934494

fbshipit-source-id: 4ab438c79

infer/src/IR/Procdesc.ml

@@ -545,6 +545,16 @@ let get_ret_var pdesc = Pvar.get_ret_pvar (get_proc_name pdesc)
 
 let get_ret_param_var pdesc = Pvar.get_ret_param_pvar (get_proc_name pdesc)
 
+let get_ret_type_from_signature pdesc =
+  if pdesc.attributes.has_added_return_param then
+    List.last pdesc.attributes.formals
+    |> Option.value_map
+         ~f:(fun (_, typ) ->
+           match typ.Typ.desc with Tptr (t, _) -> t | _ -> pdesc.attributes.ret_type )
+         ~default:pdesc.attributes.ret_type
+  else pdesc.attributes.ret_type
+
+
 let get_start_node pdesc = pdesc.start_node
 
 (** Return [true] iff the procedure is defined, and not just declared *)

infer/src/IR/Procdesc.mli

@@ -271,6 +271,10 @@ val get_ret_var : t -> Pvar.t
 
 val get_ret_param_var : t -> Pvar.t
 
+val get_ret_type_from_signature : t -> Typ.t
+(** Return the return type from method signature: if the procedure has added return parameter,
+    return its type *)
+
 val get_start_node : t -> Node.t
 
 val get_static_callees : t -> Procname.t list

infer/src/pulse/PulseDiagnostic.ml

@@ -57,7 +57,8 @@ let immediate_or_first_call calling_context (trace : Trace.t) =
 let get_message diagnostic =
   let pulse_start_msg = "Pulse found a potential" in
   match diagnostic with
-  | AccessToInvalidAddress {calling_context; invalidation; invalidation_trace; access_trace} -> (
+  | AccessToInvalidAddress
+      {calling_context; invalidation; invalidation_trace; access_trace; must_be_valid_reason} -> (
       let invalidation, invalidation_trace =
         Trace.get_invalidation access_trace
         |> Option.value_map
@@ -67,6 +68,14 @@ let get_message diagnostic =
       match invalidation with
       | ConstantDereference i when IntLit.equal i IntLit.zero ->
           (* Special error message for nullptr dereference *)
+          let issue_kind_str =
+            match must_be_valid_reason with
+            | Some (Invalidation.SelfOfNonPODReturnMethod non_pod_typ) ->
+                F.asprintf "undefined behaviour caused by nil messaging of non-pod return type (%a)"
+                  (Typ.pp Pp.text) non_pod_typ
+            | _ ->
+                F.sprintf "null pointer dereference"
+          in
           let pp_access_trace fmt (trace : Trace.t) =
             match immediate_or_first_call calling_context trace with
             | `Immediate ->
@@ -78,10 +87,10 @@ let get_message diagnostic =
             let pp_line fmt line = F.fprintf fmt "on line %d" line in
             match immediate_or_first_call calling_context trace with
             | `Immediate ->
-                F.fprintf fmt "null pointer dereference %a" pp_line line
+                F.fprintf fmt "%s %a" issue_kind_str pp_line line
             | `Call f ->
-                F.fprintf fmt "null pointer dereference %a indirectly during the call to %a" pp_line
+                F.fprintf fmt "%s %a indirectly during the call to %a" issue_kind_str pp_line line
-                  line CallEvent.describe f
+                  CallEvent.describe f
           in
           let invalidation_line =
             let {Location.line; _} = Trace.get_outer_location invalidation_trace in

infer/src/pulse/PulseInvalidation.ml

@@ -52,7 +52,10 @@ type t =
   | JavaIterator of java_iterator_function
 [@@deriving compare, equal]
 
-type must_be_valid_reason = BlockCall | InsertionIntoCollection | SelfOfNonPODReturnMethod
+type must_be_valid_reason =
+  | BlockCall
+  | InsertionIntoCollection
+  | SelfOfNonPODReturnMethod of Typ.t
 [@@deriving compare, equal]
 
 let pp_must_be_valid_reason f = function
@@ -62,7 +65,7 @@ let pp_must_be_valid_reason f = function
       F.fprintf f "Block"
   | Some InsertionIntoCollection ->
       F.fprintf f "InsertionIntoCollection"
-  | Some SelfOfNonPODReturnMethod ->
+  | Some (SelfOfNonPODReturnMethod _) ->
       F.fprintf f "SelfOfNonPODReturnMethod"
 
 
@@ -78,7 +81,7 @@ let issue_type_of_cause invalidation must_be_valid_reason =
         IssueType.nil_block_call
     | Some InsertionIntoCollection ->
         IssueType.nil_insertion_into_collection
-    | Some SelfOfNonPODReturnMethod ->
+    | Some (SelfOfNonPODReturnMethod _) ->
         IssueType.nil_messaging_to_non_pod )
   | ConstantDereference _ ->
       IssueType.constant_address_dereference

infer/src/pulse/PulseInvalidation.mli

@@ -40,7 +40,10 @@ val pp : F.formatter -> t -> unit
 
 val describe : F.formatter -> t -> unit
 
-type must_be_valid_reason = BlockCall | InsertionIntoCollection | SelfOfNonPODReturnMethod
+type must_be_valid_reason =
+  | BlockCall
+  | InsertionIntoCollection
+  | SelfOfNonPODReturnMethod of Typ.t
 [@@deriving compare, equal]
 
 val pp_must_be_valid_reason : F.formatter -> must_be_valid_reason option -> unit

infer/src/pulse/PulseObjectiveCSummary.ml

@@ -126,8 +126,9 @@ let update_must_be_valid_reason {InterproceduralAnalysis.tenv; proc_desc; err_lo
       let result =
         (* add reason for must be valid to be because the return type is non pod *)
         let+ astate, value = PulseOperations.eval_deref path location (Lvar self) astate in
-        AddressAttributes.replace_must_be_valid_reason path SelfOfNonPODReturnMethod (fst value)
+        AddressAttributes.replace_must_be_valid_reason path
-          astate
+          (SelfOfNonPODReturnMethod (Procdesc.get_ret_type_from_signature proc_desc))
+          (fst value) astate
       in
       PulseReport.report_result tenv proc_desc err_log location result
   | ContinueProgram _, _