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

[racerd] precondition -> snapshot

Browse Source 
Reviewed By: ngorogiannis

Differential Revision: D7754774

fbshipit-source-id: 5d04c60
master
Sam Blackshear 7 years ago committed by Facebook Github Bot
parent 771e1b7c14
commit ebc364a801
1 changed files with 45 additions and 45 deletions
Show Stats Download Patch File Download Diff File

90
infer/src/concurrency/RacerD.ml
Unescape View File

@ -304,17 +304,18 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| None -> | None ->
path path
in in
let expand_pre (snapshot: AccessSnapshot.t) = let expand_precondition (snapshot: AccessSnapshot.t) =
let access = TraceElem.map ~f:expand_path snapshot.access in let access = TraceElem.map ~f:expand_path snapshot.access in
AccessSnapshot.make_ access snapshot.lock snapshot.thread snapshot.ownership_precondition AccessSnapshot.make_ access snapshot.lock snapshot.thread snapshot.ownership_precondition
in in
AccessDomain.map expand_pre accesses AccessDomain.map expand_precondition accesses
let add_callee_accesses (caller_astate: Domain.astate) callee_accesses locks threads actuals let add_callee_accesses (caller_astate: Domain.astate) callee_accesses locks threads actuals
callee_pname pdesc loc = callee_pname pdesc loc =
let open Domain in let open Domain in
let conjoin_ownership_pre actual_exp actual_indexes : AccessSnapshot.OwnershipPrecondition.t = let conjoin_ownership_precondition actual_exp actual_indexes
: AccessSnapshot.OwnershipPrecondition.t =
match actual_exp with match actual_exp with
| HilExp.Constant _ -> | HilExp.Constant _ ->
(* the actual is a constant, so it's owned in the caller. *) (* the actual is a constant, so it's owned in the caller. *)
@ -346,7 +347,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
(* couldn't find access path, don't know if it's owned. assume not *) (* couldn't find access path, don't know if it's owned. assume not *)
False False
in in
let update_ownership_pre actual_index (acc: AccessSnapshot.OwnershipPrecondition.t) = let update_ownership_precondition actual_index (acc: AccessSnapshot.OwnershipPrecondition.t) =
match acc with match acc with
| False -> | False ->
(* precondition can't be satisfied *) (* precondition can't be satisfied *)
@ -354,7 +355,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| Conjunction actual_indexes -> | Conjunction actual_indexes ->
match List.nth actuals actual_index with match List.nth actuals actual_index with
| Some actual -> | Some actual ->
conjoin_ownership_pre actual actual_indexes conjoin_ownership_precondition actual actual_indexes
| None -> | None ->
L.internal_error "Bad actual index %d for callee %a with %d actuals." actual_index L.internal_error "Bad actual index %d for callee %a with %d actuals." actual_index
Typ.Procname.pp callee_pname (List.length actuals) ; Typ.Procname.pp callee_pname (List.length actuals) ;
@ -370,8 +371,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let ownership_precondition = let ownership_precondition =
match snapshot.ownership_precondition with match snapshot.ownership_precondition with
| Conjunction indexes -> | Conjunction indexes ->
let empty_pre = AccessSnapshot.OwnershipPrecondition.Conjunction IntSet.empty in let empty_precondition =
IntSet.fold update_ownership_pre indexes empty_pre AccessSnapshot.OwnershipPrecondition.Conjunction IntSet.empty
in
IntSet.fold update_ownership_precondition indexes empty_precondition
| False -> | False ->
snapshot.ownership_precondition snapshot.ownership_precondition
in in
@ -1110,7 +1113,7 @@ let make_unprotected_write_description pname final_sink_site initial_sink_site f
type reported_access = type reported_access =
{ threads: RacerDDomain.ThreadsDomain.astate { threads: RacerDDomain.ThreadsDomain.astate
; precondition: RacerDDomain.AccessSnapshot.t ; snapshot: RacerDDomain.AccessSnapshot.t
; tenv: Tenv.t ; tenv: Tenv.t
; procdesc: Procdesc.t ; procdesc: Procdesc.t
; wobbly_paths: RacerDDomain.StabilityDomain.astate } ; wobbly_paths: RacerDDomain.StabilityDomain.astate }
@ -1208,21 +1211,20 @@ let report_unsafe_accesses (aggregated_access_map: reported_access list AccessLi
reported reported
else reported else reported
in in
let report_unsafe_access {precondition; threads; tenv; procdesc; wobbly_paths} accesses let report_unsafe_access {snapshot; threads; tenv; procdesc; wobbly_paths} accesses reported_acc =
reported_acc =
let pname = Procdesc.get_proc_name procdesc in let pname = Procdesc.get_proc_name procdesc in
if is_duplicate_report precondition.access pname reported_acc then reported_acc if is_duplicate_report snapshot.access pname reported_acc then reported_acc
else else
match TraceElem.kind precondition.access with match TraceElem.kind snapshot.access with
| Access.InterfaceCall unannoted_call_pname -> | Access.InterfaceCall unannoted_call_pname ->
if if
AccessSnapshot.is_unprotected precondition && ThreadsDomain.is_any threads AccessSnapshot.is_unprotected snapshot && ThreadsDomain.is_any threads
&& Models.is_marked_thread_safe procdesc tenv && Models.is_marked_thread_safe procdesc tenv
then ( then (
(* un-annotated interface call + no lock in method marked thread-safe. warn *) (* un-annotated interface call + no lock in method marked thread-safe. warn *)
report_unannotated_interface_violation tenv procdesc precondition.access threads report_unannotated_interface_violation tenv procdesc snapshot.access threads
unannoted_call_pname ; unannoted_call_pname ;
update_reported precondition.access pname reported_acc ) update_reported snapshot.access pname reported_acc )
else reported_acc else reported_acc
| Access.Write _ | ContainerWrite _ -> ( | Access.Write _ | ContainerWrite _ -> (
match Procdesc.get_proc_name procdesc with match Procdesc.get_proc_name procdesc with
@ -1236,70 +1238,68 @@ let report_unsafe_accesses (aggregated_access_map: reported_access list AccessLi
(i.e., not a self race). find accesses on a background thread this access might (i.e., not a self race). find accesses on a background thread this access might
conflict with and report them *) conflict with and report them *)
List.filter_map List.filter_map
~f:(fun {precondition= other_precondition; threads= other_threads} -> ~f:(fun {snapshot= other_snapshot; threads= other_threads} ->
if if
TraceElem.is_write other_precondition.access TraceElem.is_write other_snapshot.access
&& ThreadsDomain.is_any other_threads && ThreadsDomain.is_any other_threads
then Some other_precondition.access then Some other_snapshot.access
else None ) else None )
accesses accesses
in in
if if
AccessSnapshot.is_unprotected precondition AccessSnapshot.is_unprotected snapshot
&& (not (List.is_empty writes_on_background_thread) || ThreadsDomain.is_any threads) && (not (List.is_empty writes_on_background_thread) || ThreadsDomain.is_any threads)
then ( then (
let conflict = List.hd writes_on_background_thread in let conflict = List.hd writes_on_background_thread in
report_thread_safety_violation tenv procdesc report_thread_safety_violation tenv procdesc
~make_description:make_unprotected_write_description ~make_description:make_unprotected_write_description
~report_kind:(WriteWriteRace conflict) precondition.access threads wobbly_paths ; ~report_kind:(WriteWriteRace conflict) snapshot.access threads wobbly_paths ;
update_reported precondition.access pname reported_acc ) update_reported snapshot.access pname reported_acc )
else reported_acc else reported_acc
| _ -> | _ ->
(* Do not report unprotected writes when an access can't run in parallel with itself, or (* Do not report unprotected writes when an access can't run in parallel with itself, or
for ObjC_Cpp *) for ObjC_Cpp *)
reported_acc ) reported_acc )
| (Access.Read _ | ContainerRead _) when AccessSnapshot.is_unprotected precondition -> | (Access.Read _ | ContainerRead _) when AccessSnapshot.is_unprotected snapshot ->
(* unprotected read. report all writes as conflicts for java. for c++ filter out (* unprotected read. report all writes as conflicts for java. for c++ filter out
unprotected writes *) unprotected writes *)
let is_cpp_protected_write pre = let is_cpp_protected_write snapshot =
Typ.Procname.is_java pname || not (AccessSnapshot.is_unprotected pre) Typ.Procname.is_java pname || not (AccessSnapshot.is_unprotected snapshot)
in in
let is_conflict (pre: AccessSnapshot.t) other_thread = let is_conflict (snapshot: AccessSnapshot.t) other_thread =
TraceElem.is_write pre.access TraceElem.is_write snapshot.access
&& &&
if Typ.Procname.is_java pname then if Typ.Procname.is_java pname then
ThreadsDomain.is_any threads || ThreadsDomain.is_any other_thread ThreadsDomain.is_any threads || ThreadsDomain.is_any other_thread
else is_cpp_protected_write pre else is_cpp_protected_write snapshot
in in
let all_writes = let all_writes =
List.filter List.filter
~f:(fun {precondition; threads= other_threads} -> ~f:(fun {snapshot; threads= other_threads} -> is_conflict snapshot other_threads)
is_conflict precondition other_threads )
accesses accesses
in in
if not (List.is_empty all_writes) then ( if not (List.is_empty all_writes) then (
let conflict = List.hd_exn all_writes in let conflict = List.hd_exn all_writes in
report_thread_safety_violation tenv procdesc report_thread_safety_violation tenv procdesc
~make_description:(make_read_write_race_description ~read_is_sync:false conflict) ~make_description:(make_read_write_race_description ~read_is_sync:false conflict)
~report_kind:(ReadWriteRace conflict.precondition.access) precondition.access threads ~report_kind:(ReadWriteRace conflict.snapshot.access) snapshot.access threads
wobbly_paths ; wobbly_paths ;
update_reported precondition.access pname reported_acc ) update_reported snapshot.access pname reported_acc )
else reported_acc else reported_acc
| Access.Read _ | ContainerRead _ -> | Access.Read _ | ContainerRead _ ->
(* protected read. report unprotected writes and opposite protected writes as conflicts *) (* protected read. report unprotected writes and opposite protected writes as conflicts *)
let can_conflict (pre1: AccessSnapshot.t) (pre2: AccessSnapshot.t) = let can_conflict (snapshot1: AccessSnapshot.t) (snapshot2: AccessSnapshot.t) =
if pre1.lock && pre2.lock then false if snapshot1.lock && snapshot2.lock then false
else ThreadsDomain.can_conflict pre1.thread pre2.thread else ThreadsDomain.can_conflict snapshot1.thread snapshot2.thread
in in
let conflicting_writes = let conflicting_writes =
List.filter List.filter
~f:(fun {precondition= other_precondition; threads= other_threads} -> ~f:(fun {snapshot= other_snapshot; threads= other_threads} ->
if AccessSnapshot.is_unprotected other_precondition then if AccessSnapshot.is_unprotected other_snapshot then
TraceElem.is_write other_precondition.access TraceElem.is_write other_snapshot.access && ThreadsDomain.is_any other_threads
&& ThreadsDomain.is_any other_threads
else else
TraceElem.is_write other_precondition.access TraceElem.is_write other_snapshot.access && can_conflict snapshot other_snapshot
&& can_conflict precondition other_precondition ) )
accesses accesses
in in
if not (List.is_empty conflicting_writes) then ( if not (List.is_empty conflicting_writes) then (
@ -1307,9 +1307,9 @@ let report_unsafe_accesses (aggregated_access_map: reported_access list AccessLi
(* protected read with conflicting unprotected write(s). warn. *) (* protected read with conflicting unprotected write(s). warn. *)
report_thread_safety_violation tenv procdesc report_thread_safety_violation tenv procdesc
~make_description:(make_read_write_race_description ~read_is_sync:true conflict) ~make_description:(make_read_write_race_description ~read_is_sync:true conflict)
~report_kind:(ReadWriteRace conflict.precondition.access) precondition.access threads ~report_kind:(ReadWriteRace conflict.snapshot.access) snapshot.access threads
wobbly_paths ; wobbly_paths ;
update_reported precondition.access pname reported_acc ) update_reported snapshot.access pname reported_acc )
else reported_acc else reported_acc
in in
AccessListMap.fold AccessListMap.fold
@ -1477,8 +1477,8 @@ module MayAliasQuotientedAccessListMap : QuotientedAccessListMap = struct
else else
let k, vals = AccessListMap.min_binding m in let k, vals = AccessListMap.min_binding m in
let tenv = let tenv =
(List.find_exn vals ~f:(fun {precondition} -> (List.find_exn vals ~f:(fun {snapshot} ->
RacerDDomain.Access.equal (RacerDDomain.TraceElem.kind precondition.access) k )) RacerDDomain.Access.equal (RacerDDomain.TraceElem.kind snapshot.access) k ))
.tenv .tenv
in in
(* assumption: the tenv for k is sufficient for k' too *) (* assumption: the tenv for k is sufficient for k' too *)
@ -1533,7 +1533,7 @@ let make_results_table (module AccessListMap : QuotientedAccessListMap) file_env
if should_filter_access access_kind then acc if should_filter_access access_kind then acc
else else
let reported_access : reported_access = let reported_access : reported_access =
{threads; precondition= snapshot; tenv; procdesc; wobbly_paths} {threads; snapshot; tenv; procdesc; wobbly_paths}
in in
AccessListMap.add access_kind reported_access acc ) AccessListMap.add access_kind reported_access acc )
accesses acc accesses acc

Write Preview
Loading…
Cancel
Save