From 252c78bb0e9cc1e14c260589196a2c748ca88e77 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Tue, 16 May 2017 04:02:15 -0700 Subject: [PATCH] [clang] initialize dynamically-size stack-allocated arrays Summary: Previously all knowledge of the dynamic length of such arrays was lost to infer: ``` void foo(int len) { int a[len]; } ``` The translation of this program would make no reference to `len` (except as a param of `foo`). Translate this "initialization" using the existing `__set_array_length` infer builtin, as: ``` # Declare local a[_] n$0 = len; __set_array_length(a, len); ``` update-submodule: facebook-clang-plugins Reviewed By: mbouaziz Differential Revision: D4969446 fbshipit-source-id: dff860f --- facebook-clang-plugins | 2 +- .../src/bufferoverrun/bufferOverrunChecker.ml | 259 +++++++++--------- infer/src/bufferoverrun/itv.ml | 2 + infer/src/clang/cTrans.ml | 37 ++- infer/src/clang/cType_to_sil_type.ml | 2 +- .../c/bufferoverrun/array_dynlength.c | 14 + .../codetoanalyze/c/bufferoverrun/issues.exp | 1 + .../initialization/array_initlistexpr.c | 7 +- .../initialization/array_initlistexpr.c.dot | 25 +- 9 files changed, 213 insertions(+), 136 deletions(-) create mode 100644 infer/tests/codetoanalyze/c/bufferoverrun/array_dynlength.c diff --git a/facebook-clang-plugins b/facebook-clang-plugins index 84b3c58ab..0c9c4d0eb 160000 --- a/facebook-clang-plugins +++ b/facebook-clang-plugins @@ -1 +1 @@ -Subproject commit 84b3c58ab12fd42779ea4f8c1214432801cf4a5f +Subproject commit 0c9c4d0ebb43c686143edb51c6e80e551df05b99 diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 65955d428..7c52e2d1e 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -35,13 +35,17 @@ struct type extras = Typ.Procname.t -> Procdesc.t option + let set_uninitialized (typ : Typ.t) loc mem = match typ.desc with + | Tint _ | Tfloat _ -> Dom.Mem.weak_update_heap loc Dom.Val.top_itv mem + | _ -> mem + (* NOTE: heuristic *) let get_malloc_info : Exp.t -> Typ.t * Int.t option * Exp.t = function - | Exp.BinOp (Binop.Mult, Exp.Sizeof {typ; nbytes}, length) - | Exp.BinOp (Binop.Mult, length, Exp.Sizeof {typ; nbytes}) -> (typ, nbytes, length) - | Exp.Sizeof {typ; nbytes} -> (typ, nbytes, Exp.one) - | x -> (Typ.mk (Typ.Tint Typ.IChar), Some 1, x) + | Exp.BinOp (Binop.Mult, Exp.Sizeof {typ; nbytes}, length) + | Exp.BinOp (Binop.Mult, length, Exp.Sizeof {typ; nbytes}) -> (typ, nbytes, length) + | Exp.Sizeof {typ; nbytes} -> (typ, nbytes, Exp.one) + | x -> (Typ.mk (Typ.Tint Typ.IChar), Some 1, x) let model_malloc : Typ.Procname.t -> (Ident.t * Typ.t) option -> (Exp.t * Typ.t) list -> CFG.node @@ -49,19 +53,12 @@ struct = fun pname ret params node mem -> match ret with | Some (id, _) -> - let set_uninitialized typ loc mem = - match typ.Typ.desc with - | Typ.Tint _ - | Typ.Tfloat _ -> - Dom.Mem.weak_update_heap loc Dom.Val.top_itv mem - | _ -> mem - in - let (typ, stride, length0) = get_malloc_info (List.hd_exn params |> fst) in - let length = Sem.eval length0 mem (CFG.loc node) |> Dom.Val.get_itv in - let v = Sem.eval_array_alloc pname node typ ?stride Itv.zero length 0 1 in - mem - |> Dom.Mem.add_stack (Loc.of_id id) v - |> set_uninitialized typ (Dom.Val.get_array_locs v) + let (typ, stride, length0) = get_malloc_info (List.hd_exn params |> fst) in + let length = Sem.eval length0 mem (CFG.loc node) |> Dom.Val.get_itv in + let v = Sem.eval_array_alloc pname node typ ?stride Itv.zero length 0 1 in + mem + |> Dom.Mem.add_stack (Loc.of_id id) v + |> set_uninitialized typ (Dom.Val.get_array_locs v) | _ -> mem let model_realloc @@ -74,8 +71,8 @@ struct = fun ret mem -> match ret with | Some (id, _) -> - let itv = Itv.make (Itv.Bound.of_int (-1)) Itv.Bound.PInf in - Dom.Mem.add_stack (Loc.of_id id) (Dom.Val.of_itv itv) mem + let itv = Itv.make (Itv.Bound.of_int (-1)) Itv.Bound.PInf in + Dom.Mem.add_stack (Loc.of_id id) (Dom.Val.of_itv itv) mem | _ -> mem let model_natual_itv : (Ident.t * Typ.t) option -> Dom.Mem.astate -> Dom.Mem.astate @@ -95,13 +92,28 @@ struct = fun params mem loc -> match params with | (e, _) :: _ -> - if Config.bo_debug >= 1 then - L.err "@[=== Infer Print === at %a@,%a@]%!" - Location.pp loc - Dom.Val.pp (Sem.eval e mem loc); - mem + if Config.bo_debug >= 1 then + L.err "@[=== Infer Print === at %a@,%a@]%!" + Location.pp loc + Dom.Val.pp (Sem.eval e mem loc); + mem | _ -> mem + let model_infer_set_array_length pname node params mem loc = + match params with + | (Exp.Lvar array_pvar, {Typ.desc=Typ.Tarray (typ, _, stride0)}) + :: (length_exp, _) :: [] -> + let length = Sem.eval length_exp mem loc |> Dom.Val.get_itv in + let stride = Option.map ~f:IntLit.to_int stride0 in + let v = Sem.eval_array_alloc pname node typ ?stride Itv.zero length 0 1 in + mem + |> Dom.Mem.add_stack (Loc.of_pvar array_pvar) v + |> set_uninitialized typ (Dom.Val.get_array_locs v) + | _ :: _ :: [] -> + failwithf "Unexpected type of arguments for __set_array_length()" + | _ -> + failwithf "Unexpected number of arguments for __set_array_length()" + let handle_unknown_call : Typ.Procname.t -> (Ident.t * Typ.t) option -> Typ.Procname.t -> (Exp.t * Typ.t) list -> CFG.node -> Dom.Mem.astate -> Location.t @@ -114,13 +126,14 @@ struct | "strlen" -> model_natual_itv ret mem | "fgetc" -> model_fgetc ret mem | "infer_print" -> model_infer_print params mem loc + | "__set_array_length" -> model_infer_set_array_length pname node params mem loc | _ -> model_unknown_itv ret mem let rec declare_array - : Typ.Procname.t -> CFG.node -> Loc.t -> Typ.t -> length:IntLit.t -> ?stride:int + : Typ.Procname.t -> CFG.node -> Loc.t -> Typ.t -> length:IntLit.t option -> ?stride:int -> inst_num:int -> dimension:int -> Dom.Mem.astate -> Dom.Mem.astate = fun pname node loc typ ~length ?stride ~inst_num ~dimension mem -> - let size = IntLit.to_int length |> Itv.of_int in + let size = Option.value_map ~default:Itv.top ~f:Itv.of_int_lit length in let arr = Sem.eval_array_alloc pname node typ Itv.zero size ?stride inst_num dimension in @@ -133,7 +146,7 @@ struct Loc.of_allocsite (Sem.get_allocsite pname node inst_num dimension) in match typ.Typ.desc with - | Typ.Tarray (typ, Some length, stride) -> + | Typ.Tarray (typ, length, stride) -> declare_array pname node loc typ ~length ?stride:(Option.map ~f:IntLit.to_int stride) ~inst_num ~dimension:(dimension + 1) mem | _ -> mem @@ -162,26 +175,26 @@ struct match typ.Typ.desc with | Typ.Tint _ | Typ.Tfloat _ -> - let v = Dom.Val.make_sym pname sym_num in - (Dom.Mem.add_heap field v mem, sym_num + 2) + let v = Dom.Val.make_sym pname sym_num in + (Dom.Mem.add_heap field v mem, sym_num + 2) | Typ.Tptr (typ, _) -> - let offset = Itv.make_sym pname sym_num in - let size = Itv.make_sym pname (sym_num + 2) in - let v = - Sem.eval_array_alloc pname node typ offset size inst_num dimension - in - (Dom.Mem.add_heap field v mem, sym_num + 4) + let offset = Itv.make_sym pname sym_num in + let size = Itv.make_sym pname (sym_num + 2) in + let v = + Sem.eval_array_alloc pname node typ offset size inst_num dimension + in + (Dom.Mem.add_heap field v mem, sym_num + 4) | _ -> - if Config.bo_debug >= 3 then - L.err "decl_fld of unhandled type: %a@." (Typ.pp Pp.text) typ; - (mem, sym_num) + if Config.bo_debug >= 3 then + L.err "decl_fld of unhandled type: %a@." (Typ.pp Pp.text) typ; + (mem, sym_num) in match typ.Typ.desc with | Typ.Tstruct typename -> - (match Tenv.lookup tenv typename with - | Some str -> - List.fold ~f:decl_fld ~init:(mem, sym_num + 6) str.Typ.Struct.fields - | _ -> (mem, sym_num + 6)) + (match Tenv.lookup tenv typename with + | Some str -> + List.fold ~f:decl_fld ~init:(mem, sym_num + 6) str.Typ.Struct.fields + | _ -> (mem, sym_num + 6)) | _ -> (mem, sym_num + 6) let declare_symbolic_parameter @@ -191,19 +204,19 @@ struct let add_formal (mem, inst_num, sym_num) (pvar, typ) = match typ.Typ.desc with | Typ.Tint _ -> - let v = Dom.Val.make_sym pname sym_num in - let mem = Dom.Mem.add_heap (Loc.of_pvar pvar) v mem in - (mem, inst_num + 1, sym_num + 2) + let v = Dom.Val.make_sym pname sym_num in + let mem = Dom.Mem.add_heap (Loc.of_pvar pvar) v mem in + (mem, inst_num + 1, sym_num + 2) | Typ.Tptr (typ, _) -> - let (mem, sym_num) = - declare_symbolic_array pname tenv node (Loc.of_pvar pvar) typ - ~inst_num ~sym_num ~dimension:1 mem - in - (mem, inst_num + 1, sym_num) + let (mem, sym_num) = + declare_symbolic_array pname tenv node (Loc.of_pvar pvar) typ + ~inst_num ~sym_num ~dimension:1 mem + in + (mem, inst_num + 1, sym_num) | _ -> - if Config.bo_debug >= 3 then - L.err "declare_symbolic_parameter of unhandled type: %a@." (Typ.pp Pp.text) typ; - (mem, inst_num, sym_num) (* TODO: add other cases if necessary *) + if Config.bo_debug >= 3 then + L.err "declare_symbolic_parameter of unhandled type: %a@." (Typ.pp Pp.text) typ; + (mem, inst_num, sym_num) (* TODO: add other cases if necessary *) in List.fold ~f:add_formal ~init:(mem, inst_num, 0) (Sem.get_formals pdesc) |> fst3 @@ -216,13 +229,13 @@ struct let callee_exit_mem = Dom.Summary.get_output summary in match callee_pdesc with | Some pdesc -> - let subst_map = - Sem.get_subst_map tenv pdesc params caller_mem callee_entry_mem loc - in - let ret_loc = Loc.of_pvar (Pvar.get_ret_pvar callee_pname) in - let ret_val = Dom.Mem.find_heap ret_loc callee_exit_mem in - Dom.Val.subst ret_val subst_map - |> Dom.Val.normalize (* normalize bottom *) + let subst_map = + Sem.get_subst_map tenv pdesc params caller_mem callee_entry_mem loc + in + let ret_loc = Loc.of_pvar (Pvar.get_ret_pvar callee_pname) in + let ret_val = Dom.Mem.find_heap ret_loc callee_exit_mem in + Dom.Val.subst ret_val subst_map + |> Dom.Val.normalize (* normalize bottom *) | _ -> Dom.Val.top_itv let print_debug_info : Sil.instr -> Dom.Mem.astate -> Dom.Mem.astate -> unit @@ -244,7 +257,7 @@ struct let pname = Procdesc.get_proc_name pdesc in let try_decl_arr (mem, inst_num) (pvar, typ) = match typ.Typ.desc with - | Typ.Tarray (typ, Some length, stride0) -> + | Typ.Tarray (typ, length, stride0) -> let loc = Loc.of_pvar pvar in let stride = Option.map ~f:IntLit.to_int stride0 in let mem = @@ -256,32 +269,32 @@ struct let output_mem = match instr with | Load (id, exp, _, loc) -> - let locs = Sem.eval exp mem loc |> Dom.Val.get_all_locs in - let v = Dom.Mem.find_heap_set locs mem in - Dom.Mem.add_stack (Loc.of_var (Var.of_id id)) v mem - |> Dom.Mem.load_alias id exp + let locs = Sem.eval exp mem loc |> Dom.Val.get_all_locs in + let v = Dom.Mem.find_heap_set locs mem in + Dom.Mem.add_stack (Loc.of_var (Var.of_id id)) v mem + |> Dom.Mem.load_alias id exp | Store (exp1, _, exp2, loc) -> - let locs = Sem.eval exp1 mem loc |> Dom.Val.get_all_locs in - Dom.Mem.update_mem locs (Sem.eval exp2 mem loc) mem - |> Dom.Mem.store_alias exp1 exp2 + let locs = Sem.eval exp1 mem loc |> Dom.Val.get_all_locs in + Dom.Mem.update_mem locs (Sem.eval exp2 mem loc) mem + |> Dom.Mem.store_alias exp1 exp2 | Prune (exp, loc, _, _) -> Sem.prune exp loc mem | Call (ret, Const (Cfun callee_pname), params, loc, _) -> - (match Summary.read_summary pdesc callee_pname with - | Some summary -> - let callee = extras callee_pname in - let ret_val = - instantiate_ret tenv callee callee_pname params mem summary loc - in - (match ret with - | Some (id, _) -> - Dom.Mem.add_stack (Loc.of_var (Var.of_id id)) ret_val mem - | _ -> mem) - | None -> - handle_unknown_call pname ret callee_pname params node mem loc) + (match Summary.read_summary pdesc callee_pname with + | Some summary -> + let callee = extras callee_pname in + let ret_val = + instantiate_ret tenv callee callee_pname params mem summary loc + in + (match ret with + | Some (id, _) -> + Dom.Mem.add_stack (Loc.of_var (Var.of_id id)) ret_val mem + | _ -> mem) + | None -> + handle_unknown_call pname ret callee_pname params node mem loc) | Declare_locals (locals, _) -> - (* array allocation in stack e.g., int arr[10] *) - let (mem, inst_num) = List.fold ~f:try_decl_arr ~init:(mem, 1) locals in - declare_symbolic_parameter pdesc tenv node inst_num mem + (* array allocation in stack e.g., int arr[10] *) + let (mem, inst_num) = List.fold ~f:try_decl_arr ~init:(mem, 1) locals in + declare_symbolic_parameter pdesc tenv node inst_num mem | Call _ | Remove_temps _ | Abstract _ @@ -308,33 +321,33 @@ struct let array_access = match exp with | Exp.Var _ -> - let arr = Sem.eval exp mem loc |> Dom.Val.get_array_blk in - Some (arr, Itv.zero, true) + let arr = Sem.eval exp mem loc |> Dom.Val.get_array_blk in + Some (arr, Itv.zero, true) | Exp.Lindex (e1, e2) | Exp.BinOp (Binop.PlusA, e1, e2) -> - let arr = Sem.eval e1 mem loc |> Dom.Val.get_array_blk in - let idx = Sem.eval e2 mem loc |> Dom.Val.get_itv in - Some (arr, idx, true) + let arr = Sem.eval e1 mem loc |> Dom.Val.get_array_blk in + let idx = Sem.eval e2 mem loc |> Dom.Val.get_itv in + Some (arr, idx, true) | Exp.BinOp (Binop.MinusA, e1, e2) -> - let arr = Sem.eval e1 mem loc |> Dom.Val.get_array_blk in - let idx = Sem.eval e2 mem loc |> Dom.Val.get_itv in - Some (arr, idx, false) + let arr = Sem.eval e1 mem loc |> Dom.Val.get_array_blk in + let idx = Sem.eval e2 mem loc |> Dom.Val.get_itv in + Some (arr, idx, false) | _ -> None in match array_access with | Some (arr, idx, is_plus) -> - let site = Sem.get_allocsite pname node 0 0 in - let size = ArrayBlk.sizeof arr in - let offset = ArrayBlk.offsetof arr in - let idx = (if is_plus then Itv.plus else Itv.minus) offset idx in - (if Config.bo_debug >= 2 then - (L.err "@[Add condition :@,"; - L.err "array: %a@," ArrayBlk.pp arr; - L.err " idx: %a@," Itv.pp idx; - L.err "@]@.")); - if size <> Itv.bot && idx <> Itv.bot then - Dom.ConditionSet.add_bo_safety pname loc site ~size ~idx cond_set - else cond_set + let site = Sem.get_allocsite pname node 0 0 in + let size = ArrayBlk.sizeof arr in + let offset = ArrayBlk.offsetof arr in + let idx = (if is_plus then Itv.plus else Itv.minus) offset idx in + (if Config.bo_debug >= 2 then + (L.err "@[Add condition :@,"; + L.err "array: %a@," ArrayBlk.pp arr; + L.err " idx: %a@," Itv.pp idx; + L.err "@]@.")); + if size <> Itv.bot && idx <> Itv.bot then + Dom.ConditionSet.add_bo_safety pname loc site ~size ~idx cond_set + else cond_set | None -> cond_set let instantiate_cond @@ -345,11 +358,11 @@ struct let callee_cond = Dom.Summary.get_cond_set summary in match callee_pdesc with | Some pdesc -> - let subst_map = - Sem.get_subst_map tenv pdesc params caller_mem callee_entry_mem loc - in - let pname = Procdesc.get_proc_name pdesc in - Dom.ConditionSet.subst callee_cond subst_map caller_pname pname loc + let subst_map = + Sem.get_subst_map tenv pdesc params caller_mem callee_entry_mem loc + in + let pname = Procdesc.get_proc_name pdesc in + Dom.ConditionSet.subst callee_cond subst_map caller_pname pname loc | _ -> callee_cond let print_debug_info : Sil.instr -> Dom.Mem.astate -> Dom.ConditionSet.t -> unit @@ -371,15 +384,15 @@ struct match instr with | Sil.Load (_, exp, _, loc) | Sil.Store (exp, _, _, loc) -> - add_condition pname node exp loc mem cond_set + add_condition pname node exp loc mem cond_set | Sil.Call (_, Const (Cfun callee_pname), params, loc, _) -> - (match Summary.read_summary pdesc callee_pname with - | Some summary -> - let callee = extras callee_pname in - instantiate_cond tenv pname callee params mem summary loc - |> Dom.ConditionSet.rm_invalid - |> Dom.ConditionSet.join cond_set - | _ -> cond_set) + (match Summary.read_summary pdesc callee_pname with + | Some summary -> + let callee = extras callee_pname in + instantiate_cond tenv pname callee params mem summary loc + |> Dom.ConditionSet.rm_invalid + |> Dom.ConditionSet.join cond_set + | _ -> cond_set) | _ -> cond_set in let mem = Analyzer.TransferFunctions.exec_instr mem pdata node instr in @@ -420,12 +433,12 @@ struct match alarm with | None -> () | Some bucket when Typ.Procname.equal pname caller_pname -> - let description = Dom.Condition.to_string cond in - let error_desc = Localise.desc_buffer_overrun bucket description in - let exn = - Exceptions.Checkers (Localise.to_issue_id Localise.buffer_overrun, error_desc) in - let trace = [Errlog.make_trace_element 0 loc description []] in - Reporting.log_error pname ~loc ~ltr:trace exn + let description = Dom.Condition.to_string cond in + let error_desc = Localise.desc_buffer_overrun bucket description in + let exn = + Exceptions.Checkers (Localise.to_issue_id Localise.buffer_overrun, error_desc) in + let trace = [Errlog.make_trace_element 0 loc description []] in + Reporting.log_error pname ~loc ~ltr:trace exn | _ -> () in Dom.ConditionSet.iter report1 conds @@ -449,7 +462,7 @@ let compute_post Report.report_error pdesc cond_set; match entry_mem, exit_mem with | Some entry_mem, Some exit_mem -> - Some (entry_mem, exit_mem, cond_set) + Some (entry_mem, exit_mem, cond_set) | _ -> None let print_summary : Typ.Procname.t -> Dom.Summary.t -> unit diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 5f0fe7aa4..dc9c34bae 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -859,6 +859,8 @@ let ub : t -> Bound.t let of_int : int -> astate = fun n -> NonBottom (ItvPure.of_int n) +let of_int_lit n = of_int (IntLit.to_int n) + let is_bot : t -> bool = fun x -> equal x Bottom diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index 049860b2b..f9d3de86e 100644 --- a/infer/src/clang/cTrans.ml +++ b/infer/src/clang/cTrans.ml @@ -1676,11 +1676,37 @@ struct (* something's wrong *) { empty_res_trans with root_nodes = trans_state.succ_nodes } - and init_expr_trans trans_state var_exp_typ var_stmt_info init_expr_opt = + and init_dynamic_array trans_state array_exp_typ array_stmt_info dynlength_stmt_pointer = + let dynlength_stmt = Clang_ast_main.PointerMap.find dynlength_stmt_pointer + !CFrontend_config.pointer_stmt_index in + let dynlength_stmt_info, _ = Clang_ast_proj.get_stmt_tuple dynlength_stmt in + let trans_state_pri = PriorityNode.try_claim_priority_node trans_state array_stmt_info in + let dynlength_trans_result = instruction trans_state_pri dynlength_stmt in + let dynlength_exp_typ = extract_exp_from_list dynlength_trans_result.exps + "WARNING: There should be one expression.\n" in + let sil_loc = CLocation.get_sil_location dynlength_stmt_info trans_state_pri.context in + let call_instr = + let call_exp = Exp.Const (Const.Cfun BuiltinDecl.__set_array_length) in + let actuals = [array_exp_typ; dynlength_exp_typ] in + Sil.Call (None, call_exp, actuals, sil_loc, CallFlags.default) in + let call_trans_result = { empty_res_trans with instrs = [call_instr] } in + let res_trans = PriorityNode.compute_results_to_parent trans_state_pri sil_loc + "Initialize dynamic array length" dynlength_stmt_info + [dynlength_trans_result; call_trans_result] in + { res_trans with exps = [] } + + and init_expr_trans trans_state var_exp_typ ?qual_type var_stmt_info init_expr_opt = match init_expr_opt with - | None -> - (* Nothing to do if no init expression *) - { empty_res_trans with root_nodes = trans_state.succ_nodes } + | None -> ( + match Option.map ~f:(fun qt -> qt.Clang_ast_t.qt_type_ptr) qual_type + |> Option.find_map ~f:CAst_utils.get_type with + | Some (Clang_ast_t.VariableArrayType (_, _, stmt_pointer)) -> + (* Set the dynamic length of the variable length array. Variable length array cannot + have an initialization expression. *) + init_dynamic_array trans_state var_exp_typ var_stmt_info stmt_pointer + | _ -> + (* Nothing to do if no init expression and not a variable length array *) + { empty_res_trans with root_nodes = trans_state.succ_nodes}) | Some ie -> (*For init expr, translate how to compute it and assign to the var*) let var_exp, _ = var_exp_typ in let context = trans_state.context in @@ -1732,7 +1758,8 @@ struct let typ = CType_decl.qual_type_to_sil_type context.CContext.tenv qual_type in CVar_decl.add_var_to_locals procdesc var_decl typ pvar; let trans_state' = { trans_state with succ_nodes = next_node } in - init_expr_trans trans_state' (Exp.Lvar pvar, typ) stmt_info vdi.Clang_ast_t.vdi_init_expr in + init_expr_trans trans_state' (Exp.Lvar pvar, typ) ~qual_type stmt_info + vdi.Clang_ast_t.vdi_init_expr in match var_decls with | [] -> { empty_res_trans with root_nodes = next_nodes } diff --git a/infer/src/clang/cType_to_sil_type.ml b/infer/src/clang/cType_to_sil_type.ml index c16398721..6940247e4 100644 --- a/infer/src/clang/cType_to_sil_type.ml +++ b/infer/src/clang/cType_to_sil_type.ml @@ -97,7 +97,7 @@ and type_desc_of_c_type translate_decl tenv c_type : Typ.desc = | IncompleteArrayType (_, {arti_element_type; arti_stride}) | DependentSizedArrayType (_, {arti_element_type; arti_stride}) -> build_array_type translate_decl tenv arti_element_type None arti_stride - | VariableArrayType (_, {arti_element_type; arti_stride}) -> + | VariableArrayType (_, {arti_element_type; arti_stride}, _) -> build_array_type translate_decl tenv arti_element_type None arti_stride | ConstantArrayType (_, {arti_element_type; arti_stride}, n) -> build_array_type translate_decl tenv arti_element_type (Some n) arti_stride diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/array_dynlength.c b/infer/tests/codetoanalyze/c/bufferoverrun/array_dynlength.c new file mode 100644 index 000000000..2f8bbf5e1 --- /dev/null +++ b/infer/tests/codetoanalyze/c/bufferoverrun/array_dynlength.c @@ -0,0 +1,14 @@ +/* + * Copyright (c) 2013 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ + +void init_variable_array(int len) { + int x = 2 * len; + int a[len + x + 1]; + a[len + x + 1] = 0; +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 2b1fd29cc..5337fb023 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -1,3 +1,4 @@ +codetoanalyze/c/bufferoverrun/array_dynlength.c, init_variable_array, 3, BUFFER_OVERRUN, [Offset: [3xs$0 + 1, 3xs$1 + 1] Size: [3xs$0 + 1, 3xs$1 + 1] @ codetoanalyze/c/bufferoverrun/array_dynlength.c:13:3] codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 16, BUFFER_OVERRUN, [Offset: [0, 10] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/break_continue_return.c:29:5] codetoanalyze/c/bufferoverrun/do_while.c, do_while, 2, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/do_while.c:18:5 by call `do_while_sub()` ] codetoanalyze/c/bufferoverrun/do_while.c, do_while, 3, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/do_while.c:18:5 by call `do_while_sub()` ] diff --git a/infer/tests/codetoanalyze/c/frontend/initialization/array_initlistexpr.c b/infer/tests/codetoanalyze/c/frontend/initialization/array_initlistexpr.c index 980b30495..4baa5f1f6 100644 --- a/infer/tests/codetoanalyze/c/frontend/initialization/array_initlistexpr.c +++ b/infer/tests/codetoanalyze/c/frontend/initialization/array_initlistexpr.c @@ -7,7 +7,12 @@ * of patent rights can be found in the PATENTS file in the same directory. */ -int main() { +int init_const_array() { int z; int a[2][3] = {{z + 1, 2, 3}, {5, 6, 7}}; } + +void init_variable_array(int len) { + int x = 2 * len; + int a[len + x + 1]; +} diff --git a/infer/tests/codetoanalyze/c/frontend/initialization/array_initlistexpr.c.dot b/infer/tests/codetoanalyze/c/frontend/initialization/array_initlistexpr.c.dot index e08bb8228..b215624f6 100644 --- a/infer/tests/codetoanalyze/c/frontend/initialization/array_initlistexpr.c.dot +++ b/infer/tests/codetoanalyze/c/frontend/initialization/array_initlistexpr.c.dot @@ -1,14 +1,29 @@ /* @generated */ digraph iCFG { -"main.fad58de7366495db4650cfefac2fcd61_1" [label="1: Start main\nFormals: \nLocals: a:int[3*32][2*96] z:int \n DECLARE_LOCALS(&return,&a,&z); [line 10]\n " color=yellow style=filled] +"init_const_array.b1cf412cdbd1beaf15a9f6a3789043b9_1" [label="1: Start init_const_array\nFormals: \nLocals: a:int[3*32][2*96] z:int \n DECLARE_LOCALS(&return,&a,&z); [line 10]\n " color=yellow style=filled] - "main.fad58de7366495db4650cfefac2fcd61_1" -> "main.fad58de7366495db4650cfefac2fcd61_3" ; -"main.fad58de7366495db4650cfefac2fcd61_2" [label="2: Exit main \n " color=yellow style=filled] + "init_const_array.b1cf412cdbd1beaf15a9f6a3789043b9_1" -> "init_const_array.b1cf412cdbd1beaf15a9f6a3789043b9_3" ; +"init_const_array.b1cf412cdbd1beaf15a9f6a3789043b9_2" [label="2: Exit init_const_array \n " color=yellow style=filled] -"main.fad58de7366495db4650cfefac2fcd61_3" [label="3: DeclStmt \n n$0=*&z:int [line 12]\n *&a[0][0]:int=(n$0 + 1) [line 12]\n *&a[0][1]:int=2 [line 12]\n *&a[0][2]:int=3 [line 12]\n *&a[1][0]:int=5 [line 12]\n *&a[1][1]:int=6 [line 12]\n *&a[1][2]:int=7 [line 12]\n " shape="box"] +"init_const_array.b1cf412cdbd1beaf15a9f6a3789043b9_3" [label="3: DeclStmt \n n$0=*&z:int [line 12]\n *&a[0][0]:int=(n$0 + 1) [line 12]\n *&a[0][1]:int=2 [line 12]\n *&a[0][2]:int=3 [line 12]\n *&a[1][0]:int=5 [line 12]\n *&a[1][1]:int=6 [line 12]\n *&a[1][2]:int=7 [line 12]\n " shape="box"] - "main.fad58de7366495db4650cfefac2fcd61_3" -> "main.fad58de7366495db4650cfefac2fcd61_2" ; + "init_const_array.b1cf412cdbd1beaf15a9f6a3789043b9_3" -> "init_const_array.b1cf412cdbd1beaf15a9f6a3789043b9_2" ; +"init_variable_array.8cdc6857adcb1fd04fb6555d8ce3e4c1_1" [label="1: Start init_variable_array\nFormals: len:int\nLocals: a:int[_*32] x:int \n DECLARE_LOCALS(&return,&a,&x); [line 15]\n " color=yellow style=filled] + + + "init_variable_array.8cdc6857adcb1fd04fb6555d8ce3e4c1_1" -> "init_variable_array.8cdc6857adcb1fd04fb6555d8ce3e4c1_4" ; +"init_variable_array.8cdc6857adcb1fd04fb6555d8ce3e4c1_2" [label="2: Exit init_variable_array \n " color=yellow style=filled] + + +"init_variable_array.8cdc6857adcb1fd04fb6555d8ce3e4c1_3" [label="3: Fallback node \n n$0=*&len:int [line 17]\n n$1=*&x:int [line 17]\n _fun___set_array_length(&a:int[_*32],((n$0 + n$1) + 1):int) [line 17]\n " shape="box"] + + + "init_variable_array.8cdc6857adcb1fd04fb6555d8ce3e4c1_3" -> "init_variable_array.8cdc6857adcb1fd04fb6555d8ce3e4c1_2" ; +"init_variable_array.8cdc6857adcb1fd04fb6555d8ce3e4c1_4" [label="4: DeclStmt \n n$2=*&len:int [line 16]\n *&x:int=(2 * n$2) [line 16]\n " shape="box"] + + + "init_variable_array.8cdc6857adcb1fd04fb6555d8ce3e4c1_4" -> "init_variable_array.8cdc6857adcb1fd04fb6555d8ce3e4c1_3" ; }