Add -Ofixed_int and -Ofixed_bits to assume fixed-precision ints and bitvectors in C

Assumes a Sail C library that has functions with the right types to
support this. Currently lib/int128 supports the -Ofixed_int option,
which was previously -Oint128.

Add a version of Sail C library that can be built with -nostdlib and
-ffreestanding, assuming the above options. Currently just a header
file without any implementation, but with the right types

9 files changed, 421 insertions, 41 deletions

diff --git a/lib/nostd/sail.h b/lib/nostd/sail.h
new file mode 100644
index 00000000..52318a61
--- /dev/null
+++ b/lib/nostd/sail.h
@@ -0,0 +1,341 @@
+#ifndef __SAIL_LIB
+#define __SAIL_LIB
+
+#include <stddef.h>
+#include <stdint.h>
+#include <stdbool.h>
+
+void *sail_malloc(size_t);
+void sail_free(void *);
+
+void sail_match_failure(char *message);
+
+/*
+ * 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 EQUAL(type) eq_ ## 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);
+bool EQUAL(unit)(const unit, const unit);
+
+unit skip(const unit);
+unit sail_exit(const unit);
+
+/* ***** Sail booleans ***** */
+
+/*
+ * and_bool and or_bool are special-cased by the compiler to ensure
+ * short-circuiting evaluation.
+ */
+bool not(const bool);
+bool EQUAL(bool)(const bool, const bool);
+bool UNDEFINED(bool)(const unit);
+
+/* ***** Sail strings ***** */
+
+/*
+ * Sail strings are just C strings.
+ */
+typedef char *sail_string;
+
+SAIL_BUILTIN_TYPE(sail_string);
+
+void undefined_string(sail_string *str, const unit u);
+
+bool eq_string(const sail_string, const sail_string);
+bool EQUAL(sail_string)(const sail_string, const sail_string);
+
+void concat_str(sail_string *stro, const sail_string str1, const sail_string str2);
+bool string_startswith(sail_string s, sail_string prefix);
+
+unit sail_assert(bool, sail_string);
+
+/* ***** Sail integers ***** */
+
+typedef int64_t mach_int;
+
+bool EQUAL(mach_int)(const mach_int, const mach_int);
+
+typedef __int128 sail_int;
+
+uint64_t sail_int_get_ui(const sail_int);
+
+void dec_str(sail_string *str, const sail_int n);
+void hex_str(sail_string *str, const sail_int n);
+
+#define SAIL_INT_FUNCTION(fname, rtype, ...) rtype fname(__VA_ARGS__)
+
+// SAIL_BUILTIN_TYPE(sail_int);
+
+sail_int CREATE_OF(sail_int, mach_int)(const mach_int);
+mach_int CREATE_OF(mach_int, sail_int)(const sail_int);
+
+mach_int CONVERT_OF(mach_int, sail_int)(const sail_int);
+sail_int CONVERT_OF(sail_int, mach_int)(const mach_int);
+sail_int CONVERT_OF(sail_int, sail_string)(const sail_string);
+
+/*
+ * Comparison operators for integers
+ */
+bool eq_int(const sail_int, const sail_int);
+bool EQUAL(sail_int)(const sail_int, const sail_int);
+
+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);
+
+/*
+ * Left and right shift for integers
+ */
+mach_int shl_mach_int(const mach_int, const mach_int);
+mach_int shr_mach_int(const mach_int, const mach_int);
+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);
+
+/*
+ * 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);
+
+/*
+ * 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(sub_nat, sail_int, const sail_int, const sail_int);
+SAIL_INT_FUNCTION(mult_int, sail_int, const sail_int, const sail_int);
+SAIL_INT_FUNCTION(ediv_int, sail_int, const sail_int, const sail_int);
+SAIL_INT_FUNCTION(emod_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);
+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);
+SAIL_INT_FUNCTION(neg_int, sail_int, const sail_int);
+SAIL_INT_FUNCTION(abs_int, sail_int, const sail_int);
+SAIL_INT_FUNCTION(pow_int, sail_int, const sail_int, const sail_int);
+SAIL_INT_FUNCTION(pow2, sail_int, const sail_int);
+
+SAIL_INT_FUNCTION(make_the_value, sail_int, const sail_int);
+SAIL_INT_FUNCTION(size_itself_int, sail_int, const sail_int);
+
+/* ***** Sail bitvectors ***** */
+
+typedef uint64_t fbits;
+
+bool eq_bit(const fbits a, const fbits b);
+
+bool EQUAL(fbits)(const fbits, const fbits);
+
+typedef struct {
+  uint64_t len;
+  uint64_t bits;
+} sbits;
+
+// For backwards compatability
+typedef uint64_t mach_bits;
+typedef sbits lbits;
+
+lbits append_64(const lbits, const uint64_t);
+
+lbits add_bits_int(const lbits, const sail_int);
+lbits sub_bits_int(const lbits, const sail_int);
+
+lbits UNDEFINED(lbits)(bool);
+
+lbits vector_subrange_lbits(const lbits, const sail_int, const sail_int);
+
+lbits vector_update_subrange_lbits(const lbits, const sail_int, const sail_int, const lbits);
+
+lbits slice(const lbits, const sail_int, const sail_int);
+
+lbits set_slice(const sail_int, const sail_int, const lbits, const sail_int, const lbits);
+
+lbits get_slice_int(const sail_int, const sail_int, const sail_int);
+
+lbits zeros(const sail_int);
+lbits zero_extend(const lbits, const sail_int);
+
+bool eq_bits(const lbits, const lbits);
+bool neq_bits(const lbits, const lbits);
+lbits not_bits(const lbits);
+lbits xor_bits(const lbits, const lbits);
+lbits or_bits(const lbits, const lbits);
+lbits and_bits(const lbits, const lbits);
+lbits add_bits(const lbits, const lbits);
+lbits sub_bits(const lbits, const lbits);
+
+lbits append(const lbits, const lbits);
+
+lbits replicate_bits(const lbits, const sail_int);
+
+sbits CREATE_OF(sbits, lbits)(const lbits op, const bool direction);
+fbits CREATE_OF(fbits, lbits)(const lbits op, const bool direction);
+sbits CREATE_OF(sbits, fbits)(const fbits op, const uint64_t len, const bool direction);
+
+/* Bitvector conversions */
+
+lbits CONVERT_OF(lbits, fbits)(const fbits, const uint64_t, const bool);
+lbits CONVERT_OF(lbits, sbits)(const sbits, const bool);
+
+fbits CONVERT_OF(fbits, lbits)(const lbits, const bool);
+fbits CONVERT_OF(fbits, sbits)(const sbits, const bool);
+
+sbits CONVERT_OF(sbits, fbits)(const fbits, const uint64_t, const bool);
+sbits CONVERT_OF(sbits, lbits)(const lbits, const bool);
+
+fbits UNDEFINED(fbits)(const unit);
+
+sbits undefined_sbits(void);
+
+/*
+ * Wrapper around >> operator to avoid UB when shift amount is greater
+ * than or equal to 64.
+ */
+fbits safe_rshift(const fbits, const fbits);
+
+fbits fast_zero_extend(const sbits op, const uint64_t n);
+fbits fast_sign_extend(const fbits op, const uint64_t n, const uint64_t m);
+fbits fast_sign_extend2(const sbits op, const uint64_t m);
+
+sail_int length_lbits(const lbits op);
+
+bool eq_bits(const lbits op1, const lbits op2);
+bool EQUAL(lbits)(const lbits op1, const lbits op2);
+bool neq_bits(const lbits op1, const lbits op2);
+
+fbits bitvector_access(const lbits op, const sail_int n_mpz);
+
+sail_int sail_unsigned(const lbits op);
+sail_int sail_signed(const lbits op);
+
+mach_int fast_signed(const fbits, const uint64_t);
+mach_int fast_unsigned(const fbits);
+
+sbits append_sf(const sbits, const fbits, const uint64_t);
+sbits append_fs(const fbits, const uint64_t, const sbits);
+sbits append_ss(const sbits, const sbits);
+
+fbits fast_replicate_bits(const fbits shift, const fbits v, const mach_int times);
+
+sail_int set_slice_int(const sail_int, const sail_int, const sail_int, const lbits);
+
+fbits fast_update_subrange(const fbits op,
+			   const mach_int n,
+			   const mach_int m,
+			   const fbits slice);
+
+sbits sslice(const fbits op, const mach_int start, const mach_int len);
+
+bool eq_sbits(const sbits op1, const sbits op2);
+bool neq_sbits(const sbits op1, const sbits op2);
+sbits not_sbits(const sbits op);
+sbits xor_sbits(const sbits op1, const sbits op2);
+sbits or_sbits(const sbits op1, const sbits op2);
+sbits and_sbits(const sbits op1, const sbits op2);
+sbits add_sbits(const sbits op1, const sbits op2);
+sbits sub_sbits(const sbits op1, const sbits op2);
+
+/* ***** Sail reals ***** */
+
+typedef double real;
+
+SAIL_BUILTIN_TYPE(real);
+
+void CREATE_OF(real, sail_string)(real *rop, const sail_string op);
+void CONVERT_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);
+
+SAIL_INT_FUNCTION(round_up, sail_int, const real);
+SAIL_INT_FUNCTION(round_down, sail_int, const real);
+
+void to_real(real *rop, const sail_int op);
+
+bool EQUAL(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);
+
+unit print_real(const sail_string, const real);
+unit prerr_real(const sail_string, const real);
+
+void random_real(real *rop, unit);
+
+/* ***** String utilities ***** */
+
+SAIL_INT_FUNCTION(string_length, sail_int, sail_string);
+void string_drop(sail_string *dst, sail_string s, sail_int len);
+void string_take(sail_string *dst, sail_string s, sail_int len);
+
+/* ***** Printing ***** */
+
+void string_of_int(sail_string *str, const sail_int i);
+void string_of_lbits(sail_string *str, const lbits op);
+void string_of_fbits(sail_string *str, const fbits op);
+void decimal_string_of_lbits(sail_string *str, const lbits op);
+void decimal_string_of_fbits(sail_string *str, const fbits op);
+
+unit print_bits(const sail_string str, const lbits op);
+unit prerr_bits(const sail_string str, const lbits op);
+
+unit print(const sail_string str);
+unit print_endline(const sail_string str);
+
+unit prerr(const sail_string str);
+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);
+
+/* ***** Misc ***** */
+
+sail_int get_time_ns(const unit);
+
+#endif
diff --git a/lib/sail.c b/lib/sail.c
index c544c9aa..1753ab8e 100644
--- a/lib/sail.c
+++ b/lib/sail.c
@@ -78,15 +78,15 @@ bool UNDEFINED(bool)(const unit u) {
 
 void CREATE(sail_string)(sail_string *str)
 {
-  char *istr = (char *) malloc(1 * sizeof(char));
+  char *istr = (char *) sail_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));
+  sail_free(*str);
+  char *istr = (char *) sail_malloc(1 * sizeof(char));
   istr[0] = '\0';
   *str = istr;
 }
@@ -100,18 +100,18 @@ void COPY(sail_string)(sail_string *str1, const sail_string str2)
 
 void KILL(sail_string)(sail_string *str)
 {
-  free(*str);
+  sail_free(*str);
 }
 
 void dec_str(sail_string *str, const mpz_t n)
 {
-  free(*str);
+  sail_free(*str);
   gmp_asprintf(str, "%Zd", n);
 }
 
 void hex_str(sail_string *str, const mpz_t n)
 {
-  free(*str);
+  sail_free(*str);
   gmp_asprintf(str, "0x%Zx", n);
 }
 
@@ -463,7 +463,7 @@ bool EQUAL(fbits)(const fbits op1, const fbits op2)
 
 void CREATE(lbits)(lbits *rop)
 {
-  rop->bits = malloc(sizeof(mpz_t));
+  rop->bits = sail_malloc(sizeof(mpz_t));
   rop->len = 0;
   mpz_init(*rop->bits);
 }
@@ -483,12 +483,12 @@ void COPY(lbits)(lbits *rop, const lbits op)
 void KILL(lbits)(lbits *rop)
 {
   mpz_clear(*rop->bits);
-  free(rop->bits);
+  sail_free(rop->bits);
 }
 
 void CREATE_OF(lbits, fbits)(lbits *rop, const uint64_t op, const uint64_t len, const bool direction)
 {
-  rop->bits = malloc(sizeof(mpz_t));
+  rop->bits = sail_malloc(sizeof(mpz_t));
   rop->len = len;
   mpz_init_set_ui(*rop->bits, op);
 }
@@ -522,7 +522,7 @@ void RECREATE_OF(lbits, fbits)(lbits *rop, const uint64_t op, const uint64_t len
 
 void CREATE_OF(lbits, sbits)(lbits *rop, const sbits op, const bool direction)
 {
-  rop->bits = malloc(sizeof(mpz_t));
+  rop->bits = sail_malloc(sizeof(mpz_t));
   rop->len = op.len;
   mpz_init_set_ui(*rop->bits, op.bits);
 }
@@ -1477,14 +1477,14 @@ void random_real(real *rop, const unit u)
 
 void string_of_int(sail_string *str, const sail_int i)
 {
-  free(*str);
+  sail_free(*str);
   gmp_asprintf(str, "%Zd", i);
 }
 
 /* asprintf is a GNU extension, but it should exist on BSD */
 void string_of_fbits(sail_string *str, const fbits op)
 {
-  free(*str);
+  sail_free(*str);
   int bytes = asprintf(str, "0x%" PRIx64, op);
   if (bytes == -1) {
     fprintf(stderr, "Could not print bits 0x%" PRIx64 "\n", op);
@@ -1493,11 +1493,11 @@ void string_of_fbits(sail_string *str, const fbits op)
 
 void string_of_lbits(sail_string *str, const lbits op)
 {
-  free(*str);
+  sail_free(*str);
   if ((op.len % 4) == 0) {
     gmp_asprintf(str, "0x%*0ZX", op.len / 4, *op.bits);
   } else {
-    *str = (char *) malloc((op.len + 3) * sizeof(char));
+    *str = (char *) sail_malloc((op.len + 3) * sizeof(char));
     (*str)[0] = '0';
     (*str)[1] = 'b';
     for (int i = 1; i <= op.len; ++i) {
@@ -1509,7 +1509,7 @@ void string_of_lbits(sail_string *str, const lbits op)
 
 void decimal_string_of_fbits(sail_string *str, const fbits op)
 {
-  free(*str);
+  sail_free(*str);
   int bytes = asprintf(str, "%" PRId64, op);
   if (bytes == -1) {
     fprintf(stderr, "Could not print bits %" PRId64 "\n", op);
@@ -1518,7 +1518,7 @@ void decimal_string_of_fbits(sail_string *str, const fbits op)
 
 void decimal_string_of_lbits(sail_string *str, const lbits op)
 {
-  free(*str);
+  sail_free(*str);
   gmp_asprintf(str, "%Z", *op.bits);
 }
 
@@ -1534,7 +1534,7 @@ void fprint_bits(const sail_string pre,
     mpz_t buf;
     mpz_init_set(buf, *op.bits);
 
-    char *hex = malloc((op.len / 4) * sizeof(char));
+    char *hex = sail_malloc((op.len / 4) * sizeof(char));
 
     for (int i = 0; i < op.len / 4; ++i) {
       char c = (char) ((0xF & mpz_get_ui(buf)) + 0x30);
@@ -1546,7 +1546,7 @@ void fprint_bits(const sail_string pre,
       fputc(hex[i - 1], stream);
     }
 
-    free(hex);
+    sail_free(hex);
     mpz_clear(buf);
   } else {
     fputs("0b", stream);
diff --git a/lib/sail.h b/lib/sail.h
index a79ea295..f5ff0eaa 100644
--- a/lib/sail.h
+++ b/lib/sail.h
@@ -8,6 +8,16 @@
 
 #include<time.h>
 
+static inline void *sail_malloc(size_t size)
+{
+  return malloc(size);
+}
+
+static inline void sail_free(void *ptr)
+{
+  free(ptr);
+}
+
 /*
  * Called by the RTS to initialise and clear any library state.
  */
diff --git a/src/isail.ml b/src/isail.ml
index 88408dcd..bb42804a 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -608,6 +608,11 @@ let handle_input' input =
            Interactive.ast := ast;
            interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops;
            vs_ids := val_spec_ids !Interactive.ast
+        | ":recheck_types" ->
+           let ast, env = Type_check.check Type_check.initial_env !Interactive.ast in
+           Interactive.env := env;
+           Interactive.ast := ast;
+           vs_ids := val_spec_ids !Interactive.ast
         | ":compile" ->
            let out_name = match !opt_file_out with
              | None -> "out.sail"
diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml
index 52061444..27bab7e4 100644
--- a/src/jib/c_backend.ml
+++ b/src/jib/c_backend.ml
@@ -86,7 +86,8 @@ let optimize_primops = ref false
 let optimize_hoist_allocations = ref false
 let optimize_struct_updates = ref false
 let optimize_alias = ref false
-let optimize_int128 = ref false
+let optimize_fixed_int = ref false
+let optimize_fixed_bits = ref false
 
 let c_debug str =
   if !c_verbosity > 0 then prerr_endline (Lazy.force str) else ()
@@ -192,9 +193,11 @@ let rec ctyp_of_typ ctx typ =
 let rec is_stack_ctyp ctyp = match ctyp with
   | CT_fbits _ | CT_sbits _ | CT_bit | CT_unit | CT_bool | CT_enum _ -> true
   | CT_fint n -> n <= 64
-  | CT_lint when !optimize_int128 -> true
+  | CT_lint when !optimize_fixed_int -> true
   | CT_lint -> false
-  | CT_lbits _ | CT_real | CT_string | CT_list _ | CT_vector _ -> false
+  | CT_lbits _ when !optimize_fixed_int -> true
+  | CT_lbits _ -> false
+  | 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
@@ -279,6 +282,12 @@ let rec value_of_aval_bit = function
   | AV_lit (L_aux (L_one, _), _) -> Sail2_values.B1
   | _ -> assert false
 
+(** Used to make sure the -Ofixed_int and -Ofixed_bits don't interfere
+   with assumptions made about optimizations in the common case. *)
+let rec never_optimize = function
+  | CT_lbits _ | CT_lint -> true
+  | _ -> false
+
 let rec c_aval ctx = function
   | AV_lit (lit, typ) as v ->
      begin
@@ -294,7 +303,7 @@ let rec c_aval ctx = function
        match lvar with
        | Local (_, typ) ->
           let ctyp = ctyp_of_typ ctx typ in
-          if is_stack_ctyp ctyp then
+          if is_stack_ctyp ctyp && not (never_optimize ctyp) then
             begin
               try
                 (* We need to check that id's type hasn't changed due to flow typing *)
@@ -311,9 +320,9 @@ let rec c_aval ctx = function
             end
           else
             v
-       | Register (_, _, typ) when is_stack_typ ctx typ ->
+       | Register (_, _, typ) ->
           let ctyp = ctyp_of_typ ctx typ in
-          if is_stack_ctyp ctyp then
+          if is_stack_ctyp ctyp && not (never_optimize ctyp) then
             AV_cval (V_id (name id, ctyp), typ)
           else
             v
@@ -1475,11 +1484,12 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) =
        | CT_unit -> "UNIT", []
        | CT_bit -> "UINT64_C(0)", []
        | CT_fint _ -> "INT64_C(0xdeadc0de)", []
-       | CT_lint when !optimize_int128 -> "((sail_int) 0xdeadc0de)", []
+       | CT_lint when !optimize_fixed_int -> "((sail_int) 0xdeadc0de)", []
        | CT_fbits _ -> "UINT64_C(0xdeadc0de)", []
        | CT_sbits _ -> "undefined_sbits()", []
+       | CT_lbits _ when !optimize_fixed_bits -> "undefined_lbits()", []
        | CT_bool -> "false", []
-       | CT_enum (_, ctor :: _) -> sgen_id ctor, [] 
+       | CT_enum (_, ctor :: _) -> sgen_id ctor, []
        | CT_tup ctyps when is_stack_ctyp ctyp ->
           let gs = ngensym () in
           let fold (inits, prev) (n, ctyp) =
@@ -1791,13 +1801,13 @@ let codegen_list_clear id ctyp =
   ^^ (if is_stack_ctyp ctyp then empty
       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 "  sail_free(*rop);"
   ^^ string "}"
 
 let codegen_list_set id ctyp =
   string (Printf.sprintf "static void internal_set_%s(%s *rop, const %s op) {\n" (sgen_id id) (sgen_id id) (sgen_id id))
   ^^ string "  if (op == NULL) { *rop = NULL; return; };\n"
-  ^^ string (Printf.sprintf "  *rop = malloc(sizeof(struct node_%s));\n" (sgen_id id))
+  ^^ string (Printf.sprintf "  *rop = sail_malloc(sizeof(struct node_%s));\n" (sgen_id id))
   ^^ (if is_stack_ctyp ctyp then
         string "  (*rop)->hd = op->hd;\n"
       else
@@ -1814,7 +1824,7 @@ let codegen_list_set id ctyp =
 let codegen_cons id ctyp =
   let cons_id = mk_id ("cons#" ^ string_of_ctyp ctyp) in
   string (Printf.sprintf "static void %s(%s *rop, const %s x, const %s xs) {\n" (sgen_function_id cons_id) (sgen_id id) (sgen_ctyp ctyp) (sgen_id id))
-  ^^ string (Printf.sprintf "  *rop = malloc(sizeof(struct node_%s));\n" (sgen_id id))
+  ^^ string (Printf.sprintf "  *rop = sail_malloc(sizeof(struct node_%s));\n" (sgen_id id))
   ^^ (if is_stack_ctyp ctyp then
         string "  (*rop)->hd = x;\n"
       else
@@ -1861,7 +1871,7 @@ let codegen_vector ctx (direction, ctyp) =
       string (Printf.sprintf "static 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 (Printf.sprintf "  rop->data = sail_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"
@@ -1877,7 +1887,7 @@ let codegen_vector ctx (direction, ctyp) =
            string "  for (int i = 0; i < (rop->len); i++) {\n"
            ^^ 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 "  if (rop->data != NULL) sail_free(rop->data);\n"
       ^^ string "}"
     in
     let vector_update =
@@ -1920,7 +1930,7 @@ let codegen_vector ctx (direction, ctyp) =
     let internal_vector_init =
       string (Printf.sprintf "static void internal_vector_init_%s(%s *rop, const int64_t len) {\n" (sgen_id id) (sgen_id id))
       ^^ string "  rop->len = len;\n"
-      ^^ string (Printf.sprintf "  rop->data = malloc(len * sizeof(%s));\n" (sgen_ctyp ctyp))
+      ^^ string (Printf.sprintf "  rop->data = sail_malloc(len * sizeof(%s));\n" (sgen_ctyp ctyp))
       ^^ (if not (is_stack_ctyp ctyp) then
             string "  for (int i = 0; i < len; i++) {\n"
             ^^ string (Printf.sprintf "    CREATE(%s)((rop->data) + i);\n" (sgen_ctyp_name ctyp))
@@ -1931,7 +1941,7 @@ let codegen_vector ctx (direction, ctyp) =
     let vector_undefined =
       string (Printf.sprintf "static void undefined_vector_%s(%s *rop, sail_int len, %s elem) {\n" (sgen_id id) (sgen_id id) (sgen_ctyp ctyp))
       ^^ string (Printf.sprintf "  rop->len = sail_int_get_ui(len);\n")
-      ^^ string (Printf.sprintf "  rop->data = malloc((rop->len) * sizeof(%s));\n" (sgen_ctyp ctyp))
+      ^^ string (Printf.sprintf "  rop->data = sail_malloc((rop->len) * sizeof(%s));\n" (sgen_ctyp ctyp))
       ^^ string "  for (int i = 0; i < (rop->len); i++) {\n"
       ^^ string (if is_stack_ctyp ctyp then
                    "    (rop->data)[i] = elem;\n"
@@ -2181,10 +2191,10 @@ let compile_ast env output_chan c_includes ast =
 
     let exn_boilerplate =
       if not (Bindings.mem (mk_id "exception") ctx.variants) then ([], []) else
-        ([ "  current_exception = malloc(sizeof(struct zexception));";
+        ([ "  current_exception = sail_malloc(sizeof(struct zexception));";
            "  CREATE(zexception)(current_exception);" ],
          [ "  KILL(zexception)(current_exception);";
-           "  free(current_exception);";
+           "  sail_free(current_exception);";
            "  if (have_exception) {fprintf(stderr, \"Exiting due to uncaught exception\\n\"); exit(EXIT_FAILURE);}" ])
     in
 
diff --git a/src/jib/c_backend.mli b/src/jib/c_backend.mli
index 4628691d..90e86d70 100644
--- a/src/jib/c_backend.mli
+++ b/src/jib/c_backend.mli
@@ -89,7 +89,7 @@ val opt_extra_arguments : string option ref
    definitions in file _sbuild/ccacheDIGEST where DIGEST is the md5sum
    of the original function to be compiled. Enabled using the -memo
    flag. Uses Marshal so it's quite picky about the exact version of
-b   the Sail version. This cache can obviously become stale if the C
+   the Sail version. This cache can obviously become stale if the C
    backend changes - it'll load an old version compiled without said
    changes. *)
 val opt_memo_cache : bool ref
@@ -100,7 +100,8 @@ val optimize_primops : bool ref
 val optimize_hoist_allocations : bool ref
 val optimize_struct_updates : bool ref
 val optimize_alias : bool ref
-val optimize_int128 : bool ref
+val optimize_fixed_int : bool ref
+val optimize_fixed_bits : bool ref
 
 (** Convert a typ to a IR ctyp *)
 val ctyp_of_typ : Jib_compile.ctx -> Ast.typ -> ctyp
diff --git a/src/jib/jib_util.ml b/src/jib/jib_util.ml
index 3326d4ad..48f686f1 100644
--- a/src/jib/jib_util.ml
+++ b/src/jib/jib_util.ml
@@ -919,7 +919,7 @@ let rec infer_call op vs =
   | (Unsigned n | Signed n), _ -> CT_fint n
   | (Zero_extend n | Sign_extend n), [v] ->
      begin match cval_ctyp v with
-     | CT_fbits (_, ord) | CT_sbits (_, ord) | CT_lbits ord ->
+     | CT_fbits (_, ord) | CT_sbits (_, ord) ->
         CT_fbits (n, ord)
      | _ -> Reporting.unreachable Parse_ast.Unknown __POS__ "Invalid type for zero/sign_extend argument"
      end
diff --git a/src/sail.ml b/src/sail.ml
index 21075818..fd13deea 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -209,9 +209,12 @@ let options = Arg.align ([
   ( "-Oconstant_fold",
     Arg.Set Constant_fold.optimize_constant_fold,
     " apply constant folding optimizations");
-  ( "-Oint128",
-    Arg.Set C_backend.optimize_int128,
-    " use 128-bit integers rather than GMP arbitrary precision integers");
+  ( "-Ofixed_int",
+    Arg.Set C_backend.optimize_fixed_int,
+    " assume fixed size integers rather than GMP arbitrary precision integers");
+  ( "-Ofixed_bits",
+    Arg.Set C_backend.optimize_fixed_bits,
+    " assume fixed size bitvectors rather than arbitrary precision bitvectors");
   ( "-Oaarch64_fast",
     Arg.Set Jib_compile.optimize_aarch64_fast_struct,
     " apply ARMv8.5 specific optimizations (potentially unsound in general)");
diff --git a/src/slice.ml b/src/slice.ml
index 427d5913..0011bb4d 100644
--- a/src/slice.ml
+++ b/src/slice.ml
@@ -173,6 +173,15 @@ let add_def_to_graph graph def =
        IdSet.iter (fun id -> graph := G.add_edge self (Type id) !graph) (typ_ids typ)
     | LEXP_memory (id, _) ->
        graph := G.add_edge self (Function id) !graph
+    | LEXP_id id ->
+       begin match Env.lookup_id id env with
+       | Register _ -> graph := G.add_edge self (Register id) !graph
+       | Enum _ -> graph := G.add_edge self (Constructor id) !graph
+       | _ ->
+          if IdSet.mem id (Env.get_toplevel_lets env) then
+            graph := G.add_edge self (Letbind id) !graph
+          else ()
+       end
     | _ -> ()
     end;
     LEXP_aux (lexp_aux, annot)
@@ -204,6 +213,7 @@ let add_def_to_graph graph def =
     E_aux (e_aux, annot)
   in
   let rw_exp self = { id_exp_alg with e_aux = (fun (e_aux, annot) -> scan_exp self e_aux annot);
+                                      lEXP_aux = (fun (l_aux, annot) -> scan_lexp self l_aux annot);
                                       pat_alg = rw_pat self } in
 
   let rewriters self =