From ddc15ad663a211785d61d9a8d124c97b5b5922ab Mon Sep 17 00:00:00 2001 From: Nikos Gorogiannis Date: Fri, 21 Dec 2018 12:53:22 -0800 Subject: [PATCH] [racerd] move models and domain operations to respective source files Reviewed By: mbouaziz Differential Revision: D13537501 fbshipit-source-id: 88dbc022d --- infer/src/concurrency/RacerD.ml | 92 ++-------------- infer/src/concurrency/RacerDDomain.ml | 6 ++ infer/src/concurrency/RacerDDomain.mli | 4 +- infer/src/concurrency/RacerDModels.ml | 140 ++++++++++++++++++------- infer/src/concurrency/RacerDModels.mli | 16 +-- 5 files changed, 126 insertions(+), 132 deletions(-) diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index ace467eef..0729d824c 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -24,56 +24,6 @@ module TransferFunctions (CFG : ProcCfg.S) = struct type extras = ProcData.no_extras - (* we don't want to warn on accesses to the field if it is (a) thread-confined, or - (b) volatile *) - let is_safe_access access prefix_path tenv = - match (access, AccessPath.get_typ prefix_path tenv) with - | ( AccessPath.FieldAccess fieldname - , Some ({Typ.desc= Tstruct typename} | {desc= Tptr ({desc= Tstruct typename}, _)}) ) -> ( - match Tenv.lookup tenv typename with - | Some struct_typ -> - Annotations.struct_typ_has_annot 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 ) - | _ -> - false - - - let add_unannotated_call_access pname actuals (call_flags : CallFlags.t) loc tenv ~locks ~threads - attribute_map (proc_data : extras ProcData.t) = - let open RacerDModels in - let thread_safe_or_thread_confined annot = - Annotations.ia_is_thread_safe annot || Annotations.ia_is_thread_confined annot - in - let is_receiver_safe = function - | HilExp.AccessExpression receiver_access_exp :: _ -> ( - let receiver_access_path = HilExp.AccessExpression.to_access_path receiver_access_exp in - match AccessPath.truncate receiver_access_path with - | receiver_prefix, Some receiver_field -> - is_safe_access receiver_field receiver_prefix tenv - | _ -> - false ) - | _ -> - false - in - if - call_flags.cf_interface && Typ.Procname.is_java pname - && (not (is_java_library pname || is_builder_function pname)) - (* can't ask anyone to annotate interfaces in library code, and Builder's should always be - thread-safe (would be unreasonable to ask everyone to annotate them) *) - && (not (PatternMatch.check_class_attributes thread_safe_or_thread_confined tenv pname)) - && (not (has_return_annot thread_safe_or_thread_confined pname)) - && not (is_receiver_safe actuals) - then - let open Domain in - let access = TraceElem.make_unannotated_call_access pname loc in - let snapshot = AccessSnapshot.make access locks threads False proc_data.pdesc in - AccessDomain.add snapshot attribute_map - else attribute_map - - let add_access exp loc ~is_write_access accesses locks threads ownership (proc_data : extras ProcData.t) = let open Domain in @@ -86,7 +36,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let access_acc' = AccessDomain.add pre access_acc in add_field_accesses prefix_path' access_acc' access_list in - if is_safe_access access prefix_path proc_data.tenv then + if RacerDModels.is_safe_access access prefix_path proc_data.tenv then add_field_accesses prefix_path' access_acc access_list else let is_write = if List.is_empty access_list then is_write_access else false in @@ -112,41 +62,13 @@ module TransferFunctions (CFG : ProcCfg.S) = struct ~init:accesses (HilExp.get_access_exprs exp) - let is_synchronized_container callee_pname ((_, (base_typ : Typ.t)), accesses) tenv = - let open RacerDModels in - if is_threadsafe_collection callee_pname tenv then true - else - let is_annotated_synchronized base_typename container_field tenv = - match Tenv.lookup tenv base_typename with - | Some base_typ -> - Annotations.field_has_annot container_field base_typ - Annotations.ia_is_synchronized_collection - | None -> - false - in - match List.rev accesses with - | AccessPath.FieldAccess base_field :: AccessPath.FieldAccess container_field :: _ - when Typ.Procname.is_java callee_pname -> - let base_typename = - Typ.Name.Java.from_string (Typ.Fieldname.Java.get_class base_field) - in - is_annotated_synchronized base_typename container_field tenv - | [AccessPath.FieldAccess container_field] -> ( - match base_typ.desc with - | Typ.Tstruct base_typename | Tptr ({Typ.desc= Tstruct base_typename}, _) -> - is_annotated_synchronized base_typename container_field tenv - | _ -> - false ) - | _ -> - false - - let make_container_access callee_pname ~is_write receiver_ap callee_loc tenv caller_pdesc (astate : Domain.t) = (* create a dummy write that represents mutating the contents of the container *) let open Domain in let callee_accesses = - if is_synchronized_container callee_pname receiver_ap tenv then AccessDomain.empty + if RacerDModels.is_synchronized_container callee_pname receiver_ap tenv then + AccessDomain.empty else let container_access = TraceElem.make_container_access receiver_ap ~is_write callee_pname callee_loc @@ -369,10 +291,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct {astate with accesses; ownership} | Call (ret_base, Direct callee_pname, actuals, call_flags, loc) -> let ret_access_path = (ret_base, []) in - let accesses_with_unannotated_calls = - add_unannotated_call_access callee_pname actuals call_flags loc tenv ~locks:astate.locks - ~threads:astate.threads astate.accesses proc_data + let astate = + if RacerDModels.should_flag_interface_call tenv actuals call_flags callee_pname then + Domain.add_unannotated_call_access callee_pname loc pdesc astate + else astate in + let accesses_with_unannotated_calls = astate.accesses in let accesses = add_reads actuals loc accesses_with_unannotated_calls astate.locks astate.threads astate.ownership proc_data diff --git a/infer/src/concurrency/RacerDDomain.ml b/infer/src/concurrency/RacerDDomain.ml index d2fafe397..f060152d4 100644 --- a/infer/src/concurrency/RacerDDomain.ml +++ b/infer/src/concurrency/RacerDDomain.ml @@ -598,3 +598,9 @@ let pp fmt {threads; locks; accesses; ownership; attribute_map} = F.fprintf fmt "Threads: %a, Locks: %a @\nAccesses %a @\nOwnership: %a @\nAttributes: %a @\n" ThreadsDomain.pp threads LocksDomain.pp locks AccessDomain.pp accesses OwnershipDomain.pp ownership AttributeMapDomain.pp attribute_map + + +let add_unannotated_call_access pname loc pdesc (astate : t) = + let access = TraceElem.make_unannotated_call_access pname loc in + let snapshot = AccessSnapshot.make access astate.locks astate.threads False pdesc in + {astate with accesses= AccessDomain.add snapshot astate.accesses} diff --git a/infer/src/concurrency/RacerDDomain.mli b/infer/src/concurrency/RacerDDomain.mli index 41f0e321a..64d140122 100644 --- a/infer/src/concurrency/RacerDDomain.mli +++ b/infer/src/concurrency/RacerDDomain.mli @@ -43,8 +43,6 @@ module TraceElem : sig val make_container_access : AccessPath.t -> Typ.Procname.t -> is_write:bool -> Location.t -> t val make_field_access : AccessPath.t -> is_write:bool -> Location.t -> t - - val make_unannotated_call_access : Typ.Procname.t -> Location.t -> t end module PathDomain : @@ -225,3 +223,5 @@ val empty_summary : summary include AbstractDomain.WithBottom with type t := t val pp_summary : F.formatter -> summary -> unit + +val add_unannotated_call_access : Typ.Procname.t -> Location.t -> Procdesc.t -> t -> t diff --git a/infer/src/concurrency/RacerDModels.ml b/infer/src/concurrency/RacerDModels.ml index 7dd662ca6..ce8ae2129 100644 --- a/infer/src/concurrency/RacerDModels.ml +++ b/infer/src/concurrency/RacerDModels.ml @@ -150,27 +150,6 @@ let should_skip = false -(** return true if this function is library code from the JDK core libraries or Android *) -let is_java_library = function - | Typ.Procname.Java java_pname -> ( - match Typ.Procname.Java.get_package java_pname with - | Some package_name -> - String.is_prefix ~prefix:"java." package_name - || String.is_prefix ~prefix:"android." package_name - || String.is_prefix ~prefix:"com.google." package_name - | None -> - false ) - | _ -> - false - - -let is_builder_function = function - | Typ.Procname.Java java_pname -> - String.is_suffix ~suffix:"$Builder" (Typ.Procname.Java.get_class_name java_pname) - | _ -> - false - - let has_return_annot predicate pn = Annotations.pname_has_return_annot pn ~attrs_of_pname:Summary.proc_resolve_attributes predicate @@ -253,24 +232,6 @@ let acquires_ownership pname tenv = || PatternMatch.override_exists is_owned_in_library tenv pname -let is_threadsafe_collection pn tenv = - match pn with - | Typ.Procname.Java java_pname -> - let typename = Typ.Name.Java.from_string (Typ.Procname.Java.get_class_name java_pname) in - let aux tn _ = - match Typ.Name.name tn with - | "java.util.concurrent.ConcurrentMap" - | "java.util.concurrent.CopyOnWriteArrayList" - | "android.support.v4.util.Pools$SynchronizedPool" -> - true - | _ -> - false - in - PatternMatch.supertype_exists tenv aux typename - | _ -> - false - - (* return true if the given procname boxes a primitive type into a reference type *) let is_box = function | Typ.Procname.Java java_pname -> ( @@ -382,3 +343,104 @@ let is_thread_safe_method pname tenv = let is_marked_thread_safe pdesc tenv = let pname = Procdesc.get_proc_name pdesc in is_thread_safe_class pname tenv || is_thread_safe_method pname tenv + + +let is_safe_access access prefix_path tenv = + match (access, AccessPath.get_typ prefix_path tenv) with + | ( AccessPath.FieldAccess fieldname + , Some ({Typ.desc= Tstruct typename} | {desc= Tptr ({desc= Tstruct typename}, _)}) ) -> ( + match Tenv.lookup tenv typename with + | Some struct_typ -> + Annotations.struct_typ_has_annot 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 ) + | _ -> + false + + +let should_flag_interface_call tenv exp call_flags pname = + (* return true if this function is library code from the JDK core libraries or Android *) + let is_java_library = function + | Typ.Procname.Java java_pname -> ( + match Typ.Procname.Java.get_package java_pname with + | Some package_name -> + String.is_prefix ~prefix:"java." package_name + || String.is_prefix ~prefix:"android." package_name + || String.is_prefix ~prefix:"com.google." package_name + | None -> + false ) + | _ -> + false + in + let is_builder_function = function + | Typ.Procname.Java java_pname -> + String.is_suffix ~suffix:"$Builder" (Typ.Procname.Java.get_class_name java_pname) + | _ -> + false + in + let thread_safe_or_thread_confined annot = + Annotations.ia_is_thread_safe annot || Annotations.ia_is_thread_confined annot + in + call_flags.CallFlags.cf_interface && Typ.Procname.is_java pname + && (not (is_java_library pname || is_builder_function pname)) + (* can't ask anyone to annotate interfaces in library code, and Builder's should always be + thread-safe (would be unreasonable to ask everyone to annotate them) *) + && (not (PatternMatch.check_class_attributes thread_safe_or_thread_confined tenv pname)) + && (not (has_return_annot thread_safe_or_thread_confined pname)) + && + match exp with + | HilExp.AccessExpression receiver_access_exp :: _ -> ( + HilExp.AccessExpression.to_access_path receiver_access_exp + |> AccessPath.truncate + |> function + | receiver_prefix, Some receiver_field -> + is_safe_access receiver_field receiver_prefix tenv |> not + | _ -> + true ) + | _ -> + false + + +let is_synchronized_container callee_pname ((_, (base_typ : Typ.t)), accesses) tenv = + let is_threadsafe_collection pn tenv = + match pn with + | Typ.Procname.Java java_pname -> + let typename = Typ.Name.Java.from_string (Typ.Procname.Java.get_class_name java_pname) in + let aux tn _ = + match Typ.Name.name tn with + | "java.util.concurrent.ConcurrentMap" + | "java.util.concurrent.CopyOnWriteArrayList" + | "android.support.v4.util.Pools$SynchronizedPool" -> + true + | _ -> + false + in + PatternMatch.supertype_exists tenv aux typename + | _ -> + false + in + if is_threadsafe_collection callee_pname tenv then true + else + let is_annotated_synchronized base_typename container_field tenv = + match Tenv.lookup tenv base_typename with + | Some base_typ -> + Annotations.field_has_annot container_field base_typ + Annotations.ia_is_synchronized_collection + | None -> + false + in + match List.rev accesses with + | AccessPath.FieldAccess base_field :: AccessPath.FieldAccess container_field :: _ + when Typ.Procname.is_java callee_pname -> + let base_typename = Typ.Name.Java.from_string (Typ.Fieldname.Java.get_class base_field) in + is_annotated_synchronized base_typename container_field tenv + | [AccessPath.FieldAccess container_field] -> ( + match base_typ.desc with + | Typ.Tstruct base_typename | Tptr ({Typ.desc= Tstruct base_typename}, _) -> + is_annotated_synchronized base_typename container_field tenv + | _ -> + false ) + | _ -> + false diff --git a/infer/src/concurrency/RacerDModels.mli b/infer/src/concurrency/RacerDModels.mli index 792c68299..cbd3519ca 100644 --- a/infer/src/concurrency/RacerDModels.mli +++ b/infer/src/concurrency/RacerDModels.mli @@ -12,19 +12,12 @@ type container_access = ContainerRead | ContainerWrite val get_container_access : Typ.Procname.t -> Tenv.t -> container_access option (** return Some (access) if this procedure accesses the contents of a container (e.g., Map.get) *) -val is_java_library : Typ.Procname.t -> bool -(** return true if this function is library code from the JDK core libraries or Android *) - -val is_builder_function : Typ.Procname.t -> bool - val has_return_annot : (Annot.Item.t -> bool) -> Typ.Procname.t -> bool val is_functional : Typ.Procname.t -> bool val acquires_ownership : Typ.Procname.t -> Tenv.t -> bool -val is_threadsafe_collection : Typ.Procname.t -> Tenv.t -> bool - val is_box : Typ.Procname.t -> bool (** return true if the given procname boxes a primitive type into a reference type *) @@ -50,3 +43,12 @@ val is_thread_safe_method : Typ.Procname.t -> Tenv.t -> bool as an alias of @ThreadSafe in a .inferconfig file. *) val is_marked_thread_safe : Procdesc.t -> Tenv.t -> bool + +val is_safe_access : AccessPath.access -> AccessPath.t -> Tenv.t -> bool +(** check if an access to a field is thread-confined, or whether the field is volatile *) + +val should_flag_interface_call : Tenv.t -> HilExp.t list -> CallFlags.t -> Typ.Procname.t -> bool +(** should an interface call be flagged as potentially non-thread safe? *) + +val is_synchronized_container : Typ.Procname.t -> AccessPath.t -> Tenv.t -> bool +(** is a call on an access path to a method of a synchronized container? *)