[siof] do not report on standard streams

Summary:
Moving away from C++ include-based models means that we cannot reliably detect
anymore whether a file includes <iostream> or not. In order not to be too
spammy, let's always assume standard streams are initialized for now when the
include models are off.

Recent versions of libstdc++ make these models redundant so there is hope that in a
bright future the analysis of std streams initialisation will work correctly without infer
having to have its own models anyway.

Reviewed By: mbouaziz

Differential Revision: D8043467

fbshipit-source-id: d118043

infer/src/IR/HilInstr.ml

@@ -43,8 +43,8 @@ type translation =
   | Unbind of Var.t list
   | Ignore
 
-(* convert an SIL instruction into an HIL instruction. the [f_resolve_id] function should map an SSA
-   temporary variable to the access path it represents. evaluating the HIL instruction should
+(** convert an SIL instruction into an HIL instruction. The [f_resolve_id] function should map an
+   SSA temporary variable to the access path it represents. Evaluating the HIL instruction should
    produce the same result as evaluating the SIL instruction and replacing the temporary variables
    using [f_resolve_id]. *)
 let of_sil ~include_array_indexes ~f_resolve_id (instr: Sil.instr) =

infer/src/IR/HilInstr.mli

@@ -34,4 +34,7 @@ type translation =
 val of_sil :
   include_array_indexes:bool -> f_resolve_id:(Var.t -> AccessExpression.t option) -> Sil.instr
   -> translation
-(** Convert an SIL instruction to an HIL instruction *)
+(** convert an SIL instruction into an HIL instruction. The [f_resolve_id] function should map an
+   SSA temporary variable to the access path it represents. Evaluating the HIL instruction should
+   produce the same result as evaluating the SIL instruction and replacing the temporary variables
+   using [f_resolve_id]. *)

infer/src/backend/Payloads.ml

@@ -19,7 +19,7 @@ type t =
   ; quandary: QuandarySummary.t option
   ; racerd: RacerDDomain.summary option
   ; resources: ResourceLeakDomain.summary option
-  ; siof: SiofDomain.astate option
+  ; siof: SiofDomain.Summary.astate option
   ; typestate: unit TypeState.t option
   ; uninit: UninitDomain.summary option
   ; cost: CostDomain.summary option
@@ -52,7 +52,9 @@ let pp pe fmt
     (pp_opt "CrashContext" Crashcontext.pp_stacktree)
     crashcontext_frame
     (pp_opt "Quandary" QuandarySummary.pp)
-    quandary (pp_opt "Siof" SiofDomain.pp) siof
+    quandary
+    (pp_opt "Siof" SiofDomain.Summary.pp)
+    siof
     (pp_opt "RacerD" RacerDDomain.pp_summary)
     racerd (pp_opt "Litho" LithoDomain.pp) litho
     (pp_opt "BufferOverrun" BufferOverrunDomain.Summary.pp)

infer/src/backend/Payloads.mli

@@ -19,7 +19,7 @@ type t =
   ; quandary: QuandarySummary.t option
   ; racerd: RacerDDomain.summary option
   ; resources: ResourceLeakDomain.summary option
-  ; siof: SiofDomain.astate option
+  ; siof: SiofDomain.Summary.astate option
   ; typestate: unit TypeState.t option
   ; uninit: UninitDomain.summary option
   ; cost: CostDomain.summary option

infer/src/base/Config.ml

@@ -962,12 +962,25 @@ and current_to_previous_script =
      we are on the current version already."
 
 
-and cxx_infer_headers =
-  CLOpt.mk_bool ~long:"cxx-infer-headers" ~default:false
-    ~in_help:InferCommand.[(Capture, manual_clang)]
-    "Include C++ header models during compilation. Infer swaps some C++ headers for its own in \
-     order to get a better model of, eg, the standard library. This can sometimes cause \
-     compilation failures."
+and cxx_infer_headers, siof_check_iostreams =
+  let siof_check_iostreams =
+    CLOpt.mk_bool ~long:"siof-check-iostreams"
+      ~in_help:InferCommand.[(Analyze, manual_siof)]
+      "Do not assume that iostreams (cout, cerr, ...) are always initialized. The default is to \
+       assume they are always initialized when $(b,--cxx-infer-headers) is false to avoid false \
+       positives due to lack of models of the proper initialization of io streams. However, if \
+       your program compiles against a recent libstdc++ then the infer models are not needed for \
+       precision and it is safe to turn this option on."
+  in
+  let cxx_infer_headers =
+    CLOpt.mk_bool_group ~long:"cxx-infer-headers" ~default:false
+      ~in_help:InferCommand.[(Capture, manual_clang)]
+      "Include C++ header models during compilation. Infer swaps some C++ headers for its own in \
+       order to get a better model of, eg, the standard library. This can sometimes cause \
+       compilation failures."
+      [siof_check_iostreams] []
+  in
+  (cxx_infer_headers, siof_check_iostreams)
 
 
 and cxx_scope_guards =
@@ -1805,8 +1818,8 @@ and reactive_capture =
 and relative_path_backtack =
   CLOpt.mk_int ~long:"backtrack-level" ~default:0 ~meta:"int"
     "Maximum level of backtracking to convert an absolute path to path relative to the common \
-     prefix between the project root and the path. For instance, with bactraking level 1, it \
-     will convert /my/source/File.java with project root /my/root into ../source/File.java"
+     prefix between the project root and the path. For instance, with bactraking level 1, it will \
+     convert /my/source/File.java with project root /my/root into ../source/File.java"
 
 
 and report =
@@ -2794,6 +2807,8 @@ and show_progress_bar = !progress_bar
 
 and siof = !siof
 
+and siof_check_iostreams = !siof_check_iostreams
+
 and siof_safe_methods = !siof_safe_methods
 
 and skip_analysis_in_path = !skip_analysis_in_path

infer/src/base/Config.mli

@@ -594,6 +594,8 @@ val show_progress_bar : bool
 
 val siof : bool
 
+val siof_check_iostreams : bool
+
 val siof_safe_methods : string list
 
 val skip_analysis_in_path : string list

infer/src/checkers/Siof.ml

@@ -40,6 +40,16 @@ let standard_streams =
   ; "std::wcout" ]
 
 
+let always_initialized =
+  (* We model "std::ios_base::Init::Init" as initializing [standard_streams], which works if either
+     infer's cxx models are enabled ([Config.cxx_infer_headers]) or if the stdlib is a recent
+     libstdc++ (which is kind enough to create an [std::ios_base::Init] object explicitely). In
+     other cases, we assume they are always initialized so as not to be noisy. The issue to remove
+     this assumption would be to detect when <iostream> is included in a file without swapping the
+     C++ includes for our own. *)
+  if Config.siof_check_iostreams then [] else standard_streams
+
+
 let models = List.map ~f:parse_siof_model [("std::ios_base::Init::Init", standard_streams)]
 
 let is_modelled =
@@ -51,7 +61,7 @@ let is_modelled =
 
 
 module Payload = SummaryPayload.Make (struct
-  type t = SiofDomain.astate
+  type t = SiofDomain.Summary.astate
 
   let update_payloads astate (payloads: Payloads.t) = {payloads with siof= Some astate}
 
@@ -75,16 +85,6 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         false
 
 
-  let get_globals pdesc e =
-    let is_dangerous_global pv =
-      Pvar.is_global pv && not (Pvar.is_static_local pv) && not (Pvar.is_pod pv)
-      && not (Pvar.is_compile_constant pv) && not (is_compile_time_constructed pdesc pv)
-    in
-    Exp.program_vars e
-    |> Sequence.fold ~init:GlobalVarSet.empty ~f:(fun gset g ->
-           if is_dangerous_global g then GlobalVarSet.add g gset else gset )
-
-
   let filter_global_accesses initialized =
     let initialized_matcher =
       Domain.VarNames.elements initialized |> QualifiedCppName.Match.of_fuzzy_qual_names
@@ -95,6 +95,21 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         |> Fn.non (QualifiedCppName.Match.match_qualifiers initialized_matcher) )
 
 
+  let is_not_always_initialized =
+    Staged.unstage (filter_global_accesses (Domain.VarNames.of_list always_initialized))
+
+
+  let get_globals pdesc e =
+    let is_dangerous_global pv =
+      Pvar.is_global pv && not (Pvar.is_static_local pv) && not (Pvar.is_pod pv)
+      && not (Pvar.is_compile_constant pv) && not (is_compile_time_constructed pdesc pv)
+      && is_not_always_initialized pv
+    in
+    Exp.program_vars e
+    |> Sequence.fold ~init:GlobalVarSet.empty ~f:(fun gset g ->
+           if is_dangerous_global g then GlobalVarSet.add g gset else gset )
+
+
   let add_globals astate loc globals =
     if GlobalVarSet.is_empty globals then astate
     else

infer/src/checkers/SiofDomain.ml

@@ -11,4 +11,5 @@ open! IStd
 open! AbstractDomain.Types
 module VarNames = AbstractDomain.FiniteSet (String)
 module BottomSiofTrace = AbstractDomain.BottomLifted (SiofTrace)
-include AbstractDomain.Pair (BottomSiofTrace) (VarNames)
+module Summary = AbstractDomain.Pair (BottomSiofTrace) (VarNames)
+include Summary

infer/src/checkers/SiofDomain.mli

@@ -11,6 +11,9 @@ open! IStd
 
 module VarNames : module type of AbstractDomain.FiniteSet (String)
 
+module Summary :
+    module type of AbstractDomain.Pair (AbstractDomain.BottomLifted (SiofTrace)) (VarNames)
+
 (* The domain for the analysis is:
 
    - On the one hand, sets of global variables if an initialization is needed at runtime, or Bottom
@@ -27,4 +30,4 @@ module VarNames : module type of AbstractDomain.FiniteSet (String)
    terminates (even before main() has started). For instance, this is the case for
    std::ios_base::Init::Init(). *)
 
-include module type of AbstractDomain.Pair (AbstractDomain.BottomLifted (SiofTrace)) (VarNames)
+include module type of Summary

infer/tests/codetoanalyze/cpp/siof/Makefile

@@ -10,7 +10,7 @@ TESTS_DIR = ../../..
 ANALYZER = checkers
 # see explanations in cpp/errors/Makefile for the custom isystem
 CLANG_OPTIONS = -x c++ -std=c++11 -nostdinc++ -isystem$(MODELS_DIR)/cpp/include -isystem$(CLANG_INCLUDES)/c++/v1/ -c
-INFER_OPTIONS = --siof-only --debug-exceptions --project-root $(TESTS_DIR)
+INFER_OPTIONS = --siof-only --cxx-infer-headers --debug-exceptions --project-root $(TESTS_DIR)
 INFERPRINT_OPTIONS = --issues-tests
 
 SOURCES = \