From ea26d6f179dc85fa2bdd0cab56e9693a7dedc5aa Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Wed, 2 Nov 2016 11:16:15 -0700 Subject: [PATCH] [siof] convert domain to sink trace of pvar's Summary: The Quandary-style traces are too general for checkers like SIOF. This diff adds a "suffix abstraction" of the trace for analyses that just care about sinks. To show how to use it, we add it to SIOF. Note: this diff converts the domain, but isn't actually doing the fancier reporting yet. That will come in a future diff. Reviewed By: jvillard Differential Revision: D4117393 fbshipit-source-id: e473665 --- infer/src/checkers/SinkTrace.ml | 25 +++++++++ infer/src/checkers/SinkTrace.mli | 13 +++++ infer/src/checkers/{siof.ml => Siof.ml} | 55 +++++++++++++------ infer/src/checkers/{siof.mli => Siof.mli} | 0 .../checkers/{siofDomain.ml => SiofDomain.ml} | 3 +- infer/src/checkers/SiofTrace.ml | 50 +++++++++++++++++ infer/src/checkers/SiofTrace.mli | 19 +++++++ infer/src/checkers/Source.ml | 33 +++++++++++ infer/src/checkers/Source.mli | 2 + 9 files changed, 180 insertions(+), 20 deletions(-) create mode 100644 infer/src/checkers/SinkTrace.ml create mode 100644 infer/src/checkers/SinkTrace.mli rename infer/src/checkers/{siof.ml => Siof.ml} (72%) rename infer/src/checkers/{siof.mli => Siof.mli} (100%) rename infer/src/checkers/{siofDomain.ml => SiofDomain.ml} (90%) create mode 100644 infer/src/checkers/SiofTrace.ml create mode 100644 infer/src/checkers/SiofTrace.mli 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