From 3b46c3b4da1d22cbc5cb4a08293fd859194c69ee Mon Sep 17 00:00:00 2001 From: Nikos Gorogiannis Date: Fri, 17 Apr 2020 01:42:37 -0700 Subject: [PATCH] [racerd] refactor analysis driver function Summary: Move state to summary conversion into the domain file, move a model matcher into the models file and simplify. Reviewed By: skcho Differential Revision: D21064351 fbshipit-source-id: bb5b07b6b --- infer/src/concurrency/RacerD.ml | 139 +++++++++++-------------- infer/src/concurrency/RacerDDomain.ml | 15 +++ infer/src/concurrency/RacerDDomain.mli | 2 + infer/src/concurrency/RacerDModels.ml | 4 + infer/src/concurrency/RacerDModels.mli | 3 + 5 files changed, 83 insertions(+), 80 deletions(-) diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index 6e146cf6d..b4c56e727 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -425,57 +425,53 @@ end module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (ProcCfg.Normal)) let analyze_procedure {Callbacks.exe_env; summary} = + let open RacerDDomain in let proc_desc = Summary.get_proc_desc summary in let proc_name = Summary.get_proc_name summary in let tenv = Exe_env.get_tenv exe_env proc_name in - let open RacerDModels in let open ConcurrencyModels in let method_annotation = (Procdesc.get_attributes proc_desc).method_annotation in - let is_initializer tenv proc_name = - Procname.is_constructor proc_name || FbThreadSafety.is_custom_init tenv proc_name - in - let open RacerDDomain in - if should_analyze_proc tenv proc_name then + if RacerDModels.should_analyze_proc tenv proc_name then let formal_map = FormalMap.make proc_desc in - let proc_data = ProcData.make summary tenv (FormalMap.make proc_desc) in - let initial = - let locks = - if Procdesc.is_java_synchronized proc_desc then LockDomain.(acquire_lock bottom) - else LockDomain.bottom - in - let threads = - if - runs_on_ui_thread ~attrs_of_pname tenv proc_name - || is_thread_confined_method tenv proc_name - then ThreadsDomain.AnyThreadButSelf - else if Procdesc.is_java_synchronized proc_desc || is_marked_thread_safe proc_name tenv 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 + let locks = + if Procdesc.is_java_synchronized proc_desc then LockDomain.(acquire_lock bottom) + else LockDomain.bottom + in + let threads = + if + runs_on_ui_thread ~attrs_of_pname tenv proc_name + || RacerDModels.is_thread_confined_method tenv proc_name + then ThreadsDomain.AnyThreadButSelf + else if + Procdesc.is_java_synchronized proc_desc || RacerDModels.is_marked_thread_safe proc_name tenv + 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 - if is_initializer tenv proc_name then + 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 -> @@ -483,46 +479,29 @@ let analyze_procedure {Callbacks.exe_env; summary} = | None -> acc in - let ownership = - (* 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 - in - {RacerDDomain.bottom with ownership; threads; locks} + (* 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 *) - let ownership = - List.fold ~init:own_locals ~f:add_conditional_owned_formal - (FormalMap.get_formals_indexes formal_map) - in - {RacerDDomain.bottom with ownership; threads; locks} + List.fold ~init:own_locals ~f:add_conditional_owned_formal + (FormalMap.get_formals_indexes formal_map) in - match Analyzer.compute_post proc_data ~initial with - | Some {threads; locks; accesses; ownership; attribute_map} -> - let return_var_exp = - AccessExpression.base - (Var.of_pvar (Pvar.get_ret_pvar proc_name), Procdesc.get_ret_type proc_desc) - in - let return_ownership = OwnershipDomain.get_owned return_var_exp ownership in - let return_attribute = AttributeMapDomain.find return_var_exp attribute_map in - let locks = - (* if method is [synchronized] released the lock once. *) - if Procdesc.is_java_synchronized proc_desc then LockDomain.release_lock locks else locks - in - let post = {threads; locks; accesses; return_ownership; return_attribute} in - Payload.update_summary post summary - | None -> - summary + let initial = {bottom with ownership; threads; locks} 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) + |> Option.value_map ~default:summary ~f:(fun post -> Payload.update_summary post summary) else Payload.update_summary empty_summary summary diff --git a/infer/src/concurrency/RacerDDomain.ml b/infer/src/concurrency/RacerDDomain.ml index a7175e8c0..6c7b5a625 100644 --- a/infer/src/concurrency/RacerDDomain.ml +++ b/infer/src/concurrency/RacerDDomain.ml @@ -546,3 +546,18 @@ let add_unannotated_call_access formals pname actuals loc (astate : t) = astate.threads Unowned loc in {astate with accesses= AccessDomain.add_opt snapshot astate.accesses} ) + + +let astate_to_summary proc_desc {threads; locks; accesses; ownership; attribute_map} = + let proc_name = Procdesc.get_proc_name proc_desc in + let return_var_exp = + AccessExpression.base + (Var.of_pvar (Pvar.get_ret_pvar proc_name), Procdesc.get_ret_type proc_desc) + in + let return_ownership = OwnershipDomain.get_owned return_var_exp ownership in + let return_attribute = AttributeMapDomain.find return_var_exp attribute_map in + let locks = + (* if method is [synchronized] released the lock once. *) + if Procdesc.is_java_synchronized proc_desc then LockDomain.release_lock locks else locks + in + {threads; locks; accesses; return_ownership; return_attribute} diff --git a/infer/src/concurrency/RacerDDomain.mli b/infer/src/concurrency/RacerDDomain.mli index 858654e78..595835e02 100644 --- a/infer/src/concurrency/RacerDDomain.mli +++ b/infer/src/concurrency/RacerDDomain.mli @@ -204,3 +204,5 @@ type summary = val empty_summary : summary val pp_summary : F.formatter -> summary -> unit + +val astate_to_summary : Procdesc.t -> t -> summary diff --git a/infer/src/concurrency/RacerDModels.ml b/infer/src/concurrency/RacerDModels.ml index 47037fdb3..06f63a88a 100644 --- a/infer/src/concurrency/RacerDModels.ml +++ b/infer/src/concurrency/RacerDModels.ml @@ -495,3 +495,7 @@ let is_builder_passthrough callee = false ) | _ -> false + + +let is_initializer tenv proc_name = + Procname.is_constructor proc_name || FbThreadSafety.is_custom_init tenv proc_name diff --git a/infer/src/concurrency/RacerDModels.mli b/infer/src/concurrency/RacerDModels.mli index 5c454b98e..bf217a3b8 100644 --- a/infer/src/concurrency/RacerDModels.mli +++ b/infer/src/concurrency/RacerDModels.mli @@ -61,3 +61,6 @@ val creates_builder : Procname.t -> bool val is_builder_passthrough : Procname.t -> bool (** is the callee a non-static [Builder] method returning the same type as its receiver *) + +val is_initializer : Tenv.t -> Procname.t -> bool +(** should the given procedure be treated as a constructor/initializer? *)