From 12ad6c11c1b714100509dc5b03ef04aa7e3988df Mon Sep 17 00:00:00 2001
From: Sam Blackshear <shb@fb.com>
Date: Tue, 13 Mar 2018 19:45:47 -0700
Subject: [PATCH] [ownership] return bottom on early exit or thrown exception

Reviewed By: jeremydubreil

Differential Revision: D7230168

fbshipit-source-id: 84f97a5
---
 infer/src/checkers/Ownership.ml               | 22 +++++++++++++--
 .../cpp/ownership/use_after_delete.cpp        | 27 +++++++++++++++++++
 2 files changed, 47 insertions(+), 2 deletions(-)

diff --git a/infer/src/checkers/Ownership.ml b/infer/src/checkers/Ownership.ml
index b4077f256..5ba6a4095 100644
--- a/infer/src/checkers/Ownership.ml
+++ b/infer/src/checkers/Ownership.ml
@@ -227,6 +227,16 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         false
 
 
+  let is_early_return call_exp =
+    match call_exp with
+    | HilInstr.Direct pname ->
+        Typ.Procname.equal pname BuiltinDecl.exit
+        || Typ.Procname.equal pname BuiltinDecl.objc_cpp_throw
+        || Typ.Procname.equal pname BuiltinDecl.abort
+    | _ ->
+        false
+
+
   let exec_instr (astate: Domain.astate) (proc_data: extras ProcData.t) _ (instr: HilInstr.t) =
     let summary = proc_data.extras in
     match instr with
@@ -281,10 +291,18 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         (* invoking a lambda; check that it's captured vars are valid *)
         Domain.check_var_lifetime lhs_var loc summary astate ;
         astate
-    | Call (ret_opt, _, actuals, _, loc)
+    | Call (ret_opt, call_exp, actuals, _, loc)
       -> (
         let astate' = Domain.actuals_add_reads actuals loc summary astate in
-        match ret_opt with Some (base_var, _) -> Domain.remove base_var astate' | None -> astate' )
+        if is_early_return call_exp then
+          (* thrown exception, abort(), or exit; return _|_ *)
+          Domain.empty
+        else
+          match ret_opt with
+          | Some (base_var, _) ->
+              Domain.remove base_var astate'
+          | None ->
+              astate' )
     | Assume (assume_exp, _, _, loc) ->
         Domain.exp_add_reads assume_exp loc summary astate
 end
diff --git a/infer/tests/codetoanalyze/cpp/ownership/use_after_delete.cpp b/infer/tests/codetoanalyze/cpp/ownership/use_after_delete.cpp
index 19e50dfb9..750b260fc 100644
--- a/infer/tests/codetoanalyze/cpp/ownership/use_after_delete.cpp
+++ b/infer/tests/codetoanalyze/cpp/ownership/use_after_delete.cpp
@@ -98,3 +98,30 @@ void use_in_loop_bad() {
     s->f = i;
   }
 }
+
+S* gated_delete_abort_ok(bool b) {
+  auto s = new S{1};
+  if (b) {
+    delete s;
+    std::abort();
+  }
+  return s;
+}
+
+S* gated_exit_abort_ok(bool b) {
+  auto s = new S{1};
+  if (b) {
+    delete s;
+    exit(1);
+  }
+  return s;
+}
+
+S* gated_delete_throw_ok(bool b) {
+  auto s = new S{1};
+  if (b) {
+    delete s;
+    throw 5;
+  }
+  return s;
+}