From 1503f63c2796f2b58fb13a9bf0e5d44e38ea7368 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Thu, 15 Nov 2018 18:34:28 -0800 Subject: [PATCH] [inferbo] Fix evaluation of multi-dimensional arrays Reviewed By: mbouaziz Differential Revision: D13082043 fbshipit-source-id: 5a45b4eee --- infer/src/bufferoverrun/bufferOverrunSemantics.ml | 12 ++++++++---- .../codetoanalyze/c/bufferoverrun/array_multidim.c | 2 +- infer/tests/codetoanalyze/c/bufferoverrun/issues.exp | 1 + 3 files changed, 10 insertions(+), 5 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 808db5709..d09b8bdef 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -161,11 +161,9 @@ let rec eval : Exp.t -> Mem.astate -> Val.t = Val.Itv.top -(* NOTE: multidimensional array is not supported yet *) and eval_lindex array_exp index_exp mem = let array_v, index_v = (eval array_exp mem, eval index_exp mem) in - let arr = Val.plus_pi array_v index_v in - if ArrayBlk.is_bot (Val.get_array_blk arr) then + if ArrayBlk.is_bot (Val.get_array_blk array_v) then match array_exp with | Exp.Lfield _ when not (PowLoc.is_bot (Val.get_pow_loc array_v)) -> (* It handles the case accessing an array field of struct, @@ -177,7 +175,13 @@ and eval_lindex array_exp index_exp mem = Val.plus_pi (Mem.find_set (Val.get_pow_loc array_v) mem) index_v | _ -> Val.of_pow_loc PowLoc.unknown - else arr + else + match array_exp with + | Exp.Lindex _ -> + (* It handles multi-dimensional arrays. *) + Mem.find_set (Val.get_all_locs array_v) mem + | _ -> + Val.plus_pi array_v index_v and eval_unop : Unop.t -> Exp.t -> Mem.astate -> Val.t = diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/array_multidim.c b/infer/tests/codetoanalyze/c/bufferoverrun/array_multidim.c index bfe48d98b..a3736562a 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/array_multidim.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/array_multidim.c @@ -51,7 +51,7 @@ void multidim_arr5_Good() { a[0][5] = 0; } -void multidim_arr5_Bad_FN() { +void multidim_arr5_Bad() { int a[1][10]; a[0][0] = 0; a[0][10] = 0; diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 6deea55cf..64a5aadf7 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -40,6 +40,7 @@ codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr1_Bad, 2, BUFFER_OVE codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 3 Size: 3] codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr4_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 6 Size: 3] codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr4_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 5 Size: 3] +codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr5_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10] codetoanalyze/c/bufferoverrun/big_array.c, use_big_array_bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Assignment,Return,Assignment,ArrayAccess: Offset: 999999999 Size: 26460] codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 13, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []