From 5c2ee8d85f72873758de00087f2681fad08043c2 Mon Sep 17 00:00:00 2001
From: Sam Blackshear <shb@fb.com>
Date: Tue, 21 Feb 2017 16:01:42 -0800
Subject: [PATCH] [thread-safety] model ThreadLocal.get() as acquiring
 ownership

Summary: Thread-local variables can't be shared between threads, so it's safe to mutate them outside of synchronization

Reviewed By: jeremydubreil

Differential Revision: D4568316

fbshipit-source-id: 0634cad
---
 infer/src/checkers/ThreadSafety.ml                | 15 ++++++++++-----
 .../java/threadsafety/Ownership.java              |  4 ++++
 2 files changed, 14 insertions(+), 5 deletions(-)

diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml
index 730689b64..e27d26f6f 100644
--- a/infer/src/checkers/ThreadSafety.ml
+++ b/infer/src/checkers/ThreadSafety.ml
@@ -228,20 +228,25 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
   let acquires_ownership pname tenv =
     let is_allocation pn =
       Procname.equal pn BuiltinDecl.__new || Procname.equal pn BuiltinDecl.__new_array in
-    (* in dependency injection, the allocation happens behind the scenes. so we model it. *)
-    let is_dependency_injection_provider = function
+    (* identify library functions that maintain ownership invariants behind the scenes *)
+    let is_owned_in_library = function
       | Procname.Java java_pname ->
           begin
             match Procname.java_get_class_name java_pname,
                   Procname.java_get_method java_pname with
-            | "javax.inject.Provider", "get" -> true
+            | "javax.inject.Provider", "get" ->
+                (* in dependency injection, the library allocates fresh values behind the scenes *)
+                true
+            | "java.lang.ThreadLocal", "get" ->
+                (* ThreadLocal prevents sharing between threads behind the scenes *)
+                true
             | _ -> false
           end
       | _ ->
           false in
     is_allocation pname ||
-    is_dependency_injection_provider pname ||
-    PatternMatch.override_exists is_dependency_injection_provider tenv pname
+    is_owned_in_library pname ||
+    PatternMatch.override_exists is_owned_in_library tenv pname
 
   let exec_instr (astate : Domain.astate) { ProcData.pdesc; tenv; extras; } _ =
     let is_container_write pn tenv = match pn with
diff --git a/infer/tests/codetoanalyze/java/threadsafety/Ownership.java b/infer/tests/codetoanalyze/java/threadsafety/Ownership.java
index 14c4ab2c5..c6a06c755 100644
--- a/infer/tests/codetoanalyze/java/threadsafety/Ownership.java
+++ b/infer/tests/codetoanalyze/java/threadsafety/Ownership.java
@@ -276,6 +276,10 @@ public class Ownership {
     }
   }
 
+  public void threadLocalOk(ThreadLocal<Obj> threadLocal) {
+    threadLocal.get().f = new Object();
+  }
+
   // need to handle multiple ownership attributes in order to get this one
   public void FP_twoDifferentConditionalOwnsOk() {
     Obj owned1 = new Obj();