From c2043af70d41fe2f33e94840f1c99f0f806cd867 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Tue, 16 Aug 2016 07:56:29 -0700 Subject: [PATCH] functor for creating trace domain Reviewed By: jberdine Differential Revision: D3685043 fbshipit-source-id: b177fe3 --- infer/src/quandary/Source.ml | 6 +++++- infer/src/quandary/Trace.ml | 28 +++++++++++++++++++++++++++- 2 files changed, 32 insertions(+), 2 deletions(-) diff --git a/infer/src/quandary/Source.ml b/infer/src/quandary/Source.ml index 0eb2fbf66..6f6d45df4 100644 --- a/infer/src/quandary/Source.ml +++ b/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 diff --git a/infer/src/quandary/Trace.ml b/infer/src/quandary/Trace.ml index df927cf69..6d9a47573 100644 --- a/infer/src/quandary/Trace.ml +++ b/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