diff --git a/infer/src/checkers/procCfg.ml b/infer/src/checkers/procCfg.ml index 62b2ee6c9..985a8538b 100644 --- a/infer/src/checkers/procCfg.ml +++ b/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 diff --git a/infer/src/checkers/procCfg.mli b/infer/src/checkers/procCfg.mli index 02f5c7343..9e9c0a04b 100644 --- a/infer/src/checkers/procCfg.mli +++ b/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 diff --git a/infer/src/unit/procCfgTests.ml b/infer/src/unit/procCfgTests.ml index c2c769beb..2de89c123 100644 --- a/infer/src/unit/procCfgTests.ml +++ b/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