Skip to content

Commit

Permalink
[pulse] do not add empty edges/attributes to the memory
Browse files Browse the repository at this point in the history
Summary:
This matters for joining states, which can otherwise introduce empty
edges or attributes, which is inefficient.

The extra filtering when creating summaries is just for safety.

Reviewed By: ngorogiannis

Differential Revision:
D67455984

Privacy Context Container: L1208441

fbshipit-source-id: 3cc8e2b117382d0c1dd6950469287999b0bc96c8
  • Loading branch information
jvillard authored and facebook-github-bot committed Dec 19, 2024
1 parent 6ce0768 commit 836855a
Show file tree
Hide file tree
Showing 3 changed files with 23 additions and 9 deletions.
16 changes: 13 additions & 3 deletions infer/src/pulse/PulseAbductiveDomain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1872,15 +1872,25 @@ let get_all_addrs_marked_as_always_reachable {post} =
let filter_pre_addr ~f (foot : PreDomain.t) =
let heap' = BaseMemory.filter (fun address _ -> f address) (foot :> BaseDomain.t).heap in
let heap' =
BaseMemory.filter
(fun address edges -> (not (RawMemory.Edges.is_empty edges)) && f address)
(foot :> BaseDomain.t).heap
in
let attrs' =
BaseAddressAttributes.filter (fun address _ -> f address) (foot :> BaseDomain.t).attrs
BaseAddressAttributes.filter
(fun address attrs -> (not (Attributes.is_empty attrs)) && f address)
(foot :> BaseDomain.t).attrs
in
PreDomain.update ~heap:heap' ~attrs:attrs' foot
let filter_post_addr_with_discarded_addrs ~heap_only ~f (foot : PostDomain.t) =
let heap' = BaseMemory.filter (fun address _ -> f address) (foot :> BaseDomain.t).heap in
let heap' =
BaseMemory.filter
(fun address edges -> (not (RawMemory.Edges.is_empty edges)) && f address)
(foot :> BaseDomain.t).heap
in
let attrs', discarded_addresses =
if heap_only then ((foot :> BaseDomain.t).attrs, [])
else BaseAddressAttributes.filter_with_discarded_addrs f (foot :> BaseDomain.t).attrs
Expand Down
14 changes: 8 additions & 6 deletions infer/src/pulse/PulseBaseAddressAttributes.ml
Original file line number Diff line number Diff line change
Expand Up @@ -35,12 +35,14 @@ let add_one addr attribute attrs =


let add addr attributes attrs =
match Graph.find_opt addr attrs with
| None ->
Graph.add addr attributes attrs
| Some old_attrs ->
let new_attrs = Attributes.union_prefer_left old_attrs attributes in
Graph.add addr new_attrs attrs
if Attributes.is_empty attributes then Graph.remove addr attrs
else
match Graph.find_opt addr attrs with
| None ->
Graph.add addr attributes attrs
| Some old_attrs ->
let new_attrs = Attributes.union_prefer_left old_attrs attributes in
Graph.add addr new_attrs attrs


let fold = Graph.fold
Expand Down
2 changes: 2 additions & 0 deletions infer/src/pulse/PulseBaseMemory.ml
Original file line number Diff line number Diff line change
Expand Up @@ -155,6 +155,8 @@ let compare = Graph.compare Edges.compare

let equal = Graph.equal Edges.equal

let add v edges heap = if Edges.is_empty edges then Graph.remove v heap else Graph.add v edges heap

module type S = sig
type key

Expand Down

0 comments on commit 836855a

Please sign in to comment.