From 49136a187bd1cbb863fbaa6d724fbdecb4256018 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Sat, 4 Jun 2016 01:57:45 -0700 Subject: [PATCH] fixing bug in exceptional preds/succs in per-instr procCfg Reviewed By: jeremydubreil Differential Revision: D3346275 fbshipit-source-id: 0db7cb0 --- infer/src/checkers/procCfg.ml | 14 +++++++++-- infer/src/unit/procCfgTests.ml | 43 ++++++++++++++++++++++++---------- 2 files changed, 43 insertions(+), 14 deletions(-) diff --git a/infer/src/checkers/procCfg.ml b/infer/src/checkers/procCfg.ml index 985a8538b..ff3b035c7 100644 --- a/infer/src/checkers/procCfg.ml +++ b/infer/src/checkers/procCfg.ml @@ -214,7 +214,12 @@ module OneInstrPerNode (Base : S with type node = DefaultNode.t) = struct get_succs n (Base.normal_succs t) let exceptional_succs t n = - get_succs n (Base.exceptional_succs t) + (* nodes are structured in such a way that exceptions should not occur in the middle. so if the + next instruction is in the same node as the current instruction, there are no exceptional + succs. *) + if n.instr_index < n.num_instrs - 1 + then [] + else get_succs n (Base.exceptional_succs t) let get_preds n f_get_preds = if n.instr_index <= 0 then @@ -230,7 +235,12 @@ module OneInstrPerNode (Base : S with type node = DefaultNode.t) = struct get_preds n (Base.normal_preds t) let exceptional_preds t n = - get_preds n (Base.exceptional_preds t) + (* nodes are structured in such a way that exceptions should not occur in the middle. so if the + last instruction is in the same node as the current instruction, there are no exceptional + preds. *) + if n.instr_index > 0 + then [] + else get_preds n (Base.exceptional_preds t) let start_node t = create_node (Base.start_node t) diff --git a/infer/src/unit/procCfgTests.ml b/infer/src/unit/procCfgTests.ml index 0e5b016ee..fa9cc2245 100644 --- a/infer/src/unit/procCfgTests.ml +++ b/infer/src/unit/procCfgTests.ml @@ -11,7 +11,7 @@ open! Utils module F = Format -module InstrCfg = ProcCfg.OneInstrPerNode (ProcCfg.Normal) +module InstrCfg = ProcCfg.OneInstrPerNode (ProcCfg.Exceptional) let tests = let cfg = Cfg.Node.create_cfg () in @@ -20,9 +20,10 @@ let tests = 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 dummy_instr4 = Sil.Remove_temps ([], Location.dummy) in let instrs1 = [dummy_instr1; dummy_instr2;] in let instrs2 = [dummy_instr3] in - let instrs3 = [] in + let instrs3 = [dummy_instr4] in let instrs4 = [] in let create_node cfg instrs = Cfg.Node.create cfg Location.dummy (Cfg.Node.Stmt_node "") instrs test_pdesc in @@ -50,29 +51,47 @@ let tests = 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 + let assert_one_normal_succ node = + let succs = InstrCfg.normal_succs instr_cfg node in assert_bool "Should only have one succ" ((IList.length succs) = 1); IList.hd succs in + let assert_one_normal_pred node = + let preds = InstrCfg.normal_preds instr_cfg node in + assert_bool "Should only have one pred" ((IList.length preds) = 1); + IList.hd preds in + let assert_one_exceptional_succ node = + let exceptional_succs = InstrCfg.exceptional_succs instr_cfg node in + assert_bool "Should only have one exceptional succ" ((IList.length exceptional_succs) = 1); + IList.hd exceptional_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 succ_node1 = assert_one_normal_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 succ_node2 = assert_one_normal_succ succ_node1 in let instr3 = assert_one_instr succ_node2 in assert_bool "instr should be dummy_instr3" (instr3 = dummy_instr3); + (* test exceptional edges *) + assert_bool + "internal nodes should have no exceptional succs" + ((InstrCfg.exceptional_succs instr_cfg start_node) = []); + assert_bool + "external nodes should have no exceptional preds" + ((InstrCfg.exceptional_preds instr_cfg succ_node1) = []); + let exceptional_succ = assert_one_exceptional_succ succ_node1 in + let exc_instr = assert_one_instr exceptional_succ in + assert_bool "instr should be dummy_inst4" (exc_instr = dummy_instr4); + let exceptional_preds = InstrCfg.exceptional_preds instr_cfg exceptional_succ in + assert_bool + "n3 should have two exceptional preds" + ((IList.length exceptional_preds) = 2); (* 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 pred_node1 = assert_one_normal_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 start_node = assert_one_normal_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