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
250
251
252
253
254
255
256
257
|
open import Pervasives_extra
open import Machine_word
open import Sail_values
open import Sail_operators
open import Prompt_monad
open import Prompt
(* Specialisation of operators to machine words *)
let inline uint v = unsignedIntegerFromWord v
let uint_maybe v = Just (uint v)
let uint_fail v = return (uint v)
let uint_oracle v = return (uint v)
let inline sint v = signedIntegerFromWord v
let sint_maybe v = Just (sint v)
let sint_fail v = return (sint v)
let sint_oracle v = return (sint v)
val vec_of_bits_maybe : forall 'a. Size 'a => list bitU -> maybe (mword 'a)
val vec_of_bits_fail : forall 'rv 'a 'e. Size 'a => list bitU -> monad 'rv (mword 'a) 'e
val vec_of_bits_oracle : forall 'rv 'a 'e. Size 'a => list bitU -> monad 'rv (mword 'a) 'e
val vec_of_bits_failwith : forall 'a. Size 'a => list bitU -> mword 'a
val vec_of_bits : forall 'a. Size 'a => list bitU -> mword 'a
let vec_of_bits_maybe bits = of_bits bits
let vec_of_bits_fail bits = of_bits_fail bits
let vec_of_bits_oracle bits = of_bits_oracle bits
let vec_of_bits_failwith bits = of_bits_failwith bits
let vec_of_bits bits = of_bits_failwith bits
val access_vec_inc : forall 'a. Size 'a => mword 'a -> integer -> bitU
let access_vec_inc = access_bv_inc
val access_vec_dec : forall 'a. Size 'a => mword 'a -> integer -> bitU
let access_vec_dec = access_bv_dec
let update_vec_dec_maybe w i b = update_mword_dec w i b
let update_vec_dec_fail w i b =
bool_of_bitU_fail b >>= (fun b ->
return (update_mword_bool_dec w i b))
let update_vec_dec_oracle w i b =
bool_of_bitU_oracle b >>= (fun b ->
return (update_mword_bool_dec w i b))
let update_vec_dec w i b = maybe_failwith (update_vec_dec_maybe w i b)
let update_vec_inc_maybe w i b = update_mword_inc w i b
let update_vec_inc_fail w i b =
bool_of_bitU_fail b >>= (fun b ->
return (update_mword_bool_inc w i b))
let update_vec_inc_oracle w i b =
bool_of_bitU_oracle b >>= (fun b ->
return (update_mword_bool_inc w i b))
let update_vec_inc w i b = maybe_failwith (update_vec_inc_maybe w i b)
val subrange_vec_dec : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b
let subrange_vec_dec w i j = Machine_word.word_extract (nat_of_int j) (nat_of_int i) w
val subrange_vec_inc : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b
let subrange_vec_inc w i j = subrange_vec_dec w (length w - 1 - i) (length w - 1 - j)
val update_subrange_vec_dec : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b -> mword 'a
let update_subrange_vec_dec w i j w' = Machine_word.word_update w (nat_of_int j) (nat_of_int i) w'
val update_subrange_vec_inc : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b -> mword 'a
let update_subrange_vec_inc w i j w' = update_subrange_vec_dec w (length w - 1 - i) (length w - 1 - j) w'
val extz_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b
let extz_vec _ w = Machine_word.zeroExtend w
val exts_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b
let exts_vec _ w = Machine_word.signExtend w
val concat_vec : forall 'a 'b 'c. Size 'a, Size 'b, Size 'c => mword 'a -> mword 'b -> mword 'c
let concat_vec = Machine_word.word_concat
val cons_vec_bool : forall 'a 'b 'c. Size 'a, Size 'b => bool -> mword 'a -> mword 'b
let cons_vec_bool b w = wordFromBitlist (b :: bitlistFromWord w)
let cons_vec_maybe b w = Maybe.map (fun b -> cons_vec_bool b w) (bool_of_bitU b)
let cons_vec_fail b w = bool_of_bitU_fail b >>= (fun b -> return (cons_vec_bool b w))
let cons_vec_oracle b w = bool_of_bitU_oracle b >>= (fun b -> return (cons_vec_bool b w))
let cons_vec b w = maybe_failwith (cons_vec_maybe b w)
val vec_of_bool : forall 'a. Size 'a => integer -> bool -> mword 'a
let vec_of_bool _ b = wordFromBitlist [b]
let vec_of_bit_maybe len b = Maybe.map (vec_of_bool len) (bool_of_bitU b)
let vec_of_bit_fail len b = bool_of_bitU_fail b >>= (fun b -> return (vec_of_bool len b))
let vec_of_bit_oracle len b = bool_of_bitU_oracle b >>= (fun b -> return (vec_of_bool len b))
let vec_of_bit len b = maybe_failwith (vec_of_bit_maybe len b)
val cast_bool_vec : bool -> mword ty1
let cast_bool_vec b = vec_of_bool 1 b
let cast_unit_vec_maybe b = vec_of_bit_maybe 1 b
let cast_unit_vec_fail b = bool_of_bitU_fail b >>= (fun b -> return (cast_bool_vec b))
let cast_unit_vec_oracle b = bool_of_bitU_oracle b >>= (fun b -> return (cast_bool_vec b))
let cast_unit_vec b = maybe_failwith (cast_unit_vec_maybe b)
val msb : forall 'a. Size 'a => mword 'a -> bitU
let msb = most_significant
val int_of_vec : forall 'a. Size 'a => bool -> mword 'a -> integer
let int_of_vec sign w =
if sign
then signedIntegerFromWord w
else unsignedIntegerFromWord w
let int_of_vec_maybe sign w = Just (int_of_vec sign w)
let int_of_vec_fail sign w = return (int_of_vec sign w)
val string_of_vec : forall 'a. Size 'a => mword 'a -> string
let string_of_vec = string_of_bv
val and_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
val or_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
val xor_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
val not_vec : forall 'a. Size 'a => mword 'a -> mword 'a
let and_vec = Machine_word.lAnd
let or_vec = Machine_word.lOr
let xor_vec = Machine_word.lXor
let not_vec = Machine_word.lNot
val add_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
val adds_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
val sub_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
val mult_vec : forall 'a 'b. Size 'a, Size 'b => mword 'a -> mword 'a -> mword 'b
val mults_vec : forall 'a 'b. Size 'a, Size 'b => mword 'a -> mword 'a -> mword 'b
let add_vec l r = arith_op_bv integerAdd false l r
let adds_vec l r = arith_op_bv integerAdd true l r
let sub_vec l r = arith_op_bv integerMinus true l r
let mult_vec l r = arith_op_bv integerMult false (zeroExtend l : mword 'b) (zeroExtend r : mword 'b)
let mults_vec l r = arith_op_bv integerMult true (signExtend l : mword 'b) (signExtend r : mword 'b)
val add_vec_int : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
val adds_vec_int : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
val sub_vec_int : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
val mult_vec_int : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
val mults_vec_int : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
let add_vec_int l r = arith_op_bv_int integerAdd false l r
let adds_vec_int l r = arith_op_bv_int integerAdd true l r
let sub_vec_int l r = arith_op_bv_int integerMinus true l r
let mult_vec_int l r = arith_op_bv_int integerMult false (zeroExtend l : mword 'b) r
let mults_vec_int l r = arith_op_bv_int integerMult true (signExtend l : mword 'b) r
val add_int_vec : forall 'a. Size 'a => integer -> mword 'a -> mword 'a
val adds_int_vec : forall 'a. Size 'a => integer -> mword 'a -> mword 'a
val sub_int_vec : forall 'a. Size 'a => integer -> mword 'a -> mword 'a
val mult_int_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b
val mults_int_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b
let add_int_vec l r = arith_op_int_bv integerAdd false l r
let adds_int_vec l r = arith_op_int_bv integerAdd true l r
let sub_int_vec l r = arith_op_int_bv integerMinus true l r
let mult_int_vec l r = arith_op_int_bv integerMult false l (zeroExtend r : mword 'b)
let mults_int_vec l r = arith_op_int_bv integerMult true l (signExtend r : mword 'b)
val add_vec_bool : forall 'a. Size 'a => mword 'a -> bool -> mword 'a
val adds_vec_bool : forall 'a. Size 'a => mword 'a -> bool -> mword 'a
val sub_vec_bool : forall 'a. Size 'a => mword 'a -> bool -> mword 'a
let add_vec_bool l r = arith_op_bv_bool integerAdd false l r
let add_vec_bit_maybe l r = Maybe.map (add_vec_bool l) (bool_of_bitU r)
let add_vec_bit_fail l r = bool_of_bitU_fail r >>= (fun r -> return (add_vec_bool l r))
let add_vec_bit_oracle l r = bool_of_bitU_oracle r >>= (fun r -> return (add_vec_bool l r))
let add_vec_bit l r = maybe_failwith (add_vec_bit_maybe l r)
let adds_vec_bool l r = arith_op_bv_bool integerAdd true l r
let adds_vec_bit_maybe l r = Maybe.map (adds_vec_bool l) (bool_of_bitU r)
let adds_vec_bit_fail l r = bool_of_bitU_fail r >>= (fun r -> return (adds_vec_bool l r))
let adds_vec_bit_oracle l r = bool_of_bitU_oracle r >>= (fun r -> return (adds_vec_bool l r))
let adds_vec_bit l r = maybe_failwith (adds_vec_bit_maybe l r)
let sub_vec_bool l r = arith_op_bv_bool integerMinus true l r
let sub_vec_bit_maybe l r = Maybe.map (sub_vec_bool l) (bool_of_bitU r)
let sub_vec_bit_fail l r = bool_of_bitU_fail r >>= (fun r -> return (sub_vec_bool l r))
let sub_vec_bit_oracle l r = bool_of_bitU_oracle r >>= (fun r -> return (sub_vec_bool l r))
let sub_vec_bit l r = maybe_failwith (sub_vec_bit_maybe l r)
(* TODO
val maybe_mword_of_bits_overflow : forall 'a. Size 'a => (list bitU * bitU * bitU) -> maybe (mword 'a * bitU * bitU)
let maybe_mword_of_bits_overflow (bits, overflow, carry) =
Maybe.map (fun w -> (w, overflow, carry)) (of_bits bits)
val add_overflow_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> maybe (mword 'a * bitU * bitU)
val adds_overflow_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> maybe (mword 'a * bitU * bitU)
val sub_overflow_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> maybe (mword 'a * bitU * bitU)
val subs_overflow_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> maybe (mword 'a * bitU * bitU)
val mult_overflow_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> maybe (mword 'a * bitU * bitU)
val mults_overflow_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> maybe (mword 'a * bitU * bitU)
let add_overflow_vec l r = maybe_mword_of_bits_overflow (add_overflow_bv l r)
let adds_overflow_vec l r = maybe_mword_of_bits_overflow (adds_overflow_bv l r)
let sub_overflow_vec l r = maybe_mword_of_bits_overflow (sub_overflow_bv l r)
let subs_overflow_vec l r = maybe_mword_of_bits_overflow (subs_overflow_bv l r)
let mult_overflow_vec l r = maybe_mword_of_bits_overflow (mult_overflow_bv l r)
let mults_overflow_vec l r = maybe_mword_of_bits_overflow (mults_overflow_bv l r)
val add_overflow_vec_bit : forall 'a. Size 'a => mword 'a -> bitU -> (mword 'a * bitU * bitU)
val add_overflow_vec_bit_signed : forall 'a. Size 'a => mword 'a -> bitU -> (mword 'a * bitU * bitU)
val sub_overflow_vec_bit : forall 'a. Size 'a => mword 'a -> bitU -> (mword 'a * bitU * bitU)
val sub_overflow_vec_bit_signed : forall 'a. Size 'a => mword 'a -> bitU -> (mword 'a * bitU * bitU)
let add_overflow_vec_bit = add_overflow_bv_bit
let add_overflow_vec_bit_signed = add_overflow_bv_bit_signed
let sub_overflow_vec_bit = sub_overflow_bv_bit
let sub_overflow_vec_bit_signed = sub_overflow_bv_bit_signed*)
val shiftl : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
val shiftr : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
val arith_shiftr : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
val rotl : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
val rotr : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
let shiftl = shiftl_mword
let shiftr = shiftr_mword
let arith_shiftr = arith_shiftr_mword
let rotl = rotl_mword
let rotr = rotr_mword
val mod_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
val quot_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
val quots_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
let mod_vec = mod_mword
let quot_vec = quot_mword
let quots_vec = quots_mword
val mod_vec_int : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
val quot_vec_int : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
let mod_vec_int = mod_mword_int
let quot_vec_int = quot_mword_int
val replicate_bits : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
let replicate_bits v count = wordFromBitlist (repeat (bitlistFromWord v) count)
val duplicate_bool : forall 'a. Size 'a => bool -> integer -> mword 'a
let duplicate_bool b n = wordFromBitlist (repeat [b] n)
let duplicate_maybe b n = Maybe.map (fun b -> duplicate_bool b n) (bool_of_bitU b)
let duplicate_fail b n = bool_of_bitU_fail b >>= (fun b -> return (duplicate_bool b n))
let duplicate_oracle b n = bool_of_bitU_oracle b >>= (fun b -> return (duplicate_bool b n))
let duplicate b n = maybe_failwith (duplicate_maybe b n)
val reverse_endianness : forall 'a. Size 'a => mword 'a -> mword 'a
let reverse_endianness v = wordFromBitlist (reverse_endianness_list (bitlistFromWord v))
val eq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
val neq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
val ult_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
val slt_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
val ugt_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
val sgt_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
val ulteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
val slteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
val ugteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
val sgteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
let inline eq_vec = eq_mword
let inline neq_vec = neq_mword
let inline ult_vec = ucmp_mword (<)
let inline slt_vec = scmp_mword (<)
let inline ugt_vec = ucmp_mword (>)
let inline sgt_vec = scmp_mword (>)
let inline ulteq_vec = ucmp_mword (<=)
let inline slteq_vec = scmp_mword (<=)
let inline ugteq_vec = ucmp_mword (>=)
let inline sgteq_vec = scmp_mword (>=)
|
