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

[racerd][2/n] invert inclusion between AccessSnapshot and TraceElem

Browse Source 
Summary:
For historical reasons, the record of an access is a three-level record:
1. `AccessSnapshot`, a record with info such as ownership and lock status, including
2. `TraceElem`, a record with a trace and an element which is
3. Access, the abstract addressed accessed and the type of access.

This stack flips the order to 2, 1, 3, leading up to the possibility of merging 1 and 3.

This diff inverts 2 and 1.

Reviewed By: skcho

Differential Revision: D20644100

fbshipit-source-id: 89d810b68
master
Nikos Gorogiannis 5 years ago committed by Facebook GitHub Bot
parent 8446e46103
commit b194d70860
4 changed files with 82 additions and 105 deletions
Show Stats Download Patch File Download Diff File

5
infer/src/concurrency/ExplicitTrace.ml
Unescape View File

@ -68,7 +68,10 @@ module MakeTraceElemWithComparator
let compare {elem; loc} {elem= elem'; loc= loc'} = Comp.comparator elem loc elem' loc' let compare {elem; loc} {elem= elem'; loc= loc'} = Comp.comparator elem loc elem' loc'
let pp fmt {elem} = Elem.pp fmt elem let pp fmt {elem; loc; trace} =
let pp_trace fmt trace = PrettyPrintable.pp_collection ~pp_item:CallSite.pp fmt trace in
F.fprintf fmt "{elem= %a; loc= %a; trace= %a}" Elem.pp elem Location.pp loc pp_trace trace
let describe fmt {elem} = Elem.describe fmt elem let describe fmt {elem} = Elem.describe fmt elem
end end

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

@ -115,6 +115,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let add_callee_accesses formals (caller_astate : Domain.t) callee_accesses locks threads actuals let add_callee_accesses formals (caller_astate : Domain.t) callee_accesses locks threads actuals
callee_pname loc = callee_pname loc =
let open Domain in let open Domain in
let callsite = CallSite.make callee_pname loc in
let actuals_ownership = let actuals_ownership =
(* precompute array holding ownership of each actual for fast random access *) (* precompute array holding ownership of each actual for fast random access *)
Array.of_list_map actuals ~f:(fun actual_exp -> Array.of_list_map actuals ~f:(fun actual_exp ->
@ -129,15 +130,15 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let update_callee_access (snapshot : AccessSnapshot.t) acc = let update_callee_access (snapshot : AccessSnapshot.t) acc =
(* update precondition with caller ownership info *) (* update precondition with caller ownership info *)
let ownership_precondition = let ownership_precondition =
match snapshot.ownership_precondition with match snapshot.elem.ownership_precondition with
| OwnedIf indexes -> | OwnedIf indexes ->
IntSet.fold update_ownership_precondition indexes OwnershipAbstractValue.owned IntSet.fold update_ownership_precondition indexes OwnershipAbstractValue.owned
| Unowned -> | Unowned ->
snapshot.ownership_precondition snapshot.elem.ownership_precondition
in in
let snapshot_opt = let snapshot_opt =
AccessSnapshot.update_callee_access formals snapshot callee_pname loc ownership_precondition AccessSnapshot.update_callee_access formals snapshot callsite ownership_precondition threads
threads locks locks
in in
AccessDomain.add_opt snapshot_opt acc AccessDomain.add_opt snapshot_opt acc
in in
@ -614,7 +615,7 @@ let describe_exp = MF.wrap_monospaced RacerDDomain.pp_exp
let describe_pname = MF.wrap_monospaced (Procname.pp_simplified_string ~withclass:true) let describe_pname = MF.wrap_monospaced (Procname.pp_simplified_string ~withclass:true)
let pp_access fmt (t : RacerDDomain.AccessSnapshot.t) = let pp_access fmt (t : RacerDDomain.AccessSnapshot.t) =
match t.access.elem with match t.elem.access with
| Read {exp} | Write {exp} -> | Read {exp} | Write {exp} ->
describe_exp fmt exp describe_exp fmt exp
| ContainerRead {exp; pname} | ContainerWrite {exp; pname} -> | ContainerRead {exp; pname} | ContainerWrite {exp; pname} ->
@ -661,9 +662,8 @@ type reported_access =
let report_thread_safety_violation ~issue_log ~make_description ~report_kind let report_thread_safety_violation ~issue_log ~make_description ~report_kind
({threads; snapshot; tenv; procname= pname} : reported_access) = ({threads; snapshot; tenv; procname= pname} : reported_access) =
let open RacerDDomain in let open RacerDDomain in
let access = snapshot.access in let final_pname = List.last snapshot.trace |> Option.value_map ~default:pname ~f:CallSite.pname in
let final_pname = List.last access.trace |> Option.value_map ~default:pname ~f:CallSite.pname in let final_sink_site = CallSite.make final_pname snapshot.loc in
let final_sink_site = CallSite.make final_pname access.loc in
let initial_sink_site = CallSite.make pname (AccessSnapshot.get_loc snapshot) in let initial_sink_site = CallSite.make pname (AccessSnapshot.get_loc snapshot) in
let loc = CallSite.loc initial_sink_site in let loc = CallSite.loc initial_sink_site in
let ltr, original_end, conflict_end = make_trace ~report_kind snapshot in let ltr, original_end, conflict_end = make_trace ~report_kind snapshot in
@ -805,7 +805,7 @@ end = struct
let empty = M.empty let empty = M.empty
let add (rep : reported_access) map = let add (rep : reported_access) map =
let access = rep.snapshot.access.elem in let access = rep.snapshot.elem.access in
if RacerDDomain.Access.get_access_exp access |> should_filter_access then map if RacerDDomain.Access.get_access_exp access |> should_filter_access then map
else else
let k = Key.of_access access in let k = Key.of_access access in
@ -856,13 +856,13 @@ let should_report_guardedby_violation classname ({snapshot; tenv; procname} : re
| _ -> | _ ->
false ) false )
in in
(not snapshot.lock) (not snapshot.elem.lock)
&& RacerDDomain.AccessSnapshot.is_write snapshot && RacerDDomain.AccessSnapshot.is_write snapshot
&& Procname.is_java procname && Procname.is_java procname
&& &&
(* restrict check to access paths of length one *) (* restrict check to access paths of length one *)
match match
RacerDDomain.Access.get_access_exp snapshot.access.elem RacerDDomain.Access.get_access_exp snapshot.elem.access
|> Option.map ~f:AccessExpression.to_accesses |> Option.map ~f:AccessExpression.to_accesses
|> Option.map ~f:(fun (base, accesses) -> |> Option.map ~f:(fun (base, accesses) ->
(base, List.filter accesses ~f:HilExp.Access.is_field_or_array_access) ) (base, List.filter accesses ~f:HilExp.Access.is_field_or_array_access) )
@ -918,7 +918,7 @@ let report_unsafe_accesses ~issue_log classname (aggregated_access_map : ReportM
if Config.deduplicate then if Config.deduplicate then
CallSite.Set.mem call_site reported_sites CallSite.Set.mem call_site reported_sites
|| ||
match snapshot.access.TraceElem.elem with match snapshot.elem.access with
| Access.Write _ | Access.ContainerWrite _ -> | Access.Write _ | Access.ContainerWrite _ ->
Procname.Set.mem pname reported_writes Procname.Set.mem pname reported_writes
| Access.Read _ | Access.ContainerRead _ -> | Access.Read _ | Access.ContainerRead _ ->
@ -931,7 +931,7 @@ let report_unsafe_accesses ~issue_log classname (aggregated_access_map : ReportM
if Config.deduplicate then if Config.deduplicate then
let call_site = CallSite.make pname (AccessSnapshot.get_loc snapshot) in let call_site = CallSite.make pname (AccessSnapshot.get_loc snapshot) in
let reported_sites = CallSite.Set.add call_site reported.reported_sites in let reported_sites = CallSite.Set.add call_site reported.reported_sites in
match snapshot.access.TraceElem.elem with match snapshot.elem.access with
| Access.Write _ | Access.ContainerWrite _ -> | Access.Write _ | Access.ContainerWrite _ ->
let reported_writes = Procname.Set.add pname reported.reported_writes in let reported_writes = Procname.Set.add pname reported.reported_writes in
{reported with reported_writes; reported_sites} {reported with reported_writes; reported_sites}
@ -965,7 +965,7 @@ let report_unsafe_accesses ~issue_log classname (aggregated_access_map : ReportM
in in
let report_unsafe_access accesses acc let report_unsafe_access accesses acc
({snapshot; threads; tenv; procname= pname} as reported_access) = ({snapshot; threads; tenv; procname= pname} as reported_access) =
match snapshot.access.elem with match snapshot.elem.access with
| Access.InterfaceCall reported_pname | Access.InterfaceCall reported_pname
when AccessSnapshot.is_unprotected snapshot when AccessSnapshot.is_unprotected snapshot
&& ThreadsDomain.is_any threads && is_marked_thread_safe pname tenv -> && ThreadsDomain.is_any threads && is_marked_thread_safe pname tenv ->
@ -1017,8 +1017,8 @@ let report_unsafe_accesses ~issue_log classname (aggregated_access_map : ReportM
| 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 (snapshot1 : AccessSnapshot.t) (snapshot2 : AccessSnapshot.t) = let can_conflict (snapshot1 : AccessSnapshot.t) (snapshot2 : AccessSnapshot.t) =
if snapshot1.lock && snapshot2.lock then false if snapshot1.elem.lock && snapshot2.elem.lock then false
else ThreadsDomain.can_conflict snapshot1.thread snapshot2.thread else ThreadsDomain.can_conflict snapshot1.elem.thread snapshot2.elem.thread
in in
let is_conflict {snapshot= other_snapshot; threads= other_threads} = let is_conflict {snapshot= other_snapshot; threads= other_threads} =
if AccessSnapshot.is_unprotected other_snapshot then if AccessSnapshot.is_unprotected other_snapshot then

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

@ -44,6 +44,8 @@ module Access = struct
if is_write then ContainerWrite {exp; pname} else ContainerRead {exp; pname} if is_write then ContainerWrite {exp; pname} else ContainerRead {exp; pname}
let make_unannotated_call_access pname = InterfaceCall pname
let is_write = function let is_write = function
| InterfaceCall _ | Read _ | ContainerRead _ -> | InterfaceCall _ | Read _ | ContainerRead _ ->
false false
@ -130,31 +132,6 @@ module CallPrinter = struct
let pp fmt cs = F.fprintf fmt "call to %a" Procname.pp (CallSite.pname cs) let pp fmt cs = F.fprintf fmt "call to %a" Procname.pp (CallSite.pname cs)
end end
module TraceElem = struct
include ExplicitTrace.MakeTraceElemModuloLocation (Access) (CallPrinter)
(** This choice means the comparator is insensitive to the location access. This preserves
correctness only if the overlying comparator (AccessSnapshot) takes into account the
characteristics of the access (eg lock status). *)
let is_write {elem} = Access.is_write elem
let is_container_write {elem} = Access.is_container_write elem
let should_keep formals {elem} = Access.should_keep formals elem
let map_access ~f trace_elem = map ~f:(Access.map ~f) trace_elem
let make_container_access access_exp pname ~is_write loc =
make (Access.make_container_access access_exp pname ~is_write) loc
let make_field_access access_exp ~is_write loc =
make (Access.make_field_access access_exp ~is_write) loc
let make_unannotated_call_access pname loc = make (Access.InterfaceCall pname) loc
end
module LocksDomain = struct module LocksDomain = struct
include AbstractDomain.CountDomain (struct include AbstractDomain.CountDomain (struct
(** arbitrary threshold for max locks we expect to be held simultaneously *) (** arbitrary threshold for max locks we expect to be held simultaneously *)
@ -281,83 +258,85 @@ module OwnershipAbstractValue = struct
end end
module AccessSnapshot = struct module AccessSnapshot = struct
module AccessSnapshotElem = struct
type t = type t =
{ access: TraceElem.t { access: Access.t
; thread: ThreadsDomain.t ; thread: ThreadsDomain.t
; lock: bool ; lock: bool
; ownership_precondition: OwnershipAbstractValue.t } ; ownership_precondition: OwnershipAbstractValue.t }
[@@deriving compare] [@@deriving compare]
let is_write {access} = TraceElem.is_write access let pp fmt {access; thread; lock; ownership_precondition} =
F.fprintf fmt "Access: %a Thread: %a Lock: %b Pre: %a" Access.pp access ThreadsDomain.pp
thread lock OwnershipAbstractValue.pp ownership_precondition
let describe fmt {access} = Access.describe fmt access
end
let make_loc_trace {access} = TraceElem.make_loc_trace access include ExplicitTrace.MakeTraceElemModuloLocation (AccessSnapshotElem) (CallPrinter)
let get_loc {access} = TraceElem.get_loc access let is_write {elem= {access}} = Access.is_write access
let is_container_write {access} = TraceElem.is_container_write access let is_container_write {elem= {access}} = Access.is_container_write access
let make_if_not_owned formals access lock thread ownership_precondition = let filter formals t =
if if
(not (OwnershipAbstractValue.is_owned ownership_precondition)) (not (OwnershipAbstractValue.is_owned t.elem.ownership_precondition))
&& TraceElem.should_keep formals access && Access.should_keep formals t.elem.access
then Some {access; lock; thread; ownership_precondition} then Some t
else None else None
let make formals access lock_astate thread ownership_precondition = let make_if_not_owned formals access lock thread ownership_precondition loc =
let lock = not (LocksDomain.is_bottom lock_astate) in make {access; lock; thread; ownership_precondition} loc |> filter formals
make_if_not_owned formals access lock thread ownership_precondition
let make_unannotated_call_access formals pname lock ownership loc =
let lock = LocksDomain.is_locked lock in
let access = Access.make_unannotated_call_access pname in
make_if_not_owned formals access lock ownership loc
let make_access formals acc_exp ~is_write loc lock thread ownership_precondition = let make_access formals acc_exp ~is_write loc lock thread ownership_precondition =
let lock = LocksDomain.is_locked lock in let lock = LocksDomain.is_locked lock in
let access = TraceElem.make_field_access acc_exp ~is_write loc in let access = Access.make_field_access acc_exp ~is_write in
make_if_not_owned formals access lock thread ownership_precondition make_if_not_owned formals access lock thread ownership_precondition loc
let make_container_access formals acc_exp ~is_write callee loc lock thread ownership_precondition let make_container_access formals acc_exp ~is_write callee loc lock thread ownership_precondition
= =
let lock = LocksDomain.is_locked lock in let lock = LocksDomain.is_locked lock in
let access = TraceElem.make_container_access acc_exp callee ~is_write loc in let access = Access.make_container_access acc_exp callee ~is_write in
make_if_not_owned formals access lock thread ownership_precondition make_if_not_owned formals access lock thread ownership_precondition loc
let make_from_snapshot formals access {lock; thread; ownership_precondition} =
make_if_not_owned formals access lock thread ownership_precondition
let map_opt formals ~f t = let map_opt formals ~f t =
let access = TraceElem.map_access ~f t.access in map t ~f:(fun elem -> {elem with access= Access.map ~f elem.access}) |> filter formals
make_from_snapshot formals access t
let update_callee_access formals snapshot callee_pname loc ownership_precondition threads locks = let update_callee_access formals snapshot callsite ownership_precondition threads locks =
let access = TraceElem.with_callsite snapshot.access (CallSite.make callee_pname loc) in
let locks = if snapshot.lock then LocksDomain.acquire_lock locks else locks in
let thread = let thread =
ThreadsDomain.integrate_summary ~callee_astate:snapshot.thread ~caller_astate:threads ThreadsDomain.integrate_summary ~callee_astate:snapshot.elem.thread ~caller_astate:threads
in in
make formals access locks thread ownership_precondition let lock = snapshot.elem.lock || LocksDomain.is_locked locks in
with_callsite snapshot callsite
|> map ~f:(fun elem -> {elem with lock; thread; ownership_precondition})
|> filter formals
let is_unprotected {thread; lock; ownership_precondition} = let is_unprotected {elem= {thread; lock; ownership_precondition}} =
(not (ThreadsDomain.is_any_but_self thread)) (not (ThreadsDomain.is_any_but_self thread))
&& (not lock) && (not lock)
&& not (OwnershipAbstractValue.is_owned ownership_precondition) && not (OwnershipAbstractValue.is_owned ownership_precondition)
let pp fmt {access; thread; lock; ownership_precondition} =
F.fprintf fmt "Loc: %a Access: %a Thread: %a Lock: %b Pre: %a" Location.pp
(TraceElem.get_loc access) TraceElem.pp access ThreadsDomain.pp thread lock
OwnershipAbstractValue.pp ownership_precondition
end end
module AccessDomain = struct module AccessDomain = struct
include AbstractDomain.FiniteSet (AccessSnapshot) include AbstractDomain.FiniteSet (AccessSnapshot)
let add ({AccessSnapshot.access= {elem}} as s) astate = let add ({AccessSnapshot.elem= {access}} as s) astate =
let skip = let skip =
Access.get_access_exp elem Access.get_access_exp access
|> Option.exists ~f:(fun exp -> AccessExpression.get_base exp |> fst |> should_skip_var) |> Option.exists ~f:(fun exp -> AccessExpression.get_base exp |> fst |> should_skip_var)
in in
if skip then astate else add s astate if skip then astate else add s astate
@ -567,6 +546,8 @@ let pp fmt {threads; locks; accesses; ownership; attribute_map} =
let add_unannotated_call_access formals pname loc (astate : t) = let add_unannotated_call_access formals pname loc (astate : t) =
let access = TraceElem.make_unannotated_call_access pname loc in let snapshot =
let snapshot = AccessSnapshot.make formals access astate.locks astate.threads Unowned in AccessSnapshot.make_unannotated_call_access formals pname astate.locks astate.threads Unowned
loc
in
{astate with accesses= AccessDomain.add_opt snapshot astate.accesses} {astate with accesses= AccessDomain.add_opt snapshot astate.accesses}

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

@ -28,10 +28,6 @@ module Access : sig
val get_access_exp : t -> AccessExpression.t option val get_access_exp : t -> AccessExpression.t option
end end
module TraceElem : sig
include ExplicitTrace.TraceElem with type elem_t = Access.t
end
(** Overapproximation of number of locks that are currently held *) (** Overapproximation of number of locks that are currently held *)
module LocksDomain : sig module LocksDomain : sig
type t type t
@ -89,21 +85,21 @@ end
(** snapshot of the relevant state at the time of a heap access: concurrent thread(s), lock(s) held, (** snapshot of the relevant state at the time of a heap access: concurrent thread(s), lock(s) held,
ownership precondition *) ownership precondition *)
module AccessSnapshot : sig module AccessSnapshot : sig
type t = private module AccessSnapshotElem : sig
{ access: TraceElem.t type t =
{ access: Access.t
; thread: ThreadsDomain.t ; thread: ThreadsDomain.t
; lock: bool ; lock: bool
; ownership_precondition: OwnershipAbstractValue.t } ; ownership_precondition: OwnershipAbstractValue.t }
end
include PrettyPrintable.PrintableOrderedType with type t := t include ExplicitTrace.TraceElem with type elem_t = AccessSnapshotElem.t
val is_write : t -> bool val is_write : t -> bool
(** is it a write OR a container write *) (** is it a write OR a container write *)
val is_container_write : t -> bool val is_container_write : t -> bool
val make_loc_trace : t -> Errlog.loc_trace
val get_loc : t -> Location.t val get_loc : t -> Location.t
val make_access : val make_access :
@ -135,16 +131,13 @@ module AccessSnapshot : sig
val update_callee_access : val update_callee_access :
FormalMap.t FormalMap.t
-> t -> t
-> Procname.t -> CallSite.t
-> Location.t
-> OwnershipAbstractValue.t -> OwnershipAbstractValue.t
-> ThreadsDomain.t -> ThreadsDomain.t
-> LocksDomain.t -> LocksDomain.t
-> t option -> t option
end end
(** map of access metadata |-> set of accesses. the map should hold all accesses to a
possibly-unowned access path *)
module AccessDomain : sig module AccessDomain : sig
include AbstractDomain.FiniteSetS with type elt = AccessSnapshot.t include AbstractDomain.FiniteSetS with type elt = AccessSnapshot.t
@ -197,6 +190,10 @@ type t =
; attribute_map: AttributeMapDomain.t ; attribute_map: AttributeMapDomain.t
(** map of access paths to attributes such as owned, functional, ... *) } (** map of access paths to attributes such as owned, functional, ... *) }
include AbstractDomain.WithBottom with type t := t
val add_unannotated_call_access : FormalMap.t -> Procname.t -> Location.t -> t -> t
(** same as astate, but without [attribute_map] (since these involve locals) and with the addition (** same as astate, but without [attribute_map] (since these involve locals) and with the addition
of the ownership/attributes associated with the return value as well as the set of formals which of the ownership/attributes associated with the return value as well as the set of formals which
may escape *) may escape *)
@ -209,8 +206,4 @@ type summary =
val empty_summary : summary val empty_summary : summary
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 : FormalMap.t -> Procname.t -> Location.t -> t -> t

Write Preview
Loading…
Cancel
Save