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

[racerd] use set of access snapshots instead of map

Browse Source 
Reviewed By: ngorogiannis

Differential Revision: D7708831

fbshipit-source-id: e6b61cf
master
Sam Blackshear 7 years ago committed by Facebook Github Bot
parent 8069559bd8
commit 501577defc
3 changed files with 67 additions and 106 deletions
Show Stats Download Patch File Download Diff File

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

@ -134,8 +134,9 @@ 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 = AccessSnapshot.make locks threads False proc_data.pdesc in let access = TraceElem.make_unannotated_call_access pname loc in
AccessDomain.add_access pre (TraceElem.make_unannotated_call_access pname loc) attribute_map let snapshot = AccessSnapshot.make access locks threads False proc_data.pdesc in
AccessDomain.add snapshot attribute_map
else attribute_map else attribute_map
@ -155,21 +156,18 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| access :: access_list -> | access :: access_list ->
let prefix_path' = (fst prefix_path, snd prefix_path @ [access]) in let prefix_path' = (fst prefix_path, snd prefix_path @ [access]) in
let add_field_access pre = let add_field_access pre =
let is_write = if List.is_empty access_list then is_write_access else false in let access_acc' = AccessDomain.add pre access_acc in
let access_acc' =
AccessDomain.add_access pre
(TraceElem.make_field_access prefix_path' ~is_write loc)
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 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 access = TraceElem.make_field_access prefix_path' ~is_write loc in
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 =
AccessSnapshot.make locks threads AccessSnapshot.make access locks threads
(AccessSnapshot.OwnershipPrecondition.Conjunction formal_indexes) (AccessSnapshot.OwnershipPrecondition.Conjunction formal_indexes)
proc_data.pdesc proc_data.pdesc
in in
@ -177,7 +175,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| 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 = AccessSnapshot.make locks threads False proc_data.pdesc in let pre = AccessSnapshot.make access locks threads False proc_data.pdesc in
add_field_access pre add_field_access pre
in in
List.fold List.fold
@ -226,11 +224,11 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
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
in in
let pre = let snapshot =
AccessSnapshot.make astate.locks astate.threads AccessSnapshot.make container_access astate.locks astate.threads
(AccessSnapshot.OwnershipPrecondition.Conjunction (IntSet.singleton 0)) caller_pdesc (AccessSnapshot.OwnershipPrecondition.Conjunction (IntSet.singleton 0)) caller_pdesc
in in
AccessDomain.add_access pre container_access AccessDomain.empty AccessDomain.singleton snapshot
in in
(* if a container c is owned in cpp, make c[i] owned for all i *) (* if a container c is owned in cpp, make c[i] owned for all i *)
let return_ownership = let return_ownership =
@ -306,29 +304,16 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| None -> | None ->
path path
in in
let expand_pre accesses = let expand_pre (snapshot: AccessSnapshot.t) =
let sinks = let access = TraceElem.map ~f:expand_path snapshot.access in
PathDomain.Sinks.fold AccessSnapshot.make_ access snapshot.lock snapshot.thread snapshot.ownership_precondition
(fun elem acc ->
let new_elem = TraceElem.map ~f:expand_path elem in
PathDomain.Sinks.add new_elem acc )
(PathDomain.sinks accesses) PathDomain.Sinks.empty
in
PathDomain.update_sinks accesses sinks
in in
AccessDomain.map expand_pre accesses AccessDomain.map expand_pre accesses
let add_callee_accesses (caller_astate: Domain.astate) accesses locks threads actuals let add_callee_accesses (caller_astate: Domain.astate) callee_accesses locks threads actuals
callee_pname pdesc loc = callee_pname pdesc loc =
let open Domain in let open Domain in
let update_caller_accesses pre callee_accesses caller_accesses =
let combined_accesses =
PathDomain.with_callsite callee_accesses (CallSite.make callee_pname loc)
|> PathDomain.join (AccessDomain.get_accesses pre caller_accesses)
in
AccessDomain.add pre combined_accesses caller_accesses
in
let conjoin_ownership_pre actual_exp actual_indexes : AccessSnapshot.OwnershipPrecondition.t = let conjoin_ownership_pre actual_exp actual_indexes : AccessSnapshot.OwnershipPrecondition.t =
match actual_exp with match actual_exp with
| HilExp.Constant _ -> | HilExp.Constant _ ->
@ -375,29 +360,29 @@ 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: AccessSnapshot.t) callee_accesses accesses_acc = let update_callee_access (snapshot: AccessSnapshot.t) acc =
let access = TraceElem.with_callsite snapshot.access (CallSite.make callee_pname loc) in
let locks = if snapshot.lock then LocksDomain.add_lock locks else locks in
let thread =
ThreadsDomain.integrate_summary ~callee_astate:snapshot.thread ~caller_astate:threads
in
(* update precondition with caller ownership info *) (* update precondition with caller ownership info *)
let ownership_precondition' = let ownership_precondition =
match pre.ownership_precondition with match snapshot.ownership_precondition with
| Conjunction indexes -> | Conjunction indexes ->
let empty_pre = AccessSnapshot.OwnershipPrecondition.Conjunction IntSet.empty in let empty_pre = AccessSnapshot.OwnershipPrecondition.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 snapshot.ownership_precondition
in in
if AccessSnapshot.OwnershipPrecondition.is_true ownership_precondition' then accesses_acc if AccessSnapshot.OwnershipPrecondition.is_true ownership_precondition then
(* discard accesses to owned memory *)
acc
else else
let locks' = if pre.lock then LocksDomain.add_lock locks else locks in let snapshot = AccessSnapshot.make access locks thread ownership_precondition pdesc in
(* if the access occurred on a main thread in the callee, we should remember this when AccessDomain.add snapshot acc
moving it to the callee. if we don't know what thread it ran on, use the caller's
thread *)
let threads' =
ThreadsDomain.integrate_summary ~callee_astate:pre.thread ~caller_astate:threads
in
let pre' = AccessSnapshot.make locks' threads' ownership_precondition' pdesc in
update_caller_accesses pre' callee_accesses accesses_acc
in in
AccessDomain.fold update_accesses accesses caller_astate.accesses AccessDomain.fold update_callee_access callee_accesses caller_astate.accesses
(***********************************************************************) (***********************************************************************)
@ -949,9 +934,12 @@ let trace_of_pname orig_sink orig_pdesc callee_pname =
let orig_access = PathDomain.Sink.kind orig_sink in let orig_access = PathDomain.Sink.kind orig_sink in
match Summary.read_summary orig_pdesc callee_pname with match Summary.read_summary orig_pdesc callee_pname with
| Some {accesses} -> | Some {accesses} ->
get_all_accesses AccessDomain.fold
(fun access -> Access.matches ~caller:orig_access ~callee:(PathDomain.Sink.kind access)) (fun snapshot acc ->
accesses if Access.matches ~caller:orig_access ~callee:(PathDomain.Sink.kind snapshot.access) then
PathDomain.add_sink snapshot.access acc
else acc )
accesses PathDomain.empty
| _ -> | _ ->
PathDomain.empty PathDomain.empty
@ -1539,17 +1527,14 @@ let make_results_table (module AccessListMap : QuotientedAccessListMap) file_env
let open RacerDDomain in let open RacerDDomain in
let aggregate_post {threads; accesses; wobbly_paths} tenv procdesc acc = let aggregate_post {threads; accesses; wobbly_paths} tenv procdesc acc =
AccessDomain.fold AccessDomain.fold
(fun precondition accesses acc -> (fun snapshot acc ->
PathDomain.Sinks.fold let access_kind = TraceElem.kind snapshot.access in
(fun access acc -> if should_filter_access access_kind then acc
let access_kind = TraceElem.kind access in else
if should_filter_access access_kind then acc let reported_access : reported_access =
else {access= snapshot.access; threads; precondition= snapshot; tenv; procdesc; wobbly_paths}
let reported_access : reported_access = in
{access; threads; precondition; tenv; procdesc; wobbly_paths} AccessListMap.add access_kind reported_access acc )
in
AccessListMap.add access_kind reported_access acc )
(PathDomain.sinks accesses) acc )
accesses acc accesses acc
in in
let aggregate_posts acc (tenv, proc_desc) = let aggregate_posts acc (tenv, proc_desc) =

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

@ -420,15 +420,22 @@ module AccessSnapshot = struct
end end
type t = type t =
{thread: ThreadsDomain.astate; lock: bool; ownership_precondition: OwnershipPrecondition.t} { access: PathDomain.Sink.t
; thread: ThreadsDomain.astate
; lock: bool
; ownership_precondition: OwnershipPrecondition.t }
[@@deriving compare] [@@deriving compare]
let make lock thread ownership_precondition pdesc = let make_ access lock thread ownership_precondition =
(* shouldn't be creating metadata for accesses that are known to be owned; we should discard (* shouldn't be creating metadata for accesses that are known to be owned; we should discard
such accesses *) such accesses *)
assert (not (OwnershipPrecondition.is_true ownership_precondition)) ; assert (not (OwnershipPrecondition.is_true ownership_precondition)) ;
{access; thread; lock; ownership_precondition}
let make access lock thread ownership_precondition pdesc =
let lock = LocksDomain.is_locked lock || Procdesc.is_java_synchronized pdesc in let lock = LocksDomain.is_locked lock || Procdesc.is_java_synchronized pdesc in
{thread; lock; ownership_precondition} make_ access lock thread ownership_precondition
let is_unprotected {thread; lock; ownership_precondition} = let is_unprotected {thread; lock; ownership_precondition} =
@ -436,25 +443,12 @@ module AccessSnapshot = struct
&& not (OwnershipPrecondition.is_true ownership_precondition) && not (OwnershipPrecondition.is_true ownership_precondition)
let pp fmt {thread; lock; ownership_precondition} = let pp fmt {access; thread; lock; ownership_precondition} =
F.fprintf fmt "Thread: %a Lock: %b Pre: %a" ThreadsDomain.pp thread lock F.fprintf fmt "Access: %a Thread: %a Lock: %b Pre: %a" TraceElem.pp access ThreadsDomain.pp
OwnershipPrecondition.pp ownership_precondition thread lock OwnershipPrecondition.pp ownership_precondition
end end
module AccessDomain = struct module AccessDomain = AbstractDomain.FiniteSet (AccessSnapshot)
include AbstractDomain.Map (AccessSnapshot) (PathDomain)
let add_access precondition access_path t =
let precondition_accesses =
try find precondition t with Caml.Not_found -> PathDomain.empty
in
let precondition_accesses' = PathDomain.add_sink access_path precondition_accesses in
add precondition precondition_accesses' t
let get_accesses precondition t =
try find precondition t with Caml.Not_found -> PathDomain.empty
end
module StabilityDomain = struct module StabilityDomain = struct
include AccessTree.PathSet (AccessTree.DefaultConfig) include AccessTree.PathSet (AccessTree.DefaultConfig)
@ -684,17 +678,3 @@ let rec ownership_of_expr expr ownership =
ownership_of_expr e ownership ownership_of_expr e ownership
| _ -> | _ ->
OwnershipAbstractValue.unowned OwnershipAbstractValue.unowned
let filter_by_access access_filter trace =
PathDomain.Sinks.filter access_filter (PathDomain.sinks trace) |> PathDomain.update_sinks trace
let get_all_accesses_with_pre pre_filter access_filter accesses =
AccessDomain.fold
(fun pre trace acc ->
if pre_filter pre then PathDomain.join (filter_by_access access_filter trace) acc else acc )
accesses PathDomain.empty
let get_all_accesses = get_all_accesses_with_pre (fun _ -> true)

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

@ -176,11 +176,17 @@ module AccessSnapshot : sig
end end
type t = private type t = private
{thread: ThreadsDomain.astate; lock: bool; ownership_precondition: OwnershipPrecondition.t} { access: PathDomain.Sink.t
; thread: ThreadsDomain.astate
; lock: bool
; ownership_precondition: OwnershipPrecondition.t }
[@@deriving compare] [@@deriving compare]
val make : val make :
LocksDomain.astate -> ThreadsDomain.astate -> OwnershipPrecondition.t -> Procdesc.t -> t PathDomain.Sink.t -> LocksDomain.astate -> ThreadsDomain.astate -> OwnershipPrecondition.t
-> Procdesc.t -> t
val make_ : PathDomain.Sink.t -> bool -> ThreadsDomain.astate -> OwnershipPrecondition.t -> t
val is_unprotected : t -> bool val is_unprotected : t -> bool
(** return true if not protected by lock, thread, or ownership *) (** return true if not protected by lock, thread, or ownership *)
@ -190,15 +196,7 @@ 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 : module type of AbstractDomain.FiniteSet (AccessSnapshot)
include module type of AbstractDomain.Map (AccessSnapshot) (PathDomain)
val add_access : AccessSnapshot.t -> TraceElem.t -> astate -> astate
(** add the given (access, precondition) pair to the map *)
val get_accesses : AccessSnapshot.t -> astate -> PathDomain.astate
(** get all accesses with the given snapshot *)
end
module StabilityDomain : sig module StabilityDomain : sig
include module type of AccessTree.PathSet (AccessTree.DefaultConfig) include module type of AccessTree.PathSet (AccessTree.DefaultConfig)
@ -244,5 +242,3 @@ val attributes_of_expr :
val ownership_of_expr : val ownership_of_expr :
HilExp.t -> OwnershipAbstractValue.astate AttributeMapDomain.t -> OwnershipAbstractValue.astate HilExp.t -> OwnershipAbstractValue.astate AttributeMapDomain.t -> OwnershipAbstractValue.astate
val get_all_accesses : (TraceElem.t -> bool) -> PathDomain.t AccessDomain.t -> PathDomain.t

Write Preview
Loading…
Cancel
Save