[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

@@ -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

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

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 sink_of_global global pname loc =
-
+        let site = CallSite.make pname loc in
-  let add_params_globals astate tenv pdesc params =
+        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, _, _)
+    | Load (_, exp, _, loc)
-    | Store (_, _, exp, _)
+    | Store (_, _, exp, loc)
-    | Prune (exp, _, _, _) ->
+    | Prune (exp, loc, _, _) ->
-        Domain.join astate (get_globals tenv pdesc exp)
+        Domain.join astate (get_globals tenv astate pdesc loc exp)
-    | Call (_, Const (Cfun callee_pname), params, _, _) ->
+    | 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, _, _) ->
+    | Call (_, _, params, loc, _) ->
-        add_params_globals astate tenv pdesc params
+        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
+      let foreign_global_sinks =
-      if not (SiofDomain.PvarSetDomain.is_empty foreign_globals) then
+        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 ->
       ()

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)

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)

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

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

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