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
|
open import Pervasives_extra
(*open import Sail_impl_base*)
open import Sail_instr_kinds
open import Sail_values
type register_name = string
type address = list bitU
type monad 'regval 'a 'e =
| Done of 'a
(* Read a number of bytes from memory, returned in little endian order *)
| Read_mem of read_kind * address * nat * (list memory_byte -> monad 'regval 'a 'e)
(* Read the tag of a memory address *)
| Read_tag of address * (bitU -> monad 'regval 'a 'e)
(* Tell the system a write is imminent, at address lifted, of size nat *)
| Write_ea of write_kind * address * nat * monad 'regval 'a 'e
(* Request the result of store-exclusive *)
| Excl_res of (bool -> monad 'regval 'a 'e)
(* Request to write memory at last signalled address. Memory value should be 8
times the size given in ea signal, given in little endian order *)
| Write_memv of list memory_byte * (bool -> monad 'regval 'a 'e)
(* Request to write the tag at given address. *)
| Write_tag of address * bitU * (bool -> monad 'regval 'a 'e)
(* Tell the system to dynamically recalculate dependency footprint *)
| Footprint of monad 'regval 'a 'e
(* Request a memory barrier *)
| Barrier of barrier_kind * monad 'regval 'a 'e
(* Request to read register, will track dependency when mode.track_values *)
| Read_reg of register_name * ('regval -> monad 'regval 'a 'e)
(* Request to write register *)
| Write_reg of register_name * 'regval * monad 'regval 'a 'e
| Undefined of (bool -> monad 'regval 'a 'e)
(* Print debugging or tracing information *)
| Print of string * monad 'regval 'a 'e
(*Result of a failed assert with possible error message to report*)
| Fail of string
| Error of string
(* Exception of type 'e *)
| Exception of 'e
(* TODO: Reading/writing tags *)
val return : forall 'rv 'a 'e. 'a -> monad 'rv 'a 'e
let return a = Done a
val bind : forall 'rv 'a 'b 'e. monad 'rv 'a 'e -> ('a -> monad 'rv 'b 'e) -> monad 'rv 'b 'e
let rec bind m f = match m with
| Done a -> f a
| Read_mem rk a sz k -> Read_mem rk a sz (fun v -> bind (k v) f)
| Read_tag a k -> Read_tag a (fun v -> bind (k v) f)
| Write_memv descr k -> Write_memv descr (fun v -> bind (k v) f)
| Write_tag a t k -> Write_tag a t (fun v -> bind (k v) f)
| Read_reg descr k -> Read_reg descr (fun v -> bind (k v) f)
| Excl_res k -> Excl_res (fun v -> bind (k v) f)
| Undefined k -> Undefined (fun v -> bind (k v) f)
| Write_ea wk a sz k -> Write_ea wk a sz (bind k f)
| Footprint k -> Footprint (bind k f)
| Barrier bk k -> Barrier bk (bind k f)
| Write_reg r v k -> Write_reg r v (bind k f)
| Print msg k -> Print msg (bind k f)
| Fail descr -> Fail descr
| Error descr -> Error descr
| Exception e -> Exception e
end
let inline (>>=) = bind
val (>>) : forall 'rv 'b 'e. monad 'rv unit 'e -> monad 'rv 'b 'e -> monad 'rv 'b 'e
let inline (>>) m n = m >>= fun (_ : unit) -> n
val exit : forall 'rv 'a 'e. unit -> monad 'rv 'a 'e
let exit () = Fail "exit"
val undefined_bool : forall 'rv 'e. unit -> monad 'rv bool 'e
let undefined_bool () = Undefined return
val assert_exp : forall 'rv 'e. bool -> string -> monad 'rv unit 'e
let assert_exp exp msg = if exp then Done () else Fail msg
val throw : forall 'rv 'a 'e. 'e -> monad 'rv 'a 'e
let throw e = Exception e
val try_catch : forall 'rv 'a 'e1 'e2. monad 'rv 'a 'e1 -> ('e1 -> monad 'rv 'a 'e2) -> monad 'rv 'a 'e2
let rec try_catch m h = match m with
| Done a -> Done a
| Read_mem rk a sz k -> Read_mem rk a sz (fun v -> try_catch (k v) h)
| Read_tag a k -> Read_tag a (fun v -> try_catch (k v) h)
| Write_memv descr k -> Write_memv descr (fun v -> try_catch (k v) h)
| Write_tag a t k -> Write_tag a t (fun v -> try_catch (k v) h)
| Read_reg descr k -> Read_reg descr (fun v -> try_catch (k v) h)
| Excl_res k -> Excl_res (fun v -> try_catch (k v) h)
| Undefined k -> Undefined (fun v -> try_catch (k v) h)
| Write_ea wk a sz k -> Write_ea wk a sz (try_catch k h)
| Footprint k -> Footprint (try_catch k h)
| Barrier bk k -> Barrier bk (try_catch k h)
| Write_reg r v k -> Write_reg r v (try_catch k h)
| Print msg k -> Print msg (try_catch k h)
| Fail descr -> Fail descr
| Error descr -> Error descr
| Exception e -> h e
end
(* For early return, we abuse exceptions by throwing and catching
the return value. The exception type is "either 'r 'e", where "Right e"
represents a proper exception and "Left r" an early return of value "r". *)
type monadR 'rv 'a 'r 'e = monad 'rv 'a (either 'r 'e)
val early_return : forall 'rv 'a 'r 'e. 'r -> monadR 'rv 'a 'r 'e
let early_return r = throw (Left r)
val catch_early_return : forall 'rv 'a 'e. monadR 'rv 'a 'a 'e -> monad 'rv 'a 'e
let catch_early_return m =
try_catch m
(function
| Left a -> return a
| Right e -> throw e
end)
(* Lift to monad with early return by wrapping exceptions *)
val liftR : forall 'rv 'a 'r 'e. monad 'rv 'a 'e -> monadR 'rv 'a 'r 'e
let liftR m = try_catch m (fun e -> throw (Right e))
(* Catch exceptions in the presence of early returns *)
val try_catchR : forall 'rv 'a 'r 'e1 'e2. monadR 'rv 'a 'r 'e1 -> ('e1 -> monadR 'rv 'a 'r 'e2) -> monadR 'rv 'a 'r 'e2
let try_catchR m h =
try_catch m
(function
| Left r -> throw (Left r)
| Right e -> h e
end)
val read_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv 'b 'e
let read_mem rk addr sz =
let k bytes = Done (bits_of_mem_bytes bytes) in
Read_mem rk (bits_of addr) (natFromInteger sz) k
val read_tag : forall 'rv 'a 'e. Bitvector 'a => 'a -> monad 'rv bitU 'e
let read_tag addr = Read_tag (bits_of addr) return
val excl_result : forall 'rv 'e. unit -> monad 'rv bool 'e
let excl_result () =
let k successful = (return successful) in
Excl_res k
val write_mem_ea : forall 'rv 'a 'e. Bitvector 'a => write_kind -> 'a -> integer -> monad 'rv unit 'e
let write_mem_ea wk addr sz = Write_ea wk (bits_of addr) (natFromInteger sz) (Done ())
val write_mem_val : forall 'rv 'a 'e. Bitvector 'a => 'a -> monad 'rv bool 'e
let write_mem_val v = match mem_bytes_of_bits v with
| Just v -> Write_memv v return
| Nothing -> Fail "write_mem_val"
end
val write_tag : forall 'rv 'a 'e. Bitvector 'a => 'a -> bitU -> monad 'rv bool 'e
let write_tag addr b = Write_tag (bits_of addr) b return
val read_reg : forall 's 'rv 'a 'e. register_ref 's 'rv 'a -> monad 'rv 'a 'e
let read_reg reg =
let k v =
match reg.of_regval v with
| Just v -> Done v
| Nothing -> Error "read_reg: unrecognised value"
end
in
Read_reg reg.name k
(* TODO
val read_reg_range : forall 's 'r 'rv 'a 'e. Bitvector 'a => register_ref 's 'rv 'r -> integer -> integer -> monad 'rv 'a 'e
let read_reg_range reg i j =
read_reg_aux of_bits (external_reg_slice reg (natFromInteger i,natFromInteger j))
let read_reg_bit reg i =
read_reg_aux (fun v -> v) (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)
let read_reg_bitfield reg regfield =
read_reg_aux (external_reg_field_whole reg regfield) >>= fun v ->
return (extract_only_element v)*)
let reg_deref = read_reg
val write_reg : forall 's 'rv 'a 'e. register_ref 's 'rv 'a -> 'a -> monad 'rv unit 'e
let write_reg reg v = Write_reg reg.name (reg.regval_of v) (Done ())
(* TODO
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 : forall 'rv 'e. barrier_kind -> monad 'rv unit 'e
let barrier bk = Barrier bk (Done ())
val footprint : forall 'rv 'e. unit -> monad 'rv unit 'e
let footprint _ = Footprint (Done ())
|
