[cost] add inferbo model for init function of NSString and NSArray

Summary: As title

Reviewed By: ezgicicek

Differential Revision: D22844475

fbshipit-source-id: 0eb757bb0

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -1045,6 +1045,16 @@ module NSCollection = struct
         ~last_included:true mem location cond_set
     in
     {exec; check}
+
+
+  let copy coll_id src_exp =
+    let exec model_env ~ret:((id, _) as ret) mem =
+      let coll = Dom.Mem.find_stack (Loc.of_id coll_id) mem in
+      let set_length = Collection.eval_collection_length src_exp mem |> Dom.Val.get_itv in
+      Collection.change_size_by ~size_f:(fun _ -> set_length) coll_id model_env ~ret mem
+      |> model_by_value coll id
+    in
+    {exec; check= no_check}
 end
 
 module JavaClass = struct
@@ -1334,6 +1344,29 @@ module NSString = struct
     {exec; check= no_check}
 
 
+  let init_with_string tgt_exp src_exp =
+    let {exec= copy_exec; check= _} = JavaString.copy_constructor tgt_exp src_exp in
+    let exec ({integer_type_widths} as model_env) ~ret:((id, _) as ret) mem =
+      let mem = copy_exec model_env ~ret mem in
+      let v = Sem.eval integer_type_widths tgt_exp mem in
+      model_by_value v id mem
+    in
+    {exec; check= no_check}
+
+
+  let init_with_c_string_with_len tgt_exp src_exp len_exp =
+    let exec ({integer_type_widths; location} as model_env) ~ret:(id, _) mem =
+      let len_v = Sem.eval integer_type_widths len_exp mem in
+      let tgt_v = Sem.eval integer_type_widths tgt_exp mem in
+      let tgt_deref = Dom.Val.get_all_locs tgt_v in
+      let tgt_arr_loc = JavaString.deref_of model_env tgt_exp mem in
+      ArrObjCommon.constructor_from_char_ptr model_env tgt_deref ~fn src_exp mem
+      |> Dom.Mem.transform_mem ~f:(Dom.Val.set_array_length location ~length:len_v) tgt_arr_loc
+      |> model_by_value tgt_v id
+    in
+    {exec; check= no_check}
+
+
   let substring_from_index = JavaString.substring_no_end
 
   let length = JavaString.length
@@ -1527,6 +1560,11 @@ module Call = struct
       ; -"MCFArrayGetCount" <>$ capt_exp $!--> Collection.size
       ; +PatternMatch.ObjectiveC.implements "NSArray" &:: "init" <>$ capt_exp $--> id
       ; +PatternMatch.ObjectiveC.implements "NSArray" &:: "array" <>--> Collection.new_collection
+      ; +PatternMatch.ObjectiveC.implements "NSArray"
+        &:: "initWithArray:" <>$ capt_var_exn $+ capt_exp $--> NSCollection.copy
+      ; +PatternMatch.ObjectiveC.implements "NSArray"
+        &:: "initWithArray:copyItems:" <>$ capt_var_exn $+ capt_exp $+ any_arg
+        $--> NSCollection.copy
       ; +PatternMatch.ObjectiveC.implements "NSArray" &:: "count" <>$ capt_exp $!--> Collection.size
       ; +PatternMatch.ObjectiveC.implements "NSArray"
         &:: "objectAtIndexedSubscript:" <>$ capt_var_exn $+ capt_exp $!--> Collection.get_at_index
@@ -1561,6 +1599,11 @@ module Call = struct
         &:: "appendString:" <>$ capt_exp $+ capt_exp $--> NSString.append_string
       ; +PatternMatch.ObjectiveC.implements "NSString"
         &:: "componentsSeparatedByString:" <>$ capt_exp $+ any_arg $--> NSString.split
+      ; +PatternMatch.ObjectiveC.implements "NSString"
+        &:: "initWithString:" <>$ capt_exp $+ capt_exp $--> NSString.init_with_string
+      ; +PatternMatch.ObjectiveC.implements "NSString"
+        &:: "initWithBytes:length:encoding:" <>$ capt_exp $+ capt_exp $+ capt_exp $+ any_arg
+        $!--> NSString.init_with_c_string_with_len
       ; (* C++ models *)
         -"boost" &:: "split"
         $ capt_arg_of_typ (-"std" &:: "vector")

infer/tests/codetoanalyze/objc/performance/NSArray.m

@@ -22,19 +22,19 @@ void nsarray_init_constant() {
   }
 }
 
-void nsarray_init_with_array_linear_FP(NSArray* array) {
+void nsarray_init_with_array_linear(NSArray* array) {
   NSArray* ref_array = [[NSArray alloc] initWithArray:array];
 
   for (int i = 0; i < ref_array.count; i++) {
   }
 }
 
-void nsarray_init_with_array_constant_FP() {
+void nsarray_init_with_array_constant() {
   NSArray* array = [[NSArray alloc] init];
-  nsarray_init_with_array_linear_FP(array);
+  nsarray_init_with_array_linear(array);
 }
 
-void nsarray_init_with_array_copy_linear_FP(NSArray* array) {
+void nsarray_init_with_array_copy_linear(NSArray* array) {
   NSArray* copy_array = [[NSArray alloc] initWithArray:array copyItems:YES];
   for (int i = 0; i < copy_array.count; i++) {
   }

infer/tests/codetoanalyze/objc/performance/NSString.m

@@ -53,7 +53,7 @@ void call_component_separated_by_char_constant() {
   component_seperated_by_char_linear(s);
 }
 
-void init_with_bytes_linear_FP(const void* bytes,
+void init_with_bytes_linear(const void* bytes,
                             NSUInteger length,
                             NSStringEncoding encoding) {
   NSString* s = [[NSString alloc] initWithBytes:bytes
@@ -69,22 +69,22 @@ void init_string_constant() {
   }
 }
 
-void init_with_string_constant_FP() {
+void init_with_string_constant() {
   NSString* s = @"abcd";
   NSString* str = [[NSString alloc] initWithString:s];
   for (int i = 0; i < str.length; i++) {
   }
 }
 
-void init_with_string_linear_FP(NSString* s) {
+void init_with_string_linear(NSString* s) {
   NSString* str = [[NSString alloc] initWithString:s];
   for (int i = 0; i < str.length; i++) {
   }
 }
 
-void call_init_with_string_constant_FP() {
+void call_init_with_string_constant() {
   NSString* s = [[NSString alloc] init];
-  init_with_string_linear_FP(s);
+  init_with_string_linear(s);
 }
 
 void substring_no_end_linear(NSString* s, int x) {

infer/tests/codetoanalyze/objc/performance/cost-issues.exp

@@ -11,9 +11,9 @@ codetoanalyze/objc/performance/NSArray.m, nsarray_enumerator_linear_FN, 14,  OnU
 codetoanalyze/objc/performance/NSArray.m, nsarray_find_linear, 4 + 9 ⋅ array.length.ub + 3 ⋅ (array.length.ub + 1),  OnUIThread:false, [{array.length.ub + 1},Loop,{array.length.ub},Loop]
 codetoanalyze/objc/performance/NSArray.m, nsarray_first_object_constant, 4,  OnUIThread:false, []
 codetoanalyze/objc/performance/NSArray.m, nsarray_init_constant, 9,  OnUIThread:false, []
-codetoanalyze/objc/performance/NSArray.m, nsarray_init_with_array_constant_FP, ⊤,  OnUIThread:false, [Call to nsarray_init_with_array_linear_FP,Unbounded loop,Loop]
+codetoanalyze/objc/performance/NSArray.m, nsarray_init_with_array_constant, 15,  OnUIThread:false, []
-codetoanalyze/objc/performance/NSArray.m, nsarray_init_with_array_copy_linear_FP, ⊤,  OnUIThread:false, [Unbounded loop,Loop]
+codetoanalyze/objc/performance/NSArray.m, nsarray_init_with_array_copy_linear, 7 + 3 ⋅ array.length.ub + 3 ⋅ (array.length.ub + 1),  OnUIThread:false, [{array.length.ub + 1},Loop,{array.length.ub},Loop]
-codetoanalyze/objc/performance/NSArray.m, nsarray_init_with_array_linear_FP, ⊤,  OnUIThread:false, [Unbounded loop,Loop]
+codetoanalyze/objc/performance/NSArray.m, nsarray_init_with_array_linear, 7 + 3 ⋅ array.length.ub + 3 ⋅ (array.length.ub + 1),  OnUIThread:false, [{array.length.ub + 1},Loop,{array.length.ub},Loop]
 codetoanalyze/objc/performance/NSArray.m, nsarray_init_with_objects_constant, 39,  OnUIThread:false, []
 codetoanalyze/objc/performance/NSArray.m, nsarray_is_equal_to_array_linear_FN, 5,  OnUIThread:false, []
 codetoanalyze/objc/performance/NSArray.m, nsarray_iterate_linear_FN, 14,  OnUIThread:false, []
@@ -51,14 +51,14 @@ codetoanalyze/objc/performance/NSMutableDictionary.m, nsmutabledictionary_set_el
 codetoanalyze/objc/performance/NSMutableString.m, nsmstring_append_string_constant, 14 + 3 ⋅ (str.length.ub + 5) + 3 ⋅ (str.length.ub + 6),  OnUIThread:false, [{str.length.ub + 6},Loop,{str.length.ub + 5},Loop]
 codetoanalyze/objc/performance/NSMutableString.m, nsmstring_append_string_linear, 5 + str2.length.ub + 3 ⋅ (str2.length.ub + str1.length.ub) + 3 ⋅ (str2.length.ub + str1.length.ub + 1),  OnUIThread:false, [{str2.length.ub + str1.length.ub + 1},Loop,{str2.length.ub + str1.length.ub},Loop,{str2.length.ub},Modeled call to NSMutableString.appendString:]
 codetoanalyze/objc/performance/NSString.m, call_component_separated_by_char_constant, 46,  OnUIThread:false, []
-codetoanalyze/objc/performance/NSString.m, call_init_with_string_constant_FP, ⊤,  OnUIThread:false, [Call to init_with_string_linear_FP,Unbounded loop,Loop]
+codetoanalyze/objc/performance/NSString.m, call_init_with_string_constant, 15,  OnUIThread:false, []
 codetoanalyze/objc/performance/NSString.m, component_seperated_by_char_linear, 6 + m.length.ub + 3 ⋅ (-1+max(2, m.length.ub)) + 3 ⋅ (max(2, m.length.ub)),  OnUIThread:false, [{max(2, m.length.ub)},Loop,{-1+max(2, m.length.ub)},Loop,{m.length.ub},Modeled call to NSString.componentsSeparatedByString:]
 codetoanalyze/objc/performance/NSString.m, component_seperated_by_string_linear, 6 + sep.length.ub × m.length.ub + 3 ⋅ (-1+max(2, m.length.ub)) + 3 ⋅ (max(2, m.length.ub)),  OnUIThread:false, [{max(2, m.length.ub)},Loop,{-1+max(2, m.length.ub)},Loop,{m.length.ub},Modeled call to NSString.componentsSeparatedByString:,{sep.length.ub},Modeled call to NSString.componentsSeparatedByString:]
 codetoanalyze/objc/performance/NSString.m, has_prefix_constant, 13,  OnUIThread:false, []
 codetoanalyze/objc/performance/NSString.m, init_string_constant, 9,  OnUIThread:false, []
-codetoanalyze/objc/performance/NSString.m, init_with_bytes_linear_FP, ⊤,  OnUIThread:false, [Unbounded loop,Loop]
+codetoanalyze/objc/performance/NSString.m, init_with_bytes_linear, 9 + 3 ⋅ length + 3 ⋅ (length + 1),  OnUIThread:false, [{length + 1},Loop,{length},Loop]
-codetoanalyze/objc/performance/NSString.m, init_with_string_constant_FP, ⊤,  OnUIThread:false, [Unbounded loop,Loop]
+codetoanalyze/objc/performance/NSString.m, init_with_string_constant, 39,  OnUIThread:false, []
-codetoanalyze/objc/performance/NSString.m, init_with_string_linear_FP, ⊤,  OnUIThread:false, [Unbounded loop,Loop]
+codetoanalyze/objc/performance/NSString.m, init_with_string_linear, 7 + 3 ⋅ s.length.ub + 3 ⋅ (s.length.ub + 1),  OnUIThread:false, [{s.length.ub + 1},Loop,{s.length.ub},Loop]
 codetoanalyze/objc/performance/NSString.m, rangeof_character_from_set_linear, 5 + m.length.ub,  OnUIThread:false, [{m.length.ub},Modeled call to NSString.rangeOfString:]
 codetoanalyze/objc/performance/NSString.m, rangeof_string_quadratic, 5 + n.length.ub × m.length.ub,  OnUIThread:false, [{m.length.ub},Modeled call to NSString.rangeOfString:,{n.length.ub},Modeled call to NSString.rangeOfString:]
 codetoanalyze/objc/performance/NSString.m, replace_linear_FP, ⊤,  OnUIThread:false, [Unbounded loop,Loop]

infer/tests/codetoanalyze/objc/performance/issues.exp

@@ -1,11 +1,6 @@
 codetoanalyze/objc/performance/NSArray.m, nsarray_empty_array_constant, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/objc/performance/NSArray.m, nsarray_enumerator_linear_FN, 7, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Unknown value from: NSEnumerator.nextObject,Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed64]
 codetoanalyze/objc/performance/NSArray.m, nsarray_init_constant, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
-codetoanalyze/objc/performance/NSArray.m, nsarray_init_with_array_constant_FP, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Call to nsarray_init_with_array_linear_FP,Unbounded loop,Loop]
-codetoanalyze/objc/performance/NSArray.m, nsarray_init_with_array_copy_linear_FP, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop]
-codetoanalyze/objc/performance/NSArray.m, nsarray_init_with_array_copy_linear_FP, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Unknown value from: NSArray.initWithArray:copyItems:,Binary operation: ([0, +oo] + 1):signed32]
-codetoanalyze/objc/performance/NSArray.m, nsarray_init_with_array_linear_FP, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop]
-codetoanalyze/objc/performance/NSArray.m, nsarray_init_with_array_linear_FP, 3, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Unknown value from: NSArray.initWithArray:,Binary operation: ([0, +oo] + 1):signed32]
 codetoanalyze/objc/performance/NSArray.m, nsarray_iterate_linear_FN, 3, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Unknown value from: NSEnumerator.nextObject,Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed64]
 codetoanalyze/objc/performance/NSDictionary.m, nsdictionary_enumerate_constant, 6, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Offset trace>,Unknown value from: NSEnumerator.nextObject,Assignment,<Length trace>,Unknown value from: NSEnumerator.nextObject,Array access: Offset: [-oo, +oo] (⇐ [-oo, +oo] + [-oo, +oo]) Size: [0, +oo]]
 codetoanalyze/objc/performance/NSDictionary.m, nsdictionary_find_key_linear_FN, 3, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Offset trace>,Unknown value from: NSEnumerator.nextObject,Assignment,<Length trace>,Unknown value from: NSEnumerator.nextObject,Array access: Offset: [-oo, +oo] (⇐ [-oo, +oo] + [-oo, +oo]) Size: [0, +oo]]
@@ -19,14 +14,7 @@ codetoanalyze/objc/performance/NSMutableArray.m, nsmarray_remove_constant, 5, BU
 codetoanalyze/objc/performance/NSMutableArray.m, nsmarray_remove_in_loop_constant, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/objc/performance/NSMutableArray.m, nsmarray_set_in_loop_constant, 6, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/objc/performance/NSMutableArray.m, nsmarray_set_linear, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Unknown value from: NSNumber.intValue,Binary operation: ([-oo, +oo] + 1):signed32]
-codetoanalyze/objc/performance/NSString.m, call_init_with_string_constant_FP, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Call to init_with_string_linear_FP,Unbounded loop,Loop]
 codetoanalyze/objc/performance/NSString.m, init_string_constant, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
-codetoanalyze/objc/performance/NSString.m, init_with_bytes_linear_FP, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop]
-codetoanalyze/objc/performance/NSString.m, init_with_bytes_linear_FP, 6, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Unknown value from: NSString.initWithBytes:length:encoding:,Binary operation: ([0, +oo] + 1):signed32]
-codetoanalyze/objc/performance/NSString.m, init_with_string_constant_FP, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop]
-codetoanalyze/objc/performance/NSString.m, init_with_string_constant_FP, 3, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Unknown value from: NSString.initWithString:,Binary operation: ([0, +oo] + 1):signed32]
-codetoanalyze/objc/performance/NSString.m, init_with_string_linear_FP, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop]
-codetoanalyze/objc/performance/NSString.m, init_with_string_linear_FP, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Unknown value from: NSString.initWithString:,Binary operation: ([0, +oo] + 1):signed32]
 codetoanalyze/objc/performance/NSString.m, replace_linear_FP, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop]
 codetoanalyze/objc/performance/NSString.m, replace_linear_FP, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Unknown value from: NSString.stringByReplacingOccurrencesOfString:withString:,Binary operation: ([0, +oo] + 1):signed32]
 codetoanalyze/objc/performance/block.m, objc_blockblock_multiply_array_linear_FN_1, 3, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Unknown value from: NSEnumerator.nextObject,Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed64]