diff --git a/infer/src/IR/Procdesc.mli b/infer/src/IR/Procdesc.mli index 7734af750..35c602d54 100644 --- a/infer/src/IR/Procdesc.mli +++ b/infer/src/IR/Procdesc.mli @@ -139,9 +139,6 @@ val did_preanalysis : t -> bool val fold_instrs : t -> init:'accum -> f:('accum -> Node.t -> Sil.instr -> 'accum) -> 'accum (** fold over all nodes and their instructions *) -val fold_nodes : t -> init:'accum -> f:('accum -> Node.t -> 'accum) -> 'accum -(** fold over all nodes *) - val from_proc_attributes : ProcAttributes.t -> t (** Use [Cfg.create_proc_desc] if you are adding a proc desc to a cfg *) diff --git a/infer/src/absint/ProcCfg.ml b/infer/src/absint/ProcCfg.ml index 93f4e1ce2..31338b4f3 100644 --- a/infer/src/absint/ProcCfg.ml +++ b/infer/src/absint/ProcCfg.ml @@ -14,8 +14,6 @@ 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 [@@deriving compare] - module type Node = sig type t @@ -31,6 +29,8 @@ module type Node = sig val underlying_node : t -> Procdesc.Node.t + val of_underlying_node : Procdesc.Node.t -> t + val compare_id : id -> id -> int val pp_id : F.formatter -> id -> unit @@ -55,6 +55,8 @@ module DefaultNode = struct let underlying_node t = t + let of_underlying_node t = t + let compare_id = Procdesc.Node.compare_id let pp_id = Procdesc.Node.pp_id @@ -72,34 +74,23 @@ module DefaultNode = struct end module InstrNode = struct - type t = Procdesc.Node.t - - type id = Procdesc.Node.id * index + type t = Procdesc.Node.t * int - let kind = Procdesc.Node.get_kind - - let underlying_node t = t + type id = Procdesc.Node.id * int [@@deriving compare] - let id t = (Procdesc.Node.get_id (underlying_node t), Node_index) - - let hash node = Hashtbl.hash (id node) + let kind (t, _) = Procdesc.Node.get_kind t - let loc t = Procdesc.Node.get_loc t + let underlying_node (t, _) = t - let compare_index = compare_index + let of_underlying_node t = (t, 0) - let compare_id (id1, index1) (id2, index2) = - let n = Procdesc.Node.compare_id id1 id2 in - if n <> 0 then n else compare_index index1 index2 + let id (t, index) = (Procdesc.Node.get_id t, index) + let hash node = Hashtbl.hash (id node) - let pp_id fmt (id, index) = - match index with - | Node_index -> - Procdesc.Node.pp_id fmt id - | Instr_index i -> - F.fprintf fmt "(%a: %d)" Procdesc.Node.pp_id id i + let loc (t, _) = Procdesc.Node.get_loc t + let pp_id fmt (id, index) = F.fprintf fmt "(%a: %d)" Procdesc.Node.pp_id id index module OrderedId = struct type t = id @@ -302,15 +293,11 @@ end module OneInstrPerNode (Base : S with type node = Procdesc.Node.t and type id = Procdesc.Node.id) = struct - include ( - Base : - module type of Base - with type id := Procdesc.Node.id - and type t = Base.t - and module IdMap := Base.IdMap - and module IdSet := Base.IdSet ) + type t = Base.t + + type node = InstrNode.t - type id = Base.id * index + type id = InstrNode.id include ( InstrNode : @@ -320,13 +307,67 @@ struct and module IdMap = InstrNode.IdMap and module IdSet = InstrNode.IdSet ) - (* keep the invariants before/after each instruction *) - let instr_ids t = - List.mapi - ~f:(fun i instr -> - let id = (Procdesc.Node.get_id t, Instr_index i) in - (instr, Some id) ) - (instrs t) + let instrs (node, index) = + match Base.instrs node with [] -> [] | instrs -> [List.nth_exn instrs index] + + + let instr_ids (node, index) = + match Base.instr_ids node with + | [] -> + [] + | instr_ids -> + let instr, id_opt = List.nth_exn instr_ids index in + [(instr, Option.map id_opt ~f:(fun base_id -> (base_id, index)))] + + + let first_of_node node = (node, 0) + + let last_of_node node = (node, max 0 (List.length (Base.instrs node) - 1)) + + let normal_succs _ _ = (* not used *) assert false + + let exceptional_succs _ _ = (* not used *) assert false + + let list_mem_nth list index = List.drop list index |> List.is_empty |> not + + let succs cfg (node, index) = + let succ_index = index + 1 in + if list_mem_nth (Base.instrs node) succ_index then [(node, succ_index)] + else List.map ~f:first_of_node (Base.succs cfg node) + + + let normal_preds cfg (node, index) = + if index >= 1 then [(node, index - 1)] + else List.map ~f:last_of_node (Base.normal_preds cfg node) + + + (* HACK: Use first_of_node instead of last_of_node because it is used to get the pre only *) + let exceptional_preds cfg (node, index) = + if index >= 1 then [] else List.map ~f:first_of_node (Base.exceptional_preds cfg node) + + + let preds cfg t = List.rev_append (exceptional_preds cfg t) (normal_preds cfg t) + + let start_node cfg = first_of_node (Base.start_node cfg) + + let exit_node cfg = last_of_node (Base.exit_node cfg) + + let proc_desc = Base.proc_desc + + let nodes = + let nodes_of_node node = + match Base.instrs node with + | [] -> + [(node, 0)] + | instrs -> + List.mapi ~f:(fun index _instr -> (node, index)) instrs + in + fun cfg -> List.concat_map ~f:nodes_of_node (Base.nodes cfg) + + + let from_pdesc = Base.from_pdesc + + let is_loop_head pdesc = function node, 0 -> Base.is_loop_head pdesc node | _ -> false end module NormalOneInstrPerNode = OneInstrPerNode (Normal) diff --git a/infer/src/absint/ProcCfg.mli b/infer/src/absint/ProcCfg.mli index 5d4c36149..07d9712df 100644 --- a/infer/src/absint/ProcCfg.mli +++ b/infer/src/absint/ProcCfg.mli @@ -13,8 +13,6 @@ open! IStd 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 @@ -30,6 +28,8 @@ module type Node = sig val underlying_node : t -> Procdesc.Node.t + val of_underlying_node : Procdesc.Node.t -> t + val compare_id : id -> id -> int val pp_id : Format.formatter -> id -> unit @@ -88,7 +88,7 @@ end module DefaultNode : Node with type t = Procdesc.Node.t and type id = Procdesc.Node.id -module InstrNode : Node with type t = Procdesc.Node.t and type id = Procdesc.Node.id * index +module InstrNode : Node with type t = Procdesc.Node.t * int and type id = Procdesc.Node.id * int (** Forward CFG with no exceptional control-flow *) module Normal : @@ -107,7 +107,7 @@ module Backward (Base : S) : S with type t = Base.t and type node = Base.node an module OneInstrPerNode (Base : S with type node = DefaultNode.t and type id = DefaultNode.id) : S with type t = Base.t - and type node = Base.node + and type node = InstrNode.t and type id = InstrNode.id and module IdMap = InstrNode.IdMap and module IdSet = InstrNode.IdSet diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 2f10471f4..172295f35 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -330,17 +330,17 @@ module Report = struct * of a procedure (no more significant instruction) * or of a block (goes directly to a node with multiple predecessors) *) - let rec is_end_of_block_or_procedure node rem_instrs = + let rec is_end_of_block_or_procedure (cfg: CFG.t) node rem_instrs = List.for_all rem_instrs ~f:non_significant_instr && - match Procdesc.Node.get_succs node with + match CFG.succs cfg node with | [] -> true | [succ] -> ( - is_end_of_block_or_procedure succ (CFG.instrs succ) + is_end_of_block_or_procedure cfg succ (CFG.instrs succ) || - match Procdesc.Node.get_preds succ with + match CFG.preds cfg succ with | _ :: _ :: _ -> true (* [succ] is a join, i.e. [node] is the end of a block *) | _ -> @@ -349,7 +349,7 @@ module Report = struct false end - let check_unreachable_code summary tenv node instr rem_instrs mem = + let check_unreachable_code summary tenv (cfg: CFG.t) (node: CFG.node) instr rem_instrs mem = match mem with | NonBottom _ -> () @@ -359,13 +359,16 @@ module Report = struct () | Sil.Prune (cond, location, true_branch, _) -> let i = match cond with Exp.Const (Const.Cint i) -> i | _ -> IntLit.zero in - let desc = Errdesc.explain_condition_always_true_false tenv i cond node location in + let desc = + Errdesc.explain_condition_always_true_false tenv i cond (CFG.underlying_node node) + location + in let exn = Exceptions.Condition_always_true_false (desc, not true_branch, __POS__) in Reporting.log_warning summary ~loc:location exn (* special case for `exit` when we're at the end of a block / procedure *) | Sil.Call (_, Const (Cfun pname), _, _, _) when String.equal (Typ.Procname.get_method pname) "exit" - && ExitStatement.is_end_of_block_or_procedure node rem_instrs -> + && ExitStatement.is_end_of_block_or_procedure cfg node rem_instrs -> () | _ -> let location = Sil.instr_get_loc instr in @@ -479,36 +482,37 @@ module Report = struct let rec check_instrs - : Specs.summary -> extras ProcData.t -> CFG.node -> Sil.instr list -> Dom.Mem.astate + : Specs.summary -> extras ProcData.t -> CFG.t -> CFG.node -> Sil.instr list -> Dom.Mem.astate -> PO.ConditionSet.t -> PO.ConditionSet.t = - fun summary ({tenv} as pdata) node instrs mem cond_set -> + fun summary ({tenv} as pdata) cfg node instrs mem cond_set -> match (mem, instrs) with | _, [] | Bottom, _ -> cond_set | NonBottom _, instr :: rem_instrs -> let cond_set = check_instr pdata node instr mem cond_set in let mem = Analyzer.TransferFunctions.exec_instr mem pdata node instr in - let () = check_unreachable_code summary tenv node instr rem_instrs mem in + let () = check_unreachable_code summary tenv cfg node instr rem_instrs mem in print_debug_info instr mem cond_set ; - check_instrs summary pdata node rem_instrs mem cond_set + check_instrs summary pdata cfg node rem_instrs mem cond_set let check_node - : Specs.summary -> extras ProcData.t -> Analyzer.invariant_map -> PO.ConditionSet.t + : Specs.summary -> extras ProcData.t -> CFG.t -> Analyzer.invariant_map -> PO.ConditionSet.t -> CFG.node -> PO.ConditionSet.t = - fun summary pdata inv_map cond_set node -> + fun summary pdata cfg inv_map cond_set node -> match Analyzer.extract_pre (CFG.id node) inv_map with | Some mem -> let instrs = CFG.instrs node in - check_instrs summary pdata node instrs mem cond_set + check_instrs summary pdata cfg node instrs mem cond_set | _ -> cond_set let check_proc - : Specs.summary -> extras ProcData.t -> Analyzer.invariant_map -> PO.ConditionSet.t = - fun summary ({pdesc} as pdata) inv_map -> - Procdesc.fold_nodes pdesc ~f:(check_node summary pdata inv_map) ~init:PO.ConditionSet.empty + : Specs.summary -> extras ProcData.t -> CFG.t -> Analyzer.invariant_map -> PO.ConditionSet.t = + fun summary pdata cfg inv_map -> + CFG.nodes cfg + |> List.fold ~f:(check_node summary pdata cfg inv_map) ~init:PO.ConditionSet.empty let make_err_trace : Trace.t -> string -> Errlog.loc_trace = @@ -578,7 +582,9 @@ let compute_post let inv_map = Analyzer.exec_pdesc ~initial:Dom.Mem.init pdata in let entry_mem = extract_post inv_map (CFG.start_node cfg) in let exit_mem = extract_post inv_map (CFG.exit_node cfg) in - let cond_set = Report.check_proc summary pdata inv_map |> Report.report_errors summary pdesc in + let cond_set = + Report.check_proc summary pdata cfg inv_map |> Report.report_errors summary pdesc + in match (entry_mem, exit_mem) with | Some entry_mem, Some exit_mem -> Some (entry_mem, exit_mem, cond_set) diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index 93fab9211..489e91d64 100644 --- a/infer/src/checkers/cost.ml +++ b/infer/src/checkers/cost.ml @@ -68,7 +68,7 @@ module TransferFunctionsNodesBasicCost (CFG : ProcCfg.S) = struct {ProcData.pdesc} (node: CFG.node) instr : CostDomain.NodeInstructionToCostMap.astate = let nid_int = Procdesc.Node.get_id (CFG.underlying_node node) in let instr_idx = instr_idx node instr in - let key = (nid_int, ProcCfg.Instr_index instr_idx) in + let key = (nid_int, instr_idx) in let astate' = match instr with | Sil.Call (_, Exp.Const (Const.Cfun callee_pname), _, _, _) -> ( diff --git a/infer/src/checkers/liveness.ml b/infer/src/checkers/liveness.ml index ee81e4176..1a3f10d1f 100644 --- a/infer/src/checkers/liveness.ml +++ b/infer/src/checkers/liveness.ml @@ -200,14 +200,11 @@ let checker {Callbacks.tenv; summary; proc_desc} : Specs.summary = | None -> VarSet.empty in - List.iter (CFG.instr_ids node) ~f:(fun (instr, node_id_opt) -> - match node_id_opt with - | Some node_id -> ( - match Analyzer.extract_pre node_id invariant_map with - | Some live_vars -> - report_dead_store live_vars captured_by_ref_vars instr - | None -> - () ) + let node_id = CFG.id node in + List.iter (CFG.instrs node) ~f:(fun instr -> + match Analyzer.extract_pre node_id invariant_map with + | Some live_vars -> + report_dead_store live_vars captured_by_ref_vars instr | None -> () ) in diff --git a/infer/src/unit/procCfgTests.ml b/infer/src/unit/procCfgTests.ml index f7c964765..a6626761d 100644 --- a/infer/src/unit/procCfgTests.ml +++ b/infer/src/unit/procCfgTests.ml @@ -66,28 +66,36 @@ let tests = assert_bool "Second instr should be dummy_instr1" (phys_equal instr2 dummy_instr1) | _ -> assert_failure "Expected exactly two instructions" ) ; - (let node_id, _ = InstrCfg.id n1 in - match InstrCfg.instr_ids n1 with - | [(instr1, Some (id1, ProcCfg.Instr_index 0)); (instr2, Some (id2, ProcCfg.Instr_index 1))] -> - assert_bool "First instr should be dummy_instr1" (phys_equal instr1 dummy_instr1) ; - assert_bool "Second instr should be dummy_instr2" (phys_equal instr2 dummy_instr2) ; - assert_bool "id1 should be id of underlying node" (phys_equal id1 node_id) ; - assert_bool "id2 should be id of underlying node" (phys_equal id2 node_id) - | _ -> - assert_failure "Expected exactly two instructions with correct indices") ; - let backward_node_id, _ = BackwardInstrCfg.id n1 in - ( match BackwardInstrCfg.instr_ids n1 with - | [(instr1, Some (id1, ProcCfg.Instr_index 1)); (instr2, Some (id2, ProcCfg.Instr_index 0))] -> - assert_bool "First instr should be dummy_instr2" (phys_equal instr1 dummy_instr2) ; - assert_bool "Second instr should be dummy_instr1" (phys_equal instr2 dummy_instr1) ; - assert_bool "id1 should be id of underlying node" (phys_equal id1 backward_node_id) ; - assert_bool "id2 should be id of underlying node" (phys_equal id2 backward_node_id) + let instr_n1 = InstrCfg.of_underlying_node n1 in + ( match InstrCfg.instrs instr_n1 with + | [instr] -> + assert_bool "Only instr should be dummy_instr1" (phys_equal instr dummy_instr1) + | _ -> + assert_failure "Expected exactly one instruction" ) ; + let n1' = InstrCfg.underlying_node instr_n1 in + assert_bool "underlying_node should return node of underlying CFG type" (phys_equal n1 n1') ; + let backward_instr_n1 = BackwardInstrCfg.of_underlying_node n1 in + ( match BackwardInstrCfg.instrs backward_instr_n1 with + | [instr] -> + assert_bool "Only instr should be dummy_instr1" (phys_equal instr dummy_instr1) | _ -> - assert_failure "Expected exactly two instructions with correct indices" ) ; - assert_bool "underlying_node should return node of underlying CFG type" - (Procdesc.Node.equal_id - (Procdesc.Node.get_id (BackwardInstrCfg.underlying_node n1)) - (BackwardCfg.id n1)) + assert_failure "Expected exactly one instruction" ) ; + let n1'' = BackwardInstrCfg.underlying_node backward_instr_n1 in + assert_bool "underlying_node should return node of underlying CFG type" (phys_equal n1 n1'') ; + (* test the preds/succs using backward + instr cfg *) + let check_backward_instr_ f backward_instr_node expected_instrs = + match f backward_instr_proc_cfg backward_instr_node with + | [n] -> + assert_equal (BackwardInstrCfg.instrs n) expected_instrs + | _ -> + assert_failure "Expected exactly one node" + in + check_backward_instr_ BackwardInstrCfg.preds backward_instr_n1 [dummy_instr2] ; + let backward_instr_n2 = BackwardInstrCfg.of_underlying_node n2 in + check_backward_instr_ BackwardInstrCfg.preds backward_instr_n2 [] ; + let backward_instr_n3 = BackwardInstrCfg.of_underlying_node n3 in + check_backward_instr_ BackwardInstrCfg.preds backward_instr_n3 [] ; + check_backward_instr_ BackwardInstrCfg.normal_succs backward_instr_n2 [dummy_instr2] in "instr_test" >:: instr_test_ in @@ -106,41 +114,18 @@ let tests = ; ("normal_succs_n2_bw", BackwardCfg.normal_preds backward_proc_cfg n2, [n4]) ; ("succs_n3_bw", BackwardCfg.preds backward_proc_cfg n3, [n4]) ; ("normal_succs_n3_bw", BackwardCfg.normal_preds backward_proc_cfg n3, [n4]) - ; (* ...and make sure it all works when using backward + instr cfg *) - ("succs_n1_bw_instrcfg", BackwardInstrCfg.preds backward_instr_proc_cfg n1, [n2]) - ; ( "normal_succs_n1_bw_instrcfg" - , BackwardInstrCfg.normal_preds backward_instr_proc_cfg n1 - , [n2] ) - ; ("succs_n2_bw_instrcfg", BackwardInstrCfg.preds backward_instr_proc_cfg n2, [n4]) - ; ( "normal_succs_n2_bw_instrcfg" - , BackwardInstrCfg.normal_preds backward_instr_proc_cfg n2 - , [n4] ) - ; ("succs_n3_bw_instrcfg", BackwardInstrCfg.preds backward_instr_proc_cfg n3, [n4]) - ; ( "normal_succs_n3_bw_instrcfg" - , BackwardInstrCfg.normal_preds backward_instr_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]) ; (* ...and the backward cfg... *) ("preds_n2_bw", BackwardCfg.normal_succs backward_proc_cfg n2, [n1]) ; ("normal_preds_n2_bw", BackwardCfg.normal_succs backward_proc_cfg n2, [n1]) - ; (* ...and again make sure it works with backward + instr cfg *) - ("preds_n2_bw_instr", BackwardInstrCfg.normal_succs backward_instr_proc_cfg n2, [n1]) - ; ("normal_preds_n2_bw_instr", BackwardInstrCfg.normal_succs backward_instr_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, []) ; (* same in the backward cfg *) ("no_exn_succs_n1_bw", BackwardCfg.exceptional_preds backward_proc_cfg n1, []) ; ("no_exn_preds_n3_bw", BackwardCfg.exceptional_succs backward_proc_cfg n3, []) - ; (* same in backward + instr cfg *) - ( "no_exn_succs_n1_bw_instr" - , BackwardInstrCfg.exceptional_preds backward_instr_proc_cfg n1 - , [] ) - ; ( "no_exn_preds_n3_bw_instr" - , BackwardInstrCfg.exceptional_succs backward_instr_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]) diff --git a/infer/src/unit/schedulerTests.ml b/infer/src/unit/schedulerTests.ml index f7862888a..a743f40f5 100644 --- a/infer/src/unit/schedulerTests.ml +++ b/infer/src/unit/schedulerTests.ml @@ -30,6 +30,8 @@ module MockNode = struct let underlying_node _ = assert false + let of_underlying_node _ = assert false + let kind _ = Procdesc.Node.Stmt_node "" let compare_id = Int.compare