[cpp] Improve creating of fake captured edges for Cpp lambdas

Reviewed By: skcho

Differential Revision: D49186797

fbshipit-source-id: 1fd34a6101849de1ffae1210cb7f06db8f070e0f

infer/src/pulse/PulseOperations.ml

@@ -159,12 +159,46 @@ let eval_var path location pvar astate =
 
 let eval_ident id astate = Stack.eval ValueHistory.epoch (Var.of_id id) astate
 
+let write_access path location addr_trace_ref access addr_trace_obj astate =
+  check_addr_access path Write location addr_trace_ref astate
+  >>| Memory.add_edge path addr_trace_ref access addr_trace_obj location
+
+
+let write_deref path location ~ref:addr_trace_ref ~obj:addr_trace_obj astate =
+  write_access path location addr_trace_ref Dereference addr_trace_obj astate
+
+
 let rec eval (path : PathContext.t) mode location exp astate :
     (t * (AbstractValue.t * ValueHistory.t)) PulseOperationResult.t =
   let++ astate, value_origin = eval_to_value_origin path mode location exp astate in
   (astate, ValueOrigin.addr_hist value_origin)
 
 
+and record_closure_cpp_lambda astate (path : PathContext.t) loc procname
+    (captured_vars : (Exp.t * Pvar.t * Typ.t * CapturedVar.capture_mode) list) =
+  let assign_event = ValueHistory.Assignment (loc, path.timestamp) in
+  let closure_addr_hist = (AbstractValue.mk_fresh (), ValueHistory.singleton assign_event) in
+  let astate =
+    AddressAttributes.add_one (fst closure_addr_hist) (Attribute.Closure procname) astate
+  in
+  let** astate = PulseArithmetic.and_positive (fst closure_addr_hist) astate in
+  let store_captured_var result (exp, var, _typ, mode) =
+    let field_name = Fieldname.mk_capture_field_in_cpp_lambda (Pvar.get_name var) mode in
+    let** astate = result in
+    let** astate, rhs_value_origin = eval_to_value_origin path NoAccess loc exp astate in
+    let rhs_addr, rhs_history = ValueOrigin.addr_hist rhs_value_origin in
+    let astate = conservatively_initialize_args [rhs_addr] astate in
+    L.d_printfln "Storing %a.%a = %a" AbstractValue.pp (fst closure_addr_hist) Fieldname.pp
+      field_name AbstractValue.pp rhs_addr ;
+    let=+ astate, lhs_addr_hist =
+      eval_access path Read loc closure_addr_hist (FieldAccess field_name) astate
+    in
+    write_deref path loc ~ref:lhs_addr_hist ~obj:(rhs_addr, rhs_history) astate
+  in
+  let++ astate = List.fold captured_vars ~init:(Sat (Ok astate)) ~f:store_captured_var in
+  (astate, ValueOrigin.Unknown closure_addr_hist)
+
+
 and eval_to_value_origin (path : PathContext.t) mode location exp astate :
     (t * ValueOrigin.t) PulseOperationResult.t =
   match (exp : Exp.t) with
@@ -186,21 +220,25 @@ and eval_to_value_origin (path : PathContext.t) mode location exp astate :
         (ArrayAccess (StdTyp.void, fst addr_hist_index))
         astate
   | Closure {name; captured_vars} ->
-      let** astate, rev_captured =
-        List.fold captured_vars
-          ~init:(Sat (Ok (astate, [])))
-          ~f:(fun result (capt_exp, captured_as, typ, mode) ->
-            let** astate, rev_captured = result in
-            let++ astate, addr_trace = eval path Read location capt_exp astate in
-            (astate, (captured_as, addr_trace, typ, mode) :: rev_captured) )
-      in
-      let++ astate, v_hist = Closures.record path location name (List.rev rev_captured) astate in
-      let astate =
-        conservatively_initialize_args
-          (List.rev_map rev_captured ~f:(fun (_, (addr, _), _, _) -> addr))
-          astate
-      in
-      (astate, ValueOrigin.Unknown v_hist)
+      if Procname.is_cpp_lambda name then
+        let++ astate, v_hist = record_closure_cpp_lambda astate path location name captured_vars in
+        (astate, v_hist)
+      else
+        let** astate, rev_captured =
+          List.fold captured_vars
+            ~init:(Sat (Ok (astate, [])))
+            ~f:(fun result (capt_exp, captured_as, typ, mode) ->
+              let** astate, rev_captured = result in
+              let++ astate, addr_trace = eval path Read location capt_exp astate in
+              (astate, (captured_as, addr_trace, typ, mode) :: rev_captured) )
+        in
+        let++ astate, v_hist = Closures.record path location name (List.rev rev_captured) astate in
+        let astate =
+          conservatively_initialize_args
+            (List.rev_map rev_captured ~f:(fun (_, (addr, _), _, _) -> addr))
+            astate
+        in
+        (astate, ValueOrigin.Unknown v_hist)
   | Const (Cfun proc_name) ->
       (* function pointers are represented as closures with no captured variables *)
       let++ astate, addr_hist = Closures.record path location proc_name [] astate in
@@ -340,15 +378,6 @@ let havoc_id id loc_opt astate =
   else astate
 
 
-let write_access path location addr_trace_ref access addr_trace_obj astate =
-  check_addr_access path Write location addr_trace_ref astate
-  >>| Memory.add_edge path addr_trace_ref access addr_trace_obj location
-
-
-let write_deref path location ~ref:addr_trace_ref ~obj:addr_trace_obj astate =
-  write_access path location addr_trace_ref Dereference addr_trace_obj astate
-
-
 let write_field path location ~ref:addr_trace_ref field ~obj:addr_trace_obj astate =
   write_access path location addr_trace_ref (FieldAccess field) addr_trace_obj astate
 
@@ -783,7 +812,9 @@ let get_var_captured_actuals path location ~is_lambda ~captured_formals ~actual_
               else Fieldname.mk_capture_field_in_cpp_lambda var_name mode
             in
             let+ astate, captured_actual =
-              eval_access path Read location actual_closure (FieldAccess field_name) astate
+              if is_lambda then
+                eval_deref_access path Read location actual_closure (FieldAccess field_name) astate
+              else eval_access path Read location actual_closure (FieldAccess field_name) astate
             in
             (id + 1, astate, (captured_actual, typ) :: captured)
         | Var.LogicalVar _ ->

infer/tests/codetoanalyze/cpp/pulse/call_lambdas.cpp

@@ -84,7 +84,7 @@ int call_lambda_after_copy_test_bad() {
   }
 }
 
-int call_lambda_after_copy_test_good_FP() {
+int call_lambda_after_copy_test_good() {
   if (call_lambda_after_copy() == 143) {
     int* p = NULL;
     return *p;

infer/tests/codetoanalyze/cpp/pulse/closures.cpp

@@ -419,7 +419,7 @@ S* update_inside_lambda_as_argument(S* s) {
   return object;
 }
 
-int update_inside_lambda_as_argument_ok_FP(S* param_s) {
+int update_inside_lambda_as_argument_ok(S* param_s) {
   return update_inside_lambda_as_argument(param_s)->f;
 }
 

infer/tests/codetoanalyze/cpp/pulse/issues.exp

@@ -19,11 +19,11 @@ codetoanalyze/cpp/pulse/basics.cpp, call_builtin_sub_overflow_bad, 5, NULLPTR_DE
 codetoanalyze/cpp/pulse/call_lambdas.cpp, call_lambda_through_function_test_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `call_lambda_through_function`,in call to `call_lambda<(lambda_at_call_lambdas.cpp:16:22)>`,in call to `lambda_call_lambdas.cpp:16_f4cfd8cf::operator()`,value captured by value as `c`,returned,return from call to `lambda_call_lambdas.cpp:16_f4cfd8cf::operator()`,returned,return from call to `call_lambda<(lambda_at_call_lambdas.cpp:16:22)>`,returned,return from call to `call_lambda_through_function`,taking "then" branch,is assigned to the null pointer,assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/call_lambdas.cpp, call_lambda_directly_test_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `call_lambda_directly`,in call to `lambda_call_lambdas.cpp:21_901326c8::operator()`,value captured by value as `c`,returned,return from call to `lambda_call_lambdas.cpp:21_901326c8::operator()`,returned,return from call to `call_lambda_directly`,taking "then" branch,is assigned to the null pointer,assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/call_lambdas.cpp, call_std_fun_constructor_test_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `call_std_fun_constructor`,in call to `lambda_call_lambdas.cpp:54_bd5fef1c::operator()`,value captured by value as `c`,returned,return from call to `lambda_call_lambdas.cpp:54_bd5fef1c::operator()`,returned,return from call to `call_std_fun_constructor`,taking "then" branch,is assigned to the null pointer,assigned,invalid access occurs here]
-codetoanalyze/cpp/pulse/call_lambdas.cpp, call_lambda_after_copy, 4, CONSTANT_ADDRESS_DEREFERENCE, no_bucket, WARNING, [is assigned to the constant 41,assigned,value captured by value as `c`,when calling `lambda_call_lambdas.cpp:75_9a48b9fa::lambda_(lambda_at_call_lambdas.cpp:75_ccd8a01d` here,parameter `__param_0` of lambda_call_lambdas.cpp:75_9a48b9fa::lambda_(lambda_at_call_lambdas.cpp:75_ccd8a01d,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 `s` declared here,is the address of a stack variable `s` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `s` declared here,value captured by ref as `s`,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 `s` declared here,is the address of a stack variable `s` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `s` declared here,value captured by ref 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 `s` declared here,is the address of a stack variable `s` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `s` declared here,value captured by ref as `s`,invalid access occurs here]
-codetoanalyze/cpp/pulse/closures.cpp, ref_capture_return_local_lambda_bad, 7, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [variable `x` declared here,value captured by ref as `x`,in call to `lambda_closures.cpp:129_1d2f7e92::operator()`,value captured by ref as `x`,returned,return from call to `lambda_closures.cpp:129_1d2f7e92::operator()`,returned here]
+codetoanalyze/cpp/pulse/call_lambdas.cpp, call_lambda_after_copy_test_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `call_lambda_after_copy`,in call to `lambda_call_lambdas.cpp:75_9a48b9fa::operator()`,value captured by ref as `d`,returned,return from call to `lambda_call_lambdas.cpp:75_9a48b9fa::operator()`,returned,return from call to `call_lambda_after_copy`,taking "then" branch,is assigned to the null pointer,assigned,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 `s` declared here,is the address of a stack variable `s` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `s` declared here,when calling `lambda_closures.cpp:20_0780ad07::operator()` here,value captured by ref as `s`,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 `s` declared here,is the address of a stack variable `s` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `s` declared here,when calling `lambda_closures.cpp:29_cd6cc34a::operator()` here,value captured by ref 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 `s` declared here,is the address of a stack variable `s` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `s` declared here,when calling `lambda_closures.cpp:41_8d512e76::operator()` here,value captured by ref as `s`,invalid access occurs here]
+codetoanalyze/cpp/pulse/closures.cpp, ref_capture_return_local_lambda_bad, 7, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [variable `x` declared here,in call to `lambda_closures.cpp:129_1d2f7e92::operator()`,value captured by ref as `x`,returned,return from call to `lambda_closures.cpp:129_1d2f7e92::operator()`,returned here]
 codetoanalyze/cpp/pulse/closures.cpp, call_lambda_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,allocated by call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,allocated by call to `new` (modelled),in call to `S::S`,parameter `this` of S::S,return from call to `S::S`,when calling `lambda_closures.cpp:164_d955040c::operator()` here,parameter `s` of lambda_closures.cpp:164_d955040c::operator(),invalid access occurs here]
 codetoanalyze/cpp/pulse/closures.cpp, call_lambda_std_fun_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,allocated by call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,allocated by call to `new` (modelled),in call to `S::S`,parameter `this` of S::S,return from call to `S::S`,when calling `lambda_closures.cpp:172_a042e7e3::operator()` here,parameter `s` of lambda_closures.cpp:172_a042e7e3::operator(),invalid access occurs here]
 codetoanalyze/cpp/pulse/closures.cpp, call_std_fun_constructor_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,allocated by call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,allocated by call to `new` (modelled),in call to `S::S`,parameter `this` of S::S,return from call to `S::S`,when calling `lambda_closures.cpp:179_5441e9d1::operator()` here,parameter `s` of lambda_closures.cpp:179_5441e9d1::operator(),invalid access occurs here]
@@ -37,7 +37,6 @@ codetoanalyze/cpp/pulse/closures.cpp, struct_capture_by_ref_bad, 7, NULLPTR_DERE
 codetoanalyze/cpp/pulse/closures.cpp, struct_capture_by_val_bad, 7, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/closures.cpp, struct_capture_by_val_ok_FP, 7, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/closures.cpp, call_argument, 0, PULSE_CONST_REFABLE, no_bucket, ERROR, [Parameter f with type `std::function<_fn_>`]
-codetoanalyze/cpp/pulse/closures.cpp, update_inside_lambda_as_argument_ok_FP, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `update_inside_lambda_as_argument`,is assigned to the null pointer,assigned,returned,return from call to `update_inside_lambda_as_argument`,invalid access occurs here]
 codetoanalyze/cpp/pulse/closures.cpp, FP_update_inside_lambda_visible_outside_ok, 10, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the constant 7,assigned,taking "then" branch,is assigned to the null pointer,assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/conditional_temporaries.cpp, condtemp::Counter::Counter, 1, PULSE_UNNECESSARY_COPY_INTERMEDIATE, no_bucket, ERROR, [copied here (with type `std::basic_string<char,std::char_traits<char>,std::allocator<char>>&`)]
 codetoanalyze/cpp/pulse/conditional_temporaries.cpp, condtemp::X::__infer_inner_destructor_~X, 1, NULLPTR_DEREFERENCE_LATENT, no_bucket, ERROR, [*** SUPPRESSED ***,source of the null value part of the trace starts here,is assigned to the null pointer,null pointer dereference part of the trace starts here,parameter `this` of condtemp::X::__infer_inner_destructor_~X,when calling `condtemp::X::name` here,parameter `this` of condtemp::X::name,invalid access occurs here]