From 5bd4daa90035a154bab4741acd72dcef9564e033 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Tue, 13 Dec 2016 08:57:13 -0800 Subject: [PATCH] [absint] make Interprocedural functor easier to customize Summary: Before, the Interprocedural functor was a bit inflexible. You couldn't do custom postprocessing like normalizing the post state or coverting the post from an astate type to a summary type. Now, you can do whatever you want by passing a custom `~compute_post` function. Since `AbstractInterpreter.compute_post` can be used by clients who don't care to do anything custom, this doesn't create too much boilerplate. Reviewed By: jvillard Differential Revision: D4309877 fbshipit-source-id: 8d1d85d --- infer/src/checkers/AbstractInterpreter.mli | 20 +++--- infer/src/checkers/Siof.ml | 8 ++- infer/src/checkers/ThreadSafety.ml | 14 +++- infer/src/checkers/abstractInterpreter.ml | 69 ++++++++++--------- infer/src/checkers/annotationReachability.ml | 7 +- infer/src/checkers/procData.ml | 2 + infer/src/checkers/procData.mli | 2 + infer/src/checkers/summary.ml | 6 ++ infer/src/quandary/TaintAnalysis.ml | 70 ++++++++------------ 9 files changed, 112 insertions(+), 86 deletions(-) diff --git a/infer/src/checkers/AbstractInterpreter.mli b/infer/src/checkers/AbstractInterpreter.mli index 14b0ca8f0..a72d497c3 100644 --- a/infer/src/checkers/AbstractInterpreter.mli +++ b/infer/src/checkers/AbstractInterpreter.mli @@ -17,14 +17,6 @@ module type S = sig module InvariantMap : Map.S with type key = TransferFunctions.CFG.id - (** create an interprocedural abstract interpreter given logic for handling summaries *) - module Interprocedural - (Summary : Summary.S with type summary = TransferFunctions.Domain.astate) : - sig - val checker : Callbacks.proc_callback_args -> TransferFunctions.extras -> - TransferFunctions.Domain.astate option - end - (** invariant map from node id -> state representing postcondition for node id *) type invariant_map = TransferFunctions.Domain.astate state InvariantMap.t @@ -60,3 +52,15 @@ module Make (MakeScheduler : Scheduler.Make) (MakeTransferFunctions : TransferFunctions.Make) : S with module TransferFunctions = MakeTransferFunctions(CFG) + +(** create an interprocedural abstract interpreter given logic for handling summaries *) +module Interprocedural (Summary : Summary.S) : sig + + (** compute and return the summary for the given procedure and store it on disk using + [compute_post]. *) + val compute_and_store_post : + compute_post: ('a ProcData.t -> Summary.summary option) -> + make_extras : (Procdesc.t -> 'a) -> + Callbacks.proc_callback_args -> + Summary.summary option +end diff --git a/infer/src/checkers/Siof.ml b/infer/src/checkers/Siof.ml index e37815b83..12ea45e4d 100644 --- a/infer/src/checkers/Siof.ml +++ b/infer/src/checkers/Siof.ml @@ -103,7 +103,7 @@ module Analyzer = (Scheduler.ReversePostorder) (TransferFunctions) -module Interprocedural = Analyzer.Interprocedural (Summary) +module Interprocedural = AbstractInterpreter.Interprocedural (Summary) let is_foreign tu_opt v = @@ -176,7 +176,11 @@ let siof_check pdesc gname = function () let checker ({ Callbacks.proc_desc; } as callback) = - let post = Interprocedural.checker callback ProcData.empty_extras in + let post = + Interprocedural.compute_and_store_post + ~compute_post:Analyzer.compute_post + ~make_extras:ProcData.make_empty_extras + callback in let pname = Procdesc.get_proc_name proc_desc in match Procname.get_global_name_of_initializer pname with | Some gname -> diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index 3796a9398..fd06b5225 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/infer/src/checkers/ThreadSafety.ml @@ -157,12 +157,16 @@ module Analyzer = (Scheduler.ReversePostorder) (TransferFunctions) -module Interprocedural = Analyzer.Interprocedural (Summary) +module Interprocedural = AbstractInterpreter.Interprocedural (Summary) (*This is a "checker"*) let method_analysis callback = let proc_desc = callback.Callbacks.proc_desc in - let opost = Interprocedural.checker callback ProcData.empty_extras in + let opost = + Interprocedural.compute_and_store_post + ~compute_post:Analyzer.compute_post + ~make_extras:ProcData.make_empty_extras + callback in match opost with | Some post -> (* I am printing to commandline and out to cater to javac and buck*) (L.stdout "\n Procedure: %s@ " @@ -201,7 +205,11 @@ let make_results_table get_proc_desc file_env = let callback_arg = {Callbacks.get_proc_desc; get_procs_in_file = (fun _ -> []); idenv; tenv; proc_name; proc_desc} in - match Interprocedural.checker callback_arg ProcData.empty_extras with + match + Interprocedural.compute_and_store_post + ~compute_post:Analyzer.compute_post + ~make_extras:ProcData.make_empty_extras + callback_arg with | Some post -> post | None -> ThreadSafetyDomain.initial in diff --git a/infer/src/checkers/abstractInterpreter.ml b/infer/src/checkers/abstractInterpreter.ml index 51ee73280..a89304346 100644 --- a/infer/src/checkers/abstractInterpreter.ml +++ b/infer/src/checkers/abstractInterpreter.ml @@ -19,8 +19,14 @@ module type S = sig module Interprocedural (Summary : Summary.S with type summary = TransferFunctions.Domain.astate) : sig - val checker : Callbacks.proc_callback_args -> TransferFunctions.extras -> - TransferFunctions.Domain.astate option + + (** compute and return the summary for the given procedure and store it on disk using + [compute_post]. *) + val compute_and_store_post : + compute_post: ('a ProcData.t -> Summary.summary option) -> + make_extras : (Procdesc.t -> 'a) -> + Callbacks.proc_callback_args -> + Summary.summary option end type invariant_map = TransferFunctions.Domain.astate state InvariantMap.t @@ -129,35 +135,38 @@ module MakeNoCFG let inv_map = exec_cfg cfg proc_data in extract_post (CFG.id (CFG.exit_node cfg)) inv_map - module Interprocedural (Summ : Summary.S with type summary = Domain.astate) = struct - - let checker { Callbacks.get_proc_desc; proc_desc; proc_name; tenv; } extras = - let analyze_ondemand_ _ pdesc = - match compute_post (ProcData.make pdesc tenv extras) with - | Some post -> - Summ.write_summary (Procdesc.get_proc_name pdesc) post; - Some post - | None -> - None in - let analyze_ondemand source pdesc = - ignore (analyze_ondemand_ source pdesc) in - let callbacks = - { - Ondemand.analyze_ondemand; - get_proc_desc; - } in - if Ondemand.procedure_should_be_analyzed proc_name - then - begin - Ondemand.set_callbacks callbacks; - let post_opt = analyze_ondemand_ SourceFile.empty proc_desc in - Ondemand.unset_callbacks (); - post_opt - end - else - Summ.read_summary proc_desc proc_name - end end +module Interprocedural (Summ : Summary.S) = struct + + let compute_and_store_post + ~compute_post ~make_extras { Callbacks.get_proc_desc; proc_desc; proc_name; tenv; } = + let analyze_ondemand_ _ pdesc = + match compute_post (ProcData.make pdesc tenv (make_extras pdesc)) with + | Some post -> + Summ.write_summary (Procdesc.get_proc_name pdesc) post; + Some post + | None -> + None in + let analyze_ondemand source pdesc = + ignore (analyze_ondemand_ source pdesc) in + let callbacks = + { + Ondemand.analyze_ondemand; + get_proc_desc; + } in + if Ondemand.procedure_should_be_analyzed proc_name + then + begin + Ondemand.set_callbacks callbacks; + let post_opt = analyze_ondemand_ SourceFile.empty proc_desc in + Ondemand.unset_callbacks (); + post_opt + end + else + Summ.read_summary proc_desc proc_name +end + + module Make (C : ProcCfg.S) (S : Scheduler.Make) (T : TransferFunctions.Make) = MakeNoCFG (S (C)) (T (C)) diff --git a/infer/src/checkers/annotationReachability.ml b/infer/src/checkers/annotationReachability.ml index 067fe1cb4..ea272d5a0 100644 --- a/infer/src/checkers/annotationReachability.ml +++ b/infer/src/checkers/annotationReachability.ml @@ -353,7 +353,7 @@ module Analyzer = (TransferFunctions) module Interprocedural = struct - include Analyzer.Interprocedural(Summary) + include AbstractInterpreter.Interprocedural(Summary) let is_expensive tenv pname = check_attributes Annotations.ia_is_expensive tenv pname @@ -403,7 +403,10 @@ module Interprocedural = struct if not (IList.length calls = 0) then IList.iter (report_src_snk_path calls) src_annot_list in - match checker proc_data ProcData.empty_extras with + match compute_and_store_post + ~compute_post:Analyzer.compute_post + ~make_extras:ProcData.make_empty_extras + proc_data with | Some Domain.NonBottom (call_map, _) -> IList.iter (report_src_snk_paths call_map) (src_snk_pairs ()) | Some Domain.Bottom | None -> diff --git a/infer/src/checkers/procData.ml b/infer/src/checkers/procData.ml index 4c5c4c0c7..17a051c13 100644 --- a/infer/src/checkers/procData.ml +++ b/infer/src/checkers/procData.ml @@ -15,6 +15,8 @@ type no_extras = unit let empty_extras = () +let make_empty_extras _ = () + let make pdesc tenv extras = { pdesc; tenv; extras; } diff --git a/infer/src/checkers/procData.mli b/infer/src/checkers/procData.mli index 2b4d34020..e3623085b 100644 --- a/infer/src/checkers/procData.mli +++ b/infer/src/checkers/procData.mli @@ -17,4 +17,6 @@ val empty_extras : no_extras val make : Procdesc.t -> Tenv.t -> 'a -> 'a t +val make_empty_extras : Procdesc.t -> no_extras + val make_default : Procdesc.t -> Tenv.t -> no_extras t diff --git a/infer/src/checkers/summary.ml b/infer/src/checkers/summary.ml index 14e347464..285bc5a94 100644 --- a/infer/src/checkers/summary.ml +++ b/infer/src/checkers/summary.ml @@ -11,21 +11,27 @@ open! IStd module type Helper = sig type summary + (* type astate*) (* update the specs payload with [summary] *) val update_payload : summary -> Specs.payload -> Specs.payload (* extract [summmary] from the specs payload *) val read_from_payload : Specs.payload -> summary option + + (*val to_summary : astate -> summary*) end module type S = sig type summary + (* type astate*) (* write the summary for [name] to persistent storage *) val write_summary : Procname.t -> summary -> unit (* read and return the summary for [callee_pname] called from [caller_pdesc]. does the analysis to create the summary if needed *) val read_summary : Procdesc.t -> Procname.t -> summary option + + (* val to_summary : astate -> summary*) end module Make (H : Helper) = struct diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml index 5a71df659..90a6cdb19 100644 --- a/infer/src/quandary/TaintAnalysis.ml +++ b/infer/src/quandary/TaintAnalysis.ml @@ -35,6 +35,9 @@ module Make (TaintSpecification : TaintSpec.S) = struct module TaintDomain = AccessTree.Make (TraceDomain) module IdMapDomain = IdAccessPathMapDomain + (** map from formals to their position *) + type formal_map = int AccessPath.BaseMap.t + module Domain = struct type astate = { @@ -83,8 +86,6 @@ module Make (TaintSpecification : TaintSpec.S) = struct module CFG = CFG module Domain = Domain - (** map from formals to their position *) - type formal_map = int AccessPath.BaseMap.t type extras = formal_map let is_formal base formal_map = @@ -547,46 +548,33 @@ module Make (TaintSpecification : TaintSpec.S) = struct TraceDomain.Source.Set.fold add_summary_for_source (TraceDomain.sources trace) summary_acc in TaintDomain.fold add_summaries_for_trace access_tree [] - let dummy_cg = Cg.create None - - let checker { Callbacks.get_proc_desc; proc_name; proc_desc; tenv; } = - let analyze_ondemand _ pdesc = - let make_formal_access_paths pdesc = - let pname = Procdesc.get_proc_name pdesc in - let attrs = Procdesc.get_attributes pdesc in - let formals_with_nums = - IList.mapi - (fun index (name, typ) -> - let pvar = Pvar.mk name pname in - AccessPath.base_of_pvar pvar typ, index) - attrs.ProcAttributes.formals in - IList.fold_left - (fun formal_map (base, index) -> AccessPath.BaseMap.add base index formal_map) - AccessPath.BaseMap.empty - formals_with_nums in - - Preanal.doit ~handle_dynamic_dispatch:true pdesc dummy_cg tenv; - let formals = make_formal_access_paths pdesc in - let proc_data = ProcData.make pdesc tenv formals in + module Interprocedural = AbstractInterpreter.Interprocedural(Summary) + + let checker callback = + + let compute_post (proc_data : formal_map ProcData.t) = + Preanal.doit ~handle_dynamic_dispatch:true proc_data.pdesc (Cg.create None) proc_data.tenv; match Analyzer.compute_post proc_data with | Some { access_tree; } -> - let summary = make_summary formals access_tree in - Summary.write_summary (Procdesc.get_proc_name pdesc) summary; + Some (make_summary proc_data.extras access_tree) | None -> - if Procdesc.Node.get_succs (Procdesc.get_start_node pdesc) <> [] - then failwith "Couldn't compute post" in - - let callbacks = - { - Ondemand.analyze_ondemand; - get_proc_desc; - } in - if Ondemand.procedure_should_be_analyzed proc_name - then - begin - Ondemand.set_callbacks callbacks; - analyze_ondemand SourceFile.empty proc_desc; - Ondemand.unset_callbacks (); - end - + 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 pname = Procdesc.get_proc_name pdesc in + let attrs = Procdesc.get_attributes pdesc in + let formals_with_nums = + IList.mapi + (fun index (name, typ) -> + let pvar = Pvar.mk name pname in + AccessPath.base_of_pvar pvar typ, index) + attrs.ProcAttributes.formals in + IList.fold_left + (fun formal_map (base, index) -> AccessPath.BaseMap.add base index formal_map) + AccessPath.BaseMap.empty + formals_with_nums in + + ignore(Interprocedural.compute_and_store_post ~compute_post ~make_extras callback) end