From 26d4a2d14f2f10ab41720dadcf20fb1810958d32 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Wed, 12 Dec 2018 09:09:17 -0800 Subject: [PATCH] [HIL] simplify some functors around TransferFunctions Summary: A lot of functors that take a `Make{SIL,HIL}` can take a `{SIL,HIL}` directly instead. This makes my head hurt a bit less. Reviewed By: mbouaziz Differential Revision: D13416967 fbshipit-source-id: eb0b33bc4 --- infer/src/absint/LowerHil.ml | 30 ++++++++----- infer/src/absint/LowerHil.mli | 50 +++++++++++----------- infer/src/absint/TransferFunctions.ml | 8 ---- infer/src/absint/TransferFunctions.mli | 8 ---- infer/src/checkers/Litho.ml | 2 +- infer/src/checkers/Ownership.ml | 2 +- infer/src/checkers/Pulse.ml | 6 +-- infer/src/checkers/purity.ml | 2 +- infer/src/checkers/uninit.ml | 2 +- infer/src/concurrency/RacerD.ml | 2 +- infer/src/concurrency/starvation.ml | 2 +- infer/src/labs/ResourceLeaks.ml | 12 +++--- infer/src/nullsafe/NullabilityCheck.ml | 2 +- infer/src/nullsafe/NullabilitySuggest.ml | 2 +- infer/src/quandary/TaintAnalysis.ml | 3 +- infer/src/unit/BoundedCallTreeTests.ml | 2 +- infer/src/unit/TaintTests.ml | 3 +- infer/src/unit/abstractInterpreterTests.ml | 4 +- infer/src/unit/addressTakenTests.ml | 2 +- infer/src/unit/analyzerTester.ml | 14 +++--- infer/src/unit/livenessTests.ml | 2 +- 21 files changed, 74 insertions(+), 86 deletions(-) diff --git a/infer/src/absint/LowerHil.ml b/infer/src/absint/LowerHil.ml index 9cd0bd39d..3ef068889 100644 --- a/infer/src/absint/LowerHil.ml +++ b/infer/src/absint/LowerHil.ml @@ -36,12 +36,7 @@ module MakeHILDomain (Domain : AbstractDomain.S) = struct Domain.pp fmt astate end -module Make - (MakeTransferFunctions : TransferFunctions.MakeHIL) - (HilConfig : HilConfig) - (CFG : ProcCfg.S) = -struct - module TransferFunctions = MakeTransferFunctions (CFG) +module Make (TransferFunctions : TransferFunctions.HIL) (HilConfig : HilConfig) = struct module CFG = TransferFunctions.CFG module Domain = MakeHILDomain (TransferFunctions.Domain) @@ -95,13 +90,25 @@ struct else (actual_state', id_map') end +module type S = sig + module Interpreter : AbstractInterpreter.S + + type domain + + val compute_post : + Interpreter.TransferFunctions.extras ProcData.t -> initial:domain -> domain option +end + module MakeAbstractInterpreterWithConfig (MakeAbstractInterpreter : AbstractInterpreter.Make) (HilConfig : HilConfig) - (CFG : ProcCfg.S) - (MakeTransferFunctions : TransferFunctions.MakeHIL) = -struct - module Interpreter = MakeAbstractInterpreter (Make (MakeTransferFunctions) (HilConfig) (CFG)) + (TransferFunctions : TransferFunctions.HIL) : + S + with type domain = TransferFunctions.Domain.t + and module Interpreter = MakeAbstractInterpreter(Make(TransferFunctions)(HilConfig)) = struct + module Interpreter = MakeAbstractInterpreter (Make (TransferFunctions) (HilConfig)) + + type domain = TransferFunctions.Domain.t let compute_post ({ProcData.pdesc; tenv} as proc_data) ~initial = Preanal.do_preanalysis pdesc tenv ; @@ -120,5 +127,6 @@ struct Interpreter.compute_post ~pp_instr proc_data ~initial:initial' |> Option.map ~f:fst end -module MakeAbstractInterpreter = +module MakeAbstractInterpreter (TransferFunctions : TransferFunctions.HIL) = MakeAbstractInterpreterWithConfig (AbstractInterpreter.MakeRPO) (DefaultConfig) + (TransferFunctions) diff --git a/infer/src/absint/LowerHil.mli b/infer/src/absint/LowerHil.mli index a37a974b3..a4b1ac21b 100644 --- a/infer/src/absint/LowerHil.mli +++ b/infer/src/absint/LowerHil.mli @@ -15,13 +15,15 @@ end module DefaultConfig : HilConfig (** Functor for turning HIL transfer functions into SIL transfer functions *) -module Make - (MakeTransferFunctions : TransferFunctions.MakeHIL) - (HilConfig : HilConfig) - (CFG : ProcCfg.S) : sig - module TransferFunctions : module type of MakeTransferFunctions (CFG) - - module CFG : module type of TransferFunctions.CFG +module Make (TransferFunctions : TransferFunctions.HIL) (HilConfig : HilConfig) : sig + module CFG : + ProcCfg.S + with type t = TransferFunctions.CFG.t + and type instrs_dir = TransferFunctions.CFG.instrs_dir + and type Node.t = TransferFunctions.CFG.Node.t + and type Node.id = TransferFunctions.CFG.Node.id + and module Node.IdMap = TransferFunctions.CFG.Node.IdMap + and module Node.IdSet = TransferFunctions.CFG.Node.IdSet module Domain : module type of AbstractDomain.Pair (TransferFunctions.Domain) (IdAccessPathMapDomain) @@ -33,28 +35,28 @@ module Make val pp_session_name : CFG.Node.t -> Format.formatter -> unit end +module type S = sig + module Interpreter : AbstractInterpreter.S + + type domain + + val compute_post : + Interpreter.TransferFunctions.extras ProcData.t -> initial:domain -> domain option + (** compute and return the postcondition for the given procedure starting from [initial]. *) +end + (** Wrapper around Interpreter to prevent clients from having to deal with IdAccessPathMapDomain *) module MakeAbstractInterpreterWithConfig (MakeAbstractInterpreter : AbstractInterpreter.Make) (HilConfig : HilConfig) - (CFG : ProcCfg.S) - (MakeTransferFunctions : TransferFunctions.MakeHIL) : sig - module Interpreter : - module type of AbstractInterpreter.MakeRPO (Make (MakeTransferFunctions) (HilConfig) (CFG)) - - val compute_post : - Interpreter.TransferFunctions.extras ProcData.t - -> initial:MakeTransferFunctions(CFG).Domain.t - -> MakeTransferFunctions(CFG).Domain.t option - (** compute and return the postcondition for the given procedure starting from [initial]. If - [debug] is true, print html debugging output. *) -end + (TransferFunctions : TransferFunctions.HIL) : + S + with type domain = TransferFunctions.Domain.t + and module Interpreter = MakeAbstractInterpreter(Make(TransferFunctions)(HilConfig)) (** Simpler version of the above wrapper that uses the default HIL config *) -module MakeAbstractInterpreter - (CFG : ProcCfg.S) - (MakeTransferFunctions : TransferFunctions.MakeHIL) : sig +module MakeAbstractInterpreter (TransferFunctions : TransferFunctions.HIL) : sig include module type of - MakeAbstractInterpreterWithConfig (AbstractInterpreter.MakeRPO) (DefaultConfig) (CFG) - (MakeTransferFunctions) + MakeAbstractInterpreterWithConfig (AbstractInterpreter.MakeRPO) (DefaultConfig) + (TransferFunctions) end diff --git a/infer/src/absint/TransferFunctions.ml b/infer/src/absint/TransferFunctions.ml index 875d0911a..b18cc0d0d 100644 --- a/infer/src/absint/TransferFunctions.ml +++ b/infer/src/absint/TransferFunctions.ml @@ -28,11 +28,3 @@ end module type HIL = sig include S with type instr := HilInstr.t end - -module type MakeSIL = functor (C : ProcCfg.S) -> sig - include SIL with module CFG = C -end - -module type MakeHIL = functor (C : ProcCfg.S) -> sig - include HIL with module CFG = C -end diff --git a/infer/src/absint/TransferFunctions.mli b/infer/src/absint/TransferFunctions.mli index 3c43a61bb..a09092183 100644 --- a/infer/src/absint/TransferFunctions.mli +++ b/infer/src/absint/TransferFunctions.mli @@ -36,11 +36,3 @@ end module type HIL = sig include S with type instr := HilInstr.t end - -module type MakeSIL = functor (C : ProcCfg.S) -> sig - include SIL with module CFG = C -end - -module type MakeHIL = functor (C : ProcCfg.S) -> sig - include HIL with module CFG = C -end diff --git a/infer/src/checkers/Litho.ml b/infer/src/checkers/Litho.ml index 1791e1f88..5c5034d34 100644 --- a/infer/src/checkers/Litho.ml +++ b/infer/src/checkers/Litho.ml @@ -270,7 +270,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let pp_session_name _node fmt = F.pp_print_string fmt "litho" end -module Analyzer = LowerHil.MakeAbstractInterpreter (ProcCfg.Exceptional) (TransferFunctions) +module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (ProcCfg.Exceptional)) let checker {Callbacks.summary; proc_desc; tenv} = let proc_data = ProcData.make_default proc_desc tenv in diff --git a/infer/src/checkers/Ownership.ml b/infer/src/checkers/Ownership.ml index b1d5796ec..bb135bb2b 100644 --- a/infer/src/checkers/Ownership.ml +++ b/infer/src/checkers/Ownership.ml @@ -379,7 +379,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let pp_session_name _node fmt = F.pp_print_string fmt "ownership" end -module Analyzer = LowerHil.MakeAbstractInterpreter (ProcCfg.Exceptional) (TransferFunctions) +module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (ProcCfg.Exceptional)) let report_invalid_return post end_loc summary = let locals = diff --git a/infer/src/checkers/Pulse.ml b/infer/src/checkers/Pulse.ml index 956632923..97f6377d3 100644 --- a/infer/src/checkers/Pulse.ml +++ b/infer/src/checkers/Pulse.ml @@ -132,10 +132,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let pp_session_name _node fmt = F.pp_print_string fmt "Pulse" end +module HilConfig = LowerHil.DefaultConfig module Analyzer = - LowerHil.MakeAbstractInterpreterWithConfig (AbstractInterpreter.MakeWTO) (LowerHil.DefaultConfig) - (ProcCfg.Exceptional) - (TransferFunctions) + LowerHil.MakeAbstractInterpreterWithConfig (AbstractInterpreter.MakeWTO) (HilConfig) + (TransferFunctions (ProcCfg.Exceptional)) let checker {Callbacks.proc_desc; tenv; summary} = let proc_data = ProcData.make proc_desc tenv summary in diff --git a/infer/src/checkers/purity.ml b/infer/src/checkers/purity.ml index 3d82b0a5b..f20c6cf9c 100644 --- a/infer/src/checkers/purity.ml +++ b/infer/src/checkers/purity.ml @@ -121,7 +121,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let pp_session_name _node fmt = F.pp_print_string fmt "purity checker" end -module Analyzer = LowerHil.MakeAbstractInterpreter (ProcCfg.Normal) (TransferFunctions) +module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (ProcCfg.Normal)) let should_report pdesc = (not Config.loop_hoisting) diff --git a/infer/src/checkers/uninit.ml b/infer/src/checkers/uninit.ml index 3661247b8..c81c1e1d9 100644 --- a/infer/src/checkers/uninit.ml +++ b/infer/src/checkers/uninit.ml @@ -307,7 +307,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct end module CFG = ProcCfg.Normal -module Analyzer = LowerHil.MakeAbstractInterpreter (CFG) (TransferFunctions) +module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (CFG)) module Initial = struct let get_locals tenv pdesc = diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index 8caee65e4..23fea7a2f 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -602,7 +602,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let pp_session_name _node fmt = F.pp_print_string fmt "racerd" end -module Analyzer = LowerHil.MakeAbstractInterpreter (ProcCfg.Normal) (TransferFunctions) +module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (ProcCfg.Normal)) let analyze_procedure {Callbacks.proc_desc; tenv; summary} = let open RacerDModels in diff --git a/infer/src/concurrency/starvation.ml b/infer/src/concurrency/starvation.ml index c2734a849..cc9351c8a 100644 --- a/infer/src/concurrency/starvation.ml +++ b/infer/src/concurrency/starvation.ml @@ -135,7 +135,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let pp_session_name _node fmt = F.pp_print_string fmt "starvation" end -module Analyzer = LowerHil.MakeAbstractInterpreter (ProcCfg.Normal) (TransferFunctions) +module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (ProcCfg.Normal)) let analyze_procedure {Callbacks.proc_desc; tenv; summary} = let open StarvationDomain in diff --git a/infer/src/labs/ResourceLeaks.ml b/infer/src/labs/ResourceLeaks.ml index 3f7434276..2c1214104 100644 --- a/infer/src/labs/ResourceLeaks.ml +++ b/infer/src/labs/ResourceLeaks.ml @@ -92,14 +92,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let pp_session_name _node fmt = F.pp_print_string fmt "resource leaks" end +(** 5(a) Type of CFG to analyze--Exceptional to follow exceptional control-flow edges, Normal to + ignore them *) +module CFG = ProcCfg.Normal + (* Create an intraprocedural abstract interpreter from the transfer functions we defined *) -module Analyzer = - LowerHil.MakeAbstractInterpreter - (* Type of CFG to analyze--Exceptional to follow exceptional control-flow edges, Normal to - ignore them *) - (ProcCfg.Normal) - (* 5(a) *) - (TransferFunctions) +module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (CFG)) (* Callback for invoking the checker from the outside--registered in RegisterCheckers *) let checker {Callbacks.summary; proc_desc; tenv} : Summary.t = diff --git a/infer/src/nullsafe/NullabilityCheck.ml b/infer/src/nullsafe/NullabilityCheck.ml index ac56f1c17..7eb944ea8 100644 --- a/infer/src/nullsafe/NullabilityCheck.ml +++ b/infer/src/nullsafe/NullabilityCheck.ml @@ -333,7 +333,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let pp_session_name _node fmt = F.pp_print_string fmt "nullability check" end -module Analyzer = LowerHil.MakeAbstractInterpreter (ProcCfg.Exceptional) (TransferFunctions) +module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (ProcCfg.Exceptional)) let checker {Callbacks.summary; proc_desc; tenv} = let initial = (NullableAP.empty, NullCheckedPname.empty) in diff --git a/infer/src/nullsafe/NullabilitySuggest.ml b/infer/src/nullsafe/NullabilitySuggest.ml index e6d6052bf..18ceee2bb 100644 --- a/infer/src/nullsafe/NullabilitySuggest.ml +++ b/infer/src/nullsafe/NullabilitySuggest.ml @@ -119,7 +119,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let pp_session_name _node fmt = F.pp_print_string fmt "nullability suggest" end -module Analyzer = LowerHil.MakeAbstractInterpreter (ProcCfg.Exceptional) (TransferFunctions) +module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (ProcCfg.Exceptional)) let make_error_trace astate ap ud = let name_of ap = diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml index a447d5d85..5724c6d7b 100644 --- a/infer/src/quandary/TaintAnalysis.ml +++ b/infer/src/quandary/TaintAnalysis.ml @@ -738,8 +738,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct module Analyzer = LowerHil.MakeAbstractInterpreterWithConfig (AbstractInterpreter.MakeRPO) (HilConfig) - (ProcCfg.Exceptional) - (TransferFunctions) + (TransferFunctions (ProcCfg.Exceptional)) (* sanity checks for summaries. should only be used in developer mode *) let check_invariants access_tree = diff --git a/infer/src/unit/BoundedCallTreeTests.ml b/infer/src/unit/BoundedCallTreeTests.ml index 055da9fc1..fc81da5f5 100644 --- a/infer/src/unit/BoundedCallTreeTests.ml +++ b/infer/src/unit/BoundedCallTreeTests.ml @@ -7,7 +7,7 @@ open! IStd module TestInterpreter = - AnalyzerTester.Make (ProcCfg.Exceptional) (BoundedCallTree.TransferFunctions) + AnalyzerTester.Make (BoundedCallTree.TransferFunctions (ProcCfg.Exceptional)) let tests = let open OUnit2 in diff --git a/infer/src/unit/TaintTests.ml b/infer/src/unit/TaintTests.ml index 118c970e3..c654cd2e6 100644 --- a/infer/src/unit/TaintTests.ml +++ b/infer/src/unit/TaintTests.ml @@ -60,8 +60,7 @@ end) module TestInterpreter = AnalyzerTester.Make - (ProcCfg.Normal) - (LowerHil.Make (MockTaintAnalysis.TransferFunctions) (LowerHil.DefaultConfig)) + (LowerHil.Make (MockTaintAnalysis.TransferFunctions (ProcCfg.Normal)) (LowerHil.DefaultConfig)) let tests = let open OUnit2 in diff --git a/infer/src/unit/abstractInterpreterTests.ml b/infer/src/unit/abstractInterpreterTests.ml index 15857e420..e10da7a30 100644 --- a/infer/src/unit/abstractInterpreterTests.ml +++ b/infer/src/unit/abstractInterpreterTests.ml @@ -57,9 +57,9 @@ module PathCountTransferFunctions (CFG : ProcCfg.S) = struct let pp_session_name _node _fmt = () end -module NormalTestInterpreter = AnalyzerTester.Make (ProcCfg.Normal) (PathCountTransferFunctions) +module NormalTestInterpreter = AnalyzerTester.Make (PathCountTransferFunctions (ProcCfg.Normal)) module ExceptionalTestInterpreter = - AnalyzerTester.Make (ProcCfg.Exceptional) (PathCountTransferFunctions) + AnalyzerTester.Make (PathCountTransferFunctions (ProcCfg.Exceptional)) let tests = let open OUnit2 in diff --git a/infer/src/unit/addressTakenTests.ml b/infer/src/unit/addressTakenTests.ml index d8439ff97..dba51f907 100644 --- a/infer/src/unit/addressTakenTests.ml +++ b/infer/src/unit/addressTakenTests.ml @@ -6,7 +6,7 @@ *) open! IStd -module TestInterpreter = AnalyzerTester.Make (ProcCfg.Exceptional) (AddressTaken.TransferFunctions) +module TestInterpreter = AnalyzerTester.Make (AddressTaken.TransferFunctions (ProcCfg.Exceptional)) let tests = let open OUnit2 in diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml index 7316fccf3..d4739bd50 100644 --- a/infer/src/unit/analyzerTester.ml +++ b/infer/src/unit/analyzerTester.ml @@ -149,11 +149,10 @@ end module MakeMake (MakeAbstractInterpreter : AbstractInterpreter.Make) - (CFG : ProcCfg.S with type Node.t = Procdesc.Node.t) - (T : TransferFunctions.MakeSIL) = + (T : TransferFunctions.SIL with type CFG.Node.t = Procdesc.Node.t) = struct open StructuredSil - module I = MakeAbstractInterpreter (T (CFG)) + module I = MakeAbstractInterpreter (T) module M = I.InvariantMap let structured_program_to_cfg program test_pname = @@ -224,7 +223,7 @@ struct let node = create_node (Procdesc.Node.Stmt_node (Skip "Invariant")) [] in set_succs last_node [node] ~exn_handlers ; (* add the assertion to be checked after analysis converges *) - (node, M.add (CFG.Node.id node) (inv_str, inv_label) assert_map) + (node, M.add (T.CFG.Node.id node) (inv_str, inv_label) assert_map) and structured_instrs_to_node last_node assert_map exn_handlers instrs = List.fold ~f:(fun acc instr -> structured_instr_to_node acc exn_handlers instr) @@ -278,10 +277,9 @@ struct OUnit2.assert_failure assert_fail_message end -module Make (CFG : ProcCfg.S with type Node.t = Procdesc.Node.t) (T : TransferFunctions.MakeSIL) = -struct - module AI_RPO = MakeMake (AbstractInterpreter.MakeRPO) (CFG) (T) - module AI_WTO = MakeMake (AbstractInterpreter.MakeWTO) (CFG) (T) +module Make (T : TransferFunctions.SIL with type CFG.Node.t = Procdesc.Node.t) = struct + module AI_RPO = MakeMake (AbstractInterpreter.MakeRPO) (T) + module AI_WTO = MakeMake (AbstractInterpreter.MakeWTO) (T) let ai_list = [("ai_rpo", AI_RPO.create_test); ("ai_wto", AI_WTO.create_test)] diff --git a/infer/src/unit/livenessTests.ml b/infer/src/unit/livenessTests.ml index 72c026964..184e847ef 100644 --- a/infer/src/unit/livenessTests.ml +++ b/infer/src/unit/livenessTests.ml @@ -7,7 +7,7 @@ open! IStd module TestInterpreter = - AnalyzerTester.Make (ProcCfg.Backward (ProcCfg.Normal)) (Liveness.TransferFunctions) + AnalyzerTester.Make (Liveness.TransferFunctions (ProcCfg.Backward (ProcCfg.Normal))) let tests = let open OUnit2 in