From 3d6168cd0d8541a3dd7b266c9e2b106ebcf30455 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Tue, 24 Oct 2017 11:03:46 -0700 Subject: [PATCH] [hil] add HIL wrapper for abstract interpreter Summary: Before this change, analyses using HIL needed to pass `IdAcessPathMapDomain.empty` to abstract interpreter, and would get back the map as part of the post. This is a confusing API and was a pain point for Dino in trying to use HIL. This diff adds a HIL wrapper around the abstract interpreter that hides these details. It replaces `LowerHIL.makeDefault` as the new "simplest possible way" to use HIL. Reviewed By: jberdine Differential Revision: D6125597 fbshipit-source-id: 560856b --- infer/src/absint/LowerHil.ml | 14 ++++++++++++-- infer/src/absint/LowerHil.mli | 15 +++++++++++++-- infer/src/checkers/NullabilityCheck.ml | 6 ++---- infer/src/checkers/NullabilitySuggest.ml | 8 +++----- infer/src/checkers/uninit.ml | 3 ++- infer/src/concurrency/RacerD.ml | 9 ++++----- infer/src/labs/ResourceLeaks.ml | 9 ++++----- infer/src/unit/TaintTests.ml | 4 +++- 8 files changed, 43 insertions(+), 25 deletions(-) diff --git a/infer/src/absint/LowerHil.ml b/infer/src/absint/LowerHil.ml index 5ed4b4cb2..5723ba963 100644 --- a/infer/src/absint/LowerHil.ml +++ b/infer/src/absint/LowerHil.ml @@ -60,5 +60,15 @@ struct end -module MakeDefault (MakeTransferFunctions : TransferFunctions.MakeHIL) (CFG : ProcCfg.S) = - Make (MakeTransferFunctions) (DefaultConfig) (CFG) +module MakeAbstractInterpreter + (CFG : ProcCfg.S) + (MakeTransferFunctions : TransferFunctions.MakeHIL) = +struct + module Interpreter = + AbstractInterpreter.Make (CFG) (Make (MakeTransferFunctions) (DefaultConfig)) + + let compute_post ?(debug= Config.debug_mode) proc_data ~initial = + let initial' = (initial, IdAccessPathMapDomain.empty) in + Option.map ~f:fst (Interpreter.compute_post ~debug proc_data ~initial:initial') + +end diff --git a/infer/src/absint/LowerHil.mli b/infer/src/absint/LowerHil.mli index 30bd52149..e6112df79 100644 --- a/infer/src/absint/LowerHil.mli +++ b/infer/src/absint/LowerHil.mli @@ -33,6 +33,17 @@ module Make val exec_instr : Domain.astate -> extras ProcData.t -> CFG.node -> Sil.instr -> Domain.astate end -module MakeDefault (MakeTransferFunctions : TransferFunctions.MakeHIL) (CFG : ProcCfg.S) : sig - include module type of Make (MakeTransferFunctions) (DefaultConfig) (CFG) +(** Wrapper around Interpreter to prevent clients from having to deal with IdAccessPathMapDomain *) +module MakeAbstractInterpreter + (CFG : ProcCfg.S) + (MakeTransferFunctions : TransferFunctions.MakeHIL) : sig + module Interpreter : + module type of AbstractInterpreter.Make (CFG) (Make (MakeTransferFunctions) (DefaultConfig)) + + val compute_post : + ?debug:bool -> Interpreter.TransferFunctions.extras ProcData.t + -> initial:MakeTransferFunctions(CFG).Domain.astate + -> MakeTransferFunctions(CFG).Domain.astate option + (** compute and return the postcondition for the given procedure starting from [initial]. If + [debug] is true, print html debugging output. *) end diff --git a/infer/src/checkers/NullabilityCheck.ml b/infer/src/checkers/NullabilityCheck.ml index 2ab711003..559f7c240 100644 --- a/infer/src/checkers/NullabilityCheck.ml +++ b/infer/src/checkers/NullabilityCheck.ml @@ -114,12 +114,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct end -module Analyzer = - AbstractInterpreter.Make (ProcCfg.Exceptional) (LowerHil.MakeDefault (TransferFunctions)) +module Analyzer = LowerHil.MakeAbstractInterpreter (ProcCfg.Exceptional) (TransferFunctions) let checker {Callbacks.summary; proc_desc; tenv} = - let initial = (Domain.empty, IdAccessPathMapDomain.empty) in + let initial = Domain.empty in let proc_data = ProcData.make proc_desc tenv summary in ignore (Analyzer.compute_post proc_data ~initial ~debug:false) ; summary - diff --git a/infer/src/checkers/NullabilitySuggest.ml b/infer/src/checkers/NullabilitySuggest.ml index 3db375833..e1fc32d20 100644 --- a/infer/src/checkers/NullabilitySuggest.ml +++ b/infer/src/checkers/NullabilitySuggest.ml @@ -104,8 +104,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct end -module Analyzer = - AbstractInterpreter.Make (ProcCfg.Exceptional) (LowerHil.MakeDefault (TransferFunctions)) +module Analyzer = LowerHil.MakeAbstractInterpreter (ProcCfg.Exceptional) (TransferFunctions) let make_error_trace astate ap ud = let name_of ap = @@ -184,11 +183,10 @@ let checker {Callbacks.summary; proc_desc; tenv} = summary else (* Assume all fields are not null in the beginning *) - let initial = (Domain.empty, IdAccessPathMapDomain.empty) in + let initial = Domain.empty in let proc_data = ProcData.make_default proc_desc tenv in match Analyzer.compute_post proc_data ~initial ~debug:false with - | Some (post, _) -> + | Some post -> report post proc_data ; summary | None -> L.(die InternalError) "Analyzer failed to compute post for %a" Typ.Procname.pp proc_name - diff --git a/infer/src/checkers/uninit.ml b/infer/src/checkers/uninit.ml index 57bab634a..a2db1ad14 100644 --- a/infer/src/checkers/uninit.ml +++ b/infer/src/checkers/uninit.ml @@ -74,7 +74,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct end module CFG = ProcCfg.OneInstrPerNode (ProcCfg.Normal) -module Analyzer = AbstractInterpreter.Make (CFG) (LowerHil.MakeDefault (TransferFunctions)) +module Analyzer = + AbstractInterpreter.Make (CFG) (LowerHil.Make (TransferFunctions) (LowerHil.DefaultConfig)) let checker {Callbacks.tenv; summary; proc_desc} : Specs.summary = let cfg = CFG.from_pdesc proc_desc in diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index 51ef5a055..b8f306db2 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -967,8 +967,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct end -module Analyzer = - AbstractInterpreter.Make (ProcCfg.Normal) (LowerHil.MakeDefault (TransferFunctions)) +module Analyzer = LowerHil.MakeAbstractInterpreter (ProcCfg.Normal) (TransferFunctions) (* Methods in @ThreadConfined classes and methods annotated with @ThreadConfined are assumed to all run on the same thread. For the moment we won't warn on accesses resulting from use of such @@ -1131,7 +1130,7 @@ let analyze_procedure {Callbacks.proc_desc; get_proc_desc; tenv; summary} = (* express that the constructor owns [this] *) in let ownership = List.fold ~f:add_owned_formal owned_formals ~init:own_locals_in_cpp in - ({RacerDDomain.empty with ownership; threads}, IdAccessPathMapDomain.empty) + {RacerDDomain.empty with ownership; threads} else (* add Owned(formal_index) predicates for each formal to indicate that each one is owned if it is owned in the caller *) @@ -1143,10 +1142,10 @@ let analyze_procedure {Callbacks.proc_desc; get_proc_desc; tenv; summary} = (FormalMap.get_formals_indexes formal_map) ~init:own_locals_in_cpp in - ({RacerDDomain.empty with ownership; threads}, IdAccessPathMapDomain.empty) + {RacerDDomain.empty with ownership; threads} in match Analyzer.compute_post proc_data ~initial ~debug:false with - | Some ({threads; locks; accesses; ownership; attribute_map}, _) -> + | Some {threads; locks; accesses; ownership; attribute_map} -> let return_var_ap = AccessPath.of_pvar (Pvar.get_ret_pvar (Procdesc.get_proc_name proc_desc)) diff --git a/infer/src/labs/ResourceLeaks.ml b/infer/src/labs/ResourceLeaks.ml index 09c61083f..19b4b3323 100644 --- a/infer/src/labs/ResourceLeaks.ml +++ b/infer/src/labs/ResourceLeaks.ml @@ -93,12 +93,12 @@ end (* Create an intraprocedural abstract interpreter from the transfer functions we defined *) module Analyzer = - AbstractInterpreter.Make + LowerHil.MakeAbstractInterpreter (* Type of CFG to analyze--Exceptional to follow exceptional control-flow edges, Normal to ignore them *) (ProcCfg.Normal) (* 5(a) *) - (LowerHil.Make (TransferFunctions) (LowerHil.DefaultConfig)) + (TransferFunctions) (* Callback for invoking the checker from the outside--registered in RegisterCheckers *) let checker {Callbacks.summary; proc_desc; tenv} : Specs.summary = @@ -118,9 +118,8 @@ let checker {Callbacks.summary; proc_desc; tenv} : Specs.summary = in 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, _) -> + match Analyzer.compute_post proc_data ~initial:ResourceLeakDomain.initial ~debug:false with + | Some post -> (* 1(f) *) report post proc_data ; Summary.update_summary (convert_to_summary post) summary diff --git a/infer/src/unit/TaintTests.ml b/infer/src/unit/TaintTests.ml index 5cab7c65c..8c741c943 100644 --- a/infer/src/unit/TaintTests.ml +++ b/infer/src/unit/TaintTests.ml @@ -60,7 +60,9 @@ module MockTaintAnalysis = TaintAnalysis.Make (struct end) module TestInterpreter = - AnalyzerTester.Make (ProcCfg.Normal) (LowerHil.MakeDefault (MockTaintAnalysis.TransferFunctions)) + AnalyzerTester.Make + (ProcCfg.Normal) + (LowerHil.Make (MockTaintAnalysis.TransferFunctions) (LowerHil.DefaultConfig)) let tests = let open OUnit2 in