pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[racerd] move models and domain operations to respective source files

Browse Source 
Reviewed By: mbouaziz

Differential Revision: D13537501

fbshipit-source-id: 88dbc022d
master
Nikos Gorogiannis 6 years ago committed by Facebook Github Bot
parent 11373c8a6b
commit ddc15ad663
5 changed files with 126 additions and 132 deletions
Show Stats Download Patch File Download Diff File

92
infer/src/concurrency/RacerD.ml
Unescape View File

@ -24,56 +24,6 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
type extras = ProcData.no_extras 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 let add_access exp loc ~is_write_access accesses locks threads ownership
(proc_data : extras ProcData.t) = (proc_data : extras ProcData.t) =
let open Domain in let open Domain in
@ -86,7 +36,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let access_acc' = AccessDomain.add pre access_acc in let access_acc' = AccessDomain.add pre access_acc in
add_field_accesses prefix_path' access_acc' access_list add_field_accesses prefix_path' access_acc' access_list
in 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 add_field_accesses prefix_path' access_acc access_list
else else
let is_write = if List.is_empty access_list then is_write_access else false in 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) ~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 let make_container_access callee_pname ~is_write receiver_ap callee_loc tenv caller_pdesc
(astate : Domain.t) = (astate : Domain.t) =
(* create a dummy write that represents mutating the contents of the container *) (* create a dummy write that represents mutating the contents of the container *)
let open Domain in let open Domain in
let callee_accesses = 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 else
let container_access = let container_access =
TraceElem.make_container_access receiver_ap ~is_write callee_pname callee_loc 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} {astate with accesses; ownership}
| Call (ret_base, Direct callee_pname, actuals, call_flags, loc) -> | Call (ret_base, Direct callee_pname, actuals, call_flags, loc) ->
let ret_access_path = (ret_base, []) in let ret_access_path = (ret_base, []) in
let accesses_with_unannotated_calls = let astate =
add_unannotated_call_access callee_pname actuals call_flags loc tenv ~locks:astate.locks if RacerDModels.should_flag_interface_call tenv actuals call_flags callee_pname then
~threads:astate.threads astate.accesses proc_data Domain.add_unannotated_call_access callee_pname loc pdesc astate
else astate
in in
let accesses_with_unannotated_calls = astate.accesses in
let accesses = let accesses =
add_reads actuals loc accesses_with_unannotated_calls astate.locks astate.threads add_reads actuals loc accesses_with_unannotated_calls astate.locks astate.threads
astate.ownership proc_data astate.ownership proc_data

6
infer/src/concurrency/RacerDDomain.ml
Unescape View File

@ -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" 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 ThreadsDomain.pp threads LocksDomain.pp locks AccessDomain.pp accesses OwnershipDomain.pp
ownership AttributeMapDomain.pp attribute_map 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}

4
infer/src/concurrency/RacerDDomain.mli
Unescape View File

@ -43,8 +43,6 @@ module TraceElem : sig
val make_container_access : AccessPath.t -> Typ.Procname.t -> is_write:bool -> Location.t -> t 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_field_access : AccessPath.t -> is_write:bool -> Location.t -> t
val make_unannotated_call_access : Typ.Procname.t -> Location.t -> t
end end
module PathDomain : module PathDomain :
@ -225,3 +223,5 @@ val empty_summary : summary
include AbstractDomain.WithBottom with type t := t include AbstractDomain.WithBottom with type t := t
val pp_summary : F.formatter -> summary -> unit val pp_summary : F.formatter -> summary -> unit
val add_unannotated_call_access : Typ.Procname.t -> Location.t -> Procdesc.t -> t -> t

140
infer/src/concurrency/RacerDModels.ml
Unescape View File

@ -150,27 +150,6 @@ let should_skip =
false 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 = let has_return_annot predicate pn =
Annotations.pname_has_return_annot pn ~attrs_of_pname:Summary.proc_resolve_attributes predicate 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 || 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 *) (* return true if the given procname boxes a primitive type into a reference type *)
let is_box = function let is_box = function
| Typ.Procname.Java java_pname -> ( | Typ.Procname.Java java_pname -> (
@ -382,3 +343,104 @@ let is_thread_safe_method pname tenv =
let is_marked_thread_safe pdesc tenv = let is_marked_thread_safe pdesc tenv =
let pname = Procdesc.get_proc_name pdesc in let pname = Procdesc.get_proc_name pdesc in
is_thread_safe_class pname tenv || is_thread_safe_method pname tenv 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

16
infer/src/concurrency/RacerDModels.mli
Unescape View File

@ -12,19 +12,12 @@ type container_access = ContainerRead | ContainerWrite
val get_container_access : Typ.Procname.t -> Tenv.t -> container_access option 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) *) (** 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 has_return_annot : (Annot.Item.t -> bool) -> Typ.Procname.t -> bool
val is_functional : Typ.Procname.t -> bool val is_functional : Typ.Procname.t -> bool
val acquires_ownership : Typ.Procname.t -> Tenv.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 val is_box : Typ.Procname.t -> bool
(** return true if the given procname boxes a primitive type into a reference type *) (** 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. *) as an alias of @ThreadSafe in a .inferconfig file. *)
val is_marked_thread_safe : Procdesc.t -> Tenv.t -> bool 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? *)

Write Preview
Loading…
Cancel
Save