diff --git a/infer/src/IR/Annot.re b/infer/src/IR/Annot.re index 1083bfa46..7133abb3d 100644 --- a/infer/src/IR/Annot.re +++ b/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; diff --git a/infer/src/IR/Annot.rei b/infer/src/IR/Annot.rei index 39771aba0..f1c98a1e6 100644 --- a/infer/src/IR/Annot.rei +++ b/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; diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index 52f448398..db10ab37a 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/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 diff --git a/infer/src/checkers/annotations.ml b/infer/src/checkers/annotations.ml index a3e75b99c..abd120cf8 100644 --- a/infer/src/checkers/annotations.ml +++ b/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; diff --git a/infer/src/checkers/annotations.mli b/infer/src/checkers/annotations.mli index b995579a1..261bc2e8a 100644 --- a/infer/src/checkers/annotations.mli +++ b/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 diff --git a/infer/src/java/jTransType.ml b/infer/src/java/jTransType.ml index 5de1435d6..7e60e90a8 100644 --- a/infer/src/java/jTransType.ml +++ b/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) diff --git a/infer/tests/codetoanalyze/java/threadsafety/ThreadSafeExample.java b/infer/tests/codetoanalyze/java/threadsafety/ThreadSafeExample.java index 82698213b..16d08d97f 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/ThreadSafeExample.java +++ b/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{