Simplify abstract interpreter

Summary:
Now that we have a proper InstrNode, we can kill `instr_ids`!
Of course:
Depends on D7608526

Reviewed By: sblackshear

Differential Revision: D7618124

fbshipit-source-id: b3609cd

infer/src/absint/AbstractInterpreter.ml

@@ -63,33 +63,23 @@ struct
 
   let exec_node node astate_pre work_queue inv_map ({ProcData.pdesc} as proc_data) ~debug =
     let node_id = CFG.id node in
-    let update_inv_map pre visit_count =
+    let update_inv_map pre ~visit_count =
-      let compute_post (pre, inv_map) (instr, id_opt) =
+      let compute_post pre instr = TransferFunctions.exec_instr pre proc_data node instr in
-        let post = TransferFunctions.exec_instr pre proc_data node instr in
-        match id_opt with
-        | Some id ->
-            (post, InvariantMap.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 [] -> [(Sil.skip_instr, None)] | l -> l in
+      let instrs = match CFG.instrs node with [] -> [Sil.skip_instr] | l -> l in
       if debug then
         NodePrinter.start_session
           ~pp_name:(TransferFunctions.pp_session_name node)
           (CFG.underlying_node node) ;
-      let astate_post, inv_map_post = List.fold ~f:compute_post ~init:(pre, inv_map) instr_ids in
+      let astate_post = List.fold ~f:compute_post ~init:pre instrs in
       if debug then (
-        let instrs = List.map ~f:fst instr_ids in
         L.d_strln
           (Format.asprintf "PRE: %a@.INSTRS: %aPOST: %a@." Domain.pp pre
              (Sil.pp_instr_list Pp.(html Green))
              instrs Domain.pp astate_post) ;
         NodePrinter.finish_session (CFG.underlying_node node) ) ;
-      let inv_map'' =
+      let inv_map' = InvariantMap.add node_id {pre; post= astate_post; visit_count} inv_map in
-        InvariantMap.add node_id {pre; post= astate_post; visit_count} inv_map_post
+      (inv_map', Scheduler.schedule_succs work_queue node)
-      in
-      (inv_map'', Scheduler.schedule_succs work_queue node)
     in
     if InvariantMap.mem node_id inv_map then (
       let old_state = InvariantMap.find node_id inv_map in
@@ -106,11 +96,9 @@ struct
             "Exceeded max widening threshold %d while analyzing %a. Please check your widening \
              operator or increase the threshold"
             Config.max_widens Typ.Procname.pp (Procdesc.get_proc_name pdesc) ;
-        update_inv_map widened_pre visit_count' )
+        update_inv_map widened_pre ~visit_count:visit_count' )
-    else
+    else (* first time visiting this node *)
-      (* first time visiting this node *)
+      update_inv_map astate_pre ~visit_count:1
-      let visit_count = 1 in
-      update_inv_map astate_pre visit_count
 
 
   let rec exec_worklist cfg work_queue inv_map proc_data ~debug =

infer/src/absint/ProcCfg.ml

@@ -114,12 +114,6 @@ module type S = sig
   val instrs : node -> Sil.instr list
   (** get the instructions from a node *)
 
-  val instr_ids : node -> (Sil.instr * id option) 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 succs : t -> node -> node list
 
   val preds : t -> node -> node list
@@ -160,8 +154,6 @@ module Normal = struct
 
   let instrs = Procdesc.Node.get_instrs
 
-  let instr_ids n = List.map ~f:(fun i -> (i, None)) (instrs n)
-
   let normal_succs _ n = Procdesc.Node.get_succs n
 
   let normal_preds _ n = Procdesc.Node.get_preds n
@@ -223,8 +215,6 @@ module Exceptional = struct
 
   let instrs = Procdesc.Node.get_instrs
 
-  let instr_ids n = List.map ~f:(fun i -> (i, None)) (instrs n)
-
   let nodes (t, _) = Procdesc.get_nodes t
 
   let normal_succs _ n = Procdesc.Node.get_succs n
@@ -272,8 +262,6 @@ module Backward (Base : S) = struct
 
   let instrs n = List.rev (Base.instrs n)
 
-  let instr_ids n = List.rev (Base.instr_ids n)
-
   let succs = Base.preds
 
   let preds = Base.succs
@@ -311,15 +299,6 @@ struct
     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))

infer/src/absint/ProcCfg.mli

@@ -49,12 +49,6 @@ module type S = sig
   val instrs : node -> Sil.instr list
   (** get the instructions from a node *)
 
-  val instr_ids : node -> (Sil.instr * id option) 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 succs : t -> node -> node list
   (** all succcessors (normal and exceptional) *)
 

infer/src/unit/schedulerTests.ml

@@ -18,8 +18,6 @@ module MockNode = struct
 
   let instrs _ = []
 
-  let instr_ids _ = []
-
   let hash = Hashtbl.hash
 
   let to_instr_nodes _ = assert false