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 []