diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 91a155ce1..09c6e7f5c 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -252,6 +252,18 @@ module ObjC = struct PulseCallOperations.call tenv ~caller_proc_desc:proc_desc ~callee_data:(analyze_dependency callee_proc_name) location callee_proc_name ~ret ~actuals:[] ~formals_opt:None astate ) + + + let insertion_into_dictionary (value, value_hist) (key, key_hist) ~desc : model = + 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 + in + let<+> astate, _ = + PulseOperations.eval_access Read location (key, event :: key_hist) Dereference astate + in + astate end module Optional = struct @@ -1694,6 +1706,9 @@ module ProcNameDispatcher = struct <>$ capt_exp $--> ObjC.alloc_not_null_alloc_ev ~desc:"alloc" ; -"NSObject" &:: "init" <>$ capt_arg_payload $--> Misc.id_first_arg ~desc:"NSObject.init" + ; +map_context_tenv (PatternMatch.ObjectiveC.implements "NSMutableDictionary") + &:: "setObject:forKey:" <>$ any_arg $+ capt_arg_payload $+ capt_arg_payload + $--> ObjC.insertion_into_dictionary ~desc:"NSMutableDictionary.setObject:forKey:" ; +match_regexp_opt Config.pulse_model_return_nonnull &::.*--> Misc.return_positive ~desc:"modelled as returning not null due to configuration option" diff --git a/infer/tests/codetoanalyze/objcpp/pulse/NPEBasic.mm b/infer/tests/codetoanalyze/objcpp/pulse/NPEBasic.mm index ef7b7ebcf..dc20d77fd 100644 --- a/infer/tests/codetoanalyze/objcpp/pulse/NPEBasic.mm +++ b/infer/tests/codetoanalyze/objcpp/pulse/NPEBasic.mm @@ -169,3 +169,36 @@ void testUnknownNilSpecOk() { }; NSDictionary* dict = @{@"helloString" : str}; } + +void addNilInDictBad(NSMutableDictionary* mDict) { + id value = nil; + [mDict setObject:value forKey:@"somestring"]; +} + +void addNSNullInDictOk(NSMutableDictionary* mDict) { + [mDict setObject:[NSNull null] forKey:@"somestring"]; +} + +void addObjectInDictOk(NSMutableDictionary* mDict) { + SomeObject* o = [SomeObject new]; + [mDict setObject:o forKey:@"somestring"]; +} + +void addObjectKeyNilInDictBad(NSMutableDictionary* mDict) { + SomeObject* o = [SomeObject new]; + [mDict setObject:o forKey:nil]; +} + +void addObjectInDict(NSMutableDictionary* mDict, id value) { + [mDict setObject:value forKey:@"somestring"]; +} + +void testNilMessagingForModelNilNilOK_FP() { addObjectInDict(nil, nil); } + +void testNilMessagingForModelNilStringOK() { + addObjectInDict(nil, @"somestring"); +} + +void testNilMessagingForModelNotNilDictBad(NSMutableDictionary* mDict) { + addObjectInDict(mDict, nil); +} diff --git a/infer/tests/codetoanalyze/objcpp/pulse/issues.exp b/infer/tests/codetoanalyze/objcpp/pulse/issues.exp index 9781f47f9..ad5ca695d 100644 --- a/infer/tests/codetoanalyze/objcpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/objcpp/pulse/issues.exp @@ -1,9 +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, 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, 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]