[pulse] support modelling destructors

Summary:
We want to detect that variables and C++ temporaries go out of scope
even when their destructor happens to be modelled.

We lost a test to that because `std::function::~function` was poorly
modeled as deleting the lambda itself which would now cause a double
invalidation. This has to be modelled better now as something that
invalidates something *inside* the lambda, and also model `operator()`
as something that accesses that something, to recover that test. It's
not a vital test though, so Do It Later©.

Reviewed By: ngorogiannis

Differential Revision: D16121091

fbshipit-source-id: 6b777ca18

infer/src/pulse/Pulse.ml

@@ -132,26 +132,27 @@ module PulseTransferFunctions = struct
           (* function pointer, etc.: skip for now *)
           None
     in
-    match model with
+    (* do interprocedural call then destroy objects going out of scope *)
-    | Some model ->
+    let posts =
-        L.d_printfln "Found model for call@\n" ;
+      match model with
-        model ~caller_summary:summary call_loc ~ret ~actuals:actuals_evaled astate
+      | Some model ->
-    | None -> (
+          L.d_printfln "Found model for call@\n" ;
-        (* do interprocedural call then destroy objects going out of scope *)
+          model ~caller_summary:summary call_loc ~ret ~actuals:actuals_evaled astate
-        PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse interproc call" ())) ;
+      | None ->
-        let posts =
+          PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse interproc call" ())) ;
-          interprocedural_call summary ret call_exp actuals_evaled flags call_loc astate
+          let r = interprocedural_call summary ret call_exp actuals_evaled flags call_loc astate in
-        in
+          PerfEvent.(log (fun logger -> log_end_event logger ())) ;
-        PerfEvent.(log (fun logger -> log_end_event logger ())) ;
+          r
-        match get_out_of_scope_object call_exp actuals flags with
+    in
-        | Some pvar_typ ->
+    match get_out_of_scope_object call_exp actuals flags with
-            L.d_printfln "%a is going out of scope" Pvar.pp_value (fst pvar_typ) ;
+    | Some pvar_typ ->
-            posts
+        L.d_printfln "%a is going out of scope" Pvar.pp_value (fst pvar_typ) ;
-            >>= fun posts ->
+        posts
-            List.map posts ~f:(fun astate -> exec_object_out_of_scope call_loc pvar_typ astate)
+        >>= fun posts ->
-            |> Result.all
+        List.map posts ~f:(fun astate -> exec_object_out_of_scope call_loc pvar_typ astate)
-        | None ->
+        |> Result.all
-            posts )
+    | None ->
+        posts
 
 
   let exec_instr (astate : Domain.t) {ProcData.summary} _cfg_node (instr : Sil.instr) =

infer/src/pulse/PulseModels.ml

@@ -194,7 +194,6 @@ module ProcNameDispatcher = struct
       [ -"folly" &:: "DelayedDestruction" &:: "destroy" &--> Misc.skip
       ; -"folly" &:: "Optional" &:: "reset" &--> Misc.skip
       ; -"folly" &:: "SocketAddress" &:: "~SocketAddress" &--> Misc.skip
-      ; -"std" &:: "function" &:: "~function" &--> Cplusplus.delete
       ; -"std" &:: "function" &:: "operator()" &--> StdFunction.operator_call
       ; -"std" &:: "function" &:: "operator=" &--> Misc.shallow_copy "std::function::operator="
       ; -"std" &:: "vector" &:: "assign" &--> StdVector.invalidate_references Assign

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

@@ -95,7 +95,8 @@ std::function<int()> ref_capture_read_lambda_ok() {
       f; // reading (but not invoking) the lambda doesn't use its captured vars
 }
 
-int delete_lambda_then_call_bad() {
+// explicit destructor call is not modelled
+int FN_delete_lambda_then_call_bad() {
   std::function<int()> lambda = [] { return 1; };
   lambda.~function();
   return lambda();

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

@@ -1,7 +1,6 @@
 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]
 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]
-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 `call_lambda_bad::lambda_closures.cpp:162:12::operator()()` here,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,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,when calling `call_lambda_bad::lambda_closures.cpp:163:12::operator()()` here,invalid access occurs here]
-codetoanalyze/cpp/pulse/closures.cpp, delete_lambda_then_call_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,variable declared,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,variable declared,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 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]
 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 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]
 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]