From 9deec6ffdebf0ae8413da0cfb9134602d4b94837 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Mon, 20 Nov 2017 05:27:00 -0800 Subject: [PATCH] [inferbo] Fix evaluation of Lindex Reviewed By: mbouaziz Differential Revision: D6371898 fbshipit-source-id: ba0508d --- infer/src/bufferoverrun/bufferOverrunSemantics.ml | 14 +++++++------- .../tests/codetoanalyze/c/bufferoverrun/issues.exp | 1 + .../codetoanalyze/c/bufferoverrun/pointer_arith.c | 6 ++++++ 3 files changed, 14 insertions(+), 7 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 9492a9b75..9d578862b 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -207,13 +207,13 @@ module Make (CFG : ProcCfg.S) = struct eval e mem | Exp.Lfield (e, fn, _) -> eval e mem |> Val.get_array_locs |> Fn.flip PowLoc.append_field fn |> Val.of_pow_loc - | Exp.Lindex (e1, _) -> - let arr = eval e1 mem |> Val.get_array_blk in - (* must have array blk *) - (* let idx = eval e2 mem in *) - let ploc = if ArrayBlk.is_bot arr then PowLoc.unknown else ArrayBlk.get_pow_loc arr in - (* if nested array, add the array blk *) - let arr = Mem.find_heap_set ploc mem in + | Exp.Lindex (e1, e2) -> + let arr = Val.plus_pi (eval e1 mem) (eval e2 mem) in + let ploc = + if ArrayBlk.is_bot (Val.get_array_blk arr) then PowLoc.unknown + else Val.get_all_locs arr + in + (* NOTE: multidimensional array is not supported yet *) Val.join (Val.of_pow_loc ploc) arr | Exp.Sizeof {nbytes= Some size} -> Val.of_int size diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index d1cbfb852..626ef0fb8 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -45,6 +45,7 @@ codetoanalyze/c/bufferoverrun/models.c, fgetc_256_bad, 3, BUFFER_OVERRUN_L2, [Ar codetoanalyze/c/bufferoverrun/models.c, fgetc_m1_bad, 3, BUFFER_OVERRUN_L3, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [-1, 255] Size: [10000, 10000]] codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 7, BUFFER_OVERRUN_L2, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 10] Size: [10, 10]] codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 6, BUFFER_OVERRUN_L4, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, +oo] Size: [10, 10]] +codetoanalyze/c/bufferoverrun/pointer_arith.c, array_pointer_arith_Bad, 3, BUFFER_OVERRUN_L1, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [10, 10] Size: [10, 10]] codetoanalyze/c/bufferoverrun/pointer_arith.c, pointer_arith_bad, 4, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [10, 10]] codetoanalyze/c/bufferoverrun/prune_alias.c, FP_prune_alias_exp_Ok, 4, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [1, 1] Size: [1, 1]] codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_and_Ok, 3, CONDITION_ALWAYS_FALSE, [] diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/pointer_arith.c b/infer/tests/codetoanalyze/c/bufferoverrun/pointer_arith.c index 9f01f343a..ca192f8a3 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/pointer_arith.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/pointer_arith.c @@ -13,3 +13,9 @@ void pointer_arith_bad() { if (&x - 1 == 0) arr[10] = 1; } + +void array_pointer_arith_Bad() { + int arr[10]; + int* p = &arr[5]; + p[5] = 1; +}