blob: c5a1b8bc8f329e6ca8661364957c73ca8eb7180f (
plain)
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
|
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_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
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 : 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 |>
|
