From 09ab685c7e6e07b32ac7b082575a1df68a349a5f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Thu, 25 Jul 2019 03:09:49 -0700 Subject: [PATCH] [pulse] Handle stack refs escaping their scope via pointer Summary: Pulse didn't treat local variables going out of scope as invalidating the corresponding address in memory. This diff fixes that by - marking all local variables that exits the scope with the attribute `AddressOfStackVariable` - before we write the summary for the proc, we make sure to invalidate all such addresses local to the procedure as `Invalid.` If such an address is read, then we would raise a use-after-lifetime issue. Reviewed By: jvillard Differential Revision: D16458355 fbshipit-source-id: 3686524cb --- infer/src/pulse/Pulse.ml | 10 ++-- infer/src/pulse/PulseAbductiveDomain.ml | 49 +++++++++++++++++-- infer/src/pulse/PulseAbductiveDomain.mli | 4 +- infer/src/pulse/PulseDomain.ml | 19 ++++++- infer/src/pulse/PulseDomain.mli | 3 ++ infer/src/pulse/PulseOperations.ml | 19 +++++-- infer/src/pulse/PulseOperations.mli | 2 +- infer/src/pulse/PulseSummary.ml | 2 +- infer/src/pulse/PulseSummary.mli | 2 +- .../tests/codetoanalyze/cpp/pulse/issues.exp | 3 +- .../cpp/pulse/use_after_scope.cpp | 24 +++++++++ 11 files changed, 120 insertions(+), 17 deletions(-) create mode 100644 infer/tests/codetoanalyze/cpp/pulse/use_after_scope.cpp diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 2d01d2825..31111a3da 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -191,8 +191,8 @@ module PulseTransferFunctions = struct [post] | Call (ret, call_exp, actuals, loc, call_flags) -> dispatch_call summary ret call_exp actuals loc call_flags astate |> check_error summary - | Metadata (ExitScope (vars, _)) -> - [PulseOperations.remove_vars vars astate] + | Metadata (ExitScope (vars, location)) -> + [PulseOperations.remove_vars vars location astate] | Metadata (VariableLifetimeBegins (pvar, _, location)) -> [PulseOperations.realloc_var (Var.of_pvar pvar) location astate] | Metadata (Abstract _ | Nullify _ | Skip) -> @@ -219,14 +219,14 @@ let checker {Callbacks.exe_env; summary} = let tenv = Exe_env.get_tenv exe_env (Summary.get_proc_name summary) in let proc_data = ProcData.make summary tenv () in AbstractAddress.init () ; + let pdesc = Summary.get_proc_desc summary in let initial = - DisjunctiveTransferFunctions.Disjuncts.singleton - (PulseAbductiveDomain.mk_initial (Summary.get_proc_desc summary)) + DisjunctiveTransferFunctions.Disjuncts.singleton (PulseAbductiveDomain.mk_initial pdesc) in match DisjunctiveAnalyzer.compute_post proc_data ~initial with | Some posts -> PulsePayload.update_summary - (PulseSummary.of_posts (DisjunctiveTransferFunctions.Disjuncts.elements posts)) + (PulseSummary.of_posts pdesc (DisjunctiveTransferFunctions.Disjuncts.elements posts)) summary | None -> summary diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 4d44c09db..271256c40 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -275,6 +275,8 @@ let discard_unreachable ({pre; post} as astate) = ; post= Domain.make (post :> PulseDomain.t).stack post_new_heap } +let is_local var astate = not (Var.is_return var || Stack.is_abducible astate var) + module PrePost = struct type domain_t = t @@ -283,7 +285,7 @@ module PrePost = struct let filter_for_summary astate = let post_stack = BaseStack.filter - (fun var _ -> Var.is_return var || Stack.is_abducible astate var) + (fun var _ -> not (is_local var astate)) (astate.post :> PulseDomain.t).stack in (* deregister empty edges in pre *) @@ -296,7 +298,44 @@ module PrePost = struct ; post= Domain.update ~stack:post_stack astate.post } - let of_post astate = filter_for_summary astate |> discard_unreachable + let add_out_of_scope_attribute addr pvar location history heap typ = + let action = + PulseDomain.InterprocAction.Immediate + {imm= PulseDomain.Invalidation.GoneOutOfScope (pvar, typ); location} + in + let attr = PulseDomain.Attributes.singleton (Invalid {action; history}) in + PulseDomain.Memory.add_attributes addr attr heap + + + (** invalidate local variables going out of scope *) + let invalidate_locals pdesc astate : t = + let heap : BaseMemory.t = (astate.post :> PulseDomain.t).heap in + let heap' = + PulseDomain.Memory.fold_attrs + (fun addr attrs heap -> + PulseDomain.Attributes.get_address_of_stack_variable attrs + |> Option.value_map ~default:heap ~f:(fun (var, history, location) -> + let get_local_typ_opt pvar = + Procdesc.get_locals pdesc + |> List.find_map ~f:(fun ProcAttributes.{name; typ} -> + if Mangled.equal name (Pvar.get_name pvar) then Some typ else None ) + in + match var with + | Var.ProgramVar pvar -> + get_local_typ_opt pvar + |> Option.value_map ~default:heap + ~f:(add_out_of_scope_attribute addr pvar location history heap) + | _ -> + heap ) ) + heap heap + in + if phys_equal heap heap' then astate + else {pre= astate.pre; post= Domain.update astate.post ~heap:heap'} + + + let of_post pdesc astate = + filter_for_summary astate |> discard_unreachable |> invalidate_locals pdesc + (* {2 machinery to apply a pre/post pair corresponding to a function's summary in a function call to the current state} *) @@ -533,7 +572,11 @@ module PrePost = struct PulseDomain.InterprocAction.ViaCall {action= trace.action; f= Call proc_name; location} ; history= trace.history } - | MustBeValid _ | AddressOfCppTemporary (_, _) | Closure _ | StdVectorReserve -> + | MustBeValid _ + | AddressOfCppTemporary (_, _) + | AddressOfStackVariable (_, _, _) + | Closure _ + | StdVectorReserve -> attr diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index 9e92515ff..4707daf05 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -76,6 +76,8 @@ module Memory : sig what it points to or creates a fresh value if that edge didn't exist. *) end +val is_local : Var.t -> t -> bool + module PrePost : sig type domain_t = t @@ -83,7 +85,7 @@ module PrePost : sig val pp : Format.formatter -> t -> unit - val of_post : domain_t -> t + val of_post : Procdesc.t -> domain_t -> t val apply : Typ.Procname.t diff --git a/infer/src/pulse/PulseDomain.ml b/infer/src/pulse/PulseDomain.ml index febdb7ffa..cd888bc6e 100644 --- a/infer/src/pulse/PulseDomain.ml +++ b/infer/src/pulse/PulseDomain.ml @@ -247,6 +247,7 @@ module Attribute = struct | Invalid of Invalidation.t Trace.t | MustBeValid of unit InterprocAction.t | AddressOfCppTemporary of Var.t * ValueHistory.t + | AddressOfStackVariable of Var.t * ValueHistory.t * Location.t | Closure of Typ.Procname.t | StdVectorReserve [@@deriving compare, variants] @@ -257,6 +258,13 @@ module Attribute = struct let closure_rank = Variants.to_rank (Closure (Typ.Procname.from_string_c_fun "")) + let address_of_stack_variable_rank = + let pname = Typ.Procname.from_string_c_fun "" in + let var = Var.of_pvar (Pvar.mk (Mangled.from_string "") pname) in + let location = Location.dummy in + Variants.to_rank (AddressOfStackVariable (var, [], location)) + + let invalid_rank = Variants.to_rank (Invalid @@ -278,7 +286,9 @@ module Attribute = struct action Location.pp (InterprocAction.to_outer_location action) | AddressOfCppTemporary (var, history) -> - F.fprintf f "&%a (%a)" Var.pp var ValueHistory.pp history + F.fprintf f "t&%a (%a)" Var.pp var ValueHistory.pp history + | AddressOfStackVariable (var, history, location) -> + F.fprintf f "s&%a (%a) at %a" Var.pp var ValueHistory.pp history Location.pp location | Closure pname -> Typ.Procname.pp f pname | StdVectorReserve -> @@ -309,6 +319,13 @@ module Attributes = struct proc_name ) + let get_address_of_stack_variable attrs = + Set.find_rank attrs Attribute.address_of_stack_variable_rank + |> Option.map ~f:(fun attr -> + let[@warning "-8"] (Attribute.AddressOfStackVariable (var, history, loc)) = attr in + (var, history, loc) ) + + let is_std_vector_reserved attrs = Set.find_rank attrs Attribute.std_vector_reserve_rank |> Option.is_some diff --git a/infer/src/pulse/PulseDomain.mli b/infer/src/pulse/PulseDomain.mli index c06f07e68..fcb6894c0 100644 --- a/infer/src/pulse/PulseDomain.mli +++ b/infer/src/pulse/PulseDomain.mli @@ -84,6 +84,7 @@ module Attribute : sig | Invalid of Invalidation.t Trace.t | MustBeValid of unit InterprocAction.t | AddressOfCppTemporary of Var.t * ValueHistory.t + | AddressOfStackVariable of Var.t * ValueHistory.t * Location.t | Closure of Typ.Procname.t | StdVectorReserve [@@deriving compare] @@ -93,6 +94,8 @@ module Attributes : sig include PrettyPrintable.PPUniqRankSet with type elt = Attribute.t val get_must_be_valid : t -> unit InterprocAction.t option + + val get_address_of_stack_variable : t -> (Var.t * ValueHistory.t * Location.t) option end module AbstractAddress : sig diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 17730fa6c..8d563b5d7 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -291,12 +291,25 @@ let mark_address_of_cpp_temporary history variable address astate = astate -let remove_vars vars astate = +let mark_address_of_stack_variable history variable location address astate = + Memory.add_attributes address + (Attributes.singleton (AddressOfStackVariable (variable, history, location))) + astate + + +let remove_vars vars location astate = let astate = List.fold vars ~init:astate ~f:(fun astate var -> match Stack.find_opt var astate with - | Some (address, history) when Var.is_cpp_temporary var -> - mark_address_of_cpp_temporary history var address astate + | Some (address, history) -> + let astate = + if PulseAbductiveDomain.is_local var astate then + mark_address_of_stack_variable history var location address astate + else astate + in + if Var.is_cpp_temporary var then + mark_address_of_cpp_temporary history var address astate + else astate | _ -> astate ) in diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index 6a7f44c18..6fc11a270 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -90,7 +90,7 @@ val shallow_copy : Location.t -> PulseDomain.AddrTracePair.t -> t -> (t * AbstractAddress.t) access_result (** returns the address of a new cell with the same edges as the original *) -val remove_vars : Var.t list -> t -> t +val remove_vars : Var.t list -> Location.t -> t -> t val check_address_escape : Location.t diff --git a/infer/src/pulse/PulseSummary.ml b/infer/src/pulse/PulseSummary.ml index 81cef0698..fa65ce1bc 100644 --- a/infer/src/pulse/PulseSummary.ml +++ b/infer/src/pulse/PulseSummary.ml @@ -8,7 +8,7 @@ open! IStd type t = PulseAbductiveDomain.PrePost.t list -let of_posts posts = List.map posts ~f:PulseAbductiveDomain.PrePost.of_post +let of_posts pdesc posts = List.map posts ~f:(PulseAbductiveDomain.PrePost.of_post pdesc) let pp fmt summary = PrettyPrintable.pp_collection ~pp_item:PulseAbductiveDomain.PrePost.pp fmt summary diff --git a/infer/src/pulse/PulseSummary.mli b/infer/src/pulse/PulseSummary.mli index 17c25350f..94ded779c 100644 --- a/infer/src/pulse/PulseSummary.mli +++ b/infer/src/pulse/PulseSummary.mli @@ -8,6 +8,6 @@ open! IStd type t = PulseAbductiveDomain.PrePost.t list -val of_posts : PulseAbductiveDomain.t list -> t +val of_posts : Procdesc.t -> PulseAbductiveDomain.t list -> t val pp : Format.formatter -> t -> unit diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index e39224e22..ff7bd637e 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -1,4 +1,4 @@ -codetoanalyze/cpp/pulse/basic_string.cpp, use_range_of_invalidated_temporary_string_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `setLanguage()` here,when calling `std::basic_string::~basic_string()` (modelled) here,when calling `deleting the underlying string` (modelled) here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,variable declared,when calling `Range::operator[]()` here,invalid access occurs here] +codetoanalyze/cpp/pulse/basic_string.cpp, use_range_of_invalidated_temporary_string_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,returned from call to `Range::Range()`,when calling `setLanguage()` here,when calling `std::basic_string::~basic_string()` (modelled) here,when calling `deleting the underlying string` (modelled) here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,variable declared,when calling `Range::operator[]()` here,invalid access occurs here] codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,invalid access occurs here] codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,invalid access occurs here] codetoanalyze/cpp/pulse/closures.cpp, call_lambda_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,when calling `call_lambda_bad::lambda_closures.cpp:163:12::operator()()` here,invalid access occurs here] @@ -45,6 +45,7 @@ codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_afte codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_global_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `free_global_pointer_ok()` here,memory was invalidated by call to `free()` here,use-after-lifetime part of the trace starts here,when calling `free_global_pointer_ok()` here,invalid access occurs here] codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by call to `free()` here,use-after-lifetime part of the trace starts here,invalid access occurs here] codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by call to `free()` here,use-after-lifetime part of the trace starts here,invalid access occurs here] +codetoanalyze/cpp/pulse/use_after_scope.cpp, access_out_of_scope_stack_ref_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable declared,when calling `invalidate_local_ok()` here,memory is the address of a stack variable `t` whose lifetime has ended here,use-after-lifetime part of the trace starts here,variable declared,assigned,returned from call to `invalidate_local_ok()`,invalid access occurs here] codetoanalyze/cpp/pulse/vector.cpp, FP_init_fill_then_push_back_loop_ok, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::push_back()` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at()` (modelled),assigned,invalid access occurs here] codetoanalyze/cpp/pulse/vector.cpp, assign_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::assign()` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at()` (modelled),assigned,invalid access occurs here] codetoanalyze/cpp/pulse/vector.cpp, clear_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::clear()` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at()` (modelled),assigned,invalid access occurs here] diff --git a/infer/tests/codetoanalyze/cpp/pulse/use_after_scope.cpp b/infer/tests/codetoanalyze/cpp/pulse/use_after_scope.cpp new file mode 100644 index 000000000..f71c4b388 --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/pulse/use_after_scope.cpp @@ -0,0 +1,24 @@ +/* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ +#include + +void invalidate_local_ok(int** pp) { + int t = 0xdeadbeef; + *pp = &t; // <-- potential bug here since t goes out of scope +} + +void access_out_of_scope_stack_ref_bad() { + int* p = NULL; + invalidate_local_ok(&p); + int k = *p; // accessing invalid +} + +void no_access_out_of_scope_stack_ref_ok() { + int* p = NULL; + invalidate_local_ok(&p); + // p is not accessed, hence ok +}