[thread-safety] don't warn on writes to volatile fields

Summary:
Races on volatile fields are less concerning than races on non-volatile fields because at least the read/write won't result in garbage.
For now, let's de-prioritize these writes by ignoring them.

Reviewed By: peterogithub

Differential Revision: D4434023

fbshipit-source-id: 05043ba

infer/src/IR/Annot.re

@@ -26,6 +26,8 @@ type t = {
 }
 [@@deriving compare];
 
+let volatile = {class_name: "volatile", parameters: []};
+
 
 /** Pretty print an annotation. */
 let pp fmt annotation => F.fprintf fmt "@@%s" annotation.class_name;

infer/src/IR/Annot.rei

@@ -25,6 +25,10 @@ type t = {
 [@@deriving compare];
 
 
+/** annotation for fields/methods marked with the "volatile" keyword */
+let volatile: t;
+
+
 /** Pretty print an annotation. */
 let pp: F.formatter => t => unit;
 

infer/src/checkers/ThreadSafety.ml

@@ -70,12 +70,15 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       | base, []
       | base, _ :: [] -> base, []
       | base, accesses -> base, IList.rev (IList.tl (IList.rev accesses)) in
-    let is_thread_confined (_, accesses) = match IList.rev accesses with
+    (* we don't want to warn on writes to the field if it is (a) thread-confined, or (b) volatile *)
+    let is_safe_write (_, accesses) = match IList.rev accesses with
       | AccessPath.FieldAccess (fieldname, Typ.Tstruct typename) :: _ ->
           begin
             match Tenv.lookup tenv typename with
             | Some struct_typ ->
-                Annotations.field_has_annot fieldname struct_typ Annotations.ia_is_thread_confined
+                Annotations.field_has_annot
+                  fieldname struct_typ Annotations.ia_is_thread_confined ||
+                Annotations.field_has_annot fieldname struct_typ Annotations.ia_is_volatile
             | None ->
                 false
           end
@@ -86,7 +89,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     IList.fold_left
       (fun acc rawpath ->
          if not (ThreadSafetyDomain.OwnershipDomain.mem (truncate rawpath) owned) &&
-            not (is_thread_confined rawpath)
+            not (is_safe_write rawpath)
          then
            ThreadSafetyDomain.PathDomain.add_sink (ThreadSafetyDomain.make_access rawpath loc) acc
          else

infer/src/checkers/annotations.ml

@@ -109,6 +109,7 @@ let present = "Present"
 let strict = "com.facebook.infer.annotation.Strict"
 let true_on_null = "TrueOnNull"
 let verify_annotation = "com.facebook.infer.annotation.Verify"
+let volatile = "volatile"
 let expensive = "Expensive"
 let performance_critical = "PerformanceCritical"
 let no_allocation = "NoAllocation"
@@ -162,6 +163,9 @@ let ia_is_true_on_null ia =
 let ia_is_initializer ia =
   ia_ends_with ia initializer_
 
+let ia_is_volatile ia =
+  ia_contains ia volatile
+
 let field_injector_readwrite_list =
   [
     inject_view;

infer/src/checkers/annotations.mli

@@ -105,6 +105,7 @@ val ia_is_thread_safe_method : Annot.Item.t -> bool
 val ia_is_assume_thread_safe : Annot.Item.t -> bool
 val ia_is_ui_thread : Annot.Item.t -> bool
 val ia_is_thread_confined : Annot.Item.t -> bool
+val ia_is_volatile : Annot.Item.t -> bool
 
 val ia_iter : (Annot.t -> unit) -> Annot.Item.t -> unit
 

infer/src/java/jTransType.ml

@@ -215,7 +215,12 @@ let create_sil_class_field cn cf =
   let fs = cf.Javalib.cf_signature in
   let field_name = create_fieldname cn fs
   and field_type = get_named_type (JBasics.fs_type fs)
-  and annotation = JAnnotation.translate_item cf.Javalib.cf_annotations in
+  and annotation =
+    let real_annotations = JAnnotation.translate_item cf.Javalib.cf_annotations in
+    (* translate modifers like "volatile" as annotations *)
+    match cf.Javalib.cf_kind with
+    | Javalib.Volatile -> (Annot.volatile, true) :: real_annotations
+    | Javalib.NotFinal | Final -> real_annotations in
   (field_name, field_type, annotation)
 
 

infer/tests/codetoanalyze/java/threadsafety/ThreadSafeExample.java

@@ -94,6 +94,13 @@ public class ThreadSafeExample{
     returnConstructorOk();
   }
 
+  volatile Object volatileField;
+
+  // we don't warn on unsafe writes to volatile fields
+  public void unsafeVolatileWriteOk() {
+    this.volatileField = new Object();
+  }
+
 }
 
 class ExtendsThreadSafeExample extends ThreadSafeExample{