From a45844f40979c0c215bd808d51d307ca4c4810ea Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Wed, 18 May 2016 09:04:15 -0700 Subject: [PATCH] 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 | 3 ++ infer/src/backend/config.mli | 1 + infer/src/backend/rearrange.ml | 63 +++++++++++++++++++++++++++++- infer/src/checkers/annotations.ml | 16 ++++++-- infer/src/checkers/annotations.mli | 8 ++++ 5 files changed, 86 insertions(+), 5 deletions(-) diff --git a/infer/src/backend/config.ml b/infer/src/backend/config.ml index ea696c672..49e471115 100644 --- a/infer/src/backend/config.ml +++ b/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 diff --git a/infer/src/backend/config.mli b/infer/src/backend/config.mli index 7fc51be9f..d3be6598a 100644 --- a/infer/src/backend/config.mli +++ b/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 diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml index a2975ffb9..97b3a74d6 100644 --- a/infer/src/backend/rearrange.ml +++ b/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 (); diff --git a/infer/src/checkers/annotations.ml b/infer/src/checkers/annotations.ml index 27a3b55b8..0659e8c02 100644 --- a/infer/src/checkers/annotations.ml +++ b/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 diff --git a/infer/src/checkers/annotations.mli b/infer/src/checkers/annotations.mli index b329ad08d..80ac40ab6 100644 --- a/infer/src/checkers/annotations.mli +++ b/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