C: Improve Jib IR, add SSA representation

Add a CL_void l-expression so we don't have redundant unit-typed
variables everywhere, and add an optimization in Jib_optimize called
optimize_unit which introduces these.

Remove the basic control-flow graph in Jib_util and add a new mutable
control-flow graph type in Jib_ssa which allows the IR to be converted
into SSA form. The mutable graph allows for more efficient updates,
and includes both back and forwards references making it much more
convenient to traverse.

Having an SSA representation should make some optimizations much
simpler, and is also probably more natural for SMT generation where
variables have to be defined once using declare-const anyway.

Debug option -ddump_flow_graphs now outputs SSA'd graphs of the
functions in a specification.

13 files changed, 954 insertions, 173 deletions

diff --git a/language/jib.ott b/language/jib.ott
index 7b5d0162..e54e2ea5 100644
--- a/language/jib.ott
+++ b/language/jib.ott
@@ -136,6 +136,7 @@ clexp :: 'CL_' ::=
   | current_exception : ctyp :: :: current_exception
   | have_exception           :: :: have_exception
   | return : ctyp            :: :: return
+  | void                     :: :: void
 
 ctype_def :: 'CTD_' ::=
   {{ com C type definition }}
diff --git a/src/graph.ml b/src/graph.ml
index 21863e47..703deba9 100644
--- a/src/graph.ml
+++ b/src/graph.ml
@@ -234,6 +234,6 @@ module Make(Ord: OrderedType) = struct
     NM.bindings graph |> List.iter (fun (from_node, _) -> make_node from_node);
     NM.bindings graph |> List.iter (fun (from_node, to_nodes) -> NS.iter (make_line from_node) to_nodes);
     output_string out_chan "}\n";
-    Util.opt_colors := true;
+    Util.opt_colors := true
 
 end
diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml
index aab2894e..846b619f 100644
--- a/src/jib/c_backend.ml
+++ b/src/jib/c_backend.ml
@@ -63,7 +63,6 @@ module Big_int = Nat_big_num
 
 let c_verbosity = ref 0
 
-let opt_debug_flow_graphs = ref false
 let opt_static = ref false
 let opt_no_main = ref false
 let opt_memo_cache = ref false
@@ -849,48 +848,6 @@ let hoist_allocations recursive_functions = function
 
   | cdef -> [cdef]
 
-let flat_counter = ref 0
-let flat_id () =
-  let id = mk_id ("local#" ^ string_of_int !flat_counter) in
-  incr flat_counter;
-  id
-
-let rec flatten_instrs = function
-  | I_aux (I_decl (ctyp, decl_id), aux) :: instrs ->
-     let fid = flat_id () in
-     I_aux (I_decl (ctyp, fid), aux) :: flatten_instrs (instrs_rename decl_id fid instrs)
-
-  | I_aux ((I_block block | I_try_block block), _) :: instrs ->
-     flatten_instrs block @ flatten_instrs instrs
-
-  | I_aux (I_if (cval, then_instrs, else_instrs, _), _) :: instrs ->
-     let then_label = label "then_" in
-     let endif_label = label "endif_" in
-     [ijump cval then_label]
-     @ flatten_instrs else_instrs
-     @ [igoto endif_label]
-     @ [ilabel then_label]
-     @ flatten_instrs then_instrs
-     @ [ilabel endif_label]
-     @ flatten_instrs instrs
-
-  | I_aux (I_comment _, _) :: instrs -> flatten_instrs instrs
-
-  | instr :: instrs -> instr :: flatten_instrs instrs
-  | [] -> []
-
-let flatten_cdef =
-  function
-  | CDEF_fundef (function_id, heap_return, args, body) ->
-     flat_counter := 0;
-     CDEF_fundef (function_id, heap_return, args, flatten_instrs body)
-
-  | CDEF_let (n, bindings, instrs) ->
-    flat_counter := 0;
-    CDEF_let (n, bindings, flatten_instrs instrs)
-
-  | cdef -> cdef
-
 let rec specialize_variants ctx prior =
   let unifications = ref (Bindings.empty) in
 
@@ -1386,6 +1343,7 @@ let rec sgen_clexp = function
   | CL_have_exception -> "have_exception"
   | CL_current_exception _ -> "current_exception"
   | CL_return _ -> assert false
+  | CL_void -> assert false
 
 let rec sgen_clexp_pure = function
   | CL_id (id, _) -> sgen_id id
@@ -1395,6 +1353,7 @@ let rec sgen_clexp_pure = function
   | CL_have_exception -> "have_exception"
   | CL_current_exception _ -> "current_exception"
   | CL_return _ -> assert false
+  | CL_void -> assert false
 
 (** Generate instructions to copy from a cval to a clexp. This will
    insert any needed type conversions from big integers to small
@@ -2079,8 +2038,6 @@ let codegen_def' ctx = function
        string (Printf.sprintf "%svoid %s(%s%s *rop, %s);" static (sgen_function_id id) (extra_params ()) (sgen_ctyp ret_ctyp) (Util.string_of_list ", " sgen_ctyp arg_ctyps))
 
   | CDEF_fundef (id, ret_arg, args, instrs) as def ->
-     if !opt_debug_flow_graphs then make_dot id (instrs_graph instrs) else ();
-
      (* Extract type information about the function from the environment. *)
      let quant, Typ_aux (fn_typ, _) = Env.get_val_spec id ctx.tc_env in
      let arg_typs, ret_typ = match fn_typ with
diff --git a/src/jib/c_backend.mli b/src/jib/c_backend.mli
index 2fc5be94..7314eb5a 100644
--- a/src/jib/c_backend.mli
+++ b/src/jib/c_backend.mli
@@ -53,10 +53,6 @@ open Type_check
 
 (** Global compilation options *)
 
-(** Output a dataflow graph for each generated function in Graphviz
-   (dot) format. *)
-val opt_debug_flow_graphs : bool ref
-
 (** Define generated functions as static *)
 val opt_static : bool ref
 
@@ -109,10 +105,5 @@ val optimize_experimental : bool ref
 (** Convert a typ to a IR ctyp *)
 val ctyp_of_typ : Jib_compile.ctx -> Ast.typ -> ctyp
 
-(** Rewriting steps for compiled ASTs *)
-val flatten_instrs : instr list -> instr list
-
-val flatten_cdef : cdef -> cdef
-
 val jib_of_ast : Env.t -> tannot Ast.defs -> cdef list * Jib_compile.ctx
 val compile_ast : Env.t -> out_channel -> string list -> tannot Ast.defs -> unit
diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml
index 36a28d9f..27f833d8 100644
--- a/src/jib/jib_compile.ml
+++ b/src/jib/jib_compile.ml
@@ -58,6 +58,7 @@ open Value2
 open Anf
 
 let opt_debug_function = ref ""
+let opt_debug_flow_graphs = ref false
 let opt_memo_cache = ref false
 
 (**************************************************************************)
@@ -1174,7 +1175,16 @@ and compile_def' n total ctx = function
        prerr_endline (Util.header header (List.length arg_ctyps + 2));
        prerr_endline (Pretty_print_sail.to_string PPrint.(separate_map hardline pp_instr instrs))
      else ();
-     
+
+     if !opt_debug_flow_graphs then
+       begin
+         let instrs = Jib_optimize.(instrs |> optimize_unit |> flatten_instrs) in
+         let cfg = Jib_ssa.ssa instrs in
+         let out_chan = open_out (Util.zencode_string (string_of_id id) ^ ".gv") in
+         Jib_ssa.make_dot out_chan cfg;
+         close_out out_chan;
+       end;
+
      [CDEF_fundef (id, None, List.map fst compiled_args, instrs)], orig_ctx
 
   | DEF_fundef (FD_aux (FD_function (_, _, _, []), (l, _))) ->
diff --git a/src/jib/jib_compile.mli b/src/jib/jib_compile.mli
index 173e5c5f..f3bd8c76 100644
--- a/src/jib/jib_compile.mli
+++ b/src/jib/jib_compile.mli
@@ -55,10 +55,13 @@ open Ast
 open Ast_util
 open Jib
 open Type_check
-   
+
+(** Output a dataflow graph for each generated function in Graphviz
+   (dot) format. *)
+val opt_debug_flow_graphs : bool ref
+
 (** Print the IR representation of a specific function. *)
 val opt_debug_function : string ref
-  
 
 (** {2 Jib context} *)
 
diff --git a/src/jib/jib_optimize.ml b/src/jib/jib_optimize.ml
new file mode 100644
index 00000000..889e650e
--- /dev/null
+++ b/src/jib/jib_optimize.ml
@@ -0,0 +1,129 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*    Alasdair Armstrong                                                  *)
+(*    Brian Campbell                                                      *)
+(*    Thomas Bauereiss                                                    *)
+(*    Anthony Fox                                                         *)
+(*    Jon French                                                          *)
+(*    Dominic Mulligan                                                    *)
+(*    Stephen Kell                                                        *)
+(*    Mark Wassell                                                        *)
+(*                                                                        *)
+(*  All rights reserved.                                                  *)
+(*                                                                        *)
+(*  This software was developed by the University of Cambridge Computer   *)
+(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
+(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
+(*                                                                        *)
+(*  Redistribution and use in source and binary forms, with or without    *)
+(*  modification, are permitted provided that the following conditions    *)
+(*  are met:                                                              *)
+(*  1. Redistributions of source code must retain the above copyright     *)
+(*     notice, this list of conditions and the following disclaimer.      *)
+(*  2. Redistributions in binary form must reproduce the above copyright  *)
+(*     notice, this list of conditions and the following disclaimer in    *)
+(*     the documentation and/or other materials provided with the         *)
+(*     distribution.                                                      *)
+(*                                                                        *)
+(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
+(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
+(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
+(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
+(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
+(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
+(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
+(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
+(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
+(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
+(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
+(*  SUCH DAMAGE.                                                          *)
+(**************************************************************************)
+
+open Ast_util
+open Jib
+open Jib_util
+
+let optimize_unit instrs =
+  let unit_cval cval =
+    match cval_ctyp cval with
+    | CT_unit -> (F_lit V_unit, CT_unit)
+    | _ -> cval
+  in
+  let unit_instr = function
+    | I_aux (I_funcall (clexp, extern, id, args), annot) as instr ->
+       begin match clexp_ctyp clexp with
+       | CT_unit ->
+          I_aux (I_funcall (CL_void, extern, id, List.map unit_cval args), annot)
+       | _ -> instr
+       end
+    | I_aux (I_copy (clexp, cval), annot) as instr ->
+       begin match clexp_ctyp clexp with
+       | CT_unit ->
+          I_aux (I_copy (CL_void, unit_cval cval), annot)
+       | _ -> instr
+       end
+    | I_aux (I_alias (clexp, cval), annot) as instr ->
+       begin match clexp_ctyp clexp with
+       | CT_unit ->
+          I_aux (I_alias (CL_void, unit_cval cval), annot)
+       | _ -> instr
+       end
+    | instr -> instr
+  in
+  let non_pointless_copy (I_aux (aux, annot)) =
+    match aux with
+    | I_copy (CL_void, _) -> false
+    | _ -> true
+  in
+  filter_instrs non_pointless_copy (map_instr_list unit_instr instrs)
+
+let flat_counter = ref 0
+let flat_id () =
+  let id = mk_id ("local#" ^ string_of_int !flat_counter) in
+  incr flat_counter;
+  id
+
+let rec flatten_instrs = function
+  | I_aux (I_decl (ctyp, decl_id), aux) :: instrs ->
+     let fid = flat_id () in
+     I_aux (I_decl (ctyp, fid), aux) :: flatten_instrs (instrs_rename decl_id fid instrs)
+
+  | I_aux ((I_block block | I_try_block block), _) :: instrs ->
+     flatten_instrs block @ flatten_instrs instrs
+
+  | I_aux (I_if (cval, then_instrs, else_instrs, _), _) :: instrs ->
+     let then_label = label "then_" in
+     let endif_label = label "endif_" in
+     [ijump cval then_label]
+     @ flatten_instrs else_instrs
+     @ [igoto endif_label]
+     @ [ilabel then_label]
+     @ flatten_instrs then_instrs
+     @ [ilabel endif_label]
+     @ flatten_instrs instrs
+
+  | I_aux (I_comment _, _) :: instrs -> flatten_instrs instrs
+
+  | instr :: instrs -> instr :: flatten_instrs instrs
+  | [] -> []
+
+let flatten_cdef =
+  function
+  | CDEF_fundef (function_id, heap_return, args, body) ->
+     flat_counter := 0;
+     CDEF_fundef (function_id, heap_return, args, flatten_instrs body)
+
+  | CDEF_let (n, bindings, instrs) ->
+    flat_counter := 0;
+    CDEF_let (n, bindings, flatten_instrs instrs)
+
+  | cdef -> cdef
diff --git a/src/jib/jib_optimize.mli b/src/jib/jib_optimize.mli
new file mode 100644
index 00000000..beffa81e
--- /dev/null
+++ b/src/jib/jib_optimize.mli
@@ -0,0 +1,63 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*    Alasdair Armstrong                                                  *)
+(*    Brian Campbell                                                      *)
+(*    Thomas Bauereiss                                                    *)
+(*    Anthony Fox                                                         *)
+(*    Jon French                                                          *)
+(*    Dominic Mulligan                                                    *)
+(*    Stephen Kell                                                        *)
+(*    Mark Wassell                                                        *)
+(*                                                                        *)
+(*  All rights reserved.                                                  *)
+(*                                                                        *)
+(*  This software was developed by the University of Cambridge Computer   *)
+(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
+(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
+(*                                                                        *)
+(*  Redistribution and use in source and binary forms, with or without    *)
+(*  modification, are permitted provided that the following conditions    *)
+(*  are met:                                                              *)
+(*  1. Redistributions of source code must retain the above copyright     *)
+(*     notice, this list of conditions and the following disclaimer.      *)
+(*  2. Redistributions in binary form must reproduce the above copyright  *)
+(*     notice, this list of conditions and the following disclaimer in    *)
+(*     the documentation and/or other materials provided with the         *)
+(*     distribution.                                                      *)
+(*                                                                        *)
+(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
+(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
+(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
+(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
+(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
+(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
+(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
+(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
+(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
+(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
+(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
+(*  SUCH DAMAGE.                                                          *)
+(**************************************************************************)
+
+open Jib
+
+(** Remove redundant assignments and variables of type
+   unit. unit-typed identifiers that are assigned to are replaced with
+   CL_void, and cvals (which should be pure!) are replaced with unit
+   types are replaced by unit-literals. *)
+val optimize_unit : instr list -> instr list
+
+(** Remove all instructions that can contain other nested
+   instructions, prodcing a flat list of instructions. *)
+val flatten_instrs : instr list -> instr list
+val flatten_cdef : cdef -> cdef
+
diff --git a/src/jib/jib_ssa.ml b/src/jib/jib_ssa.ml
new file mode 100644
index 00000000..1f477696
--- /dev/null
+++ b/src/jib/jib_ssa.ml
@@ -0,0 +1,602 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*    Alasdair Armstrong                                                  *)
+(*    Brian Campbell                                                      *)
+(*    Thomas Bauereiss                                                    *)
+(*    Anthony Fox                                                         *)
+(*    Jon French                                                          *)
+(*    Dominic Mulligan                                                    *)
+(*    Stephen Kell                                                        *)
+(*    Mark Wassell                                                        *)
+(*                                                                        *)
+(*  All rights reserved.                                                  *)
+(*                                                                        *)
+(*  This software was developed by the University of Cambridge Computer   *)
+(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
+(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
+(*                                                                        *)
+(*  Redistribution and use in source and binary forms, with or without    *)
+(*  modification, are permitted provided that the following conditions    *)
+(*  are met:                                                              *)
+(*  1. Redistributions of source code must retain the above copyright     *)
+(*     notice, this list of conditions and the following disclaimer.      *)
+(*  2. Redistributions in binary form must reproduce the above copyright  *)
+(*     notice, this list of conditions and the following disclaimer in    *)
+(*     the documentation and/or other materials provided with the         *)
+(*     distribution.                                                      *)
+(*                                                                        *)
+(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
+(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
+(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
+(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
+(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
+(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
+(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
+(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
+(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
+(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
+(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
+(*  SUCH DAMAGE.                                                          *)
+(**************************************************************************)
+
+open Ast_util
+open Jib
+open Jib_util
+
+module IntSet = Set.Make(struct type t = int let compare = compare end)
+
+(**************************************************************************)
+(* 1. Mutable graph type                                                  *)
+(**************************************************************************)
+
+type 'a array_graph = {
+    mutable next : int;
+    mutable nodes : ('a * IntSet.t * IntSet.t) option array
+  }
+
+let make ~initial_size () = {
+    next = 0;
+    nodes = Array.make initial_size None
+  }
+
+(** Add a vertex to a graph, returning the node index *)
+let add_vertex data graph =
+  let n = graph.next in
+  if n >= Array.length graph.nodes then
+    begin
+      let new_nodes = Array.make (Array.length graph.nodes * 2) None in
+      Array.blit graph.nodes 0 new_nodes 0 (Array.length graph.nodes);
+      graph.nodes <- new_nodes
+    end;
+  let n = graph.next in
+  graph.nodes.(n) <- Some (data, IntSet.empty, IntSet.empty);
+  graph.next <- n + 1;
+  n
+
+(** Add an edge between two existing vertices. Raises Invalid_argument
+   if either of the vertices do not exist. *)
+let add_edge n m graph =
+  begin match graph.nodes.(n) with
+  | Some (data, parents, children) ->
+     graph.nodes.(n) <- Some (data, parents, IntSet.add m children)
+  | None ->
+     raise (Invalid_argument "Parent node does not exist in graph")
+  end;
+  match graph.nodes.(m) with
+  | Some (data, parents, children) ->
+     graph.nodes.(m) <- Some (data, IntSet.add n parents, children)
+  | None ->
+     raise (Invalid_argument "Child node does not exist in graph")
+
+let cardinal graph = graph.next
+
+let reachable roots graph =
+  let visited = ref IntSet.empty in
+
+  let rec reachable' n =
+    if IntSet.mem n !visited then ()
+    else
+      begin
+        visited := IntSet.add n !visited;
+        match graph.nodes.(n) with
+        | Some (_, _, successors) ->
+           IntSet.iter reachable' successors
+        | None -> ()
+      end
+  in
+  IntSet.iter reachable' roots; !visited
+
+let prune visited graph =
+  for i = 0 to graph.next - 1 do
+    match graph.nodes.(i) with
+    | Some (n, preds, succs) ->
+       if IntSet.mem i visited then
+         graph.nodes.(i) <- Some (n, IntSet.inter visited preds, IntSet.inter visited succs)
+       else
+         graph.nodes.(i) <- None
+    | None -> ()
+  done
+
+(**************************************************************************)
+(* 2. Mutable control flow graph                                          *)
+(**************************************************************************)
+
+type cf_node =
+  | CF_label of string
+  | CF_block of instr list
+  | CF_start
+
+let control_flow_graph instrs =
+  let module StringMap = Map.Make(String) in
+  let labels = ref StringMap.empty in
+
+  let graph = make ~initial_size:512 () in
+
+  iter_instr (fun (I_aux (instr, annot)) ->
+      match instr with
+      | I_label label ->
+         labels := StringMap.add label (add_vertex ([], CF_label label) graph) !labels
+      | _ -> ()
+    ) (iblock instrs);
+
+  let cf_split (I_aux (aux, _)) =
+    match aux with
+    | I_block _ | I_label _ | I_goto _ | I_jump _ | I_if _ | I_end | I_match_failure | I_undefined _ -> true
+    | _ -> false
+  in
+
+  let rec cfg preds instrs =
+    let before, after = instr_split_at cf_split instrs in
+    let last = match after with
+      | I_aux (I_label _, _) :: _ -> []
+      | instr :: _ -> [instr]
+      | _ -> []
+    in
+    let preds = match before @ last with
+      | [] -> preds
+      | instrs ->
+         let n = add_vertex ([], CF_block instrs) graph in
+         List.iter (fun p -> add_edge p n graph) preds;
+         [n]
+    in
+    match after with
+    | I_aux (I_if (cond, then_instrs, else_instrs, _), _) :: after ->
+       let t = cfg preds then_instrs in
+       let e = cfg preds else_instrs in
+       cfg (t @ e) after
+
+    | I_aux ((I_end | I_match_failure | I_undefined _), _) :: after ->
+       cfg [] after
+
+    | I_aux (I_goto label, _) :: after ->
+       List.iter (fun p -> add_edge p (StringMap.find label !labels) graph) preds;
+       cfg [] after
+
+    | I_aux (I_jump (cval, label), _) :: after ->
+       List.iter (fun p -> add_edge p (StringMap.find label !labels) graph) preds;
+       cfg preds after
+
+    | I_aux (I_label label, _) :: after ->
+       cfg (StringMap.find label !labels :: preds) after
+
+    | I_aux (I_block instrs, _) :: after ->
+       let m = cfg preds instrs in
+       cfg m after
+
+    | _ :: after -> assert false
+
+    | [] -> preds
+  in
+
+  let start = add_vertex ([], CF_start) graph in
+  let finish = cfg [start] instrs in
+
+  let visited = reachable (IntSet.singleton start) graph in
+  prune visited graph;
+
+  start, finish, graph
+
+(**************************************************************************)
+(* 3. Computing dominators                                                *)
+(**************************************************************************)
+
+(** Calculate the (immediate) dominators of a graph using the
+   Lengauer-Tarjan algorithm. This is the slightly less sophisticated
+   version from Appel's book 'Modern compiler implementation in ML'
+   which runs in O(n log(n)) time. *)
+let immediate_dominators graph root =
+  let none = -1 in
+  let vertex   = Array.make (cardinal graph) 0 in
+  let parent   = Array.make (cardinal graph) none in
+  let ancestor = Array.make (cardinal graph) none in
+  let semi     = Array.make (cardinal graph) none in
+  let idom     = Array.make (cardinal graph) none in
+  let samedom  = Array.make (cardinal graph) none in
+  let best     = Array.make (cardinal graph) none in
+  let dfnum    = Array.make (cardinal graph) 0 in
+  let bucket   = Array.make (cardinal graph) IntSet.empty in
+
+  let rec ancestor_with_lowest_semi v =
+    let a = ancestor.(v) in
+    if ancestor.(a) <> none then
+      let b = ancestor_with_lowest_semi a in
+      ancestor.(v) <- ancestor.(a);
+      if dfnum.(semi.(b)) < dfnum.(semi.(best.(v))) then
+        best.(v) <- b
+      else ();
+    else ();
+    if best.(v) <> none then best.(v) else v
+  in
+
+  let link p n =
+    ancestor.(n) <- p;
+    best.(n) <- n
+  in
+
+  let count = ref 0 in
+
+  let rec dfs p n =
+    if dfnum.(n) = 0 then
+      begin
+        dfnum.(n) <- !count;
+        vertex.(!count) <- n;
+        parent.(n) <- p;
+        incr count;
+        match graph.nodes.(n) with
+        | Some (_, _, successors) ->
+           IntSet.iter (fun w -> dfs n w) successors
+        | None -> assert false
+      end
+  in
+  dfs none root;
+
+  for i = !count - 1 downto 1 do
+    let n = vertex.(i) in
+    let p = parent.(n) in
+    let s = ref p in
+
+    begin match graph.nodes.(n) with
+    | Some (_, predecessors, _) ->
+       IntSet.iter (fun v ->
+           let s' =
+             if dfnum.(v) <= dfnum.(n) then
+               v
+             else
+               semi.(ancestor_with_lowest_semi v)
+           in
+           if dfnum.(s') < dfnum.(!s) then s := s'
+         ) predecessors
+    | None -> assert false
+    end;
+    semi.(n) <- !s;
+    bucket.(!s) <- IntSet.add n bucket.(!s);
+    link p n;
+    IntSet.iter (fun v ->
+        let y = ancestor_with_lowest_semi v in
+        if semi.(y) = semi.(v) then
+          idom.(v) <- p
+        else
+          samedom.(n) <- y
+      ) bucket.(p);
+  done;
+  for i = 1 to !count - 1 do
+    let n = vertex.(i) in
+    if samedom.(n) <> none then
+      idom.(n) <- idom.(samedom.(n))
+  done;
+  idom
+
+(** [(dominator_children idoms).(n)] are the nodes whose immediate dominator
+   (idom) is n. *)
+let dominator_children idom =
+  let none = -1 in
+  let children = Array.make (Array.length idom) IntSet.empty in
+
+  for n = 0 to Array.length idom - 1 do
+    let p = idom.(n) in
+    if p <> none then
+      children.(p) <- IntSet.add n (children.(p))
+  done;
+  children
+
+(** [dominate idom n w] is true if n dominates w in the tree of
+   immediate dominators idom. *)
+let rec dominate idom n w =
+  let none = -1 in
+  let p = idom.(n) in
+  if p = none then
+    false
+  else if p = w then
+    true
+  else
+    dominate idom p w
+
+let dominance_frontiers graph root idom children =
+  let df = Array.make (cardinal graph) IntSet.empty in
+
+  let rec compute_df n =
+    let set = ref IntSet.empty in
+
+    begin match graph.nodes.(n) with
+    | Some (content, _, succs) ->
+       IntSet.iter (fun y ->
+           if idom.(y) <> n then
+             set := IntSet.add y !set
+         ) succs
+    | None -> ()
+    end;
+    IntSet.iter (fun c ->
+        compute_df c;
+        IntSet.iter (fun w ->
+            if not (dominate idom n w) then
+              set := IntSet.add w !set
+          ) (df.(c))
+      ) (children.(n));
+    df.(n) <- !set
+  in
+  compute_df root;
+  df
+
+(**************************************************************************)
+(* 4. Conversion to SSA form                                              *)
+(**************************************************************************)
+
+type ssa_elem =
+  | Phi of Ast.id * Ast.id list
+
+let place_phi_functions graph df =
+  let defsites = ref Bindings.empty in
+
+  let all_vars = ref IdSet.empty in
+
+  let rec all_decls = function
+    | I_aux (I_decl (_, id), _) :: instrs ->
+       IdSet.add id (all_decls instrs)
+    | _ :: instrs -> all_decls instrs
+    | [] -> IdSet.empty
+  in
+
+  let orig_A n =
+    match graph.nodes.(n) with
+    | Some ((_, CF_block instrs), _, _) ->
+       let vars = List.fold_left IdSet.union IdSet.empty (List.map instr_writes instrs) in
+       let vars = IdSet.diff vars (all_decls instrs) in
+       all_vars := IdSet.union vars !all_vars;
+       vars
+    | Some _ -> IdSet.empty
+    | None -> IdSet.empty
+  in
+  let phi_A = ref Bindings.empty in
+
+  for n = 0 to graph.next - 1 do
+    IdSet.iter (fun a ->
+        let ds = match Bindings.find_opt a !defsites with Some ds -> ds | None -> IntSet.empty in
+        defsites := Bindings.add a (IntSet.add n ds) !defsites
+      ) (orig_A n)
+  done;
+
+  IdSet.iter (fun a ->
+      let workset = ref (Bindings.find a !defsites) in
+      while not (IntSet.is_empty !workset) do
+        let n = IntSet.choose !workset in
+        workset := IntSet.remove n !workset;
+        IntSet.iter (fun y ->
+            let phi_A_a = match Bindings.find_opt a !phi_A with Some set -> set | None -> IntSet.empty in
+            if not (IntSet.mem y phi_A_a) then
+              begin
+                begin match graph.nodes.(y) with
+                | Some ((phis, cfnode), preds, succs) ->
+                   graph.nodes.(y) <- Some ((Phi (a, Util.list_init (IntSet.cardinal preds) (fun _ -> a)) :: phis, cfnode), preds, succs)
+                | None -> assert false
+                end;
+                phi_A := Bindings.add a (IntSet.add y phi_A_a) !phi_A;
+                if not (IdSet.mem a (orig_A y)) then
+                  workset := IntSet.add y !workset
+              end
+          ) df.(n)
+      done
+    ) !all_vars
+
+let rename_variables graph root children =
+  let counts = ref Bindings.empty in
+  let stacks = ref Bindings.empty in
+
+  let get_count id =
+    match Bindings.find_opt id !counts with Some n -> n | None -> 0
+  in
+  let top_stack id =
+    match Bindings.find_opt id !stacks with Some (x :: _) -> x | (Some [] | None) -> 0
+  in
+  let push_stack id n =
+    stacks := Bindings.add id (n :: match Bindings.find_opt id !stacks with Some s -> s | None -> []) !stacks
+  in
+
+  let rec fold_frag = function
+    | F_id id ->
+       let i = top_stack id in
+       F_id (append_id id ("_" ^ string_of_int i))
+    | F_ref id ->
+       let i = top_stack id in
+       F_ref (append_id id ("_" ^ string_of_int i))
+    | F_lit vl -> F_lit vl
+    | F_have_exception -> F_have_exception
+    | F_current_exception -> F_current_exception
+    | F_op (f1, op, f2) -> F_op (fold_frag f1, op, fold_frag f2)
+    | F_unary (op, f) -> F_unary (op, fold_frag f)
+    | F_call (id, fs) -> F_call (id, List.map fold_frag fs)
+    | F_field (f, field) -> F_field (fold_frag f, field)
+    | F_raw str -> F_raw str
+    | F_poly f -> F_poly (fold_frag f)
+  in
+
+  let rec fold_clexp = function
+    | CL_id (id, ctyp) ->
+       let i = get_count id + 1 in
+       counts := Bindings.add id i !counts;
+       push_stack id i;
+       CL_id (append_id id ("_" ^ string_of_int i), ctyp)
+    | CL_field (clexp, field) -> CL_field (fold_clexp clexp, field)
+    | CL_addr clexp -> CL_addr (fold_clexp clexp)
+    | CL_tuple (clexp, n) -> CL_tuple (fold_clexp clexp, n)
+    | CL_current_exception ctyp -> CL_current_exception ctyp
+    | CL_have_exception -> CL_have_exception
+    | CL_return ctyp -> CL_return ctyp
+    | CL_void -> CL_void
+  in
+
+  let fold_cval (f, ctyp) = (fold_frag f, ctyp) in
+
+  let ssa_instr (I_aux (aux, annot)) =
+    let aux = match aux with
+      | I_funcall (clexp, extern, id, args) ->
+         let args = List.map fold_cval args in
+         I_funcall (fold_clexp clexp, extern, id, args)
+      | I_copy (clexp, cval) ->
+         let cval = fold_cval cval in
+         I_copy (fold_clexp clexp, cval)
+      | I_decl (ctyp, id) ->
+         let i = get_count id + 1 in
+         counts := Bindings.add id i !counts;
+         push_stack id i;
+         I_decl (ctyp, append_id id ("_" ^ string_of_int i))
+      | I_init (ctyp, id, cval) ->
+         let cval = fold_cval cval in
+         let i = get_count id + 1 in
+         counts := Bindings.add id i !counts;
+         push_stack id i;
+         I_init (ctyp, append_id id ("_" ^ string_of_int i), cval)
+      | instr -> instr
+    in
+    I_aux (aux, annot)
+  in
+
+  let ssa_cfnode = function
+    | CF_start -> CF_start
+    | CF_block instrs -> CF_block (List.map ssa_instr instrs)
+    | CF_label label -> CF_label label
+  in
+
+  let ssa_ssanode = function
+    | Phi (id, args) ->
+       let i = get_count id + 1 in
+       counts := Bindings.add id i !counts;
+       push_stack id i;
+       Phi (append_id id ("_" ^ string_of_int i), args)
+  in
+
+  let fix_phi j = function
+    | Phi (id, ids) ->
+       Phi (id, List.mapi (fun k a ->
+                    if k = j then
+                      let i = top_stack a in
+                      append_id a ("_" ^ string_of_int i)
+                    else a)
+                  ids)
+  in
+
+  let rec rename n =
+    let old_stacks = !stacks in
+    begin match graph.nodes.(n) with
+    | Some ((ssa, cfnode), preds, succs) ->
+       let ssa = List.map ssa_ssanode ssa in
+       graph.nodes.(n) <- Some ((ssa, ssa_cfnode cfnode), preds, succs);
+       List.iter (fun succ ->
+           match graph.nodes.(succ) with
+           | Some ((ssa, cfnode), preds, succs) ->
+              (* Suppose n is the j-th predecessor of succ *)
+              let rec find_j n succ = function
+                | pred :: preds ->
+                   if pred = succ then n else find_j (n + 1) succ preds
+                | [] -> assert false
+              in
+              let j = find_j 0 n (IntSet.elements preds) in
+              graph.nodes.(succ) <- Some ((List.map (fix_phi j) ssa, cfnode), preds, succs)
+           | None -> assert false
+         ) (IntSet.elements succs)
+    | None -> assert false
+    end;
+    IntSet.iter (fun child -> rename child) (children.(n));
+    stacks := old_stacks
+  in
+  rename root
+
+let ssa instrs =
+  let start, finish, cfg = control_flow_graph instrs in
+  let idom = immediate_dominators cfg start in
+  let children = dominator_children idom in
+  let df = dominance_frontiers cfg start idom children in
+  place_phi_functions cfg df;
+  rename_variables cfg start children;
+  cfg
+
+(* Debugging utilities for outputing Graphviz files. *)
+
+let string_of_phis = function
+  | [] -> ""
+  | phis -> Util.string_of_list "\\l" (fun (Phi (id, args)) -> string_of_id id ^ " = phi(" ^ Util.string_of_list ", " string_of_id args ^ ")") phis ^ "\\l"
+
+let string_of_node = function
+  | (phis, CF_label label) -> string_of_phis phis ^ label
+  | (phis, CF_block instrs) -> string_of_phis phis ^ Util.string_of_list "\\l" (fun instr -> String.escaped (Pretty_print_sail.to_string (pp_instr ~short:true instr))) instrs
+  | (phis, CF_start) -> string_of_phis phis ^ "START"
+
+let vertex_color = function
+  | (_, CF_start)   -> "peachpuff"
+  | (_, CF_block _) -> "white"
+  | (_, CF_label _) -> "springgreen"
+
+let edge_color node_from node_to =
+  match node_from, node_to with
+  | CF_block _, CF_block _ -> "black"
+  | CF_label _, CF_block _ -> "red"
+  | CF_block _, CF_label _ -> "blue"
+  | _, _ -> "deeppink"
+
+let make_dot out_chan graph =
+  Util.opt_colors := false;
+  output_string out_chan "digraph DEPS {\n";
+  let make_node i n =
+    output_string out_chan (Printf.sprintf "  n%i [label=\"%s\";shape=box;style=filled;fillcolor=%s];\n" i (string_of_node n) (vertex_color n))
+  in
+  let make_line i s =
+    output_string out_chan (Printf.sprintf "  n%i -> n%i [color=black];\n" i s)
+  in
+  for i = 0 to graph.next - 1 do
+    match graph.nodes.(i) with
+    | Some (n, _, successors) ->
+       make_node i n;
+       IntSet.iter (fun s -> make_line i s) successors
+    | None -> ()
+  done;
+  output_string out_chan "}\n";
+  Util.opt_colors := true
+
+let make_dominators_dot out_chan idom graph =
+  Util.opt_colors := false;
+  output_string out_chan "digraph DOMS {\n";
+  let make_node i n =
+    output_string out_chan (Printf.sprintf "  n%i [label=\"%s\";shape=box;style=filled;fillcolor=%s];\n" i (string_of_node n) (vertex_color n))
+  in
+  let make_line i s =
+    output_string out_chan (Printf.sprintf "  n%i -> n%i [color=black];\n" i s)
+  in
+  for i = 0 to Array.length idom - 1 do
+    match graph.nodes.(i) with
+    | Some (n, _, _) ->
+       if idom.(i) = -1 then
+         make_node i n
+       else
+         (make_node i n; make_line i idom.(i))
+    | None -> ()
+  done;
+  output_string out_chan "}\n";
+  Util.opt_colors := true
diff --git a/src/jib/jib_ssa.mli b/src/jib/jib_ssa.mli
new file mode 100644
index 00000000..3796a114
--- /dev/null
+++ b/src/jib/jib_ssa.mli
@@ -0,0 +1,85 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*    Alasdair Armstrong                                                  *)
+(*    Brian Campbell                                                      *)
+(*    Thomas Bauereiss                                                    *)
+(*    Anthony Fox                                                         *)
+(*    Jon French                                                          *)
+(*    Dominic Mulligan                                                    *)
+(*    Stephen Kell                                                        *)
+(*    Mark Wassell                                                        *)
+(*                                                                        *)
+(*  All rights reserved.                                                  *)
+(*                                                                        *)
+(*  This software was developed by the University of Cambridge Computer   *)
+(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
+(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
+(*                                                                        *)
+(*  Redistribution and use in source and binary forms, with or without    *)
+(*  modification, are permitted provided that the following conditions    *)
+(*  are met:                                                              *)
+(*  1. Redistributions of source code must retain the above copyright     *)
+(*     notice, this list of conditions and the following disclaimer.      *)
+(*  2. Redistributions in binary form must reproduce the above copyright  *)
+(*     notice, this list of conditions and the following disclaimer in    *)
+(*     the documentation and/or other materials provided with the         *)
+(*     distribution.                                                      *)
+(*                                                                        *)
+(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
+(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
+(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
+(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
+(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
+(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
+(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
+(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
+(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
+(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
+(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
+(*  SUCH DAMAGE.                                                          *)
+(**************************************************************************)
+
+open Array
+
+(** A mutable array based graph type, with nodes indexed by integers. *)
+type 'a array_graph
+
+(** Create an empty array_graph, specifying the initial size of the
+   underlying array. *)
+val make : initial_size:int -> unit -> 'a array_graph
+
+(** Add a vertex to a graph, returning the index of the inserted
+   vertex. If the number of vertices exceeds the size of the
+   underlying array, then it is dynamically resized. *)
+val add_vertex : 'a -> 'a array_graph -> int
+
+(** Add an edge between two existing vertices. Raises Invalid_argument
+   if either of the vertices do not exist. *)
+val add_edge : int -> int -> 'a array_graph -> unit
+
+type cf_node =
+  | CF_label of string
+  | CF_block of Jib.instr list
+  | CF_start
+
+val control_flow_graph : Jib.instr list -> int * int list * ('a list * cf_node) array_graph
+
+type ssa_elem =
+  | Phi of Ast.id * Ast.id list
+
+(** Convert a list of instructions into SSA form *)
+val ssa : Jib.instr list -> (ssa_elem list * cf_node) array_graph
+
+(** Output the control-flow graph in graphviz format for
+   debugging. Can use 'dot -Tpng X.gv -o X.png' to generate a png
+   image of the graph. *)
+val make_dot : out_channel -> (ssa_elem list * cf_node) array_graph -> unit
diff --git a/src/jib/jib_util.ml b/src/jib/jib_util.ml
index 17227875..81cd07ef 100644
--- a/src/jib/jib_util.ml
+++ b/src/jib/jib_util.ml
@@ -154,6 +154,7 @@ let rec clexp_rename from_id to_id = function
   | CL_current_exception ctyp -> CL_current_exception ctyp
   | CL_have_exception -> CL_have_exception
   | CL_return ctyp -> CL_return ctyp
+  | CL_void -> CL_void
 
 let rec instr_rename from_id to_id (I_aux (instr, aux)) =
   let instr = match instr with
@@ -482,6 +483,7 @@ let rec pp_clexp = function
   | CL_current_exception ctyp -> string "current_exception : " ^^ pp_ctyp ctyp
   | CL_have_exception -> string "have_exception"
   | CL_return ctyp -> string "return : " ^^ pp_ctyp ctyp
+  | CL_void -> string "void"
 
 let rec pp_instr ?short:(short=false) (I_aux (instr, aux)) =
   match instr with
@@ -581,40 +583,6 @@ let pp_cdef = function
      ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace
      ^^ hardline
 
-(**************************************************************************)
-(* 2. Dependency Graphs                                                   *)
-(**************************************************************************)
-
-type graph_node =
-  | G_label of string
-  | G_instr of int * instr
-  | G_start
-
-let string_of_node = function
-  | G_label label -> label
-  | G_instr (n, instr) -> string_of_int n ^ ": " ^ Pretty_print_sail.to_string (pp_instr ~short:true instr)
-  | G_start -> "START"
-
-module Node = struct
-  type t = graph_node
-  let compare gn1 gn2 =
-    match gn1, gn2 with
-    | G_label str1, G_label str2 -> String.compare str1 str2
-    | G_instr (n1, _), G_instr (n2, _) -> compare n1 n2
-    | G_start  , G_start   -> 0
-    | G_start  , _         -> 1
-    | _        , G_start   -> -1
-    | G_instr _, _         -> 1
-    | _        , G_instr _ -> -1
-end
-
-module NodeGraph = Graph.Make(Node)
-
-module NM = Map.Make(Node)
-module NS = Set.Make(Node)
-
-type dep_graph = NodeGraph.graph
-
 let rec fragment_deps = function
   | F_id id | F_ref id -> IdSet.singleton id
   | F_lit _ -> IdSet.empty
@@ -635,6 +603,7 @@ let rec clexp_deps = function
   | CL_have_exception -> IdSet.empty
   | CL_current_exception _ -> IdSet.empty
   | CL_return _ -> IdSet.empty
+  | CL_void -> IdSet.empty
 
 (* Return the direct, read/write dependencies of a single instruction *)
 let instr_deps = function
@@ -646,7 +615,7 @@ let instr_deps = function
   | I_funcall (clexp, _, _, cvals) -> List.fold_left IdSet.union IdSet.empty (List.map cval_deps cvals), clexp_deps clexp
   | I_copy (clexp, cval) -> cval_deps cval, clexp_deps clexp
   | I_alias (clexp, cval) -> cval_deps cval, clexp_deps clexp
-  | I_clear (_, id) -> IdSet.singleton id, IdSet.singleton id
+  | I_clear (_, id) -> IdSet.singleton id, IdSet.empty
   | I_throw cval | I_return cval -> cval_deps cval, IdSet.empty
   | I_block _ | I_try_block _ -> IdSet.empty, IdSet.empty
   | I_comment _ | I_raw _ -> IdSet.empty, IdSet.empty
@@ -656,80 +625,6 @@ let instr_deps = function
   | I_match_failure -> IdSet.empty, IdSet.empty
   | I_end -> IdSet.empty, IdSet.empty
 
-(* instrs_graph returns the control-flow graph for a list of
-   instructions. *)
-let instrs_graph instrs =
-  let icounter = ref 0 in
-  let graph = ref NodeGraph.empty in
-
-  let rec add_instr last_instrs (I_aux (instr, _) as iaux) =
-    incr icounter;
-    let node = G_instr (!icounter, iaux) in
-    match instr with
-    | I_block instrs | I_try_block instrs ->
-       List.fold_left add_instr last_instrs instrs
-    | I_if (_, then_instrs, else_instrs, _) ->
-       List.iter (fun i -> graph := NodeGraph.add_edge' i node !graph) last_instrs;
-       let n1 = List.fold_left add_instr [node] then_instrs in
-       let n2 = List.fold_left add_instr [node] else_instrs in
-       incr icounter;
-       let join = G_instr (!icounter, icomment "join") in
-       List.iter (fun i -> graph := NodeGraph.add_edge' i join !graph) n1;
-       List.iter (fun i -> graph := NodeGraph.add_edge' i join !graph) n2;
-       [join]
-    | I_return _ ->
-       List.iter (fun i -> graph := NodeGraph.add_edge' i node !graph) last_instrs;
-       []
-    | I_label label ->
-       graph := NodeGraph.add_edge' (G_label label) node !graph;
-       node :: last_instrs
-    | I_goto label ->
-       List.iter (fun i -> graph := NodeGraph.add_edge' i node !graph) last_instrs;
-       graph := NodeGraph.add_edge' node (G_label label) !graph;
-       []
-    | I_jump (cval, label) ->
-       List.iter (fun i -> graph := NodeGraph.add_edge' i node !graph) last_instrs;
-       graph := NodeGraph.add_edges' (G_label label) [] !graph;
-       [node]
-    | I_match_failure ->
-       List.iter (fun i -> graph := NodeGraph.add_edge' i node !graph) last_instrs;
-       []
-    | _ ->
-       List.iter (fun i -> graph := NodeGraph.add_edge' i node !graph) last_instrs;
-       [node]
-  in
-  ignore (List.fold_left add_instr [G_start] instrs);
-  let graph = NodeGraph.fix_leaves !graph in
-  graph
-
-let make_dot id graph =
-  Util.opt_colors := false;
-  let to_string node = String.escaped (string_of_node node) in
-  let node_color = function
-    | G_start                               -> "lightpink"
-    | G_instr (_, I_aux (I_decl _, _))      -> "olivedrab1"
-    | G_instr (_, I_aux (I_init _, _))      -> "springgreen"
-    | G_instr (_, I_aux (I_clear _, _))     -> "peachpuff"
-    | G_instr (_, I_aux (I_goto _, _))      -> "orange1"
-    | G_instr (_, I_aux (I_label _, _))     -> "white"
-    | G_instr (_, I_aux (I_raw _, _))       -> "khaki"
-    | G_instr (_, I_aux (I_return _, _))    -> "deeppink"
-    | G_instr (_, I_aux (I_undefined _, _)) -> "deeppink"
-    | G_instr _                             -> "azure"
-    | G_label _                             -> "lightpink"
-  in
-  let edge_color from_node to_node =
-    match from_node, to_node with
-    | G_start  , _         -> "goldenrod4"
-    | G_label _, _         -> "darkgreen"
-    | _        , G_label _ -> "goldenrod4"
-    | G_instr _, G_instr _ -> "black"
-    | _        , _         -> "coral3"
-  in
-  let out_chan = open_out (Util.zencode_string (string_of_id id) ^ ".gv") in
-  NodeGraph.make_dot node_color edge_color to_string out_chan graph;
-  close_out out_chan
-
 let rec map_clexp_ctyp f = function
   | CL_id (id, ctyp) -> CL_id (id, f ctyp)
   | CL_field (clexp, field) -> CL_field (map_clexp_ctyp f clexp, field)
@@ -738,6 +633,7 @@ let rec map_clexp_ctyp f = function
   | CL_current_exception ctyp -> CL_current_exception (f ctyp)
   | CL_have_exception -> CL_have_exception
   | CL_return ctyp -> CL_return (f ctyp)
+  | CL_void -> CL_void
 
 let rec map_instr_ctyp f (I_aux (instr, aux)) =
   let instr = match instr with
@@ -778,6 +674,18 @@ let rec map_instr f (I_aux (instr, aux)) =
   in
   f (I_aux (instr, aux))
 
+(** Iterate over each instruction within an instruction, bottom-up *)
+let rec iter_instr f (I_aux (instr, aux)) =
+  match instr with
+  | I_decl _ | I_init _ | I_reset _ | I_reinit _
+    | I_funcall _ | I_copy _ | I_alias _ | I_clear _ | I_jump _ | I_throw _ | I_return _
+    | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_match_failure | I_undefined _ | I_end -> f (I_aux (instr, aux))
+  | I_if (cval, instrs1, instrs2, ctyp) ->
+     List.iter (iter_instr f) instrs1;
+     List.iter (iter_instr f) instrs2
+  | I_block instrs | I_try_block instrs ->
+     List.iter (iter_instr f) instrs
+
 (** Map over each instruction in a cdef using map_instr *)
 let cdef_map_instr f = function
   | CDEF_reg_dec (id, ctyp, instrs) -> CDEF_reg_dec (id, ctyp, List.map (map_instr f) instrs)
@@ -816,17 +724,21 @@ let rec map_instrs f (I_aux (instr, aux)) =
   in
   I_aux (instr, aux)
 
+let map_instr_list f instrs =
+  List.map (map_instr f) instrs
+
+let map_instrs_list f instrs =
+  f (List.map (map_instrs f) instrs)
+
 let rec instr_ids (I_aux (instr, _)) =
   let reads, writes = instr_deps instr in
-  IdSet.of_list (IdSet.elements reads @ IdSet.elements writes)
+  IdSet.union reads writes
 
 let rec instr_reads (I_aux (instr, _)) =
-  let reads, _ = instr_deps instr in
-  IdSet.of_list (IdSet.elements reads)
+  fst (instr_deps instr)
 
 let rec instr_writes (I_aux (instr, _)) =
-  let _, writes = instr_deps instr in
-  IdSet.of_list (IdSet.elements writes)
+  snd (instr_deps instr)
 
 let rec filter_instrs f instrs =
   let filter_instrs' = function
@@ -878,6 +790,7 @@ let rec clexp_ctyp = function
      end
   | CL_have_exception -> CT_bool
   | CL_current_exception ctyp -> ctyp
+  | CL_void -> CT_unit
 
 let rec instr_ctyps (I_aux (instr, aux)) =
   match instr with
@@ -933,3 +846,29 @@ let instr_split_at f =
     | instr :: instrs -> instr_split_at' f (instr :: before) instrs
   in
   instr_split_at' f []
+
+let rec instrs_rename from_id to_id =
+  let rename id = if Id.compare id from_id = 0 then to_id else id in
+  let crename = cval_rename from_id to_id in
+  let irename instrs = instrs_rename from_id to_id instrs in
+  let lrename = clexp_rename from_id to_id in
+  function
+  | (I_aux (I_decl (ctyp, new_id), _) :: _) as instrs when Id.compare from_id new_id = 0 -> instrs
+  | I_aux (I_decl (ctyp, new_id), aux) :: instrs -> I_aux (I_decl (ctyp, new_id), aux) :: irename instrs
+  | I_aux (I_reset (ctyp, id), aux) :: instrs -> I_aux (I_reset (ctyp, rename id), aux) :: irename instrs
+  | I_aux (I_init (ctyp, id, cval), aux) :: instrs -> I_aux (I_init (ctyp, rename id, crename cval), aux) :: irename instrs
+  | I_aux (I_reinit (ctyp, id, cval), aux) :: instrs -> I_aux (I_reinit (ctyp, rename id, crename cval), aux) :: irename instrs
+  | I_aux (I_if (cval, then_instrs, else_instrs, ctyp), aux) :: instrs ->
+     I_aux (I_if (crename cval, irename then_instrs, irename else_instrs, ctyp), aux) :: irename instrs
+  | I_aux (I_jump (cval, label), aux) :: instrs -> I_aux (I_jump (crename cval, label), aux) :: irename instrs
+  | I_aux (I_funcall (clexp, extern, id, cvals), aux) :: instrs ->
+     I_aux (I_funcall (lrename clexp, extern, rename id, List.map crename cvals), aux) :: irename instrs
+  | I_aux (I_copy (clexp, cval), aux) :: instrs -> I_aux (I_copy (lrename clexp, crename cval), aux) :: irename instrs
+  | I_aux (I_alias (clexp, cval), aux) :: instrs -> I_aux (I_alias (lrename clexp, crename cval), aux) :: irename instrs
+  | I_aux (I_clear (ctyp, id), aux) :: instrs -> I_aux (I_clear (ctyp, rename id), aux) :: irename instrs
+  | I_aux (I_return cval, aux) :: instrs -> I_aux (I_return (crename cval), aux) :: irename instrs
+  | I_aux (I_block block, aux) :: instrs -> I_aux (I_block (irename block), aux) :: irename instrs
+  | I_aux (I_try_block block, aux) :: instrs -> I_aux (I_try_block (irename block), aux) :: irename instrs
+  | I_aux (I_throw cval, aux) :: instrs -> I_aux (I_throw (crename cval), aux) :: irename instrs
+  | (I_aux ((I_comment _ | I_raw _ | I_end | I_label _ | I_goto _ | I_match_failure | I_undefined _), _) as instr) :: instrs -> instr :: irename instrs
+  | [] -> []
diff --git a/src/sail.ml b/src/sail.ml
index 50719776..b654831b 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -290,7 +290,7 @@ let options = Arg.align ([
     Arg.String (fun l -> opt_ddump_rewrite_ast := Some (l, 0)),
     "<prefix> (debug) dump the ast after each rewriting step to <prefix>_<i>.lem");
   ( "-ddump_flow_graphs",
-    Arg.Set C_backend.opt_debug_flow_graphs,
+    Arg.Set Jib_compile.opt_debug_flow_graphs,
     " (debug) dump flow analysis for Sail functions when compiling to C");
   ( "-dtc_verbose",
     Arg.Int (fun verbosity -> Type_check.opt_tc_debug := verbosity),
diff --git a/src/sail.odocl b/src/sail.odocl
index 4e91e22e..0a45eba3 100644
--- a/src/sail.odocl
+++ b/src/sail.odocl
@@ -11,6 +11,7 @@ specialize
 anf
 jib
 jib_compile
+jib_ssa
 jib_util
 util
 graph
\ No newline at end of file