From cf5871e76f03b185c11a5dda067583171211d09e Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Sun, 3 Jul 2016 08:23:59 -0700 Subject: [PATCH] fixing broken backward/per-instr cfg by taking a different approach Reviewed By: jeremydubreil Differential Revision: D3461619 fbshipit-source-id: 491b28b --- infer/src/checkers/abstractInterpreter.ml | 31 ++--- infer/src/checkers/procCfg.ml | 134 ++++++++-------------- infer/src/checkers/procCfg.mli | 21 ++-- infer/src/unit/procCfgTests.ml | 55 +-------- infer/src/unit/schedulerTests.ml | 2 + 5 files changed, 77 insertions(+), 166 deletions(-) diff --git a/infer/src/checkers/abstractInterpreter.ml b/infer/src/checkers/abstractInterpreter.ml index d2485e618..2e45b01cc 100644 --- a/infer/src/checkers/abstractInterpreter.ml +++ b/infer/src/checkers/abstractInterpreter.ml @@ -55,22 +55,23 @@ module MakeNoCFG let exec_node node astate_pre work_queue inv_map proc_data = let node_id = CFG.id node in L.out "Doing analysis of node %a from pre %a@." CFG.pp_id node_id A.pp astate_pre; - let update_inv_map astate_pre visit_count = - let astate_post = - let exec_instrs astate_acc instr = - if A.is_bottom astate_acc - then astate_acc - else TF.exec_instr astate_acc proc_data node instr in - (* hack to ensure that the transfer functions see every node *) - let node_instrs = match CFG.instrs node with - | [] -> - (* TODO: get rid of Stackop and replace it with Skip *) - [Sil.Stackop (Push, Location.dummy)] - | instrs -> instrs in - IList.fold_left exec_instrs astate_pre node_instrs in + let update_inv_map pre visit_count = + let compute_post (pre, inv_map) (instr, id_opt) = + let post = TF.exec_instr pre proc_data node instr in + match id_opt with + | Some id -> post, M.add id { pre; post; visit_count; } inv_map + | None -> post, inv_map in + (* hack to ensure that we call `exec_instr` on a node even if it has no instructions *) + let instr_ids = match CFG.instr_ids node with + | [] -> + (* TODO: get rid of Stackop and replace it with Skip *) + [Sil.Stackop (Push, Location.dummy), None] + | l -> + l in + let astate_post, inv_map_post = IList.fold_left compute_post (pre, inv_map) instr_ids in L.out "Post for node %a is %a@." CFG.pp_id node_id A.pp astate_post; - let inv_map' = M.add node_id { pre=astate_pre; post=astate_post; visit_count; } inv_map in - inv_map', Sched.schedule_succs work_queue node in + let inv_map'' = M.add node_id { pre; post=astate_post; visit_count; } inv_map_post in + inv_map'', Sched.schedule_succs work_queue node in if M.mem node_id inv_map then let old_state = M.find node_id inv_map in let widened_pre = diff --git a/infer/src/checkers/procCfg.ml b/infer/src/checkers/procCfg.ml index ff3b035c7..8125741dd 100644 --- a/infer/src/checkers/procCfg.ml +++ b/infer/src/checkers/procCfg.ml @@ -15,11 +15,12 @@ module F = Format file). Defines useful wrappers that allows us to do tricks like turn a forward cfg into a backward one, or view a cfg as having a single instruction per node. *) +type index = Node_index | Instr_index of int + module type Node = sig type t type id - val instrs : t -> Sil.instr list val kind : t -> Cfg.Node.nodekind val id : t -> id val id_compare : id -> id -> int @@ -30,38 +31,34 @@ module DefaultNode = struct type t = Cfg.Node.t type id = Cfg.Node.id - let instrs = Cfg.Node.get_instrs let kind = Cfg.Node.get_kind let id = Cfg.Node.get_id let id_compare = Cfg.Node.id_compare 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 +module InstrNode = struct + type t = Cfg.Node.t + type id = Cfg.Node.id * index - let instrs t = - match DefaultNode.instrs t.node with - | [] -> [] - | instrs -> [IList.nth instrs t.instr_index] + let kind = Cfg.Node.get_kind - let kind t = - DefaultNode.kind t.node + let id t = Cfg.Node.get_id t, Node_index - let id t = - DefaultNode.id t.node, t.instr_index + let index_compare index1 index2 = match index1, index2 with + | Node_index, Node_index -> 0 + | Instr_index i1, Instr_index i2 -> int_compare i1 i2 + | Node_index, Instr_index _ -> 1 + | Instr_index _, Node_index -> -1 - let id_compare (t_id1, i_index1) (t_id2, i_index2) = - let n = DefaultNode.id_compare t_id1 t_id2 in + let id_compare (id1, index1) (id2, index2) = + let n = Cfg.Node.id_compare id1 id2 in if n <> 0 then n - else int_compare i_index1 i_index2 + else index_compare index1 index2 - let pp_id fmt (id, index) = - F.fprintf fmt "(%a: %d)" DefaultNode.pp_id id index + let pp_id fmt (id, index) = match index with + | Node_index -> Cfg.Node.pp_id fmt id + | Instr_index i -> F.fprintf fmt "(%a: %d)" Cfg.Node.pp_id id i end module type S = sig @@ -69,6 +66,13 @@ module type S = sig type node include (Node with type t := node) + (** get the instructions from a node *) + val instrs : node -> Sil.instr list + (** explode a block into its instructions and an optional id for the instruction. the purpose of + this is to specify a policy for fine-grained storage of invariants by the abstract + interpreter. the interpreter will forget invariants at program points where the id is None, + and remember them otherwise *) + val instr_ids : node -> (Sil.instr * id option) list val succs : t -> node -> node list (** all predecessors (normal and exceptional) *) val preds : t -> node -> node list @@ -93,6 +97,8 @@ module Normal = struct type node = DefaultNode.t include (DefaultNode : module type of DefaultNode with type t := node) + let instrs = Cfg.Node.get_instrs + let instr_ids n = IList.map (fun i -> i, None) (instrs n) let normal_succs _ n = Cfg.Node.get_succs n let normal_preds _ n = Cfg.Node.get_preds n (* prune away exceptional control flow *) @@ -132,6 +138,10 @@ module Exceptional = struct IList.fold_left add_exn_preds Cfg.IdMap.empty (Cfg.Procdesc.get_nodes pdesc) in pdesc, exceptional_preds + let instrs = Cfg.Node.get_instrs + + let instr_ids n = IList.map (fun i -> i, None) (instrs n) + let nodes (t, _) = Cfg.Procdesc.get_nodes t let normal_succs _ n = Cfg.Node.get_succs n @@ -175,6 +185,7 @@ end module Backward (Base : S) = struct include Base let instrs n = IList.rev (Base.instrs n) + let instr_ids n = IList.rev (Base.instr_ids n) let succs = Base.preds let preds = Base.succs @@ -186,74 +197,19 @@ 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 = - (* 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 - 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 = - (* 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) - - 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 +module OneInstrPerNode (Base : S with type node = Cfg.Node.t + and type id = Cfg.Node.id) = struct + include (Base : module type of Base with type id := Cfg.Node.id and type t = Base.t) + type id = Base.id * index + include (InstrNode : module type of InstrNode with type t := node and type id := id) + + (* keep the invariants before/after each instruction *) + let instr_ids t = + IList.mapi + (fun i instr -> + let id = Cfg.Node.get_id t, Instr_index i in + instr, Some id) + (instrs t) end module NodeIdMap (CFG : S) = Map.Make(struct diff --git a/infer/src/checkers/procCfg.mli b/infer/src/checkers/procCfg.mli index 9e9c0a04b..d9db642e6 100644 --- a/infer/src/checkers/procCfg.mli +++ b/infer/src/checkers/procCfg.mli @@ -11,11 +11,12 @@ file). Defines useful wrappers that allows us to do tricks like turn a forward cfg to into a backward one, or view a cfg as having a single instruction per block *) +type index = Node_index | Instr_index of int + module type Node = sig type t type id - val instrs : t -> Sil.instr list val kind : t -> Cfg.Node.nodekind val id : t -> id val id_compare : id -> id -> int @@ -27,6 +28,13 @@ module type S = sig type node include (Node with type t := node) + (** get the instructions from a node *) + val instrs : node -> Sil.instr list + (** explode a block into its instructions and an optional id for the instruction. the purpose of + this is to specify a policy for fine-grained storage of invariants by the abstract + interpreter. the interpreter will forget invariants at program points where the id is None, + and remember them otherwise *) + val instr_ids : node -> (Sil.instr * id option) list val succs : t -> node -> node list (** all predecessors (normal and exceptional) *) val preds : t -> node -> node list @@ -47,10 +55,7 @@ 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 +module InstrNode : Node with type t = Cfg.Node.t and type id = Cfg.Node.id * index (** Forward CFG with no exceptional control-flow *) module Normal : S with type t = Cfg.Procdesc.t @@ -67,10 +72,10 @@ 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) : +module OneInstrPerNode (Base : S with type node = DefaultNode.t and type id = DefaultNode.id) : S with type t = Base.t - and type node = OneInstrNode.t - and type id = OneInstrNode.id + and type node = Base.node + and type id = Base.id * index module NodeIdMap (CFG : S) : Map.S with type key = CFG.id diff --git a/infer/src/unit/procCfgTests.ml b/infer/src/unit/procCfgTests.ml index fa9cc2245..638d0f146 100644 --- a/infer/src/unit/procCfgTests.ml +++ b/infer/src/unit/procCfgTests.ml @@ -41,61 +41,8 @@ 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 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_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_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_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 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_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 - let cmp l1 l2 = let sort = IList.sort Cfg.Node.compare in IList.equal Cfg.Node.compare (sort l1) (sort l2) in @@ -138,5 +85,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 - let tests = instr_cfg_test :: normal_exceptional_tests in + let tests = normal_exceptional_tests in "procCfgSuite">:::tests diff --git a/infer/src/unit/schedulerTests.ml b/infer/src/unit/schedulerTests.ml index f2fb6efea..939f32011 100644 --- a/infer/src/unit/schedulerTests.ml +++ b/infer/src/unit/schedulerTests.ml @@ -19,6 +19,8 @@ module MockNode = struct type id = int let instrs _ = [] + let instr_ids _ = [] + let to_instr_nodes _ = assert false let id n = n let kind _ = Cfg.Node.Stmt_node "" let id_compare = int_compare