From 433c144840d8c71dbaaedc2ec3109b5d7ed723d5 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Thu, 27 Jun 2019 12:19:23 -0700 Subject: [PATCH] [pulse] calling known lambdas calls the corresponding proc name Summary: We know how to do interprocedural calls so let's use that! Reviewed By: mbouaziz Differential Revision: D16008164 fbshipit-source-id: 4c34bf704 --- infer/src/pulse/Pulse.ml | 44 +++-------------- infer/src/pulse/PulseAbductiveDomain.ml | 4 ++ infer/src/pulse/PulseAbductiveDomain.mli | 2 + infer/src/pulse/PulseDomain.ml | 16 +++++++ infer/src/pulse/PulseDomain.mli | 2 + infer/src/pulse/PulseModels.ml | 48 +++++++++++-------- infer/src/pulse/PulseModels.mli | 3 +- infer/src/pulse/PulseOperations.ml | 29 +++++++++++ infer/src/pulse/PulseOperations.mli | 11 +++++ infer/src/pulse/PulsePayload.ml | 14 ++++++ infer/src/pulse/PulsePayload.mli | 10 ++++ .../codetoanalyze/cpp/pulse/closures.cpp | 13 +++++ .../tests/codetoanalyze/cpp/pulse/issues.exp | 1 + 13 files changed, 139 insertions(+), 58 deletions(-) create mode 100644 infer/src/pulse/PulsePayload.ml create mode 100644 infer/src/pulse/PulsePayload.mli diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index abda2f70c..698b715dc 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -40,12 +40,6 @@ let check_error summary = function raise_notrace AbstractDomain.Stop_analysis -module Payload = SummaryPayload.Make (struct - type t = PulseSummary.t - - let field = Payloads.Fields.pulse -end) - let proc_name_of_call call_exp = match (call_exp : Exp.t) with | Const (Cfun proc_name) | Closure {name= proc_name} -> @@ -86,39 +80,13 @@ module PulseTransferFunctions = struct let interprocedural_call caller_summary ret call_exp actuals flags call_loc astate = - let unknown_function reason = - exec_unknown_call reason ret call_exp actuals flags call_loc astate >>| List.return - in match proc_name_of_call call_exp with - | Some callee_pname -> ( - match Payload.read_full caller_summary.Summary.proc_desc callee_pname with - | Some (callee_proc_desc, preposts) -> - let formals = - Procdesc.get_formals callee_proc_desc - |> List.map ~f:(fun (mangled, _) -> Pvar.mk mangled callee_pname |> Var.of_pvar) - in - (* call {!PulseAbductiveDomain.PrePost.apply} on each pre/post pair in the summary. *) - List.fold_result preposts ~init:[] ~f:(fun posts pre_post -> - (* apply all pre/post specs *) - PulseAbductiveDomain.PrePost.apply callee_pname call_loc pre_post ~formals ~actuals - astate - >>| fun (post, return_val_opt) -> - let event = ValueHistory.Call {f= `Call callee_pname; location= call_loc} in - let post = - match return_val_opt with - | Some return_val -> - PulseOperations.write_id (fst ret) (return_val, [event]) post - | None -> - PulseOperations.havoc_id (fst ret) [event] post - in - post :: posts ) - | None -> - (* no spec found for some reason (unknown function, ...) *) - L.d_printfln "No spec found for %a@\n" Typ.Procname.pp callee_pname ; - unknown_function (`UnknownCall callee_pname) ) + | Some callee_pname -> + PulseOperations.call ~caller_summary call_loc callee_pname ~ret ~actuals astate | None -> L.d_printfln "Indirect call %a@\n" Exp.pp call_exp ; - unknown_function (`IndirectCall call_exp) + exec_unknown_call (`IndirectCall call_exp) ret call_exp actuals flags call_loc astate + >>| List.return (** has an object just gone out of scope? *) @@ -167,7 +135,7 @@ module PulseTransferFunctions = struct match model with | Some model -> L.d_printfln "Found model for call@\n" ; - model call_loc ~ret ~actuals:actuals_evaled astate + model ~caller_summary:summary call_loc ~ret ~actuals:actuals_evaled astate | None -> ( (* do interprocedural call then destroy objects going out of scope *) PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse interproc call" ())) ; @@ -254,7 +222,7 @@ let checker {Callbacks.proc_desc; tenv; summary} = in match DisjunctiveAnalyzer.compute_post proc_data ~initial with | Some posts -> - Payload.update_summary + PulsePayload.update_summary (PulseSummary.of_posts (DisjunctiveTransferFunctions.Disjuncts.elements posts)) summary | None -> diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index b3926100b..2f98bc913 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -204,6 +204,10 @@ module Memory = struct map_post_heap astate ~f:(fun heap -> BaseMemory.add_attributes address attributes heap) + let get_closure_proc_name addr astate = + BaseMemory.get_closure_proc_name addr (astate.post :> base_domain).heap + + let std_vector_reserve addr astate = map_post_heap astate ~f:(fun heap -> BaseMemory.std_vector_reserve addr heap) diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index fb052e864..9e92515ff 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -65,6 +65,8 @@ module Memory : sig -> t -> t + val get_closure_proc_name : AbstractAddress.t -> t -> Typ.Procname.t option + val is_std_vector_reserved : AbstractAddress.t -> t -> bool val std_vector_reserve : AbstractAddress.t -> t -> t diff --git a/infer/src/pulse/PulseDomain.ml b/infer/src/pulse/PulseDomain.ml index ecc48ef1a..6d82c57bc 100644 --- a/infer/src/pulse/PulseDomain.ml +++ b/infer/src/pulse/PulseDomain.ml @@ -248,6 +248,8 @@ module Attribute = struct let to_rank = Variants.to_rank + let closure_rank = Variants.to_rank (Closure (Typ.Procname.from_string_c_fun "")) + let invalid_rank = Variants.to_rank (Invalid @@ -293,6 +295,13 @@ module Attributes = struct action ) + let get_closure_proc_name attrs = + Set.find_rank attrs Attribute.closure_rank + |> Option.map ~f:(fun attr -> + let[@warning "-8"] (Attribute.Closure proc_name) = attr in + proc_name ) + + let is_std_vector_reserved attrs = Set.find_rank attrs Attribute.std_vector_reserve_rank |> Option.is_some @@ -397,6 +406,8 @@ module Memory : sig val check_valid : AbstractAddress.t -> t -> (unit, Invalidation.t Trace.t) result + val get_closure_proc_name : AbstractAddress.t -> t -> Typ.Procname.t option + val std_vector_reserve : AbstractAddress.t -> t -> t val is_std_vector_reserved : AbstractAddress.t -> t -> bool @@ -471,6 +482,11 @@ end = struct Ok () + let get_closure_proc_name address memory = + Graph.find_opt address (snd memory) + |> Option.bind ~f:(fun attributes -> Attributes.get_closure_proc_name attributes) + + let std_vector_reserve address memory = add_attribute address Attribute.StdVectorReserve memory let is_std_vector_reserved address memory = diff --git a/infer/src/pulse/PulseDomain.mli b/infer/src/pulse/PulseDomain.mli index 7246742fa..0a3ab71ba 100644 --- a/infer/src/pulse/PulseDomain.mli +++ b/infer/src/pulse/PulseDomain.mli @@ -163,6 +163,8 @@ module Memory : sig val check_valid : AbstractAddress.t -> t -> (unit, Invalidation.t Trace.t) result + val get_closure_proc_name : AbstractAddress.t -> t -> Typ.Procname.t option + val std_vector_reserve : AbstractAddress.t -> t -> t val is_std_vector_reserved : AbstractAddress.t -> t -> bool diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 9145897bd..397e084ac 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -8,7 +8,8 @@ open! IStd open Result.Monad_infix type exec_fun = - Location.t + caller_summary:Summary.t + -> Location.t -> ret:Ident.t * Typ.t -> actuals:(PulseDomain.AddrTracePair.t * Typ.t) list -> PulseAbductiveDomain.t @@ -18,7 +19,7 @@ type model = exec_fun module Misc = struct let shallow_copy model_desc : model = - fun location ~ret:(ret_id, _) ~actuals astate -> + fun ~caller_summary:_ location ~ret:(ret_id, _) ~actuals astate -> let event = PulseDomain.ValueHistory.Call {f= `Model model_desc; location} in ( match actuals with | [(dest_pointer_hist, _); (src_pointer_hist, _)] -> @@ -35,14 +36,14 @@ module Misc = struct >>| fun astate -> [PulseOperations.havoc_id ret_id [event] astate] - let early_exit : model = fun _ ~ret:_ ~actuals:_ _ -> Ok [] + let early_exit : model = fun ~caller_summary:_ _ ~ret:_ ~actuals:_ _ -> Ok [] - let skip : model = fun _ ~ret:_ ~actuals:_ astate -> Ok [astate] + let skip : model = fun ~caller_summary:_ _ ~ret:_ ~actuals:_ astate -> Ok [astate] end module C = struct let free : model = - fun location ~ret:_ ~actuals astate -> + fun ~caller_summary:_ location ~ret:_ ~actuals astate -> match actuals with | [(deleted_access, _)] -> PulseOperations.invalidate location @@ -55,7 +56,7 @@ end module Cplusplus = struct let delete : model = - fun location ~ret:_ ~actuals astate -> + fun ~caller_summary:_ location ~ret:_ ~actuals astate -> match actuals with | [(deleted_access, _)] -> PulseOperations.invalidate location @@ -67,7 +68,7 @@ module Cplusplus = struct let placement_new : model = - fun location ~ret:(ret_id, _) ~actuals astate -> + fun ~caller_summary:_ location ~ret:(ret_id, _) ~actuals astate -> let event = PulseDomain.ValueHistory.Call {f= `Model ""; location} in match List.rev actuals with | ((address, _), _) :: _ -> @@ -78,19 +79,28 @@ end module StdFunction = struct let operator_call : model = - fun location ~ret:(ret_id, _) ~actuals astate -> - ( match actuals with - | (lambda_ptr_hist, _) :: _ -> + fun ~caller_summary location ~ret ~actuals astate -> + let havoc_ret (ret_id, _) astate = + let event = + PulseDomain.ValueHistory.Call {f= `Model "std::function::operator()"; location} + in + [PulseOperations.havoc_id ret_id [event] astate] + in + match actuals with + | [] -> + Ok (havoc_ret ret astate) + | (lambda_ptr_hist, _) :: actuals -> ( PulseOperations.eval_access location lambda_ptr_hist Dereference astate >>= fun (astate, (lambda, _)) -> PulseOperations.Closures.check_captured_addresses (PulseDomain.InterprocAction.Immediate {imm= (); location}) lambda astate - | _ -> - Ok astate ) - >>| fun astate -> - let event = PulseDomain.ValueHistory.Call {f= `Model ""; location} in - [PulseOperations.havoc_id ret_id [event] astate] + >>= fun astate -> + match PulseAbductiveDomain.Memory.get_closure_proc_name lambda astate with + | None -> + (* we don't know what proc name this lambda resolves to *) Ok (havoc_ret ret astate) + | Some callee_proc_name -> + PulseOperations.call ~caller_summary location callee_proc_name ~ret ~actuals astate ) end module StdVector = struct @@ -125,7 +135,7 @@ module StdVector = struct let invalidate_references vector_f : model = - fun location ~ret:_ ~actuals astate -> + fun ~caller_summary:_ location ~ret:_ ~actuals astate -> match actuals with | (vector, _) :: _ -> let crumb = @@ -141,7 +151,7 @@ module StdVector = struct let at : model = - fun location ~ret ~actuals astate -> + fun ~caller_summary:_ location ~ret ~actuals astate -> let event = PulseDomain.ValueHistory.Call {f= `Model "std::vector::at"; location} in match actuals with | [(vector, _); (index, _)] -> @@ -152,7 +162,7 @@ module StdVector = struct let reserve : model = - fun location ~ret:_ ~actuals astate -> + fun ~caller_summary:_ location ~ret:_ ~actuals astate -> match actuals with | [(vector, _); _value] -> let crumb = PulseDomain.ValueHistory.Call {f= `Model "std::vector::reserve"; location} in @@ -164,7 +174,7 @@ module StdVector = struct let push_back : model = - fun location ~ret:_ ~actuals astate -> + fun ~caller_summary:_ location ~ret:_ ~actuals astate -> match actuals with | [(vector, _); _value] -> let crumb = PulseDomain.ValueHistory.Call {f= `Model "std::vector::push_back"; location} in diff --git a/infer/src/pulse/PulseModels.mli b/infer/src/pulse/PulseModels.mli index 8e9360fec..59664bb57 100644 --- a/infer/src/pulse/PulseModels.mli +++ b/infer/src/pulse/PulseModels.mli @@ -7,7 +7,8 @@ open! IStd type exec_fun = - Location.t + caller_summary:Summary.t + -> Location.t -> ret:Ident.t * Typ.t -> actuals:(PulseDomain.AddrTracePair.t * Typ.t) list -> PulseAbductiveDomain.t diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index b17050b53..b7e272a64 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -292,3 +292,32 @@ let remove_vars vars astate = in let astate' = Stack.remove_vars vars astate in if phys_equal astate' astate then astate else PulseAbductiveDomain.discard_unreachable astate' + + +let call ~caller_summary call_loc callee_pname ~ret ~actuals astate = + match PulsePayload.read_full caller_summary.Summary.proc_desc callee_pname with + | Some (callee_proc_desc, preposts) -> + let formals = + Procdesc.get_formals callee_proc_desc + |> List.map ~f:(fun (mangled, _) -> Pvar.mk mangled callee_pname |> Var.of_pvar) + in + (* call {!PulseAbductiveDomain.PrePost.apply} on each pre/post pair in the summary. *) + List.fold_result preposts ~init:[] ~f:(fun posts pre_post -> + (* apply all pre/post specs *) + PulseAbductiveDomain.PrePost.apply callee_pname call_loc pre_post ~formals ~actuals + astate + >>| fun (post, return_val_opt) -> + let event = ValueHistory.Call {f= `Call callee_pname; location= call_loc} in + let post = + match return_val_opt with + | Some return_val -> + write_id (fst ret) (return_val, [event]) post + | None -> + havoc_id (fst ret) [event] post + in + post :: posts ) + | None -> + (* no spec found for some reason (unknown function, ...) *) + L.d_printfln "No spec found for %a@\n" Typ.Procname.pp callee_pname ; + let event = ValueHistory.Call {f= `UnknownCall callee_pname; location= call_loc} in + Ok [havoc_id (fst ret) [event] astate] diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index 314de8787..6a7f44c18 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -99,3 +99,14 @@ val check_address_escape : -> PulseDomain.ValueHistory.t -> t -> t access_result + +val call : + caller_summary:Summary.t + -> Location.t + -> Typ.Procname.t + -> ret:Ident.t * Typ.t + -> actuals:((AbstractAddress.t * PulseDomain.ValueHistory.t) * Typ.t) list + -> t + -> t list access_result +(** perform an interprocedural call: apply the summary for the call proc name passed as argument if + it exists *) diff --git a/infer/src/pulse/PulsePayload.ml b/infer/src/pulse/PulsePayload.ml new file mode 100644 index 000000000..241ec9aa0 --- /dev/null +++ b/infer/src/pulse/PulsePayload.ml @@ -0,0 +1,14 @@ +(* + * 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. + *) + +open! IStd + +include SummaryPayload.Make (struct + type nonrec t = PulseSummary.t + + let field = Payloads.Fields.pulse +end) diff --git a/infer/src/pulse/PulsePayload.mli b/infer/src/pulse/PulsePayload.mli new file mode 100644 index 000000000..fb002744f --- /dev/null +++ b/infer/src/pulse/PulsePayload.mli @@ -0,0 +1,10 @@ +(* + * 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. + *) + +open! IStd + +include SummaryPayload.S with type t = PulseSummary.t diff --git a/infer/tests/codetoanalyze/cpp/pulse/closures.cpp b/infer/tests/codetoanalyze/cpp/pulse/closures.cpp index 6265d52d3..367d5e8ee 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/closures.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/closures.cpp @@ -156,3 +156,16 @@ void capture_multiple_vars_by_value_ok(C c, C c2) { return d; }; } + +void call_lambda_ok() { + auto f = [](S* s) { int x = s->f; }; + S* s = new S(); + f(s); +} + +void call_lambda_bad() { + auto f = [](S* s) { int x = s->f; }; + S* s = new S(); + delete s; + f(s); +} diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 65a32c9e3..dc866975e 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -2,6 +2,7 @@ codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AF 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 here] codetoanalyze/cpp/pulse/closures.cpp, FP_implicit_value_capture_destroy_invoke_ok, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable declared,memory is the address of a stack variable `s` whose lifetime has ended here,use-after-lifetime part of the trace starts here,value captured as `&s`,invalid access occurs here here] codetoanalyze/cpp/pulse/closures.cpp, FP_value_capture_destroy_invoke_ok, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable declared,memory is the address of a stack variable `s` whose lifetime has ended here,use-after-lifetime part of the trace starts here,value captured as `&s`,invalid access occurs here 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 `operator()` here,invalid access occurs here here] codetoanalyze/cpp/pulse/closures.cpp, implicit_ref_capture_destroy_invoke_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable declared,memory is the address of a stack variable `s` whose lifetime has ended here,use-after-lifetime part of the trace starts here,variable declared,value captured as `&s`,invalid access occurs here here] codetoanalyze/cpp/pulse/closures.cpp, ref_capture_destroy_invoke_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable declared,memory is the address of a stack variable `s` whose lifetime has ended here,use-after-lifetime part of the trace starts here,variable declared,value captured as `&s`,invalid access occurs here here] codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::SomeTemplatedClass::lifetime_error_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `templated_wrapper_delete_ok` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,when calling `templated_wrapper_access_ok` here,invalid access occurs here here]