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
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
|
open import Pervasives_extra
open import Sail_impl_base
open import Sail_values
type MR 'a 'r = outcome_r 'a 'r
type M 'a = outcome 'a
val return : forall 'a 'r. 'a -> MR 'a 'r
let return a = Done a
val bind : forall 'a 'b 'r. MR 'a 'r -> ('a -> MR 'b 'r) -> MR 'b 'r
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))
| Excl_res k -> Excl_res (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 descr -> Escape descr
| Fail descr -> Fail descr
| Error descr -> Error descr
| Return a -> Return a
| Internal descr o_s -> Internal descr (let (o,opt) = o_s in (bind o f ,opt))
end
let inline (>>=) = bind
val (>>) : forall 'b 'r. MR unit 'r -> MR 'b 'r -> MR 'b 'r
let inline (>>) m n = m >>= fun _ -> n
val exit : forall 'a 'b. 'b -> M 'a
let exit s = Fail Nothing
val assert_exp : bool -> string -> M unit
let assert_exp exp msg = if exp then Done () else Fail (Just msg)
val early_return : forall 'r. 'r -> MR unit 'r
let early_return r = Return r
val liftR : forall 'a 'r. M 'a -> MR 'a 'r
let rec liftR m = match m with
| Done a -> Done a
| Read_mem descr k -> Read_mem descr (fun v -> let (o,opt) = k v in (liftR o,opt))
| Read_reg descr k -> Read_reg descr (fun v -> let (o,opt) = k v in (liftR o,opt))
| Write_memv descr k -> Write_memv descr (fun v -> let (o,opt) = k v in (liftR o,opt))
| Excl_res k -> Excl_res (fun v -> let (o,opt) = k v in (liftR o,opt))
| Write_ea descr o_s -> Write_ea descr (let (o,opt) = o_s in (liftR o,opt))
| Barrier descr o_s -> Barrier descr (let (o,opt) = o_s in (liftR o,opt))
| Footprint o_s -> Footprint (let (o,opt) = o_s in (liftR o,opt))
| Write_reg descr o_s -> Write_reg descr (let (o,opt) = o_s in (liftR o,opt))
| Internal descr o_s -> Internal descr (let (o,opt) = o_s in (liftR o,opt))
| Escape descr -> Escape descr
| Fail descr -> Fail descr
| Error descr -> Error descr
| Return _ -> Error "uncaught early return"
end
val catch_early_return : forall 'a 'r. MR 'a 'a -> M 'a
let rec catch_early_return m = match m with
| Done a -> Done a
| Read_mem descr k -> Read_mem descr (fun v -> let (o,opt) = k v in (catch_early_return o,opt))
| Read_reg descr k -> Read_reg descr (fun v -> let (o,opt) = k v in (catch_early_return o,opt))
| Write_memv descr k -> Write_memv descr (fun v -> let (o,opt) = k v in (catch_early_return o,opt))
| Excl_res k -> Excl_res (fun v -> let (o,opt) = k v in (catch_early_return o,opt))
| Write_ea descr o_s -> Write_ea descr (let (o,opt) = o_s in (catch_early_return o,opt))
| Barrier descr o_s -> Barrier descr (let (o,opt) = o_s in (catch_early_return o,opt))
| Footprint o_s -> Footprint (let (o,opt) = o_s in (catch_early_return o,opt))
| Write_reg descr o_s -> Write_reg descr (let (o,opt) = o_s in (catch_early_return o,opt))
| Internal descr o_s -> Internal descr (let (o,opt) = o_s in (catch_early_return o,opt))
| Escape descr -> Escape descr
| Fail descr -> Fail descr
| Error descr -> Error descr
| Return a -> Done a
end
val read_mem : forall 'a 'b. Bitvector 'a, Bitvector 'b => bool -> read_kind -> 'a -> integer -> M 'b
let read_mem dir rk addr sz =
let addr = address_lifted_of_bitv (bits_of addr) in
let sz = natFromInteger sz in
let k memory_value =
let bitv = of_bits (internal_mem_value dir memory_value) in
(Done bitv,Nothing) in
Read_mem (rk,addr,sz) k
val excl_result : unit -> M bool
let excl_result () =
let k successful = (return successful,Nothing) in
Excl_res k
val write_mem_ea : forall 'a. Bitvector 'a => write_kind -> 'a -> integer -> M unit
let write_mem_ea wk addr sz =
let addr = address_lifted_of_bitv (bits_of addr) in
let sz = natFromInteger sz in
Write_ea (wk,addr,sz) (Done (),Nothing)
val write_mem_val : forall 'a. Bitvector 'a => 'a -> M bool
let write_mem_val v =
let v = external_mem_value (bits_of v) in
let k successful = (return successful,Nothing) in
Write_memv v k
val read_reg_aux : forall 'a. Bitvector 'a => reg_name -> M 'a
let read_reg_aux reg =
let k reg_value =
let v = of_bits (internal_reg_value reg_value) in
(Done v,Nothing) in
Read_reg reg k
let read_reg reg =
read_reg_aux (external_reg_whole reg)
let read_reg_range reg i j =
read_reg_aux (external_reg_slice reg (natFromInteger i,natFromInteger j))
let read_reg_bit reg i =
read_reg_aux (external_reg_slice reg (natFromInteger i,natFromInteger i)) >>= fun v ->
return (extract_only_element v)
let read_reg_field reg regfield =
read_reg_aux (external_reg_field_whole reg regfield.field_name)
let read_reg_bitfield reg regfield =
read_reg_aux (external_reg_field_whole reg regfield.field_name) >>= fun v ->
return (extract_only_element v)
let reg_deref = read_reg
val write_reg_aux : forall 'a. Bitvector 'a => reg_name -> 'a -> M unit
let write_reg_aux reg_name v =
let regval = external_reg_value reg_name (bits_of v) in
Write_reg (reg_name,regval) (Done (), Nothing)
let write_reg reg v =
write_reg_aux (external_reg_whole reg) v
let write_reg_range reg i j v =
write_reg_aux (external_reg_slice reg (natFromInteger i,natFromInteger j)) v
let write_reg_pos reg i v =
let iN = natFromInteger i in
write_reg_aux (external_reg_slice reg (iN,iN)) [v]
let write_reg_bit = write_reg_pos
let write_reg_field reg regfield v =
write_reg_aux (external_reg_field_whole reg regfield.field_name) v
(*let write_reg_field_bit reg regfield bit =
write_reg_aux (external_reg_field_whole reg regfield.field_name)
(Vector [bit] 0 (is_inc_of_reg reg))*)
let write_reg_field_range reg regfield i j v =
write_reg_aux (external_reg_field_slice reg regfield.field_name (natFromInteger i,natFromInteger j)) v
let write_reg_field_pos reg regfield i v =
write_reg_field_range reg regfield i i [v]
let write_reg_field_bit = write_reg_field_pos
val barrier : barrier_kind -> M unit
let barrier bk = Barrier bk (Done (), Nothing)
val footprint : M unit
let footprint = Footprint (Done (),Nothing)
val foreachM_inc : forall 'vars 'r. (integer * integer * integer) -> 'vars ->
(integer -> 'vars -> MR 'vars 'r) -> MR 'vars 'r
let rec foreachM_inc (i,stop,by) vars body =
if (by > 0 && i <= stop) || (by < 0 && stop <= i)
then
body i vars >>= fun vars ->
foreachM_inc (i + by,stop,by) vars body
else return vars
val foreachM_dec : forall 'vars 'r. (integer * integer * integer) -> 'vars ->
(integer -> 'vars -> MR 'vars 'r) -> MR 'vars 'r
let rec foreachM_dec (stop,i,by) vars body =
if (by > 0 && i >= stop) || (by < 0 && stop >= i)
then
body i vars >>= fun vars ->
foreachM_dec (stop,i - by,by) vars body
else return vars
val while_PP : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars
let rec while_PP vars cond body =
if cond vars then while_PP (body vars) cond body else vars
val while_PM : forall 'vars 'r. 'vars -> ('vars -> bool) ->
('vars -> MR 'vars 'r) -> MR 'vars 'r
let rec while_PM vars cond body =
if cond vars then
body vars >>= fun vars -> while_PM vars cond body
else return vars
val while_MP : forall 'vars 'r. 'vars -> ('vars -> MR bool 'r) ->
('vars -> 'vars) -> MR 'vars 'r
let rec while_MP vars cond body =
cond vars >>= fun cond_val ->
if cond_val then while_MP (body vars) cond body else return vars
val while_MM : forall 'vars 'r. 'vars -> ('vars -> MR bool 'r) ->
('vars -> MR 'vars 'r) -> MR 'vars 'r
let rec while_MM vars cond body =
cond vars >>= fun cond_val ->
if cond_val then
body vars >>= fun vars -> while_MM vars cond body
else return vars
val until_PP : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars
let rec until_PP vars cond body =
let vars = body vars in
if (cond vars) then vars else until_PP (body vars) cond body
val until_PM : forall 'vars 'r. 'vars -> ('vars -> bool) ->
('vars -> MR 'vars 'r) -> MR 'vars 'r
let rec until_PM vars cond body =
body vars >>= fun vars ->
if (cond vars) then return vars else until_PM vars cond body
val until_MP : forall 'vars 'r. 'vars -> ('vars -> MR bool 'r) ->
('vars -> 'vars) -> MR 'vars 'r
let rec until_MP vars cond body =
let vars = body vars in
cond vars >>= fun cond_val ->
if cond_val then return vars else until_MP vars cond body
val until_MM : forall 'vars 'r. 'vars -> ('vars -> MR bool 'r) ->
('vars -> MR 'vars 'r) -> MR 'vars 'r
let rec until_MM vars cond body =
body vars >>= fun vars ->
cond vars >>= fun cond_val ->
if cond_val then return vars else until_MM vars cond body
(*let write_two_regs r1 r2 vec =
let is_inc =
let is_inc_r1 = is_inc_of_reg r1 in
let is_inc_r2 = is_inc_of_reg r2 in
let () = ensure (is_inc_r1 = is_inc_r2)
"write_two_regs called with vectors of different direction" in
is_inc_r1 in
let (size_r1 : integer) = size_of_reg r1 in
let (start_vec : integer) = get_start vec in
let size_vec = length vec in
let r1_v =
if is_inc
then slice vec start_vec (size_r1 - start_vec - 1)
else slice vec start_vec (start_vec - size_r1 - 1) in
let r2_v =
if is_inc
then slice vec (size_r1 - start_vec) (size_vec - start_vec)
else slice vec (start_vec - size_r1) (start_vec - size_vec) in
write_reg r1 r1_v >> write_reg r2 r2_v*)
|
