diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index 505c0d289..2965fa730 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -39,9 +39,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct then add_field_accesses prefix_path' acc access_list else let is_write = List.is_empty access_list && is_write_access in - let access = TraceElem.make_field_access prefix_path' ~is_write loc in let pre = OwnershipDomain.get_owned prefix_path ownership in - let snapshot_opt = AccessSnapshot.make formals access locks threads pre in + let snapshot_opt = + AccessSnapshot.make_access formals prefix_path' ~is_write loc locks threads pre + in let access_acc' = AccessDomain.add_opt snapshot_opt acc in add_field_accesses prefix_path' access_acc' access_list in @@ -55,16 +56,13 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let open Domain in if RacerDModels.is_synchronized_container callee_pname receiver_ap tenv then None else + let ownership_pre = OwnershipDomain.get_owned receiver_ap astate.ownership in let callee_access = - let container_access = - TraceElem.make_container_access receiver_ap ~is_write callee_pname callee_loc - in - let ownership_pre = OwnershipDomain.get_owned receiver_ap astate.ownership in - AccessSnapshot.make formals container_access astate.locks astate.threads ownership_pre + AccessSnapshot.make_container_access formals receiver_ap ~is_write callee_pname callee_loc + astate.locks astate.threads ownership_pre in - let ownership_value = OwnershipDomain.get_owned receiver_ap astate.ownership in let ownership = - OwnershipDomain.add (AccessExpression.base ret_base) ownership_value astate.ownership + OwnershipDomain.add (AccessExpression.base ret_base) ownership_pre astate.ownership in let accesses = AccessDomain.add_opt callee_access astate.accesses in Some {astate with accesses; ownership} @@ -108,8 +106,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct exp in let add snapshot acc = - let access' = TraceElem.map ~f:expand_exp snapshot.AccessSnapshot.access in - let snapshot_opt' = AccessSnapshot.make_from_snapshot formals access' snapshot in + let snapshot_opt' = AccessSnapshot.map_opt formals ~f:expand_exp snapshot in AccessDomain.add_opt snapshot_opt' acc in AccessDomain.fold add accesses AccessDomain.empty @@ -130,11 +127,6 @@ module TransferFunctions (CFG : ProcCfg.S) = struct else OwnershipAbstractValue.join acc actuals_ownership.(actual_index) in 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.acquire_lock locks else locks in - let thread = - ThreadsDomain.integrate_summary ~callee_astate:snapshot.thread ~caller_astate:threads - in (* update precondition with caller ownership info *) let ownership_precondition = match snapshot.ownership_precondition with @@ -143,7 +135,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | Unowned -> snapshot.ownership_precondition in - let snapshot_opt = AccessSnapshot.make formals access locks thread ownership_precondition in + let snapshot_opt = + AccessSnapshot.update_callee_access formals snapshot callee_pname loc ownership_precondition + threads locks + in AccessDomain.add_opt snapshot_opt acc in AccessDomain.fold update_callee_access callee_accesses caller_astate.accesses @@ -534,7 +529,7 @@ let analyze_procedure {Callbacks.exe_env; summary} = else Payload.update_summary empty_summary summary -type conflict = RacerDDomain.TraceElem.t +type conflict = RacerDDomain.AccessSnapshot.t type report_kind = | GuardedByViolation @@ -618,8 +613,8 @@ 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.TraceElem.t) = - match t.elem with +let pp_access fmt (t : RacerDDomain.AccessSnapshot.t) = + match t.access.elem with | Read {exp} | Write {exp} -> describe_exp fmt exp | ContainerRead {exp; pname} | ContainerWrite {exp; pname} -> @@ -630,7 +625,7 @@ let pp_access fmt (t : RacerDDomain.TraceElem.t) = let make_trace ~report_kind original_exp = let open RacerDDomain in - let loc_trace_of_path path = TraceElem.make_loc_trace path in + let loc_trace_of_path path = AccessSnapshot.make_loc_trace path in let original_trace = loc_trace_of_path original_exp in let get_end_loc trace = Option.map (List.last trace) ~f:(function {Errlog.lt_loc} -> lt_loc) in let original_end = get_end_loc original_trace in @@ -669,11 +664,11 @@ let report_thread_safety_violation ~issue_log ~make_description ~report_kind 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 initial_sink_site = CallSite.make pname (TraceElem.get_loc access) 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 access in + let ltr, original_end, conflict_end = make_trace ~report_kind snapshot in (* what the potential bug is *) - let description = make_description pname final_sink_site initial_sink_site access in + let description = make_description pname final_sink_site initial_sink_site snapshot in (* why we are reporting it *) let issue_type, explanation = get_reporting_explanation report_kind tenv pname threads in let error_message = F.sprintf "%s%s" description explanation in @@ -703,7 +698,8 @@ let make_unprotected_write_description pname final_sink_site initial_sink_site f Format.asprintf "Unprotected write. Non-private method %a%s %s %a outside of synchronization." describe_pname pname (if CallSite.equal final_sink_site initial_sink_site then "" else " indirectly") - (if RacerDDomain.TraceElem.is_container_write final_sink then "mutates" else "writes to field") + ( if RacerDDomain.AccessSnapshot.is_container_write final_sink then "mutates" + else "writes to field" ) pp_access final_sink @@ -861,7 +857,7 @@ let should_report_guardedby_violation classname ({snapshot; tenv; procname} : re false ) in (not snapshot.lock) - && RacerDDomain.TraceElem.is_write snapshot.access + && RacerDDomain.AccessSnapshot.is_write snapshot && Procname.is_java procname && (* restrict check to access paths of length one *) @@ -918,7 +914,7 @@ let report_unsafe_accesses ~issue_log classname (aggregated_access_map : ReportM let open RacerDModels in let is_duplicate_report ({snapshot; procname= pname} : reported_access) ({reported_sites; reported_writes; reported_reads; reported_unannotated_calls}, _) = - let call_site = CallSite.make pname (TraceElem.get_loc snapshot.access) in + let call_site = CallSite.make pname (AccessSnapshot.get_loc snapshot) in if Config.deduplicate then CallSite.Set.mem call_site reported_sites || @@ -933,7 +929,7 @@ let report_unsafe_accesses ~issue_log classname (aggregated_access_map : ReportM in let update_reported ({snapshot; procname= pname} : reported_access) reported = if Config.deduplicate then - let call_site = CallSite.make pname (TraceElem.get_loc snapshot.access) in + 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 | Access.Write _ | Access.ContainerWrite _ -> @@ -987,8 +983,8 @@ let report_unsafe_accesses ~issue_log classname (aggregated_access_map : ReportM (i.e., not a self race). find accesses on a background thread this access might conflict with and report them *) List.find_map accesses ~f:(fun {snapshot= other_snapshot; threads= other_threads} -> - if TraceElem.is_write other_snapshot.access && ThreadsDomain.is_any other_threads - then Some other_snapshot.access + if AccessSnapshot.is_write other_snapshot && ThreadsDomain.is_any other_threads then + Some other_snapshot else None ) in if @@ -1005,7 +1001,7 @@ let report_unsafe_accesses ~issue_log classname (aggregated_access_map : ReportM (* unprotected read. report all writes as conflicts for java. for c++ filter out unprotected writes *) let is_conflict {snapshot; threads= other_threads} = - TraceElem.is_write snapshot.access + AccessSnapshot.is_write snapshot && if Procname.is_java pname then ThreadsDomain.is_any threads || ThreadsDomain.is_any other_threads @@ -1016,7 +1012,7 @@ let report_unsafe_accesses ~issue_log classname (aggregated_access_map : ReportM let make_description = make_read_write_race_description ~read_is_sync:false conflict in - let report_kind = ReadWriteRace conflict.snapshot.access in + let report_kind = ReadWriteRace conflict.snapshot in report_thread_safety_violation ~acc ~make_description ~report_kind reported_access ) | Access.Read _ | ContainerRead _ -> (* protected read. report unprotected writes and opposite protected writes as conflicts *) @@ -1026,8 +1022,8 @@ let report_unsafe_accesses ~issue_log classname (aggregated_access_map : ReportM in let is_conflict {snapshot= other_snapshot; threads= other_threads} = if AccessSnapshot.is_unprotected other_snapshot then - TraceElem.is_write other_snapshot.access && ThreadsDomain.is_any other_threads - else TraceElem.is_write other_snapshot.access && can_conflict snapshot other_snapshot + AccessSnapshot.is_write other_snapshot && ThreadsDomain.is_any other_threads + else AccessSnapshot.is_write other_snapshot && can_conflict snapshot other_snapshot in List.find accesses ~f:is_conflict |> Option.value_map ~default:acc ~f:(fun conflict -> @@ -1035,7 +1031,7 @@ let report_unsafe_accesses ~issue_log classname (aggregated_access_map : ReportM let make_description = make_read_write_race_description ~read_is_sync:true conflict in - let report_kind = ReadWriteRace conflict.snapshot.access in + let report_kind = ReadWriteRace conflict.snapshot in report_thread_safety_violation ~acc ~make_description ~report_kind reported_access ) in let report_accesses_on_location reportable_accesses init = diff --git a/infer/src/concurrency/RacerDDomain.ml b/infer/src/concurrency/RacerDDomain.ml index f2a6d903a..c70c0de7f 100644 --- a/infer/src/concurrency/RacerDDomain.ml +++ b/infer/src/concurrency/RacerDDomain.ml @@ -142,7 +142,7 @@ module TraceElem = struct let should_keep formals {elem} = Access.should_keep formals elem - let map ~f trace_elem = map ~f:(Access.map ~f) trace_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 @@ -157,9 +157,8 @@ end module LocksDomain = struct include AbstractDomain.CountDomain (struct + (** arbitrary threshold for max locks we expect to be held simultaneously *) let max = 5 - - (* arbitrary threshold for max locks we expect to be held simultaneously *) end) let acquire_lock = increment @@ -167,6 +166,8 @@ module LocksDomain = struct let release_lock = decrement let integrate_summary ~caller_astate ~callee_astate = add caller_astate callee_astate + + let is_locked t = not (is_bottom t) end module ThreadsDomain = struct @@ -287,6 +288,14 @@ module AccessSnapshot = struct ; ownership_precondition: OwnershipAbstractValue.t } [@@deriving compare] + let is_write {access} = TraceElem.is_write access + + let make_loc_trace {access} = TraceElem.make_loc_trace access + + let get_loc {access} = TraceElem.get_loc access + + let is_container_write {access} = TraceElem.is_container_write access + let make_if_not_owned formals access lock thread ownership_precondition = if (not (OwnershipAbstractValue.is_owned ownership_precondition)) @@ -300,10 +309,37 @@ module AccessSnapshot = struct make_if_not_owned formals access 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 access = TraceElem.make_field_access acc_exp ~is_write loc in + make_if_not_owned formals access 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 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 map_opt formals ~f t = + let access = TraceElem.map_access ~f t.access in + make_from_snapshot formals access t + + + 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 thread = + ThreadsDomain.integrate_summary ~callee_astate:snapshot.thread ~caller_astate:threads + in + make formals access locks thread ownership_precondition + + let is_unprotected {thread; lock; ownership_precondition} = (not (ThreadsDomain.is_any_but_self thread)) && (not lock) diff --git a/infer/src/concurrency/RacerDDomain.mli b/infer/src/concurrency/RacerDDomain.mli index 81bcf480e..e3deab5fb 100644 --- a/infer/src/concurrency/RacerDDomain.mli +++ b/infer/src/concurrency/RacerDDomain.mli @@ -30,17 +30,6 @@ end module TraceElem : sig include ExplicitTrace.TraceElem with type elem_t = Access.t - - val is_write : t -> bool - (** is it a write OR a container write *) - - val is_container_write : t -> bool - - val map : f:(AccessExpression.t -> AccessExpression.t) -> t -> t - - val make_container_access : AccessExpression.t -> Procname.t -> is_write:bool -> Location.t -> t - - val make_field_access : AccessExpression.t -> is_write:bool -> Location.t -> t end (** Overapproximation of number of locks that are currently held *) @@ -108,18 +97,50 @@ module AccessSnapshot : sig include PrettyPrintable.PrintableOrderedType with type t := t - val make : + 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 : FormalMap.t - -> TraceElem.t + -> AccessExpression.t + -> is_write:bool + -> Location.t -> LocksDomain.t -> ThreadsDomain.t -> OwnershipAbstractValue.t -> t option - val make_from_snapshot : FormalMap.t -> TraceElem.t -> t -> t option + val make_container_access : + FormalMap.t + -> AccessExpression.t + -> is_write:bool + -> Procname.t + -> Location.t + -> LocksDomain.t + -> ThreadsDomain.t + -> OwnershipAbstractValue.t + -> t option val is_unprotected : t -> bool (** return true if not protected by lock, thread, or ownership *) + + val map_opt : FormalMap.t -> f:(AccessExpression.t -> AccessExpression.t) -> t -> t option + + val update_callee_access : + FormalMap.t + -> t + -> Procname.t + -> Location.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