diff options
Diffstat (limited to 'aarch64_small/armV8_extras_embed.lem')
| -rw-r--r-- | aarch64_small/armV8_extras_embed.lem | 67 |
1 files changed, 52 insertions, 15 deletions
diff --git a/aarch64_small/armV8_extras_embed.lem b/aarch64_small/armV8_extras_embed.lem index c5a1b8bc..54f9fc8a 100644 --- a/aarch64_small/armV8_extras_embed.lem +++ b/aarch64_small/armV8_extras_embed.lem @@ -43,24 +43,61 @@ let wMem_Val_ATOMIC_ORDERED addr size v = write_mem Write_exclusive_release () a let speculate_exclusive_success () = excl_result () -val DataMemoryBarrier_Reads : forall 'rv 'e. unit -> monad 'rv unit 'e -val DataMemoryBarrier_Writes : forall 'rv 'e. unit -> monad 'rv unit 'e -val DataMemoryBarrier_All : forall 'rv 'e. unit -> monad 'rv unit 'e -val DataSynchronizationBarrier_Reads : forall 'rv 'e. unit -> monad 'rv unit 'e -val DataSynchronizationBarrier_Writes : forall 'rv 'e. unit -> monad 'rv unit 'e -val DataSynchronizationBarrier_All : forall 'rv 'e. unit -> monad 'rv unit 'e -val InstructionSynchronizationBarrier : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_NonShReads : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_NonShWrites : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_NonShAll : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_InnerShReads : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_InnerShWrites : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_InnerShAll : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_OuterShReads : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_OuterShWrites : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_OuterShAll : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_FullShReads : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_FullShWrites : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_FullShAll : forall 'rv 'e. unit -> monad 'rv unit 'e +let DataMemoryBarrier_NonShReads () = barrier (Barrier_DMB (A64_NonShare, A64_barrier_LD)) +let DataMemoryBarrier_NonShWrites () = barrier (Barrier_DMB (A64_NonShare, A64_barrier_ST)) +let DataMemoryBarrier_NonShAll () = barrier (Barrier_DMB (A64_NonShare, A64_barrier_all)) +let DataMemoryBarrier_InnerShReads () = barrier (Barrier_DMB (A64_InnerShare, A64_barrier_LD)) +let DataMemoryBarrier_InnerShWrites () = barrier (Barrier_DMB (A64_InnerShare, A64_barrier_ST)) +let DataMemoryBarrier_InnerShAll () = barrier (Barrier_DMB (A64_InnerShare, A64_barrier_all)) +let DataMemoryBarrier_OuterShReads () = barrier (Barrier_DMB (A64_OuterShare, A64_barrier_LD)) +let DataMemoryBarrier_OuterShWrites () = barrier (Barrier_DMB (A64_OuterShare, A64_barrier_ST)) +let DataMemoryBarrier_OuterShAll () = barrier (Barrier_DMB (A64_OuterShare, A64_barrier_all)) +let DataMemoryBarrier_FullShReads () = barrier (Barrier_DMB (A64_FullShare, A64_barrier_LD)) +let DataMemoryBarrier_FullShWrites () = barrier (Barrier_DMB (A64_FullShare, A64_barrier_ST)) +let DataMemoryBarrier_FullShAll () = barrier (Barrier_DMB (A64_FullShare, A64_barrier_all)) + +val DataSynchronizationBarrier_NonShReads : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_NonShWrites : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_NonShAll : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_InnerShReads : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_InnerShWrites : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_InnerShAll : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_OuterShReads : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_OuterShWrites : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_OuterShAll : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_FullShReads : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_FullShWrites : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_FullShAll : forall 'rv 'e. unit -> monad 'rv unit 'e +let DataSynchronizationBarrier_NonShReads () = barrier (Barrier_DSB (A64_NonShare, A64_barrier_LD)) +let DataSynchronizationBarrier_NonShWrites () = barrier (Barrier_DSB (A64_NonShare, A64_barrier_ST)) +let DataSynchronizationBarrier_NonShAll () = barrier (Barrier_DSB (A64_NonShare, A64_barrier_all)) +let DataSynchronizationBarrier_InnerShReads () = barrier (Barrier_DSB (A64_InnerShare, A64_barrier_LD)) +let DataSynchronizationBarrier_InnerShWrites () = barrier (Barrier_DSB (A64_InnerShare, A64_barrier_ST)) +let DataSynchronizationBarrier_InnerShAll () = barrier (Barrier_DSB (A64_InnerShare, A64_barrier_all)) +let DataSynchronizationBarrier_OuterShReads () = barrier (Barrier_DSB (A64_OuterShare, A64_barrier_LD)) +let DataSynchronizationBarrier_OuterShWrites () = barrier (Barrier_DSB (A64_OuterShare, A64_barrier_ST)) +let DataSynchronizationBarrier_OuterShAll () = barrier (Barrier_DSB (A64_OuterShare, A64_barrier_all)) +let DataSynchronizationBarrier_FullShReads () = barrier (Barrier_DSB (A64_FullShare, A64_barrier_LD)) +let DataSynchronizationBarrier_FullShWrites () = barrier (Barrier_DSB (A64_FullShare, A64_barrier_ST)) +let DataSynchronizationBarrier_FullShAll () = barrier (Barrier_DSB (A64_FullShare, A64_barrier_all)) -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 InstructionSynchronizationBarrier : forall 'rv 'e. unit -> monad 'rv unit 'e +let InstructionSynchronizationBarrier () = barrier (Barrier_ISB ()) val TMCommitEffect : forall 'rv 'e. unit -> monad 'rv unit 'e -let TMCommitEffect () = barrier Barrier_TM_COMMIT +let TMCommitEffect () = barrier (Barrier_TM_COMMIT ()) val SCTLR_EL1_type_to_SCTLR_type : SCTLR_EL1_type -> SCTLR_type let SCTLR_EL1_type_to_SCTLR_type <| SCTLR_EL1_type_SCTLR_EL1_type_chunk_0 = x |> = <| SCTLR_type_SCTLR_type_chunk_0 = x |> |