From 6f84e31f7a3a4686dbde4a1450ba245001873f87 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Fri, 29 Nov 2024 09:16:55 -0800 Subject: [PATCH] [pulse][minor] add [`Pre|`Post] selector to AddressAttributes.find_opt Summary: Needed soon. Reviewed By: dulmarod Differential Revision: D66581408 fbshipit-source-id: 2acc9634a8d99e1a908620a2b5ea0d0844ad1563 --- infer/src/pulse/PulseAbductiveDomain.ml | 16 ++++++++++++---- infer/src/pulse/PulseAbductiveDomain.mli | 2 +- infer/src/pulse/PulseOperations.ml | 4 ++-- 3 files changed, 15 insertions(+), 7 deletions(-) diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 955e4288ec..08e2ba8eb4 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -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 = @@ -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 -> @@ -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 diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index eca60cc73c..5b2f1a1509 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -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 diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 1d26d880fc..3980ef500b 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -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 @@ -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