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

[thread-safety][cleanup] open ThreadSafetyDomain locally to avoid excess typing

Browse Source 
Reviewed By: jeremydubreil

Differential Revision: D4452386

fbshipit-source-id: f4ba5df
master
Sam Blackshear 8 years ago committed by Facebook Github Bot
parent e132188361
commit d25a3edbd7
1 changed files with 35 additions and 50 deletions
Show Stats Download Patch File Download Diff File

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

@ -65,7 +65,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
with Not_found -> None with Not_found -> None
let is_owned access_path owned_set = let is_owned access_path owned_set =
ThreadSafetyDomain.OwnershipDomain.mem access_path owned_set Domain.OwnershipDomain.mem access_path owned_set
let is_initializer tenv proc_name = let is_initializer tenv proc_name =
Procname.is_constructor proc_name || Procname.is_constructor proc_name ||
@ -107,14 +107,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
IList.fold_left IList.fold_left
(fun acc rawpath -> (fun acc rawpath ->
if not (is_owned (truncate rawpath) owned) && not (is_safe_write rawpath pname tenv) if not (is_owned (truncate rawpath) owned) && not (is_safe_write rawpath pname tenv)
then then Domain.PathDomain.add_sink (Domain.make_access rawpath loc) acc
ThreadSafetyDomain.PathDomain.add_sink (ThreadSafetyDomain.make_access rawpath loc) acc else acc)
else
acc)
path_state path_state
(AccessPath.of_exp exp typ ~f_resolve_id) (AccessPath.of_exp exp typ ~f_resolve_id)
let analyze_id_assignment lhs_id rhs_exp rhs_typ { ThreadSafetyDomain.id_map; } = let analyze_id_assignment lhs_id rhs_exp rhs_typ { Domain.id_map; } =
let f_resolve_id = resolve_id id_map in let f_resolve_id = resolve_id id_map in
match AccessPath.of_lhs_exp rhs_exp rhs_typ ~f_resolve_id with match AccessPath.of_lhs_exp rhs_exp rhs_typ ~f_resolve_id with
| Some rhs_access_path -> IdAccessPathMapDomain.add lhs_id rhs_access_path id_map | Some rhs_access_path -> IdAccessPathMapDomain.add lhs_id rhs_access_path id_map
@ -138,7 +136,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
PatternMatch.supertype_exists tenv is_container_write_ typename && PatternMatch.supertype_exists tenv is_container_write_ typename &&
not (PatternMatch.supertype_exists tenv is_threadsafe_collection typename) not (PatternMatch.supertype_exists tenv is_threadsafe_collection typename)
| _ -> false in | _ -> false in
let add_container_write pn loc exp typ (astate : ThreadSafetyDomain.astate) = let add_container_write pn loc exp typ (astate : Domain.astate) =
let dummy_fieldname = let dummy_fieldname =
Ident.create_fieldname (Mangled.from_string (Procname.get_method pn)) 0 in Ident.create_fieldname (Mangled.from_string (Procname.get_method pn)) 0 in
let dummy_access_exp = Exp.Lfield (exp, dummy_fieldname, typ) in let dummy_access_exp = Exp.Lfield (exp, dummy_fieldname, typ) in
@ -157,12 +155,13 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
not is_locked && not (Procdesc.is_java_synchronized pdesc) in not is_locked && not (Procdesc.is_java_synchronized pdesc) in
let f_resolve_id = resolve_id astate.id_map in let f_resolve_id = resolve_id astate.id_map in
let open Domain in
function function
| Sil.Call (Some (lhs_id, lhs_typ), Const (Cfun pn), _, _, _) when is_allocation pn -> | Sil.Call (Some (lhs_id, lhs_typ), Const (Cfun pn), _, _, _) when is_allocation pn ->
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 = ThreadSafetyDomain.OwnershipDomain.add lhs_access_path astate.owned in let owned = OwnershipDomain.add lhs_access_path astate.owned in
{ astate with owned; } { astate with owned; }
| None -> | None ->
astate astate
@ -206,11 +205,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
try try
let callee_cond_writes_for_index' = let callee_cond_writes_for_index' =
let callee_cond_writes_for_index = let callee_cond_writes_for_index =
ThreadSafetyDomain.ConditionalWritesDomain.find ConditionalWritesDomain.find index callee_conditional_writes in
index callee_conditional_writes in PathDomain.with_callsite callee_cond_writes_for_index call_site in
ThreadSafetyDomain.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 ->
@ -229,44 +225,39 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
a formal. add to conditional writes *) a formal. add to conditional writes *)
let conditional_writes' = let conditional_writes' =
try try
ThreadSafetyDomain.ConditionalWritesDomain.find ConditionalWritesDomain.find
formal_index formal_index cond_writes
cond_writes |> PathDomain.join callee_cond_writes_for_index'
|> ThreadSafetyDomain.PathDomain.join
callee_cond_writes_for_index'
with Not_found -> with Not_found ->
callee_cond_writes_for_index' in callee_cond_writes_for_index' in
let cond_writes' = let cond_writes' =
ThreadSafetyDomain.ConditionalWritesDomain.add ConditionalWritesDomain.add
formal_index conditional_writes' cond_writes in formal_index conditional_writes' cond_writes in
cond_writes', uncond_writes cond_writes', uncond_writes
| None -> | None ->
(* access path not owned and not rooted in a formal. add (* access path not owned and not rooted in a formal. add
to unconditional writes *) to unconditional writes *)
cond_writes, cond_writes,
ThreadSafetyDomain.PathDomain.join PathDomain.join
uncond_writes callee_cond_writes_for_index' uncond_writes callee_cond_writes_for_index'
end end
| _ -> | _ ->
cond_writes, cond_writes,
ThreadSafetyDomain.PathDomain.join PathDomain.join uncond_writes callee_cond_writes_for_index'
uncond_writes callee_cond_writes_for_index'
end end
with Not_found -> with Not_found ->
acc in acc in
let conditional_writes, unconditional_writes = let conditional_writes, unconditional_writes =
let combined_unconditional_writes = let combined_unconditional_writes =
ThreadSafetyDomain.PathDomain.with_callsite PathDomain.with_callsite callee_unconditional_writes call_site
callee_unconditional_writes |> PathDomain.join astate.unconditional_writes in
call_site
|> ThreadSafetyDomain.PathDomain.join astate.unconditional_writes in
IList.fold_lefti IList.fold_lefti
add_conditional_writes add_conditional_writes
(astate.conditional_writes, combined_unconditional_writes) (astate.conditional_writes, combined_unconditional_writes)
actuals in actuals in
let reads = let reads =
ThreadSafetyDomain.PathDomain.with_callsite callee_reads call_site PathDomain.with_callsite callee_reads call_site
|> ThreadSafetyDomain.PathDomain.join astate.reads in |> PathDomain.join astate.reads in
{ astate with reads; conditional_writes; unconditional_writes; } { astate with reads; conditional_writes; unconditional_writes; }
else else
astate in astate in
@ -292,11 +283,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
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 conditional_writes_for_index =
try try ConditionalWritesDomain.find formal_index astate.conditional_writes
ThreadSafetyDomain.ConditionalWritesDomain.find with Not_found -> PathDomain.empty in
formal_index astate.conditional_writes
with Not_found ->
ThreadSafetyDomain.PathDomain.empty in
let conditional_writes_for_index' = let conditional_writes_for_index' =
add_path_to_state add_path_to_state
lhs_exp lhs_exp
@ -307,7 +295,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
astate.owned astate.owned
pname pname
tenv in tenv in
ThreadSafetyDomain.ConditionalWritesDomain.add ConditionalWritesDomain.add
formal_index conditional_writes_for_index' astate.conditional_writes, formal_index conditional_writes_for_index' astate.conditional_writes,
astate.unconditional_writes astate.unconditional_writes
| None -> | None ->
@ -330,11 +318,11 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
match AccessPath.of_lhs_exp lhs_exp lhs_typ ~f_resolve_id, match AccessPath.of_lhs_exp lhs_exp lhs_typ ~f_resolve_id,
AccessPath.of_lhs_exp rhs_exp lhs_typ ~f_resolve_id with AccessPath.of_lhs_exp rhs_exp lhs_typ ~f_resolve_id with
| Some lhs_access_path, Some rhs_access_path -> | Some lhs_access_path, Some rhs_access_path ->
if ThreadSafetyDomain.OwnershipDomain.mem rhs_access_path astate.owned if OwnershipDomain.mem rhs_access_path astate.owned
then ThreadSafetyDomain.OwnershipDomain.add lhs_access_path astate.owned then OwnershipDomain.add lhs_access_path astate.owned
else ThreadSafetyDomain.OwnershipDomain.remove lhs_access_path astate.owned else OwnershipDomain.remove lhs_access_path astate.owned
| Some lhs_access_path, None -> | Some lhs_access_path, None ->
ThreadSafetyDomain.OwnershipDomain.remove lhs_access_path astate.owned OwnershipDomain.remove lhs_access_path astate.owned
| _ -> | _ ->
astate.owned in astate.owned in
{ astate with conditional_writes; unconditional_writes; owned; } { astate with conditional_writes; unconditional_writes; owned; }
@ -351,8 +339,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let owned = let owned =
match AccessPath.of_lhs_exp rhs_exp rhs_typ ~f_resolve_id with match AccessPath.of_lhs_exp rhs_exp rhs_typ ~f_resolve_id with
| Some rhs_access_path | Some rhs_access_path
when ThreadSafetyDomain.OwnershipDomain.mem rhs_access_path astate.owned -> when OwnershipDomain.mem rhs_access_path astate.owned ->
ThreadSafetyDomain.OwnershipDomain.add (AccessPath.of_id lhs_id rhs_typ) astate.owned OwnershipDomain.add (AccessPath.of_id lhs_id rhs_typ) astate.owned
| _ -> | _ ->
astate.owned in astate.owned in
{ astate with Domain.reads; id_map; owned; } { astate with Domain.reads; id_map; owned; }
@ -467,11 +455,8 @@ let make_results_table get_proc_desc file_env =
in in
let compute_post_for_procedure = (* takes proc_env as arg *) let compute_post_for_procedure = (* takes proc_env as arg *)
fun (idenv, tenv, proc_name, proc_desc) -> fun (idenv, tenv, proc_name, proc_desc) ->
let empty = let open ThreadSafetyDomain in
false, let empty = false, PathDomain.empty, ConditionalWritesDomain.empty, PathDomain.empty in
ThreadSafetyDomain.PathDomain.empty,
ThreadSafetyDomain.ConditionalWritesDomain.empty,
ThreadSafetyDomain.PathDomain.empty 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; } as proc_data) = let compute_post ({ ProcData.pdesc; tenv; } as proc_data) =
if should_analyze_proc pdesc tenv if should_analyze_proc pdesc tenv
@ -487,8 +472,8 @@ let make_results_table get_proc_desc file_env =
else else
Some empty in Some empty in
let callback_arg = let callback_arg =
{Callbacks.get_proc_desc; get_procs_in_file = (fun _ -> []); let get_procs_in_file _ = [] in
idenv; tenv; proc_name; proc_desc} in { Callbacks.get_proc_desc; get_procs_in_file; idenv; tenv; proc_name; proc_desc } in
match match
Interprocedural.compute_and_store_post Interprocedural.compute_and_store_post
~compute_post ~compute_post
@ -522,12 +507,12 @@ let calculate_addendum_message tenv pname =
| _ -> "" | _ -> ""
let combine_conditional_unconditional_writes conditional_writes unconditional_writes = let combine_conditional_unconditional_writes conditional_writes unconditional_writes =
ThreadSafetyDomain.ConditionalWritesDomain.fold let open ThreadSafetyDomain in
(fun _ writes acc -> ThreadSafetyDomain.PathDomain.join writes acc) ConditionalWritesDomain.fold
(fun _ writes acc -> PathDomain.join writes acc)
conditional_writes conditional_writes
unconditional_writes unconditional_writes
let report_thread_safety_violations ( _, tenv, pname, pdesc) trace = let report_thread_safety_violations ( _, tenv, pname, pdesc) trace =
let open ThreadSafetyDomain in let open ThreadSafetyDomain in
let trace_of_pname callee_pname = let trace_of_pname callee_pname =

Write Preview
Loading…
Cancel
Save