[pulse] Separate issue type for nil messaging of non-pod return type

Summary: Added a new issue type for sending a message to nil when its return type is non-POD. To distinguish these issues from other nullptr dereference issues, we extend the `MustBeValid` attribute to contain the reason of why an address must be valid. For now a reason can only have `SelfOfNonPODReturnMethod` as it's value, but in the future we will use it for other nullability issue types, such as nil insertion into collections.

Reviewed By: jvillard

Differential Revision: D27762333

fbshipit-source-id: 689e5a431

infer/man/man1/infer-full.txt

@@ -541,6 +541,7 @@ OPTIONS
              MULTIPLE_WEAKSELF (enabled by default),
              MUTABLE_LOCAL_VARIABLE_IN_COMPONENT_FILE (enabled by default),
              Missing_fld (enabled by default),
+             NIL_MESSAGING_TO_NON_POD (disabled by default),
              NULLPTR_DEREFERENCE (enabled by default),
              NULL_DEREFERENCE (enabled by default),
              OPTIONAL_EMPTY_ACCESS (enabled by default),

infer/man/man1/infer-report.txt

@@ -218,6 +218,7 @@ OPTIONS
              MULTIPLE_WEAKSELF (enabled by default),
              MUTABLE_LOCAL_VARIABLE_IN_COMPONENT_FILE (enabled by default),
              Missing_fld (enabled by default),
+             NIL_MESSAGING_TO_NON_POD (disabled by default),
              NULLPTR_DEREFERENCE (enabled by default),
              NULL_DEREFERENCE (enabled by default),
              OPTIONAL_EMPTY_ACCESS (enabled by default),

infer/man/man1/infer.txt

@@ -541,6 +541,7 @@ OPTIONS
              MULTIPLE_WEAKSELF (enabled by default),
              MUTABLE_LOCAL_VARIABLE_IN_COMPONENT_FILE (enabled by default),
              Missing_fld (enabled by default),
+             NIL_MESSAGING_TO_NON_POD (disabled by default),
              NULLPTR_DEREFERENCE (enabled by default),
              NULL_DEREFERENCE (enabled by default),
              OPTIONAL_EMPTY_ACCESS (enabled by default),

infer/src/base/IssueType.ml

@@ -799,6 +799,11 @@ let nullptr_dereference =
     ~user_documentation:[%blob "../../documentation/issues/NULLPTR_DEREFERENCE.md"]
 
 
+let nil_messaging_to_non_pod =
+  register ~enabled:false ~id:"NIL_MESSAGING_TO_NON_POD" Error Pulse
+    ~user_documentation:"See [NULLPTR_DEREFERENCE](#nullptr_dereference)."
+
+
 let optional_empty_access =
   register ~id:"OPTIONAL_EMPTY_ACCESS" Error Pulse
     ~user_documentation:[%blob "../../documentation/issues/OPTIONAL_EMPTY_ACCESS.md"]

infer/src/base/IssueType.mli

@@ -276,6 +276,8 @@ val multiple_weakself : t
 
 val mutable_local_variable_in_component_file : t
 
+val nil_messaging_to_non_pod : t
+
 val null_dereference : t
 
 val nullptr_dereference : t

infer/src/pulse/PulseAbductiveDomain.ml

@@ -163,7 +163,8 @@ module Stack = struct
         let post_attrs =
           if Config.pulse_isl then
             let access_trace = Trace.Immediate {location; history= []} in
-            BaseAddressAttributes.add_one addr (MustBeValid access_trace)
+            BaseAddressAttributes.add_one addr
+              (MustBeValid (access_trace, None))
               (astate.post :> base_domain).attrs
           else (astate.post :> base_domain).attrs
         in
@@ -242,7 +243,7 @@ module AddressAttributes = struct
   let check_valid access_trace addr astate =
     let+ () = BaseAddressAttributes.check_valid addr (astate.post :> base_domain).attrs in
     (* if [address] is in [pre] and it should be valid then that fact goes in the precondition *)
-    abduce_attribute addr (MustBeValid access_trace) astate
+    abduce_attribute addr (MustBeValid (access_trace, None)) astate
 
 
   let check_initialized access_trace addr astate =
@@ -312,6 +313,14 @@ module AddressAttributes = struct
     map_post_attrs astate ~f:(BaseAddressAttributes.mark_as_end_of_collection addr)
 
 
+  let replace_must_be_valid_reason reason addr astate =
+    match BaseAddressAttributes.get_must_be_valid addr (astate.pre :> base_domain).attrs with
+    | Some (trace, _reason) ->
+        abduce_attribute addr (MustBeValid (trace, Some reason)) astate
+    | None ->
+        astate
+
+
   let is_end_of_collection addr astate =
     BaseAddressAttributes.is_end_of_collection addr (astate.post :> base_domain).attrs
 
@@ -353,7 +362,7 @@ module AddressAttributes = struct
         BaseAddressAttributes.get_must_be_valid_or_allocated_isl addr
           (astate.post :> BaseDomain.t).attrs
       with
-      | None ->
+      | None, reason ->
           let null_astates =
             if PathCondition.is_known_not_equal_zero astate.path_condition addr then []
             else
@@ -369,7 +378,7 @@ module AddressAttributes = struct
             else
               let valid_astate =
                 let abdalloc = Attribute.ISLAbduced access_trace in
-                let valid_attr = Attribute.MustBeValid access_trace in
+                let valid_attr = Attribute.MustBeValid (access_trace, reason) in
                 add_one addr abdalloc astate |> abduce_attribute addr valid_attr
                 |> abduce_attribute addr abdalloc
               in
@@ -381,7 +390,7 @@ module AddressAttributes = struct
               [Ok valid_astate; Error (`ISLError invalid_free)]
           in
           not_null_astates @ null_astates
-      | Some _ ->
+      | Some _, _ ->
           [Ok astate] )
     | Some (invalidation, invalidation_trace) ->
         [Error (`InvalidAccess (invalidation, invalidation_trace, astate))]
@@ -457,7 +466,9 @@ let rec set_uninitialized_post tenv src typ location ?(fields_prefix = RevList.e
       let stack, addr = add_edge_on_src src location stack in
       let attrs =
         if Config.pulse_isl then
-          BaseAddressAttributes.add_one addr (MustBeValid (Immediate {location; history= []})) attrs
+          BaseAddressAttributes.add_one addr
+            (MustBeValid (Immediate {location; history= []}, None))
+            attrs
         else attrs
       in
       let attrs = BaseAddressAttributes.add_one addr Uninitialized attrs in
@@ -541,7 +552,9 @@ let mk_initial tenv proc_desc =
     if Config.pulse_isl then
       List.fold formals_and_captured ~init:(PreDomain.empty :> base_domain).attrs
         ~f:(fun attrs (_, _, (addr, _)) ->
-          BaseAddressAttributes.add_one addr (MustBeValid (Immediate {location; history= []})) attrs )
+          BaseAddressAttributes.add_one addr
+            (MustBeValid (Immediate {location; history= []}, None))
+            attrs )
     else (PreDomain.empty :> base_domain).attrs
   in
   let pre =

infer/src/pulse/PulseAbductiveDomain.mli

@@ -141,6 +141,8 @@ module AddressAttributes : sig
 
   val invalidate : AbstractValue.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t
 
+  val replace_must_be_valid_reason : Invalidation.must_be_valid_reason -> AbstractValue.t -> t -> t
+
   val allocate : Procname.t -> AbstractValue.t * ValueHistory.t -> Location.t -> t -> t
 
   val add_dynamic_type : Typ.t -> AbstractValue.t -> t -> t
@@ -190,7 +192,10 @@ val summary_of_post :
      Tenv.t
   -> Procdesc.t
   -> t
-  -> (summary, [> `PotentialInvalidAccessSummary of summary * AbstractValue.t * Trace.t]) result
+  -> ( summary
+     , [> `PotentialInvalidAccessSummary of
+          summary * AbstractValue.t * (Trace.t * Invalidation.must_be_valid_reason option) ] )
+     result
      SatUnsat.t
 (** trim the state down to just the procedure's interface (formals and globals), and simplify and
     normalize the state *)
@@ -204,7 +209,10 @@ val set_post_cell : AbstractValue.t * ValueHistory.t -> BaseDomain.cell -> Locat
 val incorporate_new_eqs :
      PathCondition.new_eqs
   -> t
-  -> (t, [> `PotentialInvalidAccess of t * AbstractValue.t * Trace.t]) result
+  -> ( t
+     , [> `PotentialInvalidAccess of
+          t * AbstractValue.t * (Trace.t * Invalidation.must_be_valid_reason option) ] )
+     result
 (** Check that the new equalities discovered are compatible with the current pre and post heaps,
     e.g. [x = 0] is not compatible with [x] being allocated, and [x = y] is not compatible with [x]
     and [y] being allocated separately. In those cases, the resulting path condition is

infer/src/pulse/PulseAccessResult.ml

@@ -10,9 +10,14 @@ open PulseBasicInterface
 module AbductiveDomain = PulseAbductiveDomain
 
 type 'astate error =
-  | PotentialInvalidAccess of {astate: 'astate; address: AbstractValue.t; must_be_valid: Trace.t}
+  | PotentialInvalidAccess of
+      { astate: 'astate
+      ; address: AbstractValue.t
+      ; must_be_valid: Trace.t * Invalidation.must_be_valid_reason option }
   | PotentialInvalidAccessSummary of
-      {astate: AbductiveDomain.summary; address: AbstractValue.t; must_be_valid: Trace.t}
+      { astate: AbductiveDomain.summary
+      ; address: AbstractValue.t
+      ; must_be_valid: Trace.t * Invalidation.must_be_valid_reason option }
   | ReportableError of {astate: 'astate; diagnostic: Diagnostic.t}
   | ISLError of 'astate
 
@@ -22,8 +27,11 @@ type 'a t = ('a, AbductiveDomain.t) base_t
 
 type 'astate abductive_error =
   [ `ISLError of 'astate
-  | `PotentialInvalidAccess of 'astate * AbstractValue.t * Trace.t
+  | `PotentialInvalidAccess of
-  | `PotentialInvalidAccessSummary of AbductiveDomain.summary * AbstractValue.t * Trace.t ]
+    'astate * AbstractValue.t * (Trace.t * Invalidation.must_be_valid_reason option)
+  | `PotentialInvalidAccessSummary of
+    AbductiveDomain.summary * AbstractValue.t * (Trace.t * Invalidation.must_be_valid_reason option)
+  ]
 
 let of_abductive_error = function
   | `ISLError astate ->
@@ -43,6 +51,10 @@ let of_abductive_access_result access_trace abductive_result =
           { astate
           ; diagnostic=
               AccessToInvalidAddress
-                {calling_context= []; invalidation; invalidation_trace; access_trace} }
+                { calling_context= []
+                ; invalidation
+                ; invalidation_trace
+                ; access_trace
+                ; must_be_valid_reason= None } }
     | (`ISLError _ | `PotentialInvalidAccess _ | `PotentialInvalidAccessSummary _) as error ->
         of_abductive_error error )

infer/src/pulse/PulseAccessResult.mli

@@ -10,9 +10,14 @@ open PulseBasicInterface
 module AbductiveDomain = PulseAbductiveDomain
 
 type 'astate error =
-  | PotentialInvalidAccess of {astate: 'astate; address: AbstractValue.t; must_be_valid: Trace.t}
+  | PotentialInvalidAccess of
+      { astate: 'astate
+      ; address: AbstractValue.t
+      ; must_be_valid: Trace.t * Invalidation.must_be_valid_reason option }
   | PotentialInvalidAccessSummary of
-      {astate: AbductiveDomain.summary; address: AbstractValue.t; must_be_valid: Trace.t}
+      { astate: AbductiveDomain.summary
+      ; address: AbstractValue.t
+      ; must_be_valid: Trace.t * Invalidation.must_be_valid_reason option }
   | ReportableError of {astate: 'astate; diagnostic: Diagnostic.t}
   | ISLError of 'astate
 
@@ -24,8 +29,11 @@ type 'a t = ('a, AbductiveDomain.t) base_t
     circular dependency. *)
 type 'astate abductive_error =
   [ `ISLError of 'astate
-  | `PotentialInvalidAccess of 'astate * AbstractValue.t * Trace.t
+  | `PotentialInvalidAccess of
-  | `PotentialInvalidAccessSummary of AbductiveDomain.summary * AbstractValue.t * Trace.t ]
+    'astate * AbstractValue.t * (Trace.t * Invalidation.must_be_valid_reason option)
+  | `PotentialInvalidAccessSummary of
+    AbductiveDomain.summary * AbstractValue.t * (Trace.t * Invalidation.must_be_valid_reason option)
+  ]
 
 val of_abductive_error : 'astate abductive_error -> 'astate error
 

infer/src/pulse/PulseAttribute.ml

@@ -34,7 +34,7 @@ module Attribute = struct
     | Invalid of Invalidation.t * Trace.t
     | ISLAbduced of Trace.t
     | MustBeInitialized of Trace.t
-    | MustBeValid of Trace.t
+    | MustBeValid of Trace.t * Invalidation.must_be_valid_reason option
     | StdVectorReserve
     | Uninitialized
     | WrittenTo of Trace.t
@@ -63,7 +63,7 @@ module Attribute = struct
     Variants.to_rank (Invalid (Invalidation.ConstantDereference IntLit.zero, dummy_trace))
 
 
-  let must_be_valid_rank = Variants.to_rank (MustBeValid dummy_trace)
+  let must_be_valid_rank = Variants.to_rank (MustBeValid (dummy_trace, None))
 
   let std_vector_reserve_rank = Variants.to_rank StdVectorReserve
 
@@ -125,8 +125,10 @@ module Attribute = struct
         F.fprintf f "MustBeInitialized %a"
           (Trace.pp ~pp_immediate:(pp_string_if_debug "read"))
           trace
-    | MustBeValid trace ->
+    | MustBeValid (trace, reason) ->
-        F.fprintf f "MustBeValid %a" (Trace.pp ~pp_immediate:(pp_string_if_debug "access")) trace
+        F.fprintf f "MustBeValid %a (%a)"
+          (Trace.pp ~pp_immediate:(pp_string_if_debug "access"))
+          trace Invalidation.pp_must_be_valid_reason reason
     | StdVectorReserve ->
         F.pp_print_string f "std::vector::reserve()"
     | Uninitialized ->
@@ -148,8 +150,8 @@ module Attributes = struct
   let get_must_be_valid attrs =
     Set.find_rank attrs Attribute.must_be_valid_rank
     |> Option.map ~f:(fun attr ->
-           let[@warning "-8"] (Attribute.MustBeValid action) = attr in
+           let[@warning "-8"] (Attribute.MustBeValid (trace, reason)) = attr in
-           action )
+           (trace, reason) )
 
 
   let get_written_to attrs =
@@ -294,8 +296,8 @@ let map_trace ~f = function
       ISLAbduced (f trace)
   | Invalid (invalidation, trace) ->
       Invalid (invalidation, f trace)
-  | MustBeValid trace ->
+  | MustBeValid (trace, reason) ->
-      MustBeValid (f trace)
+      MustBeValid (f trace, reason)
   | WrittenTo trace ->
       WrittenTo (f trace)
   | MustBeInitialized trace ->

infer/src/pulse/PulseAttribute.mli

@@ -21,7 +21,7 @@ type t =
   | Invalid of Invalidation.t * Trace.t
   | ISLAbduced of Trace.t  (** The allocation is abduced so as the analysis could run normally *)
   | MustBeInitialized of Trace.t
-  | MustBeValid of Trace.t
+  | MustBeValid of Trace.t * Invalidation.must_be_valid_reason option
   | StdVectorReserve
   | Uninitialized
   | WrittenTo of Trace.t
@@ -53,7 +53,7 @@ module Attributes : sig
 
   val get_isl_abduced : t -> Trace.t option
 
-  val get_must_be_valid : t -> Trace.t option
+  val get_must_be_valid : t -> (Trace.t * Invalidation.must_be_valid_reason option) option
 
   val get_written_to : t -> Trace.t option
 

infer/src/pulse/PulseBaseAddressAttributes.ml

@@ -116,8 +116,8 @@ let remove_isl_abduced_attr address memory =
 
 let remove_must_be_valid_attr address memory =
   match get_attribute Attributes.get_must_be_valid address memory with
-  | Some trace ->
+  | Some (trace, reason) ->
-      remove_one address (Attribute.MustBeValid trace) memory
+      remove_one address (Attribute.MustBeValid (trace, reason)) memory
   | None ->
       memory
 
@@ -136,14 +136,14 @@ let get_must_be_valid = get_attribute Attributes.get_must_be_valid
 
 let get_must_be_valid_or_allocated_isl address attrs =
   match get_must_be_valid address attrs with
-  | Some trace ->
+  | Some (trace, reason) ->
-      Some trace
+      (Some trace, reason)
   | None -> (
     match get_attribute Attributes.get_allocation address attrs with
     | Some (_, trace) ->
-        Some trace
+        (Some trace, None)
     | None ->
-        get_attribute Attributes.get_isl_abduced address attrs )
+        (get_attribute Attributes.get_isl_abduced address attrs, None) )
 
 
 let get_must_be_initialized = get_attribute Attributes.get_must_be_initialized

infer/src/pulse/PulseBaseAddressAttributes.mli

@@ -37,9 +37,11 @@ val get_closure_proc_name : AbstractValue.t -> t -> Procname.t option
 
 val get_invalid : AbstractValue.t -> t -> (Invalidation.t * Trace.t) option
 
-val get_must_be_valid : AbstractValue.t -> t -> Trace.t option
+val get_must_be_valid :
+  AbstractValue.t -> t -> (Trace.t * Invalidation.must_be_valid_reason option) option
 
-val get_must_be_valid_or_allocated_isl : AbstractValue.t -> t -> Trace.t option
+val get_must_be_valid_or_allocated_isl :
+  AbstractValue.t -> t -> Trace.t option * Invalidation.must_be_valid_reason option
 
 val get_must_be_initialized : AbstractValue.t -> t -> Trace.t option
 

infer/src/pulse/PulseCallOperations.ml

@@ -173,7 +173,8 @@ let apply_callee tenv ~caller_proc_desc callee_pname call_loc callee_exec_state
                                     { calling_context
                                     ; invalidation
                                     ; invalidation_trace
-                                    ; access_trace= must_be_valid }
+                                    ; access_trace= fst must_be_valid
+                                    ; must_be_valid_reason= snd must_be_valid }
                               ; astate= (astate_summary :> AbductiveDomain.t) })) ) ) ) )
   | ISLLatentMemoryError astate ->
       map_call_result ~is_isl_error_prepost:true

infer/src/pulse/PulseDiagnostic.ml

@@ -16,7 +16,8 @@ type access_to_invalid_address =
   { calling_context: (CallEvent.t * Location.t) list
   ; invalidation: Invalidation.t
   ; invalidation_trace: Trace.t
-  ; access_trace: Trace.t }
+  ; access_trace: Trace.t
+  ; must_be_valid_reason: Invalidation.must_be_valid_reason option }
 [@@deriving compare, equal]
 
 type read_uninitialized_value = {calling_context: (CallEvent.t * Location.t) list; trace: Trace.t}
@@ -257,8 +258,8 @@ let get_trace = function
 
 
 let get_issue_type = function
-  | AccessToInvalidAddress {invalidation; _} ->
+  | AccessToInvalidAddress {invalidation; must_be_valid_reason} ->
-      Invalidation.issue_type_of_cause invalidation
+      Invalidation.issue_type_of_cause invalidation must_be_valid_reason
   | MemoryLeak _ ->
       IssueType.pulse_memory_leak
   | ReadUninitializedValue _ ->

infer/src/pulse/PulseDiagnostic.mli

@@ -21,7 +21,8 @@ type access_to_invalid_address =
             further assumptions *)
   ; access_trace: Trace.t
         (** assuming we are in the calling context, the trace leads to an access to the value
-            invalidated in [invalidation_trace] without further assumptions *) }
+            invalidated in [invalidation_trace] without further assumptions *)
+  ; must_be_valid_reason: Invalidation.must_be_valid_reason option }
 [@@deriving compare, equal, yojson_of]
 
 type read_uninitialized_value =

infer/src/pulse/PulseExecutionDomain.ml

@@ -23,7 +23,7 @@ type 'abductive_domain_t base_t =
   | LatentInvalidAccess of
       { astate: AbductiveDomain.summary
       ; address: AbstractValue.t
-      ; must_be_valid: (Trace.t[@yojson.opaque])
+      ; must_be_valid: (Trace.t * Invalidation.must_be_valid_reason option[@yojson.opaque])
       ; calling_context: ((CallEvent.t * Location.t) list[@yojson.opaque]) }
   | ISLLatentMemoryError of AbductiveDomain.summary
 [@@deriving equal, compare, yojson_of]

infer/src/pulse/PulseExecutionDomain.mli

@@ -21,7 +21,7 @@ type 'abductive_domain_t base_t =
   | LatentInvalidAccess of
       { astate: AbductiveDomain.summary
       ; address: AbstractValue.t
-      ; must_be_valid: Trace.t
+      ; must_be_valid: Trace.t * Invalidation.must_be_valid_reason option
       ; calling_context: (CallEvent.t * Location.t) list }
       (** if [address] is ever observed to be invalid then there is an invalid access because it
           [must_be_valid] *)

infer/src/pulse/PulseInterproc.ml

@@ -620,7 +620,7 @@ let check_all_valid callee_proc_name call_location {AbductiveDomain.pre; _} call
         match BaseAddressAttributes.get_must_be_valid addr_pre (pre :> BaseDomain.t).attrs with
         | None ->
             astate_result
-        | Some callee_access_trace ->
+        | Some (callee_access_trace, must_be_valid_reason) ->
             let access_trace = mk_access_trace callee_access_trace in
             AddressAttributes.check_valid access_trace addr_caller astate
             |> Result.map_error ~f:(fun (invalidation, invalidation_trace) ->
@@ -628,7 +628,11 @@ let check_all_valid callee_proc_name call_location {AbductiveDomain.pre; _} call
                    AccessResult.ReportableError
                      { diagnostic=
                          Diagnostic.AccessToInvalidAddress
-                           {calling_context= []; invalidation; invalidation_trace; access_trace}
+                           { calling_context= []
+                           ; invalidation
+                           ; invalidation_trace
+                           ; access_trace
+                           ; must_be_valid_reason }
                      ; astate } )
       in
       match BaseAddressAttributes.get_must_be_initialized addr_pre (pre :> BaseDomain.t).attrs with
@@ -678,7 +682,11 @@ let isl_check_all_invalid invalid_addr_callers callee_proc_name call_location
                 (AccessResult.ReportableError
                    { diagnostic=
                        Diagnostic.AccessToInvalidAddress
-                         {calling_context= []; invalidation; invalidation_trace; access_trace}
+                         { calling_context= []
+                         ; invalidation
+                         ; invalidation_trace
+                         ; access_trace
+                         ; must_be_valid_reason= None }
                    ; astate }) ) ) )
     invalid_addr_callers (Ok astate)
 

infer/src/pulse/PulseInvalidation.ml

@@ -52,11 +52,25 @@ type t =
   | JavaIterator of java_iterator_function
 [@@deriving compare, equal]
 
-let issue_type_of_cause = function
+type must_be_valid_reason = SelfOfNonPODReturnMethod [@@deriving compare, equal]
+
+let pp_must_be_valid_reason f = function
+  | None ->
+      F.fprintf f "None"
+  | Some SelfOfNonPODReturnMethod ->
+      F.fprintf f "SelfOfNonPODReturnMethod"
+
+
+let issue_type_of_cause invalidation must_be_valid_reason =
+  match invalidation with
   | CFree ->
       IssueType.use_after_free
-  | ConstantDereference i when IntLit.iszero i ->
+  | ConstantDereference i when IntLit.iszero i -> (
+    match must_be_valid_reason with
+    | None ->
         IssueType.nullptr_dereference
+    | Some SelfOfNonPODReturnMethod ->
+        IssueType.nil_messaging_to_non_pod )
   | ConstantDereference _ ->
       IssueType.constant_address_dereference
   | CppDelete ->

infer/src/pulse/PulseInvalidation.mli

@@ -38,6 +38,10 @@ val isl_equiv : t -> t -> bool
 
 val pp : F.formatter -> t -> unit
 
-val issue_type_of_cause : t -> IssueType.t
-
 val describe : F.formatter -> t -> unit
+
+type must_be_valid_reason = SelfOfNonPODReturnMethod [@@deriving compare, equal]
+
+val pp_must_be_valid_reason : F.formatter -> must_be_valid_reason option -> unit
+
+val issue_type_of_cause : t -> must_be_valid_reason option -> IssueType.t

infer/src/pulse/PulseModels.ml

@@ -681,7 +681,11 @@ module GenericArrayBackedCollectionIterator = struct
           (ReportableError
              { diagnostic=
                  Diagnostic.AccessToInvalidAddress
-                   {calling_context= []; invalidation= EndIterator; invalidation_trace; access_trace}
+                   { calling_context= []
+                   ; invalidation= EndIterator
+                   ; invalidation_trace
+                   ; access_trace
+                   ; must_be_valid_reason= None }
              ; astate })
       else Ok astate
     in

infer/src/pulse/PulseObjectiveCSummary.ml

@@ -8,6 +8,7 @@
 open! IStd
 open PulseDomainInterface
 open PulseOperations.Import
+open PulseBasicInterface
 
 let mk_objc_self_pvar proc_desc =
   let proc_name = Procdesc.get_proc_name proc_desc in
@@ -104,10 +105,38 @@ let append_objc_actual_self_positive procdesc self_actual astate =
       Ok astate
 
 
+let update_must_be_valid_reason {InterproceduralAnalysis.tenv; proc_desc; err_log} astate =
+  let location = Procdesc.get_loc proc_desc in
+  let self = mk_objc_self_pvar proc_desc in
+  let proc_name = Procdesc.get_proc_name proc_desc in
+  match (astate, proc_name) with
+  | ContinueProgram astate, Procname.ObjC_Cpp {kind= ObjCInstanceMethod}
+    when not (Procdesc.is_ret_type_pod proc_desc) ->
+      let result =
+        (* add reason for must be valid to be because the return type is non pod *)
+        let+ astate, value = PulseOperations.eval_deref location (Lvar self) astate in
+        let astate =
+          AddressAttributes.replace_must_be_valid_reason Invalidation.SelfOfNonPODReturnMethod
+            (fst value) astate
+        in
+        astate
+      in
+      PulseReport.report_result tenv proc_desc err_log result
+  | ContinueProgram _, _
+  | ExitProgram _, _
+  | AbortProgram _, _
+  | LatentAbortProgram _, _
+  | LatentInvalidAccess _, _
+  | ISLLatentMemoryError _, _ ->
+      [astate]
+
+
 let update_objc_method_posts ({InterproceduralAnalysis.tenv; proc_desc; err_log} as analysis_data)
     ~initial_astate ~posts =
-  mk_objc_method_nil_summary tenv proc_desc initial_astate
+  match mk_objc_method_nil_summary tenv proc_desc initial_astate with
-  |> Option.value_map ~default:posts ~f:(function result ->
+  | None ->
+      List.concat_map ~f:(update_must_be_valid_reason analysis_data) posts
+  | Some result ->
       let nil_summary = PulseReport.report_result tenv proc_desc err_log result in
       let posts = List.concat_map ~f:(append_objc_self_positive analysis_data) posts in
-         nil_summary @ posts )
+      nil_summary @ posts

infer/src/pulse/PulseOperations.ml

@@ -23,14 +23,19 @@ module Import = struct
     | LatentInvalidAccess of
         { astate: AbductiveDomain.summary
         ; address: AbstractValue.t
-        ; must_be_valid: Trace.t
+        ; must_be_valid: Trace.t * Invalidation.must_be_valid_reason option
         ; calling_context: (CallEvent.t * Location.t) list }
     | ISLLatentMemoryError of AbductiveDomain.summary
 
   type 'astate base_error = 'astate AccessResult.error =
-    | PotentialInvalidAccess of {astate: 'astate; address: AbstractValue.t; must_be_valid: Trace.t}
+    | PotentialInvalidAccess of
+        { astate: 'astate
+        ; address: AbstractValue.t
+        ; must_be_valid: Trace.t * Invalidation.must_be_valid_reason option }
     | PotentialInvalidAccessSummary of
-        {astate: AbductiveDomain.summary; address: AbstractValue.t; must_be_valid: Trace.t}
+        { astate: AbductiveDomain.summary
+        ; address: AbstractValue.t
+        ; must_be_valid: Trace.t * Invalidation.must_be_valid_reason option }
     | ReportableError of {astate: 'astate; diagnostic: Diagnostic.t}
     | ISLError of 'astate
 
@@ -52,7 +57,11 @@ let check_addr_access access_mode location (address, history) astate =
            ReportableError
              { diagnostic=
                  Diagnostic.AccessToInvalidAddress
-                   {calling_context= []; invalidation; invalidation_trace; access_trace}
+                   { calling_context= []
+                   ; invalidation
+                   ; invalidation_trace
+                   ; access_trace
+                   ; must_be_valid_reason= None }
              ; astate } )
   in
   match access_mode with

infer/src/pulse/PulseOperations.mli

@@ -30,14 +30,19 @@ module Import : sig
     | LatentInvalidAccess of
         { astate: AbductiveDomain.summary
         ; address: AbstractValue.t
-        ; must_be_valid: Trace.t
+        ; must_be_valid: Trace.t * Invalidation.must_be_valid_reason option
         ; calling_context: (CallEvent.t * Location.t) list }
     | ISLLatentMemoryError of AbductiveDomain.summary
 
   type 'astate base_error = 'astate AccessResult.error =
-    | PotentialInvalidAccess of {astate: 'astate; address: AbstractValue.t; must_be_valid: Trace.t}
+    | PotentialInvalidAccess of
+        { astate: 'astate
+        ; address: AbstractValue.t
+        ; must_be_valid: Trace.t * Invalidation.must_be_valid_reason option }
     | PotentialInvalidAccessSummary of
-        {astate: AbductiveDomain.summary; address: AbstractValue.t; must_be_valid: Trace.t}
+        { astate: AbductiveDomain.summary
+        ; address: AbstractValue.t
+        ; must_be_valid: Trace.t * Invalidation.must_be_valid_reason option }
     | ReportableError of {astate: 'astate; diagnostic: Diagnostic.t}
     | ISLError of 'astate
 

infer/src/pulse/PulseReport.ml

@@ -87,7 +87,8 @@ let report_summary_error tenv proc_desc err_log
              { calling_context= []
              ; invalidation= ConstantDereference IntLit.zero
              ; invalidation_trace= Immediate {location= Procdesc.get_loc proc_desc; history= []}
-             ; access_trace= must_be_valid }) ;
+             ; access_trace= fst must_be_valid
+             ; must_be_valid_reason= snd must_be_valid }) ;
       LatentInvalidAccess {astate; address; must_be_valid; calling_context= []}
   | ISLError astate ->
       ISLLatentMemoryError astate

infer/src/pulse/PulseSummary.ml

@@ -45,7 +45,8 @@ let exec_summary_of_post_common tenv ~continue_program proc_desc err_log
                      { calling_context= []
                      ; invalidation
                      ; invalidation_trace
-                     ; access_trace= must_be_valid }
+                     ; access_trace= fst must_be_valid
+                     ; must_be_valid_reason= snd must_be_valid }
                ; astate })
           |> Option.some ) )
   (* already a summary but need to reconstruct the variants to make the type system happy :( *)

infer/tests/codetoanalyze/objcpp/pulse/Makefile

@@ -10,7 +10,8 @@ INFER_OPTIONS = --pulse-only --debug-exceptions --project-root $(TESTS_DIR) \
 --pulse-model-alloc-pattern "AB[IF].*Create.*" \
 --pulse-model-release-pattern "ABFRelease" \
 --pulse-model-transfer-ownership "abf::BridgingRelease" \
---pulse-model-transfer-ownership "ABFBridgingRelease"
+--pulse-model-transfer-ownership "ABFBridgingRelease" \
+--pulse-report-latent-issues
 
 INFERPRINT_OPTIONS = --issues-tests
 

infer/tests/codetoanalyze/objcpp/pulse/NPEBasic.mm

@@ -92,6 +92,25 @@ std::shared_ptr<int> testNonPODTraceBad() {
   return result;
 }
 
+std::shared_ptr<int> testCallMethodReturnsnonPODLatent(bool b) {
+  SomeObject* obj;
+  if (b) {
+    obj = nil;
+  } else {
+    obj = [SomeObject new];
+  }
+  std::shared_ptr<int> d = [obj returnsnonPOD]; // UB if obj nil
+  return d;
+}
+
+std::shared_ptr<int> testCallMethodReturnsnonPODLatentBad(bool b) {
+  return testCallMethodReturnsnonPODLatent(true);
+}
+
+std::shared_ptr<int> testCallMethodReturnsnonPODLatentOk(bool b) {
+  return testCallMethodReturnsnonPODLatent(false);
+}
+
 int testAccessPropertyAccessorOk() {
   SomeObject* obj = nil;
   return obj.x; // calls property accessor method

infer/tests/codetoanalyze/objcpp/pulse/issues.exp

@@ -1,8 +1,10 @@
 codetoanalyze/objcpp/pulse/AllocPatternMemLeak.mm, A.create_no_release_leak_bad, 1, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `ABFDataCreate` (modelled),allocation part of the trace ends here,memory becomes unreachable here]
 codetoanalyze/objcpp/pulse/NPEBasic.mm, dereferenceNilBad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here]
-codetoanalyze/objcpp/pulse/NPEBasic.mm, testAccessPropertyAccessorBad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,when calling `SomeObject.ptr` here,parameter `self` of SomeObject.ptr,invalid access occurs here]
+codetoanalyze/objcpp/pulse/NPEBasic.mm, testAccessPropertyAccessorBad, 2, NIL_MESSAGING_TO_NON_POD, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,when calling `SomeObject.ptr` here,parameter `self` of SomeObject.ptr,invalid access occurs here]
-codetoanalyze/objcpp/pulse/NPEBasic.mm, testCallMethodReturnsnonPODBad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,when calling `SomeObject.returnsnonPOD` here,parameter `self` of SomeObject.returnsnonPOD,invalid access occurs here]
+codetoanalyze/objcpp/pulse/NPEBasic.mm, testCallMethodReturnsnonPODBad, 2, NIL_MESSAGING_TO_NON_POD, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,when calling `SomeObject.returnsnonPOD` here,parameter `self` of SomeObject.returnsnonPOD,invalid access occurs here]
-codetoanalyze/objcpp/pulse/NPEBasic.mm, testNonPODTraceBad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,when calling `SomeObject.returnsNil` here,assigned,is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `SomeObject.returnsNil`,return from call to `SomeObject.returnsNil`,passed as argument to `SomeObject.get`,return from call to `SomeObject.get`,assigned,when calling `SomeObject.returnsnonPOD` here,parameter `self` of SomeObject.returnsnonPOD,invalid access occurs here]
+codetoanalyze/objcpp/pulse/NPEBasic.mm, testCallMethodReturnsnonPODLatent, 7, NIL_MESSAGING_TO_NON_POD, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,when calling `SomeObject.returnsnonPOD` here,parameter `self` of SomeObject.returnsnonPOD,invalid access occurs here]
+codetoanalyze/objcpp/pulse/NPEBasic.mm, testCallMethodReturnsnonPODLatentBad, 1, NIL_MESSAGING_TO_NON_POD, no_bucket, ERROR, [calling context starts here,in call to `testCallMethodReturnsnonPODLatent`,source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,when calling `SomeObject.returnsnonPOD` here,parameter `self` of SomeObject.returnsnonPOD,invalid access occurs here]
+codetoanalyze/objcpp/pulse/NPEBasic.mm, testNonPODTraceBad, 2, NIL_MESSAGING_TO_NON_POD, no_bucket, ERROR, [source of the null value part of the trace starts here,when calling `SomeObject.returnsNil` here,assigned,is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `SomeObject.returnsNil`,return from call to `SomeObject.returnsNil`,passed as argument to `SomeObject.get`,return from call to `SomeObject.get`,assigned,when calling `SomeObject.returnsnonPOD` here,parameter `self` of SomeObject.returnsnonPOD,invalid access occurs here]
 codetoanalyze/objcpp/pulse/NPEBasic.mm, testTraceBad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,passed as argument to `SomeObject.getXPtr`,return from call to `SomeObject.getXPtr`,assigned,invalid access occurs here]
 codetoanalyze/objcpp/pulse/use_after_delete.mm, PulseTest.deref_deleted_in_objc_method_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,when calling `Simple::Simple` here,parameter `__param_0` of Simple::Simple,invalid access occurs here]
 codetoanalyze/objcpp/pulse/use_after_delete.mm, deref_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,when calling `Simple::Simple` here,parameter `__param_0` of Simple::Simple,invalid access occurs here]