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

@@ -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 MapOfPPMap (M : PrettyPrintable.PPMap) (ValueDomain : S) = struct
-  module M = PrettyPrintable.MakePPMap (Key)
   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

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

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)

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)

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

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 ->
+        (fun ((node_id, _) as instr_node_id) c acc ->
-          match Int.Map.find trees nid with
+          let nid = (node_id :> int) in
-          | Some t ->
+          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: (%i,%i) --> c =%a  t = %a @\n" nid idx
+            "@\n  [AnalyzerWCET] Adding cost: (%a) --> c =%a  t = %a @\n" ProcCfg.InstrNode.pp_id
-                Itv.Bound.pp c Itv.Bound.pp t ;
+            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: (%i,%i) --> c_node=%a  cost = %a @\n" nid idx
+            "@\n  [AnalyzerWCET] Adding cost: (%a) --> c_node=%a  cost = %a @\n"
-                Itv.Bound.pp c_node Itv.Bound.pp c_node' ;
+            ProcCfg.InstrNode.pp_id instr_node_id Itv.Bound.pp c_node Itv.Bound.pp c_node' ;
-              c_node'
+          c_node' )
-          | _ ->
-              assert false )
         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) ->

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) *)

infer/src/checkers/uninit.ml

@@ -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))