From b194d70860087a292accacc8cdd66f8ffed4b1ec Mon Sep 17 00:00:00 2001 From: Nikos Gorogiannis Date: Fri, 27 Mar 2020 06:45:34 -0700 Subject: [PATCH] [racerd][2/n] invert inclusion between AccessSnapshot and TraceElem 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 --- infer/src/concurrency/ExplicitTrace.ml | 5 +- infer/src/concurrency/RacerD.ml | 32 +++---- infer/src/concurrency/RacerDDomain.ml | 117 +++++++++++-------------- infer/src/concurrency/RacerDDomain.mli | 33 +++---- 4 files changed, 82 insertions(+), 105 deletions(-) diff --git a/infer/src/concurrency/ExplicitTrace.ml b/infer/src/concurrency/ExplicitTrace.ml index d93430472..c817992f7 100644 --- a/infer/src/concurrency/ExplicitTrace.ml +++ b/infer/src/concurrency/ExplicitTrace.ml @@ -68,7 +68,10 @@ module MakeTraceElemWithComparator 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 end diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index 2965fa730..35ef4f1ef 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -115,6 +115,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let add_callee_accesses formals (caller_astate : Domain.t) callee_accesses locks threads actuals callee_pname loc = let open Domain in + let callsite = CallSite.make callee_pname loc in let actuals_ownership = (* precompute array holding ownership of each actual for fast random access *) 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 = (* update precondition with caller ownership info *) let ownership_precondition = - match snapshot.ownership_precondition with + match snapshot.elem.ownership_precondition with | OwnedIf indexes -> IntSet.fold update_ownership_precondition indexes OwnershipAbstractValue.owned | Unowned -> - snapshot.ownership_precondition + snapshot.elem.ownership_precondition in let snapshot_opt = - AccessSnapshot.update_callee_access formals snapshot callee_pname loc ownership_precondition - threads locks + AccessSnapshot.update_callee_access formals snapshot callsite ownership_precondition threads + locks in AccessDomain.add_opt snapshot_opt acc 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 pp_access fmt (t : RacerDDomain.AccessSnapshot.t) = - match t.access.elem with + match t.elem.access with | Read {exp} | Write {exp} -> describe_exp fmt exp | ContainerRead {exp; pname} | ContainerWrite {exp; pname} -> @@ -661,9 +662,8 @@ type reported_access = let report_thread_safety_violation ~issue_log ~make_description ~report_kind ({threads; snapshot; tenv; procname= pname} : reported_access) = let open RacerDDomain in - let access = snapshot.access 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 access.loc in + let final_pname = List.last snapshot.trace |> Option.value_map ~default:pname ~f:CallSite.pname in + let final_sink_site = CallSite.make final_pname snapshot.loc in let initial_sink_site = CallSite.make pname (AccessSnapshot.get_loc snapshot) in let loc = CallSite.loc initial_sink_site in let ltr, original_end, conflict_end = make_trace ~report_kind snapshot in @@ -805,7 +805,7 @@ end = struct let empty = M.empty 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 else let k = Key.of_access access in @@ -856,13 +856,13 @@ let should_report_guardedby_violation classname ({snapshot; tenv; procname} : re | _ -> false ) in - (not snapshot.lock) + (not snapshot.elem.lock) && RacerDDomain.AccessSnapshot.is_write snapshot && Procname.is_java procname && (* restrict check to access paths of length one *) 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:(fun (base, accesses) -> (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 CallSite.Set.mem call_site reported_sites || - match snapshot.access.TraceElem.elem with + match snapshot.elem.access with | Access.Write _ | Access.ContainerWrite _ -> Procname.Set.mem pname reported_writes | Access.Read _ | Access.ContainerRead _ -> @@ -931,7 +931,7 @@ let report_unsafe_accesses ~issue_log classname (aggregated_access_map : ReportM if Config.deduplicate then let call_site = CallSite.make pname (AccessSnapshot.get_loc snapshot) 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 _ -> let reported_writes = Procname.Set.add pname reported.reported_writes in {reported with reported_writes; reported_sites} @@ -965,7 +965,7 @@ let report_unsafe_accesses ~issue_log classname (aggregated_access_map : ReportM in let report_unsafe_access accesses acc ({snapshot; threads; tenv; procname= pname} as reported_access) = - match snapshot.access.elem with + match snapshot.elem.access with | Access.InterfaceCall reported_pname when AccessSnapshot.is_unprotected snapshot && 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 _ -> (* protected read. report unprotected writes and opposite protected writes as conflicts *) let can_conflict (snapshot1 : AccessSnapshot.t) (snapshot2 : AccessSnapshot.t) = - if snapshot1.lock && snapshot2.lock then false - else ThreadsDomain.can_conflict snapshot1.thread snapshot2.thread + if snapshot1.elem.lock && snapshot2.elem.lock then false + else ThreadsDomain.can_conflict snapshot1.elem.thread snapshot2.elem.thread in let is_conflict {snapshot= other_snapshot; threads= other_threads} = if AccessSnapshot.is_unprotected other_snapshot then diff --git a/infer/src/concurrency/RacerDDomain.ml b/infer/src/concurrency/RacerDDomain.ml index c70c0de7f..0863f44d3 100644 --- a/infer/src/concurrency/RacerDDomain.ml +++ b/infer/src/concurrency/RacerDDomain.ml @@ -44,6 +44,8 @@ module Access = struct if is_write then ContainerWrite {exp; pname} else ContainerRead {exp; pname} + let make_unannotated_call_access pname = InterfaceCall pname + let is_write = function | InterfaceCall _ | Read _ | ContainerRead _ -> false @@ -130,31 +132,6 @@ module CallPrinter = struct let pp fmt cs = F.fprintf fmt "call to %a" Procname.pp (CallSite.pname cs) 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 include AbstractDomain.CountDomain (struct (** arbitrary threshold for max locks we expect to be held simultaneously *) @@ -281,83 +258,85 @@ module OwnershipAbstractValue = struct end module AccessSnapshot = struct - type t = - { access: TraceElem.t - ; thread: ThreadsDomain.t - ; lock: bool - ; ownership_precondition: OwnershipAbstractValue.t } - [@@deriving compare] + module AccessSnapshotElem = struct + type t = + { access: Access.t + ; thread: ThreadsDomain.t + ; lock: bool + ; ownership_precondition: OwnershipAbstractValue.t } + [@@deriving compare] + + 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 is_write {access} = TraceElem.is_write access - let make_loc_trace {access} = TraceElem.make_loc_trace access + let describe fmt {access} = Access.describe fmt access + end - let get_loc {access} = TraceElem.get_loc access + include ExplicitTrace.MakeTraceElemModuloLocation (AccessSnapshotElem) (CallPrinter) - let is_container_write {access} = TraceElem.is_container_write access + let is_write {elem= {access}} = Access.is_write access - let make_if_not_owned formals access lock thread ownership_precondition = + let is_container_write {elem= {access}} = Access.is_container_write access + + let filter formals t = if - (not (OwnershipAbstractValue.is_owned ownership_precondition)) - && TraceElem.should_keep formals access - then Some {access; lock; thread; ownership_precondition} + (not (OwnershipAbstractValue.is_owned t.elem.ownership_precondition)) + && Access.should_keep formals t.elem.access + then Some t else None - let make formals access lock_astate thread ownership_precondition = - let lock = not (LocksDomain.is_bottom lock_astate) in - make_if_not_owned formals access lock thread ownership_precondition + let make_if_not_owned formals access lock thread ownership_precondition loc = + make {access; lock; thread; ownership_precondition} loc |> filter formals + + + 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 lock = LocksDomain.is_locked lock in - let access = TraceElem.make_field_access acc_exp ~is_write loc in - make_if_not_owned formals access lock thread ownership_precondition + let access = Access.make_field_access acc_exp ~is_write in + 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 lock = LocksDomain.is_locked lock in - let access = TraceElem.make_container_access acc_exp callee ~is_write loc in - make_if_not_owned formals access lock thread ownership_precondition - - - let make_from_snapshot formals access {lock; thread; ownership_precondition} = - make_if_not_owned formals access lock thread ownership_precondition + let access = Access.make_container_access acc_exp callee ~is_write in + make_if_not_owned formals access lock thread ownership_precondition loc let map_opt formals ~f t = - let access = TraceElem.map_access ~f t.access in - make_from_snapshot formals access t + map t ~f:(fun elem -> {elem with access= Access.map ~f elem.access}) |> filter formals - let update_callee_access formals snapshot callee_pname loc 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 update_callee_access formals snapshot callsite ownership_precondition threads locks = let thread = - ThreadsDomain.integrate_summary ~callee_astate:snapshot.thread ~caller_astate:threads + ThreadsDomain.integrate_summary ~callee_astate:snapshot.elem.thread ~caller_astate:threads 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 lock) && 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 module AccessDomain = struct include AbstractDomain.FiniteSet (AccessSnapshot) - let add ({AccessSnapshot.access= {elem}} as s) astate = + let add ({AccessSnapshot.elem= {access}} as s) astate = 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) in 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 access = TraceElem.make_unannotated_call_access pname loc in - let snapshot = AccessSnapshot.make formals access astate.locks astate.threads Unowned in + let snapshot = + AccessSnapshot.make_unannotated_call_access formals pname astate.locks astate.threads Unowned + loc + in {astate with accesses= AccessDomain.add_opt snapshot astate.accesses} diff --git a/infer/src/concurrency/RacerDDomain.mli b/infer/src/concurrency/RacerDDomain.mli index e3deab5fb..19b84b81c 100644 --- a/infer/src/concurrency/RacerDDomain.mli +++ b/infer/src/concurrency/RacerDDomain.mli @@ -28,10 +28,6 @@ module Access : sig val get_access_exp : t -> AccessExpression.t option end -module TraceElem : sig - include ExplicitTrace.TraceElem with type elem_t = Access.t -end - (** Overapproximation of number of locks that are currently held *) module LocksDomain : sig 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, ownership precondition *) module AccessSnapshot : sig - type t = private - { access: TraceElem.t - ; thread: ThreadsDomain.t - ; lock: bool - ; ownership_precondition: OwnershipAbstractValue.t } + module AccessSnapshotElem : sig + type t = + { access: Access.t + ; thread: ThreadsDomain.t + ; lock: bool + ; 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 (** is it a write OR a container write *) val is_container_write : t -> bool - val make_loc_trace : t -> Errlog.loc_trace - val get_loc : t -> Location.t val make_access : @@ -135,16 +131,13 @@ module AccessSnapshot : sig val update_callee_access : FormalMap.t -> t - -> Procname.t - -> Location.t + -> CallSite.t -> OwnershipAbstractValue.t -> ThreadsDomain.t -> LocksDomain.t -> t option end -(** map of access metadata |-> set of accesses. the map should hold all accesses to a - possibly-unowned access path *) module AccessDomain : sig include AbstractDomain.FiniteSetS with type elt = AccessSnapshot.t @@ -197,6 +190,10 @@ type t = ; attribute_map: AttributeMapDomain.t (** 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 of the ownership/attributes associated with the return value as well as the set of formals which may escape *) @@ -209,8 +206,4 @@ type summary = val empty_summary : summary -include AbstractDomain.WithBottom with type t := t - val pp_summary : F.formatter -> summary -> unit - -val add_unannotated_call_access : FormalMap.t -> Procname.t -> Location.t -> t -> t