diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index b61f4425c..565383988 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -136,6 +136,8 @@ module Stack = struct let find_opt var astate = BaseStack.find_opt var (astate.post :> base_domain).stack let mem var astate = BaseStack.mem var (astate.post :> base_domain).stack + + let exists f astate = BaseStack.exists f (astate.post :> base_domain).stack end module Memory = struct @@ -170,8 +172,12 @@ module Memory = struct map_post_heap astate ~f:(fun heap -> BaseMemory.add_edge addr access new_addr_trace heap) + let find_edge_opt address access astate = + BaseMemory.find_edge_opt address access (astate.post :> base_domain).heap + + let eval_edge addr access astate = - match BaseMemory.find_edge_opt addr access (astate.post :> base_domain).heap with + match find_edge_opt addr access astate with | Some addr_trace' -> (astate, addr_trace') | None -> diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index 33ee62724..fb052e864 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -33,6 +33,8 @@ module Stack : sig (** return the value of the variable in the stack or create a fresh one if needed *) val mem : Var.t -> t -> bool + + val exists : (Var.t -> PulseDomain.Stack.value -> bool) -> t -> bool end (** stack operations like {!PulseDomain.Heap} but that also take care of propagating facts to the @@ -53,6 +55,8 @@ module Memory : sig val find_opt : AbstractAddress.t -> t -> PulseDomain.Memory.cell option + val find_edge_opt : AbstractAddress.t -> Access.t -> t -> PulseDomain.AddrTracePair.t option + val set_cell : AbstractAddress.t -> PulseDomain.Memory.cell -> t -> t val invalidate : diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index afe6c464a..d4580ca34 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -216,12 +216,24 @@ let invalidate_array_elements location cause addr_trace astate = let check_address_escape escape_location proc_desc address history astate = + let is_assigned_to_global address astate = + let points_to_address pointer address astate = + Memory.find_edge_opt pointer Dereference astate + |> Option.exists ~f:(fun (pointee, _) -> AbstractAddress.equal pointee address) + in + Stack.exists + (fun var (pointer, _) -> Var.is_global var && points_to_address pointer address astate) + astate + in let check_address_of_cpp_temporary () = Memory.find_opt address astate |> Option.fold_result ~init:() ~f:(fun () (_, attrs) -> IContainer.iter_result ~fold:Attributes.fold attrs ~f:(fun attr -> match attr with - | Attribute.AddressOfCppTemporary (variable, _) -> + | Attribute.AddressOfCppTemporary (variable, _) + when not (is_assigned_to_global address astate) -> + (* The returned address corresponds to a C++ temporary. It will have gone out of + scope by now except if it was bound to a global. *) Error (PulseDiagnostic.StackVariableAddressEscape {variable; location= escape_location; history}) diff --git a/infer/tests/codetoanalyze/cpp/pulse/returns.cpp b/infer/tests/codetoanalyze/cpp/pulse/returns.cpp index d8b3ec1f7..a560fbc51 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/returns.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/returns.cpp @@ -94,6 +94,11 @@ S* return_static_local_ok() { return local; } +static const S& return_static_local_ref_ok() { + static const S& s{1}; + return s; +} + S* return_static_local_inner_scope_ok(bool b) { S* local = nullptr; if (b) {