Real InstrNode

Reviewed By: sblackshear

Differential Revision: D7608526

fbshipit-source-id: e68b596

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

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)

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

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)

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), _, _, _) -> (

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

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

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