[Cost] Forces Inferbo

Reviewed By: jvillard

Differential Revision: D7783117

fbshipit-source-id: 14074af

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 =
+let print_summary : Typ.Procname.t -> Dom.Summary.t -> unit =
- fun pdesc tenv ->
+ fun proc_name s ->
-  let pdata = ProcData.make_default pdesc tenv in
+  L.(debug BufferOverrun Medium)
-  Analyzer.exec_pdesc ~initial:Dom.Mem.init pdata
+    "@\n@[<v 2>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 =
+let compute_invariant_map_and_check : Callbacks.proc_callback_args -> invariant_map * Specs.summary =
- fun summary pdesc tenv ->
+ fun {proc_desc; tenv; summary} ->
-  let inv_map = compute_invariant_map pdesc tenv in
+  Preanal.do_preanalysis proc_desc tenv ;
-  let cfg = CFG.from_pdesc pdesc in
+  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
+  let summary =
-  | Some entry_mem, Some exit_mem ->
+    match (entry_mem, exit_mem) with
-      Some (entry_mem, exit_mem, cond_set)
+    | Some entry_mem, Some exit_mem ->
-  | _ ->
+        let post = (entry_mem, exit_mem, cond_set) in
-      None
+        ( if Config.bo_debug >= 1 then
-
+            let proc_name = Procdesc.get_proc_name proc_desc in
-
+            print_summary proc_name post ) ;
-let print_summary : Typ.Procname.t -> Dom.Summary.t -> unit =
+        Summary.update_summary post summary
- fun proc_name s ->
+    | _ ->
-  L.(debug BufferOverrun Medium)
+        summary
-    "@\n@[<v 2>Summary of %a :@,%a@]@." Typ.Procname.pp proc_name Dom.Summary.pp_summary s
+  in
+  (inv_map, summary)
 
 
 let checker : Callbacks.proc_callback_args -> Specs.summary =
- fun {proc_desc; tenv; summary} ->
+ fun args -> compute_invariant_map_and_check args |> snd
-  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

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

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 =
+let checker ({Callbacks.tenv; proc_desc} as callback_args) : Specs.summary =
-  Preanal.do_preanalysis proc_desc tenv ;
+  let inferbo_invariant_map, summary =
-  let inferbo_invariant_map = BufferOverrunChecker.compute_invariant_map proc_desc tenv in
+    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) *)

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) ] }