[threadsafety] Add ownership on stack-allocated variables in cpp

Summary: Stack-allocated variables cannot be raced on in cpp as every thread has its own stack. At the beginning of the analysis we add ownership to the local variables.

Reviewed By: jberdine

Differential Revision: D6020506

fbshipit-source-id: 0a90a97

infer/src/checkers/ThreadSafety.ml

@@ -1065,6 +1065,21 @@ let analyze_procedure {Callbacks.proc_desc; get_proc_desc; tenv; summary} =
         else if is_marked_thread_safe proc_desc tenv then ThreadsDomain.AnyThread
         else ThreadsDomain.NoThread
       in
+      let add_owned_local acc (name, typ) =
+        let pvar = Pvar.mk name (Procdesc.get_proc_name proc_desc) in
+        let base = AccessPath.base_of_pvar pvar typ in
+        OwnershipDomain.add (base, []) OwnershipAbstractValue.owned acc
+      in
+      (* Add ownership to local variables. In cpp, stack-allocated local
+         variables cannot be raced on as every thread has its own stack. *)
+      let own_locals_in_cpp =
+        match Procdesc.get_proc_name proc_desc with
+        | ObjC_Cpp _
+         -> List.fold ~f:add_owned_local (Procdesc.get_locals proc_desc)
+              ~init:OwnershipDomain.empty
+        | _
+         -> OwnershipDomain.empty
+      in
       if is_initializer tenv (Procdesc.get_proc_name proc_desc) then
         let add_owned_formal acc formal_index =
           match FormalMap.get_formal_base formal_index formal_map with
@@ -1082,7 +1097,7 @@ let analyze_procedure {Callbacks.proc_desc; get_proc_desc; tenv; summary} =
           else [0]
           (* express that the constructor owns [this] *)
         in
-        let ownership = List.fold ~f:add_owned_formal owned_formals ~init:OwnershipDomain.empty in
+        let ownership = List.fold ~f:add_owned_formal owned_formals ~init:own_locals_in_cpp in
         ({ThreadSafetyDomain.empty with ownership; threads}, IdAccessPathMapDomain.empty)
       else
         (* add Owned(formal_index) predicates for each formal to indicate that each one is owned if
@@ -1092,7 +1107,7 @@ let analyze_procedure {Callbacks.proc_desc; get_proc_desc; tenv; summary} =
         in
         let ownership =
           List.fold ~f:add_owned_formal (FormalMap.get_formals_indexes formal_map)
-            ~init:OwnershipDomain.empty
+            ~init:own_locals_in_cpp
         in
         ({ThreadSafetyDomain.empty with ownership; threads}, IdAccessPathMapDomain.empty)
     in

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

@@ -1,6 +1,8 @@
 codetoanalyze/cpp/threadsafety/basics.cpp, basics::Basic_get2, 3, THREAD_SAFETY_VIOLATION, [<Read trace>,access to `&this.suspiciously_written`,<Write trace>,access to `&this.suspiciously_written`]
 codetoanalyze/cpp/threadsafety/basics.cpp, basics::Basic_get4, 0, THREAD_SAFETY_VIOLATION, [<Read trace>,access to `&this.suspiciously_read`,<Write trace>,access to `&this.suspiciously_read`]
 codetoanalyze/cpp/threadsafety/basics.cpp, basics::Basic_get5, 0, THREAD_SAFETY_VIOLATION, [<Read trace>,call to basics::Basic_get_private_suspiciously_read,access to `&this.suspiciously_read`,<Write trace>,access to `&this.suspiciously_read`]
+codetoanalyze/cpp/threadsafety/locals_ownership.cpp, locals::Ownership_test2_bad, 5, THREAD_SAFETY_VIOLATION, [<Read trace>,access to `&x.f`,<Write trace>,access to `&x.f`]
+codetoanalyze/cpp/threadsafety/locals_ownership.cpp, locals::Ownership_test3_bad, 5, THREAD_SAFETY_VIOLATION, [<Read trace>,access to `&x.f`,<Write trace>,access to `&x.f`]
 codetoanalyze/cpp/threadsafety/lock_guard.cpp, basics::LockGuard_get2, 3, THREAD_SAFETY_VIOLATION, [<Read trace>,access to `&this.suspiciously_written`,<Write trace>,access to `&this.suspiciously_written`]
 codetoanalyze/cpp/threadsafety/lock_guard.cpp, basics::LockGuard_get4, 0, THREAD_SAFETY_VIOLATION, [<Read trace>,access to `&this.suspiciously_read`,<Write trace>,access to `&this.suspiciously_read`]
 codetoanalyze/cpp/threadsafety/lock_guard.cpp, basics::LockGuard_test1, 2, THREAD_SAFETY_VIOLATION, [<Read trace>,access to `&this.suspiciously_read`,<Write trace>,access to `&this.suspiciously_read`]

infer/tests/codetoanalyze/cpp/threadsafety/locals_ownership.cpp

@@ -0,0 +1,74 @@
+/*
+ * Copyright (c) 2017 - 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 <mutex>
+
+namespace locals {
+
+struct X {
+  int f;
+};
+
+class Ownership {
+ public:
+  Ownership() {}
+
+  int test0_ok() {
+    X x;
+    mutex_.lock();
+    x.f = 7;
+    mutex_.unlock();
+    return x.f;
+  }
+
+  int test1_ok() {
+    X* x = new X();
+    mutex_.lock();
+    x->f = 7;
+    mutex_.unlock();
+    return x->f;
+  }
+
+  int test2_ok() {
+    X x = current; // copy constructor
+    mutex_.lock();
+    x.f = 7;
+    mutex_.unlock();
+    return x.f;
+  }
+
+  int test2_bad() {
+    X* x = &current;
+    mutex_.lock();
+    x->f = 7;
+    mutex_.unlock();
+    return x->f;
+  }
+
+  int test3_ok(X xformal) {
+    X x = xformal; // copy constructor
+    mutex_.lock();
+    x.f = 7;
+    mutex_.unlock();
+    return x.f;
+  }
+
+  int test3_bad(X* xformal) {
+    X* x = xformal;
+    mutex_.lock();
+    x->f = 7;
+    mutex_.unlock();
+    return x->f;
+  }
+
+ private:
+  X current;
+  std::mutex mutex_;
+};
+} // namespace locals