[pulse] calling known lambdas calls the corresponding proc name

Summary: We know how to do interprocedural calls so let's use that!

Reviewed By: mbouaziz

Differential Revision: D16008164

fbshipit-source-id: 4c34bf704

infer/src/pulse/Pulse.ml

@@ -40,12 +40,6 @@ let check_error summary = function
       raise_notrace AbstractDomain.Stop_analysis
 
 
-module Payload = SummaryPayload.Make (struct
-  type t = PulseSummary.t
-
-  let field = Payloads.Fields.pulse
-end)
-
 let proc_name_of_call call_exp =
   match (call_exp : Exp.t) with
   | Const (Cfun proc_name) | Closure {name= proc_name} ->
@@ -86,39 +80,13 @@ module PulseTransferFunctions = struct
 
 
   let interprocedural_call caller_summary ret call_exp actuals flags call_loc astate =
-    let unknown_function reason =
-      exec_unknown_call reason ret call_exp actuals flags call_loc astate >>| List.return
-    in
     match proc_name_of_call call_exp with
-    | Some callee_pname -> (
-      match Payload.read_full caller_summary.Summary.proc_desc callee_pname with
-      | Some (callee_proc_desc, preposts) ->
-          let formals =
-            Procdesc.get_formals callee_proc_desc
-            |> List.map ~f:(fun (mangled, _) -> Pvar.mk mangled callee_pname |> Var.of_pvar)
-          in
-          (* call {!PulseAbductiveDomain.PrePost.apply} on each pre/post pair in the summary. *)
-          List.fold_result preposts ~init:[] ~f:(fun posts pre_post ->
-              (* apply all pre/post specs *)
-              PulseAbductiveDomain.PrePost.apply callee_pname call_loc pre_post ~formals ~actuals
-                astate
-              >>| fun (post, return_val_opt) ->
-              let event = ValueHistory.Call {f= `Call callee_pname; location= call_loc} in
-              let post =
-                match return_val_opt with
-                | Some return_val ->
-                    PulseOperations.write_id (fst ret) (return_val, [event]) post
-                | None ->
-                    PulseOperations.havoc_id (fst ret) [event] post
-              in
-              post :: posts )
-      | None ->
-          (* no spec found for some reason (unknown function, ...) *)
-          L.d_printfln "No spec found for %a@\n" Typ.Procname.pp callee_pname ;
-          unknown_function (`UnknownCall callee_pname) )
+    | Some callee_pname ->
+        PulseOperations.call ~caller_summary call_loc callee_pname ~ret ~actuals astate
     | None ->
         L.d_printfln "Indirect call %a@\n" Exp.pp call_exp ;
-        unknown_function (`IndirectCall call_exp)
+        exec_unknown_call (`IndirectCall call_exp) ret call_exp actuals flags call_loc astate
+        >>| List.return
 
 
   (** has an object just gone out of scope? *)
@@ -167,7 +135,7 @@ module PulseTransferFunctions = struct
     match model with
     | Some model ->
         L.d_printfln "Found model for call@\n" ;
-        model call_loc ~ret ~actuals:actuals_evaled astate
+        model ~caller_summary:summary call_loc ~ret ~actuals:actuals_evaled astate
     | None -> (
         (* do interprocedural call then destroy objects going out of scope *)
         PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse interproc call" ())) ;
@@ -254,7 +222,7 @@ let checker {Callbacks.proc_desc; tenv; summary} =
   in
   match DisjunctiveAnalyzer.compute_post proc_data ~initial with
   | Some posts ->
-      Payload.update_summary
+      PulsePayload.update_summary
         (PulseSummary.of_posts (DisjunctiveTransferFunctions.Disjuncts.elements posts))
         summary
   | None ->

infer/src/pulse/PulseAbductiveDomain.ml

@@ -204,6 +204,10 @@ module Memory = struct
     map_post_heap astate ~f:(fun heap -> BaseMemory.add_attributes address attributes heap)
 
 
+  let get_closure_proc_name addr astate =
+    BaseMemory.get_closure_proc_name addr (astate.post :> base_domain).heap
+
+
   let std_vector_reserve addr astate =
     map_post_heap astate ~f:(fun heap -> BaseMemory.std_vector_reserve addr heap)
 

infer/src/pulse/PulseAbductiveDomain.mli

@@ -65,6 +65,8 @@ module Memory : sig
     -> t
     -> t
 
+  val get_closure_proc_name : AbstractAddress.t -> t -> Typ.Procname.t option
+
   val is_std_vector_reserved : AbstractAddress.t -> t -> bool
 
   val std_vector_reserve : AbstractAddress.t -> t -> t

infer/src/pulse/PulseDomain.ml

@@ -248,6 +248,8 @@ module Attribute = struct
 
   let to_rank = Variants.to_rank
 
+  let closure_rank = Variants.to_rank (Closure (Typ.Procname.from_string_c_fun ""))
+
   let invalid_rank =
     Variants.to_rank
       (Invalid
@@ -293,6 +295,13 @@ module Attributes = struct
            action )
 
 
+  let get_closure_proc_name attrs =
+    Set.find_rank attrs Attribute.closure_rank
+    |> Option.map ~f:(fun attr ->
+           let[@warning "-8"] (Attribute.Closure proc_name) = attr in
+           proc_name )
+
+
   let is_std_vector_reserved attrs =
     Set.find_rank attrs Attribute.std_vector_reserve_rank |> Option.is_some
 
@@ -397,6 +406,8 @@ module Memory : sig
 
   val check_valid : AbstractAddress.t -> t -> (unit, Invalidation.t Trace.t) result
 
+  val get_closure_proc_name : AbstractAddress.t -> t -> Typ.Procname.t option
+
   val std_vector_reserve : AbstractAddress.t -> t -> t
 
   val is_std_vector_reserved : AbstractAddress.t -> t -> bool
@@ -471,6 +482,11 @@ end = struct
         Ok ()
 
 
+  let get_closure_proc_name address memory =
+    Graph.find_opt address (snd memory)
+    |> Option.bind ~f:(fun attributes -> Attributes.get_closure_proc_name attributes)
+
+
   let std_vector_reserve address memory = add_attribute address Attribute.StdVectorReserve memory
 
   let is_std_vector_reserved address memory =

infer/src/pulse/PulseDomain.mli

@@ -163,6 +163,8 @@ module Memory : sig
 
   val check_valid : AbstractAddress.t -> t -> (unit, Invalidation.t Trace.t) result
 
+  val get_closure_proc_name : AbstractAddress.t -> t -> Typ.Procname.t option
+
   val std_vector_reserve : AbstractAddress.t -> t -> t
 
   val is_std_vector_reserved : AbstractAddress.t -> t -> bool

infer/src/pulse/PulseModels.ml

@@ -8,7 +8,8 @@ open! IStd
 open Result.Monad_infix
 
 type exec_fun =
-     Location.t
+     caller_summary:Summary.t
+  -> Location.t
   -> ret:Ident.t * Typ.t
   -> actuals:(PulseDomain.AddrTracePair.t * Typ.t) list
   -> PulseAbductiveDomain.t
@@ -18,7 +19,7 @@ type model = exec_fun
 
 module Misc = struct
   let shallow_copy model_desc : model =
-   fun location ~ret:(ret_id, _) ~actuals astate ->
+   fun ~caller_summary:_ location ~ret:(ret_id, _) ~actuals astate ->
     let event = PulseDomain.ValueHistory.Call {f= `Model model_desc; location} in
     ( match actuals with
     | [(dest_pointer_hist, _); (src_pointer_hist, _)] ->
@@ -35,14 +36,14 @@ module Misc = struct
     >>| fun astate -> [PulseOperations.havoc_id ret_id [event] astate]
 
 
-  let early_exit : model = fun _ ~ret:_ ~actuals:_ _ -> Ok []
+  let early_exit : model = fun ~caller_summary:_ _ ~ret:_ ~actuals:_ _ -> Ok []
 
-  let skip : model = fun _ ~ret:_ ~actuals:_ astate -> Ok [astate]
+  let skip : model = fun ~caller_summary:_ _ ~ret:_ ~actuals:_ astate -> Ok [astate]
 end
 
 module C = struct
   let free : model =
-   fun location ~ret:_ ~actuals astate ->
+   fun ~caller_summary:_ location ~ret:_ ~actuals astate ->
     match actuals with
     | [(deleted_access, _)] ->
         PulseOperations.invalidate location
@@ -55,7 +56,7 @@ end
 
 module Cplusplus = struct
   let delete : model =
-   fun location ~ret:_ ~actuals astate ->
+   fun ~caller_summary:_ location ~ret:_ ~actuals astate ->
     match actuals with
     | [(deleted_access, _)] ->
         PulseOperations.invalidate location
@@ -67,7 +68,7 @@ module Cplusplus = struct
 
 
   let placement_new : model =
-   fun location ~ret:(ret_id, _) ~actuals astate ->
+   fun ~caller_summary:_ location ~ret:(ret_id, _) ~actuals astate ->
     let event = PulseDomain.ValueHistory.Call {f= `Model "<placement new>"; location} in
     match List.rev actuals with
     | ((address, _), _) :: _ ->
@@ -78,19 +79,28 @@ end
 
 module StdFunction = struct
   let operator_call : model =
-   fun location ~ret:(ret_id, _) ~actuals astate ->
-    ( match actuals with
-    | (lambda_ptr_hist, _) :: _ ->
+   fun ~caller_summary location ~ret ~actuals astate ->
+    let havoc_ret (ret_id, _) astate =
+      let event =
+        PulseDomain.ValueHistory.Call {f= `Model "std::function::operator()"; location}
+      in
+      [PulseOperations.havoc_id ret_id [event] astate]
+    in
+    match actuals with
+    | [] ->
+        Ok (havoc_ret ret astate)
+    | (lambda_ptr_hist, _) :: actuals -> (
         PulseOperations.eval_access location lambda_ptr_hist Dereference astate
         >>= fun (astate, (lambda, _)) ->
         PulseOperations.Closures.check_captured_addresses
           (PulseDomain.InterprocAction.Immediate {imm= (); location})
           lambda astate
-    | _ ->
-        Ok astate )
-    >>| fun astate ->
-    let event = PulseDomain.ValueHistory.Call {f= `Model "<lambda>"; location} in
-    [PulseOperations.havoc_id ret_id [event] astate]
+        >>= fun astate ->
+        match PulseAbductiveDomain.Memory.get_closure_proc_name lambda astate with
+        | None ->
+            (* we don't know what proc name this lambda resolves to *) Ok (havoc_ret ret astate)
+        | Some callee_proc_name ->
+            PulseOperations.call ~caller_summary location callee_proc_name ~ret ~actuals astate )
 end
 
 module StdVector = struct
@@ -125,7 +135,7 @@ module StdVector = struct
 
 
   let invalidate_references vector_f : model =
-   fun location ~ret:_ ~actuals astate ->
+   fun ~caller_summary:_ location ~ret:_ ~actuals astate ->
     match actuals with
     | (vector, _) :: _ ->
         let crumb =
@@ -141,7 +151,7 @@ module StdVector = struct
 
 
   let at : model =
-   fun location ~ret ~actuals astate ->
+   fun ~caller_summary:_ location ~ret ~actuals astate ->
     let event = PulseDomain.ValueHistory.Call {f= `Model "std::vector::at"; location} in
     match actuals with
     | [(vector, _); (index, _)] ->
@@ -152,7 +162,7 @@ module StdVector = struct
 
 
   let reserve : model =
-   fun location ~ret:_ ~actuals astate ->
+   fun ~caller_summary:_ location ~ret:_ ~actuals astate ->
     match actuals with
     | [(vector, _); _value] ->
         let crumb = PulseDomain.ValueHistory.Call {f= `Model "std::vector::reserve"; location} in
@@ -164,7 +174,7 @@ module StdVector = struct
 
 
   let push_back : model =
-   fun location ~ret:_ ~actuals astate ->
+   fun ~caller_summary:_ location ~ret:_ ~actuals astate ->
     match actuals with
     | [(vector, _); _value] ->
         let crumb = PulseDomain.ValueHistory.Call {f= `Model "std::vector::push_back"; location} in

infer/src/pulse/PulseModels.mli

@@ -7,7 +7,8 @@
 open! IStd
 
 type exec_fun =
-     Location.t
+     caller_summary:Summary.t
+  -> Location.t
   -> ret:Ident.t * Typ.t
   -> actuals:(PulseDomain.AddrTracePair.t * Typ.t) list
   -> PulseAbductiveDomain.t

infer/src/pulse/PulseOperations.ml

@@ -292,3 +292,32 @@ let remove_vars vars astate =
   in
   let astate' = Stack.remove_vars vars astate in
   if phys_equal astate' astate then astate else PulseAbductiveDomain.discard_unreachable astate'
+
+
+let call ~caller_summary call_loc callee_pname ~ret ~actuals astate =
+  match PulsePayload.read_full caller_summary.Summary.proc_desc callee_pname with
+  | Some (callee_proc_desc, preposts) ->
+      let formals =
+        Procdesc.get_formals callee_proc_desc
+        |> List.map ~f:(fun (mangled, _) -> Pvar.mk mangled callee_pname |> Var.of_pvar)
+      in
+      (* call {!PulseAbductiveDomain.PrePost.apply} on each pre/post pair in the summary. *)
+      List.fold_result preposts ~init:[] ~f:(fun posts pre_post ->
+          (* apply all pre/post specs *)
+          PulseAbductiveDomain.PrePost.apply callee_pname call_loc pre_post ~formals ~actuals
+            astate
+          >>| fun (post, return_val_opt) ->
+          let event = ValueHistory.Call {f= `Call callee_pname; location= call_loc} in
+          let post =
+            match return_val_opt with
+            | Some return_val ->
+                write_id (fst ret) (return_val, [event]) post
+            | None ->
+                havoc_id (fst ret) [event] post
+          in
+          post :: posts )
+  | None ->
+      (* no spec found for some reason (unknown function, ...) *)
+      L.d_printfln "No spec found for %a@\n" Typ.Procname.pp callee_pname ;
+      let event = ValueHistory.Call {f= `UnknownCall callee_pname; location= call_loc} in
+      Ok [havoc_id (fst ret) [event] astate]

infer/src/pulse/PulseOperations.mli

@@ -99,3 +99,14 @@ val check_address_escape :
   -> PulseDomain.ValueHistory.t
   -> t
   -> t access_result
+
+val call :
+     caller_summary:Summary.t
+  -> Location.t
+  -> Typ.Procname.t
+  -> ret:Ident.t * Typ.t
+  -> actuals:((AbstractAddress.t * PulseDomain.ValueHistory.t) * Typ.t) list
+  -> t
+  -> t list access_result
+(** perform an interprocedural call: apply the summary for the call proc name passed as argument if
+    it exists *)

infer/src/pulse/PulsePayload.ml

@@ -0,0 +1,14 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! IStd
+
+include SummaryPayload.Make (struct
+  type nonrec t = PulseSummary.t
+
+  let field = Payloads.Fields.pulse
+end)

infer/src/pulse/PulsePayload.mli

@@ -0,0 +1,10 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! IStd
+
+include SummaryPayload.S with type t = PulseSummary.t

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

@@ -156,3 +156,16 @@ void capture_multiple_vars_by_value_ok(C c, C c2) {
     return d;
   };
 }
+
+void call_lambda_ok() {
+  auto f = [](S* s) { int x = s->f; };
+  S* s = new S();
+  f(s);
+}
+
+void call_lambda_bad() {
+  auto f = [](S* s) { int x = s->f; };
+  S* s = new S();
+  delete s;
+  f(s);
+}

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

@@ -2,6 +2,7 @@ codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AF
 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]
 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,when calling `templated_wrapper_delete_ok` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,when calling `templated_wrapper_access_ok` here,invalid access occurs here here]