From fecabb3bf33eb4e0b58f445e46fa1436a267fd3f Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Fri, 25 May 2018 03:01:20 -0700 Subject: [PATCH] [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 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 | 4 +-- infer/src/IR/HilInstr.mli | 5 ++- infer/src/backend/Payloads.ml | 6 ++-- infer/src/backend/Payloads.mli | 2 +- infer/src/base/Config.ml | 31 ++++++++++++----- infer/src/base/Config.mli | 2 ++ infer/src/checkers/Siof.ml | 37 +++++++++++++++------ infer/src/checkers/SiofDomain.ml | 3 +- infer/src/checkers/SiofDomain.mli | 5 ++- infer/tests/codetoanalyze/cpp/siof/Makefile | 2 +- 10 files changed, 69 insertions(+), 28 deletions(-) diff --git a/infer/src/IR/HilInstr.ml b/infer/src/IR/HilInstr.ml index 8caaa941d..746abc632 100644 --- a/infer/src/IR/HilInstr.ml +++ b/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) = diff --git a/infer/src/IR/HilInstr.mli b/infer/src/IR/HilInstr.mli index 3ec1fbde5..0f2b76639 100644 --- a/infer/src/IR/HilInstr.mli +++ b/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]. *) diff --git a/infer/src/backend/Payloads.ml b/infer/src/backend/Payloads.ml index a5a73a48d..8f1505775 100644 --- a/infer/src/backend/Payloads.ml +++ b/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) diff --git a/infer/src/backend/Payloads.mli b/infer/src/backend/Payloads.mli index b0c740f18..6d3382aa1 100644 --- a/infer/src/backend/Payloads.mli +++ b/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 diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 1ac1c6c03..4e2cb5e85 100644 --- a/infer/src/base/Config.ml +++ b/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 diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 65ff3b760..37ab4782d 100644 --- a/infer/src/base/Config.mli +++ b/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 diff --git a/infer/src/checkers/Siof.ml b/infer/src/checkers/Siof.ml index fbb441ab2..175453ce6 100644 --- a/infer/src/checkers/Siof.ml +++ b/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 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 diff --git a/infer/src/checkers/SiofDomain.ml b/infer/src/checkers/SiofDomain.ml index 53c75aea2..3505c97db 100644 --- a/infer/src/checkers/SiofDomain.ml +++ b/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 diff --git a/infer/src/checkers/SiofDomain.mli b/infer/src/checkers/SiofDomain.mli index 5e1e7bc8a..4dbb2eae5 100644 --- a/infer/src/checkers/SiofDomain.mli +++ b/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 diff --git a/infer/tests/codetoanalyze/cpp/siof/Makefile b/infer/tests/codetoanalyze/cpp/siof/Makefile index 2eb4139f8..ed5f5be7b 100644 --- a/infer/tests/codetoanalyze/cpp/siof/Makefile +++ b/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 = \