[inferbo] Detach Summary from Domain module

Summary:
It detaches the Summary module from BufferOverrunDomain.

Depends on D9194130

Reviewed By: jvillard

Differential Revision: D9194375

fbshipit-source-id: 30392b5ce

infer/src/backend/Payloads.ml

@@ -11,7 +11,7 @@ module F = Format
 type t =
   { annot_map: AnnotReachabilityDomain.astate option
   ; biabduction: BiabductionSummary.t option
-  ; buffer_overrun: BufferOverrunDomain.Summary.t option
+  ; buffer_overrun: BufferOverrunSummary.t option
   ; crashcontext_frame: Stacktree_t.stacktree option
   ; litho: LithoDomain.astate option
   ; quandary: QuandarySummary.t option
@@ -53,7 +53,7 @@ let pp pe fmt
     siof
     (pp_opt "RacerD" RacerDDomain.pp_summary)
     racerd (pp_opt "Litho" LithoDomain.pp) litho
-    (pp_opt "BufferOverrun" BufferOverrunDomain.Summary.pp)
+    (pp_opt "BufferOverrun" BufferOverrunSummary.pp)
     buffer_overrun
     (pp_opt "AnnotationReachability" AnnotReachabilityDomain.pp)
     annot_map

infer/src/backend/Payloads.mli

@@ -11,7 +11,7 @@ open! IStd
 type t =
   { annot_map: AnnotReachabilityDomain.astate option
   ; biabduction: BiabductionSummary.t option
-  ; buffer_overrun: BufferOverrunDomain.Summary.t option
+  ; buffer_overrun: BufferOverrunSummary.t option
   ; crashcontext_frame: Stacktree_t.stacktree option
   ; litho: LithoDomain.astate option
   ; quandary: QuandarySummary.t option

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -21,7 +21,7 @@ module Trace = BufferOverrunTrace
 module TraceSet = Trace.Set
 
 module Payload = SummaryPayload.Make (struct
-  type t = Dom.Summary.t
+  type t = BufferOverrunSummary.t
 
   let update_payloads astate (payloads : Payloads.t) = {payloads with buffer_overrun= Some astate}
 
@@ -124,11 +124,11 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       -> Typ.Procname.t
       -> (Exp.t * Typ.t) list
       -> Dom.Mem.astate
-      -> Dom.Summary.t
+      -> BufferOverrunSummary.t
       -> Location.t
       -> Dom.Mem.astate =
    fun tenv ret callee_pdesc callee_pname params caller_mem summary location ->
-    let callee_exit_mem = Dom.Summary.get_output summary in
+    let callee_exit_mem = BufferOverrunSummary.get_output summary in
     let rel_subst_map = Sem.get_subst_map tenv callee_pdesc params caller_mem callee_exit_mem in
     let eval_sym_trace, eval_locpath = Sem.mk_eval_sym_trace callee_pdesc params caller_mem in
     let caller_mem =
@@ -505,8 +505,8 @@ module Report = struct
       -> Location.t
       -> PO.ConditionSet.t =
    fun tenv callee_pdesc params caller_mem summary location ->
-    let callee_exit_mem = Dom.Summary.get_output summary in
+    let callee_exit_mem = BufferOverrunSummary.get_output summary in
-    let callee_cond = Dom.Summary.get_cond_set summary in
+    let callee_cond = BufferOverrunSummary.get_cond_set summary in
     let rel_subst_map = Sem.get_subst_map tenv callee_pdesc params caller_mem callee_exit_mem in
     let pname = Procdesc.get_proc_name callee_pdesc in
     let caller_rel = Dom.Mem.get_relation caller_mem in
@@ -684,10 +684,10 @@ let extract_pre = Analyzer.extract_pre
 
 let extract_post = Analyzer.extract_post
 
-let print_summary : Typ.Procname.t -> Dom.Summary.t -> unit =
+let print_summary : Typ.Procname.t -> BufferOverrunSummary.t -> unit =
  fun proc_name s ->
   L.(debug BufferOverrun Medium)
-    "@\n@[<v 2>Summary of %a:@,%a@]@." Typ.Procname.pp proc_name Dom.Summary.pp s
+    "@\n@[<v 2>Summary of %a:@,%a@]@." Typ.Procname.pp proc_name BufferOverrunSummary.pp s
 
 
 let get_local_decls proc_desc =

infer/src/bufferoverrun/bufferOverrunChecker.mli

@@ -9,7 +9,7 @@ open! IStd
 
 val checker : Callbacks.proc_callback_t
 
-module Payload : SummaryPayload.S with type t = BufferOverrunDomain.Summary.t
+module Payload : SummaryPayload.S with type t = BufferOverrunSummary.t
 
 module CFG = ProcCfg.NormalOneInstrPerNode
 

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -14,7 +14,6 @@ open! AbstractDomain.Types
 module F = Format
 module L = Logging
 module Relation = BufferOverrunDomainRelation
-module PO = BufferOverrunProofObligations
 module Trace = BufferOverrunTrace
 module TraceSet = Trace.Set
 
@@ -999,15 +998,3 @@ module Mem = struct
     | NonBottom callee ->
         f_lift (fun caller -> MemReach.instantiate_relation subst_map ~caller ~callee) caller
 end
-
-module Summary = struct
-  type t = Mem.t * PO.ConditionSet.summary_t
-
-  let get_output : t -> Mem.t = 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" Mem.pp exit_mem PO.ConditionSet.pp_summary condition_set
-end

infer/src/bufferoverrun/bufferOverrunSummary.ml

@@ -0,0 +1,21 @@
+(*
+ * 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 t = Dom.Mem.t * PO.ConditionSet.summary_t
+
+let get_output : t -> Dom.Mem.t = 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