identify reads of fields protected by @GuardedBy

Summary:
If we see a read of a field f annotated with GuardedBy("mLock"), we spring into action.
What we do is look for some hpred `A.mLock |-> B` and return `B` as the "guarded-by object".
Once we have models for montitorenter/exit in place, `B.__inferIsLocked = true` will mean "lock held", and `B.__inferIsLocked = false` will mean "lock not held".

Reviewed By: jvillard

Differential Revision: D3316288

fbshipit-source-id: 8625e04

infer/src/backend/config.ml

@@ -143,6 +143,9 @@ let suppress_warnings_annotations_long = "suppress-warnings-annotations"
 (** If true performs taint analysis *)
 let taint_analysis = true
 
+(** Experimental: if true do some specialized analysis of concurrent constructs. *)
+let csl_analysis = true
+
 (** Enable detailed tracing information during array abstraction *)
 let trace_absarray = false
 

infer/src/backend/config.mli

@@ -77,6 +77,7 @@ val specs_dir_name : string
 val specs_files_suffix : string
 val start_filename : string
 val taint_analysis : bool
+val csl_analysis : bool
 val trace_absarray : bool
 val undo_join : bool
 val unsafe_unret : string

infer/src/backend/rearrange.ml

@@ -600,14 +600,75 @@ let prop_iter_add_hpred_footprint_to_prop pname tenv prop (lexp, typ) inst =
   let offsets_default = Sil.exp_get_offsets lexp in
   Prop.prop_iter_set_state iter offsets_default
 
+(* TODO: have to call this on both reads and writes *)
+let add_guarded_by_constraints prop lexp =
+  let sigma = Prop.get_sigma prop in
+  (** if [fld] is annotated with @GuardedBy("mLock"), return mLock *)
+  let get_guarded_by_fld_str fld typ =
+    let extract_guarded_by_str (annot, _) =
+      if Annotations.annot_ends_with annot Annotations.guarded_by
+      then
+        match annot.Sil.parameters with
+        | [guarded_by_str] -> Some guarded_by_str
+        | _ -> None
+      else
+        None in
+    match Annotations.get_field_type_and_annotation fld typ with
+    | Some (_, item_annot) -> IList.find_map_opt extract_guarded_by_str item_annot
+    | _ -> None in
+  (* find A.guarded_by_fld_str |-> B and return Some B, or None if there is no such hpred *)
+  let find_guarded_by_exp fld typ sigma =
+    match get_guarded_by_fld_str fld typ with
+    | Some guarded_by_fld_str ->
+        let extract_guarded_by_strexp (fld, strexp) =
+          (* this comparison needs to be somewhat fuzzy, since programmers are free to write
+             @GuardedBy("mLock"), @GuardedBy("MyClass.mLock"), or use other conventions *)
+          if Ident.fieldname_to_flat_string fld = guarded_by_fld_str ||
+             Ident.fieldname_to_string fld = guarded_by_fld_str
+          then Some strexp
+          else None in
+        IList.find_map_opt
+          (function
+            | Sil.Hpointsto (_, Estruct (flds, _), _) ->
+                IList.find_map_opt extract_guarded_by_strexp flds
+            | _ ->
+                None)
+          sigma
+    | None ->
+        None in
+  let check_fld_locks typ prop_acc (fld, strexp) = match strexp with
+    | Sil.Eexp (exp, _) when Sil.exp_equal exp lexp ->
+        begin
+          match find_guarded_by_exp fld typ sigma with
+          | Some guarded_by_strexp ->
+              L.stderr "Got guarded_by_exp %a@." (Sil.pp_sexp pe_text) guarded_by_strexp;
+              (* TODO: check if the lock is held, act accordingly *)
+              prop_acc
+          | None ->
+              (* field not guarded; proceed with abduction as we normally would *)
+              prop_acc
+        end
+    | _ ->
+        prop_acc in
+  let hpred_check_flds prop_acc = function
+    | Sil.Hpointsto (_, Estruct (flds, _), Sizeof (typ, _)) ->
+        IList.fold_left (check_fld_locks typ) prop_acc flds
+    | _ ->
+        prop_acc in
+  IList.fold_left hpred_check_flds prop sigma
+
 (** Add a pointsto for [root(lexp): typ] to the iterator and to the
     footprint, if it's compatible with the allowed footprint
     variables. This function ensures that [root(lexp): typ] is the
     current hpred of the iterator. typ is the type of the root of lexp. *)
 let prop_iter_add_hpred_footprint pname tenv orig_prop iter (lexp, typ) inst =
+  let orig_prop' =
+    if Config.csl_analysis && Procname.is_java pname
+    then add_guarded_by_constraints orig_prop lexp
+    else orig_prop in
   let max_stamp = fav_max_stamp (Prop.prop_iter_footprint_fav iter) in
   let ptsto, ptsto_foot, atoms =
-    mk_ptsto_exp_footprint pname tenv orig_prop (lexp, typ) max_stamp inst in
+    mk_ptsto_exp_footprint pname tenv orig_prop' (lexp, typ) max_stamp inst in
   L.d_strln "++++ Adding footprint frame";
   Prop.d_prop (Prop.prop_hpred_star Prop.prop_emp ptsto);
   L.d_ln (); L.d_ln ();

infer/src/checkers/annotations.ml

@@ -77,14 +77,18 @@ let ia_has_annotation_with
     ia;
   !found
 
-(** Check if there is an annotation which ends with the given name *)
-let ia_ends_with ia ann_name =
-  let found = ref false in
+(** Return true if [annot] ends with [ann_name] *)
+let annot_ends_with annot ann_name =
   let filter s =
     let sl = String.length s in
     let al = String.length ann_name in
     sl >= al && String.sub s (sl - al) al = ann_name in
-  ia_iter (fun a -> if filter a.Sil.class_name then found := true) ia;
+  filter annot.Sil.class_name
+
+(** Check if there is an annotation in [ia] which ends with the given name *)
+let ia_ends_with ia ann_name =
+  let found = ref false in
+  ia_iter (fun a -> if annot_ends_with a ann_name then found := true) ia;
   !found
 
 let ia_contains ia ann_name =
@@ -130,6 +134,7 @@ let privacy_source = "PrivacySource"
 let privacy_sink = "PrivacySink"
 let integrity_source = "IntegritySource"
 let integrity_sink = "IntegritySink"
+let guarded_by = "GuardedBy"
 
 let ia_is_nullable ia =
   ia_ends_with ia nullable
@@ -217,6 +222,9 @@ let ia_is_integrity_source ia =
 let ia_is_integrity_sink ia =
   ia_ends_with ia integrity_sink
 
+let ia_is_guarded_by ia =
+  ia_ends_with ia guarded_by
+
 type annotation =
   | Nullable
   | Present

infer/src/checkers/annotations.mli

@@ -61,8 +61,14 @@ val get_declaring_class_annotations : Procname.java -> Tenv.t -> Sil.item_annota
 
 val nullable : string
 
+(** Return true if [annot] ends with [ann_name] *)
+val annot_ends_with : Sil.annotation -> string -> bool
+
 val ia_contains : Sil.item_annotation -> string -> bool
 
+(** Check if there is an annotation in [ia] which ends with the given name *)
+val ia_ends_with : Sil.item_annotation -> string -> bool
+
 val ia_has_annotation_with : Sil.item_annotation -> (Sil.annotation -> bool) -> bool
 
 val ia_get_strict : Sil.item_annotation -> Sil.annotation option
@@ -93,6 +99,7 @@ val ia_is_privacy_source : Sil.item_annotation -> bool
 val ia_is_privacy_sink : Sil.item_annotation -> bool
 val ia_is_integrity_source : Sil.item_annotation -> bool
 val ia_is_integrity_sink : Sil.item_annotation -> bool
+val ia_is_guarded_by : Sil.item_annotation -> bool
 
 val ia_iter : (Sil.annotation -> unit) -> Sil.item_annotation -> unit
 
@@ -112,3 +119,4 @@ val mk_ia : annotation -> Sil.item_annotation -> Sil.item_annotation
 val pp_annotated_signature : Procname.t -> Format.formatter -> annotated_signature -> unit
 
 val visibleForTesting : string
+val guarded_by : string