C: Refactor C backend

Main change is splitting apart the Sail->IR compilation stage and the
C code generation and optimization phase. Rather than variously
calling the intermediate language either bytecode (when it's not
really) or simply IR, we give it a name: Jib (a type of Sail). Most of
the types are still prefixed by c/C, and I don't think it's worth
changing this.

The various parts of the C backend are now in the src/jib/ subdirectory

src/jib/anf.ml         - Sail->ANF translation
src/jib/jib_util.ml    - various Jib AST processing and helper functions (formerly bytecode_util)
src/jib/jib_compile.ml - Sail->Jib translation (using Sail->ANF)
src/jib/c_backend.ml   - Jib->C code generator and optimizations

Further, bytecode.ott is now jib.ott and generates jib.ml (which still
lives in src/ for now)

The optimizations in c_backend.ml should eventually be moved in a
separate jib_optimization file.

The Sail->Jib compilation can be parameterised by two functions - one
is a custom ANF->ANF optimization pass that can be specified on a per
Jib backend basis, and the other is the rule for translating Sail
types in Jib types. This can be more or less precise depending on how
precise we want to be about bit-widths etc, i.e. we only care about <64
and >64 for C, but for SMT generation we would want to be as precise
as possible.

Additional improvements:

The Jib IR is now agnostic about whether arguments are allocated on
the heap vs the stack and this is handled by the C code generator.

jib.ott now has some more comments explaining various parts of the Jib
AST.

A Set module and comparison function for ctyps is defined, and some
functions now return ctyp sets rather than lists to avoid repeated
work.

1 files changed, 0 insertions, 771 deletions

diff --git a/src/bytecode_util.ml b/src/bytecode_util.ml
deleted file mode 100644
index 630d2a48..00000000
--- a/src/bytecode_util.ml
+++ /dev/null
@@ -1,771 +0,0 @@
-(**************************************************************************)
-(*     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 ireset ?loc:(l=Parse_ast.Unknown) ctyp id =
-  I_aux (I_reset (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 =
-  I_aux (I_funcall (clexp, false, id, cvals), (instr_number (), l))
-
-let iextern ?loc:(l=Parse_ast.Unknown) clexp id cvals =
-  I_aux (I_funcall (clexp, true, id, cvals), (instr_number (), l))
-
-let icopy l clexp cval =
-  I_aux (I_copy (clexp, cval), (instr_number (), l))
-
-let ialias l clexp cval =
-  I_aux (I_alias (clexp, cval), (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 iundefined ?loc:(l=Parse_ast.Unknown) ctyp =
-  I_aux (I_undefined ctyp, (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 rec frag_rename from_id to_id = function
-  | F_id id when Id.compare id from_id = 0 -> F_id to_id
-  | F_id id -> F_id id
-  | F_ref id when Id.compare id from_id = 0 -> F_ref to_id
-  | F_ref id -> F_ref id
-  | F_lit v -> F_lit v
-  | F_have_exception -> F_have_exception
-  | F_current_exception -> F_current_exception
-  | F_call (call, frags) -> F_call (call, List.map (frag_rename from_id to_id) frags)
-  | F_op (f1, op, f2) -> F_op (frag_rename from_id to_id f1, op, frag_rename from_id to_id f2)
-  | F_unary (op, f) -> F_unary (op, frag_rename from_id to_id f)
-  | F_field (f, field) -> F_field (frag_rename from_id to_id f, field)
-  | F_raw raw -> F_raw raw
-  | F_poly f -> F_poly (frag_rename from_id to_id f)
-
-let cval_rename from_id to_id (frag, ctyp) = (frag_rename from_id to_id frag, ctyp)
-
-let rec clexp_rename from_id to_id = function
-  | CL_id (id, ctyp) when Id.compare id from_id = 0 -> CL_id (to_id, ctyp)
-  | CL_id (id, ctyp) -> CL_id (id, ctyp)
-  | CL_field (clexp, field) ->
-     CL_field (clexp_rename from_id to_id clexp, field)
-  | CL_addr clexp ->
-     CL_addr (clexp_rename from_id to_id clexp)
-  | CL_tuple (clexp, n) ->
-     CL_tuple (clexp_rename from_id to_id clexp, n)
-  | CL_current_exception ctyp -> CL_current_exception ctyp
-  | CL_have_exception -> CL_have_exception
-
-let rec instr_rename from_id to_id (I_aux (instr, aux)) =
-  let instr = match instr with
-    | I_decl (ctyp, id) when Id.compare id from_id = 0 -> I_decl (ctyp, to_id)
-    | I_decl (ctyp, id) -> I_decl (ctyp, id)
-
-    | I_init (ctyp, id, cval) when Id.compare id from_id = 0 ->
-       I_init (ctyp, to_id, cval_rename from_id to_id cval)
-    | I_init (ctyp, id, cval) ->
-       I_init (ctyp, id, cval_rename from_id to_id cval)
-
-    | I_if (cval, then_instrs, else_instrs, ctyp2) ->
-       I_if (cval_rename from_id to_id cval,
-             List.map (instr_rename from_id to_id) then_instrs,
-             List.map (instr_rename from_id to_id) else_instrs,
-             ctyp2)
-
-    | I_jump (cval, label) -> I_jump (cval_rename from_id to_id cval, label)
-
-    | I_funcall (clexp, extern, id, args) ->
-       I_funcall (clexp_rename from_id to_id clexp, extern, id, List.map (cval_rename from_id to_id) args)
-
-    | I_copy (clexp, cval) -> I_copy (clexp_rename from_id to_id clexp, cval_rename from_id to_id cval)
-    | I_alias (clexp, cval) -> I_alias (clexp_rename from_id to_id clexp, cval_rename from_id to_id cval)
-
-    | I_clear (ctyp, id) when Id.compare id from_id = 0 -> I_clear (ctyp, to_id)
-    | I_clear (ctyp, id) -> I_clear (ctyp, id)
-
-    | I_return cval -> I_return (cval_rename from_id to_id cval)
-
-    | I_block instrs -> I_block (List.map (instr_rename from_id to_id) instrs)
-
-    | I_try_block instrs -> I_try_block (List.map (instr_rename from_id to_id) instrs)
-
-    | I_throw cval -> I_throw (cval_rename from_id to_id cval)
-
-    | I_comment str -> I_comment str
-
-    | I_raw str -> I_raw str
-
-    | I_label label -> I_label label
-
-    | I_goto label -> I_goto label
-
-    | I_undefined ctyp -> I_undefined ctyp
-
-    | I_match_failure -> I_match_failure
-
-    | I_reset (ctyp, id) when Id.compare id from_id = 0 -> I_reset (ctyp, to_id)
-    | I_reset (ctyp, id) -> I_reset (ctyp, id)
-
-    | I_reinit (ctyp, id, cval) when Id.compare id from_id = 0 ->
-       I_reinit (ctyp, to_id, cval_rename from_id to_id cval)
-    | I_reinit (ctyp, id, cval) ->
-       I_reinit (ctyp, id, cval_rename from_id to_id cval)
-  in
-  I_aux (instr, aux)
-
-(**************************************************************************)
-(* 1. Instruction pretty printer                                          *)
-(**************************************************************************)
-
-let string_of_value = function
-  | V_bits [] -> "UINT64_C(0)"
-  | V_bits bs -> "UINT64_C(" ^ Sail2_values.show_bitlist bs ^ ")"
-  | 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 Sail2_values.B0 -> "UINT64_C(0)"
-  | V_bit Sail2_values.B1 -> "UINT64_C(1)"
-  | 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
-  | F_poly f -> string_of_fragment ~zencode:zencode f
-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. *)
-and string_of_ctyp = function
-  | CT_lint -> "int"
-  | CT_lbits true -> "lbits(dec)"
-  | CT_lbits false -> "lbits(inc)"
-  | CT_fbits (n, true) -> "fbits(" ^ string_of_int n ^ ", dec)"
-  | CT_fbits (n, false) -> "fbits(" ^ string_of_int n ^ ", int)"
-  | CT_sbits true -> "sbits(dec)"
-  | CT_sbits false -> "sbits(inc)"
-  | CT_fint n -> "int(" ^ string_of_int n ^ ")"
-  | 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 ^ ")"
-  | CT_poly -> "*"
-
-(** This function is like string_of_ctyp, but recursively prints all
-   constructors in variants and structs. Used for debug output. *)
-and full_string_of_ctyp = function
-  | CT_lint -> "int"
-  | CT_lbits true -> "lbits(dec)"
-  | CT_lbits false -> "lbits(inc)"
-  | CT_fbits (n, true) -> "fbits(" ^ string_of_int n ^ ", dec)"
-  | CT_fbits (n, false) -> "fbits(" ^ string_of_int n ^ ", int)"
-  | CT_sbits true -> "sbits(dec)"
-  | CT_sbits false -> "sbits(inc)"
-  | CT_fint n -> "int(" ^ string_of_int n ^ ")"
-  | CT_bit -> "bit"
-  | CT_unit -> "unit"
-  | CT_bool -> "bool"
-  | CT_real -> "real"
-  | CT_tup ctyps -> "(" ^ Util.string_of_list ", " full_string_of_ctyp ctyps ^ ")"
-  | CT_enum (id, _) -> string_of_id id
-  | CT_struct (id, ctors) | CT_variant (id, ctors) ->
-     "struct " ^ string_of_id id
-     ^ "{ "
-     ^ Util.string_of_list ", " (fun (id, ctyp) -> string_of_id id ^ " : " ^ full_string_of_ctyp ctyp) ctors
-     ^ "}"
-  | CT_string -> "string"
-  | CT_vector (true, ctyp) -> "vector(dec, " ^ full_string_of_ctyp ctyp ^ ")"
-  | CT_vector (false, ctyp) -> "vector(inc, " ^ full_string_of_ctyp ctyp ^ ")"
-  | CT_list ctyp -> "list(" ^ full_string_of_ctyp ctyp ^ ")"
-  | CT_ref ctyp -> "ref(" ^ full_string_of_ctyp ctyp ^ ")"
-  | CT_poly -> "*"
-
-let rec map_ctyp f = function
-  | (CT_lint | CT_fint _ | CT_lbits _ | CT_fbits _ | CT_sbits _
-     | CT_bit | CT_unit | CT_bool | CT_real | CT_string | CT_poly | CT_enum _) as ctyp -> f ctyp
-  | CT_tup ctyps -> f (CT_tup (List.map (map_ctyp f) ctyps))
-  | CT_ref ctyp -> f (CT_ref (map_ctyp f ctyp))
-  | CT_vector (direction, ctyp) -> f (CT_vector (direction, map_ctyp f ctyp))
-  | CT_list ctyp -> f (CT_list (map_ctyp f ctyp))
-  | CT_struct (id, ctors) -> f (CT_struct (id, List.map (fun (id, ctyp) -> id, map_ctyp f ctyp) ctors))
-  | CT_variant (id, ctors) -> f (CT_variant (id, List.map (fun (id, ctyp) -> id, map_ctyp f ctyp) ctors))
-
-let rec ctyp_equal ctyp1 ctyp2 =
-  match ctyp1, ctyp2 with
-  | CT_lint, CT_lint -> true
-  | CT_lbits d1, CT_lbits d2 -> d1 = d2
-  | CT_sbits d1, CT_sbits d2 -> d1 = d2
-  | CT_fbits (m1, d1), CT_fbits (m2, d2) -> m1 = m2 && d1 = d2
-  | CT_bit, CT_bit -> true
-  | CT_fint n, CT_fint m -> n = m
-  | CT_unit, CT_unit -> true
-  | CT_bool, CT_bool -> true
-  | CT_struct (id1, _), CT_struct (id2, _) -> Id.compare id1 id2 = 0
-  | CT_enum (id1, _), CT_enum (id2, _) -> Id.compare id1 id2 = 0
-  | CT_variant (id1, _), CT_variant (id2, _) -> Id.compare id1 id2 = 0
-  | CT_tup ctyps1, CT_tup ctyps2 when List.length ctyps1 = List.length ctyps2 ->
-     List.for_all2 ctyp_equal ctyps1 ctyps2
-  | CT_string, CT_string -> true
-  | CT_real, CT_real -> true
-  | CT_vector (d1, ctyp1), CT_vector (d2, ctyp2) -> d1 = d2 && ctyp_equal ctyp1 ctyp2
-  | CT_list ctyp1, CT_list ctyp2 -> ctyp_equal ctyp1 ctyp2
-  | CT_ref ctyp1, CT_ref ctyp2 -> ctyp_equal ctyp1 ctyp2
-  | CT_poly, CT_poly -> true
-  | _, _ -> false
-
-let rec ctyp_unify ctyp1 ctyp2 =
-  match ctyp1, ctyp2 with
-  | CT_tup ctyps1, CT_tup ctyps2 when List.length ctyps1 = List.length ctyps2 ->
-     List.concat (List.map2 ctyp_unify ctyps1 ctyps2)
-
-  | CT_vector (b1, ctyp1), CT_vector (b2, ctyp2) when b1 = b2 ->
-     ctyp_unify ctyp1 ctyp2
-
-  | CT_list ctyp1, CT_list ctyp2 -> ctyp_unify ctyp1 ctyp2
-
-  | CT_ref ctyp1, CT_ref ctyp2 -> ctyp_unify ctyp1 ctyp2
-
-  | CT_poly, _ -> [ctyp2]
-
-  | _, _ when ctyp_equal ctyp1 ctyp2 -> []
-  | _, _ -> raise (Invalid_argument "ctyp_unify")
-
-let rec ctyp_suprema = function
-  | CT_lint -> CT_lint
-  | CT_lbits d -> CT_lbits d
-  | CT_fbits (_, d) -> CT_lbits d
-  | CT_sbits d -> CT_lbits d
-  | CT_fint _ -> CT_lint
-  | CT_unit -> CT_unit
-  | CT_bool -> CT_bool
-  | CT_real -> CT_real
-  | CT_bit -> CT_bit
-  | CT_tup ctyps -> CT_tup (List.map ctyp_suprema ctyps)
-  | CT_string -> CT_string
-  | CT_enum (id, ids) -> CT_enum (id, ids)
-  (* Do we really never want to never call ctyp_suprema on constructor
-     fields?  Doing it causes issues for structs (see
-     test/c/stack_struct.sail) but it might be wrong to not call it
-     for nested variants... *)
-  | CT_struct (id, ctors) -> CT_struct (id, ctors)
-  | CT_variant (id, ctors) -> CT_variant (id, ctors)
-  | CT_vector (d, ctyp) -> CT_vector (d, ctyp_suprema ctyp)
-  | CT_list ctyp -> CT_list (ctyp_suprema ctyp)
-  | CT_ref ctyp -> CT_ref (ctyp_suprema ctyp)
-  | CT_poly -> CT_poly
-
-let rec ctyp_ids = function
-  | CT_enum (id, _) -> IdSet.singleton id
-  | CT_struct (id, ctors) | CT_variant (id, ctors) ->
-     IdSet.add id (List.fold_left (fun ids (_, ctyp) -> IdSet.union (ctyp_ids ctyp) ids) IdSet.empty ctors)
-  | CT_tup ctyps -> List.fold_left (fun ids ctyp -> IdSet.union (ctyp_ids ctyp) ids) IdSet.empty ctyps
-  | CT_vector (_, ctyp) | CT_list ctyp | CT_ref ctyp -> ctyp_ids ctyp
-  | CT_lint | CT_fint _ | CT_lbits _ | CT_fbits _ | CT_sbits _ | CT_unit
-    | CT_bool | CT_real | CT_bit | CT_string | CT_poly -> IdSet.empty
-
-let rec unpoly = function
-  | F_poly f -> unpoly f
-  | F_call (call, fs) -> F_call (call, List.map unpoly fs)
-  | F_field (f, field) -> F_field (unpoly f, field)
-  | F_op (f1, op, f2) -> F_op (unpoly f1, op, unpoly f2)
-  | F_unary (op, f) -> F_unary (op, unpoly f)
-  | f -> f
-
-let rec is_polymorphic = function
-  | CT_lint | CT_fint _ | CT_lbits _ | CT_fbits _ | CT_sbits _ | CT_bit | CT_unit | CT_bool | CT_real | CT_string -> false
-  | CT_tup ctyps -> List.exists is_polymorphic ctyps
-  | CT_enum _ -> false
-  | CT_struct (_, ctors) | CT_variant (_, ctors) -> List.exists (fun (_, ctyp) -> is_polymorphic ctyp) ctors
-  | CT_vector (_, ctyp) | CT_list ctyp | CT_ref ctyp -> is_polymorphic ctyp
-  | CT_poly -> true
-
-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, ctyp) -> pp_id id ^^ string " : " ^^ pp_ctyp ctyp
-  | CL_field (clexp, field) -> parens (pp_clexp clexp) ^^ string "." ^^ string field
-  | CL_tuple (clexp, n) -> parens (pp_clexp clexp) ^^ string "." ^^ string (string_of_int n)
-  | CL_addr clexp -> string "*" ^^ pp_clexp clexp
-  | CL_current_exception ctyp -> string "current_exception : " ^^ pp_ctyp ctyp
-  | 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_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) ->
-     separate space [ pp_clexp x; string "=";
-                      string (string_of_id f |> Util.green |> Util.clear) ^^ parens (separate_map (string ", ") pp_cval args) ]
-  | I_copy (clexp, cval) ->
-     separate space [pp_clexp clexp; string "="; pp_cval cval]
-  | I_alias (clexp, cval) ->
-     pp_keyword "alias" ^^ 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_undefined ctyp ->
-     pp_keyword "undefined" ^^ pp_ctyp ctyp
-  | 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, instrs) ->
-     pp_keyword "register" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp ^^ space
-     ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace
-     ^^ hardline
-  | CDEF_type tdef -> pp_ctype_def tdef ^^ hardline
-  | CDEF_let (n, bindings, instrs) ->
-     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
-     ^^ 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_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
-  | F_field (frag, _) | F_unary (_, frag) | F_poly frag -> fragment_deps frag
-  | F_call (_, frags) -> List.fold_left IdSet.union IdSet.empty (List.map fragment_deps frags)
-  | F_op (frag1, _, frag2) -> IdSet.union (fragment_deps frag1) (fragment_deps frag2)
-  | F_current_exception -> IdSet.empty
-  | F_have_exception -> IdSet.empty
-  | F_raw _ -> IdSet.empty
-
-let cval_deps = function (frag, _) -> fragment_deps frag
-
-let rec clexp_deps = function
-  | CL_id (id, _) -> IdSet.singleton id
-  | CL_field (clexp, _) -> clexp_deps clexp
-  | CL_tuple (clexp, _) -> clexp_deps clexp
-  | CL_addr clexp -> clexp_deps clexp
-  | CL_have_exception -> IdSet.empty
-  | CL_current_exception _ -> IdSet.empty
-
-(* Return the direct, read/write dependencies of a single instruction *)
-let instr_deps = function
-  | I_decl (ctyp, id) -> IdSet.empty, IdSet.singleton id
-  | I_reset (ctyp, id) -> IdSet.empty, IdSet.singleton id
-  | I_init (ctyp, id, cval) | I_reinit (ctyp, id, cval) -> cval_deps cval, IdSet.singleton id
-  | I_if (cval, _, _, _) -> cval_deps cval, IdSet.empty
-  | I_jump (cval, label) -> cval_deps cval, IdSet.empty
-  | 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_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
-  | I_label label -> IdSet.empty, IdSet.empty
-  | I_goto label -> IdSet.empty, IdSet.empty
-  | I_undefined _ -> IdSet.empty, IdSet.empty
-  | I_match_failure -> 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)
-  | CL_tuple (clexp, n) -> CL_tuple (map_clexp_ctyp f clexp, n)
-  | CL_addr clexp -> CL_addr (map_clexp_ctyp f clexp)
-  | CL_current_exception ctyp -> CL_current_exception (f ctyp)
-  | CL_have_exception -> CL_have_exception
-
-let rec map_instr_ctyp f (I_aux (instr, aux)) =
-  let instr = match instr with
-    | I_decl (ctyp, id) -> I_decl (f ctyp, id)
-    | I_init (ctyp1, id, (frag, ctyp2)) -> I_init (f ctyp1, id, (frag, f ctyp2))
-    | I_if ((frag, ctyp1), then_instrs, else_instrs, ctyp2) ->
-       I_if ((frag, f ctyp1), List.map (map_instr_ctyp f) then_instrs, List.map (map_instr_ctyp f) else_instrs, f ctyp2)
-    | I_jump ((frag, ctyp), label) -> I_jump ((frag, f ctyp), label)
-    | I_funcall (clexp, extern, id, cvals) ->
-       I_funcall (map_clexp_ctyp f clexp, extern, id, List.map (fun (frag, ctyp) -> frag, f ctyp) cvals)
-    | I_copy (clexp, (frag, ctyp)) -> I_copy (map_clexp_ctyp f clexp, (frag, f ctyp))
-    | I_alias (clexp, (frag, ctyp)) -> I_alias (map_clexp_ctyp f clexp, (frag, f ctyp))
-    | I_clear (ctyp, id) -> I_clear (f ctyp, id)
-    | I_return (frag, ctyp) -> I_return (frag, f ctyp)
-    | I_block instrs -> I_block (List.map (map_instr_ctyp f) instrs)
-    | I_try_block instrs -> I_try_block (List.map (map_instr_ctyp f) instrs)
-    | I_throw (frag, ctyp) -> I_throw (frag, f ctyp)
-    | I_undefined ctyp -> I_undefined (f ctyp)
-    | I_reset (ctyp, id) -> I_reset (f ctyp, id)
-    | I_reinit (ctyp1, id, (frag, ctyp2)) -> I_reinit (f ctyp1, id, (frag, f ctyp2))
-    | (I_comment _ | I_raw _ | I_label _ | I_goto _ | I_match_failure) as instr -> instr
-  in
-  I_aux (instr, aux)
-
-(** Map over each instruction within an instruction, bottom-up *)
-let rec map_instr f (I_aux (instr, aux)) =
-  let instr = 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 _ -> instr
-    | I_if (cval, instrs1, instrs2, ctyp) ->
-       I_if (cval, List.map (map_instr f) instrs1, List.map (map_instr f) instrs2, ctyp)
-    | I_block instrs ->
-       I_block (List.map (map_instr f) instrs)
-    | I_try_block instrs ->
-       I_try_block (List.map (map_instr f) instrs)
-  in
-  f (I_aux (instr, aux))
-
-(** 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)
-  | CDEF_let (n, bindings, instrs) -> CDEF_let (n, bindings, List.map (map_instr f) instrs)
-  | CDEF_fundef (id, heap_return, args, instrs) -> CDEF_fundef (id, heap_return, args, List.map (map_instr f) instrs)
-  | CDEF_startup (id, instrs) -> CDEF_startup (id, List.map (map_instr f) instrs)
-  | CDEF_finish (id, instrs) -> CDEF_finish (id, List.map (map_instr f) instrs)
-  | CDEF_spec (id, ctyps, ctyp) -> CDEF_spec (id, ctyps, ctyp)
-  | CDEF_type tdef -> CDEF_type tdef
-
-let ctype_def_map_ctyp f = function
-  | CTD_enum (id, ids) -> CTD_enum (id, ids)
-  | CTD_struct (id, ctors) -> CTD_struct (id, List.map (fun (field, ctyp) -> (field, f ctyp)) ctors)
-  | CTD_variant (id, ctors) -> CTD_variant (id, List.map (fun (field, ctyp) -> (field, f ctyp)) ctors)
-
-(** Map over each ctyp in a cdef using map_instr_ctyp *)
-let cdef_map_ctyp f = function
-  | CDEF_reg_dec (id, ctyp, instrs) -> CDEF_reg_dec (id, f ctyp, List.map (map_instr_ctyp f) instrs)
-  | CDEF_let (n, bindings, instrs) -> CDEF_let (n, bindings, List.map (map_instr_ctyp f) instrs)
-  | CDEF_fundef (id, heap_return, args, instrs) -> CDEF_fundef (id, heap_return, args, List.map (map_instr_ctyp f) instrs)
-  | CDEF_startup (id, instrs) -> CDEF_startup (id, List.map (map_instr_ctyp f) instrs)
-  | CDEF_finish (id, instrs) -> CDEF_finish (id, List.map (map_instr_ctyp f) instrs)
-  | CDEF_spec (id, ctyps, ctyp) -> CDEF_spec (id, List.map f ctyps, f ctyp)
-  | CDEF_type tdef -> CDEF_type (ctype_def_map_ctyp f tdef)
-
-(* Map over all sequences of instructions contained within an instruction *)
-let rec map_instrs f (I_aux (instr, aux)) =
-  let instr = match instr with
-    | I_decl _ | I_init _ | I_reset _ | I_reinit _ -> instr
-    | I_if (cval, instrs1, instrs2, ctyp) ->
-       I_if (cval, f (List.map (map_instrs f) instrs1), f (List.map (map_instrs f) instrs2), ctyp)
-    | I_funcall _ | I_copy _ | I_alias _ | I_clear _ | I_jump _ | I_throw _ | I_return _ -> instr
-    | I_block instrs -> I_block (f (List.map (map_instrs f) instrs))
-    | I_try_block instrs -> I_try_block (f (List.map (map_instrs f) instrs))
-    | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_match_failure | I_undefined _ -> instr
-  in
-  I_aux (instr, aux)
-
-let rec instr_ids (I_aux (instr, _)) =
-  let reads, writes = instr_deps instr in
-  IdSet.of_list (IdSet.elements reads @ IdSet.elements writes)
-
-let rec instr_reads (I_aux (instr, _)) =
-  let reads, _ = instr_deps instr in
-  IdSet.of_list (IdSet.elements reads)
-
-let rec instr_writes (I_aux (instr, _)) =
-  let _, writes = instr_deps instr in
-  IdSet.of_list (IdSet.elements writes)
-
-let rec filter_instrs f instrs =
-  let filter_instrs' = function
-    | I_aux (I_block instrs, aux) -> I_aux (I_block (filter_instrs f instrs), aux)
-    | I_aux (I_try_block instrs, aux) -> I_aux (I_try_block (filter_instrs f instrs), aux)
-    | I_aux (I_if (cval, instrs1, instrs2, ctyp), aux) ->
-       I_aux (I_if (cval, filter_instrs f instrs1, filter_instrs f instrs2, ctyp), aux)
-    | instr -> instr
-  in
-  List.filter f (List.map filter_instrs' instrs)