update arm and mips models for new type of write_ram builtin. Also fix c and interpreter implementations of same.

5 files changed, 9 insertions, 9 deletions

diff --git a/aarch64/no_devices.sail b/aarch64/no_devices.sail
index 882aa6b3..57dad4e2 100644
--- a/aarch64/no_devices.sail
+++ b/aarch64/no_devices.sail
@@ -1,6 +1,6 @@
 
 val ___WriteRAM = "write_ram" : forall 'n 'm.
-  (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> unit effect {wmem}
+  (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmem}
 
 val __InitRAM : forall 'm. (atom('m), int, bits('m), bits(8)) -> unit
 
@@ -25,7 +25,7 @@ val __WriteRAM : forall 'n 'm.
 
 function __WriteRAM(addr_length, bytes, hex_ram, addr, data) =
 {
-  ___WriteRAM(addr_length, bytes, hex_ram, addr, data)
+  let _ = ___WriteRAM(addr_length, bytes, hex_ram, addr, data) in ()
 }
 
 function __TraceMemoryWrite(bytes, addr, data) = ()
diff --git a/lib/rts.c b/lib/rts.c
index 84ff4916..97aad8a4 100644
--- a/lib/rts.c
+++ b/lib/rts.c
@@ -208,7 +208,7 @@ void kill_mem()
 
 // ***** Memory builtins *****
 
-unit write_ram(const mpz_t addr_size,     // Either 32 or 64
+bool write_ram(const mpz_t addr_size,     // Either 32 or 64
 	       const mpz_t data_size_mpz, // Number of bytes
 	       const sail_bits  hex_ram,       // Currently unused
 	       const sail_bits  addr_bv,
@@ -231,7 +231,7 @@ unit write_ram(const mpz_t addr_size,     // Either 32 or 64
   }
 
   mpz_clear(buf);
-  return UNIT;
+  return true;
 }
 
 void read_ram(sail_bits *data,
diff --git a/lib/rts.h b/lib/rts.h
index cedb555e..98bbd078 100644
--- a/lib/rts.h
+++ b/lib/rts.h
@@ -53,7 +53,7 @@ uint64_t read_mem(uint64_t);
 // These memory builtins are intended to match the semantics for the
 // __ReadRAM and __WriteRAM functions in ASL.
 
-unit write_ram(const mpz_t addr_size,     // Either 32 or 64
+bool write_ram(const mpz_t addr_size,     // Either 32 or 64
 	       const mpz_t data_size_mpz, // Number of bytes
 	       const sail_bits hex_ram,       // Currently unused
 	       const sail_bits addr_bv,
diff --git a/mips/prelude.sail b/mips/prelude.sail
index 037819bc..85060dda 100644
--- a/mips/prelude.sail
+++ b/mips/prelude.sail
@@ -125,10 +125,10 @@ overload min = {min_atom, min_nat, min_int}
 overload max = {max_atom, max_nat, max_int}
 
 val __WriteRAM = "write_ram" : forall 'n 'm.
-  (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> unit effect {wmv}
+  (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv}
 
 val __MIPS_write : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {wmv}
-function __MIPS_write (addr, width, data) = __WriteRAM(64, width, 0x0000_0000_0000_0000, addr, data)
+function __MIPS_write (addr, width, data) = let _ = __WriteRAM(64, width, 0x0000_0000_0000_0000, addr, data) in ()
 
 val __ReadRAM = "read_ram" : forall 'n 'm, 'n >= 0.
   (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
diff --git a/src/value.ml b/src/value.ml
index 1d2346af..dccb216e 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -406,8 +406,8 @@ let value_read_ram = function
 
 let value_write_ram = function
   | [v1; v2; v3; v4; v5] ->
-     Sail_lib.write_ram (coerce_int v1, coerce_int v2, coerce_bv v3, coerce_bv v4, coerce_bv v5);
-     V_unit
+     let b = Sail_lib.write_ram (coerce_int v1, coerce_int v2, coerce_bv v3, coerce_bv v4, coerce_bv v5) in
+     V_bool(b)
   | _ -> failwith "value write_ram"
 
 let value_load_raw = function