diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index a309f46a0..ccd41c7fe 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/infer/src/checkers/ThreadSafety.ml @@ -68,10 +68,27 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | Exp.Const _ -> true | _ -> false - let is_owned access_path owned_set = - Domain.AccessPathSetDomain.mem access_path owned_set + let propagate_attributes lhs_access_path_opt rhs_access_path_opt rhs_exp attribute_map = + match lhs_access_path_opt, rhs_access_path_opt with + | Some lhs_access_path, Some rhs_access_path -> + let rhs_attributes = + try Domain.AttributeMapDomain.find rhs_access_path attribute_map + with Not_found -> Domain.AttributeSetDomain.empty in + Domain.AttributeMapDomain.add lhs_access_path rhs_attributes attribute_map + | Some lhs_access_path, None -> + let rhs_attributes = + if is_constant rhs_exp + then + (* constants are both owned and functional *) + Domain.AttributeSetDomain.of_list + [Domain.Attribute.Owned; Domain.Attribute.Functional] + else + Domain.AttributeSetDomain.empty in + Domain.AttributeMapDomain.add lhs_access_path rhs_attributes attribute_map + | _ -> + attribute_map - let add_path_to_state exp typ loc path_state id_map owned tenv = + let add_path_to_state exp typ loc path_state id_map attribute_map tenv = (* remove the last field of the access path, if it has any *) let truncate = function | base, [] @@ -103,7 +120,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct else IList.fold_left (fun acc rawpath -> - if not (is_owned (truncate rawpath) owned) && not (is_safe_write rawpath tenv) + if not (Domain.AttributeMapDomain.has_attribute + (truncate rawpath) Domain.Attribute.Owned attribute_map) && + not (is_safe_write rawpath tenv) then Domain.PathDomain.add_sink (Domain.make_access rawpath loc) acc else acc) path_state @@ -155,7 +174,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct loc astate.unconditional_writes astate.id_map - astate.owned + astate.attribute_map tenv in { astate with unconditional_writes; } in let is_unprotected is_locked = @@ -186,8 +205,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct begin match AccessPath.of_lhs_exp (Exp.Var lhs_id) lhs_typ ~f_resolve_id with | Some lhs_access_path -> - let owned = AccessPathSetDomain.add lhs_access_path astate.owned in - { astate with owned; } + let attribute_map = + AttributeMapDomain.add_attribute lhs_access_path Owned astate.attribute_map in + { astate with attribute_map; } | None -> astate end @@ -239,7 +259,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct 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.owned + if AttributeMapDomain.has_attribute + actual_access_path Owned 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 @@ -290,12 +311,13 @@ module TransferFunctions (CFG : ProcCfg.S) = struct { astate with reads; conditional_writes; unconditional_writes; } else astate in - let owned = match ret_opt with + let attribute_map = match ret_opt with | Some (ret_id, ret_typ) when is_retval_owned -> - AccessPathSetDomain.add (AccessPath.of_id ret_id ret_typ) astate'.owned + AttributeMapDomain.add_attribute + (AccessPath.of_id ret_id ret_typ) Owned astate'.attribute_map | _ -> - astate'.owned in - { astate' with locks = locks'; owned; } + astate'.attribute_map in + { astate' with locks = locks'; attribute_map; } | None -> if is_box callee_pname then @@ -303,11 +325,15 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | Some (ret_id, ret_typ), (actual_exp, actual_typ) :: _ -> begin match AccessPath.of_lhs_exp actual_exp actual_typ ~f_resolve_id with - | Some ap when AccessPathSetDomain.mem ap astate.functional -> - let functional = - AccessPathSetDomain.add - (AccessPath.of_id ret_id ret_typ) astate.functional in - { astate with functional; } + | Some ap + when AttributeMapDomain.has_attribute + ap Functional astate.attribute_map -> + let attribute_map = + AttributeMapDomain.add_attribute + (AccessPath.of_id ret_id ret_typ) + Functional + astate.attribute_map in + { astate with attribute_map; } | _ -> astate end @@ -323,10 +349,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct astate_callee | Some (ret_id, ret_typ) when proc_or_override_is_annotated callee_pname tenv Annotations.ia_is_functional -> - let functional = - AccessPathSetDomain.add - (AccessPath.of_id ret_id ret_typ) astate_callee.functional in - { astate_callee with functional; } + let attribute_map = + AttributeMapDomain.add_attribute + (AccessPath.of_id ret_id ret_typ) Functional astate.attribute_map in + { astate_callee with attribute_map; } | _ -> astate_callee end @@ -339,15 +365,17 @@ module TransferFunctions (CFG : ProcCfg.S) = struct 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 functional_set = + let is_marked_functional exp typ attribute_map = match AccessPath.of_lhs_exp exp typ ~f_resolve_id with - | Some access_path -> AccessPathSetDomain.mem access_path functional_set - | None -> false in + | Some access_path -> + AttributeMapDomain.has_attribute access_path Functional attribute_map + | None -> + false in let conditional_writes, unconditional_writes = match lhs_exp with | Lfield (base_exp, _, typ) when is_unprotected astate.locks (* abstracts no lock being held *) && - not (is_marked_functional rhs_exp lhs_typ astate.functional) -> + not (is_marked_functional rhs_exp lhs_typ astate.attribute_map) -> begin match get_formal_index base_exp typ with | Some formal_index -> @@ -361,7 +389,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct loc conditional_writes_for_index astate.id_map - astate.owned + astate.attribute_map tenv in ConditionalWritesDomain.add formal_index conditional_writes_for_index' astate.conditional_writes, @@ -374,7 +402,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct loc astate.unconditional_writes astate.id_map - astate.owned + astate.attribute_map tenv end | _ -> @@ -385,48 +413,26 @@ module TransferFunctions (CFG : ProcCfg.S) = struct loc and is now being reassigned *) let lhs_access_path_opt = AccessPath.of_lhs_exp lhs_exp lhs_typ ~f_resolve_id in let rhs_access_path_opt = AccessPath.of_lhs_exp rhs_exp lhs_typ ~f_resolve_id in - let update_access_path_set access_path_set = - match lhs_access_path_opt, rhs_access_path_opt with - | Some lhs_access_path, Some rhs_access_path -> - if AccessPathSetDomain.mem rhs_access_path access_path_set - then AccessPathSetDomain.add lhs_access_path access_path_set - else AccessPathSetDomain.remove lhs_access_path access_path_set - | Some lhs_access_path, None -> - if is_constant rhs_exp - then AccessPathSetDomain.add lhs_access_path access_path_set - else AccessPathSetDomain.remove lhs_access_path access_path_set - | _ -> - access_path_set in - let owned = update_access_path_set astate.owned in - let functional = update_access_path_set astate.functional in - { astate with conditional_writes; unconditional_writes; owned; functional; } + let attribute_map = + propagate_attributes + lhs_access_path_opt rhs_access_path_opt rhs_exp astate.attribute_map in + { astate with conditional_writes; unconditional_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 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.owned tenv + add_path_to_state rhs_exp typ loc astate.reads astate.id_map astate.attribute_map tenv | _ -> astate.reads in - (* if rhs is owned/functional, propagate to lhs *) - let owned, functional = - match AccessPath.of_lhs_exp rhs_exp rhs_typ ~f_resolve_id with - | Some rhs_access_path -> - let propagate_to_lhs access_path_set = - if AccessPathSetDomain.mem rhs_access_path access_path_set - then AccessPathSetDomain.add (AccessPath.of_id lhs_id rhs_typ) access_path_set - else access_path_set in - propagate_to_lhs astate.owned, propagate_to_lhs astate.functional - | _ -> - if is_constant rhs_exp - then - AccessPathSetDomain.add (AccessPath.of_id lhs_id rhs_typ) astate.owned, - astate.functional - else - astate.owned, astate.functional in - { astate with Domain.reads; id_map; owned; functional; } + let lhs_access_path_opt = Some (AccessPath.of_id lhs_id rhs_typ) in + let rhs_access_path_opt = AccessPath.of_lhs_exp rhs_exp rhs_typ ~f_resolve_id in + let attribute_map = + propagate_attributes + lhs_access_path_opt rhs_access_path_opt rhs_exp astate.attribute_map in + { astate with Domain.reads; id_map; attribute_map; } | Sil.Remove_temps (ids, _) -> let id_map = @@ -557,18 +563,23 @@ let make_results_table get_proc_desc file_env = (* express that the constructor owns [this] *) match FormalMap.get_formal_base 0 extras with | Some base -> - let owned = ThreadSafetyDomain.AccessPathSetDomain.singleton (base, []) in - { ThreadSafetyDomain.empty with owned; } + let attribute_map = + AttributeMapDomain.add_attribute + (base, []) + Owned + ThreadSafetyDomain.empty.attribute_map in + { ThreadSafetyDomain.empty with attribute_map; } | None -> ThreadSafetyDomain.empty else ThreadSafetyDomain.empty in match Analyzer.compute_post proc_data ~initial with - | Some { locks; reads; conditional_writes; unconditional_writes; owned; } -> + | Some { locks; reads; conditional_writes; unconditional_writes; attribute_map; } -> let return_var_ap = AccessPath.of_pvar (Pvar.get_ret_pvar (Procdesc.get_proc_name pdesc)) (Procdesc.get_ret_type pdesc) in - let return_is_owned = AccessPathSetDomain.mem return_var_ap owned in + let return_is_owned = + AttributeMapDomain.has_attribute return_var_ap Owned attribute_map in Some (locks, reads, conditional_writes, unconditional_writes, return_is_owned) | None -> None diff --git a/infer/src/checkers/ThreadSafetyDomain.ml b/infer/src/checkers/ThreadSafetyDomain.ml index 9cf71f0ca..0436f94bb 100644 --- a/infer/src/checkers/ThreadSafetyDomain.ml +++ b/infer/src/checkers/ThreadSafetyDomain.ml @@ -51,6 +51,43 @@ module IntMap = PrettyPrintable.MakePPMap(Int) module ConditionalWritesDomain = AbstractDomain.Map (IntMap) (PathDomain) +module Attribute = struct + type t = + | Owned + | Functional + [@@deriving compare] + + let pp fmt = function + | Owned -> F.fprintf fmt "Owned" + | Functional -> F.fprintf fmt "Functional" + + module Set = PrettyPrintable.MakePPSet(struct + type nonrec t = t + let compare = compare + let pp = pp + end) +end + +module AttributeSetDomain = AbstractDomain.InvertedSet (Attribute.Set) + +module AttributeMapDomain = struct + include AbstractDomain.InvertedMap (AccessPath.RawMap) (AttributeSetDomain) + + let has_attribute access_path attribute t = + try + find access_path t + |> AttributeSetDomain.mem attribute + with Not_found -> + false + + let add_attribute access_path attribute t = + let attribute_set = + (try find access_path t + with Not_found -> AttributeSetDomain.empty) + |> AttributeSetDomain.add attribute in + add access_path attribute_set t +end + type astate = { locks : LocksDomain.astate; @@ -58,11 +95,9 @@ type astate = conditional_writes : ConditionalWritesDomain.astate; unconditional_writes : PathDomain.astate; id_map : IdAccessPathMapDomain.astate; - owned : AccessPathSetDomain.astate; - functional : AccessPathSetDomain.astate; + attribute_map : AttributeMapDomain.astate; } - type summary = LocksDomain.astate * PathDomain.astate * ConditionalWritesDomain.astate * PathDomain.astate * bool @@ -72,9 +107,8 @@ let empty = let conditional_writes = ConditionalWritesDomain.empty in let unconditional_writes = PathDomain.empty in let id_map = IdAccessPathMapDomain.empty in - let owned = AccessPathSetDomain.empty in - let functional = AccessPathSetDomain.empty in - { locks; reads; conditional_writes; unconditional_writes; id_map; owned; functional; } + let attribute_map = AccessPath.RawMap.empty in + { locks; reads; conditional_writes; unconditional_writes; id_map; attribute_map; } let (<=) ~lhs ~rhs = if phys_equal lhs rhs @@ -85,7 +119,7 @@ let (<=) ~lhs ~rhs = ConditionalWritesDomain.(<=) ~lhs:lhs.conditional_writes ~rhs:rhs.conditional_writes && PathDomain.(<=) ~lhs:lhs.unconditional_writes ~rhs:rhs.unconditional_writes && IdAccessPathMapDomain.(<=) ~lhs:lhs.id_map ~rhs:rhs.id_map && - AccessPathSetDomain.(<=) ~lhs:lhs.owned ~rhs:rhs.owned + AttributeMapDomain.(<=) ~lhs:lhs.attribute_map ~rhs:rhs.attribute_map let join astate1 astate2 = if phys_equal astate1 astate2 @@ -99,9 +133,8 @@ let join astate1 astate2 = let unconditional_writes = PathDomain.join astate1.unconditional_writes astate2.unconditional_writes in let id_map = IdAccessPathMapDomain.join astate1.id_map astate2.id_map in - let owned = AccessPathSetDomain.join astate1.owned astate2.owned in - let functional = AccessPathSetDomain.join astate1.functional astate2.functional in - { locks; reads; conditional_writes; unconditional_writes; id_map; owned; functional; } + let attribute_map = AttributeMapDomain.join astate1.attribute_map astate2.attribute_map in + { locks; reads; conditional_writes; unconditional_writes; id_map; attribute_map; } let widen ~prev ~next ~num_iters = if phys_equal prev next @@ -116,10 +149,9 @@ let widen ~prev ~next ~num_iters = let unconditional_writes = PathDomain.widen ~prev:prev.unconditional_writes ~next:next.unconditional_writes ~num_iters in let id_map = IdAccessPathMapDomain.widen ~prev:prev.id_map ~next:next.id_map ~num_iters in - let owned = AccessPathSetDomain.widen ~prev:prev.owned ~next:next.owned ~num_iters in - let functional = - AccessPathSetDomain.widen ~prev:prev.functional ~next:next.functional ~num_iters in - { locks; reads; conditional_writes; unconditional_writes; id_map; owned; functional; } + 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; } let pp_summary fmt (locks, reads, conditional_writes, unconditional_writes, retval_owned) = F.fprintf @@ -131,15 +163,14 @@ let pp_summary fmt (locks, reads, conditional_writes, unconditional_writes, retv PathDomain.pp unconditional_writes retval_owned -let pp fmt { locks; reads; conditional_writes; unconditional_writes; id_map; owned; functional; } = +let pp fmt { locks; reads; conditional_writes; unconditional_writes; id_map; attribute_map; } = F.fprintf fmt - "Locks: %a Reads: %a Conditional Writes: %a Unconditional Writes: %a Id Map: %a Owned: %a\ - Functional: %a" + "Locks: %a Reads: %a Conditional Writes: %a Unconditional Writes: %a Id Map: %a Attribute Map:\ + %a" LocksDomain.pp locks PathDomain.pp reads ConditionalWritesDomain.pp conditional_writes PathDomain.pp unconditional_writes IdAccessPathMapDomain.pp id_map - AccessPathSetDomain.pp owned - AccessPathSetDomain.pp functional + AttributeMapDomain.pp attribute_map diff --git a/infer/src/checkers/ThreadSafetyDomain.mli b/infer/src/checkers/ThreadSafetyDomain.mli index d498d6ab9..5429f0767 100644 --- a/infer/src/checkers/ThreadSafetyDomain.mli +++ b/infer/src/checkers/ThreadSafetyDomain.mli @@ -28,6 +28,27 @@ module IntMap : PrettyPrintable.PPMap with type key = int module ConditionalWritesDomain : module type of (AbstractDomain.Map (IntMap) (PathDomain)) +module Attribute : sig + type t = + | Owned + | Functional + [@@deriving compare] + + val pp : F.formatter -> t -> unit + + module Set : PrettyPrintable.PPSet with type elt = t +end + +module AttributeSetDomain : module type of AbstractDomain.InvertedSet (Attribute.Set) + +module AttributeMapDomain : sig + include module type of AbstractDomain.InvertedMap (AccessPath.RawMap) (AttributeSetDomain) + + val has_attribute : AccessPath.Raw.t -> Attribute.t -> astate -> bool + + 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 @@ -55,10 +76,8 @@ type astate = (** access paths written outside of synchronization *) id_map : IdAccessPathMapDomain.astate; (** map used to decompile temporary variables into access paths *) - owned : AccessPathSetDomain.astate; - (** access paths that must be owned by the current function *) - functional : AccessPathSetDomain.astate; - (** access paths holding values returned from a call marked with @Functional *) + attribute_map : AttributeMapDomain.astate; + (** map of access paths to attributes such as owned, functional, ... *) } (** same as astate, but without [id_map]/[owned] (since they are local) and with the addition of a diff --git a/infer/src/checkers/accessPath.ml b/infer/src/checkers/accessPath.ml index de83de8bd..4e82a3e93 100644 --- a/infer/src/checkers/accessPath.ml +++ b/infer/src/checkers/accessPath.ml @@ -161,3 +161,5 @@ module AccessMap = PrettyPrintable.MakePPMap(struct end) module RawSet = PrettyPrintable.MakePPSet(Raw) + +module RawMap = PrettyPrintable.MakePPMap(Raw) diff --git a/infer/src/checkers/accessPath.mli b/infer/src/checkers/accessPath.mli index b65ba3ef1..6336b6686 100644 --- a/infer/src/checkers/accessPath.mli +++ b/infer/src/checkers/accessPath.mli @@ -89,3 +89,5 @@ module BaseMap : PrettyPrintable.PPMap with type key = base module AccessMap : PrettyPrintable.PPMap with type key = access module RawSet : PrettyPrintable.PPSet with type elt = Raw.t + +module RawMap : PrettyPrintable.PPMap with type key = Raw.t