From 7f256844914a4f3f9b9b09dc8a850dca46f6dc03 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Mon, 3 Feb 2020 05:03:55 -0800 Subject: [PATCH] [inferbo] Check nested global array access Summary: This diff fixes the array access checking function for nested global arrays. We had assumed that RHS of `store` statement in SIL does not include array access expression, but that is not true: for global arrays, SIL can have statements like `*LHS = GlobalArray[n][m]`. Reviewed By: ezgicicek Differential Revision: D19300153 fbshipit-source-id: 256325642 --- .../src/bufferoverrun/bufferOverrunChecker.ml | 28 +++++++++++-------- .../bufferoverrun/bufferOverrunSemantics.ml | 2 +- .../cpp/bufferoverrun/global.cpp | 2 +- .../cpp/bufferoverrun/issues.exp | 3 +- 4 files changed, 20 insertions(+), 15 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 114972566..55dee0dc6 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -156,13 +156,14 @@ let check_binop : let check_expr_for_array_access : - Typ.IntegerWidths.t + ?sub_expr_only:bool + -> Typ.IntegerWidths.t -> Exp.t -> Location.t -> Dom.Mem.t -> PO.ConditionSet.checked_t -> PO.ConditionSet.checked_t = - fun integer_type_widths exp location mem cond_set -> + fun ?(sub_expr_only = false) integer_type_widths exp location mem cond_set -> let rec check_sub_expr exp cond_set = match exp with | Exp.Lindex (array_exp, index_exp) -> @@ -182,17 +183,19 @@ let check_expr_for_array_access : cond_set in let cond_set = check_sub_expr exp cond_set in - match exp with - | Exp.Var _ -> - let arr = Sem.eval integer_type_widths exp mem in - let idx = Dom.Val.Itv.zero in - let latest_prune = Dom.Mem.get_latest_prune mem in - BoUtils.Check.array_access ~arr ~idx ~is_plus:true ~last_included:false ~latest_prune location + if sub_expr_only then cond_set + else + match exp with + | Exp.Var _ -> + let arr = Sem.eval integer_type_widths exp mem in + let idx = Dom.Val.Itv.zero in + let latest_prune = Dom.Mem.get_latest_prune mem in + BoUtils.Check.array_access ~arr ~idx ~is_plus:true ~last_included:false ~latest_prune + location cond_set + | Exp.BinOp (bop, e1, e2) -> + check_binop integer_type_widths ~bop ~e1 ~e2 location mem cond_set + | _ -> cond_set - | Exp.BinOp (bop, e1, e2) -> - check_binop integer_type_widths ~bop ~e1 ~e2 location mem cond_set - | _ -> - cond_set let check_binop_for_integer_overflow integer_type_widths bop ~lhs ~rhs location mem cond_set = @@ -276,6 +279,7 @@ let check_instr : | Sil.Store {e1= lexp; e2= rexp; loc= location} -> cond_set |> check_expr_for_array_access integer_type_widths lexp location mem + |> check_expr_for_array_access ~sub_expr_only:true integer_type_widths rexp location mem |> check_expr_for_integer_overflow integer_type_widths lexp location mem |> check_expr_for_integer_overflow integer_type_widths rexp location mem | Sil.Call (_, Const (Cfun callee_pname), params, location, _) -> ( diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index ed6c99186..6243e10d3 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -318,7 +318,7 @@ let rec eval_arr : Typ.IntegerWidths.t -> Exp.t -> Mem.t -> Val.t = let locs = eval_locs e mem |> PowLoc.append_field ~fn in Mem.find_set locs mem | Exp.Lindex (e, _) -> - let locs = eval_locs e mem in + let locs = eval_arr integer_type_widths e mem |> Val.get_all_locs in Mem.find_set locs mem | Exp.Const _ | Exp.UnOp _ | Exp.Sizeof _ | Exp.Exn _ | Exp.Closure _ -> Val.bot diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/global.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/global.cpp index a1ed19ed2..e884aa79f 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/global.cpp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/global.cpp @@ -14,6 +14,6 @@ void access_constant_global_Bad() { static int StaticGlobal[][3] = { {0, 0, 0}, {0, 0, 0}, {0, 0, 0}, {0, 0, 0}, {0, 0, 0}}; -void access_static_global1_Bad_FN() { int* p = StaticGlobal[10]; } +void access_static_global1_Bad() { int* p = StaticGlobal[10]; } void access_static_global2_Bad() { int a = StaticGlobal[0][10]; } diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 332ec2740..1e7156dba 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -50,7 +50,8 @@ codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empt codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_by_ref_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Call,Assignment,,Array declaration,Array access: Offset: -1 Size: 10] codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_loop_with_init_S_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Call,Parameter `length`,Assignment,,Array declaration,Array access: Offset: 10 Size: 10] codetoanalyze/cpp/bufferoverrun/global.cpp, access_constant_global_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: 5 Size: 5] -codetoanalyze/cpp/bufferoverrun/global.cpp, access_static_global2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 5] +codetoanalyze/cpp/bufferoverrun/global.cpp, access_static_global1_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 5] +codetoanalyze/cpp/bufferoverrun/global.cpp, access_static_global2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 3] codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Assignment,Array access: Offset: 5 Size: 5] codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_flexible_array_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 7 Size: 5] codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_struct1_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Assignment,Array access: Offset: 5 Size: 5]