1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
|
open import Pervasives
open import Pervasives_extra
open import Sail2_instr_kinds
open import Sail2_values
open import Sail2_operators_mwords
open import Sail2_prompt_monad
open import Sail2_prompt
open import ArmV8_types
val rMem_NORMAL : forall 'rv 'e. list bitU -> integer -> monad 'rv (list bitU) 'e
val rMem_STREAM : forall 'rv 'e. list bitU -> integer -> monad 'rv (list bitU) 'e
val rMem_ORDERED : forall 'rv 'e. list bitU -> integer -> monad 'rv (list bitU) 'e
val rMem_ATOMICL : forall 'rv 'e. list bitU -> integer -> monad 'rv (list bitU) 'e
val rMem_ATOMIC_ORDERED : forall 'rv 'e. list bitU -> integer -> monad 'rv (list bitU) 'e
let rMem_NORMAL addr size = read_mem Read_plain () addr size
let rMem_STREAM addr size = read_mem Read_stream () addr size
let rMem_ORDERED addr size = read_mem Read_acquire () addr size
let rMem_ATOMIC addr size = read_mem Read_exclusive () addr size
let rMem_ATOMIC_ORDERED addr size = read_mem Read_exclusive_acquire () addr size
val wMem_Addr_NORMAL : forall 'rv 'e. list bitU -> integer -> monad 'rv unit 'e
val wMem_Addr_ORDERED : forall 'rv 'e. list bitU -> integer -> monad 'rv unit 'e
val wMem_Addr_ATOMIC : forall 'rv 'e. list bitU -> integer -> monad 'rv unit 'e
val wMem_Addr_ATOMIC_ORDERED : forall 'rv 'e. list bitU -> integer -> monad 'rv unit 'e
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 : forall 'rv 'e. list bitU -> integer -> list bitU -> monad 'rv unit 'e
val wMem_Val_ORDERED : forall 'rv 'e. list bitU -> integer -> list bitU -> monad 'rv unit 'e
val wMem_Val_ATOMIC : forall 'rv 'e. list bitU -> integer -> list bitU -> monad 'rv bool 'e
val wMem_Val_ATOMIC_ORDERED : forall 'rv 'e. list bitU -> integer -> list bitU -> monad 'rv bool 'e
let wMem_Val_NORMAL addr size v = write_mem Write_plain () addr size v >>= fun _ -> return ()
let wMem_Val_ORDERED addr size v = write_mem Write_release () addr size v >>= fun _ -> return ()
(* in ARM the status returned is inversed *)
let wMem_Val_ATOMIC addr size v = write_mem Write_exclusive () addr size v >>= fun b -> return (not b)
let wMem_Val_ATOMIC_ORDERED addr size v = write_mem Write_exclusive_release () addr size v >>= fun b -> return (not b)
let speculate_exclusive_success () = excl_result ()
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))
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 ())
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 |>
|
