diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 99188ef52..5f9726278 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -531,22 +531,27 @@ let incorporate_new_eqs astate new_eqs = let canonicalize astate = let open SatUnsat.Import in let get_var_repr v = PathCondition.get_var_repr astate.path_condition v in - let canonicalize_base stack heap = + let canonicalize_base stack heap attrs = let stack' = BaseStack.canonicalize ~get_var_repr stack in (* note: this step also de-registers addresses pointing to empty edges *) let+ heap' = BaseMemory.canonicalize ~get_var_repr heap in - (stack', heap') + let attrs' = BaseAddressAttributes.canonicalize ~get_var_repr attrs in + (stack', heap', attrs') in (* need different functions for pre and post to appease the type system *) let canonicalize_pre (pre : PreDomain.t) = - let+ stack', heap' = canonicalize_base (pre :> BaseDomain.t).stack (pre :> BaseDomain.t).heap in - PreDomain.update ~stack:stack' ~heap:heap' pre + let+ stack', heap', attrs' = + canonicalize_base (pre :> BaseDomain.t).stack (pre :> BaseDomain.t).heap + (pre :> BaseDomain.t).attrs + in + PreDomain.update ~stack:stack' ~heap:heap' ~attrs:attrs' pre in let canonicalize_post (post : PostDomain.t) = - let+ stack', heap' = + let+ stack', heap', attrs' = canonicalize_base (post :> BaseDomain.t).stack (post :> BaseDomain.t).heap + (post :> BaseDomain.t).attrs in - PostDomain.update ~stack:stack' ~heap:heap' post + PostDomain.update ~stack:stack' ~heap:heap' ~attrs:attrs' post in let* pre = canonicalize_pre astate.pre in let+ post = canonicalize_post astate.post in diff --git a/infer/src/pulse/PulseBaseAddressAttributes.ml b/infer/src/pulse/PulseBaseAddressAttributes.ml index 7ef3783be..0a4dcbd1d 100644 --- a/infer/src/pulse/PulseBaseAddressAttributes.ml +++ b/infer/src/pulse/PulseBaseAddressAttributes.ml @@ -130,3 +130,17 @@ let is_end_of_collection address attrs = let is_std_vector_reserved address attrs = Graph.find_opt address attrs |> Option.value_map ~default:false ~f:Attributes.is_std_vector_reserved + + +let canonicalize ~get_var_repr attrs_map = + (* TODO: merging attributes together can produce contradictory attributes, eg [MustBeValid] + + [Invalid]. We could detect these and abort execution. This is not really restricted to merging + as it might be possible to get a contradiction by accident too so maybe here is not the best + place to detect these. *) + Graph.fold + (fun addr attrs g -> + if Attributes.is_empty attrs then g + else + let addr' = get_var_repr addr in + add addr' attrs g ) + attrs_map Graph.empty diff --git a/infer/src/pulse/PulseBaseAddressAttributes.mli b/infer/src/pulse/PulseBaseAddressAttributes.mli index 4d15d9ec2..a4e7eb58d 100644 --- a/infer/src/pulse/PulseBaseAddressAttributes.mli +++ b/infer/src/pulse/PulseBaseAddressAttributes.mli @@ -54,3 +54,7 @@ val pp : F.formatter -> t -> unit val remove_allocation_attr : AbstractValue.t -> t -> t val initialize : AbstractValue.t -> t -> t + +val canonicalize : get_var_repr:(AbstractValue.t -> AbstractValue.t) -> t -> t +(** merge the attributes of all the variables that are equal according to [get_var_repr] and remove + non-canonical variables in favor of their rerpresentative *)