diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index 948193309..481c95b98 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/infer/src/checkers/ThreadSafety.ml @@ -35,8 +35,8 @@ let is_container_write_str str = let strip_container_write str = String.substr_replace_first str ~pattern:container_write_string ~with_:"" -let is_container_write_sink (sink:ThreadSafetyDomain.TraceElem.t) = - let access_list = snd (ThreadSafetyDomain.TraceElem.kind sink) in +let is_container_write_sink sink = + let _, access_list = fst (ThreadSafetyDomain.TraceElem.kind sink) in match List.rev access_list with | FieldAccess (fn) :: _ -> is_container_write_str (Ident.fieldname_to_string fn) | _ -> false @@ -159,7 +159,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | None -> attribute_map - let add_path_to_state exp typ loc path_state id_map attribute_map tenv = + let add_path_to_state access_kind exp typ loc path_state id_map attribute_map tenv = (* we don't want to warn on writes to the field if it is (a) thread-confined, or (b) volatile *) let is_safe_write access_path tenv = let is_thread_safe_write accesses tenv = @@ -190,11 +190,70 @@ module TransferFunctions (CFG : ProcCfg.S) = struct ~f:(fun acc rawpath -> if not (is_owned (AccessPath.Raw.truncate rawpath) attribute_map) && not (is_safe_write rawpath tenv) - then Domain.PathDomain.add_sink (Domain.make_access rawpath loc) acc + then Domain.PathDomain.add_sink (Domain.make_access rawpath access_kind loc) acc else acc) ~init:path_state (AccessPath.of_exp exp typ ~f_resolve_id) + let is_unprotected is_locked pdesc = + not is_locked && not (Procdesc.is_java_synchronized pdesc) + + let add_access + exp + loc + access_kind + (astate : Domain.astate) + ~f_resolve_id + (proc_data : FormalMap.t ProcData.t) = + let get_formal_index exp typ = match AccessPath.of_lhs_exp exp typ ~f_resolve_id with + | Some (base, _) -> FormalMap.get_formal_index base proc_data.extras + | None -> None in + match exp with + | Exp.Lfield (base_exp, _, typ) -> + let open Domain in + if is_unprotected astate.locks proc_data.pdesc + then + match get_formal_index base_exp typ with + | Some formal_index -> + let pre = AccessPrecondition.ProtectedIf (Some formal_index) in + let conditional_accesses_for_pre = + add_path_to_state + access_kind + exp + typ + loc + (AccessDomain.get_accesses pre astate.accesses) + astate.id_map + astate.attribute_map + proc_data.tenv in + AccessDomain.add pre conditional_accesses_for_pre astate.accesses + | None -> + let unsafe_accesses = + add_path_to_state + access_kind + exp + typ + loc + (AccessDomain.get_accesses AccessPrecondition.unprotected astate.accesses) + astate.id_map + astate.attribute_map + proc_data.tenv in + AccessDomain.add AccessPrecondition.unprotected unsafe_accesses astate.accesses + else + let safe_accesses = + add_path_to_state + access_kind + exp + typ + loc + (AccessDomain.get_accesses Protected astate.accesses) + astate.id_map + astate.attribute_map + proc_data.tenv in + AccessDomain.add Protected safe_accesses astate.accesses + | _ -> + astate.accesses + let analyze_id_assignment lhs_id rhs_exp rhs_typ { Domain.id_map; } = let f_resolve_id = resolve_id id_map in match AccessPath.of_lhs_exp rhs_exp rhs_typ ~f_resolve_id with @@ -261,7 +320,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct is_owned_in_library pname || PatternMatch.override_exists is_owned_in_library tenv pname - let exec_instr (astate : Domain.astate) { ProcData.pdesc; tenv; extras; } _ = + let exec_instr (astate : Domain.astate) ({ ProcData.pdesc; tenv; extras; } as proc_data) _ = let is_container_write pn tenv = match pn with | Typ.Procname.Java java_pname -> let typename = Typename.Java.from_string (Typ.Procname.java_get_class_name java_pname) in @@ -288,16 +347,16 @@ module TransferFunctions (CFG : ProcCfg.S) = struct (Mangled.from_string (container_write_string ^ (Typ.Procname.get_method callee_pname))) 0 in let dummy_access_exp = Exp.Lfield (receiver_exp, dummy_fieldname, receiver_typ) in - let callee_writes = + let callee_accesses = match AccessPath.of_lhs_exp dummy_access_exp receiver_typ ~f_resolve_id with | Some container_ap -> AccessDomain.add_access (ProtectedIf (Some 0)) - (make_access container_ap callee_loc) + (make_access container_ap Write callee_loc) AccessDomain.empty | None -> AccessDomain.empty in - Some (false, PathDomain.empty, callee_writes, AttributeSetDomain.empty) + Some (false, callee_accesses, AttributeSetDomain.empty) | _ -> failwithf "Call to %a is marked as a container write, but has no receiver" @@ -308,8 +367,6 @@ module TransferFunctions (CFG : ProcCfg.S) = struct add_container_write callee_pname actuals ~f_resolve_id callee_loc else Summary.read_summary caller_pdesc callee_pname in - let is_unprotected is_locked = - not is_locked && not (Procdesc.is_java_synchronized pdesc) in (* return true if the given procname boxes a primitive type into a reference type *) let is_box = function | Typ.Procname.Java java_pname -> @@ -366,10 +423,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | NoEffect -> match get_summary pdesc callee_pname actuals ~f_resolve_id loc tenv with - | Some (callee_locks, - callee_reads, - callee_writes, - return_attributes) -> + | Some (callee_locks, callee_accesses, return_attributes) -> let call_site = CallSite.make callee_pname loc in let combine_accesses_for_pre pre ~caller_accesses ~callee_accesses = let combined_accesses = @@ -377,24 +431,24 @@ module TransferFunctions (CFG : ProcCfg.S) = struct (AccessDomain.get_accesses pre callee_accesses) call_site |> PathDomain.join (AccessDomain.get_accesses pre caller_accesses) in AccessDomain.add pre combined_accesses caller_accesses in - let combined_safe_writes = + let combined_safe_accesses = combine_accesses_for_pre AccessPrecondition.Protected - ~caller_accesses:astate.writes - ~callee_accesses:callee_writes in + ~caller_accesses:astate.accesses + ~callee_accesses in let locks' = callee_locks || astate.locks in let astate' = - if is_unprotected locks' + if is_unprotected locks' pdesc then - let add_conditional_writes index writes_acc (actual_exp, actual_typ) = + let add_conditional_accesses index accesses_acc (actual_exp, actual_typ) = if is_constant actual_exp then (* the actual is a constant, so it's owned in the caller. *) - writes_acc + accesses_acc else - let callee_conditional_writes = + let callee_conditional_accesses = PathDomain.with_callsite - (AccessDomain.get_accesses (ProtectedIf (Some index)) callee_writes) + (AccessDomain.get_accesses (ProtectedIf (Some index)) callee_accesses) call_site in begin match AccessPath.of_lhs_exp actual_exp actual_typ ~f_resolve_id with @@ -403,7 +457,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct then (* the actual passed to the current callee is owned. drop all the conditional writes for that actual, since they're all safe *) - writes_acc + accesses_acc else let base = fst actual_access_path in begin @@ -414,36 +468,33 @@ module TransferFunctions (CFG : ProcCfg.S) = struct PathDomain.Sinks.fold (AccessDomain.add_access (ProtectedIf (Some formal_index))) - (PathDomain.sinks callee_conditional_writes) - writes_acc + (PathDomain.sinks callee_conditional_accesses) + accesses_acc | None -> (* access path not owned and not rooted in a formal. add to unsafe writes *) PathDomain.Sinks.fold (AccessDomain.add_access AccessPrecondition.unprotected) - (PathDomain.sinks callee_conditional_writes) - writes_acc + (PathDomain.sinks callee_conditional_accesses) + accesses_acc end | None -> PathDomain.Sinks.fold (AccessDomain.add_access AccessPrecondition.unprotected) - (PathDomain.sinks callee_conditional_writes) - writes_acc + (PathDomain.sinks callee_conditional_accesses) + accesses_acc end in - let reads = - PathDomain.with_callsite callee_reads call_site - |> PathDomain.join astate.reads in - let unsafe_writes = + let unsafe_accesses = combine_accesses_for_pre AccessPrecondition.unprotected - ~caller_accesses:combined_safe_writes - ~callee_accesses:callee_writes in - let writes = - List.foldi ~f:add_conditional_writes ~init:unsafe_writes actuals in - { astate with reads; writes; } + ~caller_accesses:combined_safe_accesses + ~callee_accesses in + let accesses = + List.foldi ~f:add_conditional_accesses ~init:unsafe_accesses actuals in + { astate with accesses; } else - { astate with writes = combined_safe_writes; } in + { astate with accesses = combined_safe_accesses; } in let attribute_map = propagate_return_attributes ret_opt @@ -517,67 +568,20 @@ module TransferFunctions (CFG : ProcCfg.S) = struct { astate with id_map = id_map'; } | Sil.Store (lhs_exp, lhs_typ, rhs_exp, loc) -> - let get_formal_index exp typ = match AccessPath.of_lhs_exp exp typ ~f_resolve_id with - | Some (base, _) -> FormalMap.get_formal_index base extras - | None -> None in let is_marked_functional exp typ attribute_map = match AccessPath.of_lhs_exp exp typ ~f_resolve_id with | Some access_path -> AttributeMapDomain.has_attribute access_path Functional attribute_map | None -> false in - let writes = - match lhs_exp with - | Lfield (base_exp, _, typ) -> - if is_marked_functional rhs_exp lhs_typ astate.attribute_map - then - (* we want to forget about writes to @Functional fields altogether, otherwise we'll - report spurious read/write races *) - astate.writes - else if is_unprotected astate.locks - then - match get_formal_index base_exp typ with - | Some formal_index -> - let pre = AccessPrecondition.ProtectedIf (Some formal_index) in - let conditional_writes_for_pre = - AccessDomain.get_accesses pre astate.writes in - let conditional_writes_for_pre' = - add_path_to_state - lhs_exp - typ - loc - conditional_writes_for_pre - astate.id_map - astate.attribute_map - tenv in - AccessDomain.add pre conditional_writes_for_pre' astate.writes - | None -> - let unsafe_writes = - AccessDomain.get_accesses AccessPrecondition.unprotected astate.writes in - let unsafe_writes' = - add_path_to_state - lhs_exp - typ - loc - unsafe_writes - astate.id_map - astate.attribute_map - tenv in - AccessDomain.add AccessPrecondition.unprotected unsafe_writes' astate.writes - else - let safe_writes = AccessDomain.get_accesses Protected astate.writes in - let safe_writes' = - add_path_to_state - lhs_exp - typ - loc - safe_writes - astate.id_map - astate.attribute_map - tenv in - AccessDomain.add Protected safe_writes' astate.writes - | _ -> - astate.writes in + let accesses = + if is_marked_functional rhs_exp lhs_typ astate.attribute_map + then + (* we want to forget about writes to @Functional fields altogether, otherwise we'll + report spurious read/write races *) + astate.accesses + else + add_access lhs_exp loc Write astate ~f_resolve_id proc_data in let attribute_map = match AccessPath.of_lhs_exp lhs_exp lhs_typ ~f_resolve_id with | Some lhs_access_path -> @@ -585,21 +589,16 @@ module TransferFunctions (CFG : ProcCfg.S) = struct lhs_access_path rhs_exp lhs_typ ~f_resolve_id astate.attribute_map extras | None -> astate.attribute_map in - { astate with writes; attribute_map; } + { astate with accesses; attribute_map; } | Sil.Load (lhs_id, rhs_exp, rhs_typ, loc) -> let id_map = analyze_id_assignment (Var.of_id lhs_id) rhs_exp rhs_typ astate in - let reads = - match rhs_exp with - | Lfield ( _, _, typ) when is_unprotected astate.locks -> - add_path_to_state rhs_exp typ loc astate.reads astate.id_map astate.attribute_map tenv - | _ -> - astate.reads in + let accesses = add_access rhs_exp loc Read astate ~f_resolve_id proc_data in let lhs_access_path = AccessPath.of_id lhs_id rhs_typ in let attribute_map = propagate_attributes lhs_access_path rhs_exp rhs_typ ~f_resolve_id astate.attribute_map extras in - { astate with Domain.reads; id_map; attribute_map; } + { astate with accesses; id_map; attribute_map; } | Sil.Remove_temps (ids, _) -> let id_map = @@ -737,8 +736,7 @@ let analyze_procedure callback = let open ThreadSafetyDomain in let has_lock = false in let return_attrs = AttributeSetDomain.empty in - let empty = - has_lock, PathDomain.empty, AccessDomain.empty, return_attrs in + let empty = has_lock, AccessDomain.empty, return_attrs in (* convert the abstract state to a summary by dropping the id map *) let compute_post ({ ProcData.pdesc; tenv; extras; } as proc_data) = if should_analyze_proc pdesc tenv @@ -760,8 +758,9 @@ let analyze_procedure callback = | None -> ThreadSafetyDomain.empty else ThreadSafetyDomain.empty in + match Analyzer.compute_post proc_data ~initial with - | Some { locks; reads; writes; attribute_map; } -> + | Some { locks; accesses; attribute_map; } -> let return_var_ap = AccessPath.of_pvar (Pvar.get_ret_pvar (Procdesc.get_proc_name pdesc)) @@ -769,7 +768,7 @@ let analyze_procedure callback = let return_attributes = try AttributeMapDomain.find return_var_ap attribute_map with Not_found -> AttributeSetDomain.empty in - Some (locks, reads, writes, return_attributes) + Some (locks, accesses, return_attributes) | None -> None end @@ -828,13 +827,34 @@ let calculate_addendum_message tenv pname = else "" | _ -> "" -let get_possibly_unsafe_writes writes = +(* keep only the accesses of the given kind *) +let filter_by_kind access_kind trace = + let open ThreadSafetyDomain in + PathDomain.Sinks.filter + (fun sink -> phys_equal access_kind (snd (TraceElem.kind sink))) + (PathDomain.sinks trace) + |> PathDomain.update_sinks trace + +(* get all of the unprotected accesses of the given kind *) +let get_possibly_unsafe_accesses access_kind accesses = let open ThreadSafetyDomain in AccessDomain.fold - (fun attribute accesses acc -> match attribute with - | ProtectedIf _ -> PathDomain.join accesses acc + (fun pre trace acc -> match pre with + | ProtectedIf _ -> PathDomain.join (filter_by_kind access_kind trace) acc | Protected -> acc) - writes + accesses + PathDomain.empty + +let get_possibly_unsafe_reads = get_possibly_unsafe_accesses Read + +let get_possibly_unsafe_writes = get_possibly_unsafe_accesses Write + +(* get all accesses of the given kind *) +let get_all_accesses access_kind accesses = + let open ThreadSafetyDomain in + AccessDomain.fold + (fun _ trace acc -> PathDomain.join (filter_by_kind access_kind trace) acc) + accesses PathDomain.empty let equal_locs (sink1 : ThreadSafetyDomain.TraceElem.t) (sink2 : ThreadSafetyDomain.TraceElem.t) = @@ -845,8 +865,8 @@ let equal_locs (sink1 : ThreadSafetyDomain.TraceElem.t) (sink2 : ThreadSafetyDom let equal_accesses (sink1 : ThreadSafetyDomain.TraceElem.t) (sink2 : ThreadSafetyDomain.TraceElem.t) = AccessPath.equal_access_list - (snd (ThreadSafetyDomain.TraceElem.kind sink1)) - (snd (ThreadSafetyDomain.TraceElem.kind sink2)) + (snd (fst (ThreadSafetyDomain.TraceElem.kind sink1))) + (snd (fst (ThreadSafetyDomain.TraceElem.kind sink2))) (* For now equal-access and conflicting-access are equivalent. But that will change when we (soon) consider conficting accesses @@ -868,14 +888,11 @@ let filter_conflicting_sinks sink trace = access-astate is a non-empty collection of conflicting write accesses*) let collect_conflicting_writes sink tab = - let open ThreadSafetyDomain in let procs_and_writes = List.map - ~f:(fun (key,(_, _, writes, _)) -> + ~f:(fun (key, (_, accesses, _)) -> let conflicting_writes = - AccessDomain.fold - (fun _ accesses acc -> PathDomain.join accesses acc) writes PathDomain.empty - |> filter_conflicting_sinks sink in + filter_conflicting_sinks sink (get_all_accesses Write accesses) in key, conflicting_writes ) (ResultsTableType.bindings tab) in @@ -919,25 +936,22 @@ let de_dup trace = (*A helper function used in the error reporting*) let pp_accesses_sink fmt ~is_write_access sink = - let access_path = ThreadSafetyDomain.PathDomain.Sink.kind sink in + let access_path, _ = ThreadSafetyDomain.PathDomain.Sink.kind sink in let container_write = is_write_access && is_container_write_sink sink in F.fprintf fmt (if container_write then "container %a" else "%a") - AccessPath.pp_access_list (if container_write then - snd (AccessPath.Raw.truncate access_path) - else snd access_path - ) - + AccessPath.pp_access_list + (if container_write + then snd (AccessPath.Raw.truncate access_path) + else snd access_path) (* trace is really a set of accesses*) let report_thread_safety_violations ( _, tenv, pname, pdesc) make_description trace tab = let open ThreadSafetyDomain in let trace_of_pname callee_pname = match Summary.read_summary pdesc callee_pname with - | Some (_, _, writes, _) -> - get_possibly_unsafe_writes writes - | _ -> - PathDomain.empty in + | Some (_, accesses, _) -> get_possibly_unsafe_writes accesses + | _ -> PathDomain.empty in let report_one_path ((_, sinks) as path) = let initial_sink, _ = List.last_exn sinks in let final_sink, _ = List.hd_exn sinks in @@ -1051,12 +1065,24 @@ let process_results_table file_env tab = (should_report_on_all_procs || is_thread_safe_method pdesc tenv) && should_report_on_proc proc_env in ResultsTableType.iter (* report errors for each method *) - (fun proc_env (_, reads, writes, _) -> - if should_report proc_env then + (fun proc_env (_, accesses, _) -> + if should_report proc_env + then + let open ThreadSafetyDomain in + let reads, writes = + AccessDomain.fold + (fun pre accesses (reads_acc, writes_acc) -> + let read_accesses, write_accesses = + PathDomain.Sinks.partition TraceElem.is_read (PathDomain.sinks accesses) in + AccessDomain.add pre (PathDomain.update_sinks accesses read_accesses) reads_acc, + AccessDomain.add pre (PathDomain.update_sinks accesses write_accesses) writes_acc) + accesses + (AccessDomain.empty, AccessDomain.empty) in begin report_thread_safety_violations proc_env make_unprotected_write_description (get_possibly_unsafe_writes writes) tab; - report_reads proc_env reads tab + let unsafe_reads = get_possibly_unsafe_reads reads in + report_reads proc_env unsafe_reads tab end ) tab diff --git a/infer/src/checkers/ThreadSafetyDomain.ml b/infer/src/checkers/ThreadSafetyDomain.ml index fa777b3fd..e66e9947f 100644 --- a/infer/src/checkers/ThreadSafetyDomain.ml +++ b/infer/src/checkers/ThreadSafetyDomain.ml @@ -13,14 +13,37 @@ module F = Format module AccessPathSetDomain = AbstractDomain.InvertedSet(AccessPath.UntypedRawSet) +module Access = struct + type kind = + | Read + | Write + [@@deriving compare] + + type t = AccessPath.Raw.t * kind [@@deriving compare] + + let pp fmt (access_path, access_kind) = match access_kind with + | Read -> F.fprintf fmt "Read of %a" AccessPath.Raw.pp access_path + | Write -> F.fprintf fmt "Write of %a" AccessPath.Raw.pp access_path +end + module TraceElem = struct - module Kind = AccessPath.Raw + module Kind = Access type t = { site : CallSite.t; kind : Kind.t; } [@@deriving compare] + let is_read { kind; } = + match snd kind with + | Read -> true + | Write -> false + + let is_write { kind; } = + match snd kind with + | Read -> false + | Write -> true + let call_site { site; } = site let kind { kind; } = kind @@ -30,7 +53,7 @@ module TraceElem = struct let with_callsite t site = { t with site; } let pp fmt { site; kind; } = - F.fprintf fmt "Unprotected access to %a at %a" Kind.pp kind CallSite.pp site + F.fprintf fmt "%a at %a" Access.pp kind CallSite.pp site module Set = PrettyPrintable.MakePPSet (struct type nonrec t = t @@ -39,9 +62,9 @@ module TraceElem = struct end) end -let make_access kind loc = +let make_access access_path access_kind loc = let site = CallSite.make Typ.Procname.empty_block loc in - TraceElem.make kind site + TraceElem.make (access_path, access_kind) site module LocksDomain = AbstractDomain.BooleanAnd @@ -125,30 +148,26 @@ end type astate = { locks : LocksDomain.astate; - reads : PathDomain.astate; - writes : AccessDomain.astate; + accesses : AccessDomain.astate; id_map : IdAccessPathMapDomain.astate; attribute_map : AttributeMapDomain.astate; } -type summary = - LocksDomain.astate * PathDomain.astate * AccessDomain.astate * AttributeSetDomain.astate +type summary = LocksDomain.astate * AccessDomain.astate * AttributeSetDomain.astate let empty = let locks = false in - let reads = PathDomain.empty in - let writes = AccessDomain.empty in + let accesses = AccessDomain.empty in let id_map = IdAccessPathMapDomain.empty in let attribute_map = AccessPath.UntypedRawMap.empty in - { locks; reads; writes; id_map; attribute_map; } + { locks; accesses; id_map; attribute_map; } let (<=) ~lhs ~rhs = if phys_equal lhs rhs then true else LocksDomain.(<=) ~lhs:lhs.locks ~rhs:rhs.locks && - PathDomain.(<=) ~lhs:lhs.reads ~rhs:rhs.reads && - AccessDomain.(<=) ~lhs:lhs.writes ~rhs:rhs.writes && + AccessDomain.(<=) ~lhs:lhs.accesses ~rhs:rhs.accesses && IdAccessPathMapDomain.(<=) ~lhs:lhs.id_map ~rhs:rhs.id_map && AttributeMapDomain.(<=) ~lhs:lhs.attribute_map ~rhs:rhs.attribute_map @@ -158,11 +177,10 @@ let join astate1 astate2 = astate1 else let locks = LocksDomain.join astate1.locks astate2.locks in - let reads = PathDomain.join astate1.reads astate2.reads in - let writes = AccessDomain.join astate1.writes astate2.writes in + let accesses = AccessDomain.join astate1.accesses astate2.accesses in let id_map = IdAccessPathMapDomain.join astate1.id_map astate2.id_map in let attribute_map = AttributeMapDomain.join astate1.attribute_map astate2.attribute_map in - { locks; reads; writes; id_map; attribute_map; } + { locks; accesses; id_map; attribute_map; } let widen ~prev ~next ~num_iters = if phys_equal prev next @@ -170,29 +188,26 @@ let widen ~prev ~next ~num_iters = prev else let locks = LocksDomain.widen ~prev:prev.locks ~next:next.locks ~num_iters in - let reads = PathDomain.widen ~prev:prev.reads ~next:next.reads ~num_iters in - let writes = AccessDomain.widen ~prev:prev.writes ~next:next.writes ~num_iters in + let accesses = AccessDomain.widen ~prev:prev.accesses ~next:next.accesses ~num_iters in let id_map = IdAccessPathMapDomain.widen ~prev:prev.id_map ~next:next.id_map ~num_iters in let attribute_map = AttributeMapDomain.widen ~prev:prev.attribute_map ~next:next.attribute_map ~num_iters in - { locks; reads; writes; id_map; attribute_map; } + { locks; accesses; id_map; attribute_map; } -let pp_summary fmt (locks, reads, writes, return_attributes) = +let pp_summary fmt (locks, accesses, return_attributes) = F.fprintf fmt - "Locks: %a Reads: %a Writes: %a Return Attributes: %a" + "Locks: %a Accesses %a Return Attributes: %a" LocksDomain.pp locks - PathDomain.pp reads - AccessDomain.pp writes + AccessDomain.pp accesses AttributeSetDomain.pp return_attributes -let pp fmt { locks; reads; writes; id_map; attribute_map; } = +let pp fmt { locks; accesses; id_map; attribute_map; } = F.fprintf fmt - "Locks: %a Reads: %a Writes: %a Id Map: %a Attribute Map:\ + "Locks: %a Accesses %a Id Map: %a Attribute Map:\ %a" LocksDomain.pp locks - PathDomain.pp reads - AccessDomain.pp writes + AccessDomain.pp accesses IdAccessPathMapDomain.pp id_map AttributeMapDomain.pp attribute_map diff --git a/infer/src/checkers/ThreadSafetyDomain.mli b/infer/src/checkers/ThreadSafetyDomain.mli index c509b5d4c..da52f326a 100644 --- a/infer/src/checkers/ThreadSafetyDomain.mli +++ b/infer/src/checkers/ThreadSafetyDomain.mli @@ -13,7 +13,24 @@ module F = Format module AccessPathSetDomain : module type of AbstractDomain.InvertedSet (AccessPath.UntypedRawSet) -module TraceElem : TraceElem.S with module Kind = AccessPath.Raw +module Access : sig + type kind = + | Read + | Write + [@@deriving compare] + + type t = AccessPath.Raw.t * kind [@@deriving compare] + + val pp : F.formatter -> t -> unit +end + +module TraceElem : sig + include TraceElem.S with module Kind = Access + + val is_write : t -> bool + + val is_read : t -> bool +end (** A bool that is true if a lock is definitely held. Note that this is unsound because it assumes the existence of one global lock. In the case that a lock is held on the access to a variable, @@ -83,10 +100,8 @@ type astate = { locks : LocksDomain.astate; (** boolean that is true if a lock must currently be held *) - reads : PathDomain.astate; - (** access paths read outside of synchronization *) - writes : AccessDomain.astate; - (** access paths written without ownership permissions *) + accesses : AccessDomain.astate; + (** read and writes accesses performed without ownership permissions *) id_map : IdAccessPathMapDomain.astate; (** map used to decompile temporary variables into access paths *) attribute_map : AttributeMapDomain.astate; @@ -95,11 +110,10 @@ type astate = (** same as astate, but without [id_map]/[owned] (since they are local) and with the addition of the attributes associated with the return value *) -type summary = - LocksDomain.astate * PathDomain.astate * AccessDomain.astate * AttributeSetDomain.astate +type summary = LocksDomain.astate * AccessDomain.astate * AttributeSetDomain.astate include AbstractDomain.WithBottom with type astate := astate -val make_access : AccessPath.Raw.t -> Location.t -> TraceElem.t +val make_access : AccessPath.Raw.t -> Access.kind -> Location.t -> TraceElem.t val pp_summary : F.formatter -> summary -> unit