exceptional procCfg

Reviewed By: cristianoc, jeremydubreil

Differential Revision: D3177625

fb-gh-sync-id: 4123d37
fbshipit-source-id: 4123d37

infer/src/checkers/addressTaken.ml

@@ -49,4 +49,4 @@ end
 
 module Analyzer =
   AbstractInterpreter.Make
-    (ProcCfg.Forward) (Scheduler.ReversePostorder) (Domain) (TransferFunctions)
+    (ProcCfg.Exceptional) (Scheduler.ReversePostorder) (Domain) (TransferFunctions)

infer/src/checkers/annotationReachability.ml

@@ -283,7 +283,7 @@ end
 
 module Analyzer =
   AbstractInterpreter.Make
-    (ProcCfg.Forward)
+    (ProcCfg.Exceptional)
     (Scheduler.ReversePostorder)
     (Domain)
     (TransferFunctions)

infer/src/checkers/copyPropagation.ml

@@ -121,7 +121,7 @@ end
 
 module Analyzer =
   AbstractInterpreter.Make
-    (ProcCfg.Forward)
+    (ProcCfg.Exceptional)
     (Scheduler.ReversePostorder)
     (Domain)
     (TransferFunctions)

infer/src/checkers/liveness.ml

@@ -61,7 +61,7 @@ end
 
 module Analyzer =
   AbstractInterpreter.Make
-    (ProcCfg.Backward(ProcCfg.Forward))
+    (ProcCfg.Backward(ProcCfg.Exceptional))
     (Scheduler.ReversePostorder)
     (Domain)
     (TransferFunctions)

infer/src/checkers/procCfg.ml

@@ -9,10 +9,9 @@
 
 open! Utils
 
-
 module F = Format
 
-(** control-flow graph for a single procedure (as opposed to cfg.ml, which represents a cfg for a
+(** Control-flow graph for a single procedure (as opposed to cfg.ml, which represents a cfg for a
     file). *)
 
 module type Base = sig
@@ -22,15 +21,24 @@ module type Base = sig
 
   val node_id : node -> node_id
   val node_id_compare : node_id -> node_id -> int
+  (** all successors (normal and exceptional) *)
   val succs : t -> node -> node list
+  (** all predecessors (normal and exceptional) *)
   val preds : t -> node -> node list
 end
 
-(* wrapper that allows us to do tricks like turn a forward cfg to into a backward one *)
+(** Wrapper that allows us to do tricks like turn a forward cfg to into a backward one *)
 module type Wrapper = sig
   include Base
 
-  val exn_succs : t -> node -> node list
+  (** non-exceptional successors *)
+  val normal_succs : t -> node -> node list
+  (** non-exceptional predecessors *)
+  val normal_preds : t -> node -> node list
+  (** exceptional successors *)
+  val exceptional_succs : t -> node -> node list
+  (** exceptional predescessors *)
+  val exceptional_preds : t -> node -> node list
   val start_node : t -> node
   val exit_node : t -> node
   val instrs : node -> Sil.instr list
@@ -42,18 +50,22 @@ module type Wrapper = sig
 
   val pp_node : F.formatter -> node -> unit
   val pp_node_id : F.formatter -> node_id -> unit
-
 end
 
-module Forward : Wrapper with type node = Cfg.node = struct
+(** Forward CFG with no exceptional control-flow *)
+module Normal = struct
   type t = Cfg.Procdesc.t
   type node = Cfg.node
   type node_id = Cfg.Node.id
 
   let node_id = Cfg.Node.get_id
-  let succs _ n = Cfg.Node.get_succs n
-  let exn_succs _ n = Cfg.Node.get_exn n
-  let preds _ n = Cfg.Node.get_preds n
+  let normal_succs _ n = Cfg.Node.get_succs n
+  let normal_preds _ n = Cfg.Node.get_preds n
+  (* prune away exceptional control flow *)
+  let exceptional_succs _ _ = []
+  let exceptional_preds _ _ = []
+  let succs = normal_succs
+  let preds = normal_preds
   let start_node = Cfg.Procdesc.get_start_node
   let exit_node = Cfg.Procdesc.get_exit_node
   let instrs = Cfg.Node.get_instrs
@@ -66,10 +78,87 @@ module Forward : Wrapper with type node = Cfg.node = struct
   let node_id_compare = Cfg.Node.id_compare
 
   let pp_node = Cfg.Node.pp
+
   let pp_node_id fmt (n : Cfg.Node.id) = F.fprintf fmt "%d" (n :> int)
+end
 
+(** Forward CFG with exceptional control-flow *)
+module Exceptional : Wrapper with type node = Cfg.node = struct
+
+  module NodeIdMap = Map.Make(struct
+      type t = Cfg.Node.id
+      let compare = Cfg.Node.id_compare
+    end)
+
+  type node = Cfg.node
+  type node_id = Cfg.Node.id
+  type id_node_map = node list NodeIdMap.t
+  type t = Cfg.Procdesc.t * id_node_map
+
+  let from_pdesc pdesc =
+    (* map from a node to its exceptional predecessors *)
+    let add_exn_preds exn_preds_acc n =
+      let add_exn_pred exn_preds_acc exn_succ_node =
+        let exn_succ_node_id = Cfg.Node.get_id exn_succ_node in
+        let existing_exn_preds =
+          try NodeIdMap.find exn_succ_node_id exn_preds_acc
+          with Not_found -> [] in
+        if not (IList.mem Cfg.Node.equal n existing_exn_preds)
+        then (* don't add duplicates *)
+          NodeIdMap.add exn_succ_node_id (n :: existing_exn_preds) exn_preds_acc
+        else
+          exn_preds_acc in
+      IList.fold_left add_exn_pred exn_preds_acc (Cfg.Node.get_exn n) in
+    let exceptional_preds =
+      IList.fold_left add_exn_preds NodeIdMap.empty (Cfg.Procdesc.get_nodes pdesc) in
+    pdesc, exceptional_preds
+
+  let nodes (t, _) = Cfg.Procdesc.get_nodes t
+
+  let normal_succs _ n = Cfg.Node.get_succs n
+
+  let normal_preds _ n = Cfg.Node.get_preds n
+
+  let exceptional_succs _ n = Cfg.Node.get_exn n
+
+  let exceptional_preds (_, exn_pred_map) n =
+    try NodeIdMap.find (Cfg.Node.get_id n) exn_pred_map
+    with Not_found -> []
+
+  (** get all normal and exceptional successors of [n]. *)
+  let succs t n =
+    let normal_succs = normal_succs t n in
+    match exceptional_succs t n with
+    | [] ->
+        normal_succs
+    | exceptional_succs ->
+        normal_succs @ exceptional_succs
+        |> IList.sort Cfg.Node.compare
+        |> IList.remove_duplicates Cfg.Node.compare
+
+  (** get all normal and exceptional predecessors of [n]. *)
+  let preds t n =
+    let normal_preds = normal_preds t n in
+    match exceptional_preds t n with
+    | [] ->
+        normal_preds
+    | exceptional_preds ->
+        normal_preds @ exceptional_preds
+        |> IList.sort Cfg.Node.compare
+        |> IList.remove_duplicates Cfg.Node.compare
+
+  let proc_desc (pdesc, _) = pdesc
+  let start_node (pdesc, _) = Cfg.Procdesc.get_start_node pdesc
+  let exit_node (pdesc, _) = Cfg.Procdesc.get_exit_node pdesc
+  let instrs = Cfg.Node.get_instrs
+  let node_id = Cfg.Node.get_id
+  let node_id_compare = Cfg.Node.id_compare
+  let pp_node = Cfg.Node.pp
+  let pp_node_id fmt (n : Cfg.Node.id) = F.fprintf fmt "%d" (n :> int)
+  let kind = Cfg.Node.get_kind
 end
 
+(** Turn a forward CFG into a backward cfg *)
 module Backward (W : Wrapper) = struct
   include W
 
@@ -78,11 +167,10 @@ module Backward (W : Wrapper) = struct
   let start_node = W.exit_node
   let exit_node = W.start_node
   let instrs t = IList.rev (W.instrs t)
-
-  (* TODO: we'll need to change the CFG to implement this correctly *)
-  let exn_succs _ =
-    failwith "Getting exceptional preds in backward analysis"
-
+  let normal_succs = W.normal_preds
+  let normal_preds = W.normal_succs
+  let exceptional_succs = W.exceptional_preds
+  let exceptional_preds = W.exceptional_succs
 end
 
 module NodeIdMap (B : Base) = Map.Make(struct

infer/src/unit/abstractInterpreterTests.ml

@@ -57,7 +57,7 @@ end
 
 
 module TestInterpreter = AnalyzerTester.Make
-    (ProcCfg.Forward)
+    (ProcCfg.Normal)
     (Scheduler.ReversePostorder)
     (PathCountDomain)
     (PathCountTransferFunctions)

infer/src/unit/addressTakenTests.ml

@@ -12,7 +12,7 @@ open! Utils
 module F = Format
 
 module TestInterpreter = AnalyzerTester.Make
-    (ProcCfg.Forward)
+    (ProcCfg.Exceptional)
     (Scheduler.ReversePostorder)
     (AddressTaken.Domain)
     (AddressTaken.TransferFunctions)

infer/src/unit/copyPropagationTests.ml

@@ -12,7 +12,7 @@ open! Utils
 module F = Format
 
 module TestInterpreter = AnalyzerTester.Make
-    (ProcCfg.Forward)
+    (ProcCfg.Exceptional)
     (Scheduler.ReversePostorder)
     (CopyPropagation.Domain)
     (CopyPropagation.TransferFunctions)

infer/src/unit/inferunit.ml

@@ -17,6 +17,7 @@ let () =
     AbstractInterpreterTests.tests;
     AddressTakenTests.tests;
     CopyPropagationTests.tests;
+    ProcCfgTests.tests;
     LivenessTests.tests;
     SchedulerTests.tests;
   ] in

infer/src/unit/livenessTests.ml

@@ -12,7 +12,7 @@ open! Utils
 module F = Format
 
 module TestInterpreter = AnalyzerTester.Make
-    (ProcCfg.Backward (ProcCfg.Forward))
+    (ProcCfg.Backward (ProcCfg.Exceptional))
     (Scheduler.ReversePostorder)
     (Liveness.Domain)
     (Liveness.TransferFunctions)

infer/src/unit/procCfgTests.ml

@@ -0,0 +1,72 @@
+(*
+ * Copyright (c) 2016 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ *)
+
+open! Utils
+
+module F = Format
+
+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 n1, n2, n3, n4 = create_node cfg, create_node cfg, create_node cfg, create_node cfg in
+  (* 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];
+  Cfg.Node.set_succs_exn cfg n2 [n4] [n3];
+  Cfg.Node.set_succs_exn cfg n3 [n4] [n4];
+
+  let normal_proc_cfg = ProcCfg.Normal.from_pdesc test_pdesc in
+  let exceptional_proc_cfg = ProcCfg.Exceptional.from_pdesc test_pdesc in
+
+  let open OUnit2 in
+  let cmp = IList.equal Cfg.Node.compare in
+  (* TODO: cleanup *)
+  let pp_diff fmt (actual, expected) =
+    let pp_node_list fmt l = F.pp_print_list 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 = [
+    (* 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]);
+    ("succs_n2", ProcCfg.Normal.succs normal_proc_cfg n2, [n4]);
+    ("normal_succs_n2", ProcCfg.Normal.normal_succs normal_proc_cfg n2, [n4]);
+    ("succs_n3", ProcCfg.Normal.succs normal_proc_cfg n3, [n4]);
+    ("normal_succs_n3", ProcCfg.Normal.normal_succs normal_proc_cfg n3, [n4]);
+    (* test the preds of the normal cfg *)
+    ("preds_n2", ProcCfg.Normal.normal_preds normal_proc_cfg n2, [n1]);
+    ("normal_preds_n2", ProcCfg.Normal.normal_preds normal_proc_cfg n2, [n1]);
+    (* we shouldn't see any exn succs or preds even though we added them *)
+    ("no_exn_succs_n1", ProcCfg.Normal.exceptional_succs normal_proc_cfg n1, []);
+    ("no_exn_preds_n3", ProcCfg.Normal.exceptional_preds normal_proc_cfg n3, []);
+
+    (* now, test the exceptional succs in the exceptional cfg. *)
+    ("exn_succs_n1", ProcCfg.Exceptional.exceptional_succs exceptional_proc_cfg n1, [n3]);
+    ("exn_succs_n2", ProcCfg.Exceptional.exceptional_succs exceptional_proc_cfg n2, [n3]);
+    ("exn_succs_n3", ProcCfg.Exceptional.exceptional_succs exceptional_proc_cfg n3, [n4]);
+    (* test exceptional pred links *)
+    ("exn_preds_n3", ProcCfg.Exceptional.exceptional_preds exceptional_proc_cfg n3, [n2; n1]);
+    (* succs should return both normal and exceptional successors *)
+    ("exn_all_succs_n1", ProcCfg.Exceptional.succs exceptional_proc_cfg n1, [n3; n2]);
+    (* but, should not return duplicates *)
+    ("exn_all_succs_n3", ProcCfg.Exceptional.succs exceptional_proc_cfg n3, [n4]);
+    (* similarly, preds should return both normal and exceptional predecessors *)
+    ("exn_all_preds_n3", ProcCfg.Exceptional.preds exceptional_proc_cfg n3, [n2; n1]);
+    ("exn_all_preds_n4", ProcCfg.Exceptional.preds exceptional_proc_cfg n4, [n3; n2]);
+    (* finally, normal_succs/normal_preds shouldn't return exceptional edges *)
+    ("exn_normal_succs_n1", ProcCfg.Exceptional.normal_succs exceptional_proc_cfg n1, [n2]);
+    ("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