From 14b9975cf3638e21aa863201dc9bf49ad3e53e55 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Mon, 15 Jul 2019 03:11:15 -0700 Subject: [PATCH] [pulse] support modelling destructors MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Summary: We want to detect that variables and C++ temporaries go out of scope even when their destructor happens to be modelled. We lost a test to that because `std::function::~function` was poorly modeled as deleting the lambda itself which would now cause a double invalidation. This has to be modelled better now as something that invalidates something *inside* the lambda, and also model `operator()` as something that accesses that something, to recover that test. It's not a vital test though, so Do It Later©. Reviewed By: ngorogiannis Differential Revision: D16121091 fbshipit-source-id: 6b777ca18 --- infer/src/pulse/Pulse.ml | 41 ++++++++++--------- infer/src/pulse/PulseModels.ml | 1 - .../codetoanalyze/cpp/pulse/closures.cpp | 3 +- .../tests/codetoanalyze/cpp/pulse/issues.exp | 3 +- 4 files changed, 24 insertions(+), 24 deletions(-) diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 6f923f1a4..2d01d2825 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -132,26 +132,27 @@ module PulseTransferFunctions = struct (* function pointer, etc.: skip for now *) None in - match model with - | Some model -> - L.d_printfln "Found model for call@\n" ; - 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" ())) ; - let posts = - interprocedural_call summary ret call_exp actuals_evaled flags call_loc astate - in - PerfEvent.(log (fun logger -> log_end_event logger ())) ; - match get_out_of_scope_object call_exp actuals flags with - | Some pvar_typ -> - L.d_printfln "%a is going out of scope" Pvar.pp_value (fst pvar_typ) ; - posts - >>= fun posts -> - List.map posts ~f:(fun astate -> exec_object_out_of_scope call_loc pvar_typ astate) - |> Result.all - | None -> - posts ) + (* do interprocedural call then destroy objects going out of scope *) + let posts = + match model with + | Some model -> + L.d_printfln "Found model for call@\n" ; + model ~caller_summary:summary call_loc ~ret ~actuals:actuals_evaled astate + | None -> + PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse interproc call" ())) ; + let r = interprocedural_call summary ret call_exp actuals_evaled flags call_loc astate in + PerfEvent.(log (fun logger -> log_end_event logger ())) ; + r + in + match get_out_of_scope_object call_exp actuals flags with + | Some pvar_typ -> + L.d_printfln "%a is going out of scope" Pvar.pp_value (fst pvar_typ) ; + posts + >>= fun posts -> + List.map posts ~f:(fun astate -> exec_object_out_of_scope call_loc pvar_typ astate) + |> Result.all + | None -> + posts let exec_instr (astate : Domain.t) {ProcData.summary} _cfg_node (instr : Sil.instr) = diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 0f4fa6a67..3ea4b90bd 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -194,7 +194,6 @@ module ProcNameDispatcher = struct [ -"folly" &:: "DelayedDestruction" &:: "destroy" &--> Misc.skip ; -"folly" &:: "Optional" &:: "reset" &--> Misc.skip ; -"folly" &:: "SocketAddress" &:: "~SocketAddress" &--> Misc.skip - ; -"std" &:: "function" &:: "~function" &--> Cplusplus.delete ; -"std" &:: "function" &:: "operator()" &--> StdFunction.operator_call ; -"std" &:: "function" &:: "operator=" &--> Misc.shallow_copy "std::function::operator=" ; -"std" &:: "vector" &:: "assign" &--> StdVector.invalidate_references Assign diff --git a/infer/tests/codetoanalyze/cpp/pulse/closures.cpp b/infer/tests/codetoanalyze/cpp/pulse/closures.cpp index c94362634..93f93a146 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/closures.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/closures.cpp @@ -95,7 +95,8 @@ std::function ref_capture_read_lambda_ok() { f; // reading (but not invoking) the lambda doesn't use its captured vars } -int delete_lambda_then_call_bad() { +// explicit destructor call is not modelled +int FN_delete_lambda_then_call_bad() { std::function lambda = [] { return 1; }; lambda.~function(); return lambda(); diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 7665340f4..2e3e49582 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -1,7 +1,6 @@ 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:162:12::operator()()` here,invalid access occurs here] -codetoanalyze/cpp/pulse/closures.cpp, delete_lambda_then_call_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,variable declared,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,variable declared,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] 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] codetoanalyze/cpp/pulse/closures.cpp, reassign_lambda_capture_destroy_invoke_bad, 9, 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] 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]