From ebc364a80121ef7b7d9625b942db9680cfb6b259 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Thu, 26 Apr 2018 13:49:38 -0700 Subject: [PATCH] [racerd] precondition -> snapshot Reviewed By: ngorogiannis Differential Revision: D7754774 fbshipit-source-id: 5d04c60 --- infer/src/concurrency/RacerD.ml | 90 ++++++++++++++++----------------- 1 file changed, 45 insertions(+), 45 deletions(-) diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index 50ebff746..a2fc64bff 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -304,17 +304,18 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | None -> path in - let expand_pre (snapshot: AccessSnapshot.t) = + let expand_precondition (snapshot: AccessSnapshot.t) = let access = TraceElem.map ~f:expand_path snapshot.access in AccessSnapshot.make_ access snapshot.lock snapshot.thread snapshot.ownership_precondition in - AccessDomain.map expand_pre accesses + AccessDomain.map expand_precondition accesses let add_callee_accesses (caller_astate: Domain.astate) callee_accesses locks threads actuals callee_pname pdesc loc = 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 | HilExp.Constant _ -> (* 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 *) False in - let update_ownership_pre actual_index (acc: AccessSnapshot.OwnershipPrecondition.t) = + let update_ownership_precondition actual_index (acc: AccessSnapshot.OwnershipPrecondition.t) = match acc with | False -> (* precondition can't be satisfied *) @@ -354,7 +355,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | Conjunction actual_indexes -> match List.nth actuals actual_index with | Some actual -> - conjoin_ownership_pre actual actual_indexes + conjoin_ownership_precondition actual actual_indexes | None -> L.internal_error "Bad actual index %d for callee %a with %d actuals." actual_index Typ.Procname.pp callee_pname (List.length actuals) ; @@ -370,8 +371,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let ownership_precondition = match snapshot.ownership_precondition with | Conjunction indexes -> - let empty_pre = AccessSnapshot.OwnershipPrecondition.Conjunction IntSet.empty in - IntSet.fold update_ownership_pre indexes empty_pre + let empty_precondition = + AccessSnapshot.OwnershipPrecondition.Conjunction IntSet.empty + in + IntSet.fold update_ownership_precondition indexes empty_precondition | False -> snapshot.ownership_precondition in @@ -1110,7 +1113,7 @@ let make_unprotected_write_description pname final_sink_site initial_sink_site f type reported_access = { threads: RacerDDomain.ThreadsDomain.astate - ; precondition: RacerDDomain.AccessSnapshot.t + ; snapshot: RacerDDomain.AccessSnapshot.t ; tenv: Tenv.t ; procdesc: Procdesc.t ; wobbly_paths: RacerDDomain.StabilityDomain.astate } @@ -1208,21 +1211,20 @@ let report_unsafe_accesses (aggregated_access_map: reported_access list AccessLi reported else reported in - let report_unsafe_access {precondition; threads; tenv; procdesc; wobbly_paths} accesses - reported_acc = + let report_unsafe_access {snapshot; threads; tenv; procdesc; wobbly_paths} accesses reported_acc = 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 - match TraceElem.kind precondition.access with + match TraceElem.kind snapshot.access with | Access.InterfaceCall unannoted_call_pname -> if - AccessSnapshot.is_unprotected precondition && ThreadsDomain.is_any threads + AccessSnapshot.is_unprotected snapshot && ThreadsDomain.is_any threads && Models.is_marked_thread_safe procdesc tenv then ( (* 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 ; - update_reported precondition.access pname reported_acc ) + update_reported snapshot.access pname reported_acc ) else reported_acc | Access.Write _ | ContainerWrite _ -> ( 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 conflict with and report them *) List.filter_map - ~f:(fun {precondition= other_precondition; threads= other_threads} -> + ~f:(fun {snapshot= other_snapshot; threads= other_threads} -> if - TraceElem.is_write other_precondition.access + TraceElem.is_write other_snapshot.access && ThreadsDomain.is_any other_threads - then Some other_precondition.access + then Some other_snapshot.access else None ) accesses in if - AccessSnapshot.is_unprotected precondition + AccessSnapshot.is_unprotected snapshot && (not (List.is_empty writes_on_background_thread) || ThreadsDomain.is_any threads) then ( let conflict = List.hd writes_on_background_thread in report_thread_safety_violation tenv procdesc ~make_description:make_unprotected_write_description - ~report_kind:(WriteWriteRace conflict) precondition.access threads wobbly_paths ; - update_reported precondition.access pname reported_acc ) + ~report_kind:(WriteWriteRace conflict) snapshot.access threads wobbly_paths ; + update_reported snapshot.access pname reported_acc ) else reported_acc | _ -> (* Do not report unprotected writes when an access can't run in parallel with itself, or for ObjC_Cpp *) 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 writes *) - let is_cpp_protected_write pre = - Typ.Procname.is_java pname || not (AccessSnapshot.is_unprotected pre) + let is_cpp_protected_write snapshot = + Typ.Procname.is_java pname || not (AccessSnapshot.is_unprotected snapshot) in - let is_conflict (pre: AccessSnapshot.t) other_thread = - TraceElem.is_write pre.access + let is_conflict (snapshot: AccessSnapshot.t) other_thread = + TraceElem.is_write snapshot.access && if Typ.Procname.is_java pname then ThreadsDomain.is_any threads || ThreadsDomain.is_any other_thread - else is_cpp_protected_write pre + else is_cpp_protected_write snapshot in let all_writes = List.filter - ~f:(fun {precondition; threads= other_threads} -> - is_conflict precondition other_threads ) + ~f:(fun {snapshot; threads= other_threads} -> is_conflict snapshot other_threads) accesses in if not (List.is_empty all_writes) then ( let conflict = List.hd_exn all_writes in report_thread_safety_violation tenv procdesc ~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 ; - update_reported precondition.access pname reported_acc ) + update_reported snapshot.access pname reported_acc ) else reported_acc | Access.Read _ | ContainerRead _ -> (* protected read. report unprotected writes and opposite protected writes as conflicts *) - let can_conflict (pre1: AccessSnapshot.t) (pre2: AccessSnapshot.t) = - if pre1.lock && pre2.lock then false - else ThreadsDomain.can_conflict pre1.thread pre2.thread + let can_conflict (snapshot1: AccessSnapshot.t) (snapshot2: AccessSnapshot.t) = + if snapshot1.lock && snapshot2.lock then false + else ThreadsDomain.can_conflict snapshot1.thread snapshot2.thread in let conflicting_writes = List.filter - ~f:(fun {precondition= other_precondition; threads= other_threads} -> - if AccessSnapshot.is_unprotected other_precondition then - TraceElem.is_write other_precondition.access - && ThreadsDomain.is_any other_threads + ~f:(fun {snapshot= other_snapshot; threads= other_threads} -> + if AccessSnapshot.is_unprotected other_snapshot then + TraceElem.is_write other_snapshot.access && ThreadsDomain.is_any other_threads else - TraceElem.is_write other_precondition.access - && can_conflict precondition other_precondition ) + TraceElem.is_write other_snapshot.access && can_conflict snapshot other_snapshot + ) accesses in 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. *) report_thread_safety_violation tenv procdesc ~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 ; - update_reported precondition.access pname reported_acc ) + update_reported snapshot.access pname reported_acc ) else reported_acc in AccessListMap.fold @@ -1477,8 +1477,8 @@ module MayAliasQuotientedAccessListMap : QuotientedAccessListMap = struct else let k, vals = AccessListMap.min_binding m in let tenv = - (List.find_exn vals ~f:(fun {precondition} -> - RacerDDomain.Access.equal (RacerDDomain.TraceElem.kind precondition.access) k )) + (List.find_exn vals ~f:(fun {snapshot} -> + RacerDDomain.Access.equal (RacerDDomain.TraceElem.kind snapshot.access) k )) .tenv in (* 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 else let reported_access : reported_access = - {threads; precondition= snapshot; tenv; procdesc; wobbly_paths} + {threads; snapshot; tenv; procdesc; wobbly_paths} in AccessListMap.add access_kind reported_access acc ) accesses acc