pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[thread-safety] AccessDomain for better tracking of writes

Browse Source 
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
master
Sam Blackshear 8 years ago committed by Facebook Github Bot
parent ee9a2aa38c
commit 5890007f8e
3 changed files with 188 additions and 177 deletions
Show Stats Download Patch File Download Diff File

224
infer/src/checkers/ThreadSafety.ml
Unescape View File

@ -289,22 +289,16 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
(Mangled.from_string (Mangled.from_string
(container_write_string ^ (Procname.get_method callee_pname))) 0 in (container_write_string ^ (Procname.get_method callee_pname))) 0 in
let dummy_access_exp = Exp.Lfield (receiver_exp, dummy_fieldname, receiver_typ) 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 match AccessPath.of_lhs_exp dummy_access_exp receiver_typ ~f_resolve_id with
| Some container_ap -> | Some container_ap ->
let writes = AccessDomain.add_access
PathDomain.add_sink (ProtectedIf (Some 0))
(make_access container_ap callee_loc) (make_access container_ap callee_loc)
PathDomain.empty in AccessDomain.empty
ConditionalWritesDomain.add 0 writes ConditionalWritesDomain.empty
| None -> | None ->
ConditionalWritesDomain.empty in AccessDomain.empty in
Some Some (false, PathDomain.empty, callee_writes, AttributeSetDomain.empty)
(false,
PathDomain.empty,
callee_conditional_writes,
PathDomain.empty,
AttributeSetDomain.empty)
| _ -> | _ ->
failwithf failwithf
"Call to %a is marked as a container write, but has no receiver" "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 get_summary pdesc callee_pname actuals ~f_resolve_id loc tenv with
| Some (callee_locks, | Some (callee_locks,
callee_reads, callee_reads,
callee_conditional_writes, callee_writes,
callee_unconditional_writes,
return_attributes) -> return_attributes) ->
let locks' = callee_locks || astate.locks in let locks' = callee_locks || astate.locks in
let astate' = let astate' =
if is_unprotected locks' if is_unprotected locks'
then then
let call_site = CallSite.make callee_pname loc in let call_site = CallSite.make callee_pname loc in
(* add the conditional writes rooted in the callee formal at [index] to let add_conditional_writes index writes_acc (actual_exp, actual_typ) =
the current state *)
let add_conditional_writes
index ((cond_writes, uncond_writes) as acc) (actual_exp, actual_typ) =
if is_constant actual_exp if is_constant actual_exp
then then
acc (* the actual is a constant, so it's owned in the caller. *)
writes_acc
else else
try let callee_conditional_writes =
let callee_cond_writes_for_index' = PathDomain.with_callsite
let callee_cond_writes_for_index = (AccessDomain.get_accesses (ProtectedIf (Some index)) callee_writes)
ConditionalWritesDomain.find index callee_conditional_writes in call_site in
PathDomain.with_callsite callee_cond_writes_for_index call_site in 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.attribute_map
if is_owned actual_access_path astate.attribute_map then
then (* the actual passed to the current callee is owned. drop all the
(* the actual passed to the current callee is owned. drop all conditional writes for that actual, since they're all safe *)
the conditional writes for that actual, since they're all writes_acc
safe *) else
acc let base = fst actual_access_path in
else begin
let base = fst actual_access_path in match FormalMap.get_formal_index base extras with
begin | Some formal_index ->
match FormalMap.get_formal_index base extras with (* the actual passed to the current callee is rooted in a
| Some formal_index -> formal. add to conditional writes *)
(* the actual passed to the current callee is rooted in PathDomain.Sinks.fold
a formal. add to conditional writes *) (AccessDomain.add_access
let conditional_writes' = (ProtectedIf (Some formal_index)))
try (PathDomain.sinks callee_conditional_writes)
ConditionalWritesDomain.find writes_acc
formal_index cond_writes | None ->
|> PathDomain.join callee_cond_writes_for_index' (* access path not owned and not rooted in a formal. add to
with Not_found -> unsafe writes *)
callee_cond_writes_for_index' in PathDomain.Sinks.fold
let cond_writes' = (AccessDomain.add_access AccessPrecondition.unprotected)
ConditionalWritesDomain.add (PathDomain.sinks callee_conditional_writes)
formal_index conditional_writes' cond_writes in writes_acc
cond_writes', uncond_writes end
| None -> | None ->
(* access path not owned and not rooted in a formal. add PathDomain.Sinks.fold
to unconditional writes *) (AccessDomain.add_access AccessPrecondition.unprotected)
cond_writes, (PathDomain.sinks callee_conditional_writes)
PathDomain.join writes_acc
uncond_writes callee_cond_writes_for_index' end in
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 reads = let reads =
PathDomain.with_callsite callee_reads call_site PathDomain.with_callsite callee_reads call_site
|> PathDomain.join astate.reads in |> 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 else
astate in astate in
let attribute_map = let attribute_map =
@ -532,7 +526,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
AttributeMapDomain.has_attribute access_path Functional attribute_map AttributeMapDomain.has_attribute access_path Functional attribute_map
| None -> | None ->
false in false in
let conditional_writes, unconditional_writes = let 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 *) &&
@ -540,34 +534,35 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
begin begin
match get_formal_index base_exp typ with match get_formal_index base_exp typ with
| Some formal_index -> | Some formal_index ->
let conditional_writes_for_index = let pre = AccessPrecondition.ProtectedIf (Some formal_index) in
try ConditionalWritesDomain.find formal_index astate.conditional_writes let conditional_writes_for_pre =
with Not_found -> PathDomain.empty in AccessDomain.get_accesses pre astate.writes in
let conditional_writes_for_index' = let conditional_writes_for_pre' =
add_path_to_state add_path_to_state
lhs_exp lhs_exp
typ typ
loc loc
conditional_writes_for_index conditional_writes_for_pre
astate.id_map astate.id_map
astate.attribute_map astate.attribute_map
tenv in tenv in
ConditionalWritesDomain.add AccessDomain.add pre conditional_writes_for_pre' astate.writes
formal_index conditional_writes_for_index' astate.conditional_writes,
astate.unconditional_writes
| None -> | None ->
astate.conditional_writes, let unsafe_writes =
add_path_to_state AccessDomain.get_accesses AccessPrecondition.unprotected astate.writes in
lhs_exp let unsafe_writes' =
typ add_path_to_state
loc lhs_exp
astate.unconditional_writes typ
astate.id_map loc
astate.attribute_map unsafe_writes
tenv astate.id_map
astate.attribute_map
tenv in
AccessDomain.add AccessPrecondition.unprotected unsafe_writes' astate.writes
end end
| _ -> | _ ->
astate.conditional_writes, astate.unconditional_writes in astate.writes in
let attribute_map = let attribute_map =
match AccessPath.of_lhs_exp lhs_exp lhs_typ ~f_resolve_id with match AccessPath.of_lhs_exp lhs_exp lhs_typ ~f_resolve_id with
| Some lhs_access_path -> | 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 lhs_access_path rhs_exp lhs_typ ~f_resolve_id astate.attribute_map extras
| None -> | None ->
astate.attribute_map in 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) -> | 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
@ -729,7 +724,7 @@ let make_results_table get_proc_desc file_env =
let has_lock = false in let has_lock = false in
let return_attrs = AttributeSetDomain.empty in let return_attrs = AttributeSetDomain.empty in
let empty = 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 *) (* convert the abstract state to a summary by dropping the id map *)
let compute_post ({ ProcData.pdesc; tenv; extras; } as proc_data) = let compute_post ({ ProcData.pdesc; tenv; extras; } as proc_data) =
if should_analyze_proc pdesc tenv if should_analyze_proc pdesc tenv
@ -752,7 +747,7 @@ let make_results_table get_proc_desc file_env =
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; attribute_map; } -> | Some { locks; reads; 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))
@ -760,7 +755,7 @@ let make_results_table get_proc_desc file_env =
let return_attributes = let return_attributes =
try AttributeMapDomain.find return_var_ap attribute_map try AttributeMapDomain.find return_var_ap attribute_map
with Not_found -> AttributeSetDomain.empty in with Not_found -> AttributeSetDomain.empty in
Some (locks, reads, conditional_writes, unconditional_writes, return_attributes) Some (locks, reads, writes, return_attributes)
| None -> | None ->
None None
end end
@ -802,16 +797,16 @@ let calculate_addendum_message tenv pname =
else "" else ""
| _ -> "" | _ -> ""
let get_possibly_unsafe_writes writes =
let combine_conditional_unconditional_writes conditional_writes unconditional_writes =
let open ThreadSafetyDomain in let open ThreadSafetyDomain in
ConditionalWritesDomain.fold AccessDomain.fold
(fun _ writes acc -> PathDomain.join writes acc) (fun attribute accesses acc -> match attribute with
conditional_writes | ProtectedIf _ -> PathDomain.join accesses acc
unconditional_writes | Protected -> acc)
writes
let equal_locs (sink1 : ThreadSafetyDomain.TraceElem.t) PathDomain.empty
(sink2 : ThreadSafetyDomain.TraceElem.t) =
let equal_locs (sink1 : ThreadSafetyDomain.TraceElem.t) (sink2 : ThreadSafetyDomain.TraceElem.t) =
Location.equal Location.equal
(CallSite.loc (ThreadSafetyDomain.TraceElem.call_site sink1)) (CallSite.loc (ThreadSafetyDomain.TraceElem.call_site sink1))
(CallSite.loc (ThreadSafetyDomain.TraceElem.call_site sink2)) (CallSite.loc (ThreadSafetyDomain.TraceElem.call_site sink2))
@ -844,10 +839,9 @@ let filter_conflicting_sinks sink trace =
let collect_conflicting_writes sink tab = let collect_conflicting_writes sink tab =
let procs_and_writes = let procs_and_writes =
List.map List.map
~f:(fun (key,(_, _, conditional_writes, unconditional_writes, _)) -> ~f:(fun (key,(_, _, writes, _)) ->
let conflicting_writes = let conflicting_writes =
combine_conditional_unconditional_writes get_possibly_unsafe_writes writes
conditional_writes unconditional_writes
|> filter_conflicting_sinks sink in |> filter_conflicting_sinks sink in
key, conflicting_writes key, conflicting_writes
) )
@ -907,8 +901,8 @@ let report_thread_safety_violations ( _, tenv, pname, pdesc) make_description tr
let open ThreadSafetyDomain in let open ThreadSafetyDomain in
let trace_of_pname callee_pname = let trace_of_pname callee_pname =
match Summary.read_summary pdesc callee_pname with match Summary.read_summary pdesc callee_pname with
| Some (_, _, conditional_writes, unconditional_writes, _) -> | Some (_, _, writes, _) ->
combine_conditional_unconditional_writes conditional_writes unconditional_writes get_possibly_unsafe_writes writes
| _ -> | _ ->
PathDomain.empty in PathDomain.empty in
let report_one_path ((_, sinks) as path) = 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_all_procs || is_thread_safe_method pdesc tenv)
&& should_report_on_proc proc_env in && should_report_on_proc proc_env in
ResultsTableType.iter (* report errors for each method *) 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 if should_report proc_env then
let writes = combine_conditional_unconditional_writes
conditional_writes unconditional_writes in
begin begin
report_thread_safety_violations report_thread_safety_violations
proc_env make_unprotected_write_description writes tab proc_env make_unprotected_write_description (get_possibly_unsafe_writes writes) tab;
; report_reads proc_env reads tab report_reads proc_env reads tab
end end
) )
tab tab

85
infer/src/checkers/ThreadSafetyDomain.ml
Unescape View File

@ -47,10 +47,6 @@ module LocksDomain = AbstractDomain.BooleanAnd
module PathDomain = SinkTrace.Make(TraceElem) module PathDomain = SinkTrace.Make(TraceElem)
module IntMap = PrettyPrintable.MakePPMap(Int)
module ConditionalWritesDomain = AbstractDomain.Map (IntMap) (PathDomain)
module Attribute = struct module Attribute = struct
type t = type t =
| OwnedIf of int option | OwnedIf of int option
@ -91,31 +87,60 @@ module AttributeMapDomain = struct
add access_path attribute_set t add access_path attribute_set t
end 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 = type astate =
{ {
locks : LocksDomain.astate; locks : LocksDomain.astate;
reads : PathDomain.astate; reads : PathDomain.astate;
conditional_writes : ConditionalWritesDomain.astate; writes : AccessDomain.astate;
unconditional_writes : PathDomain.astate;
id_map : IdAccessPathMapDomain.astate; id_map : IdAccessPathMapDomain.astate;
attribute_map : AttributeMapDomain.astate; attribute_map : AttributeMapDomain.astate;
} }
type summary = type summary =
LocksDomain.astate * LocksDomain.astate * PathDomain.astate * AccessDomain.astate * AttributeSetDomain.astate
PathDomain.astate *
ConditionalWritesDomain.astate *
PathDomain.astate *
AttributeSetDomain.astate
let empty = let empty =
let locks = false in let locks = false in
let reads = PathDomain.empty in let reads = PathDomain.empty in
let conditional_writes = ConditionalWritesDomain.empty in let writes = AccessDomain.empty in
let unconditional_writes = PathDomain.empty in
let id_map = IdAccessPathMapDomain.empty in let id_map = IdAccessPathMapDomain.empty in
let attribute_map = AccessPath.UntypedRawMap.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 = let (<=) ~lhs ~rhs =
if phys_equal lhs rhs if phys_equal lhs rhs
@ -123,8 +148,7 @@ let (<=) ~lhs ~rhs =
else else
LocksDomain.(<=) ~lhs:lhs.locks ~rhs:rhs.locks && LocksDomain.(<=) ~lhs:lhs.locks ~rhs:rhs.locks &&
PathDomain.(<=) ~lhs:lhs.reads ~rhs:rhs.reads && PathDomain.(<=) ~lhs:lhs.reads ~rhs:rhs.reads &&
ConditionalWritesDomain.(<=) ~lhs:lhs.conditional_writes ~rhs:rhs.conditional_writes && AccessDomain.(<=) ~lhs:lhs.writes ~rhs:rhs.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 &&
AttributeMapDomain.(<=) ~lhs:lhs.attribute_map ~rhs:rhs.attribute_map AttributeMapDomain.(<=) ~lhs:lhs.attribute_map ~rhs:rhs.attribute_map
@ -135,13 +159,10 @@ let join astate1 astate2 =
else else
let locks = LocksDomain.join astate1.locks astate2.locks in let locks = LocksDomain.join astate1.locks astate2.locks in
let reads = PathDomain.join astate1.reads astate2.reads in let reads = PathDomain.join astate1.reads astate2.reads in
let conditional_writes = let writes = AccessDomain.join astate1.writes astate2.writes in
ConditionalWritesDomain.join astate1.conditional_writes astate2.conditional_writes in
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 id_map = IdAccessPathMapDomain.join astate1.id_map astate2.id_map in
let attribute_map = AttributeMapDomain.join astate1.attribute_map astate2.attribute_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 = let widen ~prev ~next ~num_iters =
if phys_equal prev next if phys_equal prev next
@ -150,34 +171,28 @@ let widen ~prev ~next ~num_iters =
else else
let locks = LocksDomain.widen ~prev:prev.locks ~next:next.locks ~num_iters in 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 reads = PathDomain.widen ~prev:prev.reads ~next:next.reads ~num_iters in
let conditional_writes = let writes = AccessDomain.widen ~prev:prev.writes ~next:next.writes ~num_iters in
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 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 attribute_map = let attribute_map =
AttributeMapDomain.widen ~prev:prev.attribute_map ~next:next.attribute_map ~num_iters in 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 F.fprintf
fmt 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 LocksDomain.pp locks
PathDomain.pp reads PathDomain.pp reads
ConditionalWritesDomain.pp conditional_writes AccessDomain.pp writes
PathDomain.pp unconditional_writes
AttributeSetDomain.pp return_attributes 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 F.fprintf
fmt 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" %a"
LocksDomain.pp locks LocksDomain.pp locks
PathDomain.pp reads PathDomain.pp reads
ConditionalWritesDomain.pp conditional_writes AccessDomain.pp writes
PathDomain.pp unconditional_writes
IdAccessPathMapDomain.pp id_map IdAccessPathMapDomain.pp id_map
AttributeMapDomain.pp attribute_map AttributeMapDomain.pp attribute_map

56
infer/src/checkers/ThreadSafetyDomain.mli
Unescape View File

@ -24,10 +24,6 @@ module LocksDomain : AbstractDomain.S with type astate = bool
module PathDomain : module type of SinkTrace.Make(TraceElem) 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 module Attribute : sig
type t = type t =
| OwnedIf of int option | OwnedIf of int option
@ -54,31 +50,43 @@ module AttributeMapDomain : sig
val add_attribute : AccessPath.Raw.t -> Attribute.t -> astate -> astate val add_attribute : AccessPath.Raw.t -> Attribute.t -> astate -> astate
end end
(** the primary role of this domain is tracking *conditional* and *unconditional* writes. module AccessPrecondition : sig
conditional writes are writes that are rooted in a formal of the current procedure, and they type t =
are safe only if the actual bound to that formal is owned at the call site (as in the foo | Protected
example below). Unconditional writes are rooted in a local, and they are only safe if a lock is (** access safe due to held lock (i.e., pre is true *)
held in the caller. | ProtectedIf of int option
To demonstrate what conditional writes buy us, consider the following example: (** 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() { (* get all accesses with the given precondition *)
Object local = new Object(); val get_accesses : AccessPrecondition.t -> astate -> PathDomain.astate
iWriteToAField(local); 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 = type astate =
{ {
locks : LocksDomain.astate; locks : LocksDomain.astate;
(** boolean that is true if a lock must currently be held *) (** boolean that is true if a lock must currently be held *)
reads : PathDomain.astate; reads : PathDomain.astate;
(** access paths read outside of synchronization *) (** access paths read outside of synchronization *)
conditional_writes : ConditionalWritesDomain.astate; writes : AccessDomain.astate;
(** map of (formal index) -> set of access paths rooted in the formal index that are read (** access paths written without ownership permissions *)
outside of synrchonization if the formal is not owned by the caller *)
unconditional_writes : PathDomain.astate;
(** 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 *)
attribute_map : AttributeMapDomain.astate; 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 (** same as astate, but without [id_map]/[owned] (since they are local) and with the addition of the
attributes associated with the return value *) attributes associated with the return value *)
type summary = type summary =
LocksDomain.astate * LocksDomain.astate * PathDomain.astate * AccessDomain.astate * AttributeSetDomain.astate
PathDomain.astate *
ConditionalWritesDomain.astate *
PathDomain.astate *
AttributeSetDomain.astate
include AbstractDomain.WithBottom with type astate := astate include AbstractDomain.WithBottom with type astate := astate

Write Preview
Loading…
Cancel
Save