From 5890007f8e6b96cacd37596e8be3e7e9bb57c45c Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Mon, 6 Mar 2017 12:42:01 -0800 Subject: [PATCH] [thread-safety] AccessDomain for better tracking of writes Summary: In order to be able to report races like ``` synchronized write() { this.f = ... } read() { return this.f; } ``` , we need to track writes that happen inside of synchronization as well as writes that happen outside of synchronization. This diff takes a step toward making that possible by defining an "AccessDomain" mapping a precondition for the safety of a write ( {Safe, SafeIf i, Unsafe} =~ {true, owned(i), false} ) to a set of writes that are safe if the precondition will hold. We're not actually tracking safe writes yet, but this domain will make it easy to do so. This also lets us kill the conditional writes/unconditional writes combo, which was a bit clumsy Reviewed By: peterogithub Differential Revision: D4620153 fbshipit-source-id: 2d9c5ef --- infer/src/checkers/ThreadSafety.ml | 224 +++++++++++----------- infer/src/checkers/ThreadSafetyDomain.ml | 85 ++++---- infer/src/checkers/ThreadSafetyDomain.mli | 56 +++--- 3 files changed, 188 insertions(+), 177 deletions(-) diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index 1ffed9c9c..3f189ed3b 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/infer/src/checkers/ThreadSafety.ml @@ -289,22 +289,16 @@ module TransferFunctions (CFG : ProcCfg.S) = struct (Mangled.from_string (container_write_string ^ (Procname.get_method callee_pname))) 0 in let dummy_access_exp = Exp.Lfield (receiver_exp, dummy_fieldname, receiver_typ) in - let callee_conditional_writes = + let callee_writes = match AccessPath.of_lhs_exp dummy_access_exp receiver_typ ~f_resolve_id with | Some container_ap -> - let writes = - PathDomain.add_sink - (make_access container_ap callee_loc) - PathDomain.empty in - ConditionalWritesDomain.add 0 writes ConditionalWritesDomain.empty + AccessDomain.add_access + (ProtectedIf (Some 0)) + (make_access container_ap callee_loc) + AccessDomain.empty | None -> - ConditionalWritesDomain.empty in - Some - (false, - PathDomain.empty, - callee_conditional_writes, - PathDomain.empty, - AttributeSetDomain.empty) + AccessDomain.empty in + Some (false, PathDomain.empty, callee_writes, AttributeSetDomain.empty) | _ -> failwithf "Call to %a is marked as a container write, but has no receiver" @@ -375,79 +369,79 @@ module TransferFunctions (CFG : ProcCfg.S) = struct get_summary pdesc callee_pname actuals ~f_resolve_id loc tenv with | Some (callee_locks, callee_reads, - callee_conditional_writes, - callee_unconditional_writes, + callee_writes, return_attributes) -> let locks' = callee_locks || astate.locks in let astate' = if is_unprotected locks' then let call_site = CallSite.make callee_pname loc in - (* add the conditional writes rooted in the callee formal at [index] to - the current state *) - let add_conditional_writes - index ((cond_writes, uncond_writes) as acc) (actual_exp, actual_typ) = + let add_conditional_writes index writes_acc (actual_exp, actual_typ) = if is_constant actual_exp then - acc + (* the actual is a constant, so it's owned in the caller. *) + writes_acc else - try - let callee_cond_writes_for_index' = - let callee_cond_writes_for_index = - ConditionalWritesDomain.find index callee_conditional_writes in - PathDomain.with_callsite callee_cond_writes_for_index call_site in - begin - match AccessPath.of_lhs_exp actual_exp actual_typ ~f_resolve_id with - | Some actual_access_path -> - if is_owned actual_access_path astate.attribute_map - then - (* the actual passed to the current callee is owned. drop all - the conditional writes for that actual, since they're all - safe *) - acc - else - let base = fst actual_access_path in - begin - match FormalMap.get_formal_index base extras with - | Some formal_index -> - (* the actual passed to the current callee is rooted in - a formal. add to conditional writes *) - let conditional_writes' = - try - ConditionalWritesDomain.find - formal_index cond_writes - |> PathDomain.join callee_cond_writes_for_index' - with Not_found -> - callee_cond_writes_for_index' in - let cond_writes' = - ConditionalWritesDomain.add - formal_index conditional_writes' cond_writes in - cond_writes', uncond_writes - | None -> - (* access path not owned and not rooted in a formal. add - to unconditional writes *) - cond_writes, - PathDomain.join - uncond_writes callee_cond_writes_for_index' - end - | _ -> - cond_writes, - PathDomain.join uncond_writes callee_cond_writes_for_index' - end - with Not_found -> - acc in - let conditional_writes, unconditional_writes = - let combined_unconditional_writes = - PathDomain.with_callsite callee_unconditional_writes call_site - |> PathDomain.join astate.unconditional_writes in - List.foldi - ~f:add_conditional_writes - ~init:(astate.conditional_writes, combined_unconditional_writes) - actuals in + let callee_conditional_writes = + PathDomain.with_callsite + (AccessDomain.get_accesses (ProtectedIf (Some index)) callee_writes) + call_site in + begin + match AccessPath.of_lhs_exp actual_exp actual_typ ~f_resolve_id with + | Some actual_access_path -> + if is_owned actual_access_path astate.attribute_map + 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 + else + let base = fst actual_access_path in + begin + match FormalMap.get_formal_index base extras with + | Some formal_index -> + (* the actual passed to the current callee is rooted in a + formal. add to conditional writes *) + PathDomain.Sinks.fold + (AccessDomain.add_access + (ProtectedIf (Some formal_index))) + (PathDomain.sinks callee_conditional_writes) + writes_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 + end + | None -> + PathDomain.Sinks.fold + (AccessDomain.add_access AccessPrecondition.unprotected) + (PathDomain.sinks callee_conditional_writes) + writes_acc + end in + let reads = PathDomain.with_callsite callee_reads call_site |> PathDomain.join astate.reads in - { astate with reads; conditional_writes; unconditional_writes; } + let combined_unsafe_writes = + PathDomain.with_callsite + (AccessDomain.get_accesses AccessPrecondition.unprotected callee_writes) + call_site + |> PathDomain.join + (AccessDomain.get_accesses + AccessPrecondition.unprotected astate.writes) in + let writes_with_unsafe = + AccessDomain.add + AccessPrecondition.unprotected + combined_unsafe_writes + astate.writes in + let writes = + List.foldi + ~f:add_conditional_writes + ~init:writes_with_unsafe + actuals in + { astate with reads; writes; } else astate in let attribute_map = @@ -532,7 +526,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct AttributeMapDomain.has_attribute access_path Functional attribute_map | None -> false in - let conditional_writes, unconditional_writes = + let writes = match lhs_exp with | Lfield (base_exp, _, typ) when is_unprotected astate.locks (* abstracts no lock being held *) && @@ -540,34 +534,35 @@ module TransferFunctions (CFG : ProcCfg.S) = struct begin match get_formal_index base_exp typ with | Some formal_index -> - let conditional_writes_for_index = - try ConditionalWritesDomain.find formal_index astate.conditional_writes - with Not_found -> PathDomain.empty in - let conditional_writes_for_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_index + conditional_writes_for_pre astate.id_map astate.attribute_map tenv in - ConditionalWritesDomain.add - formal_index conditional_writes_for_index' astate.conditional_writes, - astate.unconditional_writes + AccessDomain.add pre conditional_writes_for_pre' astate.writes | None -> - astate.conditional_writes, - add_path_to_state - lhs_exp - typ - loc - astate.unconditional_writes - astate.id_map - astate.attribute_map - tenv + 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 end | _ -> - astate.conditional_writes, astate.unconditional_writes in + astate.writes in let attribute_map = match AccessPath.of_lhs_exp lhs_exp lhs_typ ~f_resolve_id with | Some lhs_access_path -> @@ -575,7 +570,7 @@ 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 conditional_writes; unconditional_writes; attribute_map; } + { astate with writes; 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 @@ -729,7 +724,7 @@ let make_results_table get_proc_desc file_env = let has_lock = false in let return_attrs = AttributeSetDomain.empty in let empty = - has_lock, PathDomain.empty, ConditionalWritesDomain.empty, PathDomain.empty, return_attrs in + has_lock, PathDomain.empty, 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 @@ -752,7 +747,7 @@ let make_results_table get_proc_desc file_env = else ThreadSafetyDomain.empty in match Analyzer.compute_post proc_data ~initial with - | Some { locks; reads; conditional_writes; unconditional_writes; attribute_map; } -> + | Some { locks; reads; writes; attribute_map; } -> let return_var_ap = AccessPath.of_pvar (Pvar.get_ret_pvar (Procdesc.get_proc_name pdesc)) @@ -760,7 +755,7 @@ let make_results_table get_proc_desc file_env = let return_attributes = try AttributeMapDomain.find return_var_ap attribute_map with Not_found -> AttributeSetDomain.empty in - Some (locks, reads, conditional_writes, unconditional_writes, return_attributes) + Some (locks, reads, writes, return_attributes) | None -> None end @@ -802,16 +797,16 @@ let calculate_addendum_message tenv pname = else "" | _ -> "" - -let combine_conditional_unconditional_writes conditional_writes unconditional_writes = +let get_possibly_unsafe_writes writes = let open ThreadSafetyDomain in - ConditionalWritesDomain.fold - (fun _ writes acc -> PathDomain.join writes acc) - conditional_writes - unconditional_writes - -let equal_locs (sink1 : ThreadSafetyDomain.TraceElem.t) - (sink2 : ThreadSafetyDomain.TraceElem.t) = + AccessDomain.fold + (fun attribute accesses acc -> match attribute with + | ProtectedIf _ -> PathDomain.join accesses acc + | Protected -> acc) + writes + PathDomain.empty + +let equal_locs (sink1 : ThreadSafetyDomain.TraceElem.t) (sink2 : ThreadSafetyDomain.TraceElem.t) = Location.equal (CallSite.loc (ThreadSafetyDomain.TraceElem.call_site sink1)) (CallSite.loc (ThreadSafetyDomain.TraceElem.call_site sink2)) @@ -844,10 +839,9 @@ let filter_conflicting_sinks sink trace = let collect_conflicting_writes sink tab = let procs_and_writes = List.map - ~f:(fun (key,(_, _, conditional_writes, unconditional_writes, _)) -> + ~f:(fun (key,(_, _, writes, _)) -> let conflicting_writes = - combine_conditional_unconditional_writes - conditional_writes unconditional_writes + get_possibly_unsafe_writes writes |> filter_conflicting_sinks sink in key, conflicting_writes ) @@ -907,8 +901,8 @@ let report_thread_safety_violations ( _, tenv, pname, pdesc) make_description tr let open ThreadSafetyDomain in let trace_of_pname callee_pname = match Summary.read_summary pdesc callee_pname with - | Some (_, _, conditional_writes, unconditional_writes, _) -> - combine_conditional_unconditional_writes conditional_writes unconditional_writes + | Some (_, _, writes, _) -> + get_possibly_unsafe_writes writes | _ -> PathDomain.empty in let report_one_path ((_, sinks) as path) = @@ -1024,14 +1018,12 @@ 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, conditional_writes, unconditional_writes, _) -> + (fun proc_env (_, reads, writes, _) -> if should_report proc_env then - let writes = combine_conditional_unconditional_writes - conditional_writes unconditional_writes in begin report_thread_safety_violations - proc_env make_unprotected_write_description writes tab - ; report_reads proc_env reads tab + proc_env make_unprotected_write_description (get_possibly_unsafe_writes writes) tab; + report_reads proc_env reads tab end ) tab diff --git a/infer/src/checkers/ThreadSafetyDomain.ml b/infer/src/checkers/ThreadSafetyDomain.ml index 3d9596af4..852143a50 100644 --- a/infer/src/checkers/ThreadSafetyDomain.ml +++ b/infer/src/checkers/ThreadSafetyDomain.ml @@ -47,10 +47,6 @@ module LocksDomain = AbstractDomain.BooleanAnd module PathDomain = SinkTrace.Make(TraceElem) -module IntMap = PrettyPrintable.MakePPMap(Int) - -module ConditionalWritesDomain = AbstractDomain.Map (IntMap) (PathDomain) - module Attribute = struct type t = | OwnedIf of int option @@ -91,31 +87,60 @@ module AttributeMapDomain = struct add access_path attribute_set t end +module AccessPrecondition = struct + type t = + | Protected + | ProtectedIf of int option + [@@deriving compare] + + let unprotected = ProtectedIf None + + let pp fmt = function + | Protected -> F.fprintf fmt "Protected" + | ProtectedIf (Some index) -> F.fprintf fmt "ProtectedIf %d" index + | ProtectedIf None -> F.fprintf fmt "Unprotected" + + module Map = PrettyPrintable.MakePPMap(struct + type nonrec t = t + let compare = compare + let pp = pp + end) +end + +module AccessDomain = struct + include AbstractDomain.Map (AccessPrecondition.Map) (PathDomain) + + let add_access precondition access_path t = + let precondition_accesses = + try find precondition t + with Not_found -> PathDomain.empty in + let precondition_accesses' = PathDomain.add_sink access_path precondition_accesses in + add precondition precondition_accesses' t + + let get_accesses precondition t = + try find precondition t + with Not_found -> PathDomain.empty +end + type astate = { locks : LocksDomain.astate; reads : PathDomain.astate; - conditional_writes : ConditionalWritesDomain.astate; - unconditional_writes : PathDomain.astate; + writes : AccessDomain.astate; id_map : IdAccessPathMapDomain.astate; attribute_map : AttributeMapDomain.astate; } type summary = - LocksDomain.astate * - PathDomain.astate * - ConditionalWritesDomain.astate * - PathDomain.astate * - AttributeSetDomain.astate + LocksDomain.astate * PathDomain.astate * AccessDomain.astate * AttributeSetDomain.astate let empty = let locks = false in let reads = PathDomain.empty in - let conditional_writes = ConditionalWritesDomain.empty in - let unconditional_writes = PathDomain.empty in + let writes = AccessDomain.empty in let id_map = IdAccessPathMapDomain.empty in let attribute_map = AccessPath.UntypedRawMap.empty in - { locks; reads; conditional_writes; unconditional_writes; id_map; attribute_map; } + { locks; reads; writes; id_map; attribute_map; } let (<=) ~lhs ~rhs = if phys_equal lhs rhs @@ -123,8 +148,7 @@ let (<=) ~lhs ~rhs = else LocksDomain.(<=) ~lhs:lhs.locks ~rhs:rhs.locks && PathDomain.(<=) ~lhs:lhs.reads ~rhs:rhs.reads && - ConditionalWritesDomain.(<=) ~lhs:lhs.conditional_writes ~rhs:rhs.conditional_writes && - PathDomain.(<=) ~lhs:lhs.unconditional_writes ~rhs:rhs.unconditional_writes && + AccessDomain.(<=) ~lhs:lhs.writes ~rhs:rhs.writes && IdAccessPathMapDomain.(<=) ~lhs:lhs.id_map ~rhs:rhs.id_map && AttributeMapDomain.(<=) ~lhs:lhs.attribute_map ~rhs:rhs.attribute_map @@ -135,13 +159,10 @@ let join astate1 astate2 = else let locks = LocksDomain.join astate1.locks astate2.locks in let reads = PathDomain.join astate1.reads astate2.reads in - let conditional_writes = - ConditionalWritesDomain.join astate1.conditional_writes astate2.conditional_writes in - let unconditional_writes = - PathDomain.join astate1.unconditional_writes astate2.unconditional_writes in + let writes = AccessDomain.join astate1.writes astate2.writes 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; conditional_writes; unconditional_writes; id_map; attribute_map; } + { locks; reads; writes; id_map; attribute_map; } let widen ~prev ~next ~num_iters = if phys_equal prev next @@ -150,34 +171,28 @@ let widen ~prev ~next ~num_iters = 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 conditional_writes = - ConditionalWritesDomain.widen - ~prev:prev.conditional_writes ~next:next.conditional_writes ~num_iters in - let unconditional_writes = - PathDomain.widen ~prev:prev.unconditional_writes ~next:next.unconditional_writes ~num_iters in + let writes = AccessDomain.widen ~prev:prev.writes ~next:next.writes ~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; conditional_writes; unconditional_writes; id_map; attribute_map; } + { locks; reads; writes; id_map; attribute_map; } -let pp_summary fmt (locks, reads, conditional_writes, unconditional_writes, return_attributes) = +let pp_summary fmt (locks, reads, writes, return_attributes) = F.fprintf fmt - "Locks: %a Reads: %a Conditional Writes: %a Unconditional Writes: %a Return Attributes: %a" + "Locks: %a Reads: %a Writes: %a Return Attributes: %a" LocksDomain.pp locks PathDomain.pp reads - ConditionalWritesDomain.pp conditional_writes - PathDomain.pp unconditional_writes + AccessDomain.pp writes AttributeSetDomain.pp return_attributes -let pp fmt { locks; reads; conditional_writes; unconditional_writes; id_map; attribute_map; } = +let pp fmt { locks; reads; writes; id_map; attribute_map; } = F.fprintf fmt - "Locks: %a Reads: %a Conditional Writes: %a Unconditional Writes: %a Id Map: %a Attribute Map:\ + "Locks: %a Reads: %a Writes: %a Id Map: %a Attribute Map:\ %a" LocksDomain.pp locks PathDomain.pp reads - ConditionalWritesDomain.pp conditional_writes - PathDomain.pp unconditional_writes + AccessDomain.pp writes IdAccessPathMapDomain.pp id_map AttributeMapDomain.pp attribute_map diff --git a/infer/src/checkers/ThreadSafetyDomain.mli b/infer/src/checkers/ThreadSafetyDomain.mli index cfe139fda..c509b5d4c 100644 --- a/infer/src/checkers/ThreadSafetyDomain.mli +++ b/infer/src/checkers/ThreadSafetyDomain.mli @@ -24,10 +24,6 @@ module LocksDomain : AbstractDomain.S with type astate = bool module PathDomain : module type of SinkTrace.Make(TraceElem) -module IntMap : PrettyPrintable.PPMap with type key = int - -module ConditionalWritesDomain : module type of (AbstractDomain.Map (IntMap) (PathDomain)) - module Attribute : sig type t = | OwnedIf of int option @@ -54,31 +50,43 @@ module AttributeMapDomain : sig val add_attribute : AccessPath.Raw.t -> Attribute.t -> astate -> astate end -(** the primary role of this domain is tracking *conditional* and *unconditional* writes. - conditional writes are writes that are rooted in a formal of the current procedure, and they - are safe only if the actual bound to that formal is owned at the call site (as in the foo - example below). Unconditional writes are rooted in a local, and they are only safe if a lock is - held in the caller. - To demonstrate what conditional writes buy us, consider the following example: +module AccessPrecondition : sig + type t = + | Protected + (** access safe due to held lock (i.e., pre is true *) + | ProtectedIf of int option + (** access safe if the formal at index i is owned (i.e., pre is owned(i)). + ProtectedIf None means unsafe (i.e., pre is false) *) + [@@deriving compare] + + (** type of an unprotected access *) + val unprotected : t + + val pp : F.formatter -> t -> unit + + module Map : PrettyPrintable.PPMap with type key = t +end + +(** map of access precondition |-> set of accesses. the map should hold all accesses to a + possibly-unowned access path *) +module AccessDomain : sig + include module type of AbstractDomain.Map (AccessPrecondition.Map) (PathDomain) + + (* add the given (access, precondition) pair to the map *) + val add_access : AccessPrecondition.t -> TraceElem.t -> astate -> astate - foo() { - Object local = new Object(); - iWriteToAField(local); - } + (* get all accesses with the given precondition *) + val get_accesses : AccessPrecondition.t -> astate -> PathDomain.astate +end - We don't want to warn on this example because the object pointed to by local is owned by the - caller foo, then ownership is transferred to the callee iWriteToAField. *) 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 *) - conditional_writes : ConditionalWritesDomain.astate; - (** map of (formal index) -> set of access paths rooted in the formal index that are read - outside of synrchonization if the formal is not owned by the caller *) - unconditional_writes : PathDomain.astate; - (** access paths written outside of synchronization *) + writes : AccessDomain.astate; + (** access paths written without ownership permissions *) id_map : IdAccessPathMapDomain.astate; (** map used to decompile temporary variables into access paths *) attribute_map : AttributeMapDomain.astate; @@ -88,11 +96,7 @@ 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 * - ConditionalWritesDomain.astate * - PathDomain.astate * - AttributeSetDomain.astate + LocksDomain.astate * PathDomain.astate * AccessDomain.astate * AttributeSetDomain.astate include AbstractDomain.WithBottom with type astate := astate