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

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

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 assert_one_normal_succ node =
-        let succs = InstrCfg.succs instr_cfg node in
+        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 pred_node1 = assert_one_normal_pred succ_node2 in
-        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 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