[quandary] adding append operation

Reviewed By: jeremydubreil

Differential Revision: D3857100

fbshipit-source-id: 030b1cb

infer/src/quandary/Trace.ml

@@ -29,14 +29,21 @@ module type S = sig
   type astate = t
   include AbstractDomain.S with type astate := astate
 
+  module Sources = Source.Set
+  module Sinks = Sink.Set
+  module Passthroughs = Passthrough.Set
+
   (** get the sources of the trace. *)
-  val sources : t -> Source.Set.t
+  val sources : t -> Sources.t
 
   (** get the sinks of the trace *)
-  val sinks : t -> Sink.Set.t
+  val sinks : t -> Sinks.t
+
+  (** get the passthroughs of the trace *)
+  val passthroughs : t -> Passthroughs.t
 
   (** get the reportable source-sink flows in this trace *)
-  val get_reports : t -> (Source.t * Sink.t * Passthrough.Set.t) list
+  val get_reports : t -> (Source.t * Sink.t * Passthroughs.t) list
 
   (** get logging-ready exceptions for the reportable source-sink flows in this trace *)
   val get_reportable_exns : t -> exn list
@@ -50,11 +57,16 @@ module type S = sig
   (** add a sink to the current trace. *)
   val add_sink : Sink.t -> t -> t
 
+  (** append the trace for given call site to the current caller trace *)
+  val append : t -> t -> CallSite.t -> t
+
   (** return true if this trace has no source or sink data *)
   val is_empty : t -> bool
 
   val compare : t -> t -> int
 
+  val equal : t -> t -> bool
+
   val pp : F.formatter -> t -> unit
 end
 
@@ -63,6 +75,7 @@ module Make (Spec : Spec) = struct
 
   module Sources = Source.Set
   module Sinks = Sink.Set
+  module Passthroughs = Passthrough.Set
 
   type t =
     {
@@ -77,13 +90,16 @@ module Make (Spec : Spec) = struct
   let compare t1 t2 =
     Sources.compare t1.sources t2.sources
     |> next Sinks.compare t1.sinks t2.sinks
-    |> next Passthrough.Set.compare t1.passthroughs t2.passthroughs
+    |> next Passthroughs.compare t1.passthroughs t2.passthroughs
+
+  let equal t1 t2 =
+    compare t1 t2 = 0
 
   let pp fmt t =
     F.fprintf
       fmt
       "%a -> %a via %a"
-      Sources.pp t.sources Sinks.pp t.sinks Passthrough.Set.pp t.passthroughs
+      Sources.pp t.sources Sinks.pp t.sinks Passthroughs.pp t.passthroughs
 
   let sources t =
     t.sources
@@ -91,6 +107,9 @@ module Make (Spec : Spec) = struct
   let sinks t =
     t.sinks
 
+  let passthroughs t =
+    t.passthroughs
+
   let is_empty t =
     (* sources empty => sinks empty and passthroughs empty *)
     Sources.is_empty t.sources
@@ -112,7 +131,7 @@ module Make (Spec : Spec) = struct
 
   let of_source source =
     let sources = Sources.singleton source in
-    let passthroughs = Passthrough.Set.empty in
+    let passthroughs = Passthroughs.empty in
     let sinks = Sinks.empty in
     { sources; passthroughs; sinks; }
 
@@ -124,17 +143,34 @@ module Make (Spec : Spec) = struct
     let sinks = Sinks.add sink t.sinks in
     { t with sinks; }
 
+  (** compute caller_trace + callee_trace *)
+  let append caller_trace callee_trace callee_site =
+    if is_empty callee_trace
+    then caller_trace
+    else
+      let sources =
+        Sources.filter (fun source -> not (Source.is_footprint source)) callee_trace.sources
+        |> Sources.union caller_trace.sources in
+      let sinks = Sinks.union caller_trace.sinks callee_trace.sinks in
+      let passthroughs =
+        let joined_passthroughs =
+          Passthroughs.union caller_trace.passthroughs callee_trace.passthroughs in
+        if Sinks.is_empty callee_trace.sinks
+        then Passthroughs.add (Passthrough.make callee_site) joined_passthroughs
+        else joined_passthroughs in
+      { sources; sinks; passthroughs; }
+
   let initial =
     let sources = Sources.empty in
     let sinks = Sinks.empty in
-    let passthroughs = Passthrough.Set.empty in
+    let passthroughs = Passthroughs.empty in
     { sources; sinks; passthroughs; }
 
   let (<=) ~lhs ~rhs =
     lhs == rhs ||
     (Sources.subset lhs.sources rhs.sources &&
      Sinks.subset lhs.sinks rhs.sinks &&
-     Passthrough.Set.subset lhs.passthroughs rhs.passthroughs)
+     Passthroughs.subset lhs.passthroughs rhs.passthroughs)
 
   let join t1 t2 =
     if t1 == t2
@@ -142,7 +178,7 @@ module Make (Spec : Spec) = struct
     else
       let sources = Sources.union t1.sources t2.sources in
       let sinks = Sinks.union t1.sinks t2.sinks in
-      let passthroughs = Passthrough.Set.union t1.passthroughs t2.passthroughs in
+      let passthroughs = Passthroughs.union t1.passthroughs t2.passthroughs in
       { sources; sinks; passthroughs; }
 
   let widen ~prev ~next ~num_iters:_ =

infer/src/quandary/Trace.mli

@@ -0,0 +1,73 @@
+(*
+ * 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 type Spec = sig
+  module Source : Source.S
+  module Sink : Sink.S
+
+  (** should a flow originating at source and entering sink be reported? *)
+  val should_report : Source.t -> Sink.t -> bool
+
+  (** get a loggable exception reporting a flow from source -> sink *)
+  val get_reportable_exn : Source.t -> Sink.t -> Passthrough.Set.t -> exn
+end
+
+module type S = sig
+  include Spec
+  type t
+  type astate = t
+  include AbstractDomain.S with type astate := astate
+
+  module Sources = Source.Set
+  module Sinks = Sink.Set
+  module Passthroughs = Passthrough.Set
+
+  (** get the sources of the trace. *)
+  val sources : t -> Sources.t
+
+  (** get the sinks of the trace *)
+  val sinks : t -> Sinks.t
+
+  (** get the passthroughs of the trace *)
+  val passthroughs : t -> Passthroughs.t
+
+  (** get the reportable source-sink flows in this trace *)
+  val get_reports : t -> (Source.t * Sink.t * Passthroughs.t) list
+
+  (** get logging-ready exceptions for the reportable source-sink flows in this trace *)
+  val get_reportable_exns : t -> exn list
+
+  (** create a trace from a source *)
+  val of_source : Source.t -> t
+
+  (** ad a source to the current trace *)
+  val add_source : Source.t -> t -> t
+
+  (** add a sink to the current trace. *)
+  val add_sink : Sink.t -> t -> t
+
+  (** append the trace for given call site to the current caller trace *)
+  val append : t -> t -> CallSite.t -> t
+
+  (** return true if this trace has no source or sink data *)
+  val is_empty : t -> bool
+
+  val compare : t -> t -> int
+
+  val equal : t -> t -> bool
+
+  val pp : F.formatter -> t -> unit
+end
+
+module Make (Spec : Spec) : S with module Source = Spec.Source and module Sink = Spec.Sink

infer/src/unit/TraceTests.ml

@@ -16,6 +16,7 @@ module MockTraceElem = struct
   type kind =
     | Kind1
     | Kind2
+    | Footprint
 
   type t = kind
 
@@ -31,6 +32,9 @@ module MockTraceElem = struct
     | Kind1, _ -> (-1)
     | _, Kind1 -> 1
     | Kind2, Kind2 -> 0
+    | Kind2, _ -> (-1)
+    | _, Kind2 -> 1
+    | Footprint, Footprint -> 0
 
   let equal t1 t2 =
     compare t1 t2 = 0
@@ -38,6 +42,7 @@ module MockTraceElem = struct
   let pp_kind fmt = function
     | Kind1 -> F.fprintf fmt "Kind1"
     | Kind2 -> F.fprintf fmt "Kind2"
+    | Footprint -> F.fprintf fmt "Footprint"
 
   let pp = pp_kind
 
@@ -53,11 +58,14 @@ end
 module MockSource = struct
   include MockTraceElem
 
-  let make : kind -> CallSite.t -> t = MockTraceElem.make
+  let make = MockTraceElem.make
+
+  let is_footprint kind =
+    kind = Footprint
+
+  let make_footprint _ _ = Footprint
 
   let get _ = assert false
-  let is_footprint _ = assert false
-  let make_footprint _ = assert false
   let get_footprint_access_path _ = assert false
   let to_return _ _ = assert false
 end
@@ -81,13 +89,14 @@ module MockTrace = Trace.Make(struct
   end)
 
 let tests =
+  let source1 = MockSource.make MockTraceElem.Kind1 CallSite.dummy in
+  let source2 = MockSource.make MockTraceElem.Kind2 CallSite.dummy in
+  let sink1 = MockSink.make MockTraceElem.Kind1 CallSite.dummy in
+  let sink2 = MockSink.make MockTraceElem.Kind2 CallSite.dummy in
+
   let open OUnit2 in
   let get_reports =
     let get_reports_ _ =
-      let source1 = MockSource.make MockTraceElem.Kind1 CallSite.dummy in
-      let source2 = MockSource.make MockTraceElem.Kind2 CallSite.dummy in
-      let sink1 = MockSink.make MockTraceElem.Kind1 CallSite.dummy in
-      let sink2 = MockSink.make MockTraceElem.Kind2 CallSite.dummy in
       let trace =
         MockTrace.of_source source1
         |> MockTrace.add_source source2
@@ -108,4 +117,28 @@ let tests =
            reports) in
     "get_reports">::get_reports_ in
 
-  "trace_domain_suite">:::[get_reports]
+  let append =
+    let append_ _ =
+      let call_site = CallSite.dummy in
+      let footprint_source = MockSource.make_footprint MockTraceElem.Kind1 call_site in
+      let source_trace =
+        MockTrace.of_source source1 in
+      let footprint_trace =
+        MockTrace.of_source footprint_source
+        |> MockTrace.add_sink sink1 in
+
+      let expected_trace =
+        MockTrace.of_source source1
+        |> MockTrace.add_sink sink1 in
+      assert_bool
+        "Appended trace should contain source and sink"
+        (MockTrace.equal (MockTrace.append source_trace footprint_trace call_site) expected_trace);
+
+      let appended_trace = MockTrace.append MockTrace.initial source_trace call_site in
+      assert_bool
+        "Appending a trace without a sink should add a passthrough"
+        (MockTrace.Passthroughs.mem
+           (Passthrough.make call_site) (MockTrace.passthroughs appended_trace)) in
+    "append">::append_ in
+
+  "trace_domain_suite">:::[get_reports; append]