Refactor C backend, and split RTS into multiple files

9 files changed, 1213 insertions, 1330 deletions

diff --git a/language/bytecode.ott b/language/bytecode.ott
index 704bda83..bcd7b5b0 100644
--- a/language/bytecode.ott
+++ b/language/bytecode.ott
@@ -65,11 +65,11 @@ fragment :: 'F_' ::=
 
 ctyp :: 'CT_' ::=
   {{ com C type }}
-  | mpz_t                   :: :: mpz
+  | mpz_t                   :: :: int
 % Arbitrary precision GMP integer, mpz_t in C. }}
-  | bv_t ( bool )           :: :: bv
+  | bv_t ( bool )           :: :: bits
 % Variable length bitvector - flag represents direction, true - dec or false - inc }}
-  | 'uint64_t' ( nat , bool ) :: :: uint64
+  | 'uint64_t' ( nat , bool ) :: :: bits64
 % Fixed length bitvector that fits within a 64-bit word. - int
 % represents length, and flag is the same as CT_bv. }}
   | 'int64_t'               :: :: int64
diff --git a/lib/rts.c b/lib/rts.c
new file mode 100644
index 00000000..b098ae0e
--- /dev/null
+++ b/lib/rts.c
@@ -0,0 +1,275 @@
+#include<string.h>
+
+#include"sail.h"
+#include"rts.h"
+
+void sail_match_failure(sail_string msg)
+{
+  fprintf(stderr, "Pattern match failure in %s\n", msg);
+  exit(EXIT_FAILURE);
+}
+
+unit sail_assert(bool b, sail_string msg)
+{
+  if (b) return UNIT;
+  fprintf(stderr, "Assertion failed: %s\n", msg);
+  exit(EXIT_FAILURE);
+}
+
+/* ***** Sail memory builtins ***** */
+
+/*
+ * We organise memory available to the sail model into a linked list
+ * of dynamically allocated MASK + 1 size blocks.
+ */
+struct block {
+  uint64_t block_id;
+  uint8_t *mem;
+  struct block *next;
+};
+
+struct block *sail_memory = NULL;
+
+/*
+ * Must be one less than a power of two.
+ */
+uint64_t MASK = 0xFFFFFFul;
+
+/*
+ * All sail vectors are at least 64-bits, but only the bottom 8 bits
+ * are used in the second argument.
+ */
+void write_mem(uint64_t address, uint64_t byte)
+{
+  //printf("ADDR: %lu, BYTE: %lu\n", address, byte);
+
+  uint64_t mask = address & ~MASK;
+  uint64_t offset = address & MASK;
+
+  struct block *current = sail_memory;
+
+  while (current != NULL) {
+    if (current->block_id == mask) {
+      current->mem[offset] = (uint8_t) byte;
+      return;
+    } else {
+      current = current->next;
+    }
+  }
+
+  /* 
+   * If we couldn't find a block matching the mask, allocate a new
+   * one, write the byte, and put it at the front of the block list.
+   */
+  fprintf(stderr, "[Sail] Allocating new block 0x%" PRIx64 "\n", mask);
+  struct block *new_block = malloc(sizeof(struct block));
+  new_block->block_id = mask;
+  new_block->mem = calloc(MASK + 1, sizeof(uint8_t));
+  new_block->mem[offset] = (uint8_t) byte;
+  new_block->next = sail_memory;
+  sail_memory = new_block;
+}
+
+uint64_t read_mem(uint64_t address)
+{
+  uint64_t mask = address & ~MASK;
+  uint64_t offset = address & MASK;
+
+  struct block *current = sail_memory;
+
+  while (current != NULL) {
+    if (current->block_id == mask) {
+      return (uint64_t) current->mem[offset];
+    } else {
+      current = current->next;
+    }
+  }
+
+  return 0x00;
+}
+
+void kill_mem()
+{
+  while (sail_memory != NULL) {
+    struct block *next = sail_memory->next;
+
+    free(sail_memory->mem);
+    free(sail_memory);
+
+    sail_memory = next;
+  }
+}
+
+// ***** Memory builtins *****
+
+unit write_ram(const mpz_t addr_size,     // Either 32 or 64
+	       const mpz_t data_size_mpz, // Number of bytes
+	       const sail_bits  hex_ram,       // Currently unused
+	       const sail_bits  addr_bv,
+	       const sail_bits  data)
+{
+  uint64_t addr = mpz_get_ui(*addr_bv.bits);
+  uint64_t data_size = mpz_get_ui(data_size_mpz);
+
+  mpz_t buf;
+  mpz_init_set(buf, *data.bits);
+
+  uint64_t byte;
+  for(uint64_t i = 0; i < data_size; ++i) {
+    // Take the 8 low bits of buf and write to addr.
+    byte = mpz_get_ui(buf) & 0xFF;
+    write_mem(addr + i, byte);
+
+    // Then shift buf 8 bits right.
+    mpz_fdiv_q_2exp(buf, buf, 8);
+  }
+
+  mpz_clear(buf);
+  return UNIT;
+}
+
+void read_ram(sail_bits *data,
+	      const mpz_t addr_size,
+	      const mpz_t data_size_mpz,
+	      const sail_bits hex_ram,
+	      const sail_bits addr_bv)
+{
+  uint64_t addr = mpz_get_ui(*addr_bv.bits);
+  uint64_t data_size = mpz_get_ui(data_size_mpz);
+
+  mpz_set_ui(*data->bits, 0);
+  data->len = data_size * 8;
+
+  mpz_t byte;
+  mpz_init(byte);
+  for(uint64_t i = data_size; i > 0; --i) {
+    mpz_set_ui(byte, read_mem(addr + (i - 1)));
+    mpz_mul_2exp(*data->bits, *data->bits, 8);
+    mpz_add(*data->bits, *data->bits, byte);
+  }
+
+  mpz_clear(byte);
+}
+
+void load_image(char *file) {
+  FILE *fp = fopen(file, "r");
+
+  if (!fp) {
+    fprintf(stderr, "Image file %s could not be loaded\n", file);
+    exit(EXIT_FAILURE);
+  }
+
+  char *addr = NULL;
+  char *data = NULL;
+  size_t len = 0;
+
+  while (true) {
+    ssize_t addr_len = getline(&addr, &len, fp);
+    if (addr_len == -1) break;
+    ssize_t data_len = getline(&data, &len, fp);
+    if (data_len == -1) break;
+
+    if (!strcmp(addr, "elf_entry\n")) {
+      if (sscanf(data, "%" PRIu64 "\n", &g_elf_entry) != 1) {
+        fprintf(stderr, "Failed to parse elf_entry\n");
+        exit(EXIT_FAILURE);
+      };
+      printf("Elf entry point: %" PRIx64 "\n", g_elf_entry);
+    } else {
+      write_mem((uint64_t) atoll(addr), (uint64_t) atoll(data));
+    }
+  }
+
+  free(addr);
+  free(data);
+  fclose(fp);
+}
+
+// ***** Tracing support *****
+
+unit enable_tracing(const unit u)
+{
+  g_trace_depth = 0;
+  g_trace_enabled = true;
+  return UNIT;
+}
+
+unit disable_tracing(const unit u)
+{
+  g_trace_depth = 0;
+  g_trace_enabled = false;
+  return UNIT;
+}
+
+void trace_uint64_t(const uint64_t x) {
+  if (g_trace_enabled) fprintf(stderr, "0x%" PRIx64, x);
+}
+
+void trace_unit(const unit u) {
+  if (g_trace_enabled) fputs("()", stderr);
+}
+
+void trace_mpz_t(const mpz_t op) {
+  if (g_trace_enabled) mpz_out_str(stderr, 10, op);
+}
+
+void trace_bool(const bool b) {
+  if (g_trace_enabled) {
+    if (b) {
+      fprintf(stderr, "true");
+    } else {
+      fprintf(stderr, "false");
+    }
+  }
+}
+
+void trace_unknown(void) {
+  if (g_trace_enabled) fputs("?", stderr);
+}
+
+void trace_argsep(void) {
+  if (g_trace_enabled) fputs(", ", stderr);
+}
+
+void trace_argend(void) {
+  if (g_trace_enabled) fputs(")\n", stderr);
+}
+
+void trace_retend(void) {
+  if (g_trace_enabled) fputs("\n", stderr);
+}
+
+void trace_start(char *name)
+{
+  if (g_trace_enabled) {
+    fprintf(stderr, "[TRACE] ");
+    for (int64_t i = 0; i < g_trace_depth; ++i) {
+      fprintf(stderr, "%s", "|   ");
+    }
+    fprintf(stderr, "%s(", name);
+  }
+}
+
+void trace_end(void)
+{
+  if (g_trace_enabled) {
+    fprintf(stderr, "[TRACE] ");
+    for (int64_t i = 0; i < g_trace_depth; ++i) {
+      fprintf(stderr, "%s", "|   ");
+    }
+  }
+}
+
+/* ***** Setup and cleanup functions for RTS ***** */
+
+void setup_rts(void)
+{
+  disable_tracing(UNIT);
+  setup_library();
+}
+
+void cleanup_rts(void)
+{
+  cleanup_library();
+  kill_mem();
+}
diff --git a/lib/rts.h b/lib/rts.h
new file mode 100644
index 00000000..de32ef8d
--- /dev/null
+++ b/lib/rts.h
@@ -0,0 +1,86 @@
+#pragma once
+
+#include<inttypes.h>
+#include<stdlib.h>
+#include<stdio.h>
+
+#include"sail.h"
+
+/*
+ * This function should be called whenever a pattern match failure
+ * occurs. Pattern match failures are always fatal.
+ */
+void sail_match_failure(sail_string msg);
+
+/* 
+ * sail_assert implements the assert construct in Sail. If any
+ * assertion fails we immediately exit the model.
+ */
+unit sail_assert(bool b, sail_string msg);
+
+/* ***** Memory builtins ***** */
+
+// These memory builtins are intended to match the semantics for the
+// __ReadRAM and __WriteRAM functions in ASL.
+
+unit write_ram(const mpz_t addr_size,     // Either 32 or 64
+	       const mpz_t data_size_mpz, // Number of bytes
+	       const sail_bits hex_ram,       // Currently unused
+	       const sail_bits addr_bv,
+	       const sail_bits data);
+
+void read_ram(sail_bits *data,
+	      const mpz_t addr_size,
+	      const mpz_t data_size_mpz,
+	      const sail_bits hex_ram,
+	      const sail_bits addr_bv);
+
+void load_image(char *);
+
+/* ***** Tracing ***** */
+
+static int64_t g_trace_depth;
+static bool g_trace_enabled;
+
+/*
+ * Bind these functions in Sail to enable and disable tracing:
+ *
+ * val "enable_tracing" : unit -> unit
+ * val "disable_tracing" : unit -> unit
+ *
+ * Compile with sail -c -c_trace.
+ */
+unit enable_tracing(const unit);
+unit disable_tracing(const unit);
+
+/*
+ * Tracing is implemented by void trace_TYPE functions, each of which
+ * takes the Sail value to print as the first argument, and prints it
+ * directly to stderr with no linebreaks.
+ *
+ * For types that don't have printing function we have trace_unknown,
+ * which simply prints '?'. trace_argsep, trace_argend, and
+ * trace_retend are used for formatting function arguments. They won't
+ * overlap with user defined types because the type names used for
+ * TYPE are zencoded. trace_start(NAME) and trace_end() are called
+ * before printing the function arguments and return value
+ * respectively.
+*/
+void trace_sail_int(const sail_int);
+void trace_bool(const bool);
+  
+void trace_unknown(void);
+void trace_argsep(void);
+void trace_argend(void);
+void trace_retend(void);
+void trace_start(char *);
+void trace_end(void);
+
+static uint64_t g_elf_entry;
+
+/*
+ * setup_rts and cleanup_rts are responsible for calling setup_library
+ * and cleanup_library in sail.h.
+ */
+void setup_rts(void);
+void cleanup_rts(void);
diff --git a/lib/sail.c b/lib/sail.c
new file mode 100644
index 00000000..5fd7a04e
--- /dev/null
+++ b/lib/sail.c
@@ -0,0 +1,558 @@
+#include<inttypes.h>
+#include<stdbool.h>
+#include<stdio.h>
+#include<stdlib.h>
+#include<string.h>
+
+#include"sail.h"
+
+/*
+ * Temporary mpzs for use in functions below. To avoid conflicts, only
+ * use in functions that do not call other functions in this file.
+ */
+static sail_int sail_lib_tmp1, sail_lib_tmp2;
+
+#define FLOAT_PRECISION 255
+
+void setup_library(void)
+{
+  mpz_init(sail_lib_tmp1);
+  mpz_init(sail_lib_tmp2);
+  mpf_set_default_prec(FLOAT_PRECISION);
+}
+
+void cleanup_library(void)
+{
+  mpz_clear(sail_lib_tmp1);
+  mpz_clear(sail_lib_tmp2);
+}
+
+/* ***** Sail bit type ***** */
+
+bool eq_bit(const mach_bits a, const mach_bits b)
+{
+  return a == b;
+}
+
+/* ***** Sail booleans ***** */
+
+bool not(const bool b) {
+  return !b;
+}
+
+bool eq_bool(const bool a, const bool b) {
+  return a == b;
+}
+
+bool UNDEFINED(bool)(const unit u) {
+  return false;
+}
+
+/* ***** Sail strings ***** */
+
+void CREATE(sail_string)(sail_string *str) {
+  char *istr = (char *) malloc(1 * sizeof(char));
+  istr[0] = '\0';
+  *str = istr;
+}
+
+void RECREATE(sail_string)(sail_string *str) {
+  free(*str);
+  char *istr = (char *) malloc(1 * sizeof(char));
+  istr[0] = '\0';
+  *str = istr;
+}
+
+void COPY(sail_string)(sail_string *str1, const sail_string str2) {
+  size_t len = strlen(str2);
+  *str1 = realloc(*str1, len + 1);
+  *str1 = strcpy(*str1, str2);
+}
+
+void KILL(sail_string)(sail_string *str) {
+  free(*str);
+}
+
+void dec_str(sail_string *str, const mpz_t n) {
+  free(*str);
+  gmp_asprintf(str, "%Zd", n);
+}
+
+void hex_str(sail_string *str, const mpz_t n) {
+  free(*str);
+  gmp_asprintf(str, "0x%Zx", n);
+}
+
+bool eq_string(const sail_string str1, const sail_string str2) {
+  return strcmp(str1, str2) == 0;
+}
+
+/* ***** Sail integers ***** */
+
+#ifndef USE_INT128
+
+inline
+void COPY(sail_int)(sail_int *rop, const sail_int op)
+{
+  mpz_set(*rop, op);
+}
+
+inline
+void CREATE(sail_int)(sail_int *rop)
+{
+  mpz_init(*rop);
+}
+
+inline
+void RECREATE(sail_int)(sail_int *rop)
+{
+  mpz_set_ui(*rop, 0);
+}
+
+inline
+void KILL(sail_int)(sail_int *rop)
+{
+  mpz_clear(*rop);
+}
+
+inline
+void CREATE_OF(sail_int, mach_int)(sail_int *rop, mach_int op)
+{
+  mpz_init_set_si(*rop, op);
+}
+
+inline
+void RECREATE_OF(sail_int, mach_int)(sail_int *rop, mach_int op)
+{
+  mpz_set_si(*rop, op);
+}
+
+inline
+void CREATE_OF(sail_int, sail_string)(sail_int *rop, sail_string str)
+{
+  mpz_init_set_str(*rop, str, 10);
+}
+
+inline
+void RECREATE_OF(sail_int, sail_string)(mpz_t *rop, sail_string str)
+{
+  mpz_set_str(*rop, str, 10);
+}
+
+inline
+mach_int CONVERT_OF(mach_int, sail_int)(const sail_int op)
+{
+  return mpz_get_si(op);
+}
+
+inline
+void CONVERT_OF(sail_int, mach_int)(sail_int *rop, const mach_int op)
+{
+  mpz_set_si(*rop, op);
+}
+
+inline
+bool eq_int(const sail_int op1, const sail_int op2)
+{
+  return !abs(mpz_cmp(op1, op2));
+}
+
+inline
+bool lt(const sail_int op1, const sail_int op2)
+{
+  return mpz_cmp(op1, op2) < 0;
+}
+
+inline
+bool gt(const mpz_t op1, const mpz_t op2)
+{
+  return mpz_cmp(op1, op2) > 0;
+}
+
+inline
+bool lteq(const mpz_t op1, const mpz_t op2)
+{
+  return mpz_cmp(op1, op2) <= 0;
+}
+
+inline
+bool gteq(const mpz_t op1, const mpz_t op2)
+{
+  return mpz_cmp(op1, op2) >= 0;
+}
+
+inline
+void shl_int(sail_int *rop, const sail_int op1, const sail_int op2)
+{
+  mpz_mul_2exp(*rop, op1, mpz_get_ui(op2));
+}
+
+inline
+void shr_int(sail_int *rop, const sail_int op1, const sail_int op2)
+{
+  mpz_fdiv_q_2exp(*rop, op1, mpz_get_ui(op2));
+}
+
+inline
+void undefined_int(sail_int *rop, const int n)
+{
+  mpz_set_ui(*rop, (uint64_t) n);
+}
+
+inline
+void undefined_range(sail_int *rop, const sail_int l, const sail_int u)
+{
+  mpz_set(*rop, l);
+}
+
+inline
+void add_int(sail_int *rop, const sail_int op1, const sail_int op2)
+{
+  mpz_add(*rop, op1, op2);
+}
+
+inline
+void sub_int(sail_int *rop, const sail_int op1, const sail_int op2)
+{
+  mpz_sub(*rop, op1, op2);
+}
+
+inline
+void mult_int(sail_int *rop, const sail_int op1, const sail_int op2)
+{
+  mpz_mul(*rop, op1, op2);
+}
+
+inline
+void tdiv_int(sail_int *rop, const sail_int op1, const sail_int op2)
+{
+  mpz_tdiv_q(*rop, op1, op2);
+}
+
+inline
+void tmod_int(sail_int *rop, const sail_int op1, const sail_int op2)
+{
+  mpz_tdiv_r(*rop, op1, op2);
+}
+
+inline
+void fdiv_int(sail_int *rop, const sail_int op1, const sail_int op2)
+{
+  mpz_fdiv_q(*rop, op1, op2);
+}
+
+inline
+void fmod_int(sail_int *rop, const sail_int op1, const sail_int op2)
+{
+  mpz_fdiv_r(*rop, op1, op2);
+}
+
+void max_int(sail_int *rop, const sail_int op1, const sail_int op2)
+{
+  if (lt(op1, op2)) {
+    mpz_set(*rop, op2);
+  } else {
+    mpz_set(*rop, op1);
+  }
+}
+
+void min_int(sail_int *rop, const sail_int op1, const sail_int op2)
+{
+  if (gt(op1, op2)) {
+    mpz_set(*rop, op2);
+  } else {
+    mpz_set(*rop, op1);
+  }
+}
+
+inline
+void neg_int(sail_int *rop, const sail_int op)
+{
+  mpz_neg(*rop, op);
+}
+
+inline
+void abs_int(sail_int *rop, const sail_int op)
+{
+  mpz_abs(*rop, op);
+}
+
+void pow2(sail_int *rop, const sail_int exp) {
+  /* Assume exponent is never more than 2^64... */
+  uint64_t exp_ui = mpz_get_ui(exp);
+  mpz_t base;
+  mpz_init_set_ui(base, 2ul);
+  mpz_pow_ui(*rop, base, exp_ui);
+  mpz_clear(base);
+}
+
+#endif
+
+/* ***** Sail bitvectors ***** */
+
+void CREATE(sail_bits)(sail_bits *rop)
+{
+  rop->bits = malloc(sizeof(mpz_t));
+  rop->len = 0;
+  mpz_init(*rop->bits);
+}
+
+void RECREATE(sail_bits)(sail_bits *rop)
+{
+  rop->len = 0;
+  mpz_set_ui(*rop->bits, 0);
+}
+
+void COPY(sail_bits)(sail_bits *rop, const sail_bits op)
+{
+  rop->len = op.len;
+  mpz_set(*rop->bits, *op.bits);
+}
+
+void KILL(sail_bits)(sail_bits *rop)
+{
+  mpz_clear(*rop->bits);
+  free(rop->bits);
+}
+
+void CREATE_OF(sail_bits, mach_bits)(sail_bits *rop, const uint64_t op, const uint64_t len, const bool direction)
+{
+  rop->bits = malloc(sizeof(mpz_t));
+  rop->len = len;
+  mpz_init_set_ui(*rop->bits, op);
+}
+
+void RECREATE_OF(sail_bits, mach_bits)(sail_bits *rop, const uint64_t op, const uint64_t len, const bool direction)
+{
+  rop->len = len;
+  mpz_set_ui(*rop->bits, op);
+}
+
+mach_bits CONVERT_OF(mach_bits, sail_bits)(const sail_bits op)
+{
+  return mpz_get_ui(*op.bits);
+}
+
+void UNDEFINED(sail_bits)(sail_bits *rop, const sail_int len, const mach_bits bit)
+{
+  zeros(rop, len);
+}
+
+mach_bits UNDEFINED(mach_bits)(const unit u) { return 0; }
+
+mach_bits safe_rshift(const mach_bits x, const mach_bits n)
+{
+  if (n >= 64) {
+    return 0ul;
+  } else {
+    return x >> n;
+  }
+}
+
+void normalize_sail_bits(sail_bits *rop) {
+  /* TODO optimisation: keep a set of masks of various sizes handy */
+  mpz_set_ui(sail_lib_tmp1, 1);
+  mpz_mul_2exp(sail_lib_tmp1, sail_lib_tmp1, rop->len);
+  mpz_sub_ui(sail_lib_tmp1, sail_lib_tmp1, 1);
+  mpz_and(*rop->bits, *rop->bits, sail_lib_tmp1);
+}
+
+void append_64(sail_bits *rop, const sail_bits op, const mach_bits chunk)
+{
+  rop->len = rop->len + 64ul;
+  mpz_mul_2exp(*rop->bits, *op.bits, 64ul);
+  mpz_add_ui(*rop->bits, *rop->bits, chunk);
+}
+
+void add_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2)
+{
+  rop->len = op1.len;
+  mpz_add(*rop->bits, *op1.bits, *op2.bits);
+  normalize_sail_bits(rop);
+}
+
+void sub_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2)
+{
+  rop->len = op1.len;
+  mpz_sub(*rop->bits, *op1.bits, *op2.bits);
+  normalize_sail_bits(rop);
+}
+
+void add_bits_int(sail_bits *rop, const sail_bits op1, const mpz_t op2)
+{
+  rop->len = op1.len;
+  mpz_add(*rop->bits, *op1.bits, op2);
+  normalize_sail_bits(rop);
+}
+
+void sub_bits_int(sail_bits *rop, const sail_bits op1, const mpz_t op2)
+{
+  rop->len = op1.len;
+  mpz_sub(*rop->bits, *op1.bits, op2);
+  normalize_sail_bits(rop);
+}
+
+void zeros(sail_bits *rop, const sail_int op)
+{
+  rop->len = mpz_get_ui(op);
+  mpz_set_ui(*rop->bits, 0);
+}
+
+void zero_extend(sail_bits *rop, const sail_bits op, const sail_int len)
+{
+  rop->len = mpz_get_ui(len);
+  mpz_set(*rop->bits, *op.bits);
+}
+
+void length_sail_bits(sail_int *rop, const sail_bits op)
+{
+  mpz_set_ui(*rop, op.len);
+}
+
+bool eq_bits(const sail_bits op1, const sail_bits op2)
+{
+  for (mp_bitcnt_t i = 0; i < op1.len; i++) {
+    if (mpz_tstbit(*op1.bits, i) != mpz_tstbit(*op2.bits, i)) return false;
+  }
+  return true;
+}
+
+void vector_subrange_sail_bits(sail_bits *rop,
+			       const sail_bits op,
+			       const sail_int n_mpz,
+			       const sail_int m_mpz)
+{
+  uint64_t n = mpz_get_ui(n_mpz);
+  uint64_t m = mpz_get_ui(m_mpz);
+
+  rop->len = n - (m - 1ul);
+  mpz_fdiv_q_2exp(*rop->bits, *op.bits, m);
+  normalize_sail_bits(rop);
+}
+
+void truncate(sail_bits *rop, const sail_bits op, const sail_int len)
+{
+  rop->len = mpz_get_ui(len);
+  mpz_set(*rop->bits, *op.bits);
+  normalize_sail_bits(rop);
+}
+
+mach_bits bitvector_access(const sail_bits op, const sail_int n_mpz)
+{
+  uint64_t n = mpz_get_ui(n_mpz);
+  return (mach_bits) mpz_tstbit(*op.bits, n);
+}
+
+void sail_unsigned(sail_int *rop, const sail_bits op)
+{
+  /* Normal form of bv_t is always positive so just return the bits. */
+  mpz_set(*rop, *op.bits);
+}
+
+void sail_signed(sail_int *rop, const sail_bits op)
+{
+  if (op.len == 0) {
+    mpz_set_ui(*rop, 0);
+  } else {
+    mp_bitcnt_t sign_bit = op.len - 1;
+    mpz_set(*rop, *op.bits);
+    if (mpz_tstbit(*op.bits, sign_bit) != 0) {
+      /* If sign bit is unset then we are done,
+         otherwise clear sign_bit and subtract 2**sign_bit */
+      mpz_set_ui(sail_lib_tmp1, 1);
+      mpz_mul_2exp(sail_lib_tmp1, sail_lib_tmp1, sign_bit); /* 2**sign_bit */
+      mpz_combit(*rop, sign_bit); /* clear sign_bit */
+      mpz_sub(*rop, *rop, sail_lib_tmp1);
+    }
+  }
+}
+
+/* ***** Printing functions ***** */
+
+void fprint_bits(const sail_string pre,
+		 const sail_bits op,
+		 const sail_string post,
+		 FILE *stream)
+{
+  fputs(pre, stream);
+
+  if (op.len % 4 == 0) {
+    fputs("0x", stream);
+    mpz_t buf;
+    mpz_init_set(buf, *op.bits);
+
+    char *hex = malloc((op.len / 4) * sizeof(char));
+
+    for (int i = 0; i < op.len / 4; ++i) {
+      char c = (char) ((0xF & mpz_get_ui(buf)) + 0x30);
+      hex[i] = (c < 0x3A) ? c : c + 0x7;
+      mpz_fdiv_q_2exp(buf, buf, 4);
+    }
+
+    for (int i = op.len / 4; i > 0; --i) {
+      fputc(hex[i - 1], stream);
+    }
+
+    free(hex);
+    mpz_clear(buf);
+  } else {
+    fputs("0b", stream);
+    for (int i = op.len; i > 0; --i) {
+      fputc(mpz_tstbit(*op.bits, i - 1) + 0x30, stream);
+    }
+  }
+
+  fputs(post, stream);
+}
+
+unit print_bits(const sail_string str, const sail_bits op)
+{
+  fprint_bits(str, op, "\n", stdout);
+  return UNIT;
+}
+
+unit prerr_bits(const sail_string str, const sail_bits op)
+{
+  fprint_bits(str, op, "\n", stderr);
+  return UNIT;
+}
+
+unit print(const sail_string str)
+{
+  printf("%s", str);
+  return UNIT;
+}
+
+unit print_endline(const sail_string str)
+{
+  printf("%s\n", str);
+  return UNIT;
+}
+
+unit prerr(const sail_string str)
+{
+  fprintf(stderr, "%s", str);
+  return UNIT;
+}
+
+unit prerr_endline(const sail_string str)
+{
+  fprintf(stderr, "%s\n", str);
+  return UNIT;
+}
+
+unit print_int(const sail_string str, const sail_int op)
+{
+  fputs(str, stdout);
+  mpz_out_str(stdout, 10, op);
+  putchar('\n');
+  return UNIT;
+}
+
+unit prerr_int(const sail_string str, const sail_int op)
+{
+  fputs(str, stderr);
+  mpz_out_str(stderr, 10, op);
+  fputs("\n", stderr);
+  return UNIT;
+}
diff --git a/lib/sail.h b/lib/sail.h
index a2f2f456..1cd5d928 100644
--- a/lib/sail.h
+++ b/lib/sail.h
@@ -1,1276 +1,236 @@
-#ifndef SAIL_LIB
-#define SAIL_LIB
+#pragma once
 
-#include<stdio.h>
 #include<inttypes.h>
 #include<stdlib.h>
+#include<stdio.h>
 #include<stdbool.h>
-#include<string.h>
+
+#ifndef USE_INT128
 #include<gmp.h>
-#include<time.h>
+#endif
+
+/*
+ * Called by the RTS to initialise and clear any library state.
+ */
+void setup_library(void);
+void cleanup_library(void);
+
+/*
+ * The Sail compiler expects functions to follow a specific naming
+ * convention for allocation, deallocation, and (deep)-copying. These
+ * macros implement this naming convention.
+ */
+#define CREATE(type) create_ ## type
+#define RECREATE(type) recreate_ ## type
+#define CREATE_OF(type1, type2) create_ ## type1 ## _of_ ## type2
+#define RECREATE_OF(type1, type2) recreate_ ## type1 ## _of_ ## type2
+#define CONVERT_OF(type1, type2) convert_ ## type1 ## _of_ ## type2
+#define COPY(type) copy_ ## type
+#define KILL(type) kill_ ## type
+#define UNDEFINED(type) undefined_ ## type
+
+#define SAIL_BUILTIN_TYPE(type)\
+  void create_ ## type(type *);\
+  void recreate_ ## type(type *);\
+  void copy_ ## type(type *, const type);\
+  void kill_ ## type(type *);
+
+/* ***** Sail unit type ***** */
 
 typedef int unit;
 
 #define UNIT 0
 
-unit undefined_unit(const unit u) {
-  return UNIT;
-}
+unit UNDEFINED(unit)(const unit);
+bool eq_unit(const unit, const unit);
+  
+/* ***** Sail booleans ***** */
 
-bool eq_unit(const unit u1, const unit u2) {
-  return true;
-}
+/*
+ * and_bool and or_bool are special-cased by the compiler to ensure
+ * short-circuiting evaluation.
+ */
+bool not(const bool);
+bool eq_bool(const bool, const bool);
+bool UNDEFINED(bool)(const unit);
 
-typedef struct {
-  mp_bitcnt_t len;
-  mpz_t *bits;
-} bv_t;
+/* ***** Sail strings ***** */
 
+/*
+ * Sail strings are just C strings.
+ */
 typedef char *sail_string;
 
-/* Temporary mpzs for use in functions below. To avoid conflicts, only
- * use in functions that do not call other functions in this file. */
-static mpz_t sail_lib_tmp1, sail_lib_tmp2;
-
-/* Wrapper around >> operator to avoid UB when shift amount is greater
-   than or equal to 64. */
-uint64_t safe_rshift(const uint64_t x, const uint64_t n) {
-  if (n >= 64) {
-    return 0ul;
-  } else {
-    return x >> n;
-  }
-}
-
-/* This function should be called whenever a pattern match failure
-   occurs. Pattern match failures are always fatal. */
-void sail_match_failure(sail_string msg) {
-  fprintf(stderr, "Pattern match failure in %s\n", msg);
-  exit(EXIT_FAILURE);
-}
-
-/* sail_assert implements the assert construct in Sail. If any
-   assertion fails we immediately exit the model. */
-unit sail_assert(bool b, sail_string msg) {
-  if (b) return UNIT;
-  fprintf(stderr, "Assertion failed: %s\n", msg);
-  exit(EXIT_FAILURE);
-}
-
-/* If the sail model calls the exit() function we print a message and
-   exit successfully. */
-unit sail_exit(const unit u) {
-  fprintf(stderr, "Sail model exit\n");
-  exit(EXIT_SUCCESS);
-}
-
-uint64_t g_elf_entry;
-
-void elf_entry(mpz_t *rop, const unit u) {
-  mpz_set_ui(*rop, g_elf_entry);
-}
-
-void elf_tohost(mpz_t *rop, const unit u) {
-  mpz_set_ui(*rop, 0x0ul);
-}
-
-/* ASL->Sail model has an EnterLowPowerState() function that calls a
-   sleep request builtin. If it gets called we print a message and
-   exit the model. */
-unit sleep_request(const unit u) {
-  fprintf(stderr, "Sail model going to sleep\n");
-  exit(EXIT_SUCCESS);
-}
-
-// Sail bits are mapped to uint64_t where bitzero = 0ul and bitone = 1ul
-bool eq_bit(const uint64_t a, const uint64_t b) {
-  return a == b;
-}
-
-uint64_t undefined_bit(unit u) { return 0; }
-
-unit skip(const unit u) {
-  return UNIT;
-}
-
-// ***** Sail booleans *****
-
-bool not(const bool b) {
-  return !b;
-}
-
-bool and_bool(const bool a, const bool b) {
-  return a && b;
-}
-
-bool or_bool(const bool a, const bool b) {
-  return a || b;
-}
-
-bool eq_bool(const bool a, const bool b) {
-  return a == b;
-}
-
-bool undefined_bool(const unit u) {
-  return false;
-}
-
-// ***** Sail strings *****
-void init_sail_string(sail_string *str) {
-  char *istr = (char *) malloc(1 * sizeof(char));
-  istr[0] = '\0';
-  *str = istr;
-}
-
-void reinit_sail_string(sail_string *str) {
-  free(*str);
-  char *istr = (char *) malloc(1 * sizeof(char));
-  istr[0] = '\0';
-  *str = istr;
-}
-
-void set_sail_string(sail_string *str1, const sail_string str2) {
-  size_t len = strlen(str2);
-  *str1 = realloc(*str1, len + 1);
-  *str1 = strcpy(*str1, str2);
-}
-
-void dec_str(sail_string *str, const mpz_t n) {
-  free(*str);
-  gmp_asprintf(str, "%Zd", n);
-}
-
-void hex_str(sail_string *str, const mpz_t n) {
-  free(*str);
-  gmp_asprintf(str, "0x%Zx", n);
-}
-
-void clear_sail_string(sail_string *str) {
-  free(*str);
-}
-
-bool eq_string(const sail_string str1, const sail_string str2) {
-  return strcmp(str1, str2) == 0;
-}
-
-void concat_str(sail_string *stro, const sail_string str1, const sail_string str2) {
-  *stro = realloc(*stro, strlen(str1) + strlen(str2) + 1);
-  (*stro)[0] = '\0';
-  strcat(*stro, str1);
-  strcat(*stro, str2);
-}
-
-void undefined_string(sail_string *str, const unit u) {
-}
-
-unit print(const sail_string str) {
-  printf("%s", str);
-  return UNIT;
-}
-
-unit print_endline(const sail_string str) {
-  printf("%s\n", str);
-  return UNIT;
-}
-
-unit print_string(const sail_string str1, const sail_string str2) {
-  printf("%s%s\n", str1, str2);
-  return UNIT;
-}
-
-unit prerr(const sail_string str) {
-  fprintf(stderr, "%s", str);
-  return UNIT;
-}
-
-unit prerr_endline(const sail_string str) {
-  fprintf(stderr, "%s\n", str);
-  return UNIT;
-}
-
-unit print_int(const sail_string str, const mpz_t op) {
-  fputs(str, stdout);
-  mpz_out_str(stdout, 10, op);
-  putchar('\n');
-  return UNIT;
-}
-
-unit prerr_int(const sail_string str, const mpz_t op) {
-  fputs(str, stderr);
-  mpz_out_str(stderr, 10, op);
-  fputs("\n", stderr);
-  return UNIT;
-}
-
-unit print_int64(const sail_string str, const int64_t op) {
-  printf("%s%" PRId64 "\n", str, op);
-  return UNIT;
-}
-
-unit sail_putchar(const mpz_t op) {
-  char c = (char) mpz_get_ui(op);
-  printf("%c", c);
-  fflush(stdout);
-  return UNIT;
-}
-
-// ***** Arbitrary precision integers *****
-
-// We wrap around the GMP functions so they follow a consistent naming
-// scheme that is shared with the other builtin sail types.
-
-void set_mpz_t(mpz_t *rop, const mpz_t op) {
-  mpz_set(*rop, op);
-}
-
-void init_mpz_t(mpz_t *op) {
-  mpz_init(*op);
-}
-
-void reinit_mpz_t(mpz_t *op) {
-  mpz_set_ui(*op, 0);
-}
-
-void clear_mpz_t(mpz_t *op) {
-  mpz_clear(*op);
-}
-
-void init_mpz_t_of_int64_t(mpz_t *rop, int64_t op) {
-  mpz_init_set_si(*rop, op);
-}
-
-void reinit_mpz_t_of_int64_t(mpz_t *rop, int64_t op) {
-  mpz_set_si(*rop, op);
-}
-
-void init_mpz_t_of_sail_string(mpz_t *rop, sail_string str) {
-  mpz_init_set_str(*rop, str, 10);
-}
-
-void reinit_mpz_t_of_sail_string(mpz_t *rop, sail_string str) {
-  mpz_set_str(*rop, str, 10);
-}
-
-int64_t convert_int64_t_of_mpz_t(const mpz_t op) {
-  return mpz_get_si(op);
-}
-
-void convert_mpz_t_of_int64_t(mpz_t *rop, const int64_t op) {
-  mpz_set_si(*rop, op);
-}
-
-// ***** Sail builtins for integers *****
-
-bool eq_int(const mpz_t op1, const mpz_t op2) {
-  return !abs(mpz_cmp(op1, op2));
-}
-
-bool lt(const mpz_t op1, const mpz_t op2) {
-  return mpz_cmp(op1, op2) < 0;
-}
-
-bool gt(const mpz_t op1, const mpz_t op2) {
-  return mpz_cmp(op1, op2) > 0;
-}
-
-bool lteq(const mpz_t op1, const mpz_t op2) {
-  return mpz_cmp(op1, op2) <= 0;
-}
-
-bool gteq(const mpz_t op1, const mpz_t op2) {
-  return mpz_cmp(op1, op2) >= 0;
-}
-
-void shl_int(mpz_t *rop, const mpz_t op1, const mpz_t op2) {
-  mpz_mul_2exp(*rop, op1, mpz_get_ui(op2));
-}
-
-void shr_int(mpz_t *rop, const mpz_t op1, const mpz_t op2) {
-  mpz_fdiv_q_2exp(*rop, op1, mpz_get_ui(op2));
-}
-
-void undefined_int(mpz_t *rop, const unit u) {
-  mpz_set_ui(*rop, 0ul);
-}
-
-void undefined_range(mpz_t *rop, const mpz_t l, const mpz_t u) {
-  mpz_set(*rop, l);
-}
-
-void add_int(mpz_t *rop, const mpz_t op1, const mpz_t op2)
-{
-  mpz_add(*rop, op1, op2);
-}
-
-void sub_int(mpz_t *rop, const mpz_t op1, const mpz_t op2)
-{
-  mpz_sub(*rop, op1, op2);
-}
-
-void mult_int(mpz_t *rop, const mpz_t op1, const mpz_t op2)
-{
-  mpz_mul(*rop, op1, op2);
-}
-
-void div_int(mpz_t *rop, const mpz_t op1, const mpz_t op2)
-{
-  mpz_tdiv_q(*rop, op1, op2);
-}
-
-void mod_int(mpz_t *rop, const mpz_t op1, const mpz_t op2)
-{
-  mpz_tdiv_r(*rop, op1, op2);
-}
-
-void max_int(mpz_t *rop, const mpz_t op1, const mpz_t op2) {
-  if (lt(op1, op2)) {
-    mpz_set(*rop, op2);
-  } else {
-    mpz_set(*rop, op1);
-  }
-}
-
-void min_int(mpz_t *rop, const mpz_t op1, const mpz_t op2) {
-  if (gt(op1, op2)) {
-    mpz_set(*rop, op2);
-  } else {
-    mpz_set(*rop, op1);
-  }
-}
-
-void neg_int(mpz_t *rop, const mpz_t op) {
-  mpz_neg(*rop, op);
-}
-
-void abs_int(mpz_t *rop, const mpz_t op) {
-  mpz_abs(*rop, op);
-}
-
-void pow2(mpz_t *rop, mpz_t exp) {
-  uint64_t exp_ui = mpz_get_ui(exp);
-  mpz_t base;
-  mpz_init_set_ui(base, 2ul);
-  mpz_pow_ui(*rop, base, exp_ui);
-  mpz_clear(base);
-}
-
-void get_time_ns(mpz_t *rop, const unit u) {
-  struct timespec t;
-  clock_gettime(CLOCK_REALTIME, &t);
-  mpz_set_si(*rop, t.tv_sec);
-  mpz_mul_ui(*rop, *rop, 1000000000);
-  mpz_add_ui(*rop, *rop, t.tv_nsec);
-}
-
-// ***** Sail bitvectors *****
-
-void string_of_int(sail_string *str, mpz_t i) {
-  gmp_asprintf(str, "%Zd", i);
-}
-
-void string_of_bits(sail_string *str, const bv_t op) {
-  if ((op.len % 4) == 0) {
-    gmp_asprintf(str, "0x%*0Zx", op.len / 4, *op.bits);
-  } else {
-    gmp_asprintf(str, "0b%*0Zb", op.len, *op.bits);
-  }
-}
-
-unit fprint_bits(const sail_string str, const bv_t op, FILE *stream)
-{
-  fputs(str, stream);
-
-  if (op.len % 4 == 0) {
-    fputs("0x", stream);
-    mpz_t buf;
-    mpz_init_set(buf, *op.bits);
-
-    char *hex = malloc((op.len / 4) * sizeof(char));
-
-    for (int i = 0; i < op.len / 4; ++i) {
-      char c = (char) ((0xF & mpz_get_ui(buf)) + 0x30);
-      hex[i] = (c < 0x3A) ? c : c + 0x7;
-      mpz_fdiv_q_2exp(buf, buf, 4);
-    }
-
-    for (int i = op.len / 4; i > 0; --i) {
-      fputc(hex[i - 1], stream);
-    }
-
-    free(hex);
-    mpz_clear(buf);
-  } else {
-    fputs("0b", stream);
-    for (int i = op.len; i > 0; --i) {
-      fputc(mpz_tstbit(*op.bits, i - 1) + 0x30, stream);
-    }
-  }
-
-  fputs("\n", stream);
-  return UNIT;
-}
-
-unit print_bits(const sail_string str, const bv_t op)
-{
-  return fprint_bits(str, op, stdout);
-}
-
-unit prerr_bits(const sail_string str, const bv_t op)
-{
-  return fprint_bits(str, op, stderr);
-}
-
-void length_bv_t(mpz_t *rop, const bv_t op) {
-  mpz_set_ui(*rop, op.len);
-}
-
-void init_bv_t(bv_t *rop) {
-  rop->bits = malloc(sizeof(mpz_t));
-  rop->len = 0;
-  mpz_init(*rop->bits);
-}
-
-void reinit_bv_t(bv_t *rop) {
-  rop->len = 0;
-  mpz_set_ui(*rop->bits, 0);
-}
-
-void normalise_bv_t(bv_t *rop) {
-  /* TODO optimisation: keep a set of masks of various sizes handy */
-  mpz_set_ui(sail_lib_tmp1, 1);
-  mpz_mul_2exp(sail_lib_tmp1, sail_lib_tmp1, rop->len);
-  mpz_sub_ui(sail_lib_tmp1, sail_lib_tmp1, 1);
-  mpz_and(*rop->bits, *rop->bits, sail_lib_tmp1);
-}
-
-void init_bv_t_of_uint64_t(bv_t *rop, const uint64_t op, const uint64_t len, const bool direction) {
-  rop->bits = malloc(sizeof(mpz_t));
-  rop->len = len;
-  mpz_init_set_ui(*rop->bits, op);
-}
-
-void reinit_bv_t_of_uint64_t(bv_t *rop, const uint64_t op, const uint64_t len, const bool direction) {
-  rop->len = len;
-  mpz_set_ui(*rop->bits, op);
-}
-
-void set_bv_t(bv_t *rop, const bv_t op) {
-  rop->len = op.len;
-  mpz_set(*rop->bits, *op.bits);
-}
-
-void append_64(bv_t *rop, const bv_t op, const uint64_t chunk) {
-  rop->len = rop->len + 64ul;
-  mpz_mul_2exp(*rop->bits, *op.bits, 64ul);
-  mpz_add_ui(*rop->bits, *rop->bits, chunk);
-}
-
-void append(bv_t *rop, const bv_t op1, const bv_t op2) {
-  rop->len = op1.len + op2.len;
-  mpz_mul_2exp(*rop->bits, *op1.bits, op2.len);
-  mpz_ior(*rop->bits, *rop->bits, *op2.bits);
-}
-
-void replicate_bits(bv_t *rop, const bv_t op1, const mpz_t op2) {
-  uint64_t op2_ui = mpz_get_ui(op2);
-  rop->len = op1.len * op2_ui;
-  mpz_set(*rop->bits, *op1.bits);
-  for (int i = 1; i < op2_ui; i++) {
-    mpz_mul_2exp(*rop->bits, *rop->bits, op1.len);
-    mpz_ior(*rop->bits, *rop->bits, *op1.bits);
-  }
-}
+SAIL_BUILTIN_TYPE(sail_string);
 
-uint64_t fast_replicate_bits(const uint64_t shift, const uint64_t v, const int64_t times) {
-  uint64_t r = v;
-  for (int i = 1; i < times; ++i) {
-    r |= (r << shift);
-  }
-  return r;
-}
+void dec_str(sail_string *str, const mpz_t n);
+void hex_str(sail_string *str, const mpz_t n);
 
-void slice(bv_t *rop, const bv_t op, const mpz_t start_mpz, const mpz_t len_mpz)
-{
-  uint64_t start = mpz_get_ui(start_mpz);
-  uint64_t len = mpz_get_ui(len_mpz);
+bool eq_string(const sail_string, const sail_string);
 
-  mpz_set_ui(*rop->bits, 0ul);
-  rop->len = len;
+/* ***** Sail integers ***** */
 
-  for (uint64_t i = 0; i < len; i++) {
-    if (mpz_tstbit(*op.bits, i + start)) mpz_setbit(*rop->bits, i);
-  }
-}
+typedef int64_t mach_int;
 
-uint64_t convert_uint64_t_of_bv_t(const bv_t op) {
-  return mpz_get_ui(*op.bits);
-}
-
-void zeros(bv_t *rop, const mpz_t op) {
-  rop->len = mpz_get_ui(op);
-  mpz_set_ui(*rop->bits, 0ul);
-}
-
-void zero_extend(bv_t *rop, const bv_t op, const mpz_t len) {
-  rop->len = mpz_get_ui(len);
-  mpz_set(*rop->bits, *op.bits);
-}
-
-void sign_extend(bv_t *rop, const bv_t op, const mpz_t len) {
-  rop->len = mpz_get_ui(len);
-  if(mpz_tstbit(*op.bits, op.len - 1)) {
-    mpz_set(*rop->bits, *op.bits);
-    for(mp_bitcnt_t i = rop->len - 1; i >= op.len; i--) {
-      mpz_setbit(*rop->bits, i);
-    }
-  } else {
-    mpz_set(*rop->bits, *op.bits);
-  }
-}
-
-void clear_bv_t(bv_t *rop) {
-  mpz_clear(*rop->bits);
-  free(rop->bits);
-}
-
-void undefined_bv_t(bv_t *rop, mpz_t len, int bit) {
-  zeros(rop, len);
-}
-
-void mask(bv_t *rop) {
-  if (mpz_sizeinbase(*rop->bits, 2) > rop->len) {
-    mpz_t m;
-    mpz_init(m);
-    mpz_ui_pow_ui(m, 2ul, rop->len);
-    mpz_sub_ui(m, m, 1ul);
-    mpz_and(*rop->bits, *rop->bits, m);
-    mpz_clear(m);
-  }
-}
-
-void truncate(bv_t *rop, const bv_t op, const mpz_t len) {
-  rop->len = mpz_get_ui(len);
-  mpz_set(*rop->bits, *op.bits);
-  mask(rop);
-}
-
-void and_bits(bv_t *rop, const bv_t op1, const bv_t op2) {
-  rop->len = op1.len;
-  mpz_and(*rop->bits, *op1.bits, *op2.bits);
-}
-
-void or_bits(bv_t *rop, const bv_t op1, const bv_t op2) {
-  rop->len = op1.len;
-  mpz_ior(*rop->bits, *op1.bits, *op2.bits);
-}
-
-void not_bits(bv_t *rop, const bv_t op) {
-  rop->len = op.len;
-  mpz_set(*rop->bits, *op.bits);
-  for (mp_bitcnt_t i = 0; i < op.len; i++) {
-    mpz_combit(*rop->bits, i);
-  }
-}
-
-void xor_bits(bv_t *rop, const bv_t op1, const bv_t op2) {
-  rop->len = op1.len;
-  mpz_xor(*rop->bits, *op1.bits, *op2.bits);
-}
-
-bool eq_bits(const bv_t op1, const bv_t op2)
-{
-  for (mp_bitcnt_t i = 0; i < op1.len; i++) {
-    if (mpz_tstbit(*op1.bits, i) != mpz_tstbit(*op2.bits, i)) return false;
-  }
-  return true;
-}
-
-void sail_uint(mpz_t *rop, const bv_t op) {
-  /* Normal form of bv_t is always positive so just return the bits. */
-  mpz_set(*rop, *op.bits);
-}
-
-void sint(mpz_t *rop, const bv_t op)
-{
-  if (op.len == 0) {
-    mpz_set_ui(*rop, 0);
-  } else {
-    mp_bitcnt_t sign_bit = op.len - 1;
-    mpz_set(*rop, *op.bits);
-    if (mpz_tstbit(*op.bits, sign_bit) != 0) {
-      /* If sign bit is unset then we are done,
-         otherwise clear sign_bit and subtract 2**sign_bit */
-      mpz_set_ui(sail_lib_tmp1, 1);
-      mpz_mul_2exp(sail_lib_tmp1, sail_lib_tmp1, sign_bit); /* 2**sign_bit */
-      mpz_combit(*rop, sign_bit); /* clear sign_bit */
-      mpz_sub(*rop, *rop, sail_lib_tmp1);
-    }
-  }
-}
-
-void add_bits(bv_t *rop, const bv_t op1, const bv_t op2) {
-  rop->len = op1.len;
-  mpz_add(*rop->bits, *op1.bits, *op2.bits);
-  normalise_bv_t(rop);
-}
-
-void sub_bits(bv_t *rop, const bv_t op1, const bv_t op2) {
-  rop->len = op1.len;
-  mpz_sub(*rop->bits, *op1.bits, *op2.bits);
-  normalise_bv_t(rop);
-}
-
-void add_bits_int(bv_t *rop, const bv_t op1, const mpz_t op2) {
-  rop->len = op1.len;
-  mpz_add(*rop->bits, *op1.bits, op2);
-  normalise_bv_t(rop);
-}
-
-void sub_bits_int(bv_t *rop, const bv_t op1, const mpz_t op2) {
-  rop->len = op1.len;
-  mpz_sub(*rop->bits, *op1.bits, op2);
-}
-
-void mults_vec(bv_t *rop, const bv_t op1, const bv_t op2) {
-  mpz_t op1_int, op2_int;
-  mpz_init(op1_int);
-  mpz_init(op2_int);
-  sint(&op1_int, op1);
-  sint(&op2_int, op2);
-  rop->len = op1.len * 2;
-  mpz_mul(*rop->bits, op1_int, op2_int);
-  normalise_bv_t(rop);
-  mpz_clear(op1_int);
-  mpz_clear(op2_int);
-}
-
-void mult_vec(bv_t *rop, const bv_t op1, const bv_t op2) {
-  rop->len = op1.len * 2;
-  mpz_mul(*rop->bits, *op1.bits, *op2.bits);
-  normalise_bv_t(rop); /* necessary? */
-}
-
-void shift_bits_left(bv_t *rop, const bv_t op1, const bv_t op2) {
-  rop->len = op1.len;
-  mpz_mul_2exp(*rop->bits, *op1.bits, mpz_get_ui(*op2.bits));
-  normalise_bv_t(rop);
-}
-
-void shift_bits_right(bv_t *rop, const bv_t op1, const bv_t op2) {
-  rop->len = op1.len;
-  mpz_tdiv_q_2exp(*rop->bits, *op1.bits, mpz_get_ui(*op2.bits));
-}
-
-/* FIXME */
-void shift_bits_right_arith(bv_t *rop, const bv_t op1, const bv_t op2) {
-  rop->len = op1.len;
-  mp_bitcnt_t shift_amt = mpz_get_ui(*op2.bits);
-  mp_bitcnt_t sign_bit = op1.len - 1;
-  mpz_fdiv_q_2exp(*rop->bits, *op1.bits, shift_amt);
-  if(mpz_tstbit(*op1.bits, sign_bit) != 0) {
-    /* */
-    for(; shift_amt > 0; shift_amt--) {
-      mpz_setbit(*rop->bits, sign_bit - shift_amt + 1);
-    }
-  }
-}
-
-void reverse_endianness(bv_t *rop, const bv_t op) {
-  rop->len = op.len;
-  if (rop->len == 64ul) {
-    uint64_t x = mpz_get_ui(*op.bits);
-    x = (x & 0xFFFFFFFF00000000) >> 32 | (x & 0x00000000FFFFFFFF) << 32;
-    x = (x & 0xFFFF0000FFFF0000) >> 16 | (x & 0x0000FFFF0000FFFF) << 16;
-    x = (x & 0xFF00FF00FF00FF00) >> 8  | (x & 0x00FF00FF00FF00FF) << 8;
-    mpz_set_ui(*rop->bits, x);
-  } else if (rop->len == 32ul) {
-    uint64_t x = mpz_get_ui(*op.bits);
-    x = (x & 0xFFFF0000FFFF0000) >> 16 | (x & 0x0000FFFF0000FFFF) << 16;
-    x = (x & 0xFF00FF00FF00FF00) >> 8  | (x & 0x00FF00FF00FF00FF) << 8;
-    mpz_set_ui(*rop->bits, x);
-  } else if (rop->len == 16ul) {
-    uint64_t x = mpz_get_ui(*op.bits);
-    x = (x & 0xFF00FF00FF00FF00) >> 8  | (x & 0x00FF00FF00FF00FF) << 8;
-    mpz_set_ui(*rop->bits, x);
-  } else if (rop->len == 8ul) {
-    mpz_set(*rop->bits, *op.bits);
-  } else {
-    /* For other numbers of bytes we reverse the bytes.
-     * XXX could use mpz_import/export for this. */
-    mpz_set_ui(sail_lib_tmp1, 0xff); // byte mask
-    mpz_set_ui(*rop->bits, 0); // reset accumulator for result
-    for(mp_bitcnt_t byte = 0; byte < op.len; byte+=8) {
-      mpz_tdiv_q_2exp(sail_lib_tmp2, *op.bits, byte); // shift byte to bottom
-      mpz_and(sail_lib_tmp2, sail_lib_tmp2, sail_lib_tmp1); // and with mask
-      mpz_mul_2exp(*rop->bits, *rop->bits, 8); // shift result left 8
-      mpz_ior(*rop->bits, *rop->bits, sail_lib_tmp2); // or byte into result
-    }
-  }
-}
-
-// Takes a slice of the (two's complement) binary representation of
-// integer n, starting at bit start, and of length len. With the
-// argument in the following order:
-//
-// get_slice_int(len, n, start)
-//
-// For example:
-//
-// get_slice_int(8, 1680, 4) =
-//
-//                    11           0
-//                    V            V
-// get_slice_int(8, 0b0110_1001_0000, 4) = 0b0110_1001
-//                    <-------^
-//                    (8 bit) 4
-//
-void get_slice_int(bv_t *rop, const mpz_t len_mpz, const mpz_t n, const mpz_t start_mpz)
-{
-  uint64_t start = mpz_get_ui(start_mpz);
-  uint64_t len = mpz_get_ui(len_mpz);
-
-  mpz_set_ui(*rop->bits, 0ul);
-  rop->len = len;
-
-  for (uint64_t i = 0; i < len; i++) {
-    if (mpz_tstbit(n, i + start)) mpz_setbit(*rop->bits, i);
-  }
-}
-
-// Set slice uses the same indexing scheme as get_slice_int, but it
-// puts a bitvector slice into an integer rather than returning it.
-void set_slice_int(mpz_t *rop,
-		   const mpz_t len_mpz,
-		   const mpz_t n,
-		   const mpz_t start_mpz,
-		   const bv_t slice)
-{
-  uint64_t start = mpz_get_ui(start_mpz);
-
-  mpz_set(*rop, n);
-
-  for (uint64_t i = 0; i < slice.len; i++) {
-    if (mpz_tstbit(*slice.bits, i)) {
-      mpz_setbit(*rop, i + start);
-    } else {
-      mpz_clrbit(*rop, i + start);
-    }
-  }
-}
-
-// This is a bit of a hack to let us optimize away the Align__1
-// function in aarch64.
-void arm_align(bv_t *rop, const bv_t x_bv, const mpz_t y_mpz) {
-  uint64_t x = mpz_get_ui(*x_bv.bits);
-  uint64_t y = mpz_get_ui(y_mpz);
-  uint64_t z = y * (x / y);
-  mp_bitcnt_t n = x_bv.len;
-  mpz_set_ui(*rop->bits, safe_rshift(UINT64_MAX, 64l - (n - 1)) & z);
-  rop->len = n;
-}
-
-void vector_update_subrange_bv_t(bv_t *rop,
-				 const bv_t op,
-				 const mpz_t n_mpz,
-				 const mpz_t m_mpz,
-				 const bv_t slice)
-{
-  uint64_t n = mpz_get_ui(n_mpz);
-  uint64_t m = mpz_get_ui(m_mpz);
-
-  mpz_set(*rop->bits, *op.bits);
-
-  for (uint64_t i = 0; i < n - (m - 1ul); i++) {
-    if (mpz_tstbit(*slice.bits, i)) {
-      mpz_setbit(*rop->bits, i + m);
-    } else {
-      mpz_clrbit(*rop->bits, i + m);
-    }
-  }
-}
-
-void vector_subrange_bv_t(bv_t *rop, const bv_t op, const mpz_t n_mpz, const mpz_t m_mpz)
-{
-  uint64_t n = mpz_get_ui(n_mpz);
-  uint64_t m = mpz_get_ui(m_mpz);
-
-  rop->len = n - (m - 1ul);
-  mpz_fdiv_q_2exp(*rop->bits, *op.bits, m);
-  normalise_bv_t(rop);
-
-  /* mpz_set_ui(*rop->bits, 0ul); */
-  /* rop->len = n - (m - 1ul); */
-
-  /* for (uint64_t i = 0; i < rop->len; i++) { */
-  /*   if (mpz_tstbit(*op.bits, i + m)) { */
-  /*     mpz_setbit(*rop->bits, i); */
-  /*   } else { */
-  /*     mpz_clrbit(*rop->bits, i); */
-  /*   } */
-  /* } */
-}
-
-int bitvector_access(const bv_t op, const mpz_t n_mpz) {
-  uint64_t n = mpz_get_ui(n_mpz);
-  return mpz_tstbit(*op.bits, n);
-}
-
-// Like slice but slices from a hexadecimal string.
-void hex_slice (bv_t *rop, const sail_string hex, const mpz_t len_mpz, const mpz_t start_mpz) {
-  mpz_t op;
-  mpz_init_set_str(op, hex, 0);
-  get_slice_int(rop, len_mpz, op, start_mpz);
-  mpz_clear(op);
-}
-
-void set_slice (bv_t *rop,
-		const mpz_t len_mpz,
-		const mpz_t slen_mpz,
-		const bv_t op,
-		const mpz_t start_mpz,
-		const bv_t slice)
-{
-  uint64_t start = mpz_get_ui(start_mpz);
-
-  mpz_set(*rop->bits, *op.bits);
-  rop->len = op.len;
-
-  for (uint64_t i = 0; i < slice.len; i++) {
-    if (mpz_tstbit(*slice.bits, i)) {
-      mpz_setbit(*rop->bits, i + start);
-    } else {
-      mpz_clrbit(*rop->bits, i + start);
-    }
-  }
-}
-
-// ***** Real number implementation *****
-
-#define REAL_FLOAT
-
-#ifdef REAL_FLOAT
-
-typedef mpf_t real;
-
-#define FLOAT_PRECISION 255
-
-void init_real(real *rop) {
-  mpf_init(*rop);
-}
-
-void reinit_real(real *rop) {
-  mpf_set_ui(*rop, 0);
-}
-
-void clear_real(real *rop) {
-  mpf_clear(*rop);
-}
-
-void set_real(real *rop, const real op) {
-  mpf_set(*rop, op);
-}
-
-void undefined_real(real *rop, unit u) {
-  mpf_set_ui(*rop, 0ul);
-}
-
-void neg_real(real *rop, const real op) {
-  mpf_neg(*rop, op);
-}
-
-void mult_real(real *rop, const real op1, const real op2) {
-  mpf_mul(*rop, op1, op2);
-}
-
-void sub_real(real *rop, const real op1, const real op2) {
-  mpf_sub(*rop, op1, op2);
-}
-
-void add_real(real *rop, const real op1, const real op2) {
-  mpf_add(*rop, op1, op2);
-}
-
-void div_real(real *rop, const real op1, const real op2) {
-  mpf_div(*rop, op1, op2);
-}
-
-void sqrt_real(real *rop, const real op) {
-  mpf_sqrt(*rop, op);
-}
-
-void abs_real(real *rop, const real op) {
-  mpf_abs(*rop, op);
-}
-
-void round_up(mpz_t *rop, const real op) {
-  mpf_t x;
-  mpf_init(x);
-  mpf_ceil(x, op);
-  mpz_set_ui(*rop, mpf_get_ui(x));
-  mpf_clear(x);
-}
-
-void round_down(mpz_t *rop, const real op) {
-  mpf_t x;
-  mpf_init(x);
-  mpf_floor(x, op);
-  mpz_set_ui(*rop, mpf_get_ui(x));
-  mpf_clear(x);
-}
-
-void to_real(real *rop, const mpz_t op) {
-  mpf_set_z(*rop, op);
-}
+/*
+ * Integers can be either stack-allocated as 128-bit integers if
+ * __int128 is available, or use GMP arbitrary precision
+ * integers. This affects the function signatures, so use a macro to
+ * paper over the differences.
+ */
+#ifndef USE_INT128
 
-bool eq_real(const real op1, const real op2) {
-  return mpf_cmp(op1, op2) == 0;
-}
+typedef mpz_t sail_int;
 
-bool lt_real(const real op1, const real op2) {
-  return mpf_cmp(op1, op2) < 0;
-}
+#define SAIL_INT_FUNCTION(fname, rtype, ...) void fname(rtype*, __VA_ARGS__)
 
-bool gt_real(const real op1, const real op2) {
-  return mpf_cmp(op1, op2) > 0;
-}
+SAIL_BUILTIN_TYPE(sail_int);
 
-bool lteq_real(const real op1, const real op2) {
-  return mpf_cmp(op1, op2) <= 0;
-}
+void CREATE_OF(sail_int, mach_int)(sail_int *, const mach_int);
+void RECREATE_OF(sail_int, mach_int)(sail_int *, const mach_int);
 
-bool gteq_real(const real op1, const real op2) {
-  return mpf_cmp(op1, op2) >= 0;
-}
+void CREATE_OF(sail_int, sail_string)(sail_int *, const sail_string);
+void RECREATE_OF(sail_int, sail_string)(mpz_t *, const sail_string);
 
-void real_power(real *rop, const real base, const mpz_t exp) {
-  uint64_t exp_ui = mpz_get_ui(exp);
-  mpf_pow_ui(*rop, base, exp_ui);
-}
+mach_int CONVERT_OF(mach_int, sail_int)(const sail_int);
+void CONVERT_OF(sail_int, mach_int)(sail_int *, const mach_int);
+  
+#else
 
-void init_real_of_sail_string(real *rop, const sail_string op) {
-  // FIXME
-  mpf_init(*rop);
-}
+typedef __int128 sail_int;
+#define SAIL_INT_FUNCTION(fname, rtype, ...) rtype fname(__VA_ARGS__)
 
 #endif
 
-/* ***** Sail memory builtins ***** */
-
-/* We organise memory available to the sail model into a linked list
-   of dynamically allocated MASK + 1 size blocks. The most recently
-   written block is moved to the front of the list, so contiguous
-   accesses should be as fast as possible. */
-
-struct block {
-  uint64_t block_id;
-  uint8_t *mem;
-  struct block *next;
-};
-
-struct block *sail_memory = NULL;
-
-/* Must be one less than a power of two. */
-uint64_t MASK = 0xFFFFFFul;
-
-// All sail vectors are at least 64-bits, but only the bottom 8 bits
-// are used in the second argument.
-void write_mem(uint64_t address, uint64_t byte)
-{
-  //printf("ADDR: %lu, BYTE: %lu\n", address, byte);
-
-  uint64_t mask = address & ~MASK;
-  uint64_t offset = address & MASK;
-
-  struct block *current = sail_memory;
-
-  while (current != NULL) {
-    if (current->block_id == mask) {
-      current->mem[offset] = (uint8_t) byte;
-      return;
-    } else {
-      current = current->next;
-    }
-  }
-
-  /* If we couldn't find a block matching the mask, allocate a new
-     one, write the byte, and put it at the front of the block
-     list. */
-  fprintf(stderr, "[Sail] Allocating new block 0x%" PRIx64 "\n", mask);
-  struct block *new_block = malloc(sizeof(struct block));
-  new_block->block_id = mask;
-  new_block->mem = calloc(MASK + 1, sizeof(uint8_t));
-  new_block->mem[offset] = (uint8_t) byte;
-  new_block->next = sail_memory;
-  sail_memory = new_block;
-}
-
-uint64_t read_mem(uint64_t address)
-{
-  uint64_t mask = address & ~MASK;
-  uint64_t offset = address & MASK;
-
-  struct block *current = sail_memory;
-
-  while (current != NULL) {
-    if (current->block_id == mask) {
-      return (uint64_t) current->mem[offset];
-    } else {
-      current = current->next;
-    }
-  }
-
-  return 0x58;
-}
-
-void kill_mem()
-{
-  while (sail_memory != NULL) {
-    struct block *next = sail_memory->next;
-
-    free(sail_memory->mem);
-    free(sail_memory);
-
-    sail_memory = next;
-  }
-}
-
-// ***** ARM Memory builtins *****
-
-// These memory builtins are intended to match the semantics for the
-// __ReadRAM and __WriteRAM functions in ASL.
-
-unit write_ram(const mpz_t addr_size,     // Either 32 or 64
-	       const mpz_t data_size_mpz, // Number of bytes
-	       const bv_t  hex_ram,       // Currently unused
-	       const bv_t  addr_bv,
-	       const bv_t  data)
-{
-  uint64_t addr = mpz_get_ui(*addr_bv.bits);
-  uint64_t data_size = mpz_get_ui(data_size_mpz);
-
-  mpz_t buf;
-  mpz_init_set(buf, *data.bits);
-
-  uint64_t byte;
-  for(uint64_t i = 0; i < data_size; ++i) {
-    // Take the 8 low bits of buf and write to addr.
-    byte = mpz_get_ui(buf) & 0xFF;
-    write_mem(addr + i, byte);
-
-    // Then shift buf 8 bits right.
-    mpz_fdiv_q_2exp(buf, buf, 8);
-  }
+/*
+ * Comparison operators for integers
+ */
+bool eq_int(const sail_int, const sail_int);
 
-  mpz_clear(buf);
-  return UNIT;
-}
+bool lt(const sail_int, const sail_int);
+bool gt(const sail_int, const sail_int);
+bool lteq(const sail_int, const sail_int);
+bool gteq(const sail_int, const sail_int);
 
-void read_ram(bv_t *data,
-	      const mpz_t addr_size,
-	      const mpz_t data_size_mpz,
-	      const bv_t hex_ram,
-	      const bv_t addr_bv)
-{
-  uint64_t addr = mpz_get_ui(*addr_bv.bits);
-  uint64_t data_size = mpz_get_ui(data_size_mpz);
+/*
+ * Left and right shift for integers
+ */
+SAIL_INT_FUNCTION(shl_int, sail_int, const sail_int, const sail_int);
+SAIL_INT_FUNCTION(shr_int, sail_int, const sail_int, const sail_int);
 
-  mpz_set_ui(*data->bits, 0);
-  data->len = data_size * 8;
+/*
+ * undefined_int and undefined_range can't use the UNDEFINED(TYPE)
+ * macro, because they're slightly magical. They take extra parameters
+ * to ensure that no undefined int can violate any type-guaranteed
+ * constraints.
+ */
+SAIL_INT_FUNCTION(undefined_int, sail_int, const int);
+SAIL_INT_FUNCTION(undefined_range, sail_int, const sail_int, const sail_int);
 
-  mpz_t byte;
-  mpz_init(byte);
-  for(uint64_t i = data_size; i > 0; --i) {
-    mpz_set_ui(byte, read_mem(addr + (i - 1)));
-    mpz_mul_2exp(*data->bits, *data->bits, 8);
-    mpz_add(*data->bits, *data->bits, byte);
-  }
+/*
+ * Arithmetic operations in integers. We include functions for both
+ * truncating towards zero, and rounding towards -infinity (floor) as
+ * fdiv/fmod and tdiv/tmod respectively.
+ */
+SAIL_INT_FUNCTION(add_int, sail_int, const sail_int, const sail_int);
+SAIL_INT_FUNCTION(sub_int, sail_int, const sail_int, const sail_int);
+SAIL_INT_FUNCTION(tdiv_int, sail_int, const sail_int, const sail_int);
+SAIL_INT_FUNCTION(tmod_int, sail_int, const sail_int, const sail_int);
+SAIL_INT_FUNCTION(fdiv_int, sail_int, const sail_int, const sail_int);
+SAIL_INT_FUNCTION(fmod_int, sail_int, const sail_int, const sail_int);
 
-  mpz_clear(byte);
-}
+SAIL_INT_FUNCTION(max_int, sail_int, const sail_int, const sail_int);
+SAIL_INT_FUNCTION(min_int, sail_int, const sail_int, const sail_int);
 
-unit load_raw(uint64_t addr, const sail_string file) {
-  fprintf(stderr, "[Sail] Loading %s from 0x%" PRIx64 " to ", file, addr);
-  FILE *fp = fopen(file, "r");
+SAIL_INT_FUNCTION(neg_int, sail_int, const sail_int);
+SAIL_INT_FUNCTION(abs_int, sail_int, const sail_int);
 
-  uint64_t byte;
-  while ((byte = (uint64_t)fgetc(fp)) != EOF) {
-    write_mem(addr, byte);
-    addr++;
-  }
+SAIL_INT_FUNCTION(pow2, sail_int, const sail_int);
 
-  fprintf(stderr, "0x%" PRIx64 "\n", addr - 1);
+/* ***** Sail bitvectors ***** */
 
-  return UNIT;
-}
+typedef uint64_t mach_bits;
 
-void load_image(char *file) {
-  FILE *fp = fopen(file, "r");
+bool eq_bit(const mach_bits a, const mach_bits b);
 
-  if (!fp) {
-    fprintf(stderr, "Image file %s could not be loaded\n", file);
-    exit(EXIT_FAILURE);
-  }
+typedef struct {
+  mp_bitcnt_t len;
+  mpz_t *bits;
+} sail_bits;
 
-  char *addr = NULL;
-  char *data = NULL;
-  size_t len = 0;
+SAIL_BUILTIN_TYPE(sail_bits);
 
-  while (true) {
-    ssize_t addr_len = getline(&addr, &len, fp);
-    if (addr_len == -1) break;
-    ssize_t data_len = getline(&data, &len, fp);
-    if (data_len == -1) break;
+void CREATE_OF(sail_bits, mach_bits)(sail_bits *,
+				     const mach_bits op,
+				     const mach_bits len,
+				     const bool direction);
 
-    if (!strcmp(addr, "elf_entry\n")) {
-      if (sscanf(data, "%" PRIu64 "\n", &g_elf_entry) != 1) {
-        fprintf(stderr, "Failed to parse elf_entry\n");
-        exit(EXIT_FAILURE);
-      };
-      printf("Elf entry point: %" PRIx64 "\n", g_elf_entry);
-    } else {
-      write_mem((uint64_t) atoll(addr), (uint64_t) atoll(data));
-    }
-  }
+void RECREATE_OF(sail_bits, mach_bits)(sail_bits *,
+				       const mach_bits op,
+				       const mach_bits len,
+				       const bool direction);
 
-  free(addr);
-  free(data);
-  fclose(fp);
-}
+mach_bits CONVERT_OF(mach_bits, sail_bits)(const sail_bits);
 
-// ***** Setup and cleanup functions for library code *****
+void UNDEFINED(sail_bits)(sail_bits *, const sail_int len, const mach_bits bit);
+mach_bits UNDEFINED(mach_bits)(const unit);
 
-static int64_t g_trace_depth;
-static bool g_trace_enabled;
+/* 
+ * Wrapper around >> operator to avoid UB when shift amount is greater
+ * than or equal to 64.
+ */
+mach_bits safe_rshift(const mach_bits, const mach_bits);
 
 /*
- * Bind these functions in Sail to enable and disable tracing:
- *
- * val "enable_tracing" : unit -> unit
- * val "disable_tracing" : unit -> unit
- *
- * Compile with sail -c -c_trace.
+ * Used internally to construct large bitvector literals.
  */
-unit enable_tracing(const unit u)
-{
-  g_trace_depth = 0;
-  g_trace_enabled = true;
-  return UNIT;
-}
-
-unit disable_tracing(const unit u)
-{
-  g_trace_depth = 0;
-  g_trace_enabled = false;
-  return UNIT;
-}
+void append_64(sail_bits *rop, const sail_bits op, const mach_bits chunk);
 
-void trace_bv_t(const bv_t op)
-{
-  if (g_trace_enabled) {
-    if (op.len % 4 == 0) {
-      fputs("0x", stderr);
-      mpz_t buf;
-      mpz_init_set(buf, *op.bits);
+void add_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2);
+void sub_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2);
 
-      char *hex = malloc((op.len / 4) * sizeof(char));
+void add_bits_int(sail_bits *rop, const sail_bits op1, const mpz_t op2);
+void sub_bits_int(sail_bits *rop, const sail_bits op1, const mpz_t op2);
 
-      for (int i = 0; i < op.len / 4; ++i) {
-	char c = (char) ((0xF & mpz_get_ui(buf)) + 0x30);
-	hex[i] = (c < 0x3A) ? c : c + 0x7;
-	mpz_fdiv_q_2exp(buf, buf, 4);
-      }
+void zeros(sail_bits *rop, const sail_int op);
+void zero_extend(sail_bits *rop, const sail_bits op, const sail_int len);
 
-      for (int i = op.len / 4; i > 0; --i) {
-	fputc(hex[i - 1], stderr);
-      }
+void length_sail_bits(sail_int *rop, const sail_bits op);
 
-      free(hex);
-      mpz_clear(buf);
-    } else {
-      fputs("0b", stderr);
-      for (int i = op.len; i > 0; --i) {
-	fputc(mpz_tstbit(*op.bits, i - 1) + 0x30, stderr);
-      }
-    }
-  }
-}
+bool eq_bits(const sail_bits op1, const sail_bits op2);
 
-void trace_uint64_t(const uint64_t x) {
-  if (g_trace_enabled) fprintf(stderr, "0x%" PRIx64, x);
-}
+void vector_subrange_sail_bits(sail_bits *rop,
+			       const sail_bits op,
+			       const sail_int n_mpz,
+			       const sail_int m_mpz);
 
-void trace_sail_string(const sail_string str) {
-  if (g_trace_enabled) fprintf(stderr, "\"%s\"", str);
-}
+void truncate(sail_bits *rop, const sail_bits op, const sail_int len);
 
-void trace_unit(const unit u) {
-  if (g_trace_enabled) fputs("()", stderr);
-}
+mach_bits bitvector_access(const sail_bits op, const sail_int n_mpz);
 
-void trace_mpz_t(const mpz_t op) {
-  if (g_trace_enabled) mpz_out_str(stderr, 10, op);
-}
+void sail_unsigned(sail_int *rop, const sail_bits op);
+void sail_signed(sail_int *rop, const sail_bits op);
 
-void trace_bool(const bool b) {
-  if (g_trace_enabled) {
-    if (b) {
-      fprintf(stderr, "true");
-    } else {
-      fprintf(stderr, "false");
-    }
-  }
-}
+/* ***** Sail reals ***** */
 
-void trace_unknown(void) {
-  if (g_trace_enabled) fputs("?", stderr);
-}
+/* ***** Printing ***** */
 
-void trace_argsep(void) {
-  if (g_trace_enabled) fputs(", ", stderr);
-}
-
-void trace_argend(void) {
-  if (g_trace_enabled) fputs(")\n", stderr);
-}
-
-void trace_retend(void) {
-  if (g_trace_enabled) fputs("\n", stderr);
-}
-
-void trace_start(char *name)
-{
-  if (g_trace_enabled) {
-    fprintf(stderr, "[TRACE] ");
-    for (int64_t i = 0; i < g_trace_depth; ++i) {
-      fprintf(stderr, "%s", "|   ");
-    }
-    fprintf(stderr, "%s(", name);
-  }
-}
-
-void trace_end(void)
-{
-  if (g_trace_enabled) {
-    fprintf(stderr, "[TRACE] ");
-    for (int64_t i = 0; i < g_trace_depth; ++i) {
-      fprintf(stderr, "%s", "|   ");
-    }
-  }
-}
+/* 
+ * Utility function not callable from Sail!
+ */
+void fprint_bits(const sail_string pre,
+		 const sail_bits op,
+		 const sail_string post,
+		 FILE *stream);
 
-// ***** Setup and cleanup functions for library code *****
+unit print_bits(const sail_string str, const sail_bits op);
+unit prerr_bits(const sail_string str, const sail_bits op);
 
-void setup_library(void) {
-  disable_tracing(UNIT);
-  mpf_set_default_prec(FLOAT_PRECISION);
-  mpz_init(sail_lib_tmp1);
-  mpz_init(sail_lib_tmp2);
-}
+unit print(const sail_string str);
+unit print_endline(const sail_string str);
 
-void cleanup_library(void) {
-  mpz_clear(sail_lib_tmp1);
-  mpz_clear(sail_lib_tmp2);
-  kill_mem();
-}
+unit prerr(const sail_string str);
+unit prerr_endline(const sail_string str);
 
-#endif
+unit print_int(const sail_string str, const sail_int op);
+unit prerr_int(const sail_string str, const sail_int op);
diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail
index ad59f50e..cff5d4d3 100644
--- a/lib/vector_dec.sail
+++ b/lib/vector_dec.sail
@@ -121,10 +121,13 @@ val unsigned = {
   ocaml: "uint",
   lem: "uint",
   interpreter: "uint",
-  c: "sail_uint",
+  c: "sail_unsigned",
   coq: "unsigned"
 } : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1)
 
-val signed = "sint" : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1)
+val signed = {
+  c: "sail_signed",
+  _: "sint"
+} : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1)
 
 $endif
diff --git a/src/bytecode_util.ml b/src/bytecode_util.ml
index 96513d7f..05709de9 100644
--- a/src/bytecode_util.ml
+++ b/src/bytecode_util.ml
@@ -161,11 +161,11 @@ and string_of_fragment' ?zencode:(zencode=true) 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_int -> "mpz_t"
+  | CT_bits true -> "bv_t(dec)"
+  | CT_bits false -> "bv_t(inc)"
+  | CT_bits64 (n, true) -> "uint64_t(" ^ string_of_int n ^ ", dec)"
+  | CT_bits64 (n, false) -> "uint64_t(" ^ string_of_int n ^ ", int)"
   | CT_int64 -> "int64_t"
   | CT_bit -> "bit"
   | CT_unit -> "unit"
diff --git a/src/c_backend.ml b/src/c_backend.ml
index 96cd9ed7..7923a49c 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -751,9 +751,9 @@ let initial_ctx env =
 
 let rec ctyp_equal ctyp1 ctyp2 =
   match ctyp1, ctyp2 with
-  | CT_mpz, CT_mpz -> true
-  | CT_bv d1, CT_bv d2 -> d1 = d2
-  | CT_uint64 (m1, d1), CT_uint64 (m2, d2) -> m1 = m2 && d1 = d2
+  | CT_int, CT_int -> true
+  | CT_bits d1, CT_bits d2 -> d1 = d2
+  | CT_bits64 (m1, d1), CT_bits64 (m2, d2) -> m1 = m2 && d1 = d2
   | CT_bit, CT_bit -> true
   | CT_int64, CT_int64 -> true
   | CT_unit, CT_unit -> true
@@ -776,8 +776,8 @@ let rec ctyp_of_typ ctx typ =
   match typ_aux with
   | Typ_id id when string_of_id id = "bit" -> CT_bit
   | Typ_id id when string_of_id id = "bool" -> CT_bool
-  | Typ_id id when string_of_id id = "int" -> CT_mpz
-  | Typ_id id when string_of_id id = "nat" -> CT_mpz
+  | Typ_id id when string_of_id id = "int" -> CT_int
+  | Typ_id id when string_of_id id = "nat" -> CT_int
   | Typ_app (id, _) when string_of_id id = "range" || string_of_id id = "atom" ->
      begin
        match destruct_range Env.empty typ with
@@ -792,8 +792,8 @@ let rec ctyp_of_typ ctx typ =
              if prove ctx.local_env (nc_lteq (nconstant min_int64) n) && prove ctx.local_env (nc_lteq m (nconstant max_int64)) then
                (prerr_endline "yes"; CT_int64)
              else
-               (prerr_endline "no"; CT_mpz)
-          | _ -> CT_mpz
+               (prerr_endline "no"; CT_int)
+          | _ -> CT_int
      end
 
   | Typ_app (id, [Typ_arg_aux (Typ_arg_typ typ, _)]) when string_of_id id = "list" ->
@@ -806,8 +806,8 @@ let rec ctyp_of_typ ctx typ =
      begin
        let direction = match ord with Ord_aux (Ord_dec, _) -> true | Ord_aux (Ord_inc, _) -> false | _ -> assert false in
        match nexp_simp n with
-       | Nexp_aux (Nexp_constant n, _) when Big_int.less_equal n (Big_int.of_int 64) -> CT_uint64 (Big_int.to_int n, direction)
-       | _ -> CT_bv direction
+       | Nexp_aux (Nexp_constant n, _) when Big_int.less_equal n (Big_int.of_int 64) -> CT_bits64 (Big_int.to_int n, direction)
+       | _ -> CT_bits direction
      end
   | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp n, _);
                   Typ_arg_aux (Typ_arg_order ord, _);
@@ -846,8 +846,8 @@ let rec ctyp_of_typ ctx typ =
   | _ -> c_error ~loc:l ("No C type for type " ^ string_of_typ typ)
 
 let rec is_stack_ctyp ctyp = match ctyp with
-  | CT_uint64 _ | CT_int64 | CT_bit | CT_unit | CT_bool | CT_enum _ -> true
-  | CT_bv _ | CT_mpz | CT_real | CT_string | CT_list _ | CT_vector _ -> false
+  | CT_bits64 _ | CT_int64 | CT_bit | CT_unit | CT_bool | CT_enum _ -> true
+  | CT_bits _ | CT_int | CT_real | CT_string | CT_list _ | CT_vector _ -> false
   | CT_struct (_, fields) -> List.for_all (fun (_, ctyp) -> is_stack_ctyp ctyp) fields
   | CT_variant (_, ctors) -> false (* List.for_all (fun (_, ctyp) -> is_stack_ctyp ctyp) ctors *) (*FIXME*)
   | CT_tup ctyps -> List.for_all is_stack_ctyp ctyps
@@ -1184,17 +1184,17 @@ let rec compile_aval ctx = function
 
   | AV_lit (L_aux (L_num n, _), typ) when Big_int.less_equal min_int64 n && Big_int.less_equal n max_int64 ->
      let gs = gensym () in
-     [idecl CT_mpz gs;
-      iinit CT_mpz gs (F_lit (V_int n), CT_int64)],
-     (F_id gs, CT_mpz),
-     [iclear CT_mpz gs]
+     [idecl CT_int gs;
+      iinit CT_int gs (F_lit (V_int n), CT_int64)],
+     (F_id gs, CT_int),
+     [iclear CT_int gs]
 
   | AV_lit (L_aux (L_num n, _), typ) ->
      let gs = gensym () in
-     [idecl CT_mpz gs;
-      iinit CT_mpz gs (F_lit (V_string (Big_int.to_string n)), CT_string)],
-     (F_id gs, CT_mpz),
-     [iclear CT_mpz gs]
+     [idecl CT_int gs;
+      iinit CT_int gs (F_lit (V_string (Big_int.to_string n)), CT_string)],
+     (F_id gs, CT_int),
+     [iclear CT_int gs]
 
   | AV_lit (L_aux (L_zero, _), _) -> [], (F_lit (V_bit Sail_values.B0), CT_bit), []
   | AV_lit (L_aux (L_one, _), _) -> [], (F_lit (V_bit Sail_values.B1), CT_bit), []
@@ -1254,9 +1254,9 @@ let rec compile_aval ctx = function
        let len = List.length avals in
        match destruct_vector ctx.tc_env typ with
        | Some (_, Ord_aux (Ord_inc, _), _) ->
-          [], (bitstring, CT_uint64 (len, false)), []
+          [], (bitstring, CT_bits64 (len, false)), []
        | Some (_, Ord_aux (Ord_dec, _), _) ->
-          [], (bitstring, CT_uint64 (len, true)), []
+          [], (bitstring, CT_bits64 (len, true)), []
        | Some _ ->
           c_error "Encountered order polymorphic bitvector literal"
        | None ->
@@ -1271,14 +1271,14 @@ let rec compile_aval ctx = function
      let first_chunk = bitstring (Util.take (len mod 64) avals) in
      let chunks = Util.drop (len mod 64) avals |> chunkify 64 |> List.map bitstring in
      let gs = gensym () in
-     [idecl (CT_bv true) gs;
-      iinit (CT_bv true) gs (first_chunk, CT_uint64 (len mod 64, true))]
+     [idecl (CT_bits true) gs;
+      iinit (CT_bits true) gs (first_chunk, CT_bits64 (len mod 64, true))]
      @ List.map (fun chunk -> ifuncall (CL_id gs)
                                        (mk_id "append_64")
-                                       [(F_id gs, CT_bv true); (chunk, CT_uint64 (64, true))]
-                                       (CT_bv true)) chunks,
-     (F_id gs, CT_bv true),
-     [iclear (CT_bv true) gs]
+                                       [(F_id gs, CT_bits true); (chunk, CT_bits64 (64, true))]
+                                       (CT_bits true)) chunks,
+     (F_id gs, CT_bits true),
+     [iclear (CT_bits true) gs]
 
   (* If we have a bitvector value, that isn't a literal then we need to set bits individually. *)
   | AV_vector (avals, Typ_aux (Typ_app (id, [_; Typ_arg_aux (Typ_arg_order ord, _); Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id bit_id, _)), _)]), _))
@@ -1290,7 +1290,7 @@ let rec compile_aval ctx = function
        | Ord_aux (Ord_var _, _) -> c_error "Polymorphic vector direction found"
      in
      let gs = gensym () in
-     let ctyp = CT_uint64 (len, direction) in
+     let ctyp = CT_bits64 (len, direction) in
      let mask i = V_bits (Util.list_init (63 - i) (fun _ -> Sail_values.B0) @ [Sail_values.B1] @ Util.list_init i (fun _ -> Sail_values.B0)) in
      let aval_mask i aval =
        let setup, cval, cleanup = compile_aval ctx aval in
@@ -2304,7 +2304,7 @@ let rec instrs_rename from_id to_id =
   | [] -> []
 
 let hoist_ctyp = function
-  | CT_mpz | CT_bv _ | CT_struct _ -> true
+  | CT_int | CT_bits _ | CT_struct _ -> true
   | _ -> false
 
 let hoist_counter = ref 0
@@ -2497,12 +2497,12 @@ let upper_codegen_id id = string (upper_sgen_id id)
 
 let rec sgen_ctyp = function
   | CT_unit -> "unit"
-  | CT_bit -> "uint64_t"
+  | CT_bit -> "mach_bits"
   | CT_bool -> "bool"
-  | CT_uint64 _ -> "uint64_t"
-  | CT_int64 -> "int64_t"
-  | CT_mpz -> "mpz_t"
-  | CT_bv _ -> "bv_t"
+  | CT_bits64 _ -> "mach_bits"
+  | CT_int64 -> "mach_int"
+  | CT_int -> "sail_int"
+  | CT_bits _ -> "sail_bits"
   | CT_tup _ as tup -> "struct " ^ Util.zencode_string ("tuple_" ^ string_of_ctyp tup)
   | CT_struct (id, _) -> "struct " ^ sgen_id id
   | CT_enum (id, _) -> "enum " ^ sgen_id id
@@ -2515,12 +2515,12 @@ let rec sgen_ctyp = function
 
 let rec sgen_ctyp_name = function
   | CT_unit -> "unit"
-  | CT_bit -> "uint64_t"
+  | CT_bit -> "mach_bits"
   | CT_bool -> "bool"
-  | CT_uint64 _ -> "uint64_t"
-  | CT_int64 -> "int64_t"
-  | CT_mpz -> "mpz_t"
-  | CT_bv _ -> "bv_t"
+  | CT_bits64 _ -> "mach_bits"
+  | CT_int64 -> "mach_int"
+  | CT_int -> "sail_int"
+  | CT_bits _ -> "sail_bits"
   | CT_tup _ as tup -> Util.zencode_string ("tuple_" ^ string_of_ctyp tup)
   | CT_struct (id, _) -> sgen_id id
   | CT_enum (id, _) -> sgen_id id
@@ -2533,9 +2533,9 @@ let rec sgen_ctyp_name = function
 
 let sgen_cval_param (frag, ctyp) =
   match ctyp with
-  | CT_bv direction ->
+  | CT_bits direction ->
      string_of_fragment frag ^ ", " ^ string_of_bool direction
-  | CT_uint64 (len, direction) ->
+  | CT_bits64 (len, direction) ->
      string_of_fragment frag ^ ", " ^ string_of_int len ^ "ul , " ^ string_of_bool direction
   | _ ->
      string_of_fragment frag
@@ -2567,7 +2567,7 @@ let rec codegen_instr fid ctx (I_aux (instr, _)) =
      if is_stack_ctyp ctyp then
        string (Printf.sprintf "  %s = %s;" (sgen_clexp_pure clexp) (sgen_cval cval))
      else
-       string (Printf.sprintf "  set_%s(%s, %s);" (sgen_ctyp_name ctyp) (sgen_clexp clexp) (sgen_cval cval))
+       string (Printf.sprintf "  COPY(%s)(%s, %s);" (sgen_ctyp_name ctyp) (sgen_clexp clexp) (sgen_cval cval))
   | I_jump (cval, label) ->
      string (Printf.sprintf "  if (%s) goto %s;" (sgen_cval cval) label)
   | I_if (cval, [then_instr], [], ctyp) ->
@@ -2620,43 +2620,44 @@ let rec codegen_instr fid ctx (I_aux (instr, _)) =
           end
        | "vector_update_subrange", _ -> Printf.sprintf "vector_update_subrange_%s" (sgen_ctyp_name ctyp)
        | "vector_subrange", _ -> Printf.sprintf "vector_subrange_%s" (sgen_ctyp_name ctyp)
-       | "vector_update", CT_uint64 _ -> "update_uint64_t"
-       | "vector_update", CT_bv _ -> "update_bv"
+       | "vector_update", CT_bits64 _ -> "update_uint64_t"
+       | "vector_update", CT_bits _ -> "update_bv"
        | "vector_update", _ -> Printf.sprintf "vector_update_%s" (sgen_ctyp_name ctyp)
        | "internal_vector_update", _ -> Printf.sprintf "internal_vector_update_%s" (sgen_ctyp_name ctyp)
        | "internal_vector_init", _ -> Printf.sprintf "internal_vector_init_%s" (sgen_ctyp_name ctyp)
-       | "undefined_vector", CT_uint64 _ -> "undefined_uint64_t"
-       | "undefined_vector", CT_bv _ -> "undefined_bv_t"
-       | "undefined_vector", _ -> Printf.sprintf "undefined_vector_%s" (sgen_ctyp_name ctyp)
+       | "undefined_vector", CT_bits64 _ -> "UNDEFINED(mach_bits)"
+       | "undefined_vector", CT_bits _ -> "UNDEFINED(sail_bits)"
+       | "undefined_bit", _ -> "UNDEFINED(mach_bits)"
+       | "undefined_vector", _ -> Printf.sprintf "UNDEFINED(vector_%s)" (sgen_ctyp_name ctyp)
        | fname, _ -> fname
      in
      if fname = "reg_deref" then
        if is_stack_ctyp ctyp then
          string (Printf.sprintf  " %s = *(%s);" (sgen_clexp_pure x) c_args)
        else
-         string (Printf.sprintf  " set_%s(&%s, *(%s));" (sgen_ctyp_name ctyp) (sgen_clexp_pure x) c_args)
+         string (Printf.sprintf  " COPY(%s)(&%s, *(%s));" (sgen_ctyp_name ctyp) (sgen_clexp_pure x) c_args)
      else if is_stack_ctyp ctyp then
        string (Printf.sprintf "  %s = %s(%s);" (sgen_clexp_pure x) fname c_args)
      else
        string (Printf.sprintf "  %s(%s, %s);" fname (sgen_clexp x) c_args)
   | I_clear (ctyp, id) ->
-     string (Printf.sprintf "  clear_%s(&%s);" (sgen_ctyp_name ctyp) (sgen_id id))
+     string (Printf.sprintf "  KILL(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id))
   | I_init (ctyp, id, cval) ->
-     string (Printf.sprintf "  init_%s_of_%s(&%s, %s);"
+     string (Printf.sprintf "  CREATE_OF(%s, %s)(&%s, %s);"
                             (sgen_ctyp_name ctyp)
                             (sgen_ctyp_name (cval_ctyp cval))
                             (sgen_id id)
                             (sgen_cval_param cval))
   | I_alloc (ctyp, id) ->
-     string (Printf.sprintf "  init_%s(&%s);" (sgen_ctyp_name ctyp) (sgen_id id))
+     string (Printf.sprintf "  CREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id))
   | I_reinit (ctyp, id, cval) ->
-     string (Printf.sprintf "  reinit_%s_of_%s(&%s, %s);"
+     string (Printf.sprintf "  RECREATE_OF(%s, %s)(&%s, %s);"
                             (sgen_ctyp_name ctyp)
                             (sgen_ctyp_name (cval_ctyp cval))
                             (sgen_id id)
                             (sgen_cval_param cval))
   | I_reset (ctyp, id) ->
-     string (Printf.sprintf "  reinit_%s(&%s);" (sgen_ctyp_name ctyp) (sgen_id id))
+     string (Printf.sprintf "  RECREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id))
   (* FIXME: This just covers the cases we see in our specs, need a
      special conversion code-generator for full generality *)
   | I_convert (x, CT_tup ctyps1, y, CT_tup ctyps2) when List.length ctyps1 = List.length ctyps2 ->
@@ -2666,7 +2667,7 @@ let rec codegen_instr fid ctx (I_aux (instr, _)) =
        else if ctyp_equal ctyp1 ctyp2 then
          c_error "heap tuple type conversion"
        else if is_stack_ctyp ctyp1 then
-         string (Printf.sprintf "  %s.ztup%i = convert_%s_of_%s(%s.ztup%i);"
+         string (Printf.sprintf "  %s.ztup%i = CONVERT_OF(%s, %s)(%s.ztup%i);"
                                 (sgen_clexp_pure x)
                                 i
                                 (sgen_ctyp_name ctyp1)
@@ -2674,7 +2675,7 @@ let rec codegen_instr fid ctx (I_aux (instr, _)) =
                                 (sgen_id y)
                                 i)
        else
-         string (Printf.sprintf "  convert_%s_of_%s(%s.ztup%i, %s.ztup%i);"
+         string (Printf.sprintf "  CONVERT_OF(%s, %s)(%s.ztup%i, %s.ztup%i);"
                                 (sgen_ctyp_name ctyp1)
                                 (sgen_ctyp_name ctyp2)
                                 (sgen_clexp x)
@@ -2685,13 +2686,13 @@ let rec codegen_instr fid ctx (I_aux (instr, _)) =
      separate hardline (List.mapi convert (List.map2 (fun x y -> (x, y)) ctyps1 ctyps2))
   | I_convert (x, ctyp1, y, ctyp2) ->
      if is_stack_ctyp ctyp1 then
-       string (Printf.sprintf "  %s = convert_%s_of_%s(%s);"
+       string (Printf.sprintf "  %s = CONVERT_OF(%s, %s)(%s);"
                  (sgen_clexp_pure x)
                  (sgen_ctyp_name ctyp1)
                  (sgen_ctyp_name ctyp2)
                  (sgen_id y))
      else
-       string (Printf.sprintf "  convert_%s_of_%s(%s, %s);"
+       string (Printf.sprintf "  CONVERT_OF(%s, %s)(%s, %s);"
                  (sgen_ctyp_name ctyp1)
                  (sgen_ctyp_name ctyp2)
                  (sgen_clexp x)
@@ -2699,7 +2700,7 @@ let rec codegen_instr fid ctx (I_aux (instr, _)) =
   | I_return cval ->
      string (Printf.sprintf "  return %s;" (sgen_cval cval))
   | I_throw cval ->
-     string (Printf.sprintf "  THROW(%s)" (sgen_cval cval))
+     c_error "I_throw reached code generator"
   | I_comment str ->
      string ("  /* " ^ str ^ " */")
   | I_label str ->
@@ -2728,10 +2729,10 @@ let codegen_type_def ctx = function
        if is_stack_ctyp ctyp then
          string (Printf.sprintf "rop->%s = op.%s;" (sgen_id id) (sgen_id id))
        else
-         string (Printf.sprintf "set_%s(&rop->%s, op.%s);" (sgen_ctyp_name ctyp) (sgen_id id) (sgen_id id))
+         string (Printf.sprintf "COPY(%s)(&rop->%s, op.%s);" (sgen_ctyp_name ctyp) (sgen_id id) (sgen_id id))
      in
      let codegen_setter id ctors =
-       string (let n = sgen_id id in Printf.sprintf "void set_%s(struct %s *rop, const struct %s op)" n n n) ^^ space
+       string (let n = sgen_id id in Printf.sprintf "void COPY(%s)(struct %s *rop, const struct %s op)" n n n) ^^ space
        ^^ surround 2 0 lbrace
                    (separate_map hardline codegen_set (Bindings.bindings ctors))
                    rbrace
@@ -2739,11 +2740,11 @@ let codegen_type_def ctx = function
      (* Generate an init/clear_T function for every struct T *)
      let codegen_field_init f (id, ctyp) =
        if not (is_stack_ctyp ctyp) then
-         [string (Printf.sprintf "%s_%s(&op->%s);" f (sgen_ctyp_name ctyp) (sgen_id id))]
+         [string (Printf.sprintf "%s(%s)(&op->%s);" f (sgen_ctyp_name ctyp) (sgen_id id))]
        else []
      in
      let codegen_init f id ctors =
-       string (let n = sgen_id id in Printf.sprintf "void %s_%s(struct %s *op)" f n n) ^^ space
+       string (let n = sgen_id id in Printf.sprintf "void %s(%s)(struct %s *op)" f n n) ^^ space
        ^^ surround 2 0 lbrace
                    (separate hardline (Bindings.bindings ctors |> List.map (codegen_field_init f) |> List.concat))
                    rbrace
@@ -2763,11 +2764,11 @@ let codegen_type_def ctx = function
      ^^ semi ^^ twice hardline
      ^^ codegen_setter id (ctor_bindings ctors)
      ^^ twice hardline
-     ^^ codegen_init "init" id (ctor_bindings ctors)
+     ^^ codegen_init "CREATE" id (ctor_bindings ctors)
      ^^ twice hardline
-     ^^ codegen_init "reinit" id (ctor_bindings ctors)
+     ^^ codegen_init "RECREATE" id (ctor_bindings ctors)
      ^^ twice hardline
-     ^^ codegen_init "clear" id (ctor_bindings ctors)
+     ^^ codegen_init "KILL" id (ctor_bindings ctors)
      ^^ twice hardline
      ^^ codegen_eq
 
@@ -2790,28 +2791,28 @@ let codegen_type_def ctx = function
      let codegen_init =
        let n = sgen_id id in
        let ctor_id, ctyp = List.hd tus in
-       string (Printf.sprintf "void init_%s(struct %s *op)" n n)
+       string (Printf.sprintf "void CREATE(%s)(struct %s *op)" n n)
        ^^ hardline
        ^^ surround 2 0 lbrace
                    (string (Printf.sprintf "op->kind = Kind_%s;" (sgen_id ctor_id)) ^^ hardline
                     ^^ if not (is_stack_ctyp ctyp) then
-                         string (Printf.sprintf "init_%s(&op->%s);" (sgen_ctyp_name ctyp) (sgen_id ctor_id))
+                         string (Printf.sprintf "CREATE(%s)(&op->%s);" (sgen_ctyp_name ctyp) (sgen_id ctor_id))
                        else empty)
                    rbrace
      in
      let codegen_reinit =
        let n = sgen_id id in
-       string (Printf.sprintf "void reinit_%s(struct %s *op) {}" n n)
+       string (Printf.sprintf "void RECREATE(%s)(struct %s *op) {}" n n)
      in
      let clear_field v ctor_id ctyp =
        if is_stack_ctyp ctyp then
          string (Printf.sprintf "/* do nothing */")
        else
-         string (Printf.sprintf "clear_%s(&%s->%s);" (sgen_ctyp_name ctyp) v (sgen_id ctor_id))
+         string (Printf.sprintf "KILL(%s)(&%s->%s);" (sgen_ctyp_name ctyp) v (sgen_id ctor_id))
      in
      let codegen_clear =
        let n = sgen_id id in
-       string (Printf.sprintf "void clear_%s(struct %s *op)" n n) ^^ hardline
+       string (Printf.sprintf "void KILL(%s)(struct %s *op)" n n) ^^ hardline
        ^^ surround 2 0 lbrace
                    (each_ctor "op->" (clear_field "op") tus ^^ semi)
                    rbrace
@@ -2828,7 +2829,7 @@ let codegen_type_def ctx = function
          | CT_tup ctyps ->
             String.concat ", " (List.mapi (fun i ctyp -> Printf.sprintf "%s op%d" (sgen_ctyp ctyp) i) ctyps),
             string (Printf.sprintf "%s op;" (sgen_ctyp ctyp)) ^^ hardline
-            ^^ string (Printf.sprintf "init_%s(&op);" (sgen_ctyp_name ctyp)) ^^ hardline
+            ^^ string (Printf.sprintf "CREATE(%s)(&op);" (sgen_ctyp_name ctyp)) ^^ hardline
             ^^ separate hardline (List.mapi tuple_set ctyps) ^^ hardline
          | ctyp -> Printf.sprintf "%s op" (sgen_ctyp ctyp), empty
        in
@@ -2840,8 +2841,8 @@ let codegen_type_def ctx = function
                     ^^ if is_stack_ctyp ctyp then
                          string (Printf.sprintf "rop->%s = op;" (sgen_id ctor_id))
                        else
-                         string (Printf.sprintf "init_%s(&rop->%s);" (sgen_ctyp_name ctyp) (sgen_id ctor_id)) ^^ hardline
-                         ^^ string (Printf.sprintf "set_%s(&rop->%s, op);" (sgen_ctyp_name ctyp) (sgen_id ctor_id)))
+                         string (Printf.sprintf "CREATE(%s)(&rop->%s);" (sgen_ctyp_name ctyp) (sgen_id ctor_id)) ^^ hardline
+                         ^^ string (Printf.sprintf "COPY(%s)(&rop->%s, op);" (sgen_ctyp_name ctyp) (sgen_id ctor_id)))
                    rbrace
      in
      let codegen_setter =
@@ -2850,10 +2851,10 @@ let codegen_type_def ctx = function
          if is_stack_ctyp ctyp then
            string (Printf.sprintf "rop->%s = op.%s;" (sgen_id ctor_id) (sgen_id ctor_id))
          else
-           string (Printf.sprintf "init_%s(&rop->%s);" (sgen_ctyp_name ctyp) (sgen_id ctor_id))
-           ^^ string (Printf.sprintf " set_%s(&rop->%s, op.%s);" (sgen_ctyp_name ctyp) (sgen_id ctor_id) (sgen_id ctor_id))
+           string (Printf.sprintf "CREATE(%s)(&rop->%s);" (sgen_ctyp_name ctyp) (sgen_id ctor_id))
+           ^^ string (Printf.sprintf " COPY(%s)(&rop->%s, op.%s);" (sgen_ctyp_name ctyp) (sgen_id ctor_id) (sgen_id ctor_id))
        in
-       string (Printf.sprintf "void set_%s(struct %s *rop, struct %s op)" n n n) ^^ hardline
+       string (Printf.sprintf "void COPY(%s)(struct %s *rop, struct %s op)" n n n) ^^ hardline
        ^^ surround 2 0 lbrace
                    (each_ctor "rop->" (clear_field "rop") tus
                     ^^ semi ^^ hardline
@@ -2935,14 +2936,14 @@ let codegen_node id ctyp =
   ^^ string (Printf.sprintf "typedef struct node_%s *%s;" (sgen_id id) (sgen_id id))
 
 let codegen_list_init id =
-  string (Printf.sprintf "void init_%s(%s *rop) { *rop = NULL; }" (sgen_id id) (sgen_id id))
+  string (Printf.sprintf "void CREATE(%s)(%s *rop) { *rop = NULL; }" (sgen_id id) (sgen_id id))
 
 let codegen_list_clear id ctyp =
-  string (Printf.sprintf "void clear_%s(%s *rop) {\n" (sgen_id id) (sgen_id id))
+  string (Printf.sprintf "void KILL(%s)(%s *rop) {\n" (sgen_id id) (sgen_id id))
   ^^ string (Printf.sprintf "  if (*rop == NULL) return;")
   ^^ (if is_stack_ctyp ctyp then empty
-      else string (Printf.sprintf "  clear_%s(&(*rop)->hd);\n" (sgen_ctyp_name ctyp)))
-  ^^ string (Printf.sprintf "  clear_%s(&(*rop)->tl);\n" (sgen_id id))
+      else string (Printf.sprintf "  KILL(%s)(&(*rop)->hd);\n" (sgen_ctyp_name ctyp)))
+  ^^ string (Printf.sprintf "  KILL(%s)(&(*rop)->tl);\n" (sgen_id id))
   ^^ string "  free(*rop);"
   ^^ string "}"
 
@@ -2953,13 +2954,13 @@ let codegen_list_set id ctyp =
   ^^ (if is_stack_ctyp ctyp then
         string "  (*rop)->hd = op->hd;\n"
       else
-        string (Printf.sprintf "  init_%s(&(*rop)->hd);\n" (sgen_ctyp_name ctyp))
-        ^^ string (Printf.sprintf "  set_%s(&(*rop)->hd, op->hd);\n" (sgen_ctyp_name ctyp)))
+        string (Printf.sprintf "  CREATE(%s)(&(*rop)->hd);\n" (sgen_ctyp_name ctyp))
+        ^^ string (Printf.sprintf "  COPY(%s)(&(*rop)->hd, op->hd);\n" (sgen_ctyp_name ctyp)))
   ^^ string (Printf.sprintf "  internal_set_%s(&(*rop)->tl, op->tl);\n" (sgen_id id))
   ^^ string "}"
   ^^ twice hardline
-  ^^ string (Printf.sprintf "void set_%s(%s *rop, const %s op) {\n" (sgen_id id) (sgen_id id) (sgen_id id))
-  ^^ string (Printf.sprintf "  clear_%s(rop);\n" (sgen_id id))
+  ^^ string (Printf.sprintf "void COPY(%s)(%s *rop, const %s op) {\n" (sgen_id id) (sgen_id id) (sgen_id id))
+  ^^ string (Printf.sprintf "  KILL(%s)(rop);\n" (sgen_id id))
   ^^ string (Printf.sprintf "  internal_set_%s(rop, op);\n" (sgen_id id))
   ^^ string "}"
 
@@ -2970,8 +2971,8 @@ let codegen_cons id ctyp =
   ^^ (if is_stack_ctyp ctyp then
         string "  (*rop)->hd = x;\n"
       else
-        string (Printf.sprintf "  init_%s(&(*rop)->hd);\n" (sgen_ctyp_name ctyp))
-        ^^ string (Printf.sprintf "  set_%s(&(*rop)->hd, x);\n" (sgen_ctyp_name ctyp)))
+        string (Printf.sprintf "  CREATE(%s)(&(*rop)->hd);\n" (sgen_ctyp_name ctyp))
+        ^^ string (Printf.sprintf "  COPY(%s)(&(*rop)->hd, x);\n" (sgen_ctyp_name ctyp)))
   ^^ string "  (*rop)->tl = xs;\n"
   ^^ string "}"
 
@@ -2979,7 +2980,7 @@ let codegen_pick id ctyp =
   if is_stack_ctyp ctyp then
     string (Printf.sprintf "%s pick_%s(const %s xs) { return xs->hd; }" (sgen_ctyp ctyp) (sgen_ctyp_name ctyp) (sgen_id id))
   else
-    string (Printf.sprintf "void pick_%s(%s *x, const %s xs) { set_%s(x, xs->hd); }" (sgen_ctyp_name ctyp) (sgen_ctyp ctyp) (sgen_id id) (sgen_ctyp_name ctyp))
+    string (Printf.sprintf "void pick_%s(%s *x, const %s xs) { COPY(%s)(x, xs->hd); }" (sgen_ctyp_name ctyp) (sgen_ctyp ctyp) (sgen_id id) (sgen_ctyp_name ctyp))
 
 let codegen_list ctx ctyp =
   let id = mk_id (string_of_ctyp (CT_list ctyp)) in
@@ -3007,27 +3008,27 @@ let codegen_vector ctx (direction, ctyp) =
       ^^ string (Printf.sprintf "typedef struct %s %s;" (sgen_id id) (sgen_id id))
     in
     let vector_init =
-      string (Printf.sprintf "void init_%s(%s *rop) {\n  rop->len = 0;\n  rop->data = NULL;\n}" (sgen_id id) (sgen_id id))
+      string (Printf.sprintf "void CREATE(%s)(%s *rop) {\n  rop->len = 0;\n  rop->data = NULL;\n}" (sgen_id id) (sgen_id id))
     in
     let vector_set =
-      string (Printf.sprintf "void set_%s(%s *rop, %s op) {\n" (sgen_id id) (sgen_id id) (sgen_id id))
-      ^^ string (Printf.sprintf "  clear_%s(rop);\n" (sgen_id id))
+      string (Printf.sprintf "void COPY(%s)(%s *rop, %s op) {\n" (sgen_id id) (sgen_id id) (sgen_id id))
+      ^^ string (Printf.sprintf "  KILL(%s)(rop);\n" (sgen_id id))
       ^^ string "  rop->len = op.len;\n"
       ^^ string (Printf.sprintf "  rop->data = malloc((rop->len) * sizeof(%s));\n" (sgen_ctyp ctyp))
       ^^ string "  for (int i = 0; i < op.len; i++) {\n"
       ^^ string (if is_stack_ctyp ctyp then
                    "    (rop->data)[i] = op.data[i];\n"
                  else
-                   Printf.sprintf "    init_%s((rop->data) + i);\n    set_%s((rop->data) + i, op.data[i]);\n" (sgen_ctyp_name ctyp) (sgen_ctyp_name ctyp))
+                   Printf.sprintf "    CREATE(%s)((rop->data) + i);\n    COPY(%s)((rop->data) + i, op.data[i]);\n" (sgen_ctyp_name ctyp) (sgen_ctyp_name ctyp))
       ^^ string "  }\n"
       ^^ string "}"
     in
     let vector_clear =
-      string (Printf.sprintf "void clear_%s(%s *rop) {\n" (sgen_id id) (sgen_id id))
+      string (Printf.sprintf "void KILL(%s)(%s *rop) {\n" (sgen_id id) (sgen_id id))
       ^^ (if is_stack_ctyp ctyp then empty
          else
            string "  for (int i = 0; i < (rop->len); i++) {\n"
-           ^^ string (Printf.sprintf "    clear_%s((rop->data) + i);\n" (sgen_ctyp_name ctyp))
+           ^^ string (Printf.sprintf "    KILL(%s)((rop->data) + i);\n" (sgen_ctyp_name ctyp))
            ^^ string "  }\n")
       ^^ string "  if (rop->data != NULL) free(rop->data);\n"
       ^^ string "}"
@@ -3039,13 +3040,13 @@ let codegen_vector ctx (direction, ctyp) =
       ^^ string (if is_stack_ctyp ctyp then
                    "    rop->data[m] = elem;\n"
                  else
-                   Printf.sprintf "  set_%s((rop->data) + m, elem);\n" (sgen_ctyp_name ctyp))
+                   Printf.sprintf "  COPY(%s)((rop->data) + m, elem);\n" (sgen_ctyp_name ctyp))
       ^^ string "  } else {\n"
-      ^^ string (Printf.sprintf "    set_%s(rop, op);\n" (sgen_id id))
+      ^^ string (Printf.sprintf "    COPY(%s)(rop, op);\n" (sgen_id id))
       ^^ string (if is_stack_ctyp ctyp then
                    "    rop->data[m] = elem;\n"
                  else
-                   Printf.sprintf "  set_%s((rop->data) + m, elem);\n" (sgen_ctyp_name ctyp))
+                   Printf.sprintf "  COPY(%s)((rop->data) + m, elem);\n" (sgen_ctyp_name ctyp))
       ^^ string "  }\n"
       ^^ string "}"
     in
@@ -3054,7 +3055,7 @@ let codegen_vector ctx (direction, ctyp) =
       ^^ string (if is_stack_ctyp ctyp then
                    "  rop->data[n] = elem;\n"
                  else
-                   Printf.sprintf "  set_%s((rop->data) + n, elem);\n" (sgen_ctyp_name ctyp))
+                   Printf.sprintf "  COPY(%s)((rop->data) + n, elem);\n" (sgen_ctyp_name ctyp))
       ^^ string "}"
     in
     let vector_access =
@@ -3066,7 +3067,7 @@ let codegen_vector ctx (direction, ctyp) =
       else
         string (Printf.sprintf "void vector_access_%s(%s *rop, %s op, mpz_t n) {\n" (sgen_id id) (sgen_ctyp ctyp) (sgen_id id))
         ^^ string "  int m = mpz_get_ui(n);\n"
-        ^^ string (Printf.sprintf "  set_%s(rop, op.data[m]);\n" (sgen_ctyp_name ctyp))
+        ^^ string (Printf.sprintf "  COPY(%s)(rop, op.data[m]);\n" (sgen_ctyp_name ctyp))
         ^^ string "}"
     in
     let internal_vector_init =
@@ -3083,7 +3084,7 @@ let codegen_vector ctx (direction, ctyp) =
       ^^ string (if is_stack_ctyp ctyp then
                    "    (rop->data)[i] = elem;\n"
                  else
-                   Printf.sprintf "    init_%s((rop->data) + i);\n    set_%s((rop->data) + i, elem);\n" (sgen_ctyp_name ctyp) (sgen_ctyp_name ctyp))
+                   Printf.sprintf "    CREATE(%s)((rop->data) + i);\n    COPY(%s)((rop->data) + i, elem);\n" (sgen_ctyp_name ctyp) (sgen_ctyp_name ctyp))
       ^^ string "  }\n"
       ^^ string "}"
     in
@@ -3152,11 +3153,9 @@ let codegen_def' ctx = function
           ^^ hardline
      in
      function_header
-     (* ^^ string (Printf.sprintf "{ fprintf(stderr, \"%s \"); " (string_of_id id)) *)
      ^^ string "{"
      ^^ jump 0 2 (separate_map hardline (codegen_instr id ctx) instrs) ^^ hardline
      ^^ string "}"
-     (* ^^ string "}" *)
 
   | CDEF_type ctype_def ->
      codegen_type_def ctx ctype_def
@@ -3290,6 +3289,7 @@ let instrument_tracing ctx =
 let bytecode_ast ctx rewrites (Defs defs) =
   let assert_vs = Initial_check.extern_of_string dec_ord (mk_id "sail_assert") "(bool, string) -> unit effect {escape}" in
   let exit_vs = Initial_check.extern_of_string dec_ord (mk_id "sail_exit") "unit -> unit effect {escape}" in
+  
   let ctx = { ctx with tc_env = snd (Type_error.check ctx.tc_env (Defs [assert_vs; exit_vs])) } in
   let chunks, ctx = List.fold_left (fun (chunks, ctx) def -> let defs, ctx = compile_def ctx def in defs :: chunks, ctx) ([], ctx) defs in
   let cdefs = List.concat (List.rev chunks) in
@@ -3314,18 +3314,19 @@ let compile_ast ctx (Defs defs) =
     let ctx = { ctx with tc_env = snd (Type_error.check ctx.tc_env (Defs [assert_vs; exit_vs])) } in
     let chunks, ctx = List.fold_left (fun (chunks, ctx) def -> let defs, ctx = compile_def ctx def in defs :: chunks, ctx) ([], ctx) defs in
     let cdefs = List.concat (List.rev chunks) in
-    let cdefs = List.map (instrument_tracing ctx) (optimize ctx cdefs) in
+    let cdefs = optimize ctx cdefs in
     let docs = List.map (codegen_def ctx) cdefs in
 
     let preamble = separate hardline
-                            [ string "#include \"sail.h\"" ]
+                     [ string "#include \"sail.h\"";
+                       string "#include \"rts.h\""]
     in
 
     let exn_boilerplate =
       if not (Bindings.mem (mk_id "exception") ctx.variants) then ([], []) else
         ([ "  current_exception = malloc(sizeof(struct zexception));";
-           "  init_zexception(current_exception);" ],
-         [ "  clear_zexception(current_exception);";
+           "  CREATE(zexception)(current_exception);" ],
+         [ "  KILL(zexception)(current_exception);";
            "  free(current_exception);";
            "  if (have_exception) fprintf(stderr, \"Exiting due to uncaught exception\\n\");" ])
     in
@@ -3349,15 +3350,15 @@ let compile_ast ctx (Defs defs) =
       if is_stack_ctyp ctyp then
         [], []
       else
-        [ Printf.sprintf "  init_%s(&%s);" (sgen_ctyp_name ctyp) (sgen_id id) ],
-        [ Printf.sprintf "  clear_%s(&%s);" (sgen_ctyp_name ctyp) (sgen_id id) ]
+        [ Printf.sprintf "  CREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id) ],
+        [ Printf.sprintf "  KILL(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id) ]
     in
 
     let postamble = separate hardline (List.map string
        ( [ "int main(int argc, char *argv[])";
            "{";
            "  if (argc > 1) { load_image(argv[1]); }";
-           "  setup_library();" ]
+           "  setup_rts();" ]
        @ fst exn_boilerplate
        @ startup cdefs
        @ List.concat (List.map (fun r -> fst (register_init_clear r)) regs)
@@ -3368,7 +3369,7 @@ let compile_ast ctx (Defs defs) =
        @ List.concat (List.map (fun r -> snd (register_init_clear r)) regs)
        @ finish cdefs
        @ snd exn_boilerplate
-       @ [ "  cleanup_library();";
+       @ [ "  cleanup_rts();";
            "  return EXIT_SUCCESS;";
            "}" ] ))
     in
diff --git a/test/c/run_tests.sh b/test/c/run_tests.sh
index 0990938d..b1ead724 100755
--- a/test/c/run_tests.sh
+++ b/test/c/run_tests.sh
@@ -54,7 +54,7 @@ function run_c_tests {
 	if $SAILDIR/sail -no_warn -c $SAIL_OPTS $file 1> ${file%.sail}.c 2> /dev/null;
 	then
 	    green "compiling $(basename $file) ($SAIL_OPTS)" "ok";
-	    if gcc $CC_OPTS ${file%.sail}.c -lgmp -I $SAILDIR/lib;
+	    if gcc $CC_OPTS ${file%.sail}.c $SAILDIR/lib/*.c -lgmp -I $SAILDIR/lib;
 	    then
 		green "compiling $(basename ${file%.sail}.c) ($CC_OPTS)" "ok";
 		$DIR/a.out 1> ${file%.sail}.result 2> /dev/null;