From 890afe30948eb1a79f130767d3684c0888069019 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Fri, 10 Nov 2017 16:31:22 -0800 Subject: [PATCH] [HIL] make it easier to customize-specialized abstract interpreter Reviewed By: jeremydubreil Differential Revision: D6299382 fbshipit-source-id: 0722a56 --- infer/src/absint/LowerHil.ml | 8 ++++--- infer/src/absint/LowerHil.mli | 13 +++++++++-- infer/src/quandary/TaintAnalysis.ml | 34 ++++++++++++++--------------- 3 files changed, 32 insertions(+), 23 deletions(-) diff --git a/infer/src/absint/LowerHil.ml b/infer/src/absint/LowerHil.ml index 9c06e1009..a8c807d7b 100644 --- a/infer/src/absint/LowerHil.ml +++ b/infer/src/absint/LowerHil.ml @@ -87,12 +87,12 @@ struct end -module MakeAbstractInterpreter +module MakeAbstractInterpreterWithConfig + (HilConfig : HilConfig) (CFG : ProcCfg.S) (MakeTransferFunctions : TransferFunctions.MakeHIL) = struct - module Interpreter = - AbstractInterpreter.Make (CFG) (Make (MakeTransferFunctions) (DefaultConfig)) + module Interpreter = AbstractInterpreter.Make (CFG) (Make (MakeTransferFunctions) (HilConfig)) let compute_post ({ProcData.pdesc; tenv} as proc_data) ~initial = if not (Procdesc.did_preanalysis pdesc) then Preanal.do_liveness pdesc tenv ; @@ -100,3 +100,5 @@ struct Option.map ~f:fst (Interpreter.compute_post ~debug:false proc_data ~initial:initial') end + +module MakeAbstractInterpreter = MakeAbstractInterpreterWithConfig (DefaultConfig) diff --git a/infer/src/absint/LowerHil.mli b/infer/src/absint/LowerHil.mli index 8a6fda889..1bc9ddd18 100644 --- a/infer/src/absint/LowerHil.mli +++ b/infer/src/absint/LowerHil.mli @@ -34,11 +34,12 @@ module Make end (** Wrapper around Interpreter to prevent clients from having to deal with IdAccessPathMapDomain *) -module MakeAbstractInterpreter +module MakeAbstractInterpreterWithConfig + (HilConfig : HilConfig) (CFG : ProcCfg.S) (MakeTransferFunctions : TransferFunctions.MakeHIL) : sig module Interpreter : - module type of AbstractInterpreter.Make (CFG) (Make (MakeTransferFunctions) (DefaultConfig)) + module type of AbstractInterpreter.Make (CFG) (Make (MakeTransferFunctions) (HilConfig)) val compute_post : Interpreter.TransferFunctions.extras ProcData.t @@ -47,3 +48,11 @@ module MakeAbstractInterpreter (** compute and return the postcondition for the given procedure starting from [initial]. If [debug] is true, print html debugging output. *) end + +(** Simpler version of the above wrapper that uses the default HIL config *) +module MakeAbstractInterpreter + (CFG : ProcCfg.S) + (MakeTransferFunctions : TransferFunctions.MakeHIL) : sig + include module type of + MakeAbstractInterpreterWithConfig (DefaultConfig) (CFG) (MakeTransferFunctions) +end diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml index a9f36b0d0..b30e15e50 100644 --- a/infer/src/quandary/TaintAnalysis.ml +++ b/infer/src/quandary/TaintAnalysis.ml @@ -708,7 +708,8 @@ module Make (TaintSpecification : TaintSpec.S) = struct end module Analyzer = - AbstractInterpreter.Make (ProcCfg.Exceptional) (LowerHil.Make (TransferFunctions) (HilConfig)) + LowerHil.MakeAbstractInterpreterWithConfig (HilConfig) (ProcCfg.Exceptional) + (TransferFunctions) (* sanity checks for summaries. should only be used in developer mode *) let check_invariants access_tree = @@ -828,21 +829,18 @@ module Make (TaintSpecification : TaintSpec.S) = struct (* bind parameters to a trace with a tainted source (if applicable) *) let make_initial pdesc = let pname = Procdesc.get_proc_name pdesc in - let access_tree = - List.fold - ~f:(fun acc (name, typ, taint_opt) -> - match taint_opt with - | Some source -> - let base_ap = - AccessPath.Abs.Abstracted (AccessPath.of_pvar (Pvar.mk name pname) typ) - in - TaintDomain.add_trace base_ap (TraceDomain.of_source source) acc - | None -> - acc) - ~init:TaintDomain.empty - (TraceDomain.Source.get_tainted_formals pdesc tenv) - in - (access_tree, IdAccessPathMapDomain.empty) + List.fold + ~f:(fun acc (name, typ, taint_opt) -> + match taint_opt with + | Some source -> + let base_ap = + AccessPath.Abs.Abstracted (AccessPath.of_pvar (Pvar.mk name pname) typ) + in + TaintDomain.add_trace base_ap (TraceDomain.of_source source) acc + | None -> + acc) + ~init:TaintDomain.empty + (TraceDomain.Source.get_tainted_formals pdesc tenv) in Preanal.do_dynamic_dispatch proc_desc (Cg.create (SourceFile.invalid __FILE__)) tenv ; let initial = make_initial proc_desc in @@ -851,8 +849,8 @@ module Make (TaintSpecification : TaintSpec.S) = struct {formal_map; summary} in let proc_data = ProcData.make proc_desc tenv extras in - match Analyzer.compute_post proc_data ~initial ~debug:false with - | Some (access_tree, _) -> + match Analyzer.compute_post proc_data ~initial 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 (