diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 3f64cefa5..eab7f1bd7 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -33,6 +33,20 @@ let no_model = {exec; check= no_check} +let at ?(size = Int64.zero) array_exp index_exp = + (* TODO? use size *) + let exec {integer_type_widths} ~ret:(id, _) mem = + L.d_printfln_escaped "Using model std::array<_, %Ld>::at" size ; + Dom.Mem.add_stack (Loc.of_id id) + (Sem.eval_lindex integer_type_widths array_exp index_exp mem) + mem + and check {location; integer_type_widths} mem cond_set = + BoUtils.Check.lindex integer_type_widths ~array_exp ~index_exp ~last_included:false mem + location cond_set + in + {exec; check} + + (* It returns a tuple of: - type of array element - stride of the type @@ -418,6 +432,37 @@ let snprintf = by_risky_value_from Trace.snprintf Dom.Val.Itv.nat let vsnprintf = by_risky_value_from Trace.vsnprintf Dom.Val.Itv.nat +module CFArray = struct + (** Creates a new array from the given array by copying the first X + elements. *) + let create_array src_exp size_exp = + let {exec= malloc_exec; check= _} = malloc ~can_be_zero:true size_exp in + let exec model_env ~ret:((id, _) as ret) mem = + let mem = malloc_exec model_env ~ret mem in + let dest_loc = Loc.of_id id |> PowLoc.singleton in + let dest_arr_loc = Dom.Val.get_array_locs (Dom.Mem.find_set dest_loc mem) in + let src_arr_v = Dom.Mem.find_set (Sem.eval_locs src_exp mem) mem in + Dom.Mem.update_mem dest_arr_loc src_arr_v mem + and check {location; integer_type_widths} mem cond_set = + BoUtils.Check.lindex integer_type_widths ~array_exp:src_exp ~index_exp:size_exp + ~last_included:true mem location cond_set + in + {exec; check} + + + (** Creates a new array with the values from the given array.*) + let create_copy_array src_exp = + let exec {integer_type_widths} ~ret:(id, _) mem = + let dest_loc = Loc.of_id id |> PowLoc.singleton in + let v = Sem.eval integer_type_widths src_exp mem in + Dom.Mem.update_mem dest_loc v mem + in + {exec; check= no_check} + + + let at (array_exp, _) (index_exp, _) = at ?size:None array_exp index_exp +end + module Split = struct let std_vector ~adds_at_least_one (vector_exp, vector_typ) location mem = let increment = if adds_at_least_one then Dom.Val.Itv.pos else Dom.Val.Itv.nat in @@ -462,19 +507,7 @@ module StdArray = struct {exec; check= no_check} - let at _size (array_exp, _) (index_exp, _) = - (* TODO? use size *) - let exec {integer_type_widths} ~ret:(id, _) mem = - L.d_printfln_escaped "Using model std::array<_, %Ld>::at" _size ; - Dom.Mem.add_stack (Loc.of_id id) - (Sem.eval_lindex integer_type_widths array_exp index_exp mem) - mem - and check {location; integer_type_widths} mem cond_set = - BoUtils.Check.lindex integer_type_widths ~array_exp ~index_exp ~last_included:false mem - location cond_set - in - {exec; check} - + let at size (array_exp, _) (index_exp, _) = at ~size array_exp index_exp let begin_ _size (array_exp, _) = let exec {location; integer_type_widths} ~ret:(id, _) mem = @@ -734,6 +767,12 @@ module Call = struct ; -"__inferbo_set_size" <>$ capt_exp $+ capt_exp $!--> inferbo_set_size ; -"__variable_initialization" <>$ capt_arg $!--> variable_initialization ; -"__exit" <>--> bottom + ; -"CFArrayCreate" <>$ any_arg $+ capt_exp $+ capt_exp $+...$--> CFArray.create_array + ; -"CFArrayCreateCopy" <>$ any_arg $+ capt_exp $!--> CFArray.create_copy_array + ; -"MCFArrayGetCount" <>$ capt_exp $!--> StdBasicString.length + ; -"CFDictionaryGetCount" <>$ capt_exp $!--> StdBasicString.length + ; -"CFArrayGetCount" <>$ capt_exp $!--> StdBasicString.length + ; -"CFArrayGetValueAtIndex" <>$ capt_arg $+ capt_arg $!--> CFArray.at ; -"exit" <>--> bottom ; -"__cast" <>$ capt_exp $+...$--> cast ; -"fgetc" <>--> by_value Dom.Val.Itv.m1_255 diff --git a/infer/tests/codetoanalyze/objc/performance/cf.m b/infer/tests/codetoanalyze/objc/performance/cf.m new file mode 100644 index 000000000..adad37580 --- /dev/null +++ b/infer/tests/codetoanalyze/objc/performance/cf.m @@ -0,0 +1,53 @@ +/* + * Copyright (c) 2019-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ +#import +#import + +#include + +typedef uint32_t UInt32; + +typedef int32_t SInt32; + +void array_count_linear(CFArrayRef arr) { + int32_t count = CFArrayGetCount(arr); + for (int i = 0; i < count; ++i) { + } +} + +void dict_count_linear(CFDictionaryRef dict) { + int32_t count = CFDictionaryGetCount(dict); + for (int i = 0; i < count; ++i) { + } +} + +void cf_array_create_linear(int x) { + int arrayValues[200]; + + arrayValues[0] = 0; + arrayValues[1] = 12; + + /* Now we can create the CF array... */ + CFArrayRef array = CFArrayCreate((CFAllocatorRef)NULL, + (const void**)arrayValues, + x, + &kCFTypeArrayCallBacks); + + int32_t count = CFArrayGetCount(array); + for (int i = 0; i < count; ++i) { + } +} + +void cf_array_create_copy_linear(int x) { + int arrayValues[200]; + + CFArrayRef array = CFArrayCreateCopy((CFAllocatorRef)NULL, arrayValues); + + int32_t count = CFArrayGetCount(array); + for (int i = 0; i < count; ++i) { + } +} diff --git a/infer/tests/codetoanalyze/objc/performance/issues.exp b/infer/tests/codetoanalyze/objc/performance/issues.exp index 7df6a28b7..9aefbd97f 100644 --- a/infer/tests/codetoanalyze/objc/performance/issues.exp +++ b/infer/tests/codetoanalyze/objc/performance/issues.exp @@ -1,2 +1,6 @@ codetoanalyze/objc/performance/araii.m, Araii_initWithBuffer, 4, EXPENSIVE_ALLOCATION_CALL, no_bucket, ERROR, [with estimated cost 4, degree = 0] codetoanalyze/objc/performance/araii.m, memory_leak_raii_main, 1, EXPENSIVE_ALLOCATION_CALL, no_bucket, ERROR, [with estimated cost 5, degree = 0] +codetoanalyze/objc/performance/cf.m, array_count_linear, 2, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 7 + 3 ⋅ arr.length + 2 ⋅ (arr.length + 1), degree = 1,{arr.length + 1},Loop at line 18, column 3,{arr.length},Loop at line 18, column 3] +codetoanalyze/objc/performance/cf.m, cf_array_create_copy_linear, 6, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 1012, degree = 0] +codetoanalyze/objc/performance/cf.m, cf_array_create_linear, 13, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 13 + 3 ⋅ x + 2 ⋅ (1+max(0, x)), degree = 1,{1+max(0, x)},Loop at line 41, column 3,{x},Loop at line 41, column 3] +codetoanalyze/objc/performance/cf.m, dict_count_linear, 2, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 7 + 3 ⋅ dict.length + 2 ⋅ (dict.length + 1), degree = 1,{dict.length + 1},Loop at line 24, column 3,{dict.length},Loop at line 24, column 3]