diff --git a/infer/src/checkers/SinkTrace.ml b/infer/src/checkers/SinkTrace.ml new file mode 100644 index 000000000..bdf332d1a --- /dev/null +++ b/infer/src/checkers/SinkTrace.ml @@ -0,0 +1,25 @@ +(* + * 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 Make (Spec : TraceElem.S) = struct + include Trace.Make(struct + module Source = Source.Dummy + module Sink = struct + include Spec + let get _ _ = [] + end + + let should_report _ _ = true + end) +end diff --git a/infer/src/checkers/SinkTrace.mli b/infer/src/checkers/SinkTrace.mli new file mode 100644 index 000000000..dbf0a53f0 --- /dev/null +++ b/infer/src/checkers/SinkTrace.mli @@ -0,0 +1,13 @@ +(* + * 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 Make (Spec : TraceElem.S) : + Trace.S with module Source = Source.Dummy + and module Sink.Kind = Spec.Kind + and type Sink.t = Spec.t diff --git a/infer/src/checkers/siof.ml b/infer/src/checkers/Siof.ml similarity index 72% rename from infer/src/checkers/siof.ml rename to infer/src/checkers/Siof.ml index 28657fcf2..3665ec8f7 100644 --- a/infer/src/checkers/siof.ml +++ b/infer/src/checkers/Siof.ml @@ -38,7 +38,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct ) | None -> true - let get_globals tenv pdesc e = + let get_globals tenv astate pdesc loc e = let is_dangerous_global pv = Pvar.is_global pv && not (Pvar.is_compile_constant pv @@ -47,32 +47,44 @@ module TransferFunctions (CFG : ProcCfg.S) = struct if globals = [] then Domain.Bottom else - Domain.NonBottom (SiofDomain.PvarSetDomain.of_list globals) - - let add_params_globals astate tenv pdesc params = + let sink_of_global global pname loc = + let site = CallSite.make pname loc in + SiofTrace.Sink.make global site in + let pname = Cfg.Procdesc.get_proc_name pdesc in + let trace = match astate with + | SiofDomain.Bottom -> SiofTrace.initial + | SiofDomain.NonBottom t -> t in + let globals_trace = + IList.fold_left (fun trace_acc global -> + SiofTrace.add_sink (sink_of_global global pname loc) trace_acc) + trace + globals in + Domain.NonBottom globals_trace + + let add_params_globals astate tenv pdesc loc params = IList.map fst params - |> IList.map (fun e -> get_globals tenv pdesc e) + |> IList.map (fun e -> get_globals tenv astate pdesc loc e) |> IList.fold_left Domain.join astate let at_least_bottom = - Domain.join (Domain.NonBottom SiofDomain.PvarSetDomain.empty) + Domain.join (Domain.NonBottom SiofTrace.initial) let exec_instr astate { ProcData.pdesc; tenv } _ (instr : Sil.instr) = match instr with - | Load (_, exp, _, _) - | Store (_, _, exp, _) - | Prune (exp, _, _, _) -> - Domain.join astate (get_globals tenv pdesc exp) - | Call (_, Const (Cfun callee_pname), params, _, _) -> + | Load (_, exp, _, loc) + | Store (_, _, exp, loc) + | Prune (exp, loc, _, _) -> + Domain.join astate (get_globals tenv astate pdesc loc exp) + | Call (_, Const (Cfun callee_pname), params, loc, _) -> let callee_globals = Option.default Domain.initial @@ Summary.read_summary tenv pdesc callee_pname in - add_params_globals astate tenv pdesc params + add_params_globals astate tenv pdesc loc 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, _, _) -> - add_params_globals astate tenv pdesc params + | Call (_, _, params, loc, _) -> + add_params_globals astate tenv pdesc loc params |> (* make sure it's not Bottom: we made a function call so this needs initialization *) at_least_bottom @@ -99,7 +111,7 @@ let report_siof pname loc bad_globals = | 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 + let pp_set f s = pp_seq pp_var f s in Format.fprintf fmt "This global variable initializer accesses the following globals in another translation \ unit: %a" @@ -109,7 +121,6 @@ let report_siof pname loc bad_globals = ("STATIC_INITIALIZATION_ORDER_FIASCO", Localise.verbatim_desc description) in Reporting.log_error pname ~loc exn - let siof_check pdesc = function | Some (SiofDomain.NonBottom post) -> let attrs = Cfg.Procdesc.get_attributes pdesc in @@ -120,8 +131,16 @@ let siof_check pdesc = function | 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 = SiofDomain.PvarSetDomain.filter is_foreign post in - if not (SiofDomain.PvarSetDomain.is_empty foreign_globals) then + let foreign_global_sinks = + SiofTrace.Sinks.filter + (fun sink -> is_foreign (SiofTrace.Sink.kind sink)) + (SiofTrace.sinks post) in + if not (SiofTrace.Sinks.is_empty foreign_global_sinks) + then + let foreign_globals = + IList.map + (fun sink -> (SiofTrace.Sink.kind sink)) + (SiofTrace.Sinks.elements foreign_global_sinks) in report_siof (Cfg.Procdesc.get_proc_name pdesc) attrs.ProcAttributes.loc foreign_globals; | Some SiofDomain.Bottom | None -> () diff --git a/infer/src/checkers/siof.mli b/infer/src/checkers/Siof.mli similarity index 100% rename from infer/src/checkers/siof.mli rename to infer/src/checkers/Siof.mli diff --git a/infer/src/checkers/siofDomain.ml b/infer/src/checkers/SiofDomain.ml similarity index 90% rename from infer/src/checkers/siofDomain.ml rename to infer/src/checkers/SiofDomain.ml index 8c7a04689..cb4bea98b 100644 --- a/infer/src/checkers/siofDomain.ml +++ b/infer/src/checkers/SiofDomain.ml @@ -6,7 +6,6 @@ * 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;` @@ -18,4 +17,4 @@ module PvarSetDomain = AbstractDomain.FiniteSet(Pvar.Set) 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) +include AbstractDomain.BottomLifted(SiofTrace) diff --git a/infer/src/checkers/SiofTrace.ml b/infer/src/checkers/SiofTrace.ml new file mode 100644 index 000000000..856e718d8 --- /dev/null +++ b/infer/src/checkers/SiofTrace.ml @@ -0,0 +1,50 @@ +(* + * 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 Globals = struct + type t = Pvar.t + let compare = Pvar.compare + let pp fmt pvar = (Pvar.pp pe_text) fmt pvar +end + +include SinkTrace.Make(struct + module Kind = Globals + + type t = { + site : CallSite.t; + kind: Kind.t; + } + + let call_site { site; } = site + + let kind { kind; } = kind + + let make kind site = { kind; site; } + + let to_callee t site = { t with site; } + + let compare t1 t2 = + CallSite.compare t1.site t2.site + |> next Kind.compare t1.kind t2.kind + + let pp fmt { site; kind; } = + F.fprintf fmt "Access to %a at %a" Kind.pp kind CallSite.pp site + + module Set = PrettyPrintable.MakePPSet (struct + type nonrec t = t + let compare = compare + let pp_element = pp + end) + + end) diff --git a/infer/src/checkers/SiofTrace.mli b/infer/src/checkers/SiofTrace.mli new file mode 100644 index 000000000..de99f9750 --- /dev/null +++ b/infer/src/checkers/SiofTrace.mli @@ -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. + *) + +open! Utils + +module Globals : +sig + type t = Pvar.t + val compare : t -> t -> int + val pp : Format.formatter -> t -> unit +end + +include Trace.S with module Sink.Kind = Globals diff --git a/infer/src/checkers/Source.ml b/infer/src/checkers/Source.ml index f349264d6..b7bc2fce7 100644 --- a/infer/src/checkers/Source.ml +++ b/infer/src/checkers/Source.ml @@ -19,3 +19,36 @@ module type S = sig (** return Some (kind) if the call site is a taint source, None otherwise *) val get : CallSite.t -> t option end + +module Dummy = struct + type t = unit + + let call_site _ = CallSite.dummy + + let kind t = t + + let make kind _ = kind + + let compare = Pervasives.compare + + let pp _ () = () + + let is_footprint _ = assert false + let make_footprint _ _ = assert false + let get_footprint_access_path _ = assert false + let get _ = None + + module Kind = struct + type nonrec t = t + let compare = compare + let pp = pp + end + + module Set = PrettyPrintable.MakePPSet(struct + type nonrec t = t + let compare = compare + let pp_element = pp + end) + + let to_callee t _ = t +end diff --git a/infer/src/checkers/Source.mli b/infer/src/checkers/Source.mli index f349264d6..f9ac628a9 100644 --- a/infer/src/checkers/Source.mli +++ b/infer/src/checkers/Source.mli @@ -19,3 +19,5 @@ module type S = sig (** return Some (kind) if the call site is a taint source, None otherwise *) val get : CallSite.t -> t option end + +module Dummy : S