checking in in-progress translation of Shaked's handwritten sail1 ARM model to sail2

1 files changed, 59 insertions, 0 deletions

diff --git a/aarch64_small/armV8_extras_embed.lem b/aarch64_small/armV8_extras_embed.lem
new file mode 100644
index 00000000..86570fc4
--- /dev/null
+++ b/aarch64_small/armV8_extras_embed.lem
@@ -0,0 +1,59 @@
+open import Pervasives
+open import Sail_impl_base
+open import Sail_values
+open import Prompt
+
+val rMem_NORMAL         : (vector bitU * integer) -> M (vector bitU)
+val rMem_STREAM         : (vector bitU * integer) -> M (vector bitU)
+val rMem_ORDERED        : (vector bitU * integer) -> M (vector bitU)
+val rMem_ATOMICL        : (vector bitU * integer) -> M (vector bitU)
+val rMem_ATOMIC_ORDERED : (vector bitU * integer) -> M (vector bitU)
+
+let rMem_NORMAL (addr,size)         = read_mem false Read_plain addr size
+let rMem_STREAM (addr,size)         = read_mem false Read_stream addr size
+let rMem_ORDERED (addr,size)        = read_mem false Read_acquire addr size
+let rMem_ATOMIC (addr,size)         = read_mem false Read_exclusive addr size
+let rMem_ATOMIC_ORDERED (addr,size) = read_mem false Read_exclusive_acquire addr size
+
+val wMem_Addr_NORMAL         : (vector bitU * integer) -> M unit
+val wMem_Addr_ORDERED        : (vector bitU * integer) -> M unit
+val wMem_Addr_ATOMIC         : (vector bitU * integer) -> M unit
+val wMem_Addr_ATOMIC_ORDERED : (vector bitU * integer) -> M unit
+
+let wMem_Addr_NORMAL (addr,size)         = write_mem_ea Write_plain addr size
+let wMem_Addr_ORDERED (addr,size)        = write_mem_ea Write_release addr size
+let wMem_Addr_ATOMIC (addr,size)         = write_mem_ea Write_exclusive addr size
+let wMem_Addr_ATOMIC_ORDERED (addr,size) = write_mem_ea Write_exclusive_release addr size
+
+
+val wMem_Val_NORMAL : (integer * vector bitU) -> M unit
+val wMem_Val_ATOMIC : (integer * vector bitU) -> M bitU
+
+let wMem_Val_NORMAL (_,v) = write_mem_val v >>= fun _ -> return ()
+(* in ARM the status returned is inversed *)
+let wMem_Val_ATOMIC (_,v) = write_mem_val v >>= fun b -> return (if b then B0 else B1)
+
+let speculate_exclusive_success () = excl_result () >>= fun b -> return (if b then B1 else B0)
+
+val DataMemoryBarrier_Reads            : unit -> M unit
+val DataMemoryBarrier_Writes           : unit -> M unit
+val DataMemoryBarrier_All              : unit -> M unit
+val DataSynchronizationBarrier_Reads   : unit -> M unit
+val DataSynchronizationBarrier_Writes  : unit -> M unit
+val DataSynchronizationBarrier_All     : unit -> M unit
+val InstructionSynchronizationBarrier  : unit -> M unit
+
+let DataMemoryBarrier_Reads ()           = barrier Barrier_DMB_LD
+let DataMemoryBarrier_Writes ()          = barrier Barrier_DMB_ST
+let DataMemoryBarrier_All ()             = barrier Barrier_DMB
+let DataSynchronizationBarrier_Reads ()  = barrier Barrier_DSB_LD
+let DataSynchronizationBarrier_Writes () = barrier Barrier_DSB_ST
+let DataSynchronizationBarrier_All ()    = barrier Barrier_DSB
+let InstructionSynchronizationBarrier () = barrier Barrier_ISB
+
+val TMCommitEffect : unit -> M unit
+let TMCommitEffect () = barrier Barrier_TM_COMMIT
+
+let duplicate_bits (Vector bits start direction,len) =
+  let bits' = repeat bits len in
+  Vector bits' start direction