[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

@@ -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.

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)

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).

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).

infer/src/IR/BUILTINS.ml

@@ -135,4 +135,6 @@ module type S = sig
   val vwscanf : t
 
   val wscanf : t
+
+  val zero_initialization : t
 end

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"

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

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

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 () = ()

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

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

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<codetoanalyze/cpp/frontend/initialization/zero_init.cpp|const|ice>$zero_init::X::kMaxKeys:unsigned int const ); [line 13, column 3]\n  *&#GB<codetoanalyze/cpp/frontend/initialization/zero_init.cpp|const|ice>$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" ;
+}