[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

@@ -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)) ->
+      List.rev_filter_map captured
-          let new_trace = ValueHistory.Capture {captured_as; location} :: trace_captured in
+        ~f:(fun (captured_as, (address_captured, trace_captured), mode) ->
-          (address_captured, new_trace) )
+          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') ->

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
+int value_capture_destroy_invoke_ok() {
-// capture-by-ref, need to fix
-int FP_value_capture_destroy_invoke_ok() {
   std::function<int()> f;
   {
     S s;
@@ -53,8 +51,7 @@ int FP_value_capture_destroy_invoke_ok() {
   return f();
 }
 
-// same thing here
+int implicit_value_capture_destroy_invoke_ok() {
-int FP_implicit_value_capture_destroy_invoke_ok() {
   std::function<int()> f;
   {
     S s;

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]