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
|
open import Pervasives
open import State
open import Sail_values
import Set_extra
(*
let memory_parameter_transformer mode v =
let mode = <|mode with endian = E_big_endian|> in
match v with
| Interp.V_tuple [location;length] ->
match length with
| Interp.V_lit (L_aux (L_num len) _) ->
let (v,regs) = extern_mem_value mode location in
(v,(natFromInteger len),regs)
| Interp.V_track (Interp.V_lit (L_aux (L_num len) _)) size_regs ->
let (v,loc_regs) = extern_mem_value mode location in
match loc_regs with
| Nothing -> (v,(natFromInteger len),Just (List.map (fun r -> extern_reg r Nothing) (Set_extra.toList size_regs)))
| Just loc_regs -> (v,(natFromInteger len),Just (loc_regs++(List.map (fun r -> extern_reg r Nothing) (Set_extra.toList size_regs))))
end
end
end
*)
let rMem_NORMAL (addr,l) = read_memory (unsigned addr) l
let rMem_STREAM (addr,l) = read_memory (unsigned addr) l
let rMem_ORDERED (addr,l) = read_memory (unsigned addr) l
let rMem_ATOMIC (addr,l) = read_memory (unsigned addr) l
let rMem_ATOMIC_ORDERED (addr,l) = read_memory (unsigned addr) l
let wMem_NORMAL (addr,l,v) = write_memory (unsigned addr) l v
let wMem_ORDERED (addr,l,v) = write_memory (unsigned addr) l v
let wMem_ATOMIC (addr,l,v) = write_memory (unsigned addr) l v
let wMem_ATOMIC_ORDERED (addr,l,v) = write_memory (unsigned addr) l v
let wMem_Addr_NORMAL (addr,l) = write_writeEA (unsigned addr) l
let wMem_Addr_ORDERED (addr,l) = write_writeEA (unsigned addr) l
let wMem_Addr_ATOMIC (addr,l) = write_writeEA (unsigned addr) l
let wMem_Addr_ATOMIC_ORDERED (addr,l) = write_writeEA (unsigned addr) l
let wMem_Val_NORMAL l v = read_writeEA () >>= fun (addr,_) -> write_memory addr l v
let wMem_Val_ATOMIC l v = read_writeEA () >>= fun (addr,_) -> write_memory addr l v
let DataMemoryBarrier_Reads = return ()
let DataMemoryBarrier_Writes = return ()
let DataMemoryBarrier_All = return ()
let DataSynchronizationBarrier_Reads = return ()
let DataSynchronizationBarrier_Writes = return ()
let DataSynchronizationBarrier_All = return ()
let InstructionSynchronizationBarrier = return ()
|
