From 72819a3865a5ad64f86d25b909f8f1201364d85a Mon Sep 17 00:00:00 2001 From: Nikos Gorogiannis Date: Fri, 17 Apr 2020 07:16:17 -0700 Subject: [PATCH] [racerd] remove ownership init logic for locals Summary: Now that only races rooted at formals or globals are reported, there is no point using the ownership domain to exclude accesses to locals, so remove the code that initialises the ownership of those. Also, remove an accidentally quadratic use of `Map.bindings |> List.find` in `FormalMap` and simplify the analysis driver. Reviewed By: skcho Differential Revision: D21066855 fbshipit-source-id: 126080778 --- infer/src/absint/FormalMap.ml | 2 - infer/src/absint/FormalMap.mli | 3 -- infer/src/concurrency/RacerD.ml | 84 +++++++++++++-------------------- 3 files changed, 34 insertions(+), 55 deletions(-) diff --git a/infer/src/absint/FormalMap.ml b/infer/src/absint/FormalMap.ml index e450869f6..6be767d40 100644 --- a/infer/src/absint/FormalMap.ml +++ b/infer/src/absint/FormalMap.ml @@ -36,8 +36,6 @@ let get_formal_base index t = |> Option.map ~f:fst -let get_formals_indexes = AccessPath.BaseMap.bindings - let pp = AccessPath.BaseMap.pp ~pp_value:Int.pp let cardinal = AccessPath.BaseMap.cardinal diff --git a/infer/src/absint/FormalMap.mli b/infer/src/absint/FormalMap.mli index 8e04433c4..f8eef7f76 100644 --- a/infer/src/absint/FormalMap.mli +++ b/infer/src/absint/FormalMap.mli @@ -27,9 +27,6 @@ val get_formal_base : int -> t -> AccessPath.base option (** return the base var for the given index if it exists, or None if it does not. Note: this is linear in the size of the formal map *) -val get_formals_indexes : t -> (AccessPath.base * int) list -(** Get a list of (base * index) pairs. Note: these are sorted by base, not index *) - val pp : F.formatter -> t -> unit [@@warning "-32"] val cardinal : t -> int diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index b4c56e727..f8fb0bf67 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -430,9 +430,22 @@ let analyze_procedure {Callbacks.exe_env; summary} = let proc_name = Summary.get_proc_name summary in let tenv = Exe_env.get_tenv exe_env proc_name in let open ConcurrencyModels in - let method_annotation = (Procdesc.get_attributes proc_desc).method_annotation in + let add_owned_formal acc base = OwnershipDomain.add base OwnershipAbstractValue.owned acc in + let add_conditionally_owned_formal = + let is_owned_formal {Annot.class_name} = + (* [@InjectProp] allocates a fresh object to bind to the parameter *) + String.is_suffix ~suffix:Annotations.inject_prop class_name + in + let method_annotation = (Procdesc.get_attributes proc_desc).method_annotation in + let is_inject_prop = Annotations.ma_has_annotation_with method_annotation is_owned_formal in + fun acc formal formal_index -> + let ownership_value = + if is_inject_prop then OwnershipAbstractValue.owned + else OwnershipAbstractValue.make_owned_if formal_index + in + OwnershipDomain.add formal ownership_value acc + in if RacerDModels.should_analyze_proc tenv proc_name then - let formal_map = FormalMap.make proc_desc in let locks = if Procdesc.is_java_synchronized proc_desc then LockDomain.(acquire_lock bottom) else LockDomain.bottom @@ -447,57 +460,28 @@ let analyze_procedure {Callbacks.exe_env; summary} = then ThreadsDomain.AnyThread else ThreadsDomain.NoThread in - let add_owned_local acc (var_data : ProcAttributes.var_data) = - let pvar = Pvar.mk var_data.name proc_name in - let base = AccessPath.base_of_pvar pvar var_data.typ in - OwnershipDomain.add (AccessExpression.base base) OwnershipAbstractValue.owned acc - in - (* Add ownership to local variables. In cpp, stack-allocated local - variables cannot be raced on as every thread has its own stack. - More generally, we will never be confident that a race exists on a local/temp. *) - let own_locals = - List.fold ~f:add_owned_local (Procdesc.get_locals proc_desc) ~init:OwnershipDomain.empty - in - let is_owned_formal {Annot.class_name} = - (* @InjectProp allocates a fresh object to bind to the parameter *) - String.is_suffix ~suffix:Annotations.inject_prop class_name - in - let add_conditional_owned_formal acc (formal, formal_index) = - let ownership_value = - if Annotations.ma_has_annotation_with method_annotation is_owned_formal then - OwnershipAbstractValue.owned - else OwnershipAbstractValue.make_owned_if formal_index - in - OwnershipDomain.add (AccessExpression.base formal) ownership_value acc - in let ownership = - if RacerDModels.is_initializer tenv proc_name then - let add_owned_formal acc formal_index = - match FormalMap.get_formal_base formal_index formal_map with - | Some base -> - OwnershipDomain.add (AccessExpression.base base) OwnershipAbstractValue.owned acc - | None -> - acc - in - (* if a constructor is called via DI, all of its formals will be freshly allocated and - therefore owned. we assume that constructors annotated with @Inject will only be - called via DI or using fresh parameters. *) - if Annotations.pdesc_has_return_annot proc_desc Annotations.ia_is_inject then - List.mapi ~f:(fun i _ -> i) (Procdesc.get_formals proc_desc) - |> List.fold ~f:add_owned_formal ~init:own_locals - else - (* express that the constructor owns [this] *) - let init = add_owned_formal own_locals 0 in - FormalMap.get_formals_indexes formal_map - |> List.filter ~f:(fun (_, index) -> not (Int.equal 0 index)) - |> List.fold ~init ~f:add_conditional_owned_formal - else - (* add Owned(formal_index) predicates for each formal to indicate that each one is owned if - it is owned in the caller *) - List.fold ~init:own_locals ~f:add_conditional_owned_formal - (FormalMap.get_formals_indexes formal_map) + let is_initializer = RacerDModels.is_initializer tenv proc_name in + let is_injected = + is_initializer && Annotations.pdesc_has_return_annot proc_desc Annotations.ia_is_inject + in + Procdesc.get_formals proc_desc + |> List.foldi ~init:OwnershipDomain.empty ~f:(fun index acc (name, typ) -> + let base = + AccessPath.base_of_pvar (Pvar.mk name proc_name) typ |> AccessExpression.base + in + if is_injected then + (* if a constructor is called via DI, all of its formals will be freshly allocated and + therefore owned. we assume that constructors annotated with [@Inject] will only be + called via DI or using fresh parameters. *) + add_owned_formal acc base + else if is_initializer && Int.equal 0 index then + (* express that the constructor owns [this] *) + add_owned_formal acc base + else add_conditionally_owned_formal acc base index ) in let initial = {bottom with ownership; threads; locks} in + let formal_map = FormalMap.make proc_desc in let proc_data = ProcData.make summary tenv formal_map in Analyzer.compute_post proc_data ~initial |> Option.map ~f:(astate_to_summary proc_desc)