[pulse] Understand captured variables in cpp lambdas

Summary: When we evaluate lambdas in pulse, we create a closure object with `fake` fields to store captured variables. However, during the function call we were not linking the captured values from the closure object. We address this missing part here.

Reviewed By: jvillard

Differential Revision: D23316750

fbshipit-source-id: 14751aa58

infer/src/pulse/PulseAbductiveDomain.ml

@@ -302,23 +302,29 @@ end
 let mk_initial proc_desc =
   (* HACK: save the formals in the stacks of the pre and the post to remember which local variables
      correspond to formals *)
-  let formals =
+  let formals_and_captured =
     let proc_name = Procdesc.get_proc_name proc_desc in
     let location = Procdesc.get_loc proc_desc in
-    Procdesc.get_formals proc_desc
-    |> List.map ~f:(fun (mangled, _) ->
-           let pvar = Pvar.mk mangled proc_name in
-           ( Var.of_pvar pvar
-           , (AbstractValue.mk_fresh (), [ValueHistory.FormalDeclared (pvar, location)]) ) )
+    let init_var mangled =
+      let pvar = Pvar.mk mangled proc_name in
+      (Var.of_pvar pvar, (AbstractValue.mk_fresh (), [ValueHistory.FormalDeclared (pvar, location)]))
+    in
+    let formals =
+      Procdesc.get_formals proc_desc |> List.map ~f:(fun (mangled, _) -> init_var mangled)
+    in
+    let captured =
+      Procdesc.get_captured proc_desc |> List.map ~f:(fun (mangled, _, _) -> init_var mangled)
+    in
+    captured @ formals
   in
   let initial_stack =
-    List.fold formals ~init:(PreDomain.empty :> BaseDomain.t).stack
+    List.fold formals_and_captured ~init:(PreDomain.empty :> BaseDomain.t).stack
       ~f:(fun stack (formal, addr_loc) -> BaseStack.add formal addr_loc stack)
   in
   let pre =
     let initial_heap =
-      List.fold formals ~init:(PreDomain.empty :> base_domain).heap ~f:(fun heap (_, (addr, _)) ->
-          BaseMemory.register_address addr heap )
+      List.fold formals_and_captured ~init:(PreDomain.empty :> base_domain).heap
+        ~f:(fun heap (_, (addr, _)) -> BaseMemory.register_address addr heap)
     in
     PreDomain.update ~stack:initial_stack ~heap:initial_heap PreDomain.empty
   in

infer/src/pulse/PulseInterproc.ml

@@ -167,6 +167,15 @@ let is_cell_read_only ~edges_pre_opt ~cell_post:(_, attrs_post) =
   match edges_pre_opt with None -> false | Some _ -> not (Attributes.is_modified attrs_post)
 
 
+let materialize_pre_for_captured_vars callee_proc_name call_location pre_post
+    ~captured_vars_with_actuals call_state =
+  List.fold_result captured_vars_with_actuals ~init:call_state
+    ~f:(fun call_state (formal, actual) ->
+      materialize_pre_from_actual callee_proc_name call_location
+        ~pre:(pre_post.AbductiveDomain.pre :> BaseDomain.t)
+        ~formal ~actual call_state )
+
+
 let materialize_pre_for_parameters callee_proc_name call_location pre_post ~formals ~actuals
     call_state =
   (* For each [(formal, actual)] pair, resolve them to addresses in their respective states then
@@ -245,13 +254,16 @@ let apply_arithmetic_constraints callee_proc_name call_location pre_post call_st
     call_state.subst call_state
 
 
-let materialize_pre callee_proc_name call_location pre_post ~formals ~actuals call_state =
+let materialize_pre callee_proc_name call_location pre_post ~captured_vars_with_actuals ~formals
+    ~actuals call_state =
   PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse call pre" ())) ;
   let r =
     let open IResult.Let_syntax in
     (* first make as large a mapping as we can between callee values and caller values... *)
     materialize_pre_for_parameters callee_proc_name call_location pre_post ~formals ~actuals
       call_state
+    >>= materialize_pre_for_captured_vars callee_proc_name call_location pre_post
+          ~captured_vars_with_actuals
     >>= materialize_pre_for_globals callee_proc_name call_location pre_post
     >>| (* ...then relational arithmetic constraints in the callee's attributes will make sense in
            terms of the caller's values *)
@@ -417,6 +429,12 @@ let apply_post_for_parameters callee_proc_name call_location pre_post ~formals ~
       call_state
 
 
+let apply_post_for_captured_vars callee_proc_name call_location pre_post ~captured_vars_with_actuals
+    call_state =
+  List.fold captured_vars_with_actuals ~init:call_state ~f:(fun call_state (formal, actual) ->
+      record_post_for_actual callee_proc_name call_location pre_post ~formal ~actual call_state )
+
+
 let apply_post_for_globals callee_proc_name call_location pre_post call_state =
   match
     fold_globals_of_stack call_location (pre_post.AbductiveDomain.pre :> BaseDomain.t).stack
@@ -457,10 +475,13 @@ let record_skipped_calls callee_proc_name call_loc pre_post call_state =
   {call_state with astate}
 
 
-let apply_post callee_proc_name call_location pre_post ~formals ~actuals call_state =
+let apply_post callee_proc_name call_location pre_post ~captured_vars_with_actuals ~formals ~actuals
+    call_state =
   PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse call post" ())) ;
   let r =
     apply_post_for_parameters callee_proc_name call_location pre_post ~formals ~actuals call_state
+    |> apply_post_for_captured_vars callee_proc_name call_location pre_post
+         ~captured_vars_with_actuals
     |> apply_post_for_globals callee_proc_name call_location pre_post
     |> record_post_for_return callee_proc_name call_location pre_post
     |> fun (call_state, return_caller) ->
@@ -514,7 +535,8 @@ let check_all_valid callee_proc_name call_location {AbductiveDomain.pre; _} call
    the noise that this will introduce since we don't care about values. For instance, if the pre
    is for a path where [formal != 0] and we pass [0] then it will be an FP. Maybe the solution is
    to bake in some value analysis. *)
-let apply_prepost callee_proc_name call_location ~callee_prepost:pre_post ~formals ~actuals astate =
+let apply_prepost callee_proc_name call_location ~callee_prepost:pre_post
+    ~captured_vars_with_actuals ~formals ~actuals astate =
   L.d_printfln "Applying pre/post for %a(%a):@\n%a" Procname.pp callee_proc_name
     (Pp.seq ~sep:"," Var.pp) formals pp pre_post ;
   let empty_call_state =
@@ -522,7 +544,8 @@ let apply_prepost callee_proc_name call_location ~callee_prepost:pre_post ~forma
   in
   (* read the precondition *)
   match
-    materialize_pre callee_proc_name call_location pre_post ~formals ~actuals empty_call_state
+    materialize_pre callee_proc_name call_location pre_post ~captured_vars_with_actuals ~formals
+      ~actuals empty_call_state
   with
   | exception Contradiction reason ->
       (* can't make sense of the pre-condition in the current context: give up on that particular
@@ -540,7 +563,8 @@ let apply_prepost callee_proc_name call_location ~callee_prepost:pre_post ~forma
         (* reset [visited] *)
         let call_state = {call_state with astate; visited= AddressSet.empty} in
         (* apply the postcondition *)
-        apply_post callee_proc_name call_location pre_post ~formals ~actuals call_state
+        apply_post callee_proc_name call_location pre_post ~captured_vars_with_actuals ~formals
+          ~actuals call_state
       with
       | Ok post ->
           Ok (Some post)

infer/src/pulse/PulseInterproc.mli

@@ -12,6 +12,7 @@ val apply_prepost :
      Procname.t
   -> Location.t
   -> callee_prepost:PulseAbductiveDomain.t
+  -> captured_vars_with_actuals:(Var.t * (AbstractValue.t * ValueHistory.t)) list
   -> formals:Var.t list
   -> actuals:((AbstractValue.t * ValueHistory.t) * Typ.t) list
   -> PulseAbductiveDomain.t

infer/src/pulse/PulseOperations.ml

@@ -69,14 +69,9 @@ module Closures = struct
 
   let record location pname captured astate =
     let captured_addresses =
-      List.rev_filter_map captured
-        ~f:(fun (captured_as, (address_captured, trace_captured), mode) ->
-          match mode with
-          | Pvar.ByValue ->
-              None
-          | Pvar.ByReference ->
-              let new_trace = ValueHistory.Capture {captured_as; location} :: trace_captured in
-              Some (address_captured, new_trace) )
+      List.filter_map captured ~f:(fun (captured_as, (address_captured, trace_captured), mode) ->
+          let new_trace = ValueHistory.Capture {captured_as; mode; location} :: trace_captured in
+          Some (address_captured, new_trace) )
     in
     let closure_addr_hist = (AbstractValue.mk_fresh (), [ValueHistory.Assignment location]) in
     let fake_capture_edges = mk_capture_edges captured_addresses in
@@ -440,9 +435,11 @@ let unknown_call call_loc reason ~ret ~actuals ~formals_opt astate =
   |> havoc_ret ret |> add_skipped_proc
 
 
-let apply_callee callee_pname call_loc callee_exec_state ~ret ~formals ~actuals astate =
+let apply_callee callee_pname call_loc callee_exec_state ~ret ~captured_vars_with_actuals ~formals
+    ~actuals astate =
   let apply callee_prepost ~f =
-    PulseInterproc.apply_prepost callee_pname call_loc ~callee_prepost ~formals ~actuals astate
+    PulseInterproc.apply_prepost callee_pname call_loc ~callee_prepost ~captured_vars_with_actuals
+      ~formals ~actuals astate
     >>| function
     | None ->
         (* couldn't apply pre/post pair *) None
@@ -468,6 +465,26 @@ let apply_callee callee_pname call_loc callee_exec_state ~ret ~formals ~actuals
       apply astate ~f:(fun astate -> ExitProgram astate)
 
 
+let get_captured_actuals location ~captured_vars ~actual_closure astate =
+  let* astate, this_value_addr = eval_access location actual_closure Dereference astate in
+  let+ _, astate, captured_vars_with_actuals =
+    List.fold_result captured_vars ~init:(0, astate, [])
+      ~f:(fun (id, astate, captured) (var, mode) ->
+        let* astate, field =
+          eval_access location this_value_addr (FieldAccess (Closures.mk_fake_field ~id)) astate
+        in
+        let+ astate, captured_actual =
+          match mode with
+          | Pvar.ByReference ->
+              eval_access location field Dereference astate
+          | Pvar.ByValue ->
+              Ok (astate, field)
+        in
+        (id + 1, astate, (var, captured_actual) :: captured) )
+  in
+  (astate, captured_vars_with_actuals)
+
+
 let call ~callee_data call_loc callee_pname ~ret ~actuals ~formals_opt (astate : AbductiveDomain.t)
     : (ExecutionDomain.t list, Diagnostic.t * t) result =
   match callee_data with
@@ -476,6 +493,21 @@ let call ~callee_data call_loc callee_pname ~ret ~actuals ~formals_opt (astate :
         Procdesc.get_formals callee_proc_desc
         |> List.map ~f:(fun (mangled, _) -> Pvar.mk mangled callee_pname |> Var.of_pvar)
       in
+      let captured_vars =
+        Procdesc.get_captured callee_proc_desc
+        |> List.map ~f:(fun (mangled, _, mode) ->
+               let pvar = Pvar.mk mangled callee_pname in
+               (Var.of_pvar pvar, mode) )
+      in
+      let* astate, captured_vars_with_actuals =
+        match actuals with
+        | (actual_closure, _) :: _
+          when not (Procname.is_objc_block callee_pname || List.is_empty captured_vars) ->
+            (* Assumption: the first parameter will be a closure *)
+            get_captured_actuals call_loc ~captured_vars ~actual_closure astate
+        | _ ->
+            Ok (astate, [])
+      in
       let is_blacklist =
         Option.exists Config.pulse_cut_to_one_path_procedures_pattern ~f:(fun regex ->
             Str.string_match regex (Procname.to_string callee_pname) 0 )
@@ -485,7 +517,8 @@ let call ~callee_data call_loc callee_pname ~ret ~actuals ~formals_opt (astate :
         ~f:(fun posts callee_exec_state ->
           (* apply all pre/post specs *)
           match
-            apply_callee callee_pname call_loc callee_exec_state ~formals ~actuals ~ret astate
+            apply_callee callee_pname call_loc callee_exec_state ~captured_vars_with_actuals
+              ~formals ~actuals ~ret astate
           with
           | Ok None ->
               (* couldn't apply pre/post pair *)

infer/src/pulse/PulseValueHistory.ml

@@ -12,7 +12,7 @@ type event =
   | Allocation of {f: CallEvent.t; location: Location.t}
   | Assignment of Location.t
   | Call of {f: CallEvent.t; location: Location.t; in_call: t}
-  | Capture of {captured_as: Pvar.t; location: Location.t}
+  | Capture of {captured_as: Pvar.t; mode: Pvar.capture_mode; location: Location.t}
   | Conditional of {is_then_branch: bool; if_kind: Sil.if_kind; location: Location.t}
   | CppTemporaryCreated of Location.t
   | FormalDeclared of Pvar.t * Location.t
@@ -33,8 +33,10 @@ let pp_event_no_location fmt event =
       F.fprintf fmt "passed as argument to %a" CallEvent.pp f
   | Allocation {f} ->
       F.fprintf fmt "allocated by call to %a" CallEvent.pp f
-  | Capture {captured_as; location= _} ->
-      F.fprintf fmt "value captured as `%a`" Pvar.pp_value_non_verbose captured_as
+  | Capture {captured_as; mode; location= _} ->
+      F.fprintf fmt "value captured by %s as `%a`"
+        (Pvar.string_of_capture_mode mode)
+        Pvar.pp_value_non_verbose captured_as
   | Conditional {is_then_branch; if_kind; location= _} ->
       F.fprintf fmt "expression in %s condition is %b" (Sil.if_kind_to_string if_kind)
         is_then_branch

infer/src/pulse/PulseValueHistory.mli

@@ -12,7 +12,7 @@ type event =
   | Allocation of {f: CallEvent.t; location: Location.t}
   | Assignment of Location.t
   | Call of {f: CallEvent.t; location: Location.t; in_call: t}
-  | Capture of {captured_as: Pvar.t; location: Location.t}
+  | Capture of {captured_as: Pvar.t; mode: Pvar.capture_mode; location: Location.t}
   | Conditional of {is_then_branch: bool; if_kind: Sil.if_kind; location: Location.t}
   | CppTemporaryCreated of Location.t
   | FormalDeclared of Pvar.t * Location.t

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

@@ -170,3 +170,84 @@ void function_assign_null_ok() {
   std::function<int()> f = [] { return 1; };
   f = nullptr;
 }
+
+void capture_by_value_ok() {
+  int value = 5;
+  auto f = [value]() -> int* { return new int(value); };
+  value++;
+  int* p = f();
+  int* q = nullptr;
+  if (*p != 5) {
+    *q = 42;
+  }
+}
+
+void capture_by_value_bad() {
+  int value = 5;
+  auto f = [value]() -> int* { return new int(value); };
+  value++;
+  int* p = f();
+  int* q = nullptr;
+  if (*p == 5) {
+    *q = 42;
+  }
+}
+
+void capture_by_ref_ok() {
+  int value = 5;
+  auto f = [&value]() -> int* { return new int(value); };
+  value++;
+  int* p = f();
+  int* q = nullptr;
+  if (*p != 6) {
+    *q = 42;
+  }
+}
+
+void capture_by_ref_bad() {
+  int value = 5;
+  auto f = [&value]() -> int* { return new int(value); };
+  value++;
+  int* p = f();
+  int* q = nullptr;
+  if (*p == 6) {
+    *q = 42;
+  }
+}
+
+S* update_inside_lambda_capture_and_init(S* s) {
+  S* object = nullptr;
+  auto f = [& o = object](S* s) { o = s; };
+  f(s);
+  return object;
+}
+
+int update_inside_lambda_capture_and_init_ok(S* param_s) {
+  return update_inside_lambda_capture_and_init(param_s)->f;
+}
+
+S* update_inside_lambda_capture_only(S* s) {
+  S* object = nullptr;
+  /* FIXME: clang AST gives us `S*` for  variable `object` in the
+     lambda's body, hence the translation misses one dereference */
+  auto f = [&object](S* s) { object = s; };
+  f(s);
+  return object;
+}
+
+int update_inside_lambda_capture_only_ok_FP(S* param_s) {
+  return update_inside_lambda_capture_only(param_s)->f;
+}
+
+void call_argument(std::function<void(S*)> f, S* s) { f(s); }
+
+S* update_inside_lambda_as_argument(S* s) {
+  S* object = nullptr;
+  auto f = [& o = object](S* s) { o = s; };
+  call_argument(f, s);
+  return object;
+}
+
+int update_inside_lambda_as_argument_ok_FP(S* param_s) {
+  return update_inside_lambda_as_argument(param_s)->f;
+}

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

@@ -7,9 +7,13 @@ codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AF
 codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_bad,invalid access occurs here]
 codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 8, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_bad,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,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,when calling `call_lambda_bad::lambda_closures.cpp:163:12::operator()` here,parameter `s` of call_lambda_bad::lambda_closures.cpp:163:12::operator(),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 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 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 `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 as `s`,invalid access occurs here]
+codetoanalyze/cpp/pulse/closures.cpp, capture_by_ref_bad, 7, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
+codetoanalyze/cpp/pulse/closures.cpp, capture_by_value_bad, 7, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,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 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 by ref 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 `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 by ref as `s`,invalid access occurs here]
+codetoanalyze/cpp/pulse/closures.cpp, update_inside_lambda_as_argument_ok_FP, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `update_inside_lambda_as_argument` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `update_inside_lambda_as_argument`,return from call to `update_inside_lambda_as_argument`,invalid access occurs here]
+codetoanalyze/cpp/pulse/closures.cpp, update_inside_lambda_capture_only_ok_FP, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `update_inside_lambda_capture_only` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `update_inside_lambda_capture_only`,return from call to `update_inside_lambda_capture_only`,invalid access occurs here]
 codetoanalyze/cpp/pulse/conditionals.cpp, add_test3_bad, 3, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of add_test3_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of add_test3_bad,invalid access occurs here]
 codetoanalyze/cpp/pulse/conditionals.cpp, add_test5_bad, 5, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of add_test5_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of add_test5_bad,invalid access occurs here]
 codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::SomeTemplatedClass<int*>::lifetime_error_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `a` of deduplication::SomeTemplatedClass<int*>::lifetime_error_bad,when calling `deduplication::SomeTemplatedClass<int*>::templated_wrapper_delete_ok` here,parameter `a` of deduplication::SomeTemplatedClass<int*>::templated_wrapper_delete_ok,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `a` of deduplication::SomeTemplatedClass<int*>::lifetime_error_bad,when calling `deduplication::SomeTemplatedClass<int*>::templated_wrapper_access_ok` here,parameter `a` of deduplication::SomeTemplatedClass<int*>::templated_wrapper_access_ok,invalid access occurs here]