From 67d74c7c3d6648077a86156e82b4b2edbef7a194 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Thu, 22 Oct 2020 07:43:46 -0700 Subject: [PATCH] [cost] Revise nextObject model to handle multiple enumerators Summary: This diff revises `nextObject` model to handle multiple symbolic enumerators. Instead joining the symbolic offsets of them, which sometimes introduces top, it sums the offsets. This is a sound & conservative semantics since they are all non-negative integers. Reviewed By: ezgicicek Differential Revision: D24474513 fbshipit-source-id: 6707aa907 --- infer/src/bufferoverrun/bufferOverrunModels.ml | 2 +- infer/tests/codetoanalyze/objc/performance/NSArray.m | 9 +++++++++ .../tests/codetoanalyze/objc/performance/cost-issues.exp | 1 + 3 files changed, 11 insertions(+), 1 deletion(-) diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 2943a3636..c26f871d9 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -1165,7 +1165,7 @@ module NSCollection = struct [nextObject] returns the offset of the enumerator instead of an object elements, which helps the cost checker select the offset as a control variable, for example, [while(obj = [enumerator nextObject]) { ... }]. *) - ArrayBlk.get_offset arrayblk |> Itv.join Itv.zero |> Dom.Val.of_itv + ArrayBlk.get_offset ~cost_mode:true arrayblk |> Itv.join Itv.zero |> Dom.Val.of_itv in model_by_value return_v ret_id mem |> Dom.Mem.add_heap_set iterator_locs iterator_v' diff --git a/infer/tests/codetoanalyze/objc/performance/NSArray.m b/infer/tests/codetoanalyze/objc/performance/NSArray.m index 9cab94586..0b873be72 100644 --- a/infer/tests/codetoanalyze/objc/performance/NSArray.m +++ b/infer/tests/codetoanalyze/objc/performance/NSArray.m @@ -172,6 +172,15 @@ void nsarray_enumerator_param_linear(NSEnumerator* enumerator) { } } +void multiple_nsarray_enumerators_param_linear(bool b, + NSEnumerator* enumerator1, + NSEnumerator* enumerator2) { + NSEnumerator* enumerator = b ? enumerator1 : enumerator2; + id obj; + while (obj = [enumerator nextObject]) { + } +} + void call_nsarray_enumerator_param_linear(NSArray* array) { NSEnumerator* enumerator = [array objectEnumerator]; nsarray_enumerator_param_linear_FN(enumerator); diff --git a/infer/tests/codetoanalyze/objc/performance/cost-issues.exp b/infer/tests/codetoanalyze/objc/performance/cost-issues.exp index 1df975541..5e7a1072d 100644 --- a/infer/tests/codetoanalyze/objc/performance/cost-issues.exp +++ b/infer/tests/codetoanalyze/objc/performance/cost-issues.exp @@ -1,5 +1,6 @@ ${XCODE_ISYSROOT}/System/Library/Frameworks/Foundation.framework/Headers/NSArray.h, NSArray.indexOfObject:inSortedRange:options:usingComparator:[objc_blocknsarray_binary_search_log_FN_1], 0, OnUIThread:false, [] codetoanalyze/objc/performance/NSArray.m, call_nsarray_enumerator_param_linear, 6, OnUIThread:false, [] +codetoanalyze/objc/performance/NSArray.m, multiple_nsarray_enumerators_param_linear, 12 + 5 ⋅ (enumerator2.length + enumerator1.length + 2), OnUIThread:false, [{enumerator2.length + enumerator1.length + 2},Loop] codetoanalyze/objc/performance/NSArray.m, nsarray_access_constant, 50, OnUIThread:false, [] codetoanalyze/objc/performance/NSArray.m, nsarray_access_linear, 3 + 7 ⋅ array->elements.length.ub + 3 ⋅ (array->elements.length.ub + 1), OnUIThread:false, [{array->elements.length.ub + 1},Loop,{array->elements.length.ub},Loop] codetoanalyze/objc/performance/NSArray.m, nsarray_add_object_constant, 8, OnUIThread:false, []