[ownership] report use after destructor

Summary: Similar to use-after-`delete`.

Reviewed By: jeremydubreil

Differential Revision: D7032893

fbshipit-source-id: a974dc3

infer/src/checkers/Ownership.ml

@@ -52,7 +52,10 @@ module Domain = struct
   include AbstractDomain.Map (Var) (Permission)
 
   let log_use_after_lifetime var loc summary =
-    let message = F.asprintf "Variable %a is used after its lifetime has ended" Var.pp var in
+    let message =
+      F.asprintf "Variable %a is used after its lifetime has ended at %a" Var.pp var Location.pp
+        loc
+    in
     let ltr = [Errlog.make_trace_element 0 loc "Use of invalid variable" []] in
     let exn = Exceptions.Checkers (IssueType.use_after_lifetime, Localise.verbatim_desc message) in
     Reporting.log_error summary ~loc ~ltr exn
@@ -104,8 +107,14 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
   type extras = Specs.summary
 
   let transfers_ownership pname =
-    (* TODO: support delete[], free, and destructors *)
+    (* TODO: support delete[], free, and (in some cases) std::move *)
     Typ.Procname.equal pname BuiltinDecl.__delete
+    ||
+    match pname with
+    | Typ.Procname.ObjC_Cpp clang_pname ->
+        Typ.Procname.ObjC_Cpp.is_destructor clang_pname
+    | _ ->
+        false
 
 
   let exec_instr (astate: Domain.astate) (proc_data: extras ProcData.t) _ (instr: HilInstr.t) =

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

@@ -6,3 +6,4 @@ codetoanalyze/cpp/ownership/use_after_delete.cpp, reassign_field_of_deleted_bad,
 codetoanalyze/cpp/ownership/use_after_delete.cpp, return_deleted_bad, 3, USE_AFTER_LIFETIME, [Use of invalid variable]
 codetoanalyze/cpp/ownership/use_after_delete.cpp, use_in_branch_bad, 4, USE_AFTER_LIFETIME, [Use of invalid variable]
 codetoanalyze/cpp/ownership/use_after_delete.cpp, use_in_loop_bad, 4, USE_AFTER_LIFETIME, [Use of invalid variable]
+codetoanalyze/cpp/ownership/use_after_destructor.cpp, double_destructor_bad, 5, USE_AFTER_LIFETIME, [Use of invalid variable]

infer/tests/codetoanalyze/cpp/ownership/use_after_destructor.cpp

@@ -0,0 +1,71 @@
+/*
+ * Copyright (c) 2018 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+
+#include <iostream>
+#include <memory>
+#include <string>
+
+struct S {
+  int f;
+
+  ~S() {}
+};
+
+// destructor called at end of function, no issues
+void normal_scope_destructor_ok() { S s{1}; }
+
+void nested_scope_destructor_ok() {
+  { S s{1}; }
+}
+
+int reinit_after_explicit_destructor_ok() {
+  S s{1};
+  s.~S();
+  s = S{2};
+  return s.f;
+}
+
+void placement_new_explicit_destructor_ok() {
+  char buf[sizeof(S)];
+  {
+    S* s = new (buf) S;
+    s->~S();
+  }
+  {
+    // this use of [buf] shouldn't be flagged
+    S* s = new (buf) S;
+    s->~S();
+  }
+}
+
+void double_destructor_bad() {
+  S s{1};
+  s.~S();
+  // destructor will be called again after S goes out of scope, which is
+  // undefined behavior
+}
+
+// frontend does the right thing here, but we need to propagate permissions from
+// tmp to s
+int FN_use_after_scope1_bad() {
+  S s;
+  {
+    S tmp{1};
+    s = tmp;
+  } // destructor runs here
+  return s.f;
+}
+
+int FN_use_after_scope2_bad() {
+  S s;
+  {
+    s = S{1};
+  } // destructor runs here, but our frontend currently doesn't insert it
+  return s.f;
+}