From 0fadbcf377e866234526287c4e61e57b18f2478d Mon Sep 17 00:00:00 2001
From: bpaul <bpaul@bpaul.xyz>
Date: Mon, 19 Jan 2026 15:09:08 +1000
Subject: [PATCH 01/16] It compiles!

---
 lib/transforms/ide.ml | 761 +++++++++++++++++++++++-------------------
 1 file changed, 414 insertions(+), 347 deletions(-)

diff --git a/lib/transforms/ide.ml b/lib/transforms/ide.ml
index 97d11bf..2bd9ea9 100644
--- a/lib/transforms/ide.ml
+++ b/lib/transforms/ide.ml
@@ -8,10 +8,22 @@ open Lang
 open Containers
 open Common
 
+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 }]
+
 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*)
+  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 *)
@@ -31,6 +43,9 @@ module Loc = struct
   let hash = Hashtbl.hash
 end
 
+module LSet = Set.Make (Loc)
+module LM = Map.Make (Loc)
+
 module IDEGraph = struct
   module Vert = struct
     include Loc
@@ -42,7 +57,8 @@ module IDEGraph = struct
     type t =
       | Stmts of Var.t Block.phi list * Program.stmt list
       | InterCall of call_info
-      | InterReturn of call_info
+      | InterReturn of ret_info
+      | Call of Program.stmt
       | Nop
     [@@deriving eq, ord, show]
 
@@ -103,24 +119,24 @@ module IDEGraph = struct
           (actual_lhs, actual_rhs, procid)
       | _ -> failwith "not a call"
     in
+    let caller, callee = (origin.proc_id, target) in
     let g = push_edge (CallSite origin) st in
     let graph = g.graph in
-    (*let graph =
+    let graph =
       GB.add_edge_e graph (CallSite origin, Call callstmt, AfterCall origin)
-    in*)
+    in
     let call_entry = IntraVertex { proc_id = target; v = Entry } in
     let call_return = IntraVertex { proc_id = target; v = Return } in
+    let ret_info = { lhs; rhs; call_from = callstmt; caller; callee } in
     let graph =
       GB.add_edge_e graph
         ( CallSite origin,
-          InterCall { rhs; lhs; call_from = callstmt },
+          InterCall
+            { rhs; lhs; call_from = callstmt; caller; callee; ret = ret_info },
           call_entry )
     in
     let graph =
-      GB.add_edge_e graph
-        ( call_return,
-          InterReturn { lhs; rhs; call_from = callstmt },
-          AfterCall origin )
+      GB.add_edge_e graph (call_return, InterReturn ret_info, AfterCall origin)
     in
     { g with graph }
 
@@ -172,34 +188,42 @@ module IDEGraph = struct
     |> 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 ())
 
+  let vertex_to_entry_table g =
+    let t = ref LM.empty in
+    let s = Stack.create () in
+    G.iter_vertex
+      (function
+        | IntraVertex { proc_id; v = l } as v
+          when Procedure.Vert.equal l Procedure.Vert.Entry ->
+            Stack.push v s
+        | _ -> ())
+      g;
+    while not (Stack.is_empty s) do
+      let entry = Stack.pop s in
+      let s2 = Stack.create () in
+      Stack.push entry s2;
+      let vis = ref (LSet.singleton entry) in
+      while not (Stack.is_empty s2) do
+        let v = Stack.pop s2 in
+        G.iter_succ_e
+          (fun (_, e, v2) ->
+            match e with
+            | Stmts _ | Call _ | Nop ->
+                if not (LSet.mem v2 !vis) then (
+                  vis := LSet.add v2 !vis;
+                  Stack.push v2 s2)
+                else ()
+            | _ -> ())
+          g v
+      done;
+      ()
+    done;
+    !t
+
   module RevTop = Graph.Topological.Make (struct
     type t = G.t
 
@@ -219,7 +243,7 @@ module IDEGraph = struct
   module Top = Graph.Topological.Make (G)
 end
 
-module type Domain = sig
+module type Lattice = sig
   include ORD_TYPE
 
   val join : t -> t -> t
@@ -229,34 +253,56 @@ module type Domain = sig
   (*val transfer : (Var.t -> t option) -> Program.stmt -> (Var.t * t) Iter.t*)
 end
 
-type 'a state_update = (Var.t * 'a) Iter.t
+(* TODO rename these types !!!!!!!!!!!!! *)
+
+(** blah blah blah *)
+type 'a dl = Label of 'a | Lambda [@@deriving eq, ord, show]
+
+module Lambda = struct
+  (* TODO not Var.t (want more generality e.g. dsa uses symbolic addresses in scala code) *)
+  type t = Var.t dl [@@deriving eq, ord, show]
+  (** blah blah blah *)
+end
+
+module Lambda2 = struct
+  type t = Lambda.t * Lambda.t [@@deriving eq, ord, show]
+end
+
+module DlMap = Map.Make (Lambda)
+
+type 'a state_update = (Var.t dl * 'a) Iter.t
 
 module type IDEDomain = sig
-  include ORD_TYPE
-  module Const : Domain
+  include Lattice
 
-  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
+  (* idk how to document this but the ordering of this domain should be of the edge functions
+   so t = EdgeFunction ... would it be better for the module to be edge functions? *)
+  module Value : Lattice
 
-  val compose_call : (Var.t -> t) -> call_info -> t state_update
+  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 compose_call : call_info -> Var.t dl -> t state_update
   (** edge calling a procedure *)
 
-  val compose_return : (Var.t -> t) -> call_info -> t state_update
+  val compose_return : ret_info -> Var.t dl -> t state_update
   (** edge return to after a call *)
 
-  val transfer : Program.stmt -> t state_update
-  (** update the state for a program statement *)
+  val compose_call_to_aftercall : Program.stmt -> Var.t dl -> t state_update
+  (** edge from a call to its aftercall 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 *)
+  val transfer : Program.stmt -> Var.t dl -> t state_update
+  (** update the state for a program statement *)
 end
 
 module IDELive = struct
-  module Const = struct
+  module Value = struct
     type t = bool [@@deriving eq, ord, show]
 
     let bottom = false
@@ -275,105 +321,87 @@ module IDELive = struct
     |> Iter.filter_map (function c, true -> Some c | _ -> None)
     |> Iter.to_string ~sep:", " (fun v -> Var.to_string v)
 
-  open Const
+  open Value
 
-  type t = Live | Dead | CondLive of Var.t [@@deriving eq, ord]
+  (*type t = Live | Dead | CondLive of Var.t [@@deriving eq, ord]*)
+  type t = IdEdge | ConstEdge of Value.t [@@deriving eq, ord]
 
-  let bottom = Dead
+  let bottom = ConstEdge dead
 
   let show v =
-    match v with
-    | Live -> "Live"
-    | Dead -> "Dead"
-    | CondLive v -> Var.to_string v
+    match v with IdEdge -> "IdEdge" | ConstEdge v -> "ConstEdge " ^ show v
 
   let pp fmt v = Format.pp_print_string fmt (show v)
-  let identity v = CondLive v
+  let identity = IdEdge
 
   (** 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)
+  let compose a b =
+    match (a, b) with
+    | IdEdge, b -> b
+    | a, IdEdge -> a
+    | ConstEdge v, ConstEdge v' -> ConstEdge v
   (** 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))
+    | 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
+  let compose_call c d = Iter.singleton (d, IdEdge)
+
+  let compose_return (r : ret_info) d =
+    match d with
+    | Lambda ->
+        List.fold_left
+          (fun i (_, out_expr) ->
+            Expr.BasilExpr.free_vars_iter out_expr
+            |> Iter.fold (fun i v -> Iter.cons (Label v, ConstEdge live) i) i)
+          (Iter.singleton (d, IdEdge))
+          r.rhs
+    | Label v when Var.is_global v -> Iter.empty
+    | Label v -> Iter.empty
+
+  let compose_call_to_aftercall stmt d =
+    match d with Lambda -> Iter.singleton (d, IdEdge) | Label _ -> Iter.empty
+
+  let transfer stmt d =
+    match d with
+    | Lambda -> (
+        let open Livevars in
+        let open Stmt in
+        match stmt with
+        | Instr_Assign _ -> Iter.empty
+        | _ ->
+            Stmt.free_vars_iter stmt
+            |> Iter.fold
+                 (fun i v -> Iter.cons (Label v, ConstEdge live) i)
+                 Iter.empty)
+    | Label v -> (
+        match stmt with
+        | Instr_Assign assigns ->
+            Iter.of_list assigns
+            |> Iter.filter (fun (v', _) -> Var.equal v v')
+            |> Iter.flat_map (fun (v, e) -> Expr.BasilExpr.free_vars_iter e)
+            |> Iter.fold (fun i v' -> Iter.cons (Label v', IdEdge) i) Iter.empty
+        (* 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
 
 (** FIXME:
@@ -383,247 +411,282 @@ end
     - 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)
+  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 -> \l l . bot *)
+      Non membership in the map means v v' -> const bottom *)
 
   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
+    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)) ->
+        "(" ^ Lambda.show v ^ "," ^ Lambda.show v' ^ "->" ^ D.show i)
 
-  let direction : [ `Forwards | `Backwards ] = `Backwards
+  let empty_summary = DlMap.empty
 
-  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))
+  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
-    globals @ locals
+    VarMap.add v j st
+
+  let direction : [ `Forwards | `Backwards ] = `Backwards
 
-  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))
+  (** Determine composites of edge functions through an intravertex block *)
+  let tf_stmts dir phi bs i =
+    let bs = match dir with `Forwards -> bs | `Backwards -> List.rev bs in
+    let stmts i =
+      List.fold_left
+        (fun efs stmt ->
+          Iter.flat_map
+            (fun (d2, e1) ->
+              D.transfer stmt d2
+              |> Iter.map (fun (d3, e2) -> (d3, D.compose e2 e1)))
+            efs)
+        i bs
     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))
+    (* 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 ->
+          Iter.of_list phi
+          |> Iter.flat_map (fun (p : Var.t Block.phi) ->
+              Iter.filter_map
+                (fun (d2, e) ->
+                  List.exists (fun (_, v) -> Lambda.equal (Label v) d2) p.rhs
+                  |> flip Option.return_if (Label p.lhs, e))
+                i)
+      | `Backwards ->
+          Iter.of_list phi
+          |> Iter.flat_map (fun (p : Var.t Block.phi) ->
+              Iter.filter (fun (d2, e) -> Lambda.equal (Label p.lhs) d2) i
+              |> Iter.flat_map (fun (d2, e) ->
+                  Iter.of_list p.rhs |> Iter.map (fun (_, d3) -> (Label d3, e))))
     in
-    globals @ locals
-
-  let tf_phis phis : (Var.t * D.t) Iter.t = Iter.empty
+    match dir with `Forwards -> stmts (phis i) | `Backwards -> phis (stmts i)
 
   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*)
+  let dldlget d1 d2 summary =
+    DlMap.get d1 summary |> Option.flat_map (DlMap.get d2)
+
+  let propagate worklist summaries priority summary loc updates =
+    let module Q = IntPQueue.Plain in
+    Iter.for_each updates (fun ((d1, d3), _) ->
+        Q.add worklist (loc, (d1, d3)) (priority loc));
+    Iter.filter_map
+      (fun ((d1, d3), e) ->
+        let l = dldlget d1 d3 summary |> Option.get_or ~default:D.bottom in
+        let j = D.join l e in
+        D.equal l j |> flip Option.return_if ((d1, d3), j))
+      updates
+    |> Iter.fold
+         (fun acc ((d1, d3), e) ->
+           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
+
+  let phase1_solve order dir start graph globals default =
     Trace.with_span ~__FILE__ ~__LINE__ "ide-phase1" @@ fun _ ->
     let module Q = IntPQueue.Plain in
-    let (worklist : edge Q.t) = Q.create () in
+    let (worklist : (Loc.t * Lambda2.t) 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)
+    (* Stores edge functions from the first procedure's entry to the second
+       procedure's entry where the d value of the second procedure's entry is
+       the given dl. *)
+    let entry_to_call_entry_cache :
+        (ID.t * Lambda.t * ID.t, D.t DlMap.t) Hashtbl.t =
+      Hashtbl.create 100
     in
-    IDEGraph.G.fold_edges_e (fun e a -> Q.add worklist e (priority e)) graph ();
+    (* 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 * Lambda.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
+    (*IDEGraph.G.fold_edges_e (fun e a -> Q.add worklist (e, (Lambda, Lambda) (priority e))) graph ();*)
+    Q.add worklist (start, (Lambda, Lambda)) (priority start);
     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)
+      let (x : Loc.t * Lambda2.t) =
+        Q.extract worklist |> Option.get_exn_or "queue empty"
       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;
-        ())
+      let l, (d1, d2) = x in
+      let ost = get_summary l in
+      let e1 = dldlget d1 d2 ost |> Option.get_exn_or "edge function missing" in
+      (match dir with
+        | `Forwards -> IDEGraph.G.succ_e graph l |> Iter.of_list
+        | `Backwards -> IDEGraph.G.pred_e graph l |> Iter.of_list)
+      |> Iter.iter (fun e ->
+          let from, target =
+            match (dir, e) with
+            | `Forwards, (from, _, target) -> (from, target)
+            | `Backwards, (target, _, from) -> (from, target)
+          in
+          match IDEGraph.G.E.label e with
+          | Stmts (phi, bs) ->
+              tf_stmts dir phi bs (Iter.singleton (d2, e1))
+              |> Iter.map (fun (d3, e) -> ((d1, d3), e))
+              |> propagate worklist summaries priority (get_summary target)
+                   target
+          | InterCall callinfo ->
+              (* This is not direction agnostic :( it would be nice to make the IDEGraph direction agnostic *)
+              D.compose_call callinfo d2
+              |> Iter.iter (fun (d3, e2) ->
+                  propagate worklist summaries priority (get_summary target)
+                    target
+                    (Iter.singleton ((d3, d3), D.identity));
+                  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;
+                  (* Surely there's a better way to do this... *)
+                  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.compose_return callinfo.ret d4
+                            |> Iter.map (fun (d5, e4) ->
+                                ((d1, d5), D.compose e4 e321))
+                            |> propagate worklist summaries priority
+                                 (get_summary target) target))
+                  in
+                  ())
+          | InterReturn retinfo ->
+              (* Duplicate work warning!! we're saving the summary of the procedure we're returning from multiple times!! *)
+              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;
+
+              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.compose_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.compose_call_to_aftercall callstmt 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
 
-  let phase2_solve order dir graph globals
+  let phase2_solve order dir start graph globals
       (summaries : (Loc.t, summary) Hashtbl.t) =
     (* FIXME: use summaries ; propertly evaluate call edges first then fill in between*)
     Trace.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 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 ->
           print_endline @@ "summary undefined " ^ Loc.show loc;
-          VarMap.empty
+          DlMap.empty
     in
-    IDEGraph.G.fold_edges_e (fun e a -> Q.add worklist e (priority e)) graph ();
+    (* The first step is to initialise the entry nodes of each procedure with
+       their initial value based on the entry procedure being initialised to
+       top, using the summary functions. *)
+    let (worklist : (Loc.t * Lambda.t) Q.t) = Q.create () in
+    let visited = ref LSet.empty in
+    Q.add worklist (start, Lambda) (priority start);
     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)
+      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
-      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;
-        ())
+      IDEGraph.G.succ_e graph l |> Iter.of_list
+      |> Iter.iter (fun e ->
+          let target =
+            match (dir, e) with
+            | `Forwards, (_, _, target) -> target
+            | `Backwards, (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.compose_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';
+                            Q.add worklist (target, d3) (priority target))
+                          else ()
+                      | _ -> ());
+                      ()))
+          | _ ->
+              if not (LSet.mem target !visited) then
+                Q.add worklist (target, d) (priority target);
+              visited := LSet.add target !visited)
     done;
-    constants
-
-  let query (r : (Loc.t, 'a VarMap.t) Hashtbl.t) ~proc_id vert =
-    Hashtbl.get r (IntraVertex { proc_id; v = vert })
+    (* We then apply all summary functions to each location *)
+    let entry_table = IDEGraph.vertex_to_entry_table graph in
+    flip IDEGraph.G.iter_vertex graph (fun l ->
+        let pst =
+          get_st
+            (LM.get l entry_table
+            |> Option.get_exn_or "vertex has no associated entry node")
+        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 dir (prog : Program.t) =
     Trace.with_span ~__FILE__ ~__LINE__ "ide-solve" @@ fun _ ->
@@ -637,8 +700,12 @@ module IDE (D : IDEDomain) = struct
       |> 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)
+    let start =
+      match dir with `Forwards -> Loc.Entry | `Backwards -> Loc.Exit
+    in
+    let summary = phase1_solve order dir start graph globals DlMap.empty in
+    ( query @@ summary,
+      query @@ phase2_solve order dir start graph globals summary )
 
   module G = Procedure.RevG
   module ResultMap = Map.Make (G.V)
@@ -656,7 +723,7 @@ end
 
 module IDELiveAnalysis = IDE (IDELive)
 
-let show_const_summary (v : IDELiveAnalysis.constant_state) =
+let show_state (v : IDELiveAnalysis.analysis_state) =
   VarMap.to_iter v |> IDELive.show_const_state
 
 let print_live_vars_dot sum r fmt prog proc_id =
@@ -679,6 +746,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)
+          print_live_vars_dot show_state (r ~proc_id:proc)
             (Format.of_chan s) prog proc));
   prog

From d40d7782c50f71eaa14f9b893274336ce197863c Mon Sep 17 00:00:00 2001
From: bpaul <bpaul@bpaul.xyz>
Date: Mon, 19 Jan 2026 15:31:10 +1000
Subject: [PATCH 02/16] Reverse graph when going backwards

---
 lib/transforms/ide.ml | 58 ++++++++++++++++++++++++++++---------------
 1 file changed, 38 insertions(+), 20 deletions(-)

diff --git a/lib/transforms/ide.ml b/lib/transforms/ide.ml
index 2bd9ea9..2321e55 100644
--- a/lib/transforms/ide.ml
+++ b/lib/transforms/ide.ml
@@ -46,6 +46,8 @@ end
 module LSet = Set.Make (Loc)
 module LM = Map.Make (Loc)
 
+let direction : [ `Forwards | `Backwards ] = `Backwards
+
 module IDEGraph = struct
   module Vert = struct
     include Loc
@@ -84,14 +86,24 @@ module IDEGraph = struct
     stmts : Var.t Block.phi list * Program.stmt list;
   }
 
-  let push_edge (ending : Loc.t) (g : bstate) =
+  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 = GB.add_edge_e graph e1; stmts = ([], []); last_vert = ending }
-
-  let add_call p (st : bstate) (origin : stmt_id) (callstmt : Program.stmt) =
+        {
+          graph = add_edge_e_dir dir 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 }) ->
@@ -120,13 +132,18 @@ module IDEGraph = struct
       | _ -> failwith "not a call"
     in
     let caller, callee = (origin.proc_id, target) in
-    let g = push_edge (CallSite origin) st in
+    let g = push_edge dir (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 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 graph =
       GB.add_edge_e graph
@@ -140,12 +157,12 @@ module IDEGraph = struct
     in
     { g with graph }
 
-  let proc_graph prog g p =
+  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 ->
-          GB.add_edge_e g
+          add_edge_e_dir dir g
             Loc.
               ( IntraVertex { proc_id; v = v1 },
                 Nop,
@@ -161,16 +178,18 @@ module IDEGraph = struct
               stmts = (b.phis, []);
             }
           in
-          Block.stmts_iter_i b
+          (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 prog st stmt_id c
+                 | 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 (IntraVertex { proc_id; v = End block })
+          |> push_edge dir (IntraVertex { proc_id; v = End block })
           |> fun x -> x.graph
       | _, _, _ -> failwith "bad proc edge"
     in
@@ -188,9 +207,9 @@ module IDEGraph = struct
     |> Option.map (fun procg -> Procedure.G.fold_edges_e add_block_edge procg g)
     |> Option.get_or ~default:g
 
-  let create (prog : Program.t) =
+  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) (GB.empty ())
+    |> Iter.fold (fun g p -> proc_graph prog g p dir) (GB.empty ())
 
   let vertex_to_entry_table g =
     let t = ref LM.empty in
@@ -352,9 +371,8 @@ module IDELive = struct
     | IdEdge, IdEdge -> IdEdge
 
   let eval f v = match f with IdEdge -> v | ConstEdge v -> v
-  let compose_call c d = Iter.singleton (d, IdEdge)
 
-  let compose_return (r : ret_info) d =
+  let compose_call (c : call_info) d =
     match d with
     | Lambda ->
         List.fold_left
@@ -362,10 +380,12 @@ module IDELive = struct
             Expr.BasilExpr.free_vars_iter out_expr
             |> Iter.fold (fun i v -> Iter.cons (Label v, ConstEdge live) i) i)
           (Iter.singleton (d, IdEdge))
-          r.rhs
+          c.rhs
     | Label v when Var.is_global v -> Iter.empty
     | Label v -> Iter.empty
 
+  let compose_return r d = Iter.singleton (d, IdEdge)
+
   let compose_call_to_aftercall stmt d =
     match d with Lambda -> Iter.singleton (d, IdEdge) | Label _ -> Iter.empty
 
@@ -434,8 +454,6 @@ module IDE (D : IDEDomain) = struct
     in
     VarMap.add v j st
 
-  let direction : [ `Forwards | `Backwards ] = `Backwards
-
   (** Determine composites of edge functions through an intravertex block *)
   let tf_stmts dir phi bs i =
     let bs = match dir with `Forwards -> bs | `Backwards -> List.rev bs in
@@ -691,7 +709,7 @@ module IDE (D : IDEDomain) = struct
   let solve dir (prog : Program.t) =
     Trace.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 graph = IDEGraph.create prog dir in
     let order =
       (match dir with
         | `Forwards -> Iter.from_iter (fun f -> IDEGraph.Top.iter f graph)
@@ -746,6 +764,6 @@ let transform (prog : Program.t) =
       CCIO.with_out
         ("idelive-const" ^ n ^ ".dot")
         (fun s ->
-          print_live_vars_dot show_state (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

From d69960791838c4e96fe94a72135d529ce9d41b25 Mon Sep 17 00:00:00 2001
From: bpaul <bpaul@bpaul.xyz>
Date: Mon, 19 Jan 2026 15:53:48 +1000
Subject: [PATCH 03/16] t

---
 lib/transforms/ide.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lib/transforms/ide.ml b/lib/transforms/ide.ml
index 2321e55..8c7fc8e 100644
--- a/lib/transforms/ide.ml
+++ b/lib/transforms/ide.ml
@@ -747,7 +747,7 @@ let show_state (v : IDELiveAnalysis.analysis_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.with_span ~__FILE__ ~__LINE__ "dot-priner" @@ fun _ ->
+  Trace.with_span ~__FILE__ ~__LINE__ "dot-printer" @@ fun _ ->
   let (module M : Viscfg.ProcPrinter) = Viscfg.dot_labels (fun v -> label v) in
   Option.iter (fun g -> M.fprint_graph fmt g) (Procedure.graph p)
 

From 3bc58062c4e18cbfe84bef284d05183ea6608e30 Mon Sep 17 00:00:00 2001
From: bpaul <bpaul@bpaul.xyz>
Date: Wed, 21 Jan 2026 11:11:01 +1000
Subject: [PATCH 04/16] Visualise the ide graph

---
 lib/transforms/ide.ml | 127 +++++++++++++++++++++++++++---------------
 1 file changed, 82 insertions(+), 45 deletions(-)

diff --git a/lib/transforms/ide.ml b/lib/transforms/ide.ml
index 8c7fc8e..9a260c8 100644
--- a/lib/transforms/ide.ml
+++ b/lib/transforms/ide.ml
@@ -155,7 +155,7 @@ module IDEGraph = struct
     let graph =
       GB.add_edge_e graph (call_return, InterReturn ret_info, AfterCall origin)
     in
-    { g with graph }
+    { g with graph; last_vert = AfterCall origin }
 
   let proc_graph prog g p dir =
     let proc_id = Procedure.id p in
@@ -203,6 +203,13 @@ module IDEGraph = struct
             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:g
@@ -211,38 +218,6 @@ module IDEGraph = struct
     ID.Map.to_iter prog.procs |> Iter.map snd
     |> Iter.fold (fun g p -> proc_graph prog g p dir) (GB.empty ())
 
-  let vertex_to_entry_table g =
-    let t = ref LM.empty in
-    let s = Stack.create () in
-    G.iter_vertex
-      (function
-        | IntraVertex { proc_id; v = l } as v
-          when Procedure.Vert.equal l Procedure.Vert.Entry ->
-            Stack.push v s
-        | _ -> ())
-      g;
-    while not (Stack.is_empty s) do
-      let entry = Stack.pop s in
-      let s2 = Stack.create () in
-      Stack.push entry s2;
-      let vis = ref (LSet.singleton entry) in
-      while not (Stack.is_empty s2) do
-        let v = Stack.pop s2 in
-        G.iter_succ_e
-          (fun (_, e, v2) ->
-            match e with
-            | Stmts _ | Call _ | Nop ->
-                if not (LSet.mem v2 !vis) then (
-                  vis := LSet.add v2 !vis;
-                  Stack.push v2 s2)
-                else ()
-            | _ -> ())
-          g v
-      done;
-      ()
-    done;
-    !t
-
   module RevTop = Graph.Topological.Make (struct
     type t = G.t
 
@@ -260,6 +235,60 @@ module IDEGraph = struct
   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 } ->
+          "\""
+          ^ 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 } ->
+            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, _ -> ""
+      in
+      [ `Label l ]
+
+    let default_edge_attributes _ = []
+    let get_subgraph _ = None
+  end)
 end
 
 module type Lattice = sig
@@ -335,7 +364,7 @@ module IDELive = struct
       | false, false -> false
   end
 
-  let show_const_state s =
+  let show_state s =
     s
     |> Iter.filter_map (function c, true -> Some c | _ -> None)
     |> Iter.to_string ~sep:", " (fun v -> Var.to_string v)
@@ -491,7 +520,9 @@ module IDE (D : IDEDomain) = struct
   type edge = Loc.t * IDEGraph.Edge.t * Loc.t
 
   let dldlget d1 d2 summary =
-    DlMap.get d1 summary |> Option.flat_map (DlMap.get d2)
+    DlMap.get d1 summary
+    |> Option.flat_map (DlMap.get d2)
+    |> Option.get_or ~default:D.bottom
 
   let propagate worklist summaries priority summary loc updates =
     let module Q = IntPQueue.Plain in
@@ -499,7 +530,7 @@ module IDE (D : IDEDomain) = struct
         Q.add worklist (loc, (d1, d3)) (priority loc));
     Iter.filter_map
       (fun ((d1, d3), e) ->
-        let l = dldlget d1 d3 summary |> Option.get_or ~default:D.bottom in
+        let l = dldlget d1 d3 summary in
         let j = D.join l e in
         D.equal l j |> flip Option.return_if ((d1, d3), j))
       updates
@@ -536,7 +567,7 @@ module IDE (D : IDEDomain) = struct
       in
       let l, (d1, d2) = x in
       let ost = get_summary l in
-      let e1 = dldlget d1 d2 ost |> Option.get_exn_or "edge function missing" in
+      let e1 = dldlget d1 d2 ost in
       (match dir with
         | `Forwards -> IDEGraph.G.succ_e graph l |> Iter.of_list
         | `Backwards -> IDEGraph.G.pred_e graph l |> Iter.of_list)
@@ -680,13 +711,16 @@ module IDE (D : IDEDomain) = struct
               visited := LSet.add target !visited)
     done;
     (* We then apply all summary functions to each location *)
-    let entry_table = IDEGraph.vertex_to_entry_table graph in
+    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
-            (LM.get l entry_table
-            |> Option.get_exn_or "vertex has no associated entry node")
-        in
+        let pst = get_st (entry_of l) in
         get_summary l
         |> DlMap.iter (fun d1 ->
             let x =
@@ -742,16 +776,19 @@ end
 module IDELiveAnalysis = IDE (IDELive)
 
 let show_state (v : IDELiveAnalysis.analysis_state) =
-  VarMap.to_iter v |> IDELive.show_const_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.with_span ~__FILE__ ~__LINE__ "dot-printer" @@ fun _ ->
-  let (module M : Viscfg.ProcPrinter) = Viscfg.dot_labels (fun v -> label v) in
+  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 g = IDEGraph.create prog `Backwards in
+  CCIO.with_out "idegraph.dot" (fun s ->
+      IDEGraph.Vis.fprint_graph (Format.of_chan s) g);
   let summary, r = IDELiveAnalysis.solve `Backwards prog in
   ID.Map.to_iter prog.procs
   |> Iter.iter (fun (proc, proc_n) ->

From c79e1c4cc5389ea6fbffce5334bafe30921a6e62 Mon Sep 17 00:00:00 2001
From: bpaul <bpaul@bpaul.xyz>
Date: Wed, 21 Jan 2026 11:53:00 +1000
Subject: [PATCH 05/16] Emit something

---
 lib/transforms/ide.ml | 88 ++++++++++++++++++++++++++++---------------
 1 file changed, 57 insertions(+), 31 deletions(-)

diff --git a/lib/transforms/ide.ml b/lib/transforms/ide.ml
index 9a260c8..f294546 100644
--- a/lib/transforms/ide.ml
+++ b/lib/transforms/ide.ml
@@ -97,7 +97,7 @@ module IDEGraph = struct
         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 dir graph e1;
+          graph = add_edge_e_dir `Forwards graph e1;
           stmts = ([], []);
           last_vert = ending;
         }
@@ -174,7 +174,15 @@ module IDEGraph = struct
           let is =
             {
               graph;
-              last_vert = IntraVertex { proc_id; v = Begin block };
+              last_vert =
+                IntraVertex
+                  {
+                    proc_id;
+                    v =
+                      (match dir with
+                      | `Forwards -> Begin block
+                      | `Backwards -> End block);
+                  };
               stmts = (b.phis, []);
             }
           in
@@ -189,7 +197,15 @@ module IDEGraph = struct
                  | stmt ->
                      { st with stmts = (fst st.stmts, stmt :: snd st.stmts) })
                is
-          |> push_edge dir (IntraVertex { proc_id; v = End block })
+          |> 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
@@ -424,12 +440,12 @@ module IDELive = struct
         let open Livevars in
         let open Stmt in
         match stmt with
-        | Instr_Assign _ -> Iter.empty
+        | Instr_Assign _ -> Iter.singleton (d, IdEdge)
         | _ ->
             Stmt.free_vars_iter stmt
             |> Iter.fold
                  (fun i v -> Iter.cons (Label v, ConstEdge live) i)
-                 Iter.empty)
+                 (Iter.singleton (d, IdEdge)))
     | Label v -> (
         match stmt with
         | Instr_Assign assigns ->
@@ -471,7 +487,7 @@ module IDE (D : IDEDomain) = struct
     |> Iter.flat_map (fun (d1, m) ->
         DlMap.to_iter m |> Iter.map (fun x -> (d1, x)))
     |> Iter.to_string ~sep:", " (fun (v, (v', i)) ->
-        "(" ^ Lambda.show v ^ "," ^ Lambda.show v' ^ "->" ^ D.show i)
+        "(" ^ Lambda.show v ^ "," ^ Lambda.show v' ^ "->" ^ D.show i ^ ")")
 
   let empty_summary = DlMap.empty
 
@@ -485,7 +501,7 @@ module IDE (D : IDEDomain) = struct
 
   (** Determine composites of edge functions through an intravertex block *)
   let tf_stmts dir phi bs i =
-    let bs = match dir with `Forwards -> bs | `Backwards -> List.rev bs in
+    (*let bs = match dir with `Forwards -> bs | `Backwards -> List.rev bs in*)
     let stmts i =
       List.fold_left
         (fun efs stmt ->
@@ -501,19 +517,26 @@ module IDE (D : IDEDomain) = struct
     let phis i =
       match dir with
       | `Forwards ->
-          Iter.of_list phi
-          |> Iter.flat_map (fun (p : Var.t Block.phi) ->
-              Iter.filter_map
+          List.fold_left
+            (fun i (p : Var.t Block.phi) ->
+              Iter.map
                 (fun (d2, e) ->
-                  List.exists (fun (_, v) -> Lambda.equal (Label v) d2) p.rhs
-                  |> flip Option.return_if (Label p.lhs, e))
+                  if List.exists (fun (_, v) -> Lambda.equal (Label v) d2) p.rhs
+                  then (Label p.lhs, e)
+                  else (d2, e))
                 i)
+            i phi
       | `Backwards ->
-          Iter.of_list phi
-          |> Iter.flat_map (fun (p : Var.t Block.phi) ->
-              Iter.filter (fun (d2, e) -> Lambda.equal (Label p.lhs) d2) i
-              |> Iter.flat_map (fun (d2, e) ->
-                  Iter.of_list p.rhs |> Iter.map (fun (_, d3) -> (Label d3, e))))
+          List.fold_left
+            (fun i (p : Var.t Block.phi) ->
+              Iter.flat_map
+                (fun (d2, e) ->
+                  if Lambda.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)
 
@@ -526,16 +549,16 @@ module IDE (D : IDEDomain) = struct
 
   let propagate worklist summaries priority summary loc updates =
     let module Q = IntPQueue.Plain in
-    Iter.for_each updates (fun ((d1, d3), _) ->
-        Q.add worklist (loc, (d1, d3)) (priority loc));
     Iter.filter_map
       (fun ((d1, d3), e) ->
         let l = dldlget d1 d3 summary in
         let j = D.join l e in
-        D.equal l j |> flip Option.return_if ((d1, d3), j))
+        print_endline (Lambda.show d3 ^ " " ^ D.show j);
+        (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
@@ -546,6 +569,8 @@ module IDE (D : IDEDomain) = struct
     let module Q = IntPQueue.Plain in
     let (worklist : (Loc.t * Lambda2.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 where the d value of the second procedure's entry is
        the given dl. *)
@@ -567,16 +592,15 @@ module IDE (D : IDEDomain) = struct
       in
       let l, (d1, d2) = x in
       let ost = get_summary l in
+      print_endline @@ show_summary ost;
       let e1 = dldlget d1 d2 ost in
-      (match dir with
-        | `Forwards -> IDEGraph.G.succ_e graph l |> Iter.of_list
-        | `Backwards -> IDEGraph.G.pred_e graph l |> Iter.of_list)
+      print_endline
+        (Loc.show l ^ ": " ^ Lambda.show d1 ^ ", " ^ Lambda.show d2 ^ ", "
+       ^ D.show e1);
+      IDEGraph.G.succ_e graph l |> Iter.of_list
       |> Iter.iter (fun e ->
-          let from, target =
-            match (dir, e) with
-            | `Forwards, (from, _, target) -> (from, target)
-            | `Backwards, (target, _, from) -> (from, target)
-          in
+          let from, target = match e with from, _, target -> (from, target) in
+          print_endline (Loc.show target);
           match IDEGraph.G.E.label e with
           | Stmts (phi, bs) ->
               tf_stmts dir phi bs (Iter.singleton (d2, e1))
@@ -658,7 +682,8 @@ module IDE (D : IDEDomain) = struct
       Hashtbl.get summaries loc |> function
       | Some e -> e
       | None ->
-          print_endline @@ "summary undefined " ^ Loc.show loc;
+          (*
+          print_endline @@ "summary undefined " ^ Loc.show loc;*)
           DlMap.empty
     in
     (* The first step is to initialise the entry nodes of each procedure with
@@ -680,7 +705,7 @@ module IDE (D : IDEDomain) = struct
           let target =
             match (dir, e) with
             | `Forwards, (_, _, target) -> target
-            | `Backwards, (target, _, _) -> target
+            | `Backwards, (_, _, target) -> target
           in
           match IDEGraph.G.E.label e with
           | InterCall callinfo ->
@@ -715,7 +740,8 @@ module IDE (D : IDEDomain) = struct
       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 }
+      | AfterCall stmt_id ->
+          IntraVertex { proc_id = stmt_id.proc_id; v = Entry }
       | Entry -> Entry
       | Exit -> Entry
     in

From 210d6552c1cb3658de424288e559c1393fdb7bcf Mon Sep 17 00:00:00 2001
From: bpaul <bpaul@bpaul.xyz>
Date: Wed, 21 Jan 2026 12:14:43 +1000
Subject: [PATCH 06/16] Fix assign transfer

---
 lib/transforms/ide.ml | 22 ++++++++++++++--------
 1 file changed, 14 insertions(+), 8 deletions(-)

diff --git a/lib/transforms/ide.ml b/lib/transforms/ide.ml
index f294546..1e16ce4 100644
--- a/lib/transforms/ide.ml
+++ b/lib/transforms/ide.ml
@@ -449,10 +449,23 @@ module IDELive = struct
     | Label v -> (
         match stmt with
         | Instr_Assign assigns ->
+            List.fold_left
+              (fun i (v', ex) ->
+                Iter.flat_map
+                  (fun (d, e) ->
+                    if Lambda.equal d (Label v') then
+                      Expr.BasilExpr.free_vars_iter ex
+                      |> Iter.map (fun v' -> (Label v', IdEdge))
+                    else Iter.singleton (Label v, e))
+                  i)
+              (Iter.singleton (d, IdEdge))
+              assigns
+        (*
             Iter.of_list assigns
             |> Iter.filter (fun (v', _) -> Var.equal v v')
             |> Iter.flat_map (fun (v, e) -> Expr.BasilExpr.free_vars_iter e)
             |> Iter.fold (fun i v' -> Iter.cons (Label v', IdEdge) i) Iter.empty
+            *)
         (* 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 ? *)
@@ -553,7 +566,6 @@ module IDE (D : IDEDomain) = struct
       (fun ((d1, d3), e) ->
         let l = dldlget d1 d3 summary in
         let j = D.join l e in
-        print_endline (Lambda.show d3 ^ " " ^ D.show j);
         (not (D.equal l j)) |> flip Option.return_if ((d1, d3), j))
       updates
     |> Iter.fold
@@ -592,15 +604,10 @@ module IDE (D : IDEDomain) = struct
       in
       let l, (d1, d2) = x in
       let ost = get_summary l in
-      print_endline @@ show_summary ost;
       let e1 = dldlget d1 d2 ost in
-      print_endline
-        (Loc.show l ^ ": " ^ Lambda.show d1 ^ ", " ^ Lambda.show d2 ^ ", "
-       ^ D.show e1);
       IDEGraph.G.succ_e graph l |> Iter.of_list
       |> Iter.iter (fun e ->
           let from, target = match e with from, _, target -> (from, target) in
-          print_endline (Loc.show target);
           match IDEGraph.G.E.label e with
           | Stmts (phi, bs) ->
               tf_stmts dir phi bs (Iter.singleton (d2, e1))
@@ -682,8 +689,7 @@ module IDE (D : IDEDomain) = struct
       Hashtbl.get summaries loc |> function
       | Some e -> e
       | None ->
-          (*
-          print_endline @@ "summary undefined " ^ Loc.show loc;*)
+          print_endline @@ "summary undefined " ^ Loc.show loc;
           DlMap.empty
     in
     (* The first step is to initialise the entry nodes of each procedure with

From 4944a951bb9aba865dc455ea1804e124c9018965 Mon Sep 17 00:00:00 2001
From: bpaul <bpaul@bpaul.xyz>
Date: Wed, 21 Jan 2026 15:41:00 +1000
Subject: [PATCH 07/16] Join edge functions when tf-ing a block

---
 lib/transforms/ide.ml | 35 ++++++++++++++++++++---------------
 1 file changed, 20 insertions(+), 15 deletions(-)

diff --git a/lib/transforms/ide.ml b/lib/transforms/ide.ml
index 1e16ce4..1fb6335 100644
--- a/lib/transforms/ide.ml
+++ b/lib/transforms/ide.ml
@@ -390,7 +390,7 @@ module IDELive = struct
   (*type t = Live | Dead | CondLive of Var.t [@@deriving eq, ord]*)
   type t = IdEdge | ConstEdge of Value.t [@@deriving eq, ord]
 
-  let bottom = ConstEdge dead
+  let bottom = ConstEdge bottom
 
   let show v =
     match v with IdEdge -> "IdEdge" | ConstEdge v -> "ConstEdge " ^ show v
@@ -404,7 +404,6 @@ module IDELive = struct
     | IdEdge, b -> b
     | a, IdEdge -> a
     | ConstEdge v, ConstEdge v' -> ConstEdge v
-  (** not representible *)
 
   let join a b =
     match (a, b) with
@@ -435,10 +434,9 @@ module IDELive = struct
     match d with Lambda -> Iter.singleton (d, IdEdge) | Label _ -> Iter.empty
 
   let transfer stmt d =
+    let open Stmt in
     match d with
     | Lambda -> (
-        let open Livevars in
-        let open Stmt in
         match stmt with
         | Instr_Assign _ -> Iter.singleton (d, IdEdge)
         | _ ->
@@ -456,7 +454,7 @@ module IDELive = struct
                     if Lambda.equal d (Label v') then
                       Expr.BasilExpr.free_vars_iter ex
                       |> Iter.map (fun v' -> (Label v', IdEdge))
-                    else Iter.singleton (Label v, e))
+                    else Iter.singleton (d, e))
                   i)
               (Iter.singleton (d, IdEdge))
               assigns
@@ -517,13 +515,21 @@ module IDE (D : IDEDomain) = struct
     (*let bs = match dir with `Forwards -> bs | `Backwards -> List.rev bs in*)
     let stmts i =
       List.fold_left
-        (fun efs stmt ->
-          Iter.flat_map
-            (fun (d2, e1) ->
+        (fun om stmt ->
+          DlMap.fold
+            (fun d2 e1 m ->
               D.transfer stmt d2
-              |> Iter.map (fun (d3, e2) -> (d3, D.compose e2 e1)))
-            efs)
-        i bs
+              |> Iter.fold
+                   (fun m (d3, e2) ->
+                     let e = D.compose e2 e1 in
+                     let j = D.join e (DlMap.get_or d3 m ~default:D.bottom) in
+                     if not (D.equal j D.bottom) then DlMap.add d3 j m else m)
+                   m)
+            om DlMap.empty)
+        (* Should be joining i *)
+        (DlMap.of_iter 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 *)
@@ -777,9 +783,7 @@ module IDE (D : IDEDomain) = struct
     let globals = prog.globals |> Var.Decls.to_iter |> Iter.map snd in
     let graph = IDEGraph.create prog dir 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.from_iter (fun f -> IDEGraph.Top.iter f graph)
       |> Iter.zip_i
       |> Iter.map (fun (i, v) -> (v, i))
       |> LM.of_iter
@@ -818,9 +822,10 @@ let print_live_vars_dot sum r fmt prog proc_id =
   Option.iter (fun g -> M.fprint_graph fmt g) (Procedure.graph p)
 
 let transform (prog : Program.t) =
+  (*
   let g = IDEGraph.create prog `Backwards in
   CCIO.with_out "idegraph.dot" (fun s ->
-      IDEGraph.Vis.fprint_graph (Format.of_chan s) g);
+      IDEGraph.Vis.fprint_graph (Format.of_chan s) g);*)
   let summary, r = IDELiveAnalysis.solve `Backwards prog in
   ID.Map.to_iter prog.procs
   |> Iter.iter (fun (proc, proc_n) ->

From 71b90b565053b41531030c579d3c294540eb7e3d Mon Sep 17 00:00:00 2001
From: bpaul <bpaul@bpaul.xyz>
Date: Wed, 21 Jan 2026 15:49:55 +1000
Subject: [PATCH 08/16] Fix call returnflow logic

---
 lib/transforms/ide.ml | 47 ++++++++++++++++++++++++++-----------------
 1 file changed, 28 insertions(+), 19 deletions(-)

diff --git a/lib/transforms/ide.ml b/lib/transforms/ide.ml
index 1fb6335..728a7c5 100644
--- a/lib/transforms/ide.ml
+++ b/lib/transforms/ide.ml
@@ -8,6 +8,21 @@ open Lang
 open Containers
 open Common
 
+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;
@@ -21,6 +36,7 @@ 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;
@@ -28,21 +44,6 @@ type call_info = {
 [@@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 LSet = Set.Make (Loc)
 module LM = Map.Make (Loc)
 
@@ -149,7 +150,15 @@ module IDEGraph = struct
       GB.add_edge_e graph
         ( CallSite origin,
           InterCall
-            { rhs; lhs; call_from = callstmt; caller; callee; ret = ret_info },
+            {
+              rhs;
+              lhs;
+              call_from = callstmt;
+              aftercall = origin;
+              caller;
+              callee;
+              ret = ret_info;
+            },
           call_entry )
     in
     let graph =
@@ -526,7 +535,7 @@ module IDE (D : IDEDomain) = struct
                      if not (D.equal j D.bottom) then DlMap.add d3 j m else m)
                    m)
             om DlMap.empty)
-        (* Should be joining i *)
+        (* TODO Should be joining i *)
         (DlMap.of_iter i)
         bs
       |> DlMap.to_iter
@@ -621,7 +630,6 @@ module IDE (D : IDEDomain) = struct
               |> propagate worklist summaries priority (get_summary target)
                    target
           | InterCall callinfo ->
-              (* This is not direction agnostic :( it would be nice to make the IDEGraph direction agnostic *)
               D.compose_call callinfo d2
               |> Iter.iter (fun (d3, e2) ->
                   propagate worklist summaries priority (get_summary target)
@@ -636,6 +644,7 @@ module IDE (D : IDEDomain) = struct
                   in
                   Hashtbl.add entry_to_call_entry_cache k m;
                   (* Surely there's a better way to do this... *)
+                  let aftercall = Loc.AfterCall callinfo.aftercall in
                   let _ =
                     Hashtbl.get entry_to_exit_cache (callinfo.callee, d3)
                     |> Option.map (fun m ->
@@ -646,7 +655,7 @@ module IDE (D : IDEDomain) = struct
                             |> Iter.map (fun (d5, e4) ->
                                 ((d1, d5), D.compose e4 e321))
                             |> propagate worklist summaries priority
-                                 (get_summary target) target))
+                                 (get_summary aftercall) aftercall))
                   in
                   ())
           | InterReturn retinfo ->

From f075809727317fd3bdedce05f53167bad4d1af6e Mon Sep 17 00:00:00 2001
From: bpaul <bpaul@bpaul.xyz>
Date: Wed, 21 Jan 2026 16:44:14 +1000
Subject: [PATCH 09/16] Fix phase 2 procedure start propagation

---
 lib/transforms/ide.ml | 47 ++++++++++++++++++++++++++-----------------
 1 file changed, 29 insertions(+), 18 deletions(-)

diff --git a/lib/transforms/ide.ml b/lib/transforms/ide.ml
index 728a7c5..6486a7d 100644
--- a/lib/transforms/ide.ml
+++ b/lib/transforms/ide.ml
@@ -243,6 +243,18 @@ module IDEGraph = struct
     ID.Map.to_iter prog.procs |> Iter.map snd
     |> Iter.fold (fun g p -> proc_graph prog g p dir) (GB.empty ())
 
+  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
 
@@ -429,11 +441,9 @@ module IDELive = struct
     match d with
     | Lambda ->
         List.fold_left
-          (fun i (_, out_expr) ->
-            Expr.BasilExpr.free_vars_iter out_expr
-            |> Iter.fold (fun i v -> Iter.cons (Label v, ConstEdge live) i) i)
+          (fun i (_, out) -> Iter.cons (Label out, IdEdge) i)
           (Iter.singleton (d, IdEdge))
-          c.rhs
+          c.lhs
     | Label v when Var.is_global v -> Iter.empty
     | Label v -> Iter.empty
 
@@ -692,7 +702,7 @@ module IDE (D : IDEDomain) = struct
     done;
     summaries
 
-  let phase2_solve order dir start graph globals
+  let phase2_solve order dir prog start_proc graph globals
       (summaries : (Loc.t, summary) Hashtbl.t) =
     (* FIXME: use summaries ; propertly evaluate call edges first then fill in between*)
     Trace.with_span ~__FILE__ ~__LINE__ "ide-phase2" @@ fun _ ->
@@ -711,8 +721,9 @@ module IDE (D : IDEDomain) = struct
        their initial value based on the entry procedure being initialised to
        top, using the summary functions. *)
     let (worklist : (Loc.t * Lambda.t) Q.t) = Q.create () in
-    let visited = ref LSet.empty in
-    Q.add worklist (start, Lambda) (priority start);
+    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
@@ -723,11 +734,7 @@ module IDE (D : IDEDomain) = struct
       in
       IDEGraph.G.succ_e graph l |> Iter.of_list
       |> Iter.iter (fun e ->
-          let target =
-            match (dir, e) with
-            | `Forwards, (_, _, target) -> target
-            | `Backwards, (_, _, target) -> target
-          in
+          let target = match e with _, _, target -> target in
           match IDEGraph.G.E.label e with
           | InterCall callinfo ->
               let summary = get_summary l in
@@ -747,14 +754,15 @@ module IDE (D : IDEDomain) = struct
                           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';
-                            Q.add worklist (target, d3) (priority target))
+                            (* This should really add all calls in the target procedure to the worklist *)
+                            Hashtbl.get_or calls_table callinfo.callee
+                              ~default:Iter.empty
+                            |> Iter.iter (fun c ->
+                                Q.add worklist (c, d3) (priority c)))
                           else ()
                       | _ -> ());
                       ()))
-          | _ ->
-              if not (LSet.mem target !visited) then
-                Q.add worklist (target, d) (priority target);
-              visited := LSet.add target !visited)
+          | _ -> ())
     done;
     (* We then apply all summary functions to each location *)
     let entry_of (l : Loc.t) =
@@ -800,9 +808,12 @@ module IDE (D : IDEDomain) = struct
     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 dir start graph globals DlMap.empty in
     ( query @@ summary,
-      query @@ phase2_solve order dir start graph globals summary )
+      query @@ phase2_solve order dir prog start_proc graph globals summary )
 
   module G = Procedure.RevG
   module ResultMap = Map.Make (G.V)

From c164e562b2ec40af957cd3bfda49b6b8b00fc2bc Mon Sep 17 00:00:00 2001
From: bpaul <bpaul@bpaul.xyz>
Date: Thu, 22 Jan 2026 10:14:20 +1000
Subject: [PATCH 10/16] docs

---
 lib/transforms/ide.ml | 174 +++++++++++++++++++++++-------------------
 1 file changed, 96 insertions(+), 78 deletions(-)

diff --git a/lib/transforms/ide.ml b/lib/transforms/ide.ml
index 6486a7d..f561ad4 100644
--- a/lib/transforms/ide.ml
+++ b/lib/transforms/ide.ml
@@ -1,13 +1,16 @@
-(** 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 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 }]
@@ -243,6 +246,8 @@ module IDEGraph = struct
     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
@@ -333,36 +338,26 @@ module type Lattice = sig
 
   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
 
-(* TODO rename these types !!!!!!!!!!!!! *)
-
-(** blah blah blah *)
-type 'a dl = Label of 'a | Lambda [@@deriving eq, ord, show]
-
-module Lambda = struct
+module DL = struct
   (* TODO not Var.t (want more generality e.g. dsa uses symbolic addresses in scala code) *)
-  type t = Var.t dl [@@deriving eq, ord, show]
-  (** blah blah blah *)
-end
-
-module Lambda2 = struct
-  type t = Lambda.t * Lambda.t [@@deriving eq, ord, show]
+  type t = Label of Var.t | Lambda [@@deriving eq, ord, show]
 end
 
-module DlMap = Map.Make (Lambda)
+module DlMap = Map.Make (DL)
 
-type 'a state_update = (Var.t dl * 'a) Iter.t
+type 'a state_update = (DL.t * 'a) Iter.t
 
+(** An IDE domain where values are edge functions *)
 module type IDEDomain = sig
   include Lattice
 
-  (* idk how to document this but the ordering of this domain should be of the edge functions
-   so t = EdgeFunction ... would it be better for the module to be edge functions? *)
+  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 *)
@@ -373,20 +368,23 @@ module type IDEDomain = sig
   val eval : t -> Value.t -> Value.t
   (** evaluate an edge function *)
 
-  val compose_call : call_info -> Var.t dl -> t state_update
-  (** edge calling a procedure *)
+  val transfer_call : call_info -> DL.t -> t state_update
+  (** edge calling a procedure (to the return block when backwards) *)
 
-  val compose_return : ret_info -> Var.t dl -> t state_update
-  (** edge return to after a call *)
+  val transfer_return : ret_info -> DL.t -> t state_update
+  (** edge return from a call (from the entry block when backwards) *)
 
-  val compose_call_to_aftercall : Program.stmt -> Var.t dl -> t state_update
-  (** edge from a call to its aftercall statement *)
+  val transfer_call_to_aftercall : Program.stmt -> DL.t -> t state_update
+  (** edge from a call to its aftercall statement (or reversed when backwards)
+  *)
 
-  val transfer : Program.stmt -> Var.t dl -> t state_update
+  val transfer : Program.stmt -> DL.t -> t state_update
   (** update the state for a program statement *)
 end
 
 module IDELive = struct
+  let direction = `Backwards
+
   module Value = struct
     type t = bool [@@deriving eq, ord, show]
 
@@ -437,7 +435,9 @@ module IDELive = struct
 
   let eval f v = match f with IdEdge -> v | ConstEdge v -> v
 
-  let compose_call (c : call_info) d =
+  open DL
+
+  let transfer_call (c : call_info) d =
     match d with
     | Lambda ->
         List.fold_left
@@ -447,9 +447,10 @@ module IDELive = struct
     | Label v when Var.is_global v -> Iter.empty
     | Label v -> Iter.empty
 
-  let compose_return r d = Iter.singleton (d, IdEdge)
+  let transfer_return r d = Iter.singleton (d, IdEdge)
 
-  let compose_call_to_aftercall stmt d =
+  (* TODO preserve locals that aren't involved in the call *)
+  let transfer_call_to_aftercall stmt d =
     match d with Lambda -> Iter.singleton (d, IdEdge) | Label _ -> Iter.empty
 
   let transfer stmt d =
@@ -470,19 +471,13 @@ module IDELive = struct
               (fun i (v', ex) ->
                 Iter.flat_map
                   (fun (d, e) ->
-                    if Lambda.equal d (Label v') then
+                    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
-        (*
-            Iter.of_list assigns
-            |> Iter.filter (fun (v', _) -> Var.equal v v')
-            |> Iter.flat_map (fun (v, e) -> Expr.BasilExpr.free_vars_iter e)
-            |> Iter.fold (fun i v' -> Iter.cons (Label v', IdEdge) i) Iter.empty
-            *)
         (* 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 ? *)
@@ -502,8 +497,7 @@ 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 *)
+      only ; composition across calls should include the globals *)
 
 module IDE (D : IDEDomain) = struct
   type summary = D.t DlMap.t DlMap.t [@@deriving eq, ord]
@@ -512,12 +506,16 @@ module IDE (D : IDEDomain) = struct
 
       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)) ->
-        "(" ^ Lambda.show v ^ "," ^ Lambda.show v' ^ "->" ^ D.show i ^ ")")
+        "(" ^ DL.show v ^ "," ^ DL.show v' ^ "->" ^ D.show i ^ ")")
 
   let empty_summary = DlMap.empty
 
@@ -530,8 +528,7 @@ module IDE (D : IDEDomain) = struct
     VarMap.add v j st
 
   (** Determine composites of edge functions through an intravertex block *)
-  let tf_stmts dir phi bs i =
-    (*let bs = match dir with `Forwards -> bs | `Backwards -> List.rev bs in*)
+  let tf_stmts phi bs i =
     let stmts i =
       List.fold_left
         (fun om stmt ->
@@ -559,7 +556,7 @@ module IDE (D : IDEDomain) = struct
             (fun i (p : Var.t Block.phi) ->
               Iter.map
                 (fun (d2, e) ->
-                  if List.exists (fun (_, v) -> Lambda.equal (Label v) d2) p.rhs
+                  if List.exists (fun (_, v) -> DL.equal (Label v) d2) p.rhs
                   then (Label p.lhs, e)
                   else (d2, e))
                 i)
@@ -569,7 +566,7 @@ module IDE (D : IDEDomain) = struct
             (fun i (p : Var.t Block.phi) ->
               Iter.flat_map
                 (fun (d2, e) ->
-                  if Lambda.equal (Label p.lhs) d2 then
+                  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))
@@ -585,6 +582,7 @@ module IDE (D : IDEDomain) = struct
     |> 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
@@ -595,39 +593,44 @@ module IDE (D : IDEDomain) = struct
       updates
     |> Iter.fold
          (fun acc ((d1, d3), e) ->
-           Q.add worklist (loc, (d1, d3)) (priority loc);
+           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
 
-  let phase1_solve order dir start graph globals default =
+  (** 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.with_span ~__FILE__ ~__LINE__ "ide-phase1" @@ fun _ ->
     let module Q = IntPQueue.Plain in
-    let (worklist : (Loc.t * Lambda2.t) Q.t) = Q.create () 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 where the d value of the second procedure's entry is
-       the given dl. *)
-    let entry_to_call_entry_cache :
-        (ID.t * Lambda.t * ID.t, D.t DlMap.t) Hashtbl.t =
+       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 * Lambda.t, D.t DlMap.t) Hashtbl.t =
+    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
-    (*IDEGraph.G.fold_edges_e (fun e a -> Q.add worklist (e, (Lambda, Lambda) (priority e))) graph ();*)
-    Q.add worklist (start, (Lambda, Lambda)) (priority start);
+    Q.add worklist (start, Lambda, Lambda) (priority start);
     while not (Q.is_empty worklist) do
-      let (x : Loc.t * Lambda2.t) =
+      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 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
@@ -635,16 +638,19 @@ module IDE (D : IDEDomain) = struct
           let from, target = match e with from, _, target -> (from, target) in
           match IDEGraph.G.E.label e with
           | Stmts (phi, bs) ->
-              tf_stmts dir phi bs (Iter.singleton (d2, e1))
+              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.compose_call callinfo d2
+              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 =
@@ -653,7 +659,11 @@ module IDE (D : IDEDomain) = struct
                     |> DlMap.add d1 e21
                   in
                   Hashtbl.add entry_to_call_entry_cache k m;
-                  (* Surely there's a better way to do this... *)
+                  (* 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)
@@ -661,7 +671,7 @@ module IDE (D : IDEDomain) = struct
                         DlMap.to_iter m
                         |> Iter.iter (fun (d4, e3) ->
                             let e321 = D.compose e3 e21 in
-                            D.compose_return callinfo.ret d4
+                            D.transfer_return callinfo.ret d4
                             |> Iter.map (fun (d5, e4) ->
                                 ((d1, d5), D.compose e4 e321))
                             |> propagate worklist summaries priority
@@ -669,14 +679,20 @@ module IDE (D : IDEDomain) = struct
                   in
                   ())
           | InterReturn retinfo ->
-              (* Duplicate work warning!! we're saving the summary of the procedure we're returning from multiple times!! *)
+              (* 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
@@ -684,7 +700,7 @@ module IDE (D : IDEDomain) = struct
                     DlMap.to_iter m
                     |> Iter.iter (fun (d3, e2) ->
                         let e12 = D.compose e1 e2 in
-                        D.compose_return retinfo d2
+                        D.transfer_return retinfo d2
                         |> Iter.map (fun (d4, e3) ->
                             ((d3, d4), D.compose e3 e12))
                         |> propagate worklist summaries priority
@@ -692,7 +708,7 @@ module IDE (D : IDEDomain) = struct
               in
               ()
           | Call callstmt ->
-              D.compose_call_to_aftercall callstmt d2
+              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
@@ -702,9 +718,9 @@ module IDE (D : IDEDomain) = struct
     done;
     summaries
 
-  let phase2_solve order dir prog start_proc graph globals
+  (** Compute the analysis result using summaries from phase 1 *)
+  let phase2_solve order prog start_proc graph globals
       (summaries : (Loc.t, summary) Hashtbl.t) =
-    (* FIXME: use summaries ; propertly evaluate call edges first then fill in between*)
     Trace.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
@@ -719,8 +735,10 @@ module IDE (D : IDEDomain) = struct
     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
-       top, using the summary functions. *)
-    let (worklist : (Loc.t * Lambda.t) Q.t) = Q.create () in
+       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));
@@ -741,7 +759,7 @@ module IDE (D : IDEDomain) = struct
               DlMap.get d summary |> Iter.of_opt
               |> Iter.flat_map DlMap.to_iter
               |> Iter.iter (fun (d2, e1) ->
-                  D.compose_call callinfo d2
+                  D.transfer_call callinfo d2
                   |> Iter.iter (fun (d3, e2) ->
                       (match d3 with
                       | Label v ->
@@ -754,7 +772,6 @@ module IDE (D : IDEDomain) = struct
                           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';
-                            (* This should really add all calls in the target procedure to the worklist *)
                             Hashtbl.get_or calls_table callinfo.callee
                               ~default:Iter.empty
                             |> Iter.iter (fun c ->
@@ -764,7 +781,8 @@ module IDE (D : IDEDomain) = struct
                       ()))
           | _ -> ())
     done;
-    (* We then apply all summary functions to each location *)
+    (* 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 }
@@ -795,7 +813,7 @@ module IDE (D : IDEDomain) = struct
   let query r ~proc_id vert =
     Hashtbl.get r (Loc.IntraVertex { proc_id; v = vert })
 
-  let solve dir (prog : Program.t) =
+  let solve (prog : Program.t) =
     Trace.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
@@ -811,9 +829,9 @@ module IDE (D : IDEDomain) = struct
     let start_proc =
       prog.entry_proc |> Option.get_exn_or "Missing entry procedure"
     in
-    let summary = phase1_solve order dir start graph globals DlMap.empty in
+    let summary = phase1_solve order start graph globals DlMap.empty in
     ( query @@ summary,
-      query @@ phase2_solve order dir prog start_proc graph globals summary )
+      query @@ phase2_solve order prog start_proc graph globals summary )
 
   module G = Procedure.RevG
   module ResultMap = Map.Make (G.V)
@@ -846,7 +864,7 @@ let transform (prog : Program.t) =
   let g = IDEGraph.create prog `Backwards in
   CCIO.with_out "idegraph.dot" (fun s ->
       IDEGraph.Vis.fprint_graph (Format.of_chan s) g);*)
-  let summary, r = IDELiveAnalysis.solve `Backwards prog in
+  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

From 6e30631954236fd83d8a4e781348d41d8ef91eb5 Mon Sep 17 00:00:00 2001
From: bpaul <bpaul@bpaul.xyz>
Date: Thu, 22 Jan 2026 10:31:57 +1000
Subject: [PATCH 11/16] Move ide solver to analysis

---
 lib/analysis/dune     |   2 +-
 lib/analysis/ide.ml   | 734 +++++++++++++++++++++++++++++++++++++++++
 lib/transforms/ide.ml | 740 +-----------------------------------------
 3 files changed, 737 insertions(+), 739 deletions(-)
 create mode 100644 lib/analysis/ide.ml

diff --git a/lib/analysis/dune b/lib/analysis/dune
index 8ed1119..84babbf 100644
--- a/lib/analysis/dune
+++ b/lib/analysis/dune
@@ -2,7 +2,7 @@
  (public_name bincaml.analysis)
  (name analysis)
  (flags -w -27)
- (modules dataflow_graph intra_analysis defuse_bool lattice_types)
+ (modules dataflow_graph ide intra_analysis defuse_bool lattice_types)
  (libraries
   patricia-tree
   loader
diff --git a/lib/analysis/ide.ml b/lib/analysis/ide.ml
new file mode 100644
index 0000000..4a9aafd
--- /dev/null
+++ b/lib/analysis/ide.ml
@@ -0,0 +1,734 @@
+(** 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 }]
+
+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 *)
+
+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 : Program.stmt -> DL.t -> t state_update
+  (** edge from a call to its aftercall statement (or reversed when backwards)
+  *)
+
+  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 Program.stmt
+      | 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 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 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 graph =
+      GB.add_edge_e graph
+        ( CallSite origin,
+          InterCall
+            {
+              rhs;
+              lhs;
+              call_from = callstmt;
+              aftercall = origin;
+              caller;
+              callee;
+              ret = ret_info;
+            },
+          call_entry )
+    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 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
+    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:g
+
+  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 } ->
+          "\""
+          ^ 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 } ->
+            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, _ -> ""
+      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
+
+  (** 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
+                     let j = D.join e (DlMap.get_or d3 m ~default:D.bottom) in
+                     if not (D.equal j D.bottom) then DlMap.add d3 j m else m)
+                   m)
+            om DlMap.empty)
+        (* TODO Should be joining i *)
+        (DlMap.of_iter 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.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
+          | 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.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 ->
+          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.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/transforms/ide.ml b/lib/transforms/ide.ml
index f561ad4..86ec1cb 100644
--- a/lib/transforms/ide.ml
+++ b/lib/transforms/ide.ml
@@ -1,386 +1,9 @@
-(** IDE solver *)
+(** IDE test transforms *)
 
 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 }]
-
-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 *)
-
-module LSet = Set.Make (Loc)
-module LM = Map.Make (Loc)
-
-let direction : [ `Forwards | `Backwards ] = `Backwards
-
-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 Program.stmt
-      | 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 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 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 graph =
-      GB.add_edge_e graph
-        ( CallSite origin,
-          InterCall
-            {
-              rhs;
-              lhs;
-              call_from = callstmt;
-              aftercall = origin;
-              caller;
-              callee;
-              ret = ret_info;
-            },
-          call_entry )
-    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 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
-    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:g
-
-  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 } ->
-          "\""
-          ^ 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 } ->
-            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, _ -> ""
-      in
-      [ `Label l ]
-
-    let default_edge_attributes _ = []
-    let get_subgraph _ = None
-  end)
-end
-
-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 : Program.stmt -> DL.t -> t state_update
-  (** edge from a call to its aftercall statement (or reversed when backwards)
-  *)
-
-  val transfer : Program.stmt -> DL.t -> t state_update
-  (** update the state for a program statement *)
-end
+open Analysis.Ide
 
 module IDELive = struct
   let direction = `Backwards
@@ -406,7 +29,6 @@ module IDELive = struct
 
   open Value
 
-  (*type t = Live | Dead | CondLive of Var.t [@@deriving eq, ord]*)
   type t = IdEdge | ConstEdge of Value.t [@@deriving eq, ord]
 
   let bottom = ConstEdge bottom
@@ -417,7 +39,6 @@ module IDELive = struct
   let pp fmt v = Format.pp_print_string fmt (show v)
   let identity = IdEdge
 
-  (** compose (\lambda v . a) (\lambda v . b) *)
   let compose a b =
     match (a, b) with
     | IdEdge, b -> b
@@ -494,359 +115,6 @@ module IDELive = struct
         | _ -> Iter.singleton (Label v, IdEdge))
 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
-
-  (** 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
-                     let j = D.join e (DlMap.get_or d3 m ~default:D.bottom) in
-                     if not (D.equal j D.bottom) then DlMap.add d3 j m else m)
-                   m)
-            om DlMap.empty)
-        (* TODO Should be joining i *)
-        (DlMap.of_iter 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.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
-          | 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.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 ->
-          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.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
-
 module IDELiveAnalysis = IDE (IDELive)
 
 let show_state (v : IDELiveAnalysis.analysis_state) =
@@ -860,10 +128,6 @@ let print_live_vars_dot sum r fmt prog proc_id =
   Option.iter (fun g -> M.fprint_graph fmt g) (Procedure.graph p)
 
 let transform (prog : Program.t) =
-  (*
-  let g = IDEGraph.create prog `Backwards in
-  CCIO.with_out "idegraph.dot" (fun s ->
-      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) ->

From ab5596fb4a14e28f4eb92cf38ef53142deceddac Mon Sep 17 00:00:00 2001
From: bpaul <bpaul@bpaul.xyz>
Date: Thu, 22 Jan 2026 11:44:04 +1000
Subject: [PATCH 12/16] Move inter live analysis to /analysis

---
 lib/analysis/dune        |   2 +-
 lib/analysis/ide.ml      |   2 +-
 lib/analysis/ide_live.ml | 118 +++++++++++++++++++++++++++++++++++++++
 lib/passes.ml            |   4 +-
 lib/transforms/ide.ml    | 114 +------------------------------------
 5 files changed, 124 insertions(+), 116 deletions(-)
 create mode 100644 lib/analysis/ide_live.ml

diff --git a/lib/analysis/dune b/lib/analysis/dune
index 84babbf..fc0ee5b 100644
--- a/lib/analysis/dune
+++ b/lib/analysis/dune
@@ -2,7 +2,7 @@
  (public_name bincaml.analysis)
  (name analysis)
  (flags -w -27)
- (modules dataflow_graph ide 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
index 4a9aafd..7e2f45b 100644
--- a/lib/analysis/ide.ml
+++ b/lib/analysis/ide.ml
@@ -616,7 +616,7 @@ module IDE (D : IDEDomain) = struct
       Hashtbl.get summaries loc |> function
       | Some e -> e
       | None ->
-          print_endline @@ "summary undefined " ^ Loc.show loc;
+          (*print_endline @@ "summary undefined " ^ Loc.show loc;*)
           DlMap.empty
     in
     (* The first step is to initialise the entry nodes of each procedure with
diff --git a/lib/analysis/ide_live.ml b/lib/analysis/ide_live.ml
new file mode 100644
index 0000000..75f6575
--- /dev/null
+++ b/lib/analysis/ide_live.ml
@@ -0,0 +1,118 @@
+(** 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 ->
+        List.fold_left
+          (fun i (_, out) -> Iter.cons (Label out, IdEdge) i)
+          (Iter.singleton (d, IdEdge))
+          c.lhs
+    | Label v when Var.is_global v -> Iter.empty
+    | Label v -> Iter.empty
+
+  let transfer_return r d = Iter.singleton (d, IdEdge)
+
+  (* TODO preserve locals that aren't involved in the call *)
+  let transfer_call_to_aftercall stmt d =
+    match d with Lambda -> Iter.singleton (d, IdEdge) | Label _ -> 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 6ff1378..047cc17 100644
--- a/lib/passes.ml
+++ b/lib/passes.ml
@@ -91,7 +91,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 86ec1cb..7753542 100644
--- a/lib/transforms/ide.ml
+++ b/lib/transforms/ide.ml
@@ -3,119 +3,7 @@
 open Lang
 open Containers
 open Common
-open Analysis.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 ->
-        List.fold_left
-          (fun i (_, out) -> Iter.cons (Label out, IdEdge) i)
-          (Iter.singleton (d, IdEdge))
-          c.lhs
-    | Label v when Var.is_global v -> Iter.empty
-    | Label v -> Iter.empty
-
-  let transfer_return r d = Iter.singleton (d, IdEdge)
-
-  (* TODO preserve locals that aren't involved in the call *)
-  let transfer_call_to_aftercall stmt d =
-    match d with Lambda -> Iter.singleton (d, IdEdge) | Label _ -> 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)
+open Analysis.Ide_live
 
 let show_state (v : IDELiveAnalysis.analysis_state) =
   VarMap.to_iter v |> IDELive.show_state

From a513d3200b11331415fed5222b9bd43ff8eeba20 Mon Sep 17 00:00:00 2001
From: bpaul <bpaul@bpaul.xyz>
Date: Thu, 22 Jan 2026 15:18:45 +1000
Subject: [PATCH 13/16] interproc livevar tests

---
 lib/analysis/ide.ml       |  45 ++++----
 lib/analysis/ide_live.ml  |  37 +++++--
 lib/transforms/ide.ml     |   3 +
 test/analysis/ide_live.ml | 212 ++++++++++++++++++++++++++++++++++++++
 4 files changed, 266 insertions(+), 31 deletions(-)
 create mode 100644 test/analysis/ide_live.ml

diff --git a/lib/analysis/ide.ml b/lib/analysis/ide.ml
index 7e2f45b..f72bfd7 100644
--- a/lib/analysis/ide.ml
+++ b/lib/analysis/ide.ml
@@ -91,7 +91,7 @@ module type IDEDomain = sig
   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 : Program.stmt -> DL.t -> t state_update
+  val transfer_call_to_aftercall : call_info -> DL.t -> t state_update
   (** edge from a call to its aftercall statement (or reversed when backwards)
   *)
 
@@ -111,7 +111,7 @@ module IDEGraph = struct
       | Stmts of Var.t Block.phi list * Program.stmt list
       | InterCall of call_info
       | InterReturn of ret_info
-      | Call of Program.stmt
+      | Call of call_info
       | Nop
     [@@deriving eq, ord, show]
 
@@ -185,9 +185,6 @@ module IDEGraph = struct
     let caller, callee = (origin.proc_id, target) in
     let g = push_edge dir (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 call_entry, call_return =
@@ -196,20 +193,22 @@ module IDEGraph = struct
       | `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
-            {
-              rhs;
-              lhs;
-              call_from = callstmt;
-              aftercall = origin;
-              caller;
-              callee;
-              ret = ret_info;
-            },
-          call_entry )
+      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)
@@ -336,7 +335,10 @@ module IDEGraph = struct
       match v with
       | IntraVertex { proc_id; v } ->
           "\""
-          ^ Procedure.Vert.block_id_string 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)
           ^ "@" ^ ID.to_string proc_id ^ "\""
       | Entry -> "\"Entry\""
       | Exit -> "\"Exit\""
@@ -351,7 +353,10 @@ module IDEGraph = struct
       let l =
         match v with
         | IntraVertex { proc_id; v } ->
-            Procedure.Vert.block_id_string 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"
diff --git a/lib/analysis/ide_live.ml b/lib/analysis/ide_live.ml
index 75f6575..90d6347 100644
--- a/lib/analysis/ide_live.ml
+++ b/lib/analysis/ide_live.ml
@@ -60,19 +60,34 @@ module IDELive = struct
 
   let transfer_call (c : call_info) d =
     match d with
-    | Lambda ->
-        List.fold_left
-          (fun i (_, out) -> Iter.cons (Label out, IdEdge) i)
-          (Iter.singleton (d, IdEdge))
-          c.lhs
-    | Label v when Var.is_global v -> Iter.empty
+    | 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 d = Iter.singleton (d, IdEdge)
-
-  (* TODO preserve locals that aren't involved in the call *)
-  let transfer_call_to_aftercall stmt d =
-    match d with Lambda -> Iter.singleton (d, IdEdge) | Label _ -> 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 stmt d =
     let open Stmt in
diff --git a/lib/transforms/ide.ml b/lib/transforms/ide.ml
index 7753542..ffead6e 100644
--- a/lib/transforms/ide.ml
+++ b/lib/transforms/ide.ml
@@ -16,6 +16,9 @@ let print_live_vars_dot sum r fmt prog proc_id =
   Option.iter (fun g -> M.fprint_graph fmt g) (Procedure.graph p)
 
 let transform (prog : Program.t) =
+  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) ->
diff --git a/test/analysis/ide_live.ml b/test/analysis/ide_live.ml
new file mode 100644
index 0000000..3f991b2
--- /dev/null
+++ b/test/analysis/ide_live.ml
@@ -0,0 +1,212 @@
+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
+    |}]

From 9ad72d328093ab257a584660ce3e0e63ea7832c4 Mon Sep 17 00:00:00 2001
From: bpaul <bpaul@bpaul.xyz>
Date: Thu, 22 Jan 2026 16:09:08 +1000
Subject: [PATCH 14/16] Stub procedure edges

---
 lib/analysis/ide.ml       | 32 ++++++++++++++++++++++++++++----
 lib/analysis/ide_live.ml  |  7 +++++++
 test/analysis/ide_live.ml | 32 ++++++++++++++++++++++++++++++++
 3 files changed, 67 insertions(+), 4 deletions(-)

diff --git a/lib/analysis/ide.ml b/lib/analysis/ide.ml
index deb5c29..9b28dfc 100644
--- a/lib/analysis/ide.ml
+++ b/lib/analysis/ide.ml
@@ -34,6 +34,7 @@ type ret_info = {
   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;
@@ -47,6 +48,9 @@ type call_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)
 
@@ -95,6 +99,9 @@ module type IDEDomain = sig
   (** 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
@@ -112,6 +119,7 @@ module IDEGraph = struct
       | InterCall of call_info
       | InterReturn of ret_info
       | Call of call_info
+      | StubProc of stub_info
       | Nop
     [@@deriving eq, ord, show]
 
@@ -268,7 +276,6 @@ module IDEGraph = struct
       | _, _, _ -> 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 ->
@@ -286,7 +293,16 @@ module IDEGraph = struct
     in
     Procedure.graph p
     |> Option.map (fun procg -> Procedure.G.fold_edges_e add_block_edge procg g)
-    |> Option.get_or ~default: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
@@ -336,8 +352,8 @@ module IDEGraph = struct
       | IntraVertex { proc_id; v } ->
           "\""
           ^ (match v with
-            | Begin _ -> "Begin " ^ Procedure.Vert.block_id_string v
-            | End _ -> "End " ^ Procedure.Vert.block_id_string v
+            | 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\""
@@ -377,6 +393,7 @@ module IDEGraph = struct
         | _, InterReturn _, _ -> "InterReturn"
         | _, Call _, _ -> "Call"
         | _, Nop, _ -> ""
+        | _, StubProc _, _ -> "StubProc"
       in
       [ `Label l ]
 
@@ -603,6 +620,11 @@ module IDE (D : IDEDomain) = struct
               |> 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)))
@@ -621,6 +643,8 @@ module IDE (D : IDEDomain) = struct
       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
diff --git a/lib/analysis/ide_live.ml b/lib/analysis/ide_live.ml
index 90d6347..a43dd41 100644
--- a/lib/analysis/ide_live.ml
+++ b/lib/analysis/ide_live.ml
@@ -89,6 +89,13 @@ module IDELive = struct
         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
diff --git a/test/analysis/ide_live.ml b/test/analysis/ide_live.ml
index 3f991b2..ee279f9 100644
--- a/test/analysis/ide_live.ml
+++ b/test/analysis/ide_live.ml
@@ -210,3 +210,35 @@ proc @fun2 (f:bv64) -> (out2:bv64)
     $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
+    |}]

From b6a18444adced9bf276ee28e8feb38a98b213de7 Mon Sep 17 00:00:00 2001
From: bpaul <bpaul@bpaul.xyz>
Date: Thu, 22 Jan 2026 16:14:13 +1000
Subject: [PATCH 15/16] Join edge functions created by phi nodes

---
 lib/analysis/ide.ml | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

diff --git a/lib/analysis/ide.ml b/lib/analysis/ide.ml
index 9b28dfc..7a872e7 100644
--- a/lib/analysis/ide.ml
+++ b/lib/analysis/ide.ml
@@ -276,6 +276,7 @@ module IDEGraph = struct
       | _, _, _ -> 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 ->
@@ -435,6 +436,10 @@ module IDE (D : IDEDomain) = struct
     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 =
@@ -446,12 +451,10 @@ module IDE (D : IDEDomain) = struct
               |> Iter.fold
                    (fun m (d3, e2) ->
                      let e = D.compose e2 e1 in
-                     let j = D.join e (DlMap.get_or d3 m ~default:D.bottom) in
-                     if not (D.equal j D.bottom) then DlMap.add d3 j m else m)
+                     join_add m d3 e)
                    m)
             om DlMap.empty)
-        (* TODO Should be joining i *)
-        (DlMap.of_iter i)
+        (Iter.fold (fun m (d, e) -> join_add m d e) DlMap.empty i)
         bs
       |> DlMap.to_iter
     in

From 1361543e1e1cd3daa256d701ecf3865186d4b164 Mon Sep 17 00:00:00 2001
From: bpaul <bpaul@bpaul.xyz>
Date: Thu, 22 Jan 2026 16:18:54 +1000
Subject: [PATCH 16/16] fmt

---
 lib/analysis/dune         |  8 +++++++-
 lib/analysis/ide_live.ml  | 15 ++++++++++-----
 test/analysis/ide_live.ml |  6 +++---
 3 files changed, 20 insertions(+), 9 deletions(-)

diff --git a/lib/analysis/dune b/lib/analysis/dune
index 8bb233f..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 ide ide_live)
+ (modules
+  dataflow_graph
+  intra_analysis
+  defuse_bool
+  lattice_types
+  ide
+  ide_live)
  (libraries
   patricia-tree
   loader
diff --git a/lib/analysis/ide_live.ml b/lib/analysis/ide_live.ml
index a43dd41..dc2776e 100644
--- a/lib/analysis/ide_live.ml
+++ b/lib/analysis/ide_live.ml
@@ -90,11 +90,16 @@ module IDELive = struct
     | 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
+    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
diff --git a/test/analysis/ide_live.ml b/test/analysis/ide_live.ml
index ee279f9..21dd2b4 100644
--- a/test/analysis/ide_live.ml
+++ b/test/analysis/ide_live.ml
@@ -197,7 +197,8 @@ proc @fun2 (f:bv64) -> (out2:bv64)
   let program = lst.prog in
   let _, results = IDELiveAnalysis.solve program in
   ID.Map.iter (fun id _ -> print_lives results id) program.procs;
-  [%expect {|
+  [%expect
+    {|
     @main
     b:bv64
     y:bv64
@@ -236,8 +237,7 @@ proc @stub() -> ();
   let _, results = IDELiveAnalysis.solve program in
   let main = program.entry_proc |> Option.get_exn_or "No entry proc" in
   print_lives results main;
-  [%expect
-    {|
+  [%expect {|
     @main
     $mem:(bv64->bv8)
     $g:bv64