Factor utility functions for IR into separate file and struct update optimizations.

Move the utility functions for graph generation and pretty printing of
intermediate representation instructions into a separate file,
bytecode_util.ml, by analogy with ast_util.ml.

Add an optimization pass that searches for specific patterns of struct
updates and removes uncessary copying of the structs involved. With
this optimisation pass the time taken for u-boot to run approx
57,000,000 instructions goes down from about 11-12 minutes to 8
minutes (about 120,000 IPS).

3 files changed, 556 insertions, 417 deletions

diff --git a/src/bytecode_util.ml b/src/bytecode_util.ml
new file mode 100644
index 00000000..96513d7f
--- /dev/null
+++ b/src/bytecode_util.ml
@@ -0,0 +1,471 @@
+(**************************************************************************)
+(*     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
+open Ast_util
+open Bytecode
+open Value2
+open PPrint
+
+(* Define wrappers for creating bytecode instructions. Each function
+   uses a counter to assign each instruction a unique identifier. *)
+
+let instr_counter = ref 0
+
+let instr_number () =
+  let n = !instr_counter in
+  incr instr_counter;
+  n
+
+let idecl ?loc:(l=Parse_ast.Unknown) ctyp id =
+  I_aux (I_decl (ctyp, id), (instr_number (), l))
+
+let ialloc ?loc:(l=Parse_ast.Unknown) ctyp id =
+  I_aux (I_alloc (ctyp, id), (instr_number (), l))
+
+let iinit ?loc:(l=Parse_ast.Unknown) ctyp id cval =
+  I_aux (I_init (ctyp, id, cval), (instr_number (), l))
+
+let iif ?loc:(l=Parse_ast.Unknown) cval then_instrs else_instrs ctyp =
+  I_aux (I_if (cval, then_instrs, else_instrs, ctyp), (instr_number (), l))
+
+let ifuncall ?loc:(l=Parse_ast.Unknown) clexp id cvals ctyp =
+  I_aux (I_funcall (clexp, false, id, cvals, ctyp), (instr_number (), l))
+
+let iextern ?loc:(l=Parse_ast.Unknown) clexp id cvals ctyp =
+  I_aux (I_funcall (clexp, true, id, cvals, ctyp), (instr_number (), l))
+
+let icopy ?loc:(l=Parse_ast.Unknown) clexp cval =
+  I_aux (I_copy (clexp, cval), (instr_number (), l))
+
+let iconvert ?loc:(l=Parse_ast.Unknown) clexp ctyp1 id ctyp2 =
+  I_aux (I_convert (clexp, ctyp1, id, ctyp2), (instr_number (), l))
+
+let iclear ?loc:(l=Parse_ast.Unknown) ctyp id =
+  I_aux (I_clear (ctyp, id), (instr_number (), l))
+
+let ireturn ?loc:(l=Parse_ast.Unknown) cval =
+  I_aux (I_return cval, (instr_number (), l))
+
+let iblock ?loc:(l=Parse_ast.Unknown) instrs =
+  I_aux (I_block instrs, (instr_number (), l))
+
+let itry_block ?loc:(l=Parse_ast.Unknown) instrs =
+  I_aux (I_try_block instrs, (instr_number (), l))
+
+let ithrow ?loc:(l=Parse_ast.Unknown) cval =
+  I_aux (I_throw cval, (instr_number (), l))
+let icomment ?loc:(l=Parse_ast.Unknown) str =
+  I_aux (I_comment str, (instr_number (), l))
+
+let ilabel ?loc:(l=Parse_ast.Unknown) label =
+  I_aux (I_label label, (instr_number (), l))
+let igoto ?loc:(l=Parse_ast.Unknown) label =
+  I_aux (I_goto label, (instr_number (), l))
+
+let imatch_failure ?loc:(l=Parse_ast.Unknown) () =
+  I_aux (I_match_failure, (instr_number (), l))
+
+let iraw ?loc:(l=Parse_ast.Unknown) str =
+  I_aux (I_raw str, (instr_number (), l))
+
+let ijump ?loc:(l=Parse_ast.Unknown) cval label =
+  I_aux (I_jump (cval, label), (instr_number (), l))
+
+(**************************************************************************)
+(* 1. Instruction pretty printer                                          *)
+(**************************************************************************)
+
+let string_of_value = function
+  | V_bits bs -> Sail_values.show_bitlist bs ^ "ul"
+  | V_int i -> Big_int.to_string i ^ "l"
+  | V_bool true -> "true"
+  | V_bool false -> "false"
+  | V_null -> "NULL"
+  | V_unit -> "UNIT"
+  | V_bit Sail_values.B0 -> "0ul"
+  | V_bit Sail_values.B1 -> "1ul"
+  | V_string str -> "\"" ^ str ^ "\""
+  | V_ctor_kind str -> "Kind_" ^ Util.zencode_string str
+  | _ -> failwith "Cannot convert value to string"
+
+let rec string_of_fragment ?zencode:(zencode=true) = function
+  | F_id id when zencode -> Util.zencode_string (string_of_id id)
+  | F_id id -> string_of_id id
+  | F_ref id when zencode -> "&" ^ Util.zencode_string (string_of_id id)
+  | F_ref id -> "&" ^ string_of_id id
+  | F_lit v -> string_of_value v
+  | F_call (str, frags) ->
+     Printf.sprintf "%s(%s)" str (Util.string_of_list ", " (string_of_fragment ~zencode:zencode) frags)
+  | F_field (f, field) ->
+     Printf.sprintf "%s.%s" (string_of_fragment' ~zencode:zencode f) field
+  | F_op (f1, op, f2) ->
+     Printf.sprintf "%s %s %s" (string_of_fragment' ~zencode:zencode f1) op (string_of_fragment' ~zencode:zencode f2)
+  | F_unary (op, f) ->
+     op ^ string_of_fragment' ~zencode:zencode f
+  | F_have_exception -> "have_exception"
+  | F_current_exception -> "(*current_exception)"
+  | F_raw raw -> raw
+and string_of_fragment' ?zencode:(zencode=true) f =
+  match f with
+  | F_op _ | F_unary _ -> "(" ^ string_of_fragment ~zencode:zencode f ^ ")"
+  | _ -> string_of_fragment ~zencode:zencode f
+
+(* String representation of ctyps here is only for debugging and
+   intermediate language pretty-printer. *)
+let rec string_of_ctyp = function
+  | CT_mpz -> "mpz_t"
+  | CT_bv true -> "bv_t(dec)"
+  | CT_bv false -> "bv_t(inc)"
+  | CT_uint64 (n, true) -> "uint64_t(" ^ string_of_int n ^ ", dec)"
+  | CT_uint64 (n, false) -> "uint64_t(" ^ string_of_int n ^ ", int)"
+  | CT_int64 -> "int64_t"
+  | CT_bit -> "bit"
+  | CT_unit -> "unit"
+  | CT_bool -> "bool"
+  | CT_real -> "real"
+  | CT_tup ctyps -> "(" ^ Util.string_of_list ", " string_of_ctyp ctyps ^ ")"
+  | CT_struct (id, _) | CT_enum (id, _) | CT_variant (id, _) -> string_of_id id
+  | CT_string -> "string"
+  | CT_vector (true, ctyp) -> "vector(dec, " ^ string_of_ctyp ctyp ^ ")"
+  | CT_vector (false, ctyp) -> "vector(inc, " ^ string_of_ctyp ctyp ^ ")"
+  | CT_list ctyp -> "list(" ^ string_of_ctyp ctyp ^ ")"
+  | CT_ref ctyp -> "ref(" ^ string_of_ctyp ctyp ^ ")"
+
+let pp_id id =
+  string (string_of_id id)
+
+let pp_ctyp ctyp =
+  string (string_of_ctyp ctyp |> Util.yellow |> Util.clear)
+
+let pp_keyword str =
+  string ((str |> Util.red |> Util.clear) ^ " ")
+
+let pp_cval (frag, ctyp) =
+  string (string_of_fragment ~zencode:false frag) ^^ string " : " ^^ pp_ctyp ctyp
+
+let rec pp_clexp = function
+  | CL_id id -> pp_id id
+  | CL_field (id, field) -> pp_id id ^^ string "." ^^ string field
+  | CL_addr id -> string "*" ^^ pp_id id
+  | CL_addr_field (id, field) -> pp_id id ^^ string "->" ^^ string field
+  | CL_current_exception -> string "current_exception"
+  | CL_have_exception -> string "have_exception"
+
+let rec pp_instr ?short:(short=false) (I_aux (instr, aux)) =
+  match instr with
+  | I_decl (ctyp, id) ->
+     pp_keyword "var" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp
+  | I_if (cval, then_instrs, else_instrs, ctyp) ->
+     let pp_if_block = function
+       | [] -> string "{}"
+       | instrs -> surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace
+     in
+     parens (pp_ctyp ctyp) ^^ space
+     ^^ pp_keyword "if" ^^ pp_cval cval
+     ^^ if short then
+          empty
+        else
+          pp_keyword " then" ^^ pp_if_block then_instrs
+          ^^ pp_keyword " else" ^^ pp_if_block else_instrs
+  | I_jump (cval, label) ->
+     pp_keyword "jump" ^^ pp_cval cval ^^ space ^^ string (label |> Util.blue |> Util.clear)
+  | I_block instrs ->
+     surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace
+  | I_try_block instrs ->
+     pp_keyword "try" ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace
+  | I_alloc (ctyp, id) ->
+     pp_keyword "create" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp
+  | I_reset (ctyp, id) ->
+     pp_keyword "recreate" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp
+  | I_init (ctyp, id, cval) ->
+     pp_keyword "create" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp ^^ string " = " ^^ pp_cval cval
+  | I_reinit (ctyp, id, cval) ->
+     pp_keyword "recreate" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp ^^ string " = " ^^ pp_cval cval
+  | I_funcall (x, _, f, args, ctyp2) ->
+     separate space [ pp_clexp x; string "=";
+                      string (string_of_id f |> Util.green |> Util.clear) ^^ parens (separate_map (string ", ") pp_cval args);
+                      string ":"; pp_ctyp ctyp2 ]
+  | I_convert (x, ctyp1, y, ctyp2) ->
+     separate space [ pp_clexp x; colon; pp_ctyp ctyp1; string "=";
+                      pp_keyword "convert" ^^ pp_id y; colon; pp_ctyp ctyp2 ]
+  | I_copy (clexp, cval) ->
+     separate space [pp_clexp clexp; string "="; pp_cval cval]
+  | I_clear (ctyp, id) ->
+     pp_keyword "kill" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp
+  | I_return cval ->
+     pp_keyword "return" ^^ pp_cval cval
+  | I_throw cval ->
+     pp_keyword "throw" ^^ pp_cval cval
+  | I_comment str ->
+     string ("// " ^ str |> Util.magenta |> Util.clear)
+  | I_label str ->
+     string (str |> Util.blue |> Util.clear) ^^ string ":"
+  | I_goto str ->
+     pp_keyword "goto" ^^ string (str |> Util.blue |> Util.clear)
+  | I_match_failure ->
+     pp_keyword "match_failure"
+  | I_raw str ->
+     pp_keyword "C" ^^ string (str |> Util.cyan |> Util.clear)
+
+let pp_ctype_def = function
+  | CTD_enum (id, ids) ->
+     pp_keyword "enum" ^^ pp_id id ^^ string " = "
+     ^^ separate_map (string " | ") pp_id ids
+  | CTD_struct (id, fields) ->
+     pp_keyword "struct" ^^ pp_id id ^^ string " = "
+     ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) (fun (id, ctyp) -> pp_id id ^^ string " : " ^^ pp_ctyp ctyp) fields) rbrace
+  | CTD_variant (id, ctors) ->
+     pp_keyword "union" ^^ pp_id id ^^ string " = "
+     ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) (fun (id, ctyp) -> pp_id id ^^ string " : " ^^ pp_ctyp ctyp) ctors) rbrace
+
+let pp_cdef = function
+  | CDEF_spec (id, ctyps, ctyp) ->
+     pp_keyword "val" ^^ pp_id id ^^ string " : " ^^ parens (separate_map (comma ^^ space) pp_ctyp ctyps) ^^ string " -> " ^^ pp_ctyp ctyp
+     ^^ hardline
+  | CDEF_fundef (id, ret, args, instrs) ->
+     let ret = match ret with
+       | None -> empty
+       | Some id -> space ^^ pp_id id
+     in
+     pp_keyword "function" ^^ pp_id id ^^ ret ^^ parens (separate_map (comma ^^ space) pp_id args) ^^ space
+     ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace
+     ^^ hardline
+  | CDEF_reg_dec (id, ctyp) ->
+     pp_keyword "register" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp
+     ^^ hardline
+  | CDEF_type tdef -> pp_ctype_def tdef ^^ hardline
+  | CDEF_let (n, bindings, instrs, cleanup) ->
+     let pp_binding (id, ctyp) = pp_id id ^^ string " : " ^^ pp_ctyp ctyp in
+     pp_keyword "let" ^^ string (string_of_int n) ^^ parens (separate_map (comma ^^ space) pp_binding bindings) ^^ space
+     ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace ^^ space
+     ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr cleanup) rbrace ^^ space
+     ^^ hardline
+  | CDEF_startup (id, instrs)->
+     pp_keyword "startup" ^^ pp_id id ^^ space
+     ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace
+     ^^ hardline
+  | CDEF_finish (id, instrs)->
+     pp_keyword "finish" ^^ pp_id id ^^ space
+     ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace
+     ^^ hardline
+
+(**************************************************************************)
+(* 2. Dependency Graphs                                                   *)
+(**************************************************************************)
+
+type graph_node =
+  | G_id of id
+  | G_label of string
+  | G_instr of int * instr
+  | G_start
+
+let string_of_node = function
+  | G_id id -> string_of_id id
+  | 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_id id1, G_id id2 -> Id.compare id1 id2
+    | G_label str1, G_label str2 -> String.compare str1 str2
+    | G_instr (n1, _), G_instr (n2, _) -> compare n1 n2
+    | G_start  , _         -> 1
+    | _        , G_start   -> -1
+    | G_instr _, _         -> 1
+    | _        , G_instr _ -> -1
+    | G_id _   , _         -> 1
+    | _        , G_id _    -> -1
+end
+
+module NM = Map.Make(Node)
+module NS = Set.Make(Node)
+
+type dep_graph = NS.t NM.t
+
+let rec fragment_deps = function
+  | F_id id | F_ref id -> NS.singleton (G_id id)
+  | F_lit _ -> NS.empty
+  | F_field (frag, _) | F_unary (_, frag) -> fragment_deps frag
+  | F_call (_, frags) -> List.fold_left NS.union NS.empty (List.map fragment_deps frags)
+  | F_op (frag1, _, frag2) -> NS.union (fragment_deps frag1) (fragment_deps frag2)
+  | F_current_exception -> NS.empty
+  | F_have_exception -> NS.empty
+  | F_raw _ -> NS.empty
+
+let cval_deps = function (frag, _) -> fragment_deps frag
+
+let rec clexp_deps = function
+  | CL_id id -> NS.singleton (G_id id)
+  | CL_field (id, _) -> NS.singleton (G_id id)
+  | CL_addr id -> NS.singleton (G_id id)
+  | CL_addr_field (id, _) -> NS.singleton (G_id id)
+  | CL_have_exception -> NS.empty
+  | CL_current_exception -> NS.empty
+
+(** Return the direct, non program-order dependencies of a single
+   instruction **)
+let instr_deps = function
+  | I_decl (ctyp, id) -> NS.empty, NS.singleton (G_id id)
+  | I_alloc (ctyp, id) | I_reset (ctyp, id) -> NS.empty, NS.singleton (G_id id)
+  | I_init (ctyp, id, cval) | I_reinit (ctyp, id, cval) -> cval_deps cval, NS.singleton (G_id id)
+  | I_if (cval, _, _, _) -> cval_deps cval, NS.empty
+  | I_jump (cval, label) -> cval_deps cval, NS.singleton (G_label label)
+  | I_funcall (clexp, _, _, cvals, _) -> List.fold_left NS.union NS.empty (List.map cval_deps cvals), clexp_deps clexp
+  | I_convert (clexp, _, id, _) -> NS.singleton (G_id id), clexp_deps clexp
+  | I_copy (clexp, cval) -> cval_deps cval, clexp_deps clexp
+  | I_clear (_, id) -> NS.singleton (G_id id), NS.singleton (G_id id)
+  | I_throw cval | I_return cval -> cval_deps cval, NS.empty
+  | I_block _ | I_try_block _ -> NS.empty, NS.empty
+  | I_comment _ | I_raw _ -> NS.empty, NS.empty
+  | I_label label -> NS.singleton (G_label label), NS.empty
+  | I_goto label -> NS.empty, NS.singleton (G_label label)
+  | I_match_failure -> NS.empty, NS.empty
+
+let add_link from_node to_node graph =
+  try
+    NM.add from_node (NS.add to_node (NM.find from_node graph)) graph
+  with
+  | Not_found -> NM.add from_node (NS.singleton to_node) graph
+
+let leaves graph =
+  List.fold_left (fun acc (from_node, to_nodes) -> NS.filter (fun to_node -> Node.compare to_node from_node != 0) (NS.union acc to_nodes))
+                 NS.empty
+                 (NM.bindings graph)
+
+(* Ensure that all leaves exist in the graph *)
+let fix_leaves graph =
+  NS.fold (fun leaf graph -> if NM.mem leaf graph then graph else NM.add leaf NS.empty graph) (leaves graph) graph
+
+let instrs_graph instrs =
+  let icounter = ref 0 in
+  let graph = ref NM.empty in
+
+  let rec add_instr last_instr (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_instr instrs
+    | I_if (_, then_instrs, else_instrs, _) ->
+       begin
+         let inputs, _ = instr_deps instr in (* if has no outputs *)
+         graph := add_link last_instr node !graph;
+         NS.iter (fun input -> graph := add_link input node !graph) inputs;
+         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
+         graph := add_link n1 join !graph;
+         graph := add_link n2 join !graph;
+         join
+       end
+    | I_goto label ->
+       begin
+         let _, outputs = instr_deps instr in
+         graph := add_link last_instr node !graph;
+         NS.iter (fun output -> graph := add_link node output !graph) outputs;
+         incr icounter;
+         G_instr (!icounter, icomment "after goto")
+       end
+    | _ ->
+       begin
+         let inputs, outputs = instr_deps instr in
+         graph := add_link last_instr node !graph;
+         NS.iter (fun input -> graph := add_link input node !graph) inputs;
+         NS.iter (fun output -> graph := add_link node output !graph) outputs;
+         node
+       end
+  in
+  ignore (List.fold_left add_instr G_start instrs);
+  fix_leaves !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_id _                            -> "yellow"
+    | G_instr (_, I_aux (I_decl _, _))  -> "olivedrab1"
+    | G_instr (_, I_aux (I_init _, _))  -> "springgreen"
+    | G_instr (_, I_aux (I_alloc _, _)) -> "palegreen"
+    | 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 _                         -> "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"
+    | G_id _   , G_instr _ -> "blue3"
+    | G_instr _, G_id _    -> "red3"
+    | _        , _         -> "coral3"
+  in
+  let out_chan = open_out (Util.zencode_string (string_of_id id) ^ ".gv") in
+  output_string out_chan "digraph DEPS {\n";
+  let make_node from_node =
+    output_string out_chan (Printf.sprintf "  \"%s\" [fillcolor=%s;style=filled];\n" (to_string from_node) (node_color from_node))
+  in
+  let make_line from_node to_node =
+    output_string out_chan (Printf.sprintf "  \"%s\" -> \"%s\" [color=%s];\n" (to_string from_node) (to_string to_node) (edge_color from_node to_node))
+  in
+  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;
+  close_out out_chan
diff --git a/src/c_backend.ml b/src/c_backend.ml
index 816e37fa..59656152 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -51,6 +51,7 @@
 open Ast
 open Ast_util
 open Bytecode
+open Bytecode_util
 open Type_check
 open PPrint
 open Value2
@@ -81,41 +82,6 @@ let lvar_typ = function
   | Enum typ -> typ
   | _ -> assert false
 
-let string_of_value = function
-  | V_bits bs -> Sail_values.show_bitlist bs ^ "ul"
-  | V_int i -> Big_int.to_string i ^ "l"
-  | V_bool true -> "true"
-  | V_bool false -> "false"
-  | V_null -> "NULL"
-  | V_unit -> "UNIT"
-  | V_bit Sail_values.B0 -> "0ul"
-  | V_bit Sail_values.B1 -> "1ul"
-  | V_string str -> "\"" ^ str ^ "\""
-  | V_ctor_kind str -> "Kind_" ^ Util.zencode_string str
-  | _ -> failwith "Cannot convert value to string"
-
-let rec string_of_fragment ?zencode:(zencode=true) = function
-  | F_id id when zencode -> Util.zencode_string (string_of_id id)
-  | F_id id -> string_of_id id
-  | F_ref id when zencode -> "&" ^ Util.zencode_string (string_of_id id)
-  | F_ref id -> "&" ^ string_of_id id
-  | F_lit v -> string_of_value v
-  | F_call (str, frags) ->
-     Printf.sprintf "%s(%s)" str (Util.string_of_list ", " (string_of_fragment ~zencode:zencode) frags)
-  | F_field (f, field) ->
-     Printf.sprintf "%s.%s" (string_of_fragment' ~zencode:zencode f) field
-  | F_op (f1, op, f2) ->
-     Printf.sprintf "%s %s %s" (string_of_fragment' ~zencode:zencode f1) op (string_of_fragment' ~zencode:zencode f2)
-  | F_unary (op, f) ->
-     op ^ string_of_fragment' ~zencode:zencode f
-  | F_have_exception -> "have_exception"
-  | F_current_exception -> "(*current_exception)"
-  | F_raw raw -> raw
-and string_of_fragment' ?zencode:(zencode=true) f =
-  match f with
-  | F_op _ | F_unary _ -> "(" ^ string_of_fragment ~zencode:zencode f ^ ")"
-  | _ -> string_of_fragment ~zencode:zencode f
-
 (**************************************************************************)
 (* 1. Conversion to A-normal form (ANF)                                   *)
 (**************************************************************************)
@@ -374,9 +340,6 @@ let rec map_functions f (AE_aux (aexp, env, l)) =
 
 (* For debugging we provide a pretty printer for ANF expressions. *)
 
-let pp_id id =
-  string (string_of_id id)
-
 let pp_lvar lvar doc =
   match lvar with
   | Register typ ->
@@ -806,27 +769,6 @@ let rec ctyp_equal ctyp1 ctyp2 =
   | CT_ref ctyp1, CT_ref ctyp2 -> ctyp_equal ctyp1 ctyp2
   | _, _ -> false
 
-(* String representation of ctyps here is only for debugging and
-   intermediate language pretty-printer. *)
-let rec string_of_ctyp = function
-  | CT_mpz -> "mpz_t"
-  | CT_bv true -> "bv_t(dec)"
-  | CT_bv false -> "bv_t(inc)"
-  | CT_uint64 (n, true) -> "uint64_t(" ^ string_of_int n ^ ", dec)"
-  | CT_uint64 (n, false) -> "uint64_t(" ^ string_of_int n ^ ", int)"
-  | CT_int64 -> "int64_t"
-  | CT_bit -> "bit"
-  | CT_unit -> "unit"
-  | CT_bool -> "bool"
-  | CT_real -> "real"
-  | CT_tup ctyps -> "(" ^ Util.string_of_list ", " string_of_ctyp ctyps ^ ")"
-  | CT_struct (id, _) | CT_enum (id, _) | CT_variant (id, _) -> string_of_id id
-  | CT_string -> "string"
-  | CT_vector (true, ctyp) -> "vector(dec, " ^ string_of_ctyp ctyp ^ ")"
-  | CT_vector (false, ctyp) -> "vector(inc, " ^ string_of_ctyp ctyp ^ ")"
-  | CT_list ctyp -> "list(" ^ string_of_ctyp ctyp ^ ")"
-  | CT_ref ctyp -> "ref(" ^ string_of_ctyp ctyp ^ ")"
-
 (** Convert a sail type into a C-type **)
 let rec ctyp_of_typ ctx typ =
   let Typ_aux (typ_aux, l) as typ = Env.expand_synonyms ctx.tc_env typ in
@@ -1040,6 +982,18 @@ let analyze_primop' ctx env l id args typ =
      AE_val (AV_C_fragment (F_op (v1, "+", v2), typ))
              *)
 
+  | "add_bits", [AV_C_fragment (v1, typ1); AV_C_fragment (v2, typ2)] ->
+     AE_val (AV_C_fragment (F_op (v1, "+", v2), typ))
+
+  | "xor_bits", [AV_C_fragment (v1, typ1); AV_C_fragment (v2, typ2)] ->
+     AE_val (AV_C_fragment (F_op (v1, "^", v2), typ))
+
+  | "or_bits", [AV_C_fragment (v1, typ1); AV_C_fragment (v2, typ2)] ->
+     AE_val (AV_C_fragment (F_op (v1, "|", v2), typ))
+
+  | "and_bits", [AV_C_fragment (v1, typ1); AV_C_fragment (v2, typ2)] ->
+     AE_val (AV_C_fragment (F_op (v1, "&", v2), typ))
+
   | "vector_subrange", [AV_C_fragment (vec, _); AV_C_fragment (f, _); AV_C_fragment (t, _)] ->
      let len = F_op (f, "-", F_op (t, "-", v_one)) in
      AE_val (AV_C_fragment (F_op (F_call ("safe_rshift", [F_raw "UINT64_MAX"; F_op (v_int 64, "-", len)]), "&", F_op (vec, ">>", t)), typ))
@@ -1072,7 +1026,7 @@ let analyze_primop' ctx env l id args typ =
         AE_val (AV_C_fragment (frag, typ))
      | _ -> no_change
      end
-(*
+
   | "replicate_bits", [AV_C_fragment (vec, vtyp); AV_C_fragment (times, _)] ->
      begin match destruct_vector ctx.tc_env typ, destruct_vector ctx.tc_env vtyp with
      | Some (Nexp_aux (Nexp_constant n, _), _, _), Some (Nexp_aux (Nexp_constant m, _), _, _)
@@ -1080,7 +1034,6 @@ let analyze_primop' ctx env l id args typ =
         AE_val (AV_C_fragment (F_call ("fast_replicate_bits", [F_lit (V_int m); vec; times]), typ))
      | _ -> no_change
      end
- *)
 
   | "undefined_bool", _ ->
      AE_val (AV_C_fragment (F_lit (V_bool false), typ))
@@ -1121,52 +1074,6 @@ let analyze_primop ctx env l id args typ =
    expression), cleanup instructions (to deallocate that memory) and
    possibly typing information about what has been translated. **)
 
-let instr_counter = ref 0
-
-let instr_number () =
-  let n = !instr_counter in
-  incr instr_counter;
-  n
-
-let idecl ?loc:(l=Parse_ast.Unknown) ctyp id =
-  I_aux (I_decl (ctyp, id), (instr_number (), l))
-let ialloc ?loc:(l=Parse_ast.Unknown) ctyp id =
-  I_aux (I_alloc (ctyp, id), (instr_number (), l))
-let iinit ?loc:(l=Parse_ast.Unknown) ctyp id cval =
-  I_aux (I_init (ctyp, id, cval), (instr_number (), l))
-let iif ?loc:(l=Parse_ast.Unknown) cval then_instrs else_instrs ctyp =
-  I_aux (I_if (cval, then_instrs, else_instrs, ctyp), (instr_number (), l))
-let ifuncall ?loc:(l=Parse_ast.Unknown) clexp id cvals ctyp =
-  I_aux (I_funcall (clexp, false, id, cvals, ctyp), (instr_number (), l))
-let iextern ?loc:(l=Parse_ast.Unknown) clexp id cvals ctyp =
-  I_aux (I_funcall (clexp, true, id, cvals, ctyp), (instr_number (), l))
-let icopy ?loc:(l=Parse_ast.Unknown) clexp cval =
-  I_aux (I_copy (clexp, cval), (instr_number (), l))
-let iconvert ?loc:(l=Parse_ast.Unknown) clexp ctyp1 id ctyp2 =
-  I_aux (I_convert (clexp, ctyp1, id, ctyp2), (instr_number (), l))
-let iclear ?loc:(l=Parse_ast.Unknown) ctyp id =
-  I_aux (I_clear (ctyp, id), (instr_number (), l))
-let ireturn ?loc:(l=Parse_ast.Unknown) cval =
-  I_aux (I_return cval, (instr_number (), l))
-let iblock ?loc:(l=Parse_ast.Unknown) instrs =
-  I_aux (I_block instrs, (instr_number (), l))
-let itry_block ?loc:(l=Parse_ast.Unknown) instrs =
-  I_aux (I_try_block instrs, (instr_number (), l))
-let ithrow ?loc:(l=Parse_ast.Unknown) cval =
-  I_aux (I_throw cval, (instr_number (), l))
-let icomment ?loc:(l=Parse_ast.Unknown) str =
-  I_aux (I_comment str, (instr_number (), l))
-let ilabel ?loc:(l=Parse_ast.Unknown) label =
-  I_aux (I_label label, (instr_number (), l))
-let igoto ?loc:(l=Parse_ast.Unknown) label =
-  I_aux (I_goto label, (instr_number (), l))
-let imatch_failure ?loc:(l=Parse_ast.Unknown) () =
-  I_aux (I_match_failure, (instr_number (), l))
-let iraw ?loc:(l=Parse_ast.Unknown) str =
-  I_aux (I_raw str, (instr_number (), l))
-let ijump ?loc:(l=Parse_ast.Unknown) cval label =
-  I_aux (I_jump (cval, label), (instr_number (), l))
-
 let ctype_def_ctyps = function
   | CTD_enum _ -> []
   | CTD_struct (_, fields) -> List.map snd fields
@@ -1227,121 +1134,6 @@ let cdef_ctyps ctx = function
      @ List.concat (List.map instr_ctyps instrs)
      @ List.concat (List.map instr_ctyps cleanup)
 
-(* For debugging we define a pretty printer for Sail IR instructions *)
-
-let pp_ctyp ctyp =
-  string (string_of_ctyp ctyp |> Util.yellow |> Util.clear)
-
-let pp_keyword str =
-  string ((str |> Util.red |> Util.clear) ^ " ")
-
-let pp_cval (frag, ctyp) = string (string_of_fragment ~zencode:false frag) ^^ string " : " ^^ pp_ctyp ctyp
-
-let rec pp_clexp = function
-  | CL_id id -> pp_id id
-  | CL_field (id, field) -> pp_id id ^^ string "." ^^ string field
-  | CL_addr id -> string "*" ^^ pp_id id
-  | CL_current_exception -> string "current_exception"
-  | CL_have_exception -> string "have_exception"
-
-let rec pp_instr ?short:(short=false) (I_aux (instr, aux)) =
-  match instr with
-  | I_decl (ctyp, id) ->
-     pp_keyword "var" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp
-  | I_if (cval, then_instrs, else_instrs, ctyp) ->
-     let pp_if_block = function
-       | [] -> string "{}"
-       | instrs -> surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace
-     in
-     parens (pp_ctyp ctyp) ^^ space
-     ^^ pp_keyword "if" ^^ pp_cval cval
-     ^^ if short then
-          empty
-        else
-          pp_keyword " then" ^^ pp_if_block then_instrs
-          ^^ pp_keyword " else" ^^ pp_if_block else_instrs
-  | I_jump (cval, label) ->
-     pp_keyword "jump" ^^ pp_cval cval ^^ space ^^ string (label |> Util.blue |> Util.clear)
-  | I_block instrs ->
-     surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace
-  | I_try_block instrs ->
-     pp_keyword "try" ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace
-  | I_alloc (ctyp, id) ->
-     pp_keyword "create" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp
-  | I_reset (ctyp, id) ->
-     pp_keyword "recreate" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp
-  | I_init (ctyp, id, cval) ->
-     pp_keyword "create" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp ^^ string " = " ^^ pp_cval cval
-  | I_reinit (ctyp, id, cval) ->
-     pp_keyword "recreate" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp ^^ string " = " ^^ pp_cval cval
-  | I_funcall (x, _, f, args, ctyp2) ->
-     separate space [ pp_clexp x; string "=";
-                      string (string_of_id f |> Util.green |> Util.clear) ^^ parens (separate_map (string ", ") pp_cval args);
-                      string ":"; pp_ctyp ctyp2 ]
-  | I_convert (x, ctyp1, y, ctyp2) ->
-     separate space [ pp_clexp x; colon; pp_ctyp ctyp1; string "=";
-                      pp_keyword "convert" ^^ pp_id y; colon; pp_ctyp ctyp2 ]
-  | I_copy (clexp, cval) ->
-     separate space [pp_clexp clexp; string "="; pp_cval cval]
-  | I_clear (ctyp, id) ->
-     pp_keyword "kill" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp
-  | I_return cval ->
-     pp_keyword "return" ^^ pp_cval cval
-  | I_throw cval ->
-     pp_keyword "throw" ^^ pp_cval cval
-  | I_comment str ->
-     string ("// " ^ str |> Util.magenta |> Util.clear)
-  | I_label str ->
-     string (str |> Util.blue |> Util.clear) ^^ string ":"
-  | I_goto str ->
-     pp_keyword "goto" ^^ string (str |> Util.blue |> Util.clear)
-  | I_match_failure ->
-     pp_keyword "match_failure"
-  | I_raw str ->
-     pp_keyword "C" ^^ string (str |> Util.cyan |> Util.clear)
-
-let pp_ctype_def = function
-  | CTD_enum (id, ids) ->
-     pp_keyword "enum" ^^ pp_id id ^^ string " = "
-     ^^ separate_map (string " | ") pp_id ids
-  | CTD_struct (id, fields) ->
-     pp_keyword "struct" ^^ pp_id id ^^ string " = "
-     ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) (fun (id, ctyp) -> pp_id id ^^ string " : " ^^ pp_ctyp ctyp) fields) rbrace
-  | CTD_variant (id, ctors) ->
-     pp_keyword "union" ^^ pp_id id ^^ string " = "
-     ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) (fun (id, ctyp) -> pp_id id ^^ string " : " ^^ pp_ctyp ctyp) ctors) rbrace
-
-let pp_cdef = function
-  | CDEF_spec (id, ctyps, ctyp) ->
-     pp_keyword "val" ^^ pp_id id ^^ string " : " ^^ parens (separate_map (comma ^^ space) pp_ctyp ctyps) ^^ string " -> " ^^ pp_ctyp ctyp
-     ^^ hardline
-  | CDEF_fundef (id, ret, args, instrs) ->
-     let ret = match ret with
-       | None -> empty
-       | Some id -> space ^^ pp_id id
-     in
-     pp_keyword "function" ^^ pp_id id ^^ ret ^^ parens (separate_map (comma ^^ space) pp_id args) ^^ space
-     ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace
-     ^^ hardline
-  | CDEF_reg_dec (id, ctyp) ->
-     pp_keyword "register" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp
-     ^^ hardline
-  | CDEF_type tdef -> pp_ctype_def tdef ^^ hardline
-  | CDEF_let (n, bindings, instrs, cleanup) ->
-     let pp_binding (id, ctyp) = pp_id id ^^ string " : " ^^ pp_ctyp ctyp in
-     pp_keyword "let" ^^ string (string_of_int n) ^^ parens (separate_map (comma ^^ space) pp_binding bindings) ^^ space
-     ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace ^^ space
-     ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr cleanup) rbrace ^^ space
-     ^^ hardline
-  | CDEF_startup (id, instrs)->
-     pp_keyword "startup" ^^ pp_id id ^^ space
-     ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace
-     ^^ hardline
-  | CDEF_finish (id, instrs)->
-     pp_keyword "finish" ^^ pp_id id ^^ space
-     ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace
-     ^^ hardline
-
 let is_ct_enum = function
   | CT_enum _ -> true
   | _ -> false
@@ -1589,18 +1381,6 @@ let compile_funcall l ctx id args typ =
       setup := iinit ctyp gs cval :: !setup;
       cleanup := iclear ctyp gs :: !cleanup;
       (F_id gs, ctyp)
-        (*
-    else if not (is_stack_ctyp have_ctyp) && is_stack_ctyp ctyp then
-      let gs1 = gensym () in
-      let gs2 = gensym () in
-      setup := idecl ctyp gs2 :: !setup;
-      setup := idecl have_ctyp gs1 :: !setup;
-      setup := ialloc have_ctyp gs1 :: !setup;
-      setup := icopy (CL_id gs1) cval :: !setup;
-      setup := iconvert (CL_id gs1) ctyp gs2 have_ctyp :: !setup;
-      cleanup := iclear have_ctyp gs1 :: !cleanup;
-      (F_id gs2, ctyp)
-         *)
     else
       c_error ~loc:l
         (Printf.sprintf "Failure when setting up function %s arguments: %s and %s." (string_of_id id) (string_of_ctyp have_ctyp) (string_of_ctyp ctyp))
@@ -1903,6 +1683,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      struct. Turned on by !optimize_struct_updates. *)
   | AE_assign (id, assign_typ, AE_aux (AE_record_update (AV_id (rid, _), fields, typ), _, _))
        when Id.compare id rid = 0 && !optimize_struct_updates ->
+     c_debug (lazy ("Optimizing struct update"));
      let compile_fields (field_id, aval) =
        let field_setup, cval, field_cleanup = compile_aval ctx aval in
        field_setup
@@ -2475,179 +2256,7 @@ let add_local_labels instrs =
   | _ -> assert false
 
 (**************************************************************************)
-(* 5. Dependency Graphs                                                   *)
-(**************************************************************************)
-
-type graph_node =
-  | G_id of id
-  | G_label of string
-  | G_instr of int * instr
-  | G_start
-
-let string_of_node = function
-  | G_id id -> string_of_id id
-  | 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_id id1, G_id id2 -> Id.compare id1 id2
-    | G_label str1, G_label str2 -> String.compare str1 str2
-    | G_instr (n1, _), G_instr (n2, _) -> compare n1 n2
-    | G_start  , _         -> 1
-    | _        , G_start   -> -1
-    | G_instr _, _         -> 1
-    | _        , G_instr _ -> -1
-    | G_id _   , _         -> 1
-    | _        , G_id _    -> -1
-end
-
-module NM = Map.Make(Node)
-module NS = Set.Make(Node)
-
-type dep_graph = NS.t NM.t
-
-let rec fragment_deps = function
-  | F_id id | F_ref id -> NS.singleton (G_id id)
-  | F_lit _ -> NS.empty
-  | F_field (frag, _) | F_unary (_, frag) -> fragment_deps frag
-  | F_call (_, frags) -> List.fold_left NS.union NS.empty (List.map fragment_deps frags)
-  | F_op (frag1, _, frag2) -> NS.union (fragment_deps frag1) (fragment_deps frag2)
-  | F_current_exception -> NS.empty
-  | F_have_exception -> NS.empty
-  | F_raw _ -> NS.empty
-
-let cval_deps = function (frag, _) -> fragment_deps frag
-
-let rec clexp_deps = function
-  | CL_id id -> NS.singleton (G_id id)
-  | CL_field (id, _) -> NS.singleton (G_id id)
-  | CL_addr id -> NS.singleton (G_id id)
-  | CL_have_exception -> NS.empty
-  | CL_current_exception -> NS.empty
-
-(** Return the direct, non program-order dependencies of a single
-   instruction **)
-let instr_deps = function
-  | I_decl (ctyp, id) -> NS.empty, NS.singleton (G_id id)
-  | I_alloc (ctyp, id) | I_reset (ctyp, id) -> NS.empty, NS.singleton (G_id id)
-  | I_init (ctyp, id, cval) | I_reinit (ctyp, id, cval) -> cval_deps cval, NS.singleton (G_id id)
-  | I_if (cval, _, _, _) -> cval_deps cval, NS.empty
-  | I_jump (cval, label) -> cval_deps cval, NS.singleton (G_label label)
-  | I_funcall (clexp, _, _, cvals, _) -> List.fold_left NS.union NS.empty (List.map cval_deps cvals), clexp_deps clexp
-  | I_convert (clexp, _, id, _) -> NS.singleton (G_id id), clexp_deps clexp
-  | I_copy (clexp, cval) -> cval_deps cval, clexp_deps clexp
-  | I_clear (_, id) -> NS.singleton (G_id id), NS.singleton (G_id id)
-  | I_throw cval | I_return cval -> cval_deps cval, NS.empty
-  | I_block _ | I_try_block _ -> NS.empty, NS.empty
-  | I_comment _ | I_raw _ -> NS.empty, NS.empty
-  | I_label label -> NS.singleton (G_label label), NS.empty
-  | I_goto label -> NS.empty, NS.singleton (G_label label)
-  | I_match_failure -> NS.empty, NS.empty
-
-let add_link from_node to_node graph =
-  try
-    NM.add from_node (NS.add to_node (NM.find from_node graph)) graph
-  with
-  | Not_found -> NM.add from_node (NS.singleton to_node) graph
-
-let leaves graph =
-  List.fold_left (fun acc (from_node, to_nodes) -> NS.filter (fun to_node -> Node.compare to_node from_node != 0) (NS.union acc to_nodes))
-                 NS.empty
-                 (NM.bindings graph)
-
-(* Ensure that all leaves exist in the graph *)
-let fix_leaves graph =
-  NS.fold (fun leaf graph -> if NM.mem leaf graph then graph else NM.add leaf NS.empty graph) (leaves graph) graph
-
-let instrs_graph instrs =
-  let icounter = ref 0 in
-  let graph = ref NM.empty in
-
-  let rec add_instr last_instr (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_instr instrs
-    | I_if (_, then_instrs, else_instrs, _) ->
-       begin
-         let inputs, _ = instr_deps instr in (* if has no outputs *)
-         graph := add_link last_instr node !graph;
-         NS.iter (fun input -> graph := add_link input node !graph) inputs;
-         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
-         graph := add_link n1 join !graph;
-         graph := add_link n2 join !graph;
-         join
-       end
-    | I_goto label ->
-       begin
-         let _, outputs = instr_deps instr in
-         graph := add_link last_instr node !graph;
-         NS.iter (fun output -> graph := add_link node output !graph) outputs;
-         incr icounter;
-         G_instr (!icounter, icomment "after goto")
-       end
-    | _ ->
-       begin
-         let inputs, outputs = instr_deps instr in
-         graph := add_link last_instr node !graph;
-         NS.iter (fun input -> graph := add_link input node !graph) inputs;
-         NS.iter (fun output -> graph := add_link node output !graph) outputs;
-         node
-       end
-  in
-  ignore (List.fold_left add_instr G_start instrs);
-  fix_leaves !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_id _                            -> "yellow"
-    | G_instr (_, I_aux (I_decl _, _))  -> "olivedrab1"
-    | G_instr (_, I_aux (I_init _, _))  -> "springgreen"
-    | G_instr (_, I_aux (I_alloc _, _)) -> "palegreen"
-    | 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 _                         -> "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"
-    | G_id _   , G_instr _ -> "blue3"
-    | G_instr _, G_id _    -> "red3"
-    | _        , _         -> "coral3"
-  in
-  let out_chan = open_out (Util.zencode_string (string_of_id id) ^ ".gv") in
-  output_string out_chan "digraph DEPS {\n";
-  let make_node from_node =
-    output_string out_chan (Printf.sprintf "  \"%s\" [fillcolor=%s;style=filled];\n" (to_string from_node) (node_color from_node))
-  in
-  let make_line from_node to_node =
-    output_string out_chan (Printf.sprintf "  \"%s\" -> \"%s\" [color=%s];\n" (to_string from_node) (to_string to_node) (edge_color from_node to_node))
-  in
-  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;
-  close_out out_chan
-
-(**************************************************************************)
-(* 6. Optimizations                                                       *)
+(* 5. Optimizations                                                       *)
 (**************************************************************************)
 
 let clexp_rename from_id to_id =
@@ -2656,6 +2265,7 @@ let clexp_rename from_id to_id =
   | CL_id id -> CL_id (rename id)
   | CL_field (id, field) -> CL_field (rename id, field)
   | CL_addr id -> CL_addr (rename id)
+  | CL_addr_field (id, field) -> CL_addr_field (rename id, field)
   | CL_current_exception -> CL_current_exception
   | CL_have_exception -> CL_have_exception
 
@@ -2799,21 +2409,78 @@ let flatten_instrs ctx =
 
   | cdef -> [cdef]
 
+(* When this optimization fires we know we have bytecode of the form
+
+   recreate x : S; x = y; ...
+
+   when this continues with x.A = a, x.B = b etc until y = x. Then
+   provided there are no further references to x we can eliminate
+   the variable x.
+
+   Must be called after hoist_allocations, otherwise does nothing. *)
+let fix_struct_updates ctx =
+  (* FIXME need to check no remaining references *)
+  let rec fix_updates struct_id id = function
+    | I_aux (I_copy (CL_field (struct_id', field), cval), aux) :: instrs
+         when Id.compare struct_id struct_id' = 0 ->
+       Util.option_map (fun instrs -> I_aux (I_copy (CL_field (id, field), cval), aux) :: instrs) (fix_updates struct_id id instrs)
+    | I_aux (I_copy (CL_id id', (F_id struct_id', ctyp)), aux) :: instrs
+         when Id.compare struct_id struct_id' = 0 && Id.compare id id' = 0->
+       Some instrs
+    | _ -> None
+  in
+  let rec fix_updates_ret struct_id id = function
+    | I_aux (I_copy (CL_field (struct_id', field), cval), aux) :: instrs
+         when Id.compare struct_id struct_id' = 0 ->
+       Util.option_map (fun instrs -> I_aux (I_copy (CL_addr_field (id, field), cval), aux) :: instrs) (fix_updates_ret struct_id id instrs)
+    | I_aux (I_copy (CL_addr id', (F_id struct_id', ctyp)), aux) :: instrs
+         when Id.compare struct_id struct_id' = 0 && Id.compare id id' = 0->
+       Some instrs
+    | _ -> None
+  in
+  let rec opt hr = function
+    | (I_aux (I_reset (ctyp, struct_id), _) as instr1)
+      :: (I_aux (I_copy (CL_id struct_id', (F_id id, ctyp')), _) as instr2)
+      :: instrs
+         when is_ct_struct ctyp && ctyp_equal ctyp ctyp' && Id.compare struct_id struct_id' = 0 ->
+       prerr_endline ("Potential struct update " ^ string_of_id struct_id);
+       begin match fix_updates struct_id id instrs with
+       | None -> instr1 :: instr2 :: opt hr instrs
+       | Some updated -> opt hr updated
+       end
+
+    | (I_aux (I_reset (ctyp, struct_id), _) as instr) :: instrs
+         when is_ct_struct ctyp && Util.is_some hr ->
+       let id = match hr with Some id -> id | None -> assert false in
+       prerr_endline ("Potential struct return " ^ string_of_id struct_id ^ " to " ^ string_of_id id);
+       begin match fix_updates_ret struct_id id instrs with
+       | None -> instr :: opt hr instrs
+       | Some updated -> opt hr updated
+       end
+
+    | I_aux (I_block block, aux) :: instrs -> I_aux (I_block (opt hr block), aux) :: opt hr instrs
+    | I_aux (I_try_block block, aux) :: instrs -> I_aux (I_try_block (opt hr block), aux) :: opt hr instrs
+    | I_aux (I_if (cval, then_instrs, else_instrs, ctyp), aux) :: instrs ->
+       I_aux (I_if (cval, opt hr then_instrs, opt hr else_instrs, ctyp), aux) :: opt hr instrs
+
+    | instr :: instrs -> instr :: opt hr instrs
+    | [] -> []
+  in
+  function
+  | CDEF_fundef (function_id, heap_return, args, body) ->
+     [CDEF_fundef (function_id, heap_return, args, opt heap_return body)]
+  | cdef -> [cdef]
+
 let concatMap f xs = List.concat (List.map f xs)
 
 let optimize ctx cdefs =
   let nothing cdefs = cdefs in
   cdefs
-  |> if !optimize_hoist_allocations then
-       begin
-         c_debug (lazy (Util.log_line __MODULE__ __LINE__ "Hoisting allocations"));
-         concatMap (hoist_allocations ctx)
-       end
-     else
-       nothing
+  |> (if !optimize_hoist_allocations then concatMap (hoist_allocations ctx) else nothing)
+  |> (if !optimize_struct_updates then concatMap (fix_struct_updates ctx) else nothing)
 
 (**************************************************************************)
-(* 7. Code generation                                                     *)
+(* 6. Code generation                                                     *)
 (**************************************************************************)
 
 let sgen_id id = Util.zencode_string (string_of_id id)
@@ -2873,6 +2540,7 @@ let sgen_clexp = function
   | CL_id id -> "&" ^ sgen_id id
   | CL_field (id, field) -> "&(" ^ sgen_id id ^ "." ^ Util.zencode_string field ^ ")"
   | CL_addr id -> sgen_id id
+  | CL_addr_field (id, field) -> "&(" ^ sgen_id id ^ "->" ^ Util.zencode_string field ^ ")"
   | CL_have_exception -> "have_exception"
   | CL_current_exception -> "current_exception"
 
@@ -2880,6 +2548,7 @@ let sgen_clexp_pure = function
   | CL_id id -> sgen_id id
   | CL_field (id, field) -> sgen_id id ^ "." ^ Util.zencode_string field
   | CL_addr id -> sgen_id id
+  | CL_addr_field (id, field) -> sgen_id id ^ "->" ^ Util.zencode_string field
   | CL_have_exception -> "have_exception"
   | CL_current_exception -> "current_exception"
 
@@ -3574,7 +3243,6 @@ let rec get_recursive_functions (Defs defs) =
   | _ :: defs -> get_recursive_functions (Defs defs)
   | [] -> IdSet.empty
 
-
 let compile_ast ctx (Defs defs) =
   try
     c_debug (lazy (Util.log_line __MODULE__ __LINE__ "Identifying recursive functions"));
diff --git a/src/isail.ml b/src/isail.ml
index 414fc50d..514b8763 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -275,7 +275,7 @@ let handle_input' input =
             let byte_ast = bytecode_ast ctx (fun cdefs -> List.concat (List.map (flatten_instrs ctx) cdefs)) ast in
             let chan = open_out arg in
             Util.opt_colors := false;
-            Pretty_print_sail.pretty_sail chan (separate_map hardline pp_cdef byte_ast);
+            Pretty_print_sail.pretty_sail chan (separate_map hardline Bytecode_util.pp_cdef byte_ast);
             Util.opt_colors := true;
             close_out chan
          | ":ast" ->