Fix MIPS wrt changes to C runtime

This plus changes to bitfield internals is enough to run some MIPS tests at 1Mhz.

7 files changed, 145 insertions, 10 deletions

diff --git a/lib/elf.c b/lib/elf.c
index e0e75c91..566ca96a 100644
--- a/lib/elf.c
+++ b/lib/elf.c
@@ -357,7 +357,7 @@ void loadELFHdr(const char* buffer, const int total_file_size) {
     }
 }
 
-void loadELF(char *filename) {
+void load_elf(char *filename) {
     // Read input file into memory
     char* buffer = NULL;
     int   size   = 0;
diff --git a/lib/elf.h b/lib/elf.h
index 16dff677..e5f90365 100644
--- a/lib/elf.h
+++ b/lib/elf.h
@@ -2,4 +2,4 @@
 
 #include<string.h>
 
-void loadELF(char *filename);
+void load_elf(char *filename);
diff --git a/lib/sail.c b/lib/sail.c
index d377b099..66321590 100644
--- a/lib/sail.c
+++ b/lib/sail.c
@@ -37,6 +37,11 @@ unit UNDEFINED(unit)(const unit u)
   return UNIT;
 }
 
+unit skip(const unit u)
+{
+  return UNIT;
+}
+
 /* ***** Sail bit type ***** */
 
 bool eq_bit(const mach_bits a, const mach_bits b)
@@ -453,6 +458,28 @@ void not_bits(sail_bits *rop, const sail_bits op)
   }
 }
 
+void mults_vec(sail_bits *rop, const sail_bits op1, const sail_bits op2)
+{
+  mpz_t op1_int, op2_int;
+  mpz_init(op1_int);
+  mpz_init(op2_int);
+  sail_signed(&op1_int, op1);
+  sail_signed(&op2_int, op2);
+  rop->len = op1.len * 2;
+  mpz_mul(*rop->bits, op1_int, op2_int);
+  normalize_sail_bits(rop);
+  mpz_clear(op1_int);
+  mpz_clear(op2_int);
+}
+
+void mult_vec(sail_bits *rop, const sail_bits op1, const sail_bits op2)
+{
+  rop->len = op1.len * 2;
+  mpz_mul(*rop->bits, *op1.bits, *op2.bits);
+  normalize_sail_bits(rop); /* necessary? */
+}
+
+
 void zeros(sail_bits *rop, const sail_int op)
 {
   rop->len = mpz_get_ui(op);
@@ -465,6 +492,19 @@ void zero_extend(sail_bits *rop, const sail_bits op, const sail_int len)
   mpz_set(*rop->bits, *op.bits);
 }
 
+void sign_extend(sail_bits *rop, const sail_bits op, const sail_int 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 length_sail_bits(sail_int *rop, const sail_bits op)
 {
   mpz_set_ui(*rop, op.len);
@@ -659,6 +699,68 @@ void set_slice(sail_bits *rop,
   }
 }
 
+void shift_bits_left(sail_bits *rop, const sail_bits op1, const sail_bits op2)
+{
+  rop->len = op1.len;
+  mpz_mul_2exp(*rop->bits, *op1.bits, mpz_get_ui(*op2.bits));
+  normalize_sail_bits(rop);
+}
+
+void shift_bits_right(sail_bits *rop, const sail_bits op1, const sail_bits op2)
+{
+  rop->len = op1.len;
+  mpz_tdiv_q_2exp(*rop->bits, *op1.bits, mpz_get_ui(*op2.bits));
+}
+
+/* FIXME */
+void shift_bits_right_arith(sail_bits *rop, const sail_bits op1, const sail_bits 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(sail_bits *rop, const sail_bits 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
+    }
+  }
+}
+
 /* ***** Sail Reals ***** */
 
 void CREATE(real)(real *rop)
@@ -890,3 +992,12 @@ unit sail_putchar(const sail_int op)
   putchar(c);
   return UNIT;
 }
+
+void get_time_ns(sail_int *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);
+}
diff --git a/lib/sail.h b/lib/sail.h
index 2a143605..e3e21c92 100644
--- a/lib/sail.h
+++ b/lib/sail.h
@@ -9,6 +9,8 @@
 #include<gmp.h>
 #endif
 
+#include<time.h>
+
 /*
  * Called by the RTS to initialise and clear any library state.
  */
@@ -44,6 +46,8 @@ typedef int unit;
 unit UNDEFINED(unit)(const unit);
 bool eq_unit(const unit, const unit);
 
+unit skip(const unit);
+
 /* ***** Sail booleans ***** */
 
 /*
@@ -203,8 +207,13 @@ 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 mults_vec(sail_bits *rop, const sail_bits op1, const sail_bits op2);
+void mult_vec(sail_bits *rop, const sail_bits op1, const sail_bits op2);
+
 void zeros(sail_bits *rop, const sail_int op);
+
 void zero_extend(sail_bits *rop, const sail_bits op, const sail_int len);
+void sign_extend(sail_bits *rop, const sail_bits op, const sail_int len);
 
 void length_sail_bits(sail_int *rop, const sail_bits op);
 
@@ -250,6 +259,13 @@ void set_slice(sail_bits *rop,
 	       const sail_int start_mpz,
 	       const sail_bits slice);
 
+
+void shift_bits_left(sail_bits *rop, const sail_bits op1, const sail_bits op2);
+void shift_bits_right(sail_bits *rop, const sail_bits op1, const sail_bits op2);
+void shift_bits_right_arith(sail_bits *rop, const sail_bits op1, const sail_bits op2);
+
+void reverse_endianness(sail_bits*, sail_bits);
+
 /* ***** Sail reals ***** */
 
 typedef mpf_t real;
@@ -310,3 +326,7 @@ 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 ***** */
+
+void get_time_ns(sail_int*, const unit);
diff --git a/mips/Makefile b/mips/Makefile
index 6abf1848..007d56c7 100644
--- a/mips/Makefile
+++ b/mips/Makefile
@@ -19,7 +19,7 @@ mips.c: $(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS) $(MIPS_MAIN) Makefile ../sail
 	$(SAIL) -O -memo_z3 -c $(filter %.sail, $^) 1> $@
 
 mips_c: mips.c ../lib/sail.h Makefile
-	gcc -O2 -g -I ../lib $< -l gmp -o $@
+	gcc -O2 -g -I ../lib $< ../lib/*.c -lgmp -lz -o $@
 
 mips_no_tlb.lem: $(MIPS_PRE) $(MIPS_TLB_STUB) $(MIPS_SAILS)
 	$(SAIL) -lem -o mips_no_tlb -lem_mwords -lem_lib Mips_extras -undefined_gen -memo_z3 $^
diff --git a/mips/prelude.sail b/mips/prelude.sail
index b2c2931b..bb80ec86 100644
--- a/mips/prelude.sail
+++ b/mips/prelude.sail
@@ -103,10 +103,10 @@ val quotient = {ocaml: "quotient", lem: "integerDiv"} : (int, int) -> int
 
 overload operator / = {quotient_nat, quotient}
 
-val quot_round_zero = {ocaml: "quot_round_zero", lem: "hardware_quot", _ : "div_int"} : (int, int) -> int
-val rem_round_zero = {ocaml: "rem_round_zero", lem: "hardware_mod", _ : "mod_int"} : (int, int) -> int
+val quot_round_zero = {ocaml: "quot_round_zero", lem: "hardware_quot", _ : "tdiv_int"} : (int, int) -> int
+val rem_round_zero = {ocaml: "rem_round_zero", lem: "hardware_mod", _ : "tmod_int"} : (int, int) -> int
 
-val modulus = {ocaml: "modulus", lem: "hardware_mod", _ : "mod_int"} : forall 'n, 'n > 0 .  (int, atom('n)) -> range(0, 'n - 1)
+val modulus = {ocaml: "modulus", lem: "hardware_mod", _ : "tmod_int"} : forall 'n, 'n > 0 .  (int, atom('n)) -> range(0, 'n - 1)
 
 overload operator % = {modulus}
 
diff --git a/src/c_backend.ml b/src/c_backend.ml
index 0a9bede0..f14fdace 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -963,6 +963,8 @@ let c_fragment = function
   | AV_C_fragment (frag, _) -> frag
   | _ -> assert false
 
+let v_mask_lower i = F_lit (V_bits (Util.list_init i (fun _ -> Sail_values.B1)))
+
 let analyze_primop' ctx env l id args typ =
   let ctx = { ctx with local_env = env } in
   let no_change = AE_app (id, args, typ) in
@@ -993,10 +995,12 @@ let analyze_primop' ctx env l id args typ =
   | "and_bits", [AV_C_fragment (v1, typ1); AV_C_fragment (v2, typ2)] ->
      AE_val (AV_C_fragment (F_op (v1, "&", v2), typ))
 
-            (*
   | "not_bits", [AV_C_fragment (v, _)] ->
-     AE_val (AV_C_fragment (F_unary ("~", v), typ))
-             *)
+     begin match destruct_vector ctx.tc_env typ with
+     | Some (Nexp_aux (Nexp_constant n, _), _, Typ_aux (Typ_id id, _))
+          when string_of_id id = "bit" && Big_int.less_equal n (Big_int.of_int 64) ->
+        AE_val (AV_C_fragment (F_op (F_unary ("~", v), "&", v_mask_lower (Big_int.to_int n)), typ))
+     end
 
   | "vector_subrange", [AV_C_fragment (vec, _); AV_C_fragment (f, _); AV_C_fragment (t, _)] ->
      let len = F_op (f, "-", F_op (t, "-", v_one)) in
@@ -3370,7 +3374,7 @@ let compile_ast ctx (Defs defs) =
     let postamble = separate hardline (List.map string
        ( [ "int main(int argc, char *argv[])";
            "{";
-           "  if (argc > 1) { loadELF(argv[1]); }";
+           "  if (argc > 1) { load_image(argv[1]); }";
            "  setup_rts();" ]
        @ fst exn_boilerplate
        @ startup cdefs