diff --git a/infer/src/checkers/addressTaken.ml b/infer/src/checkers/addressTaken.ml index 754eedc20..0cf7ba8a6 100644 --- a/infer/src/checkers/addressTaken.ml +++ b/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) diff --git a/infer/src/checkers/annotationReachability.ml b/infer/src/checkers/annotationReachability.ml index 91316f96c..b1fca8b6e 100644 --- a/infer/src/checkers/annotationReachability.ml +++ b/infer/src/checkers/annotationReachability.ml @@ -283,7 +283,7 @@ end module Analyzer = AbstractInterpreter.Make - (ProcCfg.Forward) + (ProcCfg.Exceptional) (Scheduler.ReversePostorder) (Domain) (TransferFunctions) diff --git a/infer/src/checkers/copyPropagation.ml b/infer/src/checkers/copyPropagation.ml index efb21b044..a501b8bf0 100644 --- a/infer/src/checkers/copyPropagation.ml +++ b/infer/src/checkers/copyPropagation.ml @@ -121,7 +121,7 @@ end module Analyzer = AbstractInterpreter.Make - (ProcCfg.Forward) + (ProcCfg.Exceptional) (Scheduler.ReversePostorder) (Domain) (TransferFunctions) diff --git a/infer/src/checkers/liveness.ml b/infer/src/checkers/liveness.ml index a37900ac8..5fe1f0913 100644 --- a/infer/src/checkers/liveness.ml +++ b/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) diff --git a/infer/src/checkers/procCfg.ml b/infer/src/checkers/procCfg.ml index 5cc03a0c7..20536b3a8 100644 --- a/infer/src/checkers/procCfg.ml +++ b/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 diff --git a/infer/src/unit/abstractInterpreterTests.ml b/infer/src/unit/abstractInterpreterTests.ml index 1a3faa67e..d1e43714a 100644 --- a/infer/src/unit/abstractInterpreterTests.ml +++ b/infer/src/unit/abstractInterpreterTests.ml @@ -57,7 +57,7 @@ end module TestInterpreter = AnalyzerTester.Make - (ProcCfg.Forward) + (ProcCfg.Normal) (Scheduler.ReversePostorder) (PathCountDomain) (PathCountTransferFunctions) diff --git a/infer/src/unit/addressTakenTests.ml b/infer/src/unit/addressTakenTests.ml index 8b3f05da2..2a7e91210 100644 --- a/infer/src/unit/addressTakenTests.ml +++ b/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) diff --git a/infer/src/unit/copyPropagationTests.ml b/infer/src/unit/copyPropagationTests.ml index e8238e32b..97aaf10cc 100644 --- a/infer/src/unit/copyPropagationTests.ml +++ b/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) diff --git a/infer/src/unit/inferunit.ml b/infer/src/unit/inferunit.ml index 36854d337..9d5f58cbf 100644 --- a/infer/src/unit/inferunit.ml +++ b/infer/src/unit/inferunit.ml @@ -17,6 +17,7 @@ let () = AbstractInterpreterTests.tests; AddressTakenTests.tests; CopyPropagationTests.tests; + ProcCfgTests.tests; LivenessTests.tests; SchedulerTests.tests; ] in diff --git a/infer/src/unit/livenessTests.ml b/infer/src/unit/livenessTests.ml index 4d1486f95..080049112 100644 --- a/infer/src/unit/livenessTests.ml +++ b/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) diff --git a/infer/src/unit/procCfgTests.ml b/infer/src/unit/procCfgTests.ml new file mode 100644 index 000000000..c2c769beb --- /dev/null +++ b/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