From 65d031af66f1a3c19f61bc6befb619233ea8cf04 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Wed, 12 Dec 2018 09:09:12 -0800 Subject: [PATCH] [pulse] model lambda captures MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Summary: When a lambda gets created, record the abstract addresses it captures, then complain if we see some of them be invalidated before it is called. Add a notion of "allocator" for reporting better messages. The messages are still a bit sucky, will need to improve them more generally at some point. ```  jul   lambda  ~  infer  1  infer -g --pulse-only -- clang -std=c++11 -c infer/tests/codetoanalyze/cpp/pulse/closures.cpp Logs in /home/jul/infer.fb/infer-out/logs Capturing in make/cc mode... Found 1 source file to analyze in /home/jul/infer.fb/infer-out Found 2 issues infer/tests/codetoanalyze/cpp/pulse/closures.cpp:21: error: USE_AFTER_DESTRUCTOR `&(f)` accesses address `s` captured by `&(f)` as `s` invalidated by destructor call `S_~S(s)` at line 20, column 3 past its lifetime (debug: 5). 19. f = [&s] { return s.f; }; 20. } // destructor for s called here 21. > return f(); // s used here 22. } 23. infer/tests/codetoanalyze/cpp/pulse/closures.cpp:30: error: USE_AFTER_DESTRUCTOR `&(f)` accesses address `s` captured by `&(f)` as `s` invalidated by destructor call `S_~S(s)` at line 29, column 3 past its lifetime (debug: 8). 28. f = [&] { return s.f; }; 29. } 30. > return f(); 31. } 32. Summary of the reports USE_AFTER_DESTRUCTOR: 2 ``` Reviewed By: da319 Differential Revision: D13400074 fbshipit-source-id: 3c68ff4ea --- infer/src/checkers/Pulse.ml | 2 + infer/src/checkers/PulseDomain.ml | 119 ++++++++++++++++-- infer/src/checkers/PulseDomain.mli | 15 +++ infer/src/checkers/PulseModels.ml | 19 ++- infer/src/istd/IContainer.ml | 7 ++ infer/src/istd/IContainer.mli | 6 + infer/src/istd/Pp.ml | 2 + infer/src/istd/Pp.mli | 8 ++ .../codetoanalyze/cpp/pulse/closures.cpp | 6 +- .../tests/codetoanalyze/cpp/pulse/issues.exp | 2 + 10 files changed, 171 insertions(+), 15 deletions(-) diff --git a/infer/src/checkers/Pulse.ml b/infer/src/checkers/Pulse.ml index 61bd5c755..956632923 100644 --- a/infer/src/checkers/Pulse.ml +++ b/infer/src/checkers/Pulse.ml @@ -47,6 +47,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | AccessExpression rhs_access -> PulseDomain.read loc rhs_access astate >>= fun (astate, rhs_value) -> PulseDomain.write loc lhs_access rhs_value astate + | Closure (pname, captured) -> + PulseDomain.Closures.record loc lhs_access pname captured astate | Cast (_, e) -> exec_assign lhs_access e loc astate | _ -> diff --git a/infer/src/checkers/PulseDomain.ml b/infer/src/checkers/PulseDomain.ml index d47860cfb..0021c4504 100644 --- a/infer/src/checkers/PulseDomain.ml +++ b/infer/src/checkers/PulseDomain.ml @@ -52,11 +52,25 @@ module Attribute = struct (* OPTIM: [Invalid _] is first in the order to make queries about invalidation status more efficient (only need to look at the first element in the set of attributes to know if an address is invalid) *) - type t = Invalid of Invalidation.t | StdVectorReserve [@@deriving compare] + type t = + (* DO NOT MOVE, see toplevel comment *) + | Invalid of Invalidation.t + | Closure of + Typ.Procname.t + * (AccessPath.base * HilExp.AccessExpression.t * AbstractAddressSet.t) list + * Location.t + | StdVectorReserve + [@@deriving compare] let pp f = function | Invalid invalidation -> Invalidation.pp f invalidation + | Closure (pname, captured, location) -> + F.fprintf f "%a[%a] (%a)" Typ.Procname.pp pname + (Pp.seq ~sep:"," + (Pp.triple ~fst:AccessPath.pp_base ~snd:HilExp.AccessExpression.pp + ~trd:AbstractAddressSet.pp)) + captured Location.pp location | StdVectorReserve -> F.pp_print_string f "std::vector::reserve()" end @@ -478,24 +492,51 @@ end type actor = {access_expr: HilExp.AccessExpression.t; location: Location.t} [@@deriving compare] +type allocator = + | Unknown + | Closure of + { lambda: HilExp.AccessExpression.t (** some way to refer to the closure *) + ; access_expr: HilExp.AccessExpression.t (** the access expr that was captured *) + ; as_base: AccessPath.base (** the variable it was captured as *) + ; location: Location.t } + +let pp_allocator f = function + | Unknown -> + () + | Closure {lambda; access_expr; as_base} -> + F.fprintf f "`%a` captured by `%a` as `%a` " HilExp.AccessExpression.pp access_expr + HilExp.AccessExpression.pp lambda AccessPath.pp_base as_base + + +let location_of_allocator = function Unknown -> None | Closure {location} -> Some location + module Diagnostic = struct type t = | AccessToInvalidAddress of - { invalidated_by: Invalidation.t + { allocated_by: allocator + ; invalidated_by: Invalidation.t ; accessed_by: actor ; address: AbstractAddress.t } let get_location (AccessToInvalidAddress {accessed_by= {location}}) = location - let get_message (AccessToInvalidAddress {accessed_by; invalidated_by; address}) = + let get_message (AccessToInvalidAddress {allocated_by; accessed_by; invalidated_by; address}) = let pp_debug_address f = if Config.debug_mode then F.fprintf f " (debug: %a)" AbstractAddress.pp address in - F.asprintf "`%a` accesses address %a past its lifetime%t" HilExp.AccessExpression.pp - accessed_by.access_expr Invalidation.pp invalidated_by pp_debug_address + F.asprintf "`%a` accesses address %a%a past its lifetime%t" HilExp.AccessExpression.pp + accessed_by.access_expr pp_allocator allocated_by Invalidation.pp invalidated_by + pp_debug_address - let get_trace (AccessToInvalidAddress {accessed_by; invalidated_by}) = + let get_trace (AccessToInvalidAddress {allocated_by; accessed_by; invalidated_by}) = + let allocated_by_trace = + match location_of_allocator allocated_by with + | None -> + [] + | Some location -> + [Errlog.make_trace_element 0 location (F.asprintf "%ahere" pp_allocator allocated_by) []] + in let invalidated_by_trace = Invalidation.get_location invalidated_by |> Option.map ~f:(fun location -> @@ -504,7 +545,7 @@ module Diagnostic = struct [] ) |> Option.to_list in - invalidated_by_trace + allocated_by_trace @ invalidated_by_trace @ [ Errlog.make_trace_element 0 accessed_by.location (F.asprintf "accessed `%a` here" HilExp.AccessExpression.pp accessed_by.access_expr) [] ] @@ -521,17 +562,19 @@ module Operations = struct open Result.Monad_infix (** Check that the address is not known to be invalid *) - let check_addr_access actor address astate = + let check_addr_access ?(allocated_by = Unknown) actor address astate = match Memory.get_invalidation address astate.heap with | Some invalidated_by -> - Error (Diagnostic.AccessToInvalidAddress {invalidated_by; accessed_by= actor; address}) + Error + (Diagnostic.AccessToInvalidAddress + {invalidated_by; accessed_by= actor; address; allocated_by}) | None -> Ok astate - let check_addr_access_set actor addresses astate = + let check_addr_access_set ?allocated_by actor addresses astate = AbstractAddressSet.fold - (fun addr result -> result >>= check_addr_access actor addr) + (fun addr result -> result >>= check_addr_access ?allocated_by actor addr) addresses (Ok astate) @@ -670,6 +713,60 @@ module Operations = struct if phys_equal stack astate.stack then astate else {astate with stack} end +module Closures = struct + open Result.Monad_infix + + let check_captured_address location lambda address astate = + match Memory.find_opt address astate.heap with + | None -> + Ok astate + | Some (_, attributes) -> + IContainer.iter_result ~fold:(IContainer.fold_of_pervasives_fold ~fold:Attributes.fold) + attributes ~f:(function + | Attribute.Closure (_, captured, lambda_location) -> + IContainer.iter_result ~fold:List.fold captured + ~f:(fun (base, access_expr, addresses) -> + Operations.check_addr_access_set + ~allocated_by: + (Closure {lambda; access_expr; as_base= base; location= lambda_location}) + {access_expr= lambda; location} addresses astate + >>| fun _ -> () ) + | _ -> + Ok () ) + >>| fun () -> astate + + + let check_captured_addresses location lambda addresses astate = + Container.fold_result ~fold:(IContainer.fold_of_pervasives_fold ~fold:AbstractAddressSet.fold) + addresses ~init:astate ~f:(fun astate address -> + check_captured_address location lambda address astate ) + + + let write location access_expr pname captured astate = + let closure_addr = AbstractAddress.mk_fresh () in + Operations.write location access_expr (AbstractAddressSet.singleton closure_addr) astate + >>| fun astate -> + { astate with + heap= + Memory.add_attributes closure_addr + (Attributes.singleton (Closure (pname, captured, location))) + astate.heap } + + + let record location access_expr pname captured astate = + List.fold_result captured ~init:(astate, []) + ~f:(fun ((astate, captured) as result) (captured_base, captured_exp) -> + match captured_exp with + | HilExp.AccessExpression (AddressOf access_expr) -> + Operations.read location access_expr astate + >>= fun (astate, addresses) -> + Ok (astate, (captured_base, access_expr, addresses) :: captured) + | _ -> + Ok result ) + >>= fun (astate, captured_addresses) -> + write location access_expr pname captured_addresses astate +end + module StdVector = struct open Result.Monad_infix diff --git a/infer/src/checkers/PulseDomain.mli b/infer/src/checkers/PulseDomain.mli index bcb3a097f..9a8097605 100644 --- a/infer/src/checkers/PulseDomain.mli +++ b/infer/src/checkers/PulseDomain.mli @@ -35,6 +35,21 @@ end type 'a access_result = ('a, Diagnostic.t) result +module Closures : sig + val check_captured_addresses : + Location.t -> HilExp.AccessExpression.t -> AbstractAddressSet.t -> t -> t access_result + (** assert the validity of the addresses captured by the lambda *) + + val record : + Location.t + -> HilExp.AccessExpression.t + -> Typ.Procname.t + -> (AccessPath.base * HilExp.t) list + -> t + -> t access_result + (** record that the access expression points to a lambda with its captured addresses *) +end + module StdVector : sig val is_reserved : Location.t -> HilExp.AccessExpression.t -> t -> (t * bool) access_result diff --git a/infer/src/checkers/PulseModels.ml b/infer/src/checkers/PulseModels.ml index ce3ef10f2..7735d6e53 100644 --- a/infer/src/checkers/PulseModels.ml +++ b/infer/src/checkers/PulseModels.ml @@ -57,6 +57,20 @@ module Cplusplus = struct Ok astate + let operator_call : model = + fun location ~ret:(ret_var, _) ~actuals astate -> + PulseDomain.read_all location (List.concat_map actuals ~f:HilExp.get_access_exprs) astate + >>= fun astate -> + ( match actuals with + | AccessExpression lambda :: _ -> + PulseDomain.read location HilExp.AccessExpression.(dereference (dereference lambda)) astate + >>= fun (astate, address) -> + PulseDomain.Closures.check_captured_addresses location lambda address astate + | _ -> + Ok astate ) + >>| PulseDomain.havoc_var ret_var + + let placement_new : model = fun location ~ret:(ret_var, _) ~actuals astate -> let read_all args astate = @@ -70,7 +84,7 @@ module Cplusplus = struct | _ :: other_actuals -> read_all other_actuals astate >>| PulseDomain.havoc_var ret_var | _ -> - Ok astate + Ok (PulseDomain.havoc_var ret_var astate) end module StdVector = struct @@ -146,7 +160,8 @@ module ProcNameDispatcher = struct let dispatch : (unit, model) ProcnameDispatcher.ProcName.dispatcher = let open ProcnameDispatcher.ProcName in make_dispatcher - [ -"std" &:: "vector" &:: "assign" &--> StdVector.invalidate_references Assign + [ -"std" &:: "function" &:: "operator()" &--> Cplusplus.operator_call + ; -"std" &:: "vector" &:: "assign" &--> StdVector.invalidate_references Assign ; -"std" &:: "vector" &:: "clear" &--> StdVector.invalidate_references Clear ; -"std" &:: "vector" &:: "emplace" &--> StdVector.invalidate_references Emplace ; -"std" &:: "vector" &:: "emplace_back" &--> StdVector.invalidate_references EmplaceBack diff --git a/infer/src/istd/IContainer.ml b/infer/src/istd/IContainer.ml index 36e6707ef..103e8c9ed 100644 --- a/infer/src/istd/IContainer.ml +++ b/infer/src/istd/IContainer.ml @@ -72,3 +72,10 @@ let filter ~fold ~filter t ~init ~f = let map ~f:g fold t ~init ~f = fold t ~init ~f:(fun acc item -> f acc (g item)) + +let fold_of_pervasives_fold ~fold collection ~init ~f = + fold (fun accum item -> f item accum) collection init + + +let iter_result ~fold collection ~f = + Container.fold_result ~fold ~init:() ~f:(fun () item -> f item) collection diff --git a/infer/src/istd/IContainer.mli b/infer/src/istd/IContainer.mli index ca46f4933..efdd13236 100644 --- a/infer/src/istd/IContainer.mli +++ b/infer/src/istd/IContainer.mli @@ -47,3 +47,9 @@ val filter : fold:('t, 'a, 'accum) Container.fold -> filter:('a -> bool) -> ('t, 'a, 'accum) Container.fold val map : f:('a -> 'b) -> ('t, 'a, 'accum) Container.fold -> ('t, 'b, 'accum) Container.fold + +val fold_of_pervasives_fold : + fold:(('a -> 'accum -> 'accum) -> 't -> 'accum -> 'accum) -> ('t, 'a, 'accum) Container.fold + +val iter_result : + fold:('t, 'a, unit) Container.fold -> 't -> f:('a -> (unit, 'err) result) -> (unit, 'err) result diff --git a/infer/src/istd/Pp.ml b/infer/src/istd/Pp.ml index 762306cfe..00edc6f0d 100644 --- a/infer/src/istd/Pp.ml +++ b/infer/src/istd/Pp.ml @@ -171,3 +171,5 @@ let cli_args fmt args = let pair ~fst ~snd fmt (a, b) = F.fprintf fmt "(%a,@,%a)" fst a snd b + +let triple ~fst ~snd ~trd fmt (a, b, c) = F.fprintf fmt "(%a,@,%a@,%a)" fst a snd b trd c diff --git a/infer/src/istd/Pp.mli b/infer/src/istd/Pp.mli index 5b8edcf99..2a80f4421 100644 --- a/infer/src/istd/Pp.mli +++ b/infer/src/istd/Pp.mli @@ -100,3 +100,11 @@ val pair : -> F.formatter -> 'a * 'b -> unit + +val triple : + fst:(F.formatter -> 'a -> unit) + -> snd:(F.formatter -> 'b -> unit) + -> trd:(F.formatter -> 'c -> unit) + -> F.formatter + -> 'a * 'b * 'c + -> unit diff --git a/infer/tests/codetoanalyze/cpp/pulse/closures.cpp b/infer/tests/codetoanalyze/cpp/pulse/closures.cpp index 817479b97..8ebb8c412 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/closures.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/closures.cpp @@ -12,7 +12,7 @@ struct S { S() { f = 1; } }; -int FN_ref_capture_destroy_invoke_bad() { +int ref_capture_destroy_invoke_bad() { std::function f; { S s; @@ -21,7 +21,7 @@ int FN_ref_capture_destroy_invoke_bad() { return f(); // s used here } -int FN_implicit_ref_capture_destroy_invoke_bad() { +int implicit_ref_capture_destroy_invoke_bad() { std::function f; { auto s = S(); @@ -30,10 +30,12 @@ int FN_implicit_ref_capture_destroy_invoke_bad() { return f(); } +// need to understand copy constructor int FN_reassign_lambda_capture_destroy_invoke_bad() { std::function f; { auto s = S(); + // this is a copy constructor auto tmp = [&] { return s.f; }; f = tmp; } diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index baae52f9d..7861b8ae1 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -1,5 +1,7 @@ codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 58, column 5 here,accessed `*(ptr)` here] codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 68, column 7 here,accessed `ptr` here] +codetoanalyze/cpp/pulse/closures.cpp, implicit_ref_capture_destroy_invoke_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [`s` captured by `&(f)` as `s` here,invalidated by destructor call `S_~S(s)` at line 29, column 3 here,accessed `&(f)` here] +codetoanalyze/cpp/pulse/closures.cpp, ref_capture_destroy_invoke_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [`s` captured by `&(f)` as `s` here,invalidated by destructor call `S_~S(s)` at line 20, column 3 here,accessed `&(f)` here] codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 12, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete result` at line 25, column 5 here,accessed `*(result)` here] codetoanalyze/cpp/pulse/returns.cpp, returns::return_deleted_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete x` at line 112, column 3 here,accessed `x` here] codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_branch_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 57, column 5 here,accessed `s` here]