From c8771a3eeb237e2e9251c20dae3a43dfddfb5a2e Mon Sep 17 00:00:00 2001 From: Daiva Naudziuniene Date: Mon, 24 May 2021 01:41:56 -0700 Subject: [PATCH] [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 | 14 ++++++++++---- infer/src/pulse/PulseValueHistory.ml | 5 +++++ infer/src/pulse/PulseValueHistory.mli | 1 + infer/tests/codetoanalyze/objcpp/pulse/issues.exp | 4 ++-- 4 files changed, 18 insertions(+), 6 deletions(-) diff --git a/infer/src/pulse/PulseObjectiveCSummary.ml b/infer/src/pulse/PulseObjectiveCSummary.ml index e3a753432..87e87f3ec 100644 --- a/infer/src/pulse/PulseObjectiveCSummary.ml +++ b/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 = diff --git a/infer/src/pulse/PulseValueHistory.ml b/infer/src/pulse/PulseValueHistory.ml index 39edf13bd..7f63b21d0 100644 --- a/infer/src/pulse/PulseValueHistory.ml +++ b/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) diff --git a/infer/src/pulse/PulseValueHistory.mli b/infer/src/pulse/PulseValueHistory.mli index 956855334..ec424f226 100644 --- a/infer/src/pulse/PulseValueHistory.mli +++ b/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 diff --git a/infer/tests/codetoanalyze/objcpp/pulse/issues.exp b/infer/tests/codetoanalyze/objcpp/pulse/issues.exp index 4f7a8a38a..3f88bfa03 100644 --- a/infer/tests/codetoanalyze/objcpp/pulse/issues.exp +++ b/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]