[siof] check origin of globals and complain if potential siof

Summary:
Checker for the Static Initialization Order Fiasco pattern:
https://isocpp.org/wiki/faq/ctors#static-init-order

1. Collect all globals (transitively) accessed in any given procedure.
2. Once the interprocedural analysis has finished, look at globals accessed in
   initializers that do not belong to the current translation unit.

Reviewed By: sblackshear

Differential Revision: D3780266

fbshipit-source-id: 1d07161

infer/lib/python/infer.py

@@ -124,14 +124,6 @@ def create_argparser(parents=[]):
     return parser
 
 
-def validate_args(mode, args):
-    if mode is not None and mode.LANG == ['clang'] and \
-       args.analyzer == config.ANALYZER_CHECKERS:
-        utils.stderr('error: checkers are only enabled for Java.')
-        if not args.debug:
-            exit(1)
-
-
 def main():
     toplevel_envvar_value = os.environ.get(TOP_LEVEL_ENVVAR, None)
     is_toplevel_instance = False
@@ -158,8 +150,6 @@ def main():
 
     args = global_argparser.parse_args(to_parse)
 
-    validate_args(imported_module, args)
-
     remove_infer_out = (imported_module is not None and
                         not args.reactive and
                         capture_module_name != 'analyze' and

infer/src/IR/ProcAttributes.re

@@ -39,6 +39,7 @@ type t = {
   is_synthetic_method: bool, /** the procedure is a synthetic method */
   language: Config.language, /** language of the procedure */
   loc: Location.t, /** location of this procedure in the source code */
+  translation_unit: option DB.source_file, /** translation unit to which the procedure belongs */
   mutable locals: list (Mangled.t, Typ.t), /** name and type of local variables */
   method_annotation: Annot.Method.t, /** annotations for java methods */
   objc_accessor: option objc_accessor_type, /** type of ObjC accessor, if any */
@@ -67,6 +68,7 @@ let default proc_name language => {
   is_synthetic_method: false,
   language,
   loc: Location.dummy,
+  translation_unit: None,
   locals: [],
   method_annotation: Annot.Method.empty,
   objc_accessor: None,

infer/src/IR/ProcAttributes.rei

@@ -33,6 +33,7 @@ type t = {
   is_synthetic_method: bool, /** the procedure is a synthetic method */
   language: Config.language, /** language of the procedure */
   loc: Location.t, /** location of this procedure in the source code */
+  translation_unit: option DB.source_file, /** translation unit to which the procedure belongs */
   mutable locals: list (Mangled.t, Typ.t), /** name and type of local variables */
   method_annotation: Annot.Method.t, /** annotations for java methods */
   objc_accessor: option objc_accessor_type, /** type of ObjC accessor, if any */

infer/src/IR/Procname.re

@@ -493,6 +493,8 @@ let is_infer_undefined pn =>
     false
   };
 
+let is_globals_initializer (name, _) => string_is_prefix Config.clang_initializer_prefix name;
+
 
 /** to_string for C_function type */
 let to_readable_string (c1, c2) verbose => {

infer/src/IR/Procname.rei

@@ -236,6 +236,11 @@ let is_class_initializer: t => bool;
 let is_infer_undefined: t => bool;
 
 
+/** Is this procedure one inserted by Infer to initialize the global variables of this translation
+    unit? */
+let is_globals_initializer: c => bool;
+
+
 /** Pretty print a proc name. */
 let pp: Format.formatter => t => unit;
 

infer/src/IR/Pvar.re

@@ -340,3 +340,15 @@ let mk_abduced_ref_param (proc_name: Procname.t) (pv: t) (loc: Location.t) :t =>
   let name = Mangled.from_string ("$REF_PARAM_" ^ Procname.to_unique_id proc_name);
   {pv_name: name, pv_kind: Abduced_ref_param proc_name pv loc}
 };
+
+let get_source_file pvar =>
+  switch pvar.pv_kind {
+  | Global_var f => Some f
+  | _ => None
+  };
+
+let module Set = PrettyPrintable.MakePPSet {
+  type nonrec t = t;
+  let compare = compare;
+  let pp_element = pp pe_text;
+};

infer/src/IR/Pvar.rei

@@ -133,3 +133,7 @@ let to_seed: t => t;
 
 /** Convert a pvar to string. */
 let to_string: t => string;
+
+let get_source_file: t => option DB.source_file;
+
+let module Set: PrettyPrintable.PPSet with type elt = t;

infer/src/backend/specs.ml

@@ -324,8 +324,9 @@ type payload =
     typestate : unit TypeState.t option; (** final typestate *)
     calls: call_summary option;
     crashcontext_frame: Stacktree_j.stacktree option;
-    quandary : QuandarySummary.t option;
     (** Proc location and blame_range info for crashcontext analysis *)
+    quandary : QuandarySummary.t option;
+    globals_read: Pvar.Set.t option;
   }
 
 type summary =
@@ -760,6 +761,7 @@ let empty_payload =
     calls = None;
     crashcontext_frame = None;
     quandary = None;
+    globals_read = None;
   }
 
 (** [init_summary (depend_list, nodes,

infer/src/backend/specs.mli

@@ -130,6 +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;
   }
 
 (** Procedure summary *)

infer/src/checkers/addressTaken.ml

@@ -9,13 +9,7 @@
 
 open! Utils
 
-module PvarSet = PrettyPrintable.MakePPSet(struct
-    type t = Pvar.t
-    let compare = Pvar.compare
-    let pp_element = (Pvar.pp pe_text)
-  end)
-
-module Domain = AbstractDomain.FiniteSet(PvarSet)
+module Domain = AbstractDomain.FiniteSet(Pvar.Set)
 
 module TransferFunctions (CFG : ProcCfg.S) = struct
   module CFG = CFG

infer/src/checkers/registerCheckers.ml

@@ -51,6 +51,7 @@ let active_procedure_checkers () =
         CheckDeadCode.callback_check_dead_code, false;
         Checkers.callback_print_access_to_globals, false;
         CppTaintAnalysis.checker, Config.quandary;
+        Siof.checker, checkers_enabled;
       ] in
     IList.map (fun (x, y) -> (x, y, Some Config.Clang)) l in
 

infer/src/checkers/siof.ml

@@ -0,0 +1,112 @@
+(*
+ * 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.
+ *)
+
+open! Utils
+
+module F = Format
+module L = Logging
+
+module Domain = AbstractDomain.FiniteSet(Pvar.Set)
+
+module Summary = Summary.Make (struct
+    type summary = Domain.astate
+
+    let update_payload astate payload =
+      { payload with Specs.globals_read = Some astate }
+
+    let read_from_payload payload =
+      match payload.Specs.globals_read with
+      | Some astate -> astate
+      | None -> Domain.initial
+  end)
+
+module TransferFunctions (CFG : ProcCfg.S) = struct
+  module CFG = CFG
+  module Domain = Domain
+  type extras = ProcData.no_extras
+
+  let get_globals e =
+    Exp.get_vars e |> snd |> IList.filter Pvar.is_global |> Domain.of_list
+
+  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
+    | 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
+    | Call (_, _, params, _, _) ->
+        IList.map fst params
+        |> IList.map get_globals
+        |> IList.fold_left Domain.union astate
+    | Declare_locals _ | Remove_temps _ | Abstract _ | Nullify _ ->
+        astate
+end
+
+module Analyzer =
+  AbstractInterpreter.Make
+    (ProcCfg.Backward(ProcCfg.Exceptional))
+    (Scheduler.ReversePostorder)
+    (TransferFunctions)
+
+module Interprocedural = Analyzer.Interprocedural (Summary)
+
+let report_siof pname loc bad_globals =
+  let pp_desc fmt () =
+    let pp_var f v =
+      let pp_source f v = match Pvar.get_source_file v with
+        | Some source_file when DB.source_file_equal DB.source_file_empty source_file ->
+            Format.fprintf f ""
+        | None ->
+            Format.fprintf f ""
+        | Some source_file ->
+            Format.fprintf f " from file %s" (DB.source_file_to_string source_file) in
+      Format.fprintf f "%s%a" (Pvar.get_simplified_name v) pp_source v in
+    let pp_set f s = pp_seq pp_var f (Pvar.Set.elements s) in
+    Format.fprintf fmt
+      "This global variable initializer accesses the following globals in another translation \
+       unit: %a"
+      pp_set bad_globals in
+  let description = pp_to_string pp_desc () in
+  let exn = Exceptions.Checkers
+      ("STATIC_INITIALIZATION_ORDER_FIASCO", Localise.verbatim_desc description) in
+  Reporting.log_error pname ~loc exn
+
+
+let siof_check pdesc = function
+  | Some 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
+        | 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
+        report_siof (Cfg.Procdesc.get_proc_name pdesc) attrs.ProcAttributes.loc foreign_globals;
+  | None -> ()
+
+let checker callback =
+  let pdesc = callback.Callbacks.proc_desc in
+  let post = Interprocedural.checker callback ProcData.empty_extras in
+  let pname = Cfg.Procdesc.get_proc_name pdesc in
+  match pname with
+  | Procname.C c when Procname.is_globals_initializer c ->
+      siof_check pdesc post
+  | _ -> ()

infer/src/checkers/siof.mli

@@ -0,0 +1,10 @@
+(*
+ * 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.
+ *)
+
+val checker: Callbacks.proc_callback_args -> unit

infer/src/clang/cFrontend_utils.ml

@@ -756,7 +756,13 @@ struct
             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
-          Pvar.mk_global global_mangled_name source_file
+          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
         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

infer/src/clang/cMethod_trans.ml

@@ -414,6 +414,7 @@ let create_local_procdesc trans_unit_ctx cfg tenv ms fbody captured is_objc_inst
             is_objc_instance_method = is_objc_inst_method;
             is_cpp_instance_method = is_cpp_inst_method;
             loc = loc_start;
+            translation_unit = Some trans_unit_ctx.CFrontend_config.source_file;
             method_annotation;
             ret_type;
           } in

infer/tests/codetoanalyze/cpp/checkers/Makefile

@@ -0,0 +1,26 @@
+# 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.
+
+include ../../Makefile.clang
+
+OPTIONS = -x c++ -std=c++11 -isystem$(MODELS_DIR)/cpp/include -isystem$(CLANG_INCLUDES)/c++/v1/ -c
+
+ANALYZER = checkers
+INFERPRINT_OPTIONS = --issues-txt
+
+FILES = \
+  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 \
+
+compile:
+	clang $(OPTIONS) $(FILES)
+
+analyze:
+	$(INFER_BIN) -a $(ANALYZER) --cxx --ml-buckets cpp --check-duplicate-symbols -- clang $(OPTIONS) $(FILES) >/dev/null 2>duplicates.txt
+	grep "DUPLICATE_SYMBOLS" duplicates.txt; test $$? -ne 0

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

@@ -0,0 +1,2 @@
+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/pod_across_translation_units-1.cpp

@@ -0,0 +1,14 @@
+/*
+ * 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 int foo();
+
+static int x = foo(); // BAD: report SIOF here
+static int x1 = x; // do not report here
+static int x2 = x1; // do not report here

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

@@ -0,0 +1,12 @@
+/*
+ * 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.
+ */
+
+static int y = 42;
+
+int foo() { return y; }

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

@@ -0,0 +1,23 @@
+/*
+ * 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.
+ */
+
+#include <iostream>
+
+int same_tu_foo();
+int same_tu_goo();
+
+// BAD: report SIOF here
+// This may not get the initialized value for y.
+// Infer doesn't yet report here because it only looks across translation units.
+int same_tu_x = same_tu_foo();
+int same_tu_y = same_tu_goo();
+
+int same_tu_foo() { return same_tu_y; }
+
+int same_tu_goo() { return 42; }

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

@@ -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.
+ */
+
+struct SomeObject {
+  void some_method();
+};
+
+extern SomeObject global_object;
+
+struct SomeOtherObject {
+  SomeOtherObject() { global_object.some_method(); };
+};
+
+// BAD: report SIOF here
+SomeOtherObject another_global_object;