pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[nullsafe] Move Initializer to a dedicated module

Browse Source 
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
master
Mitya Lyubarskiy 5 years ago committed by Facebook Github Bot
parent c472e95d72
commit e21a5ddda5
3 changed files with 188 additions and 137 deletions
Show Stats Download Patch File Download Diff File

140
infer/src/nullsafe/Initializers.ml
Unescape View File

@ -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)

36
infer/src/nullsafe/Initializers.mli
Unescape View File

@ -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. *)

149
infer/src/nullsafe/eradicate.ml
Unescape View File

@ -145,139 +145,6 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct
callback1 tenv find_canonical_duplicate calls_this' checks' idenv_pn pname pdesc ann_sig callback1 tenv find_canonical_duplicate calls_this' checks' idenv_pn pname pdesc ann_sig
linereader loc linereader loc
in 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_final_typestate typestate_opt calls_this =
let do_typestate typestate = let do_typestate typestate =
let start_node = Procdesc.get_start_node curr_pdesc in let start_node = Procdesc.get_start_node curr_pdesc in
@ -285,11 +152,19 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct
(not calls_this) (not calls_this)
(* if 'this(...)' is called, no need to check initialization *) (* if 'this(...)' is called, no need to check initialization *)
&& checks.TypeCheck.eradicate && 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 EradicateChecks.check_constructor_initialization tenv find_canonical_duplicate curr_pname
curr_pdesc start_node Initializers.final_initializer_typestates_lazy curr_pdesc start_node final_initializer_typestates_lazy
Initializers.final_constructor_typestates_lazy proc_loc ; final_constructor_typestates_lazy proc_loc ;
if Config.eradicate_verbose then L.result "Final Typestate@\n%a@." TypeState.pp typestate if Config.eradicate_verbose then L.result "Final Typestate@\n%a@." TypeState.pp typestate )
in in
match typestate_opt with None -> () | Some typestate -> do_typestate typestate match typestate_opt with None -> () | Some typestate -> do_typestate typestate
in in

Write Preview
Loading…
Cancel
Save