From 66ed16fd2790ac9662306b4a3790d95e449b00a7 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Mon, 6 Apr 2020 06:41:27 -0700 Subject: [PATCH] [clang] skip initialisation of large compound values Summary: It's easy to create large arrays in code, eg `int x[1UL << 16];`, but these can generate huge nodes in SIL because zero-initialization is translated by zero-ing structures element by element. Introduce a builtin to use instead. Keep the naive method for small structures (with a configurable limit on "small"). Reviewed By: dulmarod Differential Revision: D20836836 fbshipit-source-id: 6bf5410f8 --- infer/man/man1/infer-analyze.txt | 5 + infer/man/man1/infer-capture.txt | 5 + infer/man/man1/infer-full.txt | 5 + infer/man/man1/infer.txt | 5 + infer/src/IR/BUILTINS.ml | 2 + infer/src/IR/BuiltinDecl.ml | 2 + infer/src/base/Config.ml | 9 ++ infer/src/base/Config.mli | 2 + infer/src/biabduction/BuiltinDefn.ml | 2 + infer/src/clang/cTrans.ml | 133 +++++++++++------- .../cpp/frontend/initialization/zero_init.cpp | 25 ++++ .../frontend/initialization/zero_init.cpp.dot | 36 +++++ 12 files changed, 179 insertions(+), 52 deletions(-) create mode 100644 infer/tests/codetoanalyze/cpp/frontend/initialization/zero_init.cpp create mode 100644 infer/tests/codetoanalyze/cpp/frontend/initialization/zero_init.cpp.dot diff --git a/infer/man/man1/infer-analyze.txt b/infer/man/man1/infer-analyze.txt index 4484c1aa1..ed05c4942 100644 --- a/infer/man/man1/infer-analyze.txt +++ b/infer/man/man1/infer-analyze.txt @@ -371,6 +371,11 @@ CLANG OPTIONS Override sources in all cxx annotation reachability specs with the given sources spec + --clang-compound-literal-init-limit int + Limit after which initialization of compound types (structs and + arrays) is not done element by element but using a builtin + function that each analysis has to model. + --cxx-scope-guards json Specify scope guard classes that can be read only by destructors without being reported as dead stores. diff --git a/infer/man/man1/infer-capture.txt b/infer/man/man1/infer-capture.txt index b0e58aff8..9bb58a5b3 100644 --- a/infer/man/man1/infer-capture.txt +++ b/infer/man/man1/infer-capture.txt @@ -218,6 +218,11 @@ CLANG OPTIONS --clang-blacklisted-flags-with-arg +string Clang flags (taking args) to filter out + --clang-compound-literal-init-limit int + Limit after which initialization of compound types (structs and + arrays) is not done element by element but using a builtin + function that each analysis has to model. + --compilation-database +path File that contain compilation commands (can be specified multiple times) diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index 2980312fc..668dba217 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -220,6 +220,11 @@ OPTIONS --clang-blacklisted-flags-with-arg +string Clang flags (taking args) to filter out See also infer-capture(1). + --clang-compound-literal-init-limit int + Limit after which initialization of compound types (structs and + arrays) is not done element by element but using a builtin + function that each analysis has to model. See also infer-analyze(1) and infer-capture(1). + --class-loads Activates: Java class loading analysis (Conversely: --no-class-loads) See also infer-analyze(1). diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index ecb44513f..39498333d 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -220,6 +220,11 @@ OPTIONS --clang-blacklisted-flags-with-arg +string Clang flags (taking args) to filter out See also infer-capture(1). + --clang-compound-literal-init-limit int + Limit after which initialization of compound types (structs and + arrays) is not done element by element but using a builtin + function that each analysis has to model. See also infer-analyze(1) and infer-capture(1). + --class-loads Activates: Java class loading analysis (Conversely: --no-class-loads) See also infer-analyze(1). diff --git a/infer/src/IR/BUILTINS.ml b/infer/src/IR/BUILTINS.ml index 3b8b5d540..598908dc5 100644 --- a/infer/src/IR/BUILTINS.ml +++ b/infer/src/IR/BUILTINS.ml @@ -135,4 +135,6 @@ module type S = sig val vwscanf : t val wscanf : t + + val zero_initialization : t end diff --git a/infer/src/IR/BuiltinDecl.ml b/infer/src/IR/BuiltinDecl.ml index 7e82da1a7..1caffb813 100644 --- a/infer/src/IR/BuiltinDecl.ml +++ b/infer/src/IR/BuiltinDecl.ml @@ -174,3 +174,5 @@ let vswscanf = create_procname "vswscanf" let vwscanf = create_procname "vwscanf" let wscanf = create_procname "wscanf" + +let zero_initialization = create_procname "__infer_zero_initialization" diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 2c2c84580..c2f301cb0 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -851,6 +851,13 @@ and clang_biniou_file = ~meta:"file" "Specify a file containing the AST of the program, in biniou format" +and clang_compound_literal_init_limit = + CLOpt.mk_int ~default:5 ~long:"clang-compound-literal-init-limit" + ~in_help:InferCommand.[(Analyze, manual_clang); (Capture, manual_clang)] + "Limit after which initialization of compound types (structs and arrays) is not done element \ + by element but using a builtin function that each analysis has to model." + + and clang_extra_flags = CLOpt.mk_string_list ~long:"Xclang" ~in_help:InferCommand.[(Capture, manual_clang)] @@ -2637,6 +2644,8 @@ and checkers = List.map !all_checkers ~f:(fun (checker, _, var) -> (checker, !va and clang_biniou_file = !clang_biniou_file +and clang_compound_literal_init_limit = !clang_compound_literal_init_limit + and clang_extra_flags = !clang_extra_flags and clang_blacklisted_flags = !clang_blacklisted_flags diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index cee80e652..0bccfc7ea 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -260,6 +260,8 @@ val check_version : string option val clang_biniou_file : string option +val clang_compound_literal_init_limit : int + val clang_extra_flags : string list val clang_blacklisted_flags : string list diff --git a/infer/src/biabduction/BuiltinDefn.ml b/infer/src/biabduction/BuiltinDefn.ml index 2f69067c6..c60af8db7 100644 --- a/infer/src/biabduction/BuiltinDefn.ml +++ b/infer/src/biabduction/BuiltinDefn.ml @@ -1006,6 +1006,8 @@ let vwscanf = Builtin.register BuiltinDecl.vwscanf (execute_scan_function 1) let wscanf = Builtin.register BuiltinDecl.wscanf (execute_scan_function 1) +let zero_initialization = Builtin.register BuiltinDecl.zero_initialization execute_skip + (* Function exists to load module and guarantee that the side-effects of Builtin.register calls have been done. *) let init () = () diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index 78fadaea3..5b1de47c8 100644 --- a/infer/src/clang/cTrans.ml +++ b/infer/src/clang/cTrans.ml @@ -387,57 +387,6 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s mk_trans_result (zero, typ) empty_control - (** Create instructions to initialize record with zeroes. It needs to traverse whole type - structure, to assign 0 values to all transitive fields because of AST construction in C - translation *) - let implicitValueInitExpr_trans trans_state stmt_info = - match trans_state.var_exp_typ with - | Some var_exp_typ -> - (* This node will always be child of InitListExpr, claiming priority will always fail *) - let tenv = trans_state.context.CContext.tenv in - let sil_loc = - CLocation.location_of_stmt_info - trans_state.context.CContext.translation_unit_context.source_file stmt_info - in - (* Traverse structure of a type and initialize int/float/ptr fields with zero *) - let rec fill_typ_with_zero ((exp, typ) as exp_typ) = - match typ.Typ.desc with - | Tstruct tn -> - let field_exp_typs = - match Tenv.lookup tenv tn with - | Some {fields} -> - List.map fields ~f:(fun (fieldname, fieldtype, _) -> - (Exp.Lfield (exp, fieldname, typ), fieldtype) ) - | None -> - assert false - in - List.map field_exp_typs ~f:(fun exp_typ -> (fill_typ_with_zero exp_typ).control) - |> collect_controls trans_state.context.procdesc - |> mk_trans_result exp_typ - | Tarray {elt= field_typ; length= Some n} -> - let size = IntLit.to_int_exn n in - let indices = CGeneral_utils.list_range 0 (size - 1) in - List.map indices ~f:(fun i -> - let idx_exp = Exp.Const (Const.Cint (IntLit.of_int i)) in - let field_exp = Exp.Lindex (exp, idx_exp) in - (fill_typ_with_zero (field_exp, field_typ)).control ) - |> collect_controls trans_state.context.procdesc - |> mk_trans_result exp_typ - | Tint _ | Tfloat _ | Tptr _ -> - let zero_exp = Exp.zero_of_type_exn typ in - let instrs = [Sil.Store {e1= exp; root_typ= typ; typ; e2= zero_exp; loc= sil_loc}] in - mk_trans_result (exp, typ) {empty_control with instrs} - | Tfun | Tvoid | Tarray _ | TVar _ -> - CFrontend_errors.unimplemented __POS__ stmt_info.Clang_ast_t.si_source_range - "fill_typ_with_zero on type %a" (Typ.pp Pp.text) typ - in - let res_trans = fill_typ_with_zero var_exp_typ in - {res_trans with control= {res_trans.control with initd_exps= [fst var_exp_typ]}} - | None -> - CFrontend_errors.unimplemented __POS__ stmt_info.Clang_ast_t.si_source_range - "Retrieving var from non-InitListExpr parent" - - let no_op_trans succ_nodes = mk_trans_result (mk_fresh_void_exp_typ ()) {empty_control with root_nodes= succ_nodes} @@ -747,6 +696,86 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s {empty_control with root_nodes= [root_node']; leaf_nodes= trans_state.succ_nodes} + (** Create instructions to initialize record with zeroes. It needs to traverse whole type + structure, to assign 0 values to all transitive fields because of AST construction in C + translation *) + and implicitValueInitExpr_trans trans_state stmt_info = + match trans_state.var_exp_typ with + | None -> + CFrontend_errors.unimplemented __POS__ stmt_info.Clang_ast_t.si_source_range + "Retrieving var from non-InitListExpr parent" + | Some var_exp_typ -> + (* This node will always be child of InitListExpr, claiming priority will always fail *) + let tenv = trans_state.context.CContext.tenv in + let sil_loc = + CLocation.location_of_stmt_info + trans_state.context.CContext.translation_unit_context.source_file stmt_info + in + (* Traverse structure of a type and initialize int/float/ptr fields with zero *) + let rec fill_typ_with_zero ((exp, typ) as exp_typ) = + let init_with_builtin = + match typ.Typ.desc with + | Tstruct tn -> ( + match Tenv.lookup tenv tn with + | Some {fields} -> + List.length fields > Config.clang_compound_literal_init_limit + | None -> + assert false ) + | Tarray {length= Some n} -> + IntLit.gt n (IntLit.of_int Config.clang_compound_literal_init_limit) + | Tint _ | Tfloat _ | Tptr _ -> + false + | Tfun | Tvoid | Tarray _ | TVar _ -> + true + in + if init_with_builtin then + let ret_id = Ident.create_fresh Ident.knormal in + let call_instr = + Sil.Call + ( (ret_id, Typ.void) + , Const (Cfun BuiltinDecl.zero_initialization) + , [exp_typ] + , sil_loc + , CallFlags.default ) + in + mk_trans_result exp_typ {empty_control with instrs= [call_instr]} + else + match typ.Typ.desc with + | Tstruct tn -> + let field_exp_typs = + match Tenv.lookup tenv tn with + | Some {fields} -> + List.map fields ~f:(fun (fieldname, fieldtype, _) -> + (Exp.Lfield (exp, fieldname, typ), fieldtype) ) + | None -> + assert false + in + List.map field_exp_typs ~f:(fun exp_typ -> (fill_typ_with_zero exp_typ).control) + |> collect_controls trans_state.context.procdesc + |> mk_trans_result exp_typ + | Tarray {elt= field_typ; length= Some n} -> + let size = IntLit.to_int_exn n in + let indices = CGeneral_utils.list_range 0 (size - 1) in + List.map indices ~f:(fun i -> + let idx_exp = Exp.Const (Const.Cint (IntLit.of_int i)) in + let field_exp = Exp.Lindex (exp, idx_exp) in + (fill_typ_with_zero (field_exp, field_typ)).control ) + |> collect_controls trans_state.context.procdesc + |> mk_trans_result exp_typ + | Tint _ | Tfloat _ | Tptr _ -> + let zero_exp = Exp.zero_of_type_exn typ in + let instrs = + [Sil.Store {e1= exp; root_typ= typ; typ; e2= zero_exp; loc= sil_loc}] + in + mk_trans_result (exp, typ) {empty_control with instrs} + | Tfun | Tvoid | Tarray _ | TVar _ -> + CFrontend_errors.unimplemented __POS__ stmt_info.Clang_ast_t.si_source_range + "fill_typ_with_zero on type %a" (Typ.pp Pp.text) typ + in + let res_trans = fill_typ_with_zero var_exp_typ in + {res_trans with control= {res_trans.control with initd_exps= [fst var_exp_typ]}} + + and var_deref_trans trans_state stmt_info (decl_ref : Clang_ast_t.decl_ref) = let context = trans_state.context in let _, _, qual_type = CAst_utils.get_info_from_decl_ref decl_ref in @@ -2292,7 +2321,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s in let all_res_trans = match var_typ.Typ.desc with - | Typ.Tarray {elt} -> + | Tarray {elt} -> initListExpr_array_trans trans_state_pri init_stmt_info stmts var_exp elt | Tstruct _ -> initListExpr_struct_trans trans_state_pri init_stmt_info stmts var_exp var_typ diff --git a/infer/tests/codetoanalyze/cpp/frontend/initialization/zero_init.cpp b/infer/tests/codetoanalyze/cpp/frontend/initialization/zero_init.cpp new file mode 100644 index 000000000..6f1fb1a06 --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/frontend/initialization/zero_init.cpp @@ -0,0 +1,25 @@ +/* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ + +namespace zero_init { + +struct X { + // ridiculously large array's initialization should not be translated index by + // index by the frontend + static constexpr unsigned int kMaxKeys = 1UL << 16; + void* keys_[kMaxKeys]; + constexpr X() : keys_() {} +}; + +struct Y { + // this is small and can be translated index by index to save modelling burden + // in analyses + void* keys_[3]; + constexpr Y() : keys_() {} +}; + +} // namespace zero_init diff --git a/infer/tests/codetoanalyze/cpp/frontend/initialization/zero_init.cpp.dot b/infer/tests/codetoanalyze/cpp/frontend/initialization/zero_init.cpp.dot new file mode 100644 index 000000000..132b679a1 --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/frontend/initialization/zero_init.cpp.dot @@ -0,0 +1,36 @@ +/* @generated */ +digraph cfg { +"kMaxKeys#X#__infer_globals_initializer_zero_init.cd983beeff3879de64cad137bc5d5f8c_1" [label="1: Start __infer_globals_initializer_zero_init::X::kMaxKeys\nFormals: \nLocals: \n " color=yellow style=filled] + + + "kMaxKeys#X#__infer_globals_initializer_zero_init.cd983beeff3879de64cad137bc5d5f8c_1" -> "kMaxKeys#X#__infer_globals_initializer_zero_init.cd983beeff3879de64cad137bc5d5f8c_3" ; +"kMaxKeys#X#__infer_globals_initializer_zero_init.cd983beeff3879de64cad137bc5d5f8c_2" [label="2: Exit __infer_globals_initializer_zero_init::X::kMaxKeys \n " color=yellow style=filled] + + +"kMaxKeys#X#__infer_globals_initializer_zero_init.cd983beeff3879de64cad137bc5d5f8c_3" [label="3: DeclStmt \n VARIABLE_DECLARED(#GB$zero_init::X::kMaxKeys:unsigned int const ); [line 13, column 3]\n *&#GB$zero_init::X::kMaxKeys:unsigned int const =(unsigned int const )(1 << 16) [line 13, column 3]\n " shape="box"] + + + "kMaxKeys#X#__infer_globals_initializer_zero_init.cd983beeff3879de64cad137bc5d5f8c_3" -> "kMaxKeys#X#__infer_globals_initializer_zero_init.cd983beeff3879de64cad137bc5d5f8c_2" ; +"X#X#zero_init#{277870330798338824|constexpr}.16c2d483086de887db705c1e51a1bf78_1" [label="1: Start zero_init::X::X\nFormals: this:zero_init::X*\nLocals: \n " color=yellow style=filled] + + + "X#X#zero_init#{277870330798338824|constexpr}.16c2d483086de887db705c1e51a1bf78_1" -> "X#X#zero_init#{277870330798338824|constexpr}.16c2d483086de887db705c1e51a1bf78_3" ; +"X#X#zero_init#{277870330798338824|constexpr}.16c2d483086de887db705c1e51a1bf78_2" [label="2: Exit zero_init::X::X \n " color=yellow style=filled] + + +"X#X#zero_init#{277870330798338824|constexpr}.16c2d483086de887db705c1e51a1bf78_3" [label="3: Constructor Init \n n$1=*&this:zero_init::X* [line 15, column 19]\n n$2=_fun___infer_zero_initialization(n$1.keys_:void*[65536*8]) [line 15, column 25]\n " shape="box"] + + + "X#X#zero_init#{277870330798338824|constexpr}.16c2d483086de887db705c1e51a1bf78_3" -> "X#X#zero_init#{277870330798338824|constexpr}.16c2d483086de887db705c1e51a1bf78_2" ; +"Y#Y#zero_init#{11751607535979846847|constexpr}.3d7bacd58f9f66a28604db198e91fa11_1" [label="1: Start zero_init::Y::Y\nFormals: this:zero_init::Y*\nLocals: \n " color=yellow style=filled] + + + "Y#Y#zero_init#{11751607535979846847|constexpr}.3d7bacd58f9f66a28604db198e91fa11_1" -> "Y#Y#zero_init#{11751607535979846847|constexpr}.3d7bacd58f9f66a28604db198e91fa11_3" ; +"Y#Y#zero_init#{11751607535979846847|constexpr}.3d7bacd58f9f66a28604db198e91fa11_2" [label="2: Exit zero_init::Y::Y \n " color=yellow style=filled] + + +"Y#Y#zero_init#{11751607535979846847|constexpr}.3d7bacd58f9f66a28604db198e91fa11_3" [label="3: Constructor Init \n n$1=*&this:zero_init::Y* [line 22, column 19]\n *n$1.keys_[0]:void*=null [line 22, column 25]\n *n$1.keys_[1]:void*=null [line 22, column 25]\n *n$1.keys_[2]:void*=null [line 22, column 25]\n " shape="box"] + + + "Y#Y#zero_init#{11751607535979846847|constexpr}.3d7bacd58f9f66a28604db198e91fa11_3" -> "Y#Y#zero_init#{11751607535979846847|constexpr}.3d7bacd58f9f66a28604db198e91fa11_2" ; +}