aarch64_small: convert memory access functions to use sail2 primitives

2 files changed, 31 insertions, 8 deletions

diff --git a/aarch64_small/armV8.h.sail b/aarch64_small/armV8.h.sail
index b1eac1e7..d0f0b830 100644
--- a/aarch64_small/armV8.h.sail
+++ b/aarch64_small/armV8.h.sail
@@ -275,3 +275,4 @@ function UNKNOWN_BITS(N) = (replicate_bits(0b0, 'N)) : bits('N)
 let UNKNOWN_BIT = b0
 
 /* external */ val speculate_exclusive_success : unit -> bool effect {exmem}
+function speculate_exclusive_success () = __excl_res ()
diff --git a/aarch64_small/armV8_common_lib.sail b/aarch64_small/armV8_common_lib.sail
index 4ba36dc5..b758b28e 100644
--- a/aarch64_small/armV8_common_lib.sail
+++ b/aarch64_small/armV8_common_lib.sail
@@ -564,8 +564,11 @@ function BigEndianReverse (value) = {
 /** FUNCTION:shared/functions/memory/DataMemoryBarrier */
 
 /* external */ val DataMemoryBarrier_Reads : unit -> unit effect {barr}
+function DataMemoryBarrier_Reads () = __barrier(Barrier_DMB_LD)
 /* external */ val DataMemoryBarrier_Writes : unit -> unit effect {barr}
+function DataMemoryBarrier_Writes () = __barrier(Barrier_DMB_ST)
 /* external */ val DataMemoryBarrier_All : unit -> unit effect {barr}
+function DataMemoryBarrier_All () = __barrier(Barrier_DMB)
 
 val DataMemoryBarrier : (MBReqDomain, MBReqTypes) -> unit effect {barr, escape}
 function DataMemoryBarrier(domain, types) =
@@ -583,8 +586,11 @@ function DataMemoryBarrier(domain, types) =
 /** FUNCTION:shared/functions/memory/DataSynchronizationBarrier */
 
 /* external */ val DataSynchronizationBarrier_Reads : unit -> unit effect {barr}
+function DataSynchronizationBarrier_Reads () = __barrier(Barrier_DSB_LD)
 /* external */ val DataSynchronizationBarrier_Writes : unit -> unit effect {barr}
+function DataSynchronizationBarrier_Writes () = __barrier(Barrier_DSB_ST)
 /* external */ val DataSynchronizationBarrier_All : unit -> unit effect {barr}
+function DataSynchronizationBarrier_All () = __barrier(Barrier_DSB)
 
 val DataSynchronizationBarrier : (MBReqDomain, MBReqTypes) -> unit effect {barr,escape}
 function DataSynchronizationBarrier(domain, types) =
@@ -616,14 +622,19 @@ function Hint_Prefetch(addr,hint,target,stream) = ()
 
 /* regular load */
 /* external */ val rMem_NORMAL : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/,int('N) /*size*/) -> bits('N*8) effect {rmem}
+function rMem_NORMAL (address, size) = __read_mem(Read_plain, 64, address, size)
 /* non-temporal load (LDNP), see ARM ARM for special exception to normal memory ordering rules */
 /* external */ val rMem_STREAM : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/,int('N) /*size*/) -> bits('N*8) effect {rmem}
+function rMem_STREAM (address, size) = __read_mem(Read_stream, 64, address, size)
 /* load-acquire */
 /* external */ val rMem_ORDERED : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/,int('N) /*size*/) -> bits('N*8) effect {rmem}
+function rMem_ORDERED (address, size) = __read_mem(Read_acquire, 64, address, size)
 /* load-exclusive */
 /* external */ val rMem_ATOMIC : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/,int('N) /*size*/) -> bits('N*8) effect {rmem}
+function rMem_ATOMIC (address, size) = __read_mem(Read_exclusive, 64, address, size)
 /* load-exclusive+acquire */
 /* external */ val rMem_ATOMIC_ORDERED : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/,int('N) /*size*/) -> bits('N*8) effect {rmem}
+function rMem_ATOMIC_ORDERED (address, size) = __read_mem(Read_exclusive_acquire, 64, address, size)
 
 struct read_buffer_type = {
   acctype : AccType,
@@ -692,12 +703,16 @@ function flush_read_buffer(read_buffer, size) =
 
 /* regular store */
 /* external */ val wMem_Addr_NORMAL : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/, int('N) /*size*/) -> unit effect {eamem}
+function wMem_Addr_NORMAL (address, size) = { __write_mem_ea(Write_plain, 64, address, size); () }
 /* store-release */
 /* external */ val wMem_Addr_ORDERED : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/, int('N) /*size*/) -> unit effect {eamem}
+function wMem_Addr_ORDERED (address, size) = { __write_mem_ea(Write_release, 64, address, size); () }
 /* store-exclusive */
 /* external */ val wMem_Addr_ATOMIC : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/, int('N) /*size*/) -> unit effect {eamem}
+function wMem_Addr_ATOMIC (address, size) = { __write_mem_ea(Write_exclusive, 64, address, size); () }
 /* store-exclusive+release */
 /* external */ val wMem_Addr_ATOMIC_ORDERED : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/, int('N) /*size*/) -> unit effect {eamem}
+function wMem_Addr_ATOMIC_ORDERED (address, size) = { __write_mem_ea(Write_exclusive_release, 64, address, size); () }
 
 val wMem_Addr : forall 'N, 'N in {1,2,4,8,16}. (bits(64), int('N), AccType, boolean) -> unit effect {eamem, escape}
 function wMem_Addr(address, size, acctype, excl) =
@@ -715,9 +730,15 @@ function wMem_Addr(address, size, acctype, excl) =
 
 
 /* regular store */
-/* external */ val wMem_Val_NORMAL : forall 'N, 'N in {1,2,4,8,16}. (int('N) /*size*/, bits('N*8) /*value*/) -> unit effect {wmv}
+/* external */ val wMem_Val_NORMAL : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*addr*/, int('N) /*size*/, bits('N*8) /*value*/) -> unit effect {wmv}
+function wMem_Val_NORMAL (address, size, value) = { let b = __write_mem(Write_plain, 64, address, size, value); () }
+/* external */ val wMem_Val_ORDERED : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*addr*/, int('N) /*size*/, bits('N*8) /*value*/) -> unit effect {wmv}
+function wMem_Val_ORDERED (address, size, value) = { let b = __write_mem(Write_release, 64, address, size, value); () }
 /* store-exclusive */
-/* external */ val wMem_Val_ATOMIC : forall 'N, 'N in {1,2,4,8,16}. (int('N) /*size*/, bits('N*8) /*value*/) -> bool effect {wmv}
+/* external */ val wMem_Val_ATOMIC : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*addr*/, int('N) /*size*/, bits('N*8) /*value*/) -> bool effect {wmv}
+function wMem_Val_ATOMIC (address, size, value) = __write_mem(Write_exclusive, 64, address, size, value)
+/* external */ val wMem_Val_ATOMIC_ORDERED : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*addr*/, int('N) /*size*/, bits('N*8) /*value*/) -> bool effect {wmv}
+function wMem_Val_ATOMIC_ORDERED (address, size, value) = __write_mem(Write_exclusive_release, 64, address, size, value)
 
 
 struct write_buffer_type = {
@@ -766,10 +787,10 @@ function flush_write_buffer(write_buffer) = {
   let s : range(0,16) = write_buffer.size;
   assert (s == 1 | s == 2 | s == 4 | s == 8 | s == 16);
   match write_buffer.acctype {
-    AccType_NORMAL   => wMem_Val_NORMAL (s, (write_buffer.value)[((s * 8) - 1) .. 0]),
-    AccType_STREAM   => wMem_Val_NORMAL (s, (write_buffer.value)[((s * 8) - 1) .. 0]),
-    AccType_UNPRIV   => wMem_Val_NORMAL (s, (write_buffer.value)[((s * 8) - 1) .. 0]),
-    AccType_ORDERED  => wMem_Val_NORMAL (s, (write_buffer.value)[((s * 8) - 1) .. 0]),
+    AccType_NORMAL   => wMem_Val_NORMAL (write_buffer.address, s, (write_buffer.value)[((s * 8) - 1) .. 0]),
+    AccType_STREAM   => wMem_Val_NORMAL (write_buffer.address, s, (write_buffer.value)[((s * 8) - 1) .. 0]),
+    AccType_UNPRIV   => wMem_Val_NORMAL (write_buffer.address, s, (write_buffer.value)[((s * 8) - 1) .. 0]),
+    AccType_ORDERED  => wMem_Val_ORDERED (write_buffer.address, s, (write_buffer.value)[((s * 8) - 1) .. 0]),
     _  => not_implemented("unrecognised memory access")
   };
 }
@@ -780,8 +801,8 @@ function flush_write_buffer_exclusive(write_buffer) = {
   let s = write_buffer.size;
   assert (s == 1 | s == 2 | s == 4 | s == 8 | s == 16);
   match write_buffer.acctype {
-    AccType_ATOMIC   => wMem_Val_ATOMIC(s, (write_buffer.value)[((s * 8) - 1) .. 0]),
-    AccType_ORDERED  => wMem_Val_ATOMIC(s, (write_buffer.value)[((s * 8) - 1) .. 0]),
+    AccType_ATOMIC   => wMem_Val_ATOMIC(write_buffer.address, s, (write_buffer.value)[((s * 8) - 1) .. 0]),
+    AccType_ORDERED  => wMem_Val_ATOMIC_ORDERED(write_buffer.address, s, (write_buffer.value)[((s * 8) - 1) .. 0]),
     _  => { not_implemented("unrecognised memory access"); false; }
   };
 }
@@ -961,6 +982,7 @@ function Hint_Yield() -> unit = ()
 
 /** FUNCTION:shared/functions/system/InstructionSynchronizationBarrier */
 /* external */ val InstructionSynchronizationBarrier : unit -> unit effect {barr}
+function InstructionSynchronizationBarrier () = __barrier(Barrier_ISB)
 /** FUNCTION:shared/functions/system/InterruptPending */
 
 function InterruptPending () -> boolean = not_implemented_extern("InterruptPending")