Fixes for C RTS for aarch64 no it's split into multiple files

Fix a bug involving indentifers on the left hand side of assignment
statements not being shadowed correctly within foreach loops.

Make the different between different types of integer division
explicit in at least the C compilation for now. fdiv_int is division
rounding towards -infinity (floor). while tdiv_int is truncating
towards zero. Same for fmod_int and tmod_int.

10 files changed, 584 insertions, 29 deletions

diff --git a/lib/arith.sail b/lib/arith.sail
index f713805a..e5d2d6ea 100644
--- a/lib/arith.sail
+++ b/lib/arith.sail
@@ -54,7 +54,7 @@ val div_int = {
   smt: "div",
   ocaml: "quotient",
   lem: "integerDiv",
-  c: "div_int",
+  c: "tdiv_int",
   coq: "Z.quot"
 } : (int, int) -> int
 
@@ -64,7 +64,7 @@ val mod_int = {
   smt: "mod",
   ocaml: "modulus",
   lem: "integerMod",
-  c: "mod_int",
+  c: "tmod_int",
   coq: "Z.rem"
 } : (int, int) -> int
 
diff --git a/lib/rts.c b/lib/rts.c
index b098ae0e..61f772cf 100644
--- a/lib/rts.c
+++ b/lib/rts.c
@@ -16,6 +16,18 @@ unit sail_assert(bool b, sail_string msg)
   exit(EXIT_FAILURE);
 }
 
+unit sail_exit(unit u)
+{
+  exit(EXIT_SUCCESS);
+  return UNIT;
+}
+
+unit sleep_request(const unit u)
+{
+  fprintf(stderr, "Sail model going to sleep\n");
+  exit(EXIT_SUCCESS);
+}
+
 /* ***** Sail memory builtins ***** */
 
 /*
@@ -151,6 +163,19 @@ void read_ram(sail_bits *data,
   mpz_clear(byte);
 }
 
+unit load_raw(mach_bits addr, const sail_string file)
+{
+  FILE *fp = fopen(file, "r");
+
+  uint64_t byte;
+  while ((byte = (uint64_t)fgetc(fp)) != EOF) {
+    write_mem(addr, byte);
+    addr++;
+  }
+
+  return UNIT;
+}
+
 void load_image(char *file) {
   FILE *fp = fopen(file, "r");
 
@@ -201,7 +226,12 @@ unit disable_tracing(const unit u)
   return UNIT;
 }
 
-void trace_uint64_t(const uint64_t x) {
+bool is_tracing(const unit u)
+{
+  return g_trace_enabled;
+}
+
+void trace_mach_bits(const mach_bits x) {
   if (g_trace_enabled) fprintf(stderr, "0x%" PRIx64, x);
 }
 
@@ -209,10 +239,18 @@ void trace_unit(const unit u) {
   if (g_trace_enabled) fputs("()", stderr);
 }
 
-void trace_mpz_t(const mpz_t op) {
+void trace_sail_string(const sail_string str) {
+  if (g_trace_enabled) fputs(str, stderr);
+}
+
+void trace_sail_int(const sail_int op) {
   if (g_trace_enabled) mpz_out_str(stderr, 10, op);
 }
 
+void trace_sail_bits(const sail_bits op) {
+  if (g_trace_enabled) fprint_bits("", op, "", stderr);
+}
+
 void trace_bool(const bool b) {
   if (g_trace_enabled) {
     if (b) {
@@ -247,6 +285,7 @@ void trace_start(char *name)
       fprintf(stderr, "%s", "|   ");
     }
     fprintf(stderr, "%s(", name);
+    g_trace_depth++;
   }
 }
 
@@ -257,9 +296,20 @@ void trace_end(void)
     for (int64_t i = 0; i < g_trace_depth; ++i) {
       fprintf(stderr, "%s", "|   ");
     }
+    g_trace_depth--;
   }
 }
 
+/* ***** ELF functions ***** */
+
+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);
+}
+
 /* ***** Setup and cleanup functions for RTS ***** */
 
 void setup_rts(void)
diff --git a/lib/rts.h b/lib/rts.h
index de32ef8d..f86962c4 100644
--- a/lib/rts.h
+++ b/lib/rts.h
@@ -12,12 +12,21 @@
  */
 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);
 
+unit sail_exit(unit);
+
+/*
+ * 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);
+
 /* ***** Memory builtins ***** */
 
 // These memory builtins are intended to match the semantics for the
@@ -35,6 +44,8 @@ void read_ram(sail_bits *data,
 	      const sail_bits hex_ram,
 	      const sail_bits addr_bv);
 
+unit load_raw(mach_bits addr, const sail_string file);
+
 void load_image(char *);
 
 /* ***** Tracing ***** */
@@ -43,16 +54,20 @@ static int64_t g_trace_depth;
 static bool g_trace_enabled;
 
 /*
- * Bind these functions in Sail to enable and disable tracing:
+ * Bind these functions in Sail to enable and disable tracing (see
+ * lib/trace.sail):
  *
  * val "enable_tracing" : unit -> unit
  * val "disable_tracing" : unit -> unit
+ * val "is_tracing" : unit -> bool
  *
  * Compile with sail -c -c_trace.
  */
 unit enable_tracing(const unit);
 unit disable_tracing(const unit);
 
+bool is_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
@@ -68,7 +83,11 @@ unit disable_tracing(const unit);
 */
 void trace_sail_int(const sail_int);
 void trace_bool(const bool);
-  
+void trace_unit(const unit);
+void trace_sail_string(const sail_string);
+void trace_mach_bits(const mach_bits);
+void trace_sail_bits(const sail_bits);
+
 void trace_unknown(void);
 void trace_argsep(void);
 void trace_argend(void);
@@ -76,8 +95,15 @@ void trace_retend(void);
 void trace_start(char *);
 void trace_end(void);
 
+/*
+ * Functions to get info from ELF files.
+ */
+
 static uint64_t g_elf_entry;
 
+void elf_entry(sail_int *rop, const unit u);
+void elf_tohost(sail_int *rop, const unit u);
+
 /*
  * setup_rts and cleanup_rts are responsible for calling setup_library
  * and cleanup_library in sail.h.
diff --git a/lib/sail.c b/lib/sail.c
index 5fd7a04e..13f1a0e8 100644
--- a/lib/sail.c
+++ b/lib/sail.c
@@ -27,6 +27,16 @@ void cleanup_library(void)
   mpz_clear(sail_lib_tmp2);
 }
 
+bool eq_unit(const unit a, const unit b)
+{
+  return true;
+}
+
+unit UNDEFINED(unit)(const unit u)
+{
+  return UNIT;
+}
+
 /* ***** Sail bit type ***** */
 
 bool eq_bit(const mach_bits a, const mach_bits b)
@@ -50,43 +60,60 @@ bool UNDEFINED(bool)(const unit u) {
 
 /* ***** Sail strings ***** */
 
-void CREATE(sail_string)(sail_string *str) {
+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) {
+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) {
+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) {
+void KILL(sail_string)(sail_string *str)
+{
   free(*str);
 }
 
-void dec_str(sail_string *str, const mpz_t n) {
+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) {
+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) {
+bool eq_string(const sail_string str1, const sail_string str2)
+{
   return strcmp(str1, str2) == 0;
 }
 
+void undefined_string(sail_string *str, const unit u) {}
+
+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);
+}
+
 /* ***** Sail integers ***** */
 
 #ifndef USE_INT128
@@ -392,6 +419,33 @@ void sub_bits_int(sail_bits *rop, const sail_bits op1, const mpz_t op2)
   normalize_sail_bits(rop);
 }
 
+void and_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2)
+{
+  rop->len = op1.len;
+  mpz_and(*rop->bits, *op1.bits, *op2.bits);
+}
+
+void or_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2)
+{
+  rop->len = op1.len;
+  mpz_ior(*rop->bits, *op1.bits, *op2.bits);
+}
+
+void xor_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2)
+{
+  rop->len = op1.len;
+  mpz_xor(*rop->bits, *op1.bits, *op2.bits);
+}
+
+void not_bits(sail_bits *rop, const sail_bits 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 zeros(sail_bits *rop, const sail_int op)
 {
   rop->len = mpz_get_ui(op);
@@ -467,8 +521,274 @@ void sail_signed(sail_int *rop, const sail_bits op)
   }
 }
 
+void append(sail_bits *rop, const sail_bits op1, const sail_bits 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(sail_bits *rop, const sail_bits 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);
+  }
+}
+
+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;
+}
+
+// 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(sail_bits *rop, const sail_int len_mpz, const sail_int n, const sail_int 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(sail_int *rop,
+		   const sail_int len_mpz,
+		   const sail_int n,
+		   const sail_int start_mpz,
+		   const sail_bits 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);
+    }
+  }
+}
+
+void vector_update_subrange_sail_bits(sail_bits *rop,
+				 const sail_bits op,
+				 const sail_int n_mpz,
+				 const sail_int m_mpz,
+				 const sail_bits 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 slice(sail_bits *rop, const sail_bits op, const sail_int start_mpz, const sail_int len_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(*op.bits, i + start)) mpz_setbit(*rop->bits, i);
+  }
+}
+
+void set_slice(sail_bits *rop,
+	       const sail_int len_mpz,
+	       const sail_int slen_mpz,
+	       const sail_bits op,
+	       const sail_int start_mpz,
+	       const sail_bits 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);
+    }
+  }
+}
+
+/* ***** Sail Reals ***** */
+
+void CREATE(real)(real *rop)
+{
+  mpf_init(*rop);
+}
+
+void RECREATE(real)(real *rop)
+{
+  mpf_set_ui(*rop, 0);
+}
+
+void KILL(real)(real *rop)
+{
+  mpf_clear(*rop);
+}
+
+void COPY(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(sail_int *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(sail_int *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 sail_int op)
+{
+  mpf_set_z(*rop, op);
+}
+
+bool eq_real(const real op1, const real op2)
+{
+  return mpf_cmp(op1, op2) == 0;
+}
+
+bool lt_real(const real op1, const real op2)
+{
+  return mpf_cmp(op1, op2) < 0;
+}
+
+bool gt_real(const real op1, const real op2)
+{
+  return mpf_cmp(op1, op2) > 0;
+}
+
+bool lteq_real(const real op1, const real op2)
+{
+  return mpf_cmp(op1, op2) <= 0;
+}
+
+bool gteq_real(const real op1, const real op2)
+{
+  return mpf_cmp(op1, op2) >= 0;
+}
+
+void real_power(real *rop, const real base, const sail_int exp)
+{
+  uint64_t exp_ui = mpz_get_ui(exp);
+  mpf_pow_ui(*rop, base, exp_ui);
+}
+
+void CREATE_OF(real, sail_string)(real *rop, const sail_string op)
+{
+  mpf_init(*rop);
+  gmp_sscanf(op, "%Ff", *rop);
+}
+
 /* ***** Printing functions ***** */
 
+void string_of_int(sail_string *str, const sail_int i)
+{
+  gmp_asprintf(str, "%Zd", i);
+}
+
+void string_of_bits(sail_string *str, const sail_bits 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);
+  }
+}
+
 void fprint_bits(const sail_string pre,
 		 const sail_bits op,
 		 const sail_string post,
@@ -556,3 +876,10 @@ unit prerr_int(const sail_string str, const sail_int op)
   fputs("\n", stderr);
   return UNIT;
 }
+
+unit sail_putchar(const sail_int op)
+{
+  char c = (char) mpz_get_ui(op);
+  putchar(c);
+  return UNIT;
+}
diff --git a/lib/sail.h b/lib/sail.h
index 1cd5d928..23ff7f52 100644
--- a/lib/sail.h
+++ b/lib/sail.h
@@ -43,7 +43,7 @@ typedef int unit;
 
 unit UNDEFINED(unit)(const unit);
 bool eq_unit(const unit, const unit);
-  
+
 /* ***** Sail booleans ***** */
 
 /*
@@ -66,8 +66,12 @@ SAIL_BUILTIN_TYPE(sail_string);
 void dec_str(sail_string *str, const mpz_t n);
 void hex_str(sail_string *str, const mpz_t n);
 
+void undefined_string(sail_string *str, const unit u);
+
 bool eq_string(const sail_string, const sail_string);
 
+void concat_str(sail_string *stro, const sail_string str1, const sail_string str2);
+
 /* ***** Sail integers ***** */
 
 typedef int64_t mach_int;
@@ -94,7 +98,7 @@ void RECREATE_OF(sail_int, sail_string)(mpz_t *, const sail_string);
 
 mach_int CONVERT_OF(mach_int, sail_int)(const sail_int);
 void CONVERT_OF(sail_int, mach_int)(sail_int *, const mach_int);
-  
+
 #else
 
 typedef __int128 sail_int;
@@ -134,6 +138,7 @@ SAIL_INT_FUNCTION(undefined_range, sail_int, const sail_int, const sail_int);
  */
 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(mult_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);
@@ -175,7 +180,7 @@ mach_bits CONVERT_OF(mach_bits, sail_bits)(const sail_bits);
 void UNDEFINED(sail_bits)(sail_bits *, const sail_int len, const mach_bits bit);
 mach_bits UNDEFINED(mach_bits)(const unit);
 
-/* 
+/*
  * Wrapper around >> operator to avoid UB when shift amount is greater
  * than or equal to 64.
  */
@@ -192,6 +197,11 @@ void sub_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2);
 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);
 
+void and_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2);
+void or_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2);
+void xor_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2);
+void not_bits(sail_bits *rop, const sail_bits op);
+
 void zeros(sail_bits *rop, const sail_int op);
 void zero_extend(sail_bits *rop, const sail_bits op, const sail_int len);
 
@@ -211,11 +221,74 @@ mach_bits bitvector_access(const sail_bits op, const sail_int n_mpz);
 void sail_unsigned(sail_int *rop, const sail_bits op);
 void sail_signed(sail_int *rop, const sail_bits op);
 
+void append(sail_bits *rop, const sail_bits op1, const sail_bits op2);
+
+void replicate_bits(sail_bits *rop, const sail_bits op1, const sail_int op2);
+mach_bits fast_replicate_bits(const mach_bits shift, const mach_bits v, const mach_int times);
+
+void get_slice_int(sail_bits *rop, const sail_int len_mpz, const sail_int n, const sail_int start_mpz);
+
+void set_slice_int(sail_int *rop,
+		   const sail_int len_mpz,
+		   const sail_int n,
+		   const sail_int start_mpz,
+		   const sail_bits slice);
+
+void vector_update_subrange_sail_bits(sail_bits *rop,
+				      const sail_bits op,
+				      const sail_int n_mpz,
+				      const sail_int m_mpz,
+				      const sail_bits slice);
+
+void slice(sail_bits *rop, const sail_bits op, const sail_int start_mpz, const sail_int len_mpz);
+
+void set_slice(sail_bits *rop,
+	       const sail_int len_mpz,
+	       const sail_int slen_mpz,
+	       const sail_bits op,
+	       const sail_int start_mpz,
+	       const sail_bits slice);
+
 /* ***** Sail reals ***** */
 
+typedef mpf_t real;
+
+SAIL_BUILTIN_TYPE(real);
+
+void CREATE_OF(real, sail_string)(real *rop, const sail_string op);
+
+void UNDEFINED(real)(real *rop, unit u);
+
+void neg_real(real *rop, const real op);
+
+void mult_real(real *rop, const real op1, const real op2);
+void sub_real(real *rop, const real op1, const real op2);
+void add_real(real *rop, const real op1, const real op2);
+void div_real(real *rop, const real op1, const real op2);
+
+void sqrt_real(real *rop, const real op);
+void abs_real(real *rop, const real op);
+
+void round_up(sail_int *rop, const real op);
+void round_down(sail_int *rop, const real op);
+
+void to_real(real *rop, const sail_int op);
+
+bool eq_real(const real op1, const real op2);
+
+bool lt_real(const real op1, const real op2);
+bool gt_real(const real op1, const real op2);
+bool lteq_real(const real op1, const real op2);
+bool gteq_real(const real op1, const real op2);
+
+void real_power(real *rop, const real base, const sail_int exp);
+
 /* ***** Printing ***** */
 
-/* 
+void string_of_int(sail_string *str, const sail_int i);
+void string_of_bits(sail_string *str, const sail_bits op);
+
+/*
  * Utility function not callable from Sail!
  */
 void fprint_bits(const sail_string pre,
@@ -234,3 +307,5 @@ unit prerr_endline(const sail_string str);
 
 unit print_int(const sail_string str, const sail_int op);
 unit prerr_int(const sail_string str, const sail_int op);
+
+unit sail_putchar(const sail_int op);
diff --git a/lib/smt.sail b/lib/smt.sail
index ae672947..c9312819 100644
--- a/lib/smt.sail
+++ b/lib/smt.sail
@@ -7,7 +7,7 @@ val div = {
   smt: "div",
   ocaml: "quotient",
   lem: "integerDiv",
-  c: "div_int"
+  c: "tdiv_int"
 } : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = div('n, 'm). atom('o)}
 
 overload operator / = {div}
@@ -16,7 +16,7 @@ val mod = {
   smt: "mod",
   ocaml: "modulus",
   lem: "integerMod",
-  c: "mod_int"
+  c: "tmod_int"
 } : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = mod('n, 'm). atom('o)}
 
 overload operator % = {mod}
diff --git a/src/c_backend.ml b/src/c_backend.ml
index 7923a49c..1a2981e2 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -212,8 +212,8 @@ let rec aexp_rename from_id to_id (AE_aux (aexp, env, l)) =
     | AE_val aval -> AE_val (aval_rename from_id to_id aval)
     | AE_app (id, avals, typ) -> AE_app (id, List.map (aval_rename from_id to_id) avals, typ)
     | AE_cast (aexp, typ) -> AE_cast (recur aexp, typ)
-    | AE_assign (id, typ, aexp) when Id.compare from_id id = 0 -> AE_assign (to_id, typ, aexp)
-    | AE_assign (id, typ, aexp) -> AE_assign (id, typ, aexp)
+    | AE_assign (id, typ, aexp) when Id.compare from_id id = 0 -> AE_assign (to_id, typ, aexp_rename from_id to_id aexp)
+    | AE_assign (id, typ, aexp) -> AE_assign (id, typ, aexp_rename from_id to_id aexp)
     | AE_let (id, typ1, aexp1, aexp2, typ2) when Id.compare from_id id = 0 -> AE_let (id, typ1, aexp1, aexp2, typ2)
     | AE_let (id, typ1, aexp1, aexp2, typ2) -> AE_let (id, typ1, recur aexp1, recur aexp2, typ2)
     | AE_block (aexps, aexp, typ) -> AE_block (List.map recur aexps, recur aexp, typ)
@@ -1383,6 +1383,19 @@ let compile_funcall l ctx id args typ =
       setup := iinit ctyp gs cval :: !setup;
       cleanup := iclear ctyp gs :: !cleanup;
       (F_id gs, ctyp)
+    else if not (is_stack_ctyp have_ctyp) && is_stack_ctyp ctyp then
+      (* This is inefficient. FIXME: Remove id restriction on iconvert
+         instruction. Fortunatly only happens when flow typing makes a
+         length-polymorphic bitvector monomorphic. *)
+      let gs1 = gensym () in
+      let gs2 = gensym () in
+      setup := idecl have_ctyp gs1 :: !setup;
+      setup := ialloc have_ctyp gs1 :: !setup;
+      setup := icopy (CL_id gs1) cval :: !setup;
+      setup := idecl ctyp gs2 :: !setup;
+      setup := iconvert (CL_id gs2) ctyp gs1 have_ctyp :: !setup;
+      cleanup := iclear have_ctyp gs1 :: !cleanup;
+      (F_id gs2, ctyp)
     else
       c_error ~loc:l
         (Printf.sprintf "Failure when setting up function %s arguments: %s and %s." (string_of_id id) (string_of_ctyp have_ctyp) (string_of_ctyp ctyp))
@@ -3235,7 +3248,7 @@ let sgen_finish = function
 
 let instrument_tracing ctx =
   let module StringSet = Set.Make(String) in
-  let traceable = StringSet.of_list ["uint64_t"; "sail_string"; "bv_t"; "mpz_t"; "unit"; "bool"] in
+  let traceable = StringSet.of_list ["mach_bits"; "sail_string"; "sail_bits"; "sail_int"; "unit"; "bool"] in
   let rec instrument = function
     | (I_aux (I_funcall (clexp, _, id, args, ctyp), _) as instr) :: instrs ->
        let trace_start =
@@ -3262,12 +3275,10 @@ let instrument_tracing ctx =
          else
            iraw "trace_unknown();"
        in
-       [trace_start;
-        iraw "g_trace_depth++;"]
+       [trace_start]
        @ trace_args args
        @ [iraw "trace_argend();";
           instr;
-          iraw "g_trace_depth--;";
           trace_end;
           trace_ret;
           iraw "trace_retend();"]
@@ -3314,7 +3325,10 @@ 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 = optimize ctx cdefs in
+    let cdefs = if !opt_trace then List.map (instrument_tracing ctx) cdefs else cdefs in
+
     let docs = List.map (codegen_def ctx) cdefs in
 
     let preamble = separate hardline
diff --git a/src/sail.ml b/src/sail.ml
index 86c00254..af433799 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -119,9 +119,9 @@ let options = Arg.align ([
   ( "-Oconstant_fold",
     Arg.Set Constant_fold.optimize_constant_fold,
     " Apply constant folding optimizations");
-  ( "-c_trace",
-    Arg.Set C_backend.opt_trace,
-    " Instrument C ouput with tracing");
+  ( "-trace",
+    Arg.Tuple [Arg.Set C_backend.opt_trace; Arg.Set Ocaml_backend.opt_trace_ocaml],
+    " Instrument ouput with tracing");
   ( "-lem_ast",
     Arg.Set opt_print_lem_ast,
     " output a Lem AST representation of the input");
diff --git a/test/c/assign_rename_bug.expect b/test/c/assign_rename_bug.expect
new file mode 100644
index 00000000..ef2503c0
--- /dev/null
+++ b/test/c/assign_rename_bug.expect
@@ -0,0 +1,28 @@
+0xFFF0000000001
+0xFFF0000000001
+0xFFEFFFFFFFFFF
+0xFFEFFFFFFFFFF
+0xFFF0000000002
+0xFFF0000000002
+0xFFEFFFFFFFFFE
+0xFFEFFFFFFFFFE
+0xFFF0000000003
+0xFFF0000000003
+0xFFEFFFFFFFFFD
+0xFFEFFFFFFFFFD
+0xFFF0000000004
+0xFFF0000000004
+0xFFEFFFFFFFFFC
+0xFFEFFFFFFFFFC
+0xFFF0000000005
+0xFFF0000000005
+0xFFEFFFFFFFFFB
+0xFFEFFFFFFFFFB
+0xFFF0000000006
+0xFFF0000000006
+0xFFEFFFFFFFFFA
+0xFFEFFFFFFFFFA
+0xFFF0000000007
+0xFFF0000000007
+0xFFEFFFFFFFFF9
+0xFFEFFFFFFFFF9
diff --git a/test/c/assign_rename_bug.sail b/test/c/assign_rename_bug.sail
new file mode 100644
index 00000000..8b74df2a
--- /dev/null
+++ b/test/c/assign_rename_bug.sail
@@ -0,0 +1,35 @@
+default Order dec
+
+$include <flow.sail>
+$include <arith.sail>
+$include <vector_dec.sail>
+
+$include <exception_basic.sail>
+
+val sub_vec_int = {
+  ocaml: "sub_vec_int",
+  lem: "sub_vec_int",
+  c: "sub_bits_int"
+} : forall 'n. (bits('n), int) -> bits('n)
+
+overload operator - = {sub_vec_int}
+
+val print_bits52: (string, bits(52)) -> unit
+
+function print_bits52(str, x) = print_bits(str, x)
+
+val main : unit -> unit effect {undef}
+
+function main() = {
+  let addr : bits(52) = 0xF_FF00_0000_0000;
+  i : int = undefined;
+  size : int = 7;
+  ret : unit = ();
+  foreach (i from 1 to size by 1 in inc) {
+    ret = print_bits("", addr + i);
+    ret = print_bits52("", addr + i);
+    ret = print_bits("", addr - i);
+    ret = print_bits52("", addr - i);
+  };
+  return ret
+}