From b3ea287bcf8be43714595b6921a0c47d25a67eee Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Fri, 16 Nov 2018 16:26:35 +0000
Subject: Various bugfixes and a simple profiling feature for rewrites

---
 lib/arith.sail |  4 ++--
 lib/rts.c      |  4 ++++
 lib/sail.c     | 11 +++++++++++
 lib/sail.h     |  3 +++
 4 files changed, 20 insertions(+), 2 deletions(-)

(limited to 'lib')

diff --git a/lib/arith.sail b/lib/arith.sail
index e61ec473..db011f14 100644
--- a/lib/arith.sail
+++ b/lib/arith.sail
@@ -57,13 +57,13 @@ let elsize = shl_int(8, UInt(size))
 ```
 THIS ensures that in this case the typechecker knows that the end result will be a value in the set `{8, 16, 32, 64}`
 */
-val _shl8 = "shl_int" :
+val _shl8 = {c: "shl_mach_int", _: "shl_int"} :
   forall 'n, 0 <= 'n <= 3. (int(8), int('n)) -> int('m) with 'm in {8, 16, 32, 64}
 
 /*!
 Similarly, we can shift 32 by either 0 or 1 to get a value in `{32, 64}`
 */
-val _shl32 = "shl_int" :
+val _shl32 = {c: "shl_mach_int", _: "shl_int"} :
   forall 'n, 'n in {0, 1}. (int(32), int('n)) -> int('m) with 'm in {32, 64}
 
 val _shl_int = "shl_int" : (int, int) -> int
diff --git a/lib/rts.c b/lib/rts.c
index 6bd97934..2f594ff8 100644
--- a/lib/rts.c
+++ b/lib/rts.c
@@ -94,6 +94,10 @@ void write_mem(uint64_t address, uint64_t byte)
   uint64_t mask = address & ~MASK;
   uint64_t offset = address & MASK;
 
+  //if ((byte >= 97 && byte <= 122) || (byte >= 64 && byte <= 90) || (byte >= 48 && byte <= 57) || byte == 10 || byte == 32) {
+  //  fprintf(stderr, "%c", (char) byte);
+  //}
+
   struct block *current = sail_memory;
 
   while (current != NULL) {
diff --git a/lib/sail.c b/lib/sail.c
index 94cd5c2c..fc11a40d 100644
--- a/lib/sail.c
+++ b/lib/sail.c
@@ -290,6 +290,12 @@ void shl_int(sail_int *rop, const sail_int op1, const sail_int op2)
   mpz_mul_2exp(*rop, op1, mpz_get_ui(op2));
 }
 
+inline
+mach_int shl_mach_int(const mach_int op1, const mach_int op2)
+{
+  return op1 << op2;
+}
+
 inline
 void shr_int(sail_int *rop, const sail_int op1, const sail_int op2)
 {
@@ -446,6 +452,11 @@ void CREATE_OF(sail_bits, mach_bits)(sail_bits *rop, const uint64_t op, const ui
   mpz_init_set_ui(*rop->bits, op);
 }
 
+mach_bits CREATE_OF(mach_bits, sail_bits)(const sail_bits op)
+{
+  return mpz_get_ui(*op.bits);
+}
+
 void RECREATE_OF(sail_bits, mach_bits)(sail_bits *rop, const uint64_t op, const uint64_t len, const bool direction)
 {
   rop->len = len;
diff --git a/lib/sail.h b/lib/sail.h
index 4ccd8b93..b3386198 100644
--- a/lib/sail.h
+++ b/lib/sail.h
@@ -131,6 +131,7 @@ 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);
 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);
 
@@ -192,6 +193,8 @@ void RECREATE_OF(sail_bits, mach_bits)(sail_bits *,
 				       const mach_bits len,
 				       const bool direction);
 
+mach_bits CREATE_OF(mach_bits, sail_bits)(const sail_bits);
+
 mach_bits CONVERT_OF(mach_bits, sail_bits)(const sail_bits, const bool);
 void CONVERT_OF(sail_bits, mach_bits)(sail_bits *, const mach_bits, const uint64_t, const bool);
 
-- 
cgit v1.2.3