Update and fix test suite

2 files changed, 70 insertions, 33 deletions

diff --git a/riscv/prelude.sail b/riscv/prelude.sail
index ff11cf7e..c8fdd467 100644
--- a/riscv/prelude.sail
+++ b/riscv/prelude.sail
@@ -142,10 +142,10 @@ val real_power = "real_power" : (real, int) -> real
 
 overload operator ^ = {xor_vec, int_power, real_power}
 
-val add_range = "add" : forall 'n 'm 'o 'p.
+val add_range = "add_int" : forall 'n 'm 'o 'p.
   (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p)
 
-val add_int = "add" : (int, int) -> int
+val add_int = "add_int" : (int, int) -> int
 
 val add_vec = "add_vec" : forall 'n. (bits('n), bits('n)) -> bits('n)
 
@@ -155,10 +155,10 @@ val add_real = "add_real" : (real, real) -> real
 
 overload operator + = {add_range, add_int, add_vec, add_vec_int, add_real}
 
-val sub_range = "sub" : forall 'n 'm 'o 'p.
+val sub_range = "sub_int" : forall 'n 'm 'o 'p.
   (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o)
 
-val sub_int = "sub" : (int, int) -> int
+val sub_int = "sub_int" : (int, int) -> int
 
 val "sub_vec" : forall 'n. (bits('n), bits('n)) -> bits('n)
 
@@ -256,13 +256,19 @@ overload min = {min_nat, min_int}
 overload max = {max_nat, max_int}
 
 val __WriteRAM = "write_ram" : forall 'n 'm.
-  (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> unit
+  (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> unit effect {wmv}
+
+val __RISCV_write : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {wmv}
+function __RISCV_write (addr, width, data) = __WriteRAM(64, width, 0x0000_0000_0000_0000, addr, data)
 
 val __TraceMemoryWrite : forall 'n 'm.
   (atom('n), bits('m), bits(8 * 'n)) -> unit
 
 val __ReadRAM = "read_ram" : forall 'n 'm.
-  (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n)
+  (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
+
+val __RISCV_read : forall 'n. (bits(64), atom('n)) -> bits(8 * 'n) effect {rmem}
+function __RISCV_read (addr, width) = __ReadRAM(64, width, 0x0000_0000_0000_0000, addr)
 
 val __TraceMemoryRead : forall 'n 'm. (atom('n), bits('m), bits(8 * 'n)) -> unit
 
@@ -302,9 +308,15 @@ union exception = {
   Error_EBREAK,
 }
 
+val "sign_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
+val "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
+
 val EXTS : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m)
 val EXTZ : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m)
 
+function EXTS v = sign_extend(v, sizeof('m))
+function EXTZ v = zero_extend(v, sizeof('m))
+
 infix 4 <_s
 infix 4 >=_s
 infix 4 <_u
@@ -325,7 +337,9 @@ and      bit_to_bool bitzero = false
 infix 7 >>
 infix 7 <<
 
-val operator >> : forall 'n 'm. (bits('n), bits('m)) -> bits('n)
-val operator << : forall 'n 'm. (bits('n), bits('m)) -> bits('n)
+val operator >> = "shift_bits_right" : forall 'n 'm. (bits('n), bits('m)) -> bits('n)
+val operator << = "shift_bits_left" : forall 'n 'm. (bits('n), bits('m)) -> bits('n)
+
+val vector64 : int -> bits(64)
 
-val vector64 : int -> bits(64)
\ No newline at end of file
+function vector64 n = __raw_GetSlice_int(64, n, 0)
\ No newline at end of file
diff --git a/riscv/riscv_types.sail b/riscv/riscv_types.sail
index cb2ea794..8673785c 100644
--- a/riscv/riscv_types.sail
+++ b/riscv/riscv_types.sail
@@ -72,12 +72,19 @@ function wGPR (r, v) =
 function check_alignment (addr : bits(64), width : atom('n)) -> forall 'n. unit =
   if unsigned(addr) % width != 0 then throw(Error_misaligned_access) else ()
 
-val "MEMr"                         : forall 'n. (bits(64), atom('n)) -> bits(8 * 'n) effect {rmem}
-val "MEMr_acquire"                 : forall 'n. (bits(64), atom('n)) -> bits(8 * 'n) effect {rmem}
-val "MEMr_strong_acquire"          : forall 'n. (bits(64), atom('n)) -> bits(8 * 'n) effect {rmem}
-val "MEMr_reserved"                : forall 'n. (bits(64), atom('n)) -> bits(8 * 'n) effect {rmem}
-val "MEMr_reserved_acquire"        : forall 'n. (bits(64), atom('n)) -> bits(8 * 'n) effect {rmem}
-val "MEMr_reserved_strong_acquire" : forall 'n. (bits(64), atom('n)) -> bits(8 * 'n) effect {rmem}
+val MEMr                         : forall 'n. (bits(64), atom('n)) -> bits(8 * 'n) effect {rmem}
+val MEMr_acquire                 : forall 'n. (bits(64), atom('n)) -> bits(8 * 'n) effect {rmem}
+val MEMr_strong_acquire          : forall 'n. (bits(64), atom('n)) -> bits(8 * 'n) effect {rmem}
+val MEMr_reserved                : forall 'n. (bits(64), atom('n)) -> bits(8 * 'n) effect {rmem}
+val MEMr_reserved_acquire        : forall 'n. (bits(64), atom('n)) -> bits(8 * 'n) effect {rmem}
+val MEMr_reserved_strong_acquire : forall 'n. (bits(64), atom('n)) -> bits(8 * 'n) effect {rmem}
+
+function MEMr                         (addr, width) = __RISCV_read(addr, width)
+function MEMr_acquire                 (addr, width) = __RISCV_read(addr, width)
+function MEMr_strong_acquire          (addr, width) = __RISCV_read(addr, width)
+function MEMr_reserved                (addr, width) = __RISCV_read(addr, width)
+function MEMr_reserved_acquire        (addr, width) = __RISCV_read(addr, width)
+function MEMr_reserved_strong_acquire (addr, width) = __RISCV_read(addr, width)
 
 val mem_read : forall 'n. (bits(64), atom('n), bool, bool, bool) -> bits(8 * 'n) effect {rmem, escape}
 
@@ -96,12 +103,21 @@ function mem_read (addr, width, aq, rl, res) = {
   }
 }
 
-val "MEMea"                            : forall 'n. (bits(64), atom('n)) -> unit effect {eamem}
-val "MEMea_release"                    : forall 'n. (bits(64), atom('n)) -> unit effect {eamem}
-val "MEMea_strong_release"             : forall 'n. (bits(64), atom('n)) -> unit effect {eamem}
-val "MEMea_conditional"                : forall 'n. (bits(64), atom('n)) -> unit effect {eamem}
-val "MEMea_conditional_release"        : forall 'n. (bits(64), atom('n)) -> unit effect {eamem}
-val "MEMea_conditional_strong_release" : forall 'n. (bits(64), atom('n)) -> unit effect {eamem}
+val MEMea                            : forall 'n. (bits(64), atom('n)) -> unit effect {eamem}
+val MEMea_release                    : forall 'n. (bits(64), atom('n)) -> unit effect {eamem}
+val MEMea_strong_release             : forall 'n. (bits(64), atom('n)) -> unit effect {eamem}
+val MEMea_conditional                : forall 'n. (bits(64), atom('n)) -> unit effect {eamem}
+val MEMea_conditional_release        : forall 'n. (bits(64), atom('n)) -> unit effect {eamem}
+val MEMea_conditional_strong_release : forall 'n. (bits(64), atom('n)) -> unit effect {eamem}
+
+val eamem_effect = "skip" : unit -> unit effect {eamem}
+
+function MEMea                            _ = { eamem_effect(); () }
+function MEMea_release                    _ = { eamem_effect(); () }
+function MEMea_strong_release             _ = { eamem_effect(); () }
+function MEMea_conditional                _ = { eamem_effect(); () }
+function MEMea_conditional_release        _ = { eamem_effect(); () }
+function MEMea_conditional_strong_release _ = { eamem_effect(); () }
 
 val mem_write_ea : forall 'n. (bits(64), atom('n), bool, bool, bool) -> unit effect {eamem, escape}
 
@@ -120,12 +136,19 @@ function mem_write_ea (addr, width, aq, rl, con) = {
   }
 }
 
-val "MEMval"                            : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {wmv}
-val "MEMval_release"                    : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {wmv}
-val "MEMval_strong_release"             : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {wmv}
-val "MEMval_conditional"                : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {wmv}
-val "MEMval_conditional_release"        : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {wmv}
-val "MEMval_conditional_strong_release" : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {wmv}
+val MEMval                            : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {wmv}
+val MEMval_release                    : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {wmv}
+val MEMval_strong_release             : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {wmv}
+val MEMval_conditional                : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {wmv}
+val MEMval_conditional_release        : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {wmv}
+val MEMval_conditional_strong_release : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {wmv}
+
+function MEMval                            (addr, width, data) = __RISCV_write(addr, width, data)
+function MEMval_release                    (addr, width, data) = __RISCV_write(addr, width, data)
+function MEMval_strong_release             (addr, width, data) = __RISCV_write(addr, width, data)
+function MEMval_conditional                (addr, width, data) = __RISCV_write(addr, width, data)
+function MEMval_conditional_release        (addr, width, data) = __RISCV_write(addr, width, data)
+function MEMval_conditional_strong_release (addr, width, data) = __RISCV_write(addr, width, data)
 
 val mem_write_value : forall 'n. (bits(64), atom('n), bits(8 * 'n), bool, bool, bool) -> unit effect {wmv, escape}
 
@@ -146,12 +169,12 @@ function mem_write_value (addr, width, value, aq, rl, con) = {
 
 val "speculate_conditional_success" : unit -> bool effect {exmem}
 
-val "MEM_fence_rw_rw" : unit -> unit effect {barr}
-val "MEM_fence_r_rw"  : unit -> unit effect {barr}
-val "MEM_fence_r_r"   : unit -> unit effect {barr}
-val "MEM_fence_rw_w"  : unit -> unit effect {barr}
-val "MEM_fence_w_w"   : unit -> unit effect {barr}
-val "MEM_fence_i"     : unit -> unit effect {barr}
+val MEM_fence_rw_rw = "skip" : unit -> unit effect {barr}
+val MEM_fence_r_rw  = "skip" : unit -> unit effect {barr}
+val MEM_fence_r_r   = "skip" : unit -> unit effect {barr}
+val MEM_fence_rw_w  = "skip" : unit -> unit effect {barr}
+val MEM_fence_w_w   = "skip" : unit -> unit effect {barr}
+val MEM_fence_i     = "skip" : unit -> unit effect {barr}
 
 enum uop = {RISCV_LUI, RISCV_AUIPC} /* upper immediate ops */
 enum bop = {RISCV_BEQ, RISCV_BNE, RISCV_BLT, RISCV_BGE, RISCV_BLTU, RISCV_BGEU} /* branch ops */