From 0e77e3623580475860a4bcad07613e3e8ed17db4 Mon Sep 17 00:00:00 2001
From: Sam Blackshear <shb@fb.com>
Date: Thu, 2 Feb 2017 11:03:59 -0800
Subject: [PATCH] [thread-safety] propagate @Functional attribute across boxing
 of primitive types

Reviewed By: jeremydubreil

Differential Revision: D4501552

fbshipit-source-id: c4cc9ec
---
 infer/src/checkers/ThreadSafety.ml            | 37 ++++++++++++++-
 .../java/threadsafety/Annotations.java        | 47 +++++++++++++++++++
 .../java/threadsafety/issues.exp              |  3 ++
 3 files changed, 86 insertions(+), 1 deletion(-)

diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml
index 2edc5f0c9..58baea935 100644
--- a/infer/src/checkers/ThreadSafety.ml
+++ b/infer/src/checkers/ThreadSafety.ml
@@ -174,6 +174,24 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       { astate with unconditional_writes; } in
     let is_unprotected is_locked =
       not is_locked && not (Procdesc.is_java_synchronized pdesc) in
+    (* return true if the given procname boxes a primitive type into a reference type *)
+    let is_box = function
+      | Procname.Java java_pname ->
+          begin
+            match Procname.java_get_class_name java_pname, Procname.java_get_method java_pname with
+            | ("java.lang.Boolean" |
+               "java.lang.Byte" |
+               "java.lang.Char" |
+               "java.lang.Double" |
+               "java.lang.Float" |
+               "java.lang.Integer" |
+               "java.lang.Long" |
+               "java.lang.Short"),
+              "valueOf" -> true
+            | _ -> false
+          end
+      | _ ->
+          false in
     let f_resolve_id = resolve_id astate.id_map in
 
     let open Domain in
@@ -293,7 +311,24 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
                           astate'.owned in
                     { astate' with locks = locks'; owned; }
                 | None ->
-                    astate in
+                    if is_box callee_pname
+                    then
+                      match ret_opt, actuals with
+                      | Some (ret_id, ret_typ), (actual_exp, actual_typ) :: _ ->
+                          begin
+                            match AccessPath.of_lhs_exp actual_exp actual_typ ~f_resolve_id with
+                            | Some ap when AccessPathSetDomain.mem ap astate.functional ->
+                                let functional =
+                                  AccessPathSetDomain.add
+                                    (AccessPath.of_id ret_id ret_typ) astate.functional in
+                                { astate with functional; }
+                            | _ ->
+                                astate
+                          end
+                      | _ ->
+                          astate
+                    else
+                      astate in
         begin
           match ret_opt with
           | Some (_, (Typ.Tint ILong | Tfloat FDouble)) ->
diff --git a/infer/tests/codetoanalyze/java/threadsafety/Annotations.java b/infer/tests/codetoanalyze/java/threadsafety/Annotations.java
index 3a54091cc..b073205bc 100644
--- a/infer/tests/codetoanalyze/java/threadsafety/Annotations.java
+++ b/infer/tests/codetoanalyze/java/threadsafety/Annotations.java
@@ -194,4 +194,51 @@ class Annotations implements FunctionalInterface {
     return mLong;
   }
 
+  Boolean mBoxedBool;
+
+  @Functional native boolean returnBool();
+
+  public boolean functionalAcrossBoxingOk() {
+    if (mBoxedBool != null) {
+      mBoxedBool = returnBool();
+    }
+    return mBoxedBool;
+  }
+
+  boolean mBool;
+
+  @Functional native Boolean returnBoxedBool();
+
+  public boolean FP_functionalAcrossUnboxingOk() {
+    if (!mBool) {
+      mBool = returnBoxedBool();
+    }
+    return mBool;
+  }
+
+  Long mBoxedLong;
+
+  @Functional native Long returnBoxedLong();
+
+  public Long functionalBoxedLongOk() {
+    if (mBoxedLong == null) {
+      mBoxedLong = returnBoxedLong();
+    }
+    return mBoxedLong;
+  }
+
+  public long functionalAcrossUnboxingLongBad() {
+    if (mLong != 0L) {
+      mLong = returnBoxedLong();
+    }
+    return mLong;
+  }
+
+  public long FP_functionalAcrossBoxingLongOk() {
+    if (mBoxedLong != null) {
+      mBoxedLong = returnLong();
+    }
+    return mBoxedLong;
+  }
+
 }
diff --git a/infer/tests/codetoanalyze/java/threadsafety/issues.exp b/infer/tests/codetoanalyze/java/threadsafety/issues.exp
index e6a184c80..1a10b5b04 100644
--- a/infer/tests/codetoanalyze/java/threadsafety/issues.exp
+++ b/infer/tests/codetoanalyze/java/threadsafety/issues.exp
@@ -1,5 +1,8 @@
+codetoanalyze/java/threadsafety/Annotations.java, boolean Annotations.FP_functionalAcrossUnboxingOk(), 2, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Annotations.mBool]
 codetoanalyze/java/threadsafety/Annotations.java, double Annotations.functionalDoubleBad(), 2, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Annotations.mDouble]
+codetoanalyze/java/threadsafety/Annotations.java, long Annotations.FP_functionalAcrossBoxingLongOk(), 2, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Annotations.mBoxedLong]
 codetoanalyze/java/threadsafety/Annotations.java, long Annotations.functionaLongBad(), 2, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Annotations.mLong]
+codetoanalyze/java/threadsafety/Annotations.java, long Annotations.functionalAcrossUnboxingLongBad(), 2, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Annotations.mLong]
 codetoanalyze/java/threadsafety/Annotations.java, void Annotations.mutateOffUiThreadBad(), 1, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Annotations.f]
 codetoanalyze/java/threadsafety/Annotations.java, void Annotations.mutateSubfieldOfConfinedBad(), 1, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Annotations.encapsulatedField.codetoanalyze.java.checkers.Annotations$Obj.fld]
 codetoanalyze/java/threadsafety/Builders.java, Builders$Obj Builders.buildThenMutateBad(Builders$Obj), 3, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Builders$Obj.g]