diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 1fab85e0c..28f052c9d 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -345,7 +345,6 @@ end module Analyzer = AbstractInterpreter.Make (ProcCfg.Normal) (TransferFunctions) -module Interprocedural = AbstractInterpreter.Interprocedural (Summary) module CFG = Analyzer.TransferFunctions.CFG module Sem = BufferOverrunSemantics.Make (CFG) @@ -539,21 +538,12 @@ let print_summary : Typ.Procname.t -> Dom.Summary.t -> unit Dom.Summary.pp_summary s let checker : Callbacks.proc_callback_args -> Specs.summary - = fun ({ proc_desc; tenv; summary } as callback) -> + = fun { proc_desc; tenv; summary; get_proc_desc; } -> let proc_name = Specs.get_proc_name summary in - let make_extras _ = callback.get_proc_desc in - let updated_summary : Specs.summary = - Interprocedural.compute_summary - ~compute_post - ~make_extras - proc_desc - tenv - summary in - let post = - updated_summary.payload.buffer_overrun in - begin - match post with - | Some s when Config.bo_debug >= 1 -> print_summary proc_name s - | _ -> () - end; - updated_summary + let proc_data = ProcData.make proc_desc tenv get_proc_desc in + match compute_post proc_data with + | Some post -> + if Config.bo_debug >= 1 then print_summary proc_name post; + Summary.update_summary post summary + | None -> + summary diff --git a/infer/src/checkers/AbstractInterpreter.ml b/infer/src/checkers/AbstractInterpreter.ml index 4e4625532..35462f684 100644 --- a/infer/src/checkers/AbstractInterpreter.ml +++ b/infer/src/checkers/AbstractInterpreter.ml @@ -155,16 +155,6 @@ module MakeNoCFG extract_post (CFG.id (CFG.exit_node cfg)) inv_map end -module Interprocedural (Summ : Summary.S) = struct - - let compute_summary ~compute_post ~make_extras proc_desc tenv summary = - match compute_post (ProcData.make proc_desc tenv (make_extras proc_desc)) with - | Some post -> - Summ.update_summary post summary - | None -> - summary -end - module MakeWithScheduler (C : ProcCfg.S) (S : Scheduler.Make) (T : TransferFunctions.MakeSIL) = MakeNoCFG (S (C)) (T (C)) diff --git a/infer/src/checkers/AbstractInterpreter.mli b/infer/src/checkers/AbstractInterpreter.mli index bf0c8794f..416813068 100644 --- a/infer/src/checkers/AbstractInterpreter.mli +++ b/infer/src/checkers/AbstractInterpreter.mli @@ -63,17 +63,3 @@ module Make (CFG : ProcCfg.S) (MakeTransferFunctions : TransferFunctions.MakeSIL) : S with module TransferFunctions = MakeTransferFunctions(CFG) - -(** create an interprocedural abstract interpreter given logic for handling summaries *) -module Interprocedural (Summary : Summary.S) : sig - - (** compute a summary for the given procedure using [compute_post] and write it into the - aggregated [Specs.summary] *) - val compute_summary : - compute_post: ('a ProcData.t -> Summary.payload option) -> - make_extras : (Procdesc.t -> 'a) -> - Procdesc.t -> - Tenv.t -> - Specs.summary -> - Specs.summary -end diff --git a/infer/src/checkers/NullabilitySuggest.ml b/infer/src/checkers/NullabilitySuggest.ml index 33af84b1d..1616f5732 100644 --- a/infer/src/checkers/NullabilitySuggest.ml +++ b/infer/src/checkers/NullabilitySuggest.ml @@ -40,15 +40,7 @@ module UseDefChain = struct end module Domain = AbstractDomain.Map (AccessPath.Raw) (UseDefChain) -(* Right now this is just a placeholder. We'll change it to something useful when necessary *) -module Summary = Summary.Make(struct - type payload = unit - - let update_payload _ summary = summary - let read_payload _ = None - end) - -type extras = unit +type extras = ProcData.no_extras module TransferFunctions (CFG : ProcCfg.S) = struct module CFG = CFG @@ -116,7 +108,6 @@ module Analyzer = AbstractInterpreter.Make (ProcCfg.Exceptional) (LowerHil.Make (TransferFunctions)) -module Interprocedural = AbstractInterpreter.Interprocedural (Summary) let make_error_trace astate ap ud = let name_of ap = @@ -187,16 +178,14 @@ let checker { Callbacks.summary; proc_desc; tenv; } = in Domain.iter report_access_path astate in - let compute_post (proc_data : extras ProcData.t) = - (* Assume all fields are not null in the beginning *) - let initial = Domain.empty, IdAccessPathMapDomain.empty in - match Analyzer.compute_post proc_data ~initial ~debug:false with - | Some (post, _) -> - report post proc_data; - Some () - | None -> - failwithf - "Analyzer failed to compute post for %a" - Typ.Procname.pp (Procdesc.get_proc_name proc_data.pdesc) - in - Interprocedural.compute_summary ~compute_post ~make_extras:(fun _ -> ()) proc_desc tenv summary + (* Assume all fields are not null in the beginning *) + let initial = Domain.empty, IdAccessPathMapDomain.empty in + let proc_data = ProcData.make_default proc_desc tenv in + match Analyzer.compute_post proc_data ~initial ~debug:false with + | Some (post, _) -> + report post proc_data; + summary + | None -> + failwithf + "Analyzer failed to compute post for %a" + Typ.Procname.pp (Procdesc.get_proc_name proc_data.pdesc) diff --git a/infer/src/checkers/Siof.ml b/infer/src/checkers/Siof.ml index 484f5bb43..1cd632163 100644 --- a/infer/src/checkers/Siof.ml +++ b/infer/src/checkers/Siof.ml @@ -172,9 +172,6 @@ end module Analyzer = AbstractInterpreter.Make (ProcCfg.Normal) (TransferFunctions) -module Interprocedural = AbstractInterpreter.Interprocedural (Summary) - - let is_foreign tu_opt (v, _) = match Pvar.get_translation_unit v, tu_opt with | TUFile v_tu, Some current_tu -> @@ -239,25 +236,16 @@ let siof_check pdesc gname (summary : Specs.summary) = | Some (SiofDomain.BottomSiofTrace.Bottom, _) | None -> () -let compute_post proc_data = - Analyzer.compute_post proc_data - ~initial:(SiofDomain.BottomSiofTrace.Bottom, SiofDomain.VarNames.empty) - |> Option.map ~f:SiofDomain.normalize - -let checker { Callbacks.proc_desc; tenv; summary } : Specs.summary = +let checker { Callbacks.proc_desc; tenv; summary; } : Specs.summary = + let proc_data = ProcData.make_default proc_desc tenv in + let initial = SiofDomain.BottomSiofTrace.Bottom, SiofDomain.VarNames.empty in let updated_summary = - Interprocedural.compute_summary - ~compute_post - ~make_extras:ProcData.make_empty_extras - proc_desc - tenv - summary in - let pname = Procdesc.get_proc_name proc_desc in + match Analyzer.compute_post proc_data ~initial with + | Some post -> Summary.update_summary (SiofDomain.normalize post) summary + | None -> summary in begin - match Typ.Procname.get_global_name_of_initializer pname with - | Some gname -> - siof_check proc_desc gname updated_summary - | None -> - () + match Typ.Procname.get_global_name_of_initializer (Procdesc.get_proc_name proc_desc) with + | Some gname -> siof_check proc_desc gname updated_summary + | None -> () end; updated_summary diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index 391277f6c..b51682144 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/infer/src/checkers/ThreadSafety.ml @@ -761,8 +761,6 @@ end module Analyzer = AbstractInterpreter.Make (ProcCfg.Normal) (LowerHil.Make(TransferFunctions)) -module Interprocedural = AbstractInterpreter.Interprocedural (Summary) - (* similarly, we assume that immutable classes safely encapsulate their state *) let is_immutable_collection_class class_name tenv = let immutable_collections = [ @@ -871,53 +869,54 @@ let analyze_procedure { Callbacks.proc_desc; tenv; summary; } = Typ.Procname.is_constructor proc_name || FbThreadSafety.is_custom_init tenv proc_name in let open ThreadSafetyDomain in (* convert the abstract state to a summary by dropping the id map *) - let compute_post ({ ProcData.pdesc; tenv; extras; } as proc_data) = - if should_analyze_proc pdesc tenv - then - begin - if not (Procdesc.did_preanalysis pdesc) then Preanal.do_liveness pdesc tenv; - let initial = - let threads = runs_on_ui_thread pdesc || is_thread_confined_method tenv pdesc in - if is_initializer tenv (Procdesc.get_proc_name pdesc) - then - let add_owned_formal acc formal_index = - match FormalMap.get_formal_base formal_index extras with - | Some base -> - AttributeMapDomain.add_attribute (base, []) Attribute.unconditionally_owned acc - | None -> - acc in - let owned_formals = - (* if a constructer 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 pdesc Annotations.ia_is_inject - then List.mapi ~f:(fun i _ -> i) (Procdesc.get_formals pdesc) - else [0] (* express that the constructor owns [this] *) in - let attribute_map = - List.fold - ~f:add_owned_formal - owned_formals - ~init:ThreadSafetyDomain.empty.attribute_map in - { ThreadSafetyDomain.empty with attribute_map; threads; }, IdAccessPathMapDomain.empty - else - { ThreadSafetyDomain.empty with threads; }, IdAccessPathMapDomain.empty in - - match Analyzer.compute_post proc_data ~initial ~debug:false with - | Some ({ thumbs_up; threads; locks; accesses; attribute_map; }, _) -> - let return_var_ap = - AccessPath.of_pvar - (Pvar.get_ret_pvar (Procdesc.get_proc_name pdesc)) - (Procdesc.get_ret_type pdesc) in - let return_attributes = - try AttributeMapDomain.find return_var_ap attribute_map - with Not_found -> AttributeSetDomain.empty in - Some (thumbs_up, threads, locks, accesses, return_attributes) - | None -> - None - end - else - Some empty_post in - Interprocedural.compute_summary ~compute_post ~make_extras:FormalMap.make proc_desc tenv summary + if should_analyze_proc proc_desc tenv + then + begin + if not (Procdesc.did_preanalysis proc_desc) then Preanal.do_liveness proc_desc tenv; + let extras = FormalMap.make proc_desc in + let proc_data = ProcData.make proc_desc tenv extras in + let initial = + let threads = runs_on_ui_thread proc_desc || is_thread_confined_method tenv proc_desc in + if is_initializer tenv (Procdesc.get_proc_name proc_desc) + then + let add_owned_formal acc formal_index = + match FormalMap.get_formal_base formal_index extras with + | Some base -> + AttributeMapDomain.add_attribute (base, []) Attribute.unconditionally_owned acc + | None -> + acc in + let owned_formals = + (* if a constructer 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) + else [0] (* express that the constructor owns [this] *) in + let attribute_map = + List.fold + ~f:add_owned_formal + owned_formals + ~init:ThreadSafetyDomain.empty.attribute_map in + { ThreadSafetyDomain.empty with attribute_map; threads; }, IdAccessPathMapDomain.empty + else + { ThreadSafetyDomain.empty with threads; }, IdAccessPathMapDomain.empty in + + match Analyzer.compute_post proc_data ~initial ~debug:false with + | Some ({ thumbs_up; threads; locks; accesses; attribute_map; }, _) -> + let return_var_ap = + AccessPath.of_pvar + (Pvar.get_ret_pvar (Procdesc.get_proc_name proc_desc)) + (Procdesc.get_ret_type proc_desc) in + let return_attributes = + try AttributeMapDomain.find return_var_ap attribute_map + with Not_found -> AttributeSetDomain.empty in + let post = thumbs_up, threads, locks, accesses, return_attributes in + Summary.update_summary post summary + | None -> + summary + end + else + Summary.update_summary empty_post summary (* we assume two access paths can alias if their access parts are equal (we ignore the base). *) let can_alias access_path1 access_path2 = diff --git a/infer/src/checkers/annotationReachability.ml b/infer/src/checkers/annotationReachability.ml index 192b11786..f456b10c1 100644 --- a/infer/src/checkers/annotationReachability.ml +++ b/infer/src/checkers/annotationReachability.ml @@ -389,37 +389,20 @@ let check_expensive_subtyping_rules { Callbacks.proc_desc; tenv; summary } overr (expensive_overrides_unexpensive, Localise.verbatim_desc description) in Reporting.log_error summary ~loc exn -module Interprocedural = struct - include AbstractInterpreter.Interprocedural(Summary) - - let check_and_report ({ Callbacks.proc_desc; tenv; summary} as callback) : Specs.summary = - let proc_name = Procdesc.get_proc_name proc_desc in - if is_expensive tenv proc_name then - PatternMatch.override_iter (check_expensive_subtyping_rules callback) tenv proc_name; - - let initial = - (AnnotReachabilityDomain.empty, Domain.TrackingDomain.NonBottom Domain.TrackingVar.empty) in - let compute_post proc_data = - Option.map ~f:fst (Analyzer.compute_post ~initial proc_data) in - let updated_summary : Specs.summary = - compute_summary - ~compute_post:compute_post - ~make_extras:ProcData.make_empty_extras - proc_desc - tenv - summary in - begin - match updated_summary.payload.annot_map with - | Some annot_map -> - List.iter ~f:(report_src_snk_paths callback annot_map) src_snk_pairs - | None -> - () - end; - updated_summary -end - -let checker = Interprocedural.check_and_report +let checker ({ Callbacks.proc_desc; tenv; summary} as callback) : Specs.summary = + let proc_name = Procdesc.get_proc_name proc_desc in + if is_expensive tenv proc_name then + PatternMatch.override_iter (check_expensive_subtyping_rules callback) tenv proc_name; + let initial = + (AnnotReachabilityDomain.empty, Domain.TrackingDomain.NonBottom Domain.TrackingVar.empty) in + let proc_data = ProcData.make_default proc_desc tenv in + match Analyzer.compute_post proc_data ~initial with + | Some (annot_map, _) -> + List.iter ~f:(report_src_snk_paths callback annot_map) src_snk_pairs; + Summary.update_summary annot_map summary + | None -> + summary (* New implementation starts here *) diff --git a/infer/src/labs/ResourceLeaks.ml b/infer/src/labs/ResourceLeaks.ml index 46d0a0eb0..7e25e3fa2 100644 --- a/infer/src/labs/ResourceLeaks.ml +++ b/infer/src/labs/ResourceLeaks.ml @@ -92,10 +92,6 @@ module Analyzer = (ProcCfg.Normal) (* 5(a) *) (LowerHil.Make(TransferFunctions)) -(* Lift our intraprocedural abstract interpreter into an interprocedural one that computes - summaries of the type we defined earlier *) -module Interprocedural = AbstractInterpreter.Interprocedural (Summary) - (* Callback for invoking the checker from the outside--registered in RegisterCheckers *) let checker { Callbacks.summary; proc_desc; tenv; } : Specs.summary = (* Report an error when we have acquired more resources than we have released *) @@ -107,20 +103,20 @@ let checker { Callbacks.summary; proc_desc; tenv; } : Specs.summary = let message = F.asprintf "Leaked %d resource(s)" leak_count in let exn = Exceptions.Checkers (issue_kind, Localise.verbatim_desc message) in Reporting.log_error summary ~loc:last_loc exn in + (* Convert the abstract state to a summary. for now, just the identity function *) let convert_to_summary (post : Domain.astate) : Domain.summary = (* 4(a) *) post in - let compute_post (proc_data : extras ProcData.t) = - let initial = ResourceLeakDomain.initial, IdAccessPathMapDomain.empty in - match Analyzer.compute_post proc_data ~initial ~debug:false with - | Some (post, _) -> - (* 1(c) *) - report post proc_data; - Some (convert_to_summary post) - | None -> - failwithf - "Analyzer failed to compute post for %a" - Typ.Procname.pp (Procdesc.get_proc_name proc_data.pdesc) in - - Interprocedural.compute_summary ~compute_post ~make_extras:FormalMap.make proc_desc tenv summary + let extras = FormalMap.make proc_desc in + let proc_data = ProcData.make proc_desc tenv extras in + let initial = ResourceLeakDomain.initial, IdAccessPathMapDomain.empty in + match Analyzer.compute_post proc_data ~initial ~debug:false with + | Some (post, _) -> + (* 1(c) *) + report post proc_data; + Summary.update_summary (convert_to_summary post) summary + | None -> + failwithf + "Analyzer failed to compute post for %a" + Typ.Procname.pp (Procdesc.get_proc_name proc_data.pdesc) diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml index c0e76ce78..db938a860 100644 --- a/infer/src/quandary/TaintAnalysis.ml +++ b/infer/src/quandary/TaintAnalysis.ml @@ -612,8 +612,6 @@ module Make (TaintSpecification : TaintSpec.S) = struct TaintSpecification.to_summary_access_tree with_footprint_vars - module Interprocedural = AbstractInterpreter.Interprocedural(Summary) - let checker { Callbacks.tenv; summary; proc_desc; } : Specs.summary = (* bind parameters to a trace with a tainted source (if applicable) *) @@ -631,24 +629,22 @@ module Make (TaintSpecification : TaintSpec.S) = struct (TraceDomain.Source.get_tainted_formals pdesc tenv) in access_tree, IdAccessPathMapDomain.empty in - let compute_post (proc_data : extras ProcData.t) = - if not (Procdesc.did_preanalysis proc_data.pdesc) - then - begin - Preanal.do_liveness proc_data.pdesc proc_data.tenv; - Preanal.do_dynamic_dispatch - proc_data.pdesc (Cg.create (SourceFile.invalid __FILE__)) proc_data.tenv; - end; - let initial = make_initial proc_data.pdesc in - match Analyzer.compute_post proc_data ~initial ~debug:false with - | Some (access_tree, _) -> - Some (make_summary proc_data access_tree) - | None -> - if Procdesc.Node.get_succs (Procdesc.get_start_node proc_data.pdesc) <> [] - then failwith "Couldn't compute post" - else None in - let make_extras pdesc = - let formal_map = FormalMap.make pdesc in + if not (Procdesc.did_preanalysis proc_desc) + then + begin + Preanal.do_liveness proc_desc tenv; + Preanal.do_dynamic_dispatch proc_desc (Cg.create (SourceFile.invalid __FILE__)) tenv; + end; + let initial = make_initial proc_desc in + let extras = + let formal_map = FormalMap.make proc_desc in { formal_map; summary; } in - Interprocedural.compute_summary ~compute_post ~make_extras proc_desc tenv summary + let proc_data = ProcData.make proc_desc tenv extras in + match Analyzer.compute_post proc_data ~initial ~debug:false with + | Some (access_tree, _) -> + Summary.update_summary (make_summary proc_data access_tree) summary + | None -> + if Procdesc.Node.get_succs (Procdesc.get_start_node proc_desc) <> [] + then failwith "Couldn't compute post" + else summary end