Skip to content

Commit

Permalink
[pulse][minor] add [Pre|Post] selector to AddressAttributes.find_opt
Browse files Browse the repository at this point in the history
Summary: Needed soon.

Reviewed By: dulmarod

Differential Revision: D66581408

fbshipit-source-id: 2acc9634a8d99e1a908620a2b5ea0d0844ad1563
  • Loading branch information
jvillard authored and facebook-github-bot committed Nov 29, 2024
1 parent a4b6cf2 commit 6f84e31
Show file tree
Hide file tree
Showing 3 changed files with 15 additions and 7 deletions.
16 changes: 12 additions & 4 deletions infer/src/pulse/PulseAbductiveDomain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -411,8 +411,14 @@ module Internal = struct
map_post_attrs astate ~f:(fun attrs -> BaseAddressAttributes.initialize address attrs)


let find_opt address astate =
BaseAddressAttributes.find_opt address (astate.post :> base_domain).attrs
let find_opt pre_or_post address astate =
BaseAddressAttributes.find_opt address
( match pre_or_post with
| `Pre ->
(astate.pre :> base_domain)
| `Post ->
(astate.post :> base_domain) )
.attrs


let check_initialized path access_trace addr astate =
Expand Down Expand Up @@ -1830,7 +1836,7 @@ let check_memory_leaks ~live_addresses ~unreachable_addresses astate =
in
List.fold_result unreachable_addresses ~init:() ~f:(fun () addr ->
let addr = CanonValue.canon' astate addr in
match SafeAttributes.find_opt addr astate with
match SafeAttributes.find_opt `Post addr astate with
| Some unreachable_attrs ->
check_memory_leak addr unreachable_attrs
| None ->
Expand Down Expand Up @@ -2417,7 +2423,9 @@ module AddressAttributes = struct
let add_all v attrs astate = SafeAttributes.add_all (CanonValue.canon' astate v) attrs astate
let find_opt v astate = SafeAttributes.find_opt (CanonValue.canon' astate v) astate
let find_opt pre_or_post v astate =
SafeAttributes.find_opt pre_or_post (CanonValue.canon' astate v) astate
let check_valid path ?must_be_valid_reason trace v astate =
SafeAttributes.check_valid path ?must_be_valid_reason trace (CanonValue.canon' astate v) astate
Expand Down
2 changes: 1 addition & 1 deletion infer/src/pulse/PulseAbductiveDomain.mli
Original file line number Diff line number Diff line change
Expand Up @@ -189,7 +189,7 @@ module AddressAttributes : sig
val add_all : AbstractValue.t -> Attributes.t -> t -> t
(** [add_one] on each attribute in the set *)

val find_opt : AbstractValue.t -> t -> Attributes.t option
val find_opt : [`Pre | `Post] -> AbstractValue.t -> t -> Attributes.t option

val check_valid :
PathContext.t
Expand Down
4 changes: 2 additions & 2 deletions infer/src/pulse/PulseOperations.ml
Original file line number Diff line number Diff line change
Expand Up @@ -707,7 +707,7 @@ let rec deep_copy ?depth_max ({PathContext.timestamp} as path) location addr_his
in
let astate = PulseArithmetic.copy_type_constraints (fst addr_hist_src) (fst copy) astate in
let astate =
AddressAttributes.find_opt (fst addr_hist_src) astate
AddressAttributes.find_opt `Post (fst addr_hist_src) astate
|> Option.value_map ~default:astate ~f:(fun src_attrs ->
AddressAttributes.add_all (fst copy) src_attrs astate )
in
Expand All @@ -725,7 +725,7 @@ let check_address_escape escape_location proc_desc address history astate =
astate
in
let check_address_of_cpp_temporary () =
AddressAttributes.find_opt address astate
AddressAttributes.find_opt `Post address astate
|> Option.value_map ~default:(Result.Ok ()) ~f:(fun attrs ->
IContainer.iter_result ~fold:Attributes.fold attrs ~f:(fun attr ->
match attr with
Expand Down

0 comments on commit 6f84e31

Please sign in to comment.