Parameterise memory read/write primitives by address length

3 files changed, 29 insertions, 21 deletions

diff --git a/lib/regfp.sail b/lib/regfp.sail
index 90af9b44..ce361cd6 100644
--- a/lib/regfp.sail
+++ b/lib/regfp.sail
@@ -116,13 +116,13 @@ union instruction_kind = {
 
 val __read_mem
   = { ocaml: "Platform.read_mem", c: "platform_read_mem", _: "read_mem" }
-  : forall 'n, 'n > 0. (read_kind, bits(64), int('n)) -> bits(8 * 'n) effect {rmem}
+  : forall 'n 'addrsize, 'n > 0 & 'addrsize in {32, 64}. (read_kind, int('addrsize), bits('addrsize), int('n)) -> bits(8 * 'n) effect {rmem}
 val __write_mem_ea
   = { ocaml: "Platform.write_mem_ea", c: "platform_write_mem_ea", _: "write_mem_ea" }
-  : forall 'n, 'n > 0. (write_kind, bits(64), int('n)) -> unit effect {eamem}
+  : forall 'n 'addrsize, 'n > 0 & 'addrsize in {32, 64}. (write_kind, int('addrsize), bits('addrsize), int('n)) -> unit effect {eamem}
 val __write_mem
   = { ocaml: "Platform.write_mem", c: "platform_write_mem", _: "write_mem" }
-  : forall 'n, 'n > 0. (write_kind, bits(64), int('n), bits(8 * 'n)) -> bool effect {wmv}
+  : forall 'n 'addrsize, 'n > 0 & 'addrsize in {32, 64}. (write_kind, int('addrsize), bits('addrsize), int('n), bits(8 * 'n)) -> bool effect {wmv}
 val __excl_res
   = { ocaml: "Platform.excl_res", c: "platform_excl_res", _: "excl_res" }
   : unit -> bool effect {exmem}
@@ -131,10 +131,12 @@ val __barrier
   : barrier_kind -> unit effect {barr}
 
 
+/*
 val __write : forall 'n, 'n > 0. (write_kind, bits(64), int('n), bits(8 * 'n)) -> bool effect {eamem,wmv}
 function __write (wk, addr, len, value) = {
   __write_mem_ea(wk, addr, len);
   __write_mem(wk, addr, len, value)
 }
+*/
 
 $endif
diff --git a/lib/rts.c b/lib/rts.c
index ccad1f8a..d3362aec 100644
--- a/lib/rts.c
+++ b/lib/rts.c
@@ -278,40 +278,43 @@ void read_ram(lbits *data,
 
 void platform_read_mem(lbits *data,
                        const int read_kind,
-                       const uint64_t addr,
+                       const uint64_t addr_size,
+                       const sbits addr,
                        const mpz_t n)
 {
-    mpz_t addr_size;
-    mpz_init(addr_size);
-    mpz_set_ui(addr_size, 64);
+    mpz_t mpz_addr_size;
+    mpz_init(mpz_addr_size);
+    mpz_set_ui(mpz_addr_size, addr_size);
     mpz_t addr_bv;
     mpz_init(addr_bv);
-    mpz_set_ui(addr_bv, addr);
-    read_ram(data, addr_size, n, (lbits){.len=0, .bits=NULL}, (lbits){.len=64, .bits=&addr_bv});
-    mpz_clear(addr_size);
+    mpz_set_ui(addr_bv, addr.bits);
+    read_ram(data, mpz_addr_size, n, (lbits){.len=0, .bits=NULL}, (lbits){.len=addr.len, .bits=&addr_bv});
+    mpz_clear(mpz_addr_size);
     mpz_clear(addr_bv);
 }
 
 unit platform_write_mem_ea(const int write_kind,
-                           const uint64_t addr,
+                           const uint64_t addr_size,
+                           const sbits addr,
                            const mpz_t n)
 {
     return UNIT;
 }
 
 bool platform_write_mem(const int write_kind,
-                        const uint64_t addr,
+                        const uint64_t addr_size,
+                        const sbits addr,
                         const mpz_t n,
                         const lbits data)
 {
-    mpz_t addr_size;
-    mpz_init(addr_size);
-    mpz_set_ui(addr_size, 64);
+    mpz_t mpz_addr_size;
+    mpz_init(mpz_addr_size);
+    mpz_set_ui(mpz_addr_size, addr_size);
     mpz_t addr_bv;
     mpz_init(addr_bv);
-    mpz_set_ui(addr_bv, addr);
-    bool res = write_ram(addr_size, n, (lbits){.len=0, .bits=NULL}, (lbits){.len=64, .bits=&addr_bv}, data);
-    mpz_clear(addr_size);
+    mpz_set_ui(addr_bv, addr.bits);
+    bool res = write_ram(mpz_addr_size, n, (lbits){.len=0, .bits=NULL}, (lbits){.len=addr.len, .bits=&addr_bv}, data);
+    mpz_clear(mpz_addr_size);
     mpz_clear(addr_bv);
     return res;
 }
diff --git a/lib/rts.h b/lib/rts.h
index b63dfbbc..2c0722a6 100644
--- a/lib/rts.h
+++ b/lib/rts.h
@@ -73,13 +73,16 @@ bool read_tag_bool(const fbits);
 
 void platform_read_mem(lbits *data,
                        const int read_kind,
-                       const uint64_t addr,
+                       const uint64_t addr_size,
+                       const sbits addr,
                        const mpz_t n);
 unit platform_write_mem_ea(const int write_kind,
-                           const uint64_t addr,
+                           const uint64_t addr_size,
+                           const sbits addr,
                            const mpz_t n);
 bool platform_write_mem(const int write_kind,
-                        const uint64_t addr,
+                        const uint64_t addr_size,
+                        const sbits addr,
                         const mpz_t n,
                         const lbits data);
 bool platform_excl_res(const unit unit);