[SIOF] detect which variables need initialization

Summary:
- do a semantic analysis of each variable initializer to figure out if they need initialization
- add a flag to globals that is true when they are `constexpr`. In that case, no analysis is needed as the user + compile guarantee that it is a compile-time constant.

Reviewed By: sblackshear

Differential Revision: D4081273

fbshipit-source-id: 44dbe29

infer/src/IR/Pvar.re

@@ -26,7 +26,7 @@ type pvar_kind =
   | Abduced_retvar Procname.t Location.t /** synthetic variable to represent return value */
   | Abduced_ref_param Procname.t t Location.t
   /** synthetic variable to represent param passed by reference */
-  | Global_var DB.source_file /** global variable */
+  | Global_var (DB.source_file, bool) /** global variable: translation unit + is it compile constant? */
   | Seed_var /** variable used to store the initial value of formal parameters */
 /** Names for program variables. */
 and t = {pv_name: Mangled.t, pv_kind: pvar_kind};
@@ -62,7 +62,13 @@ let rec pvar_kind_compare k1 k2 =>
     }
   | (Abduced_ref_param _, _) => (-1)
   | (_, Abduced_ref_param _) => 1
-  | (Global_var f1, Global_var f2) => DB.source_file_compare f1 f2
+  | (Global_var (f1, b1), Global_var (f2, b2)) =>
+    let n = DB.source_file_compare f1 f2;
+    if (n != 0) {
+      n
+    } else {
+      bool_compare b1 b2
+    }
   | (Global_var _, _) => (-1)
   | (_, Global_var _) => 1
   | (Seed_var, Seed_var) => 0
@@ -105,7 +111,9 @@ let rec _pp f pv => {
     } else {
       F.fprintf f "%a$%a%a|abducedRefParam" Procname.pp n Location.pp l Mangled.pp name
     }
-  | Global_var fname => F.fprintf f "#GB<%s>$%a" (DB.source_file_to_string fname) Mangled.pp name
+  | Global_var (fname, b) =>
+    F.fprintf
+      f "#GB<%s%s>$%a" (DB.source_file_to_string fname) (if b {"|const"} else {""}) Mangled.pp name
   | Seed_var => F.fprintf f "old_%a" Mangled.pp name
   }
 };
@@ -319,7 +327,10 @@ let mk_callee (name: Mangled.t) (proc_name: Procname.t) :t => {
 
 
 /** create a global variable with the given name */
-let mk_global (name: Mangled.t) fname :t => {pv_name: name, pv_kind: Global_var fname};
+let mk_global is_constexpr::is_constexpr=false (name: Mangled.t) fname :t => {
+  pv_name: name,
+  pv_kind: Global_var (fname, is_constexpr)
+};
 
 
 /** create a fresh temporary variable local to procedure [pname]. for use in the frontends only! */
@@ -343,7 +354,22 @@ let mk_abduced_ref_param (proc_name: Procname.t) (pv: t) (loc: Location.t) :t =>
 
 let get_source_file pvar =>
   switch pvar.pv_kind {
-  | Global_var f => Some f
+  | Global_var (f, _) => Some f
+  | _ => None
+  };
+
+let is_compile_constant pvar =>
+  switch pvar.pv_kind {
+  | Global_var (_, b) => b
+  | _ => false
+  };
+
+let get_initializer_pname {pv_name, pv_kind} =>
+  switch pv_kind {
+  | Global_var _ =>
+    Some (
+      Procname.from_string_c_fun (Config.clang_initializer_prefix ^ Mangled.to_string_full pv_name)
+    )
   | _ => None
   };
 

infer/src/IR/Pvar.rei

@@ -104,7 +104,7 @@ let mk_callee: Mangled.t => Procname.t => t;
 
 
 /** create a global variable with the given name */
-let mk_global: Mangled.t => DB.source_file => t;
+let mk_global: is_constexpr::bool? => Mangled.t => DB.source_file => t;
 
 
 /** create a fresh temporary variable local to procedure [pname]. for use in the frontends only! */
@@ -134,6 +134,16 @@ let to_seed: t => t;
 /** Convert a pvar to string. */
 let to_string: t => string;
 
+
+/** Get the source file corresponding to a global, if known. Returns [None] if not a global. */
 let get_source_file: t => option DB.source_file;
 
+
+/** Is the variable's value a compile-time constant? Always [false] for non-globals. */
+let is_compile_constant: t => bool;
+
+
+/** Get the procname of the initializer function for the given global variable */
+let get_initializer_pname: t => option Procname.t;
+
 let module Set: PrettyPrintable.PPSet with type elt = t;

infer/src/backend/specs.ml

@@ -326,7 +326,7 @@ type payload =
     crashcontext_frame: Stacktree_j.stacktree option;
     (** Proc location and blame_range info for crashcontext analysis *)
     quandary : QuandarySummary.t option;
-    globals_read: Pvar.Set.t option;
+    siof : SiofDomain.astate option;
   }
 
 type summary =
@@ -761,7 +761,7 @@ let empty_payload =
     calls = None;
     crashcontext_frame = None;
     quandary = None;
-    globals_read = None;
+    siof = None;
   }
 
 (** [init_summary (depend_list, nodes,

infer/src/backend/specs.mli

@@ -130,7 +130,7 @@ type payload =
     crashcontext_frame: Stacktree_j.stacktree option;
     (** Procedure location and blame_range info for crashcontext analysis *)
     quandary : QuandarySummary.t option;
-    globals_read: Pvar.Set.t option;
+    siof : SiofDomain.astate option;
   }
 
 (** Procedure summary *)

infer/src/checkers/abstractDomain.ml

@@ -26,7 +26,7 @@ module BottomLifted (Domain : S) = struct
     | Bottom
     | NonBottom of Domain.astate
 
-  let initial = NonBottom Domain.initial
+  let initial = Bottom
 
   let (<=) ~lhs ~rhs =
     if lhs == rhs

infer/src/checkers/siof.ml

@@ -12,54 +12,77 @@ open! Utils
 module F = Format
 module L = Logging
 
-module Domain = AbstractDomain.FiniteSet(Pvar.Set)
-
 module Summary = Summary.Make (struct
-    type summary = Domain.astate
+    type summary = SiofDomain.astate
 
     let update_payload astate payload =
-      { payload with Specs.globals_read = Some astate }
+      { payload with Specs.siof = Some astate }
 
     let read_from_payload payload =
-      match payload.Specs.globals_read with
+      match payload.Specs.siof with
       | Some astate -> astate
-      | None -> Domain.initial
+      | None -> SiofDomain.initial
   end)
 
 module TransferFunctions (CFG : ProcCfg.S) = struct
   module CFG = CFG
-  module Domain = Domain
+  module Domain = SiofDomain
   type extras = ProcData.no_extras
 
-  let get_globals e =
-    Exp.get_vars e |> snd |> IList.filter Pvar.is_global |> Domain.of_list
+  let is_semantically_compile_constant tenv pdesc pv =
+    match Pvar.get_initializer_pname pv with
+    | Some pname -> (
+        match Summary.read_summary tenv pdesc pname with
+        | Some (Domain.NonBottom _) -> false
+        | Some Domain.Bottom | None -> true
+      )
+    | None -> true
+
+  let get_globals tenv pdesc e =
+    let is_dangerous_global pv =
+      Pvar.is_global pv
+      && not (Pvar.is_compile_constant pv
+              || is_semantically_compile_constant tenv pdesc pv) in
+    let globals = Exp.get_vars e |> snd |> IList.filter is_dangerous_global in
+    if globals = [] then
+      Domain.Bottom
+    else
+      Domain.NonBottom (SiofDomain.PvarSetDomain.of_list globals)
+
+  let add_params_globals astate tenv pdesc params =
+    IList.map fst params
+    |> IList.map (fun e -> get_globals tenv pdesc e)
+    |> IList.fold_left Domain.join astate
+
+  let at_least_bottom =
+    Domain.join (Domain.NonBottom SiofDomain.PvarSetDomain.empty)
 
   let exec_instr astate { ProcData.pdesc; tenv } _ (instr : Sil.instr) = match instr with
     | Load (_, exp, _, _)
     | Store (_, _, exp, _)
     | Prune (exp, _, _, _) ->
-        let globals = get_globals exp in
-        Domain.union astate globals
+        Domain.join astate (get_globals tenv pdesc exp)
     | Call (_, Const (Cfun callee_pname), params, _, _) ->
-        let param_globals =
-          IList.map fst params
-          |> IList.map get_globals
-          |> IList.fold_left Domain.union astate in
         let callee_globals =
           Option.default Domain.initial
           @@ Summary.read_summary tenv pdesc callee_pname in
-        Domain.union callee_globals param_globals
+        add_params_globals astate tenv pdesc params
+        |> Domain.join callee_globals
+        |>
+        (* make sure it's not Bottom: we made a function call so this needs initialization *)
+        at_least_bottom
     | Call (_, _, params, _, _) ->
-        IList.map fst params
-        |> IList.map get_globals
-        |> IList.fold_left Domain.union astate
+        add_params_globals astate tenv pdesc params
+        |>
+        (* make sure it's not Bottom: we made a function call so this needs initialization *)
+        at_least_bottom
     | Declare_locals _ | Remove_temps _ | Abstract _ | Nullify _ ->
         astate
 end
 
 module Analyzer =
   AbstractInterpreter.Make
-    (ProcCfg.Backward(ProcCfg.Exceptional))
+    (ProcCfg.Normal)
     (Scheduler.ReversePostorder)
     (TransferFunctions)
 
@@ -88,19 +111,20 @@ let report_siof pname loc bad_globals =
 
 
 let siof_check pdesc = function
-  | Some post ->
+  | Some (SiofDomain.NonBottom post) ->
       let attrs = Cfg.Procdesc.get_attributes pdesc in
       let is_orig_file f = match attrs.ProcAttributes.translation_unit with
         | Some orig_file ->
             let orig_path = DB.source_file_to_abs_path orig_file in
-            string_equal orig_path @@ DB.source_file_to_abs_path f
+            string_equal orig_path (DB.source_file_to_abs_path f)
         | None -> false in
       let is_foreign v = Option.map_default
-          (fun f -> not @@ is_orig_file f) false (Pvar.get_source_file v) in
-      let foreign_globals = Domain.filter is_foreign post in
-      if not (Domain.is_empty foreign_globals) then
+          (fun f -> not (is_orig_file f)) false (Pvar.get_source_file v) in
+      let foreign_globals = SiofDomain.PvarSetDomain.filter is_foreign post in
+      if not (SiofDomain.PvarSetDomain.is_empty foreign_globals) then
         report_siof (Cfg.Procdesc.get_proc_name pdesc) attrs.ProcAttributes.loc foreign_globals;
-  | None -> ()
+  | Some SiofDomain.Bottom | None ->
+      ()
 
 let checker callback =
   let pdesc = callback.Callbacks.proc_desc in
@@ -109,4 +133,5 @@ let checker callback =
   match pname with
   | Procname.C c when Procname.is_globals_initializer c ->
       siof_check pdesc post
-  | _ -> ()
+  | _ ->
+      ()

infer/src/checkers/siofDomain.ml

@@ -0,0 +1,21 @@
+(*
+ * Copyright (c) 2016 - 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.
+ *)
+module PvarSetDomain = AbstractDomain.FiniteSet(Pvar.Set)
+
+(* The domain for the analysis is sets of global variables if an initialization is needed at
+   runtime, or Bottom if no initialization is needed. For instance, `int x = 32; int y = x * 52;`
+   gives a summary of Bottom for both initializers corresponding to these globals, but `int x =
+   foo();` gives a summary of at least "NonBottom {}" for x's initializer since x will need runtime
+   initialization.
+
+   The encoding in terms of a BottomLifted domain is an efficiency hack to represent two pieces of
+   information: whether a global variable (via its initializer function) requires runtime
+   initialization, and which globals requiring initialization a given function (transitively)
+   accesses. *)
+include AbstractDomain.BottomLifted(PvarSetDomain)

infer/src/clang/cFrontend_decl.ml

@@ -220,11 +220,16 @@ struct
             | Some dec ->
                 Logging.out "Methods of %s skipped\n" (Ast_utils.string_of_decl dec)
             | None -> ())
-       | VarDecl (decl_info, { ni_name }, _, { vdi_is_global; vdi_init_expr })
+       | VarDecl (decl_info, named_decl_info, _, ({ vdi_is_global; vdi_init_expr } as vdi))
          when vdi_is_global && Option.is_some vdi_init_expr ->
            (* create a fake procedure that initializes the global variable so that the variable
               initializer can be analyzed by the backend (eg, the SIOF checker) *)
-           let procname = Procname.from_string_c_fun (Config.clang_initializer_prefix ^ ni_name) in
+           let procname =
+             (* create the corresponding global variable to get the right pname for its
+                initializer *)
+             let global = General_utils.mk_sil_global_var trans_unit_ctx named_decl_info vdi in
+             (* safe to Option.get because it's a global *)
+             Option.get (Pvar.get_initializer_pname global) in
            let ms = CMethod_signature.make_ms procname [] Ast_expressions.create_void_type
                [] decl_info.Clang_ast_t.di_source_range false trans_unit_ctx.CFrontend_config.lang
                None None None in

infer/src/clang/cFrontend_utils.ml

@@ -536,7 +536,7 @@ let get_fresh_block_index () =
 module General_utils =
 struct
 
-  type var_info = Clang_ast_t.decl_info * Clang_ast_t.type_ptr * Clang_ast_t.var_decl_info * bool
+  type var_info = Clang_ast_t.decl_info * Clang_ast_t.qual_type * Clang_ast_t.var_decl_info * bool
 
   let rec swap_elements_list l =
     match l with
@@ -774,24 +774,29 @@ struct
       | None -> Mangled.from_string name_string in
     name_string, mangled
 
-  let mk_sil_var {CFrontend_config.source_file} name decl_info_type_ptr_opt
-      procname outer_procname =
-    let name_string = Ast_utils.get_qualified_name name in
+  let mk_sil_global_var {CFrontend_config.source_file} ?(mk_name=fun _ x -> x)
+      named_decl_info var_decl_info =
+    let name_string, simple_name = get_var_name_mangled named_decl_info var_decl_info in
+    let translation_unit =
+      match var_decl_info.Clang_ast_t.vdi_storage_class with
+      | Some "extern" ->
+          DB.source_file_empty
+      | _ ->
+          source_file in
+    let is_constexpr = var_decl_info.Clang_ast_t.vdi_is_const_expr in
+    Pvar.mk_global ~is_constexpr (mk_name name_string simple_name) translation_unit
+
+  let mk_sil_var trans_unit_ctx named_decl_info decl_info_type_ptr_opt procname outer_procname =
     match decl_info_type_ptr_opt with
     | Some (decl_info, _, var_decl_info, should_be_mangled) ->
-        let name_string, simple_name = get_var_name_mangled name var_decl_info in
+        let name_string, simple_name = get_var_name_mangled named_decl_info var_decl_info in
         if var_decl_info.Clang_ast_t.vdi_is_global then
-          let global_mangled_name =
+          let mk_name =
             if var_decl_info.Clang_ast_t.vdi_is_static_local then
-              Mangled.from_string ((Procname.to_string outer_procname) ^ "_" ^ name_string)
-            else simple_name in
-          let translation_unit =
-            match var_decl_info.Clang_ast_t.vdi_storage_class with
-            | Some "extern" ->
-                DB.source_file_empty
-            | _ ->
-                source_file in
-          Pvar.mk_global global_mangled_name translation_unit
+              Some (fun name_string _ ->
+                  Mangled.from_string ((Procname.to_string outer_procname) ^ "_" ^ name_string))
+            else None in
+          mk_sil_global_var trans_unit_ctx ?mk_name named_decl_info var_decl_info
         else if not should_be_mangled then Pvar.mk simple_name procname
         else
           let start_location = fst decl_info.Clang_ast_t.di_source_range in
@@ -800,6 +805,8 @@ struct
           let mangled = string_crc_hex32 line_str in
           let mangled_name = Mangled.mangled name_string mangled in
           Pvar.mk mangled_name procname
-    | None -> Pvar.mk (Mangled.from_string name_string) procname
+    | None ->
+        let name_string = Ast_utils.get_qualified_name named_decl_info in
+        Pvar.mk (Mangled.from_string name_string) procname
 
 end

infer/src/clang/cFrontend_utils.mli

@@ -180,7 +180,7 @@ end
 module General_utils :
 sig
 
-  type var_info = Clang_ast_t.decl_info * Clang_ast_t.type_ptr * Clang_ast_t.var_decl_info * bool
+  type var_info = Clang_ast_t.decl_info * Clang_ast_t.qual_type * Clang_ast_t.var_decl_info * bool
 
   val string_from_list : string list -> string
 
@@ -243,6 +243,10 @@ sig
   val get_var_name_mangled : Clang_ast_t.named_decl_info -> Clang_ast_t.var_decl_info ->
     (string * Mangled.t)
 
+  val mk_sil_global_var : CFrontend_config.translation_unit_context ->
+    ?mk_name:(string -> Mangled.t -> Mangled.t) ->
+    Clang_ast_t.named_decl_info -> Clang_ast_t.var_decl_info -> Pvar.t
+
   val mk_sil_var : CFrontend_config.translation_unit_context -> Clang_ast_t.named_decl_info ->
     var_info option -> Procname.t -> Procname.t -> Pvar.t
 

infer/src/clang/cVar_decl.ml

@@ -28,11 +28,11 @@ let sil_var_of_decl context var_decl procname =
       let shoud_be_mangled =
         not (is_custom_var_pointer decl_info.Clang_ast_t.di_pointer) in
       let var_decl_details = Some
-          (decl_info, qual_type.Clang_ast_t.qt_type_ptr, var_decl_info, shoud_be_mangled) in
+          (decl_info, qual_type, var_decl_info, shoud_be_mangled) in
       General_utils.mk_sil_var trans_unit_ctx name_info var_decl_details procname outer_procname
   | ParmVarDecl (decl_info, name_info, qual_type, var_decl_info) ->
       let var_decl_details = Some
-          (decl_info, qual_type.Clang_ast_t.qt_type_ptr, var_decl_info, false) in
+          (decl_info, qual_type, var_decl_info, false) in
       General_utils.mk_sil_var trans_unit_ctx name_info var_decl_details procname outer_procname
   | _ -> assert false
 

infer/tests/codetoanalyze/cpp/checkers/Makefile

@@ -13,10 +13,13 @@ ANALYZER = checkers
 INFERPRINT_OPTIONS = --issues-txt
 
 FILES = \
+  siof/const.cpp \
+  siof/const_use.cpp \
   siof/pod_across_translation_units-1.cpp \
   siof/pod_across_translation_units-2.cpp \
   siof/pod_same_translation_unit.cpp \
   siof/siof_across_translation_units-1.cpp \
+  siof/siof_across_translation_units-2.cpp \
 
 compile:
 	clang $(OPTIONS) $(FILES)

infer/tests/codetoanalyze/cpp/checkers/issues.exp

@@ -1,2 +1,3 @@
+siof/const_use.cpp:17: ERROR: STATIC_INITIALIZATION_ORDER_FIASCO This global variable initializer accesses the following globals in another translation unit: u
 siof/pod_across_translation_units-1.cpp:12: ERROR: STATIC_INITIALIZATION_ORDER_FIASCO This global variable initializer accesses the following globals in another translation unit: y from file siof/pod_across_translation_units-2.cpp
 siof/siof_across_translation_units-1.cpp:21: ERROR: STATIC_INITIALIZATION_ORDER_FIASCO This global variable initializer accesses the following globals in another translation unit: global_object

infer/tests/codetoanalyze/cpp/checkers/siof/const.cpp

@@ -0,0 +1,15 @@
+/*
+ * Copyright (c) 2016 - 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.
+ */
+int mult(int a, int b);
+
+const int const_y = 32; // harmless global
+const int const_x = 52 * const_y; // harmless
+int constexpr z =
+    const_x / const_y + 1; // user guarantees it is harmless with constexpr
+int u = mult(32, 52); // potentially in need of initialization

infer/tests/codetoanalyze/cpp/checkers/siof/const_use.cpp

@@ -0,0 +1,17 @@
+/*
+ * Copyright (c) 2016 - 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.
+ */
+extern const int const_x;
+extern const int const_y;
+extern int z;
+extern int u;
+
+int use_x = const_x + 1;
+int use_y = const_y + 1;
+int use_z = z + 1;
+int use_u = u + 1;

infer/tests/codetoanalyze/cpp/checkers/siof/pod_across_translation_units-2.cpp

@@ -7,6 +7,8 @@
  * of patent rights can be found in the PATENTS file in the same directory.
  */
 
-static int y = 42;
+int goo();
+
+static int y = goo();
 
 int foo() { return y; }

infer/tests/codetoanalyze/cpp/checkers/siof/siof_across_translation_units-2.cpp

@@ -0,0 +1,19 @@
+/*
+ * Copyright (c) 2016 - 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.
+ */
+
+// This file exists only so that the SIOF checkers sees global_object
+// being initialized via a method call. The SIOF checker could be
+// improved to know that all non-POD types require initialization in
+// C++.
+
+struct SomeObject {
+  void some_method();
+};
+
+SomeObject global_object;

infer/tests/codetoanalyze/cpp/shared/namespace/namespace.cpp.dot

@@ -51,10 +51,10 @@ digraph iCFG {
 	
 
 	 18 -> 17 ;
-17 [label="17: Exit __infer_globals_initializer_rect \n  " color=yellow style=filled]
+17 [label="17: Exit __infer_globals_initializer_bar::rect \n  " color=yellow style=filled]
 	
 
-16 [label="16: Start __infer_globals_initializer_rect\nFormals: \nLocals:  \n   DECLARE_LOCALS(&return); [line 32]\n " color=yellow style=filled]
+16 [label="16: Start __infer_globals_initializer_bar::rect\nFormals: \nLocals:  \n   DECLARE_LOCALS(&return); [line 32]\n " color=yellow style=filled]
 	
 
 	 16 -> 18 ;
@@ -80,10 +80,10 @@ digraph iCFG {
 	
 
 	 10 -> 9 ;
-9 [label="9: Exit __infer_globals_initializer_pi \n  " color=yellow style=filled]
+9 [label="9: Exit __infer_globals_initializer_bar::pi \n  " color=yellow style=filled]
 	
 
-8 [label="8: Start __infer_globals_initializer_pi\nFormals: \nLocals:  \n   DECLARE_LOCALS(&return); [line 29]\n " color=yellow style=filled]
+8 [label="8: Start __infer_globals_initializer_bar::pi\nFormals: \nLocals:  \n   DECLARE_LOCALS(&return); [line 29]\n " color=yellow style=filled]
 	
 
 	 8 -> 10 ;

infer/tests/codetoanalyze/cpp/shared/types/typeid_expr.cpp.dot

@@ -474,10 +474,10 @@ digraph iCFG {
 	
 
 	 9 -> 8 ;
-8 [label="8: Exit __infer_globals_initializer_value \n  " color=yellow style=filled]
+8 [label="8: Exit __infer_globals_initializer_std::__1::__numeric_type<void>::value \n  " color=yellow style=filled]
 	
 
-7 [label="7: Start __infer_globals_initializer_value\nFormals: \nLocals:  \n   DECLARE_LOCALS(&return); [line 1697]\n " color=yellow style=filled]
+7 [label="7: Start __infer_globals_initializer_std::__1::__numeric_type<void>::value\nFormals: \nLocals:  \n   DECLARE_LOCALS(&return); [line 1697]\n " color=yellow style=filled]
 	
 
 	 7 -> 9 ;