From 3eed17488aa2574a787ea67197b7988e167f1174 Mon Sep 17 00:00:00 2001 From: Nikos Gorogiannis Date: Wed, 18 Nov 2020 07:34:45 -0800 Subject: [PATCH] [racerd] improve summary processing on calls Summary: At a function call, an access performed by a callee must be processed in various ways before it's added to the accesses of the caller, and several of these steps may throw away the access. Previously, this was done by effectively doing a bit of transformation, creating a new set of accesses, then folding over that to add to the caller's. This is inefficient and somewhat confusing, as this can be done with one fold and a sequence of `Option.map`s. Reviewed By: skcho Differential Revision: D24885117 fbshipit-source-id: 4ab61eab9 --- infer/src/concurrency/RacerDDomain.ml | 117 +++++++++++++------------- 1 file changed, 57 insertions(+), 60 deletions(-) diff --git a/infer/src/concurrency/RacerDDomain.ml b/infer/src/concurrency/RacerDDomain.ml index 38032dd37..5789601d7 100644 --- a/infer/src/concurrency/RacerDDomain.ml +++ b/infer/src/concurrency/RacerDDomain.ml @@ -321,18 +321,55 @@ module AccessSnapshot = struct make_if_not_owned formals access lock thread ownership_precondition loc - let map_opt formals ~f t = - map t ~f:(fun elem -> {elem with access= Access.map ~f elem.access}) |> filter formals - - - let update_callee_access formals snapshot callsite ownership_precondition threads locks = + let subst_actuals_into_formals callee_formals actuals_array (t : t) = + let exp = Access.get_access_exp t.elem.access in + match FormalMap.get_formal_index (AccessExpression.get_base exp) callee_formals with + | None -> + (* non-param base variable, leave unchanged *) + Some t + | Some formal_index when formal_index >= Array.length actuals_array -> + (* vararg param which is missing, throw away *) + None + | Some formal_index -> ( + match actuals_array.(formal_index) with + | None -> + (* no useful argument can be substituted, throw away *) + None + | Some actual -> + AccessExpression.append ~onto:actual exp + |> Option.map ~f:(fun new_exp -> + map t ~f:(fun elem -> + {elem with access= Access.map ~f:(fun _ -> new_exp) elem.access} ) ) ) + + + let update_callee_access threads locks actuals_ownership (snapshot : t) = + 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 + (* 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 thread = ThreadsDomain.integrate_summary ~callee_astate:snapshot.elem.thread ~caller_astate:threads in let lock = snapshot.elem.lock || LockDomain.is_locked locks in - with_callsite snapshot callsite - |> map ~f:(fun elem -> {elem with lock; thread; ownership_precondition}) - |> filter formals + map snapshot ~f:(fun elem -> {elem with lock; thread; ownership_precondition}) + + + let integrate_summary ~caller_formals ~callee_formals callsite threads locks actuals_array + actuals_ownership snapshot = + subst_actuals_into_formals callee_formals actuals_array snapshot + |> Option.map ~f:(update_callee_access threads locks actuals_ownership) + |> Option.map ~f:(fun snapshot -> with_callsite snapshot callsite) + |> Option.bind ~f:(filter caller_formals) let is_unprotected {elem= {thread; lock; ownership_precondition}} = @@ -346,26 +383,6 @@ 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 @@ -386,14 +403,14 @@ module OwnershipDomain = struct get_owned prefix astate ) - let rec ownership_of_expr (expr : HilExp.t) ownership = + let rec ownership_of_expr ownership (expr : HilExp.t) = match expr with | AccessExpression access_expr -> get_owned access_expr ownership | Constant _ -> OwnershipAbstractValue.owned | Exception e (* treat exceptions as transparent wrt ownership *) | Cast (_, e) -> - ownership_of_expr e ownership + ownership_of_expr ownership e | _ -> OwnershipAbstractValue.unowned @@ -403,7 +420,7 @@ module OwnershipDomain = struct (* do not assign ownership to access expressions rooted at globals *) ownership else - let rhs_ownership_value = ownership_of_expr rhs_exp ownership in + let rhs_ownership_value = ownership_of_expr ownership rhs_exp in add lhs_access_exp rhs_ownership_value ownership @@ -412,7 +429,7 @@ module OwnershipDomain = struct List.nth actuals formal_index (* simply skip formal if we cannot find its actual, as opposed to assuming non-ownership *) |> Option.fold ~init ~f:(fun acc expr -> - OwnershipAbstractValue.join acc (ownership_of_expr expr ownership) ) + OwnershipAbstractValue.join acc (ownership_of_expr ownership expr) ) in let ret_ownership_wrt_actuals = match return_ownership with @@ -671,35 +688,15 @@ let add_reads_of_hilexps tenv formals exps loc astate = 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 + (* precompute arrays for actuals and ownership for fast random access *) + let actuals_array = Array.of_list_map actuals ~f:accexp_of_hilexp 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 ) + Array.of_list_map actuals ~f:(OwnershipDomain.ownership_of_expr 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 + let process snapshot acc = + AccessSnapshot.integrate_summary ~caller_formals ~callee_formals callsite caller_astate.threads + caller_astate.locks actuals_array actuals_ownership snapshot + |> fun snapshot_opt -> AccessDomain.add_opt snapshot_opt acc in - let accesses = AccessDomain.fold update_callee_access callee_accesses caller_astate.accesses in + let accesses = AccessDomain.fold process callee_accesses caller_astate.accesses in {caller_astate with accesses}