From 91a2e2986b5235bc6d1fd3e88417703d3fd8bf15 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Thu, 27 Jun 2019 12:19:26 -0700 Subject: [PATCH] [pulse] model lambda capture by value Summary: Prevent false positives about variables captured by value gone out of scope. Reviewed By: ezgicicek Differential Revision: D16008165 fbshipit-source-id: d70e47db4 --- infer/src/pulse/PulseOperations.ml | 18 ++++++++++++++---- .../tests/codetoanalyze/cpp/pulse/closures.cpp | 7 ++----- infer/tests/codetoanalyze/cpp/pulse/issues.exp | 2 -- 3 files changed, 16 insertions(+), 11 deletions(-) diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index b7e272a64..d5856a95c 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -84,9 +84,14 @@ module Closures = struct let record location pname captured astate = let captured_addresses = - List.rev_map captured ~f:(fun (captured_as, (address_captured, trace_captured)) -> - let new_trace = ValueHistory.Capture {captured_as; location} :: trace_captured in - (address_captured, new_trace) ) + List.rev_filter_map captured + ~f:(fun (captured_as, (address_captured, trace_captured), mode) -> + match mode with + | `ByValue -> + None + | `ByReference -> + let new_trace = ValueHistory.Capture {captured_as; location} :: trace_captured in + Some (address_captured, new_trace) ) in let closure_addr = AbstractAddress.mk_fresh () in let fake_capture_edges = mk_capture_edges captured_addresses in @@ -133,7 +138,12 @@ let eval location exp0 astate = List.fold_result captured_vars ~init:(astate, []) ~f:(fun (astate, rev_captured) (capt_exp, captured_as, _) -> eval capt_exp astate - >>| fun (astate, addr_trace) -> (astate, (captured_as, addr_trace) :: rev_captured) ) + >>| fun (astate, addr_trace) -> + let mode = + (* HACK: the frontend follows this discipline *) + match (capt_exp : Exp.t) with Lvar _ -> `ByReference | _ -> `ByValue + in + (astate, (captured_as, addr_trace, mode) :: rev_captured) ) >>| fun (astate, rev_captured) -> Closures.record location name (List.rev rev_captured) astate | Cast (_, exp') -> diff --git a/infer/tests/codetoanalyze/cpp/pulse/closures.cpp b/infer/tests/codetoanalyze/cpp/pulse/closures.cpp index 367d5e8ee..017393728 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/closures.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/closures.cpp @@ -42,9 +42,7 @@ int FN_reassign_lambda_capture_destroy_invoke_bad() { return f(); } -// frontend doesn't understand difference between capture-by-value and -// capture-by-ref, need to fix -int FP_value_capture_destroy_invoke_ok() { +int value_capture_destroy_invoke_ok() { std::function f; { S s; @@ -53,8 +51,7 @@ int FP_value_capture_destroy_invoke_ok() { return f(); } -// same thing here -int FP_implicit_value_capture_destroy_invoke_ok() { +int implicit_value_capture_destroy_invoke_ok() { std::function f; { S s; diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index dc866975e..7e6dcff57 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -1,7 +1,5 @@ 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 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 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]