From 3aab371b1fa67525b1fc4642c0cd1809df9269a3 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Tue, 11 Sep 2018 18:55:25 -0700 Subject: [PATCH] [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 | 4 ++-- infer/src/backend/Payloads.mli | 2 +- .../src/bufferoverrun/bufferOverrunChecker.ml | 14 ++++++------- .../bufferoverrun/bufferOverrunChecker.mli | 2 +- .../src/bufferoverrun/bufferOverrunDomain.ml | 13 ------------ .../src/bufferoverrun/bufferOverrunSummary.ml | 21 +++++++++++++++++++ 6 files changed, 32 insertions(+), 24 deletions(-) create mode 100644 infer/src/bufferoverrun/bufferOverrunSummary.ml diff --git a/infer/src/backend/Payloads.ml b/infer/src/backend/Payloads.ml index f1a5b71d7..8cf484e8a 100644 --- a/infer/src/backend/Payloads.ml +++ b/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 diff --git a/infer/src/backend/Payloads.mli b/infer/src/backend/Payloads.mli index ba887adfc..34a737bed 100644 --- a/infer/src/backend/Payloads.mli +++ b/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 diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index a59398c3e..878f6ee64 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/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_cond = Dom.Summary.get_cond_set summary in + let callee_exit_mem = BufferOverrunSummary.get_output 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@[Summary of %a:@,%a@]@." Typ.Procname.pp proc_name Dom.Summary.pp s + "@\n@[Summary of %a:@,%a@]@." Typ.Procname.pp proc_name BufferOverrunSummary.pp s let get_local_decls proc_desc = diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.mli b/infer/src/bufferoverrun/bufferOverrunChecker.mli index b5054dcc0..30a8fe83d 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.mli +++ b/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 diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index a44e74888..9af1f8b55 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/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 diff --git a/infer/src/bufferoverrun/bufferOverrunSummary.ml b/infer/src/bufferoverrun/bufferOverrunSummary.ml new file mode 100644 index 000000000..38203a953 --- /dev/null +++ b/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