From e21a5ddda5084f7c0b1f8b02ae9785fe80e704e4 Mon Sep 17 00:00:00 2001 From: Mitya Lyubarskiy Date: Fri, 27 Sep 2019 08:07:47 -0700 Subject: [PATCH] [nullsafe] Move Initializer to a dedicated module Summary: Eradicate.ml is way too big to reason about. This diff is shallow, it does only the following: 1. Moves the module 2. Adds documentation in the header. 3. Exports two public methods as is 4. Adds corresponding params to all methods for values that were captured in the module-as-closure before Reviewed By: artempyanykh Differential Revision: D17600173 fbshipit-source-id: ba7981228 --- infer/src/nullsafe/Initializers.ml | 140 ++++++++++++++++++++++++++ infer/src/nullsafe/Initializers.mli | 36 +++++++ infer/src/nullsafe/eradicate.ml | 149 +++------------------------- 3 files changed, 188 insertions(+), 137 deletions(-) create mode 100644 infer/src/nullsafe/Initializers.ml create mode 100644 infer/src/nullsafe/Initializers.mli diff --git a/infer/src/nullsafe/Initializers.ml b/infer/src/nullsafe/Initializers.ml new file mode 100644 index 000000000..34af00e74 --- /dev/null +++ b/infer/src/nullsafe/Initializers.ml @@ -0,0 +1,140 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd + +type init = Typ.Procname.t * Procdesc.t + +let equal_class_opt = [%compare.equal: string option] + +let final_typestates initializers_current_class tenv typecheck_proc = + (* Get the private methods, from the same class, directly called by the initializers. *) + let get_private_called (initializers : init list) : init list = + let res = ref [] in + let do_proc (init_pn, init_pd) = + let filter callee_pn callee_attributes = + let is_private = + PredSymb.equal_access callee_attributes.ProcAttributes.access PredSymb.Private + in + let same_class = + let get_class_opt pn = + match pn with + | Typ.Procname.Java pn_java -> + Some (Typ.Procname.Java.get_class_name pn_java) + | _ -> + None + in + equal_class_opt (get_class_opt init_pn) (get_class_opt callee_pn) + in + is_private && same_class + in + let private_called = + PatternMatch.proc_calls (PatternMatch.lookup_attributes tenv) init_pd filter + in + let do_called (callee_pn, _) = + match Ondemand.get_proc_desc callee_pn with + | Some callee_pd -> + res := (callee_pn, callee_pd) :: !res + | None -> + () + in + List.iter ~f:do_called private_called + in + List.iter ~f:do_proc initializers ; !res + in + (* Get the initializers recursively called by computing a fixpoint. + Start from the initializers of the current class and the current procedure. *) + let initializers_recursive : init list = + let initializers_base_case = initializers_current_class in + let res = ref [] in + let seen = ref Typ.Procname.Set.empty in + let mark_seen (initializers : init list) : unit = + List.iter ~f:(fun (pn, _) -> seen := Typ.Procname.Set.add pn !seen) initializers ; + res := !res @ initializers + in + let rec fixpoint initializers_old = + let initializers_new = get_private_called initializers_old in + let initializers_new' = + List.filter ~f:(fun (pn, _) -> not (Typ.Procname.Set.mem pn !seen)) initializers_new + in + mark_seen initializers_new' ; + if initializers_new' <> [] then fixpoint initializers_new' + in + mark_seen initializers_base_case ; fixpoint initializers_base_case ; !res + in + (* Get the final typestates of all the initializers. *) + let final_typestates = ref [] in + let get_final_typestate (pname, pdesc) = + match typecheck_proc false pname pdesc None with + | _, Some final_typestate -> + final_typestates := (pname, final_typestate) :: !final_typestates + | _, None -> + () + in + List.iter ~f:get_final_typestate initializers_recursive ; + List.rev !final_typestates + + +let pname_and_pdescs_with tenv curr_pname get_procs_in_file f = + let res = ref [] in + let filter pname = + match PatternMatch.lookup_attributes tenv pname with + | Some proc_attributes -> + f (pname, proc_attributes) + | None -> + false + in + let do_proc pname = + if filter pname then + match Ondemand.get_proc_desc pname with + | Some pdesc -> + res := (pname, pdesc) :: !res + | None -> + () + in + List.iter ~f:do_proc (get_procs_in_file curr_pname) ; + List.rev !res + + +let get_class pn = + match pn with + | Typ.Procname.Java pn_java -> + Some (Typ.Procname.Java.get_class_name pn_java) + | _ -> + None + + +(** Typestates after the current procedure and all initializer procedures. *) +let final_initializer_typestates_lazy tenv curr_pname curr_pdesc get_procs_in_file typecheck_proc = + lazy + (let is_initializer proc_attributes = + PatternMatch.method_is_initializer tenv proc_attributes + || + let ia = + (Models.get_modelled_annotated_signature proc_attributes).AnnotatedSignature.ret + .ret_annotation_deprecated + in + Annotations.ia_is_initializer ia + in + let initializers_current_class = + pname_and_pdescs_with tenv curr_pname get_procs_in_file (function + | pname, proc_attributes -> + is_initializer proc_attributes + && equal_class_opt (get_class pname) (get_class curr_pname) ) + in + final_typestates ((curr_pname, curr_pdesc) :: initializers_current_class) tenv typecheck_proc) + + +(** Typestates after all constructors. *) +let final_constructor_typestates_lazy tenv curr_pname get_procs_in_file typecheck_proc = + lazy + (let constructors_current_class = + pname_and_pdescs_with tenv curr_pname get_procs_in_file (fun (pname, _) -> + Typ.Procname.is_constructor pname + && equal_class_opt (get_class pname) (get_class curr_pname) ) + in + final_typestates constructors_current_class tenv typecheck_proc) diff --git a/infer/src/nullsafe/Initializers.mli b/infer/src/nullsafe/Initializers.mli new file mode 100644 index 000000000..2e3645791 --- /dev/null +++ b/infer/src/nullsafe/Initializers.mli @@ -0,0 +1,36 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd + +(** Functionality for evaluating typestates after class initialization. + Nullsafe's notion of initialization augments Java's one in the following way: + 1. A method is considered "initializer" if it is either marked as @Initializer or is in + the list of known initializer methods (e.g. onCreate()). + 2. For each constructor, Nullsafe assumes all initializer methods will be called after + the constructor is called. (Nullsafe does not check if this assumption is indeed true). + 3. Nullsafe uses assumption 2, in order to check if class fields were initialized or not. + (a non-nullable field is considered not initialized if it is not initialized in at least + one constructor). + *) + +val final_initializer_typestates_lazy : + Tenv.t + -> Typ.Procname.t + -> Procdesc.t + -> (Typ.Procname.t -> Typ.Procname.t sexp_list) + -> (bool -> Typ.Procname.t -> Procdesc.t -> 'a sexp_option -> 'b * 'c sexp_option) + -> (Typ.Procname.t * 'c) sexp_list lazy_t +(** Typestates after the current constructor and all initializer procedures. *) + +val final_constructor_typestates_lazy : + Tenv.t + -> Typ.Procname.t + -> (Typ.Procname.t -> Typ.Procname.t sexp_list) + -> (bool -> Typ.Procname.t -> Procdesc.t -> 'a sexp_option -> 'b * 'c sexp_option) + -> (Typ.Procname.t * 'c) sexp_list lazy_t +(** Typestates after all constructors. *) diff --git a/infer/src/nullsafe/eradicate.ml b/infer/src/nullsafe/eradicate.ml index d8bc98185..1d3111932 100644 --- a/infer/src/nullsafe/eradicate.ml +++ b/infer/src/nullsafe/eradicate.ml @@ -145,139 +145,6 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct callback1 tenv find_canonical_duplicate calls_this' checks' idenv_pn pname pdesc ann_sig linereader loc in - let module Initializers = struct - type init = Typ.Procname.t * Procdesc.t - - let equal_class_opt = [%compare.equal: string option] - - let final_typestates initializers_current_class = - (* Get the private methods, from the same class, directly called by the initializers. *) - let get_private_called (initializers : init list) : init list = - let res = ref [] in - let do_proc (init_pn, init_pd) = - let filter callee_pn callee_attributes = - let is_private = - PredSymb.equal_access callee_attributes.ProcAttributes.access PredSymb.Private - in - let same_class = - let get_class_opt pn = - match pn with - | Typ.Procname.Java pn_java -> - Some (Typ.Procname.Java.get_class_name pn_java) - | _ -> - None - in - equal_class_opt (get_class_opt init_pn) (get_class_opt callee_pn) - in - is_private && same_class - in - let private_called = - PatternMatch.proc_calls (PatternMatch.lookup_attributes tenv) init_pd filter - in - let do_called (callee_pn, _) = - match Ondemand.get_proc_desc callee_pn with - | Some callee_pd -> - res := (callee_pn, callee_pd) :: !res - | None -> - () - in - List.iter ~f:do_called private_called - in - List.iter ~f:do_proc initializers ; !res - in - (* Get the initializers recursively called by computing a fixpoint. - Start from the initializers of the current class and the current procedure. *) - let initializers_recursive : init list = - let initializers_base_case = initializers_current_class in - let res = ref [] in - let seen = ref Typ.Procname.Set.empty in - let mark_seen (initializers : init list) : unit = - List.iter ~f:(fun (pn, _) -> seen := Typ.Procname.Set.add pn !seen) initializers ; - res := !res @ initializers - in - let rec fixpoint initializers_old = - let initializers_new = get_private_called initializers_old in - let initializers_new' = - List.filter ~f:(fun (pn, _) -> not (Typ.Procname.Set.mem pn !seen)) initializers_new - in - mark_seen initializers_new' ; - if initializers_new' <> [] then fixpoint initializers_new' - in - mark_seen initializers_base_case ; fixpoint initializers_base_case ; !res - in - (* Get the final typestates of all the initializers. *) - let final_typestates = ref [] in - let get_final_typestate (pname, pdesc) = - match typecheck_proc false pname pdesc None with - | _, Some final_typestate -> - final_typestates := (pname, final_typestate) :: !final_typestates - | _, None -> - () - in - List.iter ~f:get_final_typestate initializers_recursive ; - List.rev !final_typestates - - - let pname_and_pdescs_with f = - let res = ref [] in - let filter pname = - match PatternMatch.lookup_attributes tenv pname with - | Some proc_attributes -> - f (pname, proc_attributes) - | None -> - false - in - let do_proc pname = - if filter pname then - match Ondemand.get_proc_desc pname with - | Some pdesc -> - res := (pname, pdesc) :: !res - | None -> - () - in - List.iter ~f:do_proc (get_procs_in_file curr_pname) ; - List.rev !res - - - let get_class pn = - match pn with - | Typ.Procname.Java pn_java -> - Some (Typ.Procname.Java.get_class_name pn_java) - | _ -> - None - - - (** Typestates after the current procedure and all initializer procedures. *) - let final_initializer_typestates_lazy = - lazy - (let is_initializer proc_attributes = - PatternMatch.method_is_initializer tenv proc_attributes - || - let ia = - (Models.get_modelled_annotated_signature proc_attributes).AnnotatedSignature.ret - .ret_annotation_deprecated - in - Annotations.ia_is_initializer ia - in - let initializers_current_class = - pname_and_pdescs_with (function pname, proc_attributes -> - is_initializer proc_attributes - && equal_class_opt (get_class pname) (get_class curr_pname) ) - in - final_typestates ((curr_pname, curr_pdesc) :: initializers_current_class)) - - - (** Typestates after all constructors. *) - let final_constructor_typestates_lazy = - lazy - (let constructors_current_class = - pname_and_pdescs_with (fun (pname, _) -> - Typ.Procname.is_constructor pname - && equal_class_opt (get_class pname) (get_class curr_pname) ) - in - final_typestates constructors_current_class) - end - (* Initializers *) in let do_final_typestate typestate_opt calls_this = let do_typestate typestate = let start_node = Procdesc.get_start_node curr_pdesc in @@ -285,11 +152,19 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct (not calls_this) (* if 'this(...)' is called, no need to check initialization *) && checks.TypeCheck.eradicate - then + then ( + let final_initializer_typestates_lazy = + Initializers.final_initializer_typestates_lazy tenv curr_pname curr_pdesc + get_procs_in_file typecheck_proc + in + let final_constructor_typestates_lazy = + Initializers.final_constructor_typestates_lazy tenv curr_pname get_procs_in_file + typecheck_proc + in EradicateChecks.check_constructor_initialization tenv find_canonical_duplicate curr_pname - curr_pdesc start_node Initializers.final_initializer_typestates_lazy - Initializers.final_constructor_typestates_lazy proc_loc ; - if Config.eradicate_verbose then L.result "Final Typestate@\n%a@." TypeState.pp typestate + curr_pdesc start_node final_initializer_typestates_lazy + final_constructor_typestates_lazy proc_loc ; + if Config.eradicate_verbose then L.result "Final Typestate@\n%a@." TypeState.pp typestate ) in match typestate_opt with None -> () | Some typestate -> do_typestate typestate in