From e8ceedeb82de3ece1109b304d05a087296850035 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Wed, 2 May 2018 05:21:03 -0700 Subject: [PATCH] [Cost] Forces Inferbo Reviewed By: jvillard Differential Revision: D7783117 fbshipit-source-id: 14074af --- .../src/bufferoverrun/bufferOverrunChecker.ml | 54 +++++++++---------- .../bufferoverrun/bufferOverrunChecker.mli | 2 +- infer/src/checkers/cost.ml | 7 +-- infer/src/checkers/registerCheckers.ml | 2 +- 4 files changed, 30 insertions(+), 35 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 49ce6fbdf..ec11b3eca 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -582,42 +582,36 @@ let extract_pre = Analyzer.extract_pre let extract_post = Analyzer.extract_post -let compute_invariant_map : Procdesc.t -> Tenv.t -> invariant_map = - fun pdesc tenv -> - let pdata = ProcData.make_default pdesc tenv in - Analyzer.exec_pdesc ~initial:Dom.Mem.init pdata +let print_summary : Typ.Procname.t -> Dom.Summary.t -> unit = + fun proc_name s -> + L.(debug BufferOverrun Medium) + "@\n@[Summary of %a:@,%a@]@." Typ.Procname.pp proc_name Dom.Summary.pp_summary s -let compute_post : Specs.summary -> Procdesc.t -> Tenv.t -> Summary.payload option = - fun summary pdesc tenv -> - let inv_map = compute_invariant_map pdesc tenv in - let cfg = CFG.from_pdesc pdesc in +let compute_invariant_map_and_check : Callbacks.proc_callback_args -> invariant_map * Specs.summary = + fun {proc_desc; tenv; summary} -> + Preanal.do_preanalysis proc_desc tenv ; + let pdata = ProcData.make_default proc_desc tenv in + let inv_map = Analyzer.exec_pdesc ~initial:Dom.Mem.init pdata in + let cfg = CFG.from_pdesc proc_desc in let entry_mem = extract_post (CFG.start_node cfg |> CFG.id) inv_map in let exit_mem = extract_post (CFG.exit_node cfg |> CFG.id) inv_map in let cond_set = - Report.check_proc summary pdesc tenv cfg inv_map |> Report.report_errors summary pdesc + Report.check_proc summary proc_desc tenv cfg inv_map |> Report.report_errors summary proc_desc in - match (entry_mem, exit_mem) with - | Some entry_mem, Some exit_mem -> - Some (entry_mem, exit_mem, cond_set) - | _ -> - None - - -let print_summary : Typ.Procname.t -> Dom.Summary.t -> unit = - fun proc_name s -> - L.(debug BufferOverrun Medium) - "@\n@[Summary of %a :@,%a@]@." Typ.Procname.pp proc_name Dom.Summary.pp_summary s + let summary = + match (entry_mem, exit_mem) with + | Some entry_mem, Some exit_mem -> + let post = (entry_mem, exit_mem, cond_set) in + ( if Config.bo_debug >= 1 then + let proc_name = Procdesc.get_proc_name proc_desc in + print_summary proc_name post ) ; + Summary.update_summary post summary + | _ -> + summary + in + (inv_map, summary) let checker : Callbacks.proc_callback_args -> Specs.summary = - fun {proc_desc; tenv; summary} -> - Preanal.do_preanalysis proc_desc tenv ; - match compute_post summary proc_desc tenv with - | Some post -> - ( if Config.bo_debug >= 1 then - let proc_name = Specs.get_proc_name summary in - print_summary proc_name post ) ; - Summary.update_summary post summary - | None -> - summary + fun args -> compute_invariant_map_and_check args |> snd diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.mli b/infer/src/bufferoverrun/bufferOverrunChecker.mli index 18ac1900c..9986ac26f 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.mli +++ b/infer/src/bufferoverrun/bufferOverrunChecker.mli @@ -15,6 +15,6 @@ module CFG = ProcCfg.NormalOneInstrPerNode type invariant_map -val compute_invariant_map : Procdesc.t -> Tenv.t -> invariant_map +val compute_invariant_map_and_check : Callbacks.proc_callback_args -> invariant_map * Specs.summary val extract_pre : CFG.id -> invariant_map -> BufferOverrunDomain.Mem.t option diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index 97650fa31..e77ca55c7 100644 --- a/infer/src/checkers/cost.ml +++ b/infer/src/checkers/cost.ml @@ -540,9 +540,10 @@ let check_and_report_infinity cost proc_desc summary = Reporting.log_error ~loc summary exn -let checker {Callbacks.tenv; summary; proc_desc} : Specs.summary = - Preanal.do_preanalysis proc_desc tenv ; - let inferbo_invariant_map = BufferOverrunChecker.compute_invariant_map proc_desc tenv in +let checker ({Callbacks.tenv; proc_desc} as callback_args) : Specs.summary = + let inferbo_invariant_map, summary = + BufferOverrunChecker.compute_invariant_map_and_check callback_args + in let proc_data = ProcData.make_default proc_desc tenv in let node_cfg = NodeCFG.from_pdesc proc_desc in (* computes the data dependencies: node -> (var -> var set) *) diff --git a/infer/src/checkers/registerCheckers.ml b/infer/src/checkers/registerCheckers.ml index 91be670da..fe83f6307 100644 --- a/infer/src/checkers/registerCheckers.ml +++ b/infer/src/checkers/registerCheckers.ml @@ -42,7 +42,7 @@ let all_checkers = [ (Procedure Interproc.analyze_procedure, Language.Clang) ; (DynamicDispatch Interproc.analyze_procedure, Language.Java) ] } ; { name= "buffer overrun" - ; active= Config.bufferoverrun + ; active= Config.bufferoverrun && not Config.cost (* Cost analysis already triggers Inferbo *) ; callbacks= [ (Procedure BufferOverrunChecker.checker, Language.Clang) ; (Procedure BufferOverrunChecker.checker, Language.Java) ] }