diff --git a/lib/analysis/dune b/lib/analysis/dune
index f9fec8f..e3ac0ed 100644
--- a/lib/analysis/dune
+++ b/lib/analysis/dune
@@ -2,7 +2,13 @@
  (public_name bincaml.analysis)
  (name analysis)
  (flags -w -27)
- (modules dataflow_graph intra_analysis defuse_bool lattice_types)
+ (modules
+  dataflow_graph
+  intra_analysis
+  defuse_bool
+  lattice_types
+  ide
+  ide_live)
  (libraries
   patricia-tree
   loader
diff --git a/lib/analysis/ide.ml b/lib/analysis/ide.ml
new file mode 100644
index 0000000..7a872e7
--- /dev/null
+++ b/lib/analysis/ide.ml
@@ -0,0 +1,766 @@
+(** IDE solver *)
+
+open Lang
+open Containers
+open Common
+
+(* TODO (perf)
+   Nop edges create duplicate states that are redundant (we store the same
+   state before and after the edge). It may be more efficient to collapse these
+   edges somehow. I suspect this won't give a huge performance improvement since
+   mose of the time in the solver is spent on evaluating transfer functions. *)
+(* TODO write a sample forwards analysis to test forwards correctness *)
+
+module Loc = struct
+  type stmt_id = { proc_id : ID.t; block : ID.t; offset : int }
+  [@@deriving eq, ord, show { with_path = false }]
+
+  type t =
+    | IntraVertex of { proc_id : ID.t; v : Procedure.Vert.t }
+    | CallSite of stmt_id
+    | AfterCall of stmt_id
+    | Entry
+    | Exit
+  [@@deriving eq, ord, show]
+
+  let hash = Hashtbl.hash
+end
+
+type ret_info = {
+  rhs : (Var.t * Expr.BasilExpr.t) list;
+  lhs : (Var.t * Var.t) list;
+  call_from : Program.stmt; (* stmt must be variable Instr_Call*)
+  caller : ID.t;
+  callee : ID.t;
+}
+[@@deriving eq, ord, show { with_path = false }]
+(** (target.formal_in, rhs arg) assignment to call formal params *)
+
+type call_info = {
+  rhs : (Var.t * Expr.BasilExpr.t) list;
+  lhs : (Var.t * Var.t) list;
+  call_from : Program.stmt; (* stmt must be variable Instr_Call*)
+  aftercall : Loc.stmt_id;
+  caller : ID.t;
+  callee : ID.t;
+  ret : ret_info;
+}
+[@@deriving eq, ord, show { with_path = false }]
+(** (target.formal_in, rhs arg) assignment to call formal params *)
+
+type stub_info = { formal_in : Var.t list; globals : Var.t list }
+[@@deriving eq, ord, show { with_path = false }]
+
+module LSet = Set.Make (Loc)
+module LM = Map.Make (Loc)
+
+module type Lattice = sig
+  include ORD_TYPE
+
+  val join : t -> t -> t
+  val bottom : t
+end
+
+module DL = struct
+  (* TODO not Var.t (want more generality e.g. dsa uses symbolic addresses in scala code) *)
+  type t = Label of Var.t | Lambda [@@deriving eq, ord, show]
+end
+
+module DlMap = Map.Make (DL)
+
+type 'a state_update = (DL.t * 'a) Iter.t
+
+(** An IDE domain where values are edge functions *)
+module type IDEDomain = sig
+  include Lattice
+
+  val direction : [ `Forwards | `Backwards ]
+  (** The direction this analysis should be performed in *)
+
+  module Value : Lattice
+  (** The underlying lattice the edge functions operate on *)
+
+  val identity : t
+  (** identity edge function *)
+
+  val compose : t -> t -> t
+  (** the composite of edge functions *)
+
+  val eval : t -> Value.t -> Value.t
+  (** evaluate an edge function *)
+
+  val transfer_call : call_info -> DL.t -> t state_update
+  (** edge calling a procedure (to the return block when backwards) *)
+
+  val transfer_return : ret_info -> DL.t -> t state_update
+  (** edge return from a call (from the entry block when backwards) *)
+
+  val transfer_call_to_aftercall : call_info -> DL.t -> t state_update
+  (** edge from a call to its aftercall statement (or reversed when backwards)
+  *)
+
+  val transfer_stub : stub_info -> DL.t -> t state_update
+  (** edge from entry to exit (or reversed when backwards) of stub procedure *)
+
+  val transfer : Program.stmt -> DL.t -> t state_update
+  (** update the state for a program statement *)
+end
+
+module IDEGraph = struct
+  module Vert = struct
+    include Loc
+  end
+
+  open Vert
+
+  module Edge = struct
+    type t =
+      | Stmts of Var.t Block.phi list * Program.stmt list
+      | InterCall of call_info
+      | InterReturn of ret_info
+      | Call of call_info
+      | StubProc of stub_info
+      | Nop
+    [@@deriving eq, ord, show]
+
+    let default = Nop
+  end
+
+  module StmtLabel = struct
+    type 'a t = 'a Iter.t
+  end
+
+  module G = Graph.Imperative.Digraph.ConcreteBidirectionalLabeled (Vert) (Edge)
+  module GB = Graph.Builder.I (G)
+
+  type t = {
+    prog : Program.t;
+    callgraph : Program.CallGraph.G.t;
+    vertices : Loc.t Iter.t Lazy.t;
+  }
+
+  type bstate = {
+    graph : G.t;
+    last_vert : Loc.t;
+    stmts : Var.t Block.phi list * Program.stmt list;
+  }
+
+  let add_edge_e_dir dir g (v1, e, v2) =
+    match dir with
+    | `Forwards -> GB.add_edge_e g (v1, e, v2)
+    | `Backwards -> GB.add_edge_e g (v2, e, v1)
+
+  let push_edge dir (ending : Loc.t) (g : bstate) =
+    match g with
+    | { graph; last_vert; stmts } ->
+        let phi, stmts = (fst stmts, List.rev (snd stmts)) in
+        let e1 = (last_vert, Edge.Stmts (phi, stmts), ending) in
+        {
+          graph = add_edge_e_dir `Forwards graph e1;
+          stmts = ([], []);
+          last_vert = ending;
+        }
+
+  let add_call dir p (st : bstate) (origin : stmt_id) (callstmt : Program.stmt)
+      =
+    let lhs, rhs, target =
+      match callstmt with
+      | Stmt.(Instr_Call { lhs; procid; args }) ->
+          let target_proc = Program.proc p procid in
+          let formal_in =
+            Procedure.formal_in_params target_proc |> StringMap.to_iter
+          in
+          let actual_in = args |> StringMap.to_iter in
+          let actual_rhs =
+            Iter.join_by fst fst
+              ~merge:(fun id a b -> Some (snd a, snd b))
+              formal_in actual_in
+            |> Iter.to_list
+          in
+          let formal_out =
+            Procedure.formal_out_params target_proc |> StringMap.to_iter
+          in
+          let actual_out = lhs |> StringMap.to_iter in
+          let actual_lhs =
+            Iter.join_by fst fst
+              ~merge:(fun id a b -> Some (snd a, snd b))
+              actual_out formal_out
+            |> Iter.to_list
+          in
+          (actual_lhs, actual_rhs, procid)
+      | _ -> failwith "not a call"
+    in
+    let caller, callee = (origin.proc_id, target) in
+    let g = push_edge dir (CallSite origin) st in
+    let graph = g.graph in
+    let call_entry = IntraVertex { proc_id = target; v = Entry } in
+    let call_return = IntraVertex { proc_id = target; v = Return } in
+    let call_entry, call_return =
+      match dir with
+      | `Forwards -> (call_entry, call_return)
+      | `Backwards -> (call_return, call_entry)
+    in
+    let ret_info = { lhs; rhs; call_from = callstmt; caller; callee } in
+    let call_info =
+      {
+        rhs;
+        lhs;
+        call_from = callstmt;
+        aftercall = origin;
+        caller;
+        callee;
+        ret = ret_info;
+      }
+    in
+    let graph =
+      GB.add_edge_e graph (CallSite origin, InterCall call_info, call_entry)
+    in
+    let graph =
+      GB.add_edge_e graph (CallSite origin, Call call_info, AfterCall origin)
+    in
+    let graph =
+      GB.add_edge_e graph (call_return, InterReturn ret_info, AfterCall origin)
+    in
+    { g with graph; last_vert = AfterCall origin }
+
+  let proc_graph prog g p dir =
+    let proc_id = Procedure.id p in
+    let add_block_edge b graph =
+      match b with
+      | v1, Procedure.Edge.Jump, v2 ->
+          add_edge_e_dir dir g
+            Loc.
+              ( IntraVertex { proc_id; v = v1 },
+                Nop,
+                IntraVertex { proc_id; v = v2 } )
+      | ( Procedure.Vert.Begin block,
+          Procedure.Edge.Block b,
+          Procedure.Vert.End b2 ) ->
+          assert (ID.equal b2 block);
+          let is =
+            {
+              graph;
+              last_vert =
+                IntraVertex
+                  {
+                    proc_id;
+                    v =
+                      (match dir with
+                      | `Forwards -> Begin block
+                      | `Backwards -> End block);
+                  };
+              stmts = (b.phis, []);
+            }
+          in
+          (match dir with
+            | `Forwards -> Block.stmts_iter_i b
+            | `Backwards -> Block.stmts_iter_i b |> Iter.rev)
+          |> Iter.fold
+               (fun st (i, s) ->
+                 let stmt_id : Loc.stmt_id = { proc_id; block; offset = i } in
+                 match s with
+                 | Stmt.Instr_Call _ as c -> add_call dir prog st stmt_id c
+                 | stmt ->
+                     { st with stmts = (fst st.stmts, stmt :: snd st.stmts) })
+               is
+          |> push_edge dir
+               (IntraVertex
+                  {
+                    proc_id;
+                    v =
+                      (match dir with
+                      | `Forwards -> End block
+                      | `Backwards -> Begin block);
+                  })
+          |> fun x -> x.graph
+      | _, _, _ -> failwith "bad proc edge"
+    in
+    (* add all vertices *)
+    (* TODO: missing stub procedure edges *)
+    let intra_verts =
+      Option.to_iter (Procedure.graph p)
+      |> Iter.flat_map (fun graph ->
+          Procedure.G.fold_vertex
+            (fun v acc -> Iter.cons (Loc.IntraVertex { proc_id; v }) acc)
+            graph Iter.empty)
+    in
+    let g = Iter.fold GB.add_vertex g intra_verts in
+    let g =
+      if Option.equal ID.equal prog.entry_proc (Some proc_id) then
+        add_edge_e_dir dir g (Entry, Nop, IntraVertex { proc_id; v = Entry })
+        |> fun g ->
+        add_edge_e_dir dir g (IntraVertex { proc_id; v = Return }, Nop, Exit)
+      else g
+    in
+    Procedure.graph p
+    |> Option.map (fun procg -> Procedure.G.fold_edges_e add_block_edge procg g)
+    |> Option.get_or
+         ~default:
+           (let formal_in =
+              Procedure.formal_in_params p |> StringMap.to_list |> List.map snd
+            in
+            let globals = prog.globals |> Hashtbl.to_list |> List.map snd in
+            add_edge_e_dir dir g
+              ( IntraVertex { proc_id; v = Entry },
+                StubProc { formal_in; globals },
+                IntraVertex { proc_id; v = Return } ))
+
+  let create (prog : Program.t) dir =
+    ID.Map.to_iter prog.procs |> Iter.map snd
+    |> Iter.fold (fun g p -> proc_graph prog g p dir) (GB.empty ())
+
+  (** a table giving, to each procedure, all of its call sites to other
+      procedures *)
+  let proc_call_table dir g (prog : Program.t) =
+    let tbl = Hashtbl.create 100 in
+    G.iter_vertex
+      (fun l ->
+        match l with
+        | CallSite s ->
+            let cur = Hashtbl.get_or tbl s.proc_id ~default:Iter.empty in
+            Hashtbl.add tbl s.proc_id (Iter.cons (CallSite s) cur)
+        | _ -> ())
+      g;
+    tbl
+
+  module RevTop = Graph.Topological.Make (struct
+    type t = G.t
+
+    module V = G.V
+
+    module E = struct
+      include G.E
+
+      let src = G.E.dst
+      let dst = G.E.src
+    end
+
+    let iter_vertex = G.iter_vertex
+    let iter_succ = G.iter_pred
+  end)
+
+  module Top = Graph.Topological.Make (G)
+
+  module Vis = Graph.Graphviz.Dot (struct
+    include G
+    open G.V
+    open G.E
+
+    let graph_attributes _ = []
+
+    let vertex_name (v : Loc.t) =
+      match v with
+      | IntraVertex { proc_id; v } ->
+          "\""
+          ^ (match v with
+            | Begin _ -> Procedure.Vert.block_id_string v
+            | End _ -> Procedure.Vert.block_id_string v
+            | _ -> Procedure.Vert.block_id_string v)
+          ^ "@" ^ ID.to_string proc_id ^ "\""
+      | Entry -> "\"Entry\""
+      | Exit -> "\"Exit\""
+      | CallSite s ->
+          "\"" ^ "CallSite" ^ ID.to_string s.block ^ "."
+          ^ Int.to_string s.offset ^ "\""
+      | AfterCall s ->
+          "\"" ^ "AfterCall" ^ ID.to_string s.block ^ "."
+          ^ Int.to_string s.offset ^ "\""
+
+    let vertex_attributes (v : Loc.t) =
+      let l =
+        match v with
+        | IntraVertex { proc_id; v } ->
+            (match v with
+              | Begin _ -> "Begin " ^ Procedure.Vert.block_id_string v
+              | End _ -> "End " ^ Procedure.Vert.block_id_string v
+              | _ -> Procedure.Vert.block_id_string v)
+            ^ "@" ^ Int.to_string @@ ID.index proc_id
+        | Entry -> "Entry"
+        | Exit -> "Exit"
+        | CallSite s ->
+            "CallSite" ^ ID.to_string s.block ^ "." ^ Int.to_string s.offset
+        | AfterCall s ->
+            "AfterCall" ^ ID.to_string s.block ^ "." ^ Int.to_string s.offset
+      in
+      [ `Label l ]
+
+    let default_vertex_attributes _ = []
+
+    let edge_attributes (e : E.t) =
+      let l =
+        match e with
+        | _, Stmts _, _ -> "Stmts"
+        | _, InterCall _, _ -> "InterCall"
+        | _, InterReturn _, _ -> "InterReturn"
+        | _, Call _, _ -> "Call"
+        | _, Nop, _ -> ""
+        | _, StubProc _, _ -> "StubProc"
+      in
+      [ `Label l ]
+
+    let default_edge_attributes _ = []
+    let get_subgraph _ = None
+  end)
+end
+
+(** FIXME:
+    - properly handle global variables / local variables across procedure calls;
+      procedure summaries should be in terms of globals and formal paramters
+      only ; composition across calls should include the globals *)
+
+module IDE (D : IDEDomain) = struct
+  type summary = D.t DlMap.t DlMap.t [@@deriving eq, ord]
+  (** A summary associated to a location gives us all edge functions from the
+      start/end of the procedure this location is in, to this location.
+
+      Non membership in the map means v v' -> const bottom *)
+
+  let dir = D.direction
+
+  open DL
+
+  let show_summary v =
+    DlMap.to_iter v
+    |> Iter.flat_map (fun (d1, m) ->
+        DlMap.to_iter m |> Iter.map (fun x -> (d1, x)))
+    |> Iter.to_string ~sep:", " (fun (v, (v', i)) ->
+        "(" ^ DL.show v ^ "," ^ DL.show v' ^ "->" ^ D.show i ^ ")")
+
+  let empty_summary = DlMap.empty
+
+  type analysis_state = D.Value.t VarMap.t [@@deriving eq, ord]
+
+  let join_state_with st v x =
+    let j =
+      VarMap.get v st |> Option.map (D.Value.join x) |> Option.get_or ~default:x
+    in
+    VarMap.add v j st
+
+  let join_add m d e =
+    let j = D.join e (DlMap.get_or d m ~default:D.bottom) in
+    if not (D.equal j D.bottom) then DlMap.add d j m else m
+
+  (** Determine composites of edge functions through an intravertex block *)
+  let tf_stmts phi bs i =
+    let stmts i =
+      List.fold_left
+        (fun om stmt ->
+          DlMap.fold
+            (fun d2 e1 m ->
+              D.transfer stmt d2
+              |> Iter.fold
+                   (fun m (d3, e2) ->
+                     let e = D.compose e2 e1 in
+                     join_add m d3 e)
+                   m)
+            om DlMap.empty)
+        (Iter.fold (fun m (d, e) -> join_add m d e) DlMap.empty i)
+        bs
+      |> DlMap.to_iter
+    in
+    (* TODO this might be more imprecise than joining on the opposite side of the phi node
+                 https://link.springer.com/chapter/10.1007/978-3-642-11970-5_8 reckons so *)
+    let phis i =
+      match dir with
+      | `Forwards ->
+          List.fold_left
+            (fun i (p : Var.t Block.phi) ->
+              Iter.map
+                (fun (d2, e) ->
+                  if List.exists (fun (_, v) -> DL.equal (Label v) d2) p.rhs
+                  then (Label p.lhs, e)
+                  else (d2, e))
+                i)
+            i phi
+      | `Backwards ->
+          List.fold_left
+            (fun i (p : Var.t Block.phi) ->
+              Iter.flat_map
+                (fun (d2, e) ->
+                  if DL.equal (Label p.lhs) d2 then
+                    Iter.of_list p.rhs
+                    |> Iter.map (fun (_, d3) -> (Label d3, e))
+                  else Iter.singleton (d2, e))
+                i)
+            i phi
+    in
+    match dir with `Forwards -> stmts (phis i) | `Backwards -> phis (stmts i)
+
+  type edge = Loc.t * IDEGraph.Edge.t * Loc.t
+
+  let dldlget d1 d2 summary =
+    DlMap.get d1 summary
+    |> Option.flat_map (DlMap.get d2)
+    |> Option.get_or ~default:D.bottom
+
+  (** Propagate summaries into a new location and update the worklist *)
+  let propagate worklist summaries priority summary loc updates =
+    let module Q = IntPQueue.Plain in
+    Iter.filter_map
+      (fun ((d1, d3), e) ->
+        let l = dldlget d1 d3 summary in
+        let j = D.join l e in
+        (not (D.equal l j)) |> flip Option.return_if ((d1, d3), j))
+      updates
+    |> Iter.fold
+         (fun acc ((d1, d3), e) ->
+           Q.add worklist (loc, d1, d3) (priority loc);
+           let m = DlMap.get_or d1 acc ~default:DlMap.empty in
+           DlMap.add d1 (DlMap.add d3 e m) acc)
+         summary
+    |> Hashtbl.add summaries loc
+
+  (** Computes a table of summary edge functions
+
+      A summary edge function is an edge function from the start of a procedure
+      to some location in the procedure that is equal to the join of all
+      composite edge functions through paths to this location. *)
+  let phase1_solve order start graph globals default =
+    (* We compute summaries with a worklist fixpoint solver.
+       TOOD perhaps a better solver could be used?*)
+    Trace_core.with_span ~__FILE__ ~__LINE__ "ide-phase1" @@ fun _ ->
+    let module Q = IntPQueue.Plain in
+    let (worklist : (Loc.t * DL.t * DL.t) Q.t) = Q.create () in
+    let summaries : (Loc.t, summary) Hashtbl.t = Hashtbl.create 100 in
+    Hashtbl.add summaries start
+      (DlMap.singleton Lambda (DlMap.singleton Lambda D.identity));
+    (* Stores edge functions from the first procedure's entry to the second
+       procedure's entry, with a fixed dl value at the second procedure *)
+    let entry_to_call_entry_cache : (ID.t * DL.t * ID.t, D.t DlMap.t) Hashtbl.t
+        =
+      Hashtbl.create 100
+    in
+    (* Stores edge functions from the entry of a procedure to the end of said procedure for a given d value at the entry *)
+    let entry_to_exit_cache : (ID.t * DL.t, D.t DlMap.t) Hashtbl.t =
+      Hashtbl.create 100
+    in
+    let get_summary loc = Hashtbl.get summaries loc |> Option.get_or ~default in
+    let priority l = LM.find l order in
+    Q.add worklist (start, Lambda, Lambda) (priority start);
+    while not (Q.is_empty worklist) do
+      let (x : Loc.t * DL.t * DL.t) =
+        Q.extract worklist |> Option.get_exn_or "queue empty"
+      in
+      let l, d1, d2 = x in
+      let ost = get_summary l in
+      let e1 = dldlget d1 d2 ost in
+      IDEGraph.G.succ_e graph l |> Iter.of_list
+      |> Iter.iter (fun e ->
+          let from, target = match e with from, _, target -> (from, target) in
+          match IDEGraph.G.E.label e with
+          | Stmts (phi, bs) ->
+              tf_stmts phi bs (Iter.singleton (d2, e1))
+              |> Iter.map (fun (d3, e) -> ((d1, d3), e))
+              |> propagate worklist summaries priority (get_summary target)
+                   target
+          | InterCall callinfo ->
+              D.transfer_call callinfo d2
+              |> Iter.iter (fun (d3, e2) ->
+                  (* Add the callee to the worklist with an id edge at its entry
+                     so that the entry_to_exit cache eventually summarises it. *)
+                  propagate worklist summaries priority (get_summary target)
+                    target
+                    (Iter.singleton ((d3, d3), D.identity));
+                  (* Update the entry to call entry cache *)
+                  let e21 = D.compose e2 e1 in
+                  let k = (callinfo.caller, d3, callinfo.callee) in
+                  let m =
+                    Hashtbl.get_or entry_to_call_entry_cache k
+                      ~default:DlMap.empty
+                    |> DlMap.add d1 e21
+                  in
+                  Hashtbl.add entry_to_call_entry_cache k m;
+                  (* If we have entry to exit edge functions stored, propagate
+                     the composite of
+                     1. the edge function from the caller entry to callee entry
+                     2. edge functions through the callee procedure
+                     3. edge functions from the return of the callee to the caller *)
+                  let aftercall = Loc.AfterCall callinfo.aftercall in
+                  let _ =
+                    Hashtbl.get entry_to_exit_cache (callinfo.callee, d3)
+                    |> Option.map (fun m ->
+                        DlMap.to_iter m
+                        |> Iter.iter (fun (d4, e3) ->
+                            let e321 = D.compose e3 e21 in
+                            D.transfer_return callinfo.ret d4
+                            |> Iter.map (fun (d5, e4) ->
+                                ((d1, d5), D.compose e4 e321))
+                            |> propagate worklist summaries priority
+                                 (get_summary aftercall) aftercall))
+                  in
+                  ())
+          | InterReturn retinfo ->
+              (* Since we have reached the return block of a procedure, we
+                 have a complete summary of it! Store this in the entry exit cache *)
+              let k = (retinfo.callee, d1) in
+              let m =
+                Hashtbl.get_or entry_to_exit_cache k ~default:DlMap.empty
+                |> DlMap.add d2 e1
+              in
+              Hashtbl.add entry_to_exit_cache k m;
+              (* If we have an edge from the caller's entry to the callee's
+                 entry, we can propagate the same big composite as described
+                 in the InterCall branch.
+
+                 Note that we do not propagate to aftercalls of callers if the
+                 caller never propagated through its own InterCall edge *)
+              let k = (retinfo.caller, d1, retinfo.callee) in
+              let _ =
+                Hashtbl.get entry_to_call_entry_cache k
+                |> Option.map (fun m ->
+                    DlMap.to_iter m
+                    |> Iter.iter (fun (d3, e2) ->
+                        let e12 = D.compose e1 e2 in
+                        D.transfer_return retinfo d2
+                        |> Iter.map (fun (d4, e3) ->
+                            ((d3, d4), D.compose e3 e12))
+                        |> propagate worklist summaries priority
+                             (get_summary target) target))
+              in
+              ()
+          | Call callstmt ->
+              D.transfer_call_to_aftercall callstmt d2
+              |> Iter.map (fun (d3, e2) -> ((d1, d3), D.compose e2 e1))
+              |> propagate worklist summaries priority (get_summary target)
+                   target
+          | StubProc stubinfo ->
+              D.transfer_stub stubinfo d2
+              |> Iter.map (fun (d3, e2) -> ((d1, d3), D.compose e2 e1))
+              |> propagate worklist summaries priority (get_summary target)
+                   target
+          | Nop ->
+              propagate worklist summaries priority (get_summary target) target
+                (Iter.singleton ((d1, d2), e1)))
+    done;
+    summaries
+
+  (** Compute the analysis result using summaries from phase 1 *)
+  let phase2_solve order prog start_proc graph globals
+      (summaries : (Loc.t, summary) Hashtbl.t) =
+    Trace_core.with_span ~__FILE__ ~__LINE__ "ide-phase2" @@ fun _ ->
+    let module Q = IntPQueue.Plain in
+    let states : (Loc.t, analysis_state) Hashtbl.t = Hashtbl.create 100 in
+    let get_st l = Hashtbl.get_or states l ~default:VarMap.empty in
+    let priority l = LM.find l order in
+    let get_summary loc =
+      Hashtbl.get summaries loc |> function
+      | Some e -> e
+      | None ->
+          (* This issue occurs whenever there are unimplemented procedures.
+             There's a fix but I haven't written it yet. *)
+          (*print_endline @@ "summary undefined " ^ Loc.show loc;*)
+          DlMap.empty
+    in
+    (* The first step is to initialise the entry nodes of each procedure with
+       their initial value based on the entry procedure being initialised to
+       bottom, using the summary functions. This is done by looking at all call
+       sites in a procedure and evaluating the composite of the summary to the
+       callsite and the transfer of the call edge (and reaching a fixpoint). *)
+    let (worklist : (Loc.t * DL.t) Q.t) = Q.create () in
+    let calls_table = IDEGraph.proc_call_table dir graph prog in
+    Hashtbl.get_or calls_table start_proc ~default:Iter.empty
+    |> Iter.iter (fun l -> Q.add worklist (l, Lambda) (priority l));
+    while not (Q.is_empty worklist) do
+      let l, d = Q.extract worklist |> Option.get_exn_or "queue empty" in
+      let ost = get_st l in
+      let md =
+        match d with
+        | Label v -> VarMap.get_or v ost ~default:D.Value.bottom
+        | _ -> D.Value.bottom
+      in
+      IDEGraph.G.succ_e graph l |> Iter.of_list
+      |> Iter.iter (fun e ->
+          let target = match e with _, _, target -> target in
+          match IDEGraph.G.E.label e with
+          | InterCall callinfo ->
+              let summary = get_summary l in
+              DlMap.get d summary |> Iter.of_opt
+              |> Iter.flat_map DlMap.to_iter
+              |> Iter.iter (fun (d2, e1) ->
+                  D.transfer_call callinfo d2
+                  |> Iter.iter (fun (d3, e2) ->
+                      (match d3 with
+                      | Label v ->
+                          let st =
+                            Hashtbl.get_or states target ~default:VarMap.empty
+                          in
+                          let fd = D.eval e2 (D.eval e1 md) in
+                          let y = VarMap.get_or v st ~default:D.Value.bottom in
+                          let j = D.Value.join y fd in
+                          if not (D.Value.equal j y) then (
+                            let st' = VarMap.add v (D.Value.join y fd) st in
+                            Hashtbl.add states target st';
+                            Hashtbl.get_or calls_table callinfo.callee
+                              ~default:Iter.empty
+                            |> Iter.iter (fun c ->
+                                Q.add worklist (c, d3) (priority c)))
+                          else ()
+                      | _ -> ());
+                      ()))
+          | _ -> ())
+    done;
+    (* We then apply all summary functions to each location to the initial
+       values of each procedure *)
+    let entry_of (l : Loc.t) =
+      match l with
+      | IntraVertex { proc_id; v } -> Loc.IntraVertex { proc_id; v = Entry }
+      | CallSite stmt_id -> IntraVertex { proc_id = stmt_id.proc_id; v = Entry }
+      | AfterCall stmt_id ->
+          IntraVertex { proc_id = stmt_id.proc_id; v = Entry }
+      | Entry -> Entry
+      | Exit -> Entry
+    in
+    flip IDEGraph.G.iter_vertex graph (fun l ->
+        let pst = get_st (entry_of l) in
+        get_summary l
+        |> DlMap.iter (fun d1 ->
+            let x =
+              match d1 with
+              | Label v -> VarMap.get_or v pst ~default:D.Value.bottom
+              | _ -> D.Value.bottom
+            in
+            DlMap.iter (fun d2 e ->
+                match d2 with
+                | Label v ->
+                    let st = get_st l in
+                    let y = D.eval e x in
+                    Hashtbl.add states l (join_state_with st v y)
+                | _ -> ())));
+    states
+
+  let query r ~proc_id vert =
+    Hashtbl.get r (Loc.IntraVertex { proc_id; v = vert })
+
+  let solve (prog : Program.t) =
+    Trace_core.with_span ~__FILE__ ~__LINE__ "ide-solve" @@ fun _ ->
+    let globals = prog.globals |> Var.Decls.to_iter |> Iter.map snd in
+    let graph = IDEGraph.create prog dir in
+    let order =
+      Iter.from_iter (fun f -> IDEGraph.Top.iter f graph)
+      |> Iter.zip_i
+      |> Iter.map (fun (i, v) -> (v, i))
+      |> LM.of_iter
+    in
+    let start =
+      match dir with `Forwards -> Loc.Entry | `Backwards -> Loc.Exit
+    in
+    let start_proc =
+      prog.entry_proc |> Option.get_exn_or "Missing entry procedure"
+    in
+    let summary = phase1_solve order start graph globals DlMap.empty in
+    ( query @@ summary,
+      query @@ phase2_solve order prog start_proc graph globals summary )
+
+  module G = Procedure.RevG
+  module ResultMap = Map.Make (G.V)
+
+  module type LocalPhaseProcAnalysis = sig
+    val recurse :
+      G.t ->
+      G.V.t Graph.WeakTopological.t ->
+      (G.V.t -> summary) ->
+      G.V.t Graph.ChaoticIteration.widening_set ->
+      int ->
+      summary ResultMap.t
+  end
+end
diff --git a/lib/analysis/ide_live.ml b/lib/analysis/ide_live.ml
new file mode 100644
index 0000000..dc2776e
--- /dev/null
+++ b/lib/analysis/ide_live.ml
@@ -0,0 +1,145 @@
+(** Interprocedural live variable analysis using the IDE solver *)
+
+open Lang
+open Containers
+open Common
+open Ide
+
+module IDELive = struct
+  let direction = `Backwards
+
+  module Value = struct
+    type t = bool [@@deriving eq, ord, show]
+
+    let bottom = false
+    let live : t = true
+    let dead : t = false
+
+    let join a b =
+      match (a, b) with
+      | true, _ -> true
+      | _, true -> true
+      | false, false -> false
+  end
+
+  let show_state s =
+    s
+    |> Iter.filter_map (function c, true -> Some c | _ -> None)
+    |> Iter.to_string ~sep:", " (fun v -> Var.to_string v)
+
+  open Value
+
+  type t = IdEdge | ConstEdge of Value.t [@@deriving eq, ord]
+
+  let bottom = ConstEdge bottom
+
+  let show v =
+    match v with IdEdge -> "IdEdge" | ConstEdge v -> "ConstEdge " ^ show v
+
+  let pp fmt v = Format.pp_print_string fmt (show v)
+  let identity = IdEdge
+
+  let compose a b =
+    match (a, b) with
+    | IdEdge, b -> b
+    | a, IdEdge -> a
+    | ConstEdge v, ConstEdge v' -> ConstEdge v
+
+  let join a b =
+    match (a, b) with
+    | ConstEdge v, ConstEdge v' -> ConstEdge (join v v')
+    | ConstEdge true, IdEdge -> ConstEdge true
+    | ConstEdge false, IdEdge -> IdEdge
+    | IdEdge, ConstEdge true -> ConstEdge true
+    | IdEdge, ConstEdge false -> IdEdge
+    | IdEdge, IdEdge -> IdEdge
+
+  let eval f v = match f with IdEdge -> v | ConstEdge v -> v
+
+  open DL
+
+  let transfer_call (c : call_info) d =
+    match d with
+    | Lambda -> Iter.singleton (d, IdEdge)
+    | Label v when Var.is_global v -> Iter.singleton (d, IdEdge)
+    | Label v when List.exists (fun (a, _) -> Var.equal a v) c.lhs ->
+        Iter.of_list c.lhs
+        |> Iter.filter (fun (a, _) -> Var.equal a v)
+        |> Iter.map (fun (_, f) -> (Label f, IdEdge))
+    | Label v -> Iter.empty
+
+  let transfer_return (r : ret_info) d =
+    match d with
+    | Lambda -> Iter.singleton (d, IdEdge)
+    | Label v when Var.is_global v -> Iter.singleton (d, IdEdge)
+    | Label v when List.exists (fun (f, _) -> Var.equal f v) r.rhs ->
+        Iter.of_list r.rhs
+        |> Iter.filter (fun (a, _) -> Var.equal a v)
+        |> Iter.flat_map (fun (_, e) ->
+            Expr.BasilExpr.free_vars_iter e
+            |> Iter.map (fun v' -> (Label v', IdEdge)))
+    | _ -> Iter.empty
+
+  let transfer_call_to_aftercall c d =
+    match d with
+    | Lambda -> Iter.singleton (d, IdEdge)
+    | Label v
+      when Var.is_local v
+           && (not @@ List.exists (fun (a, _) -> Var.equal a v) c.lhs) ->
+        Iter.singleton (d, IdEdge)
+    | Label _ -> Iter.empty
+
+  let transfer_stub (s : stub_info) d =
+    match d with
+    | Lambda ->
+        Iter.singleton (d, IdEdge)
+        |> Iter.append
+             (Iter.of_list s.formal_in
+             |> Iter.map (fun v -> (Label v, ConstEdge live)))
+        |> Iter.append
+             (Iter.of_list s.globals
+             |> Iter.map (fun v -> (Label v, ConstEdge live)))
+    | _ -> Iter.empty
+
+  let transfer stmt d =
+    let open Stmt in
+    match d with
+    | Lambda -> (
+        match stmt with
+        | Instr_Assign _ -> Iter.singleton (d, IdEdge)
+        | _ ->
+            Stmt.free_vars_iter stmt
+            |> Iter.fold
+                 (fun i v -> Iter.cons (Label v, ConstEdge live) i)
+                 (Iter.singleton (d, IdEdge)))
+    | Label v -> (
+        match stmt with
+        | Instr_Assign assigns ->
+            List.fold_left
+              (fun i (v', ex) ->
+                Iter.flat_map
+                  (fun (d, e) ->
+                    if DL.equal d (Label v') then
+                      Expr.BasilExpr.free_vars_iter ex
+                      |> Iter.map (fun v' -> (Label v', IdEdge))
+                    else Iter.singleton (d, e))
+                  i)
+              (Iter.singleton (d, IdEdge))
+              assigns
+        (* The index variables of a memory read are always live regardless of if
+           the lhs was dead, since there are still side effects of reading
+           memory ? *)
+        | Instr_Load l when Var.equal l.lhs v -> Iter.empty
+        | Instr_IntrinCall c
+          when StringMap.exists (fun _ v' -> Var.equal v v') c.lhs ->
+            Iter.empty
+        | Instr_Call c when StringMap.exists (fun _ v' -> Var.equal v v') c.lhs
+          ->
+            Iter.empty
+        (*| Instr_IndirectCall c
+          when StringMap.exists (fun _ v' -> Var.equal v v') c.lhs ->
+            DlMap.empty*)
+        | _ -> Iter.singleton (Label v, IdEdge))
+end
+
+module IDELiveAnalysis = IDE (IDELive)
diff --git a/lib/passes.ml b/lib/passes.ml
index 2b7d184..b32ba2e 100644
--- a/lib/passes.ml
+++ b/lib/passes.ml
@@ -107,7 +107,9 @@ module PassManager = struct
       {
         name = "ide-live";
         apply = Prog Transforms.Ide.transform;
-        doc = "broken ide test analysis";
+        doc =
+          "Write the results of an ide based live variable analysis to .dot \
+           files";
       };
       remove_unused;
     ]
diff --git a/lib/transforms/ide.ml b/lib/transforms/ide.ml
index 0501f53..1072bb0 100644
--- a/lib/transforms/ide.ml
+++ b/lib/transforms/ide.ml
@@ -1,673 +1,25 @@
-(** Prototype IDE solver: proof of concept for the design for a generic ish ide
-    solver.
-
-    WARN: the implemented live variables analysis here is not correct and the
-    solver is likely wrong; particularly with regard to context sensitivity *)
+(** IDE test transforms *)
 
 open Lang
 open Containers
 open Common
+open Analysis.Ide_live
 
-type call_info = {
-  rhs : (Var.t * Expr.BasilExpr.t) list;
-  lhs : (Var.t * Var.t) list;
-  call_from : Program.stmt; (* stmt must be variable Instr_Call*)
-}
-[@@deriving eq, ord, show { with_path = false }]
-(** (target.formal_in, rhs arg) assignment to call formal params *)
-
-module Loc = struct
-  type stmt_id = { proc_id : ID.t; block : ID.t; offset : int }
-  [@@deriving eq, ord, show { with_path = false }]
-
-  type t =
-    | IntraVertex of { proc_id : ID.t; v : Procedure.Vert.t }
-    | CallSite of stmt_id
-    | AfterCall of stmt_id
-    | Entry
-    | Exit
-  [@@deriving eq, ord, show]
-
-  let hash = Hashtbl.hash
-end
-
-module IDEGraph = struct
-  module Vert = struct
-    include Loc
-  end
-
-  open Vert
-
-  module Edge = struct
-    type t =
-      | Stmts of Var.t Block.phi list * Program.stmt list
-      | InterCall of call_info
-      | InterReturn of call_info
-      | Nop
-    [@@deriving eq, ord, show]
-
-    let default = Nop
-  end
-
-  module StmtLabel = struct
-    type 'a t = 'a Iter.t
-  end
-
-  module G = Graph.Imperative.Digraph.ConcreteBidirectionalLabeled (Vert) (Edge)
-  module GB = Graph.Builder.I (G)
-
-  type t = {
-    prog : Program.t;
-    callgraph : Program.CallGraph.G.t;
-    vertices : Loc.t Iter.t Lazy.t;
-  }
-
-  type bstate = {
-    graph : G.t;
-    last_vert : Loc.t;
-    stmts : Var.t Block.phi list * Program.stmt list;
-  }
-
-  let push_edge (ending : Loc.t) (g : bstate) =
-    match g with
-    | { graph; last_vert; stmts } ->
-        let phi, stmts = (fst stmts, List.rev (snd stmts)) in
-        let e1 = (last_vert, Edge.Stmts (phi, stmts), ending) in
-        { graph = GB.add_edge_e graph e1; stmts = ([], []); last_vert = ending }
-
-  let add_call p (st : bstate) (origin : stmt_id) (callstmt : Program.stmt) =
-    let lhs, rhs, target =
-      match callstmt with
-      | Stmt.(Instr_Call { lhs; procid; args }) ->
-          let target_proc = Program.proc p procid in
-          let formal_in =
-            Procedure.formal_in_params target_proc |> StringMap.to_iter
-          in
-          let actual_in = args |> StringMap.to_iter in
-          let actual_rhs =
-            Iter.join_by fst fst
-              ~merge:(fun id a b -> Some (snd a, snd b))
-              formal_in actual_in
-            |> Iter.to_list
-          in
-          let formal_out =
-            Procedure.formal_out_params target_proc |> StringMap.to_iter
-          in
-          let actual_out = lhs |> StringMap.to_iter in
-          let actual_lhs =
-            Iter.join_by fst fst
-              ~merge:(fun id a b -> Some (snd a, snd b))
-              actual_out formal_out
-            |> Iter.to_list
-          in
-          (actual_lhs, actual_rhs, procid)
-      | _ -> failwith "not a call"
-    in
-    let g = push_edge (CallSite origin) st in
-    let graph = g.graph in
-    (*let graph =
-      GB.add_edge_e graph (CallSite origin, Call callstmt, AfterCall origin)
-    in*)
-    let call_entry = IntraVertex { proc_id = target; v = Entry } in
-    let call_return = IntraVertex { proc_id = target; v = Return } in
-    let graph =
-      GB.add_edge_e graph
-        ( CallSite origin,
-          InterCall { rhs; lhs; call_from = callstmt },
-          call_entry )
-    in
-    let graph =
-      GB.add_edge_e graph
-        ( call_return,
-          InterReturn { lhs; rhs; call_from = callstmt },
-          AfterCall origin )
-    in
-    { g with graph }
-
-  let proc_graph prog g p =
-    let proc_id = Procedure.id p in
-    let add_block_edge b graph =
-      match b with
-      | v1, Procedure.Edge.Jump, v2 ->
-          GB.add_edge_e g
-            Loc.
-              ( IntraVertex { proc_id; v = v1 },
-                Nop,
-                IntraVertex { proc_id; v = v2 } )
-      | ( Procedure.Vert.Begin block,
-          Procedure.Edge.Block b,
-          Procedure.Vert.End b2 ) ->
-          assert (ID.equal b2 block);
-          let is =
-            {
-              graph;
-              last_vert = IntraVertex { proc_id; v = Begin block };
-              stmts = (b.phis, []);
-            }
-          in
-          Block.stmts_iter_i b
-          |> Iter.fold
-               (fun st (i, s) ->
-                 let stmt_id : Loc.stmt_id = { proc_id; block; offset = i } in
-                 match s with
-                 | Stmt.Instr_Call _ as c -> add_call prog st stmt_id c
-                 | stmt ->
-                     { st with stmts = (fst st.stmts, stmt :: snd st.stmts) })
-               is
-          |> push_edge (IntraVertex { proc_id; v = End block })
-          |> fun x -> x.graph
-      | _, _, _ -> failwith "bad proc edge"
-    in
-    (* add all vertices *)
-    (* TODO: missing stub procedure edges probably *)
-    let intra_verts =
-      Option.to_iter (Procedure.graph p)
-      |> Iter.flat_map (fun graph ->
-          Procedure.G.fold_vertex
-            (fun v acc -> Iter.cons (Loc.IntraVertex { proc_id; v }) acc)
-            graph Iter.empty)
-    in
-    let g = Iter.fold GB.add_vertex g intra_verts in
-    Procedure.graph p
-    |> Option.map (fun procg -> Procedure.G.fold_edges_e add_block_edge procg g)
-    |> Option.get_or ~default:g
-
-  let proc_vertices p =
-    let proc_id = Procedure.id p in
-    let intra_verts =
-      Option.to_iter (Procedure.graph p)
-      |> Iter.flat_map (fun graph ->
-          Procedure.G.fold_vertex
-            (fun v acc -> Iter.cons (Loc.IntraVertex { proc_id; v }) acc)
-            graph Iter.empty)
-    in
-    let b =
-      Procedure.blocks_to_list p |> List.to_iter
-      |> Iter.flat_map (function
-        | Procedure.Vert.Begin block, (b : Program.bloc) ->
-            Block.stmts_iter_i b
-            |> Iter.flat_map (fun (i, s) ->
-                let stmt_id : Loc.stmt_id = { proc_id; block; offset = i } in
-                match s with
-                | Stmt.Instr_Call _ ->
-                    Loc.(Iter.doubleton (AfterCall stmt_id) (CallSite stmt_id))
-                | _ -> Iter.empty)
-        | _, _ -> Iter.empty)
-    in
-    Iter.append intra_verts b
-
-  let create (prog : Program.t) =
-    ID.Map.to_iter prog.procs |> Iter.map snd
-    |> Iter.fold (fun g p -> proc_graph prog g p) (GB.empty ())
-
-  module RevTop = Graph.Topological.Make (struct
-    type t = G.t
-
-    module V = G.V
-
-    module E = struct
-      include G.E
-
-      let src = G.E.dst
-      let dst = G.E.src
-    end
-
-    let iter_vertex = G.iter_vertex
-    let iter_succ = G.iter_pred
-  end)
-
-  module Top = Graph.Topological.Make (G)
-end
-
-module type Domain = sig
-  include ORD_TYPE
-
-  val join : t -> t -> t
-  val bottom : t
-
-  (*val eval : (Var.t -> t option) -> Expr.BasilExpr.t -> t*)
-  (*val transfer : (Var.t -> t option) -> Program.stmt -> (Var.t * t) Iter.t*)
-end
-
-type 'a state_update = (Var.t * 'a) Iter.t
-
-module type IDEDomain = sig
-  include ORD_TYPE
-  module Const : Domain
-
-  val identity : Var.t -> t
-  val compose : (Var.t -> t) -> t -> t
-  val join : t -> t -> t
-  val eval : Expr.BasilExpr.t -> t
-  val bottom : t
-
-  val compose_call : (Var.t -> t) -> call_info -> t state_update
-  (** edge calling a procedure *)
-
-  val compose_return : (Var.t -> t) -> call_info -> t state_update
-  (** edge return to after a call *)
-
-  val transfer : Program.stmt -> t state_update
-  (** update the state for a program statement *)
-
-  val transfer_const :
-    (Var.t -> Const.t) -> (Var.t * t) Iter.t -> Const.t state_update
-  (** update the constant state for each edge in the microfunction *)
-end
-
-module IDELive = struct
-  module Const = struct
-    type t = bool [@@deriving eq, ord, show]
-
-    let bottom = false
-    let live : t = true
-    let dead : t = false
-
-    let join a b =
-      match (a, b) with
-      | true, _ -> true
-      | _, true -> true
-      | false, false -> false
-  end
-
-  let show_const_state s =
-    s
-    |> Iter.filter_map (function c, true -> Some c | _ -> None)
-    |> Iter.to_string ~sep:", " (fun v -> Var.to_string v)
-
-  open Const
-
-  type t = Live | Dead | CondLive of Var.t [@@deriving eq, ord]
-
-  let bottom = Dead
-
-  let show v =
-    match v with
-    | Live -> "Live"
-    | Dead -> "Dead"
-    | CondLive v -> Var.to_string v
-
-  let pp fmt v = Format.pp_print_string fmt (show v)
-  let identity v = CondLive v
-
-  (** compose (\lambda v . a) (\lambda v . b) *)
-  let compose read b =
-    match b with
-    | Live -> Live
-    | Dead -> Dead
-    | CondLive v1 -> (
-        match read v1 with
-        | Live -> Live
-        | Dead -> Dead
-        | CondLive v2 -> CondLive v2)
-  (** not representible *)
-
-  let join a b =
-    match (a, b) with
-    | _, Live -> Live
-    | Live, _ -> Live
-    | CondLive v1, CondLive v2 when Var.equal v1 v2 -> CondLive v1
-    | CondLive _, CondLive _ -> Live
-    | Dead, CondLive v -> CondLive v
-    | CondLive v, Dead -> CondLive v
-    | Dead, Dead -> Dead
-
-  let eval e =
-    let free = Expr.BasilExpr.free_vars_iter e in
-    if Iter.length free = 1 then CondLive (Iter.head_exn free) else Live
-
-  let compose_call read (c : call_info) =
-    Iter.of_list c.rhs
-    |> Iter.flat_map (fun (formal, e) ->
-        Expr.BasilExpr.free_vars_iter e |> Iter.map (fun fv -> (formal, fv)))
-    |> Iter.map (fun (formal, v) ->
-        ( v,
-          match read v with
-          | Live -> Live
-          | Dead -> Dead
-          | CondLive v when Var.is_global v -> CondLive v
-          | CondLive _ -> Live ))
-    |> Iter.group_by ~eq:(fun a b -> Var.equal (fst a) (fst b))
-    |> Iter.map (function
-      | [ a ] -> a
-      | a :: tl -> (fst a, Live)
-      | [] -> failwith "unreachable")
-    |> Iter.append
-         (Iter.of_list c.lhs |> Iter.map (fun (lhs, rhs) -> (lhs, Dead)))
-
-  let compose_return read (c : call_info) =
-    Iter.of_list c.lhs
-    |> Iter.map (fun (lhs, rhs) ->
-        let mf =
-          match read lhs with
-          | Live -> Live
-          | Dead -> Dead
-          | CondLive v when Var.is_global v -> CondLive v
-          | CondLive _ -> Live
-        in
-        (rhs, mf))
-    |> Iter.append
-         (Iter.of_list c.lhs |> Iter.map (fun (lhs, rhs) -> (lhs, Dead)))
-
-  let transfer s =
-    let open Livevars in
-    let open Stmt in
-    let assigned = Stmt.assigned VarSet.empty s |> VarSet.to_iter in
-    let read = Stmt.free_vars VarSet.empty s |> VarSet.to_iter in
-    let rhs =
-      match s with
-      | Instr_Load _ | Instr_Store _ | Instr_Assert _ | Instr_Assume _
-      | Instr_IntrinCall _ | Instr_IndirectCall _ ->
-          Iter.map (fun v -> (v, Live)) read
-      | Instr_Call _ -> failwith "unreachable"
-      | Instr_Assign assigns ->
-          List.to_iter assigns
-          |> Iter.flat_map (fun (l, r) ->
-              Iter.cons (l, Dead)
-                (Expr.BasilExpr.free_vars_iter r
-                |> Iter.map (fun rv -> (rv, CondLive l))))
-    in
-    Iter.append rhs (Iter.map (fun v -> (v, Dead)) assigned)
-
-  let transfer_const (read : Var.t -> Const.t) (es : (Var.t * t) Iter.t) :
-      (Var.t * Const.t) Iter.t =
-    es
-    |> Iter.map (fun (v, e) ->
-        (v, match e with Live -> true | Dead -> false | CondLive v -> read v))
-end
-
-(** FIXME:
-    - properly handle global variables / local variables across procedure calls;
-      procedure summaries should be in terms of globals and formal paramters
-      only ; composition across calls should include the globals
-    - phis *)
-
-module IDE (D : IDEDomain) = struct
-  type summary = D.t VarMap.t [@@deriving eq, ord]
-  (** Edge function type: map from variables to lambda functions of at most one
-      other variable (implicit)
-
-      Non membership in the map means v -> \l l . bot *)
-
-  let show_summary v =
-    VarMap.to_iter v
-    |> Iter.to_string ~sep:", " (fun (v, i) ->
-        Var.to_string v ^ "->" ^ D.show i)
-
-  type constant_state = D.Const.t VarMap.t [@@deriving eq, ord]
-
-  let empty_summary = VarMap.empty
-
-  (** composition of an assignment var := mfun', where var |-> mfun in st: i.e.
-      becomes compose mfun compose mfun' *)
-  let compose_assigns st1 st vars =
-    Iter.fold
-      (fun acc (v, mf) ->
-        let r = D.compose (fun v -> VarMap.get_or ~default:D.bottom v st1) mf in
-        if D.equal r D.bottom then VarMap.remove v acc else VarMap.add v r acc)
-      st vars
-
-  let update_state st1 st vars =
-    Iter.fold
-      (fun acc (v, mf) ->
-        if D.equal mf D.bottom then VarMap.remove v acc else VarMap.add v mf acc)
-      st vars
-
-  let join_summaries a b =
-    (* keeps everything present in a and not b, does that make sense?*)
-    VarMap.union (fun v a b -> Some (D.join a b)) a b
-
-  let join_constant_summary (s0 : constant_state) (s1 : constant_state) :
-      constant_state =
-    (* keeps everything present in a and not b, does that make sense?*)
-    VarMap.union (fun v a b -> Some (D.Const.join a b)) s0 s1
-
-  (* compose bot f = f ? *)
-  let compose_state_updates (updates : D.t state_update) st1 st =
-    compose_assigns st1 st updates
-
-  let direction : [ `Forwards | `Backwards ] = `Backwards
-
-  let proc_entry (prog : Program.t) (proc : Program.proc) =
-    let globals =
-      prog.globals |> Hashtbl.to_list |> List.map snd
-      |> List.map (fun v -> (v, D.identity v))
-    in
-    let locals = Procedure.formal_in_params proc in
-    let locals =
-      StringMap.to_list locals |> List.map snd
-      |> List.map (fun v -> (v, D.identity v))
-    in
-    globals @ locals
-
-  let proc_return (prog : Program.t) (proc : Program.proc) =
-    let globals =
-      prog.globals |> Hashtbl.to_list |> List.map snd
-      |> List.map (fun v -> (v, D.identity v))
-    in
-    let locals = Procedure.formal_out_params proc in
-    let locals =
-      StringMap.to_list locals |> List.map snd
-      |> List.map (fun v -> (v, D.identity v))
-    in
-    globals @ locals
-
-  let tf_phis phis : (Var.t * D.t) Iter.t = Iter.empty
-
-  type edge = Loc.t * IDEGraph.Edge.t * Loc.t
-
-  let tf_edge_phase_2 st summary globals edge =
-    let open IDEGraph.Edge in
-    let read v = VarMap.get_or ~default:D.Const.bottom v st in
-    let update k v st =
-      if D.Const.equal D.Const.bottom v then VarMap.remove k st
-      else VarMap.add k v st
-    in
-    match IDEGraph.G.E.label edge with
-    | Stmts (phi, bs) ->
-        let updates = D.transfer_const read (VarMap.to_iter summary) in
-        let st' = Iter.fold (fun m (v, t) -> update v t m) st updates in
-        st'
-    | InterCall args ->
-        let args =
-          List.to_iter args.rhs
-          |> Iter.map (function formal, _ -> formal)
-          |> Iter.append globals
-          |> Iter.map (fun v -> (v, VarMap.get_or ~default:D.bottom v summary))
-        in
-        let updates = D.transfer_const read args in
-        let st' = Iter.fold (fun m (v, t) -> update v t m) st updates in
-        st'
-    | InterReturn args ->
-        let args =
-          List.to_iter args.rhs
-          |> Iter.map (function formal, _ -> formal)
-          |> Iter.append globals
-          |> Iter.map (fun v -> (v, VarMap.get_or ~default:D.bottom v summary))
-        in
-        let updates = D.transfer_const read args in
-        let st' = Iter.fold (fun m (v, t) -> update v t m) st updates in
-        st'
-    | Nop -> st
-
-  let tf_edge_phase_1 dir globals get_summary st edge =
-    let open IDEGraph.Edge in
-    let orig, target =
-      match (dir, edge) with
-      | `Forwards, (a, _, b) -> (a, b)
-      | `Backwards, (a, _, b) -> (b, a)
-    in
-    match IDEGraph.G.E.label edge with
-    | Stmts (phi, bs) -> (
-        let stmts st =
-          match dir with
-          | `Forwards ->
-              List.fold_left
-                (fun st s -> compose_state_updates (D.transfer s) st st)
-                st bs
-          | `Backwards ->
-              List.fold_right
-                (fun s st -> compose_state_updates (D.transfer s) st st)
-                bs st
-        in
-        let phis st = compose_state_updates (tf_phis phi) st st in
-        match dir with
-        | `Forwards -> phis (stmts st)
-        | `Backwards -> stmts (phis st))
-    | InterCall args ->
-        let target = get_summary target in
-        update_state st target
-          (D.compose_call
-             (fun v -> VarMap.get_or v ~default:D.bottom target)
-             args)
-        |> compose_state_updates
-             (globals |> Iter.map (fun v -> (v, D.identity v)))
-             st
-    | InterReturn args ->
-        let target = get_summary target in
-        update_state st target
-          (D.compose_return
-             (fun v -> VarMap.get_or ~default:D.bottom v target)
-             args)
-        |> compose_state_updates
-             (globals |> Iter.map (fun v -> (v, D.identity v)))
-             st
-    | Nop -> st
-
-  module LM = Map.Make (Loc)
-
-  let phase1_solve order dir graph globals default =
-    (* FIXME: this doesn't maintain context sensitivity because there is only one edgefunction
-       for each procedure entry, therefore joining all the contexts*)
-    Trace_core.with_span ~__FILE__ ~__LINE__ "ide-phase1" @@ fun _ ->
-    let module Q = IntPQueue.Plain in
-    let (worklist : edge Q.t) = Q.create () in
-    let summaries : (Loc.t, summary) Hashtbl.t = Hashtbl.create 100 in
-    let get_summary loc = Hashtbl.get summaries loc |> Option.get_or ~default in
-    let priority (edge : edge) =
-      match dir with
-      | `Forwards -> ( match edge with l, _, _ -> LM.find l order)
-      | `Backwards -> ( match edge with _, _, l -> LM.find l order)
-    in
-    IDEGraph.G.fold_edges_e (fun e a -> Q.add worklist e (priority e)) graph ();
-    while not (Q.is_empty worklist) do
-      let (p : edge) = Q.extract worklist |> Option.get_exn_or "queue empty" in
-      let st, vend, ost', siblings =
-        match (p, dir) with
-        | (b, _, e), `Forwards ->
-            (get_summary b, e, get_summary e, IDEGraph.G.pred graph e)
-        | (b, _, e), `Backwards ->
-            (get_summary e, b, get_summary b, IDEGraph.G.succ graph b)
-      in
-      let st' = tf_edge_phase_1 dir globals get_summary st p in
-      let st' = VarMap.filter (fun v i -> not (D.equal D.bottom i)) st' in
-      let st' =
-        if List.length siblings > 1 then join_summaries ost' st' else st'
-      in
-      if not (equal_summary ost' st') then (
-        Hashtbl.add summaries vend st';
-        let succ =
-          match dir with
-          | `Forwards -> IDEGraph.G.succ_e graph vend
-          | `Backwards -> IDEGraph.G.pred_e graph vend
-        in
-        List.iter (fun v -> Q.add worklist v (priority v)) succ;
-        ())
-    done;
-    summaries
-
-  let phase2_solve order dir graph globals
-      (summaries : (Loc.t, summary) Hashtbl.t) =
-    (* FIXME: use summaries ; propertly evaluate call edges first then fill in between*)
-    Trace_core.with_span ~__FILE__ ~__LINE__ "ide-phase2" @@ fun _ ->
-    let module Q = IntPQueue.Plain in
-    let (worklist : edge Q.t) = Q.create () in
-    let constants : (Loc.t, constant_state) Hashtbl.t = Hashtbl.create 100 in
-    let get_st l = Hashtbl.get_or constants l ~default:VarMap.empty in
-    let priority (edge : edge) =
-      match dir with
-      | `Forwards -> ( match edge with l, _, _ -> LM.find l order)
-      | `Backwards -> ( match edge with _, _, l -> LM.find l order)
-    in
-    let get_summary loc =
-      Hashtbl.get summaries loc |> function
-      | Some e -> e
-      | None ->
-          print_endline @@ "summary undefined " ^ Loc.show loc;
-          VarMap.empty
-    in
-    IDEGraph.G.fold_edges_e (fun e a -> Q.add worklist e (priority e)) graph ();
-    while not (Q.is_empty worklist) do
-      let (p : edge) = Q.extract worklist |> Option.get_exn_or "queue empty" in
-      let b, e, summary, st, ost', siblings =
-        match (p, dir) with
-        | (b, _, e), `Forwards ->
-            (b, e, get_summary b, get_st b, get_st e, IDEGraph.G.pred graph e)
-        | (b, _, e), `Backwards ->
-            (e, b, get_summary e, get_st e, get_st b, IDEGraph.G.succ graph b)
-      in
-      let st' = tf_edge_phase_2 st summary globals p in
-      let st' =
-        if List.length siblings > 1 then join_constant_summary st' ost' else st'
-      in
-      if not (equal_constant_state ost' st') then (
-        Hashtbl.add constants e st';
-        let succ =
-          match dir with
-          | `Forwards -> IDEGraph.G.succ_e graph e
-          | `Backwards -> IDEGraph.G.pred_e graph e
-        in
-        List.iter (fun v -> Q.add worklist v (priority v)) succ;
-        ())
-    done;
-    constants
-
-  let query (r : (Loc.t, 'a VarMap.t) Hashtbl.t) ~proc_id vert =
-    Hashtbl.get r (IntraVertex { proc_id; v = vert })
-
-  let solve dir (prog : Program.t) =
-    Trace_core.with_span ~__FILE__ ~__LINE__ "ide-solve" @@ fun _ ->
-    let globals = prog.globals |> Var.Decls.to_iter |> Iter.map snd in
-    let graph = IDEGraph.create prog in
-    let order =
-      (match dir with
-        | `Forwards -> Iter.from_iter (fun f -> IDEGraph.Top.iter f graph)
-        | `Backwards -> Iter.from_iter (fun f -> IDEGraph.RevTop.iter f graph))
-      |> Iter.zip_i
-      |> Iter.map (fun (i, v) -> (v, i))
-      |> LM.of_iter
-    in
-    let summary = phase1_solve order dir graph globals VarMap.empty in
-    (query @@ summary, query @@ phase2_solve order dir graph globals summary)
-
-  module G = Procedure.RevG
-  module ResultMap = Map.Make (G.V)
-
-  module type LocalPhaseProcAnalysis = sig
-    val recurse :
-      G.t ->
-      G.V.t Graph.WeakTopological.t ->
-      (G.V.t -> summary) ->
-      G.V.t Graph.ChaoticIteration.widening_set ->
-      int ->
-      summary ResultMap.t
-  end
-end
-
-module IDELiveAnalysis = IDE (IDELive)
-
-let show_const_summary (v : IDELiveAnalysis.constant_state) =
-  VarMap.to_iter v |> IDELive.show_const_state
+let show_state (v : IDELiveAnalysis.analysis_state) =
+  VarMap.to_iter v |> IDELive.show_state
 
 let print_live_vars_dot sum r fmt prog proc_id =
   let label (v : Procedure.G.vertex) = r v |> Option.map (fun s -> sum s) in
   let p = Program.proc prog proc_id in
-  Trace_core.with_span ~__FILE__ ~__LINE__ "dot-priner" @@ fun _ ->
-  let (module M : Viscfg.ProcPrinter) = Viscfg.dot_labels (fun v -> label v) in
+  Trace_core.with_span ~__FILE__ ~__LINE__ "dot-printer" @@ fun _ ->
+  let (module M : Viscfg.ProcPrinter) = Viscfg.dot_labels label in
   Option.iter (fun g -> M.fprint_graph fmt g) (Procedure.graph p)
 
 let transform (prog : Program.t) =
-  let summary, r = IDELiveAnalysis.solve `Backwards prog in
+  let g = Analysis.Ide.IDEGraph.create prog `Backwards in
+  CCIO.with_out "idegraph.dot" (fun s ->
+      Analysis.Ide.IDEGraph.Vis.fprint_graph (Format.of_chan s) g);
+  let summary, r = IDELiveAnalysis.solve prog in
   ID.Map.to_iter prog.procs
   |> Iter.iter (fun (proc, proc_n) ->
       let n = ID.to_string proc in
@@ -679,6 +31,6 @@ let transform (prog : Program.t) =
       CCIO.with_out
         ("idelive-const" ^ n ^ ".dot")
         (fun s ->
-          print_live_vars_dot show_const_summary (r ~proc_id:proc)
-            (Format.of_chan s) prog proc));
+          print_live_vars_dot show_state (r ~proc_id:proc) (Format.of_chan s)
+            prog proc));
   prog
diff --git a/test/analysis/ide_live.ml b/test/analysis/ide_live.ml
new file mode 100644
index 0000000..21dd2b4
--- /dev/null
+++ b/test/analysis/ide_live.ml
@@ -0,0 +1,244 @@
+open Analysis.Ide_live
+open Bincaml_util.Common
+
+let print_lives r proc =
+  print_endline @@ ID.to_string proc;
+  r ~proc_id:proc Lang.Procedure.Vert.Entry
+  |> Option.get_exn_or "No entry node"
+  |> VarMap.iter (fun v _ -> print_endline @@ Var.to_string v)
+
+let%expect_test "intra_checks" =
+  let lst =
+    Loader.Loadir.ast_of_string
+      {|
+memory shared $mem : (bv64 -> bv8);
+
+prog entry @main;
+
+proc @main () -> ()
+[
+    block %main_entry [
+        goto(%main_1, %main_2);
+    ];
+    block %main_1 [
+        $x:bv64 := bvadd($x:bv64, a:bv64);
+        assert eq($x:bv64,0);
+        assume neq(e:bv64,0);
+        goto(%main_return);
+    ];
+    block %main_2 [
+        $y:bv64 := load le $mem b:bv64 64;
+        $z:bv64 := c:bv64;
+        store le $mem $z:bv64 d:bv64 64;
+        goto(%main_return);
+    ];
+    block %main_return [
+        return();
+    ];
+];
+    |}
+  in
+  let program = lst.prog in
+  let _, results = IDELiveAnalysis.solve program in
+  let main = program.entry_proc |> Option.get_exn_or "No entry proc" in
+  print_lives results main;
+  [%expect
+    {|
+    @main
+    $mem:(bv64->bv8)
+    $x:bv64
+    a:bv64
+    e:bv64
+    b:bv64
+    c:bv64
+    d:bv64
+    |}]
+
+let%expect_test "simple_call" =
+  let lst =
+    Loader.Loadir.ast_of_string
+      {|
+prog entry @main;
+
+proc @main () -> ()
+[
+    block %main_entry [
+        var (a:bv64) := call @fun(b:bv64, b: bv64);
+        var (x:bv64) := call @fun(a:bv64, b: bv64);
+        assert eq(x:bv64, bvadd(b:bv64, b:bv64));
+        assert eq(y:bv64, 0);
+        return ();
+    ];
+];
+
+proc @fun (c:bv64, d:bv64) -> (out:bv64)
+[
+    block %fun_entry [
+        return (bvadd(c:bv64, d:bv64));
+    ];
+];
+    |}
+  in
+  let program = lst.prog in
+  let _, results = IDELiveAnalysis.solve program in
+  ID.Map.iter (fun id _ -> print_lives results id) program.procs;
+  [%expect
+    {|
+    @main
+    b:bv64
+    y:bv64
+    @fun
+    c:bv64
+    d:bv64
+    |}]
+
+let%expect_test "nested_call" =
+  let lst =
+    Loader.Loadir.ast_of_string
+      {|
+prog entry @main;
+
+var $global:bv64;
+
+proc @main () -> ()
+[
+    block %main_entry [
+        var (a:bv64) := call @fun1(b:bv64, b: bv64);
+        var (x:bv64) := call @fun1(a:bv64, b: bv64);
+        assert eq(x:bv64, bvadd(b:bv64, b:bv64));
+        assert eq(y:bv64, 0);
+        return ();
+    ];
+];
+
+proc @fun1 (c:bv64, d:bv64) -> (out:bv64)
+[
+    block %fun1_entry [
+        var (e:bv64) := call @fun2 (d:bv64);
+        return (bvadd(c:bv64, e:bv64));
+    ];
+];
+
+proc @fun2 (f:bv64) -> (out2:bv64)
+[
+    block %fun2_entry [
+        var g:bv64 := $global:bv64;
+        return (bvadd(f:bv64, g:bv64));
+    ];
+];
+    |}
+  in
+  let program = lst.prog in
+  let _, results = IDELiveAnalysis.solve program in
+  ID.Map.iter (fun id _ -> print_lives results id) program.procs;
+  [%expect
+    {|
+    @main
+    b:bv64
+    y:bv64
+    $global:bv64
+    @fun1
+    c:bv64
+    d:bv64
+    $global:bv64
+    @fun2
+    $global:bv64
+    f:bv64
+    |}]
+
+let%expect_test "mutually_recursive" =
+  let lst =
+    Loader.Loadir.ast_of_string
+      {|
+prog entry @main;
+
+var $global:bv64;
+
+proc @main () -> ()
+[
+    block %main_entry [
+        var (a:bv64) := call @fun2(b:bv64);
+        var (x:bv64) := call @fun1(a:bv64, b: bv64);
+        assert eq(x:bv64, bvadd(b:bv64, b:bv64));
+        assert eq(y:bv64, 0);
+        return ();
+    ];
+];
+
+proc @fun1 (c:bv64, d:bv64) -> (out:bv64)
+[
+    block %fun1_entry [
+        var (e:bv64) := call @fun2 (d:bv64);
+        return (bvsub(c:bv64, e:bv64));
+    ];
+];
+
+proc @fun2 (f:bv64) -> (out2:bv64)
+[
+    block %fun2_entry [
+        goto(%fun2_a, %fun2_b);
+    ];
+    block %fun2_a [
+        guard bvsle(f:bv64, 0);
+        var (g:bv64) := call @fun1(f:bv64, 1);
+        goto (%fun2_return);
+    ];
+    block %fun2_b [
+        guard bvsgt(f:bv64, 0);
+        var g:bv64 := $global:bv64;
+        goto (%fun2_return);
+    ];
+    block %fun2_return [
+        return (bvadd(f:bv64, g:bv64));
+    ];
+];
+    |}
+  in
+  let program = lst.prog in
+  let _, results = IDELiveAnalysis.solve program in
+  ID.Map.iter (fun id _ -> print_lives results id) program.procs;
+  [%expect
+    {|
+    @main
+    b:bv64
+    y:bv64
+    $global:bv64
+    @fun1
+    c:bv64
+    d:bv64
+    $global:bv64
+    @fun2
+    $global:bv64
+    f:bv64
+    |}]
+
+let%expect_test "stub" =
+  let lst =
+    Loader.Loadir.ast_of_string
+      {|
+memory shared $mem : (bv64 -> bv8);
+
+var $g: bv64;
+
+prog entry @main;
+
+proc @main () -> ()
+[
+    block %main_entry [
+        call @stub();
+        return();
+    ];
+];
+
+proc @stub() -> ();
+    |}
+  in
+  let program = lst.prog in
+  let _, results = IDELiveAnalysis.solve program in
+  let main = program.entry_proc |> Option.get_exn_or "No entry proc" in
+  print_lives results main;
+  [%expect {|
+    @main
+    $mem:(bv64->bv8)
+    $g:bv64
+    |}]