From 15943b1ea1c8a42ec743164fabe61c46acd36fa7 Mon Sep 17 00:00:00 2001 From: Nikos Gorogiannis Date: Fri, 4 Dec 2020 02:34:00 -0800 Subject: [PATCH] [biabduction] don't specialise models Summary: Models are currently not specialised*. Remove the ability entirely, to allow further changes. *this is proved by the fact that Infer doesn't crash, which it would if it tried to specialise models, because their procdesc is the already pre-analysed one, and pre-analysing twice a procdesc will crash. Reviewed By: jvillard Differential Revision: D25027698 fbshipit-source-id: 76ae5fa0d --- infer/src/IR/Attributes.ml | 15 ------- infer/src/IR/Attributes.mli | 4 -- infer/src/IR/SpecializeProcdesc.ml | 21 +-------- infer/src/IR/SpecializeProcdesc.mli | 3 +- infer/src/biabduction/SymExec.ml | 66 +++++++++++++++-------------- 5 files changed, 38 insertions(+), 71 deletions(-) diff --git a/infer/src/IR/Attributes.ml b/infer/src/IR/Attributes.ml index 07b974a36..af108d9ff 100644 --- a/infer/src/IR/Attributes.ml +++ b/infer/src/IR/Attributes.ml @@ -84,21 +84,6 @@ let store ~proc_desc (attr : ProcAttributes.t) = ~callees -let find_file_capturing_procedure pname = - Option.map (load pname) ~f:(fun proc_attributes -> - let source_file = proc_attributes.ProcAttributes.translation_unit in - let origin = - (* Procedure coming from include files if it has different location than the file where it - was captured. *) - match SourceFile.compare source_file proc_attributes.ProcAttributes.loc.file <> 0 with - | true -> - `Include - | false -> - `Source - in - (source_file, origin) ) - - let pp_attributes_kind f = function | ProcUndefined -> F.pp_print_string f "" diff --git a/infer/src/IR/Attributes.mli b/infer/src/IR/Attributes.mli index 7c3e50132..c38d5edb0 100644 --- a/infer/src/IR/Attributes.mli +++ b/infer/src/IR/Attributes.mli @@ -19,8 +19,4 @@ val store : proc_desc:Procdesc.t option -> ProcAttributes.t -> unit val load : Procname.t -> ProcAttributes.t option (** Load the attributes for the procedure from the attributes database. *) -val find_file_capturing_procedure : Procname.t -> (SourceFile.t * [`Include | `Source]) option -(** Find the file where the procedure was captured, if a cfg for that file exists. Return also a - boolean indicating whether the procedure is defined in an include file. *) - val pp_attributes_kind : Format.formatter -> attributes_kind -> unit diff --git a/infer/src/IR/SpecializeProcdesc.ml b/infer/src/IR/SpecializeProcdesc.ml index fdaeb93d9..25873991e 100644 --- a/infer/src/IR/SpecializeProcdesc.ml +++ b/infer/src/IR/SpecializeProcdesc.ml @@ -135,7 +135,7 @@ exception UnmatchedParameters typ) where name is a parameter. The resulting proc desc is isomorphic but all the type of the parameters are replaced in the instructions according to the list. The virtual calls are also replaced to match the parameter types *) -let with_formals_types ?(has_clang_model = false) callee_pdesc resolved_pname args = +let with_formals_types callee_pdesc resolved_pname args = let callee_attributes = Procdesc.get_attributes callee_pdesc in let resolved_params, substitutions = match @@ -158,28 +158,11 @@ let with_formals_types ?(has_clang_model = false) callee_pdesc resolved_pname ar (List.length args) ; raise UnmatchedParameters in - let translation_unit = - (* If it is a model, and we are using the procdesc stored in the summary, the default translation unit - won't be useful because we don't store that tenv, so we aim to find the source file of the caller to - use its tenv. *) - if has_clang_model then - let pname = Procdesc.get_proc_name callee_pdesc in - match Attributes.find_file_capturing_procedure pname with - | Some (source_file, _) -> - source_file - | None -> - Logging.die InternalError - "specialize_types should only be called with defined procedures, but we cannot find \ - the captured file of procname %a" - Procname.pp pname - else callee_attributes.translation_unit - in let resolved_attributes = { callee_attributes with formals= List.rev resolved_params ; proc_name= resolved_pname - ; is_specialized= true - ; translation_unit } + ; is_specialized= true } in let resolved_proc_desc = Procdesc.from_proc_attributes resolved_attributes in let resolved_proc_desc = with_formals_types_proc callee_pdesc resolved_proc_desc substitutions in diff --git a/infer/src/IR/SpecializeProcdesc.mli b/infer/src/IR/SpecializeProcdesc.mli index 0eda6e9b3..670c47f91 100644 --- a/infer/src/IR/SpecializeProcdesc.mli +++ b/infer/src/IR/SpecializeProcdesc.mli @@ -9,8 +9,7 @@ open! IStd exception UnmatchedParameters -val with_formals_types : - ?has_clang_model:bool -> Procdesc.t -> Procname.t -> (Exp.t * Typ.t) list -> Procdesc.t +val with_formals_types : Procdesc.t -> Procname.t -> (Exp.t * Typ.t) list -> Procdesc.t (** Creates a copy of a procedure description and a list of type substitutions of the form (name, typ) where name is a parameter. The resulting procdesc is isomorphic but all the type of the parameters are replaced in the instructions according to the list. The virtual calls are also diff --git a/infer/src/biabduction/SymExec.ml b/infer/src/biabduction/SymExec.ml index d712bf551..53890c306 100644 --- a/infer/src/biabduction/SymExec.ml +++ b/infer/src/biabduction/SymExec.ml @@ -587,36 +587,39 @@ type resolve_and_analyze_result = analyzed *) let resolve_and_analyze {InterproceduralAnalysis.analyze_dependency; analyze_pdesc_dependency; proc_desc; tenv} - ?(has_clang_model = false) prop args callee_proc_name call_flags : resolve_and_analyze_result = - (* TODO (#15748878): Fix conflict with method overloading by encoding in the procedure name - whether the method is defined or generated by the specialization *) - let analyze_ondemand resolved_pname = - if Procname.equal resolved_pname callee_proc_name then - (AnalysisCallbacks.get_proc_desc callee_proc_name, analyze_dependency callee_proc_name) - else - (* Create the type specialized procedure description and analyze it directly *) - let resolved_proc_desc_option = - match AnalysisCallbacks.get_proc_desc resolved_pname with - | Some _ as resolved_proc_desc -> - resolved_proc_desc - | None -> - let procdesc_opt = AnalysisCallbacks.get_proc_desc callee_proc_name in - Option.map procdesc_opt ~f:(fun callee_proc_desc -> - (* It is possible that the types of the arguments are not as precise as the type of - the objects in the heap, so we should update them to get the best results. *) - let resolved_args = resolve_args prop args in - SpecializeProcdesc.with_formals_types ~has_clang_model callee_proc_desc - resolved_pname resolved_args ) - in - ( resolved_proc_desc_option - , Option.bind resolved_proc_desc_option ~f:(fun pdesc -> - analyze_pdesc_dependency pdesc |> Option.map ~f:(fun summary -> (pdesc, summary)) ) ) - in - let resolved_pname = - resolve_pname ~caller_pdesc:proc_desc tenv prop args callee_proc_name call_flags - in - let resolved_procdesc_opt, resolved_summary_opt = analyze_ondemand resolved_pname in - {resolved_pname; resolved_procdesc_opt; resolved_summary_opt} + ~has_clang_model prop args callee_proc_name call_flags : resolve_and_analyze_result = + if has_clang_model then + {resolved_pname= callee_proc_name; resolved_procdesc_opt= None; resolved_summary_opt= None} + else + (* TODO (#15748878): Fix conflict with method overloading by encoding in the procedure name + whether the method is defined or generated by the specialization *) + let analyze_ondemand resolved_pname = + if Procname.equal resolved_pname callee_proc_name then + (AnalysisCallbacks.get_proc_desc callee_proc_name, analyze_dependency callee_proc_name) + else + (* Create the type specialized procedure description and analyze it directly *) + let resolved_proc_desc_option = + match AnalysisCallbacks.get_proc_desc resolved_pname with + | Some _ as resolved_proc_desc -> + resolved_proc_desc + | None -> + let procdesc_opt = AnalysisCallbacks.get_proc_desc callee_proc_name in + Option.map procdesc_opt ~f:(fun callee_proc_desc -> + (* It is possible that the types of the arguments are not as precise as the type of + the objects in the heap, so we should update them to get the best results. *) + let resolved_args = resolve_args prop args in + SpecializeProcdesc.with_formals_types callee_proc_desc resolved_pname + resolved_args ) + in + ( resolved_proc_desc_option + , Option.bind resolved_proc_desc_option ~f:(fun pdesc -> + analyze_pdesc_dependency pdesc |> Option.map ~f:(fun summary -> (pdesc, summary)) ) ) + in + let resolved_pname = + resolve_pname ~caller_pdesc:proc_desc tenv prop args callee_proc_name call_flags + in + let resolved_procdesc_opt, resolved_summary_opt = analyze_ondemand resolved_pname in + {resolved_pname; resolved_procdesc_opt; resolved_summary_opt} (** recognize calls to the constructor java.net.URL and splits the argument string to be only the @@ -1158,7 +1161,8 @@ let rec sym_exec norm_args in let resolve_and_analyze_result = - resolve_and_analyze analysis_data norm_prop norm_args callee_pname call_flags + resolve_and_analyze ~has_clang_model:false analysis_data norm_prop norm_args + callee_pname call_flags in let resolved_pname = resolve_and_analyze_result.resolved_pname in match resolve_and_analyze_result.resolved_summary_opt with