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