[thread-safety] use map of access paths to attributes rather than multiple sets of access paths

Summary: This will make it a cinch to track new "attributes" of memory locations, and to propagate more complex attributes such as conditional ownership (coming in a future diff).

Reviewed By: peterogithub

Differential Revision: D4523143

fbshipit-source-id: 57aa133
master
Sam Blackshear 8 years ago committed by Facebook Github Bot
parent a3cffa7116
commit dc9892eef5

@ -68,10 +68,27 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| Exp.Const _ -> true | Exp.Const _ -> true
| _ -> false | _ -> false
let is_owned access_path owned_set = let propagate_attributes lhs_access_path_opt rhs_access_path_opt rhs_exp attribute_map =
Domain.AccessPathSetDomain.mem access_path owned_set 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 *) (* remove the last field of the access path, if it has any *)
let truncate = function let truncate = function
| base, [] | base, []
@ -103,7 +120,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
else else
IList.fold_left IList.fold_left
(fun acc rawpath -> (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 then Domain.PathDomain.add_sink (Domain.make_access rawpath loc) acc
else acc) else acc)
path_state path_state
@ -155,7 +174,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
loc loc
astate.unconditional_writes astate.unconditional_writes
astate.id_map astate.id_map
astate.owned astate.attribute_map
tenv in tenv in
{ astate with unconditional_writes; } in { astate with unconditional_writes; } in
let is_unprotected is_locked = let is_unprotected is_locked =
@ -186,8 +205,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
begin begin
match AccessPath.of_lhs_exp (Exp.Var lhs_id) lhs_typ ~f_resolve_id with match AccessPath.of_lhs_exp (Exp.Var lhs_id) lhs_typ ~f_resolve_id with
| Some lhs_access_path -> | Some lhs_access_path ->
let owned = AccessPathSetDomain.add lhs_access_path astate.owned in let attribute_map =
{ astate with owned; } AttributeMapDomain.add_attribute lhs_access_path Owned astate.attribute_map in
{ astate with attribute_map; }
| None -> | None ->
astate astate
end end
@ -239,7 +259,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
begin begin
match AccessPath.of_lhs_exp actual_exp actual_typ ~f_resolve_id with match AccessPath.of_lhs_exp actual_exp actual_typ ~f_resolve_id with
| Some actual_access_path -> | Some actual_access_path ->
if is_owned actual_access_path astate.owned if AttributeMapDomain.has_attribute
actual_access_path Owned astate.attribute_map
then then
(* the actual passed to the current callee is owned. drop all (* the actual passed to the current callee is owned. drop all
the conditional writes for that actual, since they're 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; } { astate with reads; conditional_writes; unconditional_writes; }
else else
astate in astate in
let owned = match ret_opt with let attribute_map = match ret_opt with
| Some (ret_id, ret_typ) when is_retval_owned -> | 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'.attribute_map in
{ astate' with locks = locks'; owned; } { astate' with locks = locks'; attribute_map; }
| None -> | None ->
if is_box callee_pname if is_box callee_pname
then then
@ -303,11 +325,15 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| Some (ret_id, ret_typ), (actual_exp, actual_typ) :: _ -> | Some (ret_id, ret_typ), (actual_exp, actual_typ) :: _ ->
begin begin
match AccessPath.of_lhs_exp actual_exp actual_typ ~f_resolve_id with match AccessPath.of_lhs_exp actual_exp actual_typ ~f_resolve_id with
| Some ap when AccessPathSetDomain.mem ap astate.functional -> | Some ap
let functional = when AttributeMapDomain.has_attribute
AccessPathSetDomain.add ap Functional astate.attribute_map ->
(AccessPath.of_id ret_id ret_typ) astate.functional in let attribute_map =
{ astate with functional; } AttributeMapDomain.add_attribute
(AccessPath.of_id ret_id ret_typ)
Functional
astate.attribute_map in
{ astate with attribute_map; }
| _ -> | _ ->
astate astate
end end
@ -323,10 +349,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
astate_callee astate_callee
| Some (ret_id, ret_typ) when | Some (ret_id, ret_typ) when
proc_or_override_is_annotated callee_pname tenv Annotations.ia_is_functional -> proc_or_override_is_annotated callee_pname tenv Annotations.ia_is_functional ->
let functional = let attribute_map =
AccessPathSetDomain.add AttributeMapDomain.add_attribute
(AccessPath.of_id ret_id ret_typ) astate_callee.functional in (AccessPath.of_id ret_id ret_typ) Functional astate.attribute_map in
{ astate_callee with functional; } { astate_callee with attribute_map; }
| _ -> | _ ->
astate_callee astate_callee
end 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 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 | Some (base, _) -> FormalMap.get_formal_index base extras
| None -> None in | 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 match AccessPath.of_lhs_exp exp typ ~f_resolve_id with
| Some access_path -> AccessPathSetDomain.mem access_path functional_set | Some access_path ->
| None -> false in AttributeMapDomain.has_attribute access_path Functional attribute_map
| None ->
false in
let conditional_writes, unconditional_writes = let conditional_writes, unconditional_writes =
match lhs_exp with match lhs_exp with
| Lfield (base_exp, _, typ) | Lfield (base_exp, _, typ)
when is_unprotected astate.locks (* abstracts no lock being held *) && 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 begin
match get_formal_index base_exp typ with match get_formal_index base_exp typ with
| Some formal_index -> | Some formal_index ->
@ -361,7 +389,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
loc loc
conditional_writes_for_index conditional_writes_for_index
astate.id_map astate.id_map
astate.owned astate.attribute_map
tenv in tenv in
ConditionalWritesDomain.add ConditionalWritesDomain.add
formal_index conditional_writes_for_index' astate.conditional_writes, formal_index conditional_writes_for_index' astate.conditional_writes,
@ -374,7 +402,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
loc loc
astate.unconditional_writes astate.unconditional_writes
astate.id_map astate.id_map
astate.owned astate.attribute_map
tenv tenv
end end
| _ -> | _ ->
@ -385,48 +413,26 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
loc and is now being reassigned *) loc and is now being reassigned *)
let lhs_access_path_opt = AccessPath.of_lhs_exp lhs_exp lhs_typ ~f_resolve_id in 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 rhs_access_path_opt = AccessPath.of_lhs_exp rhs_exp lhs_typ ~f_resolve_id in
let update_access_path_set access_path_set = let attribute_map =
match lhs_access_path_opt, rhs_access_path_opt with propagate_attributes
| Some lhs_access_path, Some rhs_access_path -> lhs_access_path_opt rhs_access_path_opt rhs_exp astate.attribute_map in
if AccessPathSetDomain.mem rhs_access_path access_path_set { astate with conditional_writes; unconditional_writes; attribute_map; }
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; }
| Sil.Load (lhs_id, rhs_exp, rhs_typ, loc) -> | 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 id_map = analyze_id_assignment (Var.of_id lhs_id) rhs_exp rhs_typ astate in
let reads = let reads =
match rhs_exp with match rhs_exp with
| Lfield ( _, _, typ) when is_unprotected astate.locks -> | 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 astate.reads in
(* if rhs is owned/functional, propagate to lhs *) (* if rhs is owned/functional, propagate to lhs *)
let owned, functional = let lhs_access_path_opt = Some (AccessPath.of_id lhs_id rhs_typ) in
match AccessPath.of_lhs_exp rhs_exp rhs_typ ~f_resolve_id with let rhs_access_path_opt = AccessPath.of_lhs_exp rhs_exp rhs_typ ~f_resolve_id in
| Some rhs_access_path -> let attribute_map =
let propagate_to_lhs access_path_set = propagate_attributes
if AccessPathSetDomain.mem rhs_access_path access_path_set lhs_access_path_opt rhs_access_path_opt rhs_exp astate.attribute_map in
then AccessPathSetDomain.add (AccessPath.of_id lhs_id rhs_typ) access_path_set { astate with Domain.reads; id_map; attribute_map; }
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; }
| Sil.Remove_temps (ids, _) -> | Sil.Remove_temps (ids, _) ->
let id_map = let id_map =
@ -557,18 +563,23 @@ let make_results_table get_proc_desc file_env =
(* express that the constructor owns [this] *) (* express that the constructor owns [this] *)
match FormalMap.get_formal_base 0 extras with match FormalMap.get_formal_base 0 extras with
| Some base -> | Some base ->
let owned = ThreadSafetyDomain.AccessPathSetDomain.singleton (base, []) in let attribute_map =
{ ThreadSafetyDomain.empty with owned; } AttributeMapDomain.add_attribute
(base, [])
Owned
ThreadSafetyDomain.empty.attribute_map in
{ ThreadSafetyDomain.empty with attribute_map; }
| None -> ThreadSafetyDomain.empty | None -> ThreadSafetyDomain.empty
else else
ThreadSafetyDomain.empty in ThreadSafetyDomain.empty in
match Analyzer.compute_post proc_data ~initial with 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 = let return_var_ap =
AccessPath.of_pvar AccessPath.of_pvar
(Pvar.get_ret_pvar (Procdesc.get_proc_name pdesc)) (Pvar.get_ret_pvar (Procdesc.get_proc_name pdesc))
(Procdesc.get_ret_type pdesc) in (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) Some (locks, reads, conditional_writes, unconditional_writes, return_is_owned)
| None -> | None ->
None None

@ -51,6 +51,43 @@ module IntMap = PrettyPrintable.MakePPMap(Int)
module ConditionalWritesDomain = AbstractDomain.Map (IntMap) (PathDomain) 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 = type astate =
{ {
locks : LocksDomain.astate; locks : LocksDomain.astate;
@ -58,11 +95,9 @@ type astate =
conditional_writes : ConditionalWritesDomain.astate; conditional_writes : ConditionalWritesDomain.astate;
unconditional_writes : PathDomain.astate; unconditional_writes : PathDomain.astate;
id_map : IdAccessPathMapDomain.astate; id_map : IdAccessPathMapDomain.astate;
owned : AccessPathSetDomain.astate; attribute_map : AttributeMapDomain.astate;
functional : AccessPathSetDomain.astate;
} }
type summary = type summary =
LocksDomain.astate * PathDomain.astate * ConditionalWritesDomain.astate * PathDomain.astate * bool LocksDomain.astate * PathDomain.astate * ConditionalWritesDomain.astate * PathDomain.astate * bool
@ -72,9 +107,8 @@ let empty =
let conditional_writes = ConditionalWritesDomain.empty in let conditional_writes = ConditionalWritesDomain.empty in
let unconditional_writes = PathDomain.empty in let unconditional_writes = PathDomain.empty in
let id_map = IdAccessPathMapDomain.empty in let id_map = IdAccessPathMapDomain.empty in
let owned = AccessPathSetDomain.empty in let attribute_map = AccessPath.RawMap.empty in
let functional = AccessPathSetDomain.empty in { locks; reads; conditional_writes; unconditional_writes; id_map; attribute_map; }
{ locks; reads; conditional_writes; unconditional_writes; id_map; owned; functional; }
let (<=) ~lhs ~rhs = let (<=) ~lhs ~rhs =
if phys_equal lhs rhs if phys_equal lhs rhs
@ -85,7 +119,7 @@ let (<=) ~lhs ~rhs =
ConditionalWritesDomain.(<=) ~lhs:lhs.conditional_writes ~rhs:rhs.conditional_writes && ConditionalWritesDomain.(<=) ~lhs:lhs.conditional_writes ~rhs:rhs.conditional_writes &&
PathDomain.(<=) ~lhs:lhs.unconditional_writes ~rhs:rhs.unconditional_writes && PathDomain.(<=) ~lhs:lhs.unconditional_writes ~rhs:rhs.unconditional_writes &&
IdAccessPathMapDomain.(<=) ~lhs:lhs.id_map ~rhs:rhs.id_map && 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 = let join astate1 astate2 =
if phys_equal astate1 astate2 if phys_equal astate1 astate2
@ -99,9 +133,8 @@ let join astate1 astate2 =
let unconditional_writes = let unconditional_writes =
PathDomain.join astate1.unconditional_writes astate2.unconditional_writes in PathDomain.join astate1.unconditional_writes astate2.unconditional_writes in
let id_map = IdAccessPathMapDomain.join astate1.id_map astate2.id_map in let id_map = IdAccessPathMapDomain.join astate1.id_map astate2.id_map in
let owned = AccessPathSetDomain.join astate1.owned astate2.owned in let attribute_map = AttributeMapDomain.join astate1.attribute_map astate2.attribute_map in
let functional = AccessPathSetDomain.join astate1.functional astate2.functional in { locks; reads; conditional_writes; unconditional_writes; id_map; attribute_map; }
{ locks; reads; conditional_writes; unconditional_writes; id_map; owned; functional; }
let widen ~prev ~next ~num_iters = let widen ~prev ~next ~num_iters =
if phys_equal prev next if phys_equal prev next
@ -116,10 +149,9 @@ let widen ~prev ~next ~num_iters =
let unconditional_writes = let unconditional_writes =
PathDomain.widen ~prev:prev.unconditional_writes ~next:next.unconditional_writes ~num_iters in 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 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 attribute_map =
let functional = AttributeMapDomain.widen ~prev:prev.attribute_map ~next:next.attribute_map ~num_iters in
AccessPathSetDomain.widen ~prev:prev.functional ~next:next.functional ~num_iters in { locks; reads; conditional_writes; unconditional_writes; id_map; attribute_map; }
{ locks; reads; conditional_writes; unconditional_writes; id_map; owned; functional; }
let pp_summary fmt (locks, reads, conditional_writes, unconditional_writes, retval_owned) = let pp_summary fmt (locks, reads, conditional_writes, unconditional_writes, retval_owned) =
F.fprintf F.fprintf
@ -131,15 +163,14 @@ let pp_summary fmt (locks, reads, conditional_writes, unconditional_writes, retv
PathDomain.pp unconditional_writes PathDomain.pp unconditional_writes
retval_owned 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 F.fprintf
fmt fmt
"Locks: %a Reads: %a Conditional Writes: %a Unconditional Writes: %a Id Map: %a Owned: %a\ "Locks: %a Reads: %a Conditional Writes: %a Unconditional Writes: %a Id Map: %a Attribute Map:\
Functional: %a" %a"
LocksDomain.pp locks LocksDomain.pp locks
PathDomain.pp reads PathDomain.pp reads
ConditionalWritesDomain.pp conditional_writes ConditionalWritesDomain.pp conditional_writes
PathDomain.pp unconditional_writes PathDomain.pp unconditional_writes
IdAccessPathMapDomain.pp id_map IdAccessPathMapDomain.pp id_map
AccessPathSetDomain.pp owned AttributeMapDomain.pp attribute_map
AccessPathSetDomain.pp functional

@ -28,6 +28,27 @@ module IntMap : PrettyPrintable.PPMap with type key = int
module ConditionalWritesDomain : module type of (AbstractDomain.Map (IntMap) (PathDomain)) 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. (** 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 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 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 *) (** access paths written outside of synchronization *)
id_map : IdAccessPathMapDomain.astate; id_map : IdAccessPathMapDomain.astate;
(** map used to decompile temporary variables into access paths *) (** map used to decompile temporary variables into access paths *)
owned : AccessPathSetDomain.astate; attribute_map : AttributeMapDomain.astate;
(** access paths that must be owned by the current function *) (** map of access paths to attributes such as owned, functional, ... *)
functional : AccessPathSetDomain.astate;
(** access paths holding values returned from a call marked with @Functional *)
} }
(** same as astate, but without [id_map]/[owned] (since they are local) and with the addition of a (** same as astate, but without [id_map]/[owned] (since they are local) and with the addition of a

@ -161,3 +161,5 @@ module AccessMap = PrettyPrintable.MakePPMap(struct
end) end)
module RawSet = PrettyPrintable.MakePPSet(Raw) module RawSet = PrettyPrintable.MakePPSet(Raw)
module RawMap = PrettyPrintable.MakePPMap(Raw)

@ -89,3 +89,5 @@ module BaseMap : PrettyPrintable.PPMap with type key = base
module AccessMap : PrettyPrintable.PPMap with type key = access module AccessMap : PrettyPrintable.PPMap with type key = access
module RawSet : PrettyPrintable.PPSet with type elt = Raw.t module RawSet : PrettyPrintable.PPSet with type elt = Raw.t
module RawMap : PrettyPrintable.PPMap with type key = Raw.t

Loading…
Cancel
Save