From 3ba91fd5962b7c5699e9fc598b7ef70a25fc5a70 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Thu, 12 Mar 2020 05:27:50 -0700 Subject: [PATCH] [pulse] refactor of PrePost.t vs AbductiveDomain.t Summary: Be a bit more careful about the difference between PrePost.t and AbductiveDomain.t. It's needed in another diff where the types will be different. Reviewed By: ezgicicek Differential Revision: D20393927 fbshipit-source-id: beaf80c90 --- infer/src/checkers/impurity.ml | 6 +++--- infer/src/pulse/PulseAbductiveDomain.ml | 17 +++++++++++----- infer/src/pulse/PulseAbductiveDomain.mli | 26 +++++++++++++++--------- infer/src/pulse/PulseSummary.ml | 3 ++- 4 files changed, 33 insertions(+), 19 deletions(-) diff --git a/infer/src/checkers/impurity.ml b/infer/src/checkers/impurity.ml index e148405af..8842d714e 100644 --- a/infer/src/checkers/impurity.ml +++ b/infer/src/checkers/impurity.ml @@ -139,8 +139,8 @@ let is_modeled_pure tenv pname = (** Given Pulse summary, extract impurity info, i.e. parameters and global variables that are modified by the function and skipped functions. *) let extract_impurity tenv pdesc pre_post : ImpurityDomain.t = - let pre_heap = (AbductiveDomain.extract_pre pre_post).BaseDomain.heap in - let post = AbductiveDomain.extract_post pre_post in + let pre_heap = (AbductiveDomain.PrePost.get_pre pre_post).BaseDomain.heap in + let post = AbductiveDomain.PrePost.get_post pre_post in let post_stack = post.BaseDomain.stack in let pname = Procdesc.get_proc_name pdesc in let modified_params = @@ -148,7 +148,7 @@ let extract_impurity tenv pdesc pre_post : ImpurityDomain.t = in let modified_globals = get_modified_globals pre_heap post post_stack in let skipped_calls = - AbductiveDomain.extract_skipped_calls pre_post + AbductiveDomain.PrePost.get_skipped_calls pre_post |> PulseAbductiveDomain.SkippedCalls.filter (fun proc_name _ -> Purity.should_report proc_name && not (is_modeled_pure tenv proc_name) ) in diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 6c90e7659..dd8eef69b 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -96,6 +96,12 @@ type t = ; pre: InvertedDomain.t (** inferred pre at the current program point *) ; skipped_calls: SkippedCalls.t (** set of skipped calls *) } +let get_pre {pre} = (pre :> BaseDomain.t) + +let get_post {post} = (post :> BaseDomain.t) + +let get_skipped_calls {skipped_calls} = skipped_calls + let pp f {post; pre} = F.fprintf f "@[%a@;PRE=[%a]@]" Domain.pp post InvertedDomain.pp pre let leq ~lhs ~rhs = @@ -414,7 +420,7 @@ module PrePost = struct (** stuff we carry around when computing the result of applying one pre/post pair *) type call_state = - { astate: t (** caller's abstract state computed so far *) + { astate: domain_t (** caller's abstract state computed so far *) ; subst: (AbstractValue.t * ValueHistory.t) AddressMap.t (** translation from callee addresses to caller addresses and their caller histories *) ; rev_subst: AbstractValue.t AddressMap.t @@ -1077,10 +1083,11 @@ module PrePost = struct Ok None | Error _ as error -> error ) -end -let extract_pre {pre} = (pre :> BaseDomain.t) -let extract_post {post} = (post :> BaseDomain.t) + let get_pre {pre} = (pre :> BaseDomain.t) + + let get_post {post} = (post :> BaseDomain.t) -let extract_skipped_calls {skipped_calls} = skipped_calls + let get_skipped_calls {skipped_calls} = skipped_calls +end diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index 037261f60..9f254ebf1 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -103,6 +103,18 @@ end module SkippedCalls : AbstractDomain.MapS with type key = Procname.t and type value = SkippedTrace.t +val discard_unreachable : t -> t +(** garbage collect unreachable addresses in the state to make it smaller, just for convenience and + keep its size down *) + +val add_skipped_calls : Procname.t -> PulseTrace.t -> t -> t + +val get_pre : t -> BaseDomain.t + +val get_post : t -> BaseDomain.t + +val get_skipped_calls : t -> SkippedCalls.t + module PrePost : sig type domain_t = t @@ -122,16 +134,10 @@ module PrePost : sig -> ((domain_t * (AbstractValue.t * ValueHistory.t) option) option, Diagnostic.t) result (** return the abstract state after the call along with an optional return value, or [None] if the precondition could not be satisfied (e.g. some aliasing constraints were not satisfied) *) -end - -val discard_unreachable : t -> t -(** garbage collect unreachable addresses in the state to make it smaller, just for convenience and - keep its size down *) - -val add_skipped_calls : Procname.t -> PulseTrace.t -> t -> t -val extract_pre : PrePost.t -> BaseDomain.t + val get_pre : t -> BaseDomain.t -val extract_post : PrePost.t -> BaseDomain.t + val get_post : t -> BaseDomain.t -val extract_skipped_calls : PrePost.t -> SkippedCalls.t + val get_skipped_calls : t -> SkippedCalls.t +end diff --git a/infer/src/pulse/PulseSummary.ml b/infer/src/pulse/PulseSummary.ml index b8c57ff29..f1589bd1c 100644 --- a/infer/src/pulse/PulseSummary.ml +++ b/infer/src/pulse/PulseSummary.ml @@ -6,8 +6,9 @@ *) open! IStd module F = Format +open PulseDomainInterface -type t = PulseAbductiveDomain.PrePost.t list +type t = AbductiveDomain.PrePost.t list let of_posts pdesc posts = List.map posts ~f:(PulseAbductiveDomain.PrePost.of_post pdesc)