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

[infer] `AccessData` -> `AccessSnapshot`

Browse Source 
Reviewed By: ngorogiannis

Differential Revision: D7678073

fbshipit-source-id: fd10e41
master
Sam Blackshear 7 years ago committed by Facebook Github Bot
parent 1d792f0b48
commit fb4f9a286a
3 changed files with 26 additions and 26 deletions
Show Stats Download Patch File Download Diff File

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

@ -134,7 +134,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
&& not (is_receiver_safe actuals) && not (is_receiver_safe actuals)
then then
let open Domain in let open Domain in
let pre = AccessData.make locks threads False proc_data.pdesc in let pre = AccessSnapshot.make locks threads False proc_data.pdesc in
AccessDomain.add_access pre (TraceElem.make_unannotated_call_access pname loc) attribute_map AccessDomain.add_access pre (TraceElem.make_unannotated_call_access pname loc) attribute_map
else attribute_map else attribute_map
@ -169,14 +169,14 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
match OwnershipDomain.get_owned prefix_path ownership with match OwnershipDomain.get_owned prefix_path ownership with
| OwnershipAbstractValue.OwnedIf formal_indexes -> | OwnershipAbstractValue.OwnedIf formal_indexes ->
let pre = let pre =
AccessData.make locks threads AccessSnapshot.make locks threads
(AccessData.Precondition.Conjunction formal_indexes) proc_data.pdesc (AccessSnapshot.Precondition.Conjunction formal_indexes) proc_data.pdesc
in in
add_field_access pre add_field_access pre
| OwnershipAbstractValue.Owned -> | OwnershipAbstractValue.Owned ->
add_field_accesses prefix_path' access_acc access_list add_field_accesses prefix_path' access_acc access_list
| OwnershipAbstractValue.Unowned -> | OwnershipAbstractValue.Unowned ->
let pre = AccessData.make locks threads False proc_data.pdesc in let pre = AccessSnapshot.make locks threads False proc_data.pdesc in
add_field_access pre add_field_access pre
in in
List.fold List.fold
@ -226,8 +226,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
TraceElem.make_container_access receiver_ap ~is_write callee_pname callee_loc TraceElem.make_container_access receiver_ap ~is_write callee_pname callee_loc
in in
let pre = let pre =
AccessData.make astate.locks astate.threads AccessSnapshot.make astate.locks astate.threads
(AccessData.Precondition.Conjunction (IntSet.singleton 0)) caller_pdesc (AccessSnapshot.Precondition.Conjunction (IntSet.singleton 0)) caller_pdesc
in in
AccessDomain.add_access pre container_access AccessDomain.empty AccessDomain.add_access pre container_access AccessDomain.empty
in in
@ -328,7 +328,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
in in
AccessDomain.add pre combined_accesses caller_accesses AccessDomain.add pre combined_accesses caller_accesses
in in
let conjoin_ownership_pre actual_exp actual_indexes : AccessData.Precondition.t = let conjoin_ownership_pre actual_exp actual_indexes : AccessSnapshot.Precondition.t =
match actual_exp with match actual_exp with
| HilExp.Constant _ -> | HilExp.Constant _ ->
(* the actual is a constant, so it's owned in the caller. *) (* the actual is a constant, so it's owned in the caller. *)
@ -360,7 +360,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
(* couldn't find access path, don't know if it's owned. assume not *) (* couldn't find access path, don't know if it's owned. assume not *)
False False
in in
let update_ownership_pre actual_index (acc: AccessData.Precondition.t) = let update_ownership_pre actual_index (acc: AccessSnapshot.Precondition.t) =
match acc with match acc with
| False -> | False ->
(* precondition can't be satisfied *) (* precondition can't be satisfied *)
@ -374,24 +374,24 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
Typ.Procname.pp callee_pname (List.length actuals) ; Typ.Procname.pp callee_pname (List.length actuals) ;
acc acc
in in
let update_accesses (pre: AccessData.t) callee_accesses accesses_acc = let update_accesses (pre: AccessSnapshot.t) callee_accesses accesses_acc =
(* update precondition with caller ownership info *) (* update precondition with caller ownership info *)
let ownership_precondition' = let ownership_precondition' =
match pre.ownership_precondition with match pre.ownership_precondition with
| Conjunction indexes -> | Conjunction indexes ->
let empty_pre = AccessData.Precondition.Conjunction IntSet.empty in let empty_pre = AccessSnapshot.Precondition.Conjunction IntSet.empty in
IntSet.fold update_ownership_pre indexes empty_pre IntSet.fold update_ownership_pre indexes empty_pre
| False -> | False ->
pre.ownership_precondition pre.ownership_precondition
in in
if AccessData.Precondition.is_true ownership_precondition' then accesses_acc if AccessSnapshot.Precondition.is_true ownership_precondition' then accesses_acc
else else
let locks' = if pre.lock then LocksDomain.add_lock locks else locks in let locks' = if pre.lock then LocksDomain.add_lock locks else locks in
(* if the access occurred on a main thread in the callee, we should remember this when (* if the access occurred on a main thread in the callee, we should remember this when
moving it to the callee. if we don't know what thread it ran on, use the caller's moving it to the callee. if we don't know what thread it ran on, use the caller's
thread *) thread *)
let threads' = if pre.thread then ThreadsDomain.AnyThreadButSelf else threads in let threads' = if pre.thread then ThreadsDomain.AnyThreadButSelf else threads in
let pre' = AccessData.make locks' threads' ownership_precondition' pdesc in let pre' = AccessSnapshot.make locks' threads' ownership_precondition' pdesc in
update_caller_accesses pre' callee_accesses accesses_acc update_caller_accesses pre' callee_accesses accesses_acc
in in
AccessDomain.fold update_accesses accesses caller_astate.accesses AccessDomain.fold update_accesses accesses caller_astate.accesses
@ -1125,7 +1125,7 @@ let make_unprotected_write_description pname final_sink_site initial_sink_site f
type reported_access = type reported_access =
{ access: RacerDDomain.TraceElem.t { access: RacerDDomain.TraceElem.t
; threads: RacerDDomain.ThreadsDomain.astate ; threads: RacerDDomain.ThreadsDomain.astate
; precondition: RacerDDomain.AccessData.t ; precondition: RacerDDomain.AccessSnapshot.t
; tenv: Tenv.t ; tenv: Tenv.t
; procdesc: Procdesc.t ; procdesc: Procdesc.t
; wobbly_paths: RacerDDomain.StabilityDomain.astate } ; wobbly_paths: RacerDDomain.StabilityDomain.astate }
@ -1231,7 +1231,7 @@ let report_unsafe_accesses (aggregated_access_map: reported_access list AccessLi
match TraceElem.kind access with match TraceElem.kind access with
| Access.InterfaceCall unannoted_call_pname -> | Access.InterfaceCall unannoted_call_pname ->
if if
AccessData.is_unprotected precondition && ThreadsDomain.is_any threads AccessSnapshot.is_unprotected precondition && ThreadsDomain.is_any threads
&& Models.is_marked_thread_safe procdesc tenv && Models.is_marked_thread_safe procdesc tenv
then ( then (
(* un-annotated interface call + no lock in method marked thread-safe. warn *) (* un-annotated interface call + no lock in method marked thread-safe. warn *)
@ -1258,7 +1258,7 @@ let report_unsafe_accesses (aggregated_access_map: reported_access list AccessLi
accesses accesses
in in
if if
AccessData.is_unprotected precondition AccessSnapshot.is_unprotected precondition
&& (not (List.is_empty writes_on_background_thread) || ThreadsDomain.is_any threads) && (not (List.is_empty writes_on_background_thread) || ThreadsDomain.is_any threads)
then ( then (
let conflict = List.hd writes_on_background_thread in let conflict = List.hd writes_on_background_thread in
@ -1271,11 +1271,11 @@ let report_unsafe_accesses (aggregated_access_map: reported_access list AccessLi
(* Do not report unprotected writes when an access can't run in parallel with itself, or (* Do not report unprotected writes when an access can't run in parallel with itself, or
for ObjC_Cpp *) for ObjC_Cpp *)
reported_acc ) reported_acc )
| (Access.Read _ | ContainerRead _) when AccessData.is_unprotected precondition -> | (Access.Read _ | ContainerRead _) when AccessSnapshot.is_unprotected precondition ->
(* unprotected read. report all writes as conflicts for java. for c++ filter out (* unprotected read. report all writes as conflicts for java. for c++ filter out
unprotected writes *) unprotected writes *)
let is_cpp_protected_write pre = let is_cpp_protected_write pre =
Typ.Procname.is_java pname || not (AccessData.is_unprotected pre) Typ.Procname.is_java pname || not (AccessSnapshot.is_unprotected pre)
in in
let is_conflict other_access pre other_thread = let is_conflict other_access pre other_thread =
TraceElem.is_write other_access TraceElem.is_write other_access
@ -1299,7 +1299,7 @@ let report_unsafe_accesses (aggregated_access_map: reported_access list AccessLi
else reported_acc else reported_acc
| Access.Read _ | ContainerRead _ -> | Access.Read _ | ContainerRead _ ->
(* protected read. report unprotected writes and opposite protected writes as conflicts *) (* protected read. report unprotected writes and opposite protected writes as conflicts *)
let can_conflict (pre1: AccessData.t) (pre2: AccessData.t) = let can_conflict (pre1: AccessSnapshot.t) (pre2: AccessSnapshot.t) =
if pre1.lock && pre2.lock then false if pre1.lock && pre2.lock then false
else if pre1.thread && pre2.thread then false else if pre1.thread && pre2.thread then false
else true else true
@ -1310,7 +1310,7 @@ let report_unsafe_accesses (aggregated_access_map: reported_access list AccessLi
(fun { access= other_access (fun { access= other_access
; precondition= other_precondition ; precondition= other_precondition
; threads= other_threads } -> ; threads= other_threads } ->
if AccessData.is_unprotected other_precondition then if AccessSnapshot.is_unprotected other_precondition then
TraceElem.is_write other_access && ThreadsDomain.is_any other_threads TraceElem.is_write other_access && ThreadsDomain.is_any other_threads
else else
TraceElem.is_write other_access && can_conflict precondition other_precondition TraceElem.is_write other_access && can_conflict precondition other_precondition

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

@ -393,7 +393,7 @@ module AttributeMapDomain = struct
add access_path attribute_set t add access_path attribute_set t
end end
module AccessData = struct module AccessSnapshot = struct
module Precondition = struct module Precondition = struct
type t = Conjunction of IntSet.t | False [@@deriving compare] type t = Conjunction of IntSet.t | False [@@deriving compare]
@ -429,7 +429,7 @@ module AccessData = struct
end end
module AccessDomain = struct module AccessDomain = struct
include AbstractDomain.Map (AccessData) (PathDomain) include AbstractDomain.Map (AccessSnapshot) (PathDomain)
let add_access precondition access_path t = let add_access precondition access_path t =
let precondition_accesses = let precondition_accesses =

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

@ -153,7 +153,7 @@ module AttributeMapDomain : sig
end end
(** Data shared among a set of accesses: current thread, lock(s) held, ownership precondition *) (** Data shared among a set of accesses: current thread, lock(s) held, ownership precondition *)
module AccessData : sig module AccessSnapshot : sig
(** Precondition for owned access; access is owned if it evaluates to ture *) (** Precondition for owned access; access is owned if it evaluates to ture *)
module Precondition : sig module Precondition : sig
type t = type t =
@ -183,13 +183,13 @@ end
(** map of access metadata |-> set of accesses. the map should hold all accesses to a (** map of access metadata |-> set of accesses. the map should hold all accesses to a
possibly-unowned access path *) possibly-unowned access path *)
module AccessDomain : sig module AccessDomain : sig
include module type of AbstractDomain.Map (AccessData) (PathDomain) include module type of AbstractDomain.Map (AccessSnapshot) (PathDomain)
val add_access : AccessData.t -> TraceElem.t -> astate -> astate val add_access : AccessSnapshot.t -> TraceElem.t -> astate -> astate
(** add the given (access, precondition) pair to the map *) (** add the given (access, precondition) pair to the map *)
val get_accesses : AccessData.t -> astate -> PathDomain.astate val get_accesses : AccessSnapshot.t -> astate -> PathDomain.astate
(** get all accesses with the given precondition *) (** get all accesses with the given snapshot *)
end end
module StabilityDomain : sig module StabilityDomain : sig

Write Preview
Loading…
Cancel
Save