From 4633cd03c48386bbad5b75463fb629965ec12f70 Mon Sep 17 00:00:00 2001 From: Ilya Sergey Date: Wed, 21 Feb 2018 05:49:39 -0800 Subject: [PATCH] [racerd] Instrumenting the concurrency analysis with tracking of access path stability. Reviewed By: sblackshear Differential Revision: D6414244 fbshipit-source-id: d2acc16 --- infer/src/concurrency/RacerD.ml | 136 ++++++++++++++++++++----- infer/src/concurrency/RacerDDomain.ml | 136 +++++++++++++++++++++++-- infer/src/concurrency/RacerDDomain.mli | 17 +++- 3 files changed, 249 insertions(+), 40 deletions(-) diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index a2328567d..d3d8022bc 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -227,7 +227,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct ; threads= ThreadsDomain.empty ; accesses= callee_accesses ; return_ownership - ; return_attributes= AttributeSetDomain.empty } + ; return_attributes= AttributeSetDomain.empty + ; wobbly_paths= StabilityDomain.empty } let get_summary caller_pdesc callee_pname actuals callee_loc tenv (astate: Domain.astate) = @@ -379,6 +380,11 @@ module TransferFunctions (CFG : ProcCfg.S) = struct AccessDomain.fold update_accesses accesses caller_astate.accesses + (***********************************************************************) + (* Wobbly paths and where to find them. *) + (***********************************************************************) + (***********************************************************************) + let exec_instr (astate: Domain.astate) ({ProcData.tenv; extras; pdesc} as proc_data) _ (instr: HilInstr.t) = let open Domain in @@ -393,7 +399,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let ownership = OwnershipDomain.add (ret_base, []) OwnershipAbstractValue.owned astate.ownership in - {astate with accesses; ownership} + (* Record all actuals as wobbly paths *) + let wobbly_paths = StabilityDomain.add_wobbly_actuals actuals astate.wobbly_paths in + {astate with accesses; ownership; wobbly_paths} | Call (ret_opt, Direct callee_pname, actuals, call_flags, loc) -> ( let accesses_with_unannotated_calls = @@ -404,7 +412,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct add_reads actuals loc accesses_with_unannotated_calls astate.locks astate.threads astate.ownership proc_data in - let astate = {astate with accesses} in + let wobbly_paths = StabilityDomain.add_wobbly_actuals actuals astate.wobbly_paths in + let astate = {astate with accesses; wobbly_paths} in let astate = match Models.get_thread callee_pname with | BackgroundThread -> @@ -472,7 +481,13 @@ module TransferFunctions (CFG : ProcCfg.S) = struct in {summary with accesses= rebased_accesses} ) with - | Some {threads; locks; accesses; return_ownership; return_attributes} -> + | Some + { threads + ; locks + ; accesses + ; return_ownership + ; return_attributes + ; wobbly_paths= callee_wps } -> let locks = LocksDomain.join locks astate.locks in let threads = match (astate.threads, threads) with @@ -490,7 +505,14 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let ownership, attribute_map = propagate_return ret_opt return_ownership return_attributes actuals astate in - {locks; threads; accesses; ownership; attribute_map} + (* Remapping wobble paths; also bases that are not in caller's wobbly paths, i.e., callee's locals *) + let callee_wps_rebased = + Option.value_map ~default:callee_wps + ~f:(fun summary -> StabilityDomain.rebase_paths actuals summary callee_wps) + callee_pdesc + in + let wobbly_paths = StabilityDomain.join wobbly_paths callee_wps_rebased in + {locks; threads; accesses; ownership; attribute_map; wobbly_paths} | None -> let should_assume_returns_ownership (call_flags: CallFlags.t) actuals = (* assume non-interface methods with no summary and no parameters return @@ -582,7 +604,17 @@ module TransferFunctions (CFG : ProcCfg.S) = struct in let ownership = propagate_ownership lhs_access_path rhs_exp astate.ownership in let attribute_map = propagate_attributes lhs_access_path rhs_exp astate.attribute_map in - {astate with accesses; ownership; attribute_map} + (* [TODO] Do not add this path as wobbly, if it's the _first_ + initialization of a local variable (e.g. A z = getA(); --> + now z is considered wobbly). + + At the moment, I don't know how to distinguish those from + plain re-assignnments, so a lot of spurious wobbly paths is + negerated. *) + let wobbly_paths = + StabilityDomain.add_wobbly_paths_assign lhs_access_path rhs_exp astate.wobbly_paths + in + {astate with accesses; ownership; attribute_map; wobbly_paths} | Assume (assume_exp, _, _, loc) -> let rec eval_binop op var e1 e2 = match (eval_bexp var e1, eval_bexp var e2) with @@ -662,7 +694,8 @@ let empty_post : RacerDDomain.summary = ; locks= RacerDDomain.LocksDomain.empty ; accesses= RacerDDomain.AccessDomain.empty ; return_ownership= RacerDDomain.OwnershipAbstractValue.unowned - ; return_attributes= RacerDDomain.AttributeSetDomain.empty } + ; return_attributes= RacerDDomain.AttributeSetDomain.empty + ; wobbly_paths= RacerDDomain.StabilityDomain.empty } let analyze_procedure {Callbacks.proc_desc; get_proc_desc; tenv; summary} = @@ -736,7 +769,7 @@ let analyze_procedure {Callbacks.proc_desc; get_proc_desc; tenv; summary} = {RacerDDomain.empty with ownership; threads} in match Analyzer.compute_post proc_data ~initial with - | Some {threads; locks; accesses; ownership; attribute_map} -> + | Some {threads; locks; accesses; ownership; attribute_map; wobbly_paths} -> let return_var_ap = AccessPath.of_pvar (Pvar.get_ret_pvar (Procdesc.get_proc_name proc_desc)) @@ -747,7 +780,7 @@ let analyze_procedure {Callbacks.proc_desc; get_proc_desc; tenv; summary} = try AttributeMapDomain.find return_var_ap attribute_map with Not_found -> AttributeSetDomain.empty in - let post = {threads; locks; accesses; return_ownership; return_attributes} in + let post = {threads; locks; accesses; return_ownership; return_attributes; wobbly_paths} in Summary.update_summary post summary | None -> summary @@ -919,7 +952,45 @@ let make_trace ~report_kind original_path pdesc = (original_trace, original_end, None) -let report_thread_safety_violation tenv pdesc ~make_description ~report_kind access thread = +let ignore_var v = Var.is_global v || Var.is_return v + +(* Checking for a wobbly path *) +let contaminated_race_msg access wobbly_paths = + let open RacerDDomain in + let wobbly_path_opt = + match TraceElem.kind access with + | TraceElem.Kind.Read access_path + | Write access_path + (* Access paths rooted in static variables are always race-prone, + hence do not complain about contamination. *) + when not (access_path |> fst |> fst |> ignore_var) -> + let proper_prefix_path = AccessPath.truncate access_path in + let base, accesses = proper_prefix_path in + let rec prefix_in_wobbly_paths prefix = function + | [] -> + let wobbly = (base, []) in + if StabilityDomain.mem (AccessPath.Abs.Exact wobbly) wobbly_paths then + Some (wobbly, access_path) + else None + | access :: accesses -> + let prefix' = prefix @ [access] in + let candidate = (base, prefix') in + if StabilityDomain.mem (AccessPath.Abs.Exact candidate) wobbly_paths then + Some (candidate, access_path) + else prefix_in_wobbly_paths prefix' accesses + in + prefix_in_wobbly_paths [] accesses + | _ -> + None + in + Option.map wobbly_path_opt ~f:(fun (wobbly_path, access_path) -> + F.asprintf + "@\n\nNote that the prefix path %a has been contaminated during the execution, so the reported race on %a might be a false positive.@\n\n" + AccessPath.pp wobbly_path AccessPath.pp access_path ) + + +let report_thread_safety_violation tenv pdesc ~make_description ~report_kind access thread + wobbly_paths = let open RacerDDomain in let pname = Procdesc.get_proc_name pdesc in let report_one_path ((_, sinks) as path) = @@ -952,7 +1023,12 @@ let report_thread_safety_violation tenv pdesc ~make_description ~report_kind acc (* why we are reporting it *) let issue_type, explanation = get_reporting_explanation report_kind tenv pname thread in let error_message = F.sprintf "%s%s" description explanation in - let exn = Exceptions.Checkers (issue_type, Localise.verbatim_desc error_message) in + let contaminated = contaminated_race_msg access wobbly_paths in + let exn = + Exceptions.Checkers + ( issue_type + , Localise.verbatim_desc (error_message ^ Option.value contaminated ~default:"") ) + in let end_locs = Option.to_list original_end @ Option.to_list conflict_end in let access = IssueAuxData.encode (pname, access, end_locs) in Reporting.log_error_deprecated ~store_summary:true pname ~loc ~ltr ~access exn @@ -971,7 +1047,7 @@ let report_unannotated_interface_violation tenv pdesc access thread reported_pna class_name MF.pp_monospaced "@ThreadSafe" in report_thread_safety_violation tenv pdesc ~make_description ~report_kind:UnannotatedInterface - access thread + access thread RacerDDomain.StabilityDomain.empty | _ -> (* skip reporting on C++ *) () @@ -1000,7 +1076,8 @@ type reported_access = ; threads: RacerDDomain.ThreadsDomain.astate ; precondition: RacerDDomain.AccessData.t ; tenv: Tenv.t - ; procdesc: Procdesc.t } + ; procdesc: Procdesc.t + ; wobbly_paths: RacerDDomain.StabilityDomain.astate } let make_read_write_race_description ~read_is_sync (conflict: reported_access) pname final_sink_site initial_sink_site final_sink = @@ -1095,7 +1172,8 @@ let report_unsafe_accesses (aggregated_access_map: reported_access list AccessLi reported else reported in - let report_unsafe_access {access; precondition; threads; tenv; procdesc} accesses reported_acc = + let report_unsafe_access {access; precondition; threads; tenv; procdesc; wobbly_paths} accesses + reported_acc = let pname = Procdesc.get_proc_name procdesc in if is_duplicate_report access pname reported_acc then reported_acc else @@ -1133,7 +1211,7 @@ let report_unsafe_accesses (aggregated_access_map: reported_access list AccessLi 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) access threads ; + ~report_kind:(WriteWriteRace conflict) access threads wobbly_paths ; update_reported access pname reported_acc else reported_acc | _ -> @@ -1163,7 +1241,7 @@ let report_unsafe_accesses (aggregated_access_map: reported_access list AccessLi 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.access) access threads ; + ~report_kind:(ReadWriteRace conflict.access) access threads wobbly_paths ; update_reported access pname reported_acc else reported_acc | Access.Read _ | ContainerRead _ -> @@ -1191,7 +1269,7 @@ 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.access) access threads ; + ~report_kind:(ReadWriteRace conflict.access) access threads wobbly_paths ; update_reported access pname reported_acc else reported_acc in @@ -1331,8 +1409,8 @@ module MayAliasQuotientedAccessListMap : QuotientedAccessListMap = struct AccessPath.equal p1 p2 - (* equivalence relation computing whether two access paths may refer to the - same heap location. *) + (* equivalence relation computing whether two access paths may refer + to the same heap location. *) let may_alias tenv p1 p2 = let open Typ in let open AccessPath in @@ -1403,12 +1481,13 @@ let should_filter_access access = false -(* create a map from [abstraction of a memory loc] -> accesses that may touch that memory loc. for - now, our abstraction is an access path like x.f.g whose concretization is the set of memory cells +(* create a map from [abstraction of a memory loc] -> accesses that + may touch that memory loc. for now, our abstraction is an access + path like x.f.g whose concretization is the set of memory cells that x.f.g may point to during execution *) let make_results_table (module AccessListMap : QuotientedAccessListMap) file_env = let open RacerDDomain in - let aggregate_post {threads; accesses} tenv procdesc acc = + let aggregate_post {threads; accesses; wobbly_paths} tenv procdesc acc = AccessDomain.fold (fun precondition accesses acc -> PathDomain.Sinks.fold @@ -1416,7 +1495,9 @@ let make_results_table (module AccessListMap : QuotientedAccessListMap) file_env let access_kind = TraceElem.kind access in if should_filter_access access_kind then acc else - let reported_access = {access; precondition; threads; tenv; procdesc} in + let reported_access : reported_access = + {access; threads; precondition; tenv; procdesc; wobbly_paths} + in AccessListMap.add access_kind reported_access acc ) (PathDomain.sinks accesses) acc ) accesses acc @@ -1431,8 +1512,8 @@ let make_results_table (module AccessListMap : QuotientedAccessListMap) file_env List.fold ~f:aggregate_posts file_env ~init:AccessListMap.empty |> AccessListMap.quotient -(* aggregate all of the procedures in the file env by their declaring class. this lets us analyze - each class individually *) +(* aggregate all of the procedures in the file env by their declaring + class. this lets us analyze each class individually *) let aggregate_by_class file_env = List.fold file_env ~f:(fun acc ((_, pdesc) as proc) -> @@ -1449,8 +1530,9 @@ let aggregate_by_class file_env = ~init:String.Map.empty -(* Gathers results by analyzing all the methods in a file, then post-processes the results to check - an (approximation of) thread safety *) +(* Gathers results by analyzing all the methods in a file, then + post-processes the results to check an (approximation of) thread + safety *) let file_analysis {Callbacks.procedures} = String.Map.iter ~f:(fun class_env -> diff --git a/infer/src/concurrency/RacerDDomain.ml b/infer/src/concurrency/RacerDDomain.ml index 05dd79446..8c8e669fb 100644 --- a/infer/src/concurrency/RacerDDomain.ml +++ b/infer/src/concurrency/RacerDDomain.ml @@ -431,12 +431,116 @@ module AccessDomain = struct let get_accesses precondition t = try find precondition t with Not_found -> PathDomain.empty end +module StabilityDomain = struct + include AccessTree.PathSet (AccessTree.DefaultConfig) + + let get_all_paths t = + fold + (fun paths z _ -> + match z with AccessPath.Abs.Abstracted p | AccessPath.Abs.Exact p -> p :: paths ) + t [] + + + let add_path (access_path: AccessPath.t) t = + let (base, _), accesses = access_path in + (* Without this check, short prefixes will override longer paths in the tree *) + if mem (AccessPath.Abs.Abstracted access_path) t then t + else + match (base, accesses) with + (* Do not add a vanilla "this" as a prefix *) + | Var.ProgramVar pvar, [] + when Pvar.is_this pvar -> + t + | _ -> + let ap_abs = AccessPath.Abs.Exact access_path in + add_trace ap_abs true t + + + let add_wobbly_path_exp exp paths = + let access_paths = HilExp.get_access_paths exp in + List.fold ~f:(fun acc p -> add_path p acc) access_paths ~init:paths + + + let add_wobbly_actuals exps paths = + (* Checking conditions for inter-procedural stability: + automatically add duplicating actuals, "deep" stability + checking will be handled by processing the method's footprint + and rebasing (see StabilityDomain.rebase_paths). *) + let is_dup_access_path e = + List.count exps ~f:(fun x -> + match (x, e) with + | HilExp.AccessExpression ae1, HilExp.AccessExpression ae2 -> + AccessPath.equal + (AccessExpression.to_access_path ae1) + (AccessExpression.to_access_path ae2) + | _, _ -> + false ) + > 1 + in + let is_prefix_exp x e = + match (x, e) with + | HilExp.AccessExpression ae1, HilExp.AccessExpression ae2 -> + let open AccessExpression in + let ap1, ap2 = (to_access_path ae1, to_access_path ae2) in + AccessPath.is_prefix ap1 ap2 && not (AccessPath.equal ap1 ap2) + | _ -> + false + in + let find_all_prefixes e = List.filter exps ~f:(fun x -> is_prefix_exp x e) in + let with_duplicates = + List.fold exps ~init:paths ~f:(fun acc e -> + if is_dup_access_path e then add_wobbly_path_exp e acc else acc ) + in + let with_prefixes = + List.fold exps ~init:with_duplicates ~f:(fun acc_paths e -> + List.fold (find_all_prefixes e) ~init:acc_paths ~f:(fun acc1 e1 -> + add_wobbly_path_exp e1 acc1 ) ) + in + with_prefixes + + + let add_wobbly_paths_assign lhs_path rhs_exp paths = + let paths_with_lhs = add_path lhs_path paths in + let paths_with_lsh_rhs = add_wobbly_path_exp rhs_exp paths_with_lhs in + paths_with_lsh_rhs + + + let rebase_paths actuals pdesc t = + let formal_map = FormalMap.make pdesc in + let remove_pure_formals paths = + List.filter paths ~f:(fun p -> + match p with + | base, [] when FormalMap.get_formal_index base formal_map |> Option.is_some -> + false + | _ -> + true ) + in + let expand_path ((base, accesses) as path) = + match FormalMap.get_formal_index base formal_map with + | Some formal_index -> ( + match List.nth actuals formal_index with + | Some actual_exp -> ( + match HilExp.get_access_paths actual_exp with + | [actual] -> + AccessPath.append actual accesses + | _ -> + path ) + | None -> + path ) + | None -> + path + in + get_all_paths t |> remove_pure_formals |> List.map ~f:expand_path + |> List.fold ~f:(fun acc p -> add_path p acc) ~init:empty +end + type astate = { threads: ThreadsDomain.astate ; locks: LocksDomain.astate ; accesses: AccessDomain.astate ; ownership: OwnershipDomain.astate - ; attribute_map: AttributeMapDomain.astate } + ; attribute_map: AttributeMapDomain.astate + ; wobbly_paths: StabilityDomain.astate } let empty = let threads = ThreadsDomain.empty in @@ -444,12 +548,14 @@ let empty = let accesses = AccessDomain.empty in let ownership = OwnershipDomain.empty in let attribute_map = AttributeMapDomain.empty in - {threads; locks; accesses; ownership; attribute_map} + let wobbly_paths = StabilityDomain.empty in + {threads; locks; accesses; ownership; attribute_map; wobbly_paths} -let is_empty {threads; locks; accesses; ownership; attribute_map} = +let is_empty {threads; locks; accesses; ownership; attribute_map; wobbly_paths} = ThreadsDomain.is_empty threads && LocksDomain.is_empty locks && AccessDomain.is_empty accesses && OwnershipDomain.is_empty ownership && AttributeMapDomain.is_empty attribute_map + && StabilityDomain.is_empty wobbly_paths let ( <= ) ~lhs ~rhs = @@ -459,6 +565,7 @@ let ( <= ) ~lhs ~rhs = && LocksDomain.( <= ) ~lhs:lhs.locks ~rhs:rhs.locks && AccessDomain.( <= ) ~lhs:lhs.accesses ~rhs:rhs.accesses && AttributeMapDomain.( <= ) ~lhs:lhs.attribute_map ~rhs:rhs.attribute_map + && StabilityDomain.( <= ) ~lhs:lhs.wobbly_paths ~rhs:rhs.wobbly_paths let join astate1 astate2 = @@ -469,7 +576,8 @@ let join astate1 astate2 = let accesses = AccessDomain.join astate1.accesses astate2.accesses in let ownership = OwnershipDomain.join astate1.ownership astate2.ownership in let attribute_map = AttributeMapDomain.join astate1.attribute_map astate2.attribute_map in - {threads; locks; accesses; ownership; attribute_map} + let wobbly_paths = StabilityDomain.join astate1.wobbly_paths astate2.wobbly_paths in + {threads; locks; accesses; ownership; attribute_map; wobbly_paths} let widen ~prev ~next ~num_iters = @@ -482,7 +590,10 @@ let widen ~prev ~next ~num_iters = let attribute_map = AttributeMapDomain.widen ~prev:prev.attribute_map ~next:next.attribute_map ~num_iters in - {threads; locks; accesses; ownership; attribute_map} + let wobbly_paths = + StabilityDomain.widen ~prev:prev.wobbly_paths ~next:next.wobbly_paths ~num_iters + in + {threads; locks; accesses; ownership; attribute_map; wobbly_paths} type summary = @@ -490,19 +601,22 @@ type summary = ; locks: LocksDomain.astate ; accesses: AccessDomain.astate ; return_ownership: OwnershipAbstractValue.astate - ; return_attributes: AttributeSetDomain.astate } + ; return_attributes: AttributeSetDomain.astate + ; wobbly_paths: StabilityDomain.astate } -let pp_summary fmt {threads; locks; accesses; return_ownership; return_attributes} = +let pp_summary fmt {threads; locks; accesses; return_ownership; return_attributes; wobbly_paths} = F.fprintf fmt - "@\nThreads: %a, Locks: %a @\nAccesses %a @\nOwnership: %a @\nReturn Attributes: %a @\n" + "@\nThreads: %a, Locks: %a @\nAccesses %a @\nOwnership: %a @\nReturn Attributes: %a @\nWobbly Paths: %a@\n" ThreadsDomain.pp threads LocksDomain.pp locks AccessDomain.pp accesses OwnershipAbstractValue.pp return_ownership AttributeSetDomain.pp return_attributes + StabilityDomain.pp wobbly_paths -let pp fmt {threads; locks; accesses; ownership; attribute_map} = - F.fprintf fmt "Threads: %a, Locks: %a @\nAccesses %a @\n Ownership: %a @\nAttributes: %a @\n" +let pp fmt {threads; locks; accesses; ownership; attribute_map; wobbly_paths} = + F.fprintf fmt + "Threads: %a, Locks: %a @\nAccesses %a @\n Ownership: %a @\nAttributes: %a @\nNon-stable Paths: %a@\n" ThreadsDomain.pp threads LocksDomain.pp locks AccessDomain.pp accesses OwnershipDomain.pp - ownership AttributeMapDomain.pp attribute_map + ownership AttributeMapDomain.pp attribute_map StabilityDomain.pp wobbly_paths let rec attributes_of_expr attribute_map e = diff --git a/infer/src/concurrency/RacerDDomain.mli b/infer/src/concurrency/RacerDDomain.mli index cfe670e0e..728ac4b6a 100644 --- a/infer/src/concurrency/RacerDDomain.mli +++ b/infer/src/concurrency/RacerDDomain.mli @@ -190,6 +190,16 @@ module AccessDomain : sig (** get all accesses with the given precondition *) end +module StabilityDomain : sig + include module type of AccessTree.PathSet (AccessTree.DefaultConfig) + + val rebase_paths : HilExp.t list -> Procdesc.t -> t -> t + + val add_wobbly_paths_assign : AccessPath.t -> HilExp.t -> t -> t + + val add_wobbly_actuals : HilExp.t list -> t -> t +end + type astate = { threads: ThreadsDomain.astate (** current thread: main, background, or unknown *) ; locks: LocksDomain.astate (** boolean that is true if a lock must currently be held *) @@ -197,7 +207,9 @@ type astate = (** read and writes accesses performed without ownership permissions *) ; ownership: OwnershipDomain.astate (** map of access paths to ownership predicates *) ; attribute_map: AttributeMapDomain.astate - (** map of access paths to attributes such as owned, functional, ... *) } + (** map of access paths to attributes such as owned, functional, ... *) + ; wobbly_paths: StabilityDomain.astate + (** Record the "touched" paths that can compromise the race detection **) } (** same as astate, but without [attribute_map] (since these involve locals) and with the addition of the ownership/attributes associated with the return value as well as the set of formals which @@ -207,7 +219,8 @@ type summary = ; locks: LocksDomain.astate ; accesses: AccessDomain.astate ; return_ownership: OwnershipAbstractValue.astate - ; return_attributes: AttributeSetDomain.astate } + ; return_attributes: AttributeSetDomain.astate + ; wobbly_paths: StabilityDomain.astate } include AbstractDomain.WithBottom with type astate := astate