[inferbo] Split summary

Reviewed By: skcho

Differential Revision: D13853028

fbshipit-source-id: 77e81eb08

infer/src/backend/Payloads.ml

@@ -11,7 +11,8 @@ module F = Format
 type t =
   { annot_map: AnnotReachabilityDomain.t option
   ; biabduction: BiabductionSummary.t option
-  ; buffer_overrun: BufferOverrunSummary.t option
+  ; buffer_overrun_analysis: BufferOverrunAnalysisSummary.t option
+  ; buffer_overrun_checker: BufferOverrunCheckerSummary.t option
   ; class_loads: ClassLoadsDomain.summary option
   ; cost: CostDomain.summary option
   ; crashcontext_frame: Stacktree_t.stacktree option
@@ -28,7 +29,8 @@ type t =
 let pp pe fmt
     { annot_map
     ; biabduction
-    ; buffer_overrun
+    ; buffer_overrun_analysis
+    ; buffer_overrun_checker
     ; class_loads
     ; cost
     ; crashcontext_frame
@@ -47,7 +49,7 @@ let pp pe fmt
     | None ->
         ()
   in
-  F.fprintf fmt "%a%a%a%a%a%a%a%a%a%a%a%a%a%a%a@\n"
+  F.fprintf fmt "%a%a%a%a%a%a%a%a%a%a%a%a%a%a%a%a@\n"
     (pp_opt "Biabduction" (BiabductionSummary.pp pe))
     biabduction (pp_opt "TypeState" TypeState.pp) typestate
     (pp_opt "ClassLoads" ClassLoadsDomain.pp_summary)
@@ -60,8 +62,10 @@ let pp pe fmt
     siof
     (pp_opt "RacerD" RacerDDomain.pp_summary)
     racerd (pp_opt "Litho" LithoDomain.pp) litho
-    (pp_opt "BufferOverrun" BufferOverrunSummary.pp)
-    buffer_overrun
+    (pp_opt "BufferOverrunAnalysis" BufferOverrunAnalysisSummary.pp)
+    buffer_overrun_analysis
+    (pp_opt "BufferOverrunChecker" BufferOverrunCheckerSummary.pp)
+    buffer_overrun_checker
     (pp_opt "AnnotationReachability" AnnotReachabilityDomain.pp)
     annot_map
     (pp_opt "Uninitialised" UninitDomain.Summary.pp)
@@ -80,7 +84,8 @@ let empty =
   { annot_map= None
   ; biabduction= None
   ; class_loads= None
-  ; buffer_overrun= None
+  ; buffer_overrun_analysis= None
+  ; buffer_overrun_checker= None
   ; crashcontext_frame= None
   ; cost= None
   ; litho= None

infer/src/backend/Payloads.mli

@@ -11,7 +11,8 @@ open! IStd
 type t =
   { annot_map: AnnotReachabilityDomain.t option
   ; biabduction: BiabductionSummary.t option
-  ; buffer_overrun: BufferOverrunSummary.t option
+  ; buffer_overrun_analysis: BufferOverrunAnalysisSummary.t option
+  ; buffer_overrun_checker: BufferOverrunCheckerSummary.t option
   ; class_loads: ClassLoadsDomain.summary option
   ; cost: CostDomain.summary option
   ; crashcontext_frame: Stacktree_t.stacktree option

infer/src/bufferoverrun/bufferOverrunAnalysis.ml

@@ -17,11 +17,13 @@ module Models = BufferOverrunModels
 module Sem = BufferOverrunSemantics
 
 module Payload = SummaryPayload.Make (struct
-  type t = BufferOverrunSummary.t
+  type t = BufferOverrunAnalysisSummary.t
 
-  let update_payloads astate (payloads : Payloads.t) = {payloads with buffer_overrun= Some astate}
+  let update_payloads astate (payloads : Payloads.t) =
+    {payloads with buffer_overrun_analysis= Some astate}
 
-  let of_payloads (payloads : Payloads.t) = payloads.buffer_overrun
+
+  let of_payloads (payloads : Payloads.t) = payloads.buffer_overrun_analysis
 end)
 
 type extras = {oenv: Dom.OndemandEnv.t}
@@ -118,7 +120,7 @@ module TransferFunctions = struct
       -> Typ.Procname.t
       -> (Exp.t * Typ.t) list
       -> Dom.Mem.t
-      -> BufferOverrunSummary.memory
+      -> BufferOverrunAnalysisSummary.t
       -> Location.t
       -> Dom.Mem.t =
    fun tenv integer_type_widths ret callee_pdesc callee_pname params caller_mem callee_exit_mem
@@ -149,7 +151,6 @@ module TransferFunctions = struct
         match
           Ondemand.analyze_proc_name ~caller_pdesc:pdesc callee_pname
           |> Option.bind ~f:Payload.of_summary
-          |> Option.map ~f:BufferOverrunSummary.get_output
         with
         | Some callee_mem ->
             let v = Dom.Mem.find (Loc.of_pvar pvar) callee_mem in
@@ -232,9 +233,8 @@ module TransferFunctions = struct
             Ondemand.analyze_proc_name ~caller_pdesc:pdesc callee_pname
             |> Option.bind ~f:(fun callee_summary ->
                    Payload.of_summary callee_summary
-                   |> Option.map ~f:(fun payload ->
-                          ( BufferOverrunSummary.get_output payload
-                          , Summary.get_proc_desc callee_summary ) ) )
+                   |> Option.map ~f:(fun payload -> (payload, Summary.get_proc_desc callee_summary))
+               )
           with
           | Some (callee_exit_mem, callee_pdesc) ->
               instantiate_mem tenv integer_type_widths ret callee_pdesc callee_pname params mem
@@ -270,7 +270,7 @@ type invariant_map = Analyzer.invariant_map
 
 type local_decls = PowLoc.t
 
-type memory_summary = BufferOverrunSummary.memory
+type memory_summary = BufferOverrunAnalysisSummary.t
 
 let extract_pre = Analyzer.extract_pre
 
@@ -332,3 +332,12 @@ let compute_summary : local_decls -> CFG.t -> invariant_map -> memory_summary =
       exit_mem |> Dom.Mem.forget_locs locals |> Dom.Mem.unset_oenv
   | None ->
       Bottom
+
+
+let do_analysis : Callbacks.proc_callback_args -> Summary.t =
+ fun {proc_desc; tenv; integer_type_widths; summary} ->
+  let inv_map = cached_compute_invariant_map proc_desc tenv integer_type_widths in
+  let locals = get_local_decls proc_desc in
+  let cfg = CFG.from_pdesc proc_desc in
+  let payload = compute_summary locals cfg inv_map in
+  Payload.update_summary payload summary

infer/src/bufferoverrun/bufferOverrunAnalysis.mli

@@ -8,7 +8,7 @@
 open! IStd
 module CFG = ProcCfg.NormalOneInstrPerNode
 
-module Payload : SummaryPayload.S with type t = BufferOverrunSummary.t
+module Payload : SummaryPayload.S with type t = BufferOverrunAnalysisSummary.t
 
 type invariant_map
 
@@ -16,8 +16,6 @@ type local_decls = AbsLoc.PowLoc.t
 
 val cached_compute_invariant_map : Procdesc.t -> Tenv.t -> Typ.IntegerWidths.t -> invariant_map
 
-val compute_summary : local_decls -> CFG.t -> invariant_map -> BufferOverrunSummary.memory
-
 val extract_pre : CFG.Node.id -> invariant_map -> BufferOverrunDomain.Mem.t option
 
 val extract_post : CFG.Node.id -> invariant_map -> BufferOverrunDomain.Mem.t option
@@ -26,3 +24,5 @@ val extract_state :
   CFG.Node.id -> invariant_map -> BufferOverrunDomain.Mem.t AbstractInterpreter.State.t option
 
 val get_local_decls : Procdesc.t -> local_decls
+
+val do_analysis : Callbacks.proc_callback_t

infer/src/bufferoverrun/bufferOverrunAnalysisSummary.ml

@@ -0,0 +1,13 @@
+(*
+ * Copyright (c) 2018-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! IStd
+module DomMem = BufferOverrunDomain.Mem
+
+type t = DomMem.no_oenv_t
+
+let pp = DomMem.pp

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -20,6 +20,16 @@ module Relation = BufferOverrunDomainRelation
 module Sem = BufferOverrunSemantics
 module Trace = BufferOverrunTrace
 
+module Payload = SummaryPayload.Make (struct
+  type t = BufferOverrunCheckerSummary.t
+
+  let update_payloads astate (payloads : Payloads.t) =
+    {payloads with buffer_overrun_checker= Some astate}
+
+
+  let of_payloads (payloads : Payloads.t) = payloads.buffer_overrun_checker
+end)
+
 module UnusedBranch = struct
   type t = {node: CFG.Node.t; location: Location.t; condition: Exp.t; true_branch: bool}
 
@@ -236,12 +246,11 @@ let instantiate_cond :
     -> Procdesc.t
     -> (Exp.t * Typ.t) list
     -> Dom.Mem.t
-    -> BufferOverrunAnalysis.Payload.t
+    -> BufferOverrunAnalysisSummary.t
+    -> BufferOverrunCheckerSummary.t
     -> Location.t
     -> PO.ConditionSet.checked_t =
- fun tenv integer_type_widths callee_pdesc params caller_mem summary location ->
-  let callee_exit_mem = BufferOverrunSummary.get_output summary in
-  let callee_cond = BufferOverrunSummary.get_cond_set summary in
+ fun tenv integer_type_widths callee_pdesc params caller_mem callee_exit_mem callee_cond location ->
   let rel_subst_map =
     Sem.get_subst_map tenv integer_type_widths callee_pdesc params caller_mem callee_exit_mem
   in
@@ -288,13 +297,15 @@ let check_instr :
         match
           Ondemand.analyze_proc_name ~caller_pdesc:pdesc callee_pname
           |> Option.bind ~f:(fun callee_summary ->
-                 BufferOverrunAnalysis.Payload.of_summary callee_summary
-                 |> Option.map ~f:(fun payload -> (payload, Summary.get_proc_desc callee_summary))
-             )
+                 let analysis_payload = BufferOverrunAnalysis.Payload.of_summary callee_summary in
+                 let checker_payload = Payload.of_summary callee_summary in
+                 Option.map2 analysis_payload checker_payload
+                   ~f:(fun analysis_payload checker_payload ->
+                     (analysis_payload, checker_payload, Summary.get_proc_desc callee_summary) ) )
         with
-        | Some (callee_payload, callee_pdesc) ->
-            instantiate_cond tenv integer_type_widths callee_pdesc params mem callee_payload
-              location
+        | Some (callee_mem, callee_condset, callee_pdesc) ->
+            instantiate_cond tenv integer_type_widths callee_pdesc params mem callee_mem
+              callee_condset location
             |> PO.ConditionSet.join cond_set
         | None ->
             (* unknown call / no inferbo payload *) cond_set ) )
@@ -418,9 +429,7 @@ let checker : Callbacks.proc_callback_args -> Summary.t =
     report_errors tenv summary checks ;
     let locals = BufferOverrunAnalysis.get_local_decls proc_desc in
     let cond_set = checks_summary locals checks in
-    let exit_mem = BufferOverrunAnalysis.compute_summary locals cfg inv_map in
-    let payload = (exit_mem, cond_set) in
-    BufferOverrunAnalysis.Payload.update_summary payload summary
+    Payload.update_summary cond_set summary
   in
   NodePrinter.finish_session underlying_exit_node ;
   summary

infer/src/bufferoverrun/bufferOverrunCheckerSummary.ml

@@ -0,0 +1,13 @@
+(*
+ * Copyright (c) 2018-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! IStd
+module POCondSet = BufferOverrunProofObligations.ConditionSet
+
+type t = POCondSet.summary_t
+
+let pp = POCondSet.pp_summary

infer/src/bufferoverrun/bufferOverrunSummary.ml

@@ -1,23 +0,0 @@
-(*
- * Copyright (c) 2018-present, Facebook, Inc.
- *
- * This source code is licensed under the MIT license found in the
- * LICENSE file in the root directory of this source tree.
- *)
-
-open! IStd
-module F = Format
-module Dom = BufferOverrunDomain
-module PO = BufferOverrunProofObligations
-
-type memory = Dom.Mem.no_oenv_t
-
-type t = memory * PO.ConditionSet.summary_t
-
-let get_output : t -> memory = fst
-
-let get_cond_set : t -> PO.ConditionSet.summary_t = snd
-
-let pp : F.formatter -> t -> unit =
- fun fmt (exit_mem, condition_set) ->
-  F.fprintf fmt "%a@;%a" Dom.Mem.pp exit_mem PO.ConditionSet.pp_summary condition_set

infer/src/checkers/registerCheckers.ml

@@ -43,8 +43,17 @@ let all_checkers =
     ; callbacks=
         [ (DynamicDispatch Interproc.analyze_procedure, Language.Clang)
         ; (DynamicDispatch Interproc.analyze_procedure, Language.Java) ] }
-  ; { name= "buffer overrun"
-    ; active= Config.bufferoverrun || Config.cost || Config.purity || Config.quandaryBO
+  ; { name= "buffer overrun analysis"
+    ; active=
+        Config.bufferoverrun || Config.cost || Config.loop_hoisting || Config.purity
+        || Config.quandaryBO
+    ; callbacks=
+        [ (Procedure BufferOverrunAnalysis.do_analysis, Language.Clang)
+        ; (Procedure BufferOverrunAnalysis.do_analysis, Language.Java) ] }
+  ; { name= "buffer overrun checker"
+    ; active=
+        Config.bufferoverrun || Config.cost || Config.loop_hoisting || Config.purity
+        || Config.quandaryBO
     ; callbacks=
         [ (Procedure BufferOverrunChecker.checker, Language.Clang)
         ; (Procedure BufferOverrunChecker.checker, Language.Java) ] }