From 4d1b300e5bd36f7bccda02d46b434fbae34de807 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Mon, 22 Jul 2019 09:18:48 -0700 Subject: [PATCH] [pulse] Remove bindings with empty edges in pre Reviewed By: jvillard Differential Revision: D16419183 fbshipit-source-id: 858958ddd --- infer/src/pulse/PulseAbductiveDomain.ml | 9 ++++++++- infer/src/pulse/PulseDomain.ml | 7 +++++++ infer/src/pulse/PulseDomain.mli | 2 ++ 3 files changed, 17 insertions(+), 1 deletion(-) diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index dff26a854..4d44c09db 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -286,7 +286,14 @@ module PrePost = struct (fun var _ -> Var.is_return var || Stack.is_abducible astate var) (astate.post :> PulseDomain.t).stack in - {astate with post= Domain.update ~stack:post_stack astate.post} + (* deregister empty edges in pre *) + let pre_heap = + BaseMemory.filter_heap + (fun _addr edges -> not (BaseMemory.Edges.is_empty edges)) + (astate.pre :> base_domain).heap + in + { pre= InvertedDomain.update astate.pre ~heap:pre_heap + ; post= Domain.update ~stack:post_stack astate.post } let of_post astate = filter_for_summary astate |> discard_unreachable diff --git a/infer/src/pulse/PulseDomain.ml b/infer/src/pulse/PulseDomain.ml index 1d2402b98..febdb7ffa 100644 --- a/infer/src/pulse/PulseDomain.ml +++ b/infer/src/pulse/PulseDomain.ml @@ -389,6 +389,8 @@ module Memory : sig val filter : (AbstractAddress.t -> bool) -> t -> t + val filter_heap : (AbstractAddress.t -> edges -> bool) -> t -> t + val find_opt : AbstractAddress.t -> t -> cell option val fold_attrs : (AbstractAddress.t -> Attributes.t -> 'acc -> 'acc) -> t -> 'acc -> 'acc @@ -540,6 +542,11 @@ end = struct if phys_equal heap (fst memory) && phys_equal attrs (snd memory) then memory else (heap, attrs) + let filter_heap f memory = + let heap = Graph.filter f (fst memory) in + if phys_equal heap (fst memory) then memory else (heap, snd memory) + + let mem_edges addr memory = Graph.mem addr (fst memory) end diff --git a/infer/src/pulse/PulseDomain.mli b/infer/src/pulse/PulseDomain.mli index 444347372..c06f07e68 100644 --- a/infer/src/pulse/PulseDomain.mli +++ b/infer/src/pulse/PulseDomain.mli @@ -143,6 +143,8 @@ module Memory : sig val filter : (AbstractAddress.t -> bool) -> t -> t + val filter_heap : (AbstractAddress.t -> edges -> bool) -> t -> t + val find_opt : AbstractAddress.t -> t -> cell option val fold_attrs : (AbstractAddress.t -> Attributes.t -> 'acc -> 'acc) -> t -> 'acc -> 'acc