[pulse][objc][nullptr] Model NSArray methods to catch nil insertion into collection issues

Reviewed By: jvillard

Differential Revision: D28257293

fbshipit-source-id: c9808ebf8

infer/src/pulse/PulseModels.ml

@@ -265,18 +265,27 @@ module ObjC = struct
    fun {location} astate ->
     let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
     let<*> astate, _ =
-      PulseOperations.eval_access ~must_be_valid_reason:Invalidation.InsertionIntoCollection Read
+      PulseOperations.eval_access ~must_be_valid_reason:InsertionIntoCollection Read location
-        location
         (value, event :: value_hist)
         Dereference astate
     in
     let<+> astate, _ =
-      PulseOperations.eval_access ~must_be_valid_reason:Invalidation.InsertionIntoCollection Read
+      PulseOperations.eval_access ~must_be_valid_reason:InsertionIntoCollection Read location
-        location
         (key, event :: key_hist)
         Dereference astate
     in
     astate
+
+
+  let insertion_into_array (value, value_hist) ~desc : model =
+   fun {location} astate ->
+    let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
+    let<+> astate, _ =
+      PulseOperations.eval_access ~must_be_valid_reason:InsertionIntoCollection Read location
+        (value, event :: value_hist)
+        Dereference astate
+    in
+    astate
 end
 
 module Optional = struct
@@ -1738,6 +1747,15 @@ module ProcNameDispatcher = struct
         ; +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:"
+        ; +map_context_tenv (PatternMatch.ObjectiveC.implements "NSMutableArray")
+          &:: "addObject:" <>$ any_arg $+ capt_arg_payload
+          $--> ObjC.insertion_into_array ~desc:"NSMutableArray.addObject:"
+        ; +map_context_tenv (PatternMatch.ObjectiveC.implements "NSMutableArray")
+          &:: "insertObject:atIndex:" <>$ any_arg $+ capt_arg_payload $+ any_arg
+          $--> ObjC.insertion_into_array ~desc:"NSMutableArray.insertObject:atIndex:"
+        ; +map_context_tenv (PatternMatch.ObjectiveC.implements "NSMutableArray")
+          &:: "replaceObjectAtIndex:withObject:" <>$ any_arg $+ any_arg $+ capt_arg_payload
+          $--> ObjC.insertion_into_array ~desc:"NSMutableArray.replaceObjectAtIndex:withObject:"
         ; +match_regexp_opt Config.pulse_model_return_nonnull
           &::.*--> Misc.return_positive
                      ~desc:"modelled as returning not null due to configuration option"

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

@@ -202,3 +202,25 @@ void testNilMessagingForModelNilStringOK() {
 void testNilMessagingForModelNotNilDictBad(NSMutableDictionary* mDict) {
   addObjectInDict(mDict, nil);
 }
+
+void addNilInArrayBad(NSMutableArray* mArray) { [mArray addObject:nil]; }
+
+void addObjectInArrayOk(NSMutableArray* mArray) {
+  [mArray addObject:[SomeObject new]];
+}
+
+void insertNilInArrayBad(NSMutableArray* mArray) {
+  [mArray insertObject:nil atIndex:0];
+}
+
+void insertObjectInArrayOk(NSMutableArray* mArray) {
+  [mArray insertObject:[SomeObject new] atIndex:0];
+}
+
+void replaceNilInArrayBad(NSMutableArray* mArray) {
+  [mArray replaceObjectAtIndex:0 withObject:nil];
+}
+
+void replaceObjectInArrayOk(NSMutableArray* mArray) {
+  [mArray replaceObjectAtIndex:0 withObject:[SomeObject new]];
+}

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

@@ -1,7 +1,10 @@
 codetoanalyze/objcpp/pulse/AllocPatternMemLeak.mm, A.create_no_release_leak_bad, 2, 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, addNilInArrayBad, 0, NIL_INSERTION_INTO_COLLECTION, no_bucket, ERROR, [is the null pointer,passed as argument to `NSMutableArray.addObject:` (modelled),return from call to `NSMutableArray.addObject:` (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, insertNilInArrayBad, 1, NIL_INSERTION_INTO_COLLECTION, no_bucket, ERROR, [is the null pointer,passed as argument to `NSMutableArray.insertObject:atIndex:` (modelled),return from call to `NSMutableArray.insertObject:atIndex:` (modelled),invalid access occurs here]
+codetoanalyze/objcpp/pulse/NPEBasic.mm, replaceNilInArrayBad, 1, NIL_INSERTION_INTO_COLLECTION, no_bucket, ERROR, [is the null pointer,passed as argument to `NSMutableArray.replaceObjectAtIndex:withObject:` (modelled),return from call to `NSMutableArray.replaceObjectAtIndex:withObject:` (modelled),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]