From cc8b6fb8c18dae9f5c83f0a05fe19a0e520ddd07 Mon Sep 17 00:00:00 2001 From: Daiva Naudziuniene Date: Wed, 5 May 2021 08:45:08 -0700 Subject: [PATCH] [pulse][nullptr][objc] A separate issue type for nil insertion into collections Reviewed By: jvillard Differential Revision: D28221909 fbshipit-source-id: 49750ceb3 --- infer/man/man1/infer-full.txt | 1 + infer/man/man1/infer-report.txt | 1 + infer/man/man1/infer.txt | 1 + infer/src/base/IssueType.ml | 17 ++++++++++++----- infer/src/base/IssueType.mli | 2 ++ infer/src/pulse/PulseAbductiveDomain.ml | 4 ++-- infer/src/pulse/PulseAbductiveDomain.mli | 7 ++++++- infer/src/pulse/PulseInvalidation.ml | 7 ++++++- infer/src/pulse/PulseInvalidation.mli | 3 ++- infer/src/pulse/PulseModels.ml | 10 ++++++++-- infer/src/pulse/PulseOperations.ml | 10 +++++----- infer/src/pulse/PulseOperations.mli | 10 ++++++++-- .../tests/codetoanalyze/objcpp/pulse/issues.exp | 8 ++++---- 13 files changed, 58 insertions(+), 23 deletions(-) diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index 49bd65d7d..d8e9991e0 100644 --- a/infer/man/man1/infer-full.txt +++ b/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_INSERTION_INTO_COLLECTION (disabled by default), NIL_MESSAGING_TO_NON_POD (disabled by default), NULLPTR_DEREFERENCE (enabled by default), NULL_DEREFERENCE (enabled by default), diff --git a/infer/man/man1/infer-report.txt b/infer/man/man1/infer-report.txt index f3b5826f0..846832c9d 100644 --- a/infer/man/man1/infer-report.txt +++ b/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_INSERTION_INTO_COLLECTION (disabled by default), NIL_MESSAGING_TO_NON_POD (disabled by default), NULLPTR_DEREFERENCE (enabled by default), NULL_DEREFERENCE (enabled by default), diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index e798ae109..8693cb8eb 100644 --- a/infer/man/man1/infer.txt +++ b/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_INSERTION_INTO_COLLECTION (disabled by default), NIL_MESSAGING_TO_NON_POD (disabled by default), NULLPTR_DEREFERENCE (enabled by default), NULL_DEREFERENCE (enabled by default), diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index a34dfb3da..5fa1ff762 100644 --- a/infer/src/base/IssueType.ml +++ b/infer/src/base/IssueType.ml @@ -789,6 +789,18 @@ let mutable_local_variable_in_component_file = [%blob "../../documentation/issues/MUTABLE_LOCAL_VARIABLE_IN_COMPONENT_FILE.md"] +let nil_insertion_into_collection = + register ~enabled:false ~id:"NIL_INSERTION_INTO_COLLECTION" Error Pulse + ~user_documentation:"Inserting nil into a collection is an error in Objective-C." + + +let nil_messaging_to_non_pod = + register ~enabled:false ~id:"NIL_MESSAGING_TO_NON_POD" Error Pulse + ~user_documentation: + "Calling a method that returns a C++ non-POD object on the nil object is undefined behavior \ + in Objective-C++." + + let null_dereference = register ~id:"NULL_DEREFERENCE" Error Biabduction ~user_documentation:"See [NULLPTR_DEREFERENCE](#nullptr_dereference)." @@ -799,11 +811,6 @@ 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"] diff --git a/infer/src/base/IssueType.mli b/infer/src/base/IssueType.mli index f93edf6e9..a5845950b 100644 --- a/infer/src/base/IssueType.mli +++ b/infer/src/base/IssueType.mli @@ -278,6 +278,8 @@ val mutable_local_variable_in_component_file : t val nil_messaging_to_non_pod : t +val nil_insertion_into_collection : t + val null_dereference : t val nullptr_dereference : t diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 94c723399..699211ca3 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -245,10 +245,10 @@ module AddressAttributes = struct if phys_equal new_pre astate.pre then astate else {astate with pre= new_pre} - let check_valid access_trace addr astate = + let check_valid ?must_be_valid_reason 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, None)) astate + abduce_attribute addr (MustBeValid (access_trace, must_be_valid_reason)) astate let check_initialized access_trace addr astate = diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index 04f7c65f3..b5b8edc27 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -115,7 +115,12 @@ module AddressAttributes : sig val add_attrs : AbstractValue.t -> Attributes.t -> t -> t - val check_valid : Trace.t -> AbstractValue.t -> t -> (t, Invalidation.t * Trace.t) result + val check_valid : + ?must_be_valid_reason:Invalidation.must_be_valid_reason + -> Trace.t + -> AbstractValue.t + -> t + -> (t, Invalidation.t * Trace.t) result val check_initialized : Trace.t -> AbstractValue.t -> t -> (t, unit) result diff --git a/infer/src/pulse/PulseInvalidation.ml b/infer/src/pulse/PulseInvalidation.ml index 401a6f408..e3b56fa25 100644 --- a/infer/src/pulse/PulseInvalidation.ml +++ b/infer/src/pulse/PulseInvalidation.ml @@ -52,11 +52,14 @@ type t = | JavaIterator of java_iterator_function [@@deriving compare, equal] -type must_be_valid_reason = SelfOfNonPODReturnMethod [@@deriving compare, equal] +type must_be_valid_reason = SelfOfNonPODReturnMethod | InsertionIntoCollection +[@@deriving compare, equal] let pp_must_be_valid_reason f = function | None -> F.fprintf f "None" + | Some InsertionIntoCollection -> + F.fprintf f "InsertionIntoCollection" | Some SelfOfNonPODReturnMethod -> F.fprintf f "SelfOfNonPODReturnMethod" @@ -69,6 +72,8 @@ let issue_type_of_cause invalidation must_be_valid_reason = match must_be_valid_reason with | None -> IssueType.nullptr_dereference + | Some InsertionIntoCollection -> + IssueType.nil_insertion_into_collection | Some SelfOfNonPODReturnMethod -> IssueType.nil_messaging_to_non_pod ) | ConstantDereference _ -> diff --git a/infer/src/pulse/PulseInvalidation.mli b/infer/src/pulse/PulseInvalidation.mli index 40ee97f07..3119545df 100644 --- a/infer/src/pulse/PulseInvalidation.mli +++ b/infer/src/pulse/PulseInvalidation.mli @@ -40,7 +40,8 @@ val pp : F.formatter -> t -> unit val describe : F.formatter -> t -> unit -type must_be_valid_reason = SelfOfNonPODReturnMethod [@@deriving compare, equal] +type must_be_valid_reason = SelfOfNonPODReturnMethod | InsertionIntoCollection +[@@deriving compare, equal] val pp_must_be_valid_reason : F.formatter -> must_be_valid_reason option -> unit diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index be0e74f92..7387dc326 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -263,10 +263,16 @@ module ObjC = struct fun {location} astate -> let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let<*> astate, _ = - PulseOperations.eval_access Read location (value, event :: value_hist) Dereference astate + PulseOperations.eval_access ~must_be_valid_reason:Invalidation.InsertionIntoCollection Read + location + (value, event :: value_hist) + Dereference astate in let<+> astate, _ = - PulseOperations.eval_access Read location (key, event :: key_hist) Dereference astate + PulseOperations.eval_access ~must_be_valid_reason:Invalidation.InsertionIntoCollection Read + location + (key, event :: key_hist) + Dereference astate in astate end diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index c78be3cdc..2910e5550 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -49,10 +49,10 @@ end include Import -let check_addr_access access_mode location (address, history) astate = +let check_addr_access ?must_be_valid_reason access_mode location (address, history) astate = let access_trace = Trace.Immediate {location; history} in let* astate = - AddressAttributes.check_valid access_trace address astate + AddressAttributes.check_valid ?must_be_valid_reason access_trace address astate |> Result.map_error ~f:(fun (invalidation, invalidation_trace) -> ReportableError { diagnostic= @@ -61,7 +61,7 @@ let check_addr_access access_mode location (address, history) astate = ; invalidation ; invalidation_trace ; access_trace - ; must_be_valid_reason= None } + ; must_be_valid_reason } ; astate } ) in match access_mode with @@ -173,8 +173,8 @@ end let eval_var location hist var astate = Stack.eval location hist var astate -let eval_access mode location addr_hist access astate = - let+ astate = check_addr_access mode location addr_hist astate in +let eval_access ?must_be_valid_reason mode location addr_hist access astate = + let+ astate = check_addr_access ?must_be_valid_reason mode location addr_hist astate in Memory.eval_edge addr_hist access astate diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index 41d423bc4..bfd63fec8 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -67,7 +67,12 @@ include module type of Import type t = AbductiveDomain.t val check_addr_access : - access_mode -> Location.t -> AbstractValue.t * ValueHistory.t -> t -> t AccessResult.t + ?must_be_valid_reason:Invalidation.must_be_valid_reason + -> access_mode + -> Location.t + -> AbstractValue.t * ValueHistory.t + -> t + -> t AccessResult.t (** Check that the [address] is not known to be invalid *) module Closures : sig @@ -101,7 +106,8 @@ val eval_deref_isl : Location.t -> Exp.t -> t -> (t * (AbstractValue.t * ValueHistory.t)) AccessResult.t list val eval_access : - access_mode + ?must_be_valid_reason:Invalidation.must_be_valid_reason + -> access_mode -> Location.t -> AbstractValue.t * ValueHistory.t -> BaseMemory.Access.t diff --git a/infer/tests/codetoanalyze/objcpp/pulse/issues.exp b/infer/tests/codetoanalyze/objcpp/pulse/issues.exp index ad5ca695d..3567ad5d6 100644 --- a/infer/tests/codetoanalyze/objcpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/objcpp/pulse/issues.exp @@ -1,13 +1,13 @@ 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, addNilInDictBad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,passed as argument to `NSMutableDictionary.setObject:forKey:` (modelled),return from call to `NSMutableDictionary.setObject:forKey:` (modelled),invalid access occurs here] -codetoanalyze/objcpp/pulse/NPEBasic.mm, addObjectKeyNilInDictBad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,passed as argument to `NSMutableDictionary.setObject:forKey:` (modelled),return from call to `NSMutableDictionary.setObject:forKey:` (modelled),invalid access occurs here] +codetoanalyze/objcpp/pulse/NPEBasic.mm, addNilInDictBad, 2, NIL_INSERTION_INTO_COLLECTION, no_bucket, ERROR, [is the null pointer,assigned,passed as argument to `NSMutableDictionary.setObject:forKey:` (modelled),return from call to `NSMutableDictionary.setObject:forKey:` (modelled),invalid access occurs here] +codetoanalyze/objcpp/pulse/NPEBasic.mm, addObjectKeyNilInDictBad, 2, NIL_INSERTION_INTO_COLLECTION, no_bucket, ERROR, [is the null pointer,passed as argument to `NSMutableDictionary.setObject:forKey:` (modelled),return from call to `NSMutableDictionary.setObject:forKey:` (modelled),invalid access occurs here] codetoanalyze/objcpp/pulse/NPEBasic.mm, dereferenceNilBad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/objcpp/pulse/NPEBasic.mm, testAccessPropertyAccessorBad, 2, NIL_MESSAGING_TO_NON_POD, no_bucket, ERROR, [is the null pointer,assigned,when calling `SomeObject.ptr` here,parameter `self` of SomeObject.ptr,invalid access occurs here] codetoanalyze/objcpp/pulse/NPEBasic.mm, testCallMethodReturnsnonPODBad, 2, NIL_MESSAGING_TO_NON_POD, no_bucket, ERROR, [is the null pointer,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 ***,is the null pointer,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`,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, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,when calling `addObjectInDict` here,parameter `value` of addObjectInDict,passed as argument to `NSMutableDictionary.setObject:forKey:` (modelled),return from call to `NSMutableDictionary.setObject:forKey:` (modelled),invalid access occurs here] -codetoanalyze/objcpp/pulse/NPEBasic.mm, testNilMessagingForModelNotNilDictBad, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,when calling `addObjectInDict` here,parameter `value` of addObjectInDict,passed as argument to `NSMutableDictionary.setObject:forKey:` (modelled),return from call to `NSMutableDictionary.setObject:forKey:` (modelled),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,passed as argument to `NSMutableDictionary.setObject:forKey:` (modelled),return from 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,passed as argument to `NSMutableDictionary.setObject:forKey:` (modelled),return from 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, [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, [is the null pointer,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]