diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index e2abf8aa9..79fd5cfe2 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -20,70 +20,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct type nonrec analysis_data = analysis_data - let expand_actuals formals actuals accesses pdesc = - (* FIXME fix quadratic order with an array-backed substitution *) + let call_without_summary tenv ret_base callee_pname actuals astate = let open Domain in - if AccessDomain.is_empty accesses then accesses - else - let formal_map = FormalMap.make pdesc in - let expand_exp exp = - match FormalMap.get_formal_index (AccessExpression.get_base exp) formal_map with - | Some formal_index -> ( - match List.nth actuals formal_index with - | Some actual_exp -> ( - match accexp_of_hilexp actual_exp with - | Some actual -> - AccessExpression.append ~onto:actual exp |> Option.value ~default:exp - | None -> - exp ) - | None -> - exp ) - | None -> - exp - in - let add snapshot acc = - let snapshot_opt' = AccessSnapshot.map_opt formals ~f:expand_exp snapshot in - AccessDomain.add_opt snapshot_opt' acc - in - AccessDomain.fold add accesses AccessDomain.empty - - - let add_callee_accesses formals (caller_astate : Domain.t) callee_accesses locks threads actuals - callee_pname loc = - let open Domain in - let callsite = CallSite.make callee_pname loc in - let actuals_ownership = - (* precompute array holding ownership of each actual for fast random access *) - Array.of_list_map actuals ~f:(fun actual_exp -> - OwnershipDomain.ownership_of_expr actual_exp caller_astate.ownership ) - in - let update_ownership_precondition actual_index (acc : OwnershipAbstractValue.t) = - if actual_index >= Array.length actuals_ownership then - (* vararg methods can result into missing actuals so simply ignore *) - acc - else OwnershipAbstractValue.join acc actuals_ownership.(actual_index) - in - let update_callee_access (snapshot : AccessSnapshot.t) acc = - (* update precondition with caller ownership info *) - let ownership_precondition = - match snapshot.elem.ownership_precondition with - | OwnedIf indexes -> - IntSet.fold update_ownership_precondition indexes OwnershipAbstractValue.owned - | Unowned -> - snapshot.elem.ownership_precondition - in - let snapshot_opt = - AccessSnapshot.update_callee_access formals snapshot callsite ownership_precondition threads - locks - in - AccessDomain.add_opt snapshot_opt acc - in - AccessDomain.fold update_callee_access callee_accesses caller_astate.accesses - - - let call_without_summary tenv callee_pname ret_base actuals astate = - let open RacerDModels in - let open RacerDDomain in if RacerDModels.is_synchronized_container_constructor tenv callee_pname actuals then apply_to_first_actual actuals astate ~f:(fun receiver -> let attribute_map = AttributeMapDomain.add receiver Synchronized astate.attribute_map in @@ -93,7 +31,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct AttributeMapDomain.add (AccessExpression.base ret_base) Synchronized astate.attribute_map in {astate with attribute_map} - else if is_box callee_pname then + else if RacerDModels.is_box callee_pname then apply_to_first_actual actuals astate ~f:(fun actual_access_expr -> if AttributeMapDomain.is_functional astate.attribute_map actual_access_expr then (* TODO: check for constants, which are functional? *) @@ -176,36 +114,30 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | GuardConstruct {acquire_now= false} -> astate | NoEffect -> ( - let rebased_summary_opt = - analyze_dependency callee_pname - |> Option.map ~f:(fun (callee_proc_desc, summary) -> - let rebased_accesses = - expand_actuals formals actuals summary.accesses callee_proc_desc - in - {summary with accesses= rebased_accesses} ) - in - match rebased_summary_opt with - | Some {threads; locks; accesses; return_ownership; return_attribute} -> - let locks = - LockDomain.integrate_summary ~caller_astate:astate.locks ~callee_astate:locks - in - let accesses = - add_callee_accesses formals astate accesses locks threads actuals callee_pname loc - in - let ownership = - OwnershipDomain.propagate_return ret_access_exp return_ownership actuals - astate.ownership - in - let attribute_map = - AttributeMapDomain.add ret_access_exp return_attribute astate.attribute_map - in - let threads = - ThreadsDomain.integrate_summary ~caller_astate:astate.threads - ~callee_astate:threads - in - {locks; threads; accesses; ownership; attribute_map} - | None -> - call_without_summary tenv callee_pname ret_base actuals astate ) + match analyze_dependency callee_pname with + | Some (callee_proc_desc, summary) -> + let callee_formals = FormalMap.make callee_proc_desc in + let {threads; locks; return_ownership; return_attribute} = summary in + let astate = + Domain.add_callee_accesses ~caller_formals:formals ~callee_formals + ~callee_accesses:summary.accesses callee_pname actuals loc astate + in + let locks = + LockDomain.integrate_summary ~caller_astate:astate.locks ~callee_astate:locks + in + let ownership = + OwnershipDomain.propagate_return ret_access_exp return_ownership actuals + astate.ownership + in + let attribute_map = + AttributeMapDomain.add ret_access_exp return_attribute astate.attribute_map + in + let threads = + ThreadsDomain.integrate_summary ~caller_astate:astate.threads ~callee_astate:threads + in + {astate with locks; threads; ownership; attribute_map} + | None -> + call_without_summary tenv ret_base callee_pname actuals astate ) in let add_if_annotated predicate attribute attribute_map = if PatternMatch.override_exists predicate tenv callee_pname then diff --git a/infer/src/concurrency/RacerDDomain.ml b/infer/src/concurrency/RacerDDomain.ml index 9627512ea..38032dd37 100644 --- a/infer/src/concurrency/RacerDDomain.ml +++ b/infer/src/concurrency/RacerDDomain.ml @@ -346,6 +346,26 @@ module AccessDomain = struct let add_opt snapshot_opt astate = Option.fold snapshot_opt ~init:astate ~f:(fun acc s -> add s acc) + + + let subst_actuals_into_formals ~caller_formals ~caller_actuals accesses ~callee_formals = + if is_empty accesses then accesses + else + let actuals_array = Array.of_list_map caller_actuals ~f:accexp_of_hilexp in + let expand_exp exp = + match FormalMap.get_formal_index (AccessExpression.get_base exp) callee_formals with + | None -> + exp + | Some formal_index when formal_index >= Array.length actuals_array -> + exp + | Some formal_index -> ( + match actuals_array.(formal_index) with + | None -> + exp + | Some actual -> + AccessExpression.append ~onto:actual exp |> Option.value ~default:exp ) + in + filter_map (AccessSnapshot.map_opt caller_formals ~f:expand_exp) accesses end module OwnershipDomain = struct @@ -646,3 +666,40 @@ let add_container_access tenv formals ~is_write ret_base callee_pname actuals lo let add_reads_of_hilexps tenv formals exps loc astate = List.fold exps ~init:astate ~f:(add_access tenv formals loc ~is_write:false) + + +let add_callee_accesses ~caller_formals ~callee_formals ~callee_accesses callee_pname actuals loc + (caller_astate : t) = + let callsite = CallSite.make callee_pname loc in + let callee_accesses = + AccessDomain.subst_actuals_into_formals ~caller_formals ~caller_actuals:actuals callee_accesses + ~callee_formals + in + let actuals_ownership = + (* precompute array holding ownership of each actual for fast random access *) + Array.of_list_map actuals ~f:(fun actual_exp -> + OwnershipDomain.ownership_of_expr actual_exp caller_astate.ownership ) + in + let update_ownership_precondition actual_index (acc : OwnershipAbstractValue.t) = + if actual_index >= Array.length actuals_ownership then + (* vararg methods can result into missing actuals so simply ignore *) + acc + else OwnershipAbstractValue.join acc actuals_ownership.(actual_index) + in + let update_callee_access (snapshot : AccessSnapshot.t) acc = + (* update precondition with caller ownership info *) + let ownership_precondition = + match snapshot.elem.ownership_precondition with + | OwnedIf indexes -> + IntSet.fold update_ownership_precondition indexes OwnershipAbstractValue.owned + | Unowned -> + snapshot.elem.ownership_precondition + in + let snapshot_opt = + AccessSnapshot.update_callee_access caller_formals snapshot callsite ownership_precondition + caller_astate.threads caller_astate.locks + in + AccessDomain.add_opt snapshot_opt acc + in + let accesses = AccessDomain.fold update_callee_access callee_accesses caller_astate.accesses in + {caller_astate with accesses} diff --git a/infer/src/concurrency/RacerDDomain.mli b/infer/src/concurrency/RacerDDomain.mli index 3ead2765a..b10db45d8 100644 --- a/infer/src/concurrency/RacerDDomain.mli +++ b/infer/src/concurrency/RacerDDomain.mli @@ -9,8 +9,6 @@ open! IStd module AccessExpression = HilExp.AccessExpression module F = Format -val accexp_of_hilexp : HilExp.t -> HilExp.access_expression option - val apply_to_first_actual : HilExp.t list -> 'a -> f:(HilExp.access_expression -> 'a) -> 'a val pp_exp : F.formatter -> AccessExpression.t -> unit @@ -79,8 +77,6 @@ module OwnershipAbstractValue : sig val owned : t val make_owned_if : int -> t - - val join : t -> t -> t end (** snapshot of the relevant state at the time of a heap access: concurrent thread(s), lock(s) held, @@ -105,24 +101,9 @@ module AccessSnapshot : sig val is_unprotected : t -> bool (** return true if not protected by lock, thread, or ownership *) - - val map_opt : FormalMap.t -> f:(AccessExpression.t -> AccessExpression.t) -> t -> t option - - val update_callee_access : - FormalMap.t - -> t - -> CallSite.t - -> OwnershipAbstractValue.t - -> ThreadsDomain.t - -> LockDomain.t - -> t option end -module AccessDomain : sig - include AbstractDomain.FiniteSetS with type elt = AccessSnapshot.t - - val add_opt : elt option -> t -> t -end +module AccessDomain : AbstractDomain.FiniteSetS with type elt = AccessSnapshot.t module OwnershipDomain : sig type t @@ -134,8 +115,6 @@ module OwnershipDomain : sig val propagate_assignment : AccessExpression.t -> HilExp.t -> t -> t val propagate_return : AccessExpression.t -> OwnershipAbstractValue.t -> HilExp.t list -> t -> t - - val ownership_of_expr : HilExp.t -> t -> OwnershipAbstractValue.t end module Attribute : sig @@ -204,3 +183,13 @@ val add_container_access : -> t val add_reads_of_hilexps : Tenv.t -> FormalMap.t -> HilExp.t list -> Location.t -> t -> t + +val add_callee_accesses : + caller_formals:FormalMap.t + -> callee_formals:FormalMap.t + -> callee_accesses:AccessDomain.t + -> Procname.t + -> HilExp.t list + -> Location.t + -> t + -> t