functor for creating trace domain

Reviewed By: jberdine

Differential Revision: D3685043

fbshipit-source-id: b177fe3

infer/src/quandary/Source.ml

@@ -11,8 +11,12 @@ module type S = sig
   include TraceElem.S
 
   val is_footprint : t -> bool
+
+  val make_footprint : AccessPath.t -> CallSite.t -> t
+
+  val get_footprint_access_path: t -> AccessPath.t option
+
   val to_return : t -> CallSite.t -> t
-  val make_footprint : CallSite.t -> t
 
   (** ith return value * ith sink kind *)
   val get : CallSite.t -> (int * t) list

infer/src/quandary/Trace.ml

@@ -24,7 +24,7 @@ module type S = sig
   include Spec
   type t
 
-  (** get the sources of the trace. this should never be empty *)
+  (** get the sources of the trace. *)
   val sources : t -> Source.Set.t
 
   (** get the sinks of the trace *)
@@ -61,6 +61,8 @@ module Make (Spec : Spec) = struct
       passthroughs : Passthrough.Set.t; (** calls that occurred between source and sink *)
     }
 
+  type astate = t
+
   let compare t1 t2 =
     Sources.compare t1.sources t2.sources
     |> next Sinks.compare t1.sinks t2.sinks
@@ -101,4 +103,28 @@ module Make (Spec : Spec) = struct
   let add_sink sink t =
     let sinks = Sinks.add sink t.sinks in
     { t with sinks; }
+
+  let initial =
+    let sources = Sources.empty in
+    let sinks = Sinks.empty in
+    let passthroughs = Passthrough.Set.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)
+
+  let join t1 t2 =
+    if t1 == t2
+    then t1
+    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
+      { sources; sinks; passthroughs; }
+
+  let widen ~prev ~next ~num_iters:_ =
+    join prev next
 end