new procCfg type with each node containing at most one instruction

Reviewed By: jberdine

Differential Revision: D3273366

fbshipit-source-id: af46536

infer/src/checkers/procCfg.ml

@@ -37,6 +37,33 @@ module DefaultNode = struct
   let pp_id = Cfg.Node.pp_id
 end
 
+type instr_index = int
+type instr_node = { node: DefaultNode.t; instr_index: instr_index; num_instrs: int; }
+
+module OneInstrNode = struct
+  type t = instr_node
+  type id = DefaultNode.id * instr_index
+
+  let instrs t =
+    match DefaultNode.instrs t.node with
+    | [] -> []
+    | instrs -> [IList.nth instrs t.instr_index]
+
+  let kind t =
+    DefaultNode.kind t.node
+
+  let id t =
+    DefaultNode.id t.node, t.instr_index
+
+  let id_compare (t_id1, i_index1) (t_id2, i_index2) =
+    let n = DefaultNode.id_compare t_id1 t_id2 in
+    if n <> 0 then n
+    else int_compare i_index1 i_index2
+
+  let pp_id fmt (id, index) =
+    F.fprintf fmt "(%a: %d)" DefaultNode.pp_id id index
+end
+
 module type S = sig
   type t
   type node
@@ -159,6 +186,66 @@ module Backward (Base : S) = struct
   let exceptional_preds = Base.exceptional_succs
 end
 
+(** Wrapper that views the CFG as if it has at most one instruction per node *)
+module OneInstrPerNode (Base : S with type node = DefaultNode.t) = struct
+  type t = Base.t
+  type node = OneInstrNode.t
+  include (OneInstrNode : module type of OneInstrNode with type t := node)
+
+  let create_node cfg_node =
+    let num_instrs = IList.length (Base.instrs cfg_node) in
+    { node = cfg_node; instr_index = 0; num_instrs; }
+
+  let create_pred_node cfg_node =
+    let num_instrs = IList.length (Base.instrs cfg_node) in
+    { node = cfg_node; instr_index = num_instrs - 1; num_instrs; }
+
+  let get_succs n f_get_succs =
+    if n.instr_index >= n.num_instrs - 1 then
+      IList.map create_node (f_get_succs n.node)
+    else
+      let instr_index = n.instr_index + 1 in
+      [{ n with instr_index; }]
+
+  let succs t n =
+    get_succs n (Base.succs t)
+
+  let normal_succs t n =
+    get_succs n (Base.normal_succs t)
+
+  let exceptional_succs t n =
+    get_succs n (Base.exceptional_succs t)
+
+  let get_preds n f_get_preds =
+    if n.instr_index <= 0 then
+      IList.map create_pred_node (f_get_preds n.node)
+    else
+      let instr_index = n.instr_index - 1 in
+      [{ n with instr_index; }]
+
+  let preds t n =
+    get_preds n (Base.preds t)
+
+  let normal_preds t n =
+    get_preds n (Base.normal_preds t)
+
+  let exceptional_preds t n =
+    get_preds n (Base.exceptional_preds t)
+
+  let start_node t =
+    create_node (Base.start_node t)
+
+  let exit_node t =
+    create_node (Base.exit_node t)
+
+  let proc_desc = Base.proc_desc
+
+  let nodes t =
+    IList.map create_node (Base.nodes t)
+
+  let from_pdesc = Base.from_pdesc
+end
+
 module NodeIdMap (CFG : S) = Map.Make(struct
     type t = CFG.id
     let compare = CFG.id_compare

infer/src/checkers/procCfg.mli

@@ -47,6 +47,11 @@ end
 
 module DefaultNode : Node with type t = Cfg.Node.t and type id = Cfg.Node.id
 
+type instr_index = int
+type instr_node = { node: DefaultNode.t; instr_index: instr_index; num_instrs: int; }
+
+module OneInstrNode : Node with type t = instr_node and type id = Cfg.Node.id * instr_index
+
 (** Forward CFG with no exceptional control-flow *)
 module Normal : S with type t = Cfg.Procdesc.t
                    and type node = DefaultNode.t
@@ -62,6 +67,11 @@ 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) :
+  S with type t = Base.t
+     and type node = OneInstrNode.t
+     and type id = OneInstrNode.id
+
 module NodeIdMap (CFG : S) : Map.S with type key = CFG.id
 
 module NodeIdSet (CFG : S) : Set.S with type elt = CFG.id

infer/src/unit/procCfgTests.ml

@@ -11,14 +11,27 @@ open! Utils
 
 module F = Format
 
+module InstrCfg = ProcCfg.OneInstrPerNode (ProcCfg.Normal)
+
 let tests =
   let cfg = Cfg.Node.create_cfg () in
   let test_pdesc =
     Cfg.Procdesc.create cfg (ProcAttributes.default Procname.empty_block !Config.curr_language) in
-  let create_node cfg =
-    Cfg.Node.create cfg Location.dummy (Cfg.Node.Stmt_node "") [] test_pdesc [] in
+  let dummy_instr1 = Sil.Remove_temps ([], Location.dummy) in
+  let dummy_instr2 = Sil.Abstract Location.dummy in
+  let dummy_instr3 = Sil.Stackop (Pop, Location.dummy) in
+  let instrs1 = [dummy_instr1; dummy_instr2;] in
+  let instrs2 = [dummy_instr3] in
+  let instrs3 = [] in
+  let instrs4 = [] in
+  let create_node cfg instrs =
+    Cfg.Node.create cfg Location.dummy (Cfg.Node.Stmt_node "") instrs test_pdesc [] in
+  let n1 = create_node cfg instrs1 in
+  let n2 = create_node cfg instrs2 in
+  let n3 = create_node cfg instrs3 in
+  let n4 = create_node cfg instrs4 in
 
-  let n1, n2, n3, n4 = create_node cfg, create_node cfg, create_node cfg, create_node cfg in
+  Cfg.Procdesc.set_start_node test_pdesc n1;
   (* let -> represent normal transitions and -*-> represent exceptional transitions *)
   (* creating graph n1 -> n2, n1 -*-> n3, n2 -> n4, n2 -*-> n3, n3 -> n4 , n3 -*> n4 *)
   Cfg.Node.set_succs_exn cfg n1 [n2] [n3];
@@ -27,16 +40,53 @@ let tests =
 
   let normal_proc_cfg = ProcCfg.Normal.from_pdesc test_pdesc in
   let exceptional_proc_cfg = ProcCfg.Exceptional.from_pdesc test_pdesc in
+  let instr_cfg = InstrCfg.from_pdesc test_pdesc in
 
   let open OUnit2 in
-  let cmp = IList.equal Cfg.Node.compare in
-  (* TODO: cleanup *)
+  let instr_cfg_test =
+    let instr_cfg_test_ _ =
+      (* CFG should look like: dummy_instr1 -> dummy_instr2 -> dummy_instr3 *)
+      let assert_one_instr node =
+        let instrs = InstrCfg.instrs node in
+        assert_bool "Nodes should contain one instruction" ((IList.length instrs) = 1);
+        IList.hd instrs in
+      let assert_one_succ node =
+        let succs = InstrCfg.succs instr_cfg node in
+        assert_bool "Should only have one succ" ((IList.length succs) = 1);
+        IList.hd succs in
+      (* walk forward through the CFG and make sure everything looks ok *)
+      let start_node = InstrCfg.start_node instr_cfg in
+      let instr1 = assert_one_instr start_node in
+      assert_bool "instr should be dummy_instr1" (instr1 = dummy_instr1);
+      let succ_node1 = assert_one_succ start_node in
+      let instr2 = assert_one_instr succ_node1 in
+      assert_bool "instr should be dummy_instr2" (instr2 = dummy_instr2);
+      let succ_node2 = assert_one_succ succ_node1 in
+      let instr3 = assert_one_instr succ_node2 in
+      assert_bool "instr should be dummy_instr3" (instr3 = dummy_instr3);
+      (* now, do the same thing going backward *)
+      let assert_one_pred node =
+        let preds = InstrCfg.preds instr_cfg node in
+        assert_bool "Should only have one pred" ((IList.length preds) = 1);
+        IList.hd preds in
+      let pred_node1 = assert_one_pred succ_node2 in
+      let instr2 = assert_one_instr pred_node1 in
+      assert_bool "instr should be dummy_instr2" (instr2 = dummy_instr2);
+      let start_node = assert_one_pred pred_node1 in
+      let instr1 = assert_one_instr start_node in
+      assert_bool "instr should be dummy_instr1" (instr1 = dummy_instr1) in
+    "instr_cfg_test">::instr_cfg_test_ in
+
+  let cmp l1 l2 =
+    let sort = IList.sort Cfg.Node.compare in
+    IList.equal Cfg.Node.compare (sort l1) (sort l2) in
   let pp_diff fmt (actual, expected) =
-    let pp_node_list fmt l = F.pp_print_list Cfg.Node.pp fmt l in
+    let pp_sep fmt _ = F.pp_print_char fmt ',' in
+    let pp_node_list fmt l = F.pp_print_list ~pp_sep Cfg.Node.pp fmt l in
     F.fprintf fmt "Expected output %a but got %a" pp_node_list expected pp_node_list actual in
   let create_test input expected _ =
     assert_equal ~cmp ~pp_diff input expected in
-  let test_list = [
+  let normal_exceptional_tests = [
     (* test the succs of the normal cfg *)
     ("succs_n1", ProcCfg.Normal.succs normal_proc_cfg n1, [n2]);
     ("normal_succs_n1", ProcCfg.Normal.normal_succs normal_proc_cfg n1, [n2]);
@@ -69,4 +119,5 @@ let tests =
     ("exn_normal_preds_n2", ProcCfg.Exceptional.normal_preds exceptional_proc_cfg n2, [n1]);
   ]
     |> IList.map (fun (name, test, expected) -> name>::create_test test expected) in
-  "procCfgSuite">:::test_list
+  let tests = instr_cfg_test :: normal_exceptional_tests in
+  "procCfgSuite">:::tests