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
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
|
open import Pervasives_extra
open import Sail_impl_base
open import Vector
open import Sail_values
open import Arch
val return : forall 's 'e 'a. 'a -> outcome 's 'e 'a
let return a = Done a
val bind : forall 's 'e 'a 'b. outcome 's 'e 'a -> ('a -> outcome 's 'e 'b) -> outcome 's 'e 'b
let rec bind m f = match m with
| Done a -> f a
| Read_mem descr k -> Read_mem descr (fun v -> let (o,opt) = k v in (bind o f,opt))
| Read_reg descr k -> Read_reg descr (fun v -> let (o,opt) = k v in (bind o f,opt))
| Write_memv descr k -> Write_memv descr (fun v -> let (o,opt) = k v in (bind o f,opt))
| Write_ea descr o_s -> Write_ea descr (let (o,opt) = o_s in (bind o f,opt))
| Barrier descr o_s -> Barrier descr (let (o,opt) = o_s in (bind o f,opt))
| Footprint o_s -> Footprint (let (o,opt) = o_s in (bind o f,opt))
| Write_reg descr o_s -> Write_reg descr (let (o,opt) = o_s in (bind o f,opt))
| Escape o_s -> Escape o_s
end
type M 'e 'a = Sail_impl_base.outcome unit 'e 'a
let (>>=) = bind
val (>>) : forall 'e 'b. M 'e unit -> M 'e 'b -> M 'e 'b
let (>>) m n = m >>= fun _ -> n
val exit : forall 'a 'e. 'e -> M 'e 'a
let exit e = Escape (Just (return e,Nothing))
val read_memory : forall 'e. read_kind -> vector bitU -> integer -> M 'e (vector bitU)
let read_memory rk addr sz =
let addr = address_lifted_of_bitv addr in
let sz = natFromInteger sz in
let k memory_value =
let bitv = bitv_of_byte_lifteds memory_value in
(Done bitv,Nothing) in
Read_mem (rk,addr,sz) k
val write_memory_ea : forall 'e. write_kind -> vector bitU -> integer -> M 'e unit
let write_memory_ea wk addr sz =
let addr = address_lifted_of_bitv addr in
let sz = natFromInteger sz in
Write_ea (wk,addr,sz) (Done (),Nothing)
val write_memory_val : forall 'e. vector bitU -> M 'e bool
let write_memory_val v =
let v = byte_lifteds_of_bitv v in
let k successful = (return successful,Nothing) in
Write_memv v k
val read_reg_range : forall 'e. register -> integer -> integer -> M 'e (vector bitU)
let read_reg_range reg i j =
let (i,j) = (natFromInteger i,natFromInteger j) in
let start = natFromInteger (start_index_reg reg) in
let reg = Reg_slice (register_to_string reg) start (dir defaultDir) (i,j) in
let k register_value =
let v = bitvFromRegisterValue register_value in
(Done v,Nothing) in
Read_reg reg k
val read_reg_bit : forall 'e. register -> integer -> M 'e bitU
let read_reg_bit reg i =
read_reg_range reg i i >>= fun v -> return (access v i)
val read_reg : forall 'e. register -> M 'e (vector bitU)
let read_reg reg =
let start = natFromInteger (start_index_reg reg) in
let sz = natFromInteger (length_reg reg) in
let reg = Reg (register_to_string reg) start sz (dir defaultDir) in
let k register_value =
let v = bitvFromRegisterValue register_value in
(Done v,Nothing) in
Read_reg reg k
val read_reg_field : forall 'e. register -> register_field -> M 'e (vector bitU)
let read_reg_field reg rfield =
let (i,j) =
let (i,j) = field_indices rfield in
(natFromInteger i,natFromInteger j) in
let start = natFromInteger (start_index_reg reg) in
let reg = Reg_slice (register_to_string reg) start (dir defaultDir) (i,j) in
let k register_value =
let v = bitvFromRegisterValue register_value in
(Done v,Nothing) in
Read_reg reg k
val read_reg_bitfield : forall 'e. register -> register_bitfield -> M 'e bitU
let read_reg_bitfield reg rbit = read_reg_bit reg (field_index_bit rbit)
val write_reg_range : forall 'e. register -> integer -> integer -> vector bitU -> M 'e unit
let write_reg_range reg i j v =
let rv = registerValueFromBitv v reg in
let start = natFromInteger (start_index_reg reg) in
let (i,j) = (natFromInteger i,natFromInteger j) in
let reg = Reg_slice (register_to_string reg) start (dir defaultDir) (i,j) in
Write_reg (reg,rv) (Done (),Nothing)
val write_reg_bit : forall 'e. register -> integer -> bitU -> M 'e unit
let write_reg_bit reg i bit = write_reg_range reg i i (Vector [bit] 0 true)
val write_reg : forall 'e. register -> vector bitU -> M 'e unit
let write_reg reg v =
let rv = registerValueFromBitv v reg in
let start = natFromInteger (start_index_reg reg) in
let sz = natFromInteger (length_reg reg) in
let reg = Reg (register_to_string reg) start sz (dir defaultDir) in
Write_reg (reg,rv) (Done (),Nothing)
val write_reg_field : forall 'e. register -> register_field -> vector bitU -> M 'e unit
let write_reg_field reg rfield = uncurry (write_reg_range reg) (field_indices rfield)
val write_reg_bitfield : forall 'e. register -> register_bitfield -> bitU -> M 'e unit
let write_reg_bitfield reg rbit = write_reg_bit reg (field_index_bit rbit)
val barrier : forall 'e. barrier_kind -> M 'e unit
let barrier bk = Barrier bk (Done (), Nothing)
val footprint : forall 'e. M 'e unit
let footprint = Footprint (Done (),Nothing)
val foreachM_inc : forall 'e 'vars. (integer * integer * integer) -> 'vars ->
(integer -> 'vars -> M 'e 'vars) -> M 'e 'vars
let rec foreachM_inc (i,stop,by) vars body =
if i <= stop
then
body i vars >>= fun vars ->
foreachM_inc (i + by,stop,by) vars body
else return vars
val foreachM_dec : forall 'e 'vars. (integer * integer * integer) -> 'vars ->
(integer -> 'vars -> M 'e 'vars) -> M 'e 'vars
let rec foreachM_dec (i,stop,by) vars body =
if i >= stop
then
body i vars >>= fun vars ->
foreachM_dec (i - by,stop,by) vars body
else return vars
let write_two_regs r1 r2 vec =
let size = length_reg r1 in
let start = get_start vec in
let vsize = length vec in
let r1_v = slice vec start ((if defaultDir then size - start else start - size) - 1) in
let r2_v =
(slice vec)
(if defaultDir then size - start else start - size)
(if defaultDir then vsize - start else start - vsize) in
write_reg r1 r1_v >> write_reg r2 r2_v
|
