From 99eda7e3a8abe42da5bc2e068dbbc7b83d1e27d0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Tue, 4 Jun 2019 03:00:16 -0700 Subject: [PATCH] [inferbo,cost] Fix java arrays Reviewed By: mbouaziz, ddino Differential Revision: D15602327 fbshipit-source-id: d17253a15 --- .../src/bufferoverrun/bufferOverrunModels.ml | 25 ++++++++++++++----- infer/src/bufferoverrun/bufferOverrunUtils.ml | 7 +++++- .../java/bufferoverrun/issues.exp | 8 +++--- .../codetoanalyze/java/performance/Array.java | 12 +++++++++ .../codetoanalyze/java/performance/issues.exp | 4 ++- 5 files changed, 44 insertions(+), 12 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 679b24fb8..f1fbdc72c 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -115,19 +115,32 @@ let malloc ~can_be_zero size_exp = match Dom.Mem.find_simple_alias id mem with Some (l, None) -> Loc.get_path l | _ -> None in let offset, size = (Itv.zero, Dom.Val.get_itv length) in + let represents_multiple_values = not (Itv.is_one size) in let allocsite = - let represents_multiple_values = not (Itv.is_one size) in Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 ~path ~represents_multiple_values in let size_exp_opt = let size_exp = Option.value dyn_length ~default:length0 in Relation.SymExp.of_exp ~get_sym_f:(Sem.get_sym_f integer_type_widths mem) size_exp in - let v = Dom.Val.of_c_array_alloc allocsite ~stride ~offset ~size ~traces in - mem - |> Dom.Mem.add_stack (Loc.of_id id) v - |> Dom.Mem.init_array_relation allocsite ~offset_opt:(Some offset) ~size ~size_exp_opt - |> BoUtils.Exec.init_c_array_fields model_env path typ (Dom.Val.get_array_locs v) ?dyn_length + if Language.curr_language_is Java then + let internal_arr = + let allocsite = + Allocsite.make pname ~node_hash ~inst_num:1 ~dimension:1 ~path:None + ~represents_multiple_values + in + Dom.Val.of_java_array_alloc allocsite ~length:size ~traces + in + let arr_loc = Loc.of_allocsite allocsite in + mem + |> Dom.Mem.add_heap arr_loc internal_arr + |> Dom.Mem.add_stack (Loc.of_id id) (Dom.Val.of_pow_loc ~traces (PowLoc.singleton arr_loc)) + else + let v = Dom.Val.of_c_array_alloc allocsite ~stride ~offset ~size ~traces in + mem + |> Dom.Mem.add_stack (Loc.of_id id) v + |> Dom.Mem.init_array_relation allocsite ~offset_opt:(Some offset) ~size ~size_exp_opt + |> BoUtils.Exec.init_c_array_fields model_env path typ (Dom.Val.get_array_locs v) ?dyn_length and check = check_alloc_size ~can_be_zero size_exp in {exec; check} diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index 62fcfec67..f07180f52 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -264,7 +264,12 @@ module Check = struct let lindex integer_type_widths ~array_exp ~index_exp ~last_included mem location cond_set = let idx = Sem.eval integer_type_widths index_exp mem in - let arr = Sem.eval_arr integer_type_widths array_exp mem in + let arr = + if Language.curr_language_is Java then + let arr_locs = Sem.eval_locs array_exp mem in + if PowLoc.is_empty arr_locs then Dom.Val.Itv.top else Dom.Mem.find_set arr_locs mem + else Sem.eval_arr integer_type_widths array_exp mem + in let idx_sym_exp = Relation.SymExp.of_exp ~get_sym_f:(Sem.get_sym_f integer_type_widths mem) index_exp in diff --git a/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp index 5556b12c2..55123ff5a 100644 --- a/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp @@ -1,10 +1,10 @@ codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.collection_remove_from_empty_Bad():java.util.ArrayList, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 0 Size: 0] codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.negative_alloc_Bad():void, 1, INFERBO_ALLOC_IS_NEGATIVE, no_bucket, ERROR, [Allocation: Length: -1] codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning1_Bad():void, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] -codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning1_Bad():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Assignment,Array access: Offset: 10 Size: 5] +codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning1_Bad():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 5] codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning1_Good():void, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] -codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning2_Bad():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Assignment,Array access: Offset: 10 Size: 5] -codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning2_Good_FP():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Assignment,Array access: Offset: 10 Size: 5] -codetoanalyze/java/bufferoverrun/ArrayMember.java, codetoanalyze.java.bufferoverrun.ArrayMember.load_array_member_Bad():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Parameter `this.buf[*]`,Assignment,,Array declaration,Assignment,Array access: Offset: [max(10, this.buf[*].lb), min(10, this.buf[*].ub)] Size: 10] +codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning2_Bad():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 5] +codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning2_Good_FP():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 5] +codetoanalyze/java/bufferoverrun/ArrayMember.java, codetoanalyze.java.bufferoverrun.ArrayMember.load_array_member_Bad():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Parameter `this.buf[*]`,Assignment,,Array declaration,Array access: Offset: [max(10, this.buf[*].lb), min(10, this.buf[*].ub)] Size: 10] codetoanalyze/java/bufferoverrun/CompressedData.java, codetoanalyze.java.bufferoverrun.CompressedData.decompressData(codetoanalyze.java.bufferoverrun.CompressedData$D):int, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Parameter `this.yy`,,Parameter `d.cci[*].s`,Assignment,Binary operation: ([0, this.yy - 1] × d.cci[*].s):signed32] codetoanalyze/java/bufferoverrun/External.java, External.external_function_Bad(external.library.SomeExternalClass):void, 1, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [,Unknown value from: int Integer.intValue(),Assignment,,Unknown value from: int Integer.intValue(),Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32] diff --git a/infer/tests/codetoanalyze/java/performance/Array.java b/infer/tests/codetoanalyze/java/performance/Array.java index f7713aed7..c26c60f97 100644 --- a/infer/tests/codetoanalyze/java/performance/Array.java +++ b/infer/tests/codetoanalyze/java/performance/Array.java @@ -48,4 +48,16 @@ public class Array { void copyOf_constant(String[] arr) { String[] new_arr = Arrays.copyOf(arr, 10); } + + void init_array_linear() { + int[] table = new int[256]; + for (int i = 0; i < table.length; ++i) { + table[i] = i; + } + } + + void fill_big_constant_FP() { + String[] arr = new String[300]; + Arrays.fill(arr, 0); + } } diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index b8e69acb3..213b89689 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -1,10 +1,12 @@ codetoanalyze/java/performance/A.java, B$BArray.error():void, 4, EXPENSIVE_ALLOCATION_CALL, no_bucket, ERROR, [with estimated cost 4, degree = 0] codetoanalyze/java/performance/A.java, B.error():void, 4, EXPENSIVE_ALLOCATION_CALL, no_bucket, ERROR, [with estimated cost 4, degree = 0] -codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.array_access_overrun_bad():void, 4, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Assignment,,Array declaration,Assignment,Array access: Offset: [2, 8] Size: 8] +codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.array_access_overrun_bad():void, 4, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: [2, 8] Size: 8] codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.array_access_weird_ok(long[],int):void, 1, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 2 + 13 ⋅ length, degree = 1,{length},Loop at line 30] codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.binary_search_log(java.lang.String[]):int, 1, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 2 + log(arr.length), degree = 0 + 1⋅log,{arr.length},Modeled call to Arrays.binarySearch] codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.copyOf_linear(java.lang.String[]):void, 1, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 4 + arr.length, degree = 1,{arr.length},Modeled call to Arrays.copyOf] +codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.fill_big_constant_FP():void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [Unbounded loop,Modeled call to Arrays.fill] codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.fill_linear(java.lang.String[]):void, 1, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 2 + arr.length, degree = 1,{arr.length},Modeled call to Arrays.fill] +codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.init_array_linear():void, 2, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 2564, degree = 0] codetoanalyze/java/performance/ArrayCost.java, ArrayCost.ArrayCost(int[]):void, 5, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 5 + 5 ⋅ mag.length, degree = 1,{mag.length},Loop at line 15] codetoanalyze/java/performance/ArrayCost.java, ArrayCost.isPowOfTwo_FP(int):boolean, 4, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 883, degree = 0] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_add3_overrun_bad():void, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Through,Through,Through,Array access: Offset added: 4 Size: 3]