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