From 66b335747958c36d7511f2f4d967307939562a1f Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Thu, 12 Apr 2018 13:32:30 -0700 Subject: [PATCH] Share ProcCfg.OneInstrPerNode(Normal) Summary: So we can share stuff between analyses using the same CFG and node representation. Depends on D7586302 Depends on D7586348 Depends on D7568701 Reviewed By: sblackshear Differential Revision: D7586645 fbshipit-source-id: ed64b2c --- infer/src/absint/AbstractDomain.ml | 6 ++-- infer/src/absint/AbstractDomain.mli | 9 +++++ infer/src/absint/ProcCfg.ml | 10 +++++- infer/src/absint/ProcCfg.mli | 9 ++++- .../src/bufferoverrun/bufferOverrunChecker.ml | 2 +- infer/src/checkers/cost.ml | 36 +++++++++---------- infer/src/checkers/costDomain.ml | 9 +---- infer/src/checkers/uninit.ml | 4 +-- 8 files changed, 51 insertions(+), 34 deletions(-) diff --git a/infer/src/absint/AbstractDomain.ml b/infer/src/absint/AbstractDomain.ml index c0293a84a..ff25e772f 100644 --- a/infer/src/absint/AbstractDomain.ml +++ b/infer/src/absint/AbstractDomain.ml @@ -180,8 +180,7 @@ module InvertedSet (Element : PrettyPrintable.PrintableOrderedType) = struct let widen ~prev ~next ~num_iters:_ = join prev next end -module Map (Key : PrettyPrintable.PrintableOrderedType) (ValueDomain : S) = struct - module M = PrettyPrintable.MakePPMap (Key) +module MapOfPPMap (M : PrettyPrintable.PPMap) (ValueDomain : S) = struct include M type astate = ValueDomain.astate M.t @@ -229,6 +228,9 @@ module Map (Key : PrettyPrintable.PrintableOrderedType) (ValueDomain : S) = stru let pp fmt astate = M.pp ~pp_value:ValueDomain.pp fmt astate end +module Map (Key : PrettyPrintable.PrintableOrderedType) (ValueDomain : S) = + MapOfPPMap (PrettyPrintable.MakePPMap (Key)) (ValueDomain) + module InvertedMap (Key : PrettyPrintable.PrintableOrderedType) (ValueDomain : S) = struct module M = PrettyPrintable.MakePPMap (Key) include M diff --git a/infer/src/absint/AbstractDomain.mli b/infer/src/absint/AbstractDomain.mli index 3beb257c7..f3aa18e1b 100644 --- a/infer/src/absint/AbstractDomain.mli +++ b/infer/src/absint/AbstractDomain.mli @@ -85,6 +85,15 @@ module InvertedSet (Element : PrettyPrintable.PrintableOrderedType) : sig include S with type astate = t end +(** Map domain ordered by union over the set of bindings, so the bottom element is the empty map. + Every element implicitly maps to bottom unless it is explicitly bound to something else. + Uses PPMap as the underlying map *) +module MapOfPPMap (PPMap : PrettyPrintable.PPMap) (ValueDomain : S) : sig + include module type of PPMap with type key = PPMap.key + + include WithBottom with type astate = ValueDomain.astate t +end + (** Map domain ordered by union over the set of bindings, so the bottom element is the empty map. Every element implicitly maps to bottom unless it is explicitly bound to something else *) module Map (Key : PrettyPrintable.PrintableOrderedType) (ValueDomain : S) : sig diff --git a/infer/src/absint/ProcCfg.ml b/infer/src/absint/ProcCfg.ml index e70601476..7f4fd1787 100644 --- a/infer/src/absint/ProcCfg.ml +++ b/infer/src/absint/ProcCfg.ml @@ -312,7 +312,13 @@ struct type id = Base.id * index - include (InstrNode : module type of InstrNode with type t := node and type id := id) + include ( + InstrNode : + Node + with type t := node + and type id := id + and module IdMap = InstrNode.IdMap + and module IdSet = InstrNode.IdSet ) (* keep the invariants before/after each instruction *) let instr_ids t = @@ -322,3 +328,5 @@ struct (instr, Some id) ) (instrs t) end + +module NormalOneInstrPerNode = OneInstrPerNode (Normal) diff --git a/infer/src/absint/ProcCfg.mli b/infer/src/absint/ProcCfg.mli index a33254e56..5d4c36149 100644 --- a/infer/src/absint/ProcCfg.mli +++ b/infer/src/absint/ProcCfg.mli @@ -105,4 +105,11 @@ module Exceptional : module Backward (Base : S) : S with type t = Base.t and type node = Base.node and type id = Base.id module OneInstrPerNode (Base : S with type node = DefaultNode.t and type id = DefaultNode.id) : - S with type t = Base.t and type node = Base.node and type id = Base.id * index + S + with type t = Base.t + and type node = Base.node + and type id = InstrNode.id + and module IdMap = InstrNode.IdMap + and module IdSet = InstrNode.IdSet + +module NormalOneInstrPerNode : module type of OneInstrPerNode (Normal) diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index f06260101..226043872 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -307,7 +307,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct output_mem end -module CFG = ProcCfg.OneInstrPerNode (ProcCfg.Normal) +module CFG = ProcCfg.NormalOneInstrPerNode module Analyzer = AbstractInterpreter.Make (CFG) (TransferFunctions) module Report = struct diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index d0492aee7..17ec7d514 100644 --- a/infer/src/checkers/cost.ml +++ b/infer/src/checkers/cost.ml @@ -60,9 +60,9 @@ module TransferFunctionsNodesBasicCost (CFG : ProcCfg.S) = struct let exec_instr_cost _inferbo_mem (astate: CostDomain.NodeInstructionToCostMap.astate) {ProcData.pdesc} (node: CFG.node) instr : CostDomain.NodeInstructionToCostMap.astate = - let nid_int = (Procdesc.Node.get_id (CFG.underlying_node node) :> int) in + let nid_int = Procdesc.Node.get_id (CFG.underlying_node node) in let instr_idx = instr_idx node instr in - let key = (nid_int, instr_idx) in + let key = (nid_int, ProcCfg.Instr_index instr_idx) in let astate' = match instr with | Sil.Call (_, Exp.Const Const.Cfun callee_pname, _, _, _) -> ( @@ -486,27 +486,25 @@ module TransferFunctionsWCET (CFG : ProcCfg.S) = struct let exec_instr (astate: Domain.astate) {ProcData.extras} (node: CFG.node) instr : Domain.astate = let {basic_cost_map= invariant_map_cost; min_trees_map= trees; summary} = extras in - let und_node = CFG.underlying_node node in - let node_id = Procdesc.Node.get_id und_node in - let preds = Procdesc.Node.get_preds und_node in let map_cost m : Itv.Bound.t = CostDomain.NodeInstructionToCostMap.fold - (fun (nid, idx) c acc -> - match Int.Map.find trees nid with - | Some t -> - let c_node = Itv.Bound.mult c t in - L.(debug Analysis Medium) - "@\n [AnalyzerWCET] Adding cost: (%i,%i) --> c =%a t = %a @\n" nid idx - Itv.Bound.pp c Itv.Bound.pp t ; - let c_node' = Itv.Bound.plus_u acc c_node in - L.(debug Analysis Medium) - "@\n [AnalyzerWCET] Adding cost: (%i,%i) --> c_node=%a cost = %a @\n" nid idx - Itv.Bound.pp c_node Itv.Bound.pp c_node' ; - c_node' - | _ -> - assert false ) + (fun ((node_id, _) as instr_node_id) c acc -> + let nid = (node_id :> int) in + let t = Int.Map.find_exn trees nid in + let c_node = Itv.Bound.mult c t in + L.(debug Analysis Medium) + "@\n [AnalyzerWCET] Adding cost: (%a) --> c =%a t = %a @\n" ProcCfg.InstrNode.pp_id + instr_node_id Itv.Bound.pp c Itv.Bound.pp t ; + let c_node' = Itv.Bound.plus_u acc c_node in + L.(debug Analysis Medium) + "@\n [AnalyzerWCET] Adding cost: (%a) --> c_node=%a cost = %a @\n" + ProcCfg.InstrNode.pp_id instr_node_id Itv.Bound.pp c_node Itv.Bound.pp c_node' ; + c_node' ) m Itv.Bound.zero in + let und_node = CFG.underlying_node node in + let node_id = Procdesc.Node.get_id und_node in + let preds = Procdesc.Node.get_preds und_node in let cost_node = match AnalyzerNodesBasicCost.extract_post node_id invariant_map_cost with | Some (_, node_map) -> diff --git a/infer/src/checkers/costDomain.ml b/infer/src/checkers/costDomain.ml index f74e7079f..0bee67e74 100644 --- a/infer/src/checkers/costDomain.ml +++ b/infer/src/checkers/costDomain.ml @@ -55,15 +55,8 @@ module Cost = struct let pp_u = pp end -module IntPair = struct - (* Represents node id,instr index within node *) - include AbstractDomain.Pair (IntCost) (IntCost) - - type t = IntCost.astate * IntCost.astate [@@deriving compare] -end - (* Map (node,instr) -> basic cost *) -module NodeInstructionToCostMap = AbstractDomain.Map (IntPair) (Itv.Bound) +module NodeInstructionToCostMap = AbstractDomain.MapOfPPMap (ProcCfg.InstrNode.IdMap) (Itv.Bound) module ItvPureCost = struct (** (l, u) represents the closed interval [-l; u] (of course infinite bounds are open) *) diff --git a/infer/src/checkers/uninit.ml b/infer/src/checkers/uninit.ml index 9b763a2f9..f735e4765 100644 --- a/infer/src/checkers/uninit.ml +++ b/infer/src/checkers/uninit.ml @@ -243,7 +243,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct {astate with uninit_vars= D.empty} | Call (_, HilInstr.Direct call, [(HilExp.AccessExpression AddressOf Base base)], _, _) when is_dummy_constructor_of_a_struct call -> - (* if it's a default constructor, we use the following heuristic: we assume that it initializes + (* if it's a default constructor, we use the following heuristic: we assume that it initializes correctly all fields when there is an implementation of the constructor that initilizes at least one field. If there is no explicit implementation we cannot assume fields are initialized *) if function_initializes_some_formal_params pdesc call then @@ -292,7 +292,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct astate end -module CFG = ProcCfg.OneInstrPerNode (ProcCfg.Normal) +module CFG = ProcCfg.NormalOneInstrPerNode module Analyzer = AbstractInterpreter.Make (CFG) (LowerHil.Make (TransferFunctions) (LowerHil.DefaultConfig))