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

@@ -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 update_inv_map pre visit_count =
-      let astate_post =
+      let compute_post (pre, inv_map) (instr, id_opt) =
-        let exec_instrs astate_acc instr =
+        let post = TF.exec_instr pre proc_data node instr in
-          if A.is_bottom astate_acc
+        match id_opt with
-          then astate_acc
+        | Some id -> post, M.add id { pre; post; visit_count; } inv_map
-          else TF.exec_instr astate_acc proc_data node instr in
+        | None -> post, inv_map in
-        (* hack to ensure that the transfer functions see every node *)
+      (* hack to ensure that we call `exec_instr` on a node even if it has no instructions *)
-        let node_instrs = match CFG.instrs node with
+      let instr_ids = match CFG.instr_ids node with
         | [] ->
             (* TODO: get rid of Stackop and replace it with Skip *)
-              [Sil.Stackop (Push, Location.dummy)]
+            [Sil.Stackop (Push, Location.dummy), None]
-          | instrs -> instrs in
+        | l ->
-        IList.fold_left exec_instrs astate_pre node_instrs in
+            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
+      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
+      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 =

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
+module InstrNode = struct
-type instr_node = { node: DefaultNode.t; instr_index: instr_index; num_instrs: int; }
+  type t = Cfg.Node.t
-
+  type id = Cfg.Node.id * index
-module OneInstrNode = struct
-  type t = instr_node
-  type id = DefaultNode.id * instr_index
 
-  let instrs t =
+  let kind = Cfg.Node.get_kind
-    match DefaultNode.instrs t.node with
-    | [] -> []
-    | instrs -> [IList.nth instrs t.instr_index]
 
-  let kind t =
+  let id t = Cfg.Node.get_id t, Node_index
-    DefaultNode.kind t.node
 
-  let id t =
+  let index_compare index1 index2 = match index1, index2 with
-    DefaultNode.id t.node, t.instr_index
+    | 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 id_compare (id1, index1) (id2, index2) =
-    let n = DefaultNode.id_compare t_id1 t_id2 in
+    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) =
+  let pp_id fmt (id, index) = match index with
-    F.fprintf fmt "(%a: %d)" DefaultNode.pp_id id index
+    | 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 = Cfg.Node.t
-module OneInstrPerNode (Base : S with type node = DefaultNode.t) = struct
+                                  and type id = Cfg.Node.id) = struct
-  type t = Base.t
+  include (Base : module type of Base with type id := Cfg.Node.id and type t = Base.t)
-  type node = OneInstrNode.t
+  type id = Base.id * index
-  include (OneInstrNode : module type of OneInstrNode with type t := node)
+  include (InstrNode : module type of InstrNode with type t := node and type id := id)
-
+
-  let create_node cfg_node =
+  (* keep the invariants before/after each instruction *)
-    let num_instrs = IList.length (Base.instrs cfg_node) in
+  let instr_ids t =
-    { node = cfg_node; instr_index = 0; num_instrs; }
+    IList.mapi
-
+      (fun i instr ->
-  let create_pred_node cfg_node =
+         let id = Cfg.Node.get_id t, Instr_index i in
-    let num_instrs = IList.length (Base.instrs cfg_node) in
+         instr, Some id)
-    { node = cfg_node; instr_index = num_instrs - 1; num_instrs; }
+      (instrs t)
-
-  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
 end
 
 module NodeIdMap (CFG : S) = Map.Make(struct

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
+module InstrNode : Node with type t = Cfg.Node.t and type id = Cfg.Node.id * index
-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
 
 (** 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 node = Base.node
-     and type id = OneInstrNode.id
+     and type id = Base.id * index
 
 module NodeIdMap (CFG : S) : Map.S with type key = CFG.id
 

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

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