From e853b01051f7d157c23c8acd1cd90da1648a0ee9 Mon Sep 17 00:00:00 2001
From: Sam Blackshear <shb@fb.com>
Date: Thu, 18 Aug 2016 09:46:04 -0700
Subject: [PATCH] taint domain

Reviewed By: jvillard

Differential Revision: D3723785

fbshipit-source-id: c55f0e4
---
 infer/src/checkers/accessTree.ml    |  3 ++
 infer/src/quandary/TaintAnalysis.ml | 61 +++++++++++++++++++++++++++++
 infer/src/quandary/Trace.ml         |  9 +++++
 3 files changed, 73 insertions(+)
 create mode 100644 infer/src/quandary/TaintAnalysis.ml

diff --git a/infer/src/checkers/accessTree.ml b/infer/src/checkers/accessTree.ml
index 5c9136015..22cca7a47 100644
--- a/infer/src/checkers/accessTree.ml
+++ b/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
 
diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml
new file mode 100644
index 000000000..c1eb98b9d
--- /dev/null
+++ b/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
diff --git a/infer/src/quandary/Trace.ml b/infer/src/quandary/Trace.ml
index 6d9a47573..1de7627fa 100644
--- a/infer/src/quandary/Trace.ml
+++ b/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 []