[pulse] model lambda captures

Summary:
When a lambda gets created, record the abstract addresses it captures, then
complain if we see some of them be invalidated before it is called.

Add a notion of "allocator" for reporting better messages. The messages are
still a bit sucky, will need to improve them more generally at some point.

```
 jul   lambda  ~  infer  1  infer -g --pulse-only -- clang -std=c++11 -c infer/tests/codetoanalyze/cpp/pulse/closures.cpp
Logs in /home/jul/infer.fb/infer-out/logs
Capturing in make/cc mode...
Found 1 source file to analyze in /home/jul/infer.fb/infer-out

Found 2 issues

infer/tests/codetoanalyze/cpp/pulse/closures.cpp:21: error: USE_AFTER_DESTRUCTOR
  `&(f)` accesses address `s` captured by `&(f)` as `s` invalidated by destructor call `S_~S(s)` at line 20, column 3 past its lifetime (debug: 5).
  19.       f = [&s] { return s.f; };
  20.     } // destructor for s called here
  21. >   return f(); // s used here
  22.   }
  23.

infer/tests/codetoanalyze/cpp/pulse/closures.cpp:30: error: USE_AFTER_DESTRUCTOR
  `&(f)` accesses address `s` captured by `&(f)` as `s` invalidated by destructor call `S_~S(s)` at line 29, column 3 past its lifetime (debug: 8).
  28.       f = [&] { return s.f; };
  29.     }
  30. >   return f();
  31.   }
  32.

Summary of the reports

  USE_AFTER_DESTRUCTOR: 2
```

Reviewed By: da319

Differential Revision: D13400074

fbshipit-source-id: 3c68ff4ea

infer/src/checkers/Pulse.ml

@@ -47,6 +47,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     | AccessExpression rhs_access ->
         PulseDomain.read loc rhs_access astate
         >>= fun (astate, rhs_value) -> PulseDomain.write loc lhs_access rhs_value astate
+    | Closure (pname, captured) ->
+        PulseDomain.Closures.record loc lhs_access pname captured astate
     | Cast (_, e) ->
         exec_assign lhs_access e loc astate
     | _ ->

infer/src/checkers/PulseDomain.ml

@@ -52,11 +52,25 @@ module Attribute = struct
   (* OPTIM: [Invalid _] is first in the order to make queries about invalidation status more
        efficient (only need to look at the first element in the set of attributes to know if an
        address is invalid) *)
-  type t = Invalid of Invalidation.t | StdVectorReserve [@@deriving compare]
+  type t =
+    (* DO NOT MOVE, see toplevel comment *)
+    | Invalid of Invalidation.t
+    | Closure of
+        Typ.Procname.t
+        * (AccessPath.base * HilExp.AccessExpression.t * AbstractAddressSet.t) list
+        * Location.t
+    | StdVectorReserve
+  [@@deriving compare]
 
   let pp f = function
     | Invalid invalidation ->
         Invalidation.pp f invalidation
+    | Closure (pname, captured, location) ->
+        F.fprintf f "%a[%a] (%a)" Typ.Procname.pp pname
+          (Pp.seq ~sep:","
+             (Pp.triple ~fst:AccessPath.pp_base ~snd:HilExp.AccessExpression.pp
+                ~trd:AbstractAddressSet.pp))
+          captured Location.pp location
     | StdVectorReserve ->
         F.pp_print_string f "std::vector::reserve()"
 end
@@ -478,24 +492,51 @@ end
 
 type actor = {access_expr: HilExp.AccessExpression.t; location: Location.t} [@@deriving compare]
 
+type allocator =
+  | Unknown
+  | Closure of
+      { lambda: HilExp.AccessExpression.t  (** some way to refer to the closure *)
+      ; access_expr: HilExp.AccessExpression.t  (** the access expr that was captured *)
+      ; as_base: AccessPath.base  (** the variable it was captured as *)
+      ; location: Location.t }
+
+let pp_allocator f = function
+  | Unknown ->
+      ()
+  | Closure {lambda; access_expr; as_base} ->
+      F.fprintf f "`%a` captured by `%a` as `%a` " HilExp.AccessExpression.pp access_expr
+        HilExp.AccessExpression.pp lambda AccessPath.pp_base as_base
+
+
+let location_of_allocator = function Unknown -> None | Closure {location} -> Some location
+
 module Diagnostic = struct
   type t =
     | AccessToInvalidAddress of
-        { invalidated_by: Invalidation.t
+        { allocated_by: allocator
+        ; invalidated_by: Invalidation.t
         ; accessed_by: actor
         ; address: AbstractAddress.t }
 
   let get_location (AccessToInvalidAddress {accessed_by= {location}}) = location
 
-  let get_message (AccessToInvalidAddress {accessed_by; invalidated_by; address}) =
+  let get_message (AccessToInvalidAddress {allocated_by; accessed_by; invalidated_by; address}) =
     let pp_debug_address f =
       if Config.debug_mode then F.fprintf f " (debug: %a)" AbstractAddress.pp address
     in
-    F.asprintf "`%a` accesses address %a past its lifetime%t" HilExp.AccessExpression.pp
+    F.asprintf "`%a` accesses address %a%a past its lifetime%t" HilExp.AccessExpression.pp
-      accessed_by.access_expr Invalidation.pp invalidated_by pp_debug_address
+      accessed_by.access_expr pp_allocator allocated_by Invalidation.pp invalidated_by
+      pp_debug_address
 
 
-  let get_trace (AccessToInvalidAddress {accessed_by; invalidated_by}) =
+  let get_trace (AccessToInvalidAddress {allocated_by; accessed_by; invalidated_by}) =
+    let allocated_by_trace =
+      match location_of_allocator allocated_by with
+      | None ->
+          []
+      | Some location ->
+          [Errlog.make_trace_element 0 location (F.asprintf "%ahere" pp_allocator allocated_by) []]
+    in
     let invalidated_by_trace =
       Invalidation.get_location invalidated_by
       |> Option.map ~f:(fun location ->
@@ -504,7 +545,7 @@ module Diagnostic = struct
                [] )
       |> Option.to_list
     in
-    invalidated_by_trace
+    allocated_by_trace @ invalidated_by_trace
     @ [ Errlog.make_trace_element 0 accessed_by.location
           (F.asprintf "accessed `%a` here" HilExp.AccessExpression.pp accessed_by.access_expr)
           [] ]
@@ -521,17 +562,19 @@ module Operations = struct
   open Result.Monad_infix
 
   (** Check that the address is not known to be invalid *)
-  let check_addr_access actor address astate =
+  let check_addr_access ?(allocated_by = Unknown) actor address astate =
     match Memory.get_invalidation address astate.heap with
     | Some invalidated_by ->
-        Error (Diagnostic.AccessToInvalidAddress {invalidated_by; accessed_by= actor; address})
+        Error
+          (Diagnostic.AccessToInvalidAddress
+             {invalidated_by; accessed_by= actor; address; allocated_by})
     | None ->
         Ok astate
 
 
-  let check_addr_access_set actor addresses astate =
+  let check_addr_access_set ?allocated_by actor addresses astate =
     AbstractAddressSet.fold
-      (fun addr result -> result >>= check_addr_access actor addr)
+      (fun addr result -> result >>= check_addr_access ?allocated_by actor addr)
       addresses (Ok astate)
 
 
@@ -670,6 +713,60 @@ module Operations = struct
     if phys_equal stack astate.stack then astate else {astate with stack}
 end
 
+module Closures = struct
+  open Result.Monad_infix
+
+  let check_captured_address location lambda address astate =
+    match Memory.find_opt address astate.heap with
+    | None ->
+        Ok astate
+    | Some (_, attributes) ->
+        IContainer.iter_result ~fold:(IContainer.fold_of_pervasives_fold ~fold:Attributes.fold)
+          attributes ~f:(function
+          | Attribute.Closure (_, captured, lambda_location) ->
+              IContainer.iter_result ~fold:List.fold captured
+                ~f:(fun (base, access_expr, addresses) ->
+                  Operations.check_addr_access_set
+                    ~allocated_by:
+                      (Closure {lambda; access_expr; as_base= base; location= lambda_location})
+                    {access_expr= lambda; location} addresses astate
+                  >>| fun _ -> () )
+          | _ ->
+              Ok () )
+        >>| fun () -> astate
+
+
+  let check_captured_addresses location lambda addresses astate =
+    Container.fold_result ~fold:(IContainer.fold_of_pervasives_fold ~fold:AbstractAddressSet.fold)
+      addresses ~init:astate ~f:(fun astate address ->
+        check_captured_address location lambda address astate )
+
+
+  let write location access_expr pname captured astate =
+    let closure_addr = AbstractAddress.mk_fresh () in
+    Operations.write location access_expr (AbstractAddressSet.singleton closure_addr) astate
+    >>| fun astate ->
+    { astate with
+      heap=
+        Memory.add_attributes closure_addr
+          (Attributes.singleton (Closure (pname, captured, location)))
+          astate.heap }
+
+
+  let record location access_expr pname captured astate =
+    List.fold_result captured ~init:(astate, [])
+      ~f:(fun ((astate, captured) as result) (captured_base, captured_exp) ->
+        match captured_exp with
+        | HilExp.AccessExpression (AddressOf access_expr) ->
+            Operations.read location access_expr astate
+            >>= fun (astate, addresses) ->
+            Ok (astate, (captured_base, access_expr, addresses) :: captured)
+        | _ ->
+            Ok result )
+    >>= fun (astate, captured_addresses) ->
+    write location access_expr pname captured_addresses astate
+end
+
 module StdVector = struct
   open Result.Monad_infix
 

infer/src/checkers/PulseDomain.mli

@@ -35,6 +35,21 @@ end
 
 type 'a access_result = ('a, Diagnostic.t) result
 
+module Closures : sig
+  val check_captured_addresses :
+    Location.t -> HilExp.AccessExpression.t -> AbstractAddressSet.t -> t -> t access_result
+  (** assert the validity of the addresses captured by the lambda *)
+
+  val record :
+       Location.t
+    -> HilExp.AccessExpression.t
+    -> Typ.Procname.t
+    -> (AccessPath.base * HilExp.t) list
+    -> t
+    -> t access_result
+  (** record that the access expression points to a lambda with its captured addresses *)
+end
+
 module StdVector : sig
   val is_reserved : Location.t -> HilExp.AccessExpression.t -> t -> (t * bool) access_result
 

infer/src/checkers/PulseModels.ml

@@ -57,6 +57,20 @@ module Cplusplus = struct
         Ok astate
 
 
+  let operator_call : model =
+   fun location ~ret:(ret_var, _) ~actuals astate ->
+    PulseDomain.read_all location (List.concat_map actuals ~f:HilExp.get_access_exprs) astate
+    >>= fun astate ->
+    ( match actuals with
+    | AccessExpression lambda :: _ ->
+        PulseDomain.read location HilExp.AccessExpression.(dereference (dereference lambda)) astate
+        >>= fun (astate, address) ->
+        PulseDomain.Closures.check_captured_addresses location lambda address astate
+    | _ ->
+        Ok astate )
+    >>| PulseDomain.havoc_var ret_var
+
+
   let placement_new : model =
    fun location ~ret:(ret_var, _) ~actuals astate ->
     let read_all args astate =
@@ -70,7 +84,7 @@ module Cplusplus = struct
     | _ :: other_actuals ->
         read_all other_actuals astate >>| PulseDomain.havoc_var ret_var
     | _ ->
-        Ok astate
+        Ok (PulseDomain.havoc_var ret_var astate)
 end
 
 module StdVector = struct
@@ -146,7 +160,8 @@ module ProcNameDispatcher = struct
   let dispatch : (unit, model) ProcnameDispatcher.ProcName.dispatcher =
     let open ProcnameDispatcher.ProcName in
     make_dispatcher
-      [ -"std" &:: "vector" &:: "assign" &--> StdVector.invalidate_references Assign
+      [ -"std" &:: "function" &:: "operator()" &--> Cplusplus.operator_call
+      ; -"std" &:: "vector" &:: "assign" &--> StdVector.invalidate_references Assign
       ; -"std" &:: "vector" &:: "clear" &--> StdVector.invalidate_references Clear
       ; -"std" &:: "vector" &:: "emplace" &--> StdVector.invalidate_references Emplace
       ; -"std" &:: "vector" &:: "emplace_back" &--> StdVector.invalidate_references EmplaceBack

infer/src/istd/IContainer.ml

@@ -72,3 +72,10 @@ let filter ~fold ~filter t ~init ~f =
 
 
 let map ~f:g fold t ~init ~f = fold t ~init ~f:(fun acc item -> f acc (g item))
+
+let fold_of_pervasives_fold ~fold collection ~init ~f =
+  fold (fun accum item -> f item accum) collection init
+
+
+let iter_result ~fold collection ~f =
+  Container.fold_result ~fold ~init:() ~f:(fun () item -> f item) collection

infer/src/istd/IContainer.mli

@@ -47,3 +47,9 @@ val filter :
   fold:('t, 'a, 'accum) Container.fold -> filter:('a -> bool) -> ('t, 'a, 'accum) Container.fold
 
 val map : f:('a -> 'b) -> ('t, 'a, 'accum) Container.fold -> ('t, 'b, 'accum) Container.fold
+
+val fold_of_pervasives_fold :
+  fold:(('a -> 'accum -> 'accum) -> 't -> 'accum -> 'accum) -> ('t, 'a, 'accum) Container.fold
+
+val iter_result :
+  fold:('t, 'a, unit) Container.fold -> 't -> f:('a -> (unit, 'err) result) -> (unit, 'err) result

infer/src/istd/Pp.ml

@@ -171,3 +171,5 @@ let cli_args fmt args =
 
 
 let pair ~fst ~snd fmt (a, b) = F.fprintf fmt "(%a,@,%a)" fst a snd b
+
+let triple ~fst ~snd ~trd fmt (a, b, c) = F.fprintf fmt "(%a,@,%a@,%a)" fst a snd b trd c

infer/src/istd/Pp.mli

@@ -100,3 +100,11 @@ val pair :
   -> F.formatter
   -> 'a * 'b
   -> unit
+
+val triple :
+     fst:(F.formatter -> 'a -> unit)
+  -> snd:(F.formatter -> 'b -> unit)
+  -> trd:(F.formatter -> 'c -> unit)
+  -> F.formatter
+  -> 'a * 'b * 'c
+  -> unit

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

@@ -12,7 +12,7 @@ struct S {
   S() { f = 1; }
 };
 
-int FN_ref_capture_destroy_invoke_bad() {
+int ref_capture_destroy_invoke_bad() {
   std::function<int()> f;
   {
     S s;
@@ -21,7 +21,7 @@ int FN_ref_capture_destroy_invoke_bad() {
   return f(); // s used here
 }
 
-int FN_implicit_ref_capture_destroy_invoke_bad() {
+int implicit_ref_capture_destroy_invoke_bad() {
   std::function<int()> f;
   {
     auto s = S();
@@ -30,10 +30,12 @@ int FN_implicit_ref_capture_destroy_invoke_bad() {
   return f();
 }
 
+// need to understand copy constructor
 int FN_reassign_lambda_capture_destroy_invoke_bad() {
   std::function<int()> f;
   {
     auto s = S();
+    // this is a copy constructor
     auto tmp = [&] { return s.f; };
     f = tmp;
   }

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

@@ -1,5 +1,7 @@
 codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 58, column 5 here,accessed `*(ptr)` here]
 codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 68, column 7 here,accessed `ptr` here]
+codetoanalyze/cpp/pulse/closures.cpp, implicit_ref_capture_destroy_invoke_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [`s` captured by `&(f)` as `s` here,invalidated by destructor call `S_~S(s)` at line 29, column 3 here,accessed `&(f)` here]
+codetoanalyze/cpp/pulse/closures.cpp, ref_capture_destroy_invoke_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [`s` captured by `&(f)` as `s` here,invalidated by destructor call `S_~S(s)` at line 20, column 3 here,accessed `&(f)` here]
 codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 12, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete result` at line 25, column 5 here,accessed `*(result)` here]
 codetoanalyze/cpp/pulse/returns.cpp, returns::return_deleted_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete x` at line 112, column 3 here,accessed `x` here]
 codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_branch_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 57, column 5 here,accessed `s` here]