[pulse][objc][nullptr] Improve nil messaging traces

Summary: Improve error trace by adding a nil messaging event when we apply nil summary

Reviewed By: jvillard

Differential Revision: D28603845

fbshipit-source-id: facaec6fd

infer/src/pulse/PulseObjectiveCSummary.ml

@@ -41,19 +41,25 @@ let mk_objc_method_nil_summary_aux tenv proc_desc astate =
      This allows us to connect invalidation with invalid access in the trace *)
   let location = Procdesc.get_loc proc_desc in
   let self = mk_objc_self_pvar proc_desc in
-  let* astate, self_value = PulseOperations.eval_deref location (Lvar self) astate in
-  let* astate = PulseArithmetic.prune_eq_zero (fst self_value) astate in
+  let* astate, (self_value, self_history) =
+    PulseOperations.eval_deref location (Lvar self) astate
+  in
+  let* astate = PulseArithmetic.prune_eq_zero self_value astate in
+  let event = ValueHistory.NilMessaging location in
+  let updated_self_value_hist = (self_value, event :: self_history) in
   match List.last (Procdesc.get_formals proc_desc) with
   | Some (last_formal, {desc= Tptr (typ, _)}) when Mangled.is_return_param last_formal ->
       let ret_param_var = Procdesc.get_ret_param_var proc_desc in
       let* astate, ret_param_var_addr_hist =
         PulseOperations.eval_deref location (Lvar ret_param_var) astate
       in
-      init_fields_zero tenv location ~zero:self_value ret_param_var_addr_hist typ astate
+      init_fields_zero tenv location ~zero:updated_self_value_hist ret_param_var_addr_hist typ
+        astate
   | _ ->
       let ret_var = Procdesc.get_ret_var proc_desc in
       let* astate, ret_var_addr_hist = PulseOperations.eval Write location (Lvar ret_var) astate in
-      PulseOperations.write_deref location ~ref:ret_var_addr_hist ~obj:self_value astate
+      PulseOperations.write_deref location ~ref:ret_var_addr_hist ~obj:updated_self_value_hist
+        astate
 
 
 let mk_objc_method_nil_summary tenv proc_desc initial =

infer/src/pulse/PulseValueHistory.ml

@@ -19,6 +19,7 @@ type event =
   | CppTemporaryCreated of Location.t
   | FormalDeclared of Pvar.t * Location.t
   | Invalidated of PulseInvalidation.t * Location.t
+  | NilMessaging of Location.t
   | Returned of Location.t
   | StructFieldAddressCreated of Fieldname.t RevList.t * Location.t
   | VariableAccessed of Pvar.t * Location.t
@@ -38,6 +39,7 @@ let rec iter_event event ~f =
   | CppTemporaryCreated _
   | FormalDeclared _
   | Invalidated _
+  | NilMessaging _
   | Returned _
   | StructFieldAddressCreated _
   | VariableAccessed _
@@ -85,6 +87,8 @@ let pp_event_no_location fmt event =
       F.fprintf fmt "parameter `%a`%a" Pvar.pp_value_non_verbose pvar pp_proc pvar
   | Invalidated (invalidation, _) ->
       Invalidation.describe fmt invalidation
+  | NilMessaging _ ->
+      F.pp_print_string fmt "a message sent to nil returns nil"
   | Returned _ ->
       F.pp_print_string fmt "returned"
   | StructFieldAddressCreated (field_names, _) ->
@@ -104,6 +108,7 @@ let location_of_event = function
   | CppTemporaryCreated location
   | FormalDeclared (_, location)
   | Invalidated (_, location)
+  | NilMessaging location
   | Returned location
   | StructFieldAddressCreated (_, location)
   | VariableAccessed (_, location)

infer/src/pulse/PulseValueHistory.mli

@@ -17,6 +17,7 @@ type event =
   | CppTemporaryCreated of Location.t
   | FormalDeclared of Pvar.t * Location.t
   | Invalidated of PulseInvalidation.t * Location.t
+  | NilMessaging of Location.t
   | Returned of Location.t
   | StructFieldAddressCreated of Fieldname.t RevList.t * Location.t
   | VariableAccessed of Pvar.t * Location.t

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

@@ -28,7 +28,7 @@ codetoanalyze/objcpp/pulse/NPEBasic.mm, testCallMethodReturnsnonPODLatent, 7, NI
 codetoanalyze/objcpp/pulse/NPEBasic.mm, testCallMethodReturnsnonPODLatentBad, 1, NIL_MESSAGING_TO_NON_POD, no_bucket, ERROR, [calling context starts here,in call to `testCallMethodReturnsnonPODLatent`,null pointer dereference part of the trace starts here,is the null pointer,assigned,when calling `SomeObject.returnsnonPOD` here,parameter `self` of SomeObject.returnsnonPOD,invalid access occurs here]
 codetoanalyze/objcpp/pulse/NPEBasic.mm, testNilMessagingForModelNilNilOK_FP, 0, NIL_INSERTION_INTO_COLLECTION, no_bucket, ERROR, [is the null pointer,when calling `addObjectInDict` here,parameter `value` of addObjectInDict,in call to `NSMutableDictionary.setObject:forKey:` (modelled),invalid access occurs here]
 codetoanalyze/objcpp/pulse/NPEBasic.mm, testNilMessagingForModelNotNilDictBad, 1, NIL_INSERTION_INTO_COLLECTION, no_bucket, ERROR, [is the null pointer,when calling `addObjectInDict` here,parameter `value` of addObjectInDict,in call to `NSMutableDictionary.setObject:forKey:` (modelled),invalid access occurs here]
-codetoanalyze/objcpp/pulse/NPEBasic.mm, testNonPODTraceBad, 2, NIL_MESSAGING_TO_NON_POD, no_bucket, ERROR, [in call to `SomeObject.returnsNil`,is the null pointer,returned,return from call to `SomeObject.returnsNil`,in call to `SomeObject.get`,parameter `self` of 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, [is the null pointer,assigned,in call to `SomeObject.getXPtr`,parameter `self` of SomeObject.getXPtr,return from call to `SomeObject.getXPtr`,assigned,invalid access occurs here]
+codetoanalyze/objcpp/pulse/NPEBasic.mm, testNonPODTraceBad, 2, NIL_MESSAGING_TO_NON_POD, no_bucket, ERROR, [in call to `SomeObject.returnsNil`,is the null pointer,returned,return from call to `SomeObject.returnsNil`,in call to `SomeObject.get`,parameter `self` of SomeObject.get,a message sent to nil returns nil,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, [is the null pointer,assigned,in call to `SomeObject.getXPtr`,parameter `self` of SomeObject.getXPtr,a message sent to nil returns nil,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,allocated by call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,allocated by 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,allocated by call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,allocated by call to `new` (modelled),assigned,when calling `Simple::Simple` here,parameter `__param_0` of Simple::Simple,invalid access occurs here]