From 0f8c3e797420b4894499657c4643ea09e791ef5e Mon Sep 17 00:00:00 2001 From: Cristiano Calcagno Date: Wed, 23 Sep 2015 09:57:06 -0100 Subject: [PATCH] [eradicate][ondemand] Skeleton of on-demand analysis for Eradicate. --- infer/src/backend/ondemand.ml | 110 ++++++++++++++++++++++++++ infer/src/backend/ondemand.mli | 31 ++++++++ infer/src/backend/serialization.ml | 36 +++++++-- infer/src/backend/specs.ml | 9 ++- infer/src/checkers/annotations.ml | 12 ++- infer/src/checkers/annotations.mli | 10 ++- infer/src/checkers/eradicate.ml | 57 +++++++------ infer/src/checkers/eradicateChecks.ml | 103 ++++++++++++------------ infer/src/checkers/models.ml | 40 +--------- infer/src/checkers/typeCheck.ml | 1 + 10 files changed, 271 insertions(+), 138 deletions(-) create mode 100644 infer/src/backend/ondemand.ml create mode 100644 infer/src/backend/ondemand.mli diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml new file mode 100644 index 000000000..1cf72b22c --- /dev/null +++ b/infer/src/backend/ondemand.ml @@ -0,0 +1,110 @@ +(* + * Copyright (c) 2015 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + *) + +(** Module for on-demand analysis. *) + +module L = Logging +module F = Format +open Utils + +let trace = false + +let enabled () = false + +type analyze_proc = Procname.t -> unit + +type get_proc_desc = Procname.t -> Cfg.Procdesc.t option + +let analyze_proc_fun = ref None + +let set_analyze_proc (analyze_proc : analyze_proc) = + analyze_proc_fun := Some analyze_proc + +let unset_analyze_prop () = + analyze_proc_fun := None + +let do_analysis (get_proc_desc : get_proc_desc) curr_pname proc_name = + if trace then L.stderr "do_analysis %a -> %a@." Procname.pp curr_pname Procname.pp proc_name; + + let really_do_analysis analyze_proc proc_desc = + L.stderr "really_do_analysis@."; + + let preprocess () = + let attributes_opt = + Some (Cfg.Procdesc.get_attributes proc_desc) in + let call_graph = + let cg = Cg.create () in + Cg.add_node cg proc_name; + cg in + Specs.reset_summary call_graph proc_name attributes_opt; + Specs.set_status proc_name Specs.ACTIVE in + + let postprocess () = + let summary = Specs.get_summary_unsafe proc_name in + let summary' = + { summary with + Specs.status = Specs.INACTIVE; + timestamp = summary.Specs.timestamp + 1 } in + Specs.add_summary proc_name summary'; + Checkers.ST.store_summary proc_name in + + try + preprocess (); + analyze_proc proc_name; + postprocess () + with e -> + L.stderr "ONDEMAND EXCEPTION %a %s %s@." + Procname.pp proc_name + (Printexc.to_string e) + (Printexc.get_backtrace ()); + raise e in + + let currently_analyzed = + Specs.summary_exists proc_name && + Specs.is_active proc_name in + let already_analyzed = match Specs.get_summary proc_name with + | Some summary -> + Specs.get_timestamp summary > 0 + | None -> + false in + (* The procedure to be analyzed is in the same file as the current one. *) + let same_file proc_desc = + match get_proc_desc curr_pname with + | Some curr_pdesc -> + (Cfg.Procdesc.get_loc curr_pdesc).Location.file + = + (Cfg.Procdesc.get_loc proc_desc).Location.file + | None -> false in + + match !analyze_proc_fun, get_proc_desc proc_name with + | Some analyze_proc, Some proc_desc + when enabled () && + Cfg.Procdesc.is_defined proc_desc && (* we have the implementation *) + not currently_analyzed && (* avoid infinite loops *) + not already_analyzed && (* avoid re-analysis of the same procedure *) + same_file proc_desc (* clusters don't have enough info for other files *) -> + really_do_analysis analyze_proc proc_desc + | _ -> + if trace then L.stderr "skipping@." + + +(** Mark the return type @Nullable by modifying the spec. *) +let proc_add_return_nullable curr_pname = + let summary = Specs.get_summary_unsafe curr_pname in + let proc_attributes = Specs.get_attributes summary in + let method_annotation = proc_attributes.ProcAttributes.method_annotation in + let method_annotation' = Annotations.method_annotation_mark_return + Annotations.Nullable method_annotation in + let proc_attributes' = + { proc_attributes with + ProcAttributes.method_annotation = method_annotation' } in + let summary' = + { summary with + Specs.attributes = proc_attributes' } in + Specs.add_summary curr_pname summary' diff --git a/infer/src/backend/ondemand.mli b/infer/src/backend/ondemand.mli new file mode 100644 index 000000000..7df3fcc35 --- /dev/null +++ b/infer/src/backend/ondemand.mli @@ -0,0 +1,31 @@ +(* + * Copyright (c) 2015 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + *) + +(** Module for on-demand analysis. *) + +type analyze_proc = Procname.t -> unit + +type get_proc_desc = Procname.t -> Cfg.Procdesc.t option + +(** do_analysis get_proc_desc curr_pname proc_name + performs an on-demand analysis of proc_name + triggered during the analysis of curr_pname. *) +val do_analysis : get_proc_desc -> Procname.t -> Procname.t -> unit + +(** Check if on-demand is currently active. *) +val enabled : unit -> bool + +(** Mark the return type @Nullable by modifying the spec. *) +val proc_add_return_nullable : Procname.t -> unit + +(** Set the function to be used to perform on-demand analysis. *) +val set_analyze_proc : analyze_proc -> unit + +(** Unset the function to be used to perform on-demand analysis. *) +val unset_analyze_prop : unit -> unit diff --git a/infer/src/backend/serialization.ml b/infer/src/backend/serialization.ml index f62a70d6e..5dfa8d859 100644 --- a/infer/src/backend/serialization.ml +++ b/infer/src/backend/serialization.ml @@ -32,6 +32,19 @@ let generate_keys () = gen (), gen (), gen (), gen (), gen (), gen () +(** Retry the function while an exception filtered is thrown, + or until the timeout in seconds expires. *) +let retry_exception timeout catch_exn f x = + let init_time = Unix.gettimeofday () in + let expired () = + Unix.gettimeofday () -. init_time >= timeout in + let rec retry () = + try f x with + | e when catch_exn e && not (expired ()) -> + retry () in + retry () + + let create_serializer (key : key) : 'a serializer = let match_data ((key': key), (version': int), (value: 'a)) source_msg = if key <> key' then @@ -50,13 +63,22 @@ let create_serializer (key : key) : 'a serializer = match_data (Marshal.from_string str 0) "string" with Sys_error s -> None in let from_file (_fname : DB.filename) : 'a option = - try - let fname = DB.filename_to_string _fname in - let inc = open_in_bin fname in - let value_option = match_data (Marshal.from_channel inc) fname in - close_in inc; - value_option - with Sys_error s -> None in + let read () = + try + let fname = DB.filename_to_string _fname in + let inc = open_in_bin fname in + let value_option = match_data (Marshal.from_channel inc) fname in + close_in inc; + value_option + with + | Sys_error s -> None in + let timeout = 1.0 in + let catch_exn = function + | End_of_file -> true + | _ -> false in + (* Retry to read for 1 second in case of end of file, *) + (* which indicates that another process is writing the same file. *) + retry_exception timeout catch_exn read () in let to_file (fname : DB.filename) (value : 'a) = let outc = open_out_bin (DB.filename_to_string fname) in Marshal.to_channel outc (key, version, value) []; diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml index 44cd306f5..8c5b854b2 100644 --- a/infer/src/backend/specs.ml +++ b/infer/src/backend/specs.ml @@ -640,18 +640,19 @@ let proc_resolve_attributes get_proc_desc proc_name = | Some summary -> Some summary.attributes | None -> None in - match from_proc_desc () with + match from_specs () with | Some attributes -> if attributes.ProcAttributes.is_defined then Some attributes else begin - match from_specs () with + match from_proc_desc () with | Some attributes' -> Some attributes' - | None -> Some attributes + | None -> + Some attributes end | None -> - from_specs () + from_proc_desc () (** Like proc_resolve_attributes but start from a proc_desc. *) let pdesc_resolve_attributes proc_desc = diff --git a/infer/src/checkers/annotations.ml b/infer/src/checkers/annotations.ml index 99be090a1..1b0dcb49a 100644 --- a/infer/src/checkers/annotations.ml +++ b/infer/src/checkers/annotations.ml @@ -155,8 +155,6 @@ let ia_is ann ia = match ann with | Nullable -> ia_is_nullable ia | Present -> ia_is_present ia -type get_method_annotation = Procname.t -> Cfg.Procdesc.t -> Sil.method_annotation - (** Get a method signature with annotations from a proc_attributes. *) let get_annotated_signature proc_attributes : annotated_signature = @@ -270,13 +268,19 @@ let annotated_signature_mark proc_name ann asig (b, bs) = { ret = ret'; params = params'} (** Mark the return of the annotated signature with the given annotation. *) -let annotated_signature_mark_return proc_name ann asig = +let annotated_signature_mark_return ann asig = let ia, t = asig.ret in let ret' = mark_ia ann ia true, t in { asig with ret = ret'} (** Mark the return of the annotated signature @Strict. *) -let annotated_signature_mark_return_strict proc_name asig = +let annotated_signature_mark_return_strict asig = let ia, t = asig.ret in let ret' = mark_ia_strict ia true, t in { asig with ret = ret'} + +(** Mark the return of the method_annotation with the given annotation. *) +let method_annotation_mark_return ann method_annotation = + let ia_ret, params = method_annotation in + let ia_ret' = mark_ia ann ia_ret true in + ia_ret', params diff --git a/infer/src/checkers/annotations.mli b/infer/src/checkers/annotations.mli index b071158d4..aee1b94e5 100644 --- a/infer/src/checkers/annotations.mli +++ b/infer/src/checkers/annotations.mli @@ -34,16 +34,14 @@ val annotated_signature_mark : (** Mark the return of the annotated signature with the given annotation. *) val annotated_signature_mark_return : - Procname.t -> annotation -> annotated_signature -> annotated_signature + annotation -> annotated_signature -> annotated_signature (** Mark the return of the annotated signature @Strict. *) val annotated_signature_mark_return_strict : - Procname.t -> annotated_signature -> annotated_signature + annotated_signature -> annotated_signature val equal : annotated_signature -> annotated_signature -> bool -type get_method_annotation = Procname.t -> Cfg.Procdesc.t -> Sil.method_annotation - (** Get a method signature with annotations from a proc_attributes. *) val get_annotated_signature : ProcAttributes.t -> annotated_signature @@ -76,6 +74,10 @@ val ma_has_annotation_with : Sil.method_annotation -> (Sil.annotation -> bool) - val ma_iter : (Sil.annotation -> unit) -> Sil.method_annotation -> unit +(** Mark the return of the method_annotation with the given annotation. *) +val method_annotation_mark_return : + annotation -> Sil.method_annotation -> Sil.method_annotation + (** Add the annotation to the item_annotation. *) val mk_ia : annotation -> Sil.item_annotation -> Sil.item_annotation diff --git a/infer/src/checkers/eradicate.ml b/infer/src/checkers/eradicate.ml index 1525a3c19..fda2e434a 100644 --- a/infer/src/checkers/eradicate.ml +++ b/infer/src/checkers/eradicate.ml @@ -71,7 +71,8 @@ struct let callback1 find_canonical_duplicate calls_this checks get_proc_desc idenv tenv curr_pname - curr_pdesc annotated_signature linereader proc_loc : bool * 'a TypeState.t option = + curr_pdesc annotated_signature linereader proc_loc + : bool * Extension.extension TypeState.t option = let mk_pvar s = Sil.mk_pvar (Mangled.from_string s) curr_pname in let add_formal typestate (s, ia, typ) = let pvar = mk_pvar s in @@ -154,7 +155,16 @@ struct try Cfg.NodeSet.min_elt duplicate_nodes with | Not_found -> node in - let typecheck_proc do_checks idenv_pn pname pdesc ann_sig loc = + let typecheck_proc do_checks pname pdesc proc_details_opt = + let ann_sig, loc, idenv_pn = match proc_details_opt with + | Some (ann_sig, loc, idenv_pn) -> + (ann_sig, loc, idenv_pn) + | None -> + let ann_sig = + Models.get_modelled_annotated_signature (Cfg.Procdesc.get_attributes pdesc) in + let loc = Cfg.Procdesc.get_loc pdesc in + let idenv_pn = Idenv.create_from_idenv idenv pdesc in + (ann_sig, loc, idenv_pn) in let checks', calls_this' = if do_checks then checks, calls_this else @@ -215,11 +225,7 @@ struct (** Get the final typestates of all the initializers. *) let final_typestates = ref [] in let get_final_typestate (pname, pdesc) = - let ann_sig = - Models.get_modelled_annotated_signature (Cfg.Procdesc.get_attributes pdesc) in - let loc = Cfg.Procdesc.get_loc pdesc in - let idenv_pn = Idenv.create_from_idenv idenv pdesc in - match typecheck_proc false idenv_pn pname pdesc ann_sig loc with + match typecheck_proc false pname pdesc None with | _, Some final_typestate -> final_typestates := (pname, final_typestate) :: !final_typestates | _, None -> () in @@ -277,7 +283,6 @@ struct curr_pname curr_pdesc start_node - typestate Initializers.final_initializer_typestates_lazy Initializers.final_constructor_typestates_lazy proc_loc @@ -292,7 +297,7 @@ struct TypeErr.reset (); let calls_this, final_typestate_opt = - typecheck_proc true idenv curr_pname curr_pdesc annotated_signature proc_loc in + typecheck_proc true curr_pname curr_pdesc (Some (annotated_signature, proc_loc, idenv)) in do_final_typestate final_typestate_opt calls_this; if checks.TypeCheck.eradicate then EradicateChecks.check_overridden_annotations @@ -315,19 +320,7 @@ struct begin let annotated_signature = Models.get_modelled_annotated_signature (Specs.pdesc_resolve_attributes proc_desc) in - if (Specs.pdesc_resolve_attributes proc_desc).ProcAttributes.is_abstract then - begin - if Models.infer_library_return && - EradicateChecks.classify_procedure (Cfg.Procdesc.get_attributes proc_desc) = "L" - then - (let ret_is_nullable = (* get the existing annotation *) - let ia, _ = annotated_signature.Annotations.ret in - Annotations.ia_is_nullable ia in - EradicateChecks.pp_inferred_return_annotation ret_is_nullable proc_name); - Some annotated_signature - end - else - Some annotated_signature + Some annotated_signature end in match filter_special_cases () with | None -> () @@ -375,26 +368,30 @@ module Main = Build(EmptyExtension) (** Eradicate checker for Java @Nullable annotations. *) -let callback_eradicate all_procs get_proc_desc idenv tenv proc_name1 proc_desc1 = +let callback_eradicate all_procs get_proc_desc idenv tenv proc_name proc_desc = let checks = { TypeCheck.eradicate = true; check_extension = false; check_ret_type = []; } in - Main.callback checks all_procs get_proc_desc idenv tenv proc_name1 proc_desc1 + let _ondemand pname = + match get_proc_desc pname with + | None -> () + | Some pdesc -> + let idenv_pname = Idenv.create_from_idenv idenv pdesc in + Main.callback checks all_procs get_proc_desc idenv_pname tenv pname pdesc in + Ondemand.set_analyze_proc _ondemand; + Main.callback checks all_procs get_proc_desc idenv tenv proc_name proc_desc; + Ondemand.unset_analyze_prop () (** Call the given check_return_type at the end of every procedure. *) let callback_check_return_type check_return_type all_procs - get_proc_desc idenv tenv proc_name1 proc_desc1 = + get_proc_desc idenv tenv proc_name proc_desc = let checks = { TypeCheck.eradicate = false; check_extension = false; check_ret_type = [check_return_type]; } in - Main.callback checks all_procs get_proc_desc idenv tenv proc_name1 proc_desc1 - -(** Export the ability to add nullable annotations. *) -let field_add_nullable_annotation fieldname = - Models.Inference.field_add_nullable_annotation fieldname + Main.callback checks all_procs get_proc_desc idenv tenv proc_name proc_desc diff --git a/infer/src/checkers/eradicateChecks.ml b/infer/src/checkers/eradicateChecks.ml index 3156ea98b..7fa35b1ed 100644 --- a/infer/src/checkers/eradicateChecks.ml +++ b/infer/src/checkers/eradicateChecks.ml @@ -60,18 +60,12 @@ let classify_procedure proc_attributes = let unique_id = Procname.to_unique_id pn in let classification = if Models.is_modelled_nullable pn then "M" (* modelled *) - else if Models.is_ret_library pn then "R" (* return library *) else if Specs.proc_is_library proc_attributes then "L" (* library *) else if not proc_attributes.ProcAttributes.is_defined then "S" (* skip *) else if string_is_prefix "com.facebook" unique_id then "F" (* FB *) else "?" in classification -let pp_inferred_return_annotation is_nullable proc_name = - L.stdout "(*InferredLibraryReturnAnnotation*) %5b, \"%s\";@." - is_nullable - (Procname.to_unique_id proc_name) - let is_virtual = function | ("this", _, _):: _ -> true @@ -248,7 +242,6 @@ let check_constructor_initialization curr_pname curr_pdesc start_node - final_typestate final_initializer_typestates final_constructor_typestates loc: unit = @@ -339,52 +332,56 @@ let check_return_annotation let ret_annotated_nullable = Annotations.ia_is_nullable ret_ia in let ret_annotated_present = Annotations.ia_is_present ret_ia in let ret_annotated_nonnull = Annotations.ia_is_nonnull ret_ia in - let return_not_nullable = - match ret_range with - | Some (_, final_ta, _) -> - let final_nullable = TypeAnnotation.get_value Annotations.Nullable final_ta in - let final_present = TypeAnnotation.get_value Annotations.Present final_ta in - let origin_descr = TypeAnnotation.descr_origin final_ta in - let return_not_nullable = - final_nullable && - not ret_annotated_nullable && - not ret_implicitly_nullable && - not (return_nonnull_silent && ret_annotated_nonnull) in - let return_value_not_present = - activate_optional_present && - not final_present && - ret_annotated_present in - let return_over_annotated = - not final_nullable && - ret_annotated_nullable && - activate_return_over_annotated in - if return_not_nullable || return_value_not_present then - begin - let ann = - if return_not_nullable then Annotations.Nullable else Annotations.Present in - if Models.Inference.enabled then Models.Inference.proc_add_return_nullable curr_pname; - report_error - find_canonical_duplicate - exit_node - (TypeErr.Return_annotation_inconsistent (ann, curr_pname, origin_descr)) - None - loc curr_pname - end; - if return_over_annotated then - begin - report_error - find_canonical_duplicate - exit_node - (TypeErr.Return_over_annotated curr_pname) - None - loc curr_pname - end; - return_not_nullable - | _ -> - false in - if Models.infer_library_return && - classify_procedure (Cfg.Procdesc.get_attributes curr_pdesc) = "L" - then pp_inferred_return_annotation return_not_nullable curr_pname + match ret_range with + | Some (_, final_ta, _) -> + let final_nullable = TypeAnnotation.get_value Annotations.Nullable final_ta in + let final_present = TypeAnnotation.get_value Annotations.Present final_ta in + let origin_descr = TypeAnnotation.descr_origin final_ta in + let return_not_nullable = + final_nullable && + not ret_annotated_nullable && + not ret_implicitly_nullable && + not (return_nonnull_silent && ret_annotated_nonnull) in + let return_value_not_present = + activate_optional_present && + not final_present && + ret_annotated_present in + let return_over_annotated = + not final_nullable && + ret_annotated_nullable && + activate_return_over_annotated in + + if return_not_nullable && Models.Inference.enabled then + Models.Inference.proc_add_return_nullable curr_pname; + + if return_not_nullable && Ondemand.enabled () then + Ondemand.proc_add_return_nullable curr_pname; + + if return_not_nullable || return_value_not_present then + begin + let ann = + if return_not_nullable then Annotations.Nullable else Annotations.Present in + + + report_error + find_canonical_duplicate + exit_node + (TypeErr.Return_annotation_inconsistent (ann, curr_pname, origin_descr)) + None + loc curr_pname + end; + + if return_over_annotated then + begin + report_error + find_canonical_duplicate + exit_node + (TypeErr.Return_over_annotated curr_pname) + None + loc curr_pname + end + | None -> + () (** Check the receiver of a virtual call. *) let check_call_receiver diff --git a/infer/src/checkers/models.ml b/infer/src/checkers/models.ml index 1b3b26c54..0ff24e89b 100644 --- a/infer/src/checkers/models.ml +++ b/infer/src/checkers/models.ml @@ -13,16 +13,9 @@ module L = Logging (** Module for standard library models. *) -(* use library of inferred return annotations *) -let use_library = false - (* use model annotations for library functions *) let use_models = true -(* libary functions: infer nullable annotation of return type *) -let infer_library_return = Config.from_env_variable "ERADICATE_LIBRARY" - - (** Module for inference of parameter and return annotations. *) module Inference = struct let enabled = false @@ -105,16 +98,6 @@ let table_has_procedure table proc_name = try ignore (Hashtbl.find table proc_id); true with Not_found -> false -type table_t = (string, bool) Hashtbl.t - -(* precomputed marshalled table of inferred return annotations. *) -let ret_library_table : table_t Lazy.t = - lazy (Hashtbl.create 1) -(* -lazy (Marshal.from_string Eradicate_library.marshalled_library_table 0) -*) - - (** Return the annotated signature of the procedure, taking into account models. *) let get_modelled_annotated_signature proc_attributes = let proc_name = proc_attributes.ProcAttributes.proc_name in @@ -131,17 +114,10 @@ let get_modelled_annotated_signature proc_attributes = Annotations.annotated_signature_mark proc_name Annotations.Nullable ann_sig mark in let infer_return ann_sig = let mark_r = - let from_library = - if use_library then - try - Hashtbl.find (Lazy.force ret_library_table) proc_id - with Not_found -> false - else false in - let from_inference = Inference.enabled && - Inference.proc_return_is_marked proc_name in - from_library || from_inference in + Inference.enabled && + Inference.proc_return_is_marked proc_name in if mark_r - then Annotations.annotated_signature_mark_return proc_name Annotations.Nullable ann_sig + then Annotations.annotated_signature_mark_return Annotations.Nullable ann_sig else ann_sig in let lookup_models_nullable ann_sig = if use_models then @@ -163,7 +139,7 @@ let get_modelled_annotated_signature proc_attributes = if use_models && Hashtbl.mem annotated_table_strict proc_id then - Annotations.annotated_signature_mark_return_strict proc_name ann_sig + Annotations.annotated_signature_mark_return_strict ann_sig else ann_sig in @@ -183,14 +159,6 @@ let is_modelled_nullable proc_name = with Not_found -> false else false -(** Return true when the procedure belongs to the library of inferred return annotations. *) -let is_ret_library proc_name = - if use_library && not infer_library_return then - let proc_id = Procname.to_unique_id proc_name in - try ignore (Hashtbl.find (Lazy.force ret_library_table) proc_id); true - with Not_found -> false - else false - (** Check if the procedure is one of the known Preconditions.checkNotNull. *) let is_check_not_null proc_name = table_has_procedure check_not_null_table proc_name diff --git a/infer/src/checkers/typeCheck.ml b/infer/src/checkers/typeCheck.ml index a2c6a6d76..a0cbc46a6 100644 --- a/infer/src/checkers/typeCheck.ml +++ b/infer/src/checkers/typeCheck.ml @@ -561,6 +561,7 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc typestate (* skip othe builtins *) | Sil.Call (ret_ids, Sil.Const (Sil.Cfun callee_pname), _etl, loc, cflags) when get_proc_desc callee_pname <> None -> + Ondemand.do_analysis get_proc_desc curr_pname callee_pname; let callee_attributes = match get_proc_desc callee_pname with | Some pdesc ->