taint domain

Reviewed By: jvillard

Differential Revision: D3723785

fbshipit-source-id: c55f0e4

infer/src/checkers/accessTree.ml

@@ -34,6 +34,7 @@ module Make (TraceDomain : AbstractDomain.S) = struct
 
   (* map from base var -> access subtree *)
   type t = node BaseMap.t
+  type astate = t
 
   (** Here's how to represent a few different kinds of trace * access path associations:
       (x, T)               := { x |-> (T, Subtree {}) }
@@ -47,6 +48,8 @@ module Make (TraceDomain : AbstractDomain.S) = struct
 
   let empty = BaseMap.empty
 
+  let initial = empty
+
   let make_node trace subtree =
     trace, Subtree subtree
 

infer/src/quandary/TaintAnalysis.ml

@@ -0,0 +1,61 @@
+(*
+ * 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
+
+(** Create a taint analysis from a trace domain *)
+module Make (TraceDomain : Trace.S) = struct
+
+  module TaintDomain = AccessTree.Make (TraceDomain)
+  module IdMapDomain = IdAccessPathMapDomain
+
+  module Domain = struct
+    type astate =
+      {
+        access_tree : TaintDomain.astate; (* mapping of access paths to trace sets *)
+        id_map : IdMapDomain.astate; (* mapping of id's to access paths for normalization *)
+      }
+
+    let initial =
+      let access_tree = TaintDomain.initial in
+      let id_map = IdMapDomain.initial in
+      { access_tree; id_map; }
+
+    let (<=) ~lhs ~rhs =
+      if lhs == rhs
+      then true
+      else
+        TaintDomain.(<=) ~lhs:lhs.access_tree ~rhs:rhs.access_tree &&
+        IdMapDomain.(<=) ~lhs:lhs.id_map ~rhs:rhs.id_map
+
+    let join astate1 astate2 =
+      if astate1 == astate2
+      then astate1
+      else
+        let access_tree = TaintDomain.join astate1.access_tree astate2.access_tree in
+        let id_map = IdMapDomain.join astate1.id_map astate2.id_map in
+        { access_tree; id_map; }
+
+    let widen ~prev ~next ~num_iters =
+      if prev == next
+      then prev
+      else
+        let access_tree =
+          TaintDomain.widen ~prev:prev.access_tree ~next:next.access_tree ~num_iters in
+        let id_map = IdMapDomain.widen ~prev:prev.id_map ~next:next.id_map ~num_iters in
+        { access_tree; id_map; }
+
+    let pp fmt { access_tree; id_map; } =
+      F.fprintf fmt "(%a, %a)" TaintDomain.pp access_tree IdMapDomain.pp id_map
+  end
+
+end

infer/src/quandary/Trace.ml

@@ -23,6 +23,8 @@ end
 module type S = sig
   include Spec
   type t
+  type astate = t
+  include AbstractDomain.S with type astate := astate
 
   (** get the sources of the trace. *)
   val sources : t -> Source.Set.t
@@ -42,6 +44,9 @@ module type S = sig
   (** add a sink to the current trace. *)
   val add_sink : Sink.t -> t -> t
 
+  (** return true if this trace has no source or sink data *)
+  val is_empty : t -> bool
+
   val compare : t -> t -> int
 
   val pp : F.formatter -> t -> unit
@@ -80,6 +85,10 @@ module Make (Spec : Spec) = struct
   let sinks t =
     t.sinks
 
+  let is_empty t =
+    (* sources empty => sinks empty and passthroughs empty *)
+    Sources.is_empty t.sources
+
   let get_reports t =
     if Sinks.is_empty t.sinks
     then []